diff options
Diffstat (limited to 'language/l2_rules.ott')
| -rw-r--r-- | language/l2_rules.ott | 1051 |
1 files changed, 1051 insertions, 0 deletions
diff --git a/language/l2_rules.ott b/language/l2_rules.ott new file mode 100644 index 00000000..7359c1c6 --- /dev/null +++ b/language/l2_rules.ott @@ -0,0 +1,1051 @@ +grammar + +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 +%% % + |