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 function t -> let res =
 250 prerr_endline ("<<<<<<<<<<<<<<<<" ^ CicPp.ppterm t) ; flush stderr ;
 251   reduceaux []
 252 t in prerr_endline ("++++++++++++++++++" ^ CicPp.ppterm res) ; flush stderr ; res
 253 ;;
 254
 255 exception WrongShape;;
 256 exception AlreadySimplified;;
 257 exception WhatShouldIDo;;
 258
 259 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
 260 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where       *)
 261 (*CSC:  Fix foo                                                      *)
 262 (*CSC:   {foo [n,m:nat]:nat :=                                       *)
 263 (*CSC:     Cases m of O => n | (S p) => (foo (S O) p) end            *)
 264 (*CSC:   }                                                           *)
 265 (* Takes a well-typed term and                                               *)
 266 (*  1) Performs beta-iota-zeta reduction until delta reduction is needed     *)
 267 (*  2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted  *)
 268 (*     w.r.t. zero or more variables and if the Fix can be reduced, than it  *)
 269 (*     is reduced, the delta-reduction is succesfull and the whole algorithm *)
 270 (*     is applied again to the new redex; Step 3) is applied to the result   *)
 271 (*     of the recursive simplification. Otherwise, if the Fix can not be     *)
 272 (*     reduced, than the delta-reductions fails and the delta-redex is       *)
 273 (*     not reduced. Otherwise, if the delta-residual is not the              *)
 274 (*     lambda-abstraction of a Fix, then it is reduced and the result is     *)
 275 (*     directly returned, without performing step 3).                        *)
 276 (*  3) Folds the application of the constant to the arguments that did not   *)
 277 (*     change in every iteration, i.e. to the actual arguments for the       *)
 278 (*     lambda-abstractions that precede the Fix.                             *)
 279 (*CSC: It does not perform simplification in a Case *)
 280 let simpl =
 281  (* reduceaux is equal to the reduceaux locally defined inside *)
 282  (*reduce, but for the const case.                             *)
 283  (**** Step 1 ****)
 284  let rec reduceaux l =
 285   let module C = Cic in
 286   let module S = CicSubstitution in
 287    function
 288       C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
 289     | C.Var uri as t ->
 290        (match CicEnvironment.get_cooked_obj uri 0 with
 291            C.Definition _ -> raise ReferenceToDefinition
 292          | C.Axiom _ -> raise ReferenceToAxiom
 293          | C.CurrentProof _ -> raise ReferenceToCurrentProof
 294          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 295          | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
 296          | C.Variable (_,Some body,_) -> reduceaux l body
 297        )
 298     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
 299     | C.Sort _ as t -> t (* l should be empty *)
 300     | C.Implicit as t -> t
 301     | C.Cast (te,ty) -> reduceaux l te  (*CSC E' GIUSTO BUTTARE IL CAST? *)
 302     | C.Prod (name,s,t) ->
 303        assert (l = []) ;
 304        C.Prod (name, reduceaux [] s, reduceaux [] t)
 305     | C.Lambda (name,s,t) ->
 306        (match l with
 307            [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t)
 308          | he::tl -> reduceaux tl (S.subst he t)
 309            (* when name is Anonimous the substitution should be superfluous *)
 310        )
 311     | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t)
 312     | C.Appl (he::tl) ->
 313        let tl' = List.map (reduceaux []) tl in
 314         reduceaux (tl'@l) he
 315     | C.Appl [] -> raise (Impossible 1)
 316     | C.Const (uri,cookingsno) as t ->
 317        (match CicEnvironment.get_cooked_obj uri cookingsno with
 318            C.Definition (_,body,_,_) ->
 319             begin
 320              try
 321               (**** Step 2 ****)
 322               let res,constant_args =
 323                let rec aux rev_constant_args l =
 324                 function
 325                    C.Lambda (name,s,t) as t' ->
 326                     begin
 327                      match l with
 328                         [] -> raise WrongShape
 329                       | he::tl ->
 330                          (* when name is Anonimous the substitution should be *)
 331                          (* superfluous                                       *)
 332                          aux (he::rev_constant_args) tl (S.subst he t)
 333                     end
 334                  | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *)
 335                  | C.Fix (i,fl) as t ->
 336                     let (_,recindex,_,body) = List.nth fl i in
 337                      let recparam =
 338                       try
 339                        List.nth l recindex
 340                       with
 341                        _ -> raise AlreadySimplified
 342                      in
 343                       (match CicReduction.whd recparam with
 344                           C.MutConstruct _
 345                         | C.Appl ((C.MutConstruct _)::_) ->
 346                            let body' =
 347                             let counter = ref (List.length fl) in
 348                              List.fold_right
 349                               (function _ ->
 350                                 decr counter ; S.subst (C.Fix (!counter,fl))
 351                               ) fl body
 352                            in
 353                             (* Possible optimization: substituting whd *)
 354                             (* recparam in l                           *)
 355                             reduceaux l body', List.rev rev_constant_args
 356                         | _ -> raise AlreadySimplified
 357                       )
 358                  | _ -> raise WrongShape
 359                in
 360                 aux [] l body
 361               in
 362                (**** Step 3 ****)
 363                let term_to_fold =
 364                 match constant_args with
 365                    [] -> C.Const (uri,cookingsno)
 366                  | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
 367                in
 368                 let reduced_term_to_fold = reduce term_to_fold in
 369 prerr_endline ("TERM TO FOLD: " ^ CicPp.ppterm term_to_fold) ; flush stderr ;
 370 prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; flush stderr ;
 371                  replace reduced_term_to_fold term_to_fold res
 372              with
 373                 WrongShape ->
 374                  (* The constant does not unfold to a Fix lambda-abstracted   *)
 375                  (* w.r.t. zero or more variables. We just perform reduction. *)
 376                  reduceaux l body
 377               | AlreadySimplified ->
 378                  (* If we performed delta-reduction, we would find a Fix   *)
 379                  (* not applied to a constructor. So, we refuse to perform *)
 380                  (* delta-reduction.                                       *)
 381                  if l = [] then
 382                     t
 383                  else
 384                   C.Appl (t::l)
 385             end
 386          | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
 387          | C.Variable _ -> raise ReferenceToVariable
 388          | C.CurrentProof (_,_,body,_) -> reduceaux l body
 389          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 390        )
 391     | C.Abst _ as t -> t (*CSC l should be empty ????? *)
 392     | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
 393     | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
 394     | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
 395        let decofix =
 396         function
 397            C.CoFix (i,fl) as t ->
 398             let (_,_,body) = List.nth fl i in
 399              let body' =
 400               let counter = ref (List.length fl) in
 401                List.fold_right
 402                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 403                 fl
 404                 body
 405              in
 406               reduceaux [] body'
 407          | C.Appl (C.CoFix (i,fl) :: tl) ->
 408             let (_,_,body) = List.nth fl i in
 409              let body' =
 410               let counter = ref (List.length fl) in
 411                List.fold_right
 412                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 413                 fl
 414                 body
 415              in
 416               let tl' = List.map (reduceaux []) tl in
 417                reduceaux tl body'
 418          | t -> t
 419        in
 420         (match decofix (reduceaux [] term) with
 421             C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1))
 422           | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
 423              let (arity, r, num_ingredients) =
 424               match CicEnvironment.get_obj mutind with
 425                  C.InductiveDefinition (tl,ingredients,r) ->
 426                    let (_,_,arity,_) = List.nth tl i
 427                    and num_ingredients =
 428                     List.fold_right
 429                      (fun (k,l) i ->
 430                        if k < cookingsno then i + List.length l else i
 431                      ) ingredients 0
 432                    in
 433                     (arity,r,num_ingredients)
 434                | _ -> raise WrongUriToInductiveDefinition
 435              in
 436               let ts =
 437                let num_to_eat = r + num_ingredients in
 438                 let rec eat_first =
 439                  function
 440                     (0,l) -> l
 441                   | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 442                   | _ -> raise (Impossible 5)
 443                 in
 444                  eat_first (num_to_eat,tl)
 445               in
 446                reduceaux (ts@l) (List.nth pl (j-1))
 447          | C.Abst _ | C.Cast _ | C.Implicit ->
 448             raise (Impossible 2) (* we don't trust our whd ;-) *)
 449          | _ ->
 450            let outtype' = reduceaux [] outtype in
 451            let term' = reduceaux [] term in
 452            let pl' = List.map (reduceaux []) pl in
 453             let res =
 454              C.MutCase (mutind,cookingsno,i,outtype',term',pl')
 455             in
 456              if l = [] then res else C.Appl (res::l)
 457        )
 458     | C.Fix (i,fl) ->
 459        let t' () =
 460         let fl' =
 461          List.map
 462           (function (n,recindex,ty,bo) ->
 463             (n,recindex,reduceaux [] ty, reduceaux [] bo)
 464           ) fl
 465         in
 466          C.Fix (i, fl')
 467        in
 468         let (_,recindex,_,body) = List.nth fl i in
 469          let recparam =
 470           try
 471            Some (List.nth l recindex)
 472           with
 473            _ -> None
 474          in
 475           (match recparam with
 476               Some recparam ->
 477                (match reduceaux [] recparam with
 478                    C.MutConstruct _
 479                  | C.Appl ((C.MutConstruct _)::_) ->
 480                     let body' =
 481                      let counter = ref (List.length fl) in
 482                       List.fold_right
 483                        (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 484                        fl
 485                        body
 486                     in
 487                      (* Possible optimization: substituting whd recparam in l *)
 488                      reduceaux l body'
 489                  | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
 490                )
 491             | None -> if l = [] then t' () else C.Appl ((t' ())::l)
 492           )
 493     | C.CoFix (i,fl) ->
 494        let t' =
 495         let fl' =
 496          List.map
 497           (function (n,ty,bo) ->
 498             (n,reduceaux [] ty, reduceaux [] bo)
 499           ) fl
 500         in
 501          C.CoFix (i, fl')
 502        in
 503         if l = [] then t' else C.Appl (t'::l)
 504  in
 505   reduceaux []
 506 ;;