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