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