summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--language/Makefile4
-rw-r--r--language/l2.ott276
-rw-r--r--src/ast.lem744
-rw-r--r--src/ast.ml87
4 files changed, 902 insertions, 209 deletions
diff --git a/language/Makefile b/language/Makefile
index 4ec85aa1..6611f48f 100644
--- a/language/Makefile
+++ b/language/Makefile
@@ -11,9 +11,9 @@ l2_parse.pdf: l2_parse.tex
l2Theory.uo: l2Script.sml
Holmake --qof -I $(OTTLIB) l2Theory.uo
-l2.tex ../src/ast.ml l2Script.sml: l2.ott
+l2.tex ../src/ast.ml ../src/ast.lem 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 -o ../src/ast.ml -o l2Script.sml -picky_multiple_parses true l2.ott
+ ott -sort false -generate_aux_rules true -o ../src/ast.ml -o ../src/ast.lem -o l2Script.sml -picky_multiple_parses true l2.ott
l2_parse.tex parse_ast.ml ../src/parse_ast.ml: l2_parse.ott
ott -sort false -generate_aux_rules false -o l2_parse.tex -picky_multiple_parses true l2_parse.ott
diff --git a/language/l2.ott b/language/l2.ott
index 0fdade39..d65a3984 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -10,14 +10,6 @@ metavar num , zero ::=
{{ lem num }}
{{ com Numeric literals }}
-% metavar nat ::=
-% {{ phantom }}
-% {{ lex numeric }}
-% {{ ocaml int }}
-% {{ hol num }}
-% {{ lem num }}
-% {{ com Internal literal numbers }}
-
metavar hex ::=
{{ phantom }}
{{ lex numeric }}
@@ -137,49 +129,17 @@ 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 }}
+ | bool :: M :: bool {{ com Built in type identifiers }} {{ ichlo bool_id }}
+ | bit :: M :: bit {{ ichlo bit_id }}
+ | unit :: M :: unit {{ ichlo unit_id }}
+ | nat :: M :: nat {{ ichlo nat_id }}
+ | string :: M :: string {{ ichlo string_id }}
+ | enum :: M :: enum {{ ichlo enum_id }}
+ | vector :: M :: vector {{ ichlo vector_id }}
+ | list :: M :: list {{ ichlo list_id }}
+ | set :: M :: set {{ ichlo set_id }}
+ | reg :: M :: reg {{ ichlo reg_id }}
-%%
-%% x_l {{ tex \ottnt{x}^{l} }} , y_l {{ tex \ottnt{y}^{l} }} , z_l {{ tex \ottnt{z}^{l} }} , name :: '' ::=
-%% {{ com Location-annotated names }}
-%% | x l :: :: X_l
-%% | ( ix ) l :: :: PreX_l
-%% {{ com Remove infix status }}
-%%
-%% ix_l {{ tex \ottnt{ix}^{l} }} :: '' ::=
-%% {{ com Location-annotated infix names }}
-%% | ix l :: :: SymX_l
-%% | ` x ` l :: :: InX_l
-%% {{ com Add infix status }}
-%%
-%% embed
-%% {{ ocaml
-%% let xl_to_l = function
-%% | X_l(_,l) -> l
-%% | PreX_l(_,_,_,l) -> l
-%%
-%% let ixl_to_l = function
-%% | SymX_l(_,l) -> l
-%% | InX_l(_,_,_,l) -> l
-%% }}
-%% {{ lem
-%%
-%% (*let xl_to_l = function
-%% | X_l(_,l) -> l
-%% | PreX_l(_,_,l) -> l
-%% end
-%%
-%% let ixl_to_l = function
-%% | SymX_l(_,l) -> l
-%% | InX_l(_,_,_,l) -> l
-%% end*)
-%%
-%% }}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Kinds and Types %
@@ -280,7 +240,7 @@ nexp :: 'Nexp_' ::=
%{{ com must be linear after normalisation... except for the type of *, ahem }}
| nexp1 + nexp2 :: :: sum {{ com sum }}
| 2 ** nexp :: :: exp {{ com exponential }}
- | ( nexp ) :: S :: paren {{ icho [[nexp]] }}
+ | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }}
order :: 'Ord_' ::=
{{ com vector order specifications, of kind $[[Order]]$}}
@@ -288,7 +248,7 @@ order :: 'Ord_' ::=
| id :: :: id {{ com identifier }}
| inc :: :: inc {{ com increasing (little-endian) }}
| dec :: :: dec {{ com decreasing (big-endian) }}
- | ( order ) :: S :: paren {{ icho [[order]] }}
+ | ( order ) :: S :: paren {{ ichlo [[order]] }}
efct :: 'Effect_' ::=
{{ com effect }}
@@ -307,7 +267,7 @@ effects :: 'Effects_' ::=
{{ aux _ l }}
| effect id :: :: var
| effect { efct1 , .. , efctn } :: :: set {{ com effect set }}
- | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }}
+ | pure :: M :: pure {{ com sugar for empty effect set }} {{ ichlo [] }}
% TODO: are we going to need any effect polymorphism? Conceivably for built-in maps and folds. Yes. But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}.
@@ -327,7 +287,7 @@ typ :: 'Typ_' ::=
% TODO union in the other kind grammars? or make a syntax of argument? or glom together the grammars and leave o the typechecker
| id typ_arg1 .. typ_argn :: :: app
{{ com type constructor application }}
- | ( typ ) :: S :: paren {{ icho [[typ]] }}
+ | ( typ ) :: S :: paren {{ ichlo [[typ]] }}
typ_arg :: 'Typ_arg_' ::=
{{ com Type constructor arguments of all kinds }}
@@ -638,12 +598,12 @@ exp :: 'E_' ::=
| if exp1 then exp2 else exp3 :: :: if
{{ com conditional }}
- | if exp1 then exp2 :: S :: ifnoelse {{ icho [[ if exp1 then exp2 else unit ]] }}
+ | if exp1 then exp2 :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }}
| foreach id from exp1 to exp2 by exp3 exp4 :: :: for {{ com loop }}
- | foreach id from exp1 to exp2 exp3 :: S :: forbyone {{ icho [[ foreach id from exp1 to exp2 by 1 exp4 ]] }}
- | foreach id from exp1 downto exp2 by exp3 exp4 :: S :: fordown {{ icho [[ foreach id from exp1 to exp2 by ( - exp3 ) exp4 ]] }}
- | foreach id from exp1 downto exp2 exp3 :: S :: fordownbyone {{ icho [[ foreach id from exp1 downto exp2 by 1 exp4 ]] }}
+ | foreach id from exp1 to exp2 exp3 :: S :: forbyone {{ ichlo [[ foreach id from exp1 to exp2 by 1 exp4 ]] }}
+ | foreach id from exp1 downto exp2 by exp3 exp4 :: S :: fordown {{ ichlo [[ foreach id from exp1 to exp2 by ( - exp3 ) exp4 ]] }}
+ | foreach id from exp1 downto exp2 exp3 :: S :: fordownbyone {{ ichlo [[ foreach id from exp1 downto exp2 by 1 exp4 ]] }}
% vectors
| [ exp1 , ... , expn ] :: :: vector {{ com vector (indexed from 0) }}
@@ -1285,9 +1245,9 @@ terminals :: '' ::=
{{ tex \ensuremath{\vdash_t} }}
| |-n :: :: vdashN
{{ tex \ensuremath{\vdash_n} }}
- | |-t :: :: vdashE
+ | |-e :: :: vdashE
{{ tex \ensuremath{\vdash_e} }}
- | |-t :: :: vdashO
+ | |-o :: :: vdashO
{{ tex \ensuremath{\vdash_o} }}
| ' :: :: quote
{{ tex \mbox{'} }}
@@ -1340,11 +1300,11 @@ formula :: formula_ ::=
{{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }}
{{ lem disjoint (Pmap.domain [[E_f1]]) (Pmap.domain [[E_f2]]) }}
-%% %% | disjoint doms ( E_x1 , .... , E_xn ) :: :: E_x_disjoint_many
-%% %% {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM
-%% %% E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_x1....E_xn]] <> NONE) }}
-%% %% {{ lem disjoint_all (List.map Pmap.domain [[E_x1 .... E_xn]]) }}
-%% %% {{ com Pairwise disjoint domains }}
+ | disjoint doms ( E_t1 , .... , E_tn ) :: :: E_x_disjoint_many
+ {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM
+ E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_t1....E_tn]] <> NONE) }}
+ {{ lem disjoint_all (List.map Pmap.domain [[E_t1 .... E_tn]]) }}
+ {{ com Pairwise disjoint domains }}
%% %%
%% %% | compatible overlap ( x1 |-> t1 , .. , xn |-> tn ) :: :: E_l_compat
%% %% {{ hol (!__n __m. MEM __m [[x1 t1 .. xn tn]] /\ MEM __n [[x1 t1..xn tn]] /\ (FST __m = FST __n) ==> (SND __m = SND __n)) }}
@@ -1363,9 +1323,9 @@ formula :: formula_ ::=
{{ hol ([[id]] NOTIN FDOM [[E_k]]) }}
{{ lem Pervasives.not (Pmap.mem [[id]] [[E_k]]) }}
-%% %% | x NOTIN dom ( E_f ) :: :: notin_dom_f
-%% %% {{ hol ([[x]] NOTIN FDOM [[E_f]]) }}
-%% %% {{ lem Pervasives.not (Pmap.mem [[x]] [[E_f]]) }}
+ | id NOTIN dom ( E_t ) :: :: notin_dom_t
+ {{ hol ([[id]] NOTIN FDOM [[E_t]]) }}
+ {{ lem Pervasives.not (Pmap.mem [[id]] [[E_t]]) }}
%% %%
%% %%
%% %% | FV ( t ) SUBSET tnvs :: :: FV_t
@@ -1603,52 +1563,44 @@ E_k, K_Ord |- order ok
%% % TD |- ne = ne'
%% %
%% %
-%% % defns
-%% % convert_typ :: '' ::=
-%% %
-%% % defn
-%% % TD , E |- typ ~> t :: :: convert_typ :: convert_typ_
-%% % {{ com Convert source types to internal types }}
-%% % by
-%% %
-%% % % TODO : Can't allow things like type t = _, but it's useful to have things
-%% % % like f (x : (_, int)) = snd x
-%% % %TD |- t ok
-%% % %------------------------------------------------------------ :: wild
-%% % %TD,E |- _ l ~> t
-%% %
-%% % ------------------------------------------------------------ :: var
-%% % TD,E |- a l' l ~> a
-%% %
-%% % TD,E |- typ1 ~> t1
-%% % TD,E |- typ2 ~> t2
-%% % ------------------------------------------------------------ :: fn
-%% % TD,E |- typ1->typ2 l ~> t1->t2
-%% %
-%% % TD,E |- typ1 ~> t1 .... TD,E |- typn ~> tn
-%% % ------------------------------------------------------------ :: tup
-%% % TD,E |- typ1 * .... * typn l ~> t1 * .... * tn
-%% %
-%% % TD,E |- typ1 ~> t1 .. TD,E |- typn ~> tn
-%% % E(id) gives p
-%% % TD(p) gives a1..an tc_abbrev
-%% % ------------------------------------------------------------ :: app
-%% % TD,E |- id typ1 .. typn l ~> p t1 .. tn
-%% %
-%% % |- nexp ~> ne
-%% % ------------------------------------------------------------ :: nexp
-%% % TD,E |- nexp ~> ne
-%% %
-%% % TD,E |- typ ~> t
-%% % ------------------------------------------------------------ :: paren
-%% % TD,E |- (typ) l ~> t
-%% %
-%% %
-%% % TD,E |- typ ~> t1
-%% % TD |- t1 = t2
-%% % ------------------------------------------------------------ :: eq
-%% % TD,E |- typ ~> t2
-%% %
+
+defns
+convert_typ :: '' ::=
+
+defn
+E_k |- typ ~> t :: :: convert_typ :: convert_typ_
+{{ com Convert source types to internal types }}
+by
+
+E_k(id) gives K_Typ
+------------------------------------------------------------ :: var
+E_k |- :Typ_var: id ~> id
+
+E_k |- typ1 ~> t1
+E_k |- typ2 ~> t2
+E_k |-e effects ok
+------------------------------------------------------------ :: fn
+E_k |- typ1->typ2 effects ~> t1->t2 effects
+
+E_k |- typ1 ~> t1 .... E_k |- typn ~> tn
+------------------------------------------------------------ :: tup
+E_k |- typ1 * .... * typn ~> t1 * .... * tn
+
+E_k(id) gives K_Lam (k1..kn -> K_Typ)
+E_k,k1 |- typ_arg1 ~> t_arg1 .. E_k,kn |- typ_argn ~> t_argn
+------------------------------------------------------------ :: app
+E_k |- id typ_arg1 .. typ_argn ~> id t_arg1 .. t_argn
+
+E_k |- typ ~> t1
+%E_k |- t1 = t2
+------------------------------------------------------------ :: eq
+E_k |- typ ~> t2
+
+defn
+E_k , k |- typ_arg ~> t_arg :: :: convert_targ :: convert_targ_
+{{ com Convert source type arguments to internals }}
+by
+
%% % defn
%% % |- nexp ~> ne :: :: convert_nexp :: convert_nexp_
%% % {{ com Convert and normalize numeric expressions }}
@@ -1697,13 +1649,16 @@ by
------------------------------------------------------------ :: num
|- num : nat
+ ------------------------------------------------------------- :: string
+ |- string : string
+
num = bitlength(hex)
------------------------------------------------------------ :: hex
- |- hex : vector zero num inc bit
+ |- hex : vector zero num inc :T_var: bit
num = bitlength(bin)
------------------------------------------------------------ :: bin
- |- bin : vector zero num inc bit
+ |- bin : vector zero num inc :T_var: bit
------------------------------------------------------------ :: unit
|- () : unit
@@ -1794,48 +1749,39 @@ by
%% % E_l |- x_l1. .. x_ln.y_l.z_l l not shadowed
%% %
%% %
-%% % defns
-%% % check_pat :: '' ::=
-%% %
-%% % defn
-%% % TD , E , E_l1 |- pat : t gives E_l2 :: :: check_pat :: check_pat_
-%% % {{ com Typing patterns, building their binding environment }}
-%% % by
-%% %
-%% % :check_pat_aux: TD,E,E_l1 |- pat_aux : t gives E_l2
-%% % ------------------------------------------------------------ :: all
-%% % TD,E,E_l1 |- pat_aux l : t gives E_l2
-%% %
-%% % defn
-%% % TD , E , E_l1 |- pat_aux : t gives E_l2 :: :: check_pat_aux :: check_pat_aux_
-%% % {{ com Typing patterns, building their binding environment }}
-%% % by
-%% %
-%% % TD |- t ok
-%% % ------------------------------------------------------------ :: wild
-%% % TD,E,E_l |- _ : t gives {}
-%% %
-%% % TD,E,E_l1 |- pat : t gives E_l2
-%% % x NOTIN dom(E_l2)
-%% % ------------------------------------------------------------ :: as
-%% % TD,E,E_l1 |- (pat as x l) : t gives E_l2 u+ {x|->t}
-%% %
-%% % TD,E,E_l1 |- pat : t gives E_l2
-%% % TD,E |- typ ~> t
-%% % ------------------------------------------------------------ :: typ
-%% % TD,E,E_l1 |- (pat : typ) : t gives E_l2
-%% %
+defns
+check_pat :: '' ::=
+
+defn
+E |- pat : t gives E_t :: :: check_pat :: check_pat_
+{{ com Typing patterns, building their binding environment }}
+by
+
+E_k |-t t ok
+------------------------------------------------------------ :: wild
+<E_t,E_k> |- _ : t gives {}
+% This case should perhaps indicate the generation of a type variable, with kind Typ
+
+<E_t,E_k> |- pat : t gives E_t1
+id NOTIN dom(E_t1)
+------------------------------------------------------------ :: as
+<E_t,E_k> |- (pat as id) : t gives E_t1 u+ {id|->t}
+
+E_k |- typ ~> t
+<E_t,E_k> |- pat : t gives E_t1
+------------------------------------------------------------ :: typ
+<E_t,E_k> |- (<typ> pat) : t gives E_t1
+
%% % TD,E |- ctor id : (t1*..*tn) -> p t_args gives (x of names)
-%% % E_l |- id not shadowed
-%% % TD,E,E_l |- pat1 : t1 gives E_l1 .. TD,E,E_l |- patn : tn gives E_ln
+<E_t,E_k> |- pat1 : t1 gives E_t1 .. <E_t,E_k> |- patn : tn gives E_tn
%% % disjoint doms(E_l1,..,E_ln)
-%% % ------------------------------------------------------------ :: ident_constr
-%% % TD,E,E_l |- id pat1 .. patn : p t_args gives E_l1 u+ .. u+ E_ln
-%% %
-%% % TD |- t ok
-%% % E,E_l |- x not ctor
-%% % ------------------------------------------------------------ :: var
-%% % TD,E,E_l |- x l1 l2 : t gives {x|->t}
+------------------------------------------------------------ :: ident_constr
+<E_t,E_k> |- id pat1 .. patn : id t_args gives E_t1 u+ .. u+ E_tn
+
+E_k |-t t ok
+ ------------------------------------------------------------ :: var
+<E_t,E_k> |- :P_id: id : t gives E_t u+ {id|->t}
+
%% %
%% % </TD,E |- field idi : p t_args -> ti gives (xi of names) // i />
%% % </TD,E,E_l |- pati : ti gives E_li//i/>
@@ -1856,12 +1802,12 @@ by
%% % ----------------------------------------------------------- :: vectorConcat
%% % TD,E,E_l |- [| pat1 ... patn |] : __vector ne' t gives E_l1 u+ ... u+ E_ln
%% %
-%% %
-%% % TD,E,E_l |- pat1 : t1 gives E_l1 .... TD,E,E_l |- patn : tn gives E_ln
-%% % disjoint doms(E_l1,....,E_ln)
-%% % ------------------------------------------------------------ :: tup
-%% % TD,E,E_l |- (pat1, ...., patn) : t1 * .... * tn gives E_l1 u+ .... u+ E_ln
-%% %
+
+<E_t,E_k> |- pat1 : t1 gives E_t1 .... <E_t,E_k> |- patn : tn gives E_tn
+disjoint doms(E_t1,....,E_tn)
+------------------------------------------------------------ :: tup
+<E_t,E_k> |- (pat1, ...., patn) : t1 * .... * tn gives E_t1 u+ .... u+ E_tn
+
%% % TD |- t ok
%% % TD,E,E_l |- pat1 : t gives E_l1 .. TD,E,E_l |- patn : t gives E_ln
%% % disjoint doms(E_l1,..,E_ln)
@@ -1925,9 +1871,9 @@ by
%% % ------------------------------------------------------------ :: cons
%% % <E_m,E_p,E_f,E_x> |- x l1.</y_li.//i/> z_l l2 value
%% %
-%% % defns
-%% % check_exp :: '' ::=
-%% %
+defns
+check_exp :: '' ::=
+
%% % defn
%% % TD , E , E_l |- exp : t gives S_c , S_N :: :: check_exp :: check_exp_
%% % {{ com Typing expressions, collecting typeclass and index constraints }}
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
+
+
+
diff --git a/src/ast.ml b/src/ast.ml
index 79c7ea4f..fe990be3 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -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 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:20:13 +0000