helm/software/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 debug = false
  53 let prerr_endline =
  54   if debug then prerr_endline else (fun x -> ())
  55 ;;
  56
  57 exception WhatAndWithWhatDoNotHaveTheSameLength;;
  58
  59 (* Replaces "textually" in "where" every term in "what" with the corresponding
  60    term in "with_what". The terms in "what" ARE NOT lifted when binders are
  61    crossed. The terms in "with_what" ARE NOT lifted when binders are crossed.
  62    Every free variable in "where" IS NOT lifted by nnn.
  63 *)
  64 let replace ~equality ~what ~with_what ~where =
  65   let find_image t =
  66    let rec find_image_aux =
  67     function
  68        [],[] -> raise Not_found
  69      | what::tl1,with_what::tl2 ->
  70         if equality what t then with_what else find_image_aux (tl1,tl2)
  71      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
  72    in
  73     find_image_aux (what,with_what)
  74   in
  75   let rec aux t =
  76    try
  77     find_image t
  78    with Not_found ->
  79     match t with
  80        C.Rel _ -> t
  81      | C.Var (uri,exp_named_subst) ->
  82         C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
  83      | C.Meta _ -> t
  84      | C.Sort _ -> t
  85      | C.Implicit _ as t -> t
  86      | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
  87      | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
  88      | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
  89      | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux s, aux ty, aux t)
  90      | C.Appl l ->
  91         (* Invariant enforced: no application of an application *)
  92         (match List.map aux l with
  93             (C.Appl l')::tl -> C.Appl (l'@tl)
  94           | l' -> C.Appl l')
  95      | C.Const (uri,exp_named_subst) ->
  96         C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
  97      | C.MutInd (uri,i,exp_named_subst) ->
  98         C.MutInd
  99          (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
 100      | C.MutConstruct (uri,i,j,exp_named_subst) ->
 101         C.MutConstruct
 102          (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
 103      | C.MutCase (sp,i,outt,t,pl) ->
 104         C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
 105      | C.Fix (i,fl) ->
 106         let substitutedfl =
 107          List.map
 108           (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
 109            fl
 110         in
 111          C.Fix (i, substitutedfl)
 112      | C.CoFix (i,fl) ->
 113         let substitutedfl =
 114          List.map
 115           (fun (name,ty,bo) -> (name, aux ty, aux bo))
 116            fl
 117         in
 118          C.CoFix (i, substitutedfl)
 119    in
 120     aux where
 121 ;;
 122
 123 (* Replaces in "where" every term in "what" with the corresponding
 124    term in "with_what". The terms in "what" ARE lifted when binders are
 125    crossed. The terms in "with_what" ARE lifted when binders are crossed.
 126    Every free variable in "where" IS NOT lifted by nnn.
 127    Thus "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" is the
 128    inverse of subst up to the fact that free variables in "where" are NOT
 129    lifted.  *)
 130 let replace_lifting ~equality ~context ~what ~with_what ~where =
 131   let find_image ctx what t =
 132    let rec find_image_aux =
 133     function
 134        [],[] -> raise Not_found
 135      | what::tl1,with_what::tl2 ->
 136         if equality ctx 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 add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
 142   let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in
 143   let rec substaux k ctx what t =
 144    try
 145     S.lift (k-1) (find_image ctx what t)
 146    with Not_found ->
 147     match t with
 148       C.Rel n as t -> t
 149     | C.Var (uri,exp_named_subst) ->
 150        let exp_named_subst' =
 151         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
 152        in
 153         C.Var (uri,exp_named_subst')
 154     | C.Meta (i, l) ->
 155        let l' =
 156         List.map
 157          (function
 158              None -> None
 159            | Some t -> Some (substaux k ctx what t)
 160          ) l
 161        in
 162         C.Meta(i,l')
 163     | C.Sort _ as t -> t
 164     | C.Implicit _ as t -> t
 165     | C.Cast (te,ty) -> C.Cast (substaux k ctx what te, substaux k ctx what ty)
 166     | C.Prod (n,s,t) ->
 167        C.Prod
 168         (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
 169     | C.Lambda (n,s,t) ->
 170        C.Lambda
 171         (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
 172     | C.LetIn (n,s,ty,t) ->
 173        C.LetIn
 174         (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t)
 175     | C.Appl (he::tl) ->
 176        (* Invariant: no Appl applied to another Appl *)
 177        let tl' = List.map (substaux k ctx what) tl in
 178         begin
 179          match substaux k ctx what he with
 180             C.Appl l -> C.Appl (l@tl')
 181           | _ as he' -> C.Appl (he'::tl')
 182         end
 183     | C.Appl _ -> assert false
 184     | C.Const (uri,exp_named_subst) ->
 185        let exp_named_subst' =
 186         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
 187        in
 188        C.Const (uri,exp_named_subst')
 189     | C.MutInd (uri,i,exp_named_subst) ->
 190        let exp_named_subst' =
 191         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
 192        in
 193         C.MutInd (uri,i,exp_named_subst')
 194     | C.MutConstruct (uri,i,j,exp_named_subst) ->
 195        let exp_named_subst' =
 196         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
 197        in
 198         C.MutConstruct (uri,i,j,exp_named_subst')
 199     | C.MutCase (sp,i,outt,t,pl) ->
 200        C.MutCase (sp,i,substaux k ctx what outt, substaux k ctx what t,
 201         List.map (substaux k ctx what) pl)
 202     | C.Fix (i,fl) ->
 203        let len = List.length fl in
 204        let substitutedfl =
 205         List.map
 206          (fun (name,i,ty,bo) -> (* WRONG CTX *)
 207            (name, i, substaux k ctx what ty,
 208              substaux (k+len) ctx (List.map (S.lift len) what) bo)
 209          ) fl
 210        in
 211         C.Fix (i, substitutedfl)
 212     | C.CoFix (i,fl) ->
 213        let len = List.length fl in
 214        let substitutedfl =
 215         List.map
 216          (fun (name,ty,bo) -> (* WRONG CTX *)
 217            (name, substaux k ctx what ty,
 218              substaux (k+len) ctx (List.map (S.lift len) what) bo)
 219          ) fl
 220        in
 221         C.CoFix (i, substitutedfl)
 222  in
 223   substaux 1 context what where
 224 ;;
 225
 226 (* Replaces in "where" every term in "what" with the corresponding
 227    term in "with_what". The terms in "what" ARE NOT lifted when binders are
 228    crossed. The terms in "with_what" ARE lifted when binders are crossed.
 229    Every free variable in "where" IS lifted by nnn.
 230    Thus "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" is the
 231    inverse of subst up to the fact that "what" terms are NOT lifted. *)
 232 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
 233   let find_image t =
 234    let rec find_image_aux =
 235     function
 236        [],[] -> raise Not_found
 237      | what::tl1,with_what::tl2 ->
 238          if equality what t then with_what else find_image_aux (tl1,tl2)
 239      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
 240    in
 241     find_image_aux (what,with_what)
 242   in
 243   let rec substaux k t =
 244    try
 245     S.lift (k-1) (find_image t)
 246    with Not_found ->
 247     match t with
 248        C.Rel n ->
 249         if n < k then C.Rel n else C.Rel (n + nnn)
 250      | C.Var (uri,exp_named_subst) ->
 251         let exp_named_subst' =
 252          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
 253         in
 254          C.Var (uri,exp_named_subst')
 255      | C.Meta (i, l) ->
 256         let l' =
 257          List.map
 258           (function
 259               None -> None
 260             | Some t -> Some (substaux k t)
 261           ) l
 262         in
 263          C.Meta(i,l')
 264      | C.Sort _ as t -> t
 265      | C.Implicit _ as t -> t
 266      | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
 267      | C.Prod (n,s,t) ->
 268         C.Prod (n, substaux k s, substaux (k + 1) t)
 269      | C.Lambda (n,s,t) ->
 270         C.Lambda (n, substaux k s, substaux (k + 1) t)
 271      | C.LetIn (n,s,ty,t) ->
 272         C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
 273      | C.Appl (he::tl) ->
 274         (* Invariant: no Appl applied to another Appl *)
 275         let tl' = List.map (substaux k) tl in
 276          begin
 277           match substaux k he with
 278              C.Appl l -> C.Appl (l@tl')
 279            | _ as he' -> C.Appl (he'::tl')
 280          end
 281      | C.Appl _ -> assert false
 282      | C.Const (uri,exp_named_subst) ->
 283         let exp_named_subst' =
 284          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
 285         in
 286         C.Const (uri,exp_named_subst')
 287      | C.MutInd (uri,i,exp_named_subst) ->
 288         let exp_named_subst' =
 289          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
 290         in
 291          C.MutInd (uri,i,exp_named_subst')
 292      | C.MutConstruct (uri,i,j,exp_named_subst) ->
 293         let exp_named_subst' =
 294          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
 295         in
 296          C.MutConstruct (uri,i,j,exp_named_subst')
 297      | C.MutCase (sp,i,outt,t,pl) ->
 298         C.MutCase (sp,i,substaux k outt, substaux k t,
 299          List.map (substaux k) pl)
 300      | C.Fix (i,fl) ->
 301         let len = List.length fl in
 302         let substitutedfl =
 303          List.map
 304           (fun (name,i,ty,bo) ->
 305             (name, i, substaux k ty, substaux (k+len) bo))
 306            fl
 307         in
 308          C.Fix (i, substitutedfl)
 309      | C.CoFix (i,fl) ->
 310         let len = List.length fl in
 311         let substitutedfl =
 312          List.map
 313           (fun (name,ty,bo) ->
 314             (name, substaux k ty, substaux (k+len) bo))
 315            fl
 316         in
 317          C.CoFix (i, substitutedfl)
 318  in
 319   substaux 1 where
 320 ;;
 321
 322 (* This is like "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]"
 323    up to the fact that the index to start from can be specified *)
 324 let replace_with_rel_1_from ~equality ~what =
 325    let rec find_image t = function
 326       | []       -> false
 327       | hd :: tl -> equality t hd || find_image t tl
 328    in
 329    let rec subst_term k t =
 330       if find_image t what then C.Rel k else inspect_term k t
 331    and inspect_term k = function
 332       | C.Rel i -> if i < k then C.Rel i else C.Rel (succ i)
 333       | C.Sort _ as t -> t
 334       | C.Implicit _ as t -> t
 335       | C.Var (uri, enss) ->
 336          let enss = List.map (subst_ens k) enss in
 337          C.Var (uri, enss)
 338       | C.Const (uri ,enss) ->
 339          let enss = List.map (subst_ens k) enss in
 340          C.Const (uri, enss)
 341      | C.MutInd (uri, tyno, enss) ->
 342          let enss = List.map (subst_ens k) enss in
 343          C.MutInd (uri, tyno, enss)
 344      | C.MutConstruct (uri, tyno, consno, enss) ->
 345          let enss = List.map (subst_ens k) enss in
 346          C.MutConstruct (uri, tyno, consno, enss)
 347      | C.Meta (i, mss) ->
 348          let mss = List.map (subst_ms k) mss in
 349          C.Meta(i, mss)
 350      | C.Cast (t, v) -> C.Cast (subst_term k t, subst_term k v)
 351      | C.Appl ts ->
 352          let ts = List.map (subst_term k) ts in
 353          C.Appl ts
 354      | C.MutCase (uri, tyno, outty, t, cases) ->
 355          let cases = List.map (subst_term k) cases in
 356          C.MutCase (uri, tyno, subst_term k outty, subst_term k t, cases)
 357      | C.Prod (n, v, t) ->
 358         C.Prod (n, subst_term k v, subst_term (succ k) t)
 359      | C.Lambda (n, v, t) ->
 360         C.Lambda (n, subst_term k v, subst_term (succ k) t)
 361      | C.LetIn (n, v, ty, t) ->
 362         C.LetIn (n, subst_term k v, subst_term k ty, subst_term (succ k) t)
 363      | C.Fix (i, fixes) ->
 364         let fixesno = List.length fixes in
 365         let fixes = List.map (subst_fix fixesno k) fixes in
 366         C.Fix (i, fixes)
 367      | C.CoFix (i, cofixes) ->
 368         let cofixesno = List.length cofixes in
 369         let cofixes = List.map (subst_cofix cofixesno k) cofixes in
 370          C.CoFix (i, cofixes)
 371    and subst_ens k (uri, t) = uri, subst_term k t
 372    and subst_ms k = function
 373       | None   -> None
 374       | Some t -> Some (subst_term k t)
 375    and subst_fix fixesno k (n, ind, ty, bo) =
 376       n, ind, subst_term k ty, subst_term (k + fixesno) bo
 377    and subst_cofix cofixesno k (n, ty, bo) =
 378       n, subst_term k ty, subst_term (k + cofixesno) bo
 379 in
 380 subst_term
 381
 382 let unfold ?what context where =
 383  let contextlen = List.length context in
 384  let first_is_the_expandable_head_of_second context' t1 t2 =
 385   match t1,t2 with
 386      Cic.Const (uri,_), Cic.Const (uri',_)
 387    | Cic.Var (uri,_), Cic.Var (uri',_)
 388    | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_)
 389    | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
 390    | Cic.Const _, _
 391    | Cic.Var _, _ -> false
 392    | Cic.Rel n, Cic.Rel m
 393    | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
 394       n + (List.length context' - contextlen) = m
 395    | Cic.Rel _, _ -> false
 396    | _,_ ->
 397      raise
 398       (ProofEngineTypes.Fail
 399         (lazy "The term to unfold is not a constant, a variable or a bound variable "))
 400  in
 401  let appl he tl =
 402   if tl = [] then he else Cic.Appl (he::tl) in
 403  let cannot_delta_expand t =
 404   raise
 405    (ProofEngineTypes.Fail
 406      (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
 407  let rec hd_delta_beta context tl =
 408   function
 409     Cic.Rel n as t ->
 410      (try
 411        match List.nth context (n-1) with
 412           Some (_,Cic.Decl _) -> cannot_delta_expand t
 413         | Some (_,Cic.Def (bo,_)) ->
 414            CicReduction.head_beta_reduce
 415             (appl (CicSubstitution.lift n bo) tl)
 416         | None -> raise RelToHiddenHypothesis
 417       with
 418          Failure _ -> assert false)
 419   | Cic.Const (uri,exp_named_subst) as t ->
 420      let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 421       (match o with
 422           Cic.Constant (_,Some body,_,_,_) ->
 423            CicReduction.head_beta_reduce
 424             (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
 425         | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t
 426         | Cic.Variable _ -> raise ReferenceToVariable
 427         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
 428         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 429       )
 430   | Cic.Var (uri,exp_named_subst) as t ->
 431      let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 432       (match o with
 433           Cic.Constant _ -> raise ReferenceToConstant
 434         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
 435         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 436         | Cic.Variable (_,Some body,_,_,_) ->
 437            CicReduction.head_beta_reduce
 438             (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
 439         | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t
 440       )
 441    | Cic.Appl [] -> assert false
 442    | Cic.Appl (he::tl) -> hd_delta_beta context tl he
 443    | t -> cannot_delta_expand t
 444  in
 445  let context_and_matched_term_list =
 446   match what with
 447      None -> [context, where]
 448    | Some what ->
 449       let res =
 450        ProofEngineHelpers.locate_in_term
 451         ~equality:first_is_the_expandable_head_of_second
 452         what ~where context
 453       in
 454        if res = [] then
 455         raise
 456          (ProofEngineTypes.Fail
 457            (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
 458        else
 459         res
 460  in
 461   let reduced_terms =
 462    List.map
 463     (function (context,where) -> hd_delta_beta context [] where)
 464     context_and_matched_term_list in
 465   let whats = List.map snd context_and_matched_term_list in
 466    replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where
 467 ;;
 468
 469 exception WrongShape;;
 470 exception AlreadySimplified;;
 471
 472 (* Takes a well-typed term and                                               *)
 473 (*  1) Performs beta-iota-zeta reduction until delta reduction is needed     *)
 474 (*  2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted  *)
 475 (*     w.r.t. zero or more variables and if the Fix can be reductaed, than it*)
 476 (*     is reduced, the delta-reduction is succesfull and the whole algorithm *)
 477 (*     is applied again to the new redex; Step 3.1) is applied to the result *)
 478 (*     of the recursive simplification. Otherwise, if the Fix can not be     *)
 479 (*     reduced, than the delta-reductions fails and the delta-redex is       *)
 480 (*     not reduced. Otherwise, if the delta-residual is not the              *)
 481 (*     lambda-abstraction of a Fix, then it performs step 3.2).              *)
 482 (* 3.1) Folds the application of the constant to the arguments that did not  *)
 483 (*     change in every iteration, i.e. to the actual arguments for the       *)
 484 (*     lambda-abstractions that precede the Fix.                             *)
 485 (* 3.2) Computes the head beta-zeta normal form of the term. Then it tries   *)
 486 (*     reductions. If the reduction cannot be performed, it returns the      *)
 487 (*     original term (not the head beta-zeta normal form of the definiendum) *)
 488 (*CSC: It does not perform simplification in a Case *)
 489
 490 let simpl context =
 491  (* a simplified term is active if it can create a redex when used as an *)
 492  (* actual parameter                                                     *)
 493  let rec is_active =
 494   function
 495      C.Lambda _
 496    | C.MutConstruct _
 497    | C.Appl (C.MutConstruct _::_)
 498    | C.CoFix _ -> true
 499    | C.Cast (bo,_) -> is_active bo
 500    | C.LetIn _ -> assert false
 501    | _ -> false
 502  in
 503  (* reduceaux is equal to the reduceaux locally defined inside *)
 504  (* reduce, but for the const case.                            *)
 505  (**** Step 1 ****)
 506  let rec reduceaux context l =
 507    function
 508       C.Rel n as t ->
 509        (* we never perform delta expansion automatically *)
 510        if l = [] then t else C.Appl (t::l)
 511     | C.Var (uri,exp_named_subst) ->
 512        let exp_named_subst' =
 513         reduceaux_exp_named_subst context l exp_named_subst
 514        in
 515         (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 516           match o with
 517             C.Constant _ -> raise ReferenceToConstant
 518           | C.CurrentProof _ -> raise ReferenceToCurrentProof
 519           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 520           | C.Variable (_,None,_,_,_) ->
 521             let t' = C.Var (uri,exp_named_subst') in
 522              if l = [] then t' else C.Appl (t'::l)
 523           | C.Variable (_,Some body,_,_,_) ->
 524              reduceaux context l
 525               (CicSubstitution.subst_vars exp_named_subst' body)
 526         )
 527     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
 528     | C.Sort _ as t -> t (* l should be empty *)
 529     | C.Implicit _ as t -> t
 530     | C.Cast (te,ty) ->
 531        C.Cast (reduceaux context l te, reduceaux context [] ty)
 532     | C.Prod (name,s,t) ->
 533        assert (l = []) ;
 534        C.Prod (name,
 535         reduceaux context [] s,
 536         reduceaux ((Some (name,C.Decl s))::context) [] t)
 537     | C.Lambda (name,s,t) ->
 538        (match l with
 539            [] ->
 540             C.Lambda (name,
 541              reduceaux context [] s,
 542              reduceaux ((Some (name,C.Decl s))::context) [] t)
 543          | he::tl -> reduceaux context tl (S.subst he t)
 544            (* when name is Anonimous the substitution should be superfluous *)
 545        )
 546     | C.LetIn (n,s,ty,t) ->
 547        reduceaux context l (S.subst (reduceaux context [] s) t)
 548     | C.Appl (he::tl) ->
 549        let tl' = List.map (reduceaux context []) tl in
 550         reduceaux context (tl'@l) he
 551     | C.Appl [] -> raise (Impossible 1)
 552     | C.Const (uri,exp_named_subst) ->
 553        let exp_named_subst' =
 554         reduceaux_exp_named_subst context l exp_named_subst
 555        in
 556         (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 557           match o with
 558            C.Constant (_,Some body,_,_,_) ->
 559             if List.exists is_active l then
 560              try_delta_expansion context l
 561               (C.Const (uri,exp_named_subst'))
 562               (CicSubstitution.subst_vars exp_named_subst' body)
 563             else
 564              let t' = C.Const (uri,exp_named_subst') in
 565               if l = [] then t' else C.Appl (t'::l)
 566          | C.Constant (_,None,_,_,_) ->
 567             let t' = C.Const (uri,exp_named_subst') in
 568              if l = [] then t' else C.Appl (t'::l)
 569          | C.Variable _ -> raise ReferenceToVariable
 570          | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body
 571          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 572        )
 573     | C.MutInd (uri,i,exp_named_subst) ->
 574        let exp_named_subst' =
 575         reduceaux_exp_named_subst context l exp_named_subst
 576        in
 577         let t' = C.MutInd (uri,i,exp_named_subst') in
 578          if l = [] then t' else C.Appl (t'::l)
 579     | C.MutConstruct (uri,i,j,exp_named_subst) ->
 580        let exp_named_subst' =
 581         reduceaux_exp_named_subst context l exp_named_subst
 582        in
 583         let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
 584          if l = [] then t' else C.Appl (t'::l)
 585     | C.MutCase (mutind,i,outtype,term,pl) ->
 586        let decofix =
 587         function
 588            C.CoFix (i,fl) ->
 589              let (_,_,body) = List.nth fl i in
 590               let body' =
 591                let counter = ref (List.length fl) in
 592                 List.fold_right
 593                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 594                  fl
 595                  body
 596               in
 597                reduceaux context [] body'
 598          | C.Appl (C.CoFix (i,fl) :: tl) ->
 599              let (_,_,body) = List.nth fl i in
 600              let body' =
 601               let counter = ref (List.length fl) in
 602                List.fold_right
 603                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 604                 fl
 605                 body
 606              in
 607               let tl' = List.map (reduceaux context []) tl in
 608                reduceaux context tl' body'
 609          | t -> t
 610        in
 611         (match decofix (reduceaux context [] term) (*(CicReduction.whd context term)*) with
 612             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
 613           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 614              let (arity, r) =
 615                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph mutind in
 616                  match o with
 617                      C.InductiveDefinition (tl,ingredients,r,_) ->
 618                        let (_,_,arity,_) = List.nth tl i in
 619                          (arity,r)
 620                    | _ -> raise WrongUriToInductiveDefinition
 621              in
 622               let ts =
 623                let rec eat_first =
 624                 function
 625                    (0,l) -> l
 626                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 627                  | _ -> raise (Impossible 5)
 628                in
 629                 eat_first (r,tl)
 630               in
 631                reduceaux context (ts@l) (List.nth pl (j-1))
 632          | C.Cast _ | C.Implicit _ ->
 633             raise (Impossible 2) (* we don't trust our whd ;-) *)
 634          | _ ->
 635            let outtype' = reduceaux context [] outtype in
 636            let term' = reduceaux context [] term in
 637            let pl' = List.map (reduceaux context []) pl in
 638             let res =
 639              C.MutCase (mutind,i,outtype',term',pl')
 640             in
 641              if l = [] then res else C.Appl (res::l)
 642        )
 643     | C.Fix (i,fl) ->
 644        let tys,_ =
 645          List.fold_left
 646            (fun (types,len) (n,_,ty,_) ->
 647               (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 648                len+1)
 649           ) ([],0) fl
 650        in
 651         let t' () =
 652          let fl' =
 653           List.map
 654            (function (n,recindex,ty,bo) ->
 655              (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 656            ) fl
 657          in
 658           C.Fix (i, fl')
 659         in
 660          let (_,recindex,_,body) = List.nth fl i in
 661           let recparam =
 662            try
 663             Some (List.nth l recindex)
 664            with
 665             _ -> None
 666           in
 667            (match recparam with
 668                Some recparam ->
 669                 (match reduceaux context [] recparam with
 670                     C.MutConstruct _
 671                   | C.Appl ((C.MutConstruct _)::_) ->
 672                      let body' =
 673                       let counter = ref (List.length fl) in
 674                        List.fold_right
 675                         (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 676                         fl
 677                         body
 678                      in
 679                       (* Possible optimization: substituting whd recparam in l*)
 680                       reduceaux context l body'
 681                   | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
 682                 )
 683              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
 684            )
 685     | C.CoFix (i,fl) ->
 686        let tys,_ =
 687         List.fold_left
 688           (fun (types,len) (n,ty,_) ->
 689              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 690               len+1)
 691          ) ([],0) fl
 692        in
 693         let t' =
 694          let fl' =
 695           List.map
 696            (function (n,ty,bo) ->
 697              (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 698            ) fl
 699          in
 700          C.CoFix (i, fl')
 701        in
 702          if l = [] then t' else C.Appl (t'::l)
 703  and reduceaux_exp_named_subst context l =
 704   List.map (function uri,t -> uri,reduceaux context [] t)
 705  (**** Step 2 ****)
 706  and reduce_with_no_hope_to_fold_back t l =
 707     prerr_endline "reduce_with_no_hope_to_fold_back";
 708     let simplified = reduceaux context l t in
 709     let t' = if l = [] then t else C.Appl (t::l) in
 710     if t' = simplified then
 711       raise AlreadySimplified
 712     else
 713       simplified
 714
 715  and try_delta_expansion context l term body =
 716    try
 717     let res,constant_args =
 718      let rec aux rev_constant_args l =
 719       function
 720          C.Lambda (name,s,t) ->
 721           begin
 722            match l with
 723               [] -> raise WrongShape
 724             | he::tl ->
 725                (* when name is Anonimous the substitution should *)
 726                (* be superfluous                                 *)
 727                aux (he::rev_constant_args) tl (S.subst he t)
 728           end
 729        | C.LetIn (_,s,_,t) ->
 730           aux rev_constant_args l (S.subst s t)
 731        | C.Fix (i,fl) ->
 732            let (_,recindex,_,body) = List.nth fl i in
 733             let recparam =
 734              try
 735               List.nth l recindex
 736              with
 737               _ -> raise AlreadySimplified
 738             in
 739              (match reduceaux context [] recparam (*CicReduction.whd context recparam*) with
 740                  C.MutConstruct _
 741                | C.Appl ((C.MutConstruct _)::_) ->
 742                   let body' =
 743                    let counter = ref (List.length fl) in
 744                     List.fold_right
 745                      (function _ ->
 746                        decr counter ; S.subst (C.Fix (!counter,fl))
 747                      ) fl body
 748                   in
 749                    (* Possible optimization: substituting whd *)
 750                    (* recparam in l                           *)
 751                    reduceaux context l body',
 752                     List.rev rev_constant_args
 753                | _ -> raise AlreadySimplified
 754              )
 755        | _ -> raise WrongShape
 756      in
 757       aux [] l body
 758     in
 759      (**** Step 3.1 ****)
 760      let term_to_fold, delta_expanded_term_to_fold =
 761       match constant_args with
 762          [] -> term,body
 763        | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
 764      in
 765       let simplified_term_to_fold =
 766        reduceaux context [] delta_expanded_term_to_fold
 767       in
 768        replace_lifting ~equality:(fun _ x y -> x = y) ~context
 769          ~what:[simplified_term_to_fold] ~with_what:[term_to_fold] ~where:res
 770    with
 771       WrongShape ->
 772        let rec skip_lambda n = function
 773          | Cic.Lambda (_,_,t) -> skip_lambda (n+1) t | t -> t, n
 774        in
 775        let is_fix uri =
 776          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 777          | Cic.Constant (_,Some bo, _, _,_) ->
 778              (let t, _ = skip_lambda 0 bo in
 779              match t with | Cic.Fix _ -> true | _ -> false)
 780          | _ -> false
 781        in
 782        let guess_recno uri =
 783          prerr_endline ("GUESS: " ^ UriManager.string_of_uri uri);
 784          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 785          | Cic.Constant (_,Some bo, _, _,_ ) ->
 786              let t, n = skip_lambda 0 bo in
 787              (match t with
 788              | Cic.Fix (i,fl) ->
 789                  let _,recno,_,_ = List.nth fl i in
 790                  prerr_endline ("GUESSED: " ^ string_of_int recno ^ " after " ^
 791                  string_of_int n ^ " lambdas");
 792                  recno + n
 793              | _ -> assert false)
 794          | _ -> assert false
 795        in
 796        let original_args = l in
 797        (**** Step 3.2 ****)
 798        let rec aux l =
 799         function
 800          | C.Lambda (name,s,t) ->
 801              (match l with
 802               | [] -> raise AlreadySimplified
 803               | he::tl ->
 804                  (* when name is Anonimous the substitution should *)
 805                  (* be superfluous                                 *)
 806                  aux tl (S.subst he t))
 807          | C.LetIn (_,s,_,t) -> aux l (S.subst s t)
 808          | Cic.Appl (Cic.Const (uri,_) :: args) as t when is_fix uri ->
 809              let recno =
 810                prerr_endline ("cerco : " ^ string_of_int (guess_recno uri)
 811                  ^ " in: " ^ String.concat " "
 812                  (List.map (fun x -> CicPp.ppterm x) args));
 813                prerr_endline ("e piglio il rispettivo in :"^String.concat " "
 814                  (List.map (fun x -> CicPp.ppterm x) original_args));
 815                (* look for args[regno] in saved_args *)
 816                let wanted = List.nth (args@l) (guess_recno uri) in
 817                let rec aux n = function
 818                  | [] -> n (* DA CAPIRE *)
 819                  | t::_ when t = wanted -> n
 820                  | _::tl -> aux (n+1) tl
 821                in
 822                aux 0 original_args
 823              in
 824              if recno = List.length original_args then
 825                reduce_with_no_hope_to_fold_back t l
 826              else
 827                let simplified = reduceaux context l t in
 828                let rec mk_implicits = function
 829                  | n,_::tl when n = recno ->
 830                      Cic.Implicit None :: (mk_implicits (n+1,tl))
 831                  | n,arg::tl -> arg :: (mk_implicits (n+1,tl))
 832                  | _,[] -> []
 833                in
 834                (* we try to fold back constant that do not expand to Fix *)
 835                let _ = prerr_endline
 836                  ("INIZIO (" ^ string_of_int recno ^ ") : " ^ CicPp.ppterm
 837                  simplified) in
 838                let term_to_fold =
 839                  Cic.Appl (term:: mk_implicits (0,original_args))
 840                in
 841                (try
 842                  let term_to_fold, _, metasenv, _ =
 843                    CicRefine.type_of_aux' [] context term_to_fold
 844                      CicUniv.oblivion_ugraph
 845                  in
 846                  let _ =
 847                    prerr_endline ("RAFFINA: "^CicPp.ppterm term_to_fold) in
 848                  let _ =
 849                    prerr_endline
 850                      ("RAFFINA: "^CicMetaSubst.ppmetasenv [] metasenv) in
 851                  let simplified_term_to_fold = unfold context term_to_fold in
 852                  let _ =
 853                    prerr_endline ("SEMPLIFICA: " ^
 854                      CicPp.ppterm simplified_term_to_fold)
 855                  in
 856                  let rec do_n f t =
 857                    let t1 = f t in
 858                    if t1 = t then t else do_n f t1
 859                  in
 860                  do_n
 861                  (fun simplified ->
 862                    let subst = ref [] in
 863                    let myunif ctx t1 t2 =
 864                      if !subst <> [] then false
 865                      else
 866                      try
 867                        prerr_endline "MUNIF";
 868                        prerr_endline (CicPp.ppterm t1);
 869                        prerr_endline "VS";
 870                        prerr_endline (CicPp.ppterm t2 ^ "\n");
 871                        let subst1, _, _ =
 872                          CicUnification.fo_unif metasenv ctx t1 t2
 873                            CicUniv.oblivion_ugraph
 874                        in
 875                        prerr_endline "UNIFICANO\n\n\n";
 876                        subst := subst1;
 877                        true
 878                      with
 879                      | CicUnification.UnificationFailure s
 880                      | CicUnification.Uncertain s
 881                      | CicUnification.AssertFailure s ->
 882                          prerr_endline (Lazy.force s); false
 883                      | CicUtil.Meta_not_found _ -> false
 884                      (*
 885                      | _ as exn ->
 886                          prerr_endline (Printexc.to_string exn);
 887                          false*)
 888                    in
 889                    let t =
 890                      replace_lifting myunif context
 891                        [simplified_term_to_fold] [term_to_fold] simplified
 892                    in
 893                    let _ = prerr_endline "UNIFICA" in
 894                    if List.length metasenv <> List.length !subst then
 895                      let _ = prerr_endline ("SUBST CORTA " ^
 896                        CicMetaSubst.ppsubst !subst ~metasenv)
 897                      in
 898                        simplified
 899                    else
 900                      if t = simplified then
 901                        let _ = prerr_endline "NULLA DI FATTO" in
 902                        simplified
 903                      else
 904                        let t = CicMetaSubst.apply_subst !subst t in
 905                        prerr_endline ("ECCO: " ^ CicPp.ppterm t); t)
 906                    simplified
 907                with
 908                | CicRefine.RefineFailure s
 909                | CicRefine.Uncertain s
 910                | CicRefine.AssertFailure s ->
 911                    prerr_endline (Lazy.force s); simplified
 912                (*| exn -> prerr_endline (Printexc.to_string exn); simplified*))
 913          | t -> reduce_with_no_hope_to_fold_back t l
 914       in
 915         (try aux l body
 916          with
 917           AlreadySimplified ->
 918            if l = [] then term else C.Appl (term::l))
 919     | AlreadySimplified ->
 920        (* If we performed delta-reduction, we would find a Fix   *)
 921        (* not applied to a constructor. So, we refuse to perform *)
 922        (* delta-reduction.                                       *)
 923        if l = [] then term else C.Appl (term::l)
 924  in
 925   reduceaux context []
 926 ;;