helm/ocaml/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  (* reduceaux is equal to the reduceaux locally defined inside *)
 599  (* reduce, but for the const case.                            *)
 600  (**** Step 1 ****)
 601  let rec reduceaux context l =
 602   let module C = Cic in
 603   let module S = CicSubstitution in
 604    function
 605       C.Rel n as t ->
 606        (try
 607          match List.nth context (n-1) with
 608             Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
 609           | Some (_,C.Def (bo,_)) ->
 610              try_delta_expansion context l t (S.lift n bo)
 611           | None -> raise RelToHiddenHypothesis
 612         with
 613          Failure _ -> assert false)
 614     | C.Var (uri,exp_named_subst) ->
 615        let exp_named_subst' =
 616         reduceaux_exp_named_subst context l exp_named_subst
 617        in
 618         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 619           match o with
 620             C.Constant _ -> raise ReferenceToConstant
 621           | C.CurrentProof _ -> raise ReferenceToCurrentProof
 622           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 623           | C.Variable (_,None,_,_,_) ->
 624             let t' = C.Var (uri,exp_named_subst') in
 625              if l = [] then t' else C.Appl (t'::l)
 626           | C.Variable (_,Some body,_,_,_) ->
 627              reduceaux context l
 628               (CicSubstitution.subst_vars exp_named_subst' body)
 629         )
 630     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
 631     | C.Sort _ as t -> t (* l should be empty *)
 632     | C.Implicit _ as t -> t
 633     | C.Cast (te,ty) ->
 634        C.Cast (reduceaux context l te, reduceaux context l ty)
 635     | C.Prod (name,s,t) ->
 636        assert (l = []) ;
 637        C.Prod (name,
 638         reduceaux context [] s,
 639         reduceaux ((Some (name,C.Decl s))::context) [] t)
 640     | C.Lambda (name,s,t) ->
 641        (match l with
 642            [] ->
 643             C.Lambda (name,
 644              reduceaux context [] s,
 645              reduceaux ((Some (name,C.Decl s))::context) [] t)
 646          | he::tl -> reduceaux context tl (S.subst he t)
 647            (* when name is Anonimous the substitution should be superfluous *)
 648        )
 649     | C.LetIn (n,s,t) ->
 650        reduceaux context l (S.subst (reduceaux context [] s) t)
 651     | C.Appl (he::tl) ->
 652        let tl' = List.map (reduceaux context []) tl in
 653         reduceaux context (tl'@l) he
 654     | C.Appl [] -> raise (Impossible 1)
 655     | C.Const (uri,exp_named_subst) ->
 656        let exp_named_subst' =
 657         reduceaux_exp_named_subst context l exp_named_subst
 658        in
 659         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 660           match o with
 661            C.Constant (_,Some body,_,_,_) ->
 662             try_delta_expansion context l
 663              (C.Const (uri,exp_named_subst'))
 664              (CicSubstitution.subst_vars exp_named_subst' body)
 665          | C.Constant (_,None,_,_,_) ->
 666             let t' = C.Const (uri,exp_named_subst') in
 667              if l = [] then t' else C.Appl (t'::l)
 668          | C.Variable _ -> raise ReferenceToVariable
 669          | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body
 670          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 671        )
 672     | C.MutInd (uri,i,exp_named_subst) ->
 673        let exp_named_subst' =
 674         reduceaux_exp_named_subst context l exp_named_subst
 675        in
 676         let t' = C.MutInd (uri,i,exp_named_subst') in
 677          if l = [] then t' else C.Appl (t'::l)
 678     | C.MutConstruct (uri,i,j,exp_named_subst) ->
 679        let exp_named_subst' =
 680         reduceaux_exp_named_subst context l exp_named_subst
 681        in
 682         let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
 683          if l = [] then t' else C.Appl (t'::l)
 684     | C.MutCase (mutind,i,outtype,term,pl) ->
 685        let decofix =
 686         function
 687            C.CoFix (i,fl) ->
 688              let (_,_,body) = List.nth fl i in
 689               let body' =
 690                let counter = ref (List.length fl) in
 691                 List.fold_right
 692                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 693                  fl
 694                  body
 695               in
 696                reduceaux context [] body'
 697          | C.Appl (C.CoFix (i,fl) :: tl) ->
 698             let tys =
 699              List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl            in
 700              let (_,_,body) = List.nth fl i in
 701               let body' =
 702                let counter = ref (List.length fl) in
 703                 List.fold_right
 704                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 705                  fl
 706                  body
 707               in
 708                let tl' = List.map (reduceaux context []) tl in
 709                 reduceaux context tl' body'
 710          | t -> t
 711        in
 712         (match decofix (CicReduction.whd context term) with
 713             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
 714           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 715              let (arity, r) =
 716                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
 717                  match o with
 718                      C.InductiveDefinition (tl,ingredients,r,_) ->
 719                        let (_,_,arity,_) = List.nth tl i in
 720                          (arity,r)
 721                    | _ -> raise WrongUriToInductiveDefinition
 722              in
 723               let ts =
 724                let rec eat_first =
 725                 function
 726                    (0,l) -> l
 727                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 728                  | _ -> raise (Impossible 5)
 729                in
 730                 eat_first (r,tl)
 731               in
 732                reduceaux context (ts@l) (List.nth pl (j-1))
 733          | C.Cast _ | C.Implicit _ ->
 734             raise (Impossible 2) (* we don't trust our whd ;-) *)
 735          | _ ->
 736            let outtype' = reduceaux context [] outtype in
 737            let term' = reduceaux context [] term in
 738            let pl' = List.map (reduceaux context []) pl in
 739             let res =
 740              C.MutCase (mutind,i,outtype',term',pl')
 741             in
 742              if l = [] then res else C.Appl (res::l)
 743        )
 744     | C.Fix (i,fl) ->
 745        let tys =
 746         List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
 747        in
 748         let t' () =
 749          let fl' =
 750           List.map
 751            (function (n,recindex,ty,bo) ->
 752              (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 753            ) fl
 754          in
 755           C.Fix (i, fl')
 756         in
 757          let (_,recindex,_,body) = List.nth fl i in
 758           let recparam =
 759            try
 760             Some (List.nth l recindex)
 761            with
 762             _ -> None
 763           in
 764            (match recparam with
 765                Some recparam ->
 766                 (match reduceaux context [] recparam with
 767                     C.MutConstruct _
 768                   | C.Appl ((C.MutConstruct _)::_) ->
 769                      let body' =
 770                       let counter = ref (List.length fl) in
 771                        List.fold_right
 772                         (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 773                         fl
 774                         body
 775                      in
 776                       (* Possible optimization: substituting whd recparam in l*)
 777                       reduceaux context l body'
 778                   | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
 779                 )
 780              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
 781            )
 782     | C.CoFix (i,fl) ->
 783        let tys =
 784         List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
 785        in
 786         let t' =
 787          let fl' =
 788           List.map
 789            (function (n,ty,bo) ->
 790              (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
 791            ) fl
 792          in
 793          C.CoFix (i, fl')
 794        in
 795          if l = [] then t' else C.Appl (t'::l)
 796  and reduceaux_exp_named_subst context l =
 797   List.map (function uri,t -> uri,reduceaux context [] t)
 798  (**** Step 2 ****)
 799  and try_delta_expansion context l term body =
 800   let module C = Cic in
 801   let module S = CicSubstitution in
 802    try
 803     let res,constant_args =
 804      let rec aux rev_constant_args l =
 805       function
 806          C.Lambda (name,s,t) ->
 807           begin
 808            match l with
 809               [] -> raise WrongShape
 810             | he::tl ->
 811                (* when name is Anonimous the substitution should *)
 812                (* be superfluous                                 *)
 813                aux (he::rev_constant_args) tl (S.subst he t)
 814           end
 815        | C.LetIn (_,s,t) ->
 816           aux rev_constant_args l (S.subst s t)
 817        | C.Fix (i,fl) ->
 818            let (_,recindex,_,body) = List.nth fl i in
 819             let recparam =
 820              try
 821               List.nth l recindex
 822              with
 823               _ -> raise AlreadySimplified
 824             in
 825              (match CicReduction.whd context recparam with
 826                  C.MutConstruct _
 827                | C.Appl ((C.MutConstruct _)::_) ->
 828                   let body' =
 829                    let counter = ref (List.length fl) in
 830                     List.fold_right
 831                      (function _ ->
 832                        decr counter ; S.subst (C.Fix (!counter,fl))
 833                      ) fl body
 834                   in
 835                    (* Possible optimization: substituting whd *)
 836                    (* recparam in l                           *)
 837                    reduceaux context l body',
 838                     List.rev rev_constant_args
 839                | _ -> raise AlreadySimplified
 840              )
 841        | _ -> raise WrongShape
 842      in
 843       aux [] l body
 844     in
 845      (**** Step 3.1 ****)
 846      let term_to_fold, delta_expanded_term_to_fold =
 847       match constant_args with
 848          [] -> term,body
 849        | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
 850      in
 851       let simplified_term_to_fold =
 852        reduceaux context [] delta_expanded_term_to_fold
 853       in
 854        replace (=) [simplified_term_to_fold] [term_to_fold] res
 855    with
 856       WrongShape ->
 857        (**** Step 3.2 ****)
 858        let rec aux l =
 859         function
 860            C.Lambda (name,s,t) ->
 861              (match l with
 862                 [] -> raise AlreadySimplified
 863               | he::tl ->
 864                  (* when name is Anonimous the substitution should *)
 865                  (* be superfluous                                 *)
 866                  aux tl (S.subst he t))
 867          | C.LetIn (_,s,t) -> aux l (S.subst s t)
 868          | t ->
 869             let simplified = reduceaux context l t in
 870             if t = simplified then
 871              raise AlreadySimplified
 872             else
 873              simplified
 874        in
 875         (try aux l body
 876          with
 877           AlreadySimplified ->
 878            if l = [] then term else C.Appl (term::l))
 879     | AlreadySimplified ->
 880        (* If we performed delta-reduction, we would find a Fix   *)
 881        (* not applied to a constructor. So, we refuse to perform *)
 882        (* delta-reduction.                                       *)
 883        if l = [] then term else C.Appl (term::l)
 884  in
 885   reduceaux context []
 886 ;;
 887
 888 let unfold ?what context where =
 889  let contextlen = List.length context in
 890  let first_is_the_expandable_head_of_second context' t1 t2 =
 891   match t1,t2 with
 892      Cic.Const (uri,_), Cic.Const (uri',_)
 893    | Cic.Var (uri,_), Cic.Var (uri',_)
 894    | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_)
 895    | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
 896    | Cic.Const _, _
 897    | Cic.Var _, _ -> false
 898    | Cic.Rel n, Cic.Rel m
 899    | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
 900       n + (List.length context' - contextlen) = m
 901    | Cic.Rel _, _ -> false
 902    | _,_ ->
 903      raise
 904       (ProofEngineTypes.Fail
 905         (lazy "The term to unfold is not a constant, a variable or a bound variable "))
 906  in
 907  let appl he tl =
 908   if tl = [] then he else Cic.Appl (he::tl) in
 909  let cannot_delta_expand t =
 910   raise
 911    (ProofEngineTypes.Fail
 912      (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
 913  let rec hd_delta_beta context tl =
 914   function
 915     Cic.Rel n as t ->
 916      (try
 917        match List.nth context (n-1) with
 918           Some (_,Cic.Decl _) -> cannot_delta_expand t
 919         | Some (_,Cic.Def (bo,_)) ->
 920            CicReduction.head_beta_reduce
 921             (appl (CicSubstitution.lift n bo) tl)
 922         | None -> raise RelToHiddenHypothesis
 923       with
 924          Failure _ -> assert false)
 925   | Cic.Const (uri,exp_named_subst) as t ->
 926      let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 927       (match o with
 928           Cic.Constant (_,Some body,_,_,_) ->
 929            CicReduction.head_beta_reduce
 930             (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
 931         | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t
 932         | Cic.Variable _ -> raise ReferenceToVariable
 933         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
 934         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 935       )
 936   | Cic.Var (uri,exp_named_subst) as t ->
 937      let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 938       (match o with
 939           Cic.Constant _ -> raise ReferenceToConstant
 940         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
 941         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 942         | Cic.Variable (_,Some body,_,_,_) ->
 943            CicReduction.head_beta_reduce
 944             (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
 945         | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t
 946       )
 947    | Cic.Appl [] -> assert false
 948    | Cic.Appl (he::tl) -> hd_delta_beta context tl he
 949    | t -> cannot_delta_expand t
 950  in
 951  let context_and_matched_term_list =
 952   match what with
 953      None -> [context, where]
 954    | Some what ->
 955       let res =
 956        ProofEngineHelpers.locate_in_term
 957         ~equality:first_is_the_expandable_head_of_second
 958         what ~where context
 959       in
 960        if res = [] then
 961         raise
 962          (ProofEngineTypes.Fail
 963            (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
 964        else
 965         res
 966  in
 967   let reduced_terms =
 968    List.map
 969     (function (context,where) -> hd_delta_beta context [] where)
 970     context_and_matched_term_list in
 971   let whats = List.map snd context_and_matched_term_list in
 972    replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where
 973 ;;