diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 52 | ||||
| -rw-r--r-- | language/l2.ml | 105 | ||||
| -rw-r--r-- | language/l2.ott | 13 | ||||
| -rw-r--r-- | language/l2_parse.ml | 115 | ||||
| -rw-r--r-- | language/l2_parse.ott | 1068 |
5 files changed, 157 insertions, 1196 deletions
diff --git a/language/l2.lem b/language/l2.lem index 9f500046..969a5bbf 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -75,11 +75,6 @@ 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 *) @@ -91,8 +86,9 @@ type order_aux = (* vector order specifications, of kind Order *) | Ord_dec (* decreasing (big-endian) *) -type id = - | Id_aux of id_aux * l +type id_aux = (* Identifier *) + | Id of x + | DeIid of x (* remove infix status *) type effect = @@ -102,6 +98,10 @@ type effect = type order = | Ord_aux of order_aux * l + +type id = + | Id_aux of id_aux * l + let effect_union e1 e2 = match (e1,e2) with | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l @@ -320,7 +320,7 @@ type rec_opt = type funcl 'a = - | FCL_aux of (funcl_aux 'a) * annot 'a + | FCL_aux of (funcl_aux 'a) * l type name_scm_opt = @@ -361,6 +361,10 @@ type type_def_aux 'a = (* Type definition body *) | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) +type dec_spec_aux 'a = (* Register declarations *) + | DEC_reg of typ * id + + type fundef_aux 'a = (* Function definition *) | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) @@ -384,30 +388,30 @@ type type_def 'a = | TD_aux of (type_def_aux 'a) * annot 'a +type dec_spec 'a = + | DEC_aux of (dec_spec_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 + | DT_aux of (default_spec_aux 'a) * l type val_spec 'a = | VS_aux of (val_spec_aux 'a) * annot 'a -type def_aux 'a = (* Top-level definition *) +type def '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 def 'a = - | DEF_aux of (def_aux 'a) * annot 'a + | DEF_reg_dec of (dec_spec 'a) (* register declaration *) type defs 'a = (* Definition sequence *) @@ -471,15 +475,6 @@ type nec = (* Numeric expression constraints *) | Nec_in of x * list integer -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 x | T_var of x @@ -498,6 +493,15 @@ and t_args = (* Arguments to type constructors *) | T_args of list t_arg +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 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 diff --git a/language/l2.ml b/language/l2.ml index 927f702b..6501ff28 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -200,7 +200,10 @@ typschm_aux = (* type scheme *) type -'a pat_aux = (* Pattern *) +'a fpat = + FP_aux of 'a fpat_aux * 'a annot + +and 'a pat_aux = (* Pattern *) P_lit of lit (* literal constant pattern *) | P_wild (* wildcard *) | P_as of 'a pat * id (* named pattern *) @@ -220,9 +223,6 @@ and 'a pat = and 'a fpat_aux = (* Field pattern *) FP_Fpat of id * 'a pat -and 'a fpat = - FP_aux of 'a fpat_aux * 'a annot - type typschm = @@ -230,35 +230,7 @@ typschm = type -'a lexp = - LEXP_aux of 'a lexp_aux * 'a annot - -and 'a fexp_aux = (* Field-expression *) - FE_Fexp of id * 'a exp - -and 'a fexp = - FE_aux of 'a fexp_aux * 'a annot - -and 'a fexps_aux = (* Field-expression list *) - FES_Fexps of ('a fexp) list * bool - -and 'a fexps = - FES_aux of 'a fexps_aux * 'a annot - -and 'a pexp_aux = (* Pattern match *) - Pat_exp of 'a pat * 'a exp - -and 'a pexp = - Pat_aux of 'a pexp_aux * 'a annot - -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 - -and 'a exp_aux = (* Expression *) +'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 *) @@ -296,6 +268,34 @@ and 'a lexp_aux = (* lvalue expression *) | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *) | LEXP_field of 'a lexp * id (* struct field *) +and 'a lexp = + LEXP_aux of 'a lexp_aux * 'a annot + +and 'a fexp_aux = (* Field-expression *) + FE_Fexp of id * 'a exp + +and 'a fexp = + FE_aux of 'a fexp_aux * 'a annot + +and 'a fexps_aux = (* Field-expression list *) + FES_Fexps of ('a fexp) list * bool + +and 'a fexps = + FES_aux of 'a fexps_aux * 'a annot + +and 'a pexp_aux = (* Pattern match *) + Pat_exp of 'a pat * 'a exp + +and 'a pexp = + Pat_aux of 'a pexp_aux * 'a annot + +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 effect_opt_aux = (* Optional effect annotation for functions *) @@ -348,7 +348,7 @@ rec_opt = type 'a funcl = - FCL_aux of 'a funcl_aux * 'a annot + FCL_aux of 'a funcl_aux * l type @@ -387,12 +387,8 @@ type type -'a type_def_aux = (* Type definition body *) - TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) - | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) - | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) - | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *) - | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) +'a dec_spec_aux = (* Register declarations *) + DEC_reg of typ * id type @@ -402,6 +398,15 @@ type type +'a type_def_aux = (* Type definition body *) + TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) + | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) + | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *) + | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) + + +type 'a val_spec_aux = (* Value type specification *) VS_val_spec of typschm * id | VS_extern_no_rename of typschm * id @@ -419,13 +424,18 @@ type type -'a type_def = - TD_aux of 'a type_def_aux * 'a annot +'a dec_spec = + DEC_aux of 'a dec_spec_aux * 'a annot type 'a default_spec = - DT_aux of 'a default_spec_aux * 'a annot + DT_aux of 'a default_spec_aux * l + + +type +'a type_def = + TD_aux of 'a type_def_aux * 'a annot type @@ -434,19 +444,14 @@ type type -'a def_aux = (* Top-level definition *) +'a def = (* Top-level definition *) DEF_type of 'a type_def (* type definition *) | DEF_fundef of 'a fundef (* function definition *) | DEF_val of 'a letbind (* value definition *) | DEF_spec of 'a val_spec (* top-level type constraint *) | DEF_default of 'a default_spec (* default kind and type assumptions *) | DEF_scattered of 'a scattered_def (* scattered function and type definition *) - | DEF_reg_dec of typ * id (* register declaration *) - - -type -'a def = - DEF_aux of 'a def_aux * 'a annot + | DEF_reg_dec of 'a dec_spec (* register declaration *) type diff --git a/language/l2.ott b/language/l2.ott index 87fddc49..7b619652 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -753,7 +753,7 @@ effect_opt :: 'Effect_opt_' ::= funcl :: 'FCL_' ::= {{ com Function clause }} - {{ aux _ annot }} {{ auxparam 'a }} + {{ aux _ l }} {{ auxparam 'a }} | id pat = exp :: :: Funcl @@ -789,7 +789,7 @@ val_spec :: 'VS_' ::= default_spec :: 'DT_' ::= {{ com Default kinding or typing assumption }} - {{ aux _ annot }} {{ auxparam 'a }} + {{ aux _ l }} {{ auxparam 'a }} | default base_kind kid :: :: kind | default typschm id :: :: typ % The intended semantics of these is that if an id in binding position @@ -815,13 +815,18 @@ scattered_def :: 'SD_' ::= {{ com scattered definition end }} +dec_spec :: 'DEC_' ::= + {{ com Register declarations }} + {{ aux _ annot }} {{ auxparam 'a }} + | register typ id :: :: reg + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Top-level definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% def :: 'DEF_' ::= {{ com Top-level definition }} - {{ aux _ annot }} {{ auxparam 'a }} + {{ auxparam 'a }} | type_def :: :: type {{ com type definition }} | fundef :: :: fundef @@ -834,7 +839,7 @@ def :: 'DEF_' ::= {{ com default kind and type assumptions }} | scattered_def :: :: scattered {{ com scattered function and type definition }} - | register typ id :: :: reg_dec + | dec_spec :: :: reg_dec {{ com register declaration }} diff --git a/language/l2_parse.ml b/language/l2_parse.ml index 741a8a94..7be33bc4 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -30,6 +30,12 @@ base_kind = type +id_aux = (* Identifier *) + Id of x + | DeIid of x (* remove infix status *) + + +type kid_aux = (* identifiers with kind, ticked to differntiate from program variables *) Var of x @@ -46,14 +52,13 @@ base_effect_aux = (* effect *) type -id_aux = (* Identifier *) - Id of x - | DeIid of x (* remove infix status *) +kind_aux = (* kinds *) + K_kind of (base_kind) list type -kind_aux = (* kinds *) - K_kind of (base_kind) list +id = + Id_aux of id_aux * l type @@ -67,11 +72,6 @@ base_effect = type -id = - Id_aux of id_aux * l - - -type kind = K_aux of kind_aux * l @@ -252,21 +252,15 @@ and letbind = type -type_union_aux = (* Type union constructors *) - Tu_id of id - | Tu_ty_id of atyp * id - - -type name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) Name_sect_none | Name_sect_some of string type -effect_opt_aux = (* Optional effect annotation for functions *) - Effect_opt_pure (* sugar for empty effect set *) - | Effect_opt_effect of atyp +type_union_aux = (* Type union constructors *) + Tu_id of id + | Tu_ty_id of atyp * id type @@ -276,6 +270,12 @@ tannot_opt_aux = (* Optional type annotation for functions *) type +effect_opt_aux = (* Optional effect annotation for functions *) + Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of atyp + + +type rec_opt_aux = (* Optional recursive annotation for functions *) Rec_nonrec (* non-recursive *) | Rec_rec (* recursive *) @@ -287,6 +287,11 @@ funcl_aux = (* Function clause *) type +name_scm_opt = + Name_sect_aux of name_scm_opt_aux * l + + +type index_range_aux = (* index specification, for bitfields in register types *) BF_single of int (* single index *) | BF_range of int * int (* index range *) @@ -302,8 +307,8 @@ type_union = type -name_scm_opt = - Name_sect_aux of name_scm_opt_aux * l +tannot_opt = + Typ_annot_opt_aux of tannot_opt_aux * l type @@ -312,11 +317,6 @@ effect_opt = type -tannot_opt = - Typ_annot_opt_aux of tannot_opt_aux * l - - -type rec_opt = Rec_aux of rec_opt_aux * l @@ -327,6 +327,13 @@ funcl = type +val_spec_aux = (* Value type specification *) + VS_val_spec of typschm * id + | VS_extern_no_rename of typschm * id + | VS_extern_spec of typschm * id * string + + +type type_def_aux = (* Type definition body *) TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) | TD_record of id * name_scm_opt * typquant * ((atyp * id)) list * bool (* struct type definition *) @@ -336,12 +343,22 @@ type_def_aux = (* Type definition body *) type +dec_spec_aux = (* Register declarations *) + DEC_reg of atyp * id + + +type default_typing_spec_aux = (* Default kinding or typing assumption *) DT_kind of base_kind * kid | DT_typ of typschm * id type +fundef_aux = (* Function definition *) + FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list + + +type 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 * tannot_opt * effect_opt * id (* scattered function definition header *) @@ -352,15 +369,8 @@ scattered_def_aux = (* Function and type union definitions that can be spread a type -val_spec_aux = (* Value type specification *) - VS_val_spec of typschm * id - | VS_extern_no_rename of typschm * id - | VS_extern_spec of typschm * id * string - - -type -fundef_aux = (* Function definition *) - FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list +val_spec = + VS_aux of val_spec_aux * l type @@ -369,44 +379,34 @@ type_def = type -default_typing_spec = - DT_aux of default_typing_spec_aux * l +dec_spec = + DEC_aux of dec_spec_aux * l type -scattered_def = - SD_aux of scattered_def_aux * l +default_typing_spec = + DT_aux of default_typing_spec_aux * l type -val_spec = - VS_aux of val_spec_aux * l +fundef = + FD_aux of fundef_aux * l type -fundef = - FD_aux of fundef_aux * l +scattered_def = + SD_aux of scattered_def_aux * l type -def_aux = (* Top-level definition *) +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_typing_spec (* default kind and type assumptions *) | DEF_scattered of scattered_def (* scattered definition *) - | DEF_reg_dec of atyp * id (* register declaration *) - - -type -def = - DEF_aux of def_aux * l - - -type -defs = (* Definition sequence *) - Defs of (def) list + | DEF_reg_dec of dec_spec (* register declaration *) type @@ -421,4 +421,9 @@ and lexp = LEXP_aux of lexp_aux * l +type +defs = (* Definition sequence *) + Defs of (def) list + + diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 2e48c264..1f365a3f 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -708,6 +708,10 @@ scattered_def :: 'SD_' ::= | end id :: :: scattered_end {{ com scattered definition end }} +dec_spec :: 'DEC_' ::= + {{ com Register declarations }} + {{ aux _ l }} + | register atyp id :: :: reg %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Top-level definitions % @@ -715,8 +719,6 @@ scattered_def :: 'SD_' ::= def :: 'DEF_' ::= {{ com Top-level definition }} - {{ aux _ l }} -% {{ aux _ annot }} {{ auxparam 'a }} | type_def :: :: type {{ com type definition }} | fundef :: :: fundef @@ -729,12 +731,11 @@ def :: 'DEF_' ::= {{ com default kind and type assumptions }} | scattered_def :: :: scattered {{ com scattered definition }} - | register atyp id :: :: reg_dec + | dec_spec :: :: reg_dec {{ com register declaration }} defs :: '' ::= {{ com Definition sequence }} -% {{ auxparam 'a }} | def1 .. defn :: :: Defs @@ -1361,1062 +1362,3 @@ formula :: formula_ ::= %% %% | 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 - -%% % -%% % -%% % defns -%% % convert_tnvars :: '' ::= -%% % -%% % defn -%% % tnvars ~> tnvs :: :: convert_tnvars :: convert_tnvars_ -%% % by -%% % -%% % :convert_tnvar: tnvar1 ~> tnv1 .. :convert_tnvar: tnvarn ~> tnvn -%% % ------------------------------------------------------------ :: none -%% % tnvar1 .. tnvarn ~> tnv1 .. tnvn -%% % -%% % defn -%% % tnvar ~> tnv :: :: convert_tnvar :: convert_tnvar_ -%% % by -%% % -%% % ----------------------------------------------------------- :: a -%% % a l ~> a -%% % -%% % ---------------------------------------------------------- :: N -%% % N l ~> N -%% % -%% % -%% % defns -%% % look_m :: '' ::= -%% % -%% % defn -%% % E1 ( x_l1 .. x_ln ) gives E2 :: :: look_m :: look_m_ -%% % {{ com Name path lookup }} -%% % by -%% % -%% % ------------------------------------------------------------ :: none -%% % E() gives E -%% % -%% % E_m(x) gives E1 -%% % E1(</y_li//i/>) gives E2 -%% % ------------------------------------------------------------ :: some -%% % <E_m,E_p,E_f,E_x>(x l </y_li//i/>) gives E2 -%% % -%% % defns -%% % look_m_id :: '' ::= -%% % -%% % defn -%% % E1 ( id ) gives E2 :: :: look_m_id :: look_m_id_ -%% % {{ com Module identifier lookup }} -%% % by -%% % -%% % E1(</y_li//i/> x l1) gives E2 -%% % ------------------------------------------------------------ :: all -%% % E1(</y_li.//i/> x l1 l2) gives E2 -%% % -%% % defns -%% % look_tc :: '' ::= -%% % -%% % defn -%% % E ( id ) gives p :: :: look_tc :: look_tc_ -%% % {{ com Path identifier lookup }} -%% % by -%% % -%% % E(</y_li//i/>) gives <E_m,E_p,E_f,E_x> -%% % E_p(x) gives p -%% % ------------------------------------------------------------ :: all -%% % E(</y_li.//i/> x l1 l2) gives p -%% % -%% % -%% % defns -%% % check_t :: '' ::= -%% % -%% % defn -%% % TD |- t ok :: :: check_t :: check_t_ -%% % {{ com Well-formed types }} -%% % by -%% % -%% % ------------------------------------------------------------ :: var -%% % TD |- a ok -%% % -%% % TD |- t1 ok -%% % TD |- t2 ok -%% % ------------------------------------------------------------ :: fn -%% % TD |- t1 -> t2 ok -%% % -%% % TD |- t1 ok .... TD |- tn ok -%% % ------------------------------------------------------------ :: tup -%% % TD |- t1 * .... * tn ok -%% % -%% % TD(p) gives tnv1..tnvn tc_abbrev -%% % TD,tnv1 |- t1 ok .. TD,tnvn |- tn ok -%% % ------------------------------------------------------------ :: app -%% % TD |- p t1 .. tn ok -%% % -%% % -%% % defn -%% % TD , tnv |- t ok :: :: check_tlen :: check_tlen_ -%% % {{ com Well-formed type/nexps matching the application type variable }} -%% % by -%% % -%% % TD |- t ok -%% % ------------------------------------------------------------ :: t -%% % TD,a |- t ok -%% % -%% % ------------------------------------------------------------ :: len -%% % TD,N |- ne ok -%% % -%% % %TODO type equality isn't right; neither is type conversion -%% % -%% % defns -%% % teq :: '' ::= -%% % -%% % defn -%% % TD |- 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' -%% % -%% % -%% % defns -%% % convert_typ :: '' ::= -%% % -%% % defn -%% % TD , E |- typ ~> t :: :: convert_typ :: convert_typ_ -%% % {{ com Convert source types to internal types }} -%% % by -%% % -%% % % TODO : Can't allow things like type t = _, but it's useful to have things -%% % % like f (x : (_, int)) = snd x -%% % %TD |- t ok -%% % %------------------------------------------------------------ :: wild -%% % %TD,E |- _ l ~> t -%% % -%% % ------------------------------------------------------------ :: var -%% % TD,E |- a l' l ~> a -%% % -%% % TD,E |- typ1 ~> t1 -%% % TD,E |- typ2 ~> t2 -%% % ------------------------------------------------------------ :: fn -%% % TD,E |- typ1->typ2 l ~> t1->t2 -%% % -%% % TD,E |- typ1 ~> t1 .... TD,E |- typn ~> tn -%% % ------------------------------------------------------------ :: tup -%% % TD,E |- typ1 * .... * typn l ~> t1 * .... * tn -%% % -%% % TD,E |- typ1 ~> t1 .. TD,E |- typn ~> tn -%% % E(id) gives p -%% % TD(p) gives a1..an tc_abbrev -%% % ------------------------------------------------------------ :: app -%% % TD,E |- id typ1 .. typn l ~> p t1 .. tn -%% % -%% % |- nexp ~> ne -%% % ------------------------------------------------------------ :: nexp -%% % TD,E |- nexp ~> ne -%% % -%% % TD,E |- typ ~> t -%% % ------------------------------------------------------------ :: paren -%% % TD,E |- (typ) l ~> t -%% % -%% % -%% % TD,E |- typ ~> t1 -%% % TD |- t1 = t2 -%% % ------------------------------------------------------------ :: eq -%% % TD,E |- typ ~> t2 -%% % -%% % defn -%% % |- nexp ~> ne :: :: convert_nexp :: convert_nexp_ -%% % {{ 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 -%% % -%% % defns -%% % convert_typs :: '' ::= -%% % -%% % defn -%% % TD , E |- typs ~> t_multi :: :: convert_typs :: convert_typs_ by -%% % -%% % TD,E |- typ1 ~> t1 .. TD,E |- typn ~> tn -%% % ------------------------------------------------------------ :: all -%% % TD,E |- typ1 * .. * typn ~> (t1 * .. * tn) -%% % -%% % defns -%% % check_lit :: '' ::= -%% % -%% % defn -%% % |- lit : t :: :: check_lit :: check_lit_ -%% % {{ com Typing literal constants }} -%% % by -%% % -%% % ------------------------------------------------------------ :: true -%% % |- true l : __bool -%% % -%% % ------------------------------------------------------------ :: false -%% % |- false l : __bool -%% % -%% % ------------------------------------------------------------ :: num -%% % |- num l : __num -%% % -%% % nat = bitlength(hex) -%% % ------------------------------------------------------------ :: hex -%% % |- hex l : __vector nat __bit -%% % -%% % nat = bitlength(bin) -%% % ------------------------------------------------------------ :: bin -%% % |- bin l : __vector nat __bit -%% % -%% % ------------------------------------------------------------ :: string -%% % |- string l : __string -%% % -%% % ------------------------------------------------------------ :: unit -%% % |- () l : __unit -%% % -%% % ------------------------------------------------------------ :: bitzero -%% % |- bitzero l : __bit -%% % -%% % ------------------------------------------------------------ :: bitone -%% % |- bitone l : __bit -%% % -%% % -%% % defns -%% % inst_field :: '' ::= -%% % -%% % defn -%% % TD , E |- field id : p t_args -> t gives ( x of names ) :: :: inst_field :: inst_field_ -%% % {{ com Field typing (also returns canonical field names) }} -%% % by -%% % -%% % E(</x_li//i/>) gives <E_m,E_p,E_f,E_x> -%% % E_f(y) gives <forall tnv1..tnvn. p -> t, (z of names)> -%% % TD |- t1 ok .. TD |- tn ok -%% % ------------------------------------------------------------ :: all -%% % TD,E |- field </x_li.//i/> y l1 l2: p t1 .. tn -> {tnv1|->t1..tnvn|->tn}(t) gives (z of names) -%% % -%% % defns -%% % inst_ctor :: '' ::= -%% % -%% % defn -%% % TD , E |- ctor id : t_multi -> p t_args gives ( x of names ) :: :: inst_ctor :: inst_ctor_ -%% % {{ com Data constructor typing (also returns canonical constructor names) }} -%% % by -%% % -%% % E(</x_li//i/>) gives <E_m,E_p,E_f,E_x> -%% % E_x(y) gives <forall tnv1..tnvn. t_multi -> p, (z of names)> -%% % TD |- t1 ok .. TD |- tn ok -%% % ------------------------------------------------------------ :: all -%% % TD,E |- ctor </x_li.//i/> y l1 l2 : {tnv1|->t1..tnvn|->tn}(t_multi) -> p t1 .. tn gives (z of names) -%% % -%% % defns -%% % inst_val :: '' ::= -%% % -%% % defn -%% % TD , E |- val id : t gives S_c :: :: inst_val :: inst_val_ -%% % {{ com Typing top-level bindings, collecting typeclass constraints }} -%% % by -%% % -%% % E(</x_li//i/>) gives <E_m,E_p,E_f,E_x> -%% % E_x(y) gives <forall tnv1..tnvn. (p1 tnv'1) .. (pi tnv'i) => t,env_tag> -%% % TD |- t1 ok .. TD |- tn ok -%% % t_subst = {tnv1|->t1..tnvn|->tn} -%% % ------------------------------------------------------------ :: all -%% % TD, E |- val </x_li.//i/> y l1 l2 : t_subst(t) gives {(p1 t_subst(tnv'1)), .. , (pi t_subst(tnv'i))} -%% % -%% % defns -%% % not_ctor :: '' ::= -%% % -%% % defn -%% % E , E_l |- x not ctor :: :: not_ctor :: not_ctor_ -%% % {{ com $\ottnt{v}$ is not bound to a data constructor }} -%% % by -%% % -%% % E_l(x) gives t -%% % ------------------------------------------------------------ :: val -%% % E,E_l |- x not ctor -%% % -%% % x NOTIN dom(E_x) -%% % ------------------------------------------------------------ :: unbound -%% % <E_m,E_p,E_f,E_x>,E_l |- x not ctor -%% % -%% % E_x(x) gives <forall tnv1..tnvn. (p1 tnv'1)..(pi tnv'i) => t,env_tag> -%% % ------------------------------------------------------------ :: bound -%% % <E_m,E_p,E_f,E_x>,E_l |- x not ctor -%% % -%% % defns -%% % not_shadowed :: '' ::= -%% % -%% % defn -%% % E_l |- id not shadowed :: :: not_shadowed :: not_shadowed_ -%% % {{ com $\ottnt{id}$ is not lexically shadowed }} -%% % by -%% % -%% % x NOTIN dom(E_l) -%% % ------------------------------------------------------------ :: sing -%% % E_l |- x l1 l2 not shadowed -%% % -%% % ------------------------------------------------------------ :: multi -%% % E_l |- x_l1. .. x_ln.y_l.z_l l not shadowed -%% % -%% % -%% % defns -%% % check_pat :: '' ::= -%% % -%% % defn -%% % TD , E , E_l1 |- pat : t gives E_l2 :: :: check_pat :: check_pat_ -%% % {{ com Typing patterns, building their binding environment }} -%% % by -%% % -%% % :check_pat_aux: TD,E,E_l1 |- pat_aux : t gives E_l2 -%% % ------------------------------------------------------------ :: all -%% % TD,E,E_l1 |- pat_aux l : t gives E_l2 -%% % -%% % defn -%% % TD , E , E_l1 |- pat_aux : t gives E_l2 :: :: check_pat_aux :: check_pat_aux_ -%% % {{ com Typing patterns, building their binding environment }} -%% % by -%% % -%% % TD |- t ok -%% % ------------------------------------------------------------ :: wild -%% % TD,E,E_l |- _ : t gives {} -%% % -%% % TD,E,E_l1 |- pat : t gives E_l2 -%% % x NOTIN dom(E_l2) -%% % ------------------------------------------------------------ :: as -%% % TD,E,E_l1 |- (pat as x l) : t gives E_l2 u+ {x|->t} -%% % -%% % TD,E,E_l1 |- pat : t gives E_l2 -%% % TD,E |- typ ~> t -%% % ------------------------------------------------------------ :: typ -%% % TD,E,E_l1 |- (pat : typ) : t gives E_l2 -%% % -%% % TD,E |- ctor id : (t1*..*tn) -> p t_args gives (x of names) -%% % E_l |- id not shadowed -%% % TD,E,E_l |- pat1 : t1 gives E_l1 .. TD,E,E_l |- patn : tn gives E_ln -%% % disjoint doms(E_l1,..,E_ln) -%% % ------------------------------------------------------------ :: ident_constr -%% % TD,E,E_l |- id pat1 .. patn : p t_args gives E_l1 u+ .. u+ E_ln -%% % -%% % TD |- t ok -%% % E,E_l |- x not ctor -%% % ------------------------------------------------------------ :: var -%% % TD,E,E_l |- x l1 l2 : t gives {x|->t} -%% % -%% % </TD,E |- field idi : p t_args -> ti gives (xi of names) // i /> -%% % </TD,E,E_l |- pati : ti gives E_li//i/> -%% % disjoint doms(</E_li//i/>) -%% % duplicates(</xi//i/>) = emptyset -%% % ------------------------------------------------------------ :: record -%% % TD,E,E_l |- <| </idi = pati li//i/> semi_opt |> : p t_args gives u+ </E_li//i/> -%% % -%% % TD,E,E_l |- pat1 : t gives E_l1 ... TD,E,E_l |- patn : t gives E_ln -%% % disjoint doms(E_l1 , ... , E_ln) -%% % length(pat1 ... patn) = nat -%% % ----------------------------------------------------------- :: vector -%% % TD,E,E_l |- [| pat1 ; ... ; patn semi_opt |] : __vector nat t gives E_l1 u+ ... u+ E_ln -%% % -%% % TD,E,E_l |- pat1 : __vector ne1 t gives E_l1 ... TD,E,E_l |- patn : __vector nen t gives E_ln -%% % disjoint doms(E_l1 , ... , E_ln) -%% % ne' = ne1 + ... + nen -%% % ----------------------------------------------------------- :: vectorConcat -%% % TD,E,E_l |- [| pat1 ... patn |] : __vector ne' t gives E_l1 u+ ... u+ E_ln -%% % -%% % -%% % TD,E,E_l |- pat1 : t1 gives E_l1 .... TD,E,E_l |- patn : tn gives E_ln -%% % disjoint doms(E_l1,....,E_ln) -%% % ------------------------------------------------------------ :: tup -%% % TD,E,E_l |- (pat1, ...., patn) : t1 * .... * tn gives E_l1 u+ .... u+ E_ln -%% % -%% % TD |- t ok -%% % TD,E,E_l |- pat1 : t gives E_l1 .. TD,E,E_l |- patn : t gives E_ln -%% % disjoint doms(E_l1,..,E_ln) -%% % ------------------------------------------------------------ :: list -%% % TD,E,E_l |- [pat1; ..; patn semi_opt] : __list t gives E_l1 u+ .. u+ E_ln -%% % -%% % TD,E,E_l1 |- pat : t gives E_l2 -%% % ------------------------------------------------------------ :: paren -%% % TD,E,E_l1 |- (pat) : t gives E_l2 -%% % -%% % TD,E,E_l1 |- pat1 : t gives E_l2 -%% % TD,E,E_l1 |- pat2 : __list t gives E_l3 -%% % disjoint doms(E_l2,E_l3) -%% % ------------------------------------------------------------ :: cons -%% % TD,E,E_l1 |- pat1 :: pat2 : __list t gives E_l2 u+ E_l3 -%% % -%% % |- lit : t -%% % ------------------------------------------------------------ :: lit -%% % TD,E,E_l |- lit : t gives {} -%% % -%% % E,E_l |- x not ctor -%% % ------------------------------------------------------------ :: num_add -%% % TD,E,E_l |- x l + num : __num gives {x|->__num} -%% % -%% % -%% % defns -%% % id_field :: '' ::= -%% % -%% % defn -%% % E |- id field :: :: id_field :: id_field_ -%% % {{ com Check that the identifier is a permissible field identifier }} -%% % by -%% % -%% % E_f(x) gives f_desc -%% % ------------------------------------------------------------ :: empty -%% % <E_m,E_p,E_f,E_x> |- x l1 l2 field -%% % -%% % -%% % E_m(x) gives E -%% % x NOTIN dom(E_f) -%% % E |- </y_li.//i/> z_l l2 field -%% % ------------------------------------------------------------ :: cons -%% % <E_m,E_p,E_f,E_x> |- x l1.</y_li.//i/> z_l l2 field -%% % -%% % defns -%% % id_value :: '' ::= -%% % -%% % defn -%% % E |- id value :: :: id_value :: id_value_ -%% % {{ com Check that the identifier is a permissible value identifier }} -%% % by -%% % -%% % E_x(x) gives v_desc -%% % ------------------------------------------------------------ :: empty -%% % <E_m,E_p,E_f,E_x> |- x l1 l2 value -%% % -%% % -%% % E_m(x) gives E -%% % x NOTIN dom(E_x) -%% % E |- </y_li.//i/> z_l l2 value -%% % ------------------------------------------------------------ :: cons -%% % <E_m,E_p,E_f,E_x> |- x l1.</y_li.//i/> z_l l2 value -%% % -%% % defns -%% % check_exp :: '' ::= -%% % -%% % defn -%% % TD , E , E_l |- exp : t gives S_c , S_N :: :: check_exp :: check_exp_ -%% % {{ com Typing expressions, collecting typeclass and index constraints }} -%% % by -%% % -%% % :check_exp_aux: TD,E,E_l |- exp_aux : t gives S_c,S_N -%% % ------------------------------------------------------------ :: all -%% % TD,E,E_l |- exp_aux l : t gives S_c,S_N -%% % -%% % defn -%% % TD , E , E_l |- exp_aux : t gives S_c , S_N :: :: check_exp_aux :: check_exp_aux_ -%% % {{ com Typing expressions, collecting typeclass and index constraints }} -%% % by -%% % -%% % E_l(x) gives t -%% % ------------------------------------------------------------ :: var -%% % TD,E,E_l |- x l1 l2 : t gives {},{} -%% % -%% % %TODO KG Add check that N is in scope -%% % ------------------------------------------------------------ :: nvar -%% % TD,E,E_l |- N : __num gives {},{} -%% % -%% % E_l |- id not shadowed -%% % E |- id value -%% % TD,E |- ctor id : t_multi -> p t_args gives (x of names) -%% % ------------------------------------------------------------ :: ctor -%% % TD,E,E_l |- id : curry(t_multi, p t_args) gives {},{} -%% % -%% % E_l |- id not shadowed -%% % E |- id value -%% % TD, E |- val id : t gives S_c -%% % ------------------------------------------------------------ :: val -%% % TD,E,E_l |- id : t gives S_c,{} -%% % -%% % -%% % TD,E,E_l |- pat1 : t1 gives E_l1 ... TD,E,E_l |- patn : tn gives E_ln -%% % TD,E,E_l u+ E_l1 u+ ... u+ E_ln |- exp : u gives S_c,S_N -%% % disjoint doms(E_l1,...,E_ln) -%% % ------------------------------------------------------------ :: fn -%% % TD,E,E_l |- fun pat1 ... patn -> exp l : curry((t1*...*tn), u) gives S_c,S_N -%% % -%% % %TODO: the various patterns might want to use different specifications for vector length (i.e. 32 in one and 8+n+8 in another) -%% % % So should be pati : t gives E_li,S_Ni -%% % </TD,E,E_l |- pati : t gives E_li//i/> -%% % </TD,E,E_l u+ E_li |- expi : u gives S_ci, S_Ni//i/> -%% % ------------------------------------------------------------ :: function -%% % TD,E,E_l |- function bar_opt </pati -> expi li//i/> end : t -> u gives </S_ci//i/> , </S_Ni//i/> -%% % -%% % %TODO t1 and t1 should be t1 and t'1 so that constraints from any vectors can be extracted and added to S_N -%% % TD,E,E_l |- exp1 : t1 -> t2 gives S_c1,S_N1 -%% % TD,E,E_l |- exp2 : t1 gives S_c2,S_N2 -%% % ------------------------------------------------------------ :: app -%% % TD,E,E_l |- exp1 exp2 : t2 gives S_c1 union S_c2, S_N1 union S_N2 -%% % -%% % %TODO t1 and t1 should be t1 and t'1 so that constraints from any vectors can be extracted and added to S_N -%% % % Same for t2 -%% % :check_exp_aux: TD,E,E_l |- (ix) : t1 -> t2 -> t3 gives S_c1,S_N1 -%% % TD,E,E_l |- exp1 : t1 gives S_c2,S_N2 -%% % TD,E,E_l |- exp2 : t2 gives S_c3,S_N3 -%% % ------------------------------------------------------------ :: infix_app1 -%% % TD,E,E_l |- exp1 ix l exp2 : t3 gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3 -%% % -%% % %TODO, see above todo -%% % :check_exp_aux: TD,E,E_l |- x : t1 -> t2 -> t3 gives S_c1,S_N1 -%% % TD,E,E_l |- exp1 : t1 gives S_c2,S_N2 -%% % TD,E,E_l |- exp2 : t2 gives S_c3,S_N3 -%% % ------------------------------------------------------------ :: infix_app2 -%% % TD,E,E_l |- exp1 `x` l exp2 : t3 gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3 -%% % -%% % %TODO, see above todo, with regard to t_args -%% % </TD,E |- field idi : p t_args -> ti gives (xi of names)//i/> -%% % </TD,E,E_l |- expi : ti gives S_ci,S_Ni//i/> -%% % duplicates(</xi//i/>) = emptyset -%% % names = {</xi//i/>} -%% % ------------------------------------------------------------ :: record -%% % TD,E,E_l |- <| </idi = expi li//i/> semi_opt l |> : p t_args gives </S_ci//i/>,</S_Ni//i/> -%% % -%% % %TODO, see above todo, with regard to t_args -%% % </TD,E |- field idi : p t_args -> ti gives (xi of names)//i/> -%% % </TD,E,E_l |- expi : ti gives S_ci,S_Ni//i/> -%% % duplicates(</xi//i/>) = emptyset -%% % TD,E,E_l |- exp : p t_args gives S_c',S_N' -%% % ------------------------------------------------------------ :: recup -%% % TD,E,E_l |- <| exp with </idi = expi li//i/> semi_opt l |> : p t_args gives S_c' union </S_ci//i/>,S_N' union </S_Ni//i/> -%% % -%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 ... TD,E,E_l |- expn : t gives S_cn,S_Nn -%% % length(exp1 ... expn) = nat -%% % ------------------------------------------------------------ :: vector -%% % TD,E,E_l |- [| exp1 ; ... ; expn semi_opt |] : __vector nat t gives S_c1 union ... union S_cn, S_N1 union ... union S_Nn -%% % -%% % TD,E,E_l |- exp : __vector ne' t gives S_c,S_N -%% % |- nexp ~> ne -%% % ------------------------------------------------------------- :: vectorget -%% % TD,E,E_l |- exp .( nexp ) : t gives S_c,S_N union {ne<ne'} -%% % -%% % TD,E,E_l |- exp : __vector ne' t gives S_c,S_N -%% % |- nexp1 ~> ne1 -%% % |- nexp2 ~> ne2 -%% % ne = :Ne_add: ne2 + (- ne1) -%% % ------------------------------------------------------------- :: vectorsub -%% % TD,E,E_l |- exp .( nexp1 .. nexp2 ) : __vector ne t gives S_c,S_N union {ne1 < ne2 < ne'} -%% % -%% % E |- id field -%% % TD,E |- field id : p t_args -> t gives (x of names) -%% % TD,E,E_l |- exp : p t_args gives S_c,S_N -%% % ------------------------------------------------------------ :: field -%% % TD,E,E_l |- exp.id : t gives S_c,S_N -%% % -%% % </TD,E,E_l |- pati : t gives E_li//i/> -%% % </TD,E,E_l u+ E_li |- expi : u gives S_ci,S_Ni//i/> -%% % TD,E,E_l |- exp : t gives S_c',S_N' -%% % ------------------------------------------------------------ :: case -%% % TD,E,E_l |- match exp with bar_opt </pati -> expi li//i/> l end : u gives S_c' union </S_ci//i/>,S_N' union </S_Ni//i/> -%% % -%% % TD,E,E_l |- exp : t gives S_c,S_N -%% % TD,E |- typ ~> t -%% % ------------------------------------------------------------ :: typed -%% % TD,E,E_l |- (exp : typ) : t gives S_c,S_N -%% % -%% % %KATHYCOMMENT: where does E_l1 come from? -%% % TD,E,E_l1 |- letbind gives E_l2, S_c1,S_N1 -%% % TD,E,E_l1 u+ E_l2 |- exp : t gives S_c2,S_N2 -%% % ------------------------------------------------------------ :: let -%% % TD,E,E_l |- let letbind in exp : t gives S_c1 union S_c2,S_N1 union S_N2 -%% % -%% % TD,E,E_l |- exp1 : t1 gives S_c1,S_N1 .... TD,E,E_l |- expn : tn gives S_cn,S_Nn -%% % ------------------------------------------------------------ :: tup -%% % TD,E,E_l |- (exp1, ...., expn) : t1 * .... * tn gives S_c1 union .... union S_cn,S_N1 union .... union S_Nn -%% % -%% % TD |- t ok -%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 .. TD,E,E_l |- expn : t gives S_cn,S_Nn -%% % ------------------------------------------------------------ :: list -%% % TD,E,E_l |- [exp1; ..; expn semi_opt] : __list t gives S_c1 union .. union S_cn, S_N1 union .. union S_Nn -%% % -%% % TD,E,E_l |- exp : t gives S_c,S_N -%% % ------------------------------------------------------------ :: paren -%% % TD,E,E_l |- (exp) : t gives S_c,S_N -%% % -%% % TD,E,E_l |- exp : t gives S_c,S_N -%% % ------------------------------------------------------------ :: begin -%% % TD,E,E_l |- begin exp end : t gives S_c,S_N -%% % -%% % %TODO t might need different index constraints -%% % TD,E,E_l |- exp1 : __bool gives S_c1,S_N1 -%% % TD,E,E_l |- exp2 : t gives S_c2,S_N2 -%% % TD,E,E_l |- exp3 : t gives S_c3,S_N3 -%% % ------------------------------------------------------------ :: if -%% % TD,E,E_l |- if exp1 then exp2 else exp3 : t gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3 -%% % -%% % %TODO t might need different index constraints -%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 -%% % TD,E,E_l |- exp2 : __list t gives S_c2,S_N2 -%% % ------------------------------------------------------------ :: cons -%% % TD,E,E_l |- exp1 :: exp2 : __list t gives S_c1 union S_c2,S_N1 union S_N2 -%% % -%% % |- lit : t -%% % ------------------------------------------------------------ :: lit -%% % TD,E,E_l |- lit : t gives {},{} -%% % -%% % % TODO: should require that each xi actually appears free in exp1 -%% % </TD |- ti ok//i/> -%% % TD,E,E_l u+ {</xi|->ti//i/>} |- exp1 : t gives S_c1,S_N1 -%% % TD,E,E_l u+ {</xi|->ti//i/>} |- exp2 : __bool gives S_c2,S_N2 -%% % disjoint doms(E_l, {</xi|->ti//i/>}) -%% % E = <E_m,E_p,E_f,E_x> -%% % </xi NOTIN dom(E_x)//i/> -%% % ------------------------------------------------------------ :: set_comp -%% % TD,E,E_l |- { exp1 | exp2 } : __set t gives S_c1 union S_c2,S_N1 union S_N2 -%% % -%% % TD,E,E_l1 |- </qbindi//i/> gives E_l2,S_c1 -%% % TD,E,E_l1 u+ E_l2 |- exp1 : t gives S_c2,S_N2 -%% % TD,E,E_l1 u+ E_l2 |- exp2 : __bool gives S_c3,S_N3 -%% % ------------------------------------------------------------ :: set_comp_binding -%% % TD,E,E_l1 |- { exp1 | forall </qbindi//i/> | exp2 } : __set t gives S_c1 union S_c2 union S_c3,S_N2 union S_N3 -%% % -%% % TD |- t ok -%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 .. TD,E,E_l |- expn : t gives S_cn,S_Nn -%% % ------------------------------------------------------------ :: set -%% % TD,E,E_l |- { exp1; ..; expn semi_opt } : __set t gives S_c1 union .. union S_cn,S_N1 union .. union S_Nn -%% % -%% % TD,E,E_l1 |- </qbindi//i/> gives E_l2,S_c1 -%% % TD,E,E_l1 u+ E_l2 |- exp : __bool gives S_c2,S_N2 -%% % ------------------------------------------------------------ :: quant -%% % TD,E,E_l1 |- q </qbindi//i/> . exp : __bool gives S_c1 union S_c2,S_N2 -%% % -%% % TD,E,E_l1 |- list </qbindi//i/> gives E_l2,S_c1 -%% % TD,E,E_l1 u+ E_l2 |- exp1 : t gives S_c2,S_N2 -%% % TD,E,E_l1 u+ E_l2 |- exp2 : __bool gives S_c3,S_N3 -%% % ------------------------------------------------------------ :: list_comp_binding -%% % TD,E,E_l1 |- [ exp1 | forall </qbindi//i/> | exp2 ] : __list t gives S_c1 union S_c2 union S_c3,S_N2 union S_N3 -%% % -%% % defn -%% % TD , E , E_l1 |- qbind1 .. qbindn gives E_l2 , S_c :: :: check_listquant_binding -%% % :: check_listquant_binding_ -%% % {{ com Build the environment for quantifier bindings, collecting typeclass constraints }} -%% % by -%% % -%% % ------------------------------------------------------------ :: empty -%% % TD,E,E_l |- gives {},{} -%% % -%% % TD |- t ok -%% % TD,E,E_l1 u+ {x |-> t} |- </qbindi//i/> gives E_l2,S_c1 -%% % disjoint doms({x |-> t}, E_l2) -%% % ------------------------------------------------------------ :: var -%% % TD,E,E_l1 |- x l </qbindi//i/> gives {x |-> t} u+ E_l2,S_c1 -%% % -%% % TD,E,E_l1 |- pat : t gives E_l3 -%% % TD,E,E_l1 |- exp : __set t gives S_c1,S_N1 -%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2 -%% % disjoint doms(E_l3, E_l2) -%% % ------------------------------------------------------------ :: restr -%% % TD,E,E_l1 |- (pat IN exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2 -%% % -%% % TD,E,E_l1 |- pat : t gives E_l3 -%% % TD,E,E_l1 |- exp : __list t gives S_c1,S_N1 -%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2 -%% % disjoint doms(E_l3, E_l2) -%% % ------------------------------------------------------------ :: list_restr -%% % TD,E,E_l1 |- (pat MEM exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2 -%% % -%% % defn -%% % TD , E , E_l1 |- list qbind1 .. qbindn gives E_l2 , S_c :: :: check_quant_binding :: check_quant_binding_ -%% % {{ com Build the environment for quantifier bindings, collecting typeclass constraints }} -%% % by -%% % -%% % ------------------------------------------------------------ :: empty -%% % TD,E,E_l |- list gives {},{} -%% % -%% % TD,E,E_l1 |- pat : t gives E_l3 -%% % TD,E,E_l1 |- exp : __list t gives S_c1,S_N1 -%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2 -%% % disjoint doms(E_l3, E_l2) -%% % ------------------------------------------------------------ :: restr -%% % TD,E,E_l1 |- list (pat MEM exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2 -%% % -%% % -%% % defn -%% % TD , E , E_l |- funcl gives { x |-> t } , S_c , S_N :: :: check_funcl :: check_funcl_ -%% % {{ com Build the environment for a function definition clause, collecting typeclass and index constraints }} -%% % by -%% % -%% % TD,E,E_l |- pat1 : t1 gives E_l1 ... TD,E,E_l |- patn : tn gives E_ln -%% % TD,E,E_l u+ E_l1 u+ ... u+ E_ln |- exp : u gives S_c,S_N -%% % disjoint doms(E_l1,...,E_ln) -%% % TD,E |- typ ~> u -%% % ------------------------------------------------------------ :: annot -%% % TD,E,E_l |- x l1 pat1 ... patn : typ = exp l2 gives {x |-> curry((t1 * ... * tn), u)}, S_c,S_N -%% % -%% % TD,E,E_l |- pat1 : t1 gives E_l1 ... TD,E,E_l |- patn : tn gives E_ln -%% % TD,E,E_l u+ E_l1 u+ ... u+ E_ln |- exp : u gives S_c,S_N -%% % disjoint doms(E_l1,...,E_ln) -%% % ------------------------------------------------------------ :: noannot -%% % TD,E,E_l |- x l1 pat1 ... patn = exp l2 gives {x |-> curry((t1 * ... * tn), u)}, S_c,S_N -%% % -%% % -%% % defn -%% % TD , E , E_l1 |- letbind gives E_l2 , S_c , S_N :: :: check_letbind :: check_letbind_ -%% % {{ com Build the environment for a let binding, collecting typeclass and index constraints }} -%% % by -%% % -%% % %TODO similar type equality issues to above ones -%% % TD,E,E_l1 |- pat : t gives E_l2 -%% % TD,E,E_l1 |- exp : t gives S_c,S_N -%% % TD,E |- typ ~> t -%% % ------------------------------------------------------------ :: val_annot -%% % TD,E,E_l1 |- pat : typ = exp l gives E_l2,S_c,S_N -%% % -%% % 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 -%% % -%% % :check_funcl:TD,E,E_l1 |- funcl_aux l gives {x|->t},S_c,S_N -%% % ------------------------------------------------------------ :: fn -%% % TD,E,E_l1 |- funcl_aux l gives {x|->t},S_c,S_N -%% % -%% % defns -%% % check_rule :: '' ::= -%% % -%% % defn -%% % TD , E , E_l |- rule gives { x |-> t } , S_c , S_N :: :: check_rule :: check_rule_ -%% % {{ com Build the environment for an inductive relation clause, collecting typeclass and index constraints }} -%% % by -%% % -%% % </TD |- ti ok//i/> -%% % E_l2 = {</yi|->ti//i/>} -%% % TD,E,E_l1 u+ E_l2 |- exp' : __bool gives S_c',S_N' -%% % TD,E,E_l1 u+ E_l2 |- exp1 : u1 gives S_c1,S_N1 .. TD,E,E_l1 u+ E_l2 |- expn : un gives S_cn,S_Nn -%% % ------------------------------------------------------------ :: rule -%% % TD,E,E_l1 |- x_l_opt forall </yi li//i/> . exp' ==> x l exp1 .. expn l' gives {x|->curry((u1 * .. * un) , __bool)}, S_c' union S_c1 union .. union S_cn,S_N' union S_N1 union .. union S_Nn -%% % -%% % 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 -%% % - |