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