diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast.lem | 744 | ||||
| -rw-r--r-- | src/ast.ml | 87 |
2 files changed, 789 insertions, 42 deletions
diff --git a/src/ast.lem b/src/ast.lem new file mode 100644 index 00000000..feeafd9e --- /dev/null +++ b/src/ast.lem @@ -0,0 +1,744 @@ +(* 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_aux = (* 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_aux = (* Identifier *) + | Id of x + | DeIid of x (* 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 *) + | K_kind of list base_kind + + +type nexp_aux = (* 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 *) + +and nexp = + | Nexp_aux of nexp_aux * l + + +type kind = + | K_aux of kind_aux * l + + +type nexp_constraint_aux = (* 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 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 + + +type kinded_id = + | KOpt_aux of kinded_id_aux * l + + +type efct_aux = (* 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 quant_item_aux = (* 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 efct = + | Effect_aux of efct_aux * l + + +type quant_item = + | QI_aux of quant_item_aux * l + + +type effects_aux = (* effect set, of kind $Effects$ *) + | Effects_var of id + | Effects_set of list efct (* effect set *) + + +type order_aux = (* vector order specifications, of kind $Order$ *) + | Ord_id of id (* identifier *) + | Ord_inc (* increasing (little-endian) *) + | Ord_dec (* decreasing (big-endian) *) + + +type typquant_aux = (* type quantifiers and constraints *) + | TypQ_tq of list quant_item + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) + + +type effects = + | Effects_aux of effects_aux * l + + +type order = + | Ord_aux of order_aux * l + + +type lit_aux = (* 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_string of string (* string constant *) + + +type typquant = + | TypQ_aux of typquant_aux * l + + +type typ_aux = (* 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 = + | 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 lit = + | L_aux of lit_aux * l + + +type typschm_aux = (* type scheme *) + | TypSchm_ts of typquant * typ + + +type pat_aux = (* 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 pat = + | P_aux of pat_aux * annot + +and fpat_aux = (* Field pattern *) + | FP_Fpat of id * pat + +and fpat = + | FP_aux of fpat_aux * annot + + +type typschm = + | TypSchm_aux of typschm_aux * l + + +type exp_aux = (* 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 exp = + | E_aux of exp_aux * annot + +and lexp_aux = (* 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 lexp = + | LEXP_aux of lexp_aux * annot + +and fexp_aux = (* Field-expression *) + | FE_Fexp of id * exp + +and fexp = + | FE_aux of fexp_aux * annot + +and fexps_aux = (* Field-expression list *) + | FES_Fexps of list fexp * bool + +and fexps = + | FES_aux of fexps_aux * annot + +and pexp_aux = (* Pattern match *) + | Pat_exp of pat * exp + +and pexp = + | Pat_aux of pexp_aux * annot + +and letbind_aux = (* 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 letbind = + | LB_aux of letbind_aux * annot + + +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 naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + | Name_sect_none + | Name_sect_some of string + + +type tannot_opt_aux = (* Optional type annotation for functions *) + | Typ_annot_opt_some of typquant * typ + + +type funcl_aux = (* Function clause *) + | FCL_Funcl of id * pat * exp + + +type effects_opt_aux = (* Optional effect annotation for functions *) + | Effects_opt_pure (* sugar for empty effect set *) + | Effects_opt_effects of effects + + +type rec_opt_aux = (* Optional recursive annotation for functions *) + | Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) + + +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 t_arg = (* Argument to type constructors *) + | Typ of t + | Nexp of ne + | Effect of effects + | Order of order + +and t_args = (* Arguments to type constructors *) + | T_args of list t_arg + + +type naming_scheme_opt = + | Name_sect_aux of naming_scheme_opt_aux * l + + +type index_range_aux = (* 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 *) + +and index_range = + | BF_aux of index_range_aux * l + + +type tannot_opt = + | Typ_annot_opt_aux of tannot_opt_aux * annot + + +type funcl = + | FCL_aux of funcl_aux * annot + + +type effects_opt = + | Effects_opt_aux of effects_opt_aux * annot + + +type rec_opt = + | Rec_aux of rec_opt_aux * l + + +type type_def_aux = (* 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 default_typing_spec_aux = (* Default kinding or typing assumption *) + | DT_kind of base_kind * id + | DT_typ of typschm * id + + +type fundef_aux = (* Function definition *) + | FD_function of rec_opt * tannot_opt * effects_opt * list funcl + + +type val_spec_aux = (* Value type specification *) + | VS_val_spec of typschm * id + + +type type_def = + | TD_aux of type_def_aux * annot + + +type default_typing_spec = + | DT_aux of default_typing_spec_aux * annot + + +type fundef = + | FD_aux of fundef_aux * annot + + +type val_spec = + | VS_aux of val_spec_aux * 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 *) + | 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_aux = (* 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_aux = (* Datatype constructor definition clause *) + | CT_ct of id * typschm + + +type def = + | DEF_aux of def_aux * annot + + +type typ_lib = + | Typ_lib_aux of typ_lib_aux * l + + +type ctor_def = + | CT_aux of ctor_def_aux * annot + + +type defs = (* Definition sequence *) + | Defs of list def + +(** definitions *) + (* defns translate_ast *) +indreln + +(** definitions *) + (* defns check_t *) +indreln +(* defn check_t *) + +check_t_var: forall E_k id . +( Pmap.find id E_k = Ki_typ ) + ==> +check_t E_k (T_var id) + +and +check_t_varInfer: forall E_k id . +( Pmap.find id E_k = Ki_infer ) && +((Formula_update_k E_k id Ki_typ)) + ==> +check_t E_k (T_var id) + +and +check_t_fn: forall E_k t1 t2 effects . +(check_t E_k t1) && +(check_t E_k t2) && +(check_ef E_k effects) + ==> +check_t E_k (T_fn t1 t2 effects) + +and +check_t_tup: forall t_list E_k . +((List.for_all (fun b -> b) ((List.map (fun t_ -> check_t E_k t_) t_list)))) + ==> +check_t E_k (T_tup (t_list)) + +and +check_t_app: forall t_arg_k_list E_k id . +( Pmap.find id E_k = (Ki_ctor ((List.map (fun (t_arg_,k_) -> k_) t_arg_k_list)) Ki_typ) ) && +((List.for_all (fun b -> b) ((List.map (fun (t_arg_,k_) -> check_targs E_k k_ t_arg_) t_arg_k_list)))) + ==> +check_t E_k (T_app id (T_args ((List.map (fun (t_arg_,k_) -> t_arg_) t_arg_k_list)))) + + +and +(* defn check_ef *) + +check_ef_var: forall E_k id . +( Pmap.find id E_k = Ki_efct ) + ==> +check_ef E_k (Effects_aux (Effects_var id) Unknown ) + +and +check_ef_varInfer: forall E_k id . +( Pmap.find id E_k = Ki_infer ) && +((Formula_update_k E_k id Ki_efct)) + ==> +check_ef E_k (Effects_aux (Effects_var id) Unknown ) + +and +check_ef_set: forall efct_list E_k . +true + ==> +check_ef E_k (Effects_aux (Effects_set (efct_list)) Unknown ) + + +and +(* defn check_n *) + +check_n_var: forall E_k id . +( Pmap.find id E_k = Ki_nat ) + ==> +check_n E_k (Ne_var id) + +and +check_n_varInfer: forall E_k id . +( Pmap.find id E_k = Ki_infer ) && +((Formula_update_k E_k id Ki_nat)) + ==> +check_n E_k (Ne_var id) + +and +check_n_num: forall E_k num . +true + ==> +check_n E_k (Ne_const num) + +and +check_n_sum: forall E_k ne1 ne2 . +(check_n E_k ne1) && +(check_n E_k ne2) + ==> +check_n E_k (Ne_add ne1 ne2) + +and +check_n_mult: forall E_k ne1 ne2 . +(check_n E_k ne1) && +(check_n E_k ne2) + ==> +check_n E_k (Ne_mult ne1 ne2) + +and +check_n_exp: forall E_k ne . +(check_n E_k ne) + ==> +check_n E_k (Ne_exp ne) + + +and +(* defn check_ord *) + +check_ord_var: forall E_k id . +( Pmap.find id E_k = Ki_ord ) + ==> +check_ord E_k (Ord_aux (Ord_id id) Unknown ) + +and +check_ord_varInfer: forall E_k id . +( Pmap.find id E_k = Ki_infer ) && +((Formula_update_k E_k id Ki_ord)) + ==> +check_ord E_k (Ord_aux (Ord_id id) Unknown ) + + +and +(* defn check_targs *) + +check_targs_typ: forall E_k t . +(check_t E_k t) + ==> +check_targs E_k Ki_typ (Typ t) + +and +check_targs_eff: forall E_k effects . +(check_ef E_k effects) + ==> +check_targs E_k Ki_efct (Effect effects) + +and +check_targs_nat: forall E_k ne . +(check_n E_k ne) + ==> +check_targs E_k Ki_nat (Nexp ne) + +and +check_targs_ord: forall E_k order . +(check_ord E_k order) + ==> +check_targs E_k Ki_ord (Order order) + + +(** definitions *) + (* defns convert_typ *) +indreln +(* defn convert_typ *) + +convert_typ_var: forall E_k id . +( Pmap.find id E_k = Ki_typ ) + ==> +convert_typ E_k (Typ_aux (Typ_var id) Unknown ) (T_var id) + +and +convert_typ_fn: forall E_k typ1 typ2 effects t1 t2 . +(convert_typ E_k typ1 t1) && +(convert_typ E_k typ2 t2) && +(check_ef E_k effects) + ==> +convert_typ E_k (Typ_aux (Typ_fn typ1 typ2 effects) Unknown ) (T_fn t1 t2 effects) + +and +convert_typ_tup: forall typ_t_list E_k . +((List.for_all (fun b -> b) ((List.map (fun (typ_,t_) -> convert_typ E_k typ_ t_) typ_t_list)))) + ==> +convert_typ E_k (Typ_aux (Typ_tup ((List.map (fun (typ_,t_) -> typ_) typ_t_list))) Unknown ) (T_tup ((List.map (fun (typ_,t_) -> t_) typ_t_list))) + +and +convert_typ_app: forall typ_arg_t_arg_k_list E_k id . +( Pmap.find id E_k = (Ki_ctor ((List.map (fun (typ_arg_,t_arg_,k_) -> k_) typ_arg_t_arg_k_list)) Ki_typ) ) && +((List.for_all (fun b -> b) ((List.map (fun (typ_arg_,t_arg_,k_) -> convert_targ E_k k_ typ_arg_ t_arg_) typ_arg_t_arg_k_list)))) + ==> +convert_typ E_k (Typ_aux (Typ_app id ((List.map (fun (typ_arg_,t_arg_,k_) -> typ_arg_) typ_arg_t_arg_k_list))) Unknown ) (T_app id (T_args ((List.map (fun (typ_arg_,t_arg_,k_) -> t_arg_) typ_arg_t_arg_k_list)))) + +and +convert_typ_eq: forall E_k typ t2 t1 . +(convert_typ E_k typ t1) + ==> +convert_typ E_k typ t2 + + +and +(* defn convert_targ *) + + +(** definitions *) + (* defns check_lit *) +indreln +(* defn check_lit *) + +check_lit_true: forall . +true + ==> +check_lit (L_aux L_true Unknown ) (T_var (Id_aux bool_id Unknown )) + +and +check_lit_false: forall . +true + ==> +check_lit (L_aux L_false Unknown ) (T_var (Id_aux bool_id Unknown )) + +and +check_lit_num: forall num . +true + ==> +check_lit (L_aux (L_num num) Unknown ) (T_var (Id_aux nat_id Unknown )) + +and +check_lit_string: forall string . +true + ==> +check_lit (L_aux (L_string string) Unknown ) (T_var (Id_aux string_id Unknown )) + +and +check_lit_hex: forall hex zero num . +( ( (Ne_const num) = (hlength hex ) ) ) + ==> +check_lit (L_aux (L_hex hex) Unknown ) (T_app (Id_aux vector_id Unknown ) (T_args ([((Nexp (Ne_const zero)))] @ [((Nexp (Ne_const num)))] @ [((Order (Ord_aux Ord_inc Unknown )))] @ [((Typ (T_var (Id_aux bit_id Unknown ))))]))) + +and +check_lit_bin: forall bin zero num . +( ( (Ne_const num) = (blength bin ) ) ) + ==> +check_lit (L_aux (L_bin bin) Unknown ) (T_app (Id_aux vector_id Unknown ) (T_args ([((Nexp (Ne_const zero)))] @ [((Nexp (Ne_const num)))] @ [((Order (Ord_aux Ord_inc Unknown )))] @ [((Typ (T_var (Id_aux bit_id Unknown ))))]))) + +and +check_lit_unit: forall . +true + ==> +check_lit (L_aux L_unit Unknown ) (T_var (Id_aux unit_id Unknown )) + +and +check_lit_bitzero: forall . +true + ==> +check_lit (L_aux L_zero Unknown ) (T_var (Id_aux bit_id Unknown )) + +and +check_lit_bitone: forall . +true + ==> +check_lit (L_aux L_one Unknown ) (T_var (Id_aux bit_id Unknown )) + + +(** definitions *) + (* defns check_pat *) +indreln +(* defn check_pat *) + +check_pat_wild: forall E_k t . +(check_t E_k t) + ==> +(PARSE_ERROR "line 1762 - 1763" "no parses (char 16): <E_t,E_k> |- _ :*** t gives {} ") + +and +check_pat_as: forall E_t E_k pat t E_t1 id . +(check_pat (Env E_k E_t ) pat t E_t1) && +( Pervasives.not (Pmap.mem id E_t1 ) ) + ==> +(PARSE_ERROR "line 1768 - 1769" "no parses (char 26): <E_t,E_k> |- (pat as id) :*** t gives E_t1 u+ {id|->t} ") + +and +check_pat_typ: forall E_k typ t E_t pat E_t1 . +(convert_typ E_k typ t) && +(check_pat (Env E_k E_t ) pat t E_t1) + ==> +(PARSE_ERROR "line 1773 - 1774" "no parses (char 26): <E_t,E_k> |- (<typ> pat) :*** t gives E_t1 ") + +and +check_pat_ident_constr: forall pat_t_E_t_list E_t E_k . +((List.for_all (fun b -> b) ((List.map (fun (pat_,t_,E_t_) -> check_pat (Env E_k E_t ) pat_ t_ E_t_) pat_t_E_t_list)))) + ==> +(PARSE_ERROR "line 1779 - 1780" "no parses (char 36): <E_t,E_k> |- id pat1 .. patn : id t_***args gives E_t1 u+ .. u+ E_tn ") + +and +check_pat_var: forall E_k t . +(check_t E_k t) + ==> +(PARSE_ERROR "line 1783 - 1784" "no parses (char 24): <E_t,E_k> |- :P_id: id :*** t gives E_t u+ {id|->t} ") + +and +check_pat_tup: forall pat_t_E_t_list E_t E_k . +((List.for_all (fun b -> b) ((List.map (fun (pat_,t_,E_t_) -> check_pat (Env E_k E_t ) pat_ t_ E_t_) pat_t_E_t_list)))) && +( disjoint_all (List.map Pmap.domain ((List.map (fun (pat_,t_,E_t_) -> E_t_) pat_t_E_t_list)) ) ) + ==> +(PARSE_ERROR "line 1809 - 1810" "no parses (char 33): <E_t,E_k> |- (pat1, ...., patn) :*** t1 * .... * tn gives E_t1 u+ .... u+ E_tn ") + + +(** definitions *) + (* defns check_exp *) +indreln + + + @@ -109,12 +109,6 @@ quant_item = type -effects_aux = (* effect set, of kind $_$ *) - Effects_var of id - | Effects_set of (efct) list (* effect set *) - - -type order_aux = (* vector order specifications, of kind $_$ *) Ord_id of id (* identifier *) | Ord_inc (* increasing (little-endian) *) @@ -122,19 +116,25 @@ order_aux = (* vector order specifications, of kind $_$ *) type +effects_aux = (* effect set, of kind $_$ *) + Effects_var of id + | Effects_set of (efct) list (* effect set *) + + +type typquant_aux = (* type quantifiers and constraints *) TypQ_tq of (quant_item) list | TypQ_no_forall (* sugar, omitting quantifier and constraints *) type -effects = - Effects_aux of effects_aux * l +order = + Ord_aux of order_aux * l type -order = - Ord_aux of order_aux * l +effects = + Effects_aux of effects_aux * l type @@ -281,6 +281,16 @@ and 'a letbind = type +ne = (* internal numeric expressions *) + Ne_var of id + | Ne_const of int + | Ne_mult of ne * ne + | Ne_add of ne * ne + | Ne_exp of ne + | Ne_unary of ne + + +type naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) Name_sect_none | Name_sect_some of string @@ -309,6 +319,28 @@ rec_opt_aux = (* Optional recursive annotation for functions *) type +k = (* Internal kinds *) + Ki_typ + | Ki_nat + | Ki_ord + | Ki_efct + | Ki_val (* Representing values, for use in identifier checks *) + | Ki_ctor of (k) list * k + | Ki_infer (* Representing an unknown kind, inferred by context *) + + +type +t_arg = (* Argument to type constructors *) + Typ of t + | Nexp of ne + | Effect of effects + | Order of order + +and t_args = (* Arguments to type constructors *) + T_args of (t_arg) list + + +type naming_scheme_opt = Name_sect_aux of naming_scheme_opt_aux * l @@ -344,27 +376,6 @@ rec_opt = type -ne = (* internal numeric expressions *) - Ne_var of id - | Ne_const of int - | Ne_mult of ne * ne - | Ne_add of ne * ne - | Ne_exp of ne - | Ne_unary of ne - - -type -k = (* Internal kinds *) - Ki_typ - | Ki_nat - | Ki_ord - | Ki_efct - | Ki_val (* Representing values, for use in identifier checks *) - | Ki_ctor of (k) list * k - | Ki_infer (* Representing an unknown kind, inferred by context *) - - -type 'a type_def_aux = (* Type definition body *) TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *) | TD_record of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* struct type definition *) @@ -390,17 +401,6 @@ type type -t_arg = (* Argument to type constructors *) - Typ of t - | Nexp of ne - | Effect of effects - | Order of order - -and t_args = (* Arguments to type constructors *) - T_args of (t_arg) list - - -type 'a type_def = TD_aux of 'a type_def_aux * 'a annot @@ -480,5 +480,8 @@ type (** definitions *) (** definitions *) (** definitions *) +(** definitions *) +(** definitions *) +(** definitions *) |