--- a/src/Pure/ROOT Fri Nov 21 13:18:56 2014 +0100
+++ b/src/Pure/ROOT Fri Nov 21 18:14:39 2014 +0100
@@ -230,7 +230,9 @@
"item_net.ML"
"library.ML"
"logic.ML"
+ "more_pattern.ML"
"more_thm.ML"
+ "more_unify.ML"
"morphism.ML"
"name.ML"
"net.ML"
--- a/src/Pure/ROOT.ML Fri Nov 21 13:18:56 2014 +0100
+++ b/src/Pure/ROOT.ML Fri Nov 21 18:14:39 2014 +0100
@@ -183,6 +183,8 @@
use "theory.ML";
use "proofterm.ML";
use "thm.ML";
+use "more_pattern.ML";
+use "more_unify.ML";
use "more_thm.ML";
use "facts.ML";
use "global_theory.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/more_pattern.ML Fri Nov 21 18:14:39 2014 +0100
@@ -0,0 +1,135 @@
+(* Title: Pure/more_pattern.ML
+ Author: Tobias Nipkow, TU Muenchen
+ Author: Stefan Berghofer, TU Muenchen
+
+Add-ons to Higher-Order Patterns, outside the inference kernel.
+*)
+
+signature PATTERN =
+sig
+ include PATTERN
+ val matches: theory -> term * term -> bool
+ val matchess: theory -> term list * term list -> bool
+ val equiv: theory -> term * term -> bool
+ val matches_subterm: theory -> term * term -> bool
+ val first_order: term -> bool
+ val pattern: term -> bool
+ val match_rew: theory -> term -> term * term -> (term * term) option
+ val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
+ val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term
+end;
+
+structure Pattern: PATTERN =
+struct
+
+fun matches thy po =
+ (Pattern.match thy po (Vartab.empty, Vartab.empty); true) handle Pattern.MATCH => false;
+
+fun matchess thy (ps, os) =
+ length ps = length os andalso
+ ((fold (Pattern.match thy) (ps ~~ os) (Vartab.empty, Vartab.empty); true)
+ handle Pattern.MATCH => false);
+
+fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
+
+
+(* Does pat match a subterm of obj? *)
+fun matches_subterm thy (pat, obj) =
+ let
+ fun msub bounds obj = matches thy (pat, obj) orelse
+ (case obj of
+ Abs (x, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
+ | t $ u => msub bounds t orelse msub bounds u
+ | _ => false)
+ in msub 0 obj end;
+
+fun first_order (Abs (_, _, t)) = first_order t
+ | first_order (t $ u) = first_order t andalso first_order u andalso not (is_Var t)
+ | first_order _ = true;
+
+fun pattern (Abs (_, _, t)) = pattern t
+ | pattern t =
+ let val (head, args) = strip_comb t in
+ if is_Var head then
+ forall is_Bound args andalso not (has_duplicates (op aconv) args)
+ else forall pattern args
+ end;
+
+
+(* rewriting -- simple but fast *)
+
+fun match_rew thy tm (tm1, tm2) =
+ let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
+ SOME (Envir.subst_term (Pattern.match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
+ handle Pattern.MATCH => NONE
+ end;
+
+fun gen_rewrite_term bot thy rules procs tm =
+ let
+ val skel0 = Bound 0;
+
+ fun variant_absfree bounds (x, T, t) =
+ let
+ val (x', t') = Term.dest_abs (Name.bound bounds, T, t);
+ fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
+ in (abs, t') end;
+
+ fun rew (Abs (_, _, body) $ t) = SOME (subst_bound (t, body), skel0)
+ | rew tm =
+ (case get_first (match_rew thy tm) rules of
+ NONE => Option.map (rpair skel0) (get_first (fn p => p tm) procs)
+ | x => x);
+
+ fun rew_sub r bounds skel (tm1 $ tm2) = (case tm1 of
+ Abs (_, _, body) =>
+ let val tm' = subst_bound (tm2, body)
+ in SOME (the_default tm' (rew_sub r bounds skel0 tm')) end
+ | _ =>
+ let val (skel1, skel2) = (case skel of
+ skel1 $ skel2 => (skel1, skel2)
+ | _ => (skel0, skel0))
+ in case r bounds skel1 tm1 of
+ SOME tm1' => (case r bounds skel2 tm2 of
+ SOME tm2' => SOME (tm1' $ tm2')
+ | NONE => SOME (tm1' $ tm2))
+ | NONE => (case r bounds skel2 tm2 of
+ SOME tm2' => SOME (tm1 $ tm2')
+ | NONE => NONE)
+ end)
+ | rew_sub r bounds skel (Abs body) =
+ let
+ val (abs, tm') = variant_absfree bounds body;
+ val skel' = (case skel of Abs (_, _, skel') => skel' | _ => skel0)
+ in case r (bounds + 1) skel' tm' of
+ SOME tm'' => SOME (abs tm'')
+ | NONE => NONE
+ end
+ | rew_sub _ _ _ _ = NONE;
+
+ fun rew_bot bounds (Var _) _ = NONE
+ | rew_bot bounds skel tm = (case rew_sub rew_bot bounds skel tm of
+ SOME tm1 => (case rew tm1 of
+ SOME (tm2, skel') => SOME (the_default tm2 (rew_bot bounds skel' tm2))
+ | NONE => SOME tm1)
+ | NONE => (case rew tm of
+ SOME (tm1, skel') => SOME (the_default tm1 (rew_bot bounds skel' tm1))
+ | NONE => NONE));
+
+ fun rew_top bounds _ tm = (case rew tm of
+ SOME (tm1, _) => (case rew_sub rew_top bounds skel0 tm1 of
+ SOME tm2 => SOME (the_default tm2 (rew_top bounds skel0 tm2))
+ | NONE => SOME tm1)
+ | NONE => (case rew_sub rew_top bounds skel0 tm of
+ SOME tm1 => SOME (the_default tm1 (rew_top bounds skel0 tm1))
+ | NONE => NONE));
+
+ in the_default tm ((if bot then rew_bot else rew_top) 0 skel0 tm) end;
+
+val rewrite_term = gen_rewrite_term true;
+val rewrite_term_top = gen_rewrite_term false;
+
+
+open Pattern;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/more_unify.ML Fri Nov 21 18:14:39 2014 +0100
@@ -0,0 +1,85 @@
+(* Title: Pure/more_unify.ML
+ Author: Makarius
+
+Add-ons to Higher-Order Unification, outside the inference kernel.
+*)
+
+signature UNIFY =
+sig
+ include UNIFY
+ val matchers: Context.generic -> (term * term) list -> Envir.env Seq.seq
+ val matches_list: Context.generic -> term list -> term list -> bool
+end;
+
+structure Unify: UNIFY =
+struct
+
+(*Pattern matching*)
+fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
+ let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
+ in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
+ handle Pattern.MATCH => Seq.empty;
+
+(*General matching -- keep variables disjoint*)
+fun matchers _ [] = Seq.single (Envir.empty ~1)
+ | matchers context pairs =
+ let
+ val thy = Context.theory_of context;
+
+ val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
+ val offset = maxidx + 1;
+ val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs;
+ val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1;
+
+ val pat_tvars = fold (Term.add_tvars o #1) pairs' [];
+ val pat_vars = fold (Term.add_vars o #1) pairs' [];
+
+ val decr_indexesT =
+ Term.map_atyps (fn T as TVar ((x, i), S) =>
+ if i > maxidx then TVar ((x, i - offset), S) else T | T => T);
+ val decr_indexes =
+ Term.map_types decr_indexesT #>
+ Term.map_aterms (fn t as Var ((x, i), T) =>
+ if i > maxidx then Var ((x, i - offset), T) else t | t => t);
+
+ fun norm_tvar env ((x, i), S) =
+ let
+ val tyenv = Envir.type_env env;
+ val T' = Envir.norm_type tyenv (TVar ((x, i), S));
+ in
+ if (case T' of TVar (v, _) => v = (x, i) | _ => false) then NONE
+ else SOME ((x, i - offset), (S, decr_indexesT T'))
+ end;
+
+ fun norm_var env ((x, i), T) =
+ let
+ val tyenv = Envir.type_env env;
+ val T' = Envir.norm_type tyenv T;
+ val t' = Envir.norm_term env (Var ((x, i), T'));
+ in
+ if (case t' of Var (v, _) => v = (x, i) | _ => false) then NONE
+ else SOME ((x, i - offset), (decr_indexesT T', decr_indexes t'))
+ end;
+
+ fun result env =
+ if Envir.above env maxidx then (* FIXME proper handling of generated vars!? *)
+ SOME (Envir.Envir {maxidx = maxidx,
+ tyenv = Vartab.make (map_filter (norm_tvar env) pat_tvars),
+ tenv = Vartab.make (map_filter (norm_var env) pat_vars)})
+ else NONE;
+
+ val empty = Envir.empty maxidx';
+ in
+ Seq.append
+ (Seq.map_filter result (Unify.smash_unifiers context pairs' empty))
+ (first_order_matchers thy pairs empty)
+ end;
+
+fun matches_list context ps os =
+ length ps = length os andalso is_some (Seq.pull (matchers context (ps ~~ os)));
+
+
+open Unify;
+
+end;
+
--- a/src/Pure/pattern.ML Fri Nov 21 13:18:56 2014 +0100
+++ b/src/Pure/pattern.ML Fri Nov 21 18:14:39 2014 +0100
@@ -22,15 +22,6 @@
val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
val first_order_match: theory -> term * term
-> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
- val matches: theory -> term * term -> bool
- val matchess: theory -> term list * term list -> bool
- val equiv: theory -> term * term -> bool
- val matches_subterm: theory -> term * term -> bool
- val first_order: term -> bool
- val pattern: term -> bool
- val match_rew: theory -> term -> term * term -> (term * term) option
- val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
- val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term
end;
structure Pattern: PATTERN =
@@ -383,110 +374,5 @@
val envir' = apfst (typ_match thy (pT, oT)) envir;
in mtch [] po envir' handle Pattern => first_order_match thy po envir' end;
-fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
-
-fun matchess thy (ps, os) =
- length ps = length os andalso
- ((fold (match thy) (ps ~~ os) (Vartab.empty, Vartab.empty); true) handle MATCH => false);
-
-fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
-
-
-(* Does pat match a subterm of obj? *)
-fun matches_subterm thy (pat, obj) =
- let
- fun msub bounds obj = matches thy (pat, obj) orelse
- (case obj of
- Abs (x, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
- | t $ u => msub bounds t orelse msub bounds u
- | _ => false)
- in msub 0 obj end;
-
-fun first_order(Abs(_,_,t)) = first_order t
- | first_order(t $ u) = first_order t andalso first_order u andalso
- not(is_Var t)
- | first_order _ = true;
-
-fun pattern (Abs (_, _, t)) = pattern t
- | pattern t =
- let val (head, args) = strip_comb t in
- if is_Var head then
- forall is_Bound args andalso not (has_duplicates (op aconv) args)
- else forall pattern args
- end;
-
-
-(* rewriting -- simple but fast *)
-
-fun match_rew thy tm (tm1, tm2) =
- let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
- SOME (Envir.subst_term (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
- handle MATCH => NONE
- end;
-
-fun gen_rewrite_term bot thy rules procs tm =
- let
- val skel0 = Bound 0;
-
- fun variant_absfree bounds (x, T, t) =
- let
- val (x', t') = Term.dest_abs (Name.bound bounds, T, t);
- fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
- in (abs, t') end;
-
- fun rew (Abs (_, _, body) $ t) = SOME (subst_bound (t, body), skel0)
- | rew tm =
- (case get_first (match_rew thy tm) rules of
- NONE => Option.map (rpair skel0) (get_first (fn p => p tm) procs)
- | x => x);
-
- fun rew_sub r bounds skel (tm1 $ tm2) = (case tm1 of
- Abs (_, _, body) =>
- let val tm' = subst_bound (tm2, body)
- in SOME (the_default tm' (rew_sub r bounds skel0 tm')) end
- | _ =>
- let val (skel1, skel2) = (case skel of
- skel1 $ skel2 => (skel1, skel2)
- | _ => (skel0, skel0))
- in case r bounds skel1 tm1 of
- SOME tm1' => (case r bounds skel2 tm2 of
- SOME tm2' => SOME (tm1' $ tm2')
- | NONE => SOME (tm1' $ tm2))
- | NONE => (case r bounds skel2 tm2 of
- SOME tm2' => SOME (tm1 $ tm2')
- | NONE => NONE)
- end)
- | rew_sub r bounds skel (Abs body) =
- let
- val (abs, tm') = variant_absfree bounds body;
- val skel' = (case skel of Abs (_, _, skel') => skel' | _ => skel0)
- in case r (bounds + 1) skel' tm' of
- SOME tm'' => SOME (abs tm'')
- | NONE => NONE
- end
- | rew_sub _ _ _ _ = NONE;
-
- fun rew_bot bounds (Var _) _ = NONE
- | rew_bot bounds skel tm = (case rew_sub rew_bot bounds skel tm of
- SOME tm1 => (case rew tm1 of
- SOME (tm2, skel') => SOME (the_default tm2 (rew_bot bounds skel' tm2))
- | NONE => SOME tm1)
- | NONE => (case rew tm of
- SOME (tm1, skel') => SOME (the_default tm1 (rew_bot bounds skel' tm1))
- | NONE => NONE));
-
- fun rew_top bounds _ tm = (case rew tm of
- SOME (tm1, _) => (case rew_sub rew_top bounds skel0 tm1 of
- SOME tm2 => SOME (the_default tm2 (rew_top bounds skel0 tm2))
- | NONE => SOME tm1)
- | NONE => (case rew_sub rew_top bounds skel0 tm of
- SOME tm1 => SOME (the_default tm1 (rew_top bounds skel0 tm1))
- | NONE => NONE));
-
- in the_default tm ((if bot then rew_bot else rew_top) 0 skel0 tm) end;
-
-val rewrite_term = gen_rewrite_term true;
-val rewrite_term_top = gen_rewrite_term false;
-
end;
--- a/src/Pure/unify.ML Fri Nov 21 13:18:56 2014 +0100
+++ b/src/Pure/unify.ML Fri Nov 21 18:14:39 2014 +0100
@@ -24,8 +24,6 @@
val unifiers: Context.generic * Envir.env * ((term * term) list) ->
(Envir.env * (term * term) list) Seq.seq
val smash_unifiers: Context.generic -> (term * term) list -> Envir.env -> Envir.env Seq.seq
- val matchers: Context.generic -> (term * term) list -> Envir.env Seq.seq
- val matches_list: Context.generic -> term list -> term list -> bool
end
structure Unify : UNIFY =
@@ -664,69 +662,4 @@
fun smash_unifiers context tus env =
Seq.map smash_flexflex (unifiers (context, env, tus));
-
-(*Pattern matching*)
-fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
- let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
- in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
- handle Pattern.MATCH => Seq.empty;
-
-(*General matching -- keep variables disjoint*)
-fun matchers _ [] = Seq.single (Envir.empty ~1)
- | matchers context pairs =
- let
- val thy = Context.theory_of context;
-
- val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
- val offset = maxidx + 1;
- val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs;
- val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1;
-
- val pat_tvars = fold (Term.add_tvars o #1) pairs' [];
- val pat_vars = fold (Term.add_vars o #1) pairs' [];
-
- val decr_indexesT =
- Term.map_atyps (fn T as TVar ((x, i), S) =>
- if i > maxidx then TVar ((x, i - offset), S) else T | T => T);
- val decr_indexes =
- Term.map_types decr_indexesT #>
- Term.map_aterms (fn t as Var ((x, i), T) =>
- if i > maxidx then Var ((x, i - offset), T) else t | t => t);
-
- fun norm_tvar env ((x, i), S) =
- let
- val tyenv = Envir.type_env env;
- val T' = Envir.norm_type tyenv (TVar ((x, i), S));
- in
- if (case T' of TVar (v, _) => v = (x, i) | _ => false) then NONE
- else SOME ((x, i - offset), (S, decr_indexesT T'))
- end;
-
- fun norm_var env ((x, i), T) =
- let
- val tyenv = Envir.type_env env;
- val T' = Envir.norm_type tyenv T;
- val t' = Envir.norm_term env (Var ((x, i), T'));
- in
- if (case t' of Var (v, _) => v = (x, i) | _ => false) then NONE
- else SOME ((x, i - offset), (decr_indexesT T', decr_indexes t'))
- end;
-
- fun result env =
- if Envir.above env maxidx then (* FIXME proper handling of generated vars!? *)
- SOME (Envir.Envir {maxidx = maxidx,
- tyenv = Vartab.make (map_filter (norm_tvar env) pat_tvars),
- tenv = Vartab.make (map_filter (norm_var env) pat_vars)})
- else NONE;
-
- val empty = Envir.empty maxidx';
- in
- Seq.append
- (Seq.map_filter result (smash_unifiers context pairs' empty))
- (first_order_matchers thy pairs empty)
- end;
-
-fun matches_list context ps os =
- length ps = length os andalso is_some (Seq.pull (matchers context (ps ~~ os)));
-
end;