diff options
| -rw-r--r-- | language/Makefile | 3 | ||||
| -rw-r--r-- | language/l2.ott | 14 | ||||
| -rw-r--r-- | src/ast.ml | 453 |
3 files changed, 461 insertions, 9 deletions
diff --git a/language/Makefile b/language/Makefile index f8858e31..f1607d23 100644 --- a/language/Makefile +++ b/language/Makefile @@ -1,4 +1,3 @@ -#OTTLIB=/Users/sowens/ott/hol OTTLIB=$(dir $(shell which ott))../hol all: l2.pdf @@ -11,7 +10,7 @@ l2Theory.uo: l2Script.sml l2.tex ../src/ast.ml l2Script.sml: l2.ott ott -sort false -generate_aux_rules false -o l2.tex -picky_multiple_parses true l2.ott - ott -sort false -generate_aux_rules true -ocaml_include_terminals true -o l2.ml -o l2Script.sml -picky_multiple_parses true l2.ott + ott -sort false -generate_aux_rules true -ocaml_include_terminals true -o ../src/ast.ml -o l2Script.sml -picky_multiple_parses true l2.ott #rm -f ../src/ast.ml # chmod a-w ../src/ast.ml diff --git a/language/l2.ott b/language/l2.ott index 3c186839..d1bf5793 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -597,7 +597,7 @@ pat :: 'P_' ::= | lit :: :: lit {{ com Literal constant patterns }} -fpat :: 'FP' ::= +fpat :: 'FP_' ::= {{ com Field patterns }} {{ aux _ l }} | id = pat :: :: Fpat @@ -717,17 +717,17 @@ lexp :: 'LEXP_' ::= | lexp . id :: :: field -fexp :: 'FE' ::= +fexp :: 'FE_' ::= {{ com Field-expressions }} {{ aux _ l }} | id = exp :: :: Fexp -fexps :: 'FES' ::= +fexps :: 'FES_' ::= {{ com Field-expression lists }} {{ aux _ l }} | fexp1 ; ... ; fexpn semi_opt :: :: Fexps -pexp :: 'Pat' ::= +pexp :: 'Pat_' ::= {{ com Pattern matches }} {{ aux _ l }} | pat -> exp :: :: exp @@ -809,7 +809,7 @@ c_tannot_opt :: 'C_typ_annot_' ::= | :: :: none | typ_quant typ :: :: some -c_funcl :: 'C_FCL' ::= +c_funcl :: 'C_FCL_' ::= {{ com Function clauses }} {{ aux _ l }} | id pat = exp :: :: Funcl @@ -824,7 +824,7 @@ c_effects_opt :: '' ::= | :: :: pure {{ com sugar for pure }} | effects :: :: nonpure -c_fundef :: 'C_FD' ::= +c_fundef :: 'C_FD_' ::= {{ com Function definition}} {{ aux _ l }} | function c_rec_opt c_tannot_opt c_effects_opt c_funcl1 and ... and c_funcln :: :: function {{ texlong }} {{ com function definition }} @@ -844,7 +844,7 @@ c_letbind :: 'LB_' ::= {{ com value binding with implicit type }} -val_spec :: 'VS' ::= +val_spec :: 'VS_' ::= {{ com Value type specifications }} {{ aux _ l }} | val typschm id :: :: val_spec diff --git a/src/ast.ml b/src/ast.ml new file mode 100644 index 00000000..e39f1931 --- /dev/null +++ b/src/ast.ml @@ -0,0 +1,453 @@ +(* generated by Ott 0.21.2 from: l2.ott *) + + +type text = Ulib.Text.t + +type l = + | Unknown + | Trans of string * l option + | Range of Lexing.position * Lexing.position + +exception Parse_error_locn of l * string + +type ml_comment = + | Chars of Ulib.Text.t + | Comment of ml_comment list + +type lex_skip = + | Com of ml_comment + | Ws of Ulib.Text.t + | Nl + +type lex_skips = lex_skip list option + +let pp_lex_skips ppf sk = + match sk with + | None -> () + | Some(sks) -> + List.iter + (fun sk -> + match sk with + | Com(ml_comment) -> + (* TODO: fix? *) + Format.fprintf ppf "(**)" + | Ws(r) -> + Format.fprintf ppf "%s" (Ulib.Text.to_string r) + | Nl -> Format.fprintf ppf "\\n") + sks + +let combine_lex_skips s1 s2 = + match (s1,s2) with + | (None,_) -> s2 + | (_,None) -> s1 + | (Some(s1),Some(s2)) -> Some(s2@s1) + +type terminal = lex_skips + + +type x = terminal * text (* Variables *) +type ix = terminal * text (* Variables *) + +type +base_kind_aux = (* base kinds *) + BK_type of terminal + | BK_nat of terminal + | BK_endian of terminal + | BK_effects of terminal + + +type +id_aux = (* identifiers *) + 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 + + +type +kind_aux = (* kinds *) + Kind of (base_kind * terminal) list + + +type +nexp_aux = (* expressions of kind Nat, for vector lengths *) + Nexp_var of id + | Nexp_constant of terminal * int + | Nexp_times of nexp * terminal * nexp (* must be linear after normalisation... except for the type of *, ahem *) + | Nexp_sum of nexp * terminal * nexp + | Nexp_exp of terminal * terminal * nexp + +and nexp = + Nexp_aux of nexp_aux * l + + +type +effect_aux = (* effect *) + Effect_rreg of terminal (* read register *) + | Effect_wreg of terminal (* write register *) + | Effect_rmem of terminal (* read memory *) + | Effect_wmem of terminal (* write memory *) + | Effect_undef of terminal (* undefined-instruction exception *) + | Effect_unspec of terminal (* unspecified values *) + | Effect_nondet of terminal (* nondeterminism from intra-instruction parallelism *) + + +type +kind = + Kind_aux of kind_aux * l + + +type +nexp_constraint_aux = (* contraints over kind Nat *) + 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 +effect = + Effect_aux of effect_aux * l + + +type +opt_kind = (* optionally kind-annotated identifier *) + Ki_ant_none of id + | Ki_ant_kind of id * terminal * kind + + +type +nexp_constraint = + NC_aux of nexp_constraint_aux * l + + +type +endian_aux = (* endianness specifications *) + End_var of id + | End_inc of terminal + | End_dec of terminal + + +type +effects_aux = (* effect set *) + Effects_var of id + | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *) + + +type +typquant_aux = + TQ_Ts of terminal * (opt_kind) list * terminal * (nexp_constraint * terminal) list * terminal + | TQ_Ts_no_constraint of terminal * (opt_kind) list * terminal (* sugar *) + | TQ_Ts_no_forall (* sugar *) + + +type +endian = + End_aux of endian_aux * l + + +type +effects = + Effects_aux of effects_aux * l + + +type +typquant = + TQ_aux of typquant_aux * l + + +type +typ = (* Constructors of kind Type *) + Typ_wild of terminal (* Unspecified type *) + | Typ_var of id (* Type variables *) + | Typ_fn of typ * terminal * typ * effects (* Function types -- first-order only *) + | Typ_tup of (typ * terminal) list (* Tuple types *) + | Typ_app of id * (typ_arg) list (* type constructor applications *) + +and typ_arg = (* Type constructor arguments of all kinds *) + Typ_arg_nexp of nexp + | Typ_arg_typ of typ + | Typ_arg_endian of endian + | Typ_arg_effects of effects + + +type +lit = (* Literal constants *) + L_true of terminal + | L_false of terminal + | L_num of terminal * int + | L_hex of terminal * string (* hex and bin are constant bit vectors, entered as C-style hex or binaries *) + | L_bin of terminal * string + | L_string of terminal * Ulib.UTF8.t + | L_unit of terminal * terminal + | L_zero of terminal (* bitzero and bitone are constant bits, if commonly used we will consider overloading 0 and 1 *) + | L_one of terminal + + +type +typschm_aux = (* Type schemes *) + TS_Ts of typquant * typ + + +type +pat_aux = (* Patterns *) + P_wild of terminal (* Wildcards *) + | P_as of terminal * pat * terminal * id * terminal (* Named patterns *) + | P_typ of terminal * typ * pat * terminal (* Typed patterns *) + | P_app of id * (pat) list (* Single variable and constructor patterns *) + | P_record of terminal * (fpat * terminal) list * terminal * bool * terminal (* Record patterns *) + | P_c_record of terminal * terminal * (fpat * terminal) list * terminal * bool * terminal (* C-style struct patterns *) + | P_vector of terminal * (pat * terminal) list * terminal * bool * terminal (* Vector patterns *) + | P_vector_concat of terminal * (pat) list * terminal (* Concatenated vector patterns *) + | P_tup of terminal * (pat * terminal) list * terminal (* Tuple patterns *) + | P_list of terminal * (pat * terminal) list * terminal (* List patterns *) + | P_paren of terminal * pat * terminal + | P_cons of pat * terminal * pat (* Cons patterns *) + | P_num_add of id * terminal * terminal * int (* constant addition patterns *) + | P_lit of lit (* Literal constant patterns *) + +and pat = + P_aux of pat_aux * l + +and fpat_aux = (* Field patterns *) + FP_Fpat of id * terminal * pat + +and fpat = + FP_aux of fpat_aux * l + + +type +typschm = + TS_aux of typschm_aux * l + + +type +exp_aux = (* Expressions *) + E_block of terminal * (exp * terminal) list * terminal + | E_ident of id (* Identifiers *) + | E_lit of lit (* Literal constants *) + | E_app of exp * exp (* Function applications *) + | E_infix of exp * id * exp (* Infix applications *) + | E_tup of terminal * (exp * terminal) list * terminal (* Tuples *) + | E_if of terminal * exp * terminal * exp * terminal * exp (* Conditionals *) + | E_enummap of terminal * (exp * terminal) list * terminal + | E_enummap_e of terminal * ((terminal * int * terminal * exp) * terminal) list * terminal + | E_enummap_access of exp * terminal * exp * terminal (* enummap access *) + | E_enummap_subrange of exp * terminal * exp * terminal * exp * terminal (* Subenummap extraction *) + | E_enummap_update of terminal * exp * terminal * exp * terminal * exp * terminal (* enummap functional update *) + | E_enummap_update_range of terminal * exp * terminal * (exp) list * terminal * exp * terminal (* enummap functional subrange update (with another enummap) *) + | E_list of terminal * (exp * terminal) list * terminal (* list *) + | E_cons of exp * terminal * exp (* Cons expressions *) + | E_record of terminal * fexps * terminal (* Records *) + | E_recup of terminal * exp * terminal * fexps * terminal (* Functional update for records *) + | E_field of exp * terminal * id (* Field projection for records *) + | E_case of terminal * exp * terminal * ((terminal * pexp)) list * terminal (* Pattern matching expressions *) + | E_let of c_letbind * terminal * exp (* Let expressions *) + | E_assign of lexp * terminal * exp + +and exp = + E_aux of exp_aux * l + +and lexp = + LEXP_ident of id (* Identifiers *) + | LEXP_enummap of lexp * terminal * exp * terminal + | LEXP_enummap_range of lexp * terminal * exp * terminal * exp * terminal + | LEXP_field of lexp * terminal * id + +and fexp_aux = (* Field-expressions *) + FE_Fexp of id * terminal * exp + +and fexp = + FE_aux of fexp_aux * l + +and fexps_aux = (* Field-expression lists *) + FES_Fexps of (fexp * terminal) list * terminal * bool + +and fexps = + FES_aux of fexps_aux * l + +and pexp_aux = (* Pattern matches *) + Pat_exp of pat * terminal * exp + +and pexp = + Pat_aux of pexp_aux * l + +and c_letbind_aux = (* Let bindings *) + LB_val_exp of typschm * id * terminal * exp (* Value binding *) + | LB_val_imp of terminal * id * terminal * exp (* value binding with implicit type *) + +and c_letbind = + LB_aux of c_letbind_aux * l + + +type +c_rec_opt_aux = + Nonrec + | Rec of terminal + + +type +c_funcl_aux = (* Function clauses *) + C_FCL_Funcl of id * pat * terminal * exp + + +type +c_effects_opt_aux = + Pure (* sugar for pure *) + | Nonpure of effects + + +type +ctor_def = (* Datatype definition clauses *) + Cte of id * terminal * typschm + + +type +c_rec_opt = + C_rec_opt_aux of c_rec_opt_aux * l + + +type +c_tannot_opt = (* Optional type annotations *) + C_typ_annot_none + | C_typ_annot_some of terminal * typ + + +type +c_funcl = + C_FCL_aux of c_funcl_aux * l + + +type +c_effects_opt = + C_effects_opt_aux of c_effects_opt_aux * l + + +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 + + +type +tdefbody = (* Type definition bodies *) + Te_abbrev of typschm (* Type abbreviations *) + | Te_record of typquant * terminal * ((id * terminal * typ) * terminal) list * terminal * bool * terminal (* Record types *) + | Te_variant of terminal * terminal * (ctor_def * terminal) list (* Variant types *) + + +type +default_typing_spec_aux = (* default kinding and typing assumptions *) + DT_kind of terminal * base_kind * terminal * string + | DT_typ of terminal * typschm * terminal * string + + +type +val_spec_aux = (* Value type specifications *) + VS_val_spec of terminal * typschm * id + + +type +c_fundef_aux = (* Function definition *) + C_FD_function of terminal * c_rec_opt * c_tannot_opt * c_effects_opt * (c_funcl * terminal) list (* function definition *) + + +type +type_def = (* Type definitions *) + Td of terminal * id * terminal * kind * naming_scheme_opt * terminal * tdefbody + + +type +default_typing_spec = + DT_aux of default_typing_spec_aux * l + + +type +val_spec = + VS_aux of val_spec_aux * l + + +type +c_fundef = + C_FD_aux of c_fundef_aux * l + + +type +def_aux = (* Top-level definitions *) + DEF_type_def of type_def (* Type definition *) + | DEF_fun_def of c_fundef (* Function definition *) + | DEF_val_def of c_letbind (* Value definition *) + | DEF_spec_def of val_spec (* Top-level type constraint *) + | DEF_default_def of default_typing_spec (* default kind and type assumptions *) + | DEF_reg_dec of terminal * typ * id (* Register declaration *) + + +type +def = + DEF_aux of def_aux * l + + +type +bitfield = + BF_bit of terminal * int + | BF_bits of terminal * int * terminal * terminal * int + | BF_bitfields of bitfield * terminal * bitfield + + +type +defs_aux = (* Definition sequences *) + Defs of (def) list + + +type +typ_sugar_aux = (* library types and syntactic sugar *) + Typ_sugar_unit of terminal + | Typ_sugar_bool of terminal + | Typ_sugar_bit of terminal (* pure bits, not mutable bits! *) + | Typ_sugar_nat of terminal + | Typ_sugar_string of terminal * Ulib.UTF8.t + | Typ_sugar_enum of terminal * nexp * nexp * endian (* natural numbers from nexp to nexp+nexp-1, ordered by endian *) + | Typ_sugar_enum1 of terminal * nexp * terminal (* sugar for \texttt{enum nexp 0 inc} *) + | Typ_sugar_enum2 of terminal * nexp * terminal * nexp * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) + | Typ_sugar_enummap of terminal * nexp * nexp * endian * typ + | Typ_sugar_enummap2 of typ * terminal * nexp * terminal + | Typ_sugar_enummap3 of typ * terminal * nexp * terminal * nexp * terminal + | Typ_sugar_list of terminal * typ + | Typ_sugar_set of terminal * typ + | Typ_sugar_reg of terminal * typ (* type of mutable register components *) + + +type +c_tdefbody = (* Type definition bodies *) + C_Te_abbrev of terminal * id * naming_scheme_opt * terminal * typschm (* Type abbreviations *) + | C_Te_record of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* Struct type definition *) + | C_Te_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* Union type definition *) + | C_Te_enum of terminal * id * naming_scheme_opt * terminal * terminal * terminal * (id * terminal) list * terminal * bool * terminal (* enumeration type definition *) + | C_Te_register of terminal * id * terminal * terminal * terminal * terminal * nexp * terminal * nexp * terminal * terminal * ((bitfield * terminal * id) * terminal) list * terminal (* register mutable bitfield type *) + + +type +enum_opt = + Enum_empty + | Enum_enum of terminal + + +type +defs = + Defs_aux of defs_aux * l + + +type +typ_sugar = + Typ_sugar_aux of typ_sugar_aux * l + + + |