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