diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/Makefile | 10 | ||||
| -rw-r--r-- | language/l2.lem | 514 | ||||
| -rw-r--r-- | language/l2.ml | 18 | ||||
| -rw-r--r-- | language/l2.ott | 16 | ||||
| -rw-r--r-- | language/l2_rules.ott | 318 | ||||
| -rw-r--r-- | language/l2_typ.ott | 326 |
6 files changed, 743 insertions, 459 deletions
diff --git a/language/Makefile b/language/Makefile index d650f957..2076069c 100644 --- a/language/Makefile +++ b/language/Makefile @@ -9,7 +9,7 @@ all: l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem %Theory.uo: %Script.sml Holmake --qof -I $(OTTLIB) $@ -l2.tex: l2.ott l2_rules.ott +l2.tex: l2.ott l2_typ.ott l2_rules.ott ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ %.tex: %.ott @@ -21,12 +21,8 @@ l2.tex: l2.ott l2_rules.ott %Script.sml: %.ott ott -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^ -%.lem: %.ott - # work around what is probably a bug in -generate_aux_rules true: when we try to generate Lem code with - # that turned on, we get some surprising-looking parse failures in a - # few rules. Likely we're not doing the proper transform for rules - # generated from inductive relation syntax. - ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ +l2.lem: l2.ott l2_typ.ott + ott -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^ clean: rm -rf *~ diff --git a/language/l2.lem b/language/l2.lem index 630c976d..30027846 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -1,4 +1,4 @@ -(* generated by Ott 0.23 from: l2.ott *) +(* generated by Ott 0.24 from: l2_typ.ott l2.ott *) open import Pervasives open import Map @@ -8,7 +8,9 @@ open import Set_extra type l = | Unknown | Trans of string * maybe l - | Range of nat * nat + | Range of string * nat * nat * nat * nat + +type annot 'a = l * 'a val duplicates : forall 'a. list 'a -> list 'a @@ -20,30 +22,45 @@ val subst : forall 'a. list 'a -> list 'a -> bool type x = string (* identifier *) type ix = string (* infix identifier *) -type kid = (* variables with kind, ticked to differntiate from program variables *) - | Var of x - - -type base_kind = (* base kind *) +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_effect (* kind of effect sets *) -type nexp = (* expression of kind Nat, for vector sizes and origins *) +type base_kind = + | BK_aux of base_kind_aux * l + + +type kid_aux = (* variables with kind, ticked to differntiate from program variables *) + | Var of x + + +type kind_aux = (* kinds *) + | K_kind of list base_kind + + +type kid = + | Kid_aux of kid_aux * l + + +type kind = + | K_aux of kind_aux * l + + +type nexp_aux = (* expression of kind Nat, for vector sizes and origins *) | Nexp_var of kid (* variable *) | Nexp_constant of natural (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) | Nexp_exp of nexp (* exponential *) - -type kind = (* kinds *) - | K_kind of list base_kind +and nexp = + | Nexp_aux of nexp_aux * l -type base_effect = (* effect *) +type base_effect_aux = (* effect *) | BE_rreg (* read register *) | BE_wreg (* write register *) | BE_rmem (* read memory *) @@ -53,45 +70,78 @@ type base_effect = (* effect *) | BE_nondet (* nondeterminism from intra-instruction parallelism *) -type order = (* vector order specifications, of kind Order *) +type base_effect = + | BE_aux of base_effect_aux * l + + +type id_aux = (* Identifier *) + | Id of x + | DeIid of x (* remove infix status *) + + +type effect_aux = (* effect set, of kind Effects *) + | Effect_var of kid + | Effect_set of list base_effect (* effect set *) + + +type order_aux = (* vector order specifications, of kind Order *) | Ord_var of kid (* variable *) | Ord_inc (* increasing (little-endian) *) | Ord_dec (* decreasing (big-endian) *) -type effect = (* effect set, of kind Effects *) - | Effect_var of kid - | Effect_set of list base_effect (* effect set *) +type id = + | Id_aux of id_aux * l -type id = (* Identifier *) - | Id of x - | DeIid of x (* remove infix status *) +type effect = + | Effect_aux of effect_aux * l + + +type order = + | Ord_aux of order_aux * l let effect_union e1 e2 = match (e1,e2) with - | (Effect_set els,Effect_set els2) -> Effect_set (els++els2) + | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l end -type n_constraint = (* constraint over kind $Nat$ *) +type kinded_id_aux = (* optionally kind-annotated identifier *) + | KOpt_none of kid (* identifier *) + | KOpt_kind of kind * kid (* kind-annotated variable *) + + +type n_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 kid * list natural -type kinded_id = (* optionally kind-annotated identifier *) - | KOpt_none of kid (* identifier *) - | KOpt_kind of kind * kid (* kind-annotated variable *) +type kinded_id = + | KOpt_aux of kinded_id_aux * l + + +type n_constraint = + | NC_aux of n_constraint_aux * l -type quant_item = (* Either a kinded identifier or a nexp constraint for a typquant *) +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 n_constraint (* A constraint for this type *) -type lit = (* Literal constant *) +type quant_item = + | QI_aux of quant_item_aux * l + + +type typquant_aux = (* type quantifiers and constraints *) + | TypQ_tq of list quant_item + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) + + +type lit_aux = (* Literal constant *) | L_unit (* $() : unit$ *) | L_zero (* $bitzero : bit$ *) | L_one (* $bitone : bit$ *) @@ -104,7 +154,7 @@ type lit = (* Literal constant *) | L_string of string (* string constant *) -type typ = (* Type expressions, of kind $Type$ *) +type typ_aux = (* Type expressions, of kind $Type$ *) | Typ_wild (* Unspecified type *) | Typ_id of id (* Defined type *) | Typ_var of kid (* Type variable *) @@ -112,164 +162,390 @@ type typ = (* Type expressions, of kind $Type$ *) | Typ_tup of list typ (* Tuple type *) | Typ_app of id * list typ_arg (* type constructor application *) -and typ_arg = (* Type constructor arguments of all kinds *) +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_effect of effect +and typ_arg = + | Typ_arg_aux of typ_arg_aux * l -type typquant = (* type quantifiers and constraints *) - | TypQ_tq of list quant_item - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) + +type typquant = + | TypQ_aux of typquant_aux * l + + +type lit = + | L_aux of lit_aux * l -type pat = (* Pattern *) +type typschm_aux = (* type scheme *) + | TypSchm_ts of typquant * typ + + +type pat_aux 'a = (* 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_as of (pat 'a) * id (* named pattern *) + | P_typ of typ * (pat 'a) (* 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 (natural * 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 *) + | P_app of id * list (pat 'a) (* union constructor pattern *) + | P_record of list (fpat 'a) * bool (* struct pattern *) + | P_vector of list (pat 'a) (* vector pattern *) + | P_vector_indexed of list (natural * (pat 'a)) (* vector pattern (with explicit indices) *) + | P_vector_concat of list (pat 'a) (* concatenated vector pattern *) + | P_tup of list (pat 'a) (* tuple pattern *) + | P_list of list (pat 'a) (* list pattern *) -and fpat = (* Field pattern *) - | FP_Fpat of id * pat +and pat 'a = + | P_aux of (pat_aux 'a) * annot 'a +and fpat_aux 'a = (* Field pattern *) + | FP_Fpat of id * (pat 'a) -type typschm = (* type scheme *) - | TypSchm_ts of typquant * typ +and fpat 'a = + | FP_aux of (fpat_aux 'a) * annot 'a -type exp = (* Expression *) - | E_block of list exp (* block (parsing conflict with structs?) *) +type typschm = + | TypSchm_aux of typschm_aux * l + + +type exp_aux 'a = (* Expression *) + | E_block of list (exp 'a) (* 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 id * 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 * order * exp (* loop *) - | E_vector of list exp (* vector (indexed from 0) *) - | E_vector_indexed of list (natural * exp) (* vector (indexed consecutively) *) - | E_vector_access of exp * exp (* vector access *) - | E_vector_subrange of exp * exp * exp (* subvector extraction *) - | E_vector_update of exp * exp * exp (* vector functional update *) - | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *) - | E_list of list exp (* list *) - | E_cons of exp * exp (* cons *) - | E_record of fexps (* struct *) - | E_record_update of exp * fexps (* functional update of struct *) - | E_field of exp * id (* field projection from struct *) - | E_case of exp * list pexp (* pattern matching *) - | E_let of letbind * exp (* let expression *) - | E_assign of lexp * exp (* imperative assignment *) - -and lexp = (* lvalue expression *) + | E_cast of typ * (exp 'a) (* cast *) + | E_app of id * list (exp 'a) (* function application *) + | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *) + | E_tuple of list (exp 'a) (* tuple *) + | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *) + | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *) + | E_vector of list (exp 'a) (* vector (indexed from 0) *) + | E_vector_indexed of list (natural * (exp 'a)) (* vector (indexed consecutively) *) + | E_vector_access of (exp 'a) * (exp 'a) (* vector access *) + | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *) + | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *) + | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update (with vector) *) + | E_list of list (exp 'a) (* list *) + | E_cons of (exp 'a) * (exp 'a) (* cons *) + | E_record of (fexps 'a) (* struct *) + | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *) + | E_field of (exp 'a) * id (* field projection from struct *) + | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *) + | E_let of (letbind 'a) * (exp 'a) (* let expression *) + | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *) + +and exp 'a = + | E_aux of (exp_aux 'a) * annot 'a + +and lexp_aux 'a = (* lvalue expression *) | LEXP_id of id (* identifier *) - | LEXP_memory of id * list exp (* memory write via function call *) - | LEXP_vector of lexp * exp (* vector element *) - | LEXP_vector_range of lexp * exp * exp (* subvector *) - | LEXP_field of lexp * id (* struct field *) + | LEXP_memory of id * list (exp 'a) (* memory write via function call *) + | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *) + | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *) + | LEXP_field of (lexp 'a) * id (* struct field *) -and fexp = (* Field-expression *) - | FE_Fexp of id * exp +and lexp 'a = + | LEXP_aux of (lexp_aux 'a) * annot 'a -and fexps = (* Field-expression list *) - | FES_Fexps of list fexp * bool +and fexp_aux 'a = (* Field-expression *) + | FE_Fexp of id * (exp 'a) -and pexp = (* Pattern match *) - | Pat_exp of pat * exp +and fexp 'a = + | FE_aux of (fexp_aux 'a) * annot 'a -and letbind = (* Let binding *) - | LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *) - | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) +and fexps_aux 'a = (* Field-expression list *) + | FES_Fexps of list (fexp 'a) * bool +and fexps 'a = + | FES_aux of (fexps_aux 'a) * annot 'a -type type_union = (* Type union constructors *) - | Tu_id of id - | Tu_ty_id of typ * id +and pexp_aux 'a = (* Pattern match *) + | Pat_exp of (pat 'a) * (exp 'a) + +and pexp 'a = + | Pat_aux of (pexp_aux 'a) * annot 'a +and letbind_aux 'a = (* Let binding *) + | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *) + | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *) -type funcl = (* Function clause *) - | FCL_Funcl of id * pat * exp +and letbind 'a = + | LB_aux of (letbind_aux 'a) * annot 'a -type effect_opt = (* Optional effect annotation for functions *) +type effect_opt_aux = (* Optional effect annotation for functions *) | Effect_opt_pure (* sugar for empty effect set *) | Effect_opt_effect of effect -type name_scm_opt = (* Optional variable-naming-scheme specification for variables of defined type *) +type rec_opt_aux = (* Optional recursive annotation for functions *) + | Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) + + +type funcl_aux 'a = (* Function clause *) + | FCL_Funcl of id * (pat 'a) * (exp 'a) + + +type name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) | Name_sect_none | Name_sect_some of string -type rec_opt = (* Optional recursive annotation for functions *) - | Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) +type type_union_aux = (* Type union constructors *) + | Tu_id of id + | Tu_ty_id of typ * id -type tannot_opt = (* Optional type annotation for functions *) +type tannot_opt_aux = (* Optional type annotation for functions *) | Typ_annot_opt_some of typquant * typ -type index_range = (* index specification, for bitfields in register types *) +type effect_opt = + | Effect_opt_aux of effect_opt_aux * l + + +type rec_opt = + | Rec_aux of rec_opt_aux * l + + +type funcl 'a = + | FCL_aux of (funcl_aux 'a) * annot 'a + + +type name_scm_opt = + | Name_sect_aux of name_scm_opt_aux * l + + +type type_union = + | Tu_aux of type_union_aux * l + + +type tannot_opt = + | Typ_annot_opt_aux of tannot_opt_aux * l + + +type index_range_aux = (* index specification, for bitfields in register types *) | BF_single of natural (* single index *) | BF_range of natural * natural (* index range *) | BF_concat of index_range * index_range (* concatenation of index ranges *) - -type val_spec = (* Value type specification *) - | VS_val_spec of typschm * id - | VS_extern_no_rename 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 *) +and index_range = + | BF_aux of index_range_aux * l -type scattered_def = (* Function and type union definitions that can be spread across +type scattered_def_aux 'a = (* Function and type union definitions that can be spread across a file. Each one must end in $id$ *) | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) - | SD_scattered_funcl of funcl (* scattered function definition clause *) + | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *) | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) | SD_scattered_unioncl of id * type_union (* scattered union definition member *) | SD_scattered_end of id (* scattered definition end *) -type fundef = (* Function definition *) - | FD_function of rec_opt * tannot_opt * effect_opt * list funcl +type type_def_aux 'a = (* Type definition body *) + | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) + | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) + | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) + | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) + + +type fundef_aux 'a = (* Function definition *) + | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) -type default_spec = (* Default kinding or typing assumption *) +type default_spec_aux 'a = (* Default kinding or typing assumption *) | DT_kind of base_kind * kid | DT_typ of typschm * id -type type_def = (* Type definition body *) - | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) - | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) - | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) - | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) - | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) +type val_spec_aux 'a = (* Value type specification *) + | VS_val_spec of typschm * id + | VS_extern_no_rename 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 scattered_def 'a = + | SD_aux of (scattered_def_aux 'a) * annot 'a -type def = (* Top-level definition *) - | DEF_type of type_def (* type definition *) - | DEF_fundef of fundef (* function definition *) - | DEF_val of letbind (* value definition *) - | DEF_spec of val_spec (* top-level type constraint *) - | DEF_default of default_spec (* default kind and type assumptions *) - | DEF_scattered of scattered_def (* scattered function and type definition *) +type type_def 'a = + | TD_aux of (type_def_aux 'a) * annot 'a + + +type fundef 'a = + | FD_aux of (fundef_aux 'a) * annot 'a + + +type default_spec 'a = + | DT_aux of (default_spec_aux 'a) * annot 'a + + +type val_spec 'a = + | VS_aux of (val_spec_aux 'a) * annot 'a + + +type def_aux 'a = (* Top-level definition *) + | DEF_type of (type_def 'a) (* type definition *) + | DEF_fundef of (fundef 'a) (* function definition *) + | DEF_val of (letbind 'a) (* value definition *) + | DEF_spec of (val_spec 'a) (* top-level type constraint *) + | DEF_default of (default_spec 'a) (* default kind and type assumptions *) + | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *) | DEF_reg_dec of typ * id (* register declaration *) -type defs = (* Definition sequence *) - | Defs of list def +type def 'a = + | DEF_aux of (def_aux 'a) * annot 'a + + +type defs 'a = (* Definition sequence *) + | Defs of list (def 'a) + + +let rec remove_one i l = + match l with + | [] -> [] + | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2) +end + +let rec remove_from l l2 = + match l2 with + | [] -> l + | i::l2' -> remove_from (remove_one i l) l2' +end + +let disjoint s1 s2 = Set.null (s1 inter s2) + +let rec disjoint_all sets = + match sets with + | [] -> true + | s1::[] -> true + | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets)) +end + + +type k = (* Internal kinds *) + | Ki_typ + | Ki_nat + | Ki_ord + | Ki_efct + | Ki_ctor of list k * k + | Ki_infer (* Representing an unknown kind, inferred by context *) + + +type ne = (* internal numeric expressions *) + | Ne_var of kid + | Ne_const of natural + | Ne_mult of ne * ne + | Ne_add of list ne + | Ne_exp of ne + | Ne_unary of ne + + +type kinf = (* Whether a kind is default or from a local binding *) + | Kinf_k of k + | Kinf_def of k + + +type tid = (* A type identifier or type variable *) + | Tid_id of id + | Tid_var of kid + + +type nec = (* Numeric expression constraints *) + | Nec_lteq of ne * ne + | Nec_eq of ne * ne + | Nec_gteq of ne * ne + | Nec_in of kid * list natural + + +type tag = (* Data indicating where the identifier arises and thus information necessary in compilation *) + | Tag_empty + | Tag_ctor (* Data constructor from a type union *) + | Tag_extern of maybe string (* External function, specied only with a val statement *) + | Tag_default (* Type has come from default declaration, identifier may not be bound locally *) + | Tag_spec + | Tag_enum + + +type t = (* Internal types *) + | T_id of id + | T_var of kid + | T_fn of t * t * effect + | T_tup of list t + | T_app of id * t_args + +and t_arg = (* Argument to type constructors *) + | T_arg_typ of t + | T_arg_nexp of ne + | T_arg_effect of effect + | T_arg_order of order + +and t_args = (* Arguments to type constructors *) + | T_args of list t_arg + + +type tinf = (* Type variables, type, and constraints, bound to an identifier *) + | Tinf_typ of t + | Tinf_quant_typ of (map tid kinf) * list nec * tag * t + + type definition_env = + | DenvEmp + | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id))) + + +let blength (bit) = Ne_const 8 +let hlength (bit) = Ne_const 8 + + type env = + | EnvEmp + | Env of (map id tinf) * definition_env + + type inf = + | Iemp + | Inf of (list nec) * effect + + val denv_union : definition_env -> definition_env -> definition_env + let denv_union de1 de2 = + match (de1,de2) with + | (DenvEmp,de2) -> de2 + | (de1,DenvEmp) -> de1 + | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) -> + Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2) + end + + val env_union : env -> env -> env + let env_union e1 e2 = + match (e1,e2) with + | (EnvEmp,e2) -> e2 + | (e1,EnvEmp) -> e1 + | ((Env te1 de1),(Env te2 de2)) -> + Env (te1 union te2) (denv_union de1 de2) + end + +let inf_union i1 i2 = + match (i1,i2) with + | (Iemp,i2) -> i2 + | (i1,Iemp) -> i1 + | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2)) + end + +let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*) + + + +type I = inf + + +type E = env diff --git a/language/l2.ml b/language/l2.ml index b01a25ac..1c2a6c09 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -1,4 +1,4 @@ -(* generated by Ott 0.23 from: l2.ott *) +(* generated by Ott 0.24 from: l2.ott *) type text = string @@ -294,13 +294,13 @@ and 'a lexp_aux = (* lvalue expression *) type -'a effect_opt_aux = (* Optional effect annotation for functions *) +effect_opt_aux = (* Optional effect annotation for functions *) Effect_opt_pure (* sugar for empty effect set *) | Effect_opt_effect of effect type -'a tannot_opt_aux = (* Optional type annotation for functions *) +tannot_opt_aux = (* Optional type annotation for functions *) Typ_annot_opt_some of typquant * typ @@ -328,13 +328,13 @@ type_union_aux = (* Type union constructors *) type -'a effect_opt = - Effect_opt_aux of 'a effect_opt_aux * 'a annot +effect_opt = + Effect_opt_aux of effect_opt_aux * l type -'a tannot_opt = - Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot +tannot_opt = + Typ_annot_opt_aux of tannot_opt_aux * l type @@ -369,13 +369,13 @@ and index_range = type 'a fundef_aux = (* Function definition *) - FD_function of rec_opt * 'a tannot_opt * 'a effect_opt * ('a funcl) list + FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list type 'a scattered_def_aux = (* Function and type union definitions that can be spread across a file. Each one must end in $_$ *) - SD_scattered_function of rec_opt * 'a tannot_opt * 'a effect_opt * id (* scattered function definition header *) + SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) | SD_scattered_funcl of 'a funcl (* scattered function definition clause *) | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) | SD_scattered_unioncl of id * type_union (* scattered union definition member *) diff --git a/language/l2.ott b/language/l2.ott index 8cbacf0d..aa981cc7 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -58,7 +58,9 @@ open import Set_extra type l = | Unknown | Trans of string * maybe l - | Range of nat * nat + | Range of string * nat * nat * nat * nat + +type annot 'a = l * 'a val duplicates : forall 'a. list 'a -> list 'a @@ -102,7 +104,7 @@ l :: '' ::= {{ phantom }} annot :: '' ::= {{ phantom }} {{ ocaml 'a annot }} - {{ lem annot }} + {{ lem annot 'a }} {{ hol unit }} id :: '' ::= @@ -195,13 +197,13 @@ effect :: 'Effect_' ::= | pure :: M :: pure {{ com sugar for empty effect set }} {{ lem (Effect_set []) }} {{icho [[{}]] }} | effect1 u+ .. u+ effectn :: M :: union {{ com meta operation for combining sets of effects }} {{ icho [] }} - {{ lem (List.foldr effect_union (Effect_set []) [[effect1..effectn]]) }} + {{ lem (List.foldr effect_union (Effect_aux (Effect_set []) Unknown) [[effect1..effectn]]) }} embed {{ lem let effect_union e1 e2 = match (e1,e2) with - | (Effect_set els,Effect_set els2) -> Effect_set (els++els2) + | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l end }} @@ -727,7 +729,7 @@ grammar tannot_opt :: 'Typ_annot_opt_' ::= {{ com Optional type annotation for functions}} - {{ aux _ annot }} {{ auxparam 'a }} + {{ aux _ l }} % | :: :: none % Currently not optional; one issue, do the type parameters apply over the argument types, or should this be the type of the function and not just the return | typquant typ :: :: some @@ -740,7 +742,7 @@ rec_opt :: 'Rec_' ::= effect_opt :: 'Effect_opt_' ::= {{ com Optional effect annotation for functions }} - {{ aux _ annot }} {{ auxparam 'a }} + {{ aux _ l }} | :: :: pure {{ com sugar for empty effect set }} | effectkw effect :: :: effect @@ -837,6 +839,8 @@ defs :: '' ::= | def1 .. defn :: :: Defs + + terminals :: '' ::= | ** :: :: starstar {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} diff --git a/language/l2_rules.ott b/language/l2_rules.ott index 7e3efcb7..3bade9d4 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -1,323 +1,5 @@ - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Machinery for typing rules % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -embed -{{ lem - -let rec remove_one i l = - match l with - | [] -> [] - | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2) -end - -let rec remove_from l l2 = - match l2 with - | [] -> l - | i::l2' -> remove_from (remove_one i l) l2' -end - -let disjoint s1 s2 = Set.null (s1 inter s2) - -let rec disjoint_all sets = - match sets with - | [] -> true - | s1::[] -> true - | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets)) -end -}} - - -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_' ::= -{{ com Internal types }} - | id :: :: id - | kid :: :: var - | t1 -> t2 effect 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 - | t [ t1 / id1 ... tn / idn ] :: :: subst - -tag :: 'Tag_' ::= -{{ 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 }} - | kid :: :: var - | num :: :: const - | ne1 * ne2 :: :: mult - | ne1 + ... + nen :: :: add - | 2 ** ne :: :: exp - | ( - ne ) :: :: unary - | zero :: M :: zero - {{ lem (Ne_const 0) }} - | 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_' ::= - {{ com Argument to type constructors }} - | t :: :: typ - | ne :: :: nexp - | effect :: :: effect - | order :: :: order - - t_args :: '' ::= {{ lem list t_arg }} - {{ 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 - | kid 'IN' { num1 , ... , numn } :: :: in - -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.foldr (++) [] [[S_N1..S_Nn]]) }} - {{ 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 - {{ lem [[S_N]] (* Write constraint solver *) }} - - - E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::= {{ phantom }} - {{ lem definition_env }} - {{ com Environments storing top level information, such as defined records, enumerations, and kinds }} - | < E_k , E_r , E_e > :: :: base - {{ hol arb }} - {{ lem (Denv [[E_k]] [[E_r]] [[E_e]]) }} - | empty :: :: empty - {{ hol arb }} - {{ lem DenvEmp }} - | E_d u+ E_d' :: :: union - {{ hol arb }} - {{ lem (denv_union [[E_d]] [[E_d']]) }} - - kinf :: 'kinf_' ::= - {{ com Whether a kind is default or from a local binding }} - | k :: :: k - | k default :: :: def - - tid :: 'tid_' ::= - {{ com A type identifier or type variable }} - | id :: :: id - | kid :: :: var - - E_k {{ tex {\ottnt{E}^{\textsc{k} } } }} :: 'E_k_' ::= {{ phantom }} - {{ hol (tid-> kinf) }} - {{ lem (map tid kinf) }} - {{ com Kind environments }} - | { tid1 |-> kinf1 , .. , tidn |-> kinfn } :: :: concrete - {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[tid1 kinf1 .. tidn kinfn]]) }} - {{ lem (List.foldr (fun (x,v) m -> Map.insert x v m) Map.empty [[tid1 kinf1 .. tidn kinfn]]) }} - | 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.foldr (union) Map.empty [[E_k1..E_kn]]) }} - {{ ocaml (assert false) }} - | E_k u- E_k1 .. E_kn :: M :: multi_set_minus - {{ hol arb }} - {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_k]])) - (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_k1..E_kn]]))))) }} - {{ 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 - - field_typs :: 'FT_' ::= {{ phantom }} - {{ lem list (id * t) }} - {{ com Record fields }} - | id1 : t1 , .. , idn : tn :: :: fields - {{ lem [[id1 t1..idn tn]] }} - - E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::= {{ phantom }} - {{ hol (id*t) |-> tinf) }} - {{ lem map (list (id*t)) tinf }} - {{ com Record environments }} - | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn } :: :: concrete - {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }} - {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[field_typs1 tinf1..field_typsn tinfn]]) }} - | E_r1 u+ .. u+ E_rn :: M :: union - {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }} - {{ lem (List.foldr (union) Map.empty [[E_r1..E_rn]]) }} - {{ ocaml (assert false) }} - - enumerate_map :: '' ::= {{ phantom }} - {{ lem (list (nat*id)) }} - | { num1 |-> id1 ... numn |-> idn } :: :: enum_map - {{ lem [[num1 id1...numn idn]] }} - - E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::= {{ phantom }} - {{ lem (map t (list (nat*id))) }} - {{ com Enumeration environments }} - | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn } :: :: base - {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[t1 enumerate_map1..tn enumerate_mapn]]) }} - | E_e1 u+ .. u+ E_en :: :: union - {{ lem (List.foldr (union) Map.empty [[E_e1..E_en]]) }} - - -embed -{{ lem - type definition_env = - | DenvEmp - | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id))) - -}} - grammar - E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::= {{ phantom }} - {{ hol (id |-> tinf) }} - {{ lem map id tinf }} - {{ com Type environments }} - | { id1 |-> tinf1 , .. , idn |-> tinfn } :: :: base - {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }} - {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[id1 tinf1 .. idn tinfn]]) }} - | ( E_t1 u+ .... u+ E_tn ) :: M :: union - {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }} - {{ lem (List.foldr (union) Map.empty [[E_t1....E_tn]]) }} - {{ ocaml (assert false) }} - | u+ E_t1 .. E_tn :: M :: multi_union - {{ hol arb }} - {{ lem (List.foldr (union) Map.empty [[E_t1..E_tn]]) }} - {{ ocaml assert false }} - | E_t u- E_t1 .. E_tn :: M :: multi_set_minus - {{ hol arb }} - {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_t]])) - (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_t1..E_tn]]))))) }} - {{ ocaml assert false }} - | ( E_t1 inter .... inter E_tn ) :: M :: intersect - {{ hol arb }} - {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1....E_tn]]) }} - {{ ocaml (assert false) }} - | inter E_t1 .. E_tn :: M :: multi_inter - {{ hol arb }} - {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1..E_tn]]) }} - {{ ocaml assert false }} - - -ts :: ts_ ::= {{ phantom }} - {{ lem list t }} - | t1 , .. , tn :: :: lst - -embed -{{ lem -let blength (bit) = Ne_const 8 -let hlength (bit) = Ne_const 8 - - type env = - | EnvEmp - | Env of (map id tinf) * definition_env - - type inf = - | Iemp - | Inf of (list nec) * effect - - val denv_union : definition_env -> definition_env -> definition_env - let denv_union de1 de2 = - match (de1,de2) with - | (DenvEmp,de2) -> de2 - | (de1,DenvEmp) -> de1 - | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) -> - Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2) - end - - val env_union : env -> env -> env - let env_union e1 e2 = - match (e1,e2) with - | (EnvEmp,e2) -> e2 - | (e1,EnvEmp) -> e1 - | ((Env te1 de1),(Env te2 de2)) -> - Env (te1 union te2) (denv_union de1 de2) - end - -let inf_union i1 i2 = - match (i1,i2) with - | (Iemp,i2) -> i2 - | (i1,Iemp) -> i1 - | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2)) - end - -let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*) - -}} - -grammar - - E :: '' ::= - {{ hol ((string,env_body) fmaptree) }} - {{ lem env }} - {{ com Definition environment and lexical environment }} - | < E_t , E_d > :: :: E - {{ hol arb }} - {{ lem (Env [[E_t]] [[E_d]]) }} - | empty :: M :: E_empty - {{ hol arb }} - {{ lem EnvEmp }} - {{ ocaml assert false }} - | E u+ E' :: :: E_union - {{ lem (env_union [[E]] [[E']]) }} - - I :: '' ::= {{ lem inf }} - {{ com Information given by type checking an expression }} - | < S_N , effect > :: :: I - {{ lem (Inf [[S_N]] [[effect]]) }} - | Ie :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }} - {{ lem Iemp }} - | I1 u+ .. u+ In :: :: Iunion {{ com Unions the constraints and effect }} - {{ lem (List.foldr inf_union Iemp [[I1..In]]) }} - - formula :: formula_ ::= | judgement :: :: judgement diff --git a/language/l2_typ.ott b/language/l2_typ.ott new file mode 100644 index 00000000..43a3ea17 --- /dev/null +++ b/language/l2_typ.ott @@ -0,0 +1,326 @@ + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Machinery for typing rules % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +embed +{{ lem + +let rec remove_one i l = + match l with + | [] -> [] + | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2) +end + +let rec remove_from l l2 = + match l2 with + | [] -> l + | i::l2' -> remove_from (remove_one i l) l2' +end + +let disjoint s1 s2 = Set.null (s1 inter s2) + +let rec disjoint_all sets = + match sets with + | [] -> true + | s1::[] -> true + | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets)) +end +}} + + +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 }} + +t , u :: 'T_' ::= +{{ com Internal types }} + | id :: :: id + | kid :: :: var + | t1 -> t2 effect :: :: fn + | ( t1 * .... * tn ) :: :: tup + | id t_args :: :: app + | register t_args :: S :: reg_app {{ ichlo T_app "register" [[t_args]] }} + | t [ t1 / id1 ... tn / idn ] :: M :: subst {{ ichlo "todo" }} + +optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }} + | x :: :: optx_x + {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }} + | :: :: optx_none + {{ lem Nothing }} {{ ocaml None }} + + +tag :: 'Tag_' ::= +{{ 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 optx :: :: 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 }} + | Spec :: :: spec + | Enum :: :: enum + +ne :: 'Ne_' ::= + {{ com internal numeric expressions }} + | kid :: :: var + | num :: :: const + | ne1 * ne2 :: :: mult + | ne1 + ... + nen :: :: add + | 2 ** ne :: :: exp + | ( - ne ) :: :: unary + | zero :: S :: zero + {{ lem (Ne_const 0) }} + | 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_' ::= + {{ com Argument to type constructors }} + | t :: :: typ + | ne :: :: nexp + | effect :: :: effect + | order :: :: order + + t_args :: '' ::= {{ lem list t_arg }} + {{ 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 + | kid 'IN' { num1 , ... , numn } :: :: in + +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.foldr (++) [] [[S_N1..S_Nn]]) }} + {{ 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 + {{ lem [[S_N]] (* Write constraint solver *) }} + + + E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::= {{ phantom }} + {{ lem definition_env }} + {{ com Environments storing top level information, such as defined records, enumerations, and kinds }} + | < E_k , E_r , E_e > :: :: base + {{ hol arb }} + {{ lem (Denv [[E_k]] [[E_r]] [[E_e]]) }} + | empty :: :: empty + {{ hol arb }} + {{ lem DenvEmp }} + | E_d u+ E_d' :: :: union + {{ hol arb }} + {{ lem (denv_union [[E_d]] [[E_d']]) }} + + kinf :: 'kinf_' ::= + {{ com Whether a kind is default or from a local binding }} + | k :: :: k + | k default :: :: def + + tid :: 'tid_' ::= + {{ com A type identifier or type variable }} + | id :: :: id + | kid :: :: var + + E_k {{ tex {\ottnt{E}^{\textsc{k} } } }} :: 'E_k_' ::= {{ phantom }} + {{ hol (tid-> kinf) }} + {{ lem (map tid kinf) }} + {{ com Kind environments }} + | { tid1 |-> kinf1 , .. , tidn |-> kinfn } :: :: concrete + {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[tid1 kinf1 .. tidn kinfn]]) }} + {{ lem (List.foldr (fun (x,v) m -> Map.insert x v m) Map.empty [[tid1 kinf1 .. tidn kinfn]]) }} + | 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.foldr (union) Map.empty [[E_k1..E_kn]]) }} + {{ ocaml (assert false) }} + | E_k u- E_k1 .. E_kn :: M :: multi_set_minus + {{ hol arb }} + {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_k]])) + (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_k1..E_kn]]))))) }} + {{ 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 + + field_typs :: 'FT_' ::= {{ phantom }} + {{ lem list (id * t) }} + {{ com Record fields }} + | id1 : t1 , .. , idn : tn :: :: fields + {{ lem [[id1 t1..idn tn]] }} + + E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::= {{ phantom }} + {{ hol (id*t) |-> tinf) }} + {{ lem map (list (id*t)) tinf }} + {{ com Record environments }} + | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn } :: :: concrete + {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }} + {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[field_typs1 tinf1..field_typsn tinfn]]) }} + | E_r1 u+ .. u+ E_rn :: M :: union + {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }} + {{ lem (List.foldr (union) Map.empty [[E_r1..E_rn]]) }} + {{ ocaml (assert false) }} + + enumerate_map :: '' ::= {{ phantom }} + {{ lem (list (nat*id)) }} + | { num1 |-> id1 ... numn |-> idn } :: :: enum_map + {{ lem [[num1 id1...numn idn]] }} + + E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::= {{ phantom }} + {{ lem (map t (list (nat*id))) }} + {{ com Enumeration environments }} + | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn } :: :: base + {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[t1 enumerate_map1..tn enumerate_mapn]]) }} + | E_e1 u+ .. u+ E_en :: :: union + {{ lem (List.foldr (union) Map.empty [[E_e1..E_en]]) }} + + +embed +{{ lem + type definition_env = + | DenvEmp + | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id))) + +}} + +grammar + + E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::= {{ phantom }} + {{ hol (id |-> tinf) }} + {{ lem map id tinf }} + {{ com Type environments }} + | { id1 |-> tinf1 , .. , idn |-> tinfn } :: :: base + {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }} + {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[id1 tinf1 .. idn tinfn]]) }} + | ( E_t1 u+ .... u+ E_tn ) :: M :: union + {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }} + {{ lem (List.foldr (union) Map.empty [[E_t1....E_tn]]) }} + {{ ocaml (assert false) }} + | u+ E_t1 .. E_tn :: M :: multi_union + {{ hol arb }} + {{ lem (List.foldr (union) Map.empty [[E_t1..E_tn]]) }} + {{ ocaml assert false }} + | E_t u- E_t1 .. E_tn :: M :: multi_set_minus + {{ hol arb }} + {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_t]])) + (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_t1..E_tn]]))))) }} + {{ ocaml assert false }} + | ( E_t1 inter .... inter E_tn ) :: M :: intersect + {{ hol arb }} + {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1....E_tn]]) }} + {{ ocaml (assert false) }} + | inter E_t1 .. E_tn :: M :: multi_inter + {{ hol arb }} + {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1..E_tn]]) }} + {{ ocaml assert false }} + + +ts :: ts_ ::= {{ phantom }} + {{ lem list t }} + | t1 , .. , tn :: :: lst + +embed +{{ lem +let blength (bit) = Ne_const 8 +let hlength (bit) = Ne_const 8 + + type env = + | EnvEmp + | Env of (map id tinf) * definition_env + + type inf = + | Iemp + | Inf of (list nec) * effect + + val denv_union : definition_env -> definition_env -> definition_env + let denv_union de1 de2 = + match (de1,de2) with + | (DenvEmp,de2) -> de2 + | (de1,DenvEmp) -> de1 + | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) -> + Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2) + end + + val env_union : env -> env -> env + let env_union e1 e2 = + match (e1,e2) with + | (EnvEmp,e2) -> e2 + | (e1,EnvEmp) -> e1 + | ((Env te1 de1),(Env te2 de2)) -> + Env (te1 union te2) (denv_union de1 de2) + end + +let inf_union i1 i2 = + match (i1,i2) with + | (Iemp,i2) -> i2 + | (i1,Iemp) -> i1 + | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2)) + end + +let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*) + +}} + +grammar + + E :: '' ::= + {{ hol ((string,env_body) fmaptree) }} + {{ lem env }} + {{ com Definition environment and lexical environment }} + | < E_t , E_d > :: :: E + {{ hol arb }} + {{ lem (Env [[E_t]] [[E_d]]) }} + | empty :: M :: E_empty + {{ hol arb }} + {{ lem EnvEmp }} + {{ ocaml assert false }} + | E u+ E' :: :: E_union + {{ lem (env_union [[E]] [[E']]) }} + + I :: '' ::= {{ lem inf }} + {{ com Information given by type checking an expression }} + | < S_N , effect > :: :: I + {{ lem (Inf [[S_N]] [[effect]]) }} + | Ie :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }} + {{ lem Iemp }} + | I1 u+ .. u+ In :: :: Iunion {{ com Unions the constraints and effect }} + {{ lem (List.foldr inf_union Iemp [[I1..In]]) }} + |