diff options
Diffstat (limited to 'language/l2_parse.ott')
| -rw-r--r-- | language/l2_parse.ott | 1068 |
1 files changed, 5 insertions, 1063 deletions
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 -%% % - |