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