TFL/usyntax.sml

--- a/TFL/usyntax.sml	Fri Sep 29 16:00:04 2000 +0200
+++ b/TFL/usyntax.sml	Fri Sep 29 18:02:24 2000 +0200
@@ -44,7 +44,7 @@
   (* Destruction routines *)
   val dest_const: term -> {Name : string, Ty : typ}
   val dest_comb : term -> {Rator : term, Rand : term}
-  val dest_abs  : term -> {Bvar : term, Body : term}
+  val dest_abs  : string list -> term -> {Bvar : term, Body : term} * string list
   val dest_eq     : term -> {lhs : term, rhs : term}
   val dest_imp    : term -> {ant : term, conseq : term}
   val dest_forall : term -> {Bvar : term, Body : term}
@@ -53,7 +53,7 @@
   val dest_conj   : term -> {conj1 : term, conj2 : term}
   val dest_disj   : term -> {disj1 : term, disj2 : term}
   val dest_pair   : term -> {fst : term, snd : term}
-  val dest_pabs   : term -> {varstruct : term, body : term}
+  val dest_pabs   : string list -> term -> {varstruct : term, body : term, used : string list}
 
   val lhs   : term -> term
   val rhs   : term -> term
@@ -243,11 +243,13 @@
 fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
   | dest_comb _ =  raise USYN_ERR{func = "dest_comb", mesg = "not a comb"};
 
-fun dest_abs(a as Abs(s,ty,M)) = 
-     let val v = Free(s,ty)
-     in {Bvar = v, Body = betapply (a,v)}
+fun dest_abs used (a as Abs(s, ty, M)) = 
+     let
+       val s' = variant used s;
+       val v = Free(s', ty);
+     in ({Bvar = v, Body = betapply (a,v)}, s'::used)
      end
-  | dest_abs _ =  raise USYN_ERR{func = "dest_abs", mesg = "not an abstraction"};
+  | dest_abs _ _ =  raise USYN_ERR{func = "dest_abs", mesg = "not an abstraction"};
 
 fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
   | dest_eq _ = raise USYN_ERR{func = "dest_eq", mesg = "not an equality"};
@@ -255,10 +257,10 @@
 fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
   | dest_imp _ = raise USYN_ERR{func = "dest_imp", mesg = "not an implication"};
 
-fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a
+fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a)
   | dest_forall _ = raise USYN_ERR{func = "dest_forall", mesg = "not a forall"};
 
-fun dest_exists(Const("Ex",_) $ (a as Abs _)) = dest_abs a
+fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a)
   | dest_exists _ = raise USYN_ERR{func = "dest_exists", mesg="not an existential"};
 
 fun dest_neg(Const("not",_) $ M) = M
@@ -284,16 +286,16 @@
 local  fun ucheck t = (if #Name(dest_const t) = "split" then t
                        else raise Match)
 in
-fun dest_pabs tm =
-   let val {Bvar,Body} = dest_abs tm
-   in {varstruct = Bvar, body = Body}
+fun dest_pabs used tm =
+   let val ({Bvar,Body}, used') = dest_abs used tm
+   in {varstruct = Bvar, body = Body, used = used'}
    end 
     handle (* FIXME do not handle _ !!! *)
      _ => let val {Rator,Rand} = dest_comb tm
               val _ = ucheck Rator
-              val {varstruct = lv,body} = dest_pabs Rand
-              val {varstruct = rv,body} = dest_pabs body
-          in {varstruct = mk_pair{fst = lv, snd = rv}, body = body}
+              val {varstruct = lv, body, used = used'} = dest_pabs used Rand
+              val {varstruct = rv, body, used = used''} = dest_pabs used' body
+          in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''}
           end
 end;
 
@@ -311,7 +313,7 @@
 val is_conj   = can dest_conj
 val is_disj   = can dest_disj
 val is_pair   = can dest_pair
-val is_pabs   = can dest_pabs
+val is_pabs   = can (dest_pabs [])
 
 
 (* Construction of a cterm from a list of Terms *)
@@ -335,7 +337,7 @@
    end;
 
 fun strip_abs(tm as Abs _) =
-       let val {Bvar,Body} = dest_abs tm
+       let val ({Bvar,Body}, _) = dest_abs [] tm
            val (bvs, core) = strip_abs Body
        in (Bvar::bvs, core)
        end