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