Commit 34cd89c1 authored by POTTIER Francois's avatar POTTIER Francois

Change [extend] to take [env] as its first argument.

parent c16bc3be
......@@ -2,8 +2,6 @@
TODO (REALLY):
extend should take env as its first argument.
In BindingFormsUnbound, implement [endo] and [iter2].
copy and avoid should use [endo], not [map].
......
......@@ -128,7 +128,7 @@ let rec typeof xenv env (t : nominal_term) : nominal_typ =
let env = extend_with_tevar env x (typeof xenv env t) in
typeof xenv env u
| TeTyAbs (a, t) ->
let _, xenv = KitExport.extend a xenv in
let xenv, _ = KitExport.extend xenv a in
TyForall (a, typeof xenv (extend_with_tyvar env a) t)
| TeTyApp (t, ty2) ->
let a, ty1 = as_forall xenv (typeof xenv env t) in
......
......@@ -40,14 +40,14 @@ type ('bn, 'term) abs =
class virtual ['self] iter = object (self : 'self)
method private virtual extend: 'bn -> 'env -> 'env
method private virtual extend: 'env -> 'bn -> 'env
method private visit_abs: 'term .
_ ->
('env -> 'term -> unit) ->
'env -> ('bn, 'term) abs -> unit
= fun _ visit_term env (x, t) ->
let env' = self#extend x env in
let env' = self#extend env x in
visit_term env' t
end
......@@ -58,14 +58,14 @@ end
class virtual ['self] iter2 = object (self : 'self)
method private virtual extend: 'bn1 -> 'bn2 -> 'env -> 'env
method private virtual extend: 'env -> 'bn1 -> 'bn2 -> 'env
method private visit_abs: 'term1 'term2 .
_ ->
('env -> 'term1 -> 'term2 -> 'z) ->
'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs -> 'z
= fun _ visit_term env (x1, t1) (x2, t2) ->
let env' = self#extend x1 x2 env in
let env' = self#extend env x1 x2 in
visit_term env' t1 t2
end
......@@ -76,15 +76,15 @@ end
class virtual ['self] map = object (self : 'self)
method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env
method private virtual extend: 'env -> 'bn1 -> 'env * 'bn2
method private visit_abs: 'term1 'term2 .
_ ->
('env -> 'term1 -> 'term2) ->
'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs
= fun _ visit_term env (x1, t1) ->
let x2, env' = self#extend x1 env in
let t2 = visit_term env' t1 in
let env, x2 = self#extend env x1 in
let t2 = visit_term env t1 in
x2, t2
end
......@@ -95,15 +95,15 @@ end
class virtual ['self] endo = object (self : 'self)
method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env
method private virtual extend: 'env -> 'bn1 -> 'env * 'bn2
method private visit_abs: 'term .
_ ->
('env -> 'term -> 'term) ->
'env -> ('bn, 'term) abs -> ('bn, 'term) abs
= fun _ visit_term env ((x1, t1) as this) ->
let x2, env' = self#extend x1 env in
let t2 = visit_term env' t1 in
let env, x2 = self#extend env x1 in
let t2 = visit_term env t1 in
if x1 == x2 && t1 == t2 then
this
else
......
......@@ -155,7 +155,7 @@ let check_recursive_permitted (penv : 'env penv) : unit =
class virtual ['self] map = object (self : 'self)
method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env
method private virtual extend: 'env -> 'bn1 -> 'env * 'bn2
method private virtual lookup: 'env -> 'bn1 -> 'bn2
(* [visit_abstraction] initializes an enriched environment using the
......@@ -179,7 +179,7 @@ class virtual ['self] map = object (self : 'self)
let env = !(penv.current) in
match penv.at_binder with
| Extend ->
let x2, env = self#extend x1 env in
let env, x2 = self#extend env x1 in
penv.current := env;
x2
| Lookup ->
......@@ -279,7 +279,7 @@ end
class virtual ['self] iter = object (self : 'self)
method private virtual extend: 'bn -> 'env -> 'env
method private virtual extend: 'env -> 'bn -> 'env
method private visit_abstraction: 'env 'p .
('env penv -> 'p -> unit) ->
......@@ -294,7 +294,7 @@ class virtual ['self] iter = object (self : 'self)
let env = !(penv.current) in
match penv.at_binder with
| Extend ->
let env = self#extend x env in
let env = self#extend env x in
penv.current := env
| Lookup ->
()
......
......@@ -11,15 +11,15 @@ let empty =
let lookup =
KitCopy.lookup
let extend bad x env =
let extend bad env x =
(* If [x] is bad, it must be renamed. Otherwise, keep it. *)
if Atom.Set.mem x bad then
KitCopy.extend x env
KitCopy.extend env x
else
x, env
env, x
class ['self] map bad = object (_ : 'self)
method private extend x env = extend bad x env
method private extend env x = extend bad env x
method private lookup = lookup
method private visit_'fn = lookup
end
......@@ -6,7 +6,7 @@ exception Shadowing of Atom.t
class ['self] iter = object (_ : 'self)
method private extend x env =
method private extend env x =
if Atom.Set.mem x env then
(* There is shadowing: the atom [x] is already in scope. *)
raise (Shadowing x)
......
......@@ -8,7 +8,7 @@ class ['self] iter = object (_ : 'self)
method accu = accu (* must be public *)
(* A bound atom is added to the accumulator when its scope is entered. *)
method private extend x () =
method private extend () x =
accu <- Atom.Set.add x accu
method private visit_'fn () _x =
......
......@@ -15,14 +15,14 @@ let lookup env x =
(* Outside of its domain, the renaming acts as the identity. *)
x
let extend x env =
let extend env x =
(* Generate a fresh copy of [x]. *)
let x' = Atom.copy x in
(* Extend [env] when descending in the body. *)
x', Atom.Map.add x x' env
Atom.Map.add x x' env, x'
class ['self] map = object (_ : 'self)
method private extend x env = extend x env
method private extend = extend
method private lookup = lookup
method private visit_'fn = lookup
end
......@@ -28,7 +28,7 @@ let lookup (m : m) (x : Atom.t) : status =
let extend (m : m) (n : int) (x : Atom.t) : m =
Atom.Map.add x n m
let extend x1 x2 (m1, m2, n) =
let extend (m1, m2, n) x1 x2 =
let m1 = extend m1 n x1
and m2 = extend m2 n x2
and n = n + 1 in
......
......@@ -23,7 +23,7 @@ let next env hint : int =
with Not_found ->
0
let extend x env =
let extend env x =
(* We must pick a suitable string to stand for the atom [x]. We must
pick a string that does not appear in the image through [env] of
the free atoms of [body]. However, at this point, we do not have
......@@ -39,7 +39,7 @@ let extend x env =
graph = Atom.Map.add x s env.graph;
codomain = StringMap.add hint (i+1) env.codomain;
} in
s, env
env, s
let lookup env a =
try
......
......@@ -23,7 +23,7 @@
is free, then the method [visit_free] is invoked. *)
class virtual ['self] free = object (self : 'self)
method private extend = Atom.Set.add
method private extend env x = Atom.Set.add x env
method private visit_'fn env x =
if not (Atom.Set.mem x env) then
self#visit_free x
......
......@@ -8,7 +8,7 @@ class ['self] iter = object (_ : 'self)
val mutable accu = Atom.Set.empty
(* A bound atom is added to the accumulator when its scope is entered. *)
method private extend x () =
method private extend () x =
if Atom.Set.mem x accu then
raise (Atom.Set.NonDisjointUnion x)
else
......
......@@ -13,10 +13,10 @@ type env =
let empty =
StringMap.empty
let extend (x : string) (env : env) : Atom.t * env =
let extend (env : env) (x : string) : env * Atom.t =
let a = Atom.fresh x in
let env = StringMap.add x a env in
a, env
env, a
exception Unbound of string
......@@ -27,7 +27,7 @@ let lookup (env : env) (x : string) : Atom.t =
raise (Unbound x)
class ['self] map = object (_ : 'self)
method private extend x env = extend x env
method private extend = extend
method private lookup = lookup
method private visit_'fn = lookup
end
......@@ -6,7 +6,7 @@ let lookup _env x =
Atom.show x
class ['self] map = object (_ : 'self)
method private extend x env = Atom.show x, env
method private extend env x = env, Atom.show x
method private lookup = lookup
method private visit_'fn = lookup
end
......@@ -7,7 +7,7 @@
type 'thing env =
'thing Atom.Map.t
let extend x env =
let extend env x =
(* We would like to check that [x] is fresh for [env], but can only
perform the domain check. The codomain check cannot be performed
since the type of things is abstract here. *)
......@@ -15,7 +15,7 @@ let extend x env =
(* Since [x] is fresh for [env], no capture is possible. Thus, no
freshening of the bound name is required. Thus, we can keep the
substitution [env], unchanged, under the binder. *)
x, env
env, x
let lookup env x =
try
......
......@@ -23,14 +23,14 @@ end) = struct
let empty =
Map.empty, 0
let extend x (m, n : env) =
let extend (m, n : env) x =
(* Increment the current de Bruijn level [n]. *)
let n = n + 1 in
(* Record a mapping of the name [x] to the de Bruijn level [n],
so if [x] was looked up right now, it would receive level [n],
therefore index [0]. *)
let m = Map.add x n m in
(), (m, n)
(m, n), ()
let lookup (m, n : env) x =
try
......
......@@ -5,6 +5,6 @@
(* The type of the environment is undetermined. *)
class ['self] iter = object (_ : 'self)
method private extend _x env = env
method private extend env _x = env
method private visit_'fn _env _x = ()
end
......@@ -17,13 +17,13 @@ module type INPUT = sig
is desired. *)
class virtual ['self] iter : object ('self)
method private virtual extend : 'bn -> 'env -> 'env
method private virtual extend : 'env -> 'bn -> 'env
method private virtual visit_'fn : 'env -> 'fn -> _
method visit_term : 'env -> ('bn, 'fn) term -> unit
end
class virtual ['self] map : object ('self)
method private virtual extend : 'bn1 -> 'env -> 'bn2 * 'env
method private virtual extend : 'env -> 'bn1 -> 'env * 'bn2
method private virtual lookup : 'env -> 'bn1 -> 'bn2
method private virtual visit_'fn : 'env -> 'fn1 -> 'fn2
method visit_term : 'env -> ('bn1, 'fn1) term -> ('bn2, 'fn2) term
......@@ -31,14 +31,14 @@ module type INPUT = sig
end
class virtual ['self] endo : object ('self)
method private virtual extend : 'bn -> 'env -> 'bn * 'env
method private virtual extend : 'env -> 'bn -> 'env * 'bn
method private virtual visit_'fn : 'env -> 'fn -> 'fn
method visit_term : 'env -> ('bn, 'fn) term -> ('bn, 'fn) term
method private visit_TVar : 'env -> ('bn, 'fn) term -> 'fn -> ('bn, 'fn) term
end
class virtual ['self] iter2 : object ('self)
method private virtual extend : 'bn1 -> 'bn2 -> 'env -> 'env
method private virtual extend : 'env -> 'bn1 -> 'bn2 -> 'env
method private virtual visit_'fn : 'env -> 'fn1 -> 'fn2 -> _
method visit_term : 'env -> ('bn1, 'fn1) term -> ('bn2, 'fn2) term -> unit
end
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment