src/Pure/IsaPlanner/isa_fterm.ML
author wenzelm
Thu Jun 02 09:11:32 2005 +0200 (2005-06-02)
changeset 16179 fa7e70be26b0
parent 15915 b0e8b37642a4
child 17045 e108cd5b6986
permissions -rw-r--r--
header;
paulson@15481
     1
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
wenzelm@16179
     2
(*  Title:      Pure/IsaPlanner/isa_fterm.ML
wenzelm@16179
     3
    ID:		$Id$
paulson@15481
     4
    Author:     Lucas Dixon, University of Edinburgh
paulson@15481
     5
                lucasd@dai.ed.ac.uk
paulson@15481
     6
    Date:       16 April 2003
paulson@15481
     7
*)
paulson@15481
     8
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
paulson@15481
     9
(*  DESCRIPTION:
paulson@15481
    10
paulson@15481
    11
    Generic Foucs terms (like Zippers) instantiation for Isabelle terms. 
paulson@15481
    12
paulson@15481
    13
*)   
paulson@15481
    14
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
paulson@15481
    15
paulson@15481
    16
signature ISA_ENCODE_TERM = 
paulson@15481
    17
  F_ENCODE_TERM_SIG
paulson@15481
    18
    where type term = Term.term type TypeT = Term.typ;
paulson@15481
    19
paulson@15481
    20
paulson@15481
    21
(* signature BASIC_ISA_FTERM = 
paulson@15481
    22
FOCUS_TERM_SIG where type Term = ISA_ENCODE_TERM.Term *)
paulson@15481
    23
paulson@15481
    24
signature ISA_FTERM =
dixon@15814
    25
  sig
dixon@15814
    26
    type Term = EncodeIsaFTerm.TermT
dixon@15814
    27
    type Type = Term.typ
dixon@15814
    28
    type UpTerm
dixon@15814
    29
    datatype FcTerm = focus of Term * UpTerm
dixon@15814
    30
    structure MinTermS : F_ENCODE_TERM_SIG
dixon@15814
    31
    val add_upterm :
dixon@15814
    32
       UpTerm -> FcTerm -> FcTerm
paulson@15481
    33
    val clean_match_ft :
paulson@15481
    34
       Type.tsig ->
dixon@15814
    35
       Term.term ->
paulson@15481
    36
       FcTerm ->
paulson@15481
    37
       (
dixon@15915
    38
       ((Term.indexname * (Term.sort * Term.typ)) list 
dixon@15915
    39
        * (Term.indexname * (Term.typ * Term.term)) list)
dixon@15915
    40
       * (string * Term.typ) list 
dixon@15915
    41
       * (string * Term.typ) list 
dixon@15915
    42
       * Term.term)
dixon@15814
    43
       option
paulson@15481
    44
    val clean_unify_ft :
paulson@15481
    45
       Sign.sg ->
paulson@15481
    46
       int ->
dixon@15814
    47
       Term.term ->
paulson@15481
    48
       FcTerm ->
paulson@15481
    49
       (
dixon@15915
    50
       ((Term.indexname * (Term.sort * Term.typ)) list 
dixon@15915
    51
        * (Term.indexname * (Term.typ * Term.term)) list)
dixon@15814
    52
       * (string * Term.typ) list * (string * Term.typ) list * Term.term)
dixon@15814
    53
       Seq.seq
dixon@15814
    54
    val enc_appl :
dixon@15814
    55
       EncodeIsaFTerm.term * UpTerm -> UpTerm
dixon@15814
    56
    val enc_appr :
dixon@15814
    57
       EncodeIsaFTerm.term * UpTerm -> UpTerm
dixon@15814
    58
    val fakefree_badbounds : 
dixon@15814
    59
       (string * Term.typ) list -> Term.term ->
dixon@15814
    60
       (string * Term.typ) list * (string * Term.typ) list * Term.term
dixon@15814
    61
    val fcterm_of_term : EncodeIsaFTerm.term -> FcTerm
paulson@15481
    62
    val find_fcterm_matches :
paulson@15481
    63
       ((FcTerm -> 'a) -> FcTerm -> 'b) ->
paulson@15481
    64
       (FcTerm -> 'a) -> FcTerm -> 'b
paulson@15481
    65
    val find_sg_concl_matches :
paulson@15481
    66
       ((FcTerm -> 'a) -> FcTerm -> 'b) ->
paulson@15481
    67
       (FcTerm -> 'a) -> int -> EncodeIsaFTerm.term -> 'b
paulson@15481
    68
    val find_sg_concl_thm_matches :
paulson@15481
    69
       ((FcTerm -> 'a) -> FcTerm -> 'b) ->
paulson@15481
    70
       (FcTerm -> 'a) -> int -> Thm.thm -> 'b
paulson@15481
    71
    val find_sg_matches :
paulson@15481
    72
       ((FcTerm -> 'a) -> FcTerm -> 'b) ->
paulson@15481
    73
       (FcTerm -> 'a) -> int -> EncodeIsaFTerm.term -> 'b
paulson@15481
    74
    val find_sg_thm_matches :
paulson@15481
    75
       ((FcTerm -> 'a) -> FcTerm -> 'b) ->
paulson@15481
    76
       (FcTerm -> 'a) -> int -> Thm.thm -> 'b
dixon@15814
    77
    val focus_abs : FcTerm -> FcTerm
dixon@15814
    78
    val focus_bot_left_leaf : FcTerm -> FcTerm
dixon@15814
    79
    val focus_bot_left_nonabs_leaf :
dixon@15814
    80
       FcTerm -> FcTerm
dixon@15814
    81
    val focus_fake_abs : FcTerm -> FcTerm
dixon@15814
    82
    val focus_left : FcTerm -> FcTerm
dixon@15814
    83
    val focus_of_fcterm : FcTerm -> EncodeIsaFTerm.term
dixon@15814
    84
    val focus_right : FcTerm -> FcTerm
dixon@15814
    85
    val focus_strict_left : FcTerm -> FcTerm
dixon@15814
    86
    exception focus_term_exp of string
paulson@15481
    87
    val focus_to_concl : FcTerm -> FcTerm
paulson@15481
    88
    val focus_to_concl_of_term : EncodeIsaFTerm.term -> FcTerm
dixon@15814
    89
    val focus_to_dest_impl :
dixon@15814
    90
       FcTerm -> FcTerm * FcTerm
paulson@15481
    91
    val focus_to_subgoal :
paulson@15481
    92
       int -> FcTerm -> FcTerm
paulson@15481
    93
    val focus_to_subgoal_of_term :
paulson@15481
    94
       int -> EncodeIsaFTerm.term -> FcTerm
paulson@15481
    95
    val focus_to_term_goal_prem :
paulson@15481
    96
       int * int -> EncodeIsaFTerm.term -> FcTerm
dixon@15814
    97
    val focus_to_top : FcTerm -> FcTerm
dixon@15814
    98
    val focus_up : FcTerm -> FcTerm
dixon@15814
    99
    val focus_up_abs : FcTerm -> FcTerm option
dixon@15814
   100
    val focus_up_abs_or_appr :
dixon@15814
   101
       FcTerm -> FcTerm option
dixon@15814
   102
    val focus_up_appl : FcTerm -> FcTerm option
dixon@15814
   103
    val focus_up_appr : FcTerm -> FcTerm option
dixon@15814
   104
    val focus_up_right : FcTerm -> FcTerm
dixon@15814
   105
    val focus_up_right1 : FcTerm -> FcTerm
paulson@15481
   106
    val focuseq_to_subgoals :
paulson@15481
   107
       FcTerm -> FcTerm Seq.seq
paulson@15481
   108
    exception isa_focus_term_exp of string
dixon@15814
   109
    val leaf_seq_of_fcterm :
dixon@15814
   110
       FcTerm -> FcTerm Seq.seq
paulson@15481
   111
    val mk_foo_match :
paulson@15481
   112
       (Term.term -> Term.term) ->
paulson@15481
   113
       ('a * Term.typ) list -> Term.term -> Term.term
dixon@15814
   114
    val mk_term_of_upterm :
dixon@15814
   115
       EncodeIsaFTerm.term * UpTerm -> EncodeIsaFTerm.term
dixon@15814
   116
    val mk_termf_of_upterm :
dixon@15814
   117
       UpTerm ->
dixon@15814
   118
       (string * Type) list *
dixon@15814
   119
       (EncodeIsaFTerm.term -> EncodeIsaFTerm.term)
dixon@15814
   120
    val next_leaf_fcterm : FcTerm -> FcTerm
dixon@15814
   121
    val next_leaf_of_fcterm_seq :
dixon@15814
   122
       FcTerm -> FcTerm Seq.seq
dixon@15814
   123
    exception out_of_term_exception of string
paulson@15481
   124
    val prepmatch :
paulson@15481
   125
       FcTerm ->
dixon@15814
   126
       Term.term *
dixon@15814
   127
       ((string * Term.typ) list * (string * Term.typ) list * Term.term)
dixon@15814
   128
    val pretty_fcterm : FcTerm -> Pretty.T
dixon@15814
   129
    val pure_mk_termf_of_upterm :
dixon@15814
   130
       (EncodeIsaFTerm.term, Type) UpTermLib.T ->
dixon@15814
   131
       (string * Type) list *
dixon@15814
   132
       (EncodeIsaFTerm.term -> EncodeIsaFTerm.term)
dixon@15814
   133
    val search_all_bl_ru_f :
dixon@15814
   134
       (FcTerm -> 'a Seq.seq) ->
dixon@15814
   135
       FcTerm -> 'a Seq.seq
dixon@15814
   136
    val search_all_bl_ur_f :
paulson@15481
   137
       (FcTerm -> 'a Seq.seq) ->
paulson@15481
   138
       FcTerm -> 'a Seq.seq
dixon@15814
   139
    val search_tlr_all_f :
dixon@15814
   140
       (FcTerm -> 'a Seq.seq) ->
dixon@15814
   141
       FcTerm -> 'a Seq.seq
dixon@15814
   142
    val search_tlr_valid_f :
dixon@15814
   143
       (FcTerm -> 'a Seq.seq) ->
dixon@15814
   144
       FcTerm -> 'a Seq.seq
dixon@15814
   145
    val search_valid_bl_ru_f :
dixon@15814
   146
       (FcTerm -> 'a Seq.seq) ->
dixon@15814
   147
       FcTerm -> 'a Seq.seq
dixon@15814
   148
    val search_valid_bl_ur_f :
paulson@15481
   149
       (FcTerm -> 'a Seq.seq) ->
paulson@15481
   150
       FcTerm -> 'a Seq.seq
dixon@15814
   151
    val set_focus_of_fcterm :
dixon@15814
   152
       FcTerm -> EncodeIsaFTerm.term -> FcTerm
dixon@15814
   153
    val term_of_fcterm : FcTerm -> EncodeIsaFTerm.term
dixon@15814
   154
    val tyenv_of_focus :
dixon@15814
   155
       FcTerm -> (string * Type) list
dixon@15814
   156
    val tyenv_of_focus' : FcTerm -> Type list
dixon@15814
   157
    val upsize_of_fcterm : FcTerm -> int
dixon@15814
   158
    val upterm_of : FcTerm -> UpTerm
paulson@15481
   159
    val valid_match_start : FcTerm -> bool
dixon@15814
   160
  end
paulson@15481
   161
dixon@15814
   162
paulson@15481
   163
paulson@15481
   164
structure BasicIsaFTerm = 
paulson@15481
   165
FocusTermFUN( structure EncodeTerm = EncodeIsaFTerm);
paulson@15481
   166
paulson@15481
   167
(* HOL Dependent *)
dixon@15814
   168
structure IsaFTerm : ISA_FTERM=
paulson@15481
   169
struct 
paulson@15481
   170
paulson@15481
   171
(* include BasicIsaFTerm *)
paulson@15481
   172
(* open FocusTermFUN( structure EncodeTerm = EncodeIsaFTerm ); *)
paulson@15481
   173
paulson@15481
   174
open BasicIsaFTerm;
paulson@15481
   175
paulson@15481
   176
wenzelm@15661
   177
(* Some general search within a focus term... *)
paulson@15481
   178
paulson@15481
   179
(* Note: only upterms with a free or constant are going to yeald a
paulson@15481
   180
match, thus if we get anything else (bound or var) skip it! This is
paulson@15481
   181
important if we switch to a unification net! in particular to avoid
paulson@15481
   182
vars. *)
paulson@15481
   183
paulson@15481
   184
fun valid_match_start ft =
paulson@15481
   185
    (case TermLib.bot_left_leaf_of (focus_of_fcterm ft) of 
paulson@15481
   186
       Const _ => true
dixon@15814
   187
     | Free _ => true
dixon@15814
   188
     | Abs _ => true (* allowed to look inside abs... search decides if we actually consider the abstraction itself *)
dixon@15814
   189
     | _ => false); (* avoid vars - always suceeds uninterestingly. *)
paulson@15481
   190
paulson@15481
   191
(* match starting at the bottom left, moving up to top of the term,
paulson@15481
   192
   then moving right to the next leaf and up again etc *)
paulson@15481
   193
(* FIXME: make properly lazy! *)
dixon@15814
   194
fun search_valid_bl_ur_f f ft = 
paulson@15481
   195
    let 
paulson@15481
   196
      val fts = 
paulson@15481
   197
          Seq.filter valid_match_start
paulson@15481
   198
                     (leaf_seq_of_fcterm ft)
paulson@15481
   199
paulson@15481
   200
      fun mk_match_up_seq ft =
dixon@15814
   201
          (* avoid abstractions? - possibly infinite unifiers? *)
dixon@15814
   202
          let val hereseq = case (focus_of_fcterm ft) of 
dixon@15814
   203
                              Abs _ => Seq.empty
dixon@15814
   204
                            | _ => f ft
dixon@15814
   205
          in
dixon@15814
   206
            case focus_up_abs_or_appr ft of 
dixon@15814
   207
              SOME ft' => Seq.append(hereseq, mk_match_up_seq ft')
dixon@15814
   208
            | NONE => hereseq
dixon@15814
   209
          end
paulson@15481
   210
    in
paulson@15481
   211
      Seq.flat (Seq.map mk_match_up_seq fts)
paulson@15481
   212
    end;
paulson@15481
   213
dixon@15814
   214
fun search_all_bl_ur_f f ft = 
paulson@15481
   215
    let 
paulson@15481
   216
      val fts = (leaf_seq_of_fcterm ft)
paulson@15481
   217
dixon@15814
   218
      fun mk_match_up_seq ft =            
paulson@15481
   219
          case focus_up_abs_or_appr ft of 
skalberg@15531
   220
            SOME ft' => Seq.append(f ft, mk_match_up_seq ft')
skalberg@15531
   221
          | NONE => f ft
paulson@15481
   222
    in
paulson@15481
   223
      Seq.flat (Seq.map mk_match_up_seq fts)
paulson@15481
   224
    end;
paulson@15481
   225
paulson@15481
   226
paulson@15481
   227
(* FIXME: make properly lazy! *)
paulson@15481
   228
(* FIXME: make faking of bound vars local - for speeeeed *)
dixon@15814
   229
fun search_valid_bl_ru_f f ft = 
paulson@15481
   230
    let
paulson@15481
   231
      fun mauxtop ft = 
paulson@15481
   232
          if (valid_match_start ft)
paulson@15481
   233
            then maux ft else Seq.empty
paulson@15481
   234
      and maux ft = 
paulson@15481
   235
          let val t' = (focus_of_fcterm ft) 
paulson@15481
   236
          (* val _ = writeln ("Examining: " ^ (TermLib.string_of_term t')) *)
paulson@15481
   237
          in 
paulson@15481
   238
          (case t' of 
paulson@15481
   239
            (_ $ _) => Seq.append (maux (focus_left ft), 
paulson@15481
   240
                         Seq.append(mauxtop (focus_right ft), 
paulson@15481
   241
                                    f ft))
dixon@15814
   242
          | (Abs _) => maux (focus_abs ft)
paulson@15481
   243
          | leaf => f ft) end
paulson@15481
   244
    in
paulson@15481
   245
      mauxtop ft
paulson@15481
   246
    end;
paulson@15481
   247
paulson@15481
   248
dixon@15814
   249
fun search_all_bl_ru_f f ft = 
paulson@15481
   250
    let
paulson@15481
   251
      fun maux ft = 
paulson@15481
   252
          let val t' = (focus_of_fcterm ft) 
paulson@15481
   253
          (*   val _ = writeln ("Examining: " ^ (TermLib.string_of_term t')) *)
paulson@15481
   254
          in 
paulson@15481
   255
          (case t' of 
paulson@15481
   256
            (_ $ _) => Seq.append (maux (focus_left ft), 
paulson@15481
   257
                         Seq.append(maux (focus_right ft), 
paulson@15481
   258
                                    f ft))
paulson@15481
   259
          | (Abs _) => Seq.append (maux (focus_abs ft), 
paulson@15481
   260
                                   f ft)
paulson@15481
   261
          | leaf => f ft) end
paulson@15481
   262
    in maux ft end;
paulson@15481
   263
dixon@15814
   264
(* search from top, left to right, then down *)
dixon@15814
   265
fun search_tlr_all_f f ft = 
dixon@15814
   266
    let
dixon@15814
   267
      fun maux ft = 
dixon@15814
   268
          let val t' = (focus_of_fcterm ft) 
dixon@15814
   269
            (* val _ = 
dixon@15814
   270
                if !trace_subst_search then 
dixon@15814
   271
                  (writeln ("Examining: " ^ (TermLib.string_of_term t'));
dixon@15814
   272
                   TermLib.writeterm t'; ())
dixon@15814
   273
                else (); *)
dixon@15814
   274
          in 
dixon@15814
   275
          (case t' of 
dixon@15814
   276
            (_ $ _) => Seq.append(maux (focus_left ft), 
dixon@15814
   277
                       Seq.append(f ft, 
dixon@15814
   278
                                  maux (focus_right ft)))
dixon@15814
   279
          | (Abs _) => Seq.append(f ft, maux (focus_abs ft))
dixon@15814
   280
          | leaf => f ft) end
dixon@15814
   281
    in maux ft end;
dixon@15814
   282
dixon@15814
   283
fun search_tlr_valid_f f ft = 
dixon@15814
   284
    let
dixon@15814
   285
      fun maux ft = 
dixon@15814
   286
          let 
dixon@15814
   287
            val hereseq = if valid_match_start ft then f ft else Seq.empty
dixon@15814
   288
          in 
dixon@15814
   289
          (case (focus_of_fcterm ft) of 
dixon@15814
   290
            (_ $ _) => Seq.append(maux (focus_left ft), 
dixon@15814
   291
                       Seq.append(hereseq, 
dixon@15814
   292
                                  maux (focus_right ft)))
dixon@15814
   293
          | (Abs _) => Seq.append(hereseq, maux (focus_abs ft))
dixon@15814
   294
          | leaf => hereseq)
dixon@15814
   295
          end
dixon@15814
   296
    in maux ft end;
dixon@15814
   297
paulson@15481
   298
paulson@15481
   299
paulson@15481
   300
exception isa_focus_term_exp of string;
paulson@15481
   301
paulson@15481
   302
paulson@15481
   303
fun focus_to_dest_impl ft = 
paulson@15481
   304
    let val (lhs, rhs) = 
paulson@15481
   305
            Logic.dest_implies (focus_of_fcterm ft) 
paulson@15481
   306
    in (focus_left ft, focus_right ft) end
paulson@15481
   307
    handle Term.TERM _ => 
paulson@15481
   308
           raise isa_focus_term_exp 
paulson@15481
   309
                   "focus_to_dest_impl: applied to non implication";
paulson@15481
   310
paulson@15481
   311
paulson@15481
   312
(* move focus to the conlusion *)
paulson@15481
   313
fun focus_to_concl ft = 
paulson@15481
   314
    let val (lhs, rhs) = 
paulson@15481
   315
            Logic.dest_implies (focus_of_fcterm ft) 
paulson@15481
   316
    in focus_to_concl (focus_right ft) end
paulson@15481
   317
    handle Term.TERM _ =>  ft;
paulson@15481
   318
paulson@15481
   319
val focus_to_concl_of_term = focus_to_concl o fcterm_of_term;
paulson@15481
   320
paulson@15481
   321
paulson@15481
   322
paulson@15481
   323
(* give back sequence of focuses at different subgoals *)
paulson@15481
   324
(* FIXME: make truly lazy *)
paulson@15481
   325
fun focuseq_to_subgoals ft = 
paulson@15481
   326
    if (Logic.is_implies (focus_of_fcterm ft)) then 
paulson@15481
   327
      Seq.cons (focus_right (focus_left ft), focuseq_to_subgoals (focus_right ft))
paulson@15481
   328
    else
paulson@15481
   329
      Seq.empty;
paulson@15481
   330
paulson@15481
   331
(* move focus to a specific subgoal, 0 is first  *)
paulson@15481
   332
fun focus_to_subgoal j ft = 
paulson@15481
   333
    let fun focus_to_subgoal' (ft, 0) = 
paulson@15481
   334
            let val (lhs, rhs) = Logic.dest_implies (focus_of_fcterm ft) 
paulson@15481
   335
            in ft |> focus_left |> focus_right end
paulson@15481
   336
          | focus_to_subgoal' (ft, i) = 
paulson@15481
   337
            let val (lhs, rhs) = Logic.dest_implies (focus_of_fcterm ft) 
paulson@15481
   338
            in focus_to_subgoal' (focus_right ft, i - 1) end
paulson@15481
   339
    in focus_to_subgoal' (ft, j - 1) end
paulson@15481
   340
    handle Term.TERM _ => 
paulson@15481
   341
           raise isa_focus_term_exp 
paulson@15481
   342
                   ("focus_to_subgoal: No such subgoal: " ^ 
paulson@15481
   343
                    (string_of_int j));
paulson@15481
   344
paulson@15481
   345
fun focus_to_subgoal_of_term i t = 
paulson@15481
   346
    focus_to_subgoal i (fcterm_of_term t)
paulson@15481
   347
paulson@15481
   348
(* move focus to a specific premise *)
paulson@15481
   349
(* fun focus_past_params i ft = 
paulson@15481
   350
    (focus_to_subgoal (focus_right ft, i))
paulson@15481
   351
    handle isa_focus_term_exp _ => 
paulson@15481
   352
           raise isa_focus_term_exp 
paulson@15481
   353
             ("focus_to_prmise: No such premise: " ^ (string_of_int i)); *)
paulson@15481
   354
paulson@15481
   355
fun focus_to_term_goal_prem (premid,gaolid) t = 
paulson@15481
   356
    focus_to_subgoal premid (focus_to_subgoal_of_term gaolid t);
paulson@15481
   357
paulson@15481
   358
dixon@15814
   359
(* FIXME: make a sturcture for holding free variable names and making
dixon@15814
   360
them distinct --- ? maybe part of the new prooftree datatype ?
dixon@15814
   361
Alos: use this to fix below... *)
paulson@15481
   362
paulson@15481
   363
(* T is outer bound vars, n is number of locally bound vars *)
dixon@15814
   364
(* THINK: is order of Ts correct...? or reversed? *)
dixon@15814
   365
fun fakefree_badbounds Ts t = 
dixon@15814
   366
    let val (FakeTs,Ts,newnames) = 
dixon@15814
   367
            List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
dixon@15814
   368
                           let val newname = Term.variant usednames n
dixon@15814
   369
                           in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
dixon@15814
   370
                               (newname,ty)::Ts, 
dixon@15814
   371
                               newname::usednames) end)
dixon@15814
   372
                       ([],[],[])
dixon@15814
   373
                       Ts
dixon@15814
   374
    in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
dixon@15814
   375
dixon@15814
   376
(* fun fakefree_badbounds usednames T n (a $ b) =  *)
dixon@15814
   377
(*     let val (usednames', T', a') = fakefree_badbounds usednames T n a *)
dixon@15814
   378
(*       val (usednames'', T'', b') = fakefree_badbounds usednames' T n b in  *)
dixon@15814
   379
(*       (usednames'', T'', a' $ b') end *)
dixon@15814
   380
(*   | fakefree_badbounds usednames T n (Abs(s,ty,t)) =  *)
dixon@15814
   381
(*     let val (usednames', T', t') = fakefree_badbounds usednames T (n + 1) t in *)
dixon@15814
   382
(*     (usednames', T', Abs(s,ty, t')) *)
dixon@15814
   383
(*   | fakefree_badbounds usednames T n (b as Bound i) =  *)
dixon@15814
   384
(*     let fun mkfake_bound j [] =  *)
dixon@15814
   385
(*             raise ERROR_MESSAGE "fakefree_badbounds: bound is outside of the known types!" *)
dixon@15814
   386
(*           | mkfake_bound 0 ((s,ty)::Ts) =  *)
dixon@15814
   387
(*             let val newname = Term.variant s usednames in *)
dixon@15814
   388
(*             usednames, (newname,ty) :: T,  Free (newname,ty) *)
dixon@15814
   389
(*           | mkfake_bound j (d::Ts) = mkfake_bound (j - 1) Ts *)
dixon@15814
   390
(*     in if n <= i then mkfake_bound (i - n) T else b end *)
dixon@15814
   391
(*   | fakefree_badbounds usednames T t = t; *)
paulson@15481
   392
paulson@15481
   393
paulson@15481
   394
(* note: outerterm is the taget with the match replaced by a bound 
paulson@15481
   395
         variable : ie: "P lhs" beocmes "%x. P x" 
paulson@15481
   396
         insts is the types of instantiations of vars in lhs
paulson@15481
   397
         and typinsts is the type instantiations of types in the lhs
paulson@15481
   398
         Note: Final rule is the rule lifted into the ontext of the 
paulson@15481
   399
         taget thm. *)
paulson@15481
   400
fun mk_foo_match mkuptermfunc Ts t = 
paulson@15481
   401
    let 
paulson@15481
   402
      val ty = Term.type_of t
paulson@15481
   403
      val bigtype = (rev (map snd Ts)) ---> ty
paulson@15481
   404
      fun mk_foo 0 t = t
paulson@15481
   405
        | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
paulson@15481
   406
      val num_of_bnds = (length Ts)
paulson@15481
   407
      (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
paulson@15481
   408
      val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
paulson@15481
   409
    in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
paulson@15481
   410
dixon@15814
   411
(* before matching we need to fake the bound vars that are missing an
paulson@15481
   412
abstraction. In this function we additionally construct the
paulson@15481
   413
abstraction environment, and an outer context term (with the focus
paulson@15481
   414
abstracted out) for use in rewriting with RWInst.rw *)
paulson@15481
   415
fun prepmatch ft = 
paulson@15481
   416
    let 
paulson@15481
   417
      val t = focus_of_fcterm ft  
paulson@15481
   418
      val Ts = tyenv_of_focus ft
dixon@15814
   419
      val (FakeTs', Ts', t') = fakefree_badbounds Ts t
paulson@15481
   420
      fun mktermf t = 
paulson@15481
   421
          term_of_fcterm (set_focus_of_fcterm ft t)
dixon@15814
   422
      val absterm = mk_foo_match mktermf Ts' t'
paulson@15481
   423
    in
dixon@15814
   424
      (t', (FakeTs', Ts', absterm))
paulson@15481
   425
    end;
paulson@15481
   426
paulson@15481
   427
(* matching and unification for a focus term's focus *)
dixon@15814
   428
dixon@15814
   429
(* Note: Ts is a modified version of the original names of the outer
dixon@15814
   430
bound variables. New names have been introduced to make sure they are
dixon@15814
   431
unique w.r.t all names in the term and each other. usednames' is
dixon@15814
   432
oldnames + new names. *)
paulson@15481
   433
fun clean_match_ft tsig pat ft = 
dixon@15814
   434
    let val (t, (FakeTs,Ts,absterm)) = prepmatch ft in
paulson@15481
   435
      case TermLib.clean_match tsig (pat, t) of 
skalberg@15531
   436
        NONE => NONE 
dixon@15814
   437
      | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
paulson@15481
   438
(* ix = max var index *)
paulson@15481
   439
fun clean_unify_ft sgn ix pat ft = 
dixon@15814
   440
    let val (t, (FakeTs, Ts,absterm)) = prepmatch ft in
dixon@15814
   441
    Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) 
paulson@15481
   442
            (TermLib.clean_unify sgn ix (t, pat)) end;
paulson@15481
   443
paulson@15481
   444
paulson@15481
   445
(* THINK: ? do we not need to incremement bound indices? *)
paulson@15481
   446
(* THINK: it should be the search which localisaes the search to the
paulson@15481
   447
current focus, not this hack in the matcher... ? *)
paulson@15481
   448
(* find matches below this particular focus term *) 
paulson@15481
   449
(* The search function is to find a match within a term... *)
paulson@15481
   450
(* the matcher is something that is applied to each node chosen by the
paulson@15481
   451
searchf and the results are flattened to form a lazy list. *)
paulson@15481
   452
fun find_fcterm_matches searchf matcher ft = 
paulson@15481
   453
    let 
paulson@15481
   454
      val ftupterm = upterm_of ft
paulson@15481
   455
      val focusft = focus_of_fcterm ft
paulson@15481
   456
      val add_uptermf = add_upterm ftupterm 
paulson@15481
   457
    in
paulson@15481
   458
    searchf
paulson@15481
   459
      (fn ft' => matcher (add_uptermf ft'))
paulson@15481
   460
      (fcterm_of_term focusft)
paulson@15481
   461
    end;
paulson@15481
   462
paulson@15481
   463
(* FIXME: move argument orders for efficiency... 
paulson@15481
   464
i.e. wenzel style val foofunc = x o y;
paulson@15481
   465
*)
paulson@15481
   466
paulson@15481
   467
(* find the matches inside subgoal i of th *)
paulson@15481
   468
fun find_sg_matches searchf matcher i t = 
dixon@15814
   469
    let 
dixon@15814
   470
      val subgoal_fcterm = focus_to_subgoal_of_term i t
paulson@15481
   471
    in find_fcterm_matches searchf matcher subgoal_fcterm end;
paulson@15481
   472
paulson@15481
   473
(* find the matches inside subgoal i of th *)
paulson@15481
   474
fun find_sg_thm_matches searchf matcher i th = 
paulson@15481
   475
    find_sg_matches searchf matcher i (Thm.prop_of th);
paulson@15481
   476
paulson@15481
   477
paulson@15481
   478
(* find the matches inside subgoal i's conclusion of th *)
paulson@15481
   479
fun find_sg_concl_matches searchf matcher i t = 
paulson@15481
   480
    let 
paulson@15481
   481
      val subgoal_fcterm = 
paulson@15481
   482
          focus_to_concl (focus_to_subgoal_of_term i t)
paulson@15481
   483
    in
paulson@15481
   484
      find_fcterm_matches searchf matcher subgoal_fcterm
paulson@15481
   485
    end;
paulson@15481
   486
paulson@15481
   487
(* find the matches inside subgoal i's conclusion of th *)
paulson@15481
   488
fun find_sg_concl_thm_matches searchf matcher i th = 
paulson@15481
   489
    find_sg_concl_matches searchf matcher i (Thm.prop_of th);
paulson@15481
   490
paulson@15481
   491
end;
paulson@15481
   492
paulson@15481
   493
(* 
paulson@15481
   494
test... 
paulson@15481
   495
paulson@15481
   496
f_encode_isatermS.encode (read "P a");
paulson@15481
   497
isafocustermS.fcterm_of_term (read "f a");
paulson@15481
   498
isafocustermS.term_of_fcterm it;
paulson@15481
   499
paulson@15481
   500
Goal "P b ==> P (suc b)";
paulson@15481
   501
paulson@15481
   502
TermLib.string_of_term ((focus_of_fcterm o focus_to_subgoal_of_term 1 o prop_of) (topthm()));
paulson@15481
   503
paulson@15481
   504
TermLib.string_of_term ((focus_of_fcterm o focus_to_concl o focus_to_subgoal_of_term 1 o prop_of) (topthm()));
paulson@15481
   505
paulson@15481
   506
TermLib.string_of_term ((focus_of_fcterm o focus_to_term_goal_prem (1,1) o prop_of) (topthm()));
paulson@15481
   507
paulson@15481
   508
*)