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,t) -> C.LetIn (n, aux s, 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 = (Some (n, Cic.Def (s,None)))::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,t) ->
 173        C.LetIn
 174         (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (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,t) ->
 272         C.LetIn (n, substaux k s, 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, t) ->
 362         C.LetIn (n, subst_term k v, 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
 383
 384
 385 (* Takes a well-typed term and fully reduces it. *)
 386 (*CSC: It does not perform reduction in a Case *)
 387 let reduce context =
 388  let rec reduceaux context l =
 389    function
 390       C.Rel n as t ->
 391        (match List.nth context (n-1) with
 392            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
 393          | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo)
 394          | None -> raise RelToHiddenHypothesis
 395        )
 396     | C.Var (uri,exp_named_subst) ->
 397        let exp_named_subst' =
 398         reduceaux_exp_named_subst context l exp_named_subst
 399        in
 400        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 401          match o with
 402            C.Constant _ -> raise ReferenceToConstant
 403          | C.CurrentProof _ -> raise ReferenceToCurrentProof
 404          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 405          | C.Variable (_,None,_,_,_) ->
 406             let t' = C.Var (uri,exp_named_subst') in
 407              if l = [] then t' else C.Appl (t'::l)
 408          | C.Variable (_,Some body,_,_,_) ->
 409             (reduceaux context l
 410               (CicSubstitution.subst_vars exp_named_subst' body))
 411        )
 412     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
 413     | C.Sort _ as t -> t (* l should be empty *)
 414     | C.Implicit _ as t -> t
 415     | C.Cast (te,ty) ->
 416        C.Cast (reduceaux context l te, reduceaux context l ty)
 417     | C.Prod (name,s,t) ->
 418        assert (l = []) ;
 419        C.Prod (name,
 420         reduceaux context [] s,
 421         reduceaux ((Some (name,C.Decl s))::context) [] t)
 422     | C.Lambda (name,s,t) ->
 423        (match l with
 424            [] ->
 425             C.Lambda (name,
 426              reduceaux context [] s,
 427              reduceaux ((Some (name,C.Decl s))::context) [] t)
 428          | he::tl -> reduceaux context tl (S.subst he t)
 429            (* when name is Anonimous the substitution should be superfluous *)
 430        )
 431     | C.LetIn (n,s,t) ->
 432        reduceaux context l (S.subst (reduceaux context [] s) t)
 433     | C.Appl (he::tl) ->
 434        let tl' = List.map (reduceaux context []) tl in
 435         reduceaux context (tl'@l) he
 436     | C.Appl [] -> raise (Impossible 1)
 437     | C.Const (uri,exp_named_subst) ->
 438        let exp_named_subst' =
 439         reduceaux_exp_named_subst context l exp_named_subst
 440        in
 441         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 442           match o with
 443             C.Constant (_,Some body,_,_,_) ->
 444              (reduceaux context l
 445                (CicSubstitution.subst_vars exp_named_subst' body))
 446           | C.Constant (_,None,_,_,_) ->
 447              let t' = C.Const (uri,exp_named_subst') in
 448               if l = [] then t' else C.Appl (t'::l)
 449           | C.Variable _ -> raise ReferenceToVariable
 450           | C.CurrentProof (_,_,body,_,_,_) ->
 451              (reduceaux context l
 452                (CicSubstitution.subst_vars exp_named_subst' body))
 453           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 454         )
 455     | C.MutInd (uri,i,exp_named_subst) ->
 456        let exp_named_subst' =
 457         reduceaux_exp_named_subst context l exp_named_subst
 458        in
 459         let t' = C.MutInd (uri,i,exp_named_subst') in
 460          if l = [] then t' else C.Appl (t'::l)
 461     | C.MutConstruct (uri,i,j,exp_named_subst) ->
 462        let exp_named_subst' =
 463         reduceaux_exp_named_subst context l exp_named_subst
 464        in
 465         let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
 466          if l = [] then t' else C.Appl (t'::l)
 467     | C.MutCase (mutind,i,outtype,term,pl) ->
 468        let decofix =
 469         function
 470            C.CoFix (i,fl) ->
 471              let (_,_,body) = List.nth fl i in
 472               let body' =
 473                let counter = ref (List.length fl) in
 474                 List.fold_right
 475                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 476                  fl
 477                  body
 478               in
 479                reduceaux context [] body'
 480          | C.Appl (C.CoFix (i,fl) :: tl) ->
 481              let (_,_,body) = List.nth fl i in
 482               let body' =
 483                let counter = ref (List.length fl) in
 484                 List.fold_right
 485                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 486                  fl
 487                  body
 488               in
 489                let tl' = List.map (reduceaux context []) tl in
 490                 reduceaux context tl' body'
 491          | t -> t
 492        in
 493         (match decofix (reduceaux context [] term) with
 494             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
 495           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 496              let (arity, r) =
 497                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
 498                  match o with
 499                      C.InductiveDefinition (tl,_,r,_) ->
 500                        let (_,_,arity,_) = List.nth tl i in
 501                          (arity,r)
 502                    | _ -> raise WrongUriToInductiveDefinition
 503              in
 504               let ts =
 505                let rec eat_first =
 506                 function
 507                    (0,l) -> l
 508                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 509                  | _ -> raise (Impossible 5)
 510                in
 511                 eat_first (r,tl)
 512               in
 513                reduceaux context (ts@l) (List.nth pl (j-1))
 514          | C.Cast _ | C.Implicit _ ->
 515             raise (Impossible 2) (* we don't trust our whd ;-) *)
 516          | _ ->
 517            let outtype' = reduceaux context [] outtype in
 518            let term' = reduceaux context [] term in
 519            let pl' = List.map (reduceaux context []) pl in
 520             let res =
 521              C.MutCase (mutind,i,outtype',term',pl')
 522             in
 523              if l = [] then res else C.Appl (res::l)
 524        )
 525     | C.Fix (i,fl) ->
 526        let tys,_ =
 527         List.fold_left
 528           (fun (types,len) (n,_,ty,_) ->
 529              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 530               len+1)
 531          ) ([],0) fl
 532        in
 533         let t' () =
 534          let fl' =
 535           List.map
 536            (function (n,recindex,ty,bo) ->
 537              (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 538            ) fl
 539          in
 540           C.Fix (i, fl')
 541         in
 542          let (_,recindex,_,body) = List.nth fl i in
 543           let recparam =
 544            try
 545             Some (List.nth l recindex)
 546            with
 547             _ -> None
 548           in
 549            (match recparam with
 550                Some recparam ->
 551                 (match reduceaux context [] recparam with
 552                     C.MutConstruct _
 553                   | C.Appl ((C.MutConstruct _)::_) ->
 554                      let body' =
 555                       let counter = ref (List.length fl) in
 556                        List.fold_right
 557                         (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 558                         fl
 559                         body
 560                      in
 561                       (* Possible optimization: substituting whd recparam in l*)
 562                       reduceaux context l body'
 563                   | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
 564                 )
 565              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
 566            )
 567     | C.CoFix (i,fl) ->
 568        let tys,_ =
 569         List.fold_left
 570           (fun (types,len) (n,ty,_) ->
 571              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 572               len+1)
 573          ) ([],0) fl
 574        in
 575         let t' =
 576          let fl' =
 577           List.map
 578            (function (n,ty,bo) ->
 579              (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 580            ) fl
 581          in
 582           C.CoFix (i, fl')
 583         in
 584          if l = [] then t' else C.Appl (t'::l)
 585  and reduceaux_exp_named_subst context l =
 586   List.map (function uri,t -> uri,reduceaux context [] t)
 587  in
 588   reduceaux context []
 589 ;;
 590
 591
 592 let unfold ?what context where =
 593  let contextlen = List.length context in
 594  let first_is_the_expandable_head_of_second context' t1 t2 =
 595   match t1,t2 with
 596      Cic.Const (uri,_), Cic.Const (uri',_)
 597    | Cic.Var (uri,_), Cic.Var (uri',_)
 598    | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_)
 599    | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
 600    | Cic.Const _, _
 601    | Cic.Var _, _ -> false
 602    | Cic.Rel n, Cic.Rel m
 603    | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
 604       n + (List.length context' - contextlen) = m
 605    | Cic.Rel _, _ -> false
 606    | _,_ ->
 607      raise
 608       (ProofEngineTypes.Fail
 609         (lazy "The term to unfold is not a constant, a variable or a bound variable "))
 610  in
 611  let appl he tl =
 612   if tl = [] then he else Cic.Appl (he::tl) in
 613  let cannot_delta_expand t =
 614   raise
 615    (ProofEngineTypes.Fail
 616      (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
 617  let rec hd_delta_beta context tl =
 618   function
 619     Cic.Rel n as t ->
 620      (try
 621        match List.nth context (n-1) with
 622           Some (_,Cic.Decl _) -> cannot_delta_expand t
 623         | Some (_,Cic.Def (bo,_)) ->
 624            CicReduction.head_beta_reduce
 625             (appl (CicSubstitution.lift n bo) tl)
 626         | None -> raise RelToHiddenHypothesis
 627       with
 628          Failure _ -> assert false)
 629   | Cic.Const (uri,exp_named_subst) as t ->
 630      let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 631       (match o with
 632           Cic.Constant (_,Some body,_,_,_) ->
 633            CicReduction.head_beta_reduce
 634             (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
 635         | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t
 636         | Cic.Variable _ -> raise ReferenceToVariable
 637         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
 638         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 639       )
 640   | Cic.Var (uri,exp_named_subst) as t ->
 641      let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 642       (match o with
 643           Cic.Constant _ -> raise ReferenceToConstant
 644         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
 645         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 646         | Cic.Variable (_,Some body,_,_,_) ->
 647            CicReduction.head_beta_reduce
 648             (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
 649         | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t
 650       )
 651    | Cic.Appl [] -> assert false
 652    | Cic.Appl (he::tl) -> hd_delta_beta context tl he
 653    | t -> cannot_delta_expand t
 654  in
 655  let context_and_matched_term_list =
 656   match what with
 657      None -> [context, where]
 658    | Some what ->
 659       let res =
 660        ProofEngineHelpers.locate_in_term
 661         ~equality:first_is_the_expandable_head_of_second
 662         what ~where context
 663       in
 664        if res = [] then
 665         raise
 666          (ProofEngineTypes.Fail
 667            (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
 668        else
 669         res
 670  in
 671   let reduced_terms =
 672    List.map
 673     (function (context,where) -> hd_delta_beta context [] where)
 674     context_and_matched_term_list in
 675   let whats = List.map snd context_and_matched_term_list in
 676    replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where
 677 ;;
 678
 679 exception WrongShape;;
 680 exception AlreadySimplified;;
 681
 682 (* Takes a well-typed term and                                               *)
 683 (*  1) Performs beta-iota-zeta reduction until delta reduction is needed     *)
 684 (*  2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted  *)
 685 (*     w.r.t. zero or more variables and if the Fix can be reductaed, than it*)
 686 (*     is reduced, the delta-reduction is succesfull and the whole algorithm *)
 687 (*     is applied again to the new redex; Step 3.1) is applied to the result *)
 688 (*     of the recursive simplification. Otherwise, if the Fix can not be     *)
 689 (*     reduced, than the delta-reductions fails and the delta-redex is       *)
 690 (*     not reduced. Otherwise, if the delta-residual is not the              *)
 691 (*     lambda-abstraction of a Fix, then it performs step 3.2).              *)
 692 (* 3.1) Folds the application of the constant to the arguments that did not  *)
 693 (*     change in every iteration, i.e. to the actual arguments for the       *)
 694 (*     lambda-abstractions that precede the Fix.                             *)
 695 (* 3.2) Computes the head beta-zeta normal form of the term. Then it tries   *)
 696 (*     reductions. If the reduction cannot be performed, it returns the      *)
 697 (*     original term (not the head beta-zeta normal form of the definiendum) *)
 698 (*CSC: It does not perform simplification in a Case *)
 699
 700 let simpl context =
 701  (* a simplified term is active if it can create a redex when used as an *)
 702  (* actual parameter                                                     *)
 703  let rec is_active =
 704   function
 705      C.Lambda _
 706    | C.MutConstruct _
 707    | C.Appl (C.MutConstruct _::_)
 708    | C.CoFix _ -> true
 709    | C.Cast (bo,_) -> is_active bo
 710    | C.LetIn _ -> assert false
 711    | _ -> false
 712  in
 713  (* reduceaux is equal to the reduceaux locally defined inside *)
 714  (* reduce, but for the const case.                            *)
 715  (**** Step 1 ****)
 716  let rec reduceaux context l =
 717    function
 718       C.Rel n as t ->
 719        (* we never perform delta expansion automatically *)
 720        if l = [] then t else C.Appl (t::l)
 721     | C.Var (uri,exp_named_subst) ->
 722        let exp_named_subst' =
 723         reduceaux_exp_named_subst context l exp_named_subst
 724        in
 725         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 726           match o with
 727             C.Constant _ -> raise ReferenceToConstant
 728           | C.CurrentProof _ -> raise ReferenceToCurrentProof
 729           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 730           | C.Variable (_,None,_,_,_) ->
 731             let t' = C.Var (uri,exp_named_subst') in
 732              if l = [] then t' else C.Appl (t'::l)
 733           | C.Variable (_,Some body,_,_,_) ->
 734              reduceaux context l
 735               (CicSubstitution.subst_vars exp_named_subst' body)
 736         )
 737     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
 738     | C.Sort _ as t -> t (* l should be empty *)
 739     | C.Implicit _ as t -> t
 740     | C.Cast (te,ty) ->
 741        C.Cast (reduceaux context l te, reduceaux context [] ty)
 742     | C.Prod (name,s,t) ->
 743        assert (l = []) ;
 744        C.Prod (name,
 745         reduceaux context [] s,
 746         reduceaux ((Some (name,C.Decl s))::context) [] t)
 747     | C.Lambda (name,s,t) ->
 748        (match l with
 749            [] ->
 750             C.Lambda (name,
 751              reduceaux context [] s,
 752              reduceaux ((Some (name,C.Decl s))::context) [] t)
 753          | he::tl -> reduceaux context tl (S.subst he t)
 754            (* when name is Anonimous the substitution should be superfluous *)
 755        )
 756     | C.LetIn (n,s,t) ->
 757        reduceaux context l (S.subst (reduceaux context [] s) t)
 758     | C.Appl (he::tl) ->
 759        let tl' = List.map (reduceaux context []) tl in
 760         reduceaux context (tl'@l) he
 761     | C.Appl [] -> raise (Impossible 1)
 762     | C.Const (uri,exp_named_subst) ->
 763        let exp_named_subst' =
 764         reduceaux_exp_named_subst context l exp_named_subst
 765        in
 766         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 767           match o with
 768            C.Constant (_,Some body,_,_,_) ->
 769             if List.exists is_active l then
 770              try_delta_expansion context l
 771               (C.Const (uri,exp_named_subst'))
 772               (CicSubstitution.subst_vars exp_named_subst' body)
 773             else
 774              let t' = C.Const (uri,exp_named_subst') in
 775               if l = [] then t' else C.Appl (t'::l)
 776          | C.Constant (_,None,_,_,_) ->
 777             let t' = C.Const (uri,exp_named_subst') in
 778              if l = [] then t' else C.Appl (t'::l)
 779          | C.Variable _ -> raise ReferenceToVariable
 780          | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body
 781          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 782        )
 783     | C.MutInd (uri,i,exp_named_subst) ->
 784        let exp_named_subst' =
 785         reduceaux_exp_named_subst context l exp_named_subst
 786        in
 787         let t' = C.MutInd (uri,i,exp_named_subst') in
 788          if l = [] then t' else C.Appl (t'::l)
 789     | C.MutConstruct (uri,i,j,exp_named_subst) ->
 790        let exp_named_subst' =
 791         reduceaux_exp_named_subst context l exp_named_subst
 792        in
 793         let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
 794          if l = [] then t' else C.Appl (t'::l)
 795     | C.MutCase (mutind,i,outtype,term,pl) ->
 796        let decofix =
 797         function
 798            C.CoFix (i,fl) ->
 799              let (_,_,body) = List.nth fl i in
 800               let body' =
 801                let counter = ref (List.length fl) in
 802                 List.fold_right
 803                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 804                  fl
 805                  body
 806               in
 807                reduceaux context [] body'
 808          | C.Appl (C.CoFix (i,fl) :: tl) ->
 809              let (_,_,body) = List.nth fl i in
 810              let body' =
 811               let counter = ref (List.length fl) in
 812                List.fold_right
 813                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 814                 fl
 815                 body
 816              in
 817               let tl' = List.map (reduceaux context []) tl in
 818                reduceaux context tl' body'
 819          | t -> t
 820        in
 821         (match decofix (reduceaux context [] term) (*(CicReduction.whd context term)*) with
 822             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
 823           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 824              let (arity, r) =
 825                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
 826                  match o with
 827                      C.InductiveDefinition (tl,ingredients,r,_) ->
 828                        let (_,_,arity,_) = List.nth tl i in
 829                          (arity,r)
 830                    | _ -> raise WrongUriToInductiveDefinition
 831              in
 832               let ts =
 833                let rec eat_first =
 834                 function
 835                    (0,l) -> l
 836                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 837                  | _ -> raise (Impossible 5)
 838                in
 839                 eat_first (r,tl)
 840               in
 841                reduceaux context (ts@l) (List.nth pl (j-1))
 842          | C.Cast _ | C.Implicit _ ->
 843             raise (Impossible 2) (* we don't trust our whd ;-) *)
 844          | _ ->
 845            let outtype' = reduceaux context [] outtype in
 846            let term' = reduceaux context [] term in
 847            let pl' = List.map (reduceaux context []) pl in
 848             let res =
 849              C.MutCase (mutind,i,outtype',term',pl')
 850             in
 851              if l = [] then res else C.Appl (res::l)
 852        )
 853     | C.Fix (i,fl) ->
 854        let tys,_ =
 855          List.fold_left
 856            (fun (types,len) (n,_,ty,_) ->
 857               (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 858                len+1)
 859           ) ([],0) fl
 860        in
 861         let t' () =
 862          let fl' =
 863           List.map
 864            (function (n,recindex,ty,bo) ->
 865              (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 866            ) fl
 867          in
 868           C.Fix (i, fl')
 869         in
 870          let (_,recindex,_,body) = List.nth fl i in
 871           let recparam =
 872            try
 873             Some (List.nth l recindex)
 874            with
 875             _ -> None
 876           in
 877            (match recparam with
 878                Some recparam ->
 879                 (match reduceaux context [] recparam with
 880                     C.MutConstruct _
 881                   | C.Appl ((C.MutConstruct _)::_) ->
 882                      let body' =
 883                       let counter = ref (List.length fl) in
 884                        List.fold_right
 885                         (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 886                         fl
 887                         body
 888                      in
 889                       (* Possible optimization: substituting whd recparam in l*)
 890                       reduceaux context l body'
 891                   | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
 892                 )
 893              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
 894            )
 895     | C.CoFix (i,fl) ->
 896        let tys,_ =
 897         List.fold_left
 898           (fun (types,len) (n,ty,_) ->
 899              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 900               len+1)
 901          ) ([],0) fl
 902        in
 903         let t' =
 904          let fl' =
 905           List.map
 906            (function (n,ty,bo) ->
 907              (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 908            ) fl
 909          in
 910          C.CoFix (i, fl')
 911        in
 912          if l = [] then t' else C.Appl (t'::l)
 913  and reduceaux_exp_named_subst context l =
 914   List.map (function uri,t -> uri,reduceaux context [] t)
 915  (**** Step 2 ****)
 916  and reduce_with_no_hope_to_fold_back t l =
 917     prerr_endline "reduce_with_no_hope_to_fold_back";
 918     let simplified = reduceaux context l t in
 919     let t' = if l = [] then t else C.Appl (t::l) in
 920     if t' = simplified then
 921       raise AlreadySimplified
 922     else
 923       simplified
 924
 925  and try_delta_expansion context l term body =
 926    try
 927     let res,constant_args =
 928      let rec aux rev_constant_args l =
 929       function
 930          C.Lambda (name,s,t) ->
 931           begin
 932            match l with
 933               [] -> raise WrongShape
 934             | he::tl ->
 935                (* when name is Anonimous the substitution should *)
 936                (* be superfluous                                 *)
 937                aux (he::rev_constant_args) tl (S.subst he t)
 938           end
 939        | C.LetIn (_,s,t) ->
 940           aux rev_constant_args l (S.subst s t)
 941        | C.Fix (i,fl) ->
 942            let (_,recindex,_,body) = List.nth fl i in
 943             let recparam =
 944              try
 945               List.nth l recindex
 946              with
 947               _ -> raise AlreadySimplified
 948             in
 949              (match reduceaux context [] recparam (*CicReduction.whd context recparam*) with
 950                  C.MutConstruct _
 951                | C.Appl ((C.MutConstruct _)::_) ->
 952                   let body' =
 953                    let counter = ref (List.length fl) in
 954                     List.fold_right
 955                      (function _ ->
 956                        decr counter ; S.subst (C.Fix (!counter,fl))
 957                      ) fl body
 958                   in
 959                    (* Possible optimization: substituting whd *)
 960                    (* recparam in l                           *)
 961                    reduceaux context l body',
 962                     List.rev rev_constant_args
 963                | _ -> raise AlreadySimplified
 964              )
 965        | _ -> raise WrongShape
 966      in
 967       aux [] l body
 968     in
 969      (**** Step 3.1 ****)
 970      let term_to_fold, delta_expanded_term_to_fold =
 971       match constant_args with
 972          [] -> term,body
 973        | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
 974      in
 975       let simplified_term_to_fold =
 976        reduceaux context [] delta_expanded_term_to_fold
 977       in
 978        replace_lifting ~equality:(fun _ x y -> x = y) ~context
 979          ~what:[simplified_term_to_fold] ~with_what:[term_to_fold] ~where:res
 980    with
 981       WrongShape ->
 982        let rec skip_lambda n = function
 983          | Cic.Lambda (_,_,t) -> skip_lambda (n+1) t | t -> t, n
 984        in
 985        let is_fix uri =
 986          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 987          | Cic.Constant (_,Some bo, _, _,_) ->
 988              (let t, _ = skip_lambda 0 bo in
 989              match t with | Cic.Fix _ -> true | _ -> false)
 990          | _ -> false
 991        in
 992        let guess_recno uri =
 993          prerr_endline ("GUESS: " ^ UriManager.string_of_uri uri);
 994          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 995          | Cic.Constant (_,Some bo, _, _,_ ) ->
 996              let t, n = skip_lambda 0 bo in
 997              (match t with
 998              | Cic.Fix (i,fl) ->
 999                  let _,recno,_,_ = List.nth fl i in
1000                  prerr_endline ("GUESSED: " ^ string_of_int recno ^ " after " ^
1001                  string_of_int n ^ " lambdas");
1002                  recno + n
1003              | _ -> assert false)
1004          | _ -> assert false
1005        in
1006        let original_args = l in
1007        (**** Step 3.2 ****)
1008        let rec aux l =
1009         function
1010          | C.Lambda (name,s,t) ->
1011              (match l with
1012               | [] -> raise AlreadySimplified
1013               | he::tl ->
1014                  (* when name is Anonimous the substitution should *)
1015                  (* be superfluous                                 *)
1016                  aux tl (S.subst he t))
1017          | C.LetIn (_,s,t) -> aux l (S.subst s t)
1018          | Cic.Appl (Cic.Const (uri,_) :: args) as t when is_fix uri ->
1019              let recno =
1020                prerr_endline ("cerco : " ^ string_of_int (guess_recno uri)
1021                  ^ " in: " ^ String.concat " "
1022                  (List.map (fun x -> CicPp.ppterm x) args));
1023                prerr_endline ("e piglio il rispettivo in :"^String.concat " "
1024                  (List.map (fun x -> CicPp.ppterm x) original_args));
1025                (* look for args[regno] in saved_args *)
1026                let wanted = List.nth (args@l) (guess_recno uri) in
1027                let rec aux n = function
1028                  | [] -> n (* DA CAPIRE *)
1029                  | t::_ when t = wanted -> n
1030                  | _::tl -> aux (n+1) tl
1031                in
1032                aux 0 original_args
1033              in
1034              if recno = List.length original_args then
1035                reduce_with_no_hope_to_fold_back t l
1036              else
1037                let simplified = reduceaux context l t in
1038                let rec mk_implicits = function
1039                  | n,_::tl when n = recno ->
1040                      Cic.Implicit None :: (mk_implicits (n+1,tl))
1041                  | n,arg::tl -> arg :: (mk_implicits (n+1,tl))
1042                  | _,[] -> []
1043                in
1044                (* we try to fold back constant that do not expand to Fix *)
1045                let _ = prerr_endline
1046                  ("INIZIO (" ^ string_of_int recno ^ ") : " ^ CicPp.ppterm
1047                  simplified) in
1048                let term_to_fold =
1049                  Cic.Appl (term:: mk_implicits (0,original_args))
1050                in
1051                (try
1052                  let term_to_fold, _, metasenv, _ =
1053                    CicRefine.type_of_aux' [] context term_to_fold
1054                      CicUniv.oblivion_ugraph
1055                  in
1056                  let _ =
1057                    prerr_endline ("RAFFINA: "^CicPp.ppterm term_to_fold) in
1058                  let _ =
1059                    prerr_endline
1060                      ("RAFFINA: "^CicMetaSubst.ppmetasenv [] metasenv) in
1061                  let simplified_term_to_fold = unfold context term_to_fold in
1062                  let _ =
1063                    prerr_endline ("SEMPLIFICA: " ^
1064                      CicPp.ppterm simplified_term_to_fold)
1065                  in
1066                  let rec do_n f t =
1067                    let t1 = f t in
1068                    if t1 = t then t else do_n f t1
1069                  in
1070                  do_n
1071                  (fun simplified ->
1072                    let subst = ref [] in
1073                    let myunif ctx t1 t2 =
1074                      if !subst <> [] then false
1075                      else
1076                      try
1077                        prerr_endline "MUNIF";
1078                        prerr_endline (CicPp.ppterm t1);
1079                        prerr_endline "VS";
1080                        prerr_endline (CicPp.ppterm t2 ^ "\n");
1081                        let subst1, _, _ =
1082                          CicUnification.fo_unif metasenv ctx t1 t2
1083                            CicUniv.empty_ugraph
1084                        in
1085                        prerr_endline "UNIFICANO\n\n\n";
1086                        subst := subst1;
1087                        true
1088                      with
1089                      | CicUnification.UnificationFailure s
1090                      | CicUnification.Uncertain s
1091                      | CicUnification.AssertFailure s ->
1092                          prerr_endline (Lazy.force s); false
1093                      | CicUtil.Meta_not_found _ -> false
1094                      (*
1095                      | _ as exn ->
1096                          prerr_endline (Printexc.to_string exn);
1097                          false*)
1098                    in
1099                    let t =
1100                      replace_lifting myunif context
1101                        [simplified_term_to_fold] [term_to_fold] simplified
1102                    in
1103                    let _ = prerr_endline "UNIFICA" in
1104                    if List.length metasenv <> List.length !subst then
1105                      let _ = prerr_endline ("SUBST CORTA " ^
1106                        CicMetaSubst.ppsubst !subst ~metasenv)
1107                      in
1108                        simplified
1109                    else
1110                      if t = simplified then
1111                        let _ = prerr_endline "NULLA DI FATTO" in
1112                        simplified
1113                      else
1114                        let t = CicMetaSubst.apply_subst !subst t in
1115                        prerr_endline ("ECCO: " ^ CicPp.ppterm t); t)
1116                    simplified
1117                with
1118                | CicRefine.RefineFailure s
1119                | CicRefine.Uncertain s
1120                | CicRefine.AssertFailure s ->
1121                    prerr_endline (Lazy.force s); simplified
1122                (*| exn -> prerr_endline (Printexc.to_string exn); simplified*))
1123          | t -> reduce_with_no_hope_to_fold_back t l
1124       in
1125         (try aux l body
1126          with
1127           AlreadySimplified ->
1128            if l = [] then term else C.Appl (term::l))
1129     | AlreadySimplified ->
1130        (* If we performed delta-reduction, we would find a Fix   *)
1131        (* not applied to a constructor. So, we refuse to perform *)
1132        (* delta-reduction.                                       *)
1133        if l = [] then term else C.Appl (term::l)
1134  in
1135   reduceaux context []
1136 ;;