src/Pure/IsaPlanner/focus_term_lib.ML

domain package generates compactness lemmas for new constructors

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
(*  Title:      Pure/IsaPlanner/focus_term_lib.ML
    ID:		$Id$
    Author:     Lucas Dixon, University of Edinburgh
                [e-mail]
    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;