diff options
| -rw-r--r-- | language/l2.ott | 409 | ||||
| -rw-r--r-- | src/ast.ml | 215 |
2 files changed, 329 insertions, 295 deletions
diff --git a/language/l2.ott b/language/l2.ott index 83613080..0fdade39 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -2,7 +2,7 @@ indexvar n , i , j ::= {{ phantom }} {{ com Index variables for meta-lists }} -metavar num ::= +metavar num , zero ::= {{ phantom }} {{ lex numeric }} {{ ocaml int }} @@ -137,7 +137,12 @@ id :: '' ::= % on type variables (or variables of other kinds) % We don't enforce a lexical convention on infix operators, as some of the % targets use alphabetical infix operators. - + | bool :: S :: bool {{ com Built in type identifiers }} {{ icho bool_id }} + | bit :: S :: bit {{ icho bit_id }} + | unit :: S :: unit {{ icho unit_id }} + | nat :: S :: nat {{ icho nat_id }} + | vector :: S :: vector {{ icho vector_id }} + | list :: S :: list {{ icho list_id }} %% %% x_l {{ tex \ottnt{x}^{l} }} , y_l {{ tex \ottnt{y}^{l} }} , z_l {{ tex \ottnt{z}^{l} }} , name :: '' ::= @@ -942,7 +947,7 @@ k :: 'Ki_' ::= t , u :: 'T_' ::= {{ phantom }} {{ com Internal types }} | id :: :: var - | t1 -> t2 :: :: fn + | t1 -> t2 effects :: :: fn | t1 * .... * tn :: :: tup | id t_args :: :: app %% %% | t_subst ( t ) :: M :: subst_app @@ -961,29 +966,26 @@ t , u :: 'T_' ::= {{ phantom }} %% %% {{ hol (FOLDR T_fn [[t]] [[t_multi]]) }} %% %% {{ lem (List.fold_right T_fn [[t_multi]] [[t]]) }} %% %% -%% %% ne :: 'Ne_' ::= -%% %% {{ com internal numeric expressions }} -%% %% | N :: :: var -%% %% | nat :: :: const -%% %% | ne1 * ne2 :: :: mult -%% %% | ne1 + ne2 :: :: add -%% %% | ( - ne ) :: :: unary -%% %% | normalize ( ne ) :: M :: normalize -%% %% {{ ocaml (assert false) }} -%% %% {{ hol ARB }} -%% %% {{ lem (normalize [[ne]] ) }} +ne :: 'Ne_' ::= + {{ com internal numeric expressions }} + | id :: :: var + | num :: :: const + | ne1 * ne2 :: :: mult + | ne1 + ne2 :: :: add + | 2 ** ne :: :: exp + | ( - ne ) :: :: unary %% %% | ne1 + ... + nen :: M :: addmany %% %% {{ ocaml (assert false) }} %% %% {{ hol ARB }} %% %% {{ lem (sumation_nes [[ne1...nen]]) }} -%% %% | bitlength ( bin ) :: M :: cbin -%% %% {{ ocaml (asssert false) }} -%% %% {{ hol ARB }} -%% %% {{ lem (blength [[bin]]) }} -%% %% | bitlength ( hex ) :: M :: chex -%% %% {{ ocaml (assert false) }} -%% %% {{ hol ARB }} -%% %% {{ lem (hlength [[hex]]) }} + | bitlength ( bin ) :: M :: cbin + {{ ocaml (asssert false) }} + {{ hol ARB }} + {{ lem (blength [[bin]]) }} + | bitlength ( hex ) :: M :: chex + {{ ocaml (assert false) }} + {{ hol ARB }} + {{ lem (hlength [[hex]]) }} %% %% | length ( pat1 ... patn ) :: M :: cpat %% %% {{ ocaml (assert false) }} %% %% {{ hol ARB }} @@ -993,29 +995,17 @@ t , u :: 'T_' ::= {{ phantom }} %% %% {{ ocaml (assert false) }} %% %% {{ lem (Ne_const (List.length [[exp1...expn]])) }} %% %% -%% %% t_args :: '' ::= -%% %% {{ com Lists of types }} -%% %% | t1 .. tn :: :: T_args -%% %% | t_subst ( t_args ) :: M :: T_args_subst_app -%% %% {{ com Multiple substitutions }} -%% %% {{ ocaml (assert false) }} -%% %% {{ hol (t_subst_t_args [[t_subst]] [[t_args]]) }} -%% %% {{ lem (t_subst_t_args [[t_subst]] [[t_args]]) }} -%% %% -%% %% t_multi :: '' ::= {{ phantom }} -%% %% {{ hol t list }} -%% %% {{ ocaml t list }} -%% %% {{ lem list t }} -%% %% {{ com Lists of types }} -%% %% | ( t1 * .. * tn ) :: :: T_multi -%% %% {{ hol [[t1..tn]] }} -%% %% {{ lem [[t1..tn]] }} -%% %% | t_subst ( t_multi ) :: M :: T_multi_subst_app -%% %% {{ com Multiple substitutions }} -%% %% {{ ocaml (assert false) }} -%% %% {{ hol (MAP (t_subst_t [[t_subst]]) [[t_multi]]) }} -%% %% {{ lem (List.map (t_subst_t [[t_subst]]) [[t_multi]]) }} -%% %% + t_arg :: '' ::= + {{ com Argument to type constructors }} + | t :: :: typ + | ne :: :: nexp + | effects :: :: effect + | order :: :: order + + t_args :: '' ::= + {{ com Arguments to type constructors }} + | t_arg1 ... t_argn :: :: T_args + %% %% nec :: '' ::= %% %% {{ com Numeric expression constraints }} %% %% | ne < nec :: :: lessthan @@ -1291,6 +1281,14 @@ terminals :: '' ::= {{ tex \ensuremath{\rangle} }} | |- :: :: vdash {{ tex \ensuremath{\vdash} }} + | |-t :: :: vdashT + {{ tex \ensuremath{\vdash_t} }} + | |-n :: :: vdashN + {{ tex \ensuremath{\vdash_n} }} + | |-t :: :: vdashE + {{ tex \ensuremath{\vdash_e} }} + | |-t :: :: vdashO + {{ tex \ensuremath{\vdash_o} }} | ' :: :: quote {{ tex \mbox{'} }} | |-> :: :: mapsto @@ -1322,6 +1320,9 @@ formula :: formula_ ::= {{ hol (FLOOKUP [[E_t]] [[id]] = SOME [[t]]) }} {{ lem Pmap.find [[id]] [[E_t]] = [[t]] }} + | E_k ( id ) <-| k :: :: update_k + {{ com Update the kind associated with id to k }} + %% %% % | TD ( p ) gives tc_def :: :: lookup_tc %% %% % {{ com Type constructor lookup }} %% %% % {{ hol (FLOOKUP [[TD]] [[p]] = SOME [[tc_def]]) }} @@ -1390,18 +1391,15 @@ formula :: formula_ ::= %% %% {{ hol (~?__semC__. MEM (Inst __semC__ [[p]] [[t]]) [[I]]) }} %% %% {{ lem (Pervasives.not ((Inst [] [[p]] [[t]]) IN [[I]])) }} %% %% -%% %% | E_l1 = E_l2 :: :: E_l_eqn -%% %% {{ ichl ([[E_l1]] = [[E_l2]]) }} -%% %% -%% %% | E_x1 = E_x2 :: :: E_x_eqn -%% %% {{ ichl ([[E_x1]] = [[E_x2]]) }} -%% %% -%% %% | E_f1 = E_f2 :: :: E_f_eqn -%% %% {{ ichl ([[E_f1]] = [[E_f2]]) }} -%% %% -%% %% | E1 = E2 :: :: E_eqn -%% %% {{ ichl ([[E1]] = [[E2]]) }} -%% %% + | E_k1 = E_k2 :: :: E_k_eqn + {{ ichl ([[E_k1]] = [[E_k2]]) }} + + | E_t1 = E_t2 :: :: E_f_eqn + {{ ichl ([[E_t1]] = [[E_t2]]) }} + + | E1 = E2 :: :: E_eqn + {{ ichl ([[E1]] = [[E2]]) }} + %% %% | TD1 = TD2 :: :: TD_eqn %% %% {{ ichl ([[TD1]] = [[TD2]]) }} %% %% @@ -1414,8 +1412,10 @@ formula :: formula_ ::= %% %% | names1 = names2 :: :: names_eq %% %% {{ ichl ([[names1]] = [[names2]]) }} %% %% -%% %% | t1 = t2 :: :: t_eq -%% %% {{ ichl ([[t1]] = [[t2]]) }} + | t1 = t2 :: :: t_eq + {{ ichl ([[t1]] = [[t2]]) }} + | ne1 = ne2 :: :: ne_eq + {{ ichl ([[ne1]] = [[ne2]]) }} %% %% %% %% | t_subst1 = t_subst2 :: :: t_subst_eq %% %% {{ ichl ([[t_subst1]] = [[t_subst2]]) }} @@ -1439,109 +1439,123 @@ formula :: formula_ ::= defns translate_ast :: '' ::= -%% % -%% % -%% % defns -%% % convert_tnvars :: '' ::= -%% % -%% % defn -%% % tnvars ~> tnvs :: :: convert_tnvars :: convert_tnvars_ -%% % by -%% % -%% % :convert_tnvar: tnvar1 ~> tnv1 .. :convert_tnvar: tnvarn ~> tnvn -%% % ------------------------------------------------------------ :: none -%% % tnvar1 .. tnvarn ~> tnv1 .. tnvn -%% % -%% % defn -%% % tnvar ~> tnv :: :: convert_tnvar :: convert_tnvar_ -%% % by -%% % -%% % ----------------------------------------------------------- :: a -%% % a l ~> a -%% % -%% % ---------------------------------------------------------- :: N -%% % N l ~> N -%% % -%% % -%% % defns -%% % look_m :: '' ::= -%% % -%% % defn -%% % E1 ( x_l1 .. x_ln ) gives E2 :: :: look_m :: look_m_ -%% % {{ com Name path lookup }} -%% % by -%% % -%% % ------------------------------------------------------------ :: none -%% % E() gives E -%% % -%% % E_m(x) gives E1 -%% % E1(</y_li//i/>) gives E2 -%% % ------------------------------------------------------------ :: some -%% % <E_m,E_p,E_f,E_x>(x l </y_li//i/>) gives E2 -%% % -%% % defns -%% % look_m_id :: '' ::= -%% % -%% % defn -%% % E1 ( id ) gives E2 :: :: look_m_id :: look_m_id_ -%% % {{ com Module identifier lookup }} -%% % by -%% % -%% % E1(</y_li//i/> x l1) gives E2 -%% % ------------------------------------------------------------ :: all -%% % E1(</y_li.//i/> x l1 l2) gives E2 -%% % -%% % defns -%% % look_tc :: '' ::= -%% % -%% % defn -%% % E ( id ) gives p :: :: look_tc :: look_tc_ -%% % {{ com Path identifier lookup }} -%% % by -%% % -%% % E(</y_li//i/>) gives <E_m,E_p,E_f,E_x> -%% % E_p(x) gives p -%% % ------------------------------------------------------------ :: all -%% % E(</y_li.//i/> x l1 l2) gives p -%% % -%% % -%% % defns -%% % check_t :: '' ::= -%% % -%% % defn -%% % TD |- t ok :: :: check_t :: check_t_ -%% % {{ com Well-formed types }} -%% % by -%% % -%% % ------------------------------------------------------------ :: var -%% % TD |- a ok -%% % -%% % TD |- t1 ok -%% % TD |- t2 ok -%% % ------------------------------------------------------------ :: fn -%% % TD |- t1 -> t2 ok -%% % -%% % TD |- t1 ok .... TD |- tn ok -%% % ------------------------------------------------------------ :: tup -%% % TD |- t1 * .... * tn ok -%% % -%% % TD(p) gives tnv1..tnvn tc_abbrev -%% % TD,tnv1 |- t1 ok .. TD,tnvn |- tn ok -%% % ------------------------------------------------------------ :: app -%% % TD |- p t1 .. tn ok -%% % -%% % -%% % defn -%% % TD , tnv |- t ok :: :: check_tlen :: check_tlen_ -%% % {{ com Well-formed type/nexps matching the application type variable }} -%% % by -%% % -%% % TD |- t ok -%% % ------------------------------------------------------------ :: t -%% % TD,a |- t ok -%% % -%% % ------------------------------------------------------------ :: len -%% % TD,N |- ne ok +defns +check_t :: '' ::= + +defn +E_k |-t t ok :: :: check_t :: check_t_ + {{ com Well-formed types }} + by + + E_k(id) gives K_Typ + ------------------------------------------------------------ :: var + E_k |-t id ok + + E_k(id) gives K_infer + E_k(id) <-| K_Typ + ------------------------------------------------------------ :: varInfer + E_k |-t id ok + + E_k |-t t1 ok + E_k |-t t2 ok + E_k |-e effects ok + ------------------------------------------------------------ :: fn + E_k |-t t1 -> t2 effects ok + + E_k |-t t1 ok .... E_k |-t tn ok + ------------------------------------------------------------ :: tup + E_k |-t t1 * .... * tn ok + + E_k(id) gives K_Lam(k1..kn -> K_Typ) + E_k,k1 |- t_arg1 ok .. E_k,kn |- t_argn ok + ------------------------------------------------------------ :: app + E_k |-t id t_arg1 .. t_argn ok + +defn +E_k |-e effects ok :: :: check_ef :: check_ef_ +{{ com Well-formed effects }} +by + +E_k(id) gives K_Efct +----------------------------------------------------------- :: var +E_k |-e effect id ok + +E_k(id) gives K_infer +E_k(id) <-| K_Efct +------------------------------------------------------------ :: varInfer +E_k |-e effect id ok + +------------------------------------------------------------- :: set +E_k |-e effect { efct1 , .. , efctn } ok + +defn +E_k |-n ne ok :: :: check_n :: check_n_ +{{ com Well-formed numeric expressions }} +by + +E_k(id) gives K_Nat +----------------------------------------------------------- :: var +E_k |-n id ok + +E_k(id) gives K_infer +E_k(id) <-| K_Nat +------------------------------------------------------------ :: varInfer +E_k |-n id ok + +----------------------------------------------------------- :: num +E_k |-n num ok + +E_k |-n ne1 ok +E_k |-n ne2 ok +----------------------------------------------------------- :: sum +E_k |-n ne1 + ne2 ok + +E_k |-n ne1 ok +E_k |-n ne2 ok +------------------------------------------------------------ :: mult +E_k |-n ne1 * ne2 ok + +E_k |-n ne ok +------------------------------------------------------------ :: exp +E_k |-n 2 ** ne ok + +defn +E_k |-o order ok :: :: check_ord :: check_ord_ +{{ com Well-formed numeric expressions }} +by + +E_k(id) gives K_Ord +----------------------------------------------------------- :: var +E_k |-o id ok + + E_k(id) gives K_infer + E_k(id) <-| K_Ord + ------------------------------------------------------------ :: varInfer + E_k |-o id ok + + +defn +E_k , k |- t_arg ok :: :: check_targs :: check_targs_ +{{ com Well-formed type arguments kind check matching the application type variable }} +by + +E_k |-t t ok +--------------------------------------------------------- :: typ +E_k , K_Typ |- t ok + +E_k |-e effects ok +--------------------------------------------------------- :: eff +E_k , K_Efct |- effects ok + +E_k |-n ne ok +--------------------------------------------------------- :: nat +E_k , K_Nat |- ne ok + +E_k |-o order ok +--------------------------------------------------------- :: ord +E_k, K_Ord |- order ok + + %% % %% % %TODO type equality isn't right; neither is type conversion %% % @@ -1666,43 +1680,40 @@ translate_ast :: '' ::= %% % ------------------------------------------------------------ :: all %% % TD,E |- typ1 * .. * typn ~> (t1 * .. * tn) %% % -%% % defns -%% % check_lit :: '' ::= -%% % -%% % defn -%% % |- lit : t :: :: check_lit :: check_lit_ -%% % {{ com Typing literal constants }} -%% % by -%% % -%% % ------------------------------------------------------------ :: true -%% % |- true l : __bool -%% % -%% % ------------------------------------------------------------ :: false -%% % |- false l : __bool -%% % -%% % ------------------------------------------------------------ :: num -%% % |- num l : __num -%% % -%% % nat = bitlength(hex) -%% % ------------------------------------------------------------ :: hex -%% % |- hex l : __vector nat __bit -%% % -%% % nat = bitlength(bin) -%% % ------------------------------------------------------------ :: bin -%% % |- bin l : __vector nat __bit -%% % -%% % ------------------------------------------------------------ :: string -%% % |- string l : __string -%% % -%% % ------------------------------------------------------------ :: unit -%% % |- () l : __unit -%% % -%% % ------------------------------------------------------------ :: bitzero -%% % |- bitzero l : __bit -%% % -%% % ------------------------------------------------------------ :: bitone -%% % |- bitone l : __bit -%% % +defns +check_lit :: '' ::= + +defn +|- lit : t :: :: check_lit :: check_lit_ +{{ com Typing literal constants }} +by + + ------------------------------------------------------------ :: true + |- true : bool + + ------------------------------------------------------------ :: false + |- false : bool + + ------------------------------------------------------------ :: num + |- num : nat + + num = bitlength(hex) + ------------------------------------------------------------ :: hex + |- hex : vector zero num inc bit + + num = bitlength(bin) + ------------------------------------------------------------ :: bin + |- bin : vector zero num inc bit + + ------------------------------------------------------------ :: unit + |- () : unit + + ------------------------------------------------------------ :: bitzero + |- bitzero : bit + + ------------------------------------------------------------ :: bitone + |- bitone : bit + %% % %% % defns %% % inst_field :: '' ::= @@ -20,19 +20,14 @@ base_kind_aux = (* base kind *) type -base_kind = - BK_aux of base_kind_aux * l - - -type id_aux = (* Identifier *) Id of x | DeIid of x (* remove infix status *) type -kind_aux = (* kinds *) - K_kind of (base_kind) list +base_kind = + BK_aux of base_kind_aux * l type @@ -41,8 +36,8 @@ id = type -kind = - K_aux of kind_aux * l +kind_aux = (* kinds *) + K_kind of (base_kind) list type @@ -58,9 +53,8 @@ and nexp = type -kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) +kind = + K_aux of kind_aux * l type @@ -72,6 +66,22 @@ nexp_constraint_aux = (* constraint over kind $_$ *) 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 *) @@ -83,13 +93,9 @@ efct_aux = (* effect *) type -kinded_id = - KOpt_aux of kinded_id_aux * l - - -type -nexp_constraint = - NC_aux of nexp_constraint_aux * l +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 @@ -98,9 +104,8 @@ efct = 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 *) +quant_item = + QI_aux of quant_item_aux * l type @@ -117,8 +122,9 @@ order_aux = (* vector order specifications, of kind $_$ *) type -quant_item = - QI_aux of quant_item_aux * l +typquant_aux = (* type quantifiers and constraints *) + TypQ_tq of (quant_item) list + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) type @@ -132,22 +138,8 @@ order = type -typquant_aux = (* type quantifiers and constraints *) - TypQ_tq of (quant_item) list - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) - - -type -lit_aux = (* Literal constant *) - L_unit (* $() : _$ *) - | L_zero (* $_ : _$ *) - | L_one (* $_ : _$ *) - | L_true (* $_ : _$ *) - | L_false (* $_ : _$ *) - | L_num of int (* 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 *) +typquant = + TypQ_aux of typquant_aux * l type @@ -172,8 +164,21 @@ and typ_arg = type -typquant = - TypQ_aux of typquant_aux * l +lit_aux = (* Literal constant *) + L_unit (* $() : _$ *) + | L_zero (* $_ : _$ *) + | L_one (* $_ : _$ *) + | L_true (* $_ : _$ *) + | L_false (* $_ : _$ *) + | L_num of int (* 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 +typschm_aux = (* type scheme *) + TypSchm_ts of typquant * typ type @@ -182,8 +187,8 @@ lit = type -typschm_aux = (* type scheme *) - TypSchm_ts of typquant * typ +typschm = + TypSchm_aux of typschm_aux * l type @@ -212,11 +217,6 @@ and 'a fpat = type -typschm = - TypSchm_aux of typschm_aux * l - - -type 'a exp_aux = (* Expression *) E_block of ('a exp) list (* block (parsing conflict with structs?) *) | E_id of id (* identifier *) @@ -281,19 +281,19 @@ and 'a letbind = type -rec_opt_aux = (* Optional recursive annotation for functions *) - Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) +naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of string type -'a funcl_aux = (* Function clause *) - FCL_Funcl of id * 'a pat * 'a exp +'a tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_some of typquant * typ type -'a tannot_opt_aux = (* Optional type annotation for functions *) - Typ_annot_opt_some of typquant * typ +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * 'a exp type @@ -303,19 +303,24 @@ type type -naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - Name_sect_none - | Name_sect_some of string +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) type -rec_opt = - Rec_aux of rec_opt_aux * l +naming_scheme_opt = + Name_sect_aux of naming_scheme_opt_aux * l type -'a funcl = - FCL_aux of 'a funcl_aux * 'a annot +index_range_aux = (* index specification, for bitfields in register types *) + BF_single of int (* single index *) + | BF_range of int * int (* index range *) + | BF_concat of index_range * index_range (* concatenation of index ranges *) + +and index_range = + BF_aux of index_range_aux * l type @@ -324,33 +329,48 @@ type type +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot + + +type 'a effects_opt = Effects_opt_aux of 'a effects_opt_aux * 'a annot type -index_range_aux = (* index specification, for bitfields in register types *) - BF_single of int (* single index *) - | BF_range of int * int (* index range *) - | BF_concat of index_range * index_range (* concatenation of index ranges *) - -and index_range = - BF_aux of index_range_aux * l +rec_opt = + Rec_aux of rec_opt_aux * l type -naming_scheme_opt = - Name_sect_aux of naming_scheme_opt_aux * l +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 -'a fundef_aux = (* Function definition *) - FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list +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 val_spec_aux = (* Value type specification *) - VS_val_spec of typschm * id +'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 *) + | TD_variant of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* union type definition *) + | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *) + | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) type @@ -360,22 +380,29 @@ type 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 *) - | TD_variant of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* union type definition *) - | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *) - | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) +'a fundef_aux = (* Function definition *) + FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list type -'a fundef = - FD_aux of 'a fundef_aux * 'a annot +'a val_spec_aux = (* Value type specification *) + VS_val_spec of typschm * id type -'a val_spec = - VS_aux of 'a val_spec_aux * 'a annot +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 type @@ -384,19 +411,13 @@ type type -'a type_def = - TD_aux of 'a type_def_aux * 'a annot +'a fundef = + FD_aux of 'a fundef_aux * 'a annot 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 *) +'a val_spec = + VS_aux of 'a val_spec_aux * 'a annot type @@ -457,5 +478,7 @@ type Defs of ('a def) list (** definitions *) +(** definitions *) +(** definitions *) |