Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer

Commits: 11f83513 by Soilih BEN SOILIH at 2021-11-10T09:00:02-05:00 -

- - - - - 83c17570 by Soilih BEN SOILIH at 2021-11-11T02:00:16-05:00 -

- - - - - 4d2bb66c by Soilih BEN SOILIH at 2021-11-11T09:56:49-05:00 -

- - - - - 58600d02 by Soilih BEN SOILIH at 2021-11-11T20:16:17-05:00 fixing p.m problems in lexp, elab, inverse_subst

- - - - -

3 changed files:

- src/elab.ml - src/inverse_subst.ml - src/lexp.ml

Changes:

===================================== src/elab.ml ===================================== @@ -429,6 +429,7 @@ let meta_to_var ids (e : lexp) = | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e | Var (n,i) -> if i < o then e else mkVar (n, i + count) + | Proj (l, lxp, lbl) -> mkProj (l, loop o lxp, lbl) | Susp (e, s) -> loop o (push_susp e s) | Let (l, defs, e) -> let len = List.length defs in

===================================== src/inverse_subst.ml ===================================== @@ -264,6 +264,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = | Sort (_l, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) + | Proj (l,lxp,lbl) -> mkProj (l, apply_inv_subst lxp s, lbl) | Susp (e, s') -> apply_inv_subst (push_susp e s') s | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in

===================================== src/lexp.ml ===================================== @@ -66,7 +66,7 @@ type ltype = lexp | Sort of U.location * sort | Builtin of symbol * ltype | Var of vref - | Proj of U.location * string * lexp + | Proj of U.location * lexp * label | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vname * lexp * ltype) list * lexp @@ -246,6 +246,9 @@ let lexp'_hash (lp : lexp') = args))) | Susp (lp, subst) -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst)) + | Proj (l,lxp,lbl) + -> U.combine_hash 15 (U.combine_hash (Hashtbl.hash l) + (U.combine_hash (Hashtbl.hash lxp) (Hashtbl.hash lbl)))

(* Equality function for hash table * using physical equality for "sub-lexp" and compare for `subst`. *) @@ -310,6 +313,7 @@ let mkSortLevel l = hc (SortLevel l) let mkSort (l, s) = hc (Sort (l, s)) let mkBuiltin (v, t) = hc (Builtin (v, t)) let mkVar v = hc (Var v) +let mkProj (l,lxp,lbl) = hc (Proj (l,lxp,lbl)) let mkLet (l, ds, e) = hc (Let (l, ds, e)) let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) @@ -330,6 +334,7 @@ let lexp_head e = | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s | Var _ -> "Var" + | Proj _ -> "Proj" | Let _ -> "let" | Arrow _ -> "Arrow" | Lambda _ -> "lambda" @@ -592,6 +597,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) * in many other cases than just when we bump into a Susp. *) | Susp (e,s') -> push_susp e (scompose s' s) | (Var _ | Metavar _) -> nosusp (mkSusp e s) + | Proj (l,lxp,lbl) -> mkProj (l, mkSusp lxp s, lbl)

and nosusp e = (* Return `e` with no outermost `Susp`. *) match lexp_lexp' e with @@ -655,6 +661,7 @@ let clean e = | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e else clean S.identity (mkSusp e s) + | Proj (l,lxp,lbl) -> mkProj (l,(clean s lxp),lbl) | Metavar (idx, s', name) -> let s = scompose s' s in match metavar_lookup idx with @@ -673,6 +680,9 @@ let rec lexp_unparse lxp = | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) | Var ((loc, name), _) -> Symbol (loc, maybename name) + | Proj (l,lxp,(loc,str) ) + -> Node (Symbol (l, "__.__"), + [(lexp_unparse lxp);(Symbol (loc,str))]) | Cons (t, (l, name)) -> Node (sdatacons, [lexp_unparse t; Symbol (l, name)]) @@ -975,6 +985,9 @@ and lexp_str ctx (exp : lexp) : string =

| Var ((_loc, name), idx) -> maybename name ^ (index idx) ;

+ | Proj (l,lxp,(loc,str)) + -> "( __.__ " ^ lexp_str' lxp ^ " " ^ str ^ " )" + | Metavar (idx, subst, (_loc, name)) (* print metavar result if any *) -> (match metavar_lookup idx with

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/16eab6116a4d9414d2a0b4e9eb64af460...