--- a/src/Pure/IsaPlanner/focus_term_lib.ML Sun Jun 11 00:28:18 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,386 +0,0 @@
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* Title: Pure/IsaPlanner/focus_term_lib.ML
- ID: $Id$
- Author: Lucas Dixon, University of Edinburgh
- lucasd@dai.ed.ac.uk
- Date: 16 April 2003
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* DESCRIPTION:
-
- Generic Foucs terms (like Zippers), which allows modification and
- manipulation of term keeping track of how we got to the position
- in the term. We provide a signature for terms, ie any kind of
- lamda calculus with abs and application, and some notion of types
- and naming of abstracted vars.
-
- FIXME: at some point in the future make a library to work simply
- with polymorphic upterms - that way if I want to use them without
- the focus part, then I don't need to include all the focus stuff.
-
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-
-(* to endoce and decode general terms into the type needed by focus
-term, this is an easy thing to write, but needs to be done for each
-type that is going to be used with focus terms. *)
-
-signature F_ENCODE_TERM_SIG =
-sig
-
- type term (* type of term to be encoded into TermT for focus term manip *)
- type TypeT (* type annotation for abstractions *)
- type LeafT (* type for other leaf types in term sturcture *)
-
- (* the type to be encoded into *)
- datatype TermT = $ of TermT * TermT
- | Abs of string * TypeT * TermT
- | lf of LeafT
-
- (* the encode and decode functions *)
- val fakebounds : string * TypeT -> term -> term
- val encode : term -> TermT
- val decode : TermT -> term
-
-end;
-
-
-
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-signature FOCUS_TERM_SIG =
-sig
- structure MinTermS : F_ENCODE_TERM_SIG
-
- exception focus_term_exp of string;
- exception out_of_term_exception of string;
-
- type Term (* = MinTermS.TermT *)
- type Type (* = MinTermS.TypeT *)
-
- type UpTerm (* = (Term,Type) UpTermLib.T *)
-
-(* datatype
- UpTerm =
- abs of string * Type * UpTerm
- | appl of Term * UpTerm
- | appr of Term * UpTerm
- | root *)
-
- datatype FcTerm = focus of Term * UpTerm
-
- (* translating *)
- val fcterm_of_term : MinTermS.term -> FcTerm
- val term_of_fcterm : FcTerm -> MinTermS.term
-
- (* editing/constrution *)
- val enc_appl : (MinTermS.term * UpTerm) -> UpTerm
- val enc_appr : (MinTermS.term * UpTerm) -> UpTerm
-
- (* upterm creatioin *)
- val upterm_of : FcTerm -> UpTerm
- val add_upterm : UpTerm -> FcTerm -> FcTerm
- val mk_term_of_upterm : (MinTermS.term * UpTerm) -> MinTermS.term
- val mk_termf_of_upterm : UpTerm ->
- (((string * Type) list) *
- (MinTermS.term -> MinTermS.term))
- val pure_mk_termf_of_upterm : (MinTermS.term, Type) UpTermLib.T ->
- (((string * Type) list) *
- (MinTermS.term -> MinTermS.term))
-
- (* focusing, throws exceptions *)
- val focus_bot_left_leaf : FcTerm -> FcTerm
- val focus_bot_left_nonabs_leaf : FcTerm -> FcTerm
- val focus_left : FcTerm -> FcTerm
- val focus_strict_left : FcTerm -> FcTerm
- val focus_right : FcTerm -> FcTerm
- val focus_abs : FcTerm -> FcTerm
- val focus_fake_abs : FcTerm -> FcTerm
- val focus_to_top : FcTerm -> FcTerm
- val focus_up : FcTerm -> FcTerm
- val focus_up_right : FcTerm -> FcTerm
- val focus_up_right1 : FcTerm -> FcTerm
-
- (* optional focus changes *)
- val focus_up_abs : FcTerm -> FcTerm option
- val focus_up_appr : FcTerm -> FcTerm option
- val focus_up_appl : FcTerm -> FcTerm option
- val focus_up_abs_or_appr : FcTerm -> FcTerm option
-
- val tyenv_of_focus : FcTerm -> (string * Type) list
- val tyenv_of_focus' : FcTerm -> Type list
-
- (* set/get the focus term *)
- val set_focus_of_fcterm : FcTerm -> MinTermS.term -> FcTerm
- val focus_of_fcterm : FcTerm -> MinTermS.term
-
- (* leaf navigation *)
- val leaf_seq_of_fcterm : FcTerm -> FcTerm Seq.seq
- val next_leaf_fcterm : FcTerm -> FcTerm
- val next_leaf_of_fcterm_seq : FcTerm -> FcTerm Seq.seq
-
- (* analysis *)
- val upsize_of_fcterm : FcTerm -> int
-end;
-
-
-
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(*
-
- NOTE!!! I think this can be done in a purely functional way with a
- pair of a term (the focus) and a function, that when applied
- unfocuses one level... maybe think about this as it would be a very
- nice generic consrtuction, without the need for encoding/decoding
- strutcures.
-
-*)
-functor FocusTermFUN(structure EncodeTerm : F_ENCODE_TERM_SIG)
- : FOCUS_TERM_SIG =
-struct
-
-structure MinTermS = EncodeTerm;
-
-local open MinTermS open UpTermLib in
-
- type Term = MinTermS.TermT;
- type Type = MinTermS.TypeT;
-
- exception focus_term_exp of string;
- exception out_of_term_exception of string;
-
- infix 9 $
-
- (* datatype to hold a term tree and the path to where you are in the term *)
-(* datatype UpTerm = root
- | appl of (Term * UpTerm)
- | appr of (Term * UpTerm)
- | abs of (string * Type * UpTerm); *)
-
- type UpTerm = (Term,Type) UpTermLib.T;
-
- fun enc_appl (t,u) = appl((MinTermS.encode t),u);
- fun enc_appr (t,u) = appr((MinTermS.encode t),u);
-
- datatype FcTerm = focus of (Term * UpTerm);
-
- (* the the term of the upterm *)
- fun mk_term_of_upt_aux (t, root) = MinTermS.decode t
- | mk_term_of_upt_aux (t, appl (l,m)) = mk_term_of_upt_aux(l$t, m)
- | mk_term_of_upt_aux (t, appr (r,m)) = mk_term_of_upt_aux(t$r, m)
- | mk_term_of_upt_aux (t, abs (s,ty,m)) = mk_term_of_upt_aux(Abs(s,ty,t),m);
-
- fun mk_term_of_upterm (t, ut) = mk_term_of_upt_aux (MinTermS.encode t, ut);
-
- (* a function version of the above, given an upterm it returns:
- a function on that given a term puts it in the context of the upterm,
- and a list of bound variables that are in the upterm, added as
- we go up - so in reverse order from that typiclaly used by top-down
- parsing of terms. *)
- fun mk_termf_of_upt_aux (f, bs, root) =
- (bs, fn t => MinTermS.decode (f t))
- | mk_termf_of_upt_aux (f, bs, appl (l,m)) =
- mk_termf_of_upt_aux (fn t => l $ (f t), bs, m)
- | mk_termf_of_upt_aux (f, bs, appr (r,m)) =
- mk_termf_of_upt_aux (fn t => (f t) $ r, bs, m)
- | mk_termf_of_upt_aux (f, bs, abs (s,ty,m)) =
- mk_termf_of_upt_aux (fn t => Abs(s,ty,(f t)), (s,ty)::bs, m);
-
- fun mk_termf_of_upterm ut = mk_termf_of_upt_aux (MinTermS.encode, [], ut);
-
-
- fun upterm_of (focus(t, u)) = u;
-
- (* put a new upterm at the start of our current term *)
- fun add_upterm u2 (focus(t, u)) = focus(t, UpTermLib.apply u2 u);
-
-
- (* As above but work on the pure originial upterm type *)
- fun pure_mk_termf_of_upterm ut =
- mk_termf_of_upt_aux
- (encode, [], (map_to_upterm_parts (encode, I) ut));
-
- fun fcterm_of_term t = focus(encode t, root);
-
- fun term_of_fcterm (focus (t, m)) = mk_term_of_upt_aux (t, m);
-
-(* fun term_of_fcterm (focus (t, root)) = mk_term_of_upt_aux (t, root)
- | term_of_fcterm _ = raise focus_term_exp "term_of_fcterm: something bad has happened here."; *)
-
- fun focus_of_fcterm (focus(t, _)) = MinTermS.decode t;
-
- (* replace the focus term with a new term... *)
- fun set_focus_of_fcterm (focus(_, m)) nt = focus(MinTermS.encode nt, m);
-
- fun focus_left (focus(a $ b, m)) = focus(a, appr(b, m))
- | focus_left (focus(Abs(s,ty,t), m)) = focus_left (focus(t, abs(s,ty,m)))
- | focus_left (focus(l, m)) = raise out_of_term_exception "focus_left";
-
- fun focus_strict_left (focus(a $ b, m)) = focus(a, appr(b, m))
- | focus_strict_left (focus(l, m)) = raise out_of_term_exception "focus_left";
-
-(* Note: ":" is standard for faked bound vars... see: EQStepTacTermTools *)
- fun focus_fake_abs (focus(Abs(s,ty,t), m)) =
- let val t' = MinTermS.encode (fakebounds (s,ty) (MinTermS.decode t))
- in focus(t', abs(s,ty,m)) end
- | focus_fake_abs (focus(l, m)) = raise out_of_term_exception "focus_fake_abs";
-
- fun focus_abs (focus(Abs(s,ty,t), m)) = focus(t, abs(s,ty,m))
- | focus_abs (focus(l, m)) = raise out_of_term_exception "focus_abs";
-
-
- fun focus_right (focus(a $ b, m)) = focus(b, appl(a, m))
- | focus_right (focus(Abs(s,ty,t), m)) = focus_right (focus(t, abs(s,ty,m)))
- | focus_right (focus(l, m)) = raise out_of_term_exception "focus_right";
-
- fun focus_up (focus(t, appl(l,m))) = focus(l$t, m)
- | focus_up (focus(t, appr(r,m))) = focus(t$r, m)
- | focus_up (focus(t, abs(s,ty,m))) = focus_up (focus(Abs(s,ty,t), m))
- | focus_up (focus(t, root)) = raise out_of_term_exception "focus_up";
-
- fun focus_to_top t =
- focus_to_top (focus_up t) handle out_of_term_exception _ => t;
-
- (* focus up until you can move right, and then do so *)
- fun focus_up_right (focus(t, appl(l,m))) =
- focus_up_right (focus(l$t, m))
- | focus_up_right (focus(t, appr(r,m))) =
- focus(r, appl(t,m))
- | focus_up_right (focus(t, abs(s,ty,m))) =
- focus_up_right (focus(Abs(s,ty,t), m))
- | focus_up_right (focus(t, root)) =
- raise out_of_term_exception "focus_up_right";
-
- (* as above, but do not move up over a left application *)
- fun focus_up_right1 (focus(t, appl(l,m))) =
- raise out_of_term_exception "focus_up_right1"
- | focus_up_right1 (focus(t, appr(r,m))) =
- focus(r, appl(t,m))
- | focus_up_right1 (focus(t, abs(s,ty,m))) =
- focus_up_right (focus(Abs(s,ty,t), m))
- | focus_up_right1 (focus(t, root)) =
- raise out_of_term_exception "focus_up_right1";
-
- (* move focus to the bottom left through abstractions *)
- fun focus_bot_left_leaf (ft as focus(t, _)) =
- focus_bot_left_leaf (focus_left ft)
- handle out_of_term_exception _=> ft;
-
- (* move focus to the bottom left, but not into abstractions *)
- fun focus_bot_left_nonabs_leaf (ft as focus(t, _)) =
- focus_bot_left_nonabs_leaf (focus_strict_left ft)
- handle out_of_term_exception _=> ft;
-
- (* focus tools for working directly with the focus representation *)
- fun focus_up_appr (focus(t, appl(l,m))) = NONE
- | focus_up_appr (focus(t, appr(r,m))) = SOME (focus(t$r, m))
- | focus_up_appr (focus(t, abs(s,ty,m))) = NONE
- | focus_up_appr (focus(t, root)) = NONE;
-
- fun focus_up_appl (focus(t, appl(l,m))) = SOME (focus(l$t, m))
- | focus_up_appl (focus(t, appr(r,m))) = NONE
- | focus_up_appl (focus(t, abs(s,ty,m))) = NONE
- | focus_up_appl (focus(t, root)) = NONE;
-
- fun focus_up_abs (focus(t, appl(l,m))) = NONE
- | focus_up_abs (focus(t, appr(r,m))) = NONE
- | focus_up_abs (focus(t, abs(s,ty,m))) =
- SOME (focus_up (focus(Abs(s,ty,t), m)))
- | focus_up_abs (focus(t, root)) = NONE;
-
- fun focus_up_abs_or_appr (focus(t, appl(l,m))) = NONE
- | focus_up_abs_or_appr (focus(t, appr(r,m))) = SOME (focus(t$r, m))
- | focus_up_abs_or_appr (focus(t, abs(s,ty,m))) =
- SOME (focus(Abs(s,ty,t), m))
- | focus_up_abs_or_appr (focus(t, root)) = NONE;
-
-
- fun tyenv_of_focus (focus(t, u)) = tyenv_of_upterm u;
- fun tyenv_of_focus' (focus(t, u)) = tyenv_of_upterm' u;
-
- (* return the Term.type of the focus term, computes bound vars type,
- does a quick check only. *)
-(* fun fastype_of_focus (focus(t, m)) =
- let
- fun boundtypes_of_upterm (abs(s,ty,m)) =
- ty::(boundtypes_of_upterm m)
- | boundtypes_of_upterm (appl(t,m)) =
- boundtypes_of_upterm m
- | boundtypes_of_upterm (appr(t,m)) =
- boundtypes_of_upterm m
- | boundtypes_of_upterm (root) = []
- in
- fastype_of1 ((boundtypes_of_upterm m), t)
- end; *)
-
- (* gets the next left hand side term, or throws an exception *)
- fun next_leaf_fcterm ft = focus_bot_left_leaf (focus_up_right ft);
-
- fun next_leaf_of_fcterm_seq_aux t () =
- let val nextt = next_leaf_fcterm t
- in
- SOME (nextt, Seq.make (next_leaf_of_fcterm_seq_aux nextt))
- end handle out_of_term_exception _ => NONE;
-
- (* sequence of next upterms from start upterm...
- ie a sequence of all leafs after this one*)
- fun next_leaf_of_fcterm_seq in_t =
- Seq.make (next_leaf_of_fcterm_seq_aux in_t);
-
- (* returns a sequence of all leaf up terms from term, ie DFS on
- leafs of term, ie uses time O(n), n = sizeof term. *)
- fun leaf_seq_of_fcterm in_t =
- let
- val botleft = (focus_bot_left_leaf in_t)
- in
- Seq.cons botleft (Seq.make (next_leaf_of_fcterm_seq_aux botleft))
- end;
-
- fun upsize_of_fcterm (focus(t, ut)) = upsize_of_upterm ut;
-
-end; (* local *)
-
-end; (* functor *)
-
-
-
-
-
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* focus term encoding sturcture for isabelle terms *)
-structure EncodeIsaFTerm : F_ENCODE_TERM_SIG =
-struct
- infix 9 $;
-
- type term = Term.term;
-
- type TypeT = Term.typ;
-
- datatype LeafT = lConst of string * Term.typ
- | lVar of ((string * int) * Term.typ)
- | lFree of (string * Term.typ)
- | lBound of int;
-
- datatype TermT = op $ of TermT * TermT
- | Abs of string * TypeT * TermT
- | lf of LeafT;
-
- fun fakebounds (s, ty) t = subst_bound (Free(":" ^ s, ty), t);
-
- fun encode (Term.$(a,b)) = (encode a) $ (encode b)
- | encode (Term.Abs(s,ty,t)) = Abs(s,ty,(encode t))
- | encode (Term.Const(s,ty)) = lf(lConst(s,ty))
- | encode (Term.Var((s,i),ty)) = lf(lVar((s,i),ty))
- | encode (Term.Free(s,ty)) = lf(lFree(s,ty))
- | encode (Term.Bound i) = lf(lBound i);
-
- fun decode (a $ b) = Term.$(decode a, decode b)
- | decode (Abs(s,ty,t)) = (Term.Abs(s,ty,decode t))
- | decode (lf(lConst(s,ty))) = Term.Const(s,ty)
- | decode (lf(lVar((s,i),ty))) = Term.Var((s,i),ty)
- | decode (lf(lFree(s,ty))) = (Term.Free(s,ty))
- | decode (lf(lBound i)) = (Term.Bound i);
-
-end;
-