53 Seq.seq |
53 Seq.seq |
54 val enc_appl : |
54 val enc_appl : |
55 EncodeIsaFTerm.term * UpTerm -> UpTerm |
55 EncodeIsaFTerm.term * UpTerm -> UpTerm |
56 val enc_appr : |
56 val enc_appr : |
57 EncodeIsaFTerm.term * UpTerm -> UpTerm |
57 EncodeIsaFTerm.term * UpTerm -> UpTerm |
58 val fakefree_badbounds : |
58 |
59 (string * Term.typ) list -> Term.term -> |
|
60 (string * Term.typ) list * (string * Term.typ) list * Term.term |
|
61 val fcterm_of_term : EncodeIsaFTerm.term -> FcTerm |
59 val fcterm_of_term : EncodeIsaFTerm.term -> FcTerm |
62 val find_fcterm_matches : |
60 val find_fcterm_matches : |
63 ((FcTerm -> 'a) -> FcTerm -> 'b) -> |
61 ((FcTerm -> 'a) -> FcTerm -> 'b) -> |
64 (FcTerm -> 'a) -> FcTerm -> 'b |
62 (FcTerm -> 'a) -> FcTerm -> 'b |
65 val find_sg_concl_matches : |
63 val find_sg_concl_matches : |
106 val focuseq_to_subgoals : |
104 val focuseq_to_subgoals : |
107 FcTerm -> FcTerm Seq.seq |
105 FcTerm -> FcTerm Seq.seq |
108 exception isa_focus_term_exp of string |
106 exception isa_focus_term_exp of string |
109 val leaf_seq_of_fcterm : |
107 val leaf_seq_of_fcterm : |
110 FcTerm -> FcTerm Seq.seq |
108 FcTerm -> FcTerm Seq.seq |
111 val mk_foo_match : |
|
112 (Term.term -> Term.term) -> |
|
113 ('a * Term.typ) list -> Term.term -> Term.term |
|
114 val mk_term_of_upterm : |
109 val mk_term_of_upterm : |
115 EncodeIsaFTerm.term * UpTerm -> EncodeIsaFTerm.term |
110 EncodeIsaFTerm.term * UpTerm -> EncodeIsaFTerm.term |
116 val mk_termf_of_upterm : |
111 val mk_termf_of_upterm : |
117 UpTerm -> |
112 UpTerm -> |
118 (string * Type) list * |
113 (string * Type) list * |
119 (EncodeIsaFTerm.term -> EncodeIsaFTerm.term) |
114 (EncodeIsaFTerm.term -> EncodeIsaFTerm.term) |
120 val next_leaf_fcterm : FcTerm -> FcTerm |
115 val next_leaf_fcterm : FcTerm -> FcTerm |
121 val next_leaf_of_fcterm_seq : |
116 val next_leaf_of_fcterm_seq : |
122 FcTerm -> FcTerm Seq.seq |
117 FcTerm -> FcTerm Seq.seq |
123 exception out_of_term_exception of string |
118 exception out_of_term_exception of string |
124 val prepmatch : |
119 |
125 FcTerm -> |
|
126 Term.term * |
|
127 ((string * Term.typ) list * (string * Term.typ) list * Term.term) |
|
128 val pretty_fcterm : FcTerm -> Pretty.T |
|
129 val pure_mk_termf_of_upterm : |
120 val pure_mk_termf_of_upterm : |
130 (EncodeIsaFTerm.term, Type) UpTermLib.T -> |
121 (EncodeIsaFTerm.term, Type) UpTermLib.T -> |
131 (string * Type) list * |
122 (string * Type) list * |
132 (EncodeIsaFTerm.term -> EncodeIsaFTerm.term) |
123 (EncodeIsaFTerm.term -> EncodeIsaFTerm.term) |
133 val search_all_bl_ru_f : |
124 val search_all_bl_ru_f : |
155 FcTerm -> (string * Type) list |
146 FcTerm -> (string * Type) list |
156 val tyenv_of_focus' : FcTerm -> Type list |
147 val tyenv_of_focus' : FcTerm -> Type list |
157 val upsize_of_fcterm : FcTerm -> int |
148 val upsize_of_fcterm : FcTerm -> int |
158 val upterm_of : FcTerm -> UpTerm |
149 val upterm_of : FcTerm -> UpTerm |
159 val valid_match_start : FcTerm -> bool |
150 val valid_match_start : FcTerm -> bool |
160 end |
151 |
|
152 (* pre-matching/pre-unification *) |
|
153 val fakefree_badbounds : |
|
154 (string * Term.typ) list -> Term.term -> |
|
155 (string * Term.typ) list * (string * Term.typ) list * Term.term |
|
156 val mk_foo_match : |
|
157 (Term.term -> Term.term) -> |
|
158 ('a * Term.typ) list -> Term.term -> Term.term |
|
159 val prepmatch : |
|
160 FcTerm -> |
|
161 Term.term * |
|
162 ((string * Term.typ) list * (string * Term.typ) list * Term.term) |
|
163 |
|
164 |
|
165 val pretty : Theory.theory -> FcTerm -> Pretty.T |
|
166 |
|
167 end; |
161 |
168 |
162 |
169 |
163 |
170 |
164 structure BasicIsaFTerm = |
171 structure BasicIsaFTerm = |
165 FocusTermFUN( structure EncodeTerm = EncodeIsaFTerm); |
172 FocusTermFUN( structure EncodeTerm = EncodeIsaFTerm); |
354 |
361 |
355 fun focus_to_term_goal_prem (premid,gaolid) t = |
362 fun focus_to_term_goal_prem (premid,gaolid) t = |
356 focus_to_subgoal premid (focus_to_subgoal_of_term gaolid t); |
363 focus_to_subgoal premid (focus_to_subgoal_of_term gaolid t); |
357 |
364 |
358 |
365 |
|
366 |
359 (* FIXME: make a sturcture for holding free variable names and making |
367 (* FIXME: make a sturcture for holding free variable names and making |
360 them distinct --- ? maybe part of the new prooftree datatype ? |
368 them distinct --- ? maybe part of the new prooftree datatype ? |
361 Alos: use this to fix below... *) |
369 Alos: use this to fix below... *) |
362 |
370 |
363 (* T is outer bound vars, n is number of locally bound vars *) |
371 (* T is outer bound vars, n is number of locally bound vars *) |
422 val absterm = mk_foo_match mktermf Ts' t' |
430 val absterm = mk_foo_match mktermf Ts' t' |
423 in |
431 in |
424 (t', (FakeTs', Ts', absterm)) |
432 (t', (FakeTs', Ts', absterm)) |
425 end; |
433 end; |
426 |
434 |
|
435 |
|
436 fun pretty thy ft = |
|
437 let val (t', (_,_,absterm)) = prepmatch ft in |
|
438 Pretty.chunks |
|
439 [ Pretty.block [Pretty.str "(Abs:", |
|
440 Pretty.quote (Display.pretty_cterm (Thm.cterm_of thy absterm)), |
|
441 Pretty.str ","], |
|
442 Pretty.block [Pretty.str " Foc:", |
|
443 Pretty.quote (Display.pretty_cterm (Thm.cterm_of thy t')), |
|
444 Pretty.str ")" ] ] |
|
445 end; |
|
446 |
|
447 (* |
|
448 Pretty.str "no yet implemented"; |
|
449 Display.pretty_cterm (Thm.cterm_of t) |
|
450 Term.Free ("FOCUS", Term.type_of t) |
|
451 *) |
|
452 |
|
453 |
427 (* matching and unification for a focus term's focus *) |
454 (* matching and unification for a focus term's focus *) |
428 |
455 |
429 (* Note: Ts is a modified version of the original names of the outer |
456 (* Note: Ts is a modified version of the original names of the outer |
430 bound variables. New names have been introduced to make sure they are |
457 bound variables. New names have been introduced to make sure they are |
431 unique w.r.t all names in the term and each other. usednames' is |
458 unique w.r.t all names in the term and each other. usednames' is |