# HG changeset patch # User dixon # Date 1149978977 -7200 # Node ID 5181e317e9fff375f71a901ddbcba398ab5dbffb # Parent 81d6dc59755959c987809339356bbefec2bed5a2 moved to new location in Provers. diff -r 81d6dc597559 -r 5181e317e9ff src/Pure/IsaPlanner/ROOT.ML --- a/src/Pure/IsaPlanner/ROOT.ML Sun Jun 11 00:28:18 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* ID: $Id$ - Author: Lucas Dixon, University of Edinburgh - lucasd@dai.ed.ac.uk - -The IsaPlanner subsystem. -*) - -use "isand.ML"; -use "isaplib.ML"; -use "term_lib.ML"; -use "upterm_lib.ML"; -use "focus_term_lib.ML"; -use "rw_tools.ML"; -use "rw_inst.ML"; -use "isa_fterm.ML"; diff -r 81d6dc597559 -r 5181e317e9ff src/Pure/IsaPlanner/focus_term_lib.ML --- 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; - diff -r 81d6dc597559 -r 5181e317e9ff src/Pure/IsaPlanner/isa_fterm.ML --- a/src/Pure/IsaPlanner/isa_fterm.ML Sun Jun 11 00:28:18 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,543 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* Title: Pure/IsaPlanner/isa_fterm.ML - ID: $Id$ - Author: Lucas Dixon, University of Edinburgh - lucasd@dai.ed.ac.uk - Date: 16 April 2003 -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* DESCRIPTION: - - Generic Foucs terms (like Zippers) instantiation for Isabelle terms. - -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) - -signature ISA_ENCODE_TERM = (* cf. F_ENCODE_TERM_SIG *) -sig - type term - type typ - type LeafT - datatype TermT = $ of TermT * TermT - | Abs of string * typ * TermT - | lf of LeafT - val fakebounds : string * typ -> term -> term - val encode : term -> TermT - val decode : TermT -> term -end; - -(* signature BASIC_ISA_FTERM = -FOCUS_TERM_SIG where type Term = ISA_ENCODE_TERM.Term *) - -signature ISA_FTERM = - sig - type Term (*= EncodeIsaFTerm.TermT*) - type Type (*= Term.typ*) - type UpTerm - datatype FcTerm = focus of Term * UpTerm - structure MinTermS : F_ENCODE_TERM_SIG - val add_upterm : - UpTerm -> FcTerm -> FcTerm - val clean_match_ft : - theory -> - Term.term -> - FcTerm -> - ( - ((Term.indexname * (Term.sort * Term.typ)) list - * (Term.indexname * (Term.typ * Term.term)) list) - * (string * Term.typ) list - * (string * Term.typ) list - * Term.term) - option - val clean_unify_ft : - theory -> - int -> - Term.term -> - FcTerm -> - ( - ((Term.indexname * (Term.sort * Term.typ)) list - * (Term.indexname * (Term.typ * Term.term)) list) - * (string * Term.typ) list * (string * Term.typ) list * Term.term) - Seq.seq - val enc_appl : - EncodeIsaFTerm.term * UpTerm -> UpTerm - val enc_appr : - EncodeIsaFTerm.term * UpTerm -> UpTerm - - val fcterm_of_term : EncodeIsaFTerm.term -> FcTerm - val find_fcterm_matches : - ((FcTerm -> 'a) -> FcTerm -> 'b) -> - (FcTerm -> 'a) -> FcTerm -> 'b - val find_sg_concl_matches : - ((FcTerm -> 'a) -> FcTerm -> 'b) -> - (FcTerm -> 'a) -> int -> EncodeIsaFTerm.term -> 'b - val find_sg_concl_thm_matches : - ((FcTerm -> 'a) -> FcTerm -> 'b) -> - (FcTerm -> 'a) -> int -> Thm.thm -> 'b - val find_sg_matches : - ((FcTerm -> 'a) -> FcTerm -> 'b) -> - (FcTerm -> 'a) -> int -> EncodeIsaFTerm.term -> 'b - val find_sg_thm_matches : - ((FcTerm -> 'a) -> FcTerm -> 'b) -> - (FcTerm -> 'a) -> int -> Thm.thm -> 'b - val focus_abs : FcTerm -> FcTerm - val focus_bot_left_leaf : FcTerm -> FcTerm - val focus_bot_left_nonabs_leaf : - FcTerm -> FcTerm - val focus_fake_abs : FcTerm -> FcTerm - val focus_left : FcTerm -> FcTerm - val focus_of_fcterm : FcTerm -> EncodeIsaFTerm.term - val focus_right : FcTerm -> FcTerm - val focus_strict_left : FcTerm -> FcTerm - exception focus_term_exp of string - val focus_to_concl : FcTerm -> FcTerm - val focus_to_concl_of_term : EncodeIsaFTerm.term -> FcTerm - val focus_to_dest_impl : - FcTerm -> FcTerm * FcTerm - val focus_to_subgoal : - int -> FcTerm -> FcTerm - val focus_to_subgoal_of_term : - int -> EncodeIsaFTerm.term -> FcTerm - val focus_to_term_goal_prem : - int * int -> EncodeIsaFTerm.term -> FcTerm - val focus_to_top : FcTerm -> FcTerm - val focus_up : FcTerm -> FcTerm - val focus_up_abs : FcTerm -> FcTerm option - val focus_up_abs_or_appr : - FcTerm -> FcTerm option - val focus_up_appl : FcTerm -> FcTerm option - val focus_up_appr : FcTerm -> FcTerm option - val focus_up_right : FcTerm -> FcTerm - val focus_up_right1 : FcTerm -> FcTerm - val focuseq_to_subgoals : - FcTerm -> FcTerm Seq.seq - exception isa_focus_term_exp of string - val leaf_seq_of_fcterm : - FcTerm -> FcTerm Seq.seq - val mk_term_of_upterm : - EncodeIsaFTerm.term * UpTerm -> EncodeIsaFTerm.term - val mk_termf_of_upterm : - UpTerm -> - (string * Type) list * - (EncodeIsaFTerm.term -> EncodeIsaFTerm.term) - val next_leaf_fcterm : FcTerm -> FcTerm - val next_leaf_of_fcterm_seq : - FcTerm -> FcTerm Seq.seq - exception out_of_term_exception of string - - val pure_mk_termf_of_upterm : - (EncodeIsaFTerm.term, Type) UpTermLib.T -> - (string * Type) list * - (EncodeIsaFTerm.term -> EncodeIsaFTerm.term) - val search_all_bl_ru_f : - (FcTerm -> 'a Seq.seq) -> - FcTerm -> 'a Seq.seq - val search_all_bl_ur_f : - (FcTerm -> 'a Seq.seq) -> - FcTerm -> 'a Seq.seq - val search_tlr_all_f : - (FcTerm -> 'a Seq.seq) -> - FcTerm -> 'a Seq.seq - val search_tlr_valid_f : - (FcTerm -> 'a Seq.seq) -> - FcTerm -> 'a Seq.seq - val search_valid_bl_ru_f : - (FcTerm -> 'a Seq.seq) -> - FcTerm -> 'a Seq.seq - val search_valid_bl_ur_f : - (FcTerm -> 'a Seq.seq) -> - FcTerm -> 'a Seq.seq - val set_focus_of_fcterm : - FcTerm -> EncodeIsaFTerm.term -> FcTerm - val term_of_fcterm : FcTerm -> EncodeIsaFTerm.term - val tyenv_of_focus : - FcTerm -> (string * Type) list - val tyenv_of_focus' : FcTerm -> Type list - val upsize_of_fcterm : FcTerm -> int - val upterm_of : FcTerm -> UpTerm - val valid_match_start : FcTerm -> bool - - (* 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; - - - -structure BasicIsaFTerm = -FocusTermFUN( structure EncodeTerm = EncodeIsaFTerm); - -(* HOL Dependent *) -structure IsaFTerm : ISA_FTERM= -struct - -(* include BasicIsaFTerm *) -(* open FocusTermFUN( structure EncodeTerm = EncodeIsaFTerm ); *) - -open BasicIsaFTerm; - - -(* Some general search within a focus term... *) - -(* Note: only upterms with a free or constant are going to yeald a -match, thus if we get anything else (bound or var) skip it! This is -important if we switch to a unification net! in particular to avoid -vars. *) - -fun valid_match_start ft = - (case TermLib.bot_left_leaf_of (focus_of_fcterm ft) of - Const _ => true - | Free _ => true - | Abs _ => true (* allowed to look inside abs... search decides if we actually consider the abstraction itself *) - | _ => false); (* avoid vars - always suceeds uninterestingly. *) - -(* match starting at the bottom left, moving up to top of the term, - then moving right to the next leaf and up again etc *) -(* FIXME: make properly lazy! *) -fun search_valid_bl_ur_f f ft = - let - val fts = - Seq.filter valid_match_start - (leaf_seq_of_fcterm ft) - - fun mk_match_up_seq ft = - (* avoid abstractions? - possibly infinite unifiers? *) - let val hereseq = case (focus_of_fcterm ft) of - Abs _ => Seq.empty - | _ => f ft - in - case focus_up_abs_or_appr ft of - SOME ft' => Seq.append(hereseq, mk_match_up_seq ft') - | NONE => hereseq - end - in - Seq.flat (Seq.map mk_match_up_seq fts) - end; - -fun search_all_bl_ur_f f ft = - let - val fts = (leaf_seq_of_fcterm ft) - - fun mk_match_up_seq ft = - case focus_up_abs_or_appr ft of - SOME ft' => Seq.append(f ft, mk_match_up_seq ft') - | NONE => f ft - in - Seq.flat (Seq.map mk_match_up_seq fts) - end; - - -(* FIXME: make properly lazy! *) -(* FIXME: make faking of bound vars local - for speeeeed *) -fun search_valid_bl_ru_f f ft = - let - fun mauxtop ft = - if (valid_match_start ft) - then maux ft else Seq.empty - and maux ft = - let val t' = (focus_of_fcterm ft) - (* val _ = writeln ("Examining: " ^ (TermLib.string_of_term t')) *) - in - (case t' of - (_ $ _) => Seq.append (maux (focus_left ft), - Seq.append(mauxtop (focus_right ft), - f ft)) - | (Abs _) => maux (focus_abs ft) - | leaf => f ft) end - in - mauxtop ft - end; - - -fun search_all_bl_ru_f f ft = - let - fun maux ft = - let val t' = (focus_of_fcterm ft) - (* val _ = writeln ("Examining: " ^ (TermLib.string_of_term t')) *) - in - (case t' of - (_ $ _) => Seq.append (maux (focus_left ft), - Seq.append(maux (focus_right ft), - f ft)) - | (Abs _) => Seq.append (maux (focus_abs ft), - f ft) - | leaf => f ft) end - in maux ft end; - -(* search from top, left to right, then down *) -fun search_tlr_all_f f ft = - let - fun maux ft = - let val t' = (focus_of_fcterm ft) - (* val _ = - if !trace_subst_search then - (writeln ("Examining: " ^ (TermLib.string_of_term t')); - TermLib.writeterm t'; ()) - else (); *) - in - (case t' of - (_ $ _) => Seq.append(maux (focus_left ft), - Seq.append(f ft, - maux (focus_right ft))) - | (Abs _) => Seq.append(f ft, maux (focus_abs ft)) - | leaf => f ft) end - in maux ft end; - -fun search_tlr_valid_f f ft = - let - fun maux ft = - let - val hereseq = if valid_match_start ft then f ft else Seq.empty - in - (case (focus_of_fcterm ft) of - (_ $ _) => Seq.append(maux (focus_left ft), - Seq.append(hereseq, - maux (focus_right ft))) - | (Abs _) => Seq.append(hereseq, maux (focus_abs ft)) - | leaf => hereseq) - end - in maux ft end; - - - -exception isa_focus_term_exp of string; - - -fun focus_to_dest_impl ft = - let val (lhs, rhs) = - Logic.dest_implies (focus_of_fcterm ft) - in (focus_left ft, focus_right ft) end - handle Term.TERM _ => - raise isa_focus_term_exp - "focus_to_dest_impl: applied to non implication"; - - -(* move focus to the conlusion *) -fun focus_to_concl ft = - let val (lhs, rhs) = - Logic.dest_implies (focus_of_fcterm ft) - in focus_to_concl (focus_right ft) end - handle Term.TERM _ => ft; - -val focus_to_concl_of_term = focus_to_concl o fcterm_of_term; - - - -(* give back sequence of focuses at different subgoals *) -(* FIXME: make truly lazy *) -fun focuseq_to_subgoals ft = - if (Logic.is_implies (focus_of_fcterm ft)) then - Seq.cons (focus_right (focus_left ft)) (focuseq_to_subgoals (focus_right ft)) - else - Seq.empty; - -(* move focus to a specific subgoal, 0 is first *) -fun focus_to_subgoal j ft = - let fun focus_to_subgoal' (ft, 0) = - let val (lhs, rhs) = Logic.dest_implies (focus_of_fcterm ft) - in ft |> focus_left |> focus_right end - | focus_to_subgoal' (ft, i) = - let val (lhs, rhs) = Logic.dest_implies (focus_of_fcterm ft) - in focus_to_subgoal' (focus_right ft, i - 1) end - in focus_to_subgoal' (ft, j - 1) end - handle Term.TERM _ => - raise isa_focus_term_exp - ("focus_to_subgoal: No such subgoal: " ^ - (string_of_int j)); - -fun focus_to_subgoal_of_term i t = - focus_to_subgoal i (fcterm_of_term t) - -(* move focus to a specific premise *) -(* fun focus_past_params i ft = - (focus_to_subgoal (focus_right ft, i)) - handle isa_focus_term_exp _ => - raise isa_focus_term_exp - ("focus_to_prmise: No such premise: " ^ (string_of_int i)); *) - -fun focus_to_term_goal_prem (premid,gaolid) t = - 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... *) - -(* T is outer bound vars, n is number of locally bound vars *) -(* THINK: is order of Ts correct...? or reversed? *) -fun fakefree_badbounds Ts t = - let val (FakeTs,Ts,newnames) = - List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => - let val newname = Term.variant usednames n - in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs, - (newname,ty)::Ts, - newname::usednames) end) - ([],[],[]) - Ts - in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end; - -(* fun fakefree_badbounds usednames T n (a $ b) = *) -(* let val (usednames', T', a') = fakefree_badbounds usednames T n a *) -(* val (usednames'', T'', b') = fakefree_badbounds usednames' T n b in *) -(* (usednames'', T'', a' $ b') end *) -(* | fakefree_badbounds usednames T n (Abs(s,ty,t)) = *) -(* let val (usednames', T', t') = fakefree_badbounds usednames T (n + 1) t in *) -(* (usednames', T', Abs(s,ty, t')) *) -(* | fakefree_badbounds usednames T n (b as Bound i) = *) -(* let fun mkfake_bound j [] = *) -(* raise ERROR_MESSAGE "fakefree_badbounds: bound is outside of the known types!" *) -(* | mkfake_bound 0 ((s,ty)::Ts) = *) -(* let val newname = Term.variant s usednames in *) -(* usednames, (newname,ty) :: T, Free (newname,ty) *) -(* | mkfake_bound j (d::Ts) = mkfake_bound (j - 1) Ts *) -(* in if n <= i then mkfake_bound (i - n) T else b end *) -(* | fakefree_badbounds usednames T t = t; *) - - -(* note: outerterm is the taget with the match replaced by a bound - variable : ie: "P lhs" beocmes "%x. P x" - insts is the types of instantiations of vars in lhs - and typinsts is the type instantiations of types in the lhs - Note: Final rule is the rule lifted into the ontext of the - taget thm. *) -fun mk_foo_match mkuptermfunc Ts t = - let - val ty = Term.type_of t - val bigtype = (rev (map snd Ts)) ---> ty - fun mk_foo 0 t = t - | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1))) - val num_of_bnds = (length Ts) - (* foo_term = "fooabs y0 ... yn" where y's are local bounds *) - val foo_term = mk_foo num_of_bnds (Bound num_of_bnds) - in Abs("fooabs", bigtype, mkuptermfunc foo_term) end; - -(* before matching we need to fake the bound vars that are missing an -abstraction. In this function we additionally construct the -abstraction environment, and an outer context term (with the focus -abstracted out) for use in rewriting with RWInst.rw *) -fun prepmatch ft = - let - val t = focus_of_fcterm ft - val Ts = tyenv_of_focus ft - val (FakeTs', Ts', t') = fakefree_badbounds Ts t - fun mktermf t = - term_of_fcterm (set_focus_of_fcterm ft t) - val absterm = mk_foo_match mktermf Ts' t' - in - (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 -bound variables. New names have been introduced to make sure they are -unique w.r.t all names in the term and each other. usednames' is -oldnames + new names. *) -fun clean_match_ft thy pat ft = - let val (t, (FakeTs,Ts,absterm)) = prepmatch ft in - case TermLib.clean_match thy (pat, t) of - NONE => NONE - | SOME insts => SOME (insts, FakeTs, Ts, absterm) end; -(* ix = max var index *) -fun clean_unify_ft sgn ix pat ft = - let val (t, (FakeTs, Ts,absterm)) = prepmatch ft in - Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) - (TermLib.clean_unify sgn ix (t, pat)) end; - - -(* THINK: ? do we not need to incremement bound indices? *) -(* THINK: it should be the search which localisaes the search to the -current focus, not this hack in the matcher... ? *) -(* find matches below this particular focus term *) -(* The search function is to find a match within a term... *) -(* the matcher is something that is applied to each node chosen by the -searchf and the results are flattened to form a lazy list. *) -fun find_fcterm_matches searchf matcher ft = - let - val ftupterm = upterm_of ft - val focusft = focus_of_fcterm ft - val add_uptermf = add_upterm ftupterm - in - searchf - (fn ft' => matcher (add_uptermf ft')) - (fcterm_of_term focusft) - end; - -(* FIXME: move argument orders for efficiency... -i.e. wenzel style val foofunc = x o y; -*) - -(* find the matches inside subgoal i of th *) -fun find_sg_matches searchf matcher i t = - let - val subgoal_fcterm = focus_to_subgoal_of_term i t - in find_fcterm_matches searchf matcher subgoal_fcterm end; - -(* find the matches inside subgoal i of th *) -fun find_sg_thm_matches searchf matcher i th = - find_sg_matches searchf matcher i (Thm.prop_of th); - - -(* find the matches inside subgoal i's conclusion of th *) -fun find_sg_concl_matches searchf matcher i t = - let - val subgoal_fcterm = - focus_to_concl (focus_to_subgoal_of_term i t) - in - find_fcterm_matches searchf matcher subgoal_fcterm - end; - -(* find the matches inside subgoal i's conclusion of th *) -fun find_sg_concl_thm_matches searchf matcher i th = - find_sg_concl_matches searchf matcher i (Thm.prop_of th); - -end; - -(* -test... - -f_encode_isatermS.encode (read "P a"); -isafocustermS.fcterm_of_term (read "f a"); -isafocustermS.term_of_fcterm it; - -Goal "P b ==> P (suc b)"; - -TermLib.string_of_term ((focus_of_fcterm o focus_to_subgoal_of_term 1 o prop_of) (topthm())); - -TermLib.string_of_term ((focus_of_fcterm o focus_to_concl o focus_to_subgoal_of_term 1 o prop_of) (topthm())); - -TermLib.string_of_term ((focus_of_fcterm o focus_to_term_goal_prem (1,1) o prop_of) (topthm())); - -*) diff -r 81d6dc597559 -r 5181e317e9ff src/Pure/IsaPlanner/isand.ML --- a/src/Pure/IsaPlanner/isand.ML Sun Jun 11 00:28:18 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,644 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* Title: Pure/IsaPlanner/isand.ML - ID: $Id$ - Author: Lucas Dixon, University of Edinburgh - lucas.dixon@ed.ac.uk - Updated: 26 Apr 2005 - Date: 6 Aug 2004 -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* DESCRIPTION: - - Natural Deduction tools - - For working with Isabelle theorems in a natural detuction style. - ie, not having to deal with meta level quantified varaibles, - instead, we work with newly introduced frees, and hide the - "all"'s, exporting results from theorems proved with the frees, to - solve the all cases of the previous goal. This allows resolution - to do proof search normally. - - Note: A nice idea: allow exporting to solve any subgoal, thus - allowing the interleaving of proof, or provide a structure for the - ordering of proof, thus allowing proof attempts in parrell, but - recording the order to apply things in. - - debugging tools: - - fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t)); - fun asm_read s = - (assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT))); - - THINK: are we really ok with our varify name w.r.t the prop - do - we also need to avoid names in the hidden hyps? What about - unification contraints in flex-flex pairs - might they also have - extra free vars? -*) - -signature ISA_ND = -sig - - (* export data *) - datatype export = export of - {gth: Thm.thm, (* initial goal theorem *) - sgid: int, (* subgoal id which has been fixed etc *) - fixes: Thm.cterm list, (* frees *) - assumes: Thm.cterm list} (* assumptions *) - val fixes_of_exp : export -> Thm.cterm list - val export_back : export -> Thm.thm -> Thm.thm Seq.seq - val export_solution : export -> Thm.thm -> Thm.thm - val export_solutions : export list * Thm.thm -> Thm.thm - - (* inserting meta level params for frees in the conditions *) - val allify_conditions : - (Term.term -> Thm.cterm) -> - (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list - val allify_conditions' : - (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list - val assume_allified : - theory -> (string * Term.sort) list * (string * Term.typ) list - -> Term.term -> (Thm.cterm * Thm.thm) - - (* meta level fixed params (i.e. !! vars) *) - val fix_alls_in_term : Term.term -> Term.term * Term.term list - val fix_alls_term : int -> Term.term -> Term.term * Term.term list - val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list - val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list - val fix_alls : int -> Thm.thm -> Thm.thm * export - - (* meta variables in types and terms *) - val fix_tvars_to_tfrees_in_terms - : string list (* avoid these names *) - -> Term.term list -> - (((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *) - val fix_vars_to_frees_in_terms - : string list (* avoid these names *) - -> Term.term list -> - (((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *) - val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm - val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm - val fix_vars_and_tvars : - Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm - val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm - val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm - val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm - val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm - val unfix_frees_and_tfrees : - (Thm.cterm list * Thm.ctyp list) -> Thm.thm -> Thm.thm - - (* assumptions/subgoals *) - val assume_prems : - int -> Thm.thm -> Thm.thm list * Thm.thm * Thm.cterm list - val fixed_subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm) - val fixes_and_assumes : int -> Thm.thm -> Thm.thm list * Thm.thm * export - val hide_other_goals : Thm.thm -> Thm.thm * Thm.cterm list - val hide_prems : Thm.thm -> Thm.thm * Thm.cterm list - - (* abstracts cterms (vars) to locally meta-all bounds *) - val prepare_goal_export : string list * Thm.cterm list -> Thm.thm - -> int * Thm.thm - val solve_with : Thm.thm -> Thm.thm -> Thm.thm Seq.seq - val subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm) -end - - -structure IsaND -: ISA_ND -= struct - -(* Solve *some* subgoal of "th" directly by "sol" *) -(* Note: this is probably what Markus ment to do upon export of a -"show" but maybe he used RS/rtac instead, which would wrongly lead to -failing if there are premices to the shown goal. - -given: -sol : Thm.thm = [| Ai... |] ==> Ci -th : Thm.thm = - [| ... [| Ai... |] ==> Ci ... |] ==> G -results in: - [| ... [| Ai-1... |] ==> Ci-1 - [| Ai+1... |] ==> Ci+1 ... - |] ==> G -i.e. solves some subgoal of th that is identical to sol. -*) -fun solve_with sol th = - let fun solvei 0 = Seq.empty - | solvei i = - Seq.append (bicompose false (false,sol,0) i th, - solvei (i - 1)) - in - solvei (Thm.nprems_of th) - end; - - -(* Given ctertmify function, (string,type) pairs capturing the free -vars that need to be allified in the assumption, and a theorem with -assumptions possibly containing the free vars, then we give back the -assumptions allified as hidden hyps. - -Given: x -th: A vs ==> B vs -Results in: "B vs" [!!x. A x] -*) -fun allify_conditions ctermify Ts th = - let - val premts = Thm.prems_of th; - - fun allify_prem_var (vt as (n,ty),t) = - (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t))) - - fun allify_prem Ts p = foldr allify_prem_var p Ts - - val cTs = map (ctermify o Free) Ts - val cterm_asms = map (ctermify o allify_prem Ts) premts - val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms - in - (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms) - end; - -fun allify_conditions' Ts th = - allify_conditions (Thm.cterm_of (Thm.sign_of_thm th)) Ts th; - -(* allify types *) -fun allify_typ ts ty = - let - fun trec (x as (TFree (s,srt))) = - (case Library.find_first (fn (s2,srt2) => s = s2) ts - of NONE => x - | SOME (s2,_) => TVar ((s,0),srt)) - (* Maybe add in check here for bad sorts? - if srt = srt2 then TVar ((s,0),srt) - else raise ("thaw_typ", ts, ty) *) - | trec (Type (s,typs)) = Type (s, map trec typs) - | trec (v as TVar _) = v; - in trec ty end; - -(* implicit types and term *) -fun allify_term_typs ty = Term.map_term_types (allify_typ ty); - -(* allified version of term, given frees to allify over. Note that we -only allify over the types on the given allified cterm, we can't do -this for the theorem as we are not allowed type-vars in the hyp. *) -fun assume_allified sgn (tyvs,vs) t = - let - fun allify_var (vt as (n,ty),t) = - (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t))) - fun allify Ts p = List.foldr allify_var p Ts - - val ctermify = Thm.cterm_of sgn; - val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs - val allified_term = t |> allify vs; - val ct = ctermify allified_term; - val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term); - in (typ_allified_ct, - Drule.forall_elim_vars 0 (Thm.assume ct)) end; - - -(* change type-vars to fresh type frees *) -fun fix_tvars_to_tfrees_in_terms names ts = - let - val tfree_names = map fst (List.foldr Term.add_term_tfrees [] ts); - val tvars = List.foldr Term.add_term_tvars [] ts; - val (names',renamings) = - List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => - let val n2 = Term.variant Ns n in - (n2::Ns, (tv, (n2,s))::Rs) - end) (tfree_names @ names,[]) tvars; - in renamings end; -fun fix_tvars_to_tfrees th = - let - val sign = Thm.sign_of_thm th; - val ctypify = Thm.ctyp_of sign; - val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); - val renamings = fix_tvars_to_tfrees_in_terms - [] ((Thm.prop_of th) :: tpairs); - val crenamings = - map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f))) - renamings; - val fixedfrees = map snd crenamings; - in (fixedfrees, Thm.instantiate (crenamings, []) th) end; - - -(* change type-free's to type-vars *) -fun unfix_tfrees ns th = - let - val varfiytfrees = (map (fn x => Term.dest_TFree (Thm.typ_of x)) ns) - val skiptfrees = subtract (op =) varfiytfrees (Term.add_term_tfrees (Thm.prop_of th,[])); - in #2 (Thm.varifyT' skiptfrees th) end; - -(* change schematic/meta vars to fresh free vars *) -fun fix_vars_to_frees_in_terms names ts = - let - val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts); - val Ns = List.foldr Term.add_term_names names ts; - val (_,renamings) = - Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => - let val n2 = Term.variant Ns n in - (n2 :: Ns, (v, (n2,ty)) :: Rs) - end) ((Ns,[]), vars); - in renamings end; -fun fix_vars_to_frees th = - let - val ctermify = Thm.cterm_of (Thm.sign_of_thm th) - val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); - val renamings = fix_vars_to_frees_in_terms - [] ([Thm.prop_of th] @ tpairs); - val crenamings = - map (fn (v,f) => (ctermify (Var v), ctermify (Free f))) - renamings; - val fixedfrees = map snd crenamings; - in (fixedfrees, Thm.instantiate ([], crenamings) th) end; - -fun fix_tvars_upto_idx ix th = - let - val sgn = Thm.sign_of_thm th; - val ctypify = Thm.ctyp_of sgn - val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); - val prop = (Thm.prop_of th); - val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs); - val ctyfixes = - map_filter - (fn (v as ((s,i),ty)) => - if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty))) - else NONE) tvars; - in Thm.instantiate (ctyfixes, []) th end; -fun fix_vars_upto_idx ix th = - let - val sgn = Thm.sign_of_thm th; - val ctermify = Thm.cterm_of sgn - val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); - val prop = (Thm.prop_of th); - val vars = map Term.dest_Var (List.foldr Term.add_term_vars - [] (prop :: tpairs)); - val cfixes = - map_filter - (fn (v as ((s,i),ty)) => - if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty))) - else NONE) vars; - in Thm.instantiate ([], cfixes) th end; - - -(* make free vars into schematic vars with index zero *) - fun unfix_frees frees = - apply (map (K (Drule.forall_elim_var 0)) frees) - o Drule.forall_intr_list frees; - -(* fix term and type variables *) -fun fix_vars_and_tvars th = - let val (tvars, th') = fix_tvars_to_tfrees th - val (vars, th'') = fix_vars_to_frees th' - in ((vars, tvars), th'') end; - -(* implicit Thm.thm argument *) -(* assumes: vars may contain fixed versions of the frees *) -(* THINK: what if vs already has types varified? *) -fun unfix_frees_and_tfrees (vs,tvs) = - (unfix_tfrees tvs o unfix_frees vs); - -(* datatype to capture an exported result, ie a fix or assume. *) -datatype export = - export of {fixes : Thm.cterm list, (* fixed vars *) - assumes : Thm.cterm list, (* hidden hyps/assumed prems *) - sgid : int, - gth : Thm.thm}; (* subgoal/goalthm *) - -fun fixes_of_exp (export rep) = #fixes rep; - -(* export the result of the new goal thm, ie if we reduced teh -subgoal, then we get a new reduced subtgoal with the old -all-quantified variables *) -local - -(* allify puts in a meta level univ quantifier for a free variavble *) -fun allify_term (v, t) = - let val vt = #t (Thm.rep_cterm v) - val (n,ty) = Term.dest_Free vt - in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end; - -fun allify_for_sg_term ctermify vs t = - let val t_alls = foldr allify_term t vs; - val ct_alls = ctermify t_alls; - in - (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls)) - end; -(* lookup type of a free var name from a list *) -fun lookupfree vs vn = - case Library.find_first (fn (n,ty) => n = vn) vs of - NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term") - | SOME x => x; -in -fun export_back (export {fixes = vs, assumes = hprems, - sgid = i, gth = gth}) newth = - let - val sgn = Thm.sign_of_thm newth; - val ctermify = Thm.cterm_of sgn; - - val sgs = prems_of newth; - val (sgallcts, sgthms) = - Library.split_list (map (allify_for_sg_term ctermify vs) sgs); - val minimal_newth = - (Library.foldl (fn ( newth', sgthm) => - Drule.compose_single (sgthm, 1, newth')) - (newth, sgthms)); - val allified_newth = - minimal_newth - |> Drule.implies_intr_list hprems - |> Drule.forall_intr_list vs - - val newth' = Drule.implies_intr_list sgallcts allified_newth - in - bicompose false (false, newth', (length sgallcts)) i gth - end; - -(* -Given "vs" : names of free variables to abstract over, -Given cterms : premices to abstract over (P1... Pn) in terms of vs, -Given a thm of the form: -P1 vs; ...; Pn vs ==> Goal(C vs) - -Gives back: -(n, length of given cterms which have been allified - [| !! vs. P1 vs; !! vs. Pn vs |] ==> !! C vs) the allified thm -*) -(* note: C may contain further premices etc -Note that cterms is the assumed facts, ie prems of "P1" that are -reintroduced in allified form. -*) -fun prepare_goal_export (vs, cterms) th = - let - val sgn = Thm.sign_of_thm th; - val ctermify = Thm.cterm_of sgn; - - val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th)) - val cfrees = map (ctermify o Free o lookupfree allfrees) vs - - val sgs = prems_of th; - val (sgallcts, sgthms) = - Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs); - - val minimal_th = - Goal.conclude (Library.foldl (fn ( th', sgthm) => - Drule.compose_single (sgthm, 1, th')) - (th, sgthms)); - - val allified_th = - minimal_th - |> Drule.implies_intr_list cterms - |> Drule.forall_intr_list cfrees - - val th' = Drule.implies_intr_list sgallcts allified_th - in - ((length sgallcts), th') - end; - -end; - - -(* exporting function that takes a solution to the fixed/assumed goal, -and uses this to solve the subgoal in the main theorem *) -fun export_solution (export {fixes = cfvs, assumes = hcprems, - sgid = i, gth = gth}) solth = - let - val solth' = - solth |> Drule.implies_intr_list hcprems - |> Drule.forall_intr_list cfvs - in Drule.compose_single (solth', i, gth) end; - -fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs; - - -(* fix parameters of a subgoal "i", as free variables, and create an -exporting function that will use the result of this proved goal to -show the goal in the original theorem. - -Note, an advantage of this over Isar is that it supports instantiation -of unkowns in the earlier theorem, ie we can do instantiation of meta -vars! - -avoids constant, free and vars names. - -loosely corresponds to: -Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm -Result: - ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, - expf : - ("As ==> SGi x'" : thm) -> - ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) -*) -fun fix_alls_in_term alledt = - let - val t = Term.strip_all_body alledt; - val alls = rev (Term.strip_all_vars alledt); - val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t) - val names = Term.add_term_names (t,varnames); - val fvs = map Free - ((Term.variantlist (map fst alls, names)) - ~~ (map snd alls)); - in ((subst_bounds (fvs,t)), fvs) end; - -fun fix_alls_term i t = - let - val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t) - val names = Term.add_term_names (t,varnames); - val gt = Logic.get_goal t i; - val body = Term.strip_all_body gt; - val alls = rev (Term.strip_all_vars gt); - val fvs = map Free - ((Term.variantlist (map fst alls, names)) - ~~ (map snd alls)); - in ((subst_bounds (fvs,body)), fvs) end; - -fun fix_alls_cterm i th = - let - val ctermify = Thm.cterm_of (Thm.sign_of_thm th); - val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th); - val cfvs = rev (map ctermify fvs); - val ct_body = ctermify fixedbody - in - (ct_body, cfvs) - end; - -fun fix_alls' i = - (apfst Thm.trivial) o (fix_alls_cterm i); - - -(* hide other goals *) -(* note the export goal is rotated by (i - 1) and will have to be -unrotated to get backto the originial position(s) *) -fun hide_other_goals th = - let - (* tl beacuse fst sg is the goal we are interested in *) - val cprems = tl (Drule.cprems_of th) - val aprems = map Thm.assume cprems - in - (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, - cprems) - end; - -(* a nicer version of the above that leaves only a single subgoal (the -other subgoals are hidden hyps, that the exporter suffles about) -namely the subgoal that we were trying to solve. *) -(* loosely corresponds to: -Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm -Result: - ("(As ==> SGi x') ==> SGi x'" : thm, - expf : - ("SGi x'" : thm) -> - ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) -*) -fun fix_alls i th = - let - val (fixed_gth, fixedvars) = fix_alls' i th - val (sml_gth, othergoals) = hide_other_goals fixed_gth - in - (sml_gth, export {fixes = fixedvars, - assumes = othergoals, - sgid = i, gth = th}) - end; - - -(* assume the premises of subgoal "i", this gives back a list of -assumed theorems that are the premices of subgoal i, it also gives -back a new goal thm and an exporter, the new goalthm is as the old -one, but without the premices, and the exporter will use a proof of -the new goalthm, possibly using the assumed premices, to shoe the -orginial goal. - -Note: Dealing with meta vars, need to meta-level-all them in the -shyps, which we can later instantiate with a specific value.... ? -think about this... maybe need to introduce some new fixed vars and -then remove them again at the end... like I do with rw_inst. - -loosely corresponds to: -Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm -Result: -(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions - "SGi ==> SGi" : thm, -- new goal - "SGi" ["A0" ... "An"] : thm -> -- export function - ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list) -*) -fun assume_prems i th = - let - val t = (prop_of th); - val gt = Logic.get_goal t i; - val _ = case Term.strip_all_vars gt of [] => () - | _ => error "assume_prems: goal has params" - val body = gt; - val prems = Logic.strip_imp_prems body; - val concl = Logic.strip_imp_concl body; - - val sgn = Thm.sign_of_thm th; - val ctermify = Thm.cterm_of sgn; - val cprems = map ctermify prems; - val aprems = map Thm.assume cprems; - val gthi = Thm.trivial (ctermify concl); - - (* fun explortf thi = - Drule.compose (Drule.implies_intr_list cprems thi, - i, th) *) - in - (aprems, gthi, cprems) - end; - - -(* first fix the variables, then assume the assumptions *) -(* loosely corresponds to: -Given - "[| SG0; ... - !! xs. [| A0 xs; ... An xs |] ==> SGi xs; - ... SGm |] ==> G" : thm -Result: -(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions - "SGi xs' ==> SGi xs'" : thm, -- new goal - "SGi xs'" ["A0 xs'" ... "An xs'"] : thm -> -- export function - ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list) -*) - -(* Note: the fix_alls actually pulls through all the assumptions which -means that the second export is not needed. *) -fun fixes_and_assumes i th = - let - val (fixgth, exp1) = fix_alls i th - val (assumps, goalth, _) = assume_prems 1 fixgth - in - (assumps, goalth, exp1) - end; - - -(* Fixme: allow different order of subgoals given to expf *) -(* make each subgoal into a separate thm that needs to be proved *) -(* loosely corresponds to: -Given - "[| SG0; ... SGm |] ==> G" : thm -Result: -(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals - ["SG0", ..., "SGm"] : thm list -> -- export function - "G" : thm) -*) -fun subgoal_thms th = - let - val t = (prop_of th); - - val prems = Logic.strip_imp_prems t; - - val sgn = Thm.sign_of_thm th; - val ctermify = Thm.cterm_of sgn; - - val aprems = map (Thm.trivial o ctermify) prems; - - fun explortf premths = - Drule.implies_elim_list th premths - in - (aprems, explortf) - end; - - -(* make all the premices of a theorem hidden, and provide an unhide -function, that will bring them back out at a later point. This is -useful if you want to get back these premices, after having used the -theorem with the premices hidden *) -(* loosely corresponds to: -Given "As ==> G" : thm -Result: ("G [As]" : thm, - "G [As]" : thm -> "As ==> G" : thm -*) -fun hide_prems th = - let - val cprems = Drule.cprems_of th; - val aprems = map Thm.assume cprems; - (* val unhidef = Drule.implies_intr_list cprems; *) - in - (Drule.implies_elim_list th aprems, cprems) - end; - - - - -(* Fixme: allow different order of subgoals in exportf *) -(* as above, but also fix all parameters in all subgoals, and uses -fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent -subgoals. *) -(* loosely corresponds to: -Given - "[| !! x0s. A0s x0s ==> SG0 x0s; - ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm -Result: -(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", - ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals - ["SG0 x0s'", ..., "SGm xms'"] : thm list -> -- export function - "G" : thm) -*) -(* requires being given solutions! *) -fun fixed_subgoal_thms th = - let - val (subgoals, expf) = subgoal_thms th; -(* fun export_sg (th, exp) = exp th; *) - fun export_sgs expfs solthms = - expf (map2 (curry (op |>)) solthms expfs); -(* expf (map export_sg (ths ~~ expfs)); *) - in - apsnd export_sgs (Library.split_list (map (apsnd export_solution o - fix_alls 1) subgoals)) - end; - -end; diff -r 81d6dc597559 -r 5181e317e9ff src/Pure/IsaPlanner/isaplib.ML --- a/src/Pure/IsaPlanner/isaplib.ML Sun Jun 11 00:28:18 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,317 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* Title: Pure/IsaPlanner/isaplib.ML - ID: $Id$ - Author: Lucas Dixon, University of Edinburgh - lucasd@dai.ed.ac.uk -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* DESCRIPTION: - - A few useful system-independent utilities. -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -signature ISAP_LIB = -sig - (* seq operations *) - val ALL_BUT_LAST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq - val FST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq - val NTH : int -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq - val all_but_last_of_seq : 'a Seq.seq -> 'a Seq.seq - val nat_seq : int Seq.seq - val nth_of_seq : int -> 'a Seq.seq -> 'a option - val pair_seq : 'a Seq.seq -> 'b Seq.seq -> ('a * 'b) Seq.seq - val number_seq : 'a Seq.seq -> (int * 'a) Seq.seq - - datatype 'a skipseqT = - skipmore of int - | skipseq of 'a Seq.seq Seq.seq; - val skipto_seqseq : int -> 'a Seq.seq Seq.seq -> 'a skipseqT - val seqflat_seq : 'a Seq.seq Seq.seq -> 'a Seq.seq - - (* lists *) - val mk_num_list : int -> int list - val number_list : int -> 'a list -> (int * 'a) list - val repeated_list : int -> 'a -> 'a list - val all_pairs : 'a list -> 'b list -> ('a * 'b) list - val get_ends_of : ('a * 'a -> bool) -> - ('a * 'a) -> 'a list -> ('a * 'a) - val flatmap : ('a -> 'b list) -> 'a list -> 'b list - - val lrem : ('a * 'b -> bool) -> 'a list -> 'b list -> 'b list - val forall_list : ('a -> bool) -> 'a list -> bool - - (* the list of lists with one of each of the original sublists *) - val one_of_each : 'a list list -> 'a list list - - (* type changing *) - exception NOT_A_DIGIT of string - val int_of_string : string -> int - - (* string manipulations *) - val remove_end_spaces : string -> string - val str_indent : string -> string - val string_of_intlist : int list -> string - val string_of_list : ('a -> string) -> 'a list -> string - - (* options *) - val aptosome : 'a option -> ('a -> 'b) -> 'b option - val seq_mapfilter : ('a -> 'b option) -> 'a Seq.seq -> 'b Seq.seq - val seq_map_to_some_filter : ('a -> 'b) -> 'a option Seq.seq - -> 'b Seq.seq -end; - - - -structure IsaPLib : ISAP_LIB = -struct - -(* Seq *) -fun seq_map_to_some_filter f = Seq.map_filter (Option.map f); -fun seq_mapfilter f = Seq.map_filter f; - -(* the sequence of natural numbers *) -val nat_seq = - let fun nseq i () = SOME (i, Seq.make (nseq (i+1))) - in Seq.make (nseq 1) - end; - -(* a simple function to pair with each element of a list, a number *) -fun number_list i [] = [] - | number_list i (h::t) = - (i,h)::(number_list (i+1) t) - -(* create a sequence of pairs of the elements of the two sequences - If one sequence becomes empty, then so does the pairing of them. - - This is particularly useful if you wish to perform counting or - other repeated operations on a sequence and you want to combvine - this infinite sequence with a possibly finite one. - - behaviour: - s1: a1, a2, ... an - s2: b1, b2, ... bn ... - - pair_seq s1 s2: (a1,b1), (a2,b2), ... (an,bn) -*) -fun pair_seq seq1 seq2 = - let - fun pseq s1 s2 () = - case Seq.pull s1 of - NONE => NONE - | SOME (s1h, s1t) => - case Seq.pull s2 of - NONE => NONE - | SOME (s2h, s2t) => - SOME ((s1h, s2h), Seq.make (pseq s1t s2t)) - in - Seq.make (pseq seq1 seq2) - end; - -(* number a sequence *) -fun number_seq s = pair_seq nat_seq s; - -(* cuts off the last element of a sequence *) -fun all_but_last_of_seq s = - let - fun f () = - case Seq.pull s of - NONE => NONE - | SOME (a, s2) => - (case Seq.pull s2 of - NONE => NONE - | SOME (a2,s3) => - SOME (a, all_but_last_of_seq (Seq.cons a2 s3))) - in - Seq.make f - end; - - fun ALL_BUT_LAST r st = all_but_last_of_seq (r st); - - - (* nth elem for sequenes, return none if out of bounds *) - fun nth_of_seq i l = - (case Seq.pull l of - NONE => NONE - | SOME (x, xq) => - if i <= 1 then SOME x - else nth_of_seq (i - 1) xq); - - (* for use with tactics... gives no_tac if element isn't there *) - fun NTH n f st = - (case nth_of_seq n (f st) of - NONE => Seq.empty - | SOME r => Seq.single r); - - (* First result of a tactic... uses NTH, so if there is no elements, - - then no_tac is returned. *) - fun FST f = NTH 1 f; - -datatype 'a skipseqT = skipmore of int - | skipseq of 'a Seq.seq Seq.seq; -(* given a seqseq, skip the first m non-empty seq's *) -fun skipto_seqseq m s = - let - fun skip_occs n sq = - case Seq.pull sq of - NONE => skipmore n - | SOME (h,t) => - (case Seq.pull h of NONE => skip_occs n t - | SOME _ => if n <= 1 then skipseq (Seq.cons h t) - else skip_occs (n - 1) t) - in (skip_occs m s) end; - -(* handy function for re-arranging Sequence operations *) -(* [[a,b,c],[d,e],...] => flatten [[a,d,...], [b,e,...], [c, ...]] *) -fun seqflat_seq ss = - let - fun pulltl LL () = - (case Seq.pull LL of - NONE => NONE - | SOME (hL,tLL) => - (case Seq.pull hL of - NONE => pulltl tLL () - | SOME (h,tL) => - SOME (h, Seq.make (recf (tLL, (Seq.single tL)))))) - and recf (fstLL,sndLL) () = - (case Seq.pull fstLL of - NONE => pulltl sndLL () - | SOME (hL, tLL) => - (case Seq.pull hL of - NONE => recf (tLL, sndLL) () - | SOME (h,tL) => - SOME (h, Seq.make (recf (tLL, Seq.append (sndLL, Seq.single tL)))))) - in Seq.make (pulltl ss) end; -(* tested with: -val ss = Seq.of_list [Seq.of_list [1,2,3], Seq.of_list [4,5], Seq.of_list [7,8,9,10]]; -Seq.list_of (seqflat_seq ss); -val it = [1, 4, 7, 2, 5, 8, 3, 9, 10] : int list -*) - - - - (* create a list opf the form (n, n-1, n-2, ... ) *) - fun mk_num_list n = - if n < 1 then [] else (n :: (mk_num_list (n-1))); - - fun repeated_list n a = - if n < 1 then [] else (a :: (repeated_list (n-1) a)); - - (* create all possible pairs with fst element from the first list - and snd element from teh second list *) - fun all_pairs xs ys = - let - fun all_pairs_aux yss [] _ acc = acc - | all_pairs_aux yss (x::xs) [] acc = - all_pairs_aux yss xs yss acc - | all_pairs_aux yss (xs as (x1::x1s)) (y::ys) acc = - all_pairs_aux yss xs ys ((x1,y)::acc) - in - all_pairs_aux ys xs ys [] - end; - - - (* create all possible pairs with fst element from the first list - and snd element from teh second list *) - (* FIXME: make tail recursive and quick *) - fun one_of_each [] = [] - | one_of_each [[]] = [] - | one_of_each [(h::t)] = [h] :: (one_of_each [t]) - | one_of_each ([] :: xs) = [] - | one_of_each ((h :: t) :: xs) = - (map (fn z => h :: z) (one_of_each xs)) - @ (one_of_each (t :: xs)); - - -(* function to get the upper/lower bounds of a list -given: -gr : 'a * 'a -> bool = greater than check -e as (u,l) : ('a * 'a) = upper and lower bits -l : 'a list = the list to get the upper and lower bounds of -returns a pair ('a * 'a) of the biggest and lowest value w.r.t "gr" -*) -fun get_ends_of gr (e as (u,l)) [] = e - | get_ends_of gr (e as (u,l)) (h :: t) = - if gr(h,u) then get_ends_of gr (h,l) t - else if gr(l,h) then get_ends_of gr (u,h) t - else get_ends_of gr (u,l) t; - -fun flatmap f = maps f; - - (* quick removal of "rs" elements from "ls" when (eqf (r,l)) is true - Ignores ordering. *) - fun lrem eqf rs ls = - let fun list_remove rs ([],[]) = [] - | list_remove [] (xs,_) = xs - | list_remove (r::rs) ([],leftovers) = - list_remove rs (leftovers,[]) - | list_remove (r1::rs) ((x::xs),leftovers) = - if eqf (r1, x) then list_remove (r1::rs) (xs,leftovers) - else list_remove (r1::rs) (xs, x::leftovers) - in - list_remove rs (ls,[]) - end; - -fun forall_list f [] = true - | forall_list f (a::t) = f a orelse forall_list f t; - - - (* crappy string indeter *) - fun str_indent s = - implode (map (fn s => if s = "\n" then "\n " else s) (explode s)); - - - fun remove_end_spaces s = - let - fun rem_starts [] = [] - | rem_starts (" " :: t) = rem_starts t - | rem_starts ("\t" :: t) = rem_starts t - | rem_starts ("\n" :: t) = rem_starts t - | rem_starts l = l - fun rem_ends l = rev (rem_starts (rev l)) - in - implode (rem_ends (rem_starts (explode s))) - end; - -(* convert a string to an integer *) - exception NOT_A_DIGIT of string; - - fun int_of_string s = - let - fun digits_to_int [] x = x - | digits_to_int (h :: t) x = digits_to_int t (x * 10 + h); - - fun char_to_digit c = - case c of - "0" => 0 - | "1" => 1 - | "2" => 2 - | "3" => 3 - | "4" => 4 - | "5" => 5 - | "6" => 6 - | "7" => 7 - | "8" => 8 - | "9" => 9 - | _ => raise NOT_A_DIGIT c - in - digits_to_int (map char_to_digit (explode (remove_end_spaces s))) 0 - end; - - (* Debugging/printing code for this datatype *) - fun string_of_list f l = - let - fun auxf [] = "" - | auxf [a] = (f a) - | auxf (h :: (t as (h2 :: t2))) = (f h) ^ ", " ^ (auxf t) - in - "[" ^ (auxf l) ^ "]" - end; - - val string_of_intlist = string_of_list string_of_int; - - - (* options *) - fun aptosome opt f = Option.map f opt; - -end; diff -r 81d6dc597559 -r 5181e317e9ff src/Pure/IsaPlanner/rw_inst.ML --- a/src/Pure/IsaPlanner/rw_inst.ML Sun Jun 11 00:28:18 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,304 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* Title: Pure/IsaPlanner/rw_inst.ML - ID: $Id$ - Author: Lucas Dixon, University of Edinburgh - lucas.dixon@ed.ac.uk - Created: 25 Aug 2004 -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* DESCRIPTION: - - rewriting using a conditional meta-equality theorem which supports - schematic variable instantiation. - -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -signature RW_INST = -sig - - (* Rewrite: give it instantiation infromation, a rule, and the - target thm, and it will return the rewritten target thm *) - val rw : - ((Term.indexname * (Term.sort * Term.typ)) list * (* type var instantiations *) - (Term.indexname * (Term.typ * Term.term)) list) (* schematic var instantiations *) - * (string * Term.typ) list (* Fake named bounds + types *) - * (string * Term.typ) list (* names of bound + types *) - * Term.term -> (* outer term for instantiation *) - Thm.thm -> (* rule with indexies lifted *) - Thm.thm -> (* target thm *) - Thm.thm (* rewritten theorem possibly - with additional premises for - rule conditions *) - - (* used tools *) - val mk_abstractedrule : - (string * Term.typ) list (* faked outer bound *) - -> (string * Term.typ) list (* hopeful name of outer bounds *) - -> Thm.thm -> Thm.cterm list * Thm.thm - val mk_fixtvar_tyinsts : - (Term.indexname * (Term.sort * Term.typ)) list -> - Term.term list -> ((string * int) * (Term.sort * Term.typ)) list - * (string * Term.sort) list - val mk_renamings : - Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list - val new_tfree : - ((string * int) * Term.sort) * - (((string * int) * (Term.sort * Term.typ)) list * string list) -> - ((string * int) * (Term.sort * Term.typ)) list * string list - val cross_inst : (Term.indexname * (Term.typ * Term.term)) list - -> (Term.indexname *(Term.typ * Term.term)) list - val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list - -> (Term.indexname * (Term.sort * Term.typ)) list - - val beta_contract : Thm.thm -> Thm.thm - val beta_eta_contract : Thm.thm -> Thm.thm - -end; - -structure RWInst -(* : RW_INST *) -= struct - - -(* beta contract the theorem *) -fun beta_contract thm = - equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm; - -(* beta-eta contract the theorem *) -fun beta_eta_contract thm = - let - val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm - val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 - in thm3 end; - -(* Given a list of variables that were bound, and a that has been -instantiated with free variable placeholders for the bound vars, it -creates an abstracted version of the theorem, with local bound vars as -lambda-params: - -Ts: -("x", ty) - -rule:: -C :x ==> P :x = Q :x - -results in: -("!! x. C x", (%x. p x = %y. p y) [!! x. C x]) - -note: assumes rule is instantiated -*) -(* Note, we take abstraction in the order of last abstraction first *) -fun mk_abstractedrule TsFake Ts rule = - let - val ctermify = Thm.cterm_of (Thm.sign_of_thm rule); - - (* now we change the names of temporary free vars that represent - bound vars with binders outside the redex *) - val prop = Thm.prop_of rule; - val names = TermLib.usednames_of_thm rule; - val (fromnames,tonames,names2,Ts') = - Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => - let val n2 = Term.variant names n in - (ctermify (Free(faken,ty)) :: rnf, - ctermify (Free(n2,ty)) :: rnt, - n2 :: names, - (n2,ty) :: Ts'') - end) - (([],[],names, []), TsFake~~Ts); - - (* rename conflicting free's in the rule to avoid cconflicts - with introduced vars from bounds outside in redex *) - val rule' = rule |> Drule.forall_intr_list fromnames - |> Drule.forall_elim_list tonames; - - (* make unconditional rule and prems *) - val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts') - rule'; - - (* using these names create lambda-abstracted version of the rule *) - val abstractions = rev (Ts' ~~ tonames); - val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) => - Thm.abstract_rule n ct th) - (uncond_rule, abstractions); - in (cprems, abstract_rule) end; - - -(* given names to avoid, and vars that need to be fixed, it gives -unique new names to the vars so that they can be fixed as free -variables *) -(* make fixed unique free variable instantiations for non-ground vars *) -(* Create a table of vars to be renamed after instantiation - ie - other uninstantiated vars in the hyps of the rule - ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) -fun mk_renamings tgt rule_inst = - let - val rule_conds = Thm.prems_of rule_inst - val names = foldr Term.add_term_names [] (tgt :: rule_conds); - val (conds_tyvs,cond_vs) = - Library.foldl (fn ((tyvs, vs), t) => - (Library.union - (Term.term_tvars t, tyvs), - Library.union - (map Term.dest_Var (Term.term_vars t), vs))) - (([],[]), rule_conds); - val termvars = map Term.dest_Var (Term.term_vars tgt); - val vars_to_fix = Library.union (termvars, cond_vs); - val (renamings, names2) = - foldr (fn (((n,i),ty), (vs, names')) => - let val n' = Term.variant names' n in - ((((n,i),ty), Free (n', ty)) :: vs, n'::names') - end) - ([], names) vars_to_fix; - in renamings end; - -(* make a new fresh typefree instantiation for the given tvar *) -fun new_tfree (tv as (ix,sort), (pairs,used)) = - let val v = variant used (string_of_indexname ix) - in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; - - -(* make instantiations to fix type variables that are not - already instantiated (in ignore_ixs) from the list of terms. *) -fun mk_fixtvar_tyinsts ignore_insts ts = - let - val ignore_ixs = map fst ignore_insts; - val (tvars, tfrees) = - foldr (fn (t, (varixs, tfrees)) => - (Term.add_term_tvars (t,varixs), - Term.add_term_tfrees (t,tfrees))) - ([],[]) ts; - val unfixed_tvars = - List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars; - val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars - in (fixtyinsts, tfrees) end; - - -(* cross-instantiate the instantiations - ie for each instantiation -replace all occurances in other instantiations - no loops are possible -and thus only one-parsing of the instantiations is necessary. *) -fun cross_inst insts = - let - fun instL (ix, (ty,t)) = - map (fn (ix2,(ty2,t2)) => - (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2))); - - fun cross_instL ([], l) = rev l - | cross_instL ((ix, t) :: insts, l) = - cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); - - in cross_instL (insts, []) end; - -(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *) -fun cross_inst_typs insts = - let - fun instL (ix, (srt,ty)) = - map (fn (ix2,(srt2,ty2)) => - (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2))); - - fun cross_instL ([], l) = rev l - | cross_instL ((ix, t) :: insts, l) = - cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); - - in cross_instL (insts, []) end; - - -(* assume that rule and target_thm have distinct var names. THINK: -efficient version with tables for vars for: target vars, introduced -vars, and rule vars, for quicker instantiation? The outerterm defines -which part of the target_thm was modified. Note: we take Ts in the -upterm order, ie last abstraction first., and with an outeterm where -the abstracted subterm has the arguments in the revered order, ie -first abstraction first. FakeTs has abstractions using the fake name -- ie the name distinct from all other abstractions. *) - -fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = - let - (* general signature info *) - val target_sign = (Thm.sign_of_thm target_thm); - val ctermify = Thm.cterm_of target_sign; - val ctypeify = Thm.ctyp_of target_sign; - - (* fix all non-instantiated tvars *) - val (fixtyinsts, othertfrees) = - mk_fixtvar_tyinsts nonfixed_typinsts - [Thm.prop_of rule, Thm.prop_of target_thm]; - val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty)) - fixtyinsts; - val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); - - (* certified instantiations for types *) - val ctyp_insts = - map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) - typinsts; - - (* type instantiated versions *) - val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; - val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule; - - val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts; - (* type instanitated outer term *) - val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; - - val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) - FakeTs; - val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) - Ts; - - (* type-instantiate the var instantiations *) - val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => - (ix, (Term.typ_subst_TVars term_typ_inst ty, - Term.subst_TVars term_typ_inst t)) - :: insts_tyinst) - [] unprepinsts; - - (* cross-instantiate *) - val insts_tyinst_inst = cross_inst insts_tyinst; - - (* create certms of instantiations *) - val cinsts_tyinst = - map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)), - ctermify t)) insts_tyinst_inst; - - (* The instantiated rule *) - val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst); - - (* Create a table of vars to be renamed after instantiation - ie - other uninstantiated vars in the hyps the *instantiated* rule - ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) - val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst) - rule_inst; - val cterm_renamings = - map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings; - - (* Create the specific version of the rule for this target application *) - val outerterm_inst = - outerterm_tyinst - |> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst) - |> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings); - val couter_inst = Thm.reflexive (ctermify outerterm_inst); - val (cprems, abstract_rule_inst) = - rule_inst |> Thm.instantiate ([], cterm_renamings) - |> mk_abstractedrule FakeTs_tyinst Ts_tyinst; - val specific_tgt_rule = - beta_eta_contract - (Thm.combination couter_inst abstract_rule_inst); - - (* create an instantiated version of the target thm *) - val tgt_th_inst = - tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst) - |> Thm.instantiate ([], cterm_renamings); - - val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; - - in - (beta_eta_contract tgt_th_inst) - |> Thm.equal_elim specific_tgt_rule - |> Drule.implies_intr_list cprems - |> Drule.forall_intr_list frees_of_fixed_vars - |> Drule.forall_elim_list vars - |> Thm.varifyT' othertfrees - |-> K Drule.zero_var_indexes - end; - - -end; (* struct *) diff -r 81d6dc597559 -r 5181e317e9ff src/Pure/IsaPlanner/rw_tools.ML --- a/src/Pure/IsaPlanner/rw_tools.ML Sun Jun 11 00:28:18 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,195 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* Title: Pure/IsaPlanner/rw_tools.ML - ID: $Id$ - Author: Lucas Dixon, University of Edinburgh - lucas.dixon@ed.ac.uk - Created: 28 May 2004 -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* DESCRIPTION: - - term related tools used for rewriting - -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) - -signature RWTOOLS = -sig -end; - -structure RWTools -= struct - -(* THINKABOUT: don't need this: should be able to generate the paired - NsTs directly ? --already implemented as ~~ -fun join_lists ([],[]) = [] - | join_lists (x::xs, y::ys) = (x,y) :: (join_lists (xs,ys)) - | join_lists (_, _) = raise ERROR_MESSAGE "join_lists: unequal size lists"; - *) - -(* fake free variable names for locally bound variables - these work -as placeholders. *) - -(* don't use dest_fake.. - we should instead be working with numbers -and a list... else we rely on naming conventions which can break, or -be violated - in contrast list locations are correct by -construction/definition. *) -(* -fun dest_fake_bound_name n = - case (explode n) of - (":" :: realchars) => implode realchars - | _ => n; *) -fun is_fake_bound_name n = (hd (explode n) = ":"); -fun mk_fake_bound_name n = ":b_" ^ n; - - - -(* fake free variable names for local meta variables - these work -as placeholders. *) -fun dest_fake_fix_name n = - case (explode n) of - ("@" :: realchars) => implode realchars - | _ => n; -fun is_fake_fix_name n = (hd (explode n) = "@"); -fun mk_fake_fix_name n = "@" ^ n; - - - -(* fake free variable names for meta level bound variables *) -fun dest_fake_all_name n = - case (explode n) of - ("+" :: realchars) => implode realchars - | _ => n; -fun is_fake_all_name n = (hd (explode n) = "+"); -fun mk_fake_all_name n = "+" ^ n; - - - - -(* Ys and Ts not used, Ns are real names of faked local bounds, the -idea is that this will be mapped to free variables thus if a free -variable is a faked local bound then we change it to being a meta -variable so that it can later be instantiated *) -(* FIXME: rename this - avoid the word fix! *) -(* note we are not really "fix"'ing the free, more like making it variable! *) -(* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) = - if n mem Ns then Var((n,0),ty) else Free (n,ty); -*) - -(* make a var into a fixed free (ie prefixed with "@") *) -fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty); - - -(* mk_frees_bound: string list -> Term.term -> Term.term *) -(* This function changes free variables to being represented as bound -variables if the free's variable name is in the given list. The debruijn -index is simply the position in the list *) -(* THINKABOUT: danger of an existing free variable with the same name: fix -this so that name conflict are avoided automatically! In the meantime, -don't have free variables named starting with a ":" *) -fun bounds_of_fakefrees Ys (a $ b) = - (bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b) - | bounds_of_fakefrees Ys (Abs(n,ty,t)) = - Abs(n,ty, bounds_of_fakefrees (n::Ys) t) - | bounds_of_fakefrees Ys (Free (n,ty)) = - let fun try_mk_bound_of_free (i,[]) = Free (n,ty) - | try_mk_bound_of_free (i,(y::ys)) = - if n = y then Bound i else try_mk_bound_of_free (i+1,ys) - in try_mk_bound_of_free (0,Ys) end - | bounds_of_fakefrees Ys t = t; - - -(* map a function f onto each free variables *) -fun map_to_frees f Ys (a $ b) = - (map_to_frees f Ys a) $ (map_to_frees f Ys b) - | map_to_frees f Ys (Abs(n,ty,t)) = - Abs(n,ty, map_to_frees f ((n,ty)::Ys) t) - | map_to_frees f Ys (Free a) = - f Ys a - | map_to_frees f Ys t = t; - - -(* map a function f onto each meta variable *) -fun map_to_vars f Ys (a $ b) = - (map_to_vars f Ys a) $ (map_to_vars f Ys b) - | map_to_vars f Ys (Abs(n,ty,t)) = - Abs(n,ty, map_to_vars f ((n,ty)::Ys) t) - | map_to_vars f Ys (Var a) = - f Ys a - | map_to_vars f Ys t = t; - -(* map a function f onto each free variables *) -fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) = - let val (n2,ty2) = f (n,ty) - in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end - | map_to_alls f x = x; - -(* map a function f to each type variable in a term *) -(* implicit arg: term *) -fun map_to_term_tvars f = - Term.map_term_types (fn TVar(ix,ty) => f (ix,ty) | x => x); - - - -(* what if a param desn't occur in the concl? think about! Note: This -simply fixes meta level univ bound vars as Frees. At the end, we will -change them back to schematic vars that will then unify -appropriactely, ie with unfake_vars *) -fun fake_concl_of_goal gt i = - let - val prems = Logic.strip_imp_prems gt - val sgt = List.nth (prems, i - 1) - - val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt) - val tparams = Term.strip_all_vars sgt - - val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) - tparams - in - Term.subst_bounds (rev fakefrees,tbody) - end; - -(* what if a param desn't occur in the concl? think about! Note: This -simply fixes meta level univ bound vars as Frees. At the end, we will -change them back to schematic vars that will then unify -appropriactely, ie with unfake_vars *) -fun fake_goal gt i = - let - val prems = Logic.strip_imp_prems gt - val sgt = List.nth (prems, i - 1) - - val tbody = Term.strip_all_body sgt - val tparams = Term.strip_all_vars sgt - - val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) - tparams - in - Term.subst_bounds (rev fakefrees,tbody) - end; - - -(* hand written - for some reason the Isabelle version in drule is broken! -Example? something to do with Bin Yangs examples? - *) -fun rename_term_bvars ns (Abs(s,ty,t)) = - let val s2opt = Library.find_first (fn (x,y) => s = x) ns - in case s2opt of - NONE => (Abs(s,ty,rename_term_bvars ns t)) - | SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end - | rename_term_bvars ns (a$b) = - (rename_term_bvars ns a) $ (rename_term_bvars ns b) - | rename_term_bvars _ x = x; - -fun rename_thm_bvars ns th = - let val t = Thm.prop_of th - in Thm.rename_boundvars t (rename_term_bvars ns t) th end; - -(* Finish this to show how it breaks! (raises the exception): - -exception rename_thm_bvars_exp of ((string * string) list * Thm.thm) - - Drule.rename_bvars ns th - handle TERM _ => raise rename_thm_bvars_exp (ns, th); -*) - -end; diff -r 81d6dc597559 -r 5181e317e9ff src/Pure/IsaPlanner/term_lib.ML --- a/src/Pure/IsaPlanner/term_lib.ML Sun Jun 11 00:28:18 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,676 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* Title: Pure/IsaPlanner/term_lib.ML - ID: $Id$ - Author: Lucas Dixon, University of Edinburgh - lucasd@dai.ed.ac.uk - Created: 17 Aug 2002 -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* DESCRIPTION: - - Additional code to work with terms. - -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -signature TERM_LIB = -sig - val fo_term_height : term -> int - val ho_term_height : term -> int - - (* Matching/unification with exceptions handled *) - val clean_match : theory -> term * term - -> ((indexname * (sort * typ)) list - * (indexname * (typ * term)) list) option - val clean_unify : theory -> int -> term * term - -> ((indexname * (sort * typ)) list - * (indexname * (typ * term)) list) Seq.seq - - (* managing variables in terms, can doing conversions *) - val bounds_to_frees : term -> term - val bounds_to_frees_with_vars : - (string * typ) list -> term -> term - - val change_bounds_to_frees : term -> term - val change_frees_to_vars : term -> term - val change_vars_to_frees : term -> term - val loose_bnds_to_frees : - (string * typ) list -> term -> term - - (* make all variables named uniquely *) - val unique_namify : term -> term - - (* breasking up a term and putting it into a normal form - independent of internal term context *) - val cleaned_term_conc : term -> term - val cleaned_term_parts : term -> term list * term - val cterm_of_term : term -> cterm - - (* terms of theorems and subgoals *) - val term_of_thm : thm -> term - val get_prems_of_sg_term : term -> term list - val triv_thm_from_string : string -> thm - - (* some common term manipulations *) - val try_dest_Trueprop : term -> term - - val bot_left_leaf_of : term -> term - val bot_left_leaf_noabs_of : term -> term - - (* term containing another term - an embedding check *) - val term_contains : term -> term -> bool - - (* name-convertable checking - like ae-convertable, but allows for - var's and free's to be mixed - and doesn't used buggy code. :-) *) - val get_name_eq_member : term -> term list -> term option - val name_eq_member : term -> term list -> bool - val term_name_eq : - term -> - term -> - (term * term) list -> - (term * term) list option - - (* is the typ a function or is it atomic *) - val is_fun_typ : typ -> bool - val is_atomic_typ : typ -> bool - - (* variable analysis *) - val is_some_kind_of_var : term -> bool - val same_var_check : - ''a -> ''b -> (''a * ''b) list -> (''a * ''b) list option - val has_new_vars : term * term -> bool - val has_new_typ_vars : term * term -> bool - (* checks to see if the lhs -> rhs is a invalid rewrite rule *) - val is_not_valid_rwrule : theory -> (term * term) -> bool - - (* get the frees in a term that are of atomic type, ie non-functions *) - val atomic_frees_of_term : term -> (string * typ) list - - (* get used names in a theorem to avoid upon instantiation. *) - val usednames_of_term : term -> string list - val usednames_of_thm : thm -> string list - - (* Isar term skolemisationm and unsolemisation *) - (* I think this is written also in IsarRTechn and also in somewhere else *) - (* val skolemise_term : (string,typ) list -> term -> term *) - val unskolemise_all_term : - term -> - (((string * typ) * string) list * term) - - (* given a string describing term then a string for its type, returns - read term *) - val readwty : string -> string -> term - - (* pretty stuff *) - val print_term : term -> unit - val pretty_print_sort : string list -> string - val pretty_print_term : term -> string - val pretty_print_type : typ -> string - val pretty_print_typelist : - typ list -> (typ -> string) -> string - - (* for debugging: quickly get a string of a term w.r.t the_context() *) - val string_of_term : term -> string - - (* Pretty printing in a way that allows them to be parsed by ML. - these are perhaps redundent, check the standard basis - lib for generic versions for any datatype? *) - val writesort : string list -> unit - val writeterm : term -> unit - val writetype : typ -> unit - end - - -structure TermLib : TERM_LIB = -struct - -(* Two kinds of depth measure for HOAS terms, a first order (flat) and a - higher order one. - Note: not stable of eta-contraction: embedding eta-expands term, - thus we assume eta-expanded *) -fun fo_term_height (a $ b) = - Int.max (1 + fo_term_height b, (fo_term_height a)) - | fo_term_height (Abs(_,_,t)) = fo_term_height t - | fo_term_height _ = 0; - -fun ho_term_height (a $ b) = - 1 + (Int.max (ho_term_height b, ho_term_height a)) - | ho_term_height (Abs(_,_,t)) = ho_term_height t - | ho_term_height _ = 0; - - -(* Higher order matching with exception handled *) -(* returns optional instantiation *) -fun clean_match thy (a as (pat, t)) = - let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty) - in SOME (Vartab.dest tyenv, Vartab.dest tenv) - end handle Pattern.MATCH => NONE; -(* Higher order unification with exception handled, return the instantiations *) -(* given Signature, max var index, pat, tgt *) -(* returns Seq of instantiations *) -fun clean_unify sgn ix (a as (pat, tgt)) = - let - (* type info will be re-derived, maybe this can be cached - for efficiency? *) - val pat_ty = Term.type_of pat; - val tgt_ty = Term.type_of tgt; - (* is it OK to ignore the type instantiation info? - or should I be using it? *) - val typs_unify = - SOME (Sign.typ_unify sgn (pat_ty, tgt_ty) (Term.Vartab.empty, ix)) - handle Type.TUNIFY => NONE; - in - case typs_unify of - SOME (typinsttab, ix2) => - let - (* is it right to throw away the flexes? - or should I be using them somehow? *) - fun mk_insts env = - (Vartab.dest (Envir.type_env env), - Envir.alist_of env); - val initenv = Envir.Envir {asol = Vartab.empty, - iTs = typinsttab, maxidx = ix2}; - val useq = (Unify.smash_unifiers (sgn,initenv,[a])) - handle UnequalLengths => Seq.empty - | Term.TERM _ => Seq.empty; - fun clean_unify' useq () = - (case (Seq.pull useq) of - NONE => NONE - | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t))) - handle UnequalLengths => NONE - | Term.TERM _ => NONE; - in - (Seq.make (clean_unify' useq)) - end - | NONE => Seq.empty - end; - -fun asm_mk t = assume (cterm_of (the_context()) t); -fun asm_read s = (Thm.assume (read_cterm (the_context()) (s,propT))); - - -(* more pretty printing code for Isabelle terms etc *) - - -(* pretty_print_typelist l f = print a typelist. - l = list of types to print : typ list - f = function used to print a single type : typ -> string -*) -fun pretty_print_typelist [] f = "" - | pretty_print_typelist [(h: typ)] (f : typ -> string) = (f h) - | pretty_print_typelist ((h: typ) :: t) (f : typ -> string) = - (f h) ^ ", " ^ (pretty_print_typelist t f); - - - -(* pretty_print_sort s = print a sort - s = sort to print : string list -*) -fun pretty_print_sort [] = "" - | pretty_print_sort ([h]) = "\"" ^ h ^ "\"" - | pretty_print_sort (h :: t) = "\"" ^ h ^ "\"," ^ (pretty_print_sort t); - - -(* pretty_print_type t = print a type - t = type to print : type -*) -fun pretty_print_type (Type (n, l)) = - "Type(\"" ^ n ^ "\", [" ^ (pretty_print_typelist l pretty_print_type) ^ "])" - | pretty_print_type (TFree (n, s)) = - "TFree(\"" ^ n ^ "\", [" ^ (pretty_print_sort s) ^ "])" - | pretty_print_type (TVar ((n, i), s)) = - "TVar( (\"" ^ n ^ "\", " ^ (string_of_int i) ^ "), [" ^ (pretty_print_sort s) ^ "])"; - - -(* pretty_print_term t = print a term prints types and sorts too. - t = term to print : term -*) -fun pretty_print_term (Const (s, t)) = - "Const(\"" ^ s ^ "\", " ^ (pretty_print_type t) ^ ")" - | pretty_print_term (Free (s, t)) = - "Free(\"" ^ s ^ "\", " ^ (pretty_print_type t) ^ ")" - | pretty_print_term (Var ((n, i), t)) = - "Var( (\"" ^ n ^ "\"," ^ (string_of_int i) ^ "), " ^ (pretty_print_type t) ^ ")" - | pretty_print_term (Bound i) = - "Bound(" ^ (string_of_int i) ^ ")" - | pretty_print_term (Abs (s, t, r)) = - "Abs(\"" ^ s ^ "\"," ^ (pretty_print_type t) ^ ", \n " ^ (pretty_print_term r) ^ ")" - | pretty_print_term (op $ (t1, t2)) = - "(" ^ (pretty_print_term t1) ^ ") $\n (" ^ (pretty_print_term t2) ^ ")"; - -(* Write the term out nicly instead of just creating a string for it *) -fun writeterm t = writeln (pretty_print_term t); -fun writetype t = writeln (pretty_print_type t); -fun writesort s = writeln (pretty_print_sort s); - -fun cterm_of_term (t : term) = Thm.cterm_of (the_context()) t; -fun term_of_thm t = (Thm.prop_of t); - -fun string_of_term t = Sign.string_of_term (the_context()) t; -fun print_term t = writeln (string_of_term t); - -(* create a trivial thm from anything... *) -fun triv_thm_from_string s = - let val thy = the_context() - in Thm.trivial (cterm_of thy (Sign.read_prop thy s)) end; - - (* Checks if vars could be the same - alpha convertable - w.r.t. previous vars, a and b are assumed to be vars, - free vars, but not bound vars, - Note frees and vars must all have unique names. *) - fun same_var_check a b L = - let - fun bterm_from t [] = NONE - | bterm_from t ((a,b)::m) = - if t = a then SOME b else bterm_from t m - - val bl_opt = bterm_from a L - in - case bterm_from a L of - NONE => SOME ((a,b)::L) - | SOME b2 => if b2 = b then SOME L else NONE - end; - - (* FIXME: make more efficient, only require a single new var! *) - (* check if the new term has any meta variables not in the old term *) - fun has_new_vars (old, new) = - (case IsaPLib.lrem (op =) (Term.term_vars old) (Term.term_vars new) of - [] => false - | (_::_) => true); - (* check if the new term has any meta variables not in the old term *) - fun has_new_typ_vars (old, new) = - (case IsaPLib.lrem (op =) (Term.term_tvars old) (Term.term_tvars new) of - [] => false - | (_::_) => true); - -(* This version avoids name conflicts that might be introduced by -unskolemisation, and returns a list of (string * Term.typ) * string, -where the outer string is the original name, and the inner string is -the new name, and the type is the type of the free variable that was -renamed. *) -local - fun myadd (n,ty) (L as (renames, names)) = - let val n' = Syntax.dest_skolem n in - case (Library.find_first (fn (_,n2) => (n2 = n)) renames) of - NONE => - let val renamedn = Term.variant names n' in - (renamedn, (((renamedn, ty), n) :: renames, - renamedn :: names)) end - | (SOME ((renamedn, _), _)) => (renamedn, L) - end - handle Fail _ => (n, L); - - fun unsk (L,f) (t1 $ t2) = - let val (L', t1') = unsk (L, I) t1 - in unsk (L', (fn x => f (t1' $ x))) t2 end - | unsk (L,f) (Abs(n,ty,t)) = - unsk (L, (fn x => Abs(n,ty,x))) t - | unsk (L, f) (Free (n,ty)) = - let val (renamed_n, L') = myadd (n ,ty) L - in (L', f (Free (renamed_n, ty))) end - | unsk (L, f) l = (L, f l); -in -fun unskolemise_all_term t = - let - val names = Term.add_term_names (t,[]) - val ((renames,names'),t') = unsk (([], names),I) t - in (renames,t') end; -end - -(* true if the type t is a function *) -fun is_fun_typ (Type(s, l)) = - if s = "fun" then true else false - | is_fun_typ _ = false; - -val is_atomic_typ = not o is_fun_typ; - -(* get the frees in a term that are of atomic type, ie non-functions *) -val atomic_frees_of_term = - List.filter (is_atomic_typ o snd) - o map Term.dest_Free - o Term.term_frees; - -fun usednames_of_term t = Term.add_term_names (t,[]); -fun usednames_of_thm th = - let val rep = Thm.rep_thm th - val hyps = #hyps rep - val (tpairl,tpairr) = Library.split_list (#tpairs rep) - val prop = #prop rep - in - List.foldr Term.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps))) - end; - -(* read in a string and a top-level type and this will give back a term *) -fun readwty tstr tystr = - let val thy = the_context() - in Sign.simple_read_term thy (Sign.read_typ (thy, K NONE) tystr) tstr end; - - (* first term is equal to the second in some name convertable - way... Note: This differs from the aeconv in the Term.ML file of - Isabelle in that it allows a var to be alpha-equiv to a free var. - - Also, the isabelle term.ML version of aeconv uses a - function that it claims doesn't work! *) - fun term_name_eq (Abs(_,ty1,t1)) (Abs(_,ty2,t2)) l = - if ty1 = ty2 then term_name_eq t1 t2 l - else NONE - | term_name_eq (ah $ at) (bh $ bt) l = - (case term_name_eq ah bh l of - NONE => NONE - | SOME l' => term_name_eq at bt l') - | term_name_eq (Const(a,T)) (Const(b,U)) l = - if a=b andalso T=U then SOME l - else NONE - | term_name_eq (a as Free(s1,ty1)) (b as Free(s2,ty2)) l = - same_var_check a b l - | term_name_eq (a as Free(s1,ty1)) (b as Var(n2,ty2)) l = - same_var_check a b l - | term_name_eq (a as Var(n1,ty1)) (b as Free(s2,ty2)) l = - same_var_check a b l - | term_name_eq (a as Var(n1,ty1)) (b as Var(n2,ty2)) l = - same_var_check a b l - | term_name_eq (Bound i) (Bound j) l = - if i = j then SOME l else NONE - | term_name_eq a b l = ((*writeln ("unchecked case:\n" ^ "a:\n" ^ (pretty_print_term a) ^ "\nb:\n" ^ (pretty_print_term b));*) NONE); - - (* checks to see if the term in a name-equivalent member of the list of terms. *) - fun get_name_eq_member a [] = NONE - | get_name_eq_member a (h :: t) = - if is_some (term_name_eq a h []) then SOME h - else get_name_eq_member a t; - - fun name_eq_member a [] = false - | name_eq_member a (h :: t) = - if is_some (term_name_eq a h []) then true - else name_eq_member a t; - - (* true if term is a variable *) - fun is_some_kind_of_var (Free(s, ty)) = true - | is_some_kind_of_var (Var(i, ty)) = true - | is_some_kind_of_var (Bound(i)) = true - | is_some_kind_of_var _ = false; - - (* checks to see if the lhs -> rhs is a invalid rewrite rule *) -(* FIXME: we should really check that there is a subterm on the lhs -which embeds into the rhs, this would be much closer to the normal -notion of valid wave rule - ie there exists at least one case where it -is a valid wave rule... *) - fun is_not_valid_rwrule thy (lhs, rhs) = - Term.is_Var (Term.head_of lhs) (* if lhs is essentially just a var *) - orelse has_new_vars (lhs,rhs) - orelse has_new_typ_vars (lhs,rhs) - orelse Pattern.matches_subterm thy (lhs, rhs); - - - (* first term contains the second in some name convertable way... *) - (* note: this is equivalent to an alpha-convertable emedding *) - (* takes as args: term containing a, term contained b, - (bound vars of a, bound vars of b), - current alpha-conversion-pairs, - returns: bool:can convert, new alpha-conversion table *) - (* in bellow: we *don't* use: a loose notion that only requires - variables to match variables, and doesn't worry about the actual - pattern in the variables. *) - fun term_contains1 (Bs, FVs) (Abs(s,ty,t)) (Abs(s2,ty2,t2)) = - if ty = ty2 then - term_contains1 ((SOME(s,s2,ty)::Bs), FVs) t t2 - else [] - - | term_contains1 T t1 (Abs(s2,ty2,t2)) = [] - - | term_contains1 (Bs, FVs) (Abs(s,ty,t)) t2 = - term_contains1 (NONE::Bs, FVs) t t2 - - | term_contains1 T (ah $ at) (bh $ bt) = - (term_contains1 T ah (bh $ bt)) @ - (term_contains1 T at (bh $ bt)) @ - (maps (fn inT => (term_contains1 inT at bt)) (term_contains1 T ah bh)) - - | term_contains1 T a (bh $ bt) = [] - - | term_contains1 T (ah $ at) b = - (term_contains1 T ah b) @ (term_contains1 T at b) - - | term_contains1 T a b = - (* simple list table lookup to check if a named variable has been - mapped to a variable, if not adds the mapping and return some new - list mapping, if it is then it checks that the pair are mapped to - each other, if so returns the current mapping list, else none. *) - let - fun bterm_from t [] = NONE - | bterm_from t ((a,b)::m) = - if t = a then SOME b else bterm_from t m - - (* check to see if, w.r.t. the variable mapping, two terms are leaf - terms and are mapped to each other. Note constants are only mapped - to the same constant. *) - fun same_leaf_check (T as (Bs,FVs)) (Bound i) (Bound j) = - let - fun aux_chk (i1,i2) [] = false - | aux_chk (0,0) ((SOME _) :: bnds) = true - | aux_chk (i1,0) (NONE :: bnds) = false - | aux_chk (i1,i2) ((SOME _) :: bnds) = - aux_chk (i1 - 1,i2 - 1) bnds - | aux_chk (i1,i2) (NONE :: bnds) = - aux_chk (i1,i2 - 1) bnds - in - if (aux_chk (i,j) Bs) then [T] - else [] - end - | same_leaf_check (T as (Bs,(Fs,Vs))) - (a as (Free (an,aty))) - (b as (Free (bn,bty))) = - (case bterm_from an Fs of - SOME b2n => if bn = b2n then [T] - else [] (* conflict of var name *) - | NONE => [(Bs,((an,bn)::Fs,Vs))]) - | same_leaf_check (T as (Bs,(Fs,Vs))) - (a as (Var (an,aty))) - (b as (Var (bn,bty))) = - (case bterm_from an Vs of - SOME b2n => if bn = b2n then [T] - else [] (* conflict of var name *) - | NONE => [(Bs,(Fs,(an,bn)::Vs))]) - | same_leaf_check T (a as (Const _)) (b as (Const _)) = - if a = b then [T] else [] - | same_leaf_check T _ _ = [] - - in - same_leaf_check T a b - end; - - (* wrapper for term_contains1: checks if the term "a" contains in - some embedded way, (w.r.t. name -convertable) the term "b" *) - fun term_contains a b = - case term_contains1 ([],([],[])) a b of - (_ :: _) => true - | [] => false; - - (* change all bound variables to see ones with appropriate name and - type *) - (* naming convention is OK as we use 'variant' from term.ML *) - (* Note "bounds_to_frees" defined below, its better and quicker, but - keeps the quantifiers handing about, and changes all bounds, not - just universally quantified ones. *) - fun change_bounds_to_frees t = - let - val vars = strip_all_vars t - val frees_names = map (fn Free(s,n) => s | _ => "") (term_frees t) - val body = strip_all_body t - - fun bnds_to_frees [] _ acc = acc - | bnds_to_frees ((name,ty)::more) names acc = - let - val new_name = variant names name - in - bnds_to_frees more (new_name::names) (Free(new_name,ty)::acc) - end - in - (subst_bounds ((bnds_to_frees vars frees_names []), body)) - end; - -(* a runtime-quick function which makes sure that every variable has a -unique name *) -fun unique_namify_aux (ntab,(Abs(s,ty,t))) = - (case Symtab.lookup ntab s of - NONE => - let - val (ntab2,t2) = unique_namify_aux (Symtab.update (s, s) ntab, t) - in - (ntab2,Abs(s,ty,t2)) - end - | SOME s2 => - let - val s_new = (Term.variant (Symtab.keys ntab) s) - val (ntab2,t2) = - unique_namify_aux (Symtab.update (s_new, s_new) ntab, t) - in - (ntab2,Abs(s_new,ty,t2)) - end) - | unique_namify_aux (ntab,(a $ b)) = - let - val (ntab1,t1) = unique_namify_aux (ntab,a) - val (ntab2,t2) = unique_namify_aux (ntab1,b) - in - (ntab2, t1$t2) - end - | unique_namify_aux (nt as (ntab,Const x)) = nt - | unique_namify_aux (nt as (ntab,f as Free (s,ty))) = - (case Symtab.lookup ntab s of - NONE => (Symtab.update (s, s) ntab, f) - | SOME _ => nt) - | unique_namify_aux (nt as (ntab,v as Var ((s,i),ty))) = - (case Symtab.lookup ntab s of - NONE => (Symtab.update (s, s) ntab, v) - | SOME _ => nt) - | unique_namify_aux (nt as (ntab, Bound i)) = nt; - -fun unique_namify t = - #2 (unique_namify_aux (Symtab.empty, t)); - -(* a runtime-quick function which makes sure that every variable has a -unique name and also changes bound variables to free variables, used -for embedding checks, Note that this is a pretty naughty term -manipulation, which doesn't have necessary relation to the original -sematics of the term. This is really a trick for our embedding code. *) - -fun bounds_to_frees_aux T (ntab,(Abs(s,ty,t))) = - (case Symtab.lookup ntab s of - NONE => - let - val (ntab2,t2) = - bounds_to_frees_aux ((s,ty)::T) (Symtab.update (s, s) ntab, t) - in - (ntab2,Abs(s,ty,t2)) - end - | SOME s2 => - let - val s_new = (Term.variant (Symtab.keys ntab) s) - val (ntab2,t2) = - bounds_to_frees_aux ((s_new,ty)::T) - (Symtab.update (s_new, s_new) ntab, t) - in - (ntab2,Abs(s_new,ty,t2)) - end) - | bounds_to_frees_aux T (ntab,(a $ b)) = - let - val (ntab1,t1) = bounds_to_frees_aux T (ntab,a) - val (ntab2,t2) = bounds_to_frees_aux T (ntab1,b) - in - (ntab2, t1$t2) - end - | bounds_to_frees_aux T (nt as (ntab,Const x)) = nt - | bounds_to_frees_aux T (nt as (ntab,f as Free (s,ty))) = - (case Symtab.lookup ntab s of - NONE => (Symtab.update (s, s) ntab, f) - | SOME _ => nt) - | bounds_to_frees_aux T (nt as (ntab,v as Var ((s,i),ty))) = - (case Symtab.lookup ntab s of - NONE => (Symtab.update (s, s) ntab, v) - | SOME _ => nt) - | bounds_to_frees_aux T (nt as (ntab, Bound i)) = - let - val (s,ty) = List.nth (T,i) - in - (ntab, Free (s,ty)) - end; - - -fun bounds_to_frees t = - #2 (bounds_to_frees_aux [] (Symtab.empty,t)); - -fun bounds_to_frees_with_vars vars t = - #2 (bounds_to_frees_aux vars (Symtab.empty,t)); - - - -(* loose bounds to frees *) -fun loose_bnds_to_frees_aux (bnds,vars) (Abs(s,ty,t)) = - Abs(s,ty,loose_bnds_to_frees_aux (bnds + 1,vars) t) - | loose_bnds_to_frees_aux (bnds,vars) (a $ b) = - (loose_bnds_to_frees_aux (bnds,vars) a) - $ (loose_bnds_to_frees_aux (bnds,vars) b) - | loose_bnds_to_frees_aux (bnds,vars) (t as (Bound i)) = - if (bnds <= i) then Free (List.nth (vars,i - bnds)) - else t - | loose_bnds_to_frees_aux (bnds,vars) t = t; - - -fun loose_bnds_to_frees vars t = - loose_bnds_to_frees_aux (0,vars) t; - - - (* FIXME ObjectLogic.drop_judgment *) - fun try_dest_Trueprop (Const("Trueprop", _) $ T) = T - | try_dest_Trueprop T = T; - - fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l - | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t - | bot_left_leaf_of x = x; - - fun bot_left_leaf_noabs_of (l $ r) = bot_left_leaf_noabs_of l - | bot_left_leaf_noabs_of x = x; - -(* cleaned up normal form version of the subgoal terms conclusion *) -fun cleaned_term_conc t = - let - val concl = Logic.strip_imp_concl (change_bounds_to_frees t) - in - (try_dest_Trueprop (Logic.unprotect concl handle TERM _ => concl)) - end; - -(* fun get_prems_of_sg_term t = - map opt_dest_Trueprop (Logic.strip_imp_prems t); *) - -fun get_prems_of_sg_term t = - map try_dest_Trueprop (Logic.strip_assums_hyp t); - - -(* drop premises, clean bound var stuff, and make a trueprop... *) - fun cleaned_term_parts t = - let - val t2 = (change_bounds_to_frees t) - val concl = Logic.strip_imp_concl t2 - val prems = map try_dest_Trueprop (Logic.strip_imp_prems t2) - in - (prems, (try_dest_Trueprop ((Logic.unprotect concl handle TERM _ => concl)))) - end; - - (* change free variables to vars and visa versa *) - (* *** check naming is OK, can we just use the vasr old name? *) - (* *** Check: Logic.varify and Logic.unvarify *) - fun change_vars_to_frees (a$b) = - (change_vars_to_frees a) $ (change_vars_to_frees b) - | change_vars_to_frees (Abs(s,ty,t)) = - (Abs(s, Logic.legacy_varifyT ty,change_vars_to_frees t)) - | change_vars_to_frees (Var((s,i),ty)) = (Free(s, Logic.legacy_unvarifyT ty)) - | change_vars_to_frees l = l; - - fun change_frees_to_vars (a$b) = - (change_frees_to_vars a) $ (change_frees_to_vars b) - | change_frees_to_vars (Abs(s,ty,t)) = - (Abs(s, Logic.legacy_varifyT ty,change_frees_to_vars t)) - | change_frees_to_vars (Free(s,ty)) = (Var((s,0), Logic.legacy_varifyT ty)) - | change_frees_to_vars l = l; - - -end; diff -r 81d6dc597559 -r 5181e317e9ff src/Pure/IsaPlanner/upterm_lib.ML --- a/src/Pure/IsaPlanner/upterm_lib.ML Sun Jun 11 00:28:18 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,133 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* Title: Pure/IsaPlanner/upterm_lib.ML - ID: $Id$ - Author: Lucas Dixon, University of Edinburgh - lucas.dixon@ed.ac.uk - Created: 26 Jan 2004 -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* DESCRIPTION: - - generic upterms for lambda calculus - -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) - - -signature UPTERM_LIB = -sig - - - (* type for upterms defined in terms of a 't : a downterm type, and - 'y : types for bound variable in the downterm type *) - datatype ('t,'y) T = - abs of string * 'y * (('t,'y) T) - | appl of 't * (('t,'y) T) - | appr of 't * (('t,'y) T) - | root - - (* analysis *) - val tyenv_of_upterm : ('t,'y) T -> (string * 'y) list - val tyenv_of_upterm' : ('t,'y) T -> 'y list - val addr_of_upterm : ('t,'y) T -> int list - val upsize_of_upterm : ('t,'y) T -> int - - (* editing *) - val map_to_upterm_parts : ('t -> 't2) * ('y -> 'y2) -> - ('t,'y) T -> ('t2,'y2) T - - val expand_map_to_upterm_parts : ('t -> 't2 list) * ('y -> 'y2) -> - ('t,'y) T -> ('t2,'y2) T list - - val fold_upterm : ('a * 't -> 'a) -> (* left *) - ('a * 't -> 'a) -> (* right *) - ('a * (string * 'y) -> 'a) -> (* abs *) - ('a * ('t,'y) T) -> 'a (* everything *) - - (* apply one term to another *) - val apply : ('t,'y) T -> ('t,'y) T -> ('t,'y) T - -end; - - - -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -structure UpTermLib : UPTERM_LIB = -struct - - (* type for upterms defined in terms of a 't : a downterm type, and - 'y : types for bound variable in the downterm type *) - datatype ('t,'y) T = - abs of string * 'y * ('t,'y) T - | appl of 't * ('t,'y) T - | appr of 't * ('t,'y) T - | root; - - (* get the bound variable names and types for the current foucs *) - fun tyenv_of_upterm (appl(l,m)) = tyenv_of_upterm m - | tyenv_of_upterm (appr(r,m)) = tyenv_of_upterm m - | tyenv_of_upterm (abs(s,ty,m)) = (s, ty) :: (tyenv_of_upterm m) - | tyenv_of_upterm root = []; - - (* get the bound variable types for the current foucs *) - fun tyenv_of_upterm' (appl(l,m)) = tyenv_of_upterm' m - | tyenv_of_upterm' (appr(r,m)) = tyenv_of_upterm' m - | tyenv_of_upterm' (abs(s,ty,m)) = ty :: (tyenv_of_upterm' m) - | tyenv_of_upterm' root = []; - - (* an address construction for the upterm, ie if we were at the - root, address describes how to get to this point. *) - fun addr_of_upterm1 A root = A - | addr_of_upterm1 A (appl (l,m)) = addr_of_upterm1 (1::A) m - | addr_of_upterm1 A (appr (r,m)) = addr_of_upterm1 (2::A) m - | addr_of_upterm1 A (abs (s,ty,m)) = addr_of_upterm1 (0::A) m; - - fun addr_of_upterm m = addr_of_upterm1 [] m; - - (* the size of the upterm, ie how far to get to root *) - fun upsize_of_upterm root = 0 - | upsize_of_upterm (appl (l,m)) = (upsize_of_upterm m) + 1 - | upsize_of_upterm (appr (r,m)) = (upsize_of_upterm m) + 1 - | upsize_of_upterm (abs (s,ty,m)) = (upsize_of_upterm m) + 1; - - (* apply an upterm to to another upterm *) - fun apply x root = x - | apply x (appl (l,m)) = appl(l, apply x m) - | apply x (appr (r,m)) = appr(r, apply x m) - | apply x (abs (s,ty,m)) = abs(s, ty, apply x m); - - (* applies the term function to each term in each part of the upterm *) - fun map_to_upterm_parts (tf,yf) root = root - - | map_to_upterm_parts (tf,yf) (abs(s,ty,m)) = - abs(s,yf ty,map_to_upterm_parts (tf,yf) m) - - | map_to_upterm_parts (tf,yf) (appr(t,m)) = - appr (tf t, map_to_upterm_parts (tf,yf) m) - - | map_to_upterm_parts (tf,yf) (appl(t,m)) = - appl (tf t, map_to_upterm_parts (tf,yf) m); - - - (* applies the term function to each term in each part of the upterm *) - fun expand_map_to_upterm_parts (tf,yf) root = [root] - | expand_map_to_upterm_parts (tf,yf) (abs(s,ty,m)) = - map (fn x => abs(s,yf ty, x)) - (expand_map_to_upterm_parts (tf,yf) m) - | expand_map_to_upterm_parts (tf,yf) (appr(t,m)) = - map appr (IsaPLib.all_pairs - (tf t) (expand_map_to_upterm_parts (tf,yf) m)) - | expand_map_to_upterm_parts (tf,yf) (appl(t,m)) = - map appl (IsaPLib.all_pairs - (tf t) (expand_map_to_upterm_parts (tf,yf) m)); - - (* fold along each 't (down term) in the upterm *) - fun fold_upterm fl fr fa (d, u) = - let - fun fold_upterm' (d, root) = d - | fold_upterm' (d, abs(s,ty,m)) = fold_upterm' (fa(d,(s,ty)), m) - | fold_upterm' (d, appr(t,m)) = fold_upterm' (fr(d,t), m) - | fold_upterm' (d, appl(t,m)) = fold_upterm' (fl(d,t), m) - in fold_upterm' (d,u) end; - -end;