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