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

Commits: 13cf6a0e by Soilih BEN SOILIH at 2021-11-18T02:55:29-05:00 elexp, lexp, opslexp, positivity, unification

- - - - -

5 changed files:

- src/elexp.ml - src/lexp.ml - src/opslexp.ml - src/positivity.ml - src/unification.ml

Changes:

===================================== src/elexp.ml ===================================== @@ -52,6 +52,8 @@ type elexp = (* A variable reference, using deBruijn indexing. *) | Var of vref

+ | Proj of U.location * elexp * symbol + (* Recursive `let` binding. *) | Let of U.location * (vname * elexp) list * elexp

@@ -83,6 +85,7 @@ let rec elexp_location e = match e with | Imm s -> sexp_location s | Var ((l,_), _) -> l + | Proj (l,_,_) -> l | Builtin ((l, _)) -> l | Let (l,_,_) -> l | Lambda ((l,_),_) -> l @@ -96,6 +99,7 @@ let elexp_name e = match e with | Imm _ -> "Imm" | Var _ -> "Var" + | Proj _ -> "Proj" | Let _ -> "Let" | Call _ -> "Call" | Cons _ -> "Cons" @@ -136,6 +140,8 @@ and elexp_string lxp = | Imm(s) -> sexp_string s | Builtin((_, s)) -> s | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]" + | Proj (l,lxp,(loc,str)) + -> "( _._ " ^ elexp_string lxp ^ " " ^ str ^ " )" | Cons (_, (_, s)) -> "datacons(" ^ s ^")"

| Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b)

===================================== src/lexp.ml ===================================== @@ -986,7 +986,7 @@ and lexp_str ctx (exp : lexp) : string = | Var ((_loc, name), idx) -> maybename name ^ (index idx) ;

| Proj (l,lxp,(loc,str)) - -> "( __.__ " ^ lexp_str' lxp ^ " " ^ str ^ " )" + -> "( _._ " ^ lexp_str' lxp ^ " " ^ str ^ " )"

| Metavar (idx, subst, (_loc, name)) (* print metavar result if any *)

===================================== src/opslexp.ml ===================================== @@ -1015,7 +1015,7 @@ and get_type ctx e = | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, _name), _idx) as v) -> lookup_type ctx v - | Proj (l,lxp,lbl) -> get_type ctx lxp + | Proj (l,lxp,lbl) -> mkProj (l,lxp,lbl) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in @@ -1147,7 +1147,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) | L.Var (v) -> E.Var (v) - | L.Proj (l,lxp,lbl) -> erase_type lctx lxp + | L.Proj (l,lxp,lbl) -> E.Proj (l, erase_type lctx lxp,lbl) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s)

| L.Lambda (P.Aerasable, _, _, body)

===================================== src/positivity.ml ===================================== @@ -116,6 +116,7 @@ and positive' index lexp = * as the Call applies as a degenerate case with no arguments. *) -> true + | Lexp.Proj _ -> false

| Lexp.Case _ | Lexp.Cons _ | Lexp.Let _ | Lexp.Sort _ | Lexp.SortLevel _ (* There are no rules that have these synctactic forms as a conclusion. *)

===================================== src/unification.ml ===================================== @@ -69,6 +69,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Sort (_, (StypeOmega | StypeLevel)) -> false | Builtin _ -> false | Var (_, _i) -> false + | Proj(_,lxp,_) -> oi lxp | Susp (_e, _s) -> Log.internal_error "`e` should be "clean" here!?" (* ; oi (push_susp e s) *) | Let (_, defs, e)

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/13cf6a0ec06b3e4b6ec0a99ebb81bd82c7...