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