diff options
Diffstat (limited to 'language/l2.ott')
| -rw-r--r-- | language/l2.ott | 1052 |
1 files changed, 0 insertions, 1052 deletions
diff --git a/language/l2.ott b/language/l2.ott index ccc910c2..fdd1dadf 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -1396,1055 +1396,3 @@ formula :: formula_ ::= %freevars %t a :: ftv -defns -translate_ast :: '' ::= - -defns -check_t :: '' ::= - -defn -E_k |-t t ok :: :: check_t :: check_t_ - {{ com Well-formed types }} - by - - E_k(id) gives K_Typ - ------------------------------------------------------------ :: var - E_k |-t id ok - - E_k(id) gives K_infer - E_k(id) <-| K_Typ - ------------------------------------------------------------ :: varInfer - E_k |-t id ok - - E_k |-t t1 ok - E_k |-t t2 ok - E_k |-e effects ok - ------------------------------------------------------------ :: fn - E_k |-t t1 -> t2 effects ok - - E_k |-t t1 ok .... E_k |-t tn ok - ------------------------------------------------------------ :: tup - E_k |-t t1 * .... * tn ok - - E_k(id) gives K_Lam(k1..kn -> K_Typ) - E_k,k1 |- t_arg1 ok .. E_k,kn |- t_argn ok - ------------------------------------------------------------ :: app - E_k |-t id t_arg1 .. t_argn ok - -defn -E_k |-e effects ok :: :: check_ef :: check_ef_ -{{ com Well-formed effects }} -by - -E_k(id) gives K_Efct ------------------------------------------------------------ :: var -E_k |-e effect id ok - -E_k(id) gives K_infer -E_k(id) <-| K_Efct ------------------------------------------------------------- :: varInfer -E_k |-e effect id ok - -------------------------------------------------------------- :: set -E_k |-e effect { efct1 , .. , efctn } ok - -defn -E_k |-n ne ok :: :: check_n :: check_n_ -{{ com Well-formed numeric expressions }} -by - -E_k(id) gives K_Nat ------------------------------------------------------------ :: var -E_k |-n id ok - -E_k(id) gives K_infer -E_k(id) <-| K_Nat ------------------------------------------------------------- :: varInfer -E_k |-n id ok - ------------------------------------------------------------ :: num -E_k |-n num ok - -E_k |-n ne1 ok -E_k |-n ne2 ok ------------------------------------------------------------ :: sum -E_k |-n ne1 + ne2 ok - -E_k |-n ne1 ok -E_k |-n ne2 ok ------------------------------------------------------------- :: mult -E_k |-n ne1 * ne2 ok - -E_k |-n ne ok ------------------------------------------------------------- :: exp -E_k |-n 2 ** ne ok - -defn -E_k |-o order ok :: :: check_ord :: check_ord_ -{{ com Well-formed numeric expressions }} -by - -E_k(id) gives K_Ord ------------------------------------------------------------ :: var -E_k |-o id ok - - E_k(id) gives K_infer - E_k(id) <-| K_Ord - ------------------------------------------------------------ :: varInfer - E_k |-o id ok - - -defn -E_k , k |- t_arg ok :: :: check_targs :: check_targs_ -{{ com Well-formed type arguments kind check matching the application type variable }} -by - -E_k |-t t ok ---------------------------------------------------------- :: typ -E_k , K_Typ |- t ok - -E_k |-e effects ok ---------------------------------------------------------- :: eff -E_k , K_Efct |- effects ok - -E_k |-n ne ok ---------------------------------------------------------- :: nat -E_k , K_Nat |- ne ok - -E_k |-o order ok ---------------------------------------------------------- :: ord -E_k, K_Ord |- order 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 -E_k |- typ ~> t :: :: convert_typ :: convert_typ_ -{{ com Convert source types to internal types }} -by - -E_k(id) gives K_Typ ------------------------------------------------------------- :: var -E_k |- :Typ_var: id ~> id - -E_k |- typ1 ~> t1 -E_k |- typ2 ~> t2 -E_k |-e effects ok ------------------------------------------------------------- :: fn -E_k |- typ1->typ2 effects ~> t1->t2 effects - -E_k |- typ1 ~> t1 .... E_k |- typn ~> tn ------------------------------------------------------------- :: tup -E_k |- typ1 * .... * typn ~> t1 * .... * tn - -E_k(id) gives K_Lam (k1..kn -> K_Typ) -E_k,k1 |- typ_arg1 ~> t_arg1 .. E_k,kn |- typ_argn ~> t_argn ------------------------------------------------------------- :: app -E_k |- id typ_arg1 .. typ_argn ~> id t_arg1 .. t_argn - -E_k |- typ ~> t1 -%E_k |- t1 = t2 ------------------------------------------------------------- :: eq -E_k |- typ ~> t2 - -defn -E_k , k |- typ_arg ~> t_arg :: :: convert_targ :: convert_targ_ -{{ com Convert source type arguments to internals }} -by - -%% % 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 : bool - - ------------------------------------------------------------ :: false - |- false : bool - - ------------------------------------------------------------ :: num - |- num : nat - - ------------------------------------------------------------- :: string - |- string : string - - num = bitlength(hex) - ------------------------------------------------------------ :: hex - |- hex : vector zero num inc :T_var: bit - - num = bitlength(bin) - ------------------------------------------------------------ :: bin - |- bin : vector zero num inc :T_var: bit - - ------------------------------------------------------------ :: unit - |- () : unit - - ------------------------------------------------------------ :: bitzero - |- bitzero : bit - - ------------------------------------------------------------ :: bitone - |- bitone : 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 -E |- pat : t gives E_t :: :: check_pat :: check_pat_ -{{ com Typing patterns, building their binding environment }} -by - -E_k |-t t ok ------------------------------------------------------------- :: wild -<E_t,E_k> |- _ annot : t gives {} -% This case should perhaps indicate the generation of a type variable, with kind Typ - -<E_t,E_k> |- pat : t gives E_t1 -id NOTIN dom(E_t1) ------------------------------------------------------------- :: as -<E_t,E_k> |- (pat as id) : t gives E_t1 u+ {id|->t} - -E_k |- typ ~> t -<E_t,E_k> |- pat : t gives E_t1 ------------------------------------------------------------- :: typ -<E_t,E_k> |- (<typ> pat) : t gives E_t1 - -%% % TD,E |- ctor id : (t1*..*tn) -> p t_args gives (x of names) -<E_t,E_k> |- pat1 : t1 gives E_t1 .. <E_t,E_k> |- patn : tn gives E_tn -%% % disjoint doms(E_l1,..,E_ln) ------------------------------------------------------------- :: ident_constr -<E_t,E_k> |- id pat1 .. patn : id t_args gives E_t1 u+ .. u+ E_tn - -E_k |-t t ok - ------------------------------------------------------------ :: var -<E_t,E_k> |- :P_id: id : t gives E_t u+ {id|->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 -%% % - -<E_t,E_k> |- pat1 : t1 gives E_t1 .... <E_t,E_k> |- patn : tn gives E_tn -disjoint doms(E_t1,....,E_tn) ------------------------------------------------------------- :: tup -<E_t,E_k> |- (pat1, ...., patn) : t1 * .... * tn gives E_t1 u+ .... u+ E_tn - -%% % 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 -%% % - |