lucas - added pretty printing function and cleaned up signature a little.
--- a/src/Pure/IsaPlanner/isa_fterm.ML Mon Aug 15 21:38:25 2005 +0200
+++ b/src/Pure/IsaPlanner/isa_fterm.ML Mon Aug 15 21:39:15 2005 +0200
@@ -55,9 +55,7 @@
EncodeIsaFTerm.term * UpTerm -> UpTerm
val enc_appr :
EncodeIsaFTerm.term * UpTerm -> UpTerm
- val fakefree_badbounds :
- (string * Term.typ) list -> Term.term ->
- (string * Term.typ) list * (string * Term.typ) list * Term.term
+
val fcterm_of_term : EncodeIsaFTerm.term -> FcTerm
val find_fcterm_matches :
((FcTerm -> 'a) -> FcTerm -> 'b) ->
@@ -108,9 +106,6 @@
exception isa_focus_term_exp of string
val leaf_seq_of_fcterm :
FcTerm -> FcTerm Seq.seq
- val mk_foo_match :
- (Term.term -> Term.term) ->
- ('a * Term.typ) list -> Term.term -> Term.term
val mk_term_of_upterm :
EncodeIsaFTerm.term * UpTerm -> EncodeIsaFTerm.term
val mk_termf_of_upterm :
@@ -121,11 +116,7 @@
val next_leaf_of_fcterm_seq :
FcTerm -> FcTerm Seq.seq
exception out_of_term_exception of string
- val prepmatch :
- FcTerm ->
- Term.term *
- ((string * Term.typ) list * (string * Term.typ) list * Term.term)
- val pretty_fcterm : FcTerm -> Pretty.T
+
val pure_mk_termf_of_upterm :
(EncodeIsaFTerm.term, Type) UpTermLib.T ->
(string * Type) list *
@@ -157,7 +148,23 @@
val upsize_of_fcterm : FcTerm -> int
val upterm_of : FcTerm -> UpTerm
val valid_match_start : FcTerm -> bool
- end
+
+ (* pre-matching/pre-unification *)
+ val fakefree_badbounds :
+ (string * Term.typ) list -> Term.term ->
+ (string * Term.typ) list * (string * Term.typ) list * Term.term
+ val mk_foo_match :
+ (Term.term -> Term.term) ->
+ ('a * Term.typ) list -> Term.term -> Term.term
+ val prepmatch :
+ FcTerm ->
+ Term.term *
+ ((string * Term.typ) list * (string * Term.typ) list * Term.term)
+
+
+ val pretty : Theory.theory -> FcTerm -> Pretty.T
+
+ end;
@@ -356,6 +363,7 @@
focus_to_subgoal premid (focus_to_subgoal_of_term gaolid t);
+
(* FIXME: make a sturcture for holding free variable names and making
them distinct --- ? maybe part of the new prooftree datatype ?
Alos: use this to fix below... *)
@@ -424,6 +432,25 @@
(t', (FakeTs', Ts', absterm))
end;
+
+fun pretty thy ft =
+ let val (t', (_,_,absterm)) = prepmatch ft in
+ Pretty.chunks
+ [ Pretty.block [Pretty.str "(Abs:",
+ Pretty.quote (Display.pretty_cterm (Thm.cterm_of thy absterm)),
+ Pretty.str ","],
+ Pretty.block [Pretty.str " Foc:",
+ Pretty.quote (Display.pretty_cterm (Thm.cterm_of thy t')),
+ Pretty.str ")" ] ]
+ end;
+
+(*
+ Pretty.str "no yet implemented";
+ Display.pretty_cterm (Thm.cterm_of t)
+ Term.Free ("FOCUS", Term.type_of t)
+*)
+
+
(* matching and unification for a focus term's focus *)
(* Note: Ts is a modified version of the original names of the outer