# HG changeset patch
# User wenzelm
# Date 965422773 -7200
# Node ID b79b002f32aeff65479f97444a077260bb121f02
# Parent  a60b0be5ee968826ffcffc768fb436b9fc860366
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;

diff -r a60b0be5ee96 -r b79b002f32ae src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Aug 04 22:59:08 2000 +0200
+++ b/src/Pure/term.ML	Fri Aug 04 22:59:33 2000 +0200
@@ -1,6 +1,6 @@
-(*  Title: 	Pure/term.ML
+(*  Title:      Pure/term.ML
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   Cambridge University 1992
 
 Simply typed lambda-calculus: types, terms, and basic operations.
@@ -179,6 +179,9 @@
   val term_ord: term * term -> order
   val terms_ord: term list * term list -> order
   val termless: term * term -> bool
+  val dummy_patternN: string
+  val no_dummy_patterns: term -> term
+  val replace_dummy_patterns: int * term -> int * term
 end;
 
 structure Term: TERM =
@@ -195,7 +198,7 @@
 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
 datatype typ = Type  of string * typ list
              | TFree of string * sort
-	     | TVar  of indexname * sort;
+             | TVar  of indexname * sort;
 
 (*Terms.  Bound variables are indicated by depth number.
   Free variables, (scheme) variables and constants have names.
@@ -296,19 +299,19 @@
 fun type_of1 (Ts, Const (_,T)) = T
   | type_of1 (Ts, Free  (_,T)) = T
   | type_of1 (Ts, Bound i) = (nth_elem (i,Ts)  
-  	handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i]))
+        handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i]))
   | type_of1 (Ts, Var (_,T)) = T
   | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
   | type_of1 (Ts, f$u) = 
       let val U = type_of1(Ts,u)
           and T = type_of1(Ts,f)
       in case T of
-	    Type("fun",[T1,T2]) =>
-	      if T1=U then T2  else raise TYPE
-	            ("type_of: type mismatch in application", [T1,U], [f$u])
-	  | _ => raise TYPE 
-		    ("type_of: function type is expected in application",
-		     [T,U], [f$u])
+            Type("fun",[T1,T2]) =>
+              if T1=U then T2  else raise TYPE
+                    ("type_of: type mismatch in application", [T1,U], [f$u])
+          | _ => raise TYPE 
+                    ("type_of: function type is expected in application",
+                     [T,U], [f$u])
       end;
 
 fun type_of t : typ = type_of1 ([],t);
@@ -316,12 +319,12 @@
 (*Determines the type of a term, with minimal checking*)
 fun fastype_of1 (Ts, f$u) = 
     (case fastype_of1 (Ts,f) of
-	Type("fun",[_,T]) => T
-	| _ => raise TERM("fastype_of: expected function type", [f$u]))
+        Type("fun",[_,T]) => T
+        | _ => raise TERM("fastype_of: expected function type", [f$u]))
   | fastype_of1 (_, Const (_,T)) = T
   | fastype_of1 (_, Free (_,T)) = T
   | fastype_of1 (Ts, Bound i) = (nth_elem(i,Ts)
-  	 handle LIST _ => raise TERM("fastype_of: Bound", [Bound i]))
+         handle LIST _ => raise TERM("fastype_of: Bound", [Bound i]))
   | fastype_of1 (_, Var (_,T)) = T 
   | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
 
@@ -423,7 +426,7 @@
 
 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
 fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
-		(a,T) :: strip_all_vars t 
+                (a,T) :: strip_all_vars t 
   | strip_all_vars t  =  [] : (string*typ) list;
 
 (*increments a term's non-local bound variables
@@ -432,7 +435,7 @@
      lev is  level at which a bound variable is considered 'loose'*)
 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 
   | incr_bv (inc, lev, Abs(a,T,body)) =
-	Abs(a, T, incr_bv(inc,lev+1,body))
+        Abs(a, T, incr_bv(inc,lev+1,body))
   | incr_bv (inc, lev, f$t) = 
       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   | incr_bv (inc, lev, u) = u;
@@ -444,10 +447,10 @@
 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
    (Bound 0) is loose at level 0 *)
 fun add_loose_bnos (Bound i, lev, js) = 
-	if i<lev then js  else  (i-lev) ins_int js
+        if i<lev then js  else  (i-lev) ins_int js
   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   | add_loose_bnos (f$t, lev, js) =
-	add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
+        add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
   | add_loose_bnos (_, _, js) = js;
 
 fun loose_bnos t = add_loose_bnos (t, 0, []);
@@ -467,30 +470,30 @@
 (*Substitute arguments for loose bound variables.
   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
-	and the appropriate call is  subst_bounds([b,a], c) .
+        and the appropriate call is  subst_bounds([b,a], c) .
   Loose bound variables >=n are reduced by "n" to
      compensate for the disappearance of lambdas.
 *)
 fun subst_bounds (args: term list, t) : term = 
   let val n = length args;
       fun subst (t as Bound i, lev) =
- 	   (if i<lev then  t    (*var is locally bound*)
-	    else  incr_boundvars lev (List.nth(args, i-lev))
-		    handle Subscript => Bound(i-n)  (*loose: change it*))
-	| subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
-	| subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
-	| subst (t,lev) = t
+           (if i<lev then  t    (*var is locally bound*)
+            else  incr_boundvars lev (List.nth(args, i-lev))
+                    handle Subscript => Bound(i-n)  (*loose: change it*))
+        | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
+        | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
+        | subst (t,lev) = t
   in   case args of [] => t  | _ => subst (t,0)  end;
 
 (*Special case: one argument*)
 fun subst_bound (arg, t) : term = 
   let fun subst (t as Bound i, lev) =
- 	    if i<lev then  t    (*var is locally bound*)
-	    else  if i=lev then incr_boundvars lev arg
-		           else Bound(i-1)  (*loose: change it*)
-	| subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
-	| subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
-	| subst (t,lev) = t
+            if i<lev then  t    (*var is locally bound*)
+            else  if i=lev then incr_boundvars lev arg
+                           else Bound(i-1)  (*loose: change it*)
+        | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
+        | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
+        | subst (t,lev) = t
   in  subst (t,0)  end;
 
 (*beta-reduce if possible, else form application*)
@@ -572,9 +575,9 @@
   Terms must be NORMAL.  Treats all Vars as distinct. *)
 fun could_unify (t,u) =
   let fun matchrands (f$t, g$u) = could_unify(t,u) andalso  matchrands(f,g)
-	| matchrands _ = true
+        | matchrands _ = true
   in case (head_of t , head_of u) of
-	(_, Var _) => true
+        (_, Var _) => true
       | (Var _, _) => true
       | (Const(a,_), Const(b,_)) =>  a=b andalso matchrands(t,u)
       | (Free(a,_), Free(b,_)) =>  a=b andalso matchrands(t,u)
@@ -588,11 +591,11 @@
 fun subst_free [] = (fn t=>t)
   | subst_free pairs =
       let fun substf u = 
-	    case gen_assoc (op aconv) (pairs, u) of
-		Some u' => u'
-	      | None => (case u of Abs(a,T,t) => Abs(a, T, substf t)
-				 | t$u' => substf t $ substf u'
-				 | _ => u)
+            case gen_assoc (op aconv) (pairs, u) of
+                Some u' => u'
+              | None => (case u of Abs(a,T,t) => Abs(a, T, substf t)
+                                 | t$u' => substf t $ substf u'
+                                 | _ => u)
       in  substf  end;
 
 (*a total, irreflexive ordering on index names*)
@@ -606,8 +609,8 @@
   let fun abst (lev,u) = if (v aconv u) then (Bound lev) else
       (case u of
           Abs(a,T,t) => Abs(a, T, abst(lev+1, t))
-	| f$rand => abst(lev,f) $ abst(lev,rand)
-	| _ => u)
+        | f$rand => abst(lev,f) $ abst(lev,rand)
+        | _ => u)
   in  abst(0,body)  end;
 
 
@@ -634,16 +637,16 @@
 fun subst_atomic [] t = t : term
   | subst_atomic (instl: (term*term) list) t =
       let fun subst (Abs(a,T,body)) = Abs(a, T, subst body)
-	    | subst (f$t') = subst f $ subst t'
-	    | subst t = (case assoc(instl,t) of
-		           Some u => u  |  None => t)
+            | subst (f$t') = subst f $ subst t'
+            | subst t = (case assoc(instl,t) of
+                           Some u => u  |  None => t)
       in  subst t  end;
 
 (*Substitute for type Vars in a type*)
 fun typ_subst_TVars iTs T = if null iTs then T else
   let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
-	| subst(T as TFree _) = T
-	| subst(T as TVar(ixn,_)) =
+        | subst(T as TFree _) = T
+        | subst(T as TVar(ixn,_)) =
             (case assoc(iTs,ixn) of None => T | Some(U) => U)
   in subst T end;
 
@@ -704,10 +707,10 @@
   let val zero = ord"0"
       val limit = zero+radix
       fun scan (num,[]) = (num,[])
-	| scan (num, c::cs) =
-	      if  zero <= ord c  andalso  ord c < limit
-	      then scan(radix*num + ord c - zero, cs)
-	      else (num, c::cs)
+        | scan (num, c::cs) =
+              if  zero <= ord c  andalso  ord c < limit
+              then scan(radix*num + ord c - zero, cs)
+              else (num, c::cs)
   in  scan(0,cs)  end;
 
 fun read_int cs = read_radixint (10, cs);
@@ -752,10 +755,10 @@
   | add_term_consts (_, cs) = cs;
 
 fun exists_Const P t = let
-	fun ex (Const c      ) = P c
-	|   ex (t $ u        ) = ex t orelse ex u
-	|   ex (Abs (_, _, t)) = ex t
-	|   ex _               = false
+        fun ex (Const c      ) = P c
+        |   ex (t $ u        ) = ex t orelse ex u
+        |   ex (Abs (_, _, t)) = ex t
+        |   ex _               = false
     in ex t end;
 
 fun exists_subterm P =
@@ -831,7 +834,7 @@
 
 fun add_typ_ixns(ixns,Type(_,Ts)) = foldl add_typ_ixns (ixns,Ts)
   | add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns 
-				     else ixns@[ixn]
+                                     else ixns@[ixn]
   | add_typ_ixns(ixns,TFree(_)) = ixns;
 
 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
@@ -856,9 +859,9 @@
 fun insert_aterm (t,us) =
   let fun inserta [] = [t]
         | inserta (us as u::us') = 
-	      if atless(t,u) then t::us
-	      else if t=u then us (*duplicate*)
-	      else u :: inserta(us')
+              if atless(t,u) then t::us
+              else if t=u then us (*duplicate*)
+              else u :: inserta(us')
   in  inserta us  end;
 
 (*Accumulates the Vars in the term, suppressing duplicates*)
@@ -888,7 +891,7 @@
 (* renames and reverses the strings in vars away from names *)
 fun rename_aTs names vars : (string*typ)list =
   let fun rename_aT (vars,(a,T)) =
-		(variant (map #1 vars @ names) a, T) :: vars
+                (variant (map #1 vars @ names) a, T) :: vars
   in foldl rename_aT ([],vars) end;
 
 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
@@ -980,8 +983,8 @@
 (*Substitute for type Vars in a type, version using Vartab*)
 fun typ_subst_TVars_Vartab iTs T = if Vartab.is_empty iTs then T else
   let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
-	| subst(T as TFree _) = T
-	| subst(T as TVar(ixn, _)) =
+        | subst(T as TFree _) = T
+        | subst(T as TVar(ixn, _)) =
             (case Vartab.lookup (iTs, ixn) of None => T | Some(U) => U)
   in subst T end;
 
@@ -1015,15 +1018,15 @@
       val tylist = Symtab.lookup_multi (!memo_types, tag)
   in  
       case find_type (T,tylist) of
-	Some T' => T'
+        Some T' => T'
       | None => 
-	    let val T' =
-		case T of
-		    Type (a,Ts) => Type (a, map compress_type Ts)
-		  | _ => T
-	    in  memo_types := Symtab.update ((tag, T'::tylist), !memo_types);
-		T
-	    end
+            let val T' =
+                case T of
+                    Type (a,Ts) => Type (a, map compress_type Ts)
+                  | _ => T
+            in  memo_types := Symtab.update ((tag, T'::tylist), !memo_types);
+                T
+            end
   end
   handle Match =>
       let val Type (a,Ts) = T
@@ -1048,17 +1051,32 @@
   | share_term (Abs (a,T,u)) = Abs (a, T, share_term u)
   | share_term t =
       let val tag = const_tag t
-	  val ts = Symtab.lookup_multi (!memo_terms, tag)
+          val ts = Symtab.lookup_multi (!memo_terms, tag)
       in 
-	  case find_term (t,ts) of
-	      Some t' => t'
-	    | None => (memo_terms := Symtab.update ((tag, t::ts), !memo_terms);
-		       t)
+          case find_term (t,ts) of
+              Some t' => t'
+            | None => (memo_terms := Symtab.update ((tag, t::ts), !memo_terms);
+                       t)
       end;
 
 val compress_term = share_term o map_term_types compress_type;
 
 
+(* dummy patterns *)
+
+val dummy_patternN = "dummy_pattern";
+
+fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
+  | is_dummy_pattern _ = false;
+
+fun no_dummy_patterns tm =
+  if not (foldl_aterms (fn (b, t) => b orelse is_dummy_pattern t) (false, tm)) then tm
+  else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
+
+val replace_dummy_patterns = foldl_map_aterms (fn (i, t) =>
+  if is_dummy_pattern t then (i + 1, Var (("_dummy_", i), fastype_of t)) else (i, t));
+
+
 end;