helm/ocaml/cic_proof_checking/cicReductionMachine.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 (* TODO unify exceptions *)
  27
  28 exception CicReductionInternalError;;
  29 exception WrongUriToInductiveDefinition;;
  30 exception Impossible of int;;
  31 exception ReferenceToConstant;;
  32 exception ReferenceToVariable;;
  33 exception ReferenceToCurrentProof;;
  34 exception ReferenceToInductiveDefinition;;
  35
  36 let fdebug = ref 1;;
  37 let debug t env s =
  38  let rec debug_aux t i =
  39   let module C = Cic in
  40   let module U = UriManager in
  41    CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
  42  in
  43   if !fdebug = 0 then
  44    prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
  45 ;;
  46
  47 module type Strategy =
  48  sig
  49   type stack_term
  50   type env_term
  51   type ens_term
  52   val to_stack : Cic.term -> stack_term
  53   val to_stack_list : Cic.term list -> stack_term list
  54   val to_env : Cic.term -> env_term
  55   val to_ens : Cic.term -> ens_term
  56   val from_stack :
  57    unwind:
  58     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  59       Cic.term -> Cic.term) ->
  60    stack_term -> Cic.term
  61   val from_stack_list :
  62    unwind:
  63     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  64       Cic.term -> Cic.term) ->
  65    stack_term list -> Cic.term list
  66   val from_env : env_term -> Cic.term
  67   val from_ens : ens_term -> Cic.term
  68   val stack_to_env :
  69    reduce:
  70     (int * env_term list * ens_term Cic.explicit_named_substitution *
  71       Cic.term * stack_term list -> Cic.term) ->
  72    unwind:
  73     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  74       Cic.term -> Cic.term) ->
  75    stack_term -> env_term
  76   val compute_to_env :
  77    reduce:
  78     (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
  79       stack_term list -> Cic.term) ->
  80    unwind:
  81     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  82       Cic.term -> Cic.term) ->
  83    int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  84     Cic.term -> env_term
  85   val compute_to_stack :
  86    reduce:
  87     (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
  88       stack_term list -> Cic.term) ->
  89    unwind:
  90     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  91       Cic.term -> Cic.term) ->
  92    int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  93     Cic.term -> stack_term
  94  end
  95 ;;
  96
  97 module CallByNameStrategy =
  98  struct
  99   type stack_term = Cic.term
 100   type env_term = Cic.term
 101   type ens_term = Cic.term
 102   let to_stack v = v
 103   let to_stack_list l = l
 104   let to_env v = v
 105   let to_ens v = v
 106   let from_stack ~unwind v = v
 107   let from_stack_list ~unwind l = l
 108   let from_env v = v
 109   let from_ens v = v
 110   let stack_to_env ~reduce ~unwind v = v
 111   let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
 112   let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
 113  end
 114 ;;
 115
 116 module CallByValueStrategy =
 117  struct
 118   type stack_term = Cic.term
 119   type env_term = Cic.term
 120   type ens_term = Cic.term
 121   let to_stack v = v
 122   let to_stack_list l = l
 123   let to_env v = v
 124   let to_ens v = v
 125   let from_stack ~unwind v = v
 126   let from_stack_list ~unwind l = l
 127   let from_env v = v
 128   let from_ens v = v
 129   let stack_to_env ~reduce ~unwind v = v
 130   let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
 131   let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
 132  end
 133 ;;
 134
 135 module CallByValueStrategyByNameOnConstants =
 136  struct
 137   type stack_term = Cic.term
 138   type env_term = Cic.term
 139   type ens_term = Cic.term
 140   let to_stack v = v
 141   let to_stack_list l = l
 142   let to_env v = v
 143   let to_ens v = v
 144   let from_stack ~unwind v = v
 145   let from_stack_list ~unwind l = l
 146   let from_env v = v
 147   let from_ens v = v
 148   let stack_to_env ~reduce ~unwind v = v
 149   let compute_to_stack ~reduce ~unwind k e ens =
 150    function
 151       Cic.Const _ as t -> unwind k e ens t
 152     | t -> reduce (k,e,ens,t,[])
 153   let compute_to_env ~reduce ~unwind k e ens =
 154    function
 155       Cic.Const _ as t -> unwind k e ens t
 156     | t -> reduce (k,e,ens,t,[])
 157  end
 158 ;;
 159
 160 module LazyCallByValueStrategy =
 161  struct
 162   type stack_term = Cic.term lazy_t
 163   type env_term = Cic.term lazy_t
 164   type ens_term = Cic.term lazy_t
 165   let to_stack v = lazy v
 166   let to_stack_list l = List.map to_stack l
 167   let to_env v = lazy v
 168   let to_ens v = lazy v
 169   let from_stack ~unwind v = Lazy.force v
 170   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 171   let from_env v = Lazy.force v
 172   let from_ens v = Lazy.force v
 173   let stack_to_env ~reduce ~unwind v = v
 174   let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
 175   let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
 176  end
 177 ;;
 178
 179 module LazyCallByValueStrategyByNameOnConstants =
 180  struct
 181   type stack_term = Cic.term lazy_t
 182   type env_term = Cic.term lazy_t
 183   type ens_term = Cic.term lazy_t
 184   let to_stack v = lazy v
 185   let to_stack_list l = List.map to_stack l
 186   let to_env v = lazy v
 187   let to_ens v = lazy v
 188   let from_stack ~unwind v = Lazy.force v
 189   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 190   let from_env v = Lazy.force v
 191   let from_ens v = Lazy.force v
 192   let stack_to_env ~reduce ~unwind v = v
 193   let compute_to_stack ~reduce ~unwind k e ens t =
 194    lazy (
 195     match t with
 196        Cic.Const _ as t -> unwind k e ens t
 197      | t -> reduce (k,e,ens,t,[]))
 198   let compute_to_env ~reduce ~unwind k e ens t =
 199    lazy (
 200     match t with
 201        Cic.Const _ as t -> unwind k e ens t
 202      | t -> reduce (k,e,ens,t,[]))
 203  end
 204 ;;
 205
 206 module LazyCallByNameStrategy =
 207  struct
 208   type stack_term = Cic.term lazy_t
 209   type env_term = Cic.term lazy_t
 210   type ens_term = Cic.term lazy_t
 211   let to_stack v = lazy v
 212   let to_stack_list l = List.map to_stack l
 213   let to_env v = lazy v
 214   let to_ens v = lazy v
 215   let from_stack ~unwind v = Lazy.force v
 216   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 217   let from_env v = Lazy.force v
 218   let from_ens v = Lazy.force v
 219   let stack_to_env ~reduce ~unwind v = v
 220   let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
 221   let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
 222  end
 223 ;;
 224
 225 module
 226  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
 227 =
 228  struct
 229   type stack_term = reduce:bool -> Cic.term
 230   type env_term = reduce:bool -> Cic.term
 231   type ens_term = reduce:bool -> Cic.term
 232   let to_stack v =
 233    let value = lazy v in
 234     fun ~reduce -> Lazy.force value
 235   let to_stack_list l = List.map to_stack l
 236   let to_env v =
 237    let value = lazy v in
 238     fun ~reduce -> Lazy.force value
 239   let to_ens v =
 240    let value = lazy v in
 241     fun ~reduce -> Lazy.force value
 242   let from_stack ~unwind v = (v ~reduce:false)
 243   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 244   let from_env v = (v ~reduce:true)
 245   let from_ens v = (v ~reduce:true)
 246   let stack_to_env ~reduce ~unwind v = v
 247   let compute_to_stack ~reduce ~unwind k e ens t =
 248    let svalue =
 249      lazy (
 250       match t with
 251          Cic.Const _ as t -> unwind k e ens t
 252        | t -> reduce (k,e,ens,t,[])
 253      ) in
 254    let lvalue =
 255     lazy (unwind k e ens t)
 256    in
 257     fun ~reduce ->
 258      if reduce then Lazy.force svalue else Lazy.force lvalue
 259   let compute_to_env ~reduce ~unwind k e ens t =
 260    let svalue =
 261      lazy (
 262       match t with
 263          Cic.Const _ as t -> unwind k e ens t
 264        | t -> reduce (k,e,ens,t,[])
 265      ) in
 266    let lvalue =
 267     lazy (unwind k e ens t)
 268    in
 269     fun ~reduce ->
 270      if reduce then Lazy.force svalue else Lazy.force lvalue
 271  end
 272 ;;
 273
 274 module ClosuresOnStackByValueFromEnvOrEnsStrategy =
 275  struct
 276   type stack_term =
 277    int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
 278   type env_term = Cic.term
 279   type ens_term = Cic.term
 280   let to_stack v = (0,[],[],v)
 281   let to_stack_list l = List.map to_stack l
 282   let to_env v = v
 283   let to_ens v = v
 284   let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
 285   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 286   let from_env v = v
 287   let from_ens v = v
 288   let stack_to_env ~reduce ~unwind (k,e,ens,t) = reduce (k,e,ens,t,[])
 289   let compute_to_env ~reduce ~unwind k e ens t =
 290    unwind k e ens t
 291   let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
 292  end
 293 ;;
 294
 295 module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
 296  struct
 297   type stack_term =
 298    int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
 299   type env_term = Cic.term
 300   type ens_term = Cic.term
 301   let to_stack v = (0,[],[],v)
 302   let to_stack_list l = List.map to_stack l
 303   let to_env v = v
 304   let to_ens v = v
 305   let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
 306   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 307   let from_env v = v
 308   let from_ens v = v
 309   let stack_to_env ~reduce ~unwind (k,e,ens,t) =
 310    match t with
 311       Cic.Const _ as t -> unwind k e ens t
 312     | t -> reduce (k,e,ens,t,[])
 313   let compute_to_env ~reduce ~unwind k e ens t =
 314    unwind k e ens t
 315   let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
 316  end
 317 ;;
 318
 319 module Reduction(RS : Strategy) =
 320  struct
 321   type env = RS.env_term list
 322   type ens = RS.ens_term Cic.explicit_named_substitution
 323   type stack = RS.stack_term list
 324   type config = int * env * ens * Cic.term * stack
 325
 326   (* k is the length of the environment e *)
 327   (* m is the current depth inside the term *)
 328   let unwind' m k e ens t =
 329    let module C = Cic in
 330    let module S = CicSubstitution in
 331     if k = 0 && ens = [] then
 332      t
 333     else
 334      let rec unwind_aux m =
 335       function
 336          C.Rel n as t ->
 337           if n <= m then t else
 338            let d =
 339             try
 340              Some (RS.from_env (List.nth e (n-m-1)))
 341             with _ -> None
 342            in
 343             (match d with
 344                 Some t' ->
 345                  if m = 0 then t' else S.lift m t'
 346               | None -> C.Rel (n-k)
 347             )
 348        | C.Var (uri,exp_named_subst) ->
 349 (*
 350 prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
 351 *)
 352          if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
 353           CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
 354          else
 355           let params =
 356            (match CicEnvironment.get_obj uri with
 357                C.Constant _ -> raise ReferenceToConstant
 358              | C.Variable (_,_,_,params) -> params
 359              | C.CurrentProof _ -> raise ReferenceToCurrentProof
 360              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 361            )
 362           in
 363            let exp_named_subst' =
 364             substaux_in_exp_named_subst params exp_named_subst m
 365            in
 366             C.Var (uri,exp_named_subst')
 367        | C.Meta (i,l) ->
 368           let l' =
 369            List.map
 370             (function
 371                 None -> None
 372               | Some t -> Some (unwind_aux m t)
 373             ) l
 374           in
 375            C.Meta (i, l')
 376        | C.Sort _ as t -> t
 377        | C.Implicit _ as t -> t
 378        | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
 379        | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
 380        | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
 381        | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
 382        | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
 383        | C.Const (uri,exp_named_subst) ->
 384           let params =
 385            (match CicEnvironment.get_obj uri with
 386                C.Constant (_,_,_,params) -> params
 387              | C.Variable _ -> raise ReferenceToVariable
 388              | C.CurrentProof (_,_,_,_,params) -> params
 389              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 390            )
 391           in
 392            let exp_named_subst' =
 393             substaux_in_exp_named_subst params exp_named_subst m
 394            in
 395             C.Const (uri,exp_named_subst')
 396        | C.MutInd (uri,i,exp_named_subst) ->
 397           let params =
 398            (match CicEnvironment.get_obj uri with
 399                C.Constant _ -> raise ReferenceToConstant
 400              | C.Variable _ -> raise ReferenceToVariable
 401              | C.CurrentProof _ -> raise ReferenceToCurrentProof
 402              | C.InductiveDefinition (_,params,_) -> params
 403            )
 404           in
 405            let exp_named_subst' =
 406             substaux_in_exp_named_subst params exp_named_subst m
 407            in
 408             C.MutInd (uri,i,exp_named_subst')
 409        | C.MutConstruct (uri,i,j,exp_named_subst) ->
 410           let params =
 411            (match CicEnvironment.get_obj uri with
 412                C.Constant _ -> raise ReferenceToConstant
 413              | C.Variable _ -> raise ReferenceToVariable
 414              | C.CurrentProof _ -> raise ReferenceToCurrentProof
 415              | C.InductiveDefinition (_,params,_) -> params
 416            )
 417           in
 418            let exp_named_subst' =
 419             substaux_in_exp_named_subst params exp_named_subst m
 420            in
 421             C.MutConstruct (uri,i,j,exp_named_subst')
 422        | C.MutCase (sp,i,outt,t,pl) ->
 423           C.MutCase (sp,i,unwind_aux m outt, unwind_aux m t,
 424            List.map (unwind_aux m) pl)
 425        | C.Fix (i,fl) ->
 426           let len = List.length fl in
 427           let substitutedfl =
 428            List.map
 429             (fun (name,i,ty,bo) ->
 430               (name, i, unwind_aux m ty, unwind_aux (m+len) bo))
 431              fl
 432           in
 433            C.Fix (i, substitutedfl)
 434        | C.CoFix (i,fl) ->
 435           let len = List.length fl in
 436           let substitutedfl =
 437            List.map
 438             (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo))
 439              fl
 440           in
 441            C.CoFix (i, substitutedfl)
 442      and substaux_in_exp_named_subst params exp_named_subst' m  =
 443   (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params
 444       let ens' =
 445        List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
 446   (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *)
 447         List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens
 448       in
 449       let rec filter_and_lift =
 450        function
 451           [] -> []
 452         | uri::tl ->
 453            let r = filter_and_lift tl in
 454             (try
 455               (uri,(List.assq uri ens'))::r
 456              with
 457               Not_found -> r
 458             )
 459       in
 460        filter_and_lift params
 461   *)
 462
 463   (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
 464   (*CSC: e' vero???? una veloce prova non sembra confermare la teoria        *)
 465
 466   (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
 467   (*CSC: codice altamente inefficiente *)
 468       let rec filter_and_lift already_instantiated =
 469        function
 470           [] -> []
 471         | (uri,t)::tl when
 472             List.for_all
 473              (function (uri',_)-> not (UriManager.eq uri uri')) exp_named_subst'
 474             &&
 475              not (List.mem uri already_instantiated)
 476             &&
 477              List.mem uri params
 478            ->
 479             (uri,CicSubstitution.lift m (RS.from_ens t)) ::
 480              (filter_and_lift (uri::already_instantiated) tl)
 481         | _::tl -> filter_and_lift already_instantiated tl
 482 (*
 483         | (uri,_)::tl ->
 484 prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
 485 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
 486 prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
 487 if List.mem uri params then prerr_endline "---- OK2" ;
 488         filter_and_lift tl
 489 *)
 490       in
 491        List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
 492         (filter_and_lift [] (List.rev ens))
 493      in
 494       unwind_aux m t
 495   ;;
 496
 497   let unwind =
 498    unwind' 0
 499   ;;
 500
 501   let reduce ?(subst = []) context : config -> Cic.term =
 502    let module C = Cic in
 503    let module S = CicSubstitution in
 504    let rec reduce =
 505     function
 506        (k, e, _, (C.Rel n as t), s) ->
 507         let d =
 508          try
 509           Some (RS.from_env (List.nth e (n-1)))
 510          with
 511           _ ->
 512            try
 513             begin
 514              match List.nth context (n - 1 - k) with
 515                 None -> assert false
 516               | Some (_,C.Decl _) -> None
 517               | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x)
 518             end
 519            with
 520             _ -> None
 521         in
 522          (match d with
 523              Some t' -> reduce (0,[],[],t',s)
 524            | None ->
 525               if s = [] then
 526                C.Rel (n-k)
 527               else C.Appl (C.Rel (n-k)::(RS.from_stack_list ~unwind s))
 528          )
 529      | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) ->
 530          if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
 531           reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
 532          else
 533           (match CicEnvironment.get_obj uri with
 534               C.Constant _ -> raise ReferenceToConstant
 535             | C.CurrentProof _ -> raise ReferenceToCurrentProof
 536             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 537             | C.Variable (_,None,_,_) ->
 538                let t' = unwind k e ens t in
 539                 if s = [] then t' else
 540                  C.Appl (t'::(RS.from_stack_list ~unwind s))
 541             | C.Variable (_,Some body,_,_) ->
 542                let ens' = push_exp_named_subst k e ens exp_named_subst in
 543                 reduce (0, [], ens', body, s)
 544           )
 545      | (k, e, ens, (C.Meta (n,l) as t), s) ->
 546         (try
 547            let (_, term) = CicUtil.lookup_subst n subst in
 548            reduce (k, e, ens,CicSubstitution.lift_meta l term,s)
 549          with  CicUtil.Subst_not_found _ ->
 550            let t' = unwind k e ens t in
 551            if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
 552      | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
 553      | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
 554      | (k, e, ens, (C.Cast (te,ty) as t), s) ->
 555         reduce (k, e, ens, te, s) (* s should be empty *)
 556      | (k, e, ens, (C.Prod _ as t), s) ->
 557          unwind k e ens t (* s should be empty *)
 558      | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t'
 559      | (k, e, ens, C.Lambda (_,_,t), p::s) ->
 560          reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
 561      | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
 562         let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
 563          reduce (k+1, m'::e, ens, t, s)
 564      | (_, _, _, C.Appl [], _) -> assert false
 565      | (k, e, ens, C.Appl (he::tl), s) ->
 566         let tl' =
 567          List.map
 568           (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl
 569         in
 570          reduce (k, e, ens, he, (List.append tl') s)
 571   (* CSC: Old Dead Code
 572      | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s)
 573      | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)
 574      | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s)
 575      | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
 576   (* strict evaluation, but constants are NOT unfolded *)
 577         let red =
 578          function
 579             C.Const _ as t -> unwind k e ens t
 580           | t -> reduce (k,e,ens,t,[])
 581         in
 582          let tl' = List.map red tl in
 583           reduce (k, e, ens, he , List.append tl' s)
 584      | (k, e, ens, C.Appl l, s) ->
 585          C.Appl (List.append (List.map (unwind k e ens) l) s)
 586   *)
 587      | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
 588         (match CicEnvironment.get_obj uri with
 589             C.Constant (_,Some body,_,_) ->
 590              let ens' = push_exp_named_subst k e ens exp_named_subst in
 591               (* constants are closed *)
 592               reduce (0, [], ens', body, s)
 593           | C.Constant (_,None,_,_) ->
 594              let t' = unwind k e ens t in
 595               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 596           | C.Variable _ -> raise ReferenceToVariable
 597           | C.CurrentProof (_,_,body,_,_) ->
 598              let ens' = push_exp_named_subst k e ens exp_named_subst in
 599               (* constants are closed *)
 600               reduce (0, [], ens', body, s)
 601           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 602         )
 603      | (k, e, ens, (C.MutInd _ as t),s) ->
 604         let t' = unwind k e ens t in
 605          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 606      | (k, e, ens, (C.MutConstruct _ as t),s) ->
 607          let t' = unwind k e ens t in
 608           if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 609      | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
 610         let decofix =
 611          function
 612             C.CoFix (i,fl) as t ->
 613              let (_,_,body) = List.nth fl i in
 614               let body' =
 615                let counter = ref (List.length fl) in
 616                 List.fold_right
 617                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 618                  fl
 619                  body
 620               in
 621                (* the term is the result of a reduction; *)
 622                (* so it is already unwinded.             *)
 623                reduce (0,[],[],body',[])
 624           | C.Appl (C.CoFix (i,fl) :: tl) ->
 625              let (_,_,body) = List.nth fl i in
 626               let body' =
 627                let counter = ref (List.length fl) in
 628                 List.fold_right
 629                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 630                  fl
 631                  body
 632               in
 633                (* the term is the result of a reduction; *)
 634                (* so it is already unwinded.             *)
 635                reduce (0,[],[],body',RS.to_stack_list tl)
 636           | t -> t
 637         in
 638          (match decofix (reduce (k,e,ens,term,[])) with
 639              C.MutConstruct (_,_,j,_) ->
 640               reduce (k, e, ens, (List.nth pl (j-1)), s)
 641            | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 642               let (arity, r) =
 643                match CicEnvironment.get_obj mutind with
 644                   C.InductiveDefinition (tl,ingredients,r) ->
 645                     let (_,_,arity,_) = List.nth tl i in
 646                      (arity,r)
 647                 | _ -> raise WrongUriToInductiveDefinition
 648               in
 649                let ts =
 650                 let num_to_eat = r in
 651                  let rec eat_first =
 652                   function
 653                      (0,l) -> l
 654                    | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 655                    | _ -> raise (Impossible 5)
 656                  in
 657                   eat_first (num_to_eat,tl)
 658                in
 659                 (* ts are already unwinded because they are a sublist of tl *)
 660                 reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
 661            | C.Cast _ | C.Implicit _ ->
 662               raise (Impossible 2) (* we don't trust our whd ;-) *)
 663            | _ ->
 664              let t' = unwind k e ens t in
 665               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 666          )
 667      | (k, e, ens, (C.Fix (i,fl) as t), s) ->
 668         let (_,recindex,_,body) = List.nth fl i in
 669          let recparam =
 670           try
 671            Some (RS.from_stack ~unwind (List.nth s recindex))
 672           with
 673            _ -> None
 674          in
 675           (match recparam with
 676               Some recparam ->
 677                (match reduce (0,[],[],recparam,[]) with
 678                    (* match recparam with *)
 679                    C.MutConstruct _
 680                  | C.Appl ((C.MutConstruct _)::_) ->
 681                     (* OLD
 682                     let body' =
 683                      let counter = ref (List.length fl) in
 684                       List.fold_right
 685                        (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 686                        fl
 687                        body
 688                     in
 689                      reduce (k, e, ens, body', s) *)
 690                     (* NEW *)
 691                     let leng = List.length fl in
 692                     let fl' =
 693                      let unwind_fl (name,recindex,typ,body) =
 694                       (name,recindex,unwind k e ens typ,
 695                         unwind' leng k e ens body)
 696                      in
 697                       List.map unwind_fl fl
 698                     in
 699                      let new_env =
 700                       let counter = ref 0 in
 701                       let rec build_env e =
 702                        if !counter = leng then e
 703                        else
 704                         (incr counter ;
 705                          build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e))
 706                       in
 707                        build_env e
 708                      in
 709                       reduce (k+leng, new_env, ens, body, s)
 710                  | _ ->
 711                    let t' = unwind k e ens t in
 712                     if s = [] then t' else
 713                      C.Appl (t'::(RS.from_stack_list ~unwind s))
 714                )
 715             | None ->
 716                let t' = unwind k e ens t in
 717                 if s = [] then t' else
 718                  C.Appl (t'::(RS.from_stack_list ~unwind s))
 719           )
 720      | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
 721         let t' = unwind k e ens t in
 722          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 723    and push_exp_named_subst k e ens =
 724     function
 725        [] -> ens
 726      | (uri,t)::tl ->
 727          push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
 728    in
 729     reduce
 730   ;;
 731
 732   let rec whd ?(subst=[]) context t = reduce ~subst context (0, [], [], t, []);;
 733
 734 (* DEBUGGING ONLY
 735 let whd context t =
 736  let res = whd context t in
 737  let rescsc = CicReductionNaif.whd context t in
 738   if not (CicReductionNaif.are_convertible context res rescsc) then
 739    begin
 740     prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
 741     flush stderr ;
 742     prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
 743     flush stderr ;
 744     prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
 745     flush stderr ;
 746 CicReductionNaif.fdebug := 0 ;
 747 let _ =  CicReductionNaif.are_convertible context res rescsc in
 748     assert false ;
 749    end
 750   else
 751    res
 752 ;;
 753 *)
 754  end
 755 ;;
 756
 757
 758 (*
 759 module R = Reduction CallByNameStrategy;;
 760 module R = Reduction CallByValueStrategy;;
 761 module R = Reduction CallByValueStrategyByNameOnConstants;;
 762 module R = Reduction LazyCallByValueStrategy;;
 763 module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
 764 module R = Reduction LazyCallByNameStrategy;;
 765 module R = Reduction
 766  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
 767 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
 768 module R = Reduction
 769  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
 770 *)
 771 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
 772
 773 let whd = R.whd;;
 774
 775 (* t1, t2 must be well-typed *)
 776 let are_convertible ?(subst=[]) ?(metasenv=[]) =
 777  let module U = UriManager in
 778  let rec aux test_equality_only context t1 t2 =
 779   let aux2 test_equality_only t1 t2 =
 780    (* this trivial euristic cuts down the total time of about five times ;-) *)
 781    (* this because most of the time t1 and t2 are "sintactically" the same   *)
 782    if t1 = t2 then
 783     true
 784    else
 785     begin
 786      let module C = Cic in
 787        match (t1,t2) with
 788           (C.Rel n1, C.Rel n2) -> n1 = n2
 789         | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
 790             U.eq uri1 uri2 &&
 791              (try
 792                List.fold_right2
 793                 (fun (uri1,x) (uri2,y) b ->
 794                   U.eq uri1 uri2 && aux test_equality_only context x y && b
 795                 ) exp_named_subst1 exp_named_subst2 true
 796               with
 797                Invalid_argument _ -> false
 798              )
 799         | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
 800             n1 = n2 &&
 801              let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
 802              let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
 803              List.fold_left2
 804               (fun b t1 t2 ->
 805                 b &&
 806                  match t1,t2 with
 807                     None,_
 808                   | _,None  -> true
 809                   | Some t1',Some t2' -> aux test_equality_only context t1' t2'
 810               ) true l1 l2
 811           (* TASSI: CONSTRAINTS *)
 812         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
 813             CicUniv.add_eq t2 t1
 814           (* TASSI: CONSTRAINTS *)
 815         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 816             CicUniv.add_ge t2 t1
 817           (* TASSI: CONSTRAINTS *)
 818         | (C.Sort s1, C.Sort (C.Type _)) -> not test_equality_only
 819           (* TASSI: CONSTRAINTS *)
 820         | (C.Sort s1, C.Sort s2) -> s1 = s2
 821         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 822            aux true context s1 s2 &&
 823             aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2
 824         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
 825            aux test_equality_only context s1 s2 &&
 826             aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2
 827         | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
 828            aux test_equality_only context s1 s2 &&
 829             aux test_equality_only
 830              ((Some (name1, (C.Def (s1,None))))::context) t1 t2
 831         | (C.Appl l1, C.Appl l2) ->
 832            (try
 833              List.fold_right2
 834               (fun  x y b -> aux test_equality_only context x y && b) l1 l2 true
 835             with
 836              Invalid_argument _ -> false
 837            )
 838         | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
 839             U.eq uri1 uri2 &&
 840              (try
 841                List.fold_right2
 842                 (fun (uri1,x) (uri2,y) b ->
 843                   U.eq uri1 uri2 && aux test_equality_only context x y && b
 844                 ) exp_named_subst1 exp_named_subst2 true
 845               with
 846                Invalid_argument _ -> false
 847              )
 848         | (C.MutInd (uri1,i1,exp_named_subst1),
 849            C.MutInd (uri2,i2,exp_named_subst2)
 850           ) ->
 851             U.eq uri1 uri2 && i1 = i2 &&
 852              (try
 853                List.fold_right2
 854                 (fun (uri1,x) (uri2,y) b ->
 855                   U.eq uri1 uri2 && aux test_equality_only context x y && b
 856                 ) exp_named_subst1 exp_named_subst2 true
 857               with
 858                Invalid_argument _ -> false
 859              )
 860         | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 861            C.MutConstruct (uri2,i2,j2,exp_named_subst2)
 862           ) ->
 863             U.eq uri1 uri2 && i1 = i2 && j1 = j2 &&
 864              (try
 865                List.fold_right2
 866                 (fun (uri1,x) (uri2,y) b ->
 867                   U.eq uri1 uri2 && aux test_equality_only context x y && b
 868                 ) exp_named_subst1 exp_named_subst2 true
 869               with
 870                Invalid_argument _ -> false
 871              )
 872         | (C.MutCase (uri1,i1,outtype1,term1,pl1),
 873            C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
 874             U.eq uri1 uri2 && i1 = i2 &&
 875              aux test_equality_only context outtype1 outtype2 &&
 876              aux test_equality_only context term1 term2 &&
 877              List.fold_right2
 878               (fun x y b -> b && aux test_equality_only context x y)
 879               pl1 pl2 true
 880         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
 881            let tys =
 882             List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
 883            in
 884             i1 = i2 &&
 885              List.fold_right2
 886               (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
 887                 b && recindex1 = recindex2 &&
 888                  aux test_equality_only context ty1 ty2 &&
 889                  aux test_equality_only (tys@context) bo1 bo2)
 890               fl1 fl2 true
 891         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
 892            let tys =
 893             List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
 894            in
 895             i1 = i2 &&
 896              List.fold_right2
 897               (fun (_,ty1,bo1) (_,ty2,bo2) b ->
 898                 b && aux test_equality_only context ty1 ty2 &&
 899                  aux test_equality_only (tys@context) bo1 bo2)
 900               fl1 fl2 true
 901         | (C.Cast _, _) | (_, C.Cast _)
 902         | (C.Implicit _, _) | (_, C.Implicit _) ->
 903             assert false
 904         | (_,_) -> false
 905     end
 906   in
 907    if aux2 test_equality_only t1 t2 then true
 908    else
 909      begin
 910      debug t1 [t2] "PREWHD";
 911      (*
 912      (match t1 with
 913          Cic.Meta _ ->
 914            prerr_endline (CicPp.ppterm t1);
 915            prerr_endline (CicPp.ppterm (whd ~subst context t1));
 916            prerr_endline (CicPp.ppterm t2);
 917            prerr_endline (CicPp.ppterm (whd ~subst context t2))
 918        | _ -> ()); *)
 919      let t1' = whd ~subst context t1 in
 920      let t2' = whd ~subst context t2 in
 921       debug t1' [t2'] "POSTWHD";
 922       aux2 test_equality_only t1' t2'
 923     end
 924  in
 925   aux false
 926 ;;