components/tactics/proofEngineReduction.ml

   1 (* Copyright (C) 2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                 12/04/2002                                 *)
  32 (*                                                                            *)
  33 (*                                                                            *)
  34 (******************************************************************************)
  35
  36 (* $Id$ *)
  37
  38 (* The code of this module is derived from the code of CicReduction *)
  39
  40 exception Impossible of int;;
  41 exception ReferenceToConstant;;
  42 exception ReferenceToVariable;;
  43 exception ReferenceToCurrentProof;;
  44 exception ReferenceToInductiveDefinition;;
  45 exception WrongUriToInductiveDefinition;;
  46 exception WrongUriToConstant;;
  47 exception RelToHiddenHypothesis;;
  48
  49 module C = Cic
  50 module S = CicSubstitution
  51
  52 let alpha_equivalence =
  53   let rec aux t t' =
  54    if t = t' then true
  55    else
  56     match t,t' with
  57        C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) ->
  58         UriManager.eq uri1 uri2 &&
  59          aux_exp_named_subst exp_named_subst1 exp_named_subst2
  60      | C.Cast (te,ty), C.Cast (te',ty') ->
  61         aux te te' && aux ty ty'
  62      | C.Prod (_,s,t), C.Prod (_,s',t') ->
  63         aux s s' && aux t t'
  64      | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
  65         aux s s' && aux t t'
  66      | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
  67         aux s s' && aux t t'
  68      | C.Appl l, C.Appl l' ->
  69         (try
  70           List.fold_left2
  71            (fun b t1 t2 -> b && aux t1 t2) true l l'
  72          with
  73           Invalid_argument _ -> false)
  74      | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) ->
  75         UriManager.eq uri uri' &&
  76          aux_exp_named_subst exp_named_subst1 exp_named_subst2
  77      | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) ->
  78         UriManager.eq uri uri' && i = i' &&
  79          aux_exp_named_subst exp_named_subst1 exp_named_subst2
  80      | C.MutConstruct (uri,i,j,exp_named_subst1),
  81        C.MutConstruct (uri',i',j',exp_named_subst2) ->
  82         UriManager.eq uri uri' && i = i' && j = j' &&
  83          aux_exp_named_subst exp_named_subst1 exp_named_subst2
  84      | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
  85         UriManager.eq sp sp' && i = i' &&
  86          aux outt outt' && aux t t' &&
  87           (try
  88             List.fold_left2
  89              (fun b t1 t2 -> b && aux t1 t2) true pl pl'
  90            with
  91             Invalid_argument _ -> false)
  92      | C.Fix (i,fl), C.Fix (i',fl') ->
  93         i = i' &&
  94         (try
  95           List.fold_left2
  96            (fun b (_,i,ty,bo) (_,i',ty',bo') ->
  97              b && i = i' && aux ty ty' && aux bo bo'
  98            ) true fl fl'
  99          with
 100           Invalid_argument _ -> false)
 101      | C.CoFix (i,fl), C.CoFix (i',fl') ->
 102         i = i' &&
 103         (try
 104           List.fold_left2
 105            (fun b (_,ty,bo) (_,ty',bo') ->
 106              b && aux ty ty' && aux bo bo'
 107            ) true fl fl'
 108          with
 109           Invalid_argument _ -> false)
 110      | _,_ -> false (* we already know that t != t' *)
 111   and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
 112    try
 113      List.fold_left2
 114       (fun b (uri1,t1) (uri2,t2) ->
 115         b && UriManager.eq uri1 uri2 && aux t1 t2
 116       ) true exp_named_subst1 exp_named_subst2
 117     with
 118      Invalid_argument _ -> false
 119   in
 120    aux
 121 ;;
 122
 123 exception WhatAndWithWhatDoNotHaveTheSameLength;;
 124
 125 (* "textual" replacement of several subterms with other ones *)
 126 let replace ~equality ~what ~with_what ~where =
 127   let find_image t =
 128    let rec find_image_aux =
 129     function
 130        [],[] -> raise Not_found
 131      | what::tl1,with_what::tl2 ->
 132         if equality what t then with_what else find_image_aux (tl1,tl2)
 133      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
 134    in
 135     find_image_aux (what,with_what)
 136   in
 137   let rec aux t =
 138    try
 139     find_image t
 140    with Not_found ->
 141     match t with
 142        C.Rel _ -> t
 143      | C.Var (uri,exp_named_subst) ->
 144         C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
 145      | C.Meta _ -> t
 146      | C.Sort _ -> t
 147      | C.Implicit _ as t -> t
 148      | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
 149      | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
 150      | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
 151      | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
 152      | C.Appl l ->
 153         (* Invariant enforced: no application of an application *)
 154         (match List.map aux l with
 155             (C.Appl l')::tl -> C.Appl (l'@tl)
 156           | l' -> C.Appl l')
 157      | C.Const (uri,exp_named_subst) ->
 158         C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
 159      | C.MutInd (uri,i,exp_named_subst) ->
 160         C.MutInd
 161          (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
 162      | C.MutConstruct (uri,i,j,exp_named_subst) ->
 163         C.MutConstruct
 164          (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
 165      | C.MutCase (sp,i,outt,t,pl) ->
 166         C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
 167      | C.Fix (i,fl) ->
 168         let substitutedfl =
 169          List.map
 170           (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
 171            fl
 172         in
 173          C.Fix (i, substitutedfl)
 174      | C.CoFix (i,fl) ->
 175         let substitutedfl =
 176          List.map
 177           (fun (name,ty,bo) -> (name, aux ty, aux bo))
 178            fl
 179         in
 180          C.CoFix (i, substitutedfl)
 181    in
 182     aux where
 183 ;;
 184
 185 (* replaces in a term a term with another one. *)
 186 (* Lifting are performed as usual.             *)
 187 let replace_lifting ~equality ~what ~with_what ~where =
 188   let find_image what t =
 189    let rec find_image_aux =
 190     function
 191        [],[] -> raise Not_found
 192      | what::tl1,with_what::tl2 ->
 193         if equality what t then with_what else find_image_aux (tl1,tl2)
 194      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
 195    in
 196     find_image_aux (what,with_what)
 197   in
 198   let rec substaux k what t =
 199    try
 200     S.lift (k-1) (find_image what t)
 201    with Not_found ->
 202     match t with
 203       C.Rel n as t -> t
 204     | C.Var (uri,exp_named_subst) ->
 205        let exp_named_subst' =
 206         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
 207        in
 208         C.Var (uri,exp_named_subst')
 209     | C.Meta (i, l) ->
 210        let l' =
 211         List.map
 212          (function
 213              None -> None
 214            | Some t -> Some (substaux k what t)
 215          ) l
 216        in
 217         C.Meta(i,l')
 218     | C.Sort _ as t -> t
 219     | C.Implicit _ as t -> t
 220     | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
 221     | C.Prod (n,s,t) ->
 222        C.Prod
 223         (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
 224     | C.Lambda (n,s,t) ->
 225        C.Lambda
 226         (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
 227     | C.LetIn (n,s,t) ->
 228        C.LetIn
 229         (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
 230     | C.Appl (he::tl) ->
 231        (* Invariant: no Appl applied to another Appl *)
 232        let tl' = List.map (substaux k what) tl in
 233         begin
 234          match substaux k what he with
 235             C.Appl l -> C.Appl (l@tl')
 236           | _ as he' -> C.Appl (he'::tl')
 237         end
 238     | C.Appl _ -> assert false
 239     | C.Const (uri,exp_named_subst) ->
 240        let exp_named_subst' =
 241         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
 242        in
 243        C.Const (uri,exp_named_subst')
 244     | C.MutInd (uri,i,exp_named_subst) ->
 245        let exp_named_subst' =
 246         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
 247        in
 248         C.MutInd (uri,i,exp_named_subst')
 249     | C.MutConstruct (uri,i,j,exp_named_subst) ->
 250        let exp_named_subst' =
 251         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
 252        in
 253         C.MutConstruct (uri,i,j,exp_named_subst')
 254     | C.MutCase (sp,i,outt,t,pl) ->
 255        C.MutCase (sp,i,substaux k what outt, substaux k what t,
 256         List.map (substaux k what) pl)
 257     | C.Fix (i,fl) ->
 258        let len = List.length fl in
 259        let substitutedfl =
 260         List.map
 261          (fun (name,i,ty,bo) ->
 262            (name, i, substaux k what ty,
 263              substaux (k+len) (List.map (S.lift len) what) bo)
 264          ) fl
 265        in
 266         C.Fix (i, substitutedfl)
 267     | C.CoFix (i,fl) ->
 268        let len = List.length fl in
 269        let substitutedfl =
 270         List.map
 271          (fun (name,ty,bo) ->
 272            (name, substaux k what ty,
 273              substaux (k+len) (List.map (S.lift len) what) bo)
 274          ) fl
 275        in
 276         C.CoFix (i, substitutedfl)
 277  in
 278   substaux 1 what where
 279 ;;
 280
 281 (* replaces in a term a list of terms with other ones. *)
 282 (* Lifting are performed as usual.                     *)
 283 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
 284   let find_image t =
 285    let rec find_image_aux =
 286     function
 287        [],[] -> raise Not_found
 288      | what::tl1,with_what::tl2 ->
 289         if equality what t then with_what else find_image_aux (tl1,tl2)
 290      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
 291    in
 292     find_image_aux (what,with_what)
 293   in
 294   let rec substaux k t =
 295    try
 296     S.lift (k-1) (find_image t)
 297    with Not_found ->
 298     match t with
 299        C.Rel n ->
 300         if n < k then C.Rel n else C.Rel (n + nnn)
 301      | C.Var (uri,exp_named_subst) ->
 302         let exp_named_subst' =
 303          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
 304         in
 305          C.Var (uri,exp_named_subst')
 306      | C.Meta (i, l) ->
 307         let l' =
 308          List.map
 309           (function
 310               None -> None
 311             | Some t -> Some (substaux k t)
 312           ) l
 313         in
 314          C.Meta(i,l')
 315      | C.Sort _ as t -> t
 316      | C.Implicit _ as t -> t
 317      | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
 318      | C.Prod (n,s,t) ->
 319         C.Prod (n, substaux k s, substaux (k + 1) t)
 320      | C.Lambda (n,s,t) ->
 321         C.Lambda (n, substaux k s, substaux (k + 1) t)
 322      | C.LetIn (n,s,t) ->
 323         C.LetIn (n, substaux k s, substaux (k + 1) t)
 324      | C.Appl (he::tl) ->
 325         (* Invariant: no Appl applied to another Appl *)
 326         let tl' = List.map (substaux k) tl in
 327          begin
 328           match substaux k he with
 329              C.Appl l -> C.Appl (l@tl')
 330            | _ as he' -> C.Appl (he'::tl')
 331          end
 332      | C.Appl _ -> assert false
 333      | C.Const (uri,exp_named_subst) ->
 334         let exp_named_subst' =
 335          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
 336         in
 337         C.Const (uri,exp_named_subst')
 338      | C.MutInd (uri,i,exp_named_subst) ->
 339         let exp_named_subst' =
 340          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
 341         in
 342          C.MutInd (uri,i,exp_named_subst')
 343      | C.MutConstruct (uri,i,j,exp_named_subst) ->
 344         let exp_named_subst' =
 345          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
 346         in
 347          C.MutConstruct (uri,i,j,exp_named_subst')
 348      | C.MutCase (sp,i,outt,t,pl) ->
 349         C.MutCase (sp,i,substaux k outt, substaux k t,
 350          List.map (substaux k) pl)
 351      | C.Fix (i,fl) ->
 352         let len = List.length fl in
 353         let substitutedfl =
 354          List.map
 355           (fun (name,i,ty,bo) ->
 356             (name, i, substaux k ty, substaux (k+len) bo))
 357            fl
 358         in
 359          C.Fix (i, substitutedfl)
 360      | C.CoFix (i,fl) ->
 361         let len = List.length fl in
 362         let substitutedfl =
 363          List.map
 364           (fun (name,ty,bo) ->
 365             (name, substaux k ty, substaux (k+len) bo))
 366            fl
 367         in
 368          C.CoFix (i, substitutedfl)
 369  in
 370   substaux 1 where
 371 ;;
 372
 373 (* This is the inverse of the subst function. *)
 374 let subst_inv ~equality ~what =
 375    let rec find_image t = function
 376       | []       -> false
 377       | hd :: tl -> equality t hd || find_image t tl
 378    in
 379    let rec subst_term k t =
 380       if find_image t what then C.Rel k else inspect_term k t
 381    and inspect_term k = function
 382       | C.Rel n -> if n < k then C.Rel n else C.Rel (succ n)
 383       | C.Sort _ as t -> t
 384       | C.Implicit _ as t -> t
 385       | C.Var (uri, enss) ->
 386          let enss = List.map (subst_ens k) enss in
 387          C.Var (uri, enss)
 388       | C.Const (uri ,enss) ->
 389          let enss = List.map (subst_ens k) enss in
 390          C.Const (uri, enss)
 391      | C.MutInd (uri, tyno, enss) ->
 392          let enss = List.map (subst_ens k) enss in
 393          C.MutInd (uri, tyno, enss)
 394      | C.MutConstruct (uri, tyno, consno, enss) ->
 395          let enss = List.map (subst_ens k) enss in
 396          C.MutConstruct (uri, tyno, consno, enss)
 397      | C.Meta (i, mss) ->
 398          let mss = List.map (subst_ms k) mss in
 399          C.Meta(i, mss)
 400      | C.Cast (t, v) -> C.Cast (subst_term k t, subst_term k v)
 401      | C.Appl ts ->
 402          let ts = List.map (subst_term k) ts in
 403          C.Appl ts
 404      | C.MutCase (uri, tyno, outty, t, cases) ->
 405          let cases = List.map (subst_term k) cases in
 406          C.MutCase (uri, tyno, subst_term k outty, subst_term k t, cases)
 407      | C.Prod (n, v, t) ->
 408         C.Prod (n, subst_term k v, subst_term (succ k) t)
 409      | C.Lambda (n, v, t) ->
 410         C.Lambda (n, subst_term k v, subst_term (succ k) t)
 411      | C.LetIn (n, v, t) ->
 412         C.LetIn (n, subst_term k v, subst_term (succ k) t)
 413      | C.Fix (i, fixes) ->
 414         let fixesno = List.length fixes in
 415         let fixes = List.map (subst_fix fixesno k) fixes in
 416         C.Fix (i, fixes)
 417      | C.CoFix (i, cofixes) ->
 418         let cofixesno = List.length cofixes in
 419         let cofixes = List.map (subst_cofix cofixesno k) cofixes in
 420          C.CoFix (i, cofixes)
 421    and subst_ens k (uri, t) = uri, subst_term k t
 422    and subst_ms k = function
 423       | None   -> None
 424       | Some t -> Some (subst_term k t)
 425    and subst_fix fixesno k (n, ind, ty, bo) =
 426       n, ind, subst_term k ty, subst_term (k + fixesno) bo
 427    and subst_cofix cofixesno k (n, ty, bo) =
 428       n, subst_term k ty, subst_term (k + cofixesno) bo
 429 in
 430 subst_term
 431
 432
 433
 434
 435 (* Takes a well-typed term and fully reduces it. *)
 436 (*CSC: It does not perform reduction in a Case *)
 437 let reduce context =
 438  let rec reduceaux context l =
 439    function
 440       C.Rel n as t ->
 441        (match List.nth context (n-1) with
 442            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
 443          | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo)
 444          | None -> raise RelToHiddenHypothesis
 445        )
 446     | C.Var (uri,exp_named_subst) ->
 447        let exp_named_subst' =
 448         reduceaux_exp_named_subst context l exp_named_subst
 449        in
 450        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 451          match o with
 452            C.Constant _ -> raise ReferenceToConstant
 453          | C.CurrentProof _ -> raise ReferenceToCurrentProof
 454          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 455          | C.Variable (_,None,_,_,_) ->
 456             let t' = C.Var (uri,exp_named_subst') in
 457              if l = [] then t' else C.Appl (t'::l)
 458          | C.Variable (_,Some body,_,_,_) ->
 459             (reduceaux context l
 460               (CicSubstitution.subst_vars exp_named_subst' body))
 461        )
 462     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
 463     | C.Sort _ as t -> t (* l should be empty *)
 464     | C.Implicit _ as t -> t
 465     | C.Cast (te,ty) ->
 466        C.Cast (reduceaux context l te, reduceaux context l ty)
 467     | C.Prod (name,s,t) ->
 468        assert (l = []) ;
 469        C.Prod (name,
 470         reduceaux context [] s,
 471         reduceaux ((Some (name,C.Decl s))::context) [] t)
 472     | C.Lambda (name,s,t) ->
 473        (match l with
 474            [] ->
 475             C.Lambda (name,
 476              reduceaux context [] s,
 477              reduceaux ((Some (name,C.Decl s))::context) [] t)
 478          | he::tl -> reduceaux context tl (S.subst he t)
 479            (* when name is Anonimous the substitution should be superfluous *)
 480        )
 481     | C.LetIn (n,s,t) ->
 482        reduceaux context l (S.subst (reduceaux context [] s) t)
 483     | C.Appl (he::tl) ->
 484        let tl' = List.map (reduceaux context []) tl in
 485         reduceaux context (tl'@l) he
 486     | C.Appl [] -> raise (Impossible 1)
 487     | C.Const (uri,exp_named_subst) ->
 488        let exp_named_subst' =
 489         reduceaux_exp_named_subst context l exp_named_subst
 490        in
 491         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 492           match o with
 493             C.Constant (_,Some body,_,_,_) ->
 494              (reduceaux context l
 495                (CicSubstitution.subst_vars exp_named_subst' body))
 496           | C.Constant (_,None,_,_,_) ->
 497              let t' = C.Const (uri,exp_named_subst') in
 498               if l = [] then t' else C.Appl (t'::l)
 499           | C.Variable _ -> raise ReferenceToVariable
 500           | C.CurrentProof (_,_,body,_,_,_) ->
 501              (reduceaux context l
 502                (CicSubstitution.subst_vars exp_named_subst' body))
 503           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 504         )
 505     | C.MutInd (uri,i,exp_named_subst) ->
 506        let exp_named_subst' =
 507         reduceaux_exp_named_subst context l exp_named_subst
 508        in
 509         let t' = C.MutInd (uri,i,exp_named_subst') in
 510          if l = [] then t' else C.Appl (t'::l)
 511     | C.MutConstruct (uri,i,j,exp_named_subst) ->
 512        let exp_named_subst' =
 513         reduceaux_exp_named_subst context l exp_named_subst
 514        in
 515         let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
 516          if l = [] then t' else C.Appl (t'::l)
 517     | C.MutCase (mutind,i,outtype,term,pl) ->
 518        let decofix =
 519         function
 520            C.CoFix (i,fl) ->
 521              let (_,_,body) = List.nth fl i in
 522               let body' =
 523                let counter = ref (List.length fl) in
 524                 List.fold_right
 525                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 526                  fl
 527                  body
 528               in
 529                reduceaux context [] body'
 530          | C.Appl (C.CoFix (i,fl) :: tl) ->
 531              let (_,_,body) = List.nth fl i in
 532               let body' =
 533                let counter = ref (List.length fl) in
 534                 List.fold_right
 535                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 536                  fl
 537                  body
 538               in
 539                let tl' = List.map (reduceaux context []) tl in
 540                 reduceaux context tl' body'
 541          | t -> t
 542        in
 543         (match decofix (reduceaux context [] term) with
 544             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
 545           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 546              let (arity, r) =
 547                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
 548                  match o with
 549                      C.InductiveDefinition (tl,_,r,_) ->
 550                        let (_,_,arity,_) = List.nth tl i in
 551                          (arity,r)
 552                    | _ -> raise WrongUriToInductiveDefinition
 553              in
 554               let ts =
 555                let rec eat_first =
 556                 function
 557                    (0,l) -> l
 558                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 559                  | _ -> raise (Impossible 5)
 560                in
 561                 eat_first (r,tl)
 562               in
 563                reduceaux context (ts@l) (List.nth pl (j-1))
 564          | C.Cast _ | C.Implicit _ ->
 565             raise (Impossible 2) (* we don't trust our whd ;-) *)
 566          | _ ->
 567            let outtype' = reduceaux context [] outtype in
 568            let term' = reduceaux context [] term in
 569            let pl' = List.map (reduceaux context []) pl in
 570             let res =
 571              C.MutCase (mutind,i,outtype',term',pl')
 572             in
 573              if l = [] then res else C.Appl (res::l)
 574        )
 575     | C.Fix (i,fl) ->
 576        let tys =
 577         List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
 578        in
 579         let t' () =
 580          let fl' =
 581           List.map
 582            (function (n,recindex,ty,bo) ->
 583              (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 584            ) fl
 585          in
 586           C.Fix (i, fl')
 587         in
 588          let (_,recindex,_,body) = List.nth fl i in
 589           let recparam =
 590            try
 591             Some (List.nth l recindex)
 592            with
 593             _ -> None
 594           in
 595            (match recparam with
 596                Some recparam ->
 597                 (match reduceaux context [] recparam with
 598                     C.MutConstruct _
 599                   | C.Appl ((C.MutConstruct _)::_) ->
 600                      let body' =
 601                       let counter = ref (List.length fl) in
 602                        List.fold_right
 603                         (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 604                         fl
 605                         body
 606                      in
 607                       (* Possible optimization: substituting whd recparam in l*)
 608                       reduceaux context l body'
 609                   | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
 610                 )
 611              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
 612            )
 613     | C.CoFix (i,fl) ->
 614        let tys =
 615         List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
 616        in
 617         let t' =
 618          let fl' =
 619           List.map
 620            (function (n,ty,bo) ->
 621              (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 622            ) fl
 623          in
 624           C.CoFix (i, fl')
 625         in
 626          if l = [] then t' else C.Appl (t'::l)
 627  and reduceaux_exp_named_subst context l =
 628   List.map (function uri,t -> uri,reduceaux context [] t)
 629  in
 630   reduceaux context []
 631 ;;
 632
 633 exception WrongShape;;
 634 exception AlreadySimplified;;
 635
 636 (* Takes a well-typed term and                                               *)
 637 (*  1) Performs beta-iota-zeta reduction until delta reduction is needed     *)
 638 (*  2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted  *)
 639 (*     w.r.t. zero or more variables and if the Fix can be reductaed, than it*)
 640 (*     is reduced, the delta-reduction is succesfull and the whole algorithm *)
 641 (*     is applied again to the new redex; Step 3.1) is applied to the result *)
 642 (*     of the recursive simplification. Otherwise, if the Fix can not be     *)
 643 (*     reduced, than the delta-reductions fails and the delta-redex is       *)
 644 (*     not reduced. Otherwise, if the delta-residual is not the              *)
 645 (*     lambda-abstraction of a Fix, then it performs step 3.2).              *)
 646 (* 3.1) Folds the application of the constant to the arguments that did not  *)
 647 (*     change in every iteration, i.e. to the actual arguments for the       *)
 648 (*     lambda-abstractions that precede the Fix.                             *)
 649 (* 3.2) Computes the head beta-zeta normal form of the term. Then it tries   *)
 650 (*     reductions. If the reduction cannot be performed, it returns the      *)
 651 (*     original term (not the head beta-zeta normal form of the definiendum) *)
 652 (*CSC: It does not perform simplification in a Case *)
 653
 654 let simpl context =
 655  (* a simplified term is active if it can create a redex when used as an *)
 656  (* actual parameter                                                     *)
 657  let rec is_active =
 658   function
 659      C.Lambda _
 660    | C.MutConstruct _
 661    | C.Appl (C.MutConstruct _::_)
 662    | C.CoFix _ -> true
 663    | C.Cast (bo,_) -> is_active bo
 664    | C.LetIn _ -> assert false
 665    | _ -> false
 666  in
 667  (* reduceaux is equal to the reduceaux locally defined inside *)
 668  (* reduce, but for the const case.                            *)
 669  (**** Step 1 ****)
 670  let rec reduceaux context l =
 671    function
 672       C.Rel n as t ->
 673        (* we never perform delta expansion automatically *)
 674        if l = [] then t else C.Appl (t::l)
 675     | C.Var (uri,exp_named_subst) ->
 676        let exp_named_subst' =
 677         reduceaux_exp_named_subst context l exp_named_subst
 678        in
 679         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 680           match o with
 681             C.Constant _ -> raise ReferenceToConstant
 682           | C.CurrentProof _ -> raise ReferenceToCurrentProof
 683           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 684           | C.Variable (_,None,_,_,_) ->
 685             let t' = C.Var (uri,exp_named_subst') in
 686              if l = [] then t' else C.Appl (t'::l)
 687           | C.Variable (_,Some body,_,_,_) ->
 688              reduceaux context l
 689               (CicSubstitution.subst_vars exp_named_subst' body)
 690         )
 691     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
 692     | C.Sort _ as t -> t (* l should be empty *)
 693     | C.Implicit _ as t -> t
 694     | C.Cast (te,ty) ->
 695        C.Cast (reduceaux context l te, reduceaux context [] ty)
 696     | C.Prod (name,s,t) ->
 697        assert (l = []) ;
 698        C.Prod (name,
 699         reduceaux context [] s,
 700         reduceaux ((Some (name,C.Decl s))::context) [] t)
 701     | C.Lambda (name,s,t) ->
 702        (match l with
 703            [] ->
 704             C.Lambda (name,
 705              reduceaux context [] s,
 706              reduceaux ((Some (name,C.Decl s))::context) [] t)
 707          | he::tl -> reduceaux context tl (S.subst he t)
 708            (* when name is Anonimous the substitution should be superfluous *)
 709        )
 710     | C.LetIn (n,s,t) ->
 711        reduceaux context l (S.subst (reduceaux context [] s) t)
 712     | C.Appl (he::tl) ->
 713        let tl' = List.map (reduceaux context []) tl in
 714         reduceaux context (tl'@l) he
 715     | C.Appl [] -> raise (Impossible 1)
 716     | C.Const (uri,exp_named_subst) ->
 717        let exp_named_subst' =
 718         reduceaux_exp_named_subst context l exp_named_subst
 719        in
 720         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 721           match o with
 722            C.Constant (_,Some body,_,_,_) ->
 723             if List.exists is_active l then
 724              try_delta_expansion context l
 725               (C.Const (uri,exp_named_subst'))
 726               (CicSubstitution.subst_vars exp_named_subst' body)
 727             else
 728              let t' = C.Const (uri,exp_named_subst') in
 729               if l = [] then t' else C.Appl (t'::l)
 730          | C.Constant (_,None,_,_,_) ->
 731             let t' = C.Const (uri,exp_named_subst') in
 732              if l = [] then t' else C.Appl (t'::l)
 733          | C.Variable _ -> raise ReferenceToVariable
 734          | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body
 735          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 736        )
 737     | C.MutInd (uri,i,exp_named_subst) ->
 738        let exp_named_subst' =
 739         reduceaux_exp_named_subst context l exp_named_subst
 740        in
 741         let t' = C.MutInd (uri,i,exp_named_subst') in
 742          if l = [] then t' else C.Appl (t'::l)
 743     | C.MutConstruct (uri,i,j,exp_named_subst) ->
 744        let exp_named_subst' =
 745         reduceaux_exp_named_subst context l exp_named_subst
 746        in
 747         let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
 748          if l = [] then t' else C.Appl (t'::l)
 749     | C.MutCase (mutind,i,outtype,term,pl) ->
 750        let decofix =
 751         function
 752            C.CoFix (i,fl) ->
 753              let (_,_,body) = List.nth fl i in
 754               let body' =
 755                let counter = ref (List.length fl) in
 756                 List.fold_right
 757                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 758                  fl
 759                  body
 760               in
 761                reduceaux context [] body'
 762          | C.Appl (C.CoFix (i,fl) :: tl) ->
 763              let (_,_,body) = List.nth fl i in
 764              let body' =
 765               let counter = ref (List.length fl) in
 766                List.fold_right
 767                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 768                 fl
 769                 body
 770              in
 771               let tl' = List.map (reduceaux context []) tl in
 772                reduceaux context tl' body'
 773          | t -> t
 774        in
 775         (match decofix (reduceaux context [] term) (*(CicReduction.whd context term)*) with
 776             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
 777           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 778              let (arity, r) =
 779                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
 780                  match o with
 781                      C.InductiveDefinition (tl,ingredients,r,_) ->
 782                        let (_,_,arity,_) = List.nth tl i in
 783                          (arity,r)
 784                    | _ -> raise WrongUriToInductiveDefinition
 785              in
 786               let ts =
 787                let rec eat_first =
 788                 function
 789                    (0,l) -> l
 790                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 791                  | _ -> raise (Impossible 5)
 792                in
 793                 eat_first (r,tl)
 794               in
 795                reduceaux context (ts@l) (List.nth pl (j-1))
 796          | C.Cast _ | C.Implicit _ ->
 797             raise (Impossible 2) (* we don't trust our whd ;-) *)
 798          | _ ->
 799            let outtype' = reduceaux context [] outtype in
 800            let term' = reduceaux context [] term in
 801            let pl' = List.map (reduceaux context []) pl in
 802             let res =
 803              C.MutCase (mutind,i,outtype',term',pl')
 804             in
 805              if l = [] then res else C.Appl (res::l)
 806        )
 807     | C.Fix (i,fl) ->
 808        let tys =
 809         List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
 810        in
 811         let t' () =
 812          let fl' =
 813           List.map
 814            (function (n,recindex,ty,bo) ->
 815              (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 816            ) fl
 817          in
 818           C.Fix (i, fl')
 819         in
 820          let (_,recindex,_,body) = List.nth fl i in
 821           let recparam =
 822            try
 823             Some (List.nth l recindex)
 824            with
 825             _ -> None
 826           in
 827            (match recparam with
 828                Some recparam ->
 829                 (match reduceaux context [] recparam with
 830                     C.MutConstruct _
 831                   | C.Appl ((C.MutConstruct _)::_) ->
 832                      let body' =
 833                       let counter = ref (List.length fl) in
 834                        List.fold_right
 835                         (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 836                         fl
 837                         body
 838                      in
 839                       (* Possible optimization: substituting whd recparam in l*)
 840                       reduceaux context l body'
 841                   | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
 842                 )
 843              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
 844            )
 845     | C.CoFix (i,fl) ->
 846        let tys =
 847         List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
 848        in
 849         let t' =
 850          let fl' =
 851           List.map
 852            (function (n,ty,bo) ->
 853              (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 854            ) fl
 855          in
 856          C.CoFix (i, fl')
 857        in
 858          if l = [] then t' else C.Appl (t'::l)
 859  and reduceaux_exp_named_subst context l =
 860   List.map (function uri,t -> uri,reduceaux context [] t)
 861  (**** Step 2 ****)
 862  and try_delta_expansion context l term body =
 863    try
 864     let res,constant_args =
 865      let rec aux rev_constant_args l =
 866       function
 867          C.Lambda (name,s,t) ->
 868           begin
 869            match l with
 870               [] -> raise WrongShape
 871             | he::tl ->
 872                (* when name is Anonimous the substitution should *)
 873                (* be superfluous                                 *)
 874                aux (he::rev_constant_args) tl (S.subst he t)
 875           end
 876        | C.LetIn (_,s,t) ->
 877           aux rev_constant_args l (S.subst s t)
 878        | C.Fix (i,fl) ->
 879            let (_,recindex,_,body) = List.nth fl i in
 880             let recparam =
 881              try
 882               List.nth l recindex
 883              with
 884               _ -> raise AlreadySimplified
 885             in
 886              (match reduceaux context [] recparam (*CicReduction.whd context recparam*) with
 887                  C.MutConstruct _
 888                | C.Appl ((C.MutConstruct _)::_) ->
 889                   let body' =
 890                    let counter = ref (List.length fl) in
 891                     List.fold_right
 892                      (function _ ->
 893                        decr counter ; S.subst (C.Fix (!counter,fl))
 894                      ) fl body
 895                   in
 896                    (* Possible optimization: substituting whd *)
 897                    (* recparam in l                           *)
 898                    reduceaux context l body',
 899                     List.rev rev_constant_args
 900                | _ -> raise AlreadySimplified
 901              )
 902        | _ -> raise WrongShape
 903      in
 904       aux [] l body
 905     in
 906      (**** Step 3.1 ****)
 907      let term_to_fold, delta_expanded_term_to_fold =
 908       match constant_args with
 909          [] -> term,body
 910        | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
 911      in
 912       let simplified_term_to_fold =
 913        reduceaux context [] delta_expanded_term_to_fold
 914       in
 915        replace_lifting (=) [simplified_term_to_fold] [term_to_fold] res
 916    with
 917       WrongShape ->
 918        (**** Step 3.2 ****)
 919        let rec aux l =
 920         function
 921            C.Lambda (name,s,t) ->
 922              (match l with
 923                 [] -> raise AlreadySimplified
 924               | he::tl ->
 925                  (* when name is Anonimous the substitution should *)
 926                  (* be superfluous                                 *)
 927                  aux tl (S.subst he t))
 928          | C.LetIn (_,s,t) -> aux l (S.subst s t)
 929          | t ->
 930             let simplified = reduceaux context l t in
 931             let t' = if l = [] then t else C.Appl (t::l) in
 932              if t' = simplified then
 933               raise AlreadySimplified
 934              else
 935               simplified
 936        in
 937         (try aux l body
 938          with
 939           AlreadySimplified ->
 940            if l = [] then term else C.Appl (term::l))
 941     | AlreadySimplified ->
 942        (* If we performed delta-reduction, we would find a Fix   *)
 943        (* not applied to a constructor. So, we refuse to perform *)
 944        (* delta-reduction.                                       *)
 945        if l = [] then term else C.Appl (term::l)
 946  in
 947   reduceaux context []
 948 ;;
 949
 950 let unfold ?what context where =
 951  let contextlen = List.length context in
 952  let first_is_the_expandable_head_of_second context' t1 t2 =
 953   match t1,t2 with
 954      Cic.Const (uri,_), Cic.Const (uri',_)
 955    | Cic.Var (uri,_), Cic.Var (uri',_)
 956    | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_)
 957    | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
 958    | Cic.Const _, _
 959    | Cic.Var _, _ -> false
 960    | Cic.Rel n, Cic.Rel m
 961    | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
 962       n + (List.length context' - contextlen) = m
 963    | Cic.Rel _, _ -> false
 964    | _,_ ->
 965      raise
 966       (ProofEngineTypes.Fail
 967         (lazy "The term to unfold is not a constant, a variable or a bound variable "))
 968  in
 969  let appl he tl =
 970   if tl = [] then he else Cic.Appl (he::tl) in
 971  let cannot_delta_expand t =
 972   raise
 973    (ProofEngineTypes.Fail
 974      (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
 975  let rec hd_delta_beta context tl =
 976   function
 977     Cic.Rel n as t ->
 978      (try
 979        match List.nth context (n-1) with
 980           Some (_,Cic.Decl _) -> cannot_delta_expand t
 981         | Some (_,Cic.Def (bo,_)) ->
 982            CicReduction.head_beta_reduce
 983             (appl (CicSubstitution.lift n bo) tl)
 984         | None -> raise RelToHiddenHypothesis
 985       with
 986          Failure _ -> assert false)
 987   | Cic.Const (uri,exp_named_subst) as t ->
 988      let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 989       (match o with
 990           Cic.Constant (_,Some body,_,_,_) ->
 991            CicReduction.head_beta_reduce
 992             (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
 993         | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t
 994         | Cic.Variable _ -> raise ReferenceToVariable
 995         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
 996         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 997       )
 998   | Cic.Var (uri,exp_named_subst) as t ->
 999      let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1000       (match o with
1001           Cic.Constant _ -> raise ReferenceToConstant
1002         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
1003         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
1004         | Cic.Variable (_,Some body,_,_,_) ->
1005            CicReduction.head_beta_reduce
1006             (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
1007         | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t
1008       )
1009    | Cic.Appl [] -> assert false
1010    | Cic.Appl (he::tl) -> hd_delta_beta context tl he
1011    | t -> cannot_delta_expand t
1012  in
1013  let context_and_matched_term_list =
1014   match what with
1015      None -> [context, where]
1016    | Some what ->
1017       let res =
1018        ProofEngineHelpers.locate_in_term
1019         ~equality:first_is_the_expandable_head_of_second
1020         what ~where context
1021       in
1022        if res = [] then
1023         raise
1024          (ProofEngineTypes.Fail
1025            (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
1026        else
1027         res
1028  in
1029   let reduced_terms =
1030    List.map
1031     (function (context,where) -> hd_delta_beta context [] where)
1032     context_and_matched_term_list in
1033   let whats = List.map snd context_and_matched_term_list in
1034    replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where
1035 ;;