From 12ccd923e9bf9794f1c2440f598e7fdbbe7afb6f Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Mon, 9 Sep 2013 17:05:40 +0100 Subject: Fixes bugs in pretty printer to generate legal lem syntax; split ott grammar and rules for lem ast generation; created a new directory for the lem interpreter and moved the Lem ast to it. --- language/Makefile | 6 +- language/l2.ott | 1052 ------------------------------------------------ language/l2_rules.ott | 1051 +++++++++++++++++++++++++++++++++++++++++++++++ src/ast.lem | 602 --------------------------- src/ast.ml | 166 ++++---- src/lem_interp/ast.lem | 303 ++++++++++++++ src/pretty_print.ml | 58 +-- src/process_file.ml | 6 +- 8 files changed, 1470 insertions(+), 1774 deletions(-) create mode 100644 language/l2_rules.ott delete mode 100644 src/ast.lem create mode 100644 src/lem_interp/ast.lem diff --git a/language/Makefile b/language/Makefile index 4ac35b65..4747dc49 100644 --- a/language/Makefile +++ b/language/Makefile @@ -11,9 +11,9 @@ l2_parse.pdf: l2_parse.tex l2Theory.uo: l2Script.sml Holmake --qof -I $(OTTLIB) l2Theory.uo -l2.tex ../src/ast.ml ../src/ast.lem l2Script.sml: l2.ott - ott -sort false -generate_aux_rules false -o l2.tex -picky_multiple_parses true l2.ott - ott -sort false -generate_aux_rules false -o ../src/ast.lem -o l2Script.sml -picky_multiple_parses true l2.ott +l2.tex ../src/ast.ml ../src/ast.lem l2Script.sml: l2.ott l2_rules.ott + ott -sort false -generate_aux_rules false -o l2.tex -picky_multiple_parses true l2.ott l2_rules.ott + ott -sort false -generate_aux_rules false -o ../src/lem_interp/ast.lem -o l2Script.sml -picky_multiple_parses true l2.ott ott -sort false -generate_aux_rules true -o ../src/ast.ml -picky_multiple_parses true l2.ott # the above is working around what is probably a bug in -generate_aux_rules true: when we try to generate Lem code with that turned on, we get some surprising-looking parse failures in a few rules. Likely we're not doing the proper transform for rules generated from inductive relation syntax. 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() gives -%% % E_f(y) gives t, (z of names)> -%% % TD |- t1 ok .. TD |- tn ok -%% % ------------------------------------------------------------ :: all -%% % TD,E |- field 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() gives -%% % E_x(y) gives p, (z of names)> -%% % TD |- t1 ok .. TD |- tn ok -%% % ------------------------------------------------------------ :: all -%% % TD,E |- ctor 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() gives -%% % E_x(y) gives t,env_tag> -%% % TD |- t1 ok .. TD |- tn ok -%% % t_subst = {tnv1|->t1..tnvn|->tn} -%% % ------------------------------------------------------------ :: all -%% % TD, E |- val 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_l |- x not ctor -%% % -%% % E_x(x) gives t,env_tag> -%% % ------------------------------------------------------------ :: bound -%% % ,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 - |- _ annot : t gives {} -% This case should perhaps indicate the generation of a type variable, with kind Typ - - |- pat : t gives E_t1 -id NOTIN dom(E_t1) ------------------------------------------------------------- :: as - |- (pat as id) : t gives E_t1 u+ {id|->t} - -E_k |- typ ~> t - |- pat : t gives E_t1 ------------------------------------------------------------- :: typ - |- ( pat) : t gives E_t1 - -%% % TD,E |- ctor id : (t1*..*tn) -> p t_args gives (x of names) - |- pat1 : t1 gives E_t1 .. |- patn : tn gives E_tn -%% % disjoint doms(E_l1,..,E_ln) ------------------------------------------------------------- :: ident_constr - |- id pat1 .. patn : id t_args gives E_t1 u+ .. u+ E_tn - -E_k |-t t ok - ------------------------------------------------------------ :: var - |- :P_id: id : t gives E_t u+ {id|->t} - -%% % -%% % ti gives (xi of names) // i /> -%% % -%% % disjoint doms() -%% % duplicates() = emptyset -%% % ------------------------------------------------------------ :: record -%% % TD,E,E_l |- <| semi_opt |> : p t_args gives u+ -%% % -%% % 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 -%% % - - |- pat1 : t1 gives E_t1 .... |- patn : tn gives E_tn -disjoint doms(E_t1,....,E_tn) ------------------------------------------------------------- :: tup - |- (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 -%% % |- x l1 l2 field -%% % -%% % -%% % E_m(x) gives E -%% % x NOTIN dom(E_f) -%% % E |- z_l l2 field -%% % ------------------------------------------------------------ :: cons -%% % |- x l1. 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 -%% % |- x l1 l2 value -%% % -%% % -%% % E_m(x) gives E -%% % x NOTIN dom(E_x) -%% % E |- z_l l2 value -%% % ------------------------------------------------------------ :: cons -%% % |- x l1. 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 -%% % -%% % -%% % ------------------------------------------------------------ :: function -%% % TD,E,E_l |- function bar_opt expi li//i/> end : t -> u gives , -%% % -%% % %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 -%% % ti gives (xi of names)//i/> -%% % -%% % duplicates() = emptyset -%% % names = {} -%% % ------------------------------------------------------------ :: record -%% % TD,E,E_l |- <| semi_opt l |> : p t_args gives , -%% % -%% % %TODO, see above todo, with regard to t_args -%% % ti gives (xi of names)//i/> -%% % -%% % duplicates() = emptyset -%% % TD,E,E_l |- exp : p t_args gives S_c',S_N' -%% % ------------------------------------------------------------ :: recup -%% % TD,E,E_l |- <| exp with semi_opt l |> : p t_args gives S_c' union ,S_N' union -%% % -%% % 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 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 |- exp : t gives S_c',S_N' -%% % ------------------------------------------------------------ :: case -%% % TD,E,E_l |- match exp with bar_opt expi li//i/> l end : u gives S_c' union ,S_N' union -%% % -%% % 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,E,E_l u+ {ti//i/>} |- exp1 : t gives S_c1,S_N1 -%% % TD,E,E_l u+ {ti//i/>} |- exp2 : __bool gives S_c2,S_N2 -%% % disjoint doms(E_l, {ti//i/>}) -%% % E = -%% % -%% % ------------------------------------------------------------ :: 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 |- 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 | 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 |- 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 . exp : __bool gives S_c1 union S_c2,S_N2 -%% % -%% % TD,E,E_l1 |- list 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 | 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} |- gives E_l2,S_c1 -%% % disjoint doms({x |-> t}, E_l2) -%% % ------------------------------------------------------------ :: var -%% % TD,E,E_l1 |- x l 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 |- gives E_l2,S_c2 -%% % disjoint doms(E_l3, E_l2) -%% % ------------------------------------------------------------ :: restr -%% % TD,E,E_l1 |- (pat IN exp) 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 |- gives E_l2,S_c2 -%% % disjoint doms(E_l3, E_l2) -%% % ------------------------------------------------------------ :: list_restr -%% % TD,E,E_l1 |- (pat MEM exp) 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 |- gives E_l2,S_c2 -%% % disjoint doms(E_l3, E_l2) -%% % ------------------------------------------------------------ :: restr -%% % TD,E,E_l1 |- list (pat MEM exp) 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 -%% % -%% % -%% % E_l2 = {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 . 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 -%% % x NOTIN dom(TD) -%% % ------------------------------------------------------------ :: abbrev -%% % ,TD,E |- tc x l tnvars = typ gives {x|->tnvs.t},{x|->x} -%% % -%% % tnvars ~> tnvs -%% % duplicates(tnvs) = emptyset -%% % x NOTIN dom(TD) -%% % ------------------------------------------------------------ :: abstract -%% % ,TD,E1 |- tc x l tnvars gives {x|->tnvs},{x|->x} -%% % -%% % tnvars ~> tnvs -%% % duplicates(tnvs) = emptyset -%% % x NOTIN dom(TD) -%% % ------------------------------------------------------------ :: rec -%% % ,TD1,E |- tc x l tnvars = <| x_l1 : typ1 ; ... ; x_lj : typj semi_opt |> gives {x|->tnvs},{x|->x} -%% % -%% % tnvars ~> tnvs -%% % duplicates(tnvs) = emptyset -%% % x NOTIN dom(TD) -%% % ------------------------------------------------------------ :: var -%% % ,TD1,E |- tc x l tnvars = bar_opt ctor_def1 | ... | ctor_defj gives {x|->tnvs},{x|->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 gives TD3,E_p3 -%% % dom(E_p2) inter dom(E_p3) = emptyset -%% % ------------------------------------------------------------ :: abbrev -%% % xs,TD1,E |- tc td 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 <{},{}> -%% % -%% % ti//i/> -%% % names = {} -%% % duplicates() = emptyset -%% % -%% % E_f = { ti, (xi of names)>//i/>} -%% % ------------------------------------------------------------ :: rec -%% % TD,E |- tnvs p = <| semi_opt |> gives -%% % -%% % t_multii//i/> -%% % names = {} -%% % duplicates() = emptyset -%% % -%% % E_x = { p, (xi of names)>//i/>} -%% % ------------------------------------------------------------ :: var -%% % TD,E |- tnvs p = bar_opt gives <{},E_x> -%% % -%% % defns -%% % check_texps :: '' ::= -%% % -%% % defn -%% % xs , TD , E |- td1 .. tdn gives < E_f , E_x > :: :: check_texps :: check_texps_ by -%% % -%% % ------------------------------------------------------------ :: empty -%% % ,TD,E |- gives <{},{}> -%% % -%% % tnvars ~> tnvs -%% % TD,E1 |- tnvs x = texp gives -%% % ,TD,E |- gives -%% % dom(E_x1) inter dom(E_x2) = emptyset -%% % dom(E_f1) inter dom(E_f2) = emptyset -%% % ------------------------------------------------------------ :: cons_concrete -%% % ,TD,E |- x l tnvars = texp gives -%% % -%% % ,TD,E |- gives -%% % ------------------------------------------------------------ :: cons_abstract -%% % ,TD,E |- x l tnvars gives -%% % -%% % 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 {ti//i/>},S_c,S_N -%% % %TODO, check S_N constraints -%% % I |- S_c gives semC -%% % -%% % FV(semC) SUBSET tnvs -%% % ------------------------------------------------------------ :: val -%% % TD,I,E1 |- let targets_opt letbind gives { ti, let>//i/>} -%% % -%% % ti},S_ci,S_Ni//i/> -%% % I |- S_c gives semC -%% % -%% % FV(semC) SUBSET tnvs -%% % compatible overlap(ti//i/>) -%% % E_l = {ti//i/>} -%% % ------------------------------------------------------------ :: recfun -%% % TD,I,E |- let rec targets_opt gives { 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 -%% % -%% % , D1 , E1 |- def gives D2 , E2 :: :: check_def :: check_def_ -%% % {{ com Check a definition }} -%% % by -%% % -%% % -%% % ,TD1,E |- tc gives TD2,E_p -%% % ,TD1 u+ TD2,E u+ <{},E_p,{},{}> |- gives -%% % ------------------------------------------------------------ :: type -%% % ,,E |- type l gives ,<{},E_p,E_f,E_x> -%% % -%% % TD,I,E |- val_def gives E_x -%% % ------------------------------------------------------------ :: val_def -%% % ,,E |- val_def l gives empty,<{},{},{},E_x> -%% % -%% % ti},S_ci,S_Ni//i/> -%% % %TODO Check S_N constraints -%% % I |- gives semC -%% % -%% % FV(semC) SUBSET tnvs -%% % compatible overlap(ti//i/>) -%% % E_l = {ti//i/>} -%% % E2 = <{},{},{},{ ti,let>//i/>}> -%% % ------------------------------------------------------------ :: indreln -%% % ,,E1 |- indreln targets_opt l gives empty,E2 -%% % -%% % x,D1,E1 |- defs gives D2,E2 -%% % ------------------------------------------------------------ :: module -%% % ,D1,E1 |- module x l1 = struct defs end l2 gives D2,<{x|->E2},{},{},{}> -%% % -%% % E1(id) gives E2 -%% % ------------------------------------------------------------ :: module_rename -%% % ,D,E1 |- module x l1 = id l2 gives empty,<{x|->E2},{},{},{}> -%% % -%% % TD,E |- typ ~> t -%% % FV(t) SUBSET -%% % FV() SUBSET -%% % pk//k/> -%% % E' = <{},{},{},{x|->. => t,val>}> -%% % ------------------------------------------------------------ :: spec -%% % ,,E |- val x l1 : forall . => typ l2 gives empty,E' -%% % -%% % ti//i/> -%% % -%% % :formula_p_eq: p = x -%% % E2 = <{},{x|->p},{},{ ti,method>//i/>}> -%% % TC2 = {p|->} -%% % p NOTIN dom(TC1) -%% % ------------------------------------------------------------ :: class -%% % ,,E1 |- class (x l a l'') end l' gives <{},TC2,{}>,E2 -%% % -%% % E = -%% % TD,E |- typ' ~> t' -%% % TD,() |- t' instance -%% % tnvs = -%% % duplicates(tnvs) = emptyset -%% % pk//k/> -%% % FV() SUBSET tnvs -%% % E(id) gives p -%% % TC(p) gives -%% % I2 = { (pk a'k)//k/> } -%% % -%% % disjoint doms() -%% % tk,method>//k/> -%% % { {a''|->t'}(tk),let>//k/>} = -%% % :formula_xs_eq: = -%% % I3 = { (p t')//k/>} -%% % (p { a'''i//i/>}(t')) NOTIN I -%% % ------------------------------------------------------------ :: instance_tc -%% % ,,E |- instance forall . => (id typ') end l' gives <{},{},I3>,empty -%% % -%% % defn -%% % , 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 -%% % ,D,E |- gives empty,empty -%% % -%% % :check_def: ,D1,E1 |- def gives D2,E2 -%% % ,D1 u+ D2,E1 u+ E2 |- gives D3,E3 -%% % ------------------------------------------------------------ :: relevant_def -%% % ,D1,E1 |- def semisemi_opt gives D2 u+ D3, E2 u+ E3 -%% % -%% % E1(id) gives E2 -%% % ,D1,E1 u+ E2 |- gives D3,E3 -%% % ------------------------------------------------------------ :: open -%% % ,D1,E1 |- open id l semisemi_opt gives D3,E3 -%% % - 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() gives +%% % E_f(y) gives t, (z of names)> +%% % TD |- t1 ok .. TD |- tn ok +%% % ------------------------------------------------------------ :: all +%% % TD,E |- field 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() gives +%% % E_x(y) gives p, (z of names)> +%% % TD |- t1 ok .. TD |- tn ok +%% % ------------------------------------------------------------ :: all +%% % TD,E |- ctor 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() gives +%% % E_x(y) gives t,env_tag> +%% % TD |- t1 ok .. TD |- tn ok +%% % t_subst = {tnv1|->t1..tnvn|->tn} +%% % ------------------------------------------------------------ :: all +%% % TD, E |- val 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_l |- x not ctor +%% % +%% % E_x(x) gives t,env_tag> +%% % ------------------------------------------------------------ :: bound +%% % ,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 + |- _ annot : t gives {} +% This case should perhaps indicate the generation of a type variable, with kind Typ + + |- pat : t gives E_t1 +id NOTIN dom(E_t1) +------------------------------------------------------------ :: as + |- (pat as id) : t gives E_t1 u+ {id|->t} + +E_k |- typ ~> t + |- pat : t gives E_t1 +------------------------------------------------------------ :: typ + |- ( pat) : t gives E_t1 + +%% % TD,E |- ctor id : (t1*..*tn) -> p t_args gives (x of names) + |- pat1 : t1 gives E_t1 .. |- patn : tn gives E_tn +%% % disjoint doms(E_l1,..,E_ln) +------------------------------------------------------------ :: ident_constr + |- id pat1 .. patn : id t_args gives E_t1 u+ .. u+ E_tn + +E_k |-t t ok + ------------------------------------------------------------ :: var + |- :P_id: id : t gives E_t u+ {id|->t} + +%% % +%% % ti gives (xi of names) // i /> +%% % +%% % disjoint doms() +%% % duplicates() = emptyset +%% % ------------------------------------------------------------ :: record +%% % TD,E,E_l |- <| semi_opt |> : p t_args gives u+ +%% % +%% % 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 +%% % + + |- pat1 : t1 gives E_t1 .... |- patn : tn gives E_tn +disjoint doms(E_t1,....,E_tn) +------------------------------------------------------------ :: tup + |- (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 +%% % |- x l1 l2 field +%% % +%% % +%% % E_m(x) gives E +%% % x NOTIN dom(E_f) +%% % E |- z_l l2 field +%% % ------------------------------------------------------------ :: cons +%% % |- x l1. 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 +%% % |- x l1 l2 value +%% % +%% % +%% % E_m(x) gives E +%% % x NOTIN dom(E_x) +%% % E |- z_l l2 value +%% % ------------------------------------------------------------ :: cons +%% % |- x l1. 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 +%% % +%% % +%% % ------------------------------------------------------------ :: function +%% % TD,E,E_l |- function bar_opt expi li//i/> end : t -> u gives , +%% % +%% % %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 +%% % ti gives (xi of names)//i/> +%% % +%% % duplicates() = emptyset +%% % names = {} +%% % ------------------------------------------------------------ :: record +%% % TD,E,E_l |- <| semi_opt l |> : p t_args gives , +%% % +%% % %TODO, see above todo, with regard to t_args +%% % ti gives (xi of names)//i/> +%% % +%% % duplicates() = emptyset +%% % TD,E,E_l |- exp : p t_args gives S_c',S_N' +%% % ------------------------------------------------------------ :: recup +%% % TD,E,E_l |- <| exp with semi_opt l |> : p t_args gives S_c' union ,S_N' union +%% % +%% % 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 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 |- exp : t gives S_c',S_N' +%% % ------------------------------------------------------------ :: case +%% % TD,E,E_l |- match exp with bar_opt expi li//i/> l end : u gives S_c' union ,S_N' union +%% % +%% % 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,E,E_l u+ {ti//i/>} |- exp1 : t gives S_c1,S_N1 +%% % TD,E,E_l u+ {ti//i/>} |- exp2 : __bool gives S_c2,S_N2 +%% % disjoint doms(E_l, {ti//i/>}) +%% % E = +%% % +%% % ------------------------------------------------------------ :: 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 |- 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 | 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 |- 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 . exp : __bool gives S_c1 union S_c2,S_N2 +%% % +%% % TD,E,E_l1 |- list 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 | 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} |- gives E_l2,S_c1 +%% % disjoint doms({x |-> t}, E_l2) +%% % ------------------------------------------------------------ :: var +%% % TD,E,E_l1 |- x l 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 |- gives E_l2,S_c2 +%% % disjoint doms(E_l3, E_l2) +%% % ------------------------------------------------------------ :: restr +%% % TD,E,E_l1 |- (pat IN exp) 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 |- gives E_l2,S_c2 +%% % disjoint doms(E_l3, E_l2) +%% % ------------------------------------------------------------ :: list_restr +%% % TD,E,E_l1 |- (pat MEM exp) 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 |- gives E_l2,S_c2 +%% % disjoint doms(E_l3, E_l2) +%% % ------------------------------------------------------------ :: restr +%% % TD,E,E_l1 |- list (pat MEM exp) 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 +%% % +%% % +%% % E_l2 = {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 . 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 +%% % x NOTIN dom(TD) +%% % ------------------------------------------------------------ :: abbrev +%% % ,TD,E |- tc x l tnvars = typ gives {x|->tnvs.t},{x|->x} +%% % +%% % tnvars ~> tnvs +%% % duplicates(tnvs) = emptyset +%% % x NOTIN dom(TD) +%% % ------------------------------------------------------------ :: abstract +%% % ,TD,E1 |- tc x l tnvars gives {x|->tnvs},{x|->x} +%% % +%% % tnvars ~> tnvs +%% % duplicates(tnvs) = emptyset +%% % x NOTIN dom(TD) +%% % ------------------------------------------------------------ :: rec +%% % ,TD1,E |- tc x l tnvars = <| x_l1 : typ1 ; ... ; x_lj : typj semi_opt |> gives {x|->tnvs},{x|->x} +%% % +%% % tnvars ~> tnvs +%% % duplicates(tnvs) = emptyset +%% % x NOTIN dom(TD) +%% % ------------------------------------------------------------ :: var +%% % ,TD1,E |- tc x l tnvars = bar_opt ctor_def1 | ... | ctor_defj gives {x|->tnvs},{x|->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 gives TD3,E_p3 +%% % dom(E_p2) inter dom(E_p3) = emptyset +%% % ------------------------------------------------------------ :: abbrev +%% % xs,TD1,E |- tc td 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 <{},{}> +%% % +%% % ti//i/> +%% % names = {} +%% % duplicates() = emptyset +%% % +%% % E_f = { ti, (xi of names)>//i/>} +%% % ------------------------------------------------------------ :: rec +%% % TD,E |- tnvs p = <| semi_opt |> gives +%% % +%% % t_multii//i/> +%% % names = {} +%% % duplicates() = emptyset +%% % +%% % E_x = { p, (xi of names)>//i/>} +%% % ------------------------------------------------------------ :: var +%% % TD,E |- tnvs p = bar_opt gives <{},E_x> +%% % +%% % defns +%% % check_texps :: '' ::= +%% % +%% % defn +%% % xs , TD , E |- td1 .. tdn gives < E_f , E_x > :: :: check_texps :: check_texps_ by +%% % +%% % ------------------------------------------------------------ :: empty +%% % ,TD,E |- gives <{},{}> +%% % +%% % tnvars ~> tnvs +%% % TD,E1 |- tnvs x = texp gives +%% % ,TD,E |- gives +%% % dom(E_x1) inter dom(E_x2) = emptyset +%% % dom(E_f1) inter dom(E_f2) = emptyset +%% % ------------------------------------------------------------ :: cons_concrete +%% % ,TD,E |- x l tnvars = texp gives +%% % +%% % ,TD,E |- gives +%% % ------------------------------------------------------------ :: cons_abstract +%% % ,TD,E |- x l tnvars gives +%% % +%% % 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 {ti//i/>},S_c,S_N +%% % %TODO, check S_N constraints +%% % I |- S_c gives semC +%% % +%% % FV(semC) SUBSET tnvs +%% % ------------------------------------------------------------ :: val +%% % TD,I,E1 |- let targets_opt letbind gives { ti, let>//i/>} +%% % +%% % ti},S_ci,S_Ni//i/> +%% % I |- S_c gives semC +%% % +%% % FV(semC) SUBSET tnvs +%% % compatible overlap(ti//i/>) +%% % E_l = {ti//i/>} +%% % ------------------------------------------------------------ :: recfun +%% % TD,I,E |- let rec targets_opt gives { 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 +%% % +%% % , D1 , E1 |- def gives D2 , E2 :: :: check_def :: check_def_ +%% % {{ com Check a definition }} +%% % by +%% % +%% % +%% % ,TD1,E |- tc gives TD2,E_p +%% % ,TD1 u+ TD2,E u+ <{},E_p,{},{}> |- gives +%% % ------------------------------------------------------------ :: type +%% % ,,E |- type l gives ,<{},E_p,E_f,E_x> +%% % +%% % TD,I,E |- val_def gives E_x +%% % ------------------------------------------------------------ :: val_def +%% % ,,E |- val_def l gives empty,<{},{},{},E_x> +%% % +%% % ti},S_ci,S_Ni//i/> +%% % %TODO Check S_N constraints +%% % I |- gives semC +%% % +%% % FV(semC) SUBSET tnvs +%% % compatible overlap(ti//i/>) +%% % E_l = {ti//i/>} +%% % E2 = <{},{},{},{ ti,let>//i/>}> +%% % ------------------------------------------------------------ :: indreln +%% % ,,E1 |- indreln targets_opt l gives empty,E2 +%% % +%% % x,D1,E1 |- defs gives D2,E2 +%% % ------------------------------------------------------------ :: module +%% % ,D1,E1 |- module x l1 = struct defs end l2 gives D2,<{x|->E2},{},{},{}> +%% % +%% % E1(id) gives E2 +%% % ------------------------------------------------------------ :: module_rename +%% % ,D,E1 |- module x l1 = id l2 gives empty,<{x|->E2},{},{},{}> +%% % +%% % TD,E |- typ ~> t +%% % FV(t) SUBSET +%% % FV() SUBSET +%% % pk//k/> +%% % E' = <{},{},{},{x|->. => t,val>}> +%% % ------------------------------------------------------------ :: spec +%% % ,,E |- val x l1 : forall . => typ l2 gives empty,E' +%% % +%% % ti//i/> +%% % +%% % :formula_p_eq: p = x +%% % E2 = <{},{x|->p},{},{ ti,method>//i/>}> +%% % TC2 = {p|->} +%% % p NOTIN dom(TC1) +%% % ------------------------------------------------------------ :: class +%% % ,,E1 |- class (x l a l'') end l' gives <{},TC2,{}>,E2 +%% % +%% % E = +%% % TD,E |- typ' ~> t' +%% % TD,() |- t' instance +%% % tnvs = +%% % duplicates(tnvs) = emptyset +%% % pk//k/> +%% % FV() SUBSET tnvs +%% % E(id) gives p +%% % TC(p) gives +%% % I2 = { (pk a'k)//k/> } +%% % +%% % disjoint doms() +%% % tk,method>//k/> +%% % { {a''|->t'}(tk),let>//k/>} = +%% % :formula_xs_eq: = +%% % I3 = { (p t')//k/>} +%% % (p { a'''i//i/>}(t')) NOTIN I +%% % ------------------------------------------------------------ :: instance_tc +%% % ,,E |- instance forall . => (id typ') end l' gives <{},{},I3>,empty +%% % +%% % defn +%% % , 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 +%% % ,D,E |- gives empty,empty +%% % +%% % :check_def: ,D1,E1 |- def gives D2,E2 +%% % ,D1 u+ D2,E1 u+ E2 |- gives D3,E3 +%% % ------------------------------------------------------------ :: relevant_def +%% % ,D1,E1 |- def semisemi_opt gives D2 u+ D3, E2 u+ E3 +%% % +%% % E1(id) gives E2 +%% % ,D1,E1 u+ E2 |- gives D3,E3 +%% % ------------------------------------------------------------ :: open +%% % ,D1,E1 |- open id l semisemi_opt gives D3,E3 +%% % + diff --git a/src/ast.lem b/src/ast.lem deleted file mode 100644 index c3305c97..00000000 --- a/src/ast.lem +++ /dev/null @@ -1,602 +0,0 @@ -(* generated by Ott 0.22 from: l2.ott *) - -open Pmap -open Pervasives - -type l = - | Unknown - | Trans of string * option l - | Range of num * num - -val disjoint : forall 'a . set 'a -> set 'a -> bool -let disjoint s1 s2 = - let diff = s1 inter s2 in - diff = Pervasives.empty - -val disjoint_all : forall 'a. list (set 'a) -> bool -let rec disjoint_all ls = match ls with - | [] -> true - | [a] -> true - | a::b::rs -> (disjoint a b) && (disjoint_all (b::rs)) -end - -val duplicates : forall 'a. list 'a -> list 'a - -val union_map : forall 'a 'b. map 'a 'b -> map 'a 'b -> map 'a 'b - -val set_from_list : forall 'a. list 'a -> set 'a - -val subst : forall 'a. list 'a -> list 'a -> bool - - -type x = string (* identifier *) -type ix = string (* infix identifier *) - -type id = (* Identifier *) - | Id of x - | DeIid of x (* remove infix status *) - - -type base_kind = (* base kind *) - | BK_type (* kind of types *) - | BK_nat (* kind of natural number size expressions *) - | BK_order (* kind of vector order specifications *) - | BK_effects (* kind of effect sets *) - - -type nexp = (* expression of kind $Nat$, for vector sizes and origins *) - | Nexp_id of id (* identifier *) - | Nexp_constant of num (* constant *) - | Nexp_times of nexp * nexp (* product *) - | Nexp_sum of nexp * nexp (* sum *) - | Nexp_exp of nexp (* exponential *) - - -type kind = (* kinds *) - | K_kind of list base_kind - - -type efct = (* effect *) - | Effect_rreg (* read register *) - | Effect_wreg (* write register *) - | Effect_rmem (* read memory *) - | Effect_wmem (* write memory *) - | Effect_undef (* undefined-instruction exception *) - | Effect_unspec (* unspecified values *) - | Effect_nondet (* nondeterminism from intra-instruction parallelism *) - - -type nexp_constraint = (* constraint over kind $Nat$ *) - | NC_fixed of nexp * nexp - | NC_bounded_ge of nexp * nexp - | NC_bounded_le of nexp * nexp - | NC_nat_set_bounded of id * list num - - -type kinded_id = (* optionally kind-annotated identifier *) - | KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) - - -type order = (* vector order specifications, of kind $Order$ *) - | Ord_id of id (* identifier *) - | Ord_inc (* increasing (little-endian) *) - | Ord_dec (* decreasing (big-endian) *) - - -type effects = (* effect set, of kind $Effects$ *) - | Effects_var of id - | Effects_set of list efct (* effect set *) - - -type quant_item = (* Either a kinded identifier or a nexp constraint for a typquant *) - | QI_id of kinded_id (* An optionally kinded identifier *) - | QI_const of nexp_constraint (* A constraint for this type *) - - -type ne = (* internal numeric expressions *) - | Ne_var of id - | Ne_const of num - | Ne_mult of ne * ne - | Ne_add of ne * ne - | Ne_exp of ne - | Ne_unary of ne - - -type typ = (* Type expressions, of kind $Type$ *) - | Typ_wild (* Unspecified type *) - | Typ_var of id (* Type variable *) - | Typ_fn of typ * typ * effects (* Function type (first-order only in user code) *) - | Typ_tup of list typ (* Tuple type *) - | Typ_app of id * list typ_arg (* type constructor application *) - -and typ_arg = (* Type constructor arguments of all kinds *) - | Typ_arg_nexp of nexp - | Typ_arg_typ of typ - | Typ_arg_order of order - | Typ_arg_effects of effects - - -type lit = (* Literal constant *) - | L_unit (* $() : unit$ *) - | L_zero (* $bitzero : bit$ *) - | L_one (* $bitone : bit$ *) - | L_true (* $true : bool$ *) - | L_false (* $false : bool$ *) - | L_num of num (* natural number constant *) - | L_hex of string (* bit vector constant, C-style *) - | L_bin of string (* bit vector constant, C-style *) - | L_string of string (* string constant *) - - -type typquant = (* type quantifiers and constraints *) - | TypQ_tq of list quant_item - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) - - -type k = (* Internal kinds *) - | Ki_typ - | Ki_nat - | Ki_ord - | Ki_efct - | Ki_val (* Representing values, for use in identifier checks *) - | Ki_ctor of list k * k - | Ki_infer (* Representing an unknown kind, inferred by context *) - - -type pat = (* Pattern *) - | P_lit of lit (* literal constant pattern *) - | P_wild (* wildcard *) - | P_as of pat * id (* named pattern *) - | P_typ of typ * pat (* typed pattern *) - | P_id of id (* identifier *) - | P_app of id * list pat (* union constructor pattern *) - | P_record of list fpat * bool (* struct pattern *) - | P_vector of list pat (* vector pattern *) - | P_vector_indexed of list (num * pat) (* vector pattern (with explicit indices) *) - | P_vector_concat of list pat (* concatenated vector pattern *) - | P_tup of list pat (* tuple pattern *) - | P_list of list pat (* list pattern *) - -and fpat = (* Field pattern *) - | FP_Fpat of id * pat - - -type typschm = (* type scheme *) - | TypSchm_ts of typquant * typ - - -type exp = (* Expression *) - | E_block of list exp (* block (parsing conflict with structs?) *) - | E_id of id (* identifier *) - | E_lit of lit (* literal constant *) - | E_cast of typ * exp (* cast *) - | E_app of exp * list exp (* function application *) - | E_app_infix of exp * id * exp (* infix function application *) - | E_tuple of list exp (* tuple *) - | E_if of exp * exp * exp (* conditional *) - | E_for of id * exp * exp * exp * exp (* loop *) - | E_vector of list exp (* vector (indexed from 0) *) - | E_vector_indexed of list (num * exp) (* vector (indexed consecutively) *) - | E_vector_access of exp * exp (* vector access *) - | E_vector_subrange of exp * exp * exp (* subvector extraction *) - | E_vector_update of exp * exp * exp (* vector functional update *) - | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *) - | E_list of list exp (* list *) - | E_cons of exp * exp (* cons *) - | E_record of fexps (* struct *) - | E_record_update of exp * fexps (* functional update of struct *) - | E_field of exp * id (* field projection from struct *) - | E_case of exp * list pexp (* pattern matching *) - | E_let of letbind * exp (* let expression *) - | E_assign of lexp * exp (* imperative assignment *) - -and lexp = (* lvalue expression *) - | LEXP_id of id (* identifier *) - | LEXP_vector of lexp * exp (* vector element *) - | LEXP_vector_range of lexp * exp * exp (* subvector *) - | LEXP_field of lexp * id (* struct field *) - -and fexp = (* Field-expression *) - | FE_Fexp of id * exp - -and fexps = (* Field-expression list *) - | FES_Fexps of list fexp * bool - -and pexp = (* Pattern match *) - | Pat_exp of pat * exp - -and letbind = (* Let binding *) - | LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *) - | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) - - -type index_range = (* index specification, for bitfields in register types *) - | BF_single of num (* single index *) - | BF_range of num * num (* index range *) - | BF_concat of index_range * index_range (* concatenation of index ranges *) - - -type naming_scheme_opt = (* Optional variable-naming-scheme specification for variables of defined type *) - | Name_sect_none - | Name_sect_some of string - - -type rec_opt = (* Optional recursive annotation for functions *) - | Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) - - -type tannot_opt = (* Optional type annotation for functions *) - | Typ_annot_opt_some of typquant * typ - - -type funcl = (* Function clause *) - | FCL_Funcl of id * pat * exp - - -type effects_opt = (* Optional effect annotation for functions *) - | Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of effects - - -type val_spec = (* Value type specification *) - | VS_val_spec of typschm * id - - -type type_def = (* Type definition body *) - | TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *) - | TD_record of id * naming_scheme_opt * typquant * list (typ * id) * bool (* struct type definition *) - | TD_variant of id * naming_scheme_opt * typquant * list (typ * id) * bool (* union type definition *) - | TD_enum of id * naming_scheme_opt * list id * bool (* enumeration type definition *) - | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) - - -type default_typing_spec = (* Default kinding or typing assumption *) - | DT_kind of base_kind * id - | DT_typ of typschm * id - - -type fundef = (* Function definition *) - | FD_function of rec_opt * tannot_opt * effects_opt * list funcl - - -type def = (* Top-level definition *) - | DEF_type of type_def (* type definition *) - | DEF_fundef of fundef (* function definition *) - | DEF_val of letbind (* value definition *) - | DEF_spec of val_spec (* top-level type constraint *) - | DEF_default of default_typing_spec (* default kind and type assumptions *) - | DEF_reg_dec of typ * id (* register declaration *) - | DEF_scattered_function of rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *) - | DEF_scattered_funcl of funcl (* scattered function definition clause *) - | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *) - | DEF_scattered_unioncl of id * typ * id (* scattered union definition member *) - | DEF_scattered_end of id (* scattered definition end *) - - -type ctor_def = (* Datatype constructor definition clause *) - | CT_ct of id * typschm - - -type typ_lib = (* library types and syntactic sugar for them *) - | Typ_lib_unit (* unit type with value $()$ *) - | Typ_lib_bool (* booleans $true$ and $false$ *) - | Typ_lib_bit (* pure bit values (not mutable bits) *) - | Typ_lib_nat (* natural numbers 0,1,2,... *) - | Typ_lib_string of string (* UTF8 strings *) - | Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *) - | Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *) - | Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) - | Typ_lib_vector of nexp * nexp * order * typ (* vector of typ, indexed by natural range *) - | Typ_lib_vector2 of typ * nexp (* sugar for vector indexed by [ nexp ] *) - | Typ_lib_vector3 of typ * nexp * nexp (* sugar for vector indexed by [ nexp..nexp ] *) - | Typ_lib_list of typ (* list of typ *) - | Typ_lib_set of typ (* finite set of typ *) - | Typ_lib_reg of typ (* mutable register components holding typ *) - - -type defs = (* Definition sequence *) - | Defs of list def - -(** definitions *) - (* defns translate_ast *) -indreln - -(** definitions *) - (* defns check_t *) -indreln -(* defn check_t *) - -check_t_var: forall E_k id . -( Pmap.find id E_k = Ki_typ ) - ==> -check_t E_k (T_var id) - -and -check_t_varInfer: forall E_k id . -( Pmap.find id E_k = Ki_infer ) && -((Formula_update_k E_k id Ki_typ)) - ==> -check_t E_k (T_var id) - -and -check_t_fn: forall E_k t1 t2 effects . -(check_t E_k t1) && -(check_t E_k t2) && -(check_ef E_k effects) - ==> -check_t E_k (T_fn t1 t2 effects) - -and -check_t_tup: forall t_list E_k . -((List.for_all (fun b -> b) ((List.map (fun t_ -> check_t E_k t_) t_list)))) - ==> -check_t E_k (T_tup (t_list)) - -and -check_t_app: forall t_arg_k_list E_k id . -( Pmap.find id E_k = (Ki_ctor ((List.map (fun (t_arg_,k_) -> k_) t_arg_k_list)) Ki_typ) ) && -((List.for_all (fun b -> b) ((List.map (fun (t_arg_,k_) -> check_targs E_k k_ t_arg_) t_arg_k_list)))) - ==> -check_t E_k (T_app id (T_args ((List.map (fun (t_arg_,k_) -> t_arg_) t_arg_k_list)))) - - -and -(* defn check_ef *) - -check_ef_var: forall E_k id . -( Pmap.find id E_k = Ki_efct ) - ==> -check_ef E_k (Effects_var id) - -and -check_ef_varInfer: forall E_k id . -( Pmap.find id E_k = Ki_infer ) && -((Formula_update_k E_k id Ki_efct)) - ==> -check_ef E_k (Effects_var id) - -and -check_ef_set: forall efct_list E_k . -true - ==> -check_ef E_k (Effects_set (efct_list)) - - -and -(* defn check_n *) - -check_n_var: forall E_k id . -( Pmap.find id E_k = Ki_nat ) - ==> -check_n E_k (Ne_var id) - -and -check_n_varInfer: forall E_k id . -( Pmap.find id E_k = Ki_infer ) && -((Formula_update_k E_k id Ki_nat)) - ==> -check_n E_k (Ne_var id) - -and -check_n_num: forall E_k num . -true - ==> -check_n E_k (Ne_const num) - -and -check_n_sum: forall E_k ne1 ne2 . -(check_n E_k ne1) && -(check_n E_k ne2) - ==> -check_n E_k (Ne_add ne1 ne2) - -and -check_n_mult: forall E_k ne1 ne2 . -(check_n E_k ne1) && -(check_n E_k ne2) - ==> -check_n E_k (Ne_mult ne1 ne2) - -and -check_n_exp: forall E_k ne . -(check_n E_k ne) - ==> -check_n E_k (Ne_exp ne) - - -and -(* defn check_ord *) - -check_ord_var: forall E_k id . -( Pmap.find id E_k = Ki_ord ) - ==> -check_ord E_k (Ord_id id) - -and -check_ord_varInfer: forall E_k id . -( Pmap.find id E_k = Ki_infer ) && -((Formula_update_k E_k id Ki_ord)) - ==> -check_ord E_k (Ord_id id) - - -and -(* defn check_targs *) - -check_targs_typ: forall E_k t . -(check_t E_k t) - ==> -check_targs E_k Ki_typ (Typ t) - -and -check_targs_eff: forall E_k effects . -(check_ef E_k effects) - ==> -check_targs E_k Ki_efct (Effect effects) - -and -check_targs_nat: forall E_k ne . -(check_n E_k ne) - ==> -check_targs E_k Ki_nat (Nexp ne) - -and -check_targs_ord: forall E_k order . -(check_ord E_k order) - ==> -check_targs E_k Ki_ord (Order order) - - -(** definitions *) - (* defns convert_typ *) -indreln -(* defn convert_typ *) - -convert_typ_var: forall E_k id . -( Pmap.find id E_k = Ki_typ ) - ==> -convert_typ E_k (Typ_var id) (T_var id) - -and -convert_typ_fn: forall E_k typ1 typ2 effects t1 t2 . -(convert_typ E_k typ1 t1) && -(convert_typ E_k typ2 t2) && -(check_ef E_k effects) - ==> -convert_typ E_k (Typ_fn typ1 typ2 effects) (T_fn t1 t2 effects) - -and -convert_typ_tup: forall typ_t_list E_k . -((List.for_all (fun b -> b) ((List.map (fun (typ_,t_) -> convert_typ E_k typ_ t_) typ_t_list)))) - ==> -convert_typ E_k (Typ_tup ((List.map (fun (typ_,t_) -> typ_) typ_t_list))) (T_tup ((List.map (fun (typ_,t_) -> t_) typ_t_list))) - -and -convert_typ_app: forall typ_arg_t_arg_k_list E_k id . -( Pmap.find id E_k = (Ki_ctor ((List.map (fun (typ_arg_,t_arg_,k_) -> k_) typ_arg_t_arg_k_list)) Ki_typ) ) && -((List.for_all (fun b -> b) ((List.map (fun (typ_arg_,t_arg_,k_) -> convert_targ E_k k_ typ_arg_ t_arg_) typ_arg_t_arg_k_list)))) - ==> -convert_typ E_k (Typ_app id ((List.map (fun (typ_arg_,t_arg_,k_) -> typ_arg_) typ_arg_t_arg_k_list))) (T_app id (T_args ((List.map (fun (typ_arg_,t_arg_,k_) -> t_arg_) typ_arg_t_arg_k_list)))) - -and -convert_typ_eq: forall E_k typ t2 t1 . -(convert_typ E_k typ t1) - ==> -convert_typ E_k typ t2 - - -and -(* defn convert_targ *) - - -(** definitions *) - (* defns check_lit *) -indreln -(* defn check_lit *) - -check_lit_true: forall . -true - ==> -check_lit L_true (T_var bool_id ) - -and -check_lit_false: forall . -true - ==> -check_lit L_false (T_var bool_id ) - -and -check_lit_num: forall num . -true - ==> -check_lit (L_num num) (T_var nat_id ) - -and -check_lit_string: forall string . -true - ==> -check_lit (L_string string) (T_var string_id ) - -and -check_lit_hex: forall hex zero num . -( ( (Ne_const num) = (hlength hex ) ) ) - ==> -check_lit (L_hex hex) (T_app vector_id (T_args ([((Nexp (Ne_const zero)))] @ [((Nexp (Ne_const num)))] @ [((Order Ord_inc))] @ [((Typ (T_var bit_id )))]))) - -and -check_lit_bin: forall bin zero num . -( ( (Ne_const num) = (blength bin ) ) ) - ==> -check_lit (L_bin bin) (T_app vector_id (T_args ([((Nexp (Ne_const zero)))] @ [((Nexp (Ne_const num)))] @ [((Order Ord_inc))] @ [((Typ (T_var bit_id )))]))) - -and -check_lit_unit: forall . -true - ==> -check_lit L_unit (T_var unit_id ) - -and -check_lit_bitzero: forall . -true - ==> -check_lit L_zero (T_var bit_id ) - -and -check_lit_bitone: forall . -true - ==> -check_lit L_one (T_var bit_id ) - - -(** definitions *) - (* defns check_pat *) -indreln -(* defn check_pat *) - -check_pat_wild: forall E_k t . -(check_t E_k t) - ==> -(PARSE_ERROR "line 1762 - 1763" "no parses (char 16): |- _ a***nnot : t gives {} ") - -and -check_pat_as: forall E_t E_k pat id t E_t1 . -(check_pat (Env E_k E_t ) pat t E_t1) && -( Pervasives.not (Pmap.mem id E_t1 ) ) - ==> -check_pat (Env E_k E_t ) (P_as pat id) t (List.fold_right union_map ([(E_t1)] @ [( (List.fold_right (fun (x,f) m -> Pmap.add x f m) ([(id,t)]) Pmap.empty) )]) Pmap.empty) - -and -check_pat_typ: forall E_t E_k typ pat t E_t1 . -(convert_typ E_k typ t) && -(check_pat (Env E_k E_t ) pat t E_t1) - ==> -check_pat (Env E_k E_t ) (P_typ typ pat) t E_t1 - -and -check_pat_ident_constr: forall pat_E_t_t_list E_t E_k id t_args . -((List.for_all (fun b -> b) ((List.map (fun (pat_,E_t_,t_) -> check_pat (Env E_k E_t ) pat_ t_ E_t_) pat_E_t_t_list)))) - ==> -check_pat (Env E_k E_t ) (P_app id ((List.map (fun (pat_,E_t_,t_) -> pat_) pat_E_t_t_list))) (T_app id t_args) (List.fold_right union_map ((List.map (fun (pat_,E_t_,t_) -> E_t_) pat_E_t_t_list)) Pmap.empty) - -and -check_pat_var: forall E_t E_k id t . -(check_t E_k t) - ==> -check_pat (Env E_k E_t ) (P_id id) t (List.fold_right union_map ([(E_t)] @ [( (List.fold_right (fun (x,f) m -> Pmap.add x f m) ([(id,t)]) Pmap.empty) )]) Pmap.empty) - -and -check_pat_tup: forall pat_t_E_t_list E_t E_k . -((List.for_all (fun b -> b) ((List.map (fun (pat_,t_,E_t_) -> check_pat (Env E_k E_t ) pat_ t_ E_t_) pat_t_E_t_list)))) && -( disjoint_all (List.map Pmap.domain ((List.map (fun (pat_,t_,E_t_) -> E_t_) pat_t_E_t_list)) ) ) - ==> -check_pat (Env E_k E_t ) (P_tup ((List.map (fun (pat_,t_,E_t_) -> pat_) pat_t_E_t_list))) (T_tup ((List.map (fun (pat_,t_,E_t_) -> t_) pat_t_E_t_list))) (List.fold_right union_map ((List.map (fun (pat_,t_,E_t_) -> E_t_) pat_t_E_t_list)) Pmap.empty) - - -(** definitions *) - (* defns check_exp *) -indreln - - - diff --git a/src/ast.ml b/src/ast.ml index bc4e7a5d..d280f4b8 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -108,6 +108,12 @@ quant_item = QI_aux of quant_item_aux * l +type +effects_aux = (* effect set, of kind $_$ *) + Effects_var of id + | Effects_set of (efct) list (* effect set *) + + type order_aux = (* vector order specifications, of kind $_$ *) Ord_id of id (* identifier *) @@ -115,26 +121,33 @@ order_aux = (* vector order specifications, of kind $_$ *) | Ord_dec (* decreasing (big-endian) *) -type -effects_aux = (* effect set, of kind $_$ *) - Effects_var of id - | Effects_set of (efct) list (* effect set *) - - type typquant_aux = (* type quantifiers and constraints *) TypQ_tq of (quant_item) list | TypQ_no_forall (* sugar, omitting quantifier and constraints *) +type +effects = + Effects_aux of effects_aux * l + + type order = Ord_aux of order_aux * l type -effects = - Effects_aux of effects_aux * l +lit_aux = (* Literal constant *) + L_unit (* $() : _$ *) + | L_zero (* $_ : _$ *) + | L_one (* $_ : _$ *) + | L_true (* $_ : _$ *) + | L_false (* $_ : _$ *) + | L_num of int (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_string of string (* string constant *) type @@ -163,32 +176,14 @@ and typ_arg = Typ_arg_aux of typ_arg_aux * l -type -lit_aux = (* Literal constant *) - L_unit (* $() : _$ *) - | L_zero (* $_ : _$ *) - | L_one (* $_ : _$ *) - | L_true (* $_ : _$ *) - | L_false (* $_ : _$ *) - | L_num of int (* natural number constant *) - | L_hex of string (* bit vector constant, C-style *) - | L_bin of string (* bit vector constant, C-style *) - | L_string of string (* string constant *) - - -type -typschm_aux = (* type scheme *) - TypSchm_ts of typquant * typ - - type lit = L_aux of lit_aux * l type -typschm = - TypSchm_aux of typschm_aux * l +typschm_aux = (* type scheme *) + TypSchm_ts of typquant * typ type @@ -216,6 +211,11 @@ and 'a fpat = FP_aux of 'a fpat_aux * 'a annot +type +typschm = + TypSchm_aux of typschm_aux * l + + type 'a exp_aux = (* Expression *) E_block of ('a exp) list (* block (parsing conflict with structs?) *) @@ -281,19 +281,14 @@ and 'a letbind = type -ne = (* internal numeric expressions *) - Ne_var of id - | Ne_const of int - | Ne_mult of ne * ne - | Ne_add of ne * ne - | Ne_exp of ne - | Ne_unary of ne +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) type -naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - Name_sect_none - | Name_sect_some of string +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * 'a exp type @@ -301,11 +296,6 @@ type Typ_annot_opt_some of typquant * typ -type -'a funcl_aux = (* Function clause *) - FCL_Funcl of id * 'a pat * 'a exp - - type 'a effects_opt_aux = (* Optional effect annotation for functions *) Effects_opt_pure (* sugar for empty effect set *) @@ -313,25 +303,29 @@ type type -rec_opt_aux = (* Optional recursive annotation for functions *) - Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) +naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of string type -k = (* Internal kinds *) - Ki_typ - | Ki_nat - | Ki_ord - | Ki_efct - | Ki_val (* Representing values, for use in identifier checks *) - | Ki_ctor of (k) list * k - | Ki_infer (* Representing an unknown kind, inferred by context *) +rec_opt = + Rec_aux of rec_opt_aux * l type -naming_scheme_opt = - Name_sect_aux of naming_scheme_opt_aux * l +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot + + +type +'a tannot_opt = + Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot + + +type +'a effects_opt = + Effects_opt_aux of 'a effects_opt_aux * 'a annot type @@ -345,23 +339,24 @@ and index_range = type -'a tannot_opt = - Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot +naming_scheme_opt = + Name_sect_aux of naming_scheme_opt_aux * l type -'a funcl = - FCL_aux of 'a funcl_aux * 'a annot +'a fundef_aux = (* Function definition *) + FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list type -'a effects_opt = - Effects_opt_aux of 'a effects_opt_aux * 'a annot +'a val_spec_aux = (* Value type specification *) + VS_val_spec of typschm * id type -rec_opt = - Rec_aux of rec_opt_aux * l +'a default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of base_kind * id + | DT_typ of typschm * id type @@ -374,24 +369,23 @@ type type -'a default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * id - | DT_typ of typschm * id - - -type -'a fundef_aux = (* Function definition *) - FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list +ne = (* internal numeric expressions *) + Ne_var of id + | Ne_const of int + | Ne_mult of ne * ne + | Ne_add of ne * ne + | Ne_exp of ne + | Ne_unary of ne type -'a val_spec_aux = (* Value type specification *) - VS_val_spec of typschm * id +'a fundef = + FD_aux of 'a fundef_aux * 'a annot type -'a type_def = - TD_aux of 'a type_def_aux * 'a annot +'a val_spec = + VS_aux of 'a val_spec_aux * 'a annot type @@ -400,13 +394,19 @@ type type -'a fundef = - FD_aux of 'a fundef_aux * 'a annot +'a type_def = + TD_aux of 'a type_def_aux * 'a annot type -'a val_spec = - VS_aux of 'a val_spec_aux * 'a annot +k = (* Internal kinds *) + Ki_typ + | Ki_nat + | Ki_ord + | Ki_efct + | Ki_val (* Representing values, for use in identifier checks *) + | Ki_ctor of (k) list * k + | Ki_infer (* Representing an unknown kind, inferred by context *) type @@ -466,11 +466,5 @@ type 'a defs = (* Definition sequence *) Defs of ('a def) list -(** definitions *) -(** definitions *) -(** definitions *) -(** definitions *) -(** definitions *) -(** definitions *) diff --git a/src/lem_interp/ast.lem b/src/lem_interp/ast.lem new file mode 100644 index 00000000..aebbebc6 --- /dev/null +++ b/src/lem_interp/ast.lem @@ -0,0 +1,303 @@ +(* generated by Ott 0.22 from: l2.ott *) + +open Pmap +open Pervasives + +type l = + | Unknown + | Trans of string * option l + | Range of num * num + + val disjoint : forall 'a . set 'a -> set 'a -> bool +let disjoint s1 s2 = + let diff = s1 inter s2 in + diff = Pervasives.empty + +val disjoint_all : forall 'a. list (set 'a) -> bool +let rec disjoint_all ls = match ls with + | [] -> true + | [a] -> true + | a::b::rs -> (disjoint a b) && (disjoint_all (b::rs)) +end + +val duplicates : forall 'a. list 'a -> list 'a + +val union_map : forall 'a 'b. map 'a 'b -> map 'a 'b -> map 'a 'b + +val set_from_list : forall 'a. list 'a -> set 'a + +val subst : forall 'a. list 'a -> list 'a -> bool + + +type x = string (* identifier *) +type ix = string (* infix identifier *) + +type base_kind = (* base kind *) + | BK_type (* kind of types *) + | BK_nat (* kind of natural number size expressions *) + | BK_order (* kind of vector order specifications *) + | BK_effects (* kind of effect sets *) + + +type id = (* Identifier *) + | Id of x + | DeIid of x (* remove infix status *) + + +type kind = (* kinds *) + | K_kind of list base_kind + + +type nexp = (* expression of kind $Nat$, for vector sizes and origins *) + | Nexp_id of id (* identifier *) + | Nexp_constant of num (* constant *) + | Nexp_times of nexp * nexp (* product *) + | Nexp_sum of nexp * nexp (* sum *) + | Nexp_exp of nexp (* exponential *) + + +type efct = (* effect *) + | Effect_rreg (* read register *) + | Effect_wreg (* write register *) + | Effect_rmem (* read memory *) + | Effect_wmem (* write memory *) + | Effect_undef (* undefined-instruction exception *) + | Effect_unspec (* unspecified values *) + | Effect_nondet (* nondeterminism from intra-instruction parallelism *) + + +type kinded_id = (* optionally kind-annotated identifier *) + | KOpt_none of id (* identifier *) + | KOpt_kind of kind * id (* kind-annotated variable *) + + +type nexp_constraint = (* constraint over kind $Nat$ *) + | NC_fixed of nexp * nexp + | NC_bounded_ge of nexp * nexp + | NC_bounded_le of nexp * nexp + | NC_nat_set_bounded of id * list num + + +type order = (* vector order specifications, of kind $Order$ *) + | Ord_id of id (* identifier *) + | Ord_inc (* increasing (little-endian) *) + | Ord_dec (* decreasing (big-endian) *) + + +type effects = (* effect set, of kind $Effects$ *) + | Effects_var of id + | Effects_set of list efct (* effect set *) + + +type quant_item = (* Either a kinded identifier or a nexp constraint for a typquant *) + | QI_id of kinded_id (* An optionally kinded identifier *) + | QI_const of nexp_constraint (* A constraint for this type *) + + +type typ = (* Type expressions, of kind $Type$ *) + | Typ_wild (* Unspecified type *) + | Typ_var of id (* Type variable *) + | Typ_fn of typ * typ * effects (* Function type (first-order only in user code) *) + | Typ_tup of list typ (* Tuple type *) + | Typ_app of id * list typ_arg (* type constructor application *) + +and typ_arg = (* Type constructor arguments of all kinds *) + | Typ_arg_nexp of nexp + | Typ_arg_typ of typ + | Typ_arg_order of order + | Typ_arg_effects of effects + + +type typquant = (* type quantifiers and constraints *) + | TypQ_tq of list quant_item + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) + + +type lit = (* Literal constant *) + | L_unit (* $() : unit$ *) + | L_zero (* $bitzero : bit$ *) + | L_one (* $bitone : bit$ *) + | L_true (* $true : bool$ *) + | L_false (* $false : bool$ *) + | L_num of num (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_string of string (* string constant *) + + +type typschm = (* type scheme *) + | TypSchm_ts of typquant * typ + + +type pat = (* Pattern *) + | P_lit of lit (* literal constant pattern *) + | P_wild (* wildcard *) + | P_as of pat * id (* named pattern *) + | P_typ of typ * pat (* typed pattern *) + | P_id of id (* identifier *) + | P_app of id * list pat (* union constructor pattern *) + | P_record of list fpat * bool (* struct pattern *) + | P_vector of list pat (* vector pattern *) + | P_vector_indexed of list (num * pat) (* vector pattern (with explicit indices) *) + | P_vector_concat of list pat (* concatenated vector pattern *) + | P_tup of list pat (* tuple pattern *) + | P_list of list pat (* list pattern *) + +and fpat = (* Field pattern *) + | FP_Fpat of id * pat + + +type ne = (* internal numeric expressions *) + | Ne_var of id + | Ne_const of num + | Ne_mult of ne * ne + | Ne_add of ne * ne + | Ne_exp of ne + | Ne_unary of ne + + +type letbind = (* Let binding *) + | LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *) + | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) + +and exp = (* Expression *) + | E_block of list exp (* block (parsing conflict with structs?) *) + | E_id of id (* identifier *) + | E_lit of lit (* literal constant *) + | E_cast of typ * exp (* cast *) + | E_app of exp * list exp (* function application *) + | E_app_infix of exp * id * exp (* infix function application *) + | E_tuple of list exp (* tuple *) + | E_if of exp * exp * exp (* conditional *) + | E_for of id * exp * exp * exp * exp (* loop *) + | E_vector of list exp (* vector (indexed from 0) *) + | E_vector_indexed of list (num * exp) (* vector (indexed consecutively) *) + | E_vector_access of exp * exp (* vector access *) + | E_vector_subrange of exp * exp * exp (* subvector extraction *) + | E_vector_update of exp * exp * exp (* vector functional update *) + | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *) + | E_list of list exp (* list *) + | E_cons of exp * exp (* cons *) + | E_record of fexps (* struct *) + | E_record_update of exp * fexps (* functional update of struct *) + | E_field of exp * id (* field projection from struct *) + | E_case of exp * list pexp (* pattern matching *) + | E_let of letbind * exp (* let expression *) + | E_assign of lexp * exp (* imperative assignment *) + +and lexp = (* lvalue expression *) + | LEXP_id of id (* identifier *) + | LEXP_vector of lexp * exp (* vector element *) + | LEXP_vector_range of lexp * exp * exp (* subvector *) + | LEXP_field of lexp * id (* struct field *) + +and fexp = (* Field-expression *) + | FE_Fexp of id * exp + +and fexps = (* Field-expression list *) + | FES_Fexps of list fexp * bool + +and pexp = (* Pattern match *) + | Pat_exp of pat * exp + + +type k = (* Internal kinds *) + | Ki_typ + | Ki_nat + | Ki_ord + | Ki_efct + | Ki_val (* Representing values, for use in identifier checks *) + | Ki_ctor of list k * k + | Ki_infer (* Representing an unknown kind, inferred by context *) + + +type index_range = (* index specification, for bitfields in register types *) + | BF_single of num (* single index *) + | BF_range of num * num (* index range *) + | BF_concat of index_range * index_range (* concatenation of index ranges *) + + +type naming_scheme_opt = (* Optional variable-naming-scheme specification for variables of defined type *) + | Name_sect_none + | Name_sect_some of string + + +type rec_opt = (* Optional recursive annotation for functions *) + | Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) + + +type effects_opt = (* Optional effect annotation for functions *) + | Effects_opt_pure (* sugar for empty effect set *) + | Effects_opt_effects of effects + + +type funcl = (* Function clause *) + | FCL_Funcl of id * pat * exp + + +type tannot_opt = (* Optional type annotation for functions *) + | Typ_annot_opt_some of typquant * typ + + +type default_typing_spec = (* Default kinding or typing assumption *) + | DT_kind of base_kind * id + | DT_typ of typschm * id + + +type val_spec = (* Value type specification *) + | VS_val_spec of typschm * id + + +type type_def = (* Type definition body *) + | TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *) + | TD_record of id * naming_scheme_opt * typquant * list (typ * id) * bool (* struct type definition *) + | TD_variant of id * naming_scheme_opt * typquant * list (typ * id) * bool (* union type definition *) + | TD_enum of id * naming_scheme_opt * list id * bool (* enumeration type definition *) + | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) + + +type fundef = (* Function definition *) + | FD_function of rec_opt * tannot_opt * effects_opt * list funcl + + +type def = (* Top-level definition *) + | DEF_type of type_def (* type definition *) + | DEF_fundef of fundef (* function definition *) + | DEF_val of letbind (* value definition *) + | DEF_spec of val_spec (* top-level type constraint *) + | DEF_default of default_typing_spec (* default kind and type assumptions *) + | DEF_reg_dec of typ * id (* register declaration *) + | DEF_scattered_function of rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *) + | DEF_scattered_funcl of funcl (* scattered function definition clause *) + | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *) + | DEF_scattered_unioncl of id * typ * id (* scattered union definition member *) + | DEF_scattered_end of id (* scattered definition end *) + + +type typ_lib = (* library types and syntactic sugar for them *) + | Typ_lib_unit (* unit type with value $()$ *) + | Typ_lib_bool (* booleans $true$ and $false$ *) + | Typ_lib_bit (* pure bit values (not mutable bits) *) + | Typ_lib_nat (* natural numbers 0,1,2,... *) + | Typ_lib_string of string (* UTF8 strings *) + | Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *) + | Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *) + | Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) + | Typ_lib_vector of nexp * nexp * order * typ (* vector of typ, indexed by natural range *) + | Typ_lib_vector2 of typ * nexp (* sugar for vector indexed by [ nexp ] *) + | Typ_lib_vector3 of typ * nexp * nexp (* sugar for vector indexed by [ nexp..nexp ] *) + | Typ_lib_list of typ (* list of typ *) + | Typ_lib_set of typ (* finite set of typ *) + | Typ_lib_reg of typ (* mutable register components holding typ *) + + +type ctor_def = (* Datatype constructor definition clause *) + | CT_ct of id * typschm + + +type defs = (* Definition sequence *) + | Defs of list def + + + diff --git a/src/pretty_print.ml b/src/pretty_print.ml index d51e0c12..bcc5961d 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -340,8 +340,8 @@ let pp_defs ppf (Defs(defs)) = let pp_format_id_lem (Id_aux(i,_)) = match i with - | Id(i) -> "(Id " ^ i ^ ")" - | DeIid(x) -> "(DeIid " ^ x ^ ")" + | Id(i) -> "(Id \"" ^ i ^ "\")" + | DeIid(x) -> "(DeIid \"" ^ x ^ "\")" let pp_lem_id ppf id = base ppf (pp_format_id_lem id) @@ -352,12 +352,12 @@ let pp_format_bkind_lem (BK_aux(k,_)) = | BK_order -> "BK_order" | BK_effects -> "BK_effects" -let pp_lem_bkind ppf bk = base ppf (pp_format_bkind bk) +let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk) let pp_format_kind_lem (K_aux(K_kind(klst),_)) = - "(K_kind [" ^ list_format "; " pp_format_bkind klst ^ "])" + "(K_kind [" ^ list_format "; " pp_format_bkind_lem klst ^ "])" -let pp_lem_kind ppf k = base ppf (pp_format_kind k) +let pp_lem_kind ppf k = base ppf (pp_format_kind_lem k) let rec pp_format_typ_lem (Typ_aux(t,_)) = match t with @@ -365,7 +365,7 @@ let rec pp_format_typ_lem (Typ_aux(t,_)) = | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^ pp_format_typ_lem ret ^ " " ^ (pp_format_effects_lem efct) ^ ")" - | Typ_tup(typs) -> "(Typ_tup " ^ (list_format " " pp_format_typ_lem typs) ^ ")" + | Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])" | Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])" and pp_format_nexp_lem (Nexp_aux(n,_)) = match n with @@ -409,9 +409,9 @@ let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e) let pp_format_nexp_constraint_lem (NC_aux(nc,_)) = match nc with - | NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp n2 ^ ")" - | NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp n1 ^ " " ^ pp_format_nexp n2 ^ ")" - | NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp n1 ^ " " ^ pp_format_nexp n2 ^ ")" + | NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" + | NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" + | NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" | NC_nat_set_bounded(id,bounds) -> "(NC_nat_set_bounded " ^ pp_format_id id ^ " [" ^ @@ -422,12 +422,12 @@ let pp_lem_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint_lem nc) let pp_format_qi_lem (QI_aux(qi,_)) = match qi with - | QI_const(n_const) -> "(QI_const " ^ pp_format_nexp_constraint n_const ^ ")" + | QI_const(n_const) -> "(QI_const " ^ pp_format_nexp_constraint_lem n_const ^ ")" | QI_id(KOpt_aux(ki,_)) -> "(QI_id " ^ (match ki with - | KOpt_none(id) -> "(KOpt_none " ^ pp_format_id id ^ ")" - | KOpt_kind(k,id) -> "(KOpt_kind " ^ pp_format_kind k ^ " " ^ pp_format_id id ^ ")") ^ ")" + | KOpt_none(id) -> "(KOpt_none " ^ pp_format_id_lem id ^ ")" + | KOpt_kind(k,id) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_id_lem id ^ ")") ^ ")" let pp_lem_qi ppf qi = base ppf (pp_format_qi_lem qi) @@ -435,9 +435,9 @@ let pp_format_typquant_lem (TypQ_aux(tq,_)) = match tq with | TypQ_no_forall -> "TypQ_no_forall" | TypQ_tq(qlist) -> - "(TypQ_tq " ^ - (list_format " " pp_format_qi qlist) ^ - ")" + "(TypQ_tq [" ^ + (list_format "; " pp_format_qi_lem qlist) ^ + "])" let pp_lem_typquant ppf tq = base ppf (pp_format_typquant_lem tq) @@ -548,8 +548,8 @@ and pp_lem_lexp ppf (LEXP_aux(lexp,_)) = let pp_lem_default ppf (DT_aux(df,_)) = match df with - | DT_kind(bk,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "DT_kind" pp_lem_bkind bk pp_lem_id id - | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id + | DT_kind(bk,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_id id + | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id let pp_lem_spec ppf (VS_aux(VS_val_spec(ts,id),_)) = fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id @@ -568,25 +568,25 @@ let rec pp_lem_range ppf (BF_aux(r,_)) = let pp_lem_typdef ppf (TD_aux(td,_)) = match td with | TD_abbrev(id,namescm,typschm) -> - fprintf ppf "@[<0>(%a %a %a %a)@]@\n" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm + fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm | TD_record(id,nm,typq,fs,_) -> let f_pp ppf (typ,id) = fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in - fprintf ppf "@[<0>(%a %a %a %a [%a])]@\n" + fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs | TD_variant(id,nm,typq,ar,_) -> let a_pp ppf (typ,id) = fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in - fprintf ppf "@[<0>(%a %a %a %a [%a])]@\n" + fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar | TD_enum(id,ns,enums,_) -> let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in - fprintf ppf "@[<0>(%a %a %a [%a])@]@\n" + fprintf ppf "@[<0>(%a %a %a [%a] false)@]" kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums | TD_register(id,n1,n2,rs) -> let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in let pp_rids = (list_pp pp_rid pp_rid) in - fprintf ppf "@[<0>(%a %a %a %a [%a])@]@\n" + fprintf ppf "@[<0>(%a %a %a %a [%a])@]" kwd "TD_register" pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs let pp_lem_rec ppf (Rec_aux(r,_)) = @@ -608,17 +608,17 @@ let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) = let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),_)) = let pp_funcls ppf funcl = fprintf ppf "%a %a" kwd ";" pp_lem_funcl funcl in - fprintf ppf "@[<0>(%a %a %a %a [%a]@]@\n" + fprintf ppf "@[<0>(%a %a %a %a [%a]@]" kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls let pp_lem_def ppf (DEF_aux(d,(l,_))) = match d with - | DEF_default(df) -> fprintf ppf "(DEF_default %a)" pp_lem_default df - | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a)" pp_lem_spec v_spec - | DEF_type(t_def) -> fprintf ppf "(DEF_type %a)" pp_lem_typdef t_def - | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a)" pp_lem_fundef f_def - | DEF_val(lbind) -> fprintf ppf "(DEF_val %a)" pp_lem_let lbind - | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "DEF_reg_dec" pp_lem_typ typ pp_lem_id id + | DEF_default(df) -> fprintf ppf "(DEF_default %a);@\n" pp_lem_default df + | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a);@\n" pp_lem_spec v_spec + | DEF_type(t_def) -> fprintf ppf "(DEF_type %a);@\n" pp_lem_typdef t_def + | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a);@\n" pp_lem_fundef f_def + | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind + | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>(%a %a %a)@];@\n" kwd "DEF_reg_dec" pp_lem_typ typ pp_lem_id id | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs") let pp_lem_defs ppf (Defs(defs)) = diff --git a/src/process_file.ml b/src/process_file.ml index a73eeac3..ce99f037 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -77,7 +77,7 @@ let convert_ast (defs : Parse_ast.defs) : Type_internal.tannot Ast.defs = Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env Envmap.empty defs let open_output_with_check file_name = - let (temp_file_name, o) = Filename.open_temp_file "lem_temp" "" in + let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in let o' = Format.formatter_of_out_channel o in (o', (o, temp_file_name, file_name)) @@ -136,7 +136,9 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo | Lem_ast_out -> begin let (o, ext_o) = open_output_with_check (f' ^ ".lem") in - Format.fprintf o "(* %s *)" (generated_line filename); + Format.fprintf o "(* %s *)@\n" (generated_line filename); + Format.fprintf o "open Ast@\n"; + Format.fprintf o "let defs = "; Pretty_print.pp_lem_defs o defs; close_output_with_check ext_o end -- cgit v1.2.3