helm/gTopLevel/proofEngineReduction.ml

   1 (* Copyright (C) 2000, 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
  37 (* The code of this module is derived from the code of CicReduction *)
  38
  39 exception Impossible of int;;
  40 exception ReferenceToDefinition;;
  41 exception ReferenceToAxiom;;
  42 exception ReferenceToVariable;;
  43 exception ReferenceToCurrentProof;;
  44 exception ReferenceToInductiveDefinition;;
  45 exception WrongUriToInductiveDefinition;;
  46
  47 (* "textual" replacement of a subterm with another one *)
  48 let replace ~what ~with_what ~where =
  49  let module C = Cic in
  50   let rec aux =
  51    function
  52       t when t = what -> with_what
  53     | C.Rel _ as t -> t
  54     | C.Var _ as t  -> t
  55     | C.Meta _ as t -> t
  56     | C.Sort _ as t -> t
  57     | C.Implicit as t -> t
  58     | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
  59     | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
  60     | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
  61     | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
  62     | C.Appl l ->
  63        (* Invariant enforced: no application of an application *)
  64        (match List.map aux l with
  65            (C.Appl l')::tl -> C.Appl (l'@tl)
  66          | l' -> C.Appl l')
  67     | C.Const _ as t -> t
  68     | C.Abst _ as t -> t
  69     | C.MutInd _ as t -> t
  70     | C.MutConstruct _ as t -> t
  71     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
  72        C.MutCase (sp,cookingsno,i,aux outt, aux t,
  73         List.map aux pl)
  74     | C.Fix (i,fl) ->
  75        let substitutedfl =
  76         List.map
  77          (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
  78           fl
  79        in
  80         C.Fix (i, substitutedfl)
  81     | C.CoFix (i,fl) ->
  82        let substitutedfl =
  83         List.map
  84          (fun (name,ty,bo) -> (name, aux ty, aux bo))
  85           fl
  86        in
  87         C.CoFix (i, substitutedfl)
  88   in
  89    aux where
  90 ;;
  91
  92 (* Takes a well-typed term and fully reduces it. *)
  93 (*CSC: It does not perform reduction in a Case *)
  94 let reduce =
  95  let rec reduceaux l =
  96   let module C = Cic in
  97   let module S = CicSubstitution in
  98    function
  99       C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
 100     | C.Var uri as t ->
 101        (match CicEnvironment.get_cooked_obj uri 0 with
 102            C.Definition _ -> raise ReferenceToDefinition
 103          | C.Axiom _ -> raise ReferenceToAxiom
 104          | C.CurrentProof _ -> raise ReferenceToCurrentProof
 105          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 106          | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
 107          | C.Variable (_,Some body,_) -> reduceaux l body
 108        )
 109     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
 110     | C.Sort _ as t -> t (* l should be empty *)
 111     | C.Implicit as t -> t
 112     | C.Cast (te,ty) -> reduceaux l te  (*CSC E' GIUSTO BUTTARE IL CAST? *)
 113     | C.Prod (name,s,t) ->
 114        assert (l = []) ;
 115        C.Prod (name, reduceaux [] s, reduceaux [] t)
 116     | C.Lambda (name,s,t) ->
 117        (match l with
 118            [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t)
 119          | he::tl -> reduceaux tl (S.subst he t)
 120            (* when name is Anonimous the substitution should be superfluous *)
 121        )
 122     | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t)
 123     | C.Appl (he::tl) ->
 124        let tl' = List.map (reduceaux []) tl in
 125         reduceaux (tl'@l) he
 126     | C.Appl [] -> raise (Impossible 1)
 127     | C.Const (uri,cookingsno) as t ->
 128        (match CicEnvironment.get_cooked_obj uri cookingsno with
 129            C.Definition (_,body,_,_) -> reduceaux l body
 130          | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
 131          | C.Variable _ -> raise ReferenceToVariable
 132          | C.CurrentProof (_,_,body,_) -> reduceaux l body
 133          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 134        )
 135     | C.Abst _ as t -> t (*CSC l should be empty ????? *)
 136     | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
 137     | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
 138     | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
 139        let decofix =
 140         function
 141            C.CoFix (i,fl) as t ->
 142             let (_,_,body) = List.nth fl i in
 143              let body' =
 144               let counter = ref (List.length fl) in
 145                List.fold_right
 146                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 147                 fl
 148                 body
 149              in
 150               reduceaux [] body'
 151          | C.Appl (C.CoFix (i,fl) :: tl) ->
 152             let (_,_,body) = List.nth fl i in
 153              let body' =
 154               let counter = ref (List.length fl) in
 155                List.fold_right
 156                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 157                 fl
 158                 body
 159              in
 160               let tl' = List.map (reduceaux []) tl in
 161                reduceaux tl body'
 162          | t -> t
 163        in
 164         (match decofix (reduceaux [] term) with
 165             C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1))
 166           | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
 167              let (arity, r, num_ingredients) =
 168               match CicEnvironment.get_obj mutind with
 169                  C.InductiveDefinition (tl,ingredients,r) ->
 170                    let (_,_,arity,_) = List.nth tl i
 171                    and num_ingredients =
 172                     List.fold_right
 173                      (fun (k,l) i ->
 174                        if k < cookingsno then i + List.length l else i
 175                      ) ingredients 0
 176                    in
 177                     (arity,r,num_ingredients)
 178                | _ -> raise WrongUriToInductiveDefinition
 179              in
 180               let ts =
 181                let num_to_eat = r + num_ingredients in
 182                 let rec eat_first =
 183                  function
 184                     (0,l) -> l
 185                   | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 186                   | _ -> raise (Impossible 5)
 187                 in
 188                  eat_first (num_to_eat,tl)
 189               in
 190                reduceaux (ts@l) (List.nth pl (j-1))
 191          | C.Abst _ | C.Cast _ | C.Implicit ->
 192             raise (Impossible 2) (* we don't trust our whd ;-) *)
 193          | _ ->
 194            let outtype' = reduceaux [] outtype in
 195            let term' = reduceaux [] term in
 196            let pl' = List.map (reduceaux []) pl in
 197             let res =
 198              C.MutCase (mutind,cookingsno,i,outtype',term',pl')
 199             in
 200              if l = [] then res else C.Appl (res::l)
 201        )
 202     | C.Fix (i,fl) ->
 203        let t' () =
 204         let fl' =
 205          List.map
 206           (function (n,recindex,ty,bo) ->
 207             (n,recindex,reduceaux [] ty, reduceaux [] bo)
 208           ) fl
 209         in
 210          C.Fix (i, fl')
 211        in
 212         let (_,recindex,_,body) = List.nth fl i in
 213          let recparam =
 214           try
 215            Some (List.nth l recindex)
 216           with
 217            _ -> None
 218          in
 219           (match recparam with
 220               Some recparam ->
 221                (match reduceaux [] recparam with
 222                    C.MutConstruct _
 223                  | C.Appl ((C.MutConstruct _)::_) ->
 224                     let body' =
 225                      let counter = ref (List.length fl) in
 226                       List.fold_right
 227                        (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 228                        fl
 229                        body
 230                     in
 231                      (* Possible optimization: substituting whd recparam in l *)
 232                      reduceaux l body'
 233                  | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
 234                )
 235             | None -> if l = [] then t' () else C.Appl ((t' ())::l)
 236           )
 237     | C.CoFix (i,fl) ->
 238        let t' =
 239         let fl' =
 240          List.map
 241           (function (n,ty,bo) ->
 242             (n,reduceaux [] ty, reduceaux [] bo)
 243           ) fl
 244         in
 245          C.CoFix (i, fl')
 246        in
 247         if l = [] then t' else C.Appl (t'::l)
 248  in
 249   reduceaux []
 250 ;;
 251
 252 exception WrongShape;;
 253 exception AlreadySimplified;;
 254 exception WhatShouldIDo;;
 255
 256 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
 257 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where       *)
 258 (*CSC:  Fix foo                                                      *)
 259 (*CSC:   {foo [n,m:nat]:nat :=                                       *)
 260 (*CSC:     Cases m of O => n | (S p) => (foo (S O) p) end            *)
 261 (*CSC:   }                                                           *)
 262 (* Takes a well-typed term and                                               *)
 263 (*  1) Performs beta-iota-zeta reduction until delta reduction is needed     *)
 264 (*  2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted  *)
 265 (*     w.r.t. zero or more variables and if the Fix can be reduced, than it  *)
 266 (*     is reduced, the delta-reduction is succesfull and the whole algorithm *)
 267 (*     is applied again to the new redex; Step 3) is applied to the result   *)
 268 (*     of the recursive simplification. Otherwise, if the Fix can not be     *)
 269 (*     reduced, than the delta-reductions fails and the delta-redex is       *)
 270 (*     not reduced. Otherwise, if the delta-residual is not the              *)
 271 (*     lambda-abstraction of a Fix, then it is reduced and the result is     *)
 272 (*     directly returned, without performing step 3).                        *)
 273 (*  3) Folds the application of the constant to the arguments that did not   *)
 274 (*     change in every iteration, i.e. to the actual arguments for the       *)
 275 (*     lambda-abstractions that precede the Fix.                             *)
 276 (*CSC: It does not perform simplification in a Case *)
 277 let simpl =
 278  (* reduceaux is equal to the reduceaux locally defined inside *)
 279  (*reduce, but for the const case.                             *)
 280  (**** Step 1 ****)
 281  let rec reduceaux l =
 282   let module C = Cic in
 283   let module S = CicSubstitution in
 284    function
 285       C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
 286     | C.Var uri as t ->
 287        (match CicEnvironment.get_cooked_obj uri 0 with
 288            C.Definition _ -> raise ReferenceToDefinition
 289          | C.Axiom _ -> raise ReferenceToAxiom
 290          | C.CurrentProof _ -> raise ReferenceToCurrentProof
 291          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 292          | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
 293          | C.Variable (_,Some body,_) -> reduceaux l body
 294        )
 295     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
 296     | C.Sort _ as t -> t (* l should be empty *)
 297     | C.Implicit as t -> t
 298     | C.Cast (te,ty) -> reduceaux l te  (*CSC E' GIUSTO BUTTARE IL CAST? *)
 299     | C.Prod (name,s,t) ->
 300        assert (l = []) ;
 301        C.Prod (name, reduceaux [] s, reduceaux [] t)
 302     | C.Lambda (name,s,t) ->
 303        (match l with
 304            [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t)
 305          | he::tl -> reduceaux tl (S.subst he t)
 306            (* when name is Anonimous the substitution should be superfluous *)
 307        )
 308     | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t)
 309     | C.Appl (he::tl) ->
 310        let tl' = List.map (reduceaux []) tl in
 311         reduceaux (tl'@l) he
 312     | C.Appl [] -> raise (Impossible 1)
 313     | C.Const (uri,cookingsno) as t ->
 314        (match CicEnvironment.get_cooked_obj uri cookingsno with
 315            C.Definition (_,body,_,_) ->
 316             begin
 317              try
 318               (**** Step 2 ****)
 319               let res,constant_args =
 320                let rec aux rev_constant_args l =
 321                 function
 322                    C.Lambda (name,s,t) as t' ->
 323                     begin
 324                      match l with
 325                         [] -> raise WrongShape
 326                       | he::tl ->
 327                          (* when name is Anonimous the substitution should be *)
 328                          (* superfluous                                       *)
 329                          aux (he::rev_constant_args) tl (S.subst he t)
 330                     end
 331                  | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *)
 332                  | C.Fix (i,fl) as t ->
 333                     let (_,recindex,_,body) = List.nth fl i in
 334                      let recparam =
 335                       try
 336                        List.nth l recindex
 337                       with
 338                        _ -> raise AlreadySimplified
 339                      in
 340                       (match CicReduction.whd recparam with
 341                           C.MutConstruct _
 342                         | C.Appl ((C.MutConstruct _)::_) ->
 343                            let body' =
 344                             let counter = ref (List.length fl) in
 345                              List.fold_right
 346                               (function _ ->
 347                                 decr counter ; S.subst (C.Fix (!counter,fl))
 348                               ) fl body
 349                            in
 350                             (* Possible optimization: substituting whd *)
 351                             (* recparam in l                           *)
 352                             reduceaux l body', List.rev rev_constant_args
 353                         | _ -> raise AlreadySimplified
 354                       )
 355                  | _ -> raise WrongShape
 356                in
 357                 aux [] l body
 358               in
 359                (**** Step 3 ****)
 360                let term_to_fold =
 361                 match constant_args with
 362                    [] -> C.Const (uri,cookingsno)
 363                  | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
 364                in
 365                 let reduced_term_to_fold = reduce term_to_fold in
 366 prerr_endline ("TERM TO FOLD: " ^ CicPp.ppterm term_to_fold) ; flush stderr ;
 367 prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; flush stderr ;
 368                  replace reduced_term_to_fold term_to_fold res
 369              with
 370                 WrongShape ->
 371                  (* The constant does not unfold to a Fix lambda-abstracted   *)
 372                  (* w.r.t. zero or more variables. We just perform reduction. *)
 373                  reduceaux l body
 374               | AlreadySimplified ->
 375                  (* If we performed delta-reduction, we would find a Fix   *)
 376                  (* not applied to a constructor. So, we refuse to perform *)
 377                  (* delta-reduction.                                       *)
 378                  if l = [] then
 379                     t
 380                  else
 381                   C.Appl (t::l)
 382             end
 383          | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
 384          | C.Variable _ -> raise ReferenceToVariable
 385          | C.CurrentProof (_,_,body,_) -> reduceaux l body
 386          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 387        )
 388     | C.Abst _ as t -> t (*CSC l should be empty ????? *)
 389     | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
 390     | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
 391     | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
 392        let decofix =
 393         function
 394            C.CoFix (i,fl) as t ->
 395             let (_,_,body) = List.nth fl i in
 396              let body' =
 397               let counter = ref (List.length fl) in
 398                List.fold_right
 399                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 400                 fl
 401                 body
 402              in
 403               reduceaux [] body'
 404          | C.Appl (C.CoFix (i,fl) :: tl) ->
 405             let (_,_,body) = List.nth fl i in
 406              let body' =
 407               let counter = ref (List.length fl) in
 408                List.fold_right
 409                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 410                 fl
 411                 body
 412              in
 413               let tl' = List.map (reduceaux []) tl in
 414                reduceaux tl body'
 415          | t -> t
 416        in
 417         (match decofix (reduceaux [] term) with
 418             C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1))
 419           | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
 420              let (arity, r, num_ingredients) =
 421               match CicEnvironment.get_obj mutind with
 422                  C.InductiveDefinition (tl,ingredients,r) ->
 423                    let (_,_,arity,_) = List.nth tl i
 424                    and num_ingredients =
 425                     List.fold_right
 426                      (fun (k,l) i ->
 427                        if k < cookingsno then i + List.length l else i
 428                      ) ingredients 0
 429                    in
 430                     (arity,r,num_ingredients)
 431                | _ -> raise WrongUriToInductiveDefinition
 432              in
 433               let ts =
 434                let num_to_eat = r + num_ingredients in
 435                 let rec eat_first =
 436                  function
 437                     (0,l) -> l
 438                   | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 439                   | _ -> raise (Impossible 5)
 440                 in
 441                  eat_first (num_to_eat,tl)
 442               in
 443                reduceaux (ts@l) (List.nth pl (j-1))
 444          | C.Abst _ | C.Cast _ | C.Implicit ->
 445             raise (Impossible 2) (* we don't trust our whd ;-) *)
 446          | _ ->
 447            let outtype' = reduceaux [] outtype in
 448            let term' = reduceaux [] term in
 449            let pl' = List.map (reduceaux []) pl in
 450             let res =
 451              C.MutCase (mutind,cookingsno,i,outtype',term',pl')
 452             in
 453              if l = [] then res else C.Appl (res::l)
 454        )
 455     | C.Fix (i,fl) ->
 456        let t' () =
 457         let fl' =
 458          List.map
 459           (function (n,recindex,ty,bo) ->
 460             (n,recindex,reduceaux [] ty, reduceaux [] bo)
 461           ) fl
 462         in
 463          C.Fix (i, fl')
 464        in
 465         let (_,recindex,_,body) = List.nth fl i in
 466          let recparam =
 467           try
 468            Some (List.nth l recindex)
 469           with
 470            _ -> None
 471          in
 472           (match recparam with
 473               Some recparam ->
 474                (match reduceaux [] recparam with
 475                    C.MutConstruct _
 476                  | C.Appl ((C.MutConstruct _)::_) ->
 477                     let body' =
 478                      let counter = ref (List.length fl) in
 479                       List.fold_right
 480                        (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 481                        fl
 482                        body
 483                     in
 484                      (* Possible optimization: substituting whd recparam in l *)
 485                      reduceaux l body'
 486                  | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
 487                )
 488             | None -> if l = [] then t' () else C.Appl ((t' ())::l)
 489           )
 490     | C.CoFix (i,fl) ->
 491        let t' =
 492         let fl' =
 493          List.map
 494           (function (n,ty,bo) ->
 495             (n,reduceaux [] ty, reduceaux [] bo)
 496           ) fl
 497         in
 498          C.CoFix (i, fl')
 499        in
 500         if l = [] then t' else C.Appl (t'::l)
 501  in
 502   reduceaux []
 503 ;;