summaryrefslogtreecommitdiff
path: root/language
diff options
context:
space:
mode:
authorKathy Gray2013-11-01 17:03:40 +0000
committerKathy Gray2013-11-01 17:03:40 +0000
commitb3a69210b3e3d1b5ebc1d6687884ecfe3fd202f2 (patch)
treeaef92a73dfda5888cdb53d2b0af77298edd82863 /language
parent7fdb44465a2eb169946ec0e23b4056aafabe1b93 (diff)
Moved metatheory grammars into l2_rules.ott
Added val extern specification to language, parser, printer, and interpreter Added various def level type system support, expressions type system in place Except for assignment
Diffstat (limited to 'language')
-rw-r--r--language/l2.lem104
-rw-r--r--language/l2.ml219
-rw-r--r--language/l2.ott420
-rw-r--r--language/l2_parse.ml1
-rw-r--r--language/l2_parse.ott1
-rw-r--r--language/l2_rules.ott964
6 files changed, 740 insertions, 969 deletions
diff --git a/language/l2.lem b/language/l2.lem
index d39c7110..8e5dd4ed 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -32,11 +32,6 @@ val subst : forall 'a. list 'a -> list 'a -> bool
type x = string (* identifier *)
type ix = string (* infix identifier *)
-type id = (* Identifier *)
- | Id of x
- | DeIid of x (* remove infix status *)
-
-
type base_kind = (* base kind *)
| BK_type (* kind of types *)
| BK_nat (* kind of natural number size expressions *)
@@ -44,6 +39,15 @@ type base_kind = (* base kind *)
| 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 *)
@@ -52,10 +56,6 @@ type nexp = (* expression of kind $Nat$, for vector sizes and origins *)
| Nexp_exp of nexp (* exponential *)
-type kind = (* kinds *)
- | K_kind of list base_kind
-
-
type efct = (* effect *)
| Effect_rreg (* read register *)
| Effect_wreg (* write register *)
@@ -66,6 +66,11 @@ type efct = (* effect *)
| 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
@@ -73,9 +78,9 @@ type nexp_constraint = (* constraint over kind $Nat$ *)
| NC_nat_set_bounded of id * list num
-type kinded_id = (* optionally kind-annotated identifier *)
- | KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
+type effects = (* effect set, of kind $Effects$ *)
+ | Effects_var of id
+ | Effects_set of list efct (* effect set *)
type order = (* vector order specifications, of kind $Order$ *)
@@ -84,25 +89,11 @@ type order = (* vector order specifications, of kind $Order$ *)
| 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 ne = (* internal numeric expressions *)
- | Ne_var of id
- | Ne_const of num
- | Ne_mult of ne * ne
- | Ne_add of list ne
- | Ne_exp of ne
- | Ne_unary of ne
-
-
type typ = (* Type expressions, of kind $Type$ *)
| Typ_wild (* Unspecified type *)
| Typ_var of id (* Type variable *)
@@ -117,11 +108,6 @@ and typ_arg = (* Type constructor arguments of all kinds *)
| 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$ *)
@@ -135,14 +121,9 @@ type lit = (* Literal constant *)
| L_string of string (* string constant *)
-type nec = (* Numeric expression constraints *)
- | Nec_lteq of ne * ne
- | Nec_eq of ne * ne
- | Nec_gteq of ne * ne
-
-
-type typschm = (* type scheme *)
- | TypSchm_ts of typquant * typ
+type typquant = (* type quantifiers and constraints *)
+ | TypQ_tq of list quant_item
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
type pat = (* Pattern *)
@@ -163,6 +144,10 @@ and fpat = (* Field pattern *)
| FP_Fpat of id * pat
+type typschm = (* type scheme *)
+ | TypSchm_ts of typquant * typ
+
+
type exp = (* Expression *)
| E_block of list exp (* block (parsing conflict with structs?) *)
| E_id of id (* identifier *)
@@ -209,15 +194,12 @@ and letbind = (* Let binding *)
| LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
-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 tannot_opt = (* Optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
-type naming_scheme_opt = (* Optional variable-naming-scheme specification for variables of defined type *)
- | Name_sect_none
- | Name_sect_some of string
+type funcl = (* Function clause *)
+ | FCL_Funcl of id * pat * exp
type effects_opt = (* Optional effect annotation for functions *)
@@ -230,22 +212,15 @@ type rec_opt = (* Optional recursive annotation for functions *)
| Rec_rec (* recursive *)
-type tannot_opt = (* Optional type annotation for functions *)
- | Typ_annot_opt_some of typquant * typ
-
-
-type funcl = (* Function clause *)
- | FCL_Funcl of id * pat * exp
+type naming_scheme_opt = (* Optional variable-naming-scheme specification for variables of defined type *)
+ | Name_sect_none
+ | Name_sect_some of string
-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 default_typing_spec = (* Default kinding or typing assumption *)
@@ -253,8 +228,13 @@ type default_typing_spec = (* Default kinding or typing assumption *)
| DT_typ of typschm * id
+type fundef = (* Function definition *)
+ | FD_function of rec_opt * tannot_opt * effects_opt * list funcl
+
+
type val_spec = (* Value type specification *)
| VS_val_spec of typschm * id
+ | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
type type_def = (* Type definition body *)
@@ -265,10 +245,6 @@ type type_def = (* Type definition body *)
| 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 *)
diff --git a/language/l2.ml b/language/l2.ml
index bf87b48b..664ace51 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -20,14 +20,19 @@ 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
-base_kind =
- BK_aux of base_kind_aux * l
+kind_aux = (* kinds *)
+ K_kind of (base_kind) list
type
@@ -36,8 +41,8 @@ id =
type
-kind_aux = (* kinds *)
- K_kind of (base_kind) list
+kind =
+ K_aux of kind_aux * l
type
@@ -53,8 +58,9 @@ and nexp =
type
-kind =
- K_aux of kind_aux * l
+kinded_id_aux = (* optionally kind-annotated identifier *)
+ KOpt_none of id (* identifier *)
+ | KOpt_kind of kind * id (* kind-annotated variable *)
type
@@ -66,22 +72,6 @@ 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 *)
@@ -93,9 +83,13 @@ efct_aux = (* effect *)
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 *)
+kinded_id =
+ KOpt_aux of kinded_id_aux * l
+
+
+type
+nexp_constraint =
+ NC_aux of nexp_constraint_aux * l
type
@@ -104,8 +98,15 @@ efct =
type
-quant_item =
- QI_aux of quant_item_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
+effects_aux = (* effect set, of kind $_$ *)
+ Effects_var of id
+ | Effects_set of (efct) list (* effect set *)
type
@@ -116,15 +117,13 @@ 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 *)
+quant_item =
+ QI_aux of quant_item_aux * l
type
-typquant_aux = (* type quantifiers and constraints *)
- TypQ_tq of (quant_item) list
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+effects =
+ Effects_aux of effects_aux * l
type
@@ -133,13 +132,23 @@ order =
type
-effects =
- Effects_aux of effects_aux * l
+typquant_aux = (* type quantifiers and constraints *)
+ TypQ_tq of (quant_item) list
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
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_undef (* constant representing undefined values *)
+ | L_string of string (* string constant *)
type
@@ -164,22 +173,8 @@ and typ_arg =
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_undef (* constant representing undefined values *)
- | L_string of string (* string constant *)
-
-
-type
-typschm_aux = (* type scheme *)
- TypSchm_ts of typquant * typ
+typquant =
+ TypQ_aux of typquant_aux * l
type
@@ -188,8 +183,8 @@ lit =
type
-typschm =
- TypSchm_aux of typschm_aux * l
+typschm_aux = (* type scheme *)
+ TypSchm_ts of typquant * typ
type
@@ -218,7 +213,15 @@ and 'a fpat =
type
-'a exp_aux = (* Expression *)
+typschm =
+ TypSchm_aux of typschm_aux * l
+
+
+type
+'a letbind =
+ LB_aux of 'a letbind_aux * 'a annot
+
+and 'a exp_aux = (* Expression *)
E_block of ('a exp) list (* block (parsing conflict with structs?) *)
| E_id of id (* identifier *)
| E_lit of lit (* literal constant *)
@@ -278,24 +281,21 @@ and 'a letbind_aux = (* Let binding *)
LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
| LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
-and 'a letbind =
- LB_aux of 'a letbind_aux * 'a annot
+
+type
+'a tannot_opt_aux = (* Optional type annotation for functions *)
+ Typ_annot_opt_some of typquant * typ
type
-ne = (* internal numeric expressions *)
- Ne_var of id
- | Ne_const of int
- | Ne_mult of ne * ne
- | Ne_add of (ne) list
- | Ne_exp of ne
- | Ne_unary of ne
+'a funcl_aux = (* Function clause *)
+ FCL_Funcl of id * 'a pat * 'a exp
type
-naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *)
- Name_sect_none
- | Name_sect_some of string
+'a effects_opt_aux = (* Optional effect annotation for functions *)
+ Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of effects
type
@@ -305,26 +305,29 @@ rec_opt_aux = (* Optional recursive annotation for functions *)
type
-'a funcl_aux = (* Function clause *)
- FCL_Funcl of id * 'a pat * 'a exp
+naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *)
+ Name_sect_none
+ | Name_sect_some of string
type
-'a tannot_opt_aux = (* Optional type annotation for functions *)
- Typ_annot_opt_some of typquant * typ
+'a tannot_opt =
+ Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
type
-'a effects_opt_aux = (* Optional effect annotation for functions *)
- Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
+'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
-nec = (* Numeric expression constraints *)
- Nec_lteq of ne * ne
- | Nec_eq of ne * ne
- | Nec_gteq of ne * ne
+rec_opt =
+ Rec_aux of rec_opt_aux * l
type
@@ -343,23 +346,20 @@ naming_scheme_opt =
type
-rec_opt =
- Rec_aux of rec_opt_aux * l
-
-
-type
-'a funcl =
- FCL_aux of 'a funcl_aux * 'a annot
+'a default_typing_spec_aux = (* Default kinding or typing assumption *)
+ DT_kind of base_kind * id
+ | DT_typ of typschm * id
type
-'a tannot_opt =
- Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+'a val_spec_aux = (* Value type specification *)
+ VS_val_spec of typschm * id
+ | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
type
-'a effects_opt =
- Effects_opt_aux of 'a effects_opt_aux * 'a annot
+'a fundef_aux = (* Function definition *)
+ FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
type
@@ -372,29 +372,8 @@ type
type
-'a fundef_aux = (* Function definition *)
- FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
-
-
-type
-'a val_spec_aux = (* Value type specification *)
- VS_val_spec of typschm * id
-
-
-type
-'a default_typing_spec_aux = (* Default kinding or typing assumption *)
- DT_kind of base_kind * id
- | DT_typ of typschm * id
-
-
-type
-'a type_def =
- TD_aux of 'a type_def_aux * 'a annot
-
-
-type
-'a fundef =
- FD_aux of 'a fundef_aux * 'a annot
+'a default_typing_spec =
+ DT_aux of 'a default_typing_spec_aux * 'a annot
type
@@ -403,19 +382,13 @@ type
type
-'a default_typing_spec =
- DT_aux of 'a default_typing_spec_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 type_def =
+ TD_aux of 'a type_def_aux * 'a annot
type
diff --git a/language/l2.ott b/language/l2.ott
index bc2f0c8d..d6f8cfed 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -1,4 +1,4 @@
-indexvar n , i , j ::=
+indexvar n , m , i , j ::=
{{ phantom }}
{{ com Index variables for meta-lists }}
@@ -832,6 +832,8 @@ val_spec :: 'VS_' ::=
{{ com Value type specification }}
{{ aux _ annot }} {{ auxparam 'a }}
| val typschm id :: :: val_spec
+ | val extern typschm id = string :: :: extern_spec
+ {{ com Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked }}
default_typing_spec :: 'DT_' ::=
{{ com Default kinding or typing assumption }}
@@ -882,282 +884,6 @@ defs :: '' ::=
| def1 .. defn :: :: Defs
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Machinery for typing rules %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-grammar
-
-k :: 'Ki_' ::=
-{{ com Internal kinds }}
- | K_Typ :: :: typ
- | K_Nat :: :: nat
- | K_Ord :: :: ord
- | K_Efct :: :: efct
- | K_Val :: :: val {{ com Representing values, for use in identifier checks }}
- | K_Lam ( k0 .. kn -> k' ) :: :: ctor
- | K_infer :: :: infer {{ com Representing an unknown kind, inferred by context }}
-
-t , u :: 'T_' ::= {{ phantom }}
-{{ com Internal types }}
- | id :: :: var
- | t1 -> t2 effects tag S_N :: :: fn {{ com [[S_N]] are constraints for the function, [[tag]] holds generation data }}
- | ( t1 * .... * tn ) :: :: tup
- | id t_args :: :: app
-
-tag :: 'Tag_' ::= {{ phantom }}
-{{ com Data indicating where the function arises and thus information necessary in compilation }}
- | None :: :: empty
- | Ctor :: :: ctor {{ com Data constructor from a type union }}
- | Extern :: :: extern {{ com External function, specied only with a val statement }}
- | _ :: :: dontcare
-
-ne :: 'Ne_' ::=
- {{ com internal numeric expressions }}
- | id :: :: var
- | num :: :: const
- | ne1 * ne2 :: :: mult
- | ne1 + ... + nen :: :: 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]]) }}
- | length ( pat1 ... patn ) :: M :: cpat
- {{ ocaml (assert false) }}
- {{ hol ARB }}
- {{ lem (Ne_const (List.length [[pat1...patn]])) }}
- | length ( exp1 ... expn ) :: M :: cexp
- {{ hol ARB }}
- {{ ocaml (assert false) }}
- {{ lem (Ne_const (List.length [[exp1...expn]])) }}
-
- t_arg :: 't_arg_' ::= {{ phantom }}
- {{ com Argument to type constructors }}
- | t :: :: typ
- | ne :: :: nexp
- | effects :: :: effect
- | order :: :: order
-
- t_args :: '' ::= {{ phantom }}
- {{ com Arguments to type constructors }}
- | t_arg1 ... t_argn :: :: T_args
-
- nec :: 'Nec_' ::=
- {{ com Numeric expression constraints }}
- | ne <= ne' :: :: lteq
- | ne = ne' :: :: eq
- | ne >= ne' :: :: gteq
-
-%% %% embed
-%% %% {{ lem
-%% %%
-%% %% val t_subst_t : list (tnv * t) -> t -> t
-%% %% val t_subst_tnv : list (tnv * t) -> tnv -> t
-%% %% val ftv_t : t -> list tnv
-%% %% val ftv_tm : list t -> list tnv
-%% %% val ftv_s : list (p*tnv) -> list tnv
-%% %% val compatible_overlap : list (x*t) -> bool
-%% %%
-%% %% (*TODO Should this normalize following the implementation? And blength and hlength need a means of implementation*)
-%% %% let normalize n = n
-%% %%
-%% %% let blength (_,bit) = Ne_const 8
-%% %% let hlength (_,bit) = Ne_const 8
-%% %%
-%% %% let rec sumation_nes nes = match nes with
-%% %% | [ a; b] -> Ne_add a b
-%% %% | x :: y -> Ne_add x (sumation_nes y)
-%% %% end
-%% %%
-%% %% }}
-%% %%
-%% %% grammar
-%% %%
-%% %%
-%% %% names :: '' ::= {{ phantom }}
-%% %% {{ hol x set }}
-%% %% {{ lem set x }}
-%% %% {{ ocaml Set.Make(String).t }}
-%% %% {{ com Sets of names }}
-%% %% | { x1 , .. , xn } :: :: Names
-%% %% {{ hol (LIST_TO_SET [[x1..xn]]) }}
-%% %% {{ lem (set_from_list [[x1..xn]]) }}
-%% %%
-%% %% semC {{ tex \ensuremath{\mathcal{C} } }} :: '' ::=
-%% %% {{ hol (p#tnv) list }}
-%% %% {{ lem list (p*tnv) }}
-%% %% % {{ com Typeclass constraint lists }}
-%% %% % | ( p1 tnv1 ) .. ( pn tnvn ) :: :: SemC_concrete
-%% %% % {{ hol ([[p1 tnv1..pn tnvn]]) }}
-%% %% % {{ lem ([[p1 tnv1..pn tnvn]]) }}
-%% %%
-%% %% env_tag :: '' ::=
-%% %% {{ com Tags for the (non-constructor) value descriptions }}
-%% %% % | method :: :: method
-%% %% % {{ com Bound to a method }}
-%% %% | val :: :: spec
-%% %% {{ com Specified with val }}
-%% %% | let :: :: def
-%% %% {{ com Defined with let or indreln }}
-%% %%
-%% %% v_desc :: 'V_' ::=
-%% %% {{ com Value descriptions }}
-%% %% | < forall tnvs . t_multi -> p , ( x of names ) > :: :: constr
-%% %% {{ com Constructors }}
-%% %% | < forall tnvs . semC => t , env_tag > :: :: val
-%% %% {{ com Values }}
-%% %%
-%% %% f_desc :: 'F_' ::=
-%% %% | < forall tnvs . p -> t , ( x of names ) > :: :: field
-%% %% {{ com Fields }}
-%% %%
-%% %% embed
-%% %% {{ hol
-%% %% load "fmaptreeTheory";
-%% %% val _ =
-%% %% Hol_datatype
-%% %% `env_body = <| env_p : x|->p; env_f : x|->f_desc; env_v : x|->v_desc |>`;
-%% %%
-%% %% val _ = Define `
-%% %% env_union e1 e2 =
-%% %% let i1 = item e1 in
-%% %% let m1 = map e1 in
-%% %% let i2 = item e2 in
-%% %% let m2 = map e2 in
-%% %% FTNode <| env_p:=FUNION i1.env_p i2.env_p;
-%% %% env_f:=FUNION i1.env_f i2.env_f;
-%% %% env_v:=FUNION i1.env_v i2.env_v |>
-%% %% (FUNION m1 m2)`;
-%% %% }}
-%% %% {{ lem
-%% %% type env =
-%% %% | EnvEmp
-%% %% | Env of (map x env) * (map x p) * (map x f_desc) * (map x v_desc)
-%% %%
-%% %% val env_union : env -> env -> env
-%% %% let env_union e1 e2 =
-%% %% match (e1,e2) with
-%% %% | (EnvEmp,e2) -> e2
-%% %% | (e1,EnvEmp) -> e1
-%% %% | ((Env Em1 Ep1 Ef1 Ev1),(Env Em2 Ep2 Ef2 Ev2)) ->
-%% %% Env(union_map Em1 Em2) (union_map Ep1 Ep2) (union_map Ef1 Ef2) (union_map Ev1 Ev2)
-%% %% end
-%% %%
-%% %% }}
-%% %%
-%% %% grammar
-%% %%
-%% %% xs :: '' ::= {{ phantom }}
-%% %% {{ hol string list }}
-%% %% {{ lem list string }}
-%% %% | x1 .. xn :: :: Xs
-%% %% {{ hol [[x1..xn]] }}
-%% %% {{ lem [[x1..xn]] }}
-%% %%
-S_N {{ tex \Sigma^{\textsc{N} } }} :: '' ::= {{ phantom }}
- {{ hol nec list }}
- {{ lem list nec }}
- {{ com nexp constraint lists }}
- | { nec1 , .. , necn } :: :: Sn_concrete
- {{ hol [[nec1 .. necn]] }}
- {{ lem [[nec1 .. necn]] }}
- | S_N1 u+ .. u+ S_Nn :: M :: SN_union
- {{ hol (FOLDR FUNION FEMPTY [[S_N1..S_Nn]]) }}
- {{ lem (List.fold_right union_map [[S_N1..S_Nn]] Pmap.empty) }}
- {{ ocaml (assert false) }}
- | consistent_increase ne1 ne'1 ... nen ne'n :: M :: SN_increasing
- {{ com Generates constraints from pairs of constraints, where the first of each pair is always larger than the sum of the previous pair }}
- {{ ocaml (assert false) }}
- {{ ichl todo }}
- | consistent_decrease ne1 ne'1 ... nen ne'n :: M :: SN_decreasing
- {{ com Generates constraints from pairs of constraints, where the first of each pair is always smaller than the difference of the previous pair }}
- {{ ocaml assert false }}
- {{ ichl todo }}
-
- I :: '' ::= {{ phantom }}
- {{ com Information given by type checking an expression; tag only reflects the immediate exp }}
- | < S_N , effects > :: :: I
- | Ie :: :: Iempty {{ com Empty constraints, effetcs }} {{ tex {\ottnt{I}_{\epsilon} } }}
- | I1 u+ .. u+ In :: :: Iunion {{ com Unions the constraints and effects, setting None for the tag }}
-
- E :: '' ::= {{ phantom }}
- {{ hol ((string,env_body) fmaptree) }}
- {{ lem env }}
- {{ com Environments }}
- | < E_t , E_r , E_k > :: :: E
- {{ hol arb }}
- {{ lem (Env [[E_k]] [[E_r]] [[E_t]]) }}
- | empty :: M :: E_empty
- {{ hol arb }}
- {{ lem EnvEmp }}
- {{ ocaml assert false }}
-
- E_k {{ tex \ottnt{E}^{\textsc{k} } }} :: 'E_k_' ::= {{ phantom }}
- {{ hol (id-> k) }}
- {{ lem map id k }}
- {{ com Kind environments }}
- | { id1 |-> k1 , .. , idn |-> kn } :: :: concrete
- {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[id1 k1 .. idn kn]]) }}
- {{ lem (List.fold_right (fun (x,v) m -> Pmap.add x v m) [[id1 k1 .. idn kn]] Pmap.empty) }}
- | E_k1 u+ .. u+ E_kn :: M :: union
- {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }}
- {{ lem (List.fold_right union_map [[E_k1..E_kn]] Pmap.empty) }}
- {{ ocaml (assert false) }}
-
- E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::= {{ phantom }}
- {{ hol (id |-> t) }}
- {{ lem map x f_desc }}
- {{ com Type environments }}
- | { id1 |-> t1 , .. , idn |-> tn } :: :: base
- {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 t1 .. idn tn]]) }}
- {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) [[id1 t1 .. idn tn]] Pmap.empty) }}
- | ( E_t1 u+ .... u+ E_tn ) :: M :: union
- {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }}
- {{ lem (List.fold_right union_map [[E_t1....E_tn]] Pmap.empty) }}
- {{ ocaml (assert false) }}
- | u+ E_t1 .. E_tn :: M :: multi_union
- {{ hol arb }}
- {{ lem arb }}
- {{ ocaml assert false }}
- | E_t u- E_t1 .. E_tn :: M :: multi_set_minus
- {{ hol arb }} {{ lem arb }} {{ ocaml assert false }}
- | ( E_t1 inter .... inter E_tn ) :: M :: intersect
- {{ hol arb }}
- {{ lem syntax error }}
- {{ ocaml (assert false) }}
- | inter E_t1 .. E_tn :: M :: multi_inter
- {{ hol arb }}
- {{ lem arb }}
- {{ ocaml assert false }}
-
-
- field_typs :: 'FT_' ::= {{ phantom }}
- {{ com Record fields }}
- | id1 : t1 , .. , idn : tn :: :: fields
-
- E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::= {{ phantom }}
- {{ hol (id |-> t) }}
- {{ lem map x f_desc }}
- {{ com Record environments }}
- | { { field_typs1 } |-> t1 , .. , { field_typsn } |-> tn } :: :: concrete
- {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }}
- {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) Pmap.empty) }}
- | E_r1 u+ .. u+ E_rn :: M :: union
- {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }}
- {{ lem (List.fold_right union_map [[E_r1..E_rn]] Pmap.empty) }}
- {{ ocaml (assert false) }}
-
terminals :: '' ::=
| ** :: :: starstar
{{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }}
@@ -1231,144 +957,4 @@ terminals :: '' ::=
| consistent_decrease :: :: cd
{{ tex \ottkw{consistent\_decrease}~ }}
-ts :: ts_ ::= {{ phantom }}
- | t1 , .. , tn :: :: lst
-
-formula :: formula_ ::=
- | judgement :: :: judgement
-
- | formula1 .. formulan :: :: dots
-
- | E_k ( id ) gives k :: :: lookup_k
- {{ com Kind lookup }}
- {{ hol (FLOOKUP [[E_k]] [[id]] = SOME [[k]]) }}
- {{ lem Pmap.find [[id]] [[E_k]] = [[k]] }}
-
- | E_t ( id ) gives t :: :: lookup_t
- {{ com Type lookup }}
- {{ 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 }}
-
- | E_r ( id0 .. idn ) gives t , ts :: :: lookup_r
- {{ com Record lookup }}
-
- | E_r ( t ) gives id0 : t0 .. idn : tn :: :: lookup_rt
- {{ com Record looup by type }}
-
- | dom ( E_t1 ) inter dom ( E_t2 ) = emptyset :: :: E_t_disjoint
- {{ hol (DISJOINT (FDOM [[E_t1]]) (FDOM [[E_t2]])) }}
- {{ lem disjoint (Pmap.domain [[E_t1]]) (Pmap.domain [[E_t2]]) }}
-
- | dom ( E_k1 ) inter dom ( E_k2 ) = emptyset :: :: E_k_disjoint
- {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }}
- {{ lem disjoint (Pmap.domain [[E_f1]]) (Pmap.domain [[E_f2]]) }}
-
- | 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)) }}
-%% %% {{ lem (compatible_overlap [[x1 t1 .. xn tn]]) }}
-%% %% {{ com $(\ottnt{x}_i = \ottnt{x}_j) \ensuremath{\Longrightarrow} (\ottnt{t}_i = \ottnt{t}_j)$ }}
-%% %%
-%% %% | duplicates ( tnvs ) = emptyset :: :: no_dups_tnvs
-%% %% {{ hol (ALL_DISTINCT [[tnvs]]) }}
-%% %% {{ lem (duplicates [[tnvs]]) = [ ] }}
-%% %%
-%% %% | duplicates ( x1 , .. , xn ) = emptyset :: :: no_dups
-%% %% {{ hol (ALL_DISTINCT [[x1..xn]]) }}
-%% %% {{ lem (duplicates [[x1..xn]]) = [ ] }}
-
- | id NOTIN dom ( E_k ) :: :: notin_dom_k
- {{ hol ([[id]] NOTIN FDOM [[E_k]]) }}
- {{ lem Pervasives.not (Pmap.mem [[id]] [[E_k]]) }}
-
- | id NOTIN dom ( E_t ) :: :: notin_dom_t
- {{ hol ([[id]] NOTIN FDOM [[E_t]]) }}
- {{ lem Pervasives.not (Pmap.mem [[id]] [[E_t]]) }}
-
- | id0 : t0 .. idn : tn SUBSET id'0 : t'0 .. id'i : t'i :: :: subsetFields
-%% %%
-%% %%
-%% %% | FV ( t ) SUBSET tnvs :: :: FV_t
-%% %% {{ com Free type variables }}
-%% %% {{ hol (LIST_TO_SET (ftv_t [[t]]) SUBSET LIST_TO_SET [[tnvs]]) }}
-%% %% {{ lem subst (ftv_t [[t]]) [[tnvs]] }}
-%% %%
-%% %% | FV ( t_multi ) SUBSET tnvs :: :: FV_t_multi
-%% %% {{ com Free type variables }}
-%% %% {{ hol (LIST_TO_SET (FLAT (MAP ftv_t [[t_multi]])) SUBSET LIST_TO_SET [[tnvs]]) }}
-%% %% {{ lem subst (ftv_tm [[t_multi]]) [[tnvs]] }}
-%% %%
-%% %% | FV ( semC ) SUBSET tnvs :: :: FV_semC
-%% %% {{ com Free type variables }}
-%% %% {{ hol (LIST_TO_SET (MAP SND [[semC]]) SUBSET LIST_TO_SET [[tnvs]]) }}
-%% %% {{ lem subst (ftv_s [[semC]]) [[tnvs]] }}
-%% %%
-%% %% | inst 'IN' I :: :: inst_in
-%% %% {{ hol (MEM [[inst]] [[I]]) }}
-%% %% {{ lem ([[inst]] IN [[I]]) }}
-%% %%
-%% %% | ( p t ) NOTIN I :: :: notin_I
-%% %% {{ hol (~?__semC__. MEM (Inst __semC__ [[p]] [[t]]) [[I]]) }}
-%% %% {{ lem (Pervasives.not ((Inst [] [[p]] [[t]]) IN [[I]])) }}
-%% %%
-
- | num1 lt ... lt numn :: :: increasing
-
- | num1 gt ... gt numn :: :: decreasing
-
- | E_k1 = E_k2 :: :: E_k_eqn
- {{ ichl ([[E_k1]] = [[E_k2]]) }}
-
- | E_t1 = E_t2 :: :: E_t_eqn
- {{ ichl ([[E_t1]] = [[E_t2]]) }}
-
- | E1 = E2 :: :: E_eqn
- {{ ichl ([[E1]] = [[E2]]) }}
-
- | S_N1 = S_N2 :: :: S_N_eqn
- {{ ichl ([[S_N1]] = [[S_N2]]) }}
-
-%% %% | TD1 = TD2 :: :: TD_eqn
-%% %% {{ ichl ([[TD1]] = [[TD2]]) }}
-%% %%
-%% %% | TC1 = TC2 :: :: TC_eqn
-%% %% {{ ichl ([[TC1]] = [[TC2]]) }}
-%% %%
-%% %% | I1 = I2 :: :: I_eqn
-%% %% {{ ichl ([[I1]] = [[I2]]) }}
-%% %%
-%% %% | names1 = names2 :: :: names_eq
-%% %% {{ ichl ([[names1]] = [[names2]]) }}
-%% %%
- | 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]]) }}
-%% %%
-%% %% | p1 = p2 :: :: p_eq
-%% %% {{ ichl ([[p1]] = [[p2]]) }}
-%% %%
-%% %% | xs1 = xs2 :: :: xs_eq
-%% %% {{ ichl ([[xs1]] = [[xs2]]) }}
-%% %%
-%% %% | tnvs1 = tnvs2 :: :: tnvs_eq
-%% %% {{ ichl ([[tnvs1]] = [[tnvs2]]) }}
-
-% Substitutions and freevars are not correctly generated for the OCaml ast.ml
-%substitutions
-%multiple t a :: t_subst
-%
-%freevars
-%t a :: ftv
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index 703fc49e..c6153f89 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -323,6 +323,7 @@ type_def_aux = (* Type definition body *)
type
val_spec_aux = (* Value type specification *)
VS_val_spec of typschm * id
+ | VS_extern_spec of typschm * id * string
type
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index 1da173e1..56152bd1 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -683,6 +683,7 @@ val_spec :: 'VS_' ::=
{{ aux _ l }}
% {{ aux _ annot }} {{ auxparam 'a }}
| val typschm id :: :: val_spec
+ | val extern typschm id = string :: :: extern_spec
default_typing_spec :: 'DT_' ::=
{{ com Default kinding or typing assumption }}
diff --git a/language/l2_rules.ott b/language/l2_rules.ott
index bfb496e4..994c4914 100644
--- a/language/l2_rules.ott
+++ b/language/l2_rules.ott
@@ -1,5 +1,326 @@
grammar
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Machinery for typing rules %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+grammar
+
+k :: 'Ki_' ::=
+{{ com Internal kinds }}
+ | K_Typ :: :: typ
+ | K_Nat :: :: nat
+ | K_Ord :: :: ord
+ | K_Efct :: :: efct
+ | K_Lam ( k0 .. kn -> k' ) :: :: ctor
+ | K_infer :: :: infer {{ com Representing an unknown kind, inferred by context }}
+ | K_Abbrev t :: :: abbrev {{ com Not really a kind, but a convenient way of tracking type abbreviations }}
+
+t , u :: 'T_' ::= {{ phantom }}
+{{ com Internal types }}
+ | id :: :: var
+ | t1 -> t2 effects tag S_N :: :: fn {{ com [[S_N]] are constraints for the function, [[tag]] holds generation data }}
+ | ( t1 * .... * tn ) :: :: tup
+ | id t_args :: :: app
+ | register t_args :: :: reg_app
+
+tag :: 'Tag_' ::= {{ phantom }}
+{{ com Data indicating where the identifier arises and thus information necessary in compilation }}
+ | None :: :: empty
+ | Ctor :: :: ctor {{ com Data constructor from a type union }}
+ | Extern :: :: extern {{ com External function, specied only with a val statement }}
+ | Default :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }}
+ | _ :: :: dontcare
+
+ne :: 'Ne_' ::=
+ {{ com internal numeric expressions }}
+ | id :: :: var
+ | num :: :: const
+ | ne1 * ne2 :: :: mult
+ | ne1 + ... + nen :: :: add
+ | 2 ** ne :: :: exp
+ | ( - ne ) :: :: unary
+ | 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 }}
+ {{ lem (Ne_const (List.length [[pat1...patn]])) }}
+ | length ( exp1 ... expn ) :: M :: cexp
+ {{ hol ARB }}
+ {{ ocaml (assert false) }}
+ {{ lem (Ne_const (List.length [[exp1...expn]])) }}
+
+ t_arg :: 't_arg_' ::= {{ phantom }}
+ {{ com Argument to type constructors }}
+ | t :: :: typ
+ | ne :: :: nexp
+ | effects :: :: effect
+ | order :: :: order
+
+ t_args :: '' ::= {{ phantom }}
+ {{ com Arguments to type constructors }}
+ | t_arg1 ... t_argn :: :: T_args
+
+ nec :: 'Nec_' ::=
+ {{ com Numeric expression constraints }}
+ | ne <= ne' :: :: lteq
+ | ne = ne' :: :: eq
+ | ne >= ne' :: :: gteq
+ | id 'IN' { num1 , ... , numn } :: :: in
+
+%% %% embed
+%% %% {{ lem
+%% %%
+%% %% val t_subst_t : list (tnv * t) -> t -> t
+%% %% val t_subst_tnv : list (tnv * t) -> tnv -> t
+%% %% val ftv_t : t -> list tnv
+%% %% val ftv_tm : list t -> list tnv
+%% %% val ftv_s : list (p*tnv) -> list tnv
+%% %% val compatible_overlap : list (x*t) -> bool
+%% %%
+%% %% (*TODO Should this normalize following the implementation? And blength and hlength need a means of implementation*)
+%% %% let normalize n = n
+%% %%
+%% %% let blength (_,bit) = Ne_const 8
+%% %% let hlength (_,bit) = Ne_const 8
+%% %%
+%% %% let rec sumation_nes nes = match nes with
+%% %% | [ a; b] -> Ne_add a b
+%% %% | x :: y -> Ne_add x (sumation_nes y)
+%% %% end
+%% %%
+%% %% }}
+%% %%
+%% %% embed
+%% %% {{ hol
+%% %% load "fmaptreeTheory";
+%% %% val _ =
+%% %% Hol_datatype
+%% %% `env_body = <| env_p : x|->p; env_f : x|->f_desc; env_v : x|->v_desc |>`;
+%% %%
+%% %% val _ = Define `
+%% %% env_union e1 e2 =
+%% %% let i1 = item e1 in
+%% %% let m1 = map e1 in
+%% %% let i2 = item e2 in
+%% %% let m2 = map e2 in
+%% %% FTNode <| env_p:=FUNION i1.env_p i2.env_p;
+%% %% env_f:=FUNION i1.env_f i2.env_f;
+%% %% env_v:=FUNION i1.env_v i2.env_v |>
+%% %% (FUNION m1 m2)`;
+%% %% }}
+%% %% {{ lem
+%% %% type env =
+%% %% | EnvEmp
+%% %% | Env of (map x env) * (map x p) * (map x f_desc) * (map x v_desc)
+%% %%
+%% %% val env_union : env -> env -> env
+%% %% let env_union e1 e2 =
+%% %% match (e1,e2) with
+%% %% | (EnvEmp,e2) -> e2
+%% %% | (e1,EnvEmp) -> e1
+%% %% | ((Env Em1 Ep1 Ef1 Ev1),(Env Em2 Ep2 Ef2 Ev2)) ->
+%% %% Env(union_map Em1 Em2) (union_map Ep1 Ep2) (union_map Ef1 Ef2) (union_map Ev1 Ev2)
+%% %% end
+%% %%
+%% %% }}
+%% %%
+
+S_N {{ tex \Sigma^{\textsc{N} } }} :: '' ::= {{ phantom }}
+ {{ hol nec list }}
+ {{ lem list nec }}
+ {{ com nexp constraint lists }}
+ | { nec1 , .. , necn } :: :: Sn_concrete
+ {{ hol [[nec1 .. necn]] }}
+ {{ lem [[nec1 .. necn]] }}
+ | S_N1 u+ .. u+ S_Nn :: M :: SN_union
+ {{ hol (FOLDR FUNION FEMPTY [[S_N1..S_Nn]]) }}
+ {{ lem (List.fold_right union_map [[S_N1..S_Nn]] Pmap.empty) }}
+ {{ ocaml (assert false) }}
+ | consistent_increase ne1 ne'1 ... nen ne'n :: M :: SN_increasing
+ {{ com Generates constraints from pairs of constraints, where the first of each pair is always larger than the sum of the previous pair }}
+ {{ ocaml (assert false) }}
+ {{ ichl todo }}
+ | consistent_decrease ne1 ne'1 ... nen ne'n :: M :: SN_decreasing
+ {{ com Generates constraints from pairs of constraints, where the first of each pair is always smaller than the difference of the previous pair }}
+ {{ ocaml assert false }}
+ {{ ichl todo }}
+ | resolve S_N :: :: resolution
+
+ I :: '' ::= {{ phantom }}
+ {{ com Information given by type checking an expression }}
+ | < S_N , effects > :: :: I
+ | Ie :: :: Iempty {{ com Empty constraints, effects }} {{ tex {\ottnt{I}_{\epsilon} } }}
+ | I1 u+ .. u+ In :: :: Iunion {{ com Unions the constraints and effects }}
+
+ E :: '' ::= {{ phantom }}
+ {{ hol ((string,env_body) fmaptree) }}
+ {{ lem env }}
+ {{ com Environments }}
+ | < E_t , E_r , E_k > :: :: E
+ {{ hol arb }}
+ {{ lem (Env [[E_k]] [[E_r]] [[E_t]]) }}
+ | empty :: M :: E_empty
+ {{ hol arb }}
+ {{ lem EnvEmp }}
+ {{ ocaml assert false }}
+ | E u+ E' :: :: E_union
+
+ kinf :: 'kinf_' ::=
+ {{ com Whether a kind is default or from a local binding }}
+ | k :: :: k
+ | k default :: :: def
+
+ E_k {{ tex \ottnt{E}^{\textsc{k} } }} :: 'E_k_' ::= {{ phantom }}
+ {{ hol (id-> k) }}
+ {{ lem map id k }}
+ {{ com Kind environments }}
+ | { id1 |-> kinf1 , .. , idn |-> kinfn } :: :: concrete
+ {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[id1 kinf1 .. idn kinfn]]) }}
+ {{ lem (List.fold_right (fun (x,v) m -> Pmap.add x v m) [[id1 kinf1 .. idn kinfn]] Pmap.empty) }}
+ | E_k1 u+ .. u+ E_kn :: M :: union
+ {{ com In a unioning kinf, {k default} u {k} results in {k} (i.e. the default is locally forgotten) }}
+ {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }}
+ {{ lem (List.fold_right union_map [[E_k1..E_kn]] Pmap.empty) }}
+ {{ ocaml (assert false) }}
+ | E_k u- E_k1 .. E_kn :: M :: multi_set_minus
+ {{ hol arb }} {{ lem arb }} {{ ocaml assert false }}
+
+
+ tinf :: 'tinf_' ::=
+ {{ com Type variables, type, and constraints, bound to an identifier }}
+ | t :: :: typ
+ | E_k , S_N , tag , t :: :: quant_typ
+
+ E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::= {{ phantom }}
+ {{ hol (id |-> tinf) }}
+ {{ lem map x f_desc }}
+ {{ com Type environments }}
+ | { id1 |-> tinf1 , .. , idn |-> tinfn } :: :: base
+ {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }}
+ {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) [[id1 tinf1 .. idn tinfn]] Pmap.empty) }}
+ | ( E_t1 u+ .... u+ E_tn ) :: M :: union
+ {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }}
+ {{ lem (List.fold_right union_map [[E_t1....E_tn]] Pmap.empty) }}
+ {{ ocaml (assert false) }}
+ | u+ E_t1 .. E_tn :: M :: multi_union
+ {{ hol arb }}
+ {{ lem arb }}
+ {{ ocaml assert false }}
+ | E_t u- E_t1 .. E_tn :: M :: multi_set_minus
+ {{ hol arb }} {{ lem arb }} {{ ocaml assert false }}
+ | ( E_t1 inter .... inter E_tn ) :: M :: intersect
+ {{ hol arb }}
+ {{ lem syntax error }}
+ {{ ocaml (assert false) }}
+ | inter E_t1 .. E_tn :: M :: multi_inter
+ {{ hol arb }}
+ {{ lem arb }}
+ {{ ocaml assert false }}
+
+
+ field_typs :: 'FT_' ::= {{ phantom }}
+ {{ com Record fields }}
+ | id1 : t1 , .. , idn : tn :: :: fields
+
+ E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::= {{ phantom }}
+ {{ hol (id |-> t) }}
+ {{ lem map x f_desc }}
+ {{ com Record environments }}
+ | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn } :: :: concrete
+ {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }}
+ {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) Pmap.empty) }}
+ | E_r1 u+ .. u+ E_rn :: M :: union
+ {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }}
+ {{ lem (List.fold_right union_map [[E_r1..E_rn]] Pmap.empty) }}
+ {{ ocaml (assert false) }}
+
+ts :: ts_ ::= {{ phantom }}
+ | t1 , .. , tn :: :: lst
+
+formula :: formula_ ::=
+ | judgement :: :: judgement
+
+ | formula1 .. formulan :: :: dots
+
+ | E_k ( id ) gives kinf :: :: lookup_k
+ {{ com Kind lookup }}
+ {{ hol (FLOOKUP [[E_k]] [[id]] = SOME [[k]]) }}
+ {{ lem Pmap.find [[id]] [[E_k]] = [[k]] }}
+
+ | E_t ( id ) gives tinf :: :: lookup_t
+ {{ com Type lookup }}
+ {{ 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 }}
+
+ | E_r ( id0 .. idn ) gives t , ts :: :: lookup_r
+ {{ com Record lookup }}
+
+ | E_r ( t ) gives id0 : t0 .. idn : tn :: :: lookup_rt
+ {{ com Record looup by type }}
+
+ | dom ( E_t1 ) inter dom ( E_t2 ) = emptyset :: :: E_t_disjoint
+ {{ hol (DISJOINT (FDOM [[E_t1]]) (FDOM [[E_t2]])) }}
+ {{ lem disjoint (Pmap.domain [[E_t1]]) (Pmap.domain [[E_t2]]) }}
+
+ | dom ( E_k1 ) inter dom ( E_k2 ) = emptyset :: :: E_k_disjoint
+ {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }}
+ {{ lem disjoint (Pmap.domain [[E_f1]]) (Pmap.domain [[E_f2]]) }}
+
+ | 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 }}
+
+ | id NOTIN dom ( E_k ) :: :: notin_dom_k
+ {{ hol ([[id]] NOTIN FDOM [[E_k]]) }}
+ {{ lem Pervasives.not (Pmap.mem [[id]] [[E_k]]) }}
+
+ | id NOTIN dom ( E_t ) :: :: notin_dom_t
+ {{ hol ([[id]] NOTIN FDOM [[E_t]]) }}
+ {{ lem Pervasives.not (Pmap.mem [[id]] [[E_t]]) }}
+
+ | id0 : t0 .. idn : tn SUBSET id'0 : t'0 .. id'i : t'i :: :: subsetFields
+
+ | num1 lt ... lt numn :: :: increasing
+
+ | num1 gt ... gt numn :: :: decreasing
+
+ | E_k1 = E_k2 :: :: E_k_eqn
+ {{ ichl ([[E_k1]] = [[E_k2]]) }}
+
+ | E_t1 = E_t2 :: :: E_t_eqn
+ {{ ichl ([[E_t1]] = [[E_t2]]) }}
+
+ | E_r1 = E_r2 :: :: E_r_eqn
+ {{ ichl ([[E_r1]] = [[E_r2]]) }}
+
+ | E1 = E2 :: :: E_eqn
+ {{ ichl ([[E1]] = [[E2]]) }}
+
+ | S_N1 = S_N2 :: :: S_N_eqn
+ {{ ichl ([[S_N1]] = [[S_N2]]) }}
+
+ | I1 = I2 :: :: I_eqn
+ {{ ichl ([[I1]] = [[I2]]) }}
+
+ | t1 = t2 :: :: t_eq
+ {{ ichl ([[t1]] = [[t2]]) }}
+ | ne1 = ne2 :: :: ne_eq
+ {{ ichl ([[ne1]] = [[ne2]]) }}
+
+
defns
check_t :: '' ::=
@@ -17,6 +338,11 @@ E_k |-t t ok :: :: check_t :: check_t_
------------------------------------------------------------ :: varInfer
E_k |-t id ok
+ E_k(id) gives K_Abbrev t
+ E_k u- {id |-> K_Abbrev t} |-t t ok
+ ------------------------------------------------------------ :: varAbbrev
+ E_k |-t id ok
+
E_k |-t t1 ok
E_k |-t t2 ok
E_k |-e effects ok
@@ -127,47 +453,96 @@ defn
E_k |- t1 = t2 :: :: teq :: teq_
{{ com Type equality }}
by
-%% %
-%% % TD |- t ok
-%% % ------------------------------------------------------------ :: refl
-%% % TD |- t = t
-%% %
-%% % TD |- t2 = t1
-%% % ------------------------------------------------------------ :: sym
-%% % TD |- t1 = t2
-%% %
-%% % TD |- t1 = t2
-%% % TD |- t2 = t3
-%% % ------------------------------------------------------------ :: trans
-%% % TD |- t1 = t3
-%% %
-%% % TD |- t1 = t3
-%% % TD |- t2 = t4
-%% % ------------------------------------------------------------ :: arrow
-%% % TD |- t1 -> t2 = t3 -> t4
-%% %
-%% % TD |- t1 = u1 .... TD |- tn = un
-%% % ------------------------------------------------------------ :: tup
-%% % TD |- t1*....*tn = u1*....*un
-%% %
-%% % TD(p) gives a1..an
-%% % TD |- t1 = u1 .. TD |- tn = un
-%% % ------------------------------------------------------------ :: app
-%% % TD |- p t1 .. tn = p u1 .. un
-%% %
-%% % TD(p) gives a1..an . u
-%% % ------------------------------------------------------------ :: expand
-%% % TD |- p t1 .. tn = {a1|->t1..an|->tn}(u)
-%% %
-%% % ne = normalize (ne')
-%% % ---------------------------------------------------------- :: nexp
-%% % TD |- ne = ne'
-%% %
-%% %
+
+E_k |-t t ok
+------------------------------------------------------------ :: refl
+E_k |- t = t
+
+E_k |- t2 = t1
+------------------------------------------------------------ :: sym
+E_k |- t1 = t2
+
+E_k |- t1 = t2
+E_k |- t2 = t3
+------------------------------------------------------------ :: trans
+E_k |- t1 = t3
+
+E_k(id) gives K_Abbrev u
+E_k |- u = t
+------------------------------------------------------------ :: abbrev
+E_k |- id = t
+
+E_k |- t1 = t3
+E_k |- t2 = t4
+------------------------------------------------------------ :: arrow
+E_k |- t1 -> t2 effects tag = t3 -> t4 effects tag
+
+E_k |- t1 = u1 .... E_k |- tn = un
+------------------------------------------------------------ :: tup
+E_k |- (t1*....*tn) = (u1*....*un)
+
+E_k(id) gives K_Lam (k1 .. kn -> K_Typ)
+E_k,k1 |- t_arg1 = t_arg'1 .. E_k,kn |- t_argn = t_arg'n
+------------------------------------------------------------ :: app
+E_k |- id t_arg1 .. t_argn = id t_arg'1 .. t_arg'n
+
+defn
+E_k , k |- t_arg = t_arg' :: :: targeq :: targeq_ by
+
+defns
+convert_kind :: '' ::=
+
+defn
+E_k |- kind ~> k :: :: convert_kind :: convert_kind_ by
defns
convert_typ :: '' ::=
-
+
+defn
+E_k |- quant_item ~> E_k1 , S_N :: :: convert_quants :: convert_quants_
+{{ com Convert source quantifiers to kind environments and constraints }}
+by
+
+E_k |- kind ~> k
+----------------------------------------------------------- :: kind
+E_k |- kind id ~> {id |-> k}, {}
+
+E_k(id) gives k
+----------------------------------------------------------- :: nokind
+E_k |- id ~> {id |-> k},{}
+
+|- nexp1 ~> ne1
+|- nexp2 ~> ne2
+----------------------------------------------------------- :: eq
+E_k |- nexp1 = nexp2 ~> {}, {ne1 = ne2}
+
+|- nexp1 ~> ne1
+|- nexp2 ~> ne2
+----------------------------------------------------------- :: gteq
+E_k |- nexp1 >= nexp2 ~> {}, {ne1 >= ne2}
+
+|- nexp1 ~> ne1
+|- nexp2 ~> ne2
+----------------------------------------------------------- :: lteq
+E_k |- nexp1 <= nexp2 ~> {}, {ne1 <= ne2}
+
+----------------------------------------------------------- :: in
+E_k |- id IN {num1 , ... , numn} ~> {}, {id IN {num1 , ..., numn}}
+
+defn
+E_k |- typschm ~> t , E_k2 , S_N :: :: convert_typschm :: convert_typschm_
+{{ com Convert source types with typeschemes to internal types and kind environments }}
+by
+
+E_k |- typ ~> t
+----------------------------------------------------------- :: noquant
+E_k |- typ ~> t,E_k,{}
+
+E_k |- quant_item1 ~> E_k1, S_N1 ... E_k |- quant_itemn ~> E_kn, S_Nn
+E_k u+ E_k1 u+ ... u+ E_kn |- typ ~> t
+----------------------------------------------------------- :: quant
+E_k |- forall quant_item1 , ... , quant_itemn . typ ~> t, E_k1 u+ ... u+ E_kn, S_N1 u+ ... u+ S_Nn
+
defn
E_k |- typ ~> t :: :: convert_typ :: convert_typ_
{{ com Convert source types to internal types }}
@@ -207,22 +582,25 @@ defn
{{ com Convert and normalize numeric expressions }}
by
-%% % ------------------------------------------------------------ :: var
-%% % |- N l ~> N
-%% %
-%% % ------------------------------------------------------------ :: num
-%% % |- num l ~> nat
-%% %
-%% % |- nexp1 ~> ne1
-%% % |- nexp2 ~> ne2
-%% % ------------------------------------------------------------ :: mult
-%% % |- nexp1 * nexp2 l ~> ne1 * ne2
-%% %
-%% % |- nexp1 ~> ne1
-%% % |- nexp2 ~> ne2
-%% % ----------------------------------------------------------- :: add
-%% % |- nexp1 + nexp2 l ~> :Ne_add: ne1 + ne2
-%% %
+------------------------------------------------------------ :: var
+|- id ~> id
+
+------------------------------------------------------------ :: num
+|- num ~> num
+
+|- nexp1 ~> ne1
+|- nexp2 ~> ne2
+------------------------------------------------------------ :: mult
+|- nexp1 * nexp2 ~> ne1 * ne2
+
+|- nexp1 ~> ne1
+|- nexp2 ~> ne2
+----------------------------------------------------------- :: add
+|- nexp1 + nexp2 ~> ne1 + ne2
+
+|- nexp ~> ne
+------------------------------------------------------------ :: exp
+|- 2 ** nexp ~> 2 ** ne
defn
E_k |- t :> t' , S_N :: :: coerce_typ :: coerce_typ_ by
@@ -233,13 +611,13 @@ E_k |- t :> u, {}
E_k |- t1 :> u1, S_N1 .. E_k |- tn :> un, S_Nn
-------------------------------------- :: tuple
-E_k |- (t1 * .. * tn) :> (u1 * .. * un), u+ S_N1 .. S_Nn
+E_k |- (t1 * .. * tn) :> (u1 * .. * un), S_N1 u+ .. u+ S_Nn
-------------------------------------- :: enum
E_k |- enum ne1 ne2 order :> enum ne3 ne4 order, {ne3 <= ne1, ne3+ne4 >= ne1 + ne2}
-------------------------------------- :: toEnum
-E_k |- vector ne1 ne2 order bit :> enum ne3 ne4 order, { ne3 = zero, ne4 = 2 ^^ ne2}
+E_k |- vector ne1 ne2 order :t_arg_typ: bit :> enum ne3 ne4 order, { ne3 = zero, ne4 = 2** ne2}
%% Will also need environment of enumerations to converte between
@@ -303,6 +681,11 @@ id NOTIN dom(E_t1)
------------------------------------------------------------ :: as
<E_t,E_r,E_k> |- (pat as id) : t gives (E_t1 u+ {id|->t}),S_N
+<E_t,E_r,E_k> |- pat : t gives E_t1,S_N
+E_t(id) gives {}, {}, Default, t
+------------------------------------------------------------ :: as_default
+<E_t,E_r,E_k> |- (pat as id) : t gives (E_t1 u+ {id|->t}),S_N
+
E_k |- typ ~> t
<E_t,E_r,E_k> |- pat : t gives E_t1,S_N
------------------------------------------------------------ :: typ
@@ -315,7 +698,11 @@ disjoint doms(E_t1,..,E_tn)
<E_t,E_r,E_k> |- id pat1 .. patn : id t_args gives u+ E_t1 .. E_tn, S_N1 u+ .. u+ S_Nn
E_k |-t t ok
- ------------------------------------------------------------ :: var
+------------------------------------------------------------ :: var
+<E_t,E_r,E_k> |- :P_id: id : t gives (E_t u+ {id|->t}),{}
+
+E_t(id) gives {},{},Default,t
+------------------------------------------------------------ :: var_default
<E_t,E_r,E_k> |- :P_id: id : t gives (E_t u+ {id|->t}),{}
E_r(</idi//i/>) gives id t_args, (</ti//i/>)
@@ -374,30 +761,33 @@ E |- exp : t gives I , E_t :: :: check_exp :: check_exp_
{{ com Typing expressions, collecting nexp constraints, effects, and new bindings }}
by
-%% TODO::: if t is a reg, need to distinguish here between reg and ref cell access, and add to effect if reg
+E |- exp : u gives <S_N,effects>,E_t1
+E_k |- u :> t, S_N2
+------------------------------------------------------------ :: coerce
+<E_t,E_r,E_k> |- exp : t gives <S_N u+ S_N2,effects>,E_t1
+
+%% TODO::: if t is a reg, need to distinguish here between reg and ref cell access, and add to effect if reg, need to look at possible type variables introduced here and do substitutions
E_t(id) gives t
------------------------------------------------------------ :: var
<E_t,E_r,E_k> |- id : t gives Ie,E_t
+% Need to take into account possible type variables here
E_t(id) gives t' -> t effect {} Ctor {}
<E_t,E_r,E_k> |- exp : t' gives I,E_t
------------------------------------------------------------ :: ctor
<E_t,E_r,E_k> |- id exp : t gives I,E_t
-%We need overloading here
-
+% Need to take into account possible type variables on result of id
E_t(id) gives t' -> t effects tag S_N
-<E_t,E_r,E_k> |- exp : u gives I,E_t
-E_k |- u :> t',S_N2
+<E_t,E_r,E_k> |- exp : t' gives I,E_t
------------------------------------------------------------ :: app
-<E_t,E_r,E_k> |- id exp : t gives I u+ <S_N u+ S_N2 ,effects>, E_t
+<E_t,E_r,E_k> |- id exp : t gives I u+ <S_N,effects>, E_t
-E_t(id) gives (t1 * t2) -> t effects tag S_N
-<E_t,E_r,E_k> |- exp1 : t1 gives I2,E_t
-<E_t,E_r,E_k> |- exp2 : t2 gives I3,E_t
+E_t(id) gives t' -> t effects tag S_N
+<E_t,E_r,E_k> |- (exp1,exp2) : t' gives I,E_t
------------------------------------------------------------ :: infix_app
-<E_t,E_r,E_k> |- :E_app_infix: exp1 id exp2 : t gives I2 u+ I3 u+ <S_N, effects>, E_t
+<E_t,E_r,E_k> |- :E_app_infix: exp1 id exp2 : t gives I u+ <S_N, effects>, E_t
E_r(</idi//i/>) gives id t_args, </ti//i/>
</ <E_t,E_r,E_k> |- expi : ti gives Ii,E_t//i/>
@@ -464,16 +854,14 @@ E_r (id t_args) gives </idi : ti//i/> id : t </id'j : t'j//j/>
------------------------------------------------------------ :: case
<E_t,E_r,E_k> |- switch exp { </case pati -> expi//i/> }: u gives I u+ </Ii u+ <S_Ni,pure>//i/>, inter </E_t'i//i/> u- </E_ti//i/>
-<E_t,E_r,E_k> |- exp : t gives I,E_t
-E_k |- typ ~> u
-|- u :> t, S_N
+E |- exp : t gives I,E_t
------------------------------------------------------------ :: typed
-<E_t,E_r,E_k> |- (typ) exp : t gives I u+ <S_N,pure>,E_t
+<E_t,E_r,E_k> |- (typ) exp : t gives I,E_t
-<E_t,E_r,E_k> |- letbind gives E_t2, I1
-<(E_t u+ E_t2),E_r,E_k> |- exp : t gives I2
+<E_t,E_r,E_k> |- letbind gives E_t1, S_N, effects, {}
+<(E_t u+ E_t1),E_r,E_k> |- exp : t gives I2, E_t2
------------------------------------------------------------ :: let
-<E_t,E_r,E_k> |- let letbind in exp : t gives I1 u+ I2, E_t
+<E_t,E_r,E_k> |- letbind in exp : t gives <S_N,effects> u+ I2, E_t
E |- exp1 : t1 gives I1,E_t .... E |- expn : tn gives In,E_t
------------------------------------------------------------ :: tup
@@ -505,6 +893,14 @@ E |- exp1 :: exp2 : list t gives I1 u+ I2,E_t
------------------------------------------------------------ :: lit
<E_t,E_r,E_k> |- lit : t gives Ie,E_t
+<E_t,E_r,E_k> |- exp : t gives I, E_t1
+------------------------------------------------------------ :: blockbase
+<E_t,E_r,E_k> |- { exp } : t gives I, E_t
+
+<E_t,E_r,E_k> |- exp : u gives I1, E_t1
+<(E_t u+ E_t1),E_r,E_k> |- { </expi//i/> } : t gives I2, E_t2
+------------------------------------------------------------ :: blockrec
+<E_t,E_r,E_k> |- { exp ; </expi//i/> } : t gives I1 u+ I2, E_t
%% % defn
%% % TD , E , E_l |- funcl gives { x |-> t } , S_c , S_N :: :: check_funcl :: check_funcl_
@@ -526,301 +922,139 @@ E |- exp1 :: exp2 : list t gives I1 u+ I2,E_t
%% %
defn
-E |- letbind gives I , E_t :: :: check_letbind :: check_letbind_
+E |- letbind gives E_t , S_N , effects , E_k :: :: check_letbind :: check_letbind_
{{ com Build the environment for a let binding, collecting index constraints }}
by
-<E_t,E_r,E_k> |- pat : t gives E_t1, S_N
-<E_t,E_r,E_k2> |- exp : t gives S_c,S_N
-E_k |- typschn ~> t,E_k2
+<E_t,E_r,E_k u+ E_k2> |- pat : t gives E_t1, S_N1
+<E_t,E_r,E_k u+ E_k2> |- exp : t gives <S_N2,effects>,E_t2
+E_k |- typschm ~> t,E_k2,S_N
------------------------------------------------------------ :: val_annot
-<E_t,E_r,E_k> |- typschm pat = exp l gives I,E_t
+<E_t,E_r,E_k> |- let typschm pat = exp gives E_t1, S_N u+ S_N1 u+ S_N2, effects, E_k2
-%% % TD,E,E_l1 |- pat : t gives E_l2
-%% % TD,E,E_l1 |- exp : t gives S_c,S_N
-%% % ------------------------------------------------------------ :: val_noannot
-%% % TD,E,E_l1 |- pat = exp l gives E_l2,S_c,S_N
+<E_t,E_r,E_k> |- pat : t gives E_t1,S_N1
+<(E_t u+ E_t1),E_r,E_k> |- exp : t gives <S_N2,effects>,E_t2
+------------------------------------------------------------ :: val_noannot
+<E_t,E_r,E_k> |- let pat = exp gives E_t1, S_N1 u+ S_N2, effects,{}
-%% % defns
-%% % check_texp_tc :: '' ::=
-%% %
-%% % defn
-%% % xs , TD1 , E |- tc td gives TD2 , E_p :: :: check_texp_tc :: check_texp_tc_
-%% % {{ com Extract the type constructor information }}
-%% % by
-%% %
-%% % tnvars ~> tnvs
-%% % TD,E |- typ ~> t
-%% % duplicates(tnvs) = emptyset
-%% % FV(t) SUBSET tnvs
-%% % </yi.//i/>x NOTIN dom(TD)
-%% % ------------------------------------------------------------ :: abbrev
-%% % </yi//i/>,TD,E |- tc x l tnvars = typ gives {</yi.//i/>x|->tnvs.t},{x|-></yi.//i/>x}
-%% %
-%% % tnvars ~> tnvs
-%% % duplicates(tnvs) = emptyset
-%% % </yi.//i/>x NOTIN dom(TD)
-%% % ------------------------------------------------------------ :: abstract
-%% % </yi//i/>,TD,E1 |- tc x l tnvars gives {</yi.//i/>x|->tnvs},{x|-></yi.//i/>x}
-%% %
-%% % tnvars ~> tnvs
-%% % duplicates(tnvs) = emptyset
-%% % </yi.//i/>x NOTIN dom(TD)
-%% % ------------------------------------------------------------ :: rec
-%% % </yi//i/>,TD1,E |- tc x l tnvars = <| x_l1 : typ1 ; ... ; x_lj : typj semi_opt |> gives {</yi.//i/>x|->tnvs},{x|-></yi.//i/>x}
-%% %
-%% % tnvars ~> tnvs
-%% % duplicates(tnvs) = emptyset
-%% % </yi.//i/>x NOTIN dom(TD)
-%% % ------------------------------------------------------------ :: var
-%% % </yi//i/>,TD1,E |- tc x l tnvars = bar_opt ctor_def1 | ... | ctor_defj gives {</yi.//i/>x|->tnvs},{x|-></yi.//i/>x}
-%% %
-%% % defns
-%% % check_texps_tc :: '' ::=
-%% %
-%% % defn
-%% % xs , TD1 , E |- tc td1 .. tdi gives TD2 , E_p :: :: check_texps_tc :: check_texps_tc_
-%% % {{ com Extract the type constructor information }}
-%% % by
-%% %
-%% % ------------------------------------------------------------ :: empty
-%% % xs,TD,E |- tc gives {},{}
-%% %
-%% % :check_texp_tc: xs,TD1,E |- tc td gives TD2,E_p2
-%% % xs,TD1 u+ TD2,E u+ <{},E_p2,{},{}> |- tc </tdi//i/> gives TD3,E_p3
-%% % dom(E_p2) inter dom(E_p3) = emptyset
-%% % ------------------------------------------------------------ :: abbrev
-%% % xs,TD1,E |- tc td </tdi//i/> gives TD2 u+ TD3,E_p2 u+ E_p3
-%% %
-%% % defns
-%% % check_texp :: '' ::=
-%% %
-%% % defn
-%% % TD , E |- tnvs p = texp gives < E_f , E_x > :: :: check_texp :: check_texp_
-%% % {{ com Check a type definition, with its path already resolved }}
-%% % by
-%% %
-%% % ------------------------------------------------------------ :: abbrev
-%% % TD,E |- tnvs p = typ gives <{},{}>
-%% %
-%% % </TD,E |- typi ~> ti//i/>
-%% % names = {</xi//i/>}
-%% % duplicates(</xi//i/>) = emptyset
-%% % </FV(ti) SUBSET tnvs//i/>
-%% % E_f = {</xi|-> <forall tnvs. p -> ti, (xi of names)>//i/>}
-%% % ------------------------------------------------------------ :: rec
-%% % TD,E |- tnvs p = <| </x_li:typi//i/> semi_opt |> gives <E_f,{}>
-%% %
-%% % </TD,E |- typsi ~> t_multii//i/>
-%% % names = {</xi//i/>}
-%% % duplicates(</xi//i/>) = emptyset
-%% % </FV(t_multii) SUBSET tnvs//i/>
-%% % E_x = {</xi|-><forall tnvs. t_multii -> p, (xi of names)>//i/>}
-%% % ------------------------------------------------------------ :: var
-%% % TD,E |- tnvs p = bar_opt </x_li of typsi//i/> gives <{},E_x>
-%% %
-%% % defns
-%% % check_texps :: '' ::=
-%% %
-%% % defn
-%% % xs , TD , E |- td1 .. tdn gives < E_f , E_x > :: :: check_texps :: check_texps_ by
-%% %
-%% % ------------------------------------------------------------ :: empty
-%% % </yi//i/>,TD,E |- gives <{},{}>
-%% %
-%% % tnvars ~> tnvs
-%% % TD,E1 |- tnvs </yi.//i/>x = texp gives <E_f1,E_x1>
-%% % </yi//i/>,TD,E |- </tdj//j/> gives <E_f2,E_x2>
-%% % dom(E_x1) inter dom(E_x2) = emptyset
-%% % dom(E_f1) inter dom(E_f2) = emptyset
-%% % ------------------------------------------------------------ :: cons_concrete
-%% % </yi//i/>,TD,E |- x l tnvars = texp </tdj//j/> gives <E_f1 u+ E_f2, E_x1 u+ E_x2>
-%% %
-%% % </yi//i/>,TD,E |- </tdj//j/> gives <E_f,E_x>
-%% % ------------------------------------------------------------ :: cons_abstract
-%% % </yi//i/>,TD,E |- x l tnvars </tdj//j/> gives <E_f,E_x>
-%% %
-%% % defns
-%% % convert_class :: '' ::=
-%% %
-%% % defn
-%% % TC , E |- id ~> p :: :: convert_class :: convert_class_
-%% % {{ com Lookup a type class }}
-%% % by
-%% %
-%% % E(id) gives p
-%% % TC(p) gives xs
-%% % ------------------------------------------------------------ :: all
-%% % TC,E |- id ~> p
-%% %
-%% % defns
-%% % solve_class_constraint :: '' ::=
-%% %
-%% % defn
-%% % I |- ( p t ) 'IN' semC :: :: solve_class_constraint :: solve_class_constraint_
-%% % {{ com Solve class constraint }}
-%% % by
-%% %
-%% % ------------------------------------------------------------ :: immediate
-%% % I |- (p a) IN (p1 tnv1) .. (pi tnvi) (p a) (p'1 tnv'1) .. (p'j tnv'j)
-%% %
-%% % (p1 tnv1)..(pn tnvn)=>(p t) IN I
-%% % I |- (p1 t_subst(tnv1)) IN semC .. I |- (pn t_subst(tnvn)) IN semC
-%% % ------------------------------------------------------------ :: chain
-%% % I |- (p t_subst(t)) IN semC
-%% %
-%% % defns
-%% % solve_class_constraints :: '' ::=
-%% %
-%% % defn
-%% % I |- S_c gives semC :: :: solve_class_constraints :: solve_class_constraints_
-%% % {{ com Solve class constraints }}
-%% % by
-%% %
-%% % I |- (p1 t1) IN semC .. I |- (pn tn) IN semC
-%% % ------------------------------------------------------------ :: all
-%% % I |- {(p1 t1), .., (pn tn)} gives semC
-%% %
-%% % defns
-%% % check_val_def :: '' ::=
-%% %
-%% % defn
-%% % TD , I , E |- val_def gives E_x :: :: check_val_def :: check_val_def_
-%% % {{ com Check a value definition }}
-%% % by
-%% %
-%% % TD,E,{} |- letbind gives {</xi|->ti//i/>},S_c,S_N
-%% % %TODO, check S_N constraints
-%% % I |- S_c gives semC
-%% % </FV(ti) SUBSET tnvs//i/>
-%% % FV(semC) SUBSET tnvs
-%% % ------------------------------------------------------------ :: val
-%% % TD,I,E1 |- let targets_opt letbind gives {</xi |-> <forall tnvs. semC => ti, let>//i/>}
-%% %
-%% % </TD,E,E_l |- funcli gives {xi|->ti},S_ci,S_Ni//i/>
-%% % I |- S_c gives semC
-%% % </FV(ti) SUBSET tnvs//i/>
-%% % FV(semC) SUBSET tnvs
-%% % compatible overlap(</xi|->ti//i/>)
-%% % E_l = {</xi|->ti//i/>}
-%% % ------------------------------------------------------------ :: recfun
-%% % TD,I,E |- let rec targets_opt </funcli//i/> gives {</xi|-><forall tnvs. semC => ti,let>//i/>}
-%% %
-%% % defns
-%% % check_t_instance :: '' ::=
-%% %
-%% % defn
-%% %
-%% % TD , ( a1 , .. , an ) |- t instance :: :: check_t_instance :: check_t_instance_
-%% % {{ com Check that $\ottnt{t}$ be a typeclass instance }}
-%% % by
-%% %
-%% % ------------------------------------------------------------ :: var
-%% % TD , (a) |- a instance
-%% %
-%% % ------------------------------------------------------------ :: tup
-%% % TD , (a1, ...., an) |- a1 * .... * an instance
-%% %
-%% % ------------------------------------------------------------ :: fn
-%% % TD , (a1, a2) |- a1 -> an instance
-%% %
-%% % TD(p) gives a'1..a'n
-%% % ------------------------------------------------------------ :: tc
-%% % TD , (a1, .., an) |- p a1 .. an instance
-%% %
-%% % defns
-%% % check_defs :: '' ::=
-%% %
-%% % defn
-%% %
-%% % </ zj // j /> , D1 , E1 |- def gives D2 , E2 :: :: check_def :: check_def_
-%% % {{ com Check a definition }}
-%% % by
-%% %
-%% %
-%% % </zj//j/>,TD1,E |- tc </tdi//i/> gives TD2,E_p
-%% % </zj//j/>,TD1 u+ TD2,E u+ <{},E_p,{},{}> |- </tdi//i/> gives <E_f,E_x>
-%% % ------------------------------------------------------------ :: type
-%% % </zj//j/>,<TD1,TC,I>,E |- type </tdi//i/> l gives <TD2,{},{}>,<{},E_p,E_f,E_x>
-%% %
-%% % TD,I,E |- val_def gives E_x
-%% % ------------------------------------------------------------ :: val_def
-%% % </zj//j/>,<TD,TC,I>,E |- val_def l gives empty,<{},{},{},E_x>
-%% %
-%% % </TD,E1,E_l |- rulei gives {xi|->ti},S_ci,S_Ni//i/>
-%% % %TODO Check S_N constraints
-%% % I |- </S_ci//i/> gives semC
-%% % </FV(ti) SUBSET tnvs//i/>
-%% % FV(semC) SUBSET tnvs
-%% % compatible overlap(</xi|->ti//i/>)
-%% % E_l = {</xi|->ti//i/>}
-%% % E2 = <{},{},{},{</xi |-><forall tnvs. semC => ti,let>//i/>}>
-%% % ------------------------------------------------------------ :: indreln
-%% % </zj//j/>,<TD,TC,I>,E1 |- indreln targets_opt </rulei//i/> l gives empty,E2
-%% %
-%% % </zj//j/> x,D1,E1 |- defs gives D2,E2
-%% % ------------------------------------------------------------ :: module
-%% % </zj//j/>,D1,E1 |- module x l1 = struct defs end l2 gives D2,<{x|->E2},{},{},{}>
-%% %
-%% % E1(id) gives E2
-%% % ------------------------------------------------------------ :: module_rename
-%% % </zj//j/>,D,E1 |- module x l1 = id l2 gives empty,<{x|->E2},{},{},{}>
-%% %
-%% % TD,E |- typ ~> t
-%% % FV(t) SUBSET </ai//i/>
-%% % FV(</a'k//k/>) SUBSET </ai//i/>
-%% % </TC,E |- idk ~> pk//k/>
-%% % E' = <{},{},{},{x|-><forall </ai//i/>. </(pk a'k)//k/> => t,val>}>
-%% % ------------------------------------------------------------ :: spec
-%% % </zj//j/>,<TD,TC,I>,E |- val x l1 : forall </ai l''i//i/>. </idk a'k l'k//k/> => typ l2 gives empty,E'
-%% %
-%% % </TD,E1 |- typi ~> ti//i/>
-%% % </FV(ti) SUBSET a//i/>
-%% % :formula_p_eq: p = </zj.//j/>x
-%% % E2 = <{},{x|->p},{},{</yi |-><forall a. (p a) => ti,method>//i/>}>
-%% % TC2 = {p|-></yi//i/>}
-%% % p NOTIN dom(TC1)
-%% % ------------------------------------------------------------ :: class
-%% % </zj//j/>,<TD,TC1,I>,E1 |- class (x l a l'') </val yi li : typi li//i/> end l' gives <{},TC2,{}>,E2
-%% %
-%% % E = <E_m,E_p,E_f,E_x>
-%% % TD,E |- typ' ~> t'
-%% % TD,(</ai//i/>) |- t' instance
-%% % tnvs = </ai//i/>
-%% % duplicates(tnvs) = emptyset
-%% % </TC,E |- idk ~> pk//k/>
-%% % FV(</a'k//k/>) SUBSET tnvs
-%% % E(id) gives p
-%% % TC(p) gives </zj//j/>
-%% % I2 = { </=> (pk a'k)//k/> }
-%% % </TD,I union I2,E |- val_defn gives E_xn//n/>
-%% % disjoint doms(</E_xn//n/>)
-%% % </E_x(xk) gives <forall a''. (p a'') => tk,method>//k/>
-%% % {</xk |-> <forall tnvs. => {a''|->t'}(tk),let>//k/>} = </E_xn//n/>
-%% % :formula_xs_eq:</xk//k/> = </zj//j/>
-%% % I3 = {</(pk a'k) => (p t')//k/>}
-%% % (p {</ai |-> a'''i//i/>}(t')) NOTIN I
-%% % ------------------------------------------------------------ :: instance_tc
-%% % </zj//j/>,<TD,TC,I>,E |- instance forall </ai l'i//i/>. </idk a'k l''k//k/> => (id typ') </val_defn ln//n/> end l' gives <{},{},I3>,empty
-%% %
-%% % defn
-%% % </ zj // j /> , D1 , E1 |- defs gives D2 , E2 :: :: check_defs :: check_defs_
-%% % {{ com Check definitions, given module path, definitions and environment }}
-%% % by
-%% %
-%% % % TODO: Check compatibility for duplicate definitions
-%% %
-%% % ------------------------------------------------------------ :: empty
-%% % </zj//j/>,D,E |- gives empty,empty
-%% %
-%% % :check_def: </zj//j/>,D1,E1 |- def gives D2,E2
-%% % </zj//j/>,D1 u+ D2,E1 u+ E2 |- </defi semisemi_opti // i/> gives D3,E3
-%% % ------------------------------------------------------------ :: relevant_def
-%% % </zj//j/>,D1,E1 |- def semisemi_opt </defi semisemi_opti // i/> gives D2 u+ D3, E2 u+ E3
-%% %
-%% % E1(id) gives E2
-%% % </zj//j/>,D1,E1 u+ E2 |- </defi semisemi_opti // i/> gives D3,E3
-%% % ------------------------------------------------------------ :: open
-%% % </zj//j/>,D1,E1 |- open id l semisemi_opt </defi semisemi_opti // i/> gives D3,E3
-%% %
+defns
+check_defs :: '' ::=
+
+defn
+E_k1 |- type_def gives E_t , E_k , E_r :: :: check_td :: check_td_
+{{ com Check a type definition }}
+by
+
+%Does abbrev need a type environment? Ouch if yes
+E_k |- typschm ~> t,E_k1,S_N
+----------------------------------------------------------- :: abbrev
+E_k |- typedef id naming_scheme_opt = typschm gives {},{id |-> K_Abbrev t},{}
+
+E_k |- typ1 ~> t1 .. E_k |- typn ~> tn
+E_r = { {id1:t1, .., idn:tn} |-> id }
+----------------------------------------------------------- :: unquant_record
+E_k |- typedef id naming_scheme_opt = const struct { typ1 id1 ; .. ; typn idn semi_opt } gives {},{id |-> K_Typ},E_r
+
+</ E_k |- quant_itemi ~>E_ki, S_Ni//i/>
+E_k u+ </E_ki//i/> |- typ1 ~> t1 .. E_k u+ </E_ki//i/> |- typn ~> tn
+{ id'1 |-> k1, .. ,id'm |-> km } = u+ </E_ki//i/>
+E_r = { {id1:t1, .., idn:tn} |-> {id'1 |-> k1, ..,id'm |-> km}, u+</S_Ni//i/>, None, id :t_arg_typ: id'1 .. :t_arg_typ: id'm }
+E_k1 = { id |-> K_Lam (k1 .. km -> K_Typ) }
+----------------------------------------------------------- :: quant_record
+E_k |- typedef id naming_scheme_opt = const struct forall </quant_itemi//i/> . { typ1 id1 ; .. ; typn idn semi_opt } gives {},E_k1,E_r
+
+E_t = { id1 |-> t1 -> :T_var: id pure Ctor {}, ..., idn |-> tn -> :T_var: id pure Ctor {} }
+E_k1 = { id |-> K_Typ }
+E_k u+ E_k1 |- typ1 ~> t1 ... E_k u+ E_k1 |- typn ~> tn
+------------------------------------------------------------ :: unquant_union
+E_k |- typedef id naming_scheme_opt = const union { typ1 id1 ; ... ; typn idn semi_opt } gives E_t,E_k1,{}
+
+</ E_k |- quant_itemi ~> E_ki, S_Ni//i/>
+{ id'1 |-> k1, ... , id'm |-> km } = u+ </E_ki//i/>
+E_k1 = { id |-> K_Lam (k1 ... km -> K_Typ) } u+ </E_ki//i/>
+E_k u+ E_k1 |- typ1 ~> t1 ... E_k u+ E_k1 |- typn ~> tn
+t = id :t_arg_typ: id'1 ... :t_arg_typ: id'm
+E_t = { id1 |-> E_k1, u+</S_Ni//i/>, Ctor, t1 -> t pure Ctor {}, ... , idn |-> E_k1, u+</S_Ni//i/>, Ctor, tn -> t pure Ctor {} }
+------------------------------------------------------------ :: quant_union
+E_k |- typedef id naming_scheme_opt = const union forall </quant_itemi//i/> . { typ1 id1 ; ... ; typn idn semi_opt } gives E_t,E_k1,{}
+
+% Save these as enumerations for coercion
+E_t = {id1 |-> id, ..., idn |-> id}
+------------------------------------------------------------- :: enumerate
+E_k |- typedef id naming_scheme_opt = enumerate { id1 ; ... ; idn semi_opt } gives E_t,{id |-> K_Typ},{}
+
+defn
+E |- fundef gives E_t , S_N :: :: check_fd :: check_fd_
+{{ com Check a function definition }}
+by
+
+defn
+E |- val_spec gives E_t :: :: check_spec :: check_spec_
+{{ com Check a value specification }}
+by
+
+E_k |- typschm ~> t, E_k1, S_N
+-------------------------------------------------------- :: val_spec
+<E_t,E_r,E_k> |- val typschm id gives {id |-> E_k1,S_N,None,t }
+
+E_k |- typschm ~> t, E_k1, S_N
+-------------------------------------------------------- :: extern
+<E_t,E_r,E_k> |- val extern typschm id = string gives {id |-> E_k1,S_N,Extern,t}
+
+defn
+E_k |- default_typing_spec gives E_t , E_k1 :: :: check_default :: check_default_
+{{ com Check a default typing specification }}
+by
+
+E_k |- base_kind ~> k
+------------------------------------------------------------ :: kind
+E_k |- default base_kind id gives {}, {id |-> k default }
+
+E_k |- typschm ~> t,E_k1,S_N
+------------------------------------------------------------ :: typ
+E_k |- default typschm id gives {id |-> E_k1,S_N,Default,t},{}
+
+defn
+
+E |- def gives E' :: :: check_def :: check_def_
+{{ com Check a definition }}
+by
+
+E_k |- type_def gives E_t1,E_k1,E_r1
+--------------------------------------------------------- :: tdef
+<E_t,E_r,E_k>|- type_def gives <E_t,E_r,E_k> u+ <E_t1,E_r1,E_k1>
+
+E |- fundef gives E_t,S_N
+--------------------------------------------------------- :: fdef
+E |- fundef gives E u+ <E_t,{},{}>
+
+E |- letbind gives {id1 |-> t1 , .. , idn |-> tn},S_N,pure,E_k
+S_N1 = resolve S_N
+--------------------------------------------------------- :: vdef
+E |- letbind gives E u+ <{id1 |-> E_k,S_N,None,t1 , .. , idn |-> E_k,S_N,None,tn},{},{}>
+
+E |- val_spec gives E_t
+--------------------------------------------------------- :: vspec
+E |- val_spec gives E u+ <E_t,{},{}>
+
+E_k |- default_typing_spec gives E_t, E_k
+--------------------------------------------------------- :: default
+<E_t,E_r,E_k> |- default_typing_spec gives E u+ <E_t,{},E_k>
+
+E_k |- typ ~> t
+---------------------------------------------------------- :: register
+<E_t,E_r,E_k> |- register typ id gives E u+ <{id |-> register t},{},{}>
+
+defn
+E |- defs gives E' :: :: check_defs :: check_defs_
+{{ com Check definitions, potentially given default environment of built-in library }}
+by
+
+------------------------------------------------------------ :: empty
+E |- gives E
+
+:check_def: E |- def gives E1
+E u+ E1 |- </defi// i/> gives E2
+------------------------------------------------------------ :: defs
+E |- def </defi// i/> gives E2
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:11:45 +0000