author | wenzelm |
Sat, 08 Oct 2005 20:15:34 +0200 | |
changeset 17795 | 5b18c3343028 |
parent 17203 | 29b2563f5c11 |
child 19250 | 932a50e2332f |
permissions | -rw-r--r-- |
15481 | 1 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
16179 | 2 |
(* Title: Pure/IsaPlanner/isa_fterm.ML |
3 |
ID: $Id$ |
|
15481 | 4 |
Author: Lucas Dixon, University of Edinburgh |
5 |
lucasd@dai.ed.ac.uk |
|
6 |
Date: 16 April 2003 |
|
7 |
*) |
|
8 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
9 |
(* DESCRIPTION: |
|
10 |
||
11 |
Generic Foucs terms (like Zippers) instantiation for Isabelle terms. |
|
12 |
||
13 |
*) |
|
14 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
15 |
||
17795 | 16 |
signature ISA_ENCODE_TERM = (* cf. F_ENCODE_TERM_SIG *) |
17 |
sig |
|
18 |
type term |
|
19 |
type typ |
|
20 |
type LeafT |
|
21 |
datatype TermT = $ of TermT * TermT |
|
22 |
| Abs of string * typ * TermT |
|
23 |
| lf of LeafT |
|
24 |
val fakebounds : string * typ -> term -> term |
|
25 |
val encode : term -> TermT |
|
26 |
val decode : TermT -> term |
|
27 |
end; |
|
15481 | 28 |
|
29 |
(* signature BASIC_ISA_FTERM = |
|
30 |
FOCUS_TERM_SIG where type Term = ISA_ENCODE_TERM.Term *) |
|
31 |
||
32 |
signature ISA_FTERM = |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
33 |
sig |
17795 | 34 |
type Term (*= EncodeIsaFTerm.TermT*) |
35 |
type Type (*= Term.typ*) |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
36 |
type UpTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
37 |
datatype FcTerm = focus of Term * UpTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
38 |
structure MinTermS : F_ENCODE_TERM_SIG |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
39 |
val add_upterm : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
40 |
UpTerm -> FcTerm -> FcTerm |
15481 | 41 |
val clean_match_ft : |
17203 | 42 |
theory -> |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
43 |
Term.term -> |
15481 | 44 |
FcTerm -> |
45 |
( |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
46 |
((Term.indexname * (Term.sort * Term.typ)) list |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
47 |
* (Term.indexname * (Term.typ * Term.term)) list) |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
48 |
* (string * Term.typ) list |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
49 |
* (string * Term.typ) list |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
50 |
* Term.term) |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
51 |
option |
15481 | 52 |
val clean_unify_ft : |
53 |
Sign.sg -> |
|
54 |
int -> |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
55 |
Term.term -> |
15481 | 56 |
FcTerm -> |
57 |
( |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
58 |
((Term.indexname * (Term.sort * Term.typ)) list |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
59 |
* (Term.indexname * (Term.typ * Term.term)) list) |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
60 |
* (string * Term.typ) list * (string * Term.typ) list * Term.term) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
61 |
Seq.seq |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
62 |
val enc_appl : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
63 |
EncodeIsaFTerm.term * UpTerm -> UpTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
64 |
val enc_appr : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
65 |
EncodeIsaFTerm.term * UpTerm -> UpTerm |
17045
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
66 |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
67 |
val fcterm_of_term : EncodeIsaFTerm.term -> FcTerm |
15481 | 68 |
val find_fcterm_matches : |
69 |
((FcTerm -> 'a) -> FcTerm -> 'b) -> |
|
70 |
(FcTerm -> 'a) -> FcTerm -> 'b |
|
71 |
val find_sg_concl_matches : |
|
72 |
((FcTerm -> 'a) -> FcTerm -> 'b) -> |
|
73 |
(FcTerm -> 'a) -> int -> EncodeIsaFTerm.term -> 'b |
|
74 |
val find_sg_concl_thm_matches : |
|
75 |
((FcTerm -> 'a) -> FcTerm -> 'b) -> |
|
76 |
(FcTerm -> 'a) -> int -> Thm.thm -> 'b |
|
77 |
val find_sg_matches : |
|
78 |
((FcTerm -> 'a) -> FcTerm -> 'b) -> |
|
79 |
(FcTerm -> 'a) -> int -> EncodeIsaFTerm.term -> 'b |
|
80 |
val find_sg_thm_matches : |
|
81 |
((FcTerm -> 'a) -> FcTerm -> 'b) -> |
|
82 |
(FcTerm -> 'a) -> int -> Thm.thm -> 'b |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
83 |
val focus_abs : FcTerm -> FcTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
84 |
val focus_bot_left_leaf : FcTerm -> FcTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
85 |
val focus_bot_left_nonabs_leaf : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
86 |
FcTerm -> FcTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
87 |
val focus_fake_abs : FcTerm -> FcTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
88 |
val focus_left : FcTerm -> FcTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
89 |
val focus_of_fcterm : FcTerm -> EncodeIsaFTerm.term |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
90 |
val focus_right : FcTerm -> FcTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
91 |
val focus_strict_left : FcTerm -> FcTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
92 |
exception focus_term_exp of string |
15481 | 93 |
val focus_to_concl : FcTerm -> FcTerm |
94 |
val focus_to_concl_of_term : EncodeIsaFTerm.term -> FcTerm |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
95 |
val focus_to_dest_impl : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
96 |
FcTerm -> FcTerm * FcTerm |
15481 | 97 |
val focus_to_subgoal : |
98 |
int -> FcTerm -> FcTerm |
|
99 |
val focus_to_subgoal_of_term : |
|
100 |
int -> EncodeIsaFTerm.term -> FcTerm |
|
101 |
val focus_to_term_goal_prem : |
|
102 |
int * int -> EncodeIsaFTerm.term -> FcTerm |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
103 |
val focus_to_top : FcTerm -> FcTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
104 |
val focus_up : FcTerm -> FcTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
105 |
val focus_up_abs : FcTerm -> FcTerm option |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
106 |
val focus_up_abs_or_appr : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
107 |
FcTerm -> FcTerm option |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
108 |
val focus_up_appl : FcTerm -> FcTerm option |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
109 |
val focus_up_appr : FcTerm -> FcTerm option |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
110 |
val focus_up_right : FcTerm -> FcTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
111 |
val focus_up_right1 : FcTerm -> FcTerm |
15481 | 112 |
val focuseq_to_subgoals : |
113 |
FcTerm -> FcTerm Seq.seq |
|
114 |
exception isa_focus_term_exp of string |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
115 |
val leaf_seq_of_fcterm : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
116 |
FcTerm -> FcTerm Seq.seq |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
117 |
val mk_term_of_upterm : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
118 |
EncodeIsaFTerm.term * UpTerm -> EncodeIsaFTerm.term |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
119 |
val mk_termf_of_upterm : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
120 |
UpTerm -> |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
121 |
(string * Type) list * |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
122 |
(EncodeIsaFTerm.term -> EncodeIsaFTerm.term) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
123 |
val next_leaf_fcterm : FcTerm -> FcTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
124 |
val next_leaf_of_fcterm_seq : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
125 |
FcTerm -> FcTerm Seq.seq |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
126 |
exception out_of_term_exception of string |
17045
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
127 |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
128 |
val pure_mk_termf_of_upterm : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
129 |
(EncodeIsaFTerm.term, Type) UpTermLib.T -> |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
130 |
(string * Type) list * |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
131 |
(EncodeIsaFTerm.term -> EncodeIsaFTerm.term) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
132 |
val search_all_bl_ru_f : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
133 |
(FcTerm -> 'a Seq.seq) -> |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
134 |
FcTerm -> 'a Seq.seq |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
135 |
val search_all_bl_ur_f : |
15481 | 136 |
(FcTerm -> 'a Seq.seq) -> |
137 |
FcTerm -> 'a Seq.seq |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
138 |
val search_tlr_all_f : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
139 |
(FcTerm -> 'a Seq.seq) -> |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
140 |
FcTerm -> 'a Seq.seq |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
141 |
val search_tlr_valid_f : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
142 |
(FcTerm -> 'a Seq.seq) -> |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
143 |
FcTerm -> 'a Seq.seq |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
144 |
val search_valid_bl_ru_f : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
145 |
(FcTerm -> 'a Seq.seq) -> |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
146 |
FcTerm -> 'a Seq.seq |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
147 |
val search_valid_bl_ur_f : |
15481 | 148 |
(FcTerm -> 'a Seq.seq) -> |
149 |
FcTerm -> 'a Seq.seq |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
150 |
val set_focus_of_fcterm : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
151 |
FcTerm -> EncodeIsaFTerm.term -> FcTerm |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
152 |
val term_of_fcterm : FcTerm -> EncodeIsaFTerm.term |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
153 |
val tyenv_of_focus : |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
154 |
FcTerm -> (string * Type) list |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
155 |
val tyenv_of_focus' : FcTerm -> Type list |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
156 |
val upsize_of_fcterm : FcTerm -> int |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
157 |
val upterm_of : FcTerm -> UpTerm |
15481 | 158 |
val valid_match_start : FcTerm -> bool |
17045
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
159 |
|
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
160 |
(* pre-matching/pre-unification *) |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
161 |
val fakefree_badbounds : |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
162 |
(string * Term.typ) list -> Term.term -> |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
163 |
(string * Term.typ) list * (string * Term.typ) list * Term.term |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
164 |
val mk_foo_match : |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
165 |
(Term.term -> Term.term) -> |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
166 |
('a * Term.typ) list -> Term.term -> Term.term |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
167 |
val prepmatch : |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
168 |
FcTerm -> |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
169 |
Term.term * |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
170 |
((string * Term.typ) list * (string * Term.typ) list * Term.term) |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
171 |
|
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
172 |
|
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
173 |
val pretty : Theory.theory -> FcTerm -> Pretty.T |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
174 |
|
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
175 |
end; |
15481 | 176 |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
177 |
|
15481 | 178 |
|
179 |
structure BasicIsaFTerm = |
|
180 |
FocusTermFUN( structure EncodeTerm = EncodeIsaFTerm); |
|
181 |
||
182 |
(* HOL Dependent *) |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
183 |
structure IsaFTerm : ISA_FTERM= |
15481 | 184 |
struct |
185 |
||
186 |
(* include BasicIsaFTerm *) |
|
187 |
(* open FocusTermFUN( structure EncodeTerm = EncodeIsaFTerm ); *) |
|
188 |
||
189 |
open BasicIsaFTerm; |
|
190 |
||
191 |
||
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15531
diff
changeset
|
192 |
(* Some general search within a focus term... *) |
15481 | 193 |
|
194 |
(* Note: only upterms with a free or constant are going to yeald a |
|
195 |
match, thus if we get anything else (bound or var) skip it! This is |
|
196 |
important if we switch to a unification net! in particular to avoid |
|
197 |
vars. *) |
|
198 |
||
199 |
fun valid_match_start ft = |
|
200 |
(case TermLib.bot_left_leaf_of (focus_of_fcterm ft) of |
|
201 |
Const _ => true |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
202 |
| Free _ => true |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
203 |
| Abs _ => true (* allowed to look inside abs... search decides if we actually consider the abstraction itself *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
204 |
| _ => false); (* avoid vars - always suceeds uninterestingly. *) |
15481 | 205 |
|
206 |
(* match starting at the bottom left, moving up to top of the term, |
|
207 |
then moving right to the next leaf and up again etc *) |
|
208 |
(* FIXME: make properly lazy! *) |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
209 |
fun search_valid_bl_ur_f f ft = |
15481 | 210 |
let |
211 |
val fts = |
|
212 |
Seq.filter valid_match_start |
|
213 |
(leaf_seq_of_fcterm ft) |
|
214 |
||
215 |
fun mk_match_up_seq ft = |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
216 |
(* avoid abstractions? - possibly infinite unifiers? *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
217 |
let val hereseq = case (focus_of_fcterm ft) of |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
218 |
Abs _ => Seq.empty |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
219 |
| _ => f ft |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
220 |
in |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
221 |
case focus_up_abs_or_appr ft of |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
222 |
SOME ft' => Seq.append(hereseq, mk_match_up_seq ft') |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
223 |
| NONE => hereseq |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
224 |
end |
15481 | 225 |
in |
226 |
Seq.flat (Seq.map mk_match_up_seq fts) |
|
227 |
end; |
|
228 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
229 |
fun search_all_bl_ur_f f ft = |
15481 | 230 |
let |
231 |
val fts = (leaf_seq_of_fcterm ft) |
|
232 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
233 |
fun mk_match_up_seq ft = |
15481 | 234 |
case focus_up_abs_or_appr ft of |
15531 | 235 |
SOME ft' => Seq.append(f ft, mk_match_up_seq ft') |
236 |
| NONE => f ft |
|
15481 | 237 |
in |
238 |
Seq.flat (Seq.map mk_match_up_seq fts) |
|
239 |
end; |
|
240 |
||
241 |
||
242 |
(* FIXME: make properly lazy! *) |
|
243 |
(* FIXME: make faking of bound vars local - for speeeeed *) |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
244 |
fun search_valid_bl_ru_f f ft = |
15481 | 245 |
let |
246 |
fun mauxtop ft = |
|
247 |
if (valid_match_start ft) |
|
248 |
then maux ft else Seq.empty |
|
249 |
and maux ft = |
|
250 |
let val t' = (focus_of_fcterm ft) |
|
251 |
(* val _ = writeln ("Examining: " ^ (TermLib.string_of_term t')) *) |
|
252 |
in |
|
253 |
(case t' of |
|
254 |
(_ $ _) => Seq.append (maux (focus_left ft), |
|
255 |
Seq.append(mauxtop (focus_right ft), |
|
256 |
f ft)) |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
257 |
| (Abs _) => maux (focus_abs ft) |
15481 | 258 |
| leaf => f ft) end |
259 |
in |
|
260 |
mauxtop ft |
|
261 |
end; |
|
262 |
||
263 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
264 |
fun search_all_bl_ru_f f ft = |
15481 | 265 |
let |
266 |
fun maux ft = |
|
267 |
let val t' = (focus_of_fcterm ft) |
|
268 |
(* val _ = writeln ("Examining: " ^ (TermLib.string_of_term t')) *) |
|
269 |
in |
|
270 |
(case t' of |
|
271 |
(_ $ _) => Seq.append (maux (focus_left ft), |
|
272 |
Seq.append(maux (focus_right ft), |
|
273 |
f ft)) |
|
274 |
| (Abs _) => Seq.append (maux (focus_abs ft), |
|
275 |
f ft) |
|
276 |
| leaf => f ft) end |
|
277 |
in maux ft end; |
|
278 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
279 |
(* search from top, left to right, then down *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
280 |
fun search_tlr_all_f f ft = |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
281 |
let |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
282 |
fun maux ft = |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
283 |
let val t' = (focus_of_fcterm ft) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
284 |
(* val _ = |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
285 |
if !trace_subst_search then |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
286 |
(writeln ("Examining: " ^ (TermLib.string_of_term t')); |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
287 |
TermLib.writeterm t'; ()) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
288 |
else (); *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
289 |
in |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
290 |
(case t' of |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
291 |
(_ $ _) => Seq.append(maux (focus_left ft), |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
292 |
Seq.append(f ft, |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
293 |
maux (focus_right ft))) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
294 |
| (Abs _) => Seq.append(f ft, maux (focus_abs ft)) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
295 |
| leaf => f ft) end |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
296 |
in maux ft end; |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
297 |
|
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
298 |
fun search_tlr_valid_f f ft = |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
299 |
let |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
300 |
fun maux ft = |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
301 |
let |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
302 |
val hereseq = if valid_match_start ft then f ft else Seq.empty |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
303 |
in |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
304 |
(case (focus_of_fcterm ft) of |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
305 |
(_ $ _) => Seq.append(maux (focus_left ft), |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
306 |
Seq.append(hereseq, |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
307 |
maux (focus_right ft))) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
308 |
| (Abs _) => Seq.append(hereseq, maux (focus_abs ft)) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
309 |
| leaf => hereseq) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
310 |
end |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
311 |
in maux ft end; |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
312 |
|
15481 | 313 |
|
314 |
||
315 |
exception isa_focus_term_exp of string; |
|
316 |
||
317 |
||
318 |
fun focus_to_dest_impl ft = |
|
319 |
let val (lhs, rhs) = |
|
320 |
Logic.dest_implies (focus_of_fcterm ft) |
|
321 |
in (focus_left ft, focus_right ft) end |
|
322 |
handle Term.TERM _ => |
|
323 |
raise isa_focus_term_exp |
|
324 |
"focus_to_dest_impl: applied to non implication"; |
|
325 |
||
326 |
||
327 |
(* move focus to the conlusion *) |
|
328 |
fun focus_to_concl ft = |
|
329 |
let val (lhs, rhs) = |
|
330 |
Logic.dest_implies (focus_of_fcterm ft) |
|
331 |
in focus_to_concl (focus_right ft) end |
|
332 |
handle Term.TERM _ => ft; |
|
333 |
||
334 |
val focus_to_concl_of_term = focus_to_concl o fcterm_of_term; |
|
335 |
||
336 |
||
337 |
||
338 |
(* give back sequence of focuses at different subgoals *) |
|
339 |
(* FIXME: make truly lazy *) |
|
340 |
fun focuseq_to_subgoals ft = |
|
341 |
if (Logic.is_implies (focus_of_fcterm ft)) then |
|
342 |
Seq.cons (focus_right (focus_left ft), focuseq_to_subgoals (focus_right ft)) |
|
343 |
else |
|
344 |
Seq.empty; |
|
345 |
||
346 |
(* move focus to a specific subgoal, 0 is first *) |
|
347 |
fun focus_to_subgoal j ft = |
|
348 |
let fun focus_to_subgoal' (ft, 0) = |
|
349 |
let val (lhs, rhs) = Logic.dest_implies (focus_of_fcterm ft) |
|
350 |
in ft |> focus_left |> focus_right end |
|
351 |
| focus_to_subgoal' (ft, i) = |
|
352 |
let val (lhs, rhs) = Logic.dest_implies (focus_of_fcterm ft) |
|
353 |
in focus_to_subgoal' (focus_right ft, i - 1) end |
|
354 |
in focus_to_subgoal' (ft, j - 1) end |
|
355 |
handle Term.TERM _ => |
|
356 |
raise isa_focus_term_exp |
|
357 |
("focus_to_subgoal: No such subgoal: " ^ |
|
358 |
(string_of_int j)); |
|
359 |
||
360 |
fun focus_to_subgoal_of_term i t = |
|
361 |
focus_to_subgoal i (fcterm_of_term t) |
|
362 |
||
363 |
(* move focus to a specific premise *) |
|
364 |
(* fun focus_past_params i ft = |
|
365 |
(focus_to_subgoal (focus_right ft, i)) |
|
366 |
handle isa_focus_term_exp _ => |
|
367 |
raise isa_focus_term_exp |
|
368 |
("focus_to_prmise: No such premise: " ^ (string_of_int i)); *) |
|
369 |
||
370 |
fun focus_to_term_goal_prem (premid,gaolid) t = |
|
371 |
focus_to_subgoal premid (focus_to_subgoal_of_term gaolid t); |
|
372 |
||
373 |
||
17045
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
374 |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
375 |
(* FIXME: make a sturcture for holding free variable names and making |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
376 |
them distinct --- ? maybe part of the new prooftree datatype ? |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
377 |
Alos: use this to fix below... *) |
15481 | 378 |
|
379 |
(* T is outer bound vars, n is number of locally bound vars *) |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
380 |
(* THINK: is order of Ts correct...? or reversed? *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
381 |
fun fakefree_badbounds Ts t = |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
382 |
let val (FakeTs,Ts,newnames) = |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
383 |
List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
384 |
let val newname = Term.variant usednames n |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
385 |
in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs, |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
386 |
(newname,ty)::Ts, |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
387 |
newname::usednames) end) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
388 |
([],[],[]) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
389 |
Ts |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
390 |
in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end; |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
391 |
|
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
392 |
(* fun fakefree_badbounds usednames T n (a $ b) = *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
393 |
(* let val (usednames', T', a') = fakefree_badbounds usednames T n a *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
394 |
(* val (usednames'', T'', b') = fakefree_badbounds usednames' T n b in *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
395 |
(* (usednames'', T'', a' $ b') end *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
396 |
(* | fakefree_badbounds usednames T n (Abs(s,ty,t)) = *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
397 |
(* let val (usednames', T', t') = fakefree_badbounds usednames T (n + 1) t in *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
398 |
(* (usednames', T', Abs(s,ty, t')) *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
399 |
(* | fakefree_badbounds usednames T n (b as Bound i) = *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
400 |
(* let fun mkfake_bound j [] = *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
401 |
(* raise ERROR_MESSAGE "fakefree_badbounds: bound is outside of the known types!" *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
402 |
(* | mkfake_bound 0 ((s,ty)::Ts) = *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
403 |
(* let val newname = Term.variant s usednames in *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
404 |
(* usednames, (newname,ty) :: T, Free (newname,ty) *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
405 |
(* | mkfake_bound j (d::Ts) = mkfake_bound (j - 1) Ts *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
406 |
(* in if n <= i then mkfake_bound (i - n) T else b end *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
407 |
(* | fakefree_badbounds usednames T t = t; *) |
15481 | 408 |
|
409 |
||
410 |
(* note: outerterm is the taget with the match replaced by a bound |
|
411 |
variable : ie: "P lhs" beocmes "%x. P x" |
|
412 |
insts is the types of instantiations of vars in lhs |
|
413 |
and typinsts is the type instantiations of types in the lhs |
|
414 |
Note: Final rule is the rule lifted into the ontext of the |
|
415 |
taget thm. *) |
|
416 |
fun mk_foo_match mkuptermfunc Ts t = |
|
417 |
let |
|
418 |
val ty = Term.type_of t |
|
419 |
val bigtype = (rev (map snd Ts)) ---> ty |
|
420 |
fun mk_foo 0 t = t |
|
421 |
| mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1))) |
|
422 |
val num_of_bnds = (length Ts) |
|
423 |
(* foo_term = "fooabs y0 ... yn" where y's are local bounds *) |
|
424 |
val foo_term = mk_foo num_of_bnds (Bound num_of_bnds) |
|
425 |
in Abs("fooabs", bigtype, mkuptermfunc foo_term) end; |
|
426 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
427 |
(* before matching we need to fake the bound vars that are missing an |
15481 | 428 |
abstraction. In this function we additionally construct the |
429 |
abstraction environment, and an outer context term (with the focus |
|
430 |
abstracted out) for use in rewriting with RWInst.rw *) |
|
431 |
fun prepmatch ft = |
|
432 |
let |
|
433 |
val t = focus_of_fcterm ft |
|
434 |
val Ts = tyenv_of_focus ft |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
435 |
val (FakeTs', Ts', t') = fakefree_badbounds Ts t |
15481 | 436 |
fun mktermf t = |
437 |
term_of_fcterm (set_focus_of_fcterm ft t) |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
438 |
val absterm = mk_foo_match mktermf Ts' t' |
15481 | 439 |
in |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
440 |
(t', (FakeTs', Ts', absterm)) |
15481 | 441 |
end; |
442 |
||
17045
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
443 |
|
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
444 |
fun pretty thy ft = |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
445 |
let val (t', (_,_,absterm)) = prepmatch ft in |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
446 |
Pretty.chunks |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
447 |
[ Pretty.block [Pretty.str "(Abs:", |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
448 |
Pretty.quote (Display.pretty_cterm (Thm.cterm_of thy absterm)), |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
449 |
Pretty.str ","], |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
450 |
Pretty.block [Pretty.str " Foc:", |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
451 |
Pretty.quote (Display.pretty_cterm (Thm.cterm_of thy t')), |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
452 |
Pretty.str ")" ] ] |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
453 |
end; |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
454 |
|
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
455 |
(* |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
456 |
Pretty.str "no yet implemented"; |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
457 |
Display.pretty_cterm (Thm.cterm_of t) |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
458 |
Term.Free ("FOCUS", Term.type_of t) |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
459 |
*) |
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
460 |
|
e108cd5b6986
lucas - added pretty printing function and cleaned up signature a little.
dixon
parents:
16179
diff
changeset
|
461 |
|
15481 | 462 |
(* matching and unification for a focus term's focus *) |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
463 |
|
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
464 |
(* Note: Ts is a modified version of the original names of the outer |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
465 |
bound variables. New names have been introduced to make sure they are |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
466 |
unique w.r.t all names in the term and each other. usednames' is |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
467 |
oldnames + new names. *) |
17203 | 468 |
fun clean_match_ft thy pat ft = |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
469 |
let val (t, (FakeTs,Ts,absterm)) = prepmatch ft in |
17203 | 470 |
case TermLib.clean_match thy (pat, t) of |
15531 | 471 |
NONE => NONE |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
472 |
| SOME insts => SOME (insts, FakeTs, Ts, absterm) end; |
15481 | 473 |
(* ix = max var index *) |
474 |
fun clean_unify_ft sgn ix pat ft = |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
475 |
let val (t, (FakeTs, Ts,absterm)) = prepmatch ft in |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
476 |
Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) |
15481 | 477 |
(TermLib.clean_unify sgn ix (t, pat)) end; |
478 |
||
479 |
||
480 |
(* THINK: ? do we not need to incremement bound indices? *) |
|
481 |
(* THINK: it should be the search which localisaes the search to the |
|
482 |
current focus, not this hack in the matcher... ? *) |
|
483 |
(* find matches below this particular focus term *) |
|
484 |
(* The search function is to find a match within a term... *) |
|
485 |
(* the matcher is something that is applied to each node chosen by the |
|
486 |
searchf and the results are flattened to form a lazy list. *) |
|
487 |
fun find_fcterm_matches searchf matcher ft = |
|
488 |
let |
|
489 |
val ftupterm = upterm_of ft |
|
490 |
val focusft = focus_of_fcterm ft |
|
491 |
val add_uptermf = add_upterm ftupterm |
|
492 |
in |
|
493 |
searchf |
|
494 |
(fn ft' => matcher (add_uptermf ft')) |
|
495 |
(fcterm_of_term focusft) |
|
496 |
end; |
|
497 |
||
498 |
(* FIXME: move argument orders for efficiency... |
|
499 |
i.e. wenzel style val foofunc = x o y; |
|
500 |
*) |
|
501 |
||
502 |
(* find the matches inside subgoal i of th *) |
|
503 |
fun find_sg_matches searchf matcher i t = |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
504 |
let |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15661
diff
changeset
|
505 |
val subgoal_fcterm = focus_to_subgoal_of_term i t |
15481 | 506 |
in find_fcterm_matches searchf matcher subgoal_fcterm end; |
507 |
||
508 |
(* find the matches inside subgoal i of th *) |
|
509 |
fun find_sg_thm_matches searchf matcher i th = |
|
510 |
find_sg_matches searchf matcher i (Thm.prop_of th); |
|
511 |
||
512 |
||
513 |
(* find the matches inside subgoal i's conclusion of th *) |
|
514 |
fun find_sg_concl_matches searchf matcher i t = |
|
515 |
let |
|
516 |
val subgoal_fcterm = |
|
517 |
focus_to_concl (focus_to_subgoal_of_term i t) |
|
518 |
in |
|
519 |
find_fcterm_matches searchf matcher subgoal_fcterm |
|
520 |
end; |
|
521 |
||
522 |
(* find the matches inside subgoal i's conclusion of th *) |
|
523 |
fun find_sg_concl_thm_matches searchf matcher i th = |
|
524 |
find_sg_concl_matches searchf matcher i (Thm.prop_of th); |
|
525 |
||
526 |
end; |
|
527 |
||
528 |
(* |
|
529 |
test... |
|
530 |
||
531 |
f_encode_isatermS.encode (read "P a"); |
|
532 |
isafocustermS.fcterm_of_term (read "f a"); |
|
533 |
isafocustermS.term_of_fcterm it; |
|
534 |
||
535 |
Goal "P b ==> P (suc b)"; |
|
536 |
||
537 |
TermLib.string_of_term ((focus_of_fcterm o focus_to_subgoal_of_term 1 o prop_of) (topthm())); |
|
538 |
||
539 |
TermLib.string_of_term ((focus_of_fcterm o focus_to_concl o focus_to_subgoal_of_term 1 o prop_of) (topthm())); |
|
540 |
||
541 |
TermLib.string_of_term ((focus_of_fcterm o focus_to_term_goal_prem (1,1) o prop_of) (topthm())); |
|
542 |
||
543 |
*) |