summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast.ml453
1 files changed, 453 insertions, 0 deletions
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
+
+
+