diff options
Diffstat (limited to 'language/l2.lem')
| -rw-r--r-- | language/l2.lem | 514 |
1 files changed, 395 insertions, 119 deletions
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 |