diff options
Diffstat (limited to 'src/lem_interp/ast.lem')
| l---------[-rw-r--r--] | src/lem_interp/ast.lem | 305 |
1 files changed, 1 insertions, 304 deletions
diff --git a/src/lem_interp/ast.lem b/src/lem_interp/ast.lem index 51831898..37719b1b 100644..120000 --- a/src/lem_interp/ast.lem +++ b/src/lem_interp/ast.lem @@ -1,304 +1 @@ -(* generated by Ott 0.22 from: l2.ott *) - -open Pmap -open Pervasives - -type l = - | Unknown - | Trans of string * option l - | Range of num * num - -val disjoint : forall 'a . set 'a -> set 'a -> bool -let disjoint s1 s2 = - let diff = s1 inter s2 in - diff = Pervasives.empty - -val disjoint_all : forall 'a. list (set 'a) -> bool -let rec disjoint_all ls = match ls with - | [] -> true - | [a] -> true - | a::b::rs -> (disjoint a b) && (disjoint_all (b::rs)) -end - -val duplicates : forall 'a. list 'a -> list 'a - -val union_map : forall 'a 'b. map 'a 'b -> map 'a 'b -> map 'a 'b - -val set_from_list : forall 'a. list 'a -> set 'a - -val subst : forall 'a. list 'a -> list 'a -> bool - - -type x = string (* identifier *) -type ix = string (* infix identifier *) - -type base_kind = (* base kind *) - | BK_type (* kind of types *) - | BK_nat (* kind of natural number size expressions *) - | BK_order (* kind of vector order specifications *) - | BK_effects (* kind of effect sets *) - - -type id = (* Identifier *) - | Id of x - | DeIid of x (* remove infix status *) - - -type kind = (* kinds *) - | K_kind of list base_kind - - -type nexp = (* expression of kind $Nat$, for vector sizes and origins *) - | Nexp_id of id (* identifier *) - | Nexp_constant of num (* constant *) - | Nexp_times of nexp * nexp (* product *) - | Nexp_sum of nexp * nexp (* sum *) - | Nexp_exp of nexp (* exponential *) - - -type efct = (* effect *) - | Effect_rreg (* read register *) - | Effect_wreg (* write register *) - | Effect_rmem (* read memory *) - | Effect_wmem (* write memory *) - | Effect_undef (* undefined-instruction exception *) - | Effect_unspec (* unspecified values *) - | Effect_nondet (* nondeterminism from intra-instruction parallelism *) - - -type kinded_id = (* optionally kind-annotated identifier *) - | KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) - - -type nexp_constraint = (* constraint over kind $Nat$ *) - | NC_fixed of nexp * nexp - | NC_bounded_ge of nexp * nexp - | NC_bounded_le of nexp * nexp - | NC_nat_set_bounded of id * list num - - -type order = (* vector order specifications, of kind $Order$ *) - | Ord_id of id (* identifier *) - | Ord_inc (* increasing (little-endian) *) - | Ord_dec (* decreasing (big-endian) *) - - -type effects = (* effect set, of kind $Effects$ *) - | Effects_var of id - | Effects_set of list efct (* effect set *) - - -type quant_item = (* Either a kinded identifier or a nexp constraint for a typquant *) - | QI_id of kinded_id (* An optionally kinded identifier *) - | QI_const of nexp_constraint (* A constraint for this type *) - - -type typ = (* Type expressions, of kind $Type$ *) - | Typ_wild (* Unspecified type *) - | Typ_var of id (* Type variable *) - | Typ_fn of typ * typ * effects (* Function type (first-order only in user code) *) - | Typ_tup of list typ (* Tuple type *) - | Typ_app of id * list typ_arg (* type constructor application *) - -and typ_arg = (* 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 - - -type typquant = (* type quantifiers and constraints *) - | TypQ_tq of list quant_item - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) - - -type lit = (* Literal constant *) - | L_unit (* $() : unit$ *) - | L_zero (* $bitzero : bit$ *) - | L_one (* $bitone : bit$ *) - | L_true (* $true : bool$ *) - | L_false (* $false : bool$ *) - | L_num of num (* natural number constant *) - | L_hex of string (* bit vector constant, C-style *) - | L_bin of string (* bit vector constant, C-style *) - | L_undef (* constant representing undefined values *) - | L_string of string (* string constant *) - - -type typschm = (* type scheme *) - | TypSchm_ts of typquant * typ - - -type pat = (* Pattern *) - | P_lit of lit (* literal constant pattern *) - | P_wild (* wildcard *) - | P_as of pat * id (* named pattern *) - | P_typ of typ * pat (* typed pattern *) - | P_id of id (* identifier *) - | P_app of id * list pat (* union constructor pattern *) - | P_record of list fpat * bool (* struct pattern *) - | P_vector of list pat (* vector pattern *) - | P_vector_indexed of list (num * pat) (* vector pattern (with explicit indices) *) - | P_vector_concat of list pat (* concatenated vector pattern *) - | P_tup of list pat (* tuple pattern *) - | P_list of list pat (* list pattern *) - -and fpat = (* Field pattern *) - | FP_Fpat of id * pat - - -type ne = (* internal numeric expressions *) - | Ne_var of id - | Ne_const of num - | Ne_mult of ne * ne - | Ne_add of ne * ne - | Ne_exp of ne - | Ne_unary of ne - - -type letbind = (* Let binding *) - | LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *) - | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) - -and exp = (* Expression *) - | E_block of list exp (* block (parsing conflict with structs?) *) - | E_id of id (* identifier *) - | E_lit of lit (* literal constant *) - | E_cast of typ * exp (* cast *) - | E_app of exp * list exp (* function application *) - | E_app_infix of exp * id * exp (* infix function application *) - | E_tuple of list exp (* tuple *) - | E_if of exp * exp * exp (* conditional *) - | E_for of id * exp * exp * exp * exp (* loop *) - | E_vector of list exp (* vector (indexed from 0) *) - | E_vector_indexed of list (num * exp) (* vector (indexed consecutively) *) - | E_vector_access of exp * exp (* vector access *) - | E_vector_subrange of exp * exp * exp (* subvector extraction *) - | E_vector_update of exp * exp * exp (* vector functional update *) - | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *) - | E_list of list exp (* list *) - | E_cons of exp * exp (* cons *) - | E_record of fexps (* struct *) - | E_record_update of exp * fexps (* functional update of struct *) - | E_field of exp * id (* field projection from struct *) - | E_case of exp * list pexp (* pattern matching *) - | E_let of letbind * exp (* let expression *) - | E_assign of lexp * exp (* imperative assignment *) - -and lexp = (* lvalue expression *) - | LEXP_id of id (* identifier *) - | LEXP_vector of lexp * exp (* vector element *) - | LEXP_vector_range of lexp * exp * exp (* subvector *) - | LEXP_field of lexp * id (* struct field *) - -and fexp = (* Field-expression *) - | FE_Fexp of id * exp - -and fexps = (* Field-expression list *) - | FES_Fexps of list fexp * bool - -and pexp = (* Pattern match *) - | Pat_exp of pat * exp - - -type k = (* Internal kinds *) - | Ki_typ - | Ki_nat - | Ki_ord - | Ki_efct - | Ki_val (* Representing values, for use in identifier checks *) - | Ki_ctor of list k * k - | Ki_infer (* Representing an unknown kind, inferred by context *) - - -type index_range = (* index specification, for bitfields in register types *) - | BF_single of num (* single index *) - | BF_range of num * num (* index range *) - | BF_concat of index_range * index_range (* concatenation of index ranges *) - - -type naming_scheme_opt = (* Optional variable-naming-scheme specification for variables of defined type *) - | Name_sect_none - | Name_sect_some of string - - -type rec_opt = (* Optional recursive annotation for functions *) - | Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) - - -type effects_opt = (* Optional effect annotation for functions *) - | Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of effects - - -type funcl = (* Function clause *) - | FCL_Funcl of id * pat * exp - - -type tannot_opt = (* Optional type annotation for functions *) - | Typ_annot_opt_some of typquant * typ - - -type default_typing_spec = (* Default kinding or typing assumption *) - | DT_kind of base_kind * id - | DT_typ of typschm * id - - -type val_spec = (* Value type specification *) - | VS_val_spec of typschm * id - - -type type_def = (* Type definition body *) - | TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *) - | TD_record of id * naming_scheme_opt * typquant * list (typ * id) * bool (* struct type definition *) - | TD_variant of id * naming_scheme_opt * typquant * list (typ * id) * bool (* union type definition *) - | TD_enum of id * naming_scheme_opt * list id * bool (* enumeration type definition *) - | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) - - -type fundef = (* Function definition *) - | FD_function of rec_opt * tannot_opt * effects_opt * list funcl - - -type def = (* 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 *) - | DEF_reg_dec of typ * id (* register declaration *) - | DEF_scattered_function of rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *) - | DEF_scattered_funcl of funcl (* scattered function definition clause *) - | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *) - | DEF_scattered_unioncl of id * typ * id (* scattered union definition member *) - | DEF_scattered_end of id (* scattered definition end *) - - -type typ_lib = (* library types and syntactic sugar for them *) - | Typ_lib_unit (* unit type with value $()$ *) - | Typ_lib_bool (* booleans $true$ and $false$ *) - | Typ_lib_bit (* pure bit values (not mutable bits) *) - | Typ_lib_nat (* natural numbers 0,1,2,... *) - | Typ_lib_string of string (* UTF8 strings *) - | Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *) - | Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *) - | Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) - | Typ_lib_vector of nexp * nexp * order * typ (* vector of typ, indexed by natural range *) - | Typ_lib_vector2 of typ * nexp (* sugar for vector indexed by [ nexp ] *) - | Typ_lib_vector3 of typ * nexp * nexp (* sugar for vector indexed by [ nexp..nexp ] *) - | Typ_lib_list of typ (* list of typ *) - | Typ_lib_set of typ (* finite set of typ *) - | Typ_lib_reg of typ (* mutable register components holding typ *) - - -type ctor_def = (* Datatype constructor definition clause *) - | CT_ct of id * typschm - - -type defs = (* Definition sequence *) - | Defs of list def - - - +../../language/l2.lem
\ No newline at end of file |