Commit 848abd59 authored by POTTIER Francois's avatar POTTIER Francois

Parameterize [subst] over [copy].

parent 14882475
......@@ -14,9 +14,6 @@ System F demo:
System F-type-term:
deal with both kinds of variables
Implement a subst that does not copy the grafted term?
Or parameterize subst over the copy operation that needs to be performed when grafting?
Implement fused copy/subst, fused avoid/subst?
Implement a kit that composes two kits, so as to easily implement fused operations.
Composition of classes? Or composition of kit objects? ...
......
......@@ -10,6 +10,9 @@ open T
let ( ** ) = Atom.Set.union
let subst1 =
subst_TVar_term1 copy_term
(* -------------------------------------------------------------------------- *)
(* [interval i j] constructs a list representation of the semi-open interval
......@@ -219,34 +222,34 @@ let () =
()
| x ->
let u = generate_nominal atoms size_of_u in
let t' = subst_term_term1 u x t in
let t' = subst1 u x t in
assert (guq_term t');
assert (Atom.Set.equal
(fa_term t')
(fa_term u ** Atom.Set.remove x (fa_term t))
);
assert (t' = subst_term_term1 u x t);
assert (t' = subst1 u x t);
assert (guq_term (TLambda (x, t)));
(* subst_term_term1 u x (TLambda (x, t)) = TLambda (x, t) *)
(* subst1 u x (TLambda (x, t)) = TLambda (x, t) *)
(* cannot be checked as these are illegal arguments to substitution *)
begin match t with
| TVar _ -> assert false
| TLambda (y, t) ->
assert (subst_term_term1 u x (TLambda (y, t)) =
TLambda (y, subst_term_term1 u x t))
assert (subst1 u x (TLambda (y, t)) =
TLambda (y, subst1 u x t))
| TApp (t1, t2) ->
assert (subst_term_term1 u x (TApp (t1, t2)) =
TApp (subst_term_term1 u x t1, subst_term_term1 u x t2))
assert (subst1 u x (TApp (t1, t2)) =
TApp (subst1 u x t1, subst1 u x t2))
end
);
let x = Atom.freshh "x"
and y = Atom.freshh "y" in
let u = generate_nominal atoms size_of_u in
assert (subst_term_term1 u x (TVar x) = u);
assert (subst_term_term1 u x (TVar y) = TVar y);
assert (subst1 u x (TVar x) = u);
assert (subst1 u x (TVar y) = TVar y);
on_guq_nominal_terms (fun t ->
assert (subst_term_term1 u x t = t);
assert (subst_term_term1 u x t == t) (* note physical equality *)
assert (subst1 u x t = t);
assert (subst1 u x t == t) (* note physical equality *)
);
(* Test that [equiv] distinguishes certain terms. *)
assert (not (TVar x = TVar y));
......@@ -399,7 +402,7 @@ let () =
evaluate print_fa
let print_subst1 u x t =
let t' = subst_term_term1 u x t in
let t' = subst1 u x t in
printf "substituting %a for %a in %a = ...\n %a\n%s\n%!"
nhprint u
Atom.print x
......
......@@ -110,6 +110,6 @@ __EQUIV
EQUIV(typ)
EQUIV(term)
__SUBST(typ, TyVar)
SUBST(typ, typ)
SUBST(typ, term)
__SUBST(TyVar)
SUBST(TyVar, typ)
SUBST(TyVar, term)
......@@ -59,7 +59,7 @@ let unfold ty =
assert (Atom.Set.disjoint (fa_typ ty) (ba_typ body));
(* By the above, the bound names of [body] are disjoint with the
domain and codomain of the substitution [ty/a]. *)
subst_typ_typ1 ty a body
subst_TyVar_typ1 copy_typ ty a body
| _ ->
assert false
......@@ -135,7 +135,7 @@ let rec typeof env (t : nominal_term) : nominal_typ =
assert (not (Atom.Set.mem a (ba_typ ty1)));
(* We have ba(ty1) # fa(ty2) because fa(ty2) is a subset of dom(env), that is,
env.tyvars, and typeof has the postcondition ba(\result) # env.tyvars. *)
subst_typ_typ1 ty2 a ty1
subst_TyVar_typ1 (fun ty -> ty) ty2 a ty1
| TePair (t1, t2) ->
TyProduct (typeof env t1, typeof env t2)
| TeProj (i, t) ->
......
......@@ -284,29 +284,26 @@
in the domain of [sigma], which means that we can go down into [t] and apply
[sigma] to every variable. *)
(* The GUH is preserved by copying the things that are grafted into [t]. Thus,
it is not even necessary that [sigma] and [t] be disjoint, or that the
things in the codomain of [sigma] be pairwise disjoint. One should note,
however, that the result of the substitution is not disjoint with [t], so
one should no longer use [t] after the substitution (or, one should apply
the substitution to a copy). *)
#define SUBST_CLASS(thing) CONCAT(__subst_, thing)
#define SUBST_FUN(thing, term) CONCAT(subst_, CONCAT(thing, CONCAT(_, term)))
#define SUBST_FUN1(thing, term) CONCAT(SUBST_FUN(thing, term), 1)
#define __SUBST(thing, Var) \
class SUBST_CLASS(thing) = object \
(* Global uniqueness can be preserved, if desired, by copying the things that
are grafted into [t]. The user decides which [copy] operation should be used.
It could be [copy_thing], or it could be the identity. *)
#define SUBST_CLASS(Var) CONCAT(__subst_, Var)
#define SUBST_FUN(Var, term) CONCAT(subst_, CONCAT(Var, CONCAT(_, term)))
#define SUBST_FUN1(Var, term) CONCAT(SUBST_FUN(Var, term), 1)
#define __SUBST(Var) \
class SUBST_CLASS(Var) copy = object \
inherit [_] endo (* we could also use [map] *) \
inherit [_] KitSubst.map \
method! private VISIT(Var) sigma this x = \
KitSubst.apply COPY_FUN(thing) sigma this x \
KitSubst.apply copy sigma this x \
end \
#define SUBST(thing, term) \
let SUBST_FUN(thing, term) sigma t = \
new SUBST_CLASS(thing) # VISIT(term) sigma t \
let SUBST_FUN1(thing, term) u x t = \
SUBST_FUN(thing, term) (Atom.Map.singleton x u) t \
#define SUBST(Var, term) \
let SUBST_FUN(Var, term) copy sigma t = \
(new SUBST_CLASS(Var) copy) # VISIT(term) sigma t \
let SUBST_FUN1(Var, term) copy u x t = \
SUBST_FUN(Var, term) copy (Atom.Map.singleton x u) t \
(* -------------------------------------------------------------------------- *)
......@@ -68,8 +68,9 @@ module Make (Term : ToolboxInput.INPUT) = struct
__EQUIV
EQUIV(term)
__SUBST(term, TVar)
SUBST(term, term)
(* Mnemonic: Substitute for variables in terms. *)
__SUBST(TVar)
SUBST(TVar, term)
(* -------------------------------------------------------------------------- *)
......
......@@ -44,7 +44,11 @@ module Make (Term : ToolboxInput.INPUT) : sig
val equiv_term: nominal_term -> nominal_term -> bool
val subst_term_term : nominal_term Atom.Map.t -> nominal_term -> nominal_term
val subst_term_term1: nominal_term -> Atom.t -> nominal_term -> nominal_term
val subst_TVar_term:
(nominal_term -> nominal_term) ->
nominal_term Atom.Map.t -> nominal_term -> nominal_term
val subst_TVar_term1:
(nominal_term -> nominal_term) ->
nominal_term -> Atom.t -> nominal_term -> nominal_term
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