helm/gTopLevel/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
  37 (* The code of this module is derived from the code of CicReduction *)
  38
  39 exception Impossible of int;;
  40 exception ReferenceToConstant;;
  41 exception ReferenceToVariable;;
  42 exception ReferenceToCurrentProof;;
  43 exception ReferenceToInductiveDefinition;;
  44 exception WrongUriToInductiveDefinition;;
  45 exception RelToHiddenHypothesis;;
  46
  47 let alpha_equivalence =
  48  let module C = Cic in
  49   let rec aux t t' =
  50    if t = t' then true
  51    else
  52     match t,t' with
  53        C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) ->
  54         UriManager.eq uri1 uri2 &&
  55          aux_exp_named_subst exp_named_subst1 exp_named_subst2
  56      | C.Cast (te,ty), C.Cast (te',ty') ->
  57         aux te te' && aux ty ty'
  58      | C.Prod (_,s,t), C.Prod (_,s',t') ->
  59         aux s s' && aux t t'
  60      | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
  61         aux s s' && aux t t'
  62      | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
  63         aux s s' && aux t t'
  64      | C.Appl l, C.Appl l' ->
  65         (try
  66           List.fold_left2
  67            (fun b t1 t2 -> b && aux t1 t2) true l l'
  68          with
  69           Invalid_argument _ -> false)
  70      | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) ->
  71         UriManager.eq uri uri' &&
  72          aux_exp_named_subst exp_named_subst1 exp_named_subst2
  73      | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) ->
  74         UriManager.eq uri uri' && i = i' &&
  75          aux_exp_named_subst exp_named_subst1 exp_named_subst2
  76      | C.MutConstruct (uri,i,j,exp_named_subst1),
  77        C.MutConstruct (uri',i',j',exp_named_subst2) ->
  78         UriManager.eq uri uri' && i = i' && j = j' &&
  79          aux_exp_named_subst exp_named_subst1 exp_named_subst2
  80      | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
  81         UriManager.eq sp sp' && i = i' &&
  82          aux outt outt' && aux t t' &&
  83           (try
  84             List.fold_left2
  85              (fun b t1 t2 -> b && aux t1 t2) true pl pl'
  86            with
  87             Invalid_argument _ -> false)
  88      | C.Fix (i,fl), C.Fix (i',fl') ->
  89         i = i' &&
  90         (try
  91           List.fold_left2
  92            (fun b (_,i,ty,bo) (_,i',ty',bo') ->
  93              b && i = i' && aux ty ty' && aux bo bo'
  94            ) true fl fl'
  95          with
  96           Invalid_argument _ -> false)
  97      | C.CoFix (i,fl), C.CoFix (i',fl') ->
  98         i = i' &&
  99         (try
 100           List.fold_left2
 101            (fun b (_,ty,bo) (_,ty',bo') ->
 102              b && aux ty ty' && aux bo bo'
 103            ) true fl fl'
 104          with
 105           Invalid_argument _ -> false)
 106      | _,_ -> false (* we already know that t != t' *)
 107   and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
 108    try
 109      List.fold_left2
 110       (fun b (uri1,t1) (uri2,t2) ->
 111         b && UriManager.eq uri1 uri2 && aux t1 t2
 112       ) true exp_named_subst1 exp_named_subst2
 113     with
 114      Invalid_argument _ -> false
 115   in
 116    aux
 117 ;;
 118
 119 (* "textual" replacement of a subterm with another one *)
 120 let replace ~equality ~what ~with_what ~where =
 121  let module C = Cic in
 122   let rec aux =
 123    function
 124       t when (equality t what) -> with_what
 125     | C.Rel _ as t -> t
 126     | C.Var (uri,exp_named_subst) ->
 127        C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
 128     | C.Meta _ as t -> t
 129     | C.Sort _ as t -> t
 130     | C.Implicit as t -> t
 131     | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
 132     | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
 133     | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
 134     | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
 135     | C.Appl l ->
 136        (* Invariant enforced: no application of an application *)
 137        (match List.map aux l with
 138            (C.Appl l')::tl -> C.Appl (l'@tl)
 139          | l' -> C.Appl l')
 140     | C.Const (uri,exp_named_subst) ->
 141        C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
 142     | C.MutInd (uri,i,exp_named_subst) ->
 143        C.MutInd
 144         (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
 145     | C.MutConstruct (uri,i,j,exp_named_subst) ->
 146        C.MutConstruct
 147         (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
 148     | C.MutCase (sp,i,outt,t,pl) ->
 149        C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
 150     | C.Fix (i,fl) ->
 151        let substitutedfl =
 152         List.map
 153          (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
 154           fl
 155        in
 156         C.Fix (i, substitutedfl)
 157     | C.CoFix (i,fl) ->
 158        let substitutedfl =
 159         List.map
 160          (fun (name,ty,bo) -> (name, aux ty, aux bo))
 161           fl
 162        in
 163         C.CoFix (i, substitutedfl)
 164   in
 165    aux where
 166 ;;
 167
 168 (* replaces in a term a term with another one. *)
 169 (* Lifting are performed as usual.             *)
 170 let replace_lifting ~equality ~what ~with_what ~where =
 171  let rec substaux k what =
 172   let module C = Cic in
 173   let module S = CicSubstitution in
 174    function
 175       t when (equality t what) -> S.lift (k-1) with_what
 176     | C.Rel n as t -> t
 177     | C.Var (uri,exp_named_subst) ->
 178        let exp_named_subst' =
 179         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
 180        in
 181         C.Var (uri,exp_named_subst')
 182     | C.Meta (i, l) as t ->
 183        let l' =
 184         List.map
 185          (function
 186              None -> None
 187            | Some t -> Some (substaux k what t)
 188          ) l
 189        in
 190         C.Meta(i,l')
 191     | C.Sort _ as t -> t
 192     | C.Implicit as t -> t
 193     | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
 194     | C.Prod (n,s,t) ->
 195        C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
 196     | C.Lambda (n,s,t) ->
 197        C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
 198     | C.LetIn (n,s,t) ->
 199        C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
 200     | C.Appl (he::tl) ->
 201        (* Invariant: no Appl applied to another Appl *)
 202        let tl' = List.map (substaux k what) tl in
 203         begin
 204          match substaux k what he with
 205             C.Appl l -> C.Appl (l@tl')
 206           | _ as he' -> C.Appl (he'::tl')
 207         end
 208     | C.Appl _ -> assert false
 209     | C.Const (uri,exp_named_subst) ->
 210        let exp_named_subst' =
 211         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
 212        in
 213        C.Const (uri,exp_named_subst')
 214     | C.MutInd (uri,i,exp_named_subst) ->
 215        let exp_named_subst' =
 216         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
 217        in
 218         C.MutInd (uri,i,exp_named_subst')
 219     | C.MutConstruct (uri,i,j,exp_named_subst) ->
 220        let exp_named_subst' =
 221         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
 222        in
 223         C.MutConstruct (uri,i,j,exp_named_subst')
 224     | C.MutCase (sp,i,outt,t,pl) ->
 225        C.MutCase (sp,i,substaux k what outt, substaux k what t,
 226         List.map (substaux k what) pl)
 227     | C.Fix (i,fl) ->
 228        let len = List.length fl in
 229        let substitutedfl =
 230         List.map
 231          (fun (name,i,ty,bo) ->
 232            (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo))
 233           fl
 234        in
 235         C.Fix (i, substitutedfl)
 236     | C.CoFix (i,fl) ->
 237        let len = List.length fl in
 238        let substitutedfl =
 239         List.map
 240          (fun (name,ty,bo) ->
 241            (name, substaux k what ty, substaux (k+len) (S.lift len what) bo))
 242           fl
 243        in
 244         C.CoFix (i, substitutedfl)
 245  in
 246   substaux 1 what where
 247 ;;
 248
 249 (* Takes a well-typed term and fully reduces it. *)
 250 (*CSC: It does not perform reduction in a Case *)
 251 let reduce context =
 252  let rec reduceaux context l =
 253   let module C = Cic in
 254   let module S = CicSubstitution in
 255    function
 256       C.Rel n as t ->
 257        (match List.nth context (n-1) with
 258            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
 259          | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
 260          | None -> raise RelToHiddenHypothesis
 261        )
 262     | C.Var (uri,exp_named_subst) ->
 263        let exp_named_subst' =
 264         reduceaux_exp_named_subst context l exp_named_subst
 265        in
 266        (match CicEnvironment.get_obj uri with
 267            C.Constant _ -> raise ReferenceToConstant
 268          | C.CurrentProof _ -> raise ReferenceToCurrentProof
 269          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 270          | C.Variable (_,None,_,_) ->
 271             let t' = C.Var (uri,exp_named_subst') in
 272              if l = [] then t' else C.Appl (t'::l)
 273          | C.Variable (_,Some body,_,_) ->
 274             (reduceaux context l
 275               (CicSubstitution.subst_vars exp_named_subst' body))
 276        )
 277     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
 278     | C.Sort _ as t -> t (* l should be empty *)
 279     | C.Implicit as t -> t
 280     | C.Cast (te,ty) ->
 281        C.Cast (reduceaux context l te, reduceaux context l ty)
 282     | C.Prod (name,s,t) ->
 283        assert (l = []) ;
 284        C.Prod (name,
 285         reduceaux context [] s,
 286         reduceaux ((Some (name,C.Decl s))::context) [] t)
 287     | C.Lambda (name,s,t) ->
 288        (match l with
 289            [] ->
 290             C.Lambda (name,
 291              reduceaux context [] s,
 292              reduceaux ((Some (name,C.Decl s))::context) [] t)
 293          | he::tl -> reduceaux context tl (S.subst he t)
 294            (* when name is Anonimous the substitution should be superfluous *)
 295        )
 296     | C.LetIn (n,s,t) ->
 297        reduceaux context l (S.subst (reduceaux context [] s) t)
 298     | C.Appl (he::tl) ->
 299        let tl' = List.map (reduceaux context []) tl in
 300         reduceaux context (tl'@l) he
 301     | C.Appl [] -> raise (Impossible 1)
 302     | C.Const (uri,exp_named_subst) ->
 303        let exp_named_subst' =
 304         reduceaux_exp_named_subst context l exp_named_subst
 305        in
 306         (match CicEnvironment.get_obj uri with
 307             C.Constant (_,Some body,_,_) ->
 308              (reduceaux context l
 309                (CicSubstitution.subst_vars exp_named_subst' body))
 310           | C.Constant (_,None,_,_) ->
 311              let t' = C.Const (uri,exp_named_subst') in
 312               if l = [] then t' else C.Appl (t'::l)
 313           | C.Variable _ -> raise ReferenceToVariable
 314           | C.CurrentProof (_,_,body,_,_) ->
 315              (reduceaux context l
 316                (CicSubstitution.subst_vars exp_named_subst' body))
 317           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 318         )
 319     | C.MutInd (uri,i,exp_named_subst) ->
 320        let exp_named_subst' =
 321         reduceaux_exp_named_subst context l exp_named_subst
 322        in
 323         let t' = C.MutInd (uri,i,exp_named_subst') in
 324          if l = [] then t' else C.Appl (t'::l)
 325     | C.MutConstruct (uri,i,j,exp_named_subst) as t ->
 326        let exp_named_subst' =
 327         reduceaux_exp_named_subst context l exp_named_subst
 328        in
 329         let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
 330          if l = [] then t' else C.Appl (t'::l)
 331     | C.MutCase (mutind,i,outtype,term,pl) ->
 332        let decofix =
 333         function
 334            C.CoFix (i,fl) as t ->
 335             let tys =
 336              List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
 337             in
 338              let (_,_,body) = List.nth fl i in
 339               let body' =
 340                let counter = ref (List.length fl) in
 341                 List.fold_right
 342                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 343                  fl
 344                  body
 345               in
 346                reduceaux (tys@context) [] body'
 347          | C.Appl (C.CoFix (i,fl) :: tl) ->
 348             let tys =
 349              List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
 350             in
 351              let (_,_,body) = List.nth fl i in
 352               let body' =
 353                let counter = ref (List.length fl) in
 354                 List.fold_right
 355                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 356                  fl
 357                  body
 358               in
 359                let tl' = List.map (reduceaux context []) tl in
 360                 reduceaux (tys@context) tl' body'
 361          | t -> t
 362        in
 363         (match decofix (reduceaux context [] term) with
 364             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
 365           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 366              let (arity, r) =
 367               match CicEnvironment.get_obj mutind with
 368                  C.InductiveDefinition (tl,_,r) ->
 369                    let (_,_,arity,_) = List.nth tl i in
 370                     (arity,r)
 371                | _ -> raise WrongUriToInductiveDefinition
 372              in
 373               let ts =
 374                let rec eat_first =
 375                 function
 376                    (0,l) -> l
 377                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 378                  | _ -> raise (Impossible 5)
 379                in
 380                 eat_first (r,tl)
 381               in
 382                reduceaux context (ts@l) (List.nth pl (j-1))
 383          | C.Cast _ | C.Implicit ->
 384             raise (Impossible 2) (* we don't trust our whd ;-) *)
 385          | _ ->
 386            let outtype' = reduceaux context [] outtype in
 387            let term' = reduceaux context [] term in
 388            let pl' = List.map (reduceaux context []) pl in
 389             let res =
 390              C.MutCase (mutind,i,outtype',term',pl')
 391             in
 392              if l = [] then res else C.Appl (res::l)
 393        )
 394     | C.Fix (i,fl) ->
 395        let tys =
 396         List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
 397        in
 398         let t' () =
 399          let fl' =
 400           List.map
 401            (function (n,recindex,ty,bo) ->
 402              (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 403            ) fl
 404          in
 405           C.Fix (i, fl')
 406         in
 407          let (_,recindex,_,body) = List.nth fl i in
 408           let recparam =
 409            try
 410             Some (List.nth l recindex)
 411            with
 412             _ -> None
 413           in
 414            (match recparam with
 415                Some recparam ->
 416                 (match reduceaux context [] recparam with
 417                     C.MutConstruct _
 418                   | C.Appl ((C.MutConstruct _)::_) ->
 419                      let body' =
 420                       let counter = ref (List.length fl) in
 421                        List.fold_right
 422                         (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 423                         fl
 424                         body
 425                      in
 426                       (* Possible optimization: substituting whd recparam in l*)
 427                       reduceaux context l body'
 428                   | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
 429                 )
 430              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
 431            )
 432     | C.CoFix (i,fl) ->
 433        let tys =
 434         List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
 435        in
 436         let t' =
 437          let fl' =
 438           List.map
 439            (function (n,ty,bo) ->
 440              (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 441            ) fl
 442          in
 443           C.CoFix (i, fl')
 444         in
 445          if l = [] then t' else C.Appl (t'::l)
 446  and reduceaux_exp_named_subst context l =
 447   List.map (function uri,t -> uri,reduceaux context [] t)
 448  in
 449   reduceaux context []
 450 ;;
 451
 452 exception WrongShape;;
 453 exception AlreadySimplified;;
 454
 455 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
 456 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where       *)
 457 (*CSC:  Fix foo                                                      *)
 458 (*CSC:   {foo [n,m:nat]:nat :=                                       *)
 459 (*CSC:     Cases m of O => n | (S p) => (foo (S O) p) end            *)
 460 (*CSC:   }                                                           *)
 461 (* Takes a well-typed term and                                               *)
 462 (*  1) Performs beta-iota-zeta reduction until delta reduction is needed     *)
 463 (*  2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted  *)
 464 (*     w.r.t. zero or more variables and if the Fix can be reduced, than it  *)
 465 (*     is reduced, the delta-reduction is succesfull and the whole algorithm *)
 466 (*     is applied again to the new redex; Step 3) is applied to the result   *)
 467 (*     of the recursive simplification. Otherwise, if the Fix can not be     *)
 468 (*     reduced, than the delta-reductions fails and the delta-redex is       *)
 469 (*     not reduced. Otherwise, if the delta-residual is not the              *)
 470 (*     lambda-abstraction of a Fix, then it is reduced and the result is     *)
 471 (*     directly returned, without performing step 3).                        *)
 472 (*  3) Folds the application of the constant to the arguments that did not   *)
 473 (*     change in every iteration, i.e. to the actual arguments for the       *)
 474 (*     lambda-abstractions that precede the Fix.                             *)
 475 (*CSC: It does not perform simplification in a Case *)
 476 let simpl context =
 477  (* reduceaux is equal to the reduceaux locally defined inside *)
 478  (*reduce, but for the const case.                             *)
 479  (**** Step 1 ****)
 480  let rec reduceaux context l =
 481   let module C = Cic in
 482   let module S = CicSubstitution in
 483    function
 484       C.Rel n as t ->
 485        (match List.nth context (n-1) with
 486            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
 487          | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
 488          | None -> raise RelToHiddenHypothesis
 489        )
 490     | C.Var (uri,exp_named_subst) ->
 491        let exp_named_subst' =
 492         reduceaux_exp_named_subst context l exp_named_subst
 493        in
 494         (match CicEnvironment.get_obj uri with
 495             C.Constant _ -> raise ReferenceToConstant
 496           | C.CurrentProof _ -> raise ReferenceToCurrentProof
 497           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 498           | C.Variable (_,None,_,_) ->
 499             let t' = C.Var (uri,exp_named_subst') in
 500              if l = [] then t' else C.Appl (t'::l)
 501           | C.Variable (_,Some body,_,_) ->
 502              reduceaux context l
 503               (CicSubstitution.subst_vars exp_named_subst' body)
 504         )
 505     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
 506     | C.Sort _ as t -> t (* l should be empty *)
 507     | C.Implicit as t -> t
 508     | C.Cast (te,ty) ->
 509        C.Cast (reduceaux context l te, reduceaux context l ty)
 510     | C.Prod (name,s,t) ->
 511        assert (l = []) ;
 512        C.Prod (name,
 513         reduceaux context [] s,
 514         reduceaux ((Some (name,C.Decl s))::context) [] t)
 515     | C.Lambda (name,s,t) ->
 516        (match l with
 517            [] ->
 518             C.Lambda (name,
 519              reduceaux context [] s,
 520              reduceaux ((Some (name,C.Decl s))::context) [] t)
 521          | he::tl -> reduceaux context tl (S.subst he t)
 522            (* when name is Anonimous the substitution should be superfluous *)
 523        )
 524     | C.LetIn (n,s,t) ->
 525        reduceaux context l (S.subst (reduceaux context [] s) t)
 526     | C.Appl (he::tl) ->
 527        let tl' = List.map (reduceaux context []) tl in
 528         reduceaux context (tl'@l) he
 529     | C.Appl [] -> raise (Impossible 1)
 530     | C.Const (uri,exp_named_subst) ->
 531        let exp_named_subst' =
 532         reduceaux_exp_named_subst context l exp_named_subst
 533        in
 534         (match CicEnvironment.get_obj uri with
 535             C.Constant (_,Some body,_,_) ->
 536              begin
 537               try
 538                (**** Step 2 ****)
 539                let res,constant_args =
 540                 let rec aux rev_constant_args l =
 541                  function
 542                     C.Lambda (name,s,t) as t' ->
 543                      begin
 544                       match l with
 545                          [] -> raise WrongShape
 546                        | he::tl ->
 547                           (* when name is Anonimous the substitution should *)
 548                           (* be superfluous                                 *)
 549                           aux (he::rev_constant_args) tl (S.subst he t)
 550                      end
 551                   | C.LetIn (_,s,t) ->
 552                      aux rev_constant_args l (S.subst s t)
 553                   | C.Fix (i,fl) as t ->
 554                      let tys =
 555                       List.map (function (name,_,ty,_) ->
 556                        Some (C.Name name, C.Decl ty)) fl
 557                      in
 558                       let (_,recindex,_,body) = List.nth fl i in
 559                        let recparam =
 560                         try
 561                          List.nth l recindex
 562                         with
 563                          _ -> raise AlreadySimplified
 564                        in
 565                         (match CicReduction.whd context recparam with
 566                             C.MutConstruct _
 567                           | C.Appl ((C.MutConstruct _)::_) ->
 568                              let body' =
 569                               let counter = ref (List.length fl) in
 570                                List.fold_right
 571                                 (function _ ->
 572                                   decr counter ; S.subst (C.Fix (!counter,fl))
 573                                 ) fl body
 574                              in
 575                               (* Possible optimization: substituting whd *)
 576                               (* recparam in l                           *)
 577                               reduceaux (tys@context) l body',
 578                                List.rev rev_constant_args
 579                           | _ -> raise AlreadySimplified
 580                         )
 581                   | _ -> raise WrongShape
 582                 in
 583                  aux [] l (CicSubstitution.subst_vars exp_named_subst' body)
 584                in
 585                 (**** Step 3 ****)
 586                 let term_to_fold =
 587                  match constant_args with
 588                     [] -> C.Const (uri,exp_named_subst')
 589                   | _ -> C.Appl ((C.Const(uri,exp_named_subst'))::constant_args)
 590                 in
 591                  let reduced_term_to_fold = reduce context term_to_fold in
 592                   replace (=) reduced_term_to_fold term_to_fold res
 593               with
 594                  WrongShape ->
 595                   (* The constant does not unfold to a Fix lambda-abstracted  *)
 596                   (* w.r.t. zero or more variables. We just perform reduction.*)
 597                   reduceaux context l
 598                    (CicSubstitution.subst_vars exp_named_subst' body)
 599                | AlreadySimplified ->
 600                   (* If we performed delta-reduction, we would find a Fix   *)
 601                   (* not applied to a constructor. So, we refuse to perform *)
 602                   (* delta-reduction.                                       *)
 603                   let t' = C.Const (uri,exp_named_subst') in
 604                    if l = [] then t' else C.Appl (t'::l)
 605              end
 606          | C.Constant (_,None,_,_) ->
 607             let t' = C.Const (uri,exp_named_subst') in
 608              if l = [] then t' else C.Appl (t'::l)
 609          | C.Variable _ -> raise ReferenceToVariable
 610          | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
 611          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 612        )
 613     | C.MutInd (uri,i,exp_named_subst) ->
 614        let exp_named_subst' =
 615         reduceaux_exp_named_subst context l exp_named_subst
 616        in
 617         let t' = C.MutInd (uri,i,exp_named_subst') in
 618          if l = [] then t' else C.Appl (t'::l)
 619     | C.MutConstruct (uri,i,j,exp_named_subst) ->
 620        let exp_named_subst' =
 621         reduceaux_exp_named_subst context l exp_named_subst
 622        in
 623         let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
 624          if l = [] then t' else C.Appl (t'::l)
 625     | C.MutCase (mutind,i,outtype,term,pl) ->
 626        let decofix =
 627         function
 628            C.CoFix (i,fl) as t ->
 629             let tys =
 630              List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl            in
 631              let (_,_,body) = List.nth fl i in
 632               let body' =
 633                let counter = ref (List.length fl) in
 634                 List.fold_right
 635                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 636                  fl
 637                  body
 638               in
 639                reduceaux (tys@context) [] body'
 640          | C.Appl (C.CoFix (i,fl) :: tl) ->
 641             let tys =
 642              List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl            in
 643              let (_,_,body) = List.nth fl i in
 644               let body' =
 645                let counter = ref (List.length fl) in
 646                 List.fold_right
 647                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 648                  fl
 649                  body
 650               in
 651                let tl' = List.map (reduceaux context []) tl in
 652                 reduceaux (tys@context) tl body'
 653          | t -> t
 654        in
 655         (match decofix (reduceaux context [] term) with
 656             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
 657           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 658              let (arity, r) =
 659               match CicEnvironment.get_obj mutind with
 660                  C.InductiveDefinition (tl,ingredients,r) ->
 661                    let (_,_,arity,_) = List.nth tl i in
 662                     (arity,r)
 663                | _ -> raise WrongUriToInductiveDefinition
 664              in
 665               let ts =
 666                let rec eat_first =
 667                 function
 668                    (0,l) -> l
 669                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 670                  | _ -> raise (Impossible 5)
 671                in
 672                 eat_first (r,tl)
 673               in
 674                reduceaux context (ts@l) (List.nth pl (j-1))
 675          | C.Cast _ | C.Implicit ->
 676             raise (Impossible 2) (* we don't trust our whd ;-) *)
 677          | _ ->
 678            let outtype' = reduceaux context [] outtype in
 679            let term' = reduceaux context [] term in
 680            let pl' = List.map (reduceaux context []) pl in
 681             let res =
 682              C.MutCase (mutind,i,outtype',term',pl')
 683             in
 684              if l = [] then res else C.Appl (res::l)
 685        )
 686     | C.Fix (i,fl) ->
 687        let tys =
 688         List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
 689        in
 690         let t' () =
 691          let fl' =
 692           List.map
 693            (function (n,recindex,ty,bo) ->
 694              (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 695            ) fl
 696          in
 697           C.Fix (i, fl')
 698         in
 699          let (_,recindex,_,body) = List.nth fl i in
 700           let recparam =
 701            try
 702             Some (List.nth l recindex)
 703            with
 704             _ -> None
 705           in
 706            (match recparam with
 707                Some recparam ->
 708                 (match reduceaux context [] recparam with
 709                     C.MutConstruct _
 710                   | C.Appl ((C.MutConstruct _)::_) ->
 711                      let body' =
 712                       let counter = ref (List.length fl) in
 713                        List.fold_right
 714                         (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 715                         fl
 716                         body
 717                      in
 718                       (* Possible optimization: substituting whd recparam in l*)
 719                       reduceaux context l body'
 720                   | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
 721                 )
 722              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
 723            )
 724     | C.CoFix (i,fl) ->
 725        let tys =
 726         List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
 727        in
 728         let t' =
 729          let fl' =
 730           List.map
 731            (function (n,ty,bo) ->
 732              (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 733            ) fl
 734          in
 735          C.CoFix (i, fl')
 736        in
 737          if l = [] then t' else C.Appl (t'::l)
 738  and reduceaux_exp_named_subst context l =
 739   List.map (function uri,t -> uri,reduceaux context [] t)
 740  in
 741   reduceaux context []
 742 ;;