src/Pure/IsaPlanner/focus_term_lib.ML
author gagern
Sat Mar 26 16:14:17 2005 +0100 (2005-03-26 ago)
changeset 15632 bb178a7a69c1
parent 15531 08c8dad8e399
child 15814 d65f461c8672
permissions -rw-r--r--
op vor infix-Konstruktoren im datatype binding zum besseren Parsen
     1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     2 (*  Title:      libs/focus_term_lib.ML
     3     Author:     Lucas Dixon, University of Edinburgh
     4                 lucasd@dai.ed.ac.uk
     5     Date:       16 April 2003
     6 *)
     7 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     8 (*  DESCRIPTION:
     9 
    10     Generic Foucs terms (like Zippers), which allows modification and
    11     manipulation of term keeping track of how we got to the position
    12     in the term. We provide a signature for terms, ie any kind of
    13     lamda calculus with abs and application, and some notion of types
    14     and naming of abstracted vars. 
    15 
    16     FIXME: at some point in the future make a library to work simply
    17     with polymorphic upterms - that way if I want to use them without
    18     the focus part, then I don't need to include all the focus stuff.
    19 
    20 *)   
    21 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    22 
    23 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    24 
    25 (*  to endoce and decode general terms into the type needed by focus
    26 term, this is an easy thing to write, but needs to be done for each
    27 type that is going to be used with focus terms. *)
    28 
    29 signature F_ENCODE_TERM_SIG = 
    30 sig
    31 
    32   type term (* type of term to be encoded into TermT for focus term manip *)
    33   type TypeT (* type annotation for abstractions *)
    34   type LeafT (* type for other leaf types in term sturcture *)
    35 
    36   (* the type to be encoded into *)
    37   datatype TermT = op $ of TermT * TermT
    38     | Abs of string * TypeT * TermT
    39     | lf of LeafT
    40 
    41   (* the encode and decode functions *)
    42   val fakebounds : string * TypeT -> term -> term
    43   val encode : term -> TermT
    44   val decode : TermT -> term
    45 
    46 end;
    47 
    48 
    49 
    50 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    51 signature FOCUS_TERM_SIG = 
    52 sig
    53      structure MinTermS : F_ENCODE_TERM_SIG
    54 
    55      exception focus_term_exp of string;
    56      exception out_of_term_exception of string;
    57 
    58      type Term = MinTermS.TermT;
    59      type Type = MinTermS.TypeT;
    60 
    61      type UpTerm = (Term,Type) UpTermLib.T;
    62 
    63 (*   datatype
    64        UpTerm =
    65            abs of string * Type * UpTerm
    66          | appl of Term * UpTerm
    67          | appr of Term * UpTerm
    68          | root *)
    69 
    70      datatype FcTerm = focus of Term * UpTerm
    71 
    72      (* translating *)
    73      val fcterm_of_term : MinTermS.term -> FcTerm
    74      val term_of_fcterm : FcTerm -> MinTermS.term
    75 
    76      (* editing/constrution *)
    77      val enc_appl : (MinTermS.term * UpTerm) -> UpTerm
    78      val enc_appr : (MinTermS.term * UpTerm) -> UpTerm
    79 
    80      (* upterm creatioin *)
    81      val upterm_of : FcTerm -> UpTerm
    82      val add_upterm : UpTerm -> FcTerm -> FcTerm
    83      val mk_term_of_upterm : (MinTermS.term * UpTerm) -> MinTermS.term
    84      val mk_termf_of_upterm : UpTerm -> 
    85             (((string * Type) list) * 
    86              (MinTermS.term -> MinTermS.term))
    87      val pure_mk_termf_of_upterm : (MinTermS.term, Type) UpTermLib.T -> 
    88                                    (((string * Type) list) * 
    89                                     (MinTermS.term -> MinTermS.term))
    90 
    91      (* focusing, throws exceptions *)
    92      val focus_bot_left_leaf : FcTerm -> FcTerm
    93      val focus_left : FcTerm -> FcTerm
    94      val focus_right : FcTerm -> FcTerm
    95      val focus_abs : FcTerm -> FcTerm
    96      val focus_fake_abs : FcTerm -> FcTerm
    97      val focus_to_top : FcTerm -> FcTerm
    98      val focus_up : FcTerm -> FcTerm
    99      val focus_up_right : FcTerm -> FcTerm
   100      val focus_up_right1 : FcTerm -> FcTerm
   101 
   102      (* optional focus changes *)
   103      val focus_up_abs : FcTerm -> FcTerm option
   104      val focus_up_appr : FcTerm -> FcTerm option
   105      val focus_up_appl : FcTerm -> FcTerm option
   106      val focus_up_abs_or_appr : FcTerm -> FcTerm option
   107 
   108      val tyenv_of_focus : FcTerm -> (string * Type) list
   109      val tyenv_of_focus' : FcTerm -> Type list
   110 
   111      (* set/get the focus term *)
   112      val set_focus_of_fcterm : FcTerm -> MinTermS.term -> FcTerm
   113      val focus_of_fcterm : FcTerm -> MinTermS.term
   114 
   115      (* leaf navigation *) 
   116      val leaf_seq_of_fcterm : FcTerm -> FcTerm Seq.seq
   117      val next_leaf_fcterm : FcTerm -> FcTerm
   118      val next_leaf_of_fcterm_seq : FcTerm -> FcTerm Seq.seq
   119 
   120      (* analysis *)
   121      val upsize_of_fcterm : FcTerm -> int
   122      val pretty_fcterm : FcTerm -> Pretty.T
   123 end;
   124 
   125 
   126 
   127 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
   128 (* 
   129 
   130    NOTE!!! I think this can be done in a purely functional way with a
   131    pair of a term (the focus) and a function, that when applied
   132    unfocuses one level... maybe think about this as it would be a very
   133    nice generic consrtuction, without the need for encoding/decoding
   134    strutcures.
   135 
   136 *)
   137 functor FocusTermFUN(structure EncodeTerm : F_ENCODE_TERM_SIG)
   138   : FOCUS_TERM_SIG = 
   139 struct
   140 
   141 structure MinTermS = EncodeTerm;
   142 
   143 local open MinTermS open UpTermLib in
   144 
   145   type Term = MinTermS.TermT;
   146   type Type = MinTermS.TypeT;
   147 
   148   exception focus_term_exp of string;
   149   exception out_of_term_exception of string;
   150 
   151   infix 9 $
   152 
   153   (* datatype to hold a term tree and the path to where you are in the term *)
   154 (*   datatype UpTerm = root
   155                   | appl of (Term * UpTerm)
   156                   | appr of (Term * UpTerm)
   157                   | abs of (string * Type * UpTerm); *)
   158 
   159   type UpTerm = (Term,Type) UpTermLib.T;
   160 
   161   fun enc_appl (t,u) = appl((MinTermS.encode t),u);
   162   fun enc_appr (t,u) = appr((MinTermS.encode t),u);
   163 
   164   datatype FcTerm = focus of (Term * UpTerm);
   165 
   166   (* the the term of the upterm *)
   167   fun mk_term_of_upt_aux (t, root) = MinTermS.decode t
   168     | mk_term_of_upt_aux (t, appl (l,m)) =  mk_term_of_upt_aux(l$t, m)
   169     | mk_term_of_upt_aux (t, appr (r,m)) =  mk_term_of_upt_aux(t$r, m)
   170     | mk_term_of_upt_aux (t, abs (s,ty,m)) = mk_term_of_upt_aux(Abs(s,ty,t),m);
   171 
   172   fun mk_term_of_upterm (t, ut) = mk_term_of_upt_aux (MinTermS.encode t, ut);
   173 
   174   (* a function version of the above, given an upterm it returns:
   175      a function on that given a term puts it in the context of the upterm,
   176      and a list of bound variables that are in the upterm, added as 
   177      we go up - so in reverse order from that typiclaly used by top-down
   178      parsing of terms. *)
   179   fun mk_termf_of_upt_aux (f, bs, root) = 
   180       (bs, fn t => MinTermS.decode (f t))
   181     | mk_termf_of_upt_aux (f, bs, appl (l,m)) =  
   182       mk_termf_of_upt_aux (fn t => l $ (f t), bs, m)
   183     | mk_termf_of_upt_aux (f, bs, appr (r,m)) =  
   184       mk_termf_of_upt_aux (fn t => (f t) $ r, bs, m)
   185     | mk_termf_of_upt_aux (f, bs, abs (s,ty,m)) = 
   186       mk_termf_of_upt_aux (fn t => Abs(s,ty,(f t)), (s,ty)::bs, m);
   187 
   188   fun mk_termf_of_upterm ut = mk_termf_of_upt_aux (MinTermS.encode, [], ut);
   189 
   190  
   191   fun upterm_of (focus(t, u)) = u;
   192 
   193   (* put a new upterm at the start of our current term *)
   194   fun add_upterm u2 (focus(t, u)) = focus(t, UpTermLib.apply u2 u);
   195 
   196 
   197   (* As above but work on the pure originial upterm type *)
   198   fun pure_mk_termf_of_upterm ut = 
   199       mk_termf_of_upt_aux 
   200         (encode, [], (map_to_upterm_parts (encode, I) ut));
   201 
   202   fun fcterm_of_term t = focus(encode t, root);
   203 
   204   fun term_of_fcterm (focus (t, m)) = mk_term_of_upt_aux (t, m);
   205 
   206 (*  fun term_of_fcterm (focus (t, root)) = mk_term_of_upt_aux (t, root)
   207     | term_of_fcterm _ = raise focus_term_exp "term_of_fcterm: something bad has happened here."; *)
   208 
   209   fun focus_of_fcterm (focus(t, _)) = MinTermS.decode t;
   210 
   211   (* replace the focus term with a new term... *)
   212   fun set_focus_of_fcterm (focus(_, m)) nt = focus(MinTermS.encode nt, m);
   213 
   214   fun focus_left (focus(a $ b, m)) = focus(a, appr(b, m))
   215     | focus_left (focus(Abs(s,ty,t), m)) = focus_left (focus(t, abs(s,ty,m)))
   216     | focus_left (focus(l, m)) = raise out_of_term_exception "focus_left";
   217 
   218 (* Note: ":" is standard for faked bound vars... see: EQStepTacTermTools *)
   219   fun focus_fake_abs (focus(Abs(s,ty,t), m)) = 
   220       let val t' = MinTermS.encode (fakebounds (s,ty) (MinTermS.decode t))
   221       in focus(t', abs(s,ty,m)) end
   222     | focus_fake_abs (focus(l, m)) = raise out_of_term_exception "focus_fake_abs";
   223 
   224   fun focus_abs (focus(Abs(s,ty,t), m)) = focus(t, abs(s,ty,m))
   225     | focus_abs (focus(l, m)) = raise out_of_term_exception "focus_abs";
   226 
   227 
   228   fun focus_right (focus(a $ b, m)) = focus(b, appl(a, m))
   229     | focus_right (focus(Abs(s,ty,t), m)) = focus_right (focus(t, abs(s,ty,m)))
   230     | focus_right (focus(l, m)) = raise out_of_term_exception "focus_right";
   231 
   232   fun focus_up (focus(t, appl(l,m))) = focus(l$t, m)
   233     | focus_up (focus(t, appr(r,m))) = focus(t$r, m)
   234     | focus_up (focus(t, abs(s,ty,m))) = focus_up (focus(Abs(s,ty,t), m))
   235     | focus_up (focus(t, root)) = raise out_of_term_exception "focus_up";
   236 
   237   fun focus_to_top t = 
   238     focus_to_top (focus_up t) handle out_of_term_exception _ => t;
   239 
   240   (* focus up until you can move right, and then do so *)
   241   fun focus_up_right (focus(t, appl(l,m))) = 
   242       focus_up_right (focus(l$t, m))
   243     | focus_up_right (focus(t, appr(r,m))) = 
   244       focus(r, appl(t,m))
   245     | focus_up_right (focus(t, abs(s,ty,m))) = 
   246       focus_up_right (focus(Abs(s,ty,t), m))
   247     | focus_up_right (focus(t, root)) = 
   248       raise out_of_term_exception "focus_up_right";
   249 
   250   (* as above, but do not move up over a left application *)
   251   fun focus_up_right1 (focus(t, appl(l,m))) = 
   252       raise out_of_term_exception "focus_up_right1"
   253     | focus_up_right1 (focus(t, appr(r,m))) = 
   254       focus(r, appl(t,m))
   255     | focus_up_right1 (focus(t, abs(s,ty,m))) = 
   256       focus_up_right (focus(Abs(s,ty,t), m))
   257     | focus_up_right1 (focus(t, root)) = 
   258       raise out_of_term_exception "focus_up_right1";
   259 
   260   (* move focus to the bottom left *)
   261   fun focus_bot_left_leaf (ft as focus(t, _)) = 
   262         focus_bot_left_leaf (focus_left ft) 
   263         handle out_of_term_exception  _=> ft;
   264 
   265   (* focus tools for working directly with the focus representation *)
   266   fun focus_up_appr (focus(t, appl(l,m))) = NONE
   267     | focus_up_appr (focus(t, appr(r,m))) = SOME (focus(t$r, m))
   268     | focus_up_appr (focus(t, abs(s,ty,m))) = NONE
   269     | focus_up_appr (focus(t, root)) = NONE;
   270 
   271   fun focus_up_appl (focus(t, appl(l,m))) = SOME (focus(l$t, m))
   272     | focus_up_appl (focus(t, appr(r,m))) = NONE
   273     | focus_up_appl (focus(t, abs(s,ty,m))) = NONE
   274     | focus_up_appl (focus(t, root)) = NONE;
   275 
   276   fun focus_up_abs (focus(t, appl(l,m))) = NONE
   277     | focus_up_abs (focus(t, appr(r,m))) = NONE
   278     | focus_up_abs (focus(t, abs(s,ty,m))) = 
   279       SOME (focus_up (focus(Abs(s,ty,t), m)))
   280     | focus_up_abs (focus(t, root)) = NONE;
   281 
   282   fun focus_up_abs_or_appr (focus(t, appl(l,m))) = NONE
   283     | focus_up_abs_or_appr (focus(t, appr(r,m))) = SOME (focus(t$r, m))
   284     | focus_up_abs_or_appr (focus(t, abs(s,ty,m))) = 
   285       SOME (focus_up (focus(Abs(s,ty,t), m)))
   286     | focus_up_abs_or_appr (focus(t, root)) = NONE;
   287 
   288 
   289   fun tyenv_of_focus (focus(t, u)) = tyenv_of_upterm u;
   290   fun tyenv_of_focus' (focus(t, u)) = tyenv_of_upterm' u;
   291 
   292   (* return the Term.type of the focus term, computes bound vars type,
   293      does a quick check only. *)
   294 (*  fun fastype_of_focus (focus(t, m)) = 
   295        let 
   296          fun boundtypes_of_upterm (abs(s,ty,m)) = 
   297          ty::(boundtypes_of_upterm m)
   298            | boundtypes_of_upterm (appl(t,m)) = 
   299          boundtypes_of_upterm m
   300            | boundtypes_of_upterm (appr(t,m)) = 
   301          boundtypes_of_upterm m
   302            | boundtypes_of_upterm (root) = []
   303        in
   304          fastype_of1 ((boundtypes_of_upterm m), t)
   305        end; *)
   306 
   307   (* gets the next left hand side term, or throws an exception *)
   308   fun next_leaf_fcterm ft = focus_bot_left_leaf (focus_up_right ft);
   309 
   310   fun next_leaf_of_fcterm_seq_aux t () = 
   311     let val nextt = next_leaf_fcterm t
   312     in 
   313         SOME (nextt, Seq.make (next_leaf_of_fcterm_seq_aux nextt))
   314     end handle out_of_term_exception _ => NONE;
   315 
   316   (* sequence of next upterms from start upterm... 
   317      ie a sequence of all leafs after this one*)
   318   fun next_leaf_of_fcterm_seq in_t = 
   319     Seq.make (next_leaf_of_fcterm_seq_aux in_t);
   320 
   321   (* returns a sequence of all leaf up terms from term, ie DFS on 
   322    leafs of term, ie uses time O(n), n = sizeof term. *)
   323   fun leaf_seq_of_fcterm in_t = 
   324     let 
   325       val botleft = (focus_bot_left_leaf in_t)
   326     in
   327       Seq.cons (botleft, (Seq.make (next_leaf_of_fcterm_seq_aux botleft)) )
   328     end;
   329 
   330 
   331   fun upsize_of_fcterm (focus(t, ut)) = upsize_of_upterm ut;
   332 
   333   fun pretty_fcterm ft = Pretty.str "no yet implemented";
   334 
   335 end; (* local *)
   336 
   337 end; (* functor *)
   338 
   339 
   340 
   341 
   342 
   343 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
   344 (* focus term encoding sturcture for isabelle terms *)
   345 structure EncodeIsaFTerm : F_ENCODE_TERM_SIG = 
   346 struct
   347   infix 9 $;
   348 
   349   type term = Term.term;
   350 
   351   type TypeT = Term.typ;
   352 
   353   datatype LeafT = lConst of string * Term.typ
   354      | lVar of ((string * int) * Term.typ)
   355      | lFree of (string * Term.typ)
   356      | lBound of int;
   357 
   358   datatype TermT = op $ of TermT * TermT
   359     | Abs of string * TypeT * TermT
   360     | lf of LeafT;
   361 
   362   fun fakebounds (s, ty) t = subst_bound (Free(":" ^ s, ty), t);
   363 
   364   fun encode (Term.$(a,b)) = (encode a) $ (encode b)
   365     | encode (Term.Abs(s,ty,t)) = Abs(s,ty,(encode t))
   366     | encode (Term.Const(s,ty)) = lf(lConst(s,ty))
   367     | encode (Term.Var((s,i),ty)) = lf(lVar((s,i),ty))
   368     | encode (Term.Free(s,ty)) = lf(lFree(s,ty))
   369     | encode (Term.Bound i) = lf(lBound i);
   370 
   371   fun decode (a $ b) = Term.$(decode a, decode b)
   372     | decode (Abs(s,ty,t)) = (Term.Abs(s,ty,decode t))
   373     | decode (lf(lConst(s,ty))) = Term.Const(s,ty)
   374     | decode (lf(lVar((s,i),ty))) = Term.Var((s,i),ty)
   375     | decode (lf(lFree(s,ty))) = (Term.Free(s,ty))
   376     | decode (lf(lBound i)) = (Term.Bound i);
   377 
   378 end;
   379