Stefan pushed to branch graveline at Stefan / Typer

Commits: 3fcfd932 by Stefan Monnier at 2018-05-17T17:37:14Z Rewrite ctx2tup

* src/debruijn.ml (lct_view): Only allow LetDef in CVfix. (lctx_view): Adjust accordingly. * src/eval.ml (print_eval_result.from_lctx.from_lctx'): * src/opslexp.ml (lctx_to_subst.s2): Adjust accordingly. (mktup): Remove. (ctx2tup): Rewrite to build a let-nest with a (simpler) tuple inside.

- - - - - d6005a0c by Stefan Monnier at 2018-05-18T17:44:46Z * src/lexp.ml (push_susp): Fix list inversion

Reported by Jonathan Graveline.

- - - - - 0c789e5d by Stefan Monnier at 2018-05-18T18:31:03Z Move db_offset from env_elem to LetDef

* src/debruijn.ml (env_elem): Remove db_offset. * src/lexp.ml (varbind): Add db_offset to LetDef.

- - - - - a7ed6fa2 by Stefan Monnier at 2018-05-18T19:43:20Z Merge branch 'trunk' into graveline

Also adds bool.typer and empty.typer for testing purposes, mostly.

- - - - -

7 changed files:

- + samples/bool.typer - src/debruijn.ml - src/elab.ml - src/eval.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== samples/bool.typer ===================================== --- /dev/null +++ b/samples/bool.typer @@ -0,0 +1,44 @@ +%%% bool.typer --- Library of plain old booleans + +%% Call it `t` so when we do `Bool = load "bool.typer"`, we +%% can use `Bool.t` to refer to the type. +%% FIXME: In a type context, `Bool` should then automatically be "coerced" +%% to `Bool.t`. +type t + | false + | true; + +%% FIXME: These grammar settings currently only apply to this file, +%% whereas they should be import(ed|able) via something like `load`. +define-operator "if" () 2; +define-operator "then" 2 1; +define-operator "else" 1 66; + +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 quote (case uquote e1 + | true => uquote e2 + | false => uquote e3)); + +%% FIXME: Type annotations should not be needed below. +not : t -> t; +not x = if x then false else true; + +or : t -> t -> t; +or x y = if x then x else y; + +and : t -> t -> t; +and x y = if x then y else x; + +xor : t -> t -> t; +xor x y = if x then (not y) else y; + +%% FIXME: Can't use ?a because that is generalized to be universe-polymorphic, +%% which we don't support in `load` yet. +fold : t -> (a : Type) ≡> a -> a -> a; +fold x t e = if x then t else e; + +

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -94,7 +94,7 @@ let type_float = mkBuiltin ((dloc, "Float"), type0, None) let type_string = mkBuiltin ((dloc, "String"), type0, None)

(* easier to debug with type annotations *) -type env_elem = (db_offset * vname option * varbind * ltype) +type env_elem = (vname option * varbind * ltype) type lexp_context = env_elem M.myers

type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *) @@ -151,43 +151,46 @@ let rec senv_lookup (name: string) (ctx: elab_context): int = let (_, (n, map), _, _) = ctx in n - (SMap.find name map) - 1

-let lexp_ctx_cons (ctx : lexp_context) offset d v t = - assert (offset >= 0 +let lexp_ctx_cons (ctx : lexp_context) d v t = + assert (let offset = match v with | LetDef (o, _) -> o | _ -> 0 in + offset >= 0 && (ctx = M.nil - || let (previous_offset, _, _, _) = M.car ctx in - previous_offset >= 0 (* General constraint. *) - (* Either `ctx` is self-standing (doesn't depend on us), - * or it depends on us (and maybe other bindings to come), in - * which case we have to depend on the exact same bindings. *) - && (previous_offset <= 1 - || previous_offset = 1 + offset))); - M.cons (offset, d, v, t) ctx + || match M.car ctx with + | (_, LetDef (previous_offset, _), _) + -> previous_offset >= 0 (* General constraint. *) + (* Either `ctx` is self-standing (doesn't depend on us), + * or it depends on us (and maybe other bindings to come), in + * which case we have to depend on the exact same bindings. *) + && (previous_offset <= 1 + || previous_offset = 1 + offset) + | _ -> true)); + M.cons (d, v, t) ctx

let lctx_extend (ctx : lexp_context) (def: vname option) (v: varbind) (t: lexp) = - lexp_ctx_cons ctx 0 def v t + lexp_ctx_cons ctx def v t

-let env_extend_rec r (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = +let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = let (loc, name) = def in let (grm, (n, map), env, sl) = ctx in let nmap = SMap.add name n map in (grm, (n + 1, nmap), - lexp_ctx_cons env r (Some def) v t, + lexp_ctx_cons env (Some def) v t, sl)

-let env_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec 0 ctx def v t +let env_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t

let ectx_extend (ectx: elab_context) (def: vname option) (v: varbind) (t: lexp) : elab_context = match def with | None -> let (grm, (n, map), lctx, sl) = ectx in - (grm, (n + 1, map), lexp_ctx_cons lctx 0 None v t, sl) + (grm, (n + 1, map), lexp_ctx_cons lctx None v t, sl) | Some def -> env_extend ectx def v t

let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = let (ctx, _) = List.fold_left (fun (ctx, recursion_offset) (def, e, t) -> - lexp_ctx_cons ctx recursion_offset (Some def) (LetDef e) t, + lexp_ctx_cons ctx (Some def) (LetDef (recursion_offset, e)) t, recursion_offset - 1) (ctx, List.length defs) defs in ctx @@ -233,7 +236,7 @@ let print_lexp_ctx_n (ctx : lexp_context) start = let names = ref [] in for i = start to n do let name = match (M.nth (n - i) lst) with - | (_, Some (_, name), _, _) -> name + | (Some (_, name), _, _) -> name | _ -> "" in names := name::!names done; !names in @@ -252,9 +255,9 @@ let print_lexp_ctx_n (ctx : lexp_context) start =

try let r, name, exp, tp = match env_lookup_by_index (n - idx - 1) ctx with - | (r, Some (_, name), LetDef exp, tp) -> r, name, Some exp, tp - | (r, Some (_, name), _, tp) -> r, name, None, tp - | (r, _, _, tp) -> r, "", None, tp in + | (Some (_, name), LetDef (r, exp), tp) -> r, name, Some exp, tp + | (Some (_, name), _, tp) -> 0, name, None, tp + | (_, _, tp) -> 0, "", None, tp in

(* Print env Info *) lalign_print_int r 4; @@ -297,7 +300,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem =

try(let ret = (Myers.nth dbi ctx) in let _ = match ret with - | (_, Some (_, name), _, _) -> + | (Some (_, name), _, _) -> (* Check if names match *) if not (ename = name) then (print_lexp_ctx ctx; @@ -318,13 +321,13 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem =

let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = let (_, i) = vref in - let (_, _, _, t) = lctx_lookup ctx vref in + let (_, _, t) = lctx_lookup ctx vref in mkSusp t (S.shift (i + 1))

let lctx_lookup_value (ctx : lexp_context) (vref : vref) : lexp option = let (_, i) = vref in match lctx_lookup ctx vref with - | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o))) + | (_, LetDef (o, v), _) -> Some (push_susp v (S.shift (i + 1 - o))) | _ -> None

let env_lookup_type ctx (v : vref): lexp = @@ -343,19 +346,18 @@ type lct_view = let rec lctx_view lctx = match lctx with | Myers.Mnil -> CVempty - | Myers.Mcons ((0, loname, odef, t), lctx, _, _) - -> CVlet (loname, odef, t, lctx) - | Myers.Mcons ((1, loname, LetDef def, t), lctx, _, _) + | Myers.Mcons ((loname, LetDef (1, def), t), lctx, _, _) -> let rec loop i lctx defs = match lctx with - | Myers.Mcons ((o, loname, LetDef def, t), lctx, _, _) + | Myers.Mcons ((loname, LetDef (o, def), t), lctx, _, _) when o = i -> loop (i + 1) lctx ((loname, def, t) :: defs) | _ -> CVfix (defs, lctx) in loop 2 lctx [(loname, def, t)] - | Myers.Mcons ((_, _, _, _), _, _, _) - -> U.internal_error "Unexpected recursive non-LetDef!" - | _ -> U.internal_error "Unexpected lexp_context shape!" + | Myers.Mcons ((_, LetDef (o, def), _), _, _, _) when o > 1 + -> U.internal_error "Unexpected lexp_context shape!" + | Myers.Mcons ((loname, odef, t), lctx, _, _) + -> CVlet (loname, odef, t, lctx)

(** Sets of DeBruijn indices **)

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -188,7 +188,7 @@ let ctx_extend (ctx: elab_context) (var : vname option) def ltype =

let ctx_define (ctx: elab_context) var lxp ltype = elab_check_def ctx var lxp ltype; - env_extend ctx var (LetDef lxp) ltype + env_extend ctx var (LetDef (0, lxp)) ltype

let ctx_define_rec (ctx: elab_context) decls = let nctx = ectx_extend_rec ctx decls in @@ -882,7 +882,7 @@ and track_fv rctx lctx e = | (Some n,_) -> n | _ -> "<anon>" in match Myers.nth i lctx with - | (o, _, LetDef e, _) + | (_, LetDef (o, e), _) -> let drop = i + 1 - o in if drop <= 0 then "somevars[" ^ string_of_int i ^ "-" ^ string_of_int o ^ "]" @@ -957,12 +957,13 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) let i = senv_lookup vname nctx in assert (i < List.length defs); match Myers.nth i (ectx_to_lctx nctx) with - | (o, v', ForwardRef, t) + | (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 d = (v', LetDef (i + 1, e), t) in (IMap.add i (v, e, t) map, - (grm, ec, Myers.set_nth i (o, v', LetDef e, t) lc, sl)) + (grm, ec, Myers.set_nth i d lc, sl)) | _ -> U.internal_error "Defining same slot!") defs (IMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in @@ -1028,7 +1029,7 @@ and lexp_decls_1 let pt_idx = senv_lookup vname nctx in (* Take the previous type annotation. *) let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with - | (_, _, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) + | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) | _ -> U.internal_error "Var not found at its index!" in (* Unify it with the new one. *) let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -769,7 +769,7 @@ let from_lctx (lctx: lexp_context): runtime_env = -> let rctx = from_lctx lctx in Myers.cons (roname loname, ref (match def with - | LetDef e + | LetDef (_, e) -> let e = L.clean e in if closed_p rctx (OL.fv e) then eval (OL.erase_type e) rctx

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -120,7 +120,7 @@ type ltype = lexp type varbind = | Variable | ForwardRef - | LetDef of lexp + | 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` @@ -272,13 +272,11 @@ let rec push_susp e s = (* Push a suspension one level down. *)

| Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in - let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) - -> (ssink v s, - (v, mkSusp def s', mkSusp ty s) :: ndefs)) - (s, []) defs in - (* Why does definition list was reversed? It do not break anything to reverse it back! *) - (*mkLet (l, ndefs, mkSusp e s')*) - mkLet (l, List.rev ndefs, mkSusp e s') + let rec loop s defs = match defs with + | [] -> [] + | (v, def, ty) :: defs + -> (v, mkSusp def s', mkSusp ty s) :: loop (ssink v s) defs in + mkLet (l, loop s defs, mkSusp e s') | Arrow (ak, v, t1, l, t2) -> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink (maybev v) s)) | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s))

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -76,7 +76,7 @@ let rec lexp_defs_subst l s defs = match defs with let rec lctx_to_subst lctx = match DB.lctx_view lctx with | DB.CVempty -> Subst.identity - | DB.CVlet (_, LetDef e, _, lctx) + | DB.CVlet (_, LetDef (_, e), _, lctx) -> let s = lctx_to_subst lctx in L.scompose (S.substitute e) s | DB.CVlet (ov, _, _, lctx) @@ -242,11 +242,11 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, vd2, t21, _, t22)) -> ak1 == ak2 && conv_p t11 t21 - && conv_p' (DB.lexp_ctx_cons ctx 0 vd1 Variable t11) (set_shift vs') + && conv_p' (DB.lexp_ctx_cons ctx vd1 Variable t11) (set_shift vs') t12 t22 | (Lambda (ak1, l1, t1, e1), Lambda (ak2, l2, t2, e2)) -> ak1 == ak2 && (conv_erase || conv_p t1 t2) - && conv_p' (DB.lexp_ctx_cons ctx 0 (Some l1) Variable t1) + && conv_p' (DB.lexp_ctx_cons ctx (Some l1) Variable t1) (set_shift vs') e1 e2 | (Call (f1, args1), Call (f2, args2)) @@ -263,7 +263,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | ([], []) -> true | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2) -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_fields (DB.lexp_ctx_cons ctx 0 vd1 Variable t1) + && conv_fields (DB.lexp_ctx_cons ctx vd1 Variable t1) (set_shift vs) fields1 fields2 | _,_ -> false in @@ -275,7 +275,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = SMap.equal (conv_fields ctx vs) cases1 cases2 | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2) -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_args (DB.lexp_ctx_cons ctx 0 (Some l1) Variable t1) + && conv_args (DB.lexp_ctx_cons ctx (Some l1) Variable t1) (set_shift vs) args1 args2 | _,_ -> false in @@ -449,7 +449,7 @@ let rec check' erased ctx e = (lexp_defs_subst l S.identity defs) | Arrow (ak, v, t1, l, t2) -> (let k1 = check_type erased ctx t1 in - let nctx = DB.lexp_ctx_cons ctx 0 v Variable t1 in + let nctx = DB.lexp_ctx_cons ctx v Variable t1 in let k2 = check_type (DB.set_sink 1 erased) nctx t2 in match sort_compose ctx l ak k1 k2 with | SortResult k -> k @@ -561,8 +561,7 @@ let rec check' erased ctx e = * appears in type annotations. *) | (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) - (DB.lexp_ctx_cons ctx 0 - vdef Variable (mkSusp ftype s)) + (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) (S.cons (Var ((match vdef with Some vd -> vd | None -> (l, "_")), 0)) @@ -581,7 +580,7 @@ let rec check' erased ctx e = | Some (v, d) -> if diff <= 0 then U.msg_warning "TC" l "Redundant default clause"; - let nctx = (DB.lctx_extend ctx v (LetDef e) etype) in + let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in assert_type nctx d (mkSusp ret (S.shift 1)) (check (DB.set_sink 1 erased) nctx d) | None @@ -768,7 +767,7 @@ let rec get_type ctx e = | Arrow (ak, v, t1, l, t2) (* FIXME: Use `check` here but silencing errors? *) -> (let k1 = get_type ctx t1 in - let nctx = DB.lexp_ctx_cons ctx 0 v Variable t1 in + let nctx = DB.lexp_ctx_cons ctx v Variable t1 in let k2 = get_type nctx t2 in match sort_compose ctx l ak k1 k2 with | SortResult k -> k @@ -959,10 +958,10 @@ let ctx2tup ctx nctx = types) SMap.empty), cons_label), - List.mapi (fun i (oname, t) - -> (P.Aimplicit, Var (maybev oname, offset - i - 1))) + List.map (fun (oname, t) + -> (P.Aimplicit, Var (maybev oname, offset))) types) - | (DB.CVlet (oname, LetDef e, t, _) :: blocs) + | (DB.CVlet (oname, LetDef (_, e), t, _) :: blocs) -> Let (loc, [(maybev oname, mkSusp e (S.shift 1), t)], mk_lets_and_tup blocs ((oname, t) :: types)) | (DB.CVfix (defs, _) :: blocs)

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -1,6 +1,6 @@ (* unification.ml --- Unification of Lexp terms

-Copyright (C) 2016-2017 Free Software Foundation, Inc. +Copyright (C) 2016-2018 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -171,7 +171,7 @@ and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs -> if var_kind1 = var_kind2 then unify_and (unify' ltype1 ltype2 ctx vs) (unify' lexp1 lexp2 - (DB.lexp_ctx_cons ctx 0 v1 Variable ltype1) + (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs)) else None | (Arrow _, Imm _) -> None @@ -194,7 +194,7 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = -> if var_kind1 = var_kind2 then unify_and (unify' ltype1 ltype2 ctx vs) (unify' lexp1 lexp2 - (DB.lexp_ctx_cons ctx 0 (Some v1) Variable ltype1) + (DB.lexp_ctx_cons ctx (Some v1) Variable ltype1) (OL.set_shift vs)) else None | ((Lambda _, Var _)

View it on GitLab: https://gitlab.com/monnier/typer/compare/69659f54d60852dcd4775a9f3fc5d2594ca...