Juin 2020 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][alice] correction physical equality of lexp
by Alice de Berny 23 Jul '20

23 Jul '20

Alice de Berny pushed to branch alice at Stefan / Typer Commits: 3376edac by irradiee at 2020-06-05T10:14:41-04:00 correction physical equality of lexp - - - - - 4 changed files: - src/elab.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml Changes: ===================================== src/elab.ml ===================================== @@ -1009,7 +1009,7 @@ and lexp_parse_inductive ctors ctx = -> hc (Arrow (Aerasable, vname, t, l, e))) altacc in - if lexp_lexp' altacc' == lexp_lexp' altacc + if altacc' == altacc then acc (* No generalization! *) else (* Convert the Lexp back into a list of fields. *) ===================================== src/lexp.ml ===================================== @@ -188,6 +188,15 @@ let metavar_lookup (id : meta_id) : metavar_info | e :: l -> e lxor (apply_lxor l) let combine_hash e1 e2 = e1 lxor e2 + +let smap_hash e smap = + (combine_hash + (apply_lxor + (List.map (fun e -> let (ak, n, lt) = e in + (combine_hash (Hashtbl.hash ak) + (combine_hash (Hashtbl.hash n) (lexp_hash lt)))) + e)) (Hashtbl.hash smap)) + (* Hashtbl.hash for not lexp types * TODO: - find something else * - extract the first arg of 2 arg types ? (SMap)*) @@ -238,14 +247,11 @@ let combine_hash e1 e2 = e1 lxor e2 (combine_hash (Hashtbl.hash ak) (lexp_hash lp))) args)) | Susp (lp, subst) -> combine_hash (lexp_hash lp) (Hashtbl.hash subst) -let impossible = (let imp = Imm Sexp.dummy_epsilon in (imp, dummy_hash)) - let compare_hash x y = let (x', h1) = x in let (y', h2) = y in compare h1 h2 = 0 -(* May be a tree ? *) module WHC = Weak.Make (struct type t = lexp (* Using (=) instead of `compare` results * in an *enormous* slowdown. Apparently @@ -259,6 +265,8 @@ let hc_table : WHC.t = WHC.create 1000 let hc (e : lexp') : lexp = let lp = (e, lexp'_hash e) in WHC.merge hc_table lp +let impossible = hc (Imm Sexp.dummy_epsilon) + let mkImm s = hc (Imm s) let mkSortLevel l = hc (SortLevel l) let mkSort (l, s) = hc (Sort (l, s)) @@ -1040,10 +1048,8 @@ and lexp_str_decls ctx decls = (** Syntactic equality (i.e. without β). *******) let rec eq e1 e2 = - let e1' = lexp_lexp' e1 in - let e2' = lexp_lexp' e2 in - e1' == e2' || - match (e1', e2') with + e1 == e2 || + match (lexp_lexp' e1, lexp_lexp' e2) with | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 | (Imm (Float (_, x1)), Imm (Float (_, x2))) -> x1 = x2 | (Imm (String (_, s1)), Imm (String (_, s2))) -> s1 = s2 ===================================== src/opslexp.ml ===================================== @@ -211,8 +211,8 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = type set_plexp = (lexp * lexp) list let set_empty : set_plexp = [] let set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool - = assert (lexp_lexp' e1 == lexp_lexp' (Lexp.hc (lexp_lexp' e1))); - assert (lexp_lexp' e2 == lexp_lexp' (Lexp.hc (lexp_lexp' e2))); + = assert (e1 == Lexp.hc (lexp_lexp' e1)); + assert (e2 == Lexp.hc (lexp_lexp' e2)); try let _ = List.find (fun (e1', e2') -> L.eq e1 e1' && L.eq e2 e2') s @@ -266,14 +266,12 @@ let level_leq (c1, m1) (c2, m2) = let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let e1' = lexp_whnf e1 ctx in let e2' = lexp_whnf e2 ctx in - let e1'' = lexp'_whnf e1 ctx in - let e2'' = lexp'_whnf e2 ctx in - e1'' == e2'' || - let changed = not (lexp_lexp' e1 == e1'' && lexp_lexp' e2 == e2'') in + e1' == e2' || + let changed = not (e1 == e1' && e2 == e2') in if changed && set_member_p vs e1' e2' then true else let vs' = if changed then set_add vs e1' e2' else vs in let conv_p = conv_p' ctx vs' in - match (e1'', e2'') with + match (lexp_lexp' e1', lexp_lexp' e2') with | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 | (Imm (Float (_, i1)), Imm (Float (_, i2))) -> i1 = i2 | (Imm (String (_, i1)), Imm (String (_, i2))) -> i1 = i2 @@ -331,7 +329,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (set_shift vs) args1 args2 | _,_ -> false in - lexp_lexp' l1 == lexp_lexp' l2 && conv_args ctx vs' args1 args2 + l1 == l2 && conv_args ctx vs' args1 args2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 (* I'm not sure to understand how to compare two Metavar * * Should I do a `lookup`? Or is it that simple: *) @@ -340,7 +338,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (_, _) -> false let conv_p (ctx : DB.lexp_context) e1 e2 - = if lexp_lexp' e1 == lexp_lexp' e2 then true + = if e1 == e2 then true else conv_p' ctx set_empty e1 e2 (********* Testing if a lexp is properly typed *********) ===================================== src/unification.ml ===================================== @@ -184,30 +184,28 @@ let rec unify (e1: lexp) (e2: lexp) and unify' (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) (vs : OL.set_plexp) : return_type = - if lexp_lexp' e1 == lexp_lexp' e2 then [] else + if e1 == e2 then [] else let e1' = OL.lexp_whnf e1 ctx in let e2' = OL.lexp_whnf e2 ctx in - let e1'' = lexp_lexp' e1' in - let e2'' = lexp_lexp' e2' in - if e1'' == e2'' then [] else + if e1' == e2' then [] else let changed = true (* not (e1 == e1' && e2 == e2') *) in if changed && OL.set_member_p vs e1' e2' then [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in - match (e1'', e2'') with + match (lexp_lexp' e1', lexp_lexp' e2') with | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _)) -> if OL.conv_p ctx e1' e2' then [] else [(CKimpossible, ctx, e1, e2)] - | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s e2' e1' - | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s e1' e2' - | (l, (Call _ as r)) -> unify_call e2' e1' ctx vs' + | (_, Metavar (idx, s, _)) -> unify_metavar ctx idx s e2' e1' + | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2' + | (_, Call _) -> unify_call e2' e1' ctx vs' (* | (l, (Case _ as r)) -> unify_case r l subst *) - | (Arrow _ as l, r) -> unify_arrow e1' e2' ctx vs' - | (Lambda _ as l, r) -> unify_lambda e1' e2' ctx vs' - | (Call _ as l, r) -> unify_call e1' e2' ctx vs' + | (Arrow _ , _) -> unify_arrow e1' e2' ctx vs' + | (Lambda _, _) -> unify_lambda e1' e2' ctx vs' + | (Call _, _) -> unify_call e1' e2' ctx vs' (* | (Case _ as l, r) -> unify_case l r subst *) (* | (Inductive _ as l, r) -> unify_induct l r subst *) - | (Sort _ as l, r) -> unify_sort e1' e2' ctx vs' - | (SortLevel _ as l, r) -> unify_sortlvl e1' e2' ctx vs' + | (Sort _, _) -> unify_sort e1' e2' ctx vs' + | (SortLevel _, _) -> unify_sortlvl e1' e2' ctx vs' | (Inductive (_loc1, label1, args1, consts1), Inductive (_loc2, label2, args2, consts2)) -> (* print_string ("Unifying inductives " View it on GitLab: https://gitlab.com/monnier/typer/-/commit/3376edace9286d4aff35fb4f87be0628e… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/3376edace9286d4aff35fb4f87be0628e… You're receiving this email because of your account on gitlab.com.

2 1

[Git][monnier/typer][report/hmdup] -
by Stefan 28 Jui '20

28 Jui '20

Stefan pushed to branch report/hmdup at Stefan / Typer Commits: b9d015b4 by Stefan Monnier at 2020-06-28T17:57:48-04:00 - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -310,6 +310,7 @@ minimizing the amount of type annotations was secondary to the design. \newcommand \Arw [2] {#1 \to #2} \newcommand \Lam [2] {\lambda #1 . #2} \newcommand \TLam [2] {\Lambda #1 . #2} +\newcommand \TApp [2] {#1[#2]} \newcommand \Meta [1] {#1} \newcommand \DArw [3] {\forall #1 \: #2 . #3} \newcommand \Let [3] {\kw{let}~#1=#2~\kw{in}~#3} @@ -577,24 +578,17 @@ a $\Lam{x}{e}$. } \Infer{ - %% \Jmono{\tau} \\ - \Jsynth e \tau' \\ - \Jcoerce {\tau'} \tau + \Jcheck[\Gamma,\overrightarrow{t\:*}] e {\tau} }{ - \JcheckCoerce{e}{\tau} + \JcheckCoerce{e}{\MDArw{t\:*}{\tau}} } - %% \Infer{ - %% \Jsynth{e}{\tau'} \\ - %% \Jcoerce {\tau'} \tau - %% }{ - %% \JsynthCoerce{e}{\tau} - %% } - %% \Infer{ - \Jcheck[\Gamma,\overrightarrow{t\:*}] e {\tau} + %% \Jmono{\tau} \\ + \Jsynth e \tau' \\ + \Jcoerce {\tau'} \tau }{ - \JcheckCoerce{e}{\MDArw{t\:*}{\tau}} + \JcheckCoerce{e}{\tau} } \end{mathpar} \caption{Bidirectional type inference for System F} @@ -803,86 +797,11 @@ incompatible with things like value polymorphism. \section{Elaboration} -\FIXME{Adapt the rules to the new algorithm} - -\begin{figure} - \begin{mathpar} - \Infer{ - \Gamma(x) = \tau - }{ - \Jsynth{x}{\tau} - } - - \Infer{ - \Jsynth{e_1}{\tau_1} \\ - \tau_1' = \kw{gen}(\Gamma,\tau_1) \\ - \Jpoly[\Gamma,x\:\tau_1']{e_2}{\tau} - }{ - \Jpoly{\Let x {e_1}{e_2}}{\tau} - } - - \Infer{ - %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \\ - \Jfresh{u_1,u_2} \\ - \JcheckCoerce{e_1}{\Arw{u_1}{u_2}} \\ - \JcheckCoerce{e_2}{u_1} - }{ - \Jsynth{e_1~e_2}{u_2} - } - - \Infer{ - \Jfresh{u_1, u_2} \\ - %% FIXME: Introduce polymorphism?! - \Junify{\tau}{\Arw{u_1}{u_2}} \\ - \JcheckCoerce[\Gamma,x\:u_1] e {u_2} - }{ - \Jcheck{\Lam x e}{\tau} - } - %% - - %% - \Infer{ - \JcheckCoerce e \tau - }{ - \Jsynth{\HasType{e}{\tau}}{\tau} - } - - \Infer{ - \Jfresh{\Meta{u}} \\ \Jcheck e {\Meta{u}} - }{ - %% FIXME: Make it \JsynthCoerce? - \Jsynth e {\Meta{u}} - } - - \Infer{ - %% \Jmono{\tau} \\ - \Jsynth e \tau' \\ - \Jcoerce {\tau'} \tau - }{ - \JcheckCoerce{e}{\tau} - } - - %% \Infer{ - %% \Jsynth{e}{\tau'} \\ - %% \Jcoerce {\tau'} \tau - %% }{ - %% \JsynthCoerce{e}{\tau} - %% } - %% - \Infer{ - \Jcheck[\Gamma,\overrightarrow{t\:*}] e {\tau} - }{ - \JcheckCoerce{e}{\MDArw{t\:*}{\tau}} - } - \end{mathpar} - \caption{Bidirectional type inference for System F} - \label{fig:system-f} -\end{figure} - \newcommand \JEcheck [4][\Gamma] {#1 \vdash #2 : #3 \Rightarrow #4} \newcommand \JEsynth [4][\Gamma] {#1 \vdash #2 \Rightarrow #4 : #3} \newcommand \JEcheckCoerce [4][\Gamma] {#1 \vdash #2 : #3 \Longrightarrow #4} \newcommand \JEpoly [4][\Gamma] {#1 \vdash #2 \Leftrightarrow #4 : #3} +\newcommand \JEcoerce [4] {#1 : #2 \stackrel{\kw{coerce}}{\Longrightarrow} #3 : #4} \begin{figure} \begin{mathpar} @@ -931,18 +850,39 @@ incompatible with things like value polymorphism. \JEsynth{e}{\Meta{u}}{E} } + \Infer{ + \JEcheck[\Gamma,\overrightarrow{t\:*}] e {\tau}{E} + }{ + \JEcheckCoerce{e}{\MDArw{t\:*}{\tau}}{\TLam{\overrightarrow{t\:*}}{E}} + } + \Infer{ %% \Jmono{\tau} \\ - \JEsynth{e}{\tau'}{E} \\ - \FIXMEs{E' = \Jcoerce {\tau'} \tau} + \JEsynth{e}{\tau}{E} \\ + \JEcoerce {E}{\tau}{E'}{\tau'} + }{ + \JEcheckCoerce{e}{\tau'}{E'} + } + + %% FIXME: The rules below don't make much sense yet, I think! + %% + \Infer{ + \Jfresh {\vec {\Meta{u}}} \\ + \Junify{\tau[\vec {\Meta{u}}/\vec t]}{\tau'} }{ - \JEcheckCoerce{e}{\tau}{E'} + \JEcoerce {E} {\MDArw{t\:*}{\tau}} + {\TApp{E}{\vec {\Meta{u}}}} {\tau'} } \Infer{ - \JEcheck[\Gamma,\overrightarrow{t\:*}] e {\tau}{E} + \Jfresh {\vec {\Meta{u}}} \\ + \JEcoerce {E} {\tau} {E'} {\tau'[\vec {\Meta{u}}/\vec t]} \\ + %% FIXME: Maybe "u" was instantiated to some other + %% (uninstantiated) metavar. If so, should it still be in `fmv`? + %% FIXME: Define `fmv`!! + \vec {\Meta{u}} \subset \kw{fmv}(\Gamma,\tau'[\vec {\Meta{u}}/\vec t]) }{ - \JEcheckCoerce{e}{\MDArw{t\:*}{\tau}}{\TLam{\overrightarrow{t\:*}}{E}} + \JEcoerce {E} {\tau} {\TLam{\overrightarrow{t\:*}}{E'}} {\MDArw{t\:*}{\tau'}} } \end{mathpar} \caption{Elaboration for System F} View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b9d015b4842ea6de505a6735d5913dc01… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b9d015b4842ea6de505a6735d5913dc01… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/hmdup] 2 commits: -
by Stefan 28 Jui '20

28 Jui '20

Stefan pushed to branch report/hmdup at Stefan / Typer Commits: 7a1a6d26 by Stefan Monnier at 2020-06-28T16:07:26-04:00 - - - - - - 103c6743 by Stefan Monnier at 2020-06-28T16:07:52-04:00 - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -90,6 +90,7 @@ \newcommand \Comment[1] {} \newcommand \FIXME[1] {\fbox{\parbox{\columnwidth}{{\color{red}{¡FIXME!}} #1}}} +\newcommand \FIXMEs[1] {\fbox{{\color{red}{\text{¡FIXME!}}} #1}} %% \newtheorem{theorem}{Theorem}[section] %% \newtheorem{lemma}[theorem]{Lemma} \theoremstyle{plain} @@ -313,6 +314,7 @@ minimizing the amount of type annotations was secondary to the design. \newcommand \DArw [3] {\forall #1 \: #2 . #3} \newcommand \Let [3] {\kw{let}~#1=#2~\kw{in}~#3} \newcommand \MDArw [2] {\forall \overrightarrow{#1} . #2} +\newcommand \HasType [2] {#1 \: #2} \newcommand \Jcheck [3][\Gamma] {#1 \vdash #2 \Leftarrow #3} \newcommand \Jsynth [3][\Gamma] {#1 \vdash #2 \Rightarrow #3} @@ -447,7 +449,7 @@ $u_2$ was instantiated to. \Jcheck{\Lam x e}{\Arw{\tau_1}{\tau_2}} } - \Infer{\Jcheck e \tau}{\Jsynth{e : \tau}{\tau}} + \Infer{\Jcheck e \tau}{\Jsynth{\HasType{e}{\tau}}{\tau}} \Infer{\Jsynth e \tau' \\ \tau = \tau'}{\Jcheck{e}{\tau}} %% @@ -498,7 +500,7 @@ type check the $\lambda$-calculus. \Jcheck{\Lam x e}{\tau} } \\\\ - \Infer{\Jcheck e \tau}{\Jsynth{e : \tau}{\tau}} + \Infer{\Jcheck e \tau}{\Jsynth{\HasType{e}{\tau}}{\tau}} \Infer{\Jfresh{\Meta{u}} \\ \Jcheck e {\Meta{u}}}{\Jsynth e {\Meta{u}}} @@ -521,9 +523,9 @@ a $\Lam{x}{e}$. \section{System F} -\newcommand \JsynthCoerce [3][\Gamma] {#1 \vdash #2 \Longrightarrow #3} +%% \newcommand \JsynthCoerce [3][\Gamma] {#1 \vdash #2 \Longrightarrow #3} \newcommand \JcheckCoerce [3][\Gamma] {#1 \vdash #2 \Longleftarrow #3} -\newcommand \Jmono [1] {\kw{monotype}(#1)} +%% \newcommand \Jmono [1] {\kw{monotype}(#1)} \begin{figure} \begin{mathpar} @@ -564,7 +566,7 @@ a $\Lam{x}{e}$. \Infer{ \JcheckCoerce e \tau }{ - \Jsynth{e : \tau}{\tau} + \Jsynth{\HasType{e}{\tau}}{\tau} } \Infer{ @@ -652,7 +654,7 @@ a $\Lam{x}{e}$. %% \Infer{ %% \Jcheck e \tau %% }{ -%% \Jsynth{e : \tau}{\tau} +%% \Jsynth{\HasType{e}{\tau}}{\tau} %% } %% \Infer{ @@ -694,7 +696,8 @@ Our inference algorithm takes inspiration from bidirectional type systems to try and make better use of that information. The only change to the syntax of the language is the addition of the form -$e : \tau$. While the specific form of the type annotations is not a primary +$\HasType{e}{\tau}$. While the specific form of the type annotations is not +a primary concern for us, we did want to avoid ``non-standard'' annotations such as the freeze annotation of FreezeML~\cite{Emrich20} or the constrained quantifiers of \MLF: @@ -703,7 +706,7 @@ quantifiers of \MLF: \begin{array}{cc@{\;\;::=\;\;}l} \textit{(types)} & \tau & t ~|~ \Meta{u} ~|~ \Arw{\tau_1}{\tau_2} ~|~ \DArw t * \tau \\ \textit{(terms)} & e & x ~|~ \Lam x e ~|~ e_1~e_2 ~|~ \Let x {e_1} {e_2} - ~|~ e : \tau \\ + ~|~ \HasType{e}{\tau} \\ \textit{(context)} & \Gamma & \bullet ~|~ \Gamma,x\:\tau ~|~ \Gamma,t\:* \\ %% \textit{(substitutions)} & \sigma & \textsf{id} ~|~ \sigma,\Meta{u}\mapsto\tau \end{array} @@ -718,7 +721,7 @@ just a shorthand for a pair of rules, one that checks and one that synthesizes. The first three lines are equivalent to the base Hindley-Milner system presented earlier. The two differences are: (1) the instantiation of polymorphic terms has now been moved from the variable rule to its own -$\JsynthCoerce{e}{\tau}$ judgment and it is now applied less eagerly; (2) the +$\JcheckCoerce{e}{\tau}$ judgment and it is now applied less eagerly; (2) the application rule does not unify the synthesized type of the argument with the type expected by the function any more but instead it \emph{checks} the type of the argument against that expected by the function. @@ -802,42 +805,91 @@ incompatible with things like value polymorphism. \FIXME{Adapt the rules to the new algorithm} -\newcommand \JEcheck [4][\Gamma] {#1 \vdash #2 : #3 \Rightarrow #4} -\newcommand \JEsynth [4][\Gamma] {#1 \vdash #2 \Rightarrow #4 : #3} -\newcommand \JEsynthMono [4][\Gamma] {#1 \vdash #2 \Longrightarrow #4 : #3} -\newcommand \JEpoly [4][\Gamma] {#1 \vdash #2 \Leftrightarrow #4 : #3} - \begin{figure} \begin{mathpar} \Infer{ \Gamma(x) = \tau }{ - \JEsynth{x}{\tau}{x} + \Jsynth{x}{\tau} } \Infer{ - \JEsynth{x}{\MDArw {t\:*} \tau}{E} \\ - \Jfresh {\vec u} + \Jsynth{e_1}{\tau_1} \\ + \tau_1' = \kw{gen}(\Gamma,\tau_1) \\ + \Jpoly[\Gamma,x\:\tau_1']{e_2}{\tau} }{ - \JEsynthMono{x}{\tau[\vec u/\vec t]}{E[\vec u]} + \Jpoly{\Let x {e_1}{e_2}}{\tau} } \Infer{ - %% \Jmono{\tau} \\ - \JEsynthMono e {\tau'} {E}\\ - \Junify \tau {\tau'} + %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \\ + \Jfresh{u_1,u_2} \\ + \JcheckCoerce{e_1}{\Arw{u_1}{u_2}} \\ + \JcheckCoerce{e_2}{u_1} }{ - \JEcheck{e}{\tau} {E} + \Jsynth{e_1~e_2}{u_2} } \Infer{ - %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \\ - \JEsynthMono{e_1}{\tau}{E_1} \\ - \Jfresh{u_1,u_2} \\ + \Jfresh{u_1, u_2} \\ + %% FIXME: Introduce polymorphism?! \Junify{\tau}{\Arw{u_1}{u_2}} \\ - \JEcheck{e_2}{u_1}{E_2} + \JcheckCoerce[\Gamma,x\:u_1] e {u_2} }{ - \JEsynth{e_1~e_2}{u_2}{E_1~E_2} + \Jcheck{\Lam x e}{\tau} + } + %% + + %% + \Infer{ + \JcheckCoerce e \tau + }{ + \Jsynth{\HasType{e}{\tau}}{\tau} + } + + \Infer{ + \Jfresh{\Meta{u}} \\ \Jcheck e {\Meta{u}} + }{ + %% FIXME: Make it \JsynthCoerce? + \Jsynth e {\Meta{u}} + } + + \Infer{ + %% \Jmono{\tau} \\ + \Jsynth e \tau' \\ + \Jcoerce {\tau'} \tau + }{ + \JcheckCoerce{e}{\tau} + } + + %% \Infer{ + %% \Jsynth{e}{\tau'} \\ + %% \Jcoerce {\tau'} \tau + %% }{ + %% \JsynthCoerce{e}{\tau} + %% } + %% + \Infer{ + \Jcheck[\Gamma,\overrightarrow{t\:*}] e {\tau} + }{ + \JcheckCoerce{e}{\MDArw{t\:*}{\tau}} + } + \end{mathpar} + \caption{Bidirectional type inference for System F} + \label{fig:system-f} +\end{figure} + +\newcommand \JEcheck [4][\Gamma] {#1 \vdash #2 : #3 \Rightarrow #4} +\newcommand \JEsynth [4][\Gamma] {#1 \vdash #2 \Rightarrow #4 : #3} +\newcommand \JEcheckCoerce [4][\Gamma] {#1 \vdash #2 : #3 \Longrightarrow #4} +\newcommand \JEpoly [4][\Gamma] {#1 \vdash #2 \Leftrightarrow #4 : #3} + +\begin{figure} + \begin{mathpar} + \Infer{ + \Gamma(x) = \tau + }{ + \JEsynth{x}{\tau}{x} } \Infer{ @@ -845,42 +897,53 @@ incompatible with things like value polymorphism. \overrightarrow{t\:*} = \kw{fmv}(\Gamma,\tau_1) \\ \JEpoly[\Gamma,x\:\MDArw{t\:*}{\tau_1}]{e_2}{\tau}{E_2} }{ - \JEpoly{\Let x {e_1}{e_2}}{\tau}{\Let x {\TLam{t\:*}{E_1}}{E_2}} + \JEpoly{\Let x {e_1}{e_2}}{\tau}{ + \Let {x} {\TLam{\overrightarrow{t\:*}}{E_1}}{E_2}} } \Infer{ - \Jfresh u \\ - \JEsynthMono[\Gamma,x\:u] e {\tau}{E} + %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \\ + \Jfresh{u_1,u_2} \\ + \JEcheckCoerce{e_1}{\Arw{u_1}{u_2}}{E_1} \\ + \JEcheck{e_2}{u_1}{E_2} }{ - \JEsynth{\Lam x e}{\Arw{u}{\tau}}{\Lam{x\:u}{E}} + \JEsynth{e_1~e_2}{u_2}{E_1~E_2} } - %% - \\\\ - %% + \Infer{ - \JEcheck e \tau E + \Jfresh {\Meta{u_1},\Meta{u_2}} \\ + \Junify {\tau}{\Arw{\Meta{u_1}}{\Meta{u_2}}} \\ + \JEcheckCoerce[\Gamma,x\:\Meta{u_1}]{e}{\Meta{u_2}}{E} }{ - \JEsynth{e : \tau}{\tau}{E} + \JEcheck{\Lam x e}{\tau}{\Lam{x\:\Meta{u_1}}{E}} } \Infer{ - \JEcheck[\Gamma,x\:\tau_1] e {\tau_2} {E} + \JEcheckCoerce e \tau E }{ - \JEcheck{\Lam x e}{\Arw{\tau_1}{\tau_2}} {\Lam{x\:\tau_1}{E}} + \JEsynth{\HasType{e}{\tau}}{\tau}{E} + } + + \Infer{ + \Jfresh{\Meta{u}} \\ \JEcheck{e}{\Meta{u}}{E} + }{ + %% FIXME: Make it \JsynthCoerce? + \JEsynth{e}{\Meta{u}}{E} } - %% \Infer{ - %% \Gamma(x) = \tau' \\ \Junify{\tau'}{\DArw{t}{*}{\tau}} - %% }{ - %% \Jcheck{x}{\DArw{t}{*}{\tau}} - %% } - %% \Infer{ - \JEcheck[\Gamma,t\:*] e {\tau} {E} + %% \Jmono{\tau} \\ + \JEsynth{e}{\tau'}{E} \\ + \FIXMEs{E' = \Jcoerce {\tau'} \tau} }{ - \JEcheck{e}{\DArw{t}{*}{\tau}} {\TLam{t\:*}E} + \JEcheckCoerce{e}{\tau}{E'} } + \Infer{ + \JEcheck[\Gamma,\overrightarrow{t\:*}] e {\tau}{E} + }{ + \JEcheckCoerce{e}{\MDArw{t\:*}{\tau}}{\TLam{\overrightarrow{t\:*}}{E}} + } \end{mathpar} \caption{Elaboration for System F} \label{fig:elab-system-f} @@ -902,8 +965,9 @@ our language is extended as follows: \begin{displaymath} \begin{array}{cc@{\;\;::=\;\;}l} \textit{(types)} & \tau & t ~|~ \Meta{u} ~|~ \Arw{\tau_1}{\tau_2} ~|~ \DArw t * \tau \\ - \textit{(terms)} & e & x ~|~ \Meta{u} ~|~ \Lam x e ~|~ e_1~e_2 ~|~ \Let x {e_1} {e_2} - ~|~ e : \tau \\ + \textit{(terms)} & e & x ~|~ \Meta{u} ~|~ \Lam x e ~|~ e_1~e_2 ~|~ \Let + x {e_1} {e_2} + ~|~ \HasType{e}{\tau} \\ \textit{(context)} & \Gamma & \bullet ~|~ \Gamma,x\:\tau ~|~ \Gamma,t\:* \\ %% \textit{(substitutions)} & \sigma & \textsf{id} ~|~ \sigma,\Meta{u}\mapsto\tau \end{array} View it on GitLab: https://gitlab.com/monnier/typer/-/compare/44ef07b166dcff92504793feab10e642… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/44ef07b166dcff92504793feab10e642… You're receiving this email because of your account on gitlab.com.

1 0

Type inference paper
by Stefan Monnier 28 Jui '20

28 Jui '20

To whoever's interested in helping: I just pushed to the `report/hmdup` branch a (very much) work-in-progress article where I try to document the type inference algorithm of Typer (well, more like the one I'd like to use than the one we do use, so it's a mix of "document" and "cleanup/fix" and "after-the-fact design"). If you're interested in helping, I suggest you try and understand what is currently there and then come back with questions about what you don't understand. You'll also see a boatload of FIXMEs which you're welcome to try and attack. I think currently one of the more feasible and useful things would be to work on the proofs that our inference for System F is conservative, sound, and complete. Stefan

1 0

[Git][monnier/typer] Pushed new branch report/hmdup
by Stefan 28 Jui '20

28 Jui '20

Stefan pushed new branch report/hmdup at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/report/hmdup You're receiving this email because of your account on gitlab.com.

1 0

Re: [Typer] Question au sujet du case dans typer
by Stefan Monnier 28 Jui '20

28 Jui '20

> Si je comprends bien, ce n'est pas encore implanté en typer que la branche > du case reçoit une preuve d'égalité entre le sujet du case et la "tête" de > la branche? Yup. > Et additionnellement, si je comprends bien, il semble y avoir un bug qui > contourne ce manquement dans certaines preuves comme celle que j'ai faites > dans samples/decidable.typer, qui pourrait être relié à ce commentaire: > https://gitlab.com/monnier/typer/-/blob/master/btl/builtins.typer#L65-68? En effet. > Je me demandais ce qu'il manquerait pour implanter cette > fonctionnalité. Pas grand chose: il faut juste l'ajouter dans l'environnement de chaque branche. > D'une part, j'imagine qu'il faudrait ajouter une syntaxe > pour avoir accès à cette preuve d'égalité. Non, c'est pas nécessaire. La forme (##DeBruijn N) permet déjà de faire référence à n'importe quelle variable, y compris celle qui n'ont pas de nom. Stefan

1 0

[Git][monnier/typer][alice] add dependency between subst and lexp & hash sharing counter
by Alice de Berny 24 Jui '20

24 Jui '20

Alice de Berny pushed to branch alice at Stefan / Typer Commits: 50177654 by irradiee at 2020-06-24T10:40:07-04:00 add dependency between subst and lexp & hash sharing counter - - - - - 8 changed files: - src/REPL.ml - src/elab.ml - src/inverse_subst.ml - src/lexp.ml - src/lexp_type.ml - src/subst.ml - src/unification.ml - src/util.ml Changes: ===================================== src/REPL.ml ===================================== @@ -232,8 +232,8 @@ let rec repl i clxp rctx = | "%help" | "%h" -> (print_string help_msg; repl clxp rctx) | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx) - | "%lcollisions" | "%cl" -> (get_stats (WHC.stats hc_table)) - | "%scollisions" | "%scl" -> (get_stats (Subst.WHCSB.stats Subst.hcsb_table)) + | "%lcollisions" | "%cl" -> (get_stats (WHC.stats hc_table) !lshrct !sshrct) + | "%scollisions" | "%scl" -> (get_stats (Subst.WHCSB.stats Subst.hcsb_table) !lshrct !sshrct) (* command with arguments *) | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> ( ===================================== src/elab.ml ===================================== @@ -395,7 +395,7 @@ let rec meta_to_var ids (e : lexp) = *) (* `o` is the binding offset until the root. *) - let rec adjust_subst o (s : lsubst) = match S.subst_subst' s with + let rec adjust_subst o (s : subst) = match S.subst_subst' s with | Identity n -> let o' = o - n in if o' < 0 then ===================================== src/inverse_subst.ml ===================================== @@ -57,8 +57,8 @@ type substIR = ((int * int) list * int * int) (** Transform a substitution to a more linear substitution * makes the inversion easier * Example of result : ((new_idx, old_position)::..., shift)*) -let transfo (s: lsubst) : substIR option = - let rec transfo (s: lsubst) (off_acc: int) (idx: int) (imp_cnt : int) +let transfo (s: subst) : substIR option = + let rec transfo (s: subst) (off_acc: int) (idx: int) (imp_cnt : int) : substIR option = let indexOf (v: lexp): int = (* Helper : return the index of a variabble *) let v' = lexp_lexp' v in @@ -106,18 +106,18 @@ let mkVar (idx: int) : lexp = @param size size of the list to return @param acc recursion accumulator *) -let fill (l: (int * int) list) (nbVar: int) (shift: int): lsubst option = - let rec genDummyVar (beg_: int) (end_: int) (l: lsubst): lsubst = (* Create the filler variables *) +let fill (l: (int * int) list) (nbVar: int) (shift: int): subst option = + let rec genDummyVar (beg_: int) (end_: int) (l: subst): subst = (* Create the filler variables *) if beg_ < end_ then S.cons impossible (genDummyVar (beg_ + 1) end_ l) else l in - let fill_before (l: (int * int) list) (s: lsubst) (nbVar: int): lsubst option = (* Fill if the first var is not 0 *) + let fill_before (l: (int * int) list) (s: subst) (nbVar: int): subst option = (* Fill if the first var is not 0 *) match l with | [] -> Some (genDummyVar 0 nbVar s) | (i1, v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) | _ -> Some s - in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): lsubst option = (* Fill gaps *) + in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): subst option = (* Fill gaps *) match l with | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None @@ -144,8 +144,8 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): lsubst option = | None -> None | Some s -> fill_before l s nbVar -let is_identity (s : lsubst) = - let rec is_identity (s : lsubst) acc = +let is_identity (s : subst) = + let rec is_identity (s : subst) acc = match S.subst_subst' s with | Cons((Var(_, idx), _), s1, 0) when idx = acc -> is_identity s1 (acc + 1) | Identity o -> acc = o @@ -156,7 +156,7 @@ let is_identity (s : lsubst) = <code>s:S.subst, l:lexp, s':S.subst</code> where <code>l[s][s'] = l</code> and <code> inverse s = s' </code> *) -let inverse (s: lsubst) : lsubst option = +let inverse (s: subst) : subst option = let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) in match transfo s with | None -> None @@ -182,7 +182,7 @@ let inverse (s: lsubst) : lsubst option = (* Returns false if the application of the inverse substitution is not * possible. This happens when the substitution replaces some variables * with non-variables, in which case the "inverse" is ambiguous. *) -let rec invertible (s: lsubst) : bool = match S.subst_subst' s with +let rec invertible (s: subst) : bool = match S.subst_subst' s with | Identity _ -> true | Cons (e, s, _) -> (let e' = lexp_lexp' e in @@ -193,7 +193,7 @@ exception Not_invertible exception Ambiguous (* Lookup variable i in s⁻¹ *) -let rec lookup_inv_subst (i : db_index) (s : lsubst) : db_index +let rec lookup_inv_subst (i : db_index) (s : subst) : db_index = match S.subst_subst' s with | (Identity o | Cons (_, _, o)) when i < o -> raise Not_invertible | Identity o -> i - o @@ -240,7 +240,7 @@ let shift_inv_subst n s * One way to do it is to compute s⁻¹ and then pass it to `compose`. * But we can try and do it more directly. *) -let rec compose_inv_subst (s' : lsubst) (s : lsubst) = match S.subst_subst' s' with +let rec compose_inv_subst (s' : subst) (s : subst) = match S.subst_subst' s' with | Cons (e, s', o) -> let s = shift_inv_subst o s in (* FIXME: Why don't we ever return a Shift? *) @@ -254,7 +254,7 @@ let rec compose_inv_subst (s' : lsubst) (s : lsubst) = match S.subst_subst' s' w * The function presumes that `invertible s` was true. * This can be used like mkSusp/push_susp, but it's not lazy. * This is because it can signal errors Not_invertible or Ambiguous. *) -and apply_inv_subst (e : lexp) (s : lsubst) : lexp = +and apply_inv_subst (e : lexp) (s : subst) : lexp = let e' = lexp_lexp' e in match e' with | Imm _ -> e ===================================== src/lexp.ml ===================================== @@ -42,10 +42,28 @@ open Grammar let lexp_lexp' (e, h) = e - let rec apply_lxor (map : int list) : int = - match map with - | [] -> 31 - | e :: l -> (e * 31) lxor (apply_lxor l) +let rec apply_lxor (map : int list) : int = + match map with + | [] -> 31 + | e :: l -> (e * 31) lxor (apply_lxor l) + +let attributemap_combine_hash (k: (int * string)) (v: lexp) (p: int) : int = +shrct_inc lshrct 1; + (p * 31) lxor (((Hashtbl.hash k) * 31) lxor (lexp_hash v)) + +let ind_stringmap_combine_hash (k: string) (v: ((arg_kind * vname * ltype) list)) (p: int) : int = + (p * 31) lxor ((Hashtbl.hash k) * 31) lxor + (apply_lxor (List.map (fun e -> let (ak, n, lt) = e in + shrct_inc lshrct 1; + (U.combine_hash (Hashtbl.hash ak) + (U.combine_hash (Hashtbl.hash n) (lexp_hash lt)))) v)) + +let case_stringmap_combine_hash (k: string) (v: (U.location * (arg_kind * vname) list * lexp)) (p: int) : int = + shrct_inc lshrct 1; + let (loc, li, lp) = v in + (p * 31) lxor ((Hashtbl.hash k) * 31) lxor + (Hashtbl.hash loc) lxor (Hashtbl.hash li) lxor (lexp_hash lp) + (* Hashtbl.hash for not lexp types * TODO: - find something else @@ -56,51 +74,67 @@ open Grammar | SortLevel l -> U.combine_hash 2 (match l with | SLz -> Hashtbl.hash l - | SLsucc lp -> lexp_hash lp - | SLlub (lp1, lp2) -> U.combine_hash (lexp_hash lp1) (lexp_hash lp2)) + | SLsucc lp -> shrct_inc lshrct 1; lexp_hash lp + | SLlub (lp1, lp2) + -> shrct_inc lshrct 2; U.combine_hash (lexp_hash lp1) (lexp_hash lp2)) | Sort (l, s) -> U.combine_hash 3 (U.combine_hash (Hashtbl.hash l) (match s with - | Stype lp -> lexp_hash lp + | Stype lp -> shrct_inc lshrct 1; lexp_hash lp | StypeOmega -> Hashtbl.hash s | StypeLevel -> Hashtbl.hash s)) - | Builtin (v, t, m) as e -> U.combine_hash 4 (Hashtbl.hash e) + | Builtin (v, t, m) + -> shrct_inc lshrct 1; U.combine_hash 4 (U.combine_hash + (U.combine_hash (Hashtbl.hash v) (lexp_hash t)) + (match m with + | Some m -> (AttributeMap.fold attributemap_combine_hash + m 31) + | None -> 404)) | Var v -> U.combine_hash 5 (Hashtbl.hash v) | Let (l, ds, e) - -> U.combine_hash 6 (U.combine_hash (Hashtbl.hash l) + -> shrct_inc lshrct 1; + U.combine_hash 6 (U.combine_hash (Hashtbl.hash l) (U.combine_hash (apply_lxor (List.map (fun e -> let (n, lp, lt) = e in + shrct_inc lshrct 2; (U.combine_hash (Hashtbl.hash n) (U.combine_hash (lexp_hash lp) (lexp_hash lt)))) ds)) (lexp_hash e))) | Arrow (k, v, t1, l, t2) - -> U.combine_hash 7 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) - (U.combine_hash (lexp_hash t1) (U.combine_hash (Hashtbl.hash l) (lexp_hash t2)))) + -> shrct_inc lshrct 2; + U.combine_hash 7 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (U.combine_hash (lexp_hash t1) (U.combine_hash (Hashtbl.hash l) (lexp_hash t2)))) | Lambda (k, v, t, e) - -> U.combine_hash 8 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) - (U.combine_hash (lexp_hash t) (lexp_hash e))) + -> shrct_inc lshrct 2; + U.combine_hash 8 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (U.combine_hash (lexp_hash t) (lexp_hash e))) | Inductive (l, n, a, cs) -> U.combine_hash 9 (U.combine_hash (U.combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) (U.combine_hash (apply_lxor (List.map (fun e -> let (ak, n, lt) = e in - (U.combine_hash (Hashtbl.hash ak) + shrct_inc lshrct 1; + (U.combine_hash (Hashtbl.hash ak) (U.combine_hash (Hashtbl.hash n) (lexp_hash lt)))) a)) - (Hashtbl.hash cs))) - | Cons (t, n) -> U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n)) + (SMap.fold ind_stringmap_combine_hash + cs 21))) + | Cons (t, n) -> shrct_inc lshrct 1; U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n)) | Case (l, e, rt, bs, d) - -> U.combine_hash 11 (U.combine_hash (U.combine_hash (Hashtbl.hash l) (lexp_hash e)) - (U.combine_hash (lexp_hash rt) (U.combine_hash (Hashtbl.hash bs) + -> shrct_inc lshrct 2; + U.combine_hash 11 (U.combine_hash (U.combine_hash (Hashtbl.hash l) (lexp_hash e)) + (U.combine_hash (lexp_hash rt) (U.combine_hash + (SMap.fold case_stringmap_combine_hash bs 21) (match d with - | Some (n, lp) -> U.combine_hash (Hashtbl.hash n) (lexp_hash lp) + | Some (n, lp) -> shrct_inc lshrct 1; U.combine_hash (Hashtbl.hash n) (lexp_hash lp) | _ -> 0)))) | Metavar (id, s, v) - -> U.combine_hash 12 (Hashtbl.hash expr) - | Call (e, args) -> U.combine_hash 13 (U.combine_hash (lexp_hash e) - (apply_lxor (List.map (fun e -> let (ak, lp) = e in - (U.combine_hash (Hashtbl.hash ak) (lexp_hash lp))) args))) - | Susp (lp, subst) -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst)) - -let compare_hash x y = - let (x', h1) = x in - let (y', h2) = y in - compare h1 h2 = 0 + -> shrct_inc sshrct 1; + U.combine_hash 12 (U.combine_hash id + (U.combine_hash (S.subst_hash s) (Hashtbl.hash v))) + | Call (e, args) + -> shrct_inc lshrct 1; U.combine_hash 13 (U.combine_hash (lexp_hash e) + (apply_lxor (List.map (fun e -> let (ak, lp) = e in + shrct_inc lshrct 1; + (U.combine_hash (Hashtbl.hash ak) (lexp_hash lp))) args))) + | Susp (lp, subst) + -> shrct_inc lshrct 1; shrct_inc sshrct 1; + U.combine_hash 14 (U.combine_hash (lexp_hash lp) (S.subst_hash subst)) let hc_eq e1 e2 = e1 == e2 || @@ -241,7 +275,7 @@ let mkSLsucc e = * but Weak.Make doesn't cut it because we need to index with a pair * that is transient and hence immediately GC'd. *) -let hcs_table : ((lexp * lexp subst), lexp) Hashtbl.t = Hashtbl.create 1000 +let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 (* When computing the type of "load"ed modules * we end up building substitutions of the form ===================================== src/lexp_type.ml ===================================== @@ -1,3 +1,25 @@ +(* lexp_type.ml --- Lambda-expressions: the core language. + +Copyright (C) 2011-2020 Free Software Foundation, Inc. + +Author: Stefan Monnier <monnier(a)iro.umontreal.ca> +Keywords: languages, lisp, dependent types. + +This file is part of Typer. + +Typer is free software; you can redistribute it and/or modify it under the +terms of the GNU General Public License as published by the Free Software +Foundation, either version 3 of the License, or (at your option) any +later version. + +Typer is distributed in the hope that it will be useful, but WITHOUT ANY +WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +FOR A PARTICULAR PURPOSE. See the GNU General Public License for +more details. + +You should have received a copy of the GNU General Public License along with +this program. If not, see <http://www.gnu.org/licenses/>. *) + module U = Util module L = List module SMap = U.SMap @@ -16,38 +38,6 @@ type label = symbol type attribute_key = (int * string) (* rev_dbi * Var name *) module AttributeMap = Map.Make (struct type t = attribute_key let compare = compare end) -(* We define here substitutions which take a variable within a source context - * Δₛ and should return an expression valid in target context Δₜ. - * - * The current implementation only handles a very limited subset of such - * substitutions. One of the many limitations is that we can only encode - * substitutions which map variables to variables. - *) - -type db_index = int (* DeBruijn index. *) -type db_offset = int (* DeBruijn index offset. *) - -(* Substitution, i.e. a mapping from db_index to 'a - * In practice, 'a is always lexp, but we keep it as a parameter: - * - for better modularity of the code. - * - to break a mutual dependency between the Lexp and the Subst modules. *) -type 'a subst = 'a subst' * int - and 'a subst' = (* lexp subst *) - | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *) - | Cons of 'a * 'a subst * db_offset (* Cons (e, s, o) ≡ (e · s) ∘ ↑ₒ *) - (* Myers's extra pointers down the list: - * * int * 'a subst * db_offset *) -(* Lift (n,m) increases indices≥N by M. - * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination - * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) - (* | Lift of db_index * db_offset *) - -(* Build Myers's "stack" element. *) -(* let mkCons e s o = match s with - * | Cons (_, _, _, sk1, Cons (_, _, _, sk2, s2, o2), o1) when sk1 >= sk2 - * -> Cons (e, s, o, sk1 + sk2 + 1, s2, o1 + o2 + o) - * | _ -> Cons (e, s, o, 1, s, o) *) - (*************** Elaboration to Lexp *********************) (* The scoping of `Let` is tricky: @@ -64,7 +54,6 @@ type 'a subst = 'a subst' * int * surrounded context extended with the first and the second bindings. *) type ltype = lexp - and lsubst = lexp subst and lexp = lexp' * int and lexp' = | Imm of sexp (* Used for strings, ... *) @@ -72,7 +61,7 @@ type ltype = lexp | Sort of U.location * sort | Builtin of symbol * ltype * lexp AttributeMap.t option | Var of vref - | Susp of lexp * lsubst (* Lazy explicit substitution: e[σ]. *) + | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vname * lexp * ltype) list * lexp | Arrow of arg_kind * vname * ltype * U.location * ltype @@ -88,7 +77,7 @@ type ltype = lexp * (vname * lexp) option (* Default. *) (* The `subst` will be applied to the the metavar's value when it * gets instantiated. *) - | Metavar of meta_id * lsubst * vname + | Metavar of meta_id * subst * vname (* (\* For logical metavars, there's no substitution. *\) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -123,12 +112,43 @@ type ltype = lexp | SLsucc of lexp | SLlub of lexp * lexp + (* We define here substitutions which take a variable within a source context + * Δₛ and should return an expression valid in target context Δₜ. + * + * The current implementation only handles a very limited subset of such + * substitutions. One of the many limitations is that we can only encode + * substitutions which map variables to variables. + *) + + and db_index = int (* DeBruijn index. *) + and db_offset = int (* DeBruijn index offset. *) + + (* Substitution, i.e. a mapping from db_index to lexp *) + and subst = subst' * int + and subst' = + | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *) + | Cons of lexp * subst * db_offset (* Cons (e, s, o) ≡ (e · s) ∘ ↑ₒ *) + (* Myers's extra pointers down the list: + * * int * lexp subst * db_offset *) + (* Lift (n,m) increases indices≥N by M. + * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination + * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) + (* | Lift of db_index * db_offset *) + + (* Build Myers's "stack" element. *) + (* let mkCons e s o = match s with + * | Cons (_, _, _, sk1, Cons (_, _, _, sk2, s2, o2), o1) when sk1 >= sk2 + * -> Cons (e, s, o, sk1 + sk2 + 1, s2, o1 + o2 + o) + * | _ -> Cons (e, s, o, 1, s, o) *) + + type varbind = | Variable | ForwardRef | LetDef of U.db_offset * lexp let lexp_hash (e, h) = h + (* For metavariables, we give each metavar a (hopefully) unique integer * and then we store its corresponding info into the `metavar_table` * global map. @@ -172,3 +192,10 @@ let metavar_lookup (id : meta_id) : metavar_info = try U.IMap.find id (!metavar_table) with Not_found -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!" + +(* counter for lexp sharing *) +let lshrct = ref 0 + +(* counter for subst sharing *) +let sshrct = ref 0 +let shrct_inc e acc = e := !e + acc ===================================== src/subst.ml ===================================== @@ -122,30 +122,31 @@ open Lexp_type -> lp1 == lp2 && lps1 == lps2 && off1 = off2 | _ -> false - let subst'_hash (sb : 'a subst') : int = + let subst'_hash (sb : subst') : int = match sb with | Identity off -> U.combine_hash 1 (Hashtbl.hash off) | Cons (lp, sb, off) - -> U.combine_hash 2 - (U.combine_hash (U.combine_hash + -> shrct_inc lshrct 1; shrct_inc sshrct 1; + U.combine_hash 2 + (U.combine_hash (U.combine_hash (lexp_hash lp) (subst_hash sb)) (Hashtbl.hash off)) - module WHCSB = Weak.Make (struct type t = lexp subst + module WHCSB = Weak.Make (struct type t = subst let equal x y = hcsb_eq x y let hash = subst_hash end) let hcsb_table : WHCSB.t = WHCSB.create 1000 - let hcsb (s : lexp subst') : lexp subst = + let hcsb (s : subst') : subst = let sb = (s, subst'_hash s) in WHCSB.merge hcsb_table sb (* Apply a substitution to a single variable. *) let lookup (mkVar : 'b -> db_index -> 'a) (mkShift: 'a -> db_offset -> 'a) - (s: 'a subst) (l : 'b) (v:db_index) : 'a = - let rec lookup' (o:db_offset) (s: 'a subst) (v:db_index) : 'a = + (s: subst) (l : 'b) (v:db_index) : 'a = + let rec lookup' (o:db_offset) (s: subst) (v:db_index) : 'a = match subst_subst' s with | Identity o' -> mkVar l (v + o + o') (* Use Myers's fastlane when applicable: @@ -165,11 +166,11 @@ let mkShift s (m:db_offset) = (* A substitution which adds M to every deBruijn index. * I.e. one that takes variables from a context Δₛ to an extended * context ΔₛΔₜ where Δₜ has size M. *) -let shift (m:db_offset) : 'a subst = hcsb (Identity m) +let shift (m:db_offset) : subst = hcsb (Identity m) (* Return a substitution which replaces #0 with `e` and then applies `s` * to the rest. *) -let cons e s : 'a subst = hcsb (Cons (e, s, 0)) +let cons e s : subst = hcsb (Cons (e, s, 0)) (* The trivial substitution which doesn't do anything. *) let identity = hcsb (Identity 0) @@ -179,12 +180,12 @@ let identity_p s = match subst_subst' s with | Identity o -> o = 0 | _ -> false (* Compose two substitutions. This implements the merging rules. * Returns s₁ ∘ s₂ (i.e. s₁ is applied before s₂) *) -let compose (mkSusp : 'a -> 'a subst -> 'a) - (s1: 'a subst) (s2: 'a subst) : 'a subst = +let compose (mkSusp : 'a -> subst -> 'a) + (s1: subst) (s2: subst) : subst = (* There is a bit of flexibility in what we return, in the sense * that some shifts can be pushed more or less down. Here we * want the shifts to float as far outside as possible. *) - let rec compose' (s1: 'a subst) (s2: 'a subst) : 'a subst = + let rec compose' (s1: subst) (s2: subst) : subst = match subst_subst' s1 with | Identity o1 -> let rec compose_id o1 s o = match subst_subst' s with @@ -213,7 +214,7 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) * I.e. take a substitution from Δs to Δₜ and return a substitution * from Δs,x to Δₜ,x. * Also known as `lift`. *) -let sink (mkVar : 'b -> db_index -> 'a) (l:'b) (s:'a subst) = +let sink (mkVar : 'b -> db_index -> 'a) (l:'b) (s:subst) = cons (mkVar l 0) (mkShift s 1) (* Return a substitution which replaces #0 with `e`. *) ===================================== src/unification.ml ===================================== @@ -132,8 +132,8 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with * aka * ?a = ?b[0 => 0 · ↑1] *) -let common_subset ctx (s1 : lsubst) (s2 : lsubst) = - let rec loop (s1 : lsubst) (s2 : lsubst) o1 o2 o = +let common_subset ctx (s1 : subst) (s2 : subst) = + let rec loop (s1 : subst) (s2 : subst) o1 o2 o = match (S.subst_subst' s1, S.subst_subst' s2) with | (Cons (le1, s1', o1'), Cons (le2, s2', o2')) -> let o1 = o1 + o1' in @@ -166,7 +166,7 @@ let common_subset ctx (s1 : lsubst) (s2 : lsubst) = (* Return the number of vars difference between input and output context. * * Could be returned directly by `common_subset`, but it's pretty easy to * compute it here instead. *) -let rec s_offset (s : lsubst) = match S.subst_subst' s with +let rec s_offset (s : subst) = match S.subst_subst' s with | Identity o -> o | Cons (_, s', o) -> o - 1 + s_offset s' ===================================== src/util.ml ===================================== @@ -117,13 +117,15 @@ let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option = | None -> None | Some x -> Some (fn x) -let combine_hash e1 e2 = (e1 * 31) lxor e2 +let combine_hash (e1: int) (e2: int) : int = (e1 * 31) lxor e2 -let get_stats stats = +let get_stats stats lshrct sshrct = let (tl, ne, sumb, smallb, medianb, bigb) = stats in Printf.printf "\n\ttable length: %i\n number of entries: %i\n sum of bucket lengths: %i\n smallest bucket length: %i\n median bucket length: %i\n - biggest bucket length: %i\n" tl ne sumb smallb medianb bigb + biggest bucket length: %i\n + lexp sharing counter: %i\n + subst sharing counter: %i\n" tl ne sumb smallb medianb bigb lshrct sshrct; View it on GitLab: https://gitlab.com/monnier/typer/-/commit/501776544b12bdef314fbe4d03fbf81ec… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/501776544b12bdef314fbe4d03fbf81ec… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][ja-barszcz] [WIP] Add a set of typeclasses to the elab context
by Jean-Alexandre Barszcz 23 Jui '20

23 Jui '20

Jean-Alexandre Barszcz pushed to branch ja-barszcz at Stefan / Typer Commits: 2a7b7e3f by Jean-Alexandre Barszcz at 2020-06-23T12:39:25-04:00 [WIP] Add a set of typeclasses to the elab context - - - - - 4 changed files: - samples/decidable.typer - src/debruijn.ml - src/elab.ml - src/instances.ml Changes: ===================================== samples/decidable.typer ===================================== @@ -11,6 +11,8 @@ exfalso f = ##case_ f; yes = datacons Decidable true; no = datacons Decidable false; +typeclass Decidable; + Eq_trans : (x : ?t) => (y : ?t) => (a : ?t) -> (ax : Eq a x) => (ay : Eq a y) => Eq x y; ===================================== src/debruijn.ml ===================================== @@ -112,26 +112,29 @@ type meta_scope * lctx_length (* Length of ctx when the scope is added. *) * (meta_id SMap.t ref) (* Metavars already known in this scope. *) +type typeclass_ctx + = (ltype * lctx_length) list (* FIXME make it a set of lexps ? *) + (* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) type elab_context - = Grammar.grammar * senv_type * lexp_context * meta_scope + = Grammar.grammar * senv_type * lexp_context * meta_scope * typeclass_ctx let get_size (ctx : elab_context) - = let (_, (n, _), lctx, _) = ctx in + = let (_, (n, _), lctx, _, _) = ctx in assert (n = M.length lctx); n let ectx_to_grm (ectx : elab_context) : Grammar.grammar = - let (grm,_, _, _) = ectx in grm + let (grm,_, _, _, _) = ectx in grm (* Extract the lexp context from the context used during elaboration. *) let ectx_to_lctx (ectx : elab_context) : lexp_context = - let (_,_, lctx, _) = ectx in lctx + let (_,_, lctx, _, _) = ectx in lctx -let ectx_to_scope_level ((_, _, _, (sl, _, _)) : elab_context) : scope_level +let ectx_to_scope_level ((_, _, _, (sl, _, _), _) : elab_context) : scope_level = sl -let ectx_local_scope_size ((_, (n, _), _, (_, slen, _)) as ectx) : int +let ectx_local_scope_size ((_, (n, _), _, (_, slen, _), _) as ectx) : int = get_size ectx - slen (* Public methods: DO USE @@ -142,7 +145,7 @@ let empty_lctx = M.nil let empty_elab_context : elab_context = (Grammar.default_grammar, empty_senv, empty_lctx, - (0, 0, ref SMap.empty)) + (0, 0, ref SMap.empty), []) (* senv_lookup caller were using Not_found exception *) exception Senv_Lookup_Fail of (string list) @@ -150,7 +153,7 @@ let senv_lookup_fail relateds = raise (Senv_Lookup_Fail relateds) (* Return its current DeBruijn index. *) let senv_lookup (name: string) (ctx: elab_context): int = - let (_, (n, map), _, _) = ctx in + let (_, (n, map), _, _, _) = ctx in try n - (SMap.find name map) - 1 with Not_found -> let get_related_names (n : db_ridx) name map = @@ -189,11 +192,11 @@ let lctx_extend (ctx : lexp_context) (def: vname) (v: varbind) (t: lexp) = let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = let (loc, oname) = def in - let (grm, (n, map), env, sl) = ctx in + let (grm, (n, map), env, sl, tcctx) = ctx in let nmap = match oname with None -> map | Some name -> SMap.add name n map in (grm, (n + 1, nmap), lexp_ctx_cons env def v t, - sl) + sl, tcctx) let ectx_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t @@ -207,28 +210,33 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = ctx let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = - let (grm, (n, senv), lctx, sl) = ctx in + let (grm, (n, senv), lctx, sl, tcctx) = ctx in let senv', _ = List.fold_left (fun (senv, i) ((_, oname), _, _) -> (match oname with None -> senv | Some name -> SMap.add name i senv), i + 1) (senv, n) defs in - (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl) + (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl, tcctx) let ectx_new_scope (ectx : elab_context) : elab_context = - let (grm, senv, lctx, (scope, _, rmmap)) = ectx in - (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap))) + let (grm, senv, lctx, (scope, _, rmmap), tcctx) = ectx in + (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap)), tcctx) let ectx_get_scope (ectx : elab_context) : meta_scope = - let (_, _, _, sl) = ectx in sl + let (_, _, _, sl, _) = ectx in sl let ectx_get_grammar (ectx : elab_context) : Grammar.grammar = - let (grm, _, _, _) = ectx in grm + let (grm, _, _, _, _) = ectx in grm let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx +let env_add_typeclass (ectx : elab_context) (t : ltype) : elab_context = + let (grm, senv, lctx, sl, tcctx) = ectx in + let ntcctx = ((t, get_size ectx) :: tcctx) in + (grm, senv, lctx, sl, ntcctx) + (* Print context *) let print_lexp_ctx_n (ctx : lexp_context) start = let n = (M.length ctx) - 1 in ===================================== src/elab.ml ===================================== @@ -288,8 +288,8 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context = | Symbol (_, "") -> None | Integer (_, n) -> Some n | _ -> sexp_error (sexp_location s) "Expecting an integer or ()"; None in - let (grm, a, b, c) = ctx in - (SMap.add name (level l, level r) grm, a, b, c) + let (grm, a, b, c, d) = ctx in + (SMap.add name (level l, level r) grm, a, b, c, d) | [o; _; _] -> sexp_error (sexp_location o) "Expecting a string"; ctx | _ @@ -633,7 +633,7 @@ and get_implicit_arg ctx loc oname t = and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp_whnf t (ectx_to_lctx ctx) with - | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) when Inst.is_typeclass t1 ctx + | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) when Inst.is_typeclass ctx t1 -> let arg = newInstanceMetavar ctx (lexp_location e, v) t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) @@ -662,7 +662,7 @@ and search_instance (ctx : elab_context) (loc : location) (t : ltype) : lexp opt let t' = mkSusp t' (S.shift (i + 1)) in let (e, t') = instantiate_implicit var t' ctx in (* All candidates should have a type that is a typeclass *) - if not (Inst.is_typeclass t' ctx) then None else + if not (Inst.is_typeclass ctx t') then None else match Inst.check_typeclass_match t t' lctx sl with | (Impossible | Possible) -> None (* | Possible -> None *) @@ -706,8 +706,7 @@ and sdform_typeclass (ctx : elab_context) loc sargs _ot : elab_context = match sargs with | [se] -> let t = infer_type se ctx (loc, None) in - (* TODO add t as a typeclass in the context ? *) - ctx + Inst.add_typeclass ctx t | _ -> sexp_error loc "typeclass expects 1 argument"; ctx @@ -1191,9 +1190,9 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) (* FIXME: Generalize when/where possible, so things like `map` can be defined without type annotations! *) (* Preserve the new operators added to nctx. *) - let ectx = let (_, a, b, c) = ectx in - let (grm, _, _, _) = nctx in - (grm, a, b, c) in + let ectx = let (_, a, b, c, _) = ectx in + let (grm, _, _, _, tcctx) = nctx in + (grm, a, b, c, tcctx) in let (declmap, nctx) = List.fold_right (fun ((l, vname), pexp) (map, nctx) -> @@ -1203,10 +1202,10 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) | (v', ForwardRef, t) -> let adjusted_t = push_susp t (S.shift (i + 1)) in let e = check pexp adjusted_t nctx in - let (grm, ec, lc, sl) = nctx in + let (grm, ec, lc, sl, tcctx) = nctx in let d = (v', LetDef (i + 1, e), t) in (IMap.add i ((l, Some vname), e, t) map, - (grm, ec, Myers.set_nth i d lc, sl)) + (grm, ec, Myers.set_nth i d lc, sl, tcctx)) | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in ===================================== src/instances.ml ===================================== @@ -2,6 +2,7 @@ module Unif = Unification module U = Util module DB = Debruijn module L = Lexp +module S = Subst module OL = Opslexp (* FIXME Is it possible to have multiple references to the same @@ -12,11 +13,41 @@ let instance_metavar_lookup (id : L.meta_id) : (DB.elab_context * U.location) op let add_instance_metavar (id : L.meta_id) (ctx : DB.elab_context) (loc : U.location) : unit = instance_metavar_table := U.IMap.add id (ctx, loc) !instance_metavar_table -let is_typeclass (t : L.ltype) (ctx : DB.elab_context) = - (* TODO *) - match OL.lexp_whnf t (DB.ectx_to_lctx ctx) with - | L.Call (L.Var ((_,Some s),_), _) when s = "Decidable" -> true - | _ -> false +let env_is_typeclass (ectx : DB.elab_context) (t : L.ltype) : bool = + let (_, _, _, _, tcctx) = ectx in + let cl = DB.get_size ectx in + List.exists (fun (t', cl') -> + let i = cl - cl' in + let t' = L.mkSusp t' (S.shift i) in + OL.conv_p (DB.ectx_to_lctx ectx) t t' + (*(Unif.unify ~checking:(max_int (* FIXME *)) t t' (DB.ectx_to_lctx ectx)) = []*) + ) tcctx + + +let get_ind (lctx : DB.lexp_context) (t : L.ltype) : L.ltype option = + match OL.lexp_whnf t lctx with + | L.Call (typecons, _) -> + (match OL.lexp_whnf typecons lctx with + | L.Inductive _ as ind -> Some ind + | _ -> None + ) + | L.Inductive _ as ind -> Some ind + | _ -> None + + +let is_typeclass (ctx : DB.elab_context) (t : L.ltype) = + let lctx = DB.ectx_to_lctx ctx in + match get_ind lctx t with + | Some ind -> env_is_typeclass ctx ind + | None -> false + +let add_typeclass (ctx : DB.elab_context) (t : L.ltype) : DB.elab_context = + let lctx = DB.ectx_to_lctx ctx in + match get_ind lctx t with + | Some ind -> DB.env_add_typeclass ctx ind + | None -> Log.log_error ("Failed to add type class to context " + ^ " because it is not an inductive : `" + ^ (L.lexp_string t) ^ "`"); ctx type match_res = Impossible | Possible | Match View it on GitLab: https://gitlab.com/monnier/typer/-/commit/2a7b7e3f99aaa3880c58e70a49b0f5195… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/2a7b7e3f99aaa3880c58e70a49b0f5195… You're receiving this email because of your account on gitlab.com.

2 1

[Git][monnier/typer][ja-barszcz] WIP WIP getting there
by Jean-Alexandre Barszcz 16 Jui '20

16 Jui '20

Jean-Alexandre Barszcz pushed to branch ja-barszcz at Stefan / Typer Commits: c6bfd8b5 by Jean-Alexandre Barszcz at 2020-06-16T13:34:41-04:00 WIP WIP getting there - - - - - 5 changed files: - samples/decidable.typer - src/elab.ml - + src/instances.ml - src/opslexp.ml - src/unification.ml Changes: ===================================== samples/decidable.typer ===================================== @@ -138,7 +138,18 @@ decideLT = test1 : Bool; test1 = - let inst = decideEven (a := (succ zero)) in case (instance () : Decidable (even (succ zero))) | yes => true | no => false; % Why wrong index in eval + +if_then_else_ + = macro (lambda args -> + let e1 = List_nth 0 args Sexp_error; + e2 = List_nth 1 args Sexp_error; + e3 = List_nth 2 args Sexp_error; + in IO_return (quote (case (instance () : (Decidable (uquote e1))) + | yes => uquote e2 + | no => uquote e3))); + +test2 : Bool; +test2 = if (even (succ zero)) then false else true; \ No newline at end of file ===================================== src/elab.ml ===================================== @@ -57,12 +57,11 @@ open Grammar module BI = Builtin module Unif = Unification +module Inst = Instances module OL = Opslexp module EL = Elexp -type match_res = Impossible | Possible | Match - (* dummies *) let dloc = dummy_location @@ -259,6 +258,13 @@ let newMetavar (ctx : lexp_context) sl name t = let meta = Unif.create_metavar ctx sl t in mkMetavar (meta, S.identity, name) +let newInstanceMetavar (ctx : elab_context) name t = + let lctx = ectx_to_lctx ctx in + let sl = ectx_to_scope_level ctx in + let meta = Unif.create_metavar lctx sl t in + Inst.add_instance_metavar meta ctx (fst name); + mkMetavar (meta, S.identity, name) + let newMetalevel (ctx : lexp_context) sl loc = newMetavar ctx sl (loc, Some "ℓ") type_level @@ -623,20 +629,12 @@ and get_implicit_arg ctx loc oname t = | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) (loc, oname) t -and is_typeclass t lctx = true (* TODO *) - (* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp_whnf t (ectx_to_lctx ctx) with - | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) when is_typeclass t1 ctx - -> let lctx = ectx_to_lctx ctx in - let sl = ectx_to_scope_level ctx in - (* FIXME Should it be a special instance metavar? Or do we - know from its type? If we know from the type then - instantiation is the same for both cases (is_typeclass or - not) *) - let arg = newMetavar lctx sl (lexp_location e, v) t1 in + | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) when Inst.is_typeclass t1 ctx + -> let arg = newInstanceMetavar ctx (lexp_location e, v) t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in @@ -653,29 +651,22 @@ and myers_filter_map_index (f : int -> 'a -> 'b option) (m : 'a M.myers) | None -> (i - 1, l')) m (M.length m - 1, M.nil)) -and check_typeclass_match t1 t2 lctx sl = - match Unif.unify ~checking:sl t1 t2 lctx with - | [] -> Match - | constraints when List.exists (function | (Unif.CKimpossible,_,_,_) -> true - | _ -> false) - constraints -> Impossible - | _ -> Possible - -and search_instance (ctx : elab_context) (loc : location) (t : ltype) : lexp * sform_type = +and search_instance (ctx : elab_context) (loc : location) (t : ltype) : lexp option = Log.log_debug ~loc ("Searching for t = `" ^ (lexp_string t) ^ "`"); + let ctx = ectx_new_scope ctx in let lctx = (ectx_to_lctx ctx) in - let sl = (ectx_to_scope_level ctx) in (* FIXME should we create a new scope ? *) + let sl = (ectx_to_scope_level ctx) in let env_elem_match (i : int) (elem : DB.env_elem) : (int * DB.env_elem * lexp * ltype) option = - let (vname, _, t') = elem in - let var = mkVar (vname, i) in (* Change the location maybe *) + let ((_, namopt), _, t') = elem in + let var = mkVar ((loc,namopt), i) in let t' = mkSusp t' (S.shift (i + 1)) in let (e, t') = instantiate_implicit var t' ctx in (* All candidates should have a type that is a typeclass *) - if not (is_typeclass t' ctx) then None else - match check_typeclass_match t t' lctx sl with - | Impossible -> None + if not (Inst.is_typeclass t' ctx) then None else + match Inst.check_typeclass_match t t' lctx sl with + | (Impossible | Possible) -> None (* | Possible -> None *) - | (Possible | Match) -> Some (i, elem, e, t') in + | (Match) -> Some (i, elem, e, t') in let candidates = myers_filter_map_index env_elem_match lctx in Log.log_debug ("Candidates for instance of type `" ^ lexp_string t ^ "`:") @@ -685,31 +676,40 @@ and search_instance (ctx : elab_context) (loc : location) (t : ltype) : lexp * s lalign_print_string (match so with | Some s -> s | None -> "<none>") 10; print_endline (lexp_string t')) candidates); match M.safe_car candidates with - | None -> - (error ~loc - ("No instance found in context for type `" ^ lexp_string t ^ "`"); - sform_dummy_ret ctx loc) + | None -> None | Some (i, (vname, _, t'),e,t) -> let t' = mkSusp t' (S.shift (i + 1)) in Log.log_debug ~loc ("Found candidate at index " ^ (string_of_int i) ^ ": `" ^ (lexp_string (Var (vname, i))) ^ " : " ^ (lexp_string t') ^ "`"); - (e, Inferred t) - -and resolve_instances ctx e = - (* TODO + Some e + +and resolve_instances e = + let (_, (fv_map, _)) = OL.fv e in + U.IMap.iter (fun i (sl, t, cl, vn) -> + match Inst.instance_metavar_lookup i with + | Some (ctx, loc) -> + (match search_instance ctx loc t with + | Some e -> Unif.associate i e; resolve_instances e + | None -> + error ~loc ("No instance found for type `" ^ (lexp_string t) ^ "`") + ) + | None -> () + ) fv_map - For all instance metavars, we have to do the instance search in - their context. Maybe the elab_context is not necessary, only the - right lctx and scope level. - - Can we get a metavar's lctx from the current ctx and the - metavar's substitution? If yes then we can use OL.fv, otherwise - structural recursion on lexps MEH *) - failwith "TODO" and resolve_instances_and_generalize ctx e = - generalize ctx (resolve_instances ctx e) + resolve_instances e; + generalize ctx e + +and sdform_typeclass (ctx : elab_context) loc sargs _ot : elab_context = + match sargs with + | [se] -> + let t = infer_type se ctx (loc, None) in + (* TODO add t as a typeclass in the context ? *) + ctx + | _ + -> sexp_error loc "typeclass expects 1 argument"; ctx and infer_type pexp ectx var = (* We could also use lexp_check with an argument of the form @@ -1077,7 +1077,7 @@ and lexp_parse_inductive ctors ctx = (fun (ak, n, t) aa -> Arrow (ak, n, t, dummy_location, aa)) acc impossible in - let g = generalize nctx altacc in + let g = resolve_instances_and_generalize nctx altacc in let altacc' = g (fun _ne vname t l e -> Arrow (Aerasable, vname, t, l, e)) altacc in @@ -1242,7 +1242,7 @@ and infer_and_generalize_type (ctx : elab_context) se name = | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, t1, l, strip_rettype t2) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in - let g = generalize nctx (strip_rettype t) in + let g = resolve_instances_and_generalize nctx (strip_rettype t) in g (fun _ne name t l e -> mkArrow (Aerasable, name, t, l, e)) t @@ -1250,7 +1250,7 @@ and infer_and_generalize_type (ctx : elab_context) se name = and infer_and_generalize_def (ctx : elab_context) se = let nctx = ectx_new_scope ctx in let (e,t) = infer se nctx in - let g = generalize nctx e in + let g = resolve_instances_and_generalize nctx e in let e' = g (fun ne vname t l e -> mkLambda ((if ne then Aimplicit else Aerasable), vname, t, e)) @@ -1370,6 +1370,10 @@ and lexp_decls_1 -> lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None) pending_decls pending_defs + | Node (Symbol (l, "typeclass"), args) :: sdecls + -> lexp_decls_1 sdecls ectx (sdform_typeclass nctx l args None) + pending_decls pending_defs + | Node (Symbol ((l, _) as v), sargs) :: sdecls -> (* expand macro and get the generated declarations *) let sdecl' = lexp_decls_macro v sargs nctx in @@ -1904,17 +1908,19 @@ let sform_load usr_elctx loc sargs ot = (** Draft of a special form "instance" that gets refers to a variable - of the requested type in the context. Ultimately, this search - should be automatically triggered at the call sites for a new kind - of argument (instance arguments) similarly to implicit arguments. + of the requested type in the context. **) let sform_instance ctx loc sargs ot = - (* TODO replace with instance metavars *) match sargs, ot with - | ([se; _], _) -> search_instance ctx loc (infer_type se ctx (loc, None)) - | ([_], Some t) -> search_instance ctx loc t (* Dummy param to trigger the special form *) + | ([se; _], _) -> (* Dummy param to trigger the special form *) + let t = infer_type se ctx (loc, None) in + let mv = newInstanceMetavar ctx (loc, Some "instance") t in + (mv, Inferred t) + | ([_], Some t) -> (* Dummy param to trigger the special form *) + let mv = newInstanceMetavar ctx (loc, Some "instance") t in + (mv, Checked) | _ -> (sexp_error loc "##instance expects a type argument if not checked"; - sform_dummy_ret ctx loc) + sform_dummy_ret ctx loc) (* Register special forms. *) let register_special_forms () = ===================================== src/instances.ml ===================================== @@ -0,0 +1,30 @@ +module Unif = Unification +module U = Util +module DB = Debruijn +module L = Lexp +module OL = Opslexp + +(* FIXME Is it possible to have multiple references to the same + instance metavar? It would break the following code *) +let instance_metavar_table = ref (U.IMap.empty : (DB.elab_context * U.location) U.IMap.t) +let instance_metavar_lookup (id : L.meta_id) : (DB.elab_context * U.location) option + = U.IMap.find_opt id (!instance_metavar_table) +let add_instance_metavar (id : L.meta_id) (ctx : DB.elab_context) (loc : U.location) : unit + = instance_metavar_table := U.IMap.add id (ctx, loc) !instance_metavar_table + +let is_typeclass (t : L.ltype) (ctx : DB.elab_context) = + (* TODO *) + match OL.lexp_whnf t (DB.ectx_to_lctx ctx) with + | L.Call (L.Var ((_,Some s),_), _) when s = "Decidable" -> true + | _ -> false + +type match_res = Impossible | Possible | Match + +let check_typeclass_match t1 t2 lctx sl = + match Unif.unify ~checking:sl t1 t2 lctx with + | [] -> Match + | constraints when List.exists (function | (Unif.CKimpossible,_,_,_) -> true + | _ -> false) + constraints -> Impossible + | _ -> Possible + ===================================== src/opslexp.ml ===================================== @@ -723,6 +723,7 @@ module LMap = Hashtbl.Make (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end) let fv_memo = LMap.create 1000 +let fv_flush () = LMap.clear fv_memo let fv_empty = (DB.set_empty, mv_set_empty) let fv_union (fv1, mv1) (fv2, mv2) ===================================== src/unification.ml ===================================== @@ -55,8 +55,9 @@ type constraints = (constraint_kind * DB.lexp_context * lexp * lexp) list type return_type = constraints (** Alias for VMap.add*) -let associate (id: meta_id) (lxp: lexp) (subst: meta_subst) : meta_subst - = U.IMap.add id (MVal lxp) subst +let associate (id: meta_id) (lxp: lexp) : unit + = metavar_table := U.IMap.add id (MVal lxp) (!metavar_table); + OL.fv_flush () let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | MVal _ -> Log.internal_error @@ -288,7 +289,7 @@ and unify_metavar (checking : scope_level option) ctx idx s1 (lxp1: lexp) (lxp2: -> match checking with | Some l when l >= sl -> [(CKassoc, ctx, lxp1, lxp2)] | _ -> ( - metavar_table := associate idx lxp' (!metavar_table); + associate idx lxp'; match unify t (OL.get_type ctx lxp) ctx with | [] as r -> r (* FIXME: Let's ignore the error for now. *) @@ -352,7 +353,7 @@ and unify_metavar (checking : scope_level option) ctx idx s1 (lxp1: lexp) (lxp2: * ^ "\n =\n " * ^ subst_string (scompose s s2) * ^ "\n"); *) - metavar_table := associate idx lexp (!metavar_table); + associate idx lexp; assert (OL.conv_p ctx lxp1 lxp2); [] else View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c6bfd8b50c25b02b5d05e0843ffd4f753… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c6bfd8b50c25b02b5d05e0843ffd4f753… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][alice] hash consing of substitutions
by Alice de Berny 16 Jui '20

16 Jui '20

Alice de Berny pushed to branch alice at Stefan / Typer Commits: ab6585a3 by irradiee at 2020-06-16T05:54:24-04:00 hash consing of substitutions - - - - - 15 changed files: - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - + src/lexp_type.ml - src/opslexp.ml - src/sexp.ml - src/subst.ml - src/unification.ml - src/util.ml Changes: ===================================== src/REPL.ml ===================================== @@ -44,6 +44,7 @@ open Prelexer open Lexer open Sexp open Pexp +open Lexp_type open Lexp open Eval @@ -231,7 +232,8 @@ let rec repl i clxp rctx = | "%help" | "%h" -> (print_string help_msg; repl clxp rctx) | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx) - | "%collisions" | "%cl" -> (get_stats hc_table) + | "%lcollisions" | "%cl" -> (get_stats (WHC.stats hc_table)) + | "%scollisions" | "%scl" -> (get_stats (Subst.WHCSB.stats Subst.hcsb_table)) (* command with arguments *) | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> ( ===================================== src/builtin.ml ===================================== @@ -57,7 +57,7 @@ open Util open Sexp (* Integer/Float *) open Pexp (* arg_kind *) -module L = Lexp +open Lexp_type module OL = Opslexp open Lexp ===================================== src/debruijn.ml ===================================== @@ -35,8 +35,10 @@ module Str = Str open Util + +open Lexp_type open Lexp -module L = Lexp + module M = Myers open Fmt @@ -300,7 +302,7 @@ let print_lexp_ctx_n (ctx : lexp_context) start = (* Only print user defined variables *) let print_lexp_ctx (ctx : lexp_context) = - print_lexp_ctx_n ctx !L.builtin_size + print_lexp_ctx_n ctx !builtin_size (* Dump the whole context *) let dump_lexp_ctx (ctx : lexp_context) = ===================================== src/elab.ml ===================================== @@ -45,6 +45,7 @@ open Lexer open Sexp open Pexp +open Lexp_type open Lexp open Env @@ -394,23 +395,23 @@ let rec meta_to_var ids (e : lexp) = *) (* `o` is the binding offset until the root. *) - let rec adjust_subst o s = match s with - | S.Identity n + let rec adjust_subst o (s : lsubst) = match S.subst_subst' s with + | Identity n -> let o' = o - n in if o' < 0 then (* This metavar's original context is outside of our scope * (case (B) above), so don't let it refer to the new vars. *) - S.Identity (n + count) + S.hcsb (Identity (n + count)) else - Identity n - | S.Cons (e, s', n) + S.hcsb (Identity n) + | Cons (e, s', n) -> let o' = o - n in if o' < 0 then (* This metavar's original context is outside of our scope * (case (B) above), so don't let it refer to the new vars. *) - S.Cons (e, s', n + count) + S.hcsb (Cons (e, s', n + count)) else - S.Cons (loop o' e, adjust_subst o' s', n) + S.hcsb (Cons (loop o' e, adjust_subst o' s', n)) (* `o` is the binding depth at which we are relative to the "root" * of the expression (i.e. where the new vars will be inserted). *) ===================================== src/elexp.ml ===================================== @@ -35,6 +35,7 @@ open Sexp (* Sexp type *) open Pexp (* Anormal *) module U = Util +module LT = Lexp_type module L = Lexp type vname = U.vname @@ -77,7 +78,7 @@ type elexp = (* A Type expression. There's no useful operation we can apply to it, * but they can appear in the code. *) - | Type of L.lexp + | Type of LT.lexp let rec elexp_location e = match e with ===================================== src/env.ml ===================================== @@ -36,6 +36,7 @@ open Sexp open Elexp module M = Myers +module LT = Lexp_type module L = Lexp module BI = Z (* Was Big_int *) module DB = Debruijn @@ -58,7 +59,7 @@ type value_type = | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vundefined - | Vtype of L.lexp (* The lexp value can't be trusted. *) + | Vtype of LT.lexp (* The lexp value can't be trusted. *) | Vin of in_channel | Vout of out_channel | Vcommand of (unit -> value_type) @@ -241,7 +242,7 @@ let print_rte_ctx_n (ctx: runtime_env) start = (* Only print user defined variables *) let print_rte_ctx ctx = - print_rte_ctx_n ctx (!L.builtin_size) + print_rte_ctx_n ctx (!LT.builtin_size) (* Dump the whole context *) let dump_rte_ctx ctx = ===================================== src/eval.ml ===================================== @@ -35,6 +35,7 @@ open Fmt open Sexp open Pexp (* Arg_kind *) +open Lexp_type open Lexp (* Varbind *) open Elexp ===================================== src/inverse_subst.ml ===================================== @@ -39,6 +39,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) * So either left or right inverse can be used! *) +open Lexp_type open Lexp open Util module S = Subst @@ -56,8 +57,8 @@ type substIR = ((int * int) list * int * int) (** Transform a substitution to a more linear substitution * makes the inversion easier * Example of result : ((new_idx, old_position)::..., shift)*) -let transfo (s: Lexp.subst) : substIR option = - let rec transfo (s: Lexp.subst) (off_acc: int) (idx: int) (imp_cnt : int) +let transfo (s: lsubst) : substIR option = + let rec transfo (s: lsubst) (off_acc: int) (idx: int) (imp_cnt : int) : substIR option = let indexOf (v: lexp): int = (* Helper : return the index of a variabble *) let v' = lexp_lexp' v in @@ -68,8 +69,8 @@ let transfo (s: Lexp.subst) : substIR option = let shiftVar (var: lexp) (offset: int): int = indexOf (mkSusp var (S.shift offset)) (* Helper : shift the index of a var *) in - match s with - | S.Cons ((Var _ as v, h), s, o) -> + match S.subst_subst' s with + | Cons ((Var _ as v, h), s, o) -> let off_acc = off_acc + o in (match transfo s off_acc (idx + 1) imp_cnt with | Some (tail, off, imp) @@ -77,15 +78,15 @@ let transfo (s: Lexp.subst) : substIR option = in if newVar >= off then None (* Error *) else Some (((shiftVar (v, h) off_acc), idx)::tail, off, imp) | None -> None) - | S.Cons ((Imm (Sexp.Symbol (_, "")), _), s, o) + | Cons ((Imm (Sexp.Symbol (_, "")), _), s, o) -> transfo s (o + off_acc) (idx + 1) (imp_cnt + 1) - | S.Identity o -> Some ([], (o + off_acc), imp_cnt) + | Identity o -> Some ([], (o + off_acc), imp_cnt) | _ -> None (* Error *) in transfo s 0 0 0 (* Inverse *) -(** Returns the number of element in a sequence of S.Cons +(** Returns the number of element in a sequence of Cons *) let rec sizeOf (s: (int * int) list): int = List.length s @@ -94,7 +95,7 @@ let rec sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - Lexp.mkVar ((U.dummy_location, None), idx) + mkVar ((U.dummy_location, None), idx) (** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -105,18 +106,18 @@ let mkVar (idx: int) : lexp = @param size size of the list to return @param acc recursion accumulator *) -let fill (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = - let rec genDummyVar (beg_: int) (end_: int) (l: Lexp.subst): Lexp.subst = (* Create the filler variables *) +let fill (l: (int * int) list) (nbVar: int) (shift: int): lsubst option = + let rec genDummyVar (beg_: int) (end_: int) (l: lsubst): lsubst = (* Create the filler variables *) if beg_ < end_ then S.cons impossible (genDummyVar (beg_ + 1) end_ l) else l in - let fill_before (l: (int * int) list) (s: Lexp.subst) (nbVar: int): Lexp.subst option = (* Fill if the first var is not 0 *) + let fill_before (l: (int * int) list) (s: lsubst) (nbVar: int): lsubst option = (* Fill if the first var is not 0 *) match l with | [] -> Some (genDummyVar 0 nbVar s) | (i1, v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) | _ -> Some s - in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = (* Fill gaps *) + in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): lsubst option = (* Fill gaps *) match l with | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None @@ -143,11 +144,11 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = | None -> None | Some s -> fill_before l s nbVar -let is_identity s = - let rec is_identity s acc = - match s with - | S.Cons((Var(_, idx), _), s1, 0) when idx = acc -> is_identity s1 (acc + 1) - | S.Identity o -> acc = o +let is_identity (s : lsubst) = + let rec is_identity (s : lsubst) acc = + match S.subst_subst' s with + | Cons((Var(_, idx), _), s1, 0) when idx = acc -> is_identity s1 (acc + 1) + | Identity o -> acc = o | _ -> S.identity_p s in is_identity s 0 @@ -155,7 +156,7 @@ let is_identity s = <code>s:S.subst, l:lexp, s':S.subst</code> where <code>l[s][s'] = l</code> and <code> inverse s = s' </code> *) -let inverse (s: Lexp.subst) : Lexp.subst option = +let inverse (s: lsubst) : lsubst option = let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) in match transfo s with | None -> None @@ -181,9 +182,9 @@ let inverse (s: Lexp.subst) : Lexp.subst option = (* Returns false if the application of the inverse substitution is not * possible. This happens when the substitution replaces some variables * with non-variables, in which case the "inverse" is ambiguous. *) -let rec invertible (s: subst) : bool = match s with - | S.Identity _ -> true - | S.Cons (e, s, _) +let rec invertible (s: lsubst) : bool = match S.subst_subst' s with + | Identity _ -> true + | Cons (e, s, _) -> (let e' = lexp_lexp' e in match e' with Var _ -> true | _ -> e = impossible) && invertible s @@ -192,16 +193,16 @@ exception Not_invertible exception Ambiguous (* Lookup variable i in s⁻¹ *) -let rec lookup_inv_subst (i : db_index) (s : subst) : db_index - = match s with - | (S.Identity o | S.Cons (_, _, o)) when i < o -> raise Not_invertible - | S.Identity o -> i - o - | S.Cons ((Var (_, i'), _), s, o) when i' = i - o +let rec lookup_inv_subst (i : db_index) (s : lsubst) : db_index + = match S.subst_subst' s with + | (Identity o | Cons (_, _, o)) when i < o -> raise Not_invertible + | Identity o -> i - o + | Cons ((Var (_, i'), _), s, o) when i' = i - o -> (try let i'' = lookup_inv_subst i' s in assert (i'' != 0); raise Ambiguous with Not_invertible -> 0) - | S.Cons (e, s, o) + | Cons (e, s, o) -> assert (let e' = lexp_lexp' e in match e' with Var _ -> true | _ -> e = impossible); @@ -239,12 +240,12 @@ let shift_inv_subst n s * One way to do it is to compute s⁻¹ and then pass it to `compose`. * But we can try and do it more directly. *) -let rec compose_inv_subst (s' : subst) (s : subst) = match s' with - | S.Cons (e, s', o) -> +let rec compose_inv_subst (s' : lsubst) (s : lsubst) = match S.subst_subst' s' with + | Cons (e, s', o) -> let s = shift_inv_subst o s in (* FIXME: Why don't we ever return a Shift? *) S.cons (apply_inv_subst e s) (compose_inv_subst s' s) - | S.Identity o -> (match inverse (shift_inv_subst o s) with + | Identity o -> (match inverse (shift_inv_subst o s) with | Some s -> s (* FIXME: could also be Ambiguous, depending on `s`. *) | None -> raise Not_invertible) @@ -253,7 +254,7 @@ let rec compose_inv_subst (s' : subst) (s : subst) = match s' with * The function presumes that `invertible s` was true. * This can be used like mkSusp/push_susp, but it's not lazy. * This is because it can signal errors Not_invertible or Ambiguous. *) -and apply_inv_subst (e : lexp) (s : subst) : lexp = +and apply_inv_subst (e : lexp) (s : lsubst) : lexp = let e' = lexp_lexp' e in match e' with | Imm _ -> e ===================================== src/lexp.ml ===================================== @@ -20,161 +20,25 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>. *) -module U = Util -module L = List -module SMap = U.SMap +(* open Unify *) +module S = Subst + open Fmt open Sexp open Pexp +open Lexp_type + open Myers open Grammar -(* open Unify *) -module S = Subst - -type vname = U.vname -type vref = U.vref -type meta_id = int (* Identifier of a meta variable. *) - -type label = symbol - -type attribute_key = (int * string) (* rev_dbi * Var name *) -module AttributeMap = Map.Make (struct type t = attribute_key let compare = compare end) - -(*************** Elaboration to Lexp *********************) - -(* The scoping of `Let` is tricky: - * - * Since it's a recursive let, the definition part of each binding is - * valid in the "final" scope which includes all the new bindings. - * - * But the type of each binding is not defined in that same scope. Instead - * it's defined in the scope of all the previous bindings. - * - * For exemple the type of the second binding of such a Let is defined in - * the scope of the surrounded context extended with the first binding. - * And the type of the 3rd binding is defined in the scope of the - * surrounded context extended with the first and the second bindings. *) - -type ltype = lexp -and subst = subst' * int - and subst' = lexp S.subst - and lexp = lexp' * int - and lexp' = - | Imm of sexp (* Used for strings, ... *) - | SortLevel of sort_level - | Sort of U.location * sort - | Builtin of symbol * ltype * lexp AttributeMap.t option - | Var of vref - | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) - (* This "Let" allows recursion. *) - | Let of U.location * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname * ltype * U.location * ltype - | Lambda of arg_kind * vname * ltype * lexp - | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of U.location * label - * ((arg_kind * vname * ltype) list) (* formal Args *) - * ((arg_kind * vname * ltype) list) SMap.t - | Cons of lexp * symbol (* = Type info * ctor_name *) - | Case of U.location * lexp - * ltype (* The type of the return value of all branches *) - * (U.location * (arg_kind * vname) list * lexp) SMap.t - * (vname * lexp) option (* Default. *) - (* The `subst` will be applied to the the metavar's value when it - * gets instantiated. *) - | Metavar of meta_id * subst * vname - (* (\* For logical metavars, there's no substitution. *\) - * | Metavar of (U.location * string) * metakind * metavar ref - * and metavar = - * (\* An uninstantiated var, along with a venv (stipulating over which vars - * * it should be closed), and its type. - * * If its type is not given, it implies its type should be a sort. *\) - * | MetaUnset of (lexp option * lexp) VMap.t * ltype option * scope_level - * | MetaSet of lexp - * and metakind = - * | MetaGraft of subst - * (\* Forward reference or Free var: Not known yet, but not instantiable by - * * unification. *\) - * | MetaFoF - * and subst = lexp VMap.t *) - (* - * The PTS I'm imagining looks like: - * - * S = { TypeLevel, TypeOmega, Type ℓ } - * A = { Level : TypeLevel, Z : Level, S : Level → Level, - * Type : (ℓ : Level) → Type (S ℓ) } - * R = { (TypeLevel, Type ℓ, TypeOmega), - * (TypeLevel, TypeOmega, TypeOmega), - * (Type ℓ, TypeOmega, TypeOmega), - * (Type ℓ₁, Type ℓ₂, Type (max l₁ l₂) } - *) - and sort = - | Stype of lexp - | StypeOmega - | StypeLevel - and sort_level = - | SLz - | SLsucc of lexp - | SLlub of lexp * lexp - -type varbind = - | Variable - | ForwardRef - | LetDef of U.db_offset * lexp - -(* For metavariables, we give each metavar a (hopefully) unique integer - * and then we store its corresponding info into the `metavar_table` - * global map. - * - * Instead of this single ref-cell holding an IntMap, we could use many - * ref-cells, and do away with the unique integer. The reasons why we - * do it this way are: - * - for printing purposes, we want to have a printable unique identifier - * for each metavar. OCaml does not offer any way to turn a ref-cell - * into some kind of printable identifier (can't get a hash of the address, - * no `eq` hash-tables, ...). - * - Hashtbl.hash as well as `compare` happily follow ref-cell indirections: - * `compare (ref 0) (ref 0)` tells us they're equal! So we need the unique - * integer in order to produce a hash anyway (and we'd have to write the hash - * function by hand, tho that might be a good idea anyway). - *) - -(* Scope level is used to detect "out of scope" metavars. - * See http://okmij.org/ftp/ML/generalization.html - * The ctx_length keeps track of the length of the lctx in which the - * metavar is meant to be defined. *) -type scope_level = int -type ctx_length = int - -type metavar_info = - | MVal of lexp (* Exp to which the var is instantiated. *) - | MVar of scope_level (* Outermost scope in which the var appears. *) - * ltype (* Expected type. *) - (* We'd like to keep the lexp_content in which the type is to be - * understood, but lexp_context is not yet defined here, - * so we just keep the length of the lexp_context. *) - * ctx_length -type meta_subst = metavar_info U.IMap.t - -let dummy_scope_level = 0 - -let builtin_size = ref 0 - -let metavar_table = ref (U.IMap.empty : meta_subst) -let metavar_lookup (id : meta_id) : metavar_info - = try U.IMap.find id (!metavar_table) - with Not_found - -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!" - (********************** Hash-consing **********************) -(* let hc_table : (lexp, lexp) Hashtbl.t = Hashtbl.create 1000 - * let hc (e : lexp) : lexp = - * try Hashtbl.find hc_table e - * with Not_found -> Hashtbl.add hc_table e e; e *) - let lexp_hash (e, h) = h + (** hash-consing test ** + * with: Hashtbl.hash - lexp'_hash + * median bucket length: 7 - 7 + * biggest bucket length: 205 - 22 *) let lexp_lexp' (e, h) = e @@ -183,57 +47,55 @@ let metavar_lookup (id : meta_id) : metavar_info | [] -> 31 | e :: l -> (e * 31) lxor (apply_lxor l) -let combine_hash e1 e2 = (e1 * 31) lxor e2 - (* Hashtbl.hash for not lexp types * TODO: - find something else * - extract the first arg of 2 arg types ? (SMap) *) let lexp'_hash (expr : lexp') = match expr with - | Imm s -> combine_hash 1 (Hashtbl.hash s) + | Imm s -> U.combine_hash 1 (Hashtbl.hash s) | SortLevel l - -> combine_hash 2 (match l with + -> U.combine_hash 2 (match l with | SLz -> Hashtbl.hash l | SLsucc lp -> lexp_hash lp - | SLlub (lp1, lp2) -> combine_hash (lexp_hash lp1) (lexp_hash lp2)) + | SLlub (lp1, lp2) -> U.combine_hash (lexp_hash lp1) (lexp_hash lp2)) | Sort (l, s) - -> combine_hash 3 (combine_hash (Hashtbl.hash l) + -> U.combine_hash 3 (U.combine_hash (Hashtbl.hash l) (match s with | Stype lp -> lexp_hash lp | StypeOmega -> Hashtbl.hash s | StypeLevel -> Hashtbl.hash s)) - | Builtin (v, t, m) as e -> combine_hash 4 (Hashtbl.hash e) - | Var v -> combine_hash 5 (Hashtbl.hash v) + | Builtin (v, t, m) as e -> U.combine_hash 4 (Hashtbl.hash e) + | Var v -> U.combine_hash 5 (Hashtbl.hash v) | Let (l, ds, e) - -> combine_hash 6 (combine_hash (Hashtbl.hash l) - (combine_hash (apply_lxor (List.map (fun e -> let (n, lp, lt) = e in - (combine_hash (Hashtbl.hash n) (combine_hash (lexp_hash lp) (lexp_hash lt)))) + -> U.combine_hash 6 (U.combine_hash (Hashtbl.hash l) + (U.combine_hash (apply_lxor (List.map (fun e -> let (n, lp, lt) = e in + (U.combine_hash (Hashtbl.hash n) (U.combine_hash (lexp_hash lp) (lexp_hash lt)))) ds)) (lexp_hash e))) | Arrow (k, v, t1, l, t2) - -> combine_hash 7 (combine_hash (combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) - (combine_hash (lexp_hash t1) (combine_hash (Hashtbl.hash l) (lexp_hash t2)))) + -> U.combine_hash 7 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (U.combine_hash (lexp_hash t1) (U.combine_hash (Hashtbl.hash l) (lexp_hash t2)))) | Lambda (k, v, t, e) - -> combine_hash 8 (combine_hash (combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) - (combine_hash (lexp_hash t) (lexp_hash e))) + -> U.combine_hash 8 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (U.combine_hash (lexp_hash t) (lexp_hash e))) | Inductive (l, n, a, cs) - -> combine_hash 9 (combine_hash (combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) - (combine_hash (apply_lxor (List.map (fun e -> let (ak, n, lt) = e in - (combine_hash (Hashtbl.hash ak) - (combine_hash (Hashtbl.hash n) (lexp_hash lt)))) a)) + -> U.combine_hash 9 (U.combine_hash (U.combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) + (U.combine_hash (apply_lxor (List.map (fun e -> let (ak, n, lt) = e in + (U.combine_hash (Hashtbl.hash ak) + (U.combine_hash (Hashtbl.hash n) (lexp_hash lt)))) a)) (Hashtbl.hash cs))) - | Cons (t, n) -> combine_hash 10 (combine_hash (lexp_hash t) (Hashtbl.hash n)) + | Cons (t, n) -> U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n)) | Case (l, e, rt, bs, d) - -> combine_hash 11 (combine_hash (combine_hash (Hashtbl.hash l) (lexp_hash e)) - (combine_hash (lexp_hash rt) (combine_hash (Hashtbl.hash bs) + -> U.combine_hash 11 (U.combine_hash (U.combine_hash (Hashtbl.hash l) (lexp_hash e)) + (U.combine_hash (lexp_hash rt) (U.combine_hash (Hashtbl.hash bs) (match d with - | Some (n, lp) -> combine_hash (Hashtbl.hash n) (lexp_hash lp) + | Some (n, lp) -> U.combine_hash (Hashtbl.hash n) (lexp_hash lp) | _ -> 0)))) | Metavar (id, s, v) - -> combine_hash 12 (Hashtbl.hash expr) - | Call (e, args) -> combine_hash 13 (combine_hash (lexp_hash e) + -> U.combine_hash 12 (Hashtbl.hash expr) + | Call (e, args) -> U.combine_hash 13 (U.combine_hash (lexp_hash e) (apply_lxor (List.map (fun e -> let (ak, lp) = e in - (combine_hash (Hashtbl.hash ak) (lexp_hash lp))) args))) - | Susp (lp, subst) -> combine_hash 14 (combine_hash (lexp_hash lp) (Hashtbl.hash subst)) + (U.combine_hash (Hashtbl.hash ak) (lexp_hash lp))) args))) + | Susp (lp, subst) -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst)) let compare_hash x y = let (x', h1) = x in @@ -256,6 +118,7 @@ let hc_eq e1 e2 = | (Sort (_, Stype e1), Sort (_, Stype e2)) -> e1 == e2 | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 | (Var (_, i1), Var (_, i2)) -> i1 = i2 + (* TODO: == via hcs ? *) | ((Susp (e1, s1) as e), _) -> compare e (lexp_lexp' e2) = 0 | (_, (Susp (e2, s2) as e)) -> compare (lexp_lexp' e1) e = 0 | (Let (_, defs1, e1), Let (_, defs2, e2)) @@ -306,15 +169,6 @@ let hc_table : WHC.t = WHC.create 1000 let hc (e : lexp') : lexp = let lp = (e, lexp'_hash e) in WHC.merge hc_table lp -let get_stats table = - let (tl, ne, sumb, smallb, medianb, bigb) = WHC.stats table in - Printf.printf "\n\ttable length: %i\n - number of entries: %i\n - sum of bucket lengths: %i\n - smallest bucket length: %i\n - median bucket length: %i\n - biggest bucket length: %i\n" tl ne sumb smallb medianb bigb - let impossible = hc (Imm Sexp.dummy_epsilon) let mkImm s = hc (Imm s) @@ -387,41 +241,7 @@ let mkSLsucc e = * but Weak.Make doesn't cut it because we need to index with a pair * that is transient and hence immediately GC'd. *) -(* try... *) -type subst_pair = ((lexp * subst) * lexp) - -let subst_hash (s, h) = h - - let hcs_eq sb1 sb2 = - sb1 == sb2 || - match (sb1, sb2) with - | (((l1, S.Identity off), l2), ((l1', S.Identity off'), l2')) - -> l1 == l1' && off = off' && l2 == l2' - | (((l1, S.Cons (lp1, lps1, off1)), l2), ((l1', S.Cons (lp2, lps2, off2)), l2')) - -> l1 == l1' && lp1 == lp2 && lps1 == lps2 && off1 = off2 && l2 == l2' - | _ -> false - - let subst'_hash sb : int = - match sb with - | ((l1, S.Identity off), l2) - -> combine_hash 1 (combine_hash (lexp_hash l1) - (combine_hash (Hashtbl.hash off) (lexp_hash l2))) - | ((l1, S.Cons (lp, sb, off)), l2) - -> combine_hash 2 (combine_hash (lexp_hash l1) - (combine_hash (combine_hash (lexp_hash lp) (subst_hash sb)) - (combine_hash (Hashtbl.hash off) (lexp_hash l2)))) - - module WHCS = Hashtbl.Make (struct type t = subst_pair - let equal x y = hcs_eq x y - let hash = subst_hash - end) - -let hcs_table : WHCS.t = WHCS.create 1000 - -(* let hcs (s : subst') : subst = - let sb = (s, subst'_hash s) in WHCS.merge hcsb_table sb *) - -(******) +let hcs_table : ((lexp * lexp subst), lexp) Hashtbl.t = Hashtbl.create 1000 (* When computing the type of "load"ed modules * we end up building substitutions of the form @@ -799,10 +619,10 @@ let rec lexp_unparse lxp = (* FIXME: ¡Unify lexp_print and lexp_string! *) and lexp_string lxp = sexp_string (lexp_unparse lxp) -and subst_string s = match s with - | S.Identity o -> "↑" ^ string_of_int o - | S.Cons (l, s, 0) -> lexp_name l ^ " · " ^ subst_string s - | S.Cons (l, s, o) +and subst_string s = match S.subst_subst' s with + | Identity o -> "↑" ^ string_of_int o + | Cons (l, s, 0) -> lexp_name l ^ " · " ^ subst_string s + | Cons (l, s, o) -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")" and lexp_name e = @@ -1185,9 +1005,9 @@ let rec eq e1 e2 = and subst_eq s1 s2 = s1 == s2 || - match (s1, s2) with - | (S.Identity o1, S.Identity o2) -> o1 = o2 - | (S.Cons (e1, s1, o1), S.Cons (e2, s2, o2)) + match (S.subst_subst' s1, S.subst_subst' s2) with + | (Identity o1, Identity o2) -> o1 = o2 + | (Cons (e1, s1, o1), Cons (e2, s2, o2)) -> if o1 = o2 then eq e1 e2 && subst_eq s1 s2 else if o1 > o2 then ===================================== src/lexp_type.ml ===================================== @@ -0,0 +1,174 @@ +module U = Util +module L = List +module SMap = U.SMap + + +open Sexp +open Pexp + + +type vname = U.vname +type vref = U.vref +type meta_id = int (* Identifier of a meta variable. *) + +type label = symbol + +type attribute_key = (int * string) (* rev_dbi * Var name *) +module AttributeMap = Map.Make (struct type t = attribute_key let compare = compare end) + +(* We define here substitutions which take a variable within a source context + * Δₛ and should return an expression valid in target context Δₜ. + * + * The current implementation only handles a very limited subset of such + * substitutions. One of the many limitations is that we can only encode + * substitutions which map variables to variables. + *) + +type db_index = int (* DeBruijn index. *) +type db_offset = int (* DeBruijn index offset. *) + +(* Substitution, i.e. a mapping from db_index to 'a + * In practice, 'a is always lexp, but we keep it as a parameter: + * - for better modularity of the code. + * - to break a mutual dependency between the Lexp and the Subst modules. *) +type 'a subst = 'a subst' * int + and 'a subst' = (* lexp subst *) + | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *) + | Cons of 'a * 'a subst * db_offset (* Cons (e, s, o) ≡ (e · s) ∘ ↑ₒ *) + (* Myers's extra pointers down the list: + * * int * 'a subst * db_offset *) +(* Lift (n,m) increases indices≥N by M. + * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination + * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) + (* | Lift of db_index * db_offset *) + +(* Build Myers's "stack" element. *) +(* let mkCons e s o = match s with + * | Cons (_, _, _, sk1, Cons (_, _, _, sk2, s2, o2), o1) when sk1 >= sk2 + * -> Cons (e, s, o, sk1 + sk2 + 1, s2, o1 + o2 + o) + * | _ -> Cons (e, s, o, 1, s, o) *) + +(*************** Elaboration to Lexp *********************) + +(* The scoping of `Let` is tricky: + * + * Since it's a recursive let, the definition part of each binding is + * valid in the "final" scope which includes all the new bindings. + * + * But the type of each binding is not defined in that same scope. Instead + * it's defined in the scope of all the previous bindings. + * + * For exemple the type of the second binding of such a Let is defined in + * the scope of the surrounded context extended with the first binding. + * And the type of the 3rd binding is defined in the scope of the + * surrounded context extended with the first and the second bindings. *) + +type ltype = lexp + and lsubst = lexp subst + and lexp = lexp' * int + and lexp' = + | Imm of sexp (* Used for strings, ... *) + | SortLevel of sort_level + | Sort of U.location * sort + | Builtin of symbol * ltype * lexp AttributeMap.t option + | Var of vref + | Susp of lexp * lsubst (* Lazy explicit substitution: e[σ]. *) + (* This "Let" allows recursion. *) + | Let of U.location * (vname * lexp * ltype) list * lexp + | Arrow of arg_kind * vname * ltype * U.location * ltype + | Lambda of arg_kind * vname * ltype * lexp + | Call of lexp * (arg_kind * lexp) list (* Curried call. *) + | Inductive of U.location * label + * ((arg_kind * vname * ltype) list) (* formal Args *) + * ((arg_kind * vname * ltype) list) SMap.t + | Cons of lexp * symbol (* = Type info * ctor_name *) + | Case of U.location * lexp + * ltype (* The type of the return value of all branches *) + * (U.location * (arg_kind * vname) list * lexp) SMap.t + * (vname * lexp) option (* Default. *) + (* The `subst` will be applied to the the metavar's value when it + * gets instantiated. *) + | Metavar of meta_id * lsubst * vname + (* (\* For logical metavars, there's no substitution. *\) + * | Metavar of (U.location * string) * metakind * metavar ref + * and metavar = + * (\* An uninstantiated var, along with a venv (stipulating over which vars + * * it should be closed), and its type. + * * If its type is not given, it implies its type should be a sort. *\) + * | MetaUnset of (lexp option * lexp) VMap.t * ltype option * scope_level + * | MetaSet of lexp + * and metakind = + * | MetaGraft of subst + * (\* Forward reference or Free var: Not known yet, but not instantiable by + * * unification. *\) + * | MetaFoF + * and subst = lexp VMap.t *) + (* + * The PTS I'm imagining looks like: + * + * S = { TypeLevel, TypeOmega, Type ℓ } + * A = { Level : TypeLevel, Z : Level, S : Level → Level, + * Type : (ℓ : Level) → Type (S ℓ) } + * R = { (TypeLevel, Type ℓ, TypeOmega), + * (TypeLevel, TypeOmega, TypeOmega), + * (Type ℓ, TypeOmega, TypeOmega), + * (Type ℓ₁, Type ℓ₂, Type (max l₁ l₂) } + *) + and sort = + | Stype of lexp + | StypeOmega + | StypeLevel + and sort_level = + | SLz + | SLsucc of lexp + | SLlub of lexp * lexp + +type varbind = + | Variable + | ForwardRef + | LetDef of U.db_offset * lexp + + let lexp_hash (e, h) = h +(* For metavariables, we give each metavar a (hopefully) unique integer + * and then we store its corresponding info into the `metavar_table` + * global map. + * + * Instead of this single ref-cell holding an IntMap, we could use many + * ref-cells, and do away with the unique integer. The reasons why we + * do it this way are: + * - for printing purposes, we want to have a printable unique identifier + * for each metavar. OCaml does not offer any way to turn a ref-cell + * into some kind of printable identifier (can't get a hash of the address, + * no `eq` hash-tables, ...). + * - Hashtbl.hash as well as `compare` happily follow ref-cell indirections: + * `compare (ref 0) (ref 0)` tells us they're equal! So we need the unique + * integer in order to produce a hash anyway (and we'd have to write the hash + * function by hand, tho that might be a good idea anyway). + *) + +(* Scope level is used to detect "out of scope" metavars. + * See http://okmij.org/ftp/ML/generalization.html + * The ctx_length keeps track of the length of the lctx in which the + * metavar is meant to be defined. *) +type scope_level = int +type ctx_length = int + +type metavar_info = + | MVal of lexp (* Exp to which the var is instantiated. *) + | MVar of scope_level (* Outermost scope in which the var appears. *) + * ltype (* Expected type. *) + (* We'd like to keep the lexp_content in which the type is to be + * understood, but lexp_context is not yet defined here, + * so we just keep the length of the lexp_context. *) + * ctx_length +type meta_subst = metavar_info U.IMap.t + +let dummy_scope_level = 0 + +let builtin_size = ref 0 + +let metavar_table = ref (U.IMap.empty : meta_subst) +let metavar_lookup (id : meta_id) : metavar_info + = try U.IMap.find id (!metavar_table) + with Not_found + -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!" ===================================== src/opslexp.ml ===================================== @@ -30,6 +30,7 @@ module P = Pexp (* open Grammar *) open Lexp module E = Elexp +open Lexp_type module L = Lexp module M = Myers @@ -933,38 +934,38 @@ let rec get_type ctx e = (*********** Type erasure, before evaluation. *****************) -let rec erase_type (lxp: L.lexp): E.elexp = +let rec erase_type (lxp: lexp): E.elexp = let lxp' = lexp_lexp' lxp in match lxp' with - | L.Imm(s) -> E.Imm(s) - | L.Builtin(v, _, _) -> E.Builtin(v) - | L.Var(v) -> E.Var(v) - | L.Cons(_, s) -> E.Cons(s) - | L.Lambda (P.Aerasable, _, _, body) -> + | Imm(s) -> E.Imm(s) + | Builtin(v, _, _) -> E.Builtin(v) + | Var(v) -> E.Var(v) + | Cons(_, s) -> E.Cons(s) + | Lambda (P.Aerasable, _, _, body) -> (* The var shouldn't appear in body, basically, but we need * to adjust the debruijn indices of other vars, hence the subst. *) erase_type (L.push_susp body (S.substitute DB.type0)) - | L.Lambda (_, vdef, _, body) -> + | Lambda (_, vdef, _, body) -> E.Lambda (vdef, erase_type body) - | L.Let(l, decls, body) -> + | Let(l, decls, body) -> E.Let(l, (clean_decls decls), (erase_type body)) - | L.Call(fct, args) -> + | Call(fct, args) -> E.Call((erase_type fct), (filter_arg_list args)) - | L.Case(l, target, _, cases, default) -> + | Case(l, target, _, cases, default) -> E.Case(l, (erase_type target), (clean_map cases), (clean_maybe default)) - | L.Susp(l, s) -> erase_type (L.push_susp l s) + | Susp(l, s) -> erase_type (L.push_susp l s) (* To be thrown out *) - | L.Arrow _ -> E.Type lxp - | L.SortLevel _ -> E.Type lxp - | L.Sort _ -> E.Type lxp + | Arrow _ -> E.Type lxp + | SortLevel _ -> E.Type lxp + | Sort _ -> E.Type lxp (* Still useful to some extent. *) - | L.Inductive(l, label, _, _) -> E.Type lxp + | Inductive(l, label, _, _) -> E.Type lxp | Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> erase_type (push_susp e s) ===================================== src/sexp.ml ===================================== @@ -258,4 +258,3 @@ and sexp_eq_list ss1 ss2 = match ss1, ss2 with | (s1 :: ss1), (s2 :: ss2) -> sexp_equal s1 s2 && sexp_eq_list ss1 ss2 | _ -> false - ===================================== src/subst.ml ===================================== @@ -20,6 +20,7 @@ You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>. *) module U = Util +open Lexp_type (* Implementation of the subsitution calculus. * @@ -103,43 +104,49 @@ module U = Util * *) -(* We define here substitutions which take a variable within a source context - * Δₛ and should return an expression valid in target context Δₜ. - * - * The current implementation only handles a very limited subset of such - * substitutions. One of the many limitations is that we can only encode - * substitutions which map variables to variables. - *) + (********************** Hash-consing **********************) + + (** hash-consing test ** + * with: subst'_hash + * median bucket length: 7 + * biggest bucket length: 22 *) + + let subst_hash (s, h) = h + let subst_subst' (s, h) = s + + let hcsb_eq sb1 sb2 = + sb1 == sb2 || + match (subst_subst' sb1, subst_subst' sb2) with + | (Identity off1, Identity off2) -> off1 = off2 + | (Cons (lp1, lps1, off1), Cons (lp2, lps2, off2)) + -> lp1 == lp2 && lps1 == lps2 && off1 = off2 + | _ -> false + + let subst'_hash (sb : 'a subst') : int = + match sb with + | Identity off + -> U.combine_hash 1 (Hashtbl.hash off) + | Cons (lp, sb, off) + -> U.combine_hash 2 + (U.combine_hash (U.combine_hash + (lexp_hash lp) (subst_hash sb)) (Hashtbl.hash off)) + + module WHCSB = Weak.Make (struct type t = lexp subst + let equal x y = hcsb_eq x y + let hash = subst_hash + end) + + let hcsb_table : WHCSB.t = WHCSB.create 1000 -type db_index = int (* DeBruijn index. *) -type db_offset = int (* DeBruijn index offset. *) - -(* Substitution, i.e. a mapping from db_index to 'a - * In practice, 'a is always lexp, but we keep it as a parameter: - * - for better modularity of the code. - * - to break a mutual dependency between the Lexp and the Subst modules. *) -type 'a subst = (* lexp subst *) - | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *) - | Cons of 'a * 'a subst * db_offset (* Cons (e, s, o) ≡ (e · s) ∘ ↑ₒ *) - (* Myers's extra pointers down the list: - * * int * 'a subst * db_offset *) -(* Lift (n,m) increases indices≥N by M. - * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination - * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) - (* | Lift of db_index * db_offset *) - -(* Build Myers's "stack" element. *) -(* let mkCons e s o = match s with - * | Cons (_, _, _, sk1, Cons (_, _, _, sk2, s2, o2), o1) when sk1 >= sk2 - * -> Cons (e, s, o, sk1 + sk2 + 1, s2, o1 + o2 + o) - * | _ -> Cons (e, s, o, 1, s, o) *) + let hcsb (s : lexp subst') : lexp subst = + let sb = (s, subst'_hash s) in WHCSB.merge hcsb_table sb (* Apply a substitution to a single variable. *) let lookup (mkVar : 'b -> db_index -> 'a) (mkShift: 'a -> db_offset -> 'a) (s: 'a subst) (l : 'b) (v:db_index) : 'a = let rec lookup' (o:db_offset) (s: 'a subst) (v:db_index) : 'a = - match s with + match subst_subst' s with | Identity o' -> mkVar l (v + o + o') (* Use Myers's fastlane when applicable: * | Cons (_, _, _, sk, s, o') when v >= sk -> lookup' (o + o') s (v - sk) *) @@ -148,26 +155,27 @@ let lookup (mkVar : 'b -> db_index -> 'a) else mkShift e o in lookup' 0 s v +(* ici *) let mkShift s (m:db_offset) = if m>0 then - match s with Identity o -> Identity (o + m) - | Cons (e, s, o) -> Cons (e, s, o + m) + match subst_subst' s with Identity o -> hcsb (Identity (o + m)) + | Cons (e, s, o) -> hcsb (Cons (e, s, o + m)) else s (* A substitution which adds M to every deBruijn index. * I.e. one that takes variables from a context Δₛ to an extended * context ΔₛΔₜ where Δₜ has size M. *) -let shift (m:db_offset) = Identity m +let shift (m:db_offset) : 'a subst = hcsb (Identity m) (* Return a substitution which replaces #0 with `e` and then applies `s` * to the rest. *) -let cons e s = Cons (e, s, 0) +let cons e s : 'a subst = hcsb (Cons (e, s, 0)) (* The trivial substitution which doesn't do anything. *) -let identity = Identity 0 +let identity = hcsb (Identity 0) (* Test if a substitution is trivial. The "_p" stands for "predicate". *) -let identity_p s = match s with | Identity o -> o = 0 | _ -> false +let identity_p s = match subst_subst' s with | Identity o -> o = 0 | _ -> false (* Compose two substitutions. This implements the merging rules. * Returns s₁ ∘ s₂ (i.e. s₁ is applied before s₂) *) @@ -177,27 +185,27 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) * that some shifts can be pushed more or less down. Here we * want the shifts to float as far outside as possible. *) let rec compose' (s1: 'a subst) (s2: 'a subst) : 'a subst = - match s1 with + match subst_subst' s1 with | Identity o1 - -> let rec compose_id o1 s o = match s with - | Identity o2 -> Identity (o + o1 + o2) + -> let rec compose_id o1 s o = match subst_subst' s with + | Identity o2 -> hcsb (Identity (o + o1 + o2)) | Cons (e2, s2, o2) (* , sk2, s2', o2' *) -> (* Myers's fastlane: * if o1 >= sk2 then compose_id (o1 - sk2) s2' (o + o2') *) if o1 > 0 then compose_id (o1 - 1) s2 (o + o2) - else Cons (e2, s2, o + o2) + else hcsb (Cons (e2, s2, o + o2)) in compose_id o1 s2 0 | Cons (e1, s1, o1) - -> let rec compose_cons o1 s o = match s with - | Identity o2 -> Cons (e1, s1, o + o1 + o2) + -> let rec compose_cons o1 s o = match subst_subst' s with + | Identity o2 -> hcsb (Cons (e1, s1, o + o1 + o2)) | Cons (e2, s2, o2) (* , sk2, s2', o2' *) -> (* Myers's fastlane: * if o1 >= sk2 then compose_cons (o1 - sk1) s2' (o + o2') *) if o1 > 0 then compose_cons (o1 - 1) s2 (o + o2) - else + else (* Pull out o2's shift and compose the two Cons. *) let s' = cons e2 s2 in - Cons (mkSusp e1 s', compose' s1 s', o + o2) + hcsb (Cons (mkSusp e1 s', compose' s1 s', o + o2)) in compose_cons o1 s2 0 in compose' s1 s2 ===================================== src/unification.ml ===================================== @@ -19,7 +19,9 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>. *) +open Lexp_type open Lexp + (* open Sexp *) (* open Inverse_subst *) module OL = Opslexp @@ -130,43 +132,43 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with * aka * ?a = ?b[0 => 0 · ↑1] *) -let common_subset ctx s1 s2 = - let rec loop s1 s2 o1 o2 o = - match (s1, s2) with - | (S.Cons (le1, s1', o1'), S.Cons (le2, s2', o2')) +let common_subset ctx (s1 : lsubst) (s2 : lsubst) = + let rec loop (s1 : lsubst) (s2 : lsubst) o1 o2 o = + match (S.subst_subst' s1, S.subst_subst' s2) with + | (Cons (le1, s1', o1'), Cons (le2, s2', o2')) -> let o1 = o1 + o1' in let o2 = o2 + o2' in (* FIXME: We should check if le1 and le2 are *unifiable* instead! *) if not (le1 = impossible || le1 = impossible) && OL.conv_p ctx (mkSusp le1 (S.shift o1)) (mkSusp le2 (S.shift o2)) then match loop s1' s2' o1 o2 1 with - | S.Identity 1 -> S.Identity o (* Optimization! *) - | s' -> S.Cons (mkVar ((lexp_location le1, None), 0), - s', o) + | (Identity 1, _) -> S.hcsb (Identity o) (* Optimization! *) + | (sb, _) as s' -> S.hcsb (Cons (mkVar ((lexp_location le1, None), 0), + s', o)) else loop s1' s2' o1 o2 (o + 1) (* If one of them reached `Identity`, unroll it, knowing that * * Identity 0 = #0 · #1 · #2 ... = #0 · (Identity 1) *) - | (S.Cons _, S.Identity o2') - -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0), - S.Identity 1, o2')) + | (Cons _, Identity o2') + -> loop s1 (S.hcsb (Cons (mkVar ((U.dummy_location, None), 0), + S.hcsb (Identity 1), o2'))) o1 o2 o - | (S.Identity o1', S.Cons _) - -> loop (S.Cons (mkVar ((U.dummy_location, None), 0), - S.Identity 1, o1')) + | (Identity o1', Cons _) + -> loop (S.hcsb (Cons (mkVar ((U.dummy_location, None), 0), + S.hcsb (Identity 1), o1'))) s2 o1 o2 o - | (S.Identity o1', S.Identity o2') + | (Identity o1', Identity o2') -> assert (o1 + o1' = o2 + o2'); - S.Identity o + S.hcsb (Identity o) in loop s1 s2 0 0 0 (* Return the number of vars difference between input and output context. * * Could be returned directly by `common_subset`, but it's pretty easy to * compute it here instead. *) -let rec s_offset s = match s with - | S.Identity o -> o - | S.Cons (_, s', o) -> o - 1 + s_offset s' +let rec s_offset (s : lsubst) = match S.subst_subst' s with + | Identity o -> o + | Cons (_, s', o) -> o - 1 + s_offset s' (************************** Top level unify **********************************) @@ -311,7 +313,7 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | Metavar (idx2, s2, name) -> if idx = idx2 then match common_subset ctx s1 s2 with - | S.Identity 0 -> [] (* Optimization! *) + | (Identity 0, _) -> [] (* Optimization! *) (* ¡ s1 != s2 ! * Create a new metavar that can only refer to those vars * which are mapped identically by `s1` and `s2` @@ -319,7 +321,7 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) * This metavar doesn't necessarily live exactly in `ctx` * nor even a proper prefix of it, tho :-( !! *) - | s -> + | (sb, _) as s -> (* print_string "Metavar idx-idx s1!=s2\n"; *) assert (not (OL.conv_p ctx lxp1 lxp2)); match (Inverse_subst.inverse s, ===================================== src/util.ml ===================================== @@ -116,3 +116,14 @@ let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option = match opt with | None -> None | Some x -> Some (fn x) + +let combine_hash e1 e2 = (e1 * 31) lxor e2 + +let get_stats stats = + let (tl, ne, sumb, smallb, medianb, bigb) = stats in + Printf.printf "\n\ttable length: %i\n + number of entries: %i\n + sum of bucket lengths: %i\n + smallest bucket length: %i\n + median bucket length: %i\n + biggest bucket length: %i\n" tl ne sumb smallb medianb bigb View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ab6585a3c7ea5cd7ec35c0b9a7b4ec3ae… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ab6585a3c7ea5cd7ec35c0b9a7b4ec3ae… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Juin 2020