src/HOL/Mutabelle/mutabelle.ML
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 47004 6f00d8a83eb7
child 51092 5e6398b48030
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     1 (*  Title:      HOL/Mutabelle/mutabelle.ML
     2     Author:     Veronika Ortner, TU Muenchen
     3 
     4 Mutation of theorems.
     5 *)
     6 
     7 signature MUTABELLE =
     8 sig
     9   exception WrongPath of string;
    10   exception WrongArg of string;
    11   val freeze : term -> term
    12   val mutate_exc : term -> string list -> int -> term list 
    13   val mutate_sign : term -> theory -> (string * string) list -> int -> term list 
    14   val mutate_mix : term -> theory -> string list -> 
    15    (string * string) list -> int -> term list
    16 
    17   val all_unconcealed_thms_of : theory -> (string * thm) list
    18 end;
    19 
    20 structure Mutabelle : MUTABELLE = 
    21 struct
    22 
    23 fun all_unconcealed_thms_of thy =
    24   let
    25     val facts = Global_Theory.facts_of thy
    26   in
    27     Facts.fold_static
    28       (fn (s, ths) =>
    29         if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths))
    30       facts []
    31   end;
    32 
    33 fun thms_of thy = filter (fn (_, th) =>
    34    Context.theory_name (theory_of_thm th) = Context.theory_name thy) (all_unconcealed_thms_of thy);
    35 
    36 fun consts_of thy =
    37  let
    38    val (namespace, const_table) = #constants (Consts.dest (Sign.consts_of thy))
    39    val consts = Symtab.dest const_table
    40  in
    41    map_filter (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
    42      (filter_out (fn (s, _) => Name_Space.is_concealed namespace s) consts)
    43  end;
    44 
    45 
    46 (*thrown in case the specified path doesn't exist in the specified term*)
    47 
    48 exception WrongPath of string;
    49 
    50 
    51 (*thrown in case the arguments did not fit to the function*)
    52 
    53 exception WrongArg of string; 
    54 
    55 (*Rename the bound variables in a term with the minimal Index min of 
    56 bound variables. Variable (Bound(min)) will be renamed to Bound(0) etc. 
    57 This is needed in course auf evaluation of contexts.*)
    58 
    59 fun rename_bnds curTerm 0 = curTerm
    60  | rename_bnds (Bound(i)) minInd = 
    61    let 
    62      val erg = if (i-minInd < 0) then 0 else (i - minInd)
    63    in 
    64      Bound(erg)
    65    end
    66  | rename_bnds (Abs(name,t,uTerm)) minInd = 
    67    Abs(name,t,(rename_bnds uTerm minInd))
    68  | rename_bnds (fstUTerm $ sndUTerm) minInd =
    69    (rename_bnds fstUTerm minInd) $ (rename_bnds sndUTerm minInd)
    70  | rename_bnds elseTerm minInd = elseTerm;
    71 
    72 
    73 
    74 
    75 
    76 (*Partition a term in its subterms and create an entry 
    77 (term * type * abscontext * mincontext * path) 
    78 for each term in the return list 
    79 e.g: getSubTermList Abs(y, int, Const(f,int->int) $ Const(x,int) $ Bound(0))
    80 will give       [(Const(f,int->int),int->int,[int],[],[00]),
    81                (Const(x,int),int,[int],[],[010]),
    82                (Bound(0),int,[int],[int],[110]),
    83                (Const(x,int) $ Bound(0),type,[int],[int],[10]),
    84                (Const(f,int->int) $ Const(x,int) $ Bound(0),type,[int],[int],[0],
    85                (Abs (y,int,Const(f,int->int) $ const(x,int) $ Bound(0)),type,[],[],[])]
    86                 *)
    87 
    88 fun getSubTermList (Const(name,t)) abscontext path acc =
    89    (Const(name,t),t,abscontext,abscontext,path)::acc
    90  | getSubTermList (Free(name,t)) abscontext path acc =
    91    (Free(name,t),t,abscontext,abscontext,path)::acc
    92  | getSubTermList (Var(indname,t)) abscontext path acc =
    93    (Var(indname,t),t,abscontext,abscontext,path)::acc
    94  | getSubTermList (Bound(i)) abscontext path acc =
    95    (Bound(0),nth abscontext i,abscontext, Library.drop i abscontext,path)::acc
    96  | getSubTermList (Abs(name,t,uTerm)) abscontext path acc = 
    97    let 
    98      val curTerm = Abs(name,t,uTerm)
    99      val bnos = Term.add_loose_bnos (curTerm,0,[])
   100      val minInd = if (bnos = []) then 0 
   101        else Library.foldl (fn (n,m) => if (n<m) then n else m) (hd bnos,tl bnos)
   102      val newTerm = rename_bnds curTerm minInd
   103      val newContext = Library.drop minInd abscontext
   104    in 
   105      getSubTermList uTerm (t::abscontext) (0::path) 
   106                ((newTerm,(fastype_of1 (abscontext, curTerm)),abscontext,newContext,path)::acc)
   107    end
   108  | getSubTermList (fstUTerm $ sndUTerm) abscontext path acc = 
   109    let 
   110      val curTerm = (fstUTerm $ sndUTerm)
   111      val bnos = Term.add_loose_bnos (curTerm, 0, [])
   112      val minInd = if (bnos = []) then 0
   113        else Library.foldl (fn (n,m) => if (n<m) then n else m) (hd bnos,tl bnos)
   114      val newTerm = rename_bnds curTerm minInd
   115      val newContext = Library.drop minInd abscontext
   116    in 
   117      getSubTermList fstUTerm abscontext (0::path) 
   118        (getSubTermList sndUTerm abscontext (1::path) 
   119          ((newTerm,(fastype_of1 (abscontext, curTerm)),abscontext,newContext,path)::acc)) 
   120    end;  
   121 
   122 
   123 (*Evaluate if the longContext is more special as the shortContext. 
   124 If so, a term with shortContext can be substituted in the place of a 
   125 term with longContext*)
   126 
   127 fun is_morespecial longContext shortContext = 
   128  let 
   129    val revlC = rev longContext
   130    val revsC = rev shortContext
   131    fun is_prefix [] longList = true
   132      | is_prefix shList [] = false
   133      | is_prefix (x::xs) (y::ys) = if (x=y) then is_prefix xs ys else false
   134  in 
   135    is_prefix revsC revlC
   136  end;
   137 
   138 
   139 (*takes a (term * type * context * context * path)-tupel and searches in the specified list for 
   140 terms with the same type and appropriate context. Returns a (term * path) list of these terms.
   141 Used in order to generate a list of type-equal subterms of the original term*)
   142 
   143 fun searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) [] resultList = 
   144    resultList
   145  | searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) 
   146    ((hdterm,hdtype,hdabsContext,hdminContext,hdpath)::xs) resultList = 
   147    if ((stype = hdtype) andalso (is_morespecial sabsContext hdminContext) 
   148      andalso (is_morespecial hdabsContext sminContext)) 
   149    then searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) xs 
   150      ((hdterm,hdabsContext,hdminContext,hdpath)::resultList) 
   151    else searchForMutatableSubTerm (sterm,stype,sabsContext,sminContext,spath) xs resultList;
   152 
   153 
   154 (*evaluates if the given function is in the passed list of forbidden functions*)
   155 
   156 fun in_list_forb consSig (consNameStr,consType) [] = false
   157  | in_list_forb consSig (consNameStr,consType) ((forbNameStr,forbTypeStr)::xs) = 
   158    let 
   159      val forbType = Syntax.read_typ_global consSig forbTypeStr
   160    in
   161      if ((consNameStr = forbNameStr) 
   162        andalso (Sign.typ_instance consSig (consType,(Logic.varifyT_global forbType))))
   163      then true
   164      else in_list_forb consSig (consNameStr,consType) xs
   165    end;
   166 
   167 
   168 
   169 (*searches in the given signature Consts with the same type as sterm and 
   170 returns a list of those terms*)
   171 
   172 fun searchForSignatureMutations (sterm,stype) consSig forbidden_funs = 
   173  let 
   174    val sigConsTypeList = consts_of consSig;
   175  in 
   176    let 
   177      fun recursiveSearch mutatableTermList [] = mutatableTermList
   178        | recursiveSearch mutatableTermList ((ConsName,ConsType)::xs) = 
   179          if (Sign.typ_instance consSig (stype,ConsType) 
   180            andalso (not (sterm = Const(ConsName,stype))) 
   181            andalso (not (in_list_forb consSig (ConsName,ConsType) forbidden_funs))) 
   182          then recursiveSearch ((Term.Const(ConsName,stype), [], [], [5])::mutatableTermList) xs
   183          else recursiveSearch mutatableTermList xs
   184      in
   185        recursiveSearch [] sigConsTypeList
   186      end
   187    end;     
   188 
   189 
   190 (*generates a list of terms that can be used instead of the passed subterm in the original term. These terms either have
   191 the same type and appropriate context and are generated from the list of subterms either - in case of a Const-term they have been found
   192 in the current signature.
   193 This function has 3 versions:
   194 0: no instertion of signature functions, 
   195   only terms in the subTermList with the same type and appropriate context as the passed term are returned
   196 1: no exchange of subterms,
   197   only signature functions are inserted at the place of type-aequivalent Conses
   198 2: mixture of the two other versions. insertion of signature functions and exchange of subterms*)
   199 
   200 fun searchForMutatableTerm 0 (sterm,stype,sabscontext,smincontext,spath) 
   201    subTerms consSig resultList forbidden_funs =
   202    searchForMutatableSubTerm (sterm,stype,sabscontext,smincontext,spath) subTerms resultList
   203  | searchForMutatableTerm 1 (Const(constName,constType),stype,sabscontext,smincontext,spath) 
   204    subTerms consSig resultList forbidden_funs = 
   205    searchForSignatureMutations (Const(constName,constType),stype) consSig forbidden_funs
   206  | searchForMutatableTerm 1 _ _ _ _ _ = []
   207  | searchForMutatableTerm 2 (Const(constName,constType),stype,sabscontext,smincontext,spath) 
   208    subTerms consSig resultList forbidden_funs = 
   209      let 
   210        val subtermMutations = searchForMutatableSubTerm 
   211          (Const(constName,constType),stype,sabscontext,smincontext,spath) subTerms resultList
   212        val signatureMutations = searchForSignatureMutations 
   213          (Const(constName,constType),stype) consSig forbidden_funs
   214      in
   215        subtermMutations@signatureMutations
   216      end
   217  | searchForMutatableTerm 2 (sterm,stype,sabscontext,smincontext,spath) 
   218    subTerms consSig resultList forbidden_funs =
   219    searchForMutatableSubTerm (sterm,stype,sabscontext,smincontext,spath) subTerms resultList
   220  | searchForMutatableTerm i _ _ _ _ _ = 
   221    raise WrongArg("Version " ^ string_of_int i ^ 
   222      " doesn't exist for function searchForMutatableTerm!") ;
   223 
   224 
   225 
   226 
   227 (*evaluates if the two terms with paths passed as arguments can be exchanged, i.e. evaluates if one of the terms is a subterm of the other one*)  
   228 
   229 fun areReplacable [] [] = false
   230  | areReplacable fstPath [] = false
   231  | areReplacable [] sndPath = false
   232  | areReplacable (x::xs) (y::ys) = if (x=y) then areReplacable xs ys else true; 
   233 
   234 
   235 
   236 
   237 (*substitutes the term at the position of the first list in fstTerm by sndTerm. 
   238 The lists represent paths as generated by createSubTermList*)
   239 
   240 fun substitute [] fstTerm sndTerm = sndTerm
   241  | substitute (_::xs) (Abs(s,T,subTerm)) sndTerm = Abs(s,T,(substitute xs subTerm sndTerm))
   242  | substitute (0::xs) (t $ u) sndTerm = substitute xs t sndTerm $ u 
   243  | substitute (1::xs) (t $ u) sndTerm = t $ substitute xs u sndTerm
   244  | substitute (_::xs) _ sndTerm = 
   245    raise WrongPath ("The Term could not be found at the specified position"); 
   246 
   247 
   248 (*get the subterm with the specified path in myTerm*)
   249 
   250 fun getSubTerm myTerm [] = myTerm
   251  | getSubTerm (Abs(s,T,subTerm)) (0::xs) = getSubTerm subTerm xs
   252  | getSubTerm (t $ u) (0::xs) = getSubTerm t xs
   253  | getSubTerm (t $ u) (1::xs) = getSubTerm u xs
   254  | getSubTerm _ (_::xs) = 
   255    raise WrongPath ("The subterm could not be found at the specified position");
   256 
   257 
   258 (*exchanges two subterms with the given paths in the original Term*)
   259 
   260 fun replace origTerm (fstTerm, fstPath) (sndTerm, sndPath) = 
   261  if (areReplacable (rev fstPath) (rev sndPath))
   262  then substitute (rev sndPath) (substitute (rev fstPath) origTerm sndTerm) fstTerm
   263  else origTerm; 
   264 
   265 
   266 
   267 
   268 (*tests if the terms with the given pathes in the origTerm are commutative
   269 respecting the list of commutative operators (commutatives)*)
   270 
   271 fun areCommutative origTerm fstPath sndPath commutatives =
   272  if (sndPath = []) 
   273  then false
   274  else
   275    let 
   276      val base = (tl sndPath)
   277    in
   278      let 
   279        val fstcomm = 1::0::base
   280        val opcomm = 0::0::base
   281      in
   282        if ((fstPath = fstcomm) andalso (is_Const (getSubTerm origTerm (rev opcomm))))
   283        then
   284          let 
   285            val Const(name,_) = (getSubTerm origTerm (rev opcomm))
   286          in
   287            member (op =) commutatives name
   288          end
   289        else false
   290      end
   291    end;
   292 
   293 
   294 (*Canonizes term t with the commutative operators stored in list 
   295 commutatives*)
   296 
   297 fun canonize_term (Const (s, T) $ t $ u) comms =
   298  let
   299    val t' = canonize_term t comms;
   300    val u' = canonize_term u comms;
   301  in 
   302    if member (op =) comms s andalso Term_Ord.termless (u', t')
   303    then Const (s, T) $ u' $ t'
   304    else Const (s, T) $ t' $ u'
   305  end
   306  | canonize_term (t $ u) comms = canonize_term t comms $ canonize_term u comms
   307  | canonize_term (Abs (s, T, t)) comms = Abs (s, T, canonize_term t comms)
   308  | canonize_term t comms = t;
   309 
   310 
   311 (*inspect the passed list and mutate origTerm following the elements of the list:
   312 if the path of the current element is [5] (dummy path), the term has been found in the signature 
   313 and the subterm will be substituted by it
   314 else the term has been found in the original term and the two subterms have to be exchanged
   315 The additional parameter commutatives indicates the commutative operators  
   316 in the term whose operands won't be exchanged*)
   317 
   318 fun createMutatedTerms origTerm _ [] commutatives mutatedTerms = mutatedTerms
   319  | createMutatedTerms origTerm (hdt as (hdTerm,hdabsContext,hdminContext,hdPath))
   320    ((sndTerm,sndabsContext,sndminContext,sndPath)::xs) commutatives mutatedTerms = 
   321    if (sndPath = [5])
   322    then
   323      let 
   324          val canonized = canonize_term (substitute (rev hdPath) origTerm sndTerm) commutatives
   325        in
   326          if (canonized = origTerm)  
   327          then createMutatedTerms origTerm hdt xs commutatives mutatedTerms
   328          else createMutatedTerms origTerm hdt xs commutatives 
   329            (insert op aconv canonized mutatedTerms)
   330        end
   331      else 
   332        if ((areCommutative origTerm hdPath sndPath commutatives)
   333          orelse (areCommutative origTerm sndPath hdPath commutatives)) 
   334        then createMutatedTerms origTerm hdt xs commutatives mutatedTerms
   335        else
   336          let 
   337            val canonized = canonize_term 
   338              (replace origTerm
   339                 (incr_boundvars (length sndabsContext - length hdminContext) hdTerm,
   340                  hdPath)
   341                 (incr_boundvars (length hdabsContext - length sndminContext) sndTerm,
   342                  sndPath)) commutatives
   343          in
   344            if (not(canonized = origTerm)) 
   345            then createMutatedTerms origTerm hdt xs commutatives 
   346              (insert op aconv canonized mutatedTerms)
   347            else createMutatedTerms origTerm hdt xs commutatives mutatedTerms
   348          end;
   349 
   350 
   351 
   352 (*mutates origTerm by exchanging subterms. The mutated terms are returned in a term list
   353 The parameter commutatives consists of a list of commutative operators. The permutation of their 
   354 operands won't be considered as a new term
   355 !!!Attention!!!: The given origTerm must be canonized. Use function canonize_term!*)
   356 
   357 fun mutate_once option origTerm tsig commutatives forbidden_funs= 
   358  let 
   359    val subTermList = getSubTermList origTerm [] [] []
   360  in
   361    let 
   362      fun replaceRecursively [] mutatedTerms = mutatedTerms
   363        | replaceRecursively ((hdTerm,hdType,hdabsContext,hdminContext,hdPath)::tail) 
   364          mutatedTerms =
   365          replaceRecursively tail (union op aconv (createMutatedTerms origTerm 
   366            (hdTerm,hdabsContext,hdminContext,hdPath) 
   367            (searchForMutatableTerm option (hdTerm,hdType,hdabsContext,hdminContext,hdPath) 
   368              tail tsig [] forbidden_funs) 
   369            commutatives []) mutatedTerms)
   370    in
   371      replaceRecursively subTermList []
   372    end
   373  end;
   374 
   375 
   376 
   377 
   378 (*helper function in order to apply recursively the mutate_once function on a whole list of terms
   379 Needed for the mutate function*)
   380 
   381 fun mutate_once_rec option [] tsig commutatives forbidden_funs acc = acc
   382  | mutate_once_rec option (x::xs) tsig commutatives forbidden_funs acc = 
   383    mutate_once_rec option xs tsig commutatives forbidden_funs 
   384      (union op aconv (mutate_once option x tsig commutatives forbidden_funs) acc);
   385 
   386 
   387 
   388 (*apply function mutate_once iter times on the given origTerm. *)
   389 (*call of mutiere with canonized form of origTerm. Prevents us of the computation of
   390 canonization in the course of insertion of new terms!*)
   391 
   392 fun mutate option origTerm tsig commutatives forbidden_funs 0 = []
   393  | mutate option origTerm tsig commutatives forbidden_funs 1 = 
   394    mutate_once option (canonize_term origTerm commutatives) tsig commutatives forbidden_funs
   395  | mutate option origTerm tsig commutatives forbidden_funs iter = 
   396    mutate_once_rec option (mutate option origTerm tsig commutatives forbidden_funs (iter-1)) 
   397      tsig commutatives forbidden_funs []; 
   398 
   399 (*mutate origTerm iter times by only exchanging subterms*)
   400 
   401 fun mutate_exc origTerm commutatives iter =
   402  mutate 0 origTerm @{theory Main} commutatives [] iter;
   403 
   404 
   405 (*mutate origTerm iter times by only inserting signature functions*)
   406 
   407 fun mutate_sign origTerm tsig forbidden_funs iter = 
   408  mutate 1 origTerm tsig [] forbidden_funs iter;
   409 
   410 
   411 (*mutate origTerm iter times by exchange of subterms and insertion of subterms*)
   412 
   413 fun mutate_mix origTerm tsig commutatives forbidden_funs iter =
   414  mutate 2 origTerm tsig commutatives forbidden_funs iter;  
   415 
   416  
   417 (*helper function for the quickcheck invocation. Evaluates the quickcheck_term function on a whole list of terms
   418 and tries to print the exceptions*)
   419 
   420 fun freeze (t $ u) = freeze t $ freeze u
   421  | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
   422  | freeze (Var ((a, i), T)) =
   423      Free (if i = 0 then a else a ^ "_" ^ string_of_int i, T)
   424  | freeze t = t;
   425 
   426 fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
   427  | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T);
   428 
   429 fun preprocess thy insts t = Object_Logic.atomize_term thy
   430  (map_types (inst_type insts) (freeze t));
   431 
   432 fun is_executable thy insts th =
   433   let
   434     val ctxt' = Proof_Context.init_global thy
   435       |> Config.put Quickcheck.size 1
   436       |> Config.put Quickcheck.iterations 1
   437     val test = Quickcheck_Common.test_term
   438       ("exhaustive", ((fn _ => raise (Fail "")), Exhaustive_Generators.compile_generator_expr)) ctxt' false
   439   in  
   440     case try test (preprocess thy insts (prop_of th), []) of
   441       SOME _ => (Output.urgent_message "executable"; true)
   442     | NONE => (Output.urgent_message ("not executable"); false)
   443   end;                                               
   444 
   445 end