author | wenzelm |
Wed, 31 Jul 2019 19:50:38 +0200 | |
changeset 70451 | 550a5a822edb |
parent 63615 | d786d54efc70 |
child 74280 | 7466b17b0820 |
permissions | -rw-r--r-- |
59026
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/more_unify.ML |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
3 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
4 |
Add-ons to Higher-Order Unification, outside the inference kernel. |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
5 |
*) |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
6 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
7 |
signature UNIFY = |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
8 |
sig |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
9 |
include UNIFY |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
10 |
val matchers: Context.generic -> (term * term) list -> Envir.env Seq.seq |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
11 |
val matches_list: Context.generic -> term list -> term list -> bool |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
12 |
end; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
13 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
14 |
structure Unify: UNIFY = |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
15 |
struct |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
16 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
17 |
(*Pattern matching*) |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
18 |
fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) = |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
19 |
let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv) |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
20 |
in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
21 |
handle Pattern.MATCH => Seq.empty; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
22 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
23 |
(*General matching -- keep variables disjoint*) |
63615 | 24 |
fun matchers _ [] = Seq.single Envir.init |
59026
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
25 |
| matchers context pairs = |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
26 |
let |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
27 |
val thy = Context.theory_of context; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
28 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
29 |
val maxidx = fold (Term.maxidx_term o #2) pairs ~1; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
30 |
val offset = maxidx + 1; |
59787 | 31 |
val pairs' = map (apfst (Logic.incr_indexes ([], [], offset))) pairs; |
59026
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
32 |
val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
33 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
34 |
val pat_tvars = fold (Term.add_tvars o #1) pairs' []; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
35 |
val pat_vars = fold (Term.add_vars o #1) pairs' []; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
36 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
37 |
val decr_indexesT = |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
38 |
Term.map_atyps (fn T as TVar ((x, i), S) => |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
39 |
if i > maxidx then TVar ((x, i - offset), S) else T | T => T); |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
40 |
val decr_indexes = |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
41 |
Term.map_types decr_indexesT #> |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
42 |
Term.map_aterms (fn t as Var ((x, i), T) => |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
43 |
if i > maxidx then Var ((x, i - offset), T) else t | t => t); |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
44 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
45 |
fun norm_tvar env ((x, i), S) = |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
46 |
let |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
47 |
val tyenv = Envir.type_env env; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
48 |
val T' = Envir.norm_type tyenv (TVar ((x, i), S)); |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
49 |
in |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
50 |
if (case T' of TVar (v, _) => v = (x, i) | _ => false) then NONE |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
51 |
else SOME ((x, i - offset), (S, decr_indexesT T')) |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
52 |
end; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
53 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
54 |
fun norm_var env ((x, i), T) = |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
55 |
let |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
56 |
val tyenv = Envir.type_env env; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
57 |
val T' = Envir.norm_type tyenv T; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
58 |
val t' = Envir.norm_term env (Var ((x, i), T')); |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
59 |
in |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
60 |
if (case t' of Var (v, _) => v = (x, i) | _ => false) then NONE |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
61 |
else SOME ((x, i - offset), (decr_indexesT T', decr_indexes t')) |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
62 |
end; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
63 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
64 |
fun result env = |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
65 |
if Envir.above env maxidx then (* FIXME proper handling of generated vars!? *) |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
66 |
SOME (Envir.Envir {maxidx = maxidx, |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
67 |
tyenv = Vartab.make (map_filter (norm_tvar env) pat_tvars), |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
68 |
tenv = Vartab.make (map_filter (norm_var env) pat_vars)}) |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
69 |
else NONE; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
70 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
71 |
val empty = Envir.empty maxidx'; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
72 |
in |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
73 |
Seq.append |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
74 |
(Seq.map_filter result (Unify.smash_unifiers context pairs' empty)) |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
75 |
(first_order_matchers thy pairs empty) |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
76 |
end; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
77 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
78 |
fun matches_list context ps os = |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
79 |
length ps = length os andalso is_some (Seq.pull (matchers context (ps ~~ os))); |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
80 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
81 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
82 |
open Unify; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
83 |
|
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
84 |
end; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
diff
changeset
|
85 |