--- 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;