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