components/tactics/proofEngineReduction.ml

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