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 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 _ as t), s) ->
 546         let t' = unwind k e ens t in
 547          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 548      | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
 549      | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
 550      | (k, e, ens, (C.Cast (te,ty) as t), s) ->
 551         reduce (k, e, ens, te, s) (* s should be empty *)
 552      | (k, e, ens, (C.Prod _ as t), s) ->
 553          unwind k e ens t (* s should be empty *)
 554      | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t'
 555      | (k, e, ens, C.Lambda (_,_,t), p::s) ->
 556          reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
 557      | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
 558         let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
 559          reduce (k+1, m'::e, ens, t, s)
 560      | (_, _, _, C.Appl [], _) -> assert false
 561      | (k, e, ens, C.Appl (he::tl), s) ->
 562         let tl' =
 563          List.map
 564           (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl
 565         in
 566          reduce (k, e, ens, he, (List.append tl') s)
 567   (* CSC: Old Dead Code
 568      | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s)
 569      | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)
 570      | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s)
 571      | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
 572   (* strict evaluation, but constants are NOT unfolded *)
 573         let red =
 574          function
 575             C.Const _ as t -> unwind k e ens t
 576           | t -> reduce (k,e,ens,t,[])
 577         in
 578          let tl' = List.map red tl in
 579           reduce (k, e, ens, he , List.append tl' s)
 580      | (k, e, ens, C.Appl l, s) ->
 581          C.Appl (List.append (List.map (unwind k e ens) l) s)
 582   *)
 583      | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
 584         (match CicEnvironment.get_obj uri with
 585             C.Constant (_,Some body,_,_) ->
 586              let ens' = push_exp_named_subst k e ens exp_named_subst in
 587               (* constants are closed *)
 588               reduce (0, [], ens', body, s)
 589           | C.Constant (_,None,_,_) ->
 590              let t' = unwind k e ens t in
 591               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 592           | C.Variable _ -> raise ReferenceToVariable
 593           | C.CurrentProof (_,_,body,_,_) ->
 594              let ens' = push_exp_named_subst k e ens exp_named_subst in
 595               (* constants are closed *)
 596               reduce (0, [], ens', body, s)
 597           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 598         )
 599      | (k, e, ens, (C.MutInd _ as t),s) ->
 600         let t' = unwind k e ens t in
 601          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 602      | (k, e, ens, (C.MutConstruct _ as t),s) ->
 603          let t' = unwind k e ens t in
 604           if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 605      | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
 606         let decofix =
 607          function
 608             C.CoFix (i,fl) as t ->
 609              let (_,_,body) = List.nth fl i in
 610               let body' =
 611                let counter = ref (List.length fl) in
 612                 List.fold_right
 613                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 614                  fl
 615                  body
 616               in
 617                (* the term is the result of a reduction; *)
 618                (* so it is already unwinded.             *)
 619                reduce (0,[],[],body',[])
 620           | C.Appl (C.CoFix (i,fl) :: tl) ->
 621              let (_,_,body) = List.nth fl i in
 622               let body' =
 623                let counter = ref (List.length fl) in
 624                 List.fold_right
 625                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 626                  fl
 627                  body
 628               in
 629                (* the term is the result of a reduction; *)
 630                (* so it is already unwinded.             *)
 631                reduce (0,[],[],body',RS.to_stack_list tl)
 632           | t -> t
 633         in
 634          (match decofix (reduce (k,e,ens,term,[])) with
 635              C.MutConstruct (_,_,j,_) ->
 636               reduce (k, e, ens, (List.nth pl (j-1)), s)
 637            | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 638               let (arity, r) =
 639                match CicEnvironment.get_obj mutind with
 640                   C.InductiveDefinition (tl,ingredients,r) ->
 641                     let (_,_,arity,_) = List.nth tl i in
 642                      (arity,r)
 643                 | _ -> raise WrongUriToInductiveDefinition
 644               in
 645                let ts =
 646                 let num_to_eat = r in
 647                  let rec eat_first =
 648                   function
 649                      (0,l) -> l
 650                    | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 651                    | _ -> raise (Impossible 5)
 652                  in
 653                   eat_first (num_to_eat,tl)
 654                in
 655                 (* ts are already unwinded because they are a sublist of tl *)
 656                 reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
 657            | C.Cast _ | C.Implicit _ ->
 658               raise (Impossible 2) (* we don't trust our whd ;-) *)
 659            | _ ->
 660              let t' = unwind k e ens t in
 661               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 662          )
 663      | (k, e, ens, (C.Fix (i,fl) as t), s) ->
 664         let (_,recindex,_,body) = List.nth fl i in
 665          let recparam =
 666           try
 667            Some (RS.from_stack ~unwind (List.nth s recindex))
 668           with
 669            _ -> None
 670          in
 671           (match recparam with
 672               Some recparam ->
 673                (match reduce (0,[],[],recparam,[]) with
 674                    (* match recparam with *)
 675                    C.MutConstruct _
 676                  | C.Appl ((C.MutConstruct _)::_) ->
 677                     (* OLD
 678                     let body' =
 679                      let counter = ref (List.length fl) in
 680                       List.fold_right
 681                        (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 682                        fl
 683                        body
 684                     in
 685                      reduce (k, e, ens, body', s) *)
 686                     (* NEW *)
 687                     let leng = List.length fl in
 688                     let fl' =
 689                      let unwind_fl (name,recindex,typ,body) =
 690                       (name,recindex,unwind k e ens typ,
 691                         unwind' leng k e ens body)
 692                      in
 693                       List.map unwind_fl fl
 694                     in
 695                      let new_env =
 696                       let counter = ref 0 in
 697                       let rec build_env e =
 698                        if !counter = leng then e
 699                        else
 700                         (incr counter ;
 701                          build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e))
 702                       in
 703                        build_env e
 704                      in
 705                       reduce (k+leng, new_env, ens, body, s)
 706                  | _ ->
 707                    let t' = unwind k e ens t in
 708                     if s = [] then t' else
 709                      C.Appl (t'::(RS.from_stack_list ~unwind s))
 710                )
 711             | None ->
 712                let t' = unwind k e ens t in
 713                 if s = [] then t' else
 714                  C.Appl (t'::(RS.from_stack_list ~unwind s))
 715           )
 716      | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
 717         let t' = unwind k e ens t in
 718          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 719    and push_exp_named_subst k e ens =
 720     function
 721        [] -> ens
 722      | (uri,t)::tl ->
 723          push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
 724    in
 725     reduce
 726   ;;
 727
 728   let rec whd context t = reduce context (0, [], [], t, []);;
 729
 730 (* DEBUGGING ONLY
 731 let whd context t =
 732  let res = whd context t in
 733  let rescsc = CicReductionNaif.whd context t in
 734   if not (CicReductionNaif.are_convertible context res rescsc) then
 735    begin
 736     prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
 737     flush stderr ;
 738     prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
 739     flush stderr ;
 740     prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
 741     flush stderr ;
 742 CicReductionNaif.fdebug := 0 ;
 743 let _ =  CicReductionNaif.are_convertible context res rescsc in
 744     assert false ;
 745    end
 746   else
 747    res
 748 ;;
 749 *)
 750  end
 751 ;;
 752
 753
 754 (*
 755 module R = Reduction CallByNameStrategy;;
 756 module R = Reduction CallByValueStrategy;;
 757 module R = Reduction CallByValueStrategyByNameOnConstants;;
 758 module R = Reduction LazyCallByValueStrategy;;
 759 module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
 760 module R = Reduction LazyCallByNameStrategy;;
 761 module R = Reduction
 762  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
 763 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
 764 module R = Reduction
 765  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
 766 *)
 767 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
 768
 769 let whd = R.whd;;
 770
 771 (* t1, t2 must be well-typed *)
 772 let are_convertible =
 773  let module U = UriManager in
 774  let rec aux test_equality_only context t1 t2 =
 775   let aux2 test_equality_only t1 t2 =
 776    (* this trivial euristic cuts down the total time of about five times ;-) *)
 777    (* this because most of the time t1 and t2 are "sintactically" the same   *)
 778    if t1 = t2 then
 779     true
 780    else
 781     begin
 782      let module C = Cic in
 783        match (t1,t2) with
 784           (C.Rel n1, C.Rel n2) -> n1 = n2
 785         | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
 786             U.eq uri1 uri2 &&
 787              (try
 788                List.fold_right2
 789                 (fun (uri1,x) (uri2,y) b ->
 790                   U.eq uri1 uri2 && aux test_equality_only context x y && b
 791                 ) exp_named_subst1 exp_named_subst2 true
 792               with
 793                Invalid_argument _ -> false
 794              )
 795         | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
 796             n1 = n2 &&
 797              List.fold_left2
 798               (fun b t1 t2 ->
 799                 b &&
 800                  match t1,t2 with
 801                     None,_
 802                   | _,None  -> true
 803                   | Some t1',Some t2' -> aux test_equality_only context t1' t2'
 804               ) true l1 l2
 805           (* TASSI: CONSTRAINTS *)
 806         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
 807             CicUniv.add_eq t2 t1
 808           (* TASSI: CONSTRAINTS *)
 809         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 810             CicUniv.add_ge t2 t1
 811           (* TASSI: CONSTRAINTS *)
 812         | (C.Sort s1, C.Sort (C.Type _)) -> not test_equality_only
 813           (* TASSI: CONSTRAINTS *)
 814         | (C.Sort s1, C.Sort s2) -> s1 = s2
 815         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 816            aux true context s1 s2 &&
 817             aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2
 818         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
 819            aux test_equality_only context s1 s2 &&
 820             aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2
 821         | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
 822            aux test_equality_only context s1 s2 &&
 823             aux test_equality_only
 824              ((Some (name1, (C.Def (s1,None))))::context) t1 t2
 825         | (C.Appl l1, C.Appl l2) ->
 826            (try
 827              List.fold_right2
 828               (fun  x y b -> aux test_equality_only context x y && b) l1 l2 true
 829             with
 830              Invalid_argument _ -> false
 831            )
 832         | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
 833             U.eq uri1 uri2 &&
 834              (try
 835                List.fold_right2
 836                 (fun (uri1,x) (uri2,y) b ->
 837                   U.eq uri1 uri2 && aux test_equality_only context x y && b
 838                 ) exp_named_subst1 exp_named_subst2 true
 839               with
 840                Invalid_argument _ -> false
 841              )
 842         | (C.MutInd (uri1,i1,exp_named_subst1),
 843            C.MutInd (uri2,i2,exp_named_subst2)
 844           ) ->
 845             U.eq uri1 uri2 && i1 = i2 &&
 846              (try
 847                List.fold_right2
 848                 (fun (uri1,x) (uri2,y) b ->
 849                   U.eq uri1 uri2 && aux test_equality_only context x y && b
 850                 ) exp_named_subst1 exp_named_subst2 true
 851               with
 852                Invalid_argument _ -> false
 853              )
 854         | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 855            C.MutConstruct (uri2,i2,j2,exp_named_subst2)
 856           ) ->
 857             U.eq uri1 uri2 && i1 = i2 && j1 = j2 &&
 858              (try
 859                List.fold_right2
 860                 (fun (uri1,x) (uri2,y) b ->
 861                   U.eq uri1 uri2 && aux test_equality_only context x y && b
 862                 ) exp_named_subst1 exp_named_subst2 true
 863               with
 864                Invalid_argument _ -> false
 865              )
 866         | (C.MutCase (uri1,i1,outtype1,term1,pl1),
 867            C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
 868             U.eq uri1 uri2 && i1 = i2 &&
 869              aux test_equality_only context outtype1 outtype2 &&
 870              aux test_equality_only context term1 term2 &&
 871              List.fold_right2
 872               (fun x y b -> b && aux test_equality_only context x y)
 873               pl1 pl2 true
 874         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
 875            let tys =
 876             List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
 877            in
 878             i1 = i2 &&
 879              List.fold_right2
 880               (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
 881                 b && recindex1 = recindex2 &&
 882                  aux test_equality_only context ty1 ty2 &&
 883                  aux test_equality_only (tys@context) bo1 bo2)
 884               fl1 fl2 true
 885         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
 886            let tys =
 887             List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
 888            in
 889             i1 = i2 &&
 890              List.fold_right2
 891               (fun (_,ty1,bo1) (_,ty2,bo2) b ->
 892                 b && aux test_equality_only context ty1 ty2 &&
 893                  aux test_equality_only (tys@context) bo1 bo2)
 894               fl1 fl2 true
 895         | (C.Cast _, _) | (_, C.Cast _)
 896         | (C.Implicit _, _) | (_, C.Implicit _) ->
 897             assert false
 898         | (_,_) -> false
 899     end
 900   in
 901    if aux2 test_equality_only t1 t2 then true
 902    else
 903     begin
 904      debug t1 [t2] "PREWHD";
 905      let t1' = whd context t1 in
 906      let t2' = whd context t2 in
 907       debug t1' [t2'] "POSTWHD";
 908       aux2 test_equality_only t1' t2'
 909     end
 910  in
 911   aux false
 912 ;;