# HG changeset patch # User wenzelm # Date 1416590079 -3600 # Node ID 30b8a5825a9c053a57cdb96f749f93e2d4456d6d # Parent d885cff91200d92a7fe4a684e62d29bc74a55ab8 removed some add-ons from modules that are relevant for the inference kernel; diff -r d885cff91200 -r 30b8a5825a9c src/Pure/ROOT --- 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" diff -r d885cff91200 -r 30b8a5825a9c src/Pure/ROOT.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"; diff -r d885cff91200 -r 30b8a5825a9c src/Pure/more_pattern.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; + diff -r d885cff91200 -r 30b8a5825a9c src/Pure/more_unify.ML --- /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; + diff -r d885cff91200 -r 30b8a5825a9c src/Pure/pattern.ML --- 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; diff -r d885cff91200 -r 30b8a5825a9c src/Pure/unify.ML --- 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;