diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile | 24 | ||||
| -rw-r--r-- | src/ast.ml | 401 | ||||
| -rw-r--r-- | src/lexer.mll | 4 | ||||
| -rw-r--r-- | src/main.ml | 407 | ||||
| -rw-r--r-- | src/parser.mly | 149 | ||||
| -rw-r--r-- | src/process_file.ml | 356 | ||||
| -rw-r--r-- | src/process_file.mli | 91 |
7 files changed, 1184 insertions, 248 deletions
diff --git a/src/Makefile b/src/Makefile new file mode 100644 index 00000000..719e65a7 --- /dev/null +++ b/src/Makefile @@ -0,0 +1,24 @@ +all: + ocamlbuild main.native + +doc: + mkdir -p html-doc + ocamldoc -I _build/ *.mli ulib/*.mli -sort -html -d html-doc + +doc-pdf: + mkdir -p tex-doc + ocamldoc -I _build/ *.mli -latex -sort -d tex-doc -o tex-doc/lem-doc.tex; true + cd tex-doc; pdflatex lem-doc.tex + +doc-dot: + ocamldoc -I _build/ *.ml *.mli ulib/*.ml -dot -sort -d tex-doc -dot-reduce -o dep.dot; true + dot -Tpdf -o dep.pdf dep.dot + +debug: + ocamlbuild main.d.byte + +clean: + -ocamlbuild -clean + -rm -rf _build + -rm -rf html-doc + -rm -rf tex-doc @@ -1,22 +1,24 @@ -(* generated by Ott 0.21.2 from: l2.ott *) +(* generated by Ott 0.22 from: l2.ott *) -type text = Ulib.Text.t +type text = string type l = | Unknown | Trans of string * l option | Range of Lexing.position * Lexing.position +type 'a annot = l * 'a + exception Parse_error_locn of l * string type ml_comment = - | Chars of Ulib.Text.t + | Chars of string | Comment of ml_comment list type lex_skip = | Com of ml_comment - | Ws of Ulib.Text.t + | Ws of string | Nl type lex_skips = lex_skip list option @@ -32,7 +34,7 @@ let pp_lex_skips ppf sk = (* TODO: fix? *) Format.fprintf ppf "(**)" | Ws(r) -> - Format.fprintf ppf "%s" (Ulib.Text.to_string r) + Format.fprintf ppf "%s" r (*(Ulib.Text.to_string r)*) | Nl -> Format.fprintf ppf "\\n") sks @@ -57,19 +59,14 @@ base_kind_aux = (* base kind *) type -id_aux = (* Identifier *) - Id of x - | DeIid of terminal * x * terminal (* remove infix status *) - - -type base_kind = BK_aux of base_kind_aux * l type -id = - Id_aux of id_aux * l +id_aux = (* Identifier *) + Id of x + | DeIid of terminal * x * terminal (* remove infix status *) type @@ -78,15 +75,8 @@ kind_aux = (* kinds *) type -nexp_aux = (* expression of kind $_$, for vector sizes and origins *) - Nexp_id of id (* identifier *) - | Nexp_constant of terminal * int (* constant *) - | Nexp_times of nexp * terminal * nexp (* product *) - | Nexp_sum of nexp * terminal * nexp (* sum *) - | Nexp_exp of terminal * terminal * nexp (* exponential *) - -and nexp = - Nexp_aux of nexp_aux * l +id = + Id_aux of id_aux * l type @@ -106,11 +96,15 @@ kind = type -nexp_constraint_aux = (* constraint over kind $_$ *) - NC_fixed of nexp * terminal * nexp - | NC_bounded_ge of nexp * terminal * nexp - | NC_bounded_le of nexp * terminal * nexp - | NC_nat_set_bounded of id * terminal * terminal * (terminal * int * terminal) list * terminal +nexp_aux = (* expression of kind $_$, for vector sizes and origins *) + Nexp_id of id (* identifier *) + | Nexp_constant of terminal * int (* constant *) + | Nexp_times of nexp * terminal * nexp (* product *) + | Nexp_sum of nexp * terminal * nexp (* sum *) + | Nexp_exp of terminal * terminal * nexp (* exponential *) + +and nexp = + Nexp_aux of nexp_aux * l type @@ -119,14 +113,23 @@ effect = type -kinded_id = (* optionally kind-annotated identifier *) +kinded_id_aux = (* optionally kind-annotated identifier *) KOpt_none of id (* identifier *) | KOpt_kind of kind * id (* kind-annotated variable *) type -nexp_constraint = - NC_aux of nexp_constraint_aux * l +'a nexp_constraint_aux = (* constraint over kind $_$ *) + NC_fixed of nexp * terminal * nexp + | NC_bounded_ge of nexp * terminal * nexp + | NC_bounded_le of nexp * terminal * nexp + | NC_nat_set_bounded of id * terminal * terminal * (terminal * int * terminal) list * terminal + + +type +effects_aux = (* effect set, of kind $_$ *) + Effects_var of id + | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *) type @@ -137,16 +140,18 @@ order_aux = (* vector order specifications, of kind $_$ *) type -effects_aux = (* effect set, of kind $_$ *) - Effects_var of id - | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *) +kinded_id = + KOpt_aux of kinded_id_aux * l type -typquant_aux = (* type quantifiers and constraints *) - TypQ_tq of terminal * (kinded_id) list * terminal * (nexp_constraint * terminal) list * terminal - | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar, omitting constraints *) - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) +'a nexp_constraint = + NC_aux of 'a nexp_constraint_aux * 'a annot + + +type +effects = + Effects_aux of effects_aux * l type @@ -155,246 +160,285 @@ order = type -effects = - Effects_aux of effects_aux * l +'a typquant_aux = (* type quantifiers and constraints *) + TypQ_tq of terminal * (kinded_id) list * terminal * ('a nexp_constraint * terminal) list * terminal + | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar, omitting constraints *) + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) type -typquant = - TypQ_aux of typquant_aux * l +lit_aux = (* Literal constant *) + L_unit of terminal * terminal (* $() : _$ *) + | L_zero of terminal (* $_ : _$ *) + | L_one of terminal (* $_ : _$ *) + | L_true of terminal (* $_ : _$ *) + | L_false of terminal (* $_ : _$ *) + | L_num of terminal * int (* natural number constant *) + | L_hex of terminal * string (* bit vector constant, C-style *) + | L_bin of terminal * string (* bit vector constant, C-style *) + | L_string of terminal * string (* string constant *) type -typ = (* Type expressions, of kind $_$ *) +typ_aux = (* Type expressions, of kind $_$ *) Typ_wild of terminal (* Unspecified type *) | Typ_var of id (* Type variable *) | Typ_fn of typ * terminal * typ * effects (* Function type (first-order only in user code) *) | Typ_tup of (typ * terminal) list (* Tuple type *) | Typ_app of id * (typ_arg) list (* type constructor application *) -and typ_arg = (* Type constructor arguments of all kinds *) +and typ = + Typ_aux of typ_aux * l + +and typ_arg_aux = (* Type constructor arguments of all kinds *) Typ_arg_nexp of nexp | Typ_arg_typ of typ | Typ_arg_order of order | Typ_arg_effects of effects +and typ_arg = + Typ_arg_aux of typ_arg_aux * l + type -typschm_aux = (* type scheme *) - TypSchm_ts of typquant * typ +'a typquant = + TypQ_aux of 'a typquant_aux * 'a annot type -lit = (* Literal constant *) - L_unit of terminal * terminal (* $() : _$ *) - | L_zero of terminal (* $_ : _$ *) - | L_one of terminal (* $_ : _$ *) - | L_true of terminal (* $_ : _$ *) - | L_false of terminal (* $_ : _$ *) - | L_num of terminal * int (* natural number constant *) - | L_hex of terminal * string (* bit vector constant, C-style *) - | L_bin of terminal * string (* bit vector constant, C-style *) - | L_string of terminal * Ulib.UTF8.t (* string constant *) +lit = + L_aux of lit_aux * l type -typschm = - TypSchm_aux of typschm_aux * l +'a typschm_aux = (* type scheme *) + TypSchm_ts of 'a typquant * typ type -pat_aux = (* Pattern *) +'a pat_aux = (* Pattern *) P_lit of lit (* literal constant pattern *) | P_wild of terminal (* wildcard *) - | P_as of terminal * pat * terminal * id * terminal (* named pattern *) - | P_typ of terminal * typ * pat * terminal (* typed pattern *) + | P_as of terminal * 'a pat * terminal * id * terminal (* named pattern *) + | P_typ of terminal * typ * 'a pat * terminal (* typed pattern *) | P_id of id (* identifier *) - | P_app of id * (pat) list (* union constructor pattern *) - | P_record of terminal * (fpat * terminal) list * terminal * bool * terminal (* struct pattern *) - | P_vector of terminal * (pat * terminal) list * terminal (* vector pattern *) - | P_vector_indexed of terminal * ((terminal * int * terminal * pat) * terminal) list * terminal (* vector pattern (with explicit indices) *) - | P_vector_concat of (pat * terminal) list (* concatenated vector pattern *) - | P_tup of terminal * (pat * terminal) list * terminal (* tuple pattern *) - | P_list of terminal * (pat * terminal) list * terminal (* list pattern *) + | P_app of id * ('a pat) list (* union constructor pattern *) + | P_record of terminal * ('a fpat * terminal) list * terminal * bool * terminal (* struct pattern *) + | P_vector of terminal * ('a pat * terminal) list * terminal (* vector pattern *) + | P_vector_indexed of terminal * ((terminal * int * terminal * 'a pat) * terminal) list * terminal (* vector pattern (with explicit indices) *) + | P_vector_concat of ('a pat * terminal) list (* concatenated vector pattern *) + | P_tup of terminal * ('a pat * terminal) list * terminal (* tuple pattern *) + | P_list of terminal * ('a pat * terminal) list * terminal (* list pattern *) + +and 'a pat = + P_aux of 'a pat_aux * 'a annot -and pat = - P_aux of pat_aux * l +and 'a fpat_aux = (* Field pattern *) + FP_Fpat of id * terminal * 'a pat -and fpat_aux = (* Field pattern *) - FP_Fpat of id * terminal * pat +and 'a fpat = + FP_aux of 'a fpat_aux * 'a annot -and fpat = - FP_aux of fpat_aux * l + +type +'a typschm = + TypSchm_aux of 'a typschm_aux * 'a annot type -exp_aux = (* Expression *) - E_block of terminal * (exp * terminal) list * terminal (* block (parsing conflict with structs?) *) +'a letbind = + LB_aux of 'a letbind_aux * 'a annot + +and 'a exp_aux = (* Expression *) + E_block of terminal * ('a exp * terminal) list * terminal (* block (parsing conflict with structs?) *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) - | E_cast of terminal * typ * terminal * exp (* cast *) - | E_app of exp * (exp) list (* function application *) - | E_app_infix of exp * id * exp (* infix function application *) - | E_tuple of terminal * (exp * terminal) list * terminal (* tuple *) - | E_if of terminal * exp * terminal * exp * terminal * exp (* conditional *) - | E_vector of terminal * (exp * terminal) list * terminal (* vector (indexed from 0) *) - | E_vector_indexed of terminal * ((terminal * int * terminal * exp) * terminal) list * terminal (* vector (indexed consecutively) *) - | E_vector_access of exp * terminal * exp * terminal (* vector access *) - | E_vector_subrange of exp * terminal * exp * terminal * exp * terminal (* subvector extraction *) - | E_vector_update of terminal * exp * terminal * exp * terminal * exp * terminal (* vector functional update *) - | E_vector_update_subrange of terminal * exp * terminal * exp * terminal * exp * terminal * exp * terminal (* vector subrange update (with vector) *) - | E_list of terminal * (exp * terminal) list * terminal (* list *) - | E_cons of exp * terminal * exp (* cons *) - | E_record of terminal * fexps * terminal (* struct *) - | E_record_update of terminal * exp * terminal * fexps * terminal (* functional update of struct *) - | E_field of exp * terminal * id (* field projection from struct *) - | E_case of terminal * exp * terminal * ((terminal * pexp)) list * terminal (* pattern matching *) - | E_let of letbind * terminal * exp (* let expression *) - | E_assign of lexp * terminal * exp (* imperative assignment *) - -and exp = - E_aux of exp_aux * l - -and lexp = (* lvalue expression *) + | E_cast of terminal * typ * terminal * 'a exp (* cast *) + | E_app of 'a exp * ('a exp) list (* function application *) + | E_app_infix of 'a exp * id * 'a exp (* infix function application *) + | E_tuple of terminal * ('a exp * terminal) list * terminal (* tuple *) + | E_if of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp (* conditional *) + | E_vector of terminal * ('a exp * terminal) list * terminal (* vector (indexed from 0) *) + | E_vector_indexed of terminal * ((terminal * int * terminal * 'a exp) * terminal) list * terminal (* vector (indexed consecutively) *) + | E_vector_access of 'a exp * terminal * 'a exp * terminal (* vector access *) + | E_vector_subrange of 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector extraction *) + | E_vector_update of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector functional update *) + | E_vector_update_subrange of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector subrange update (with vector) *) + | E_list of terminal * ('a exp * terminal) list * terminal (* list *) + | E_cons of 'a exp * terminal * 'a exp (* cons *) + | E_record of terminal * 'a fexps * terminal (* struct *) + | E_record_update of terminal * 'a exp * terminal * 'a fexps * terminal (* functional update of struct *) + | E_field of 'a exp * terminal * id (* field projection from struct *) + | E_case of terminal * 'a exp * terminal * ((terminal * 'a pexp)) list * terminal (* pattern matching *) + | E_let of 'a letbind * terminal * 'a exp (* let expression *) + | E_assign of 'a lexp * terminal * 'a exp (* imperative assignment *) + +and 'a exp = + E_aux of 'a exp_aux * 'a annot + +and 'a lexp_aux = (* lvalue expression *) LEXP_id of id (* identifier *) - | LEXP_vector of lexp * terminal * exp * terminal (* vector element *) - | LEXP_vector_range of lexp * terminal * exp * terminal * exp * terminal (* subvector *) - | LEXP_field of lexp * terminal * id (* struct field *) + | LEXP_vector of 'a lexp * terminal * 'a exp * terminal (* vector element *) + | LEXP_vector_range of 'a lexp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector *) + | LEXP_field of 'a lexp * terminal * id (* struct field *) + +and 'a lexp = + LEXP_aux of 'a lexp_aux * 'a annot -and fexp_aux = (* Field-expression *) - FE_Fexp of id * terminal * exp +and 'a fexp_aux = (* Field-expression *) + FE_Fexp of id * terminal * 'a exp -and fexp = - FE_aux of fexp_aux * l +and 'a fexp = + FE_aux of 'a fexp_aux * 'a annot -and fexps_aux = (* Field-expression list *) - FES_Fexps of (fexp * terminal) list * terminal * bool +and 'a fexps_aux = (* Field-expression list *) + FES_Fexps of ('a fexp * terminal) list * terminal * bool -and fexps = - FES_aux of fexps_aux * l +and 'a fexps = + FES_aux of 'a fexps_aux * 'a annot + +and 'a pexp_aux = (* Pattern match *) + Pat_exp of 'a pat * terminal * 'a exp + +and 'a pexp = + Pat_aux of 'a pexp_aux * 'a annot + +and 'a letbind_aux = (* Let binding *) + LB_val_explicit of 'a typschm * 'a pat * terminal * 'a exp (* value binding, explicit type ('a pat must be total) *) + | LB_val_implicit of terminal * 'a pat * terminal * 'a exp (* value binding, implicit type ('a pat must be total) *) + + +type +naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of terminal * terminal * terminal * terminal * string * terminal -and pexp_aux = (* Pattern match *) - Pat_exp of pat * terminal * exp -and pexp = - Pat_aux of pexp_aux * l +type +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec of terminal (* recursive *) -and letbind_aux = (* Let binding *) - LB_val_explicit of typschm * pat * terminal * exp (* value binding, explicit type (pat must be total) *) - | LB_val_implicit of terminal * pat * terminal * exp (* value binding, implicit type (pat must be total) *) -and letbind = - LB_aux of letbind_aux * l +type +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * terminal * 'a exp type -funcl_aux = (* Function clause *) - FCL_Funcl of id * pat * terminal * exp +'a tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_none + | Typ_annot_opt_some of terminal * typ type -effects_opt_aux = (* Optional effect annotation for functions *) +'a effects_opt_aux = (* Optional effect annotation for functions *) Effects_opt_pure (* sugar for empty effect set *) | Effects_opt_effects of effects type -funcl = - FCL_aux of funcl_aux * l +index_range_aux = (* index specification, for bitfields in register types *) + BF_single of terminal * int (* single index *) + | BF_range of terminal * int * terminal * terminal * int (* index range *) + | BF_concat of index_range * terminal * index_range (* concatenation of index ranges *) + +and index_range = + BF_aux of index_range_aux * l type -rec_opt = (* Optional recursive annotation for functions *) - Rec_nonrec (* non-recursive *) - | Rec_rec of terminal (* recursive *) +naming_scheme_opt = + Name_sect_aux of naming_scheme_opt_aux * l type -effects_opt = - Effects_opt_aux of effects_opt_aux * l +rec_opt = + Rec_aux of rec_opt_aux * l type -tannot_opt = (* Optional type annotation for functions *) - Typ_annot_opt_none - | Typ_annot_opt_some of terminal * typ +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot type -val_spec_aux = (* Value type specification *) - VS_val_spec of terminal * typschm * id +'a tannot_opt = + Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot type -naming_scheme_opt = (* Optional variable-naming-scheme specification for variables of defined type *) - Name_sect_none - | Name_sect_some of terminal * terminal * terminal * terminal * string * terminal +'a effects_opt = + Effects_opt_aux of 'a effects_opt_aux * 'a annot type -index_range = (* index specification, for bitfields in register types *) - BF_single of terminal * int (* single index *) - | BF_range of terminal * int * terminal * terminal * int (* index range *) - | BF_concat of index_range * terminal * index_range (* concatenation of index ranges *) +'a type_def_aux = (* Type definition body *) + TD_abbrev of terminal * id * naming_scheme_opt * terminal * 'a typschm (* type abbreviation *) + | TD_record of terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* struct type definition *) + | TD_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* union type definition *) + | TD_enum of terminal * id * naming_scheme_opt * terminal * terminal * terminal * (id * terminal) list * terminal * bool * terminal (* enumeration type definition *) + | TD_register of terminal * id * terminal * terminal * terminal * terminal * nexp * terminal * nexp * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type definition *) type -fundef_aux = (* Function definition *) - FD_function of terminal * rec_opt * tannot_opt * effects_opt * (funcl * terminal) list +'a val_spec_aux = (* Value type specification *) + VS_val_spec of terminal * 'a typschm * id type -default_typing_spec_aux = (* Default kinding or typing assumption *) +'a default_typing_spec_aux = (* Default kinding or typing assumption *) DT_kind of terminal * base_kind * id - | DT_typ of terminal * typschm * id + | DT_typ of terminal * 'a typschm * id type -val_spec = - VS_aux of val_spec_aux * l +'a fundef_aux = (* Function definition *) + FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list type -type_def = (* Type definition body *) - TD_abbrev of terminal * id * naming_scheme_opt * terminal * typschm (* type abbreviation *) - | TD_record of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* struct type definition *) - | TD_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* union type definition *) - | TD_enum of terminal * id * naming_scheme_opt * terminal * terminal * terminal * (id * terminal) list * terminal * bool * terminal (* enumeration type definition *) - | TD_register of terminal * id * terminal * terminal * terminal * terminal * nexp * terminal * nexp * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type definition *) +'a type_def = + TD_aux of 'a type_def_aux * 'a annot + + +type +'a val_spec = + VS_aux of 'a val_spec_aux * 'a annot type -fundef = - FD_aux of fundef_aux * l +'a default_typing_spec = + DT_aux of 'a default_typing_spec_aux * 'a annot type -default_typing_spec = - DT_aux of default_typing_spec_aux * l +'a fundef = + FD_aux of 'a fundef_aux * 'a annot type -def_aux = (* Top-level definition *) - DEF_type of type_def (* type definition *) - | DEF_fundef of fundef (* function definition *) - | DEF_val of letbind (* value definition *) - | DEF_spec of val_spec (* top-level type constraint *) - | DEF_default of default_typing_spec (* default kind and type assumptions *) +'a def_aux = (* Top-level definition *) + DEF_type of 'a type_def (* type definition *) + | DEF_fundef of 'a fundef (* function definition *) + | DEF_val of 'a letbind (* value definition *) + | DEF_spec of 'a val_spec (* top-level type constraint *) + | DEF_default of 'a default_typing_spec (* default kind and type assumptions *) | DEF_reg_dec of terminal * typ * id (* register declaration *) - | DEF_scattered_function of terminal * terminal * rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *) - | DEF_scattered_funcl of terminal * terminal * funcl (* scattered function definition clause *) - | DEF_scattered_variant of terminal * terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant (* scattered union definition header *) + | DEF_scattered_function of terminal * terminal * rec_opt * 'a tannot_opt * 'a effects_opt * id (* scattered function definition header *) + | DEF_scattered_funcl of terminal * terminal * 'a funcl (* scattered function definition clause *) + | DEF_scattered_variant of terminal * terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant (* scattered union definition header *) | DEF_scattered_unioncl of terminal * id * terminal * typ * id (* scattered union definition member *) | DEF_scattered_end of terminal * id (* scattered definition end *) type -typ_lib_aux = (* library types and syntactic sugar for them *) +'a typ_lib_aux = (* library types and syntactic sugar for them *) Typ_lib_unit of terminal (* unit type with value $()$ *) | Typ_lib_bool of terminal (* booleans $_$ and $_$ *) | Typ_lib_bit of terminal (* pure bit values (not mutable bits) *) | Typ_lib_nat of terminal (* natural numbers 0,1,2,... *) - | Typ_lib_string of terminal * Ulib.UTF8.t (* UTF8 strings *) + | Typ_lib_string of terminal * string (* UTF8 strings *) | Typ_lib_enum of terminal * nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *) | Typ_lib_enum1 of terminal * nexp * terminal (* sugar for \texttt{enum nexp 0 inc} *) | Typ_lib_enum2 of terminal * nexp * terminal * nexp * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) @@ -407,23 +451,28 @@ typ_lib_aux = (* library types and syntactic sugar for them *) type -def = - DEF_aux of def_aux * l +'a ctor_def_aux = (* Datatype constructor definition clause *) + CT_ct of id * terminal * 'a typschm + + +type +'a def = + DEF_aux of 'a def_aux * 'a annot type -ctor_def = (* Datatype constructor definition clause *) - CT_ct of id * terminal * typschm +'a typ_lib = + Typ_lib_aux of 'a typ_lib_aux * l type -typ_lib = - Typ_lib_aux of typ_lib_aux * l +'a ctor_def = + CT_aux of 'a ctor_def_aux * 'a annot type -defs = (* Definition sequence *) - Defs of (def) list +'a defs = (* Definition sequence *) + Defs of ('a def) list diff --git a/src/lexer.mll b/src/lexer.mll index d6a47d5e..6c2fac21 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -129,7 +129,7 @@ rule token skips = parse | ":" { (Colon(Some(skips))) } | "," { (Comma(Some(skips))) } | "." { (Dot(Some(skips))) } - | "\" { (Div(Some(skips),r"\")) } + | "/" { (Div(Some(skips),r"/")) } | "=" { (Eq(Some(skips),r"=")) } | "!" { (Excl(Some(skips),r"!")) } | ">" { (Gt(Some(skips),r">")) } @@ -152,7 +152,7 @@ rule token skips = parse | "|]" { (BarSquare(Some(skips))) } | "^^" { (CarrotCarrot(Some(skips),r"^^")) } | "::" as i { (ColonColon(Some(skips),Ulib.Text.of_latin1 i)) } - | ".." { (DotDot(Some(skips)) } + | ".." { (DotDot(Some(skips))) } | "=/=" { (EqDivEq(Some(skips),r"=/=")) } | "==" { (EqEq(Some(skips),r"==")) } | "!=" { (ExclEq(Some(skips),r"!=")) } diff --git a/src/main.ml b/src/main.ml new file mode 100644 index 00000000..2f256cb2 --- /dev/null +++ b/src/main.ml @@ -0,0 +1,407 @@ +(**************************************************************************) +(* Lem *) +(* *) +(* Dominic Mulligan, University of Cambridge *) +(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) +(* Gabriel Kerneis, University of Cambridge *) +(* Kathy Gray, University of Cambridge *) +(* Peter Boehm, University of Cambridge (while working on Lem) *) +(* Peter Sewell, University of Cambridge *) +(* Scott Owens, University of Kent *) +(* Thomas Tuerk, University of Cambridge *) +(* *) +(* The Lem sources are copyright 2010-2013 *) +(* by the UK authors above and Institut National de Recherche en *) +(* Informatique et en Automatique (INRIA). *) +(* *) +(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) +(* are distributed under the license below. The former are distributed *) +(* under the LGPLv2, as in the LICENSE file. *) +(* *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* 3. The names of the authors may not be used to endorse or promote *) +(* products derived from this software without specific prior written *) +(* permission. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) +(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) +(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) +(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) +(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) +(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) +(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) +(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) +(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) +(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) +(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(**************************************************************************) + +open Process_file +(*open Debug + +let backends = ref [] +let opt_print_types = ref false +let opt_print_version = ref false +let opt_library = ref (Some (Build_directory.d^"/library")) +let lib = ref [] +let ocaml_lib = ref [] +let hol_lib = ref [] +let coq_lib = ref [] +let isa_lib = ref [] +let isa_theory = ref None +let opt_file_arguments = ref ([]:string list) + +let options = Arg.align ([ + ( "-i", + Arg.String (fun l -> lib := l::!lib), + " treat the file as input only and generate no output for it"); + ( "-tex", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_tex)) !backends) then + backends := Some(Typed_ast.Target_tex)::!backends), + " generate LaTeX"); + ( "-html", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_html)) !backends) then + backends := Some(Typed_ast.Target_html)::!backends), + " generate Html"); + ( "-hol", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_hol)) !backends) then + backends := Some(Typed_ast.Target_hol)::!backends), + " generate HOL"); + ( "-ocaml", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_ocaml)) !backends) then + backends := Some(Typed_ast.Target_ocaml)::!backends), + " generate OCaml"); + ( "-isa", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_isa)) !backends) then + backends := Some(Typed_ast.Target_isa)::!backends), + " generate Isabelle"); + ( "-coq", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_coq)) !backends) then + backends := Some(Typed_ast.Target_coq)::!backends), + " generate Coq"); + ( "-ident", + Arg.Unit (fun b -> if not (List.mem None !backends) then + backends := None::!backends), + " generate input on stdout"); + ( "-print_types", + Arg.Unit (fun b -> opt_print_types := true), + " print types on stdout"); + ( "-lib", + Arg.String (fun l -> opt_library := Some l), + " library path"^match !opt_library with None->"" | Some s -> " (default "^s^")"); + ( "-ocaml_lib", + Arg.String (fun l -> ocaml_lib := l::!ocaml_lib), + " add to OCaml library"); + ( "-hol_lib", + Arg.String (fun l -> hol_lib := l::!hol_lib), + " add to HOL library"); + ( "-isa_lib", + Arg.String (fun l -> isa_lib := l::!isa_lib), + " add to Isabelle library"); + ( "-isa_theory", + Arg.String (fun l -> isa_theory := Some l), + " Isabelle Lem theory"); + ( "-coq_lib", + Arg.String (fun l -> coq_lib := l::!coq_lib), + " add to Coq library"); + ( "-v", + Arg.Unit (fun b -> opt_print_version := true), + " print version"); + ( "-ident_pat_compile", + Arg.Unit (fun b -> Target_trans.ident_force_pattern_compile := true; Reporting.ignore_pat_compile_warnings()), + " activates pattern compilation for the identity backend. This is used for debugging."); + ( "-only_changed_output", + Arg.Unit (fun b -> Process_file.always_replace_files := false), + " generate only output files, whose content really changed compared to the existing file"); + ( "-extra_level", + Arg.Symbol (["none"; "auto"; "all"], (fun s -> + Backend.gen_extra_level := (match s with + | "none" -> 0 + | "auto" -> 1 + | _ -> 2))), + " generate no (none) extra-information, only extras that can be handled automatically (auto) or all (all) extra information") +] @ Reporting.warn_opts) + +let usage_msg = + ("Lem " ^ Version.v ^ "\n" + ^ "example usage: lem -hol -ocaml -lib ../lem/library test.lem\n" + ) + +let _ = + Arg.parse options + (fun s -> + opt_file_arguments := (!opt_file_arguments) @ [s]) + usage_msg + + +let check_modules (def_info,env) modules = + (* The checks. Modify these lists to add more. *) + let exp_checks env = [Patterns.check_match_exp_warn env] in + let pat_checks env = [] in + let def_checks env = [Patterns.check_match_def_warn env] in + + (* Use the Macro_expander to execute these checks *) + let (d,_) = def_info in + let module Ctxt = struct let avoid = None let check = Some(d) end in + let module M = Macro_expander.Expander(Ctxt) in + let exp_mac env = Macro_expander.list_to_mac (List.map (fun f e -> (let _ = f e in None)) (exp_checks env)) in + let exp_ty env ty = ty in + let exp_src_ty env src_t = src_t in + let exp_pat env = Macro_expander.list_to_bool_mac (List.map (fun f x p -> (let _ = f x p in None)) (pat_checks env)) in + let check_defs env defs = begin + let _ = M.expand_defs (List.rev defs) (exp_mac env, exp_ty env, exp_src_ty env, exp_pat env) in + let _ = List.map (fun d -> List.map (fun c -> c d) (def_checks env)) defs in + () + end in + let check_module m = (let (defs, _) = m.Typed_ast.typed_ast in check_defs env defs) in + let _ = List.map check_module modules in + () + + +(* Do the transformations for a given target, and then generate the output files + * *) +let per_target libpath isa_thy modules (def_info,env) consts alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum targ = + let consts = List.assoc targ consts in + let module C = struct + let (d,i) = def_info + end + in + let module T = Target_trans.Make(C) in + let (trans,avoid) = T.get_transformation targ consts in + try + let (_,transformed_m) = + List.fold_left + (fun (env,new_mods) old_mod -> + let (env,m) = trans env old_mod in + (env,m::new_mods)) + (env,[]) + modules + in + let consts' = T.extend_consts targ consts transformed_m in + let transformed_m' = T.rename_def_params targ consts' transformed_m in + output libpath isa_thy targ (avoid consts') def_info (List.rev transformed_m') alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum + with + | Trans.Trans_error(l,msg) -> + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_trans (l, msg))) + | Ident.No_type(l,msg) -> + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_internal (l, msg))) + | Typed_ast.Renaming_error(ls,msg) -> + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_rename (ls, msg))) + + +let main () = + let _ = if !opt_print_version then print_string ("Lem " ^ Version.v ^ "\n") in + let lib_path = + match !opt_library with + | None -> (try + let lp = Sys.getenv("LEMLIB") in + if Filename.is_relative lp + then Filename.concat (Sys.getcwd ()) lp + else lp + with + | Not_found -> raise (Failure("must specify a -lib argument or have a LEMLIB environment variable"))) + | Some lp -> + if Filename.is_relative lp then + Filename.concat (Sys.getcwd ()) lp + else + lp + in + let isa_thy = + match !isa_theory with + | None -> Filename.concat lib_path "../isabelle-lib/Lem" + | Some thy -> thy + in + let _ = + List.iter + (fun f -> + try + if String.compare ".lem" (String.sub f (String.length f - 4) 4) <> 0 then + raise (Failure("Files must have .lem extension")) + with + | Invalid_argument _ -> + raise (Failure("Files must have .lem extension"))) + (!opt_file_arguments @ !lib @ !ocaml_lib @ !hol_lib @ !isa_lib @ !coq_lib) + in + let _ = + List.iter + (fun f -> + if not (Str.string_match (Str.regexp "[A-Za-z]") (Filename.basename f) 0) then + raise (Failure(".lem filenames must start with a letter"))) + (!opt_file_arguments @ !lib @ !ocaml_lib @ !hol_lib @ !isa_lib @ !coq_lib) + in + let init = + try + let inchannel = open_in (Filename.concat lib_path "lib_cache") in + let v = input_value inchannel in + close_in inchannel; + v + with + | Sys_error _ -> + let module I = Initial_env.Initial_libs(struct let path = lib_path end) in + let outchannel = open_out (Filename.concat lib_path "lib_cache") in + output_value outchannel I.init; + close_out outchannel; + I.init + in + (* TODO: These should go into the sets of top-level constant names *) + let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_hol) !hol_lib init in + let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_ocaml) !ocaml_lib init in + let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_isa) !isa_lib init in + let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_coq) !coq_lib init in + + let consts = + List.map + (fun (targ,cL) -> + let consts = List.fold_left + (fun s c -> Typed_ast.NameSet.add (Name.from_rope c) s) + Typed_ast.NameSet.empty + cL in + (targ,consts)) + (snd init) + in + let type_info : (Types.type_defs * instances) * Typed_ast.env = fst init in + (* Parse and typecheck all of the .lem sources *) + let (modules, type_info, _) = + List.fold_left + (fun (mods, (def_info,env), previously_processed_modules) (f, add_to_modules) -> + let ast = parse_file f in + let f' = Filename.basename (Filename.chop_extension f) in + let mod_name = String.capitalize f' in + let mod_name_name = Name.from_rope (Ulib.Text.of_latin1 mod_name) in + let backend_set = + List.fold_right + (fun x s -> + match x with + | None -> s + | Some(Typed_ast.Target_tex) -> s + | Some(Typed_ast.Target_html) -> s + | Some(t) -> Typed_ast.Targetset.add t s) + !backends + Typed_ast.Targetset.empty + in + let ((tdefs,instances,new_instances),new_env,tast) = + check_ast backend_set [mod_name_name] (def_info,env) ast + in + let md = { Typed_ast.mod_env = new_env; Typed_ast.mod_binding = Path.mk_path [] mod_name_name } in + let e = { env with Typed_ast.m_env = Typed_ast.Nfmap.insert env.Typed_ast.m_env (mod_name_name,md) } in + let module_record = + { Typed_ast.filename = f; + Typed_ast.module_name = mod_name; + Typed_ast.predecessor_modules = previously_processed_modules; + Typed_ast.untyped_ast = ast; + Typed_ast.typed_ast = tast; } + in + if !opt_print_types then + begin + (* + Format.fprintf Format.std_formatter "%s@\nlibrary:@\n" f; + Typed_ast.pp_env Format.std_formatter (snd type_info); + *) + Format.fprintf Format.std_formatter "%s@\nenvironment:@\n" f; + Typed_ast.pp_env Format.std_formatter new_env; + Format.fprintf Format.std_formatter "@\ninstances:@\n"; + Typed_ast.pp_instances Format.std_formatter new_instances; + Format.fprintf Format.std_formatter "@\n@\n" + end; + ((if add_to_modules then + module_record::mods + else + mods), + ((tdefs,instances),e), mod_name::previously_processed_modules)) + ([],type_info,[]) + (* We don't want to add the files in !lib to the resulting module ASTs, + * because we don't want to put them throught the back end *) + (List.map (fun x -> (x, false)) (List.rev !lib) @ + List.map (fun x -> (x, true)) !opt_file_arguments) + in + + (* Check the parsed source and produce warnings for various things. Currently: + - non-exhaustive and redundant patterns + *) + let _ = check_modules type_info modules in + + let alldoc_accum = ref ([] : Ulib.Text.t list) in + let alldoc_inc_accum = ref ([] : Ulib.Text.t list) in + let alldoc_inc_usage_accum = ref ([] : Ulib.Text.t list) in + ignore (List.iter (per_target lib_path isa_thy (List.rev modules) type_info consts alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum) !backends); + (if List.mem (Some(Typed_ast.Target_tex)) !backends then + output_alldoc "alldoc" (String.concat " " !opt_file_arguments) alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum) + +let _ = + try + begin + try ignore(main ()) + with Failure(s) -> raise (Reporting_basic.err_general false Ast.Unknown ("Failure "^s)) + end + with Reporting_basic.Fatal_error e -> Reporting_basic.report_error e + +*) + +let lib = ref [] +let opt_print_version = ref false +let opt_file_arguments = ref ([]:string list) +let options = Arg.align ([ + ( "-i", + Arg.String (fun l -> lib := l::!lib), + " treat the file as input only and generate no output for it"); + (*( "-tex", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_tex)) !backends) then + backends := Some(Typed_ast.Target_tex)::!backends), + " generate LaTeX"); + ( "-html", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_html)) !backends) then + backends := Some(Typed_ast.Target_html)::!backends), + " generate Html"); + ( "-hol", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_hol)) !backends) then + backends := Some(Typed_ast.Target_hol)::!backends), + " generate HOL"); + ( "-ocaml", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_ocaml)) !backends) then + backends := Some(Typed_ast.Target_ocaml)::!backends), + " generate OCaml"); + ( "-isa", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_isa)) !backends) then + backends := Some(Typed_ast.Target_isa)::!backends), + " generate Isabelle"); + ( "-coq", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_coq)) !backends) then + backends := Some(Typed_ast.Target_coq)::!backends), + " generate Coq"); + ( "-ident", + Arg.Unit (fun b -> if not (List.mem None !backends) then + backends := None::!backends), + " generate input on stdout");*) +(* ( "-print_types", + Arg.Unit (fun b -> opt_print_types := true), + " print types on stdout");*) + ( "-v", + Arg.Unit (fun b -> opt_print_version := true), + " print version"); +] ) + +let usage_msg = + ("L2 " ^ "pre alpha" ^ "\n" + ^ "example usage: l2 test.ltwo\n" + ) + +let _ = + Arg.parse options + (fun s -> + opt_file_arguments := (!opt_file_arguments) @ [s]) + usage_msg + +let main() = + if !(opt_print_version) + then Printf.printf "L2 pre alpha \n" + else ignore(List.map (fun f -> (parse_file f)) !opt_file_arguments) + +let _ = main() diff --git a/src/parser.mly b/src/parser.mly index fe944b1c..dc024970 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -45,9 +45,8 @@ /**************************************************************************/ %{ -(* - *) -let r = Ulib.Text.of_latin1 + +let r = fun x -> x (* Ulib.Text.of_latin1 *) open Ast @@ -61,6 +60,10 @@ let ploc p = Pat_l(p,loc ()) let eloc e = Expr_l(e,loc ()) let lbloc lb = Letbind(lb,loc ()) +let bkloc k = BK_aux(k,loc ()) +let kloc k = K_aux(k,loc ()) +let nloc n = Nexp_aux(k,loc ()) + let dloc d = DEF_aux(d,loc ()) let pat_to_let p = @@ -77,23 +80,9 @@ let pat_to_letfun p = | Pat_l(_,l) -> raise (Parse_error_locn(l,"Bad pattern for let binding of a function")) -let get_target (s1,n) = - if Ulib.Text.compare n (r"hol") = 0 then - Target_hol(s1) - else if Ulib.Text.compare n (r"ocaml") = 0 then - Target_ocaml(s1) - else if Ulib.Text.compare n (r"coq") = 0 then - Target_coq(s1) - else if Ulib.Text.compare n (r"isabelle") = 0 then - Target_isa(s1) - else if Ulib.Text.compare n (r"tex") = 0 then - Target_tex(s1) - else - raise (Parse_error_locn(loc (),"Expected substitution target in {hol; isabelle; ocaml; coq; tex}, given " ^ Ulib.Text.to_string n)) - let build_fexp (Expr_l(e,_)) l = match e with - | Infix(Expr_l(Ident(i), l'),SymX_l((stx,op),l''),e2) when Ulib.Text.compare op (r"=") = 0 -> + | Infix(Expr_l(Ident(i), l'),SymX_l((stx,op),l''),e2) when String.compare op (r"=") = 0 -> Fexp(i, stx, e2, l) | _ -> raise (Parse_error_locn(l,"Invalid record field assignment (should be id = exp)")) @@ -104,10 +93,10 @@ let mod_cap n = else () -let space = Ulib.Text.of_latin1 " " -let star = Ulib.Text.of_latin1 "*" +let space = " " +let star = "*" -let mk_pre_x_l sk1 (sk2,id) sk3 l = +(*let mk_pre_x_l sk1 (sk2,id) sk3 l = if (sk2 = None || sk2 = Some []) && (sk3 = None || sk3 = Some []) then PreX_l(sk1,(None,id),None,l) else if (sk2 = Some [Ws space] && @@ -116,17 +105,15 @@ let mk_pre_x_l sk1 (sk2,id) sk3 l = Ulib.Text.right id 1 = star)) then PreX_l(sk1,(None,id),None,l) else - raise (Parse_error_locn(l, "illegal whitespace in parenthesised infix name")) + raise (Parse_error_locn(l, "illegal whitespace in parenthesised infix name"))*) %} -%{ -(*Terminals with no content*) -}% +/*Terminals with no content*/ %token <Ast.terminal> And As Case Clause Const Default Effects End Enum Else False Forall -%token <Ast.terminal> Function_ If_ In IN Let_ Member Nat Order Rec Register Scattered +%token <Ast.terminal> Function_ If_ In IN Let_ Member Nat Order Pure Rec Register Scattered %token <Ast.terminal> Struct Switch Then True Type TYPE Typedef Union With Val %token <Ast.terminal> AND Div_ EOR Mod OR Quot Rem @@ -135,33 +122,31 @@ let mk_pre_x_l sk1 (sk2,id) sk3 l = %token <Ast.terminal> Lcurly Rcurly Lparen Rparen Lsquare Rsquare %token <Ast.terminal> BarBar BarGt BarSquare DotDot MinusGt LtBar SquareBar -%{ -(*Terminals with content*) -}% +/*Terminals with content*/ -%token <Ast.terminal * Ulib.Text.t> Id +%token <Ast.terminal * string> Id %token <Ast.terminal * int> Num %token <Ast.terminal * string> String Bin Hex -%token <Ast.terminal * Ulib.Text.t> Amp At Carrot Div Eq Excl Gt Lt Plus Star Tilde -%token <Ast.terminal * Ulib.Text.t> AmpAmp CarrotCarrot ColonColon EqDivEq EqEq ExclEq ExclExcl -%token <Ast.terminal * Ulib.Text.t> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt -%token <Ast.terminal * Ulib.Text.t> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar TildeCarrot +%token <Ast.terminal * string> Amp At Carrot Div Eq Excl Gt Lt Plus Star Tilde +%token <Ast.terminal * string> AmpAmp CarrotCarrot ColonColon EqDivEq EqEq ExclEq ExclExcl +%token <Ast.terminal * string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt +%token <Ast.terminal * string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar TildeCarrot -%token <Ast.terminal * Ulib.Text.t> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS -%token <Ast.terminal * Ulib.Text.t> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU -%token <Ast.terminal * Ulib.Text.t> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarUnderS -%token <Ast.terminal * Ulib.Text.t> StarUnderSi StarUnderU StarUnderUi TwoCarrot +%token <Ast.terminal * string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS +%token <Ast.terminal * string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU +%token <Ast.terminal * string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarUnderS +%token <Ast.terminal * string> StarUnderSi StarUnderU StarUnderUi TwoCarrot -%token <Ast.terminal * Ulib.Text.t> AmpI AtI CarrotI DivI EqI ExclI GtI LtI PlusI StarI TildeI -%token <Ast.terminal * Ulib.Text.t> AmpAmpI CarrotCarrotI ColonColonI EqDivEqI EqEqI ExclEqI ExclExclI -%token <Ast.terminal * Ulib.Text.t> GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI -%token <Ast.terminal * Ulib.Text.t> LtEqI LtEqPlusI LtGtI LtLtI LtLtLtI LtPlusI StarStarI TildeCarrotI +%token <Ast.terminal * string> AmpI AtI CarrotI DivI EqI ExclI GtI LtI PlusI StarI TildeI +%token <Ast.terminal * string> AmpAmpI CarrotCarrotI ColonColonI EqDivEqI EqEqI ExclEqI ExclExclI +%token <Ast.terminal * string> GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI +%token <Ast.terminal * string> LtEqI LtEqPlusI LtGtI LtLtI LtLtLtI LtPlusI StarStarI TildeCarrotI -%token <Ast.terminal * Ulib.Text.t> GtEqUnderSI GtEqUnderSiI GtEqUnderUI GtEqUnderUiI GtGtUnderUI GtUnderSI -%token <Ast.terminal * Ulib.Text.t> GtUnderSiI GtUnderUI GtUnderUiI LtEqUnderSI LtEqUnderSiI LtEqUnderUI -%token <Ast.terminal * Ulib.Text.t> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarUnderSI -%token <Ast.terminal * Ulib.Text.t> StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI +%token <Ast.terminal * string> GtEqUnderSI GtEqUnderSiI GtEqUnderUI GtEqUnderUiI GtGtUnderUI GtUnderSI +%token <Ast.terminal * string> GtUnderSiI GtUnderUI GtUnderUiI LtEqUnderSI LtEqUnderSiI LtEqUnderUI +%token <Ast.terminal * string> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarUnderSI +%token <Ast.terminal * string> StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI %start file %type <Ast.defs> defs @@ -174,7 +159,7 @@ let mk_pre_x_l sk1 (sk2,id) sk3 l = %% id: - | X + | Id { X_l($1, loc ()) } | Lparen Eq Rparen { mk_pre_x_l $1 $2 $3 (loc ()) } @@ -212,15 +197,58 @@ id: { mk_pre_x_l $1 $2 $3 (loc ()) } atomic_kind: - | + | TYPE + { bkloc (BK_type($1)) } + | Nat + { bkloc (BK_nat($1)) } + | Order + { bkloc (BK_order($1)) } + | Effects + { bkloc (BK_effects($1)) } + +kind: + | atomic_kind + { [ ($1,None) ] } + | atomic_kind MinusGt kind + { ($1,$2)::$3 } + +atomic_nexp_no_id: + | Num + { nloc (Nexp_constant(fst $1, snd$1)) } + | Lparen nexp Rparen + { $2 } + +atomic_nexp: + | id + { nloc (Nexp_var (fst $1, snd $1)) } + | atomic_nexp_no_id + { $1 } + +star_nexp: + | atomic_nexp + { $1 } + | atomic_nexp Star star_nexp + { nloc (Nexp_times($1, fst $2, $3)) } + +exp_nexp: + | star_nexp + { $1 } + | Num StarStar nexp + { if (2 = (fst $1)) + then nloc (Nexp_exp((fst $1,snd $1),$2,$3)) + else Parse_error_locn(loc (), "Only 2 is a valid exponent base in Nats") } + +nexp: + | exp_nexp + { $1 } + | exp_nexp Plus nexp + { nloc (Nexp_sum($1,fst $2,$3)) } atomic_typ: | Under { tloc (Typ_wild($1)) } - | Tyvar - { tloc (Typ_var(A_l((fst $1, snd $1), loc()))) } | id - { tloc (Typ_app($1,[])) } + { tloc (Typ_var(A_l((fst $1, snd $1), loc()))) } | Lparen typ Rparen { tloc (Typ_paren($1,$2,$3)) } @@ -262,25 +290,6 @@ typ: | star_typ Arrow typ { tloc (Typ_fn($1,$2,$3)) } -atomic_nexp: - | Nvar - { nloc (Nexp_var (fst $1, snd $1)) } - | Num - { nloc (Nexp_constant(fst $1, snd $1)) } - | Lparen nexp Rparen - { nloc (Nexp_paren($1,$2,$3)) } - -star_nexp: - | atomic_nexp - { $1 } - | atomic_nexp Star star_nexp - { nloc (Nexp_times($1, fst $2, $3)) } - -nexp: - | star_nexp - { $1 } - | star_nexp Plus nexp - { nloc (Nexp_sum($1,fst $2,$3)) } lit: | True diff --git a/src/process_file.ml b/src/process_file.ml new file mode 100644 index 00000000..5c7e4680 --- /dev/null +++ b/src/process_file.ml @@ -0,0 +1,356 @@ +(**************************************************************************) +(* Lem *) +(* *) +(* Dominic Mulligan, University of Cambridge *) +(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) +(* Gabriel Kerneis, University of Cambridge *) +(* Kathy Gray, University of Cambridge *) +(* Peter Boehm, University of Cambridge (while working on Lem) *) +(* Peter Sewell, University of Cambridge *) +(* Scott Owens, University of Kent *) +(* Thomas Tuerk, University of Cambridge *) +(* *) +(* The Lem sources are copyright 2010-2013 *) +(* by the UK authors above and Institut National de Recherche en *) +(* Informatique et en Automatique (INRIA). *) +(* *) +(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) +(* are distributed under the license below. The former are distributed *) +(* under the LGPLv2, as in the LICENSE file. *) +(* *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* 3. The names of the authors may not be used to endorse or promote *) +(* products derived from this software without specific prior written *) +(* permission. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) +(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) +(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) +(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) +(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) +(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) +(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) +(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) +(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) +(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) +(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(**************************************************************************) + +(* XXX: for debugging the developing code: open Coq_ast *) + +(* let r = Ulib.Text.of_latin1 *) + +let get_lexbuf fn = + let lexbuf = Lexing.from_channel (open_in fn) in + lexbuf.Lexing.lex_curr_p <- { Lexing.pos_fname = fn; + Lexing.pos_lnum = 1; + Lexing.pos_bol = 0; + Lexing.pos_cnum = 0; }; + lexbuf + +let parse_file (f : string) : (bool Ast.defs * Ast.lex_skips) = + let lexbuf = get_lexbuf f in + try + Parser.file (Lexer.token []) lexbuf + with + | Parsing.Parse_error -> + let pos = Lexing.lexeme_start_p lexbuf in + raise "Parse error" (* (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "")))*) + | Ast.Parse_error_locn(l,m) -> + raise "Parse error 2" (*Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))*) + | Lexer.LexError(c,p) -> + raise "Lex error" (*Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, c))*) + +(* type instances = Types.instance list Types.Pfmap.t + +let check_ast (ts : Typed_ast.Targetset.t) (mod_path : Name.t list) + ((tdefs,env) : ((Types.type_defs * instances) * Typed_ast.env)) + (ast, end_lex_skips) + : (Types.type_defs * instances * instances) * Typed_ast.env * (Typed_ast.def list * Ast.lex_skips) = + try + let (defs,env,tast) = + Typecheck.check_defs ts mod_path tdefs env ast + in + (defs,env,(tast,end_lex_skips)) + with + | Ident.No_type(l,m) -> + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_type (l, m))) + +let check_ast_as_module (ts : Typed_ast.Targetset.t) (mod_path : Name.t list) + (e : ((Types.type_defs * instances) * Typed_ast.env)) + (mod_name : Ulib.Text.t) (ast, end_lex_skips) + : (Types.type_defs * instances * instances) * Typed_ast.env * (Typed_ast.def list * Ast.lex_skips) = + check_ast ts mod_path e + (Ast.Defs([(Ast.Def_l(Ast.Module(None, Ast.X_l((None,mod_name),Ast.Unknown), None, None, ast, None), Ast.Unknown), + None, + false)]), end_lex_skips) + + +let open_output_with_check file_name = + let (temp_file_name, o) = Filename.open_temp_file "lem_temp" "" in + (o, (o, temp_file_name, file_name)) + +let always_replace_files = ref true + +let close_output_with_check (o, temp_file_name, file_name) = + let _ = close_out o in + let do_replace = !always_replace_files || (not (Util.same_content_files temp_file_name file_name)) in + let _ = if (not do_replace) then Sys.remove temp_file_name + else Util.move_file temp_file_name file_name in + () + +let generated_line f = + Printf.sprintf "Generated by Lem from %s." f + +let tex_preamble = + "\\documentclass{article}\n" ^ + "\\usepackage{amsmath,amssymb}\n" ^ + "\\usepackage{color}\n" ^ + "\\usepackage{geometry}\n" ^ + "\\usepackage{alltt}\n" ^ + "\\usepackage{lem}\n" ^ + "\\geometry{a4paper,dvips,twoside,left=22.5mm,right=22.5mm,top=20mm,bottom=30mm}\n" ^ + "\\begin{document}\n"^ + "\\tableofcontents\n\\newpage\n" + +let tex_postamble = + "\\end{document}\n" + +(* TODO: make this not cppmem-specific *) +let html_preamble = +"\n" ^ +"<?xml version=\"1.0\" encoding=\"utf-8\"?>\n" ^ +"<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.1//EN\"\n" ^ +" \"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd\">\n" ^ +"<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^ +" <head>\n" ^ +" <meta http-equiv=\"Content-Type\" content=\"text/html; charset=UTF-8\"/> \n" ^ +" <title>C/C++ memory model definitions</title>\n" ^ +" <link rel=\"stylesheet\" type=\"text/css\" title=\"cppmem style\" media=\"screen\" href=\"cppmem.css\"/>\n" ^ +" </head>\n" ^ +" <body>\n" ^ +" <h1 id=\"title\">C/C++ memory model definitions</h1>\n" ^ +"<pre>\n" + +let html_postamble = +"\n" ^ +"</pre>\n" ^ +" </body>\n" ^ +"</html>\n" + +let output1 libpath isa_thy targ avoid type_info m alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum = + let module C = struct + let avoid = avoid + end + in + let module B = Backend.Make(C) in + let open Typed_ast in + let f' = Filename.basename (Filename.chop_extension m.filename) in + match targ with + | None -> + let r = B.ident_defs m.typed_ast in + Printf.printf "%s" (Ulib.Text.to_string r) + | Some(Typed_ast.Target_html) -> + begin + let r = B.html_defs m.typed_ast in + let (o, ext_o) = open_output_with_check (f' ^ ".html") in + Printf.fprintf o "<!-- %s -->\n" (generated_line m.filename); + Printf.fprintf o "%s" html_preamble; + Printf.fprintf o "%s" (Ulib.Text.to_string r); + Printf.fprintf o "%s" html_postamble; + close_output_with_check ext_o + end + | Some(Typed_ast.Target_hol) -> + begin + let (r_main, r_extra_opt) = B.hol_defs m.typed_ast in + let hol_header o = begin + Printf.fprintf o "(*%s*)\n" (generated_line m.filename); + Printf.fprintf o "open bossLib Theory Parse res_quanTheory\n"; + Printf.fprintf o "open fixedPointTheory finite_mapTheory listTheory pairTheory pred_setTheory\n"; + Printf.fprintf o "open integerTheory set_relationTheory sortingTheory stringTheory wordsTheory\n\n"; + Printf.fprintf o "val _ = numLib.prefer_num();\n\n"; + Printf.fprintf o "\n\n"; + begin + if m.predecessor_modules <> [] then + begin + Printf.fprintf o "open"; + List.iter + (fun f -> Printf.fprintf o " %s" f; Printf.fprintf o "Theory") + m.predecessor_modules; + Printf.fprintf o "\n\n" + end + else + () + end + end in + let _ = begin + let (o, ext_o) = open_output_with_check (m.module_name ^ "Script.sml") in + hol_header o; + Printf.fprintf o "val _ = new_theory \"%s\"\n\n" m.module_name; + Printf.fprintf o "%s" (Ulib.Text.to_string r_main); + Printf.fprintf o "val _ = export_theory()\n\n"; + close_output_with_check ext_o; + end in + let _ = match r_extra_opt with None -> () | Some r_extra -> + begin + let (o,ext_o) = open_output_with_check (m.module_name ^ "ExtraScript.sml") in + hol_header o; + Printf.fprintf o "open %sTheory\n\n" m.module_name; + Printf.fprintf o "val _ = new_theory \"%sExtra\"\n\n" m.module_name; + Printf.fprintf o "%s" (Ulib.Text.to_string r_extra); + Printf.fprintf o "val _ = export_theory()\n\n"; + close_output_with_check ext_o + end in () + end + | Some(Typed_ast.Target_tex) -> + begin + let rr = B.tex_defs m.typed_ast in + (* complete tex document, wrapped in tex_preamble and tex_postamble *) + let (^^^^) = Ulib.Text.(^^^) in + let r' = r"\\section{" ^^^^ Output.tex_escape (Ulib.Text.of_string f') ^^^^ r"}\n" ^^^^ rr in + alldoc_accum := (!alldoc_accum) @ [r']; + let (o, ext_o) = open_output_with_check (f' ^ ".tex") in + Printf.fprintf o "%%%s\n" (generated_line m.filename); + Printf.fprintf o "%s" tex_preamble; + Printf.fprintf o "%s" (Ulib.Text.to_string rr); + Printf.fprintf o "%s" tex_postamble; + close_output_with_check ext_o; + (* tex definitions to include in other documents *) + let header = r"\n%%%% generated from " ^^^^ (Ulib.Text.of_string m.filename) ^^^^ r"\n" in + let (r,r_usage) = B.tex_inc_defs m.typed_ast in + let (r,r_usage) = (header ^^^^ r, header ^^^^ r_usage) in + alldoc_inc_accum := (!alldoc_inc_accum) @ [r]; + alldoc_inc_usage_accum := (!alldoc_inc_usage_accum) @ [r_usage]; + let (o,ext_o) = open_output_with_check (f' ^ "-inc.tex") in + Printf.fprintf o "%%%s\n" (generated_line m.filename); + Printf.fprintf o "%s" (Ulib.Text.to_string r); + close_output_with_check ext_o; + let (o, ext_o) = open_output_with_check (f' ^ "-use_inc.tex") in + Printf.fprintf o "%%%s\n" (generated_line m.filename); + Printf.fprintf o "%s" (Ulib.Text.to_string r_usage); + close_output_with_check ext_o + end + | Some(Typed_ast.Target_ocaml) -> + begin + let (r_main, r_extra_opt) = B.ocaml_defs m.typed_ast in + let _ = begin + let (o, ext_o) = open_output_with_check (f' ^ ".ml") in + Printf.fprintf o "(*%s*)\n" (generated_line m.filename); + Printf.fprintf o "open Nat_num\n\n"; + Printf.fprintf o "open Sum\n\n"; + Printf.fprintf o "type 'a set = 'a Pset.set\n\n"; + Printf.fprintf o "%s" (Ulib.Text.to_string r_main); + close_output_with_check ext_o + end in + let _ = match r_extra_opt with None -> () | Some r_extra -> + begin + let (o, ext_o) = open_output_with_check (f' ^ "Extra.ml") in + Printf.fprintf o "(*%s*)\n" (generated_line m.filename); + Printf.fprintf o "open Nat_num\n"; + Printf.fprintf o "open %s\n\n" m.module_name; + Printf.fprintf o "type 'a set = 'a Pset.set\n\n"; + + Printf.fprintf o "%s" "let run_test n loc b =\n if b then (Format.printf \"%s : ok\\n\" n) else (Format.printf \"%s : FAILED\\n %s\\n\\n\" n loc);;\n\n"; + + Printf.fprintf o "%s" (Ulib.Text.to_string r_extra); + close_output_with_check ext_o + end in () + end + | Some(Typed_ast.Target_isa) -> + begin + try begin + let (r_main, r_extra_opt) = B.isa_defs m.typed_ast in + let r1 = B.isa_header_defs m.typed_ast in + let _ = + begin + let (o, ext_o) = open_output_with_check (m.module_name ^ ".thy") in + Printf.fprintf o "header{*%s*}\n\n" (generated_line m.filename); + Printf.fprintf o "theory \"%s\" \n\n" m.module_name; + Printf.fprintf o "imports \n \t Main\n"; + Printf.fprintf o "\t \"%s\"\n" isa_thy; + (* + Printf.fprintf o "imports \n \t \"%s/num_type\" \n" libpath; + *) + Printf.fprintf o "%s" (Ulib.Text.to_string r1); + + begin + if m.predecessor_modules <> [] then + begin + List.iter (fun f -> Printf.fprintf o "\t \"%s\" \n" f) m.predecessor_modules; + end + else () + end; + + Printf.fprintf o "\nbegin \n\n"; + Printf.fprintf o "%s" (Ulib.Text.to_string r_main); + Printf.fprintf o "end\n"; + close_output_with_check ext_o + end in + + let _ = match r_extra_opt with None -> () | Some r_extra -> + begin + let (o, ext_o) = open_output_with_check (m.module_name ^ "Extra.thy") in + Printf.fprintf o "header{*%s*}\n\n" (generated_line m.filename); + Printf.fprintf o "theory \"%sExtra\" \n\n" m.module_name; + Printf.fprintf o "imports \n \t Main \"~~/src/HOL/Library/Efficient_Nat\" \"%s\"\n" m.module_name; + Printf.fprintf o "\nbegin \n\n"; + Printf.fprintf o "%s" (Ulib.Text.to_string r_extra); + Printf.fprintf o "end\n"; + close_output_with_check ext_o + end in () + end + with | Trans.Trans_error(l,msg) -> + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_trans_header (l, msg))) + end + + | Some(Typed_ast.Target_coq) -> + begin + let r = B.coq_defs m.typed_ast in + let (o, ext_o) = open_output_with_check (f' ^ ".v") in + Printf.fprintf o "(* %s *)\n\n" (generated_line m.filename); + Printf.fprintf o "Require Import Arith.\n"; + Printf.fprintf o "Require Import Bool.\n"; + Printf.fprintf o "Require Import List.\n"; + Printf.fprintf o "Require Import String.\n"; + Printf.fprintf o "Require Import Program.Wf.\n\n"; + Printf.fprintf o "Open Scope nat_scope.\n"; + Printf.fprintf o "Open Scope string_scope.\n\n"; + Printf.fprintf o "%s" (Ulib.Text.to_string r); + close_output_with_check ext_o + end + +let output libpath isa_thy targ consts type_info mods alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum = + List.iter + (fun m -> + output1 libpath isa_thy targ consts type_info m alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum) + mods + + +let output_alldoc f' fs alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum = + let rs = !alldoc_accum in + let (o, ext_o) = open_output_with_check (f' ^ ".tex") in + Printf.fprintf o "%%%s\n" (generated_line fs); + Printf.fprintf o "%s" tex_preamble; + Printf.fprintf o "%s" (Ulib.Text.to_string (Ulib.Text.concat (r"") rs)); + Printf.fprintf o "%s" tex_postamble; + close_output_with_check ext_o; + let rs = !alldoc_inc_accum in + let (o, ext_o) = open_output_with_check (f' ^ "-inc.tex") in + Printf.fprintf o "%%%s\n" (generated_line fs); + Printf.fprintf o "%s" (Ulib.Text.to_string (Ulib.Text.concat (r"") rs)); + close_output_with_check ext_o; + let rs = !alldoc_inc_usage_accum in + let (o, ext_o) = open_output_with_check (f' ^ "-use_inc.tex") in + Printf.fprintf o "%%%s\n" (generated_line fs); + Printf.fprintf o "%s" (Ulib.Text.to_string (Ulib.Text.concat (r"") rs)); + close_output_with_check ext_o + +*) diff --git a/src/process_file.mli b/src/process_file.mli new file mode 100644 index 00000000..1fb8ea2f --- /dev/null +++ b/src/process_file.mli @@ -0,0 +1,91 @@ +(**************************************************************************) +(* Lem *) +(* *) +(* Dominic Mulligan, University of Cambridge *) +(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) +(* Gabriel Kerneis, University of Cambridge *) +(* Kathy Gray, University of Cambridge *) +(* Peter Boehm, University of Cambridge (while working on Lem) *) +(* Peter Sewell, University of Cambridge *) +(* Scott Owens, University of Kent *) +(* Thomas Tuerk, University of Cambridge *) +(* *) +(* The Lem sources are copyright 2010-2013 *) +(* by the UK authors above and Institut National de Recherche en *) +(* Informatique et en Automatique (INRIA). *) +(* *) +(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) +(* are distributed under the license below. The former are distributed *) +(* under the LGPLv2, as in the LICENSE file. *) +(* *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* 3. The names of the authors may not be used to endorse or promote *) +(* products derived from this software without specific prior written *) +(* permission. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) +(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) +(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) +(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) +(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) +(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) +(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) +(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) +(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) +(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) +(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(**************************************************************************) + +(* open Typed_ast *) + +val parse_file : string -> bool Ast.defs * Ast.lex_skips + +(* type instances = Types.instance list Types.Pfmap.t + +val check_ast_as_module : + Targetset.t -> + Name.t list -> + (Types.type_defs * instances) * env -> + Ulib.Text.t -> + Ast.defs * Ast.lex_skips -> + (Types.type_defs * instances * instances) * env * + (def list * Ast.lex_skips) + +val check_ast : + Targetset.t -> + Name.t list -> + (Types.type_defs * instances) * env -> + Ast.defs * Ast.lex_skips -> + (Types.type_defs * instances * instances) * env * + (def list * Ast.lex_skips) + +val output : + string -> (* The path to the library *) + string -> (* Isabelle Theory to be included *) + target option -> (* Backend name (None for the identity backend) *) + Typed_ast.var_avoid_f -> + (Types.type_defs * instances) -> (* The full environment built after all typechecking, and transforming *) + checked_module list -> (* The typechecked modules *) + Ulib.Text.t list ref -> (* alldoc accumulator *) + Ulib.Text.t list ref -> (* alldoc-inc accumulator *) + Ulib.Text.t list ref -> (* alldoc-use_inc accumulator *) + unit + +val output_alldoc : string -> string -> Ulib.Text.t list ref -> Ulib.Text.t list ref -> Ulib.Text.t list ref -> unit + +(** [always_replace_files] determines whether Lem only updates modified files. + If it is set to [true], all output files are written, regardless of whether the + files existed before. If it is set to [false] and an output file already exists, + the output file is only updated, if its content really changes. For some + backends like OCaml, HOL, Isabelle, this is benefitial, since it prevents them + from reprocessing these unchanged files. *) +val always_replace_files : bool ref +*) |