helm/ocaml/cic_proof_checking/cicReduction.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             let o,_ =
 357               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 358             in
 359            (match o with
 360                C.Constant _ -> raise ReferenceToConstant
 361              | C.Variable (_,_,_,params,_) -> params
 362              | C.CurrentProof _ -> raise ReferenceToCurrentProof
 363              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 364            )
 365           in
 366            let exp_named_subst' =
 367             substaux_in_exp_named_subst params exp_named_subst m
 368            in
 369             C.Var (uri,exp_named_subst')
 370        | C.Meta (i,l) ->
 371           let l' =
 372            List.map
 373             (function
 374                 None -> None
 375               | Some t -> Some (unwind_aux m t)
 376             ) l
 377           in
 378            C.Meta (i, l')
 379        | C.Sort _ as t -> t
 380        | C.Implicit _ as t -> t
 381        | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
 382        | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
 383        | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
 384        | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
 385        | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
 386        | C.Const (uri,exp_named_subst) ->
 387           let params =
 388             let o,_ =
 389               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 390             in
 391            (match o with
 392                C.Constant (_,_,_,params,_) -> params
 393              | C.Variable _ -> raise ReferenceToVariable
 394              | C.CurrentProof (_,_,_,_,params,_) -> params
 395              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 396            )
 397           in
 398            let exp_named_subst' =
 399             substaux_in_exp_named_subst params exp_named_subst m
 400            in
 401             C.Const (uri,exp_named_subst')
 402        | C.MutInd (uri,i,exp_named_subst) ->
 403           let params =
 404             let o,_ =
 405               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 406             in
 407            (match o with
 408                C.Constant _ -> raise ReferenceToConstant
 409              | C.Variable _ -> raise ReferenceToVariable
 410              | C.CurrentProof _ -> raise ReferenceToCurrentProof
 411              | C.InductiveDefinition (_,params,_,_) -> params
 412            )
 413           in
 414            let exp_named_subst' =
 415             substaux_in_exp_named_subst params exp_named_subst m
 416            in
 417             C.MutInd (uri,i,exp_named_subst')
 418        | C.MutConstruct (uri,i,j,exp_named_subst) ->
 419           let params =
 420             let o,_ =
 421               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 422             in
 423            (match o with
 424                C.Constant _ -> raise ReferenceToConstant
 425              | C.Variable _ -> raise ReferenceToVariable
 426              | C.CurrentProof _ -> raise ReferenceToCurrentProof
 427              | C.InductiveDefinition (_,params,_,_) -> params
 428            )
 429           in
 430            let exp_named_subst' =
 431             substaux_in_exp_named_subst params exp_named_subst m
 432            in
 433             C.MutConstruct (uri,i,j,exp_named_subst')
 434        | C.MutCase (sp,i,outt,t,pl) ->
 435           C.MutCase (sp,i,unwind_aux m outt, unwind_aux m t,
 436            List.map (unwind_aux m) pl)
 437        | C.Fix (i,fl) ->
 438           let len = List.length fl in
 439           let substitutedfl =
 440            List.map
 441             (fun (name,i,ty,bo) ->
 442               (name, i, unwind_aux m ty, unwind_aux (m+len) bo))
 443              fl
 444           in
 445            C.Fix (i, substitutedfl)
 446        | C.CoFix (i,fl) ->
 447           let len = List.length fl in
 448           let substitutedfl =
 449            List.map
 450             (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo))
 451              fl
 452           in
 453            C.CoFix (i, substitutedfl)
 454      and substaux_in_exp_named_subst params exp_named_subst' m  =
 455   (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params
 456       let ens' =
 457        List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
 458   (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *)
 459         List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens
 460       in
 461       let rec filter_and_lift =
 462        function
 463           [] -> []
 464         | uri::tl ->
 465            let r = filter_and_lift tl in
 466             (try
 467               (uri,(List.assq uri ens'))::r
 468              with
 469               Not_found -> r
 470             )
 471       in
 472        filter_and_lift params
 473   *)
 474
 475   (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
 476   (*CSC: e' vero???? una veloce prova non sembra confermare la teoria        *)
 477
 478   (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
 479   (*CSC: codice altamente inefficiente *)
 480       let rec filter_and_lift already_instantiated =
 481        function
 482           [] -> []
 483         | (uri,t)::tl when
 484             List.for_all
 485              (function (uri',_)-> not (UriManager.eq uri uri')) exp_named_subst'
 486             &&
 487              not (List.mem uri already_instantiated)
 488             &&
 489              List.mem uri params
 490            ->
 491             (uri,CicSubstitution.lift m (RS.from_ens t)) ::
 492              (filter_and_lift (uri::already_instantiated) tl)
 493         | _::tl -> filter_and_lift already_instantiated tl
 494 (*
 495         | (uri,_)::tl ->
 496 prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
 497 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
 498 prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
 499 if List.mem uri params then prerr_endline "---- OK2" ;
 500         filter_and_lift tl
 501 *)
 502       in
 503        List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
 504         (filter_and_lift [] (List.rev ens))
 505      in
 506       unwind_aux m t
 507   ;;
 508
 509   let unwind =
 510    unwind' 0
 511   ;;
 512
 513   let reduce ?(subst = []) context : config -> Cic.term =
 514    let module C = Cic in
 515    let module S = CicSubstitution in
 516    let rec reduce =
 517     function
 518        (k, e, _, (C.Rel n as t), s) ->
 519         let d =
 520          try
 521           Some (RS.from_env (List.nth e (n-1)))
 522          with
 523           _ ->
 524            try
 525             begin
 526              match List.nth context (n - 1 - k) with
 527                 None -> assert false
 528               | Some (_,C.Decl _) -> None
 529               | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x)
 530             end
 531            with
 532             _ -> None
 533         in
 534          (match d with
 535              Some t' -> reduce (0,[],[],t',s)
 536            | None ->
 537               if s = [] then
 538                C.Rel (n-k)
 539               else C.Appl (C.Rel (n-k)::(RS.from_stack_list ~unwind s))
 540          )
 541      | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) ->
 542          if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
 543           reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
 544          else
 545           ( let o,_ =
 546               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 547             in
 548             match o with
 549               C.Constant _ -> raise ReferenceToConstant
 550             | C.CurrentProof _ -> raise ReferenceToCurrentProof
 551             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 552             | C.Variable (_,None,_,_,_) ->
 553                let t' = unwind k e ens t in
 554                 if s = [] then t' else
 555                  C.Appl (t'::(RS.from_stack_list ~unwind s))
 556             | C.Variable (_,Some body,_,_,_) ->
 557                let ens' = push_exp_named_subst k e ens exp_named_subst in
 558                 reduce (0, [], ens', body, s)
 559           )
 560      | (k, e, ens, (C.Meta (n,l) as t), s) ->
 561         (try
 562            let (_, term,_) = CicUtil.lookup_subst n subst in
 563            reduce (k, e, ens,CicSubstitution.subst_meta l term,s)
 564          with  CicUtil.Subst_not_found _ ->
 565            let t' = unwind k e ens t in
 566            if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
 567      | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
 568      | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
 569      | (k, e, ens, (C.Cast (te,ty) as t), s) ->
 570         reduce (k, e, ens, te, s) (* s should be empty *)
 571      | (k, e, ens, (C.Prod _ as t), s) ->
 572          unwind k e ens t (* s should be empty *)
 573      | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t'
 574      | (k, e, ens, C.Lambda (_,_,t), p::s) ->
 575          reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
 576      | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
 577         let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
 578          reduce (k+1, m'::e, ens, t, s)
 579      | (_, _, _, C.Appl [], _) -> assert false
 580      | (k, e, ens, C.Appl (he::tl), s) ->
 581         let tl' =
 582          List.map
 583           (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl
 584         in
 585          reduce (k, e, ens, he, (List.append tl') s)
 586   (* CSC: Old Dead Code
 587      | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s)
 588      | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)
 589      | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s)
 590      | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
 591   (* strict evaluation, but constants are NOT unfolded *)
 592         let red =
 593          function
 594             C.Const _ as t -> unwind k e ens t
 595           | t -> reduce (k,e,ens,t,[])
 596         in
 597          let tl' = List.map red tl in
 598           reduce (k, e, ens, he , List.append tl' s)
 599      | (k, e, ens, C.Appl l, s) ->
 600          C.Appl (List.append (List.map (unwind k e ens) l) s)
 601   *)
 602      | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
 603         (let o,_ =
 604            CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 605          in
 606           match o with
 607             C.Constant (_,Some body,_,_,_) ->
 608              let ens' = push_exp_named_subst k e ens exp_named_subst in
 609               (* constants are closed *)
 610               reduce (0, [], ens', body, s)
 611           | C.Constant (_,None,_,_,_) ->
 612              let t' = unwind k e ens t in
 613               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 614           | C.Variable _ -> raise ReferenceToVariable
 615           | C.CurrentProof (_,_,body,_,_,_) ->
 616              let ens' = push_exp_named_subst k e ens exp_named_subst in
 617               (* constants are closed *)
 618               reduce (0, [], ens', body, s)
 619           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 620         )
 621      | (k, e, ens, (C.MutInd _ as t),s) ->
 622         let t' = unwind k e ens t in
 623          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 624      | (k, e, ens, (C.MutConstruct _ as t),s) ->
 625          let t' = unwind k e ens t in
 626           if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 627      | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
 628         let decofix =
 629          function
 630             C.CoFix (i,fl) as t ->
 631              let (_,_,body) = List.nth fl i in
 632               let body' =
 633                let counter = ref (List.length fl) in
 634                 List.fold_right
 635                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 636                  fl
 637                  body
 638               in
 639                (* the term is the result of a reduction; *)
 640                (* so it is already unwinded.             *)
 641                reduce (0,[],[],body',[])
 642           | C.Appl (C.CoFix (i,fl) :: tl) ->
 643              let (_,_,body) = List.nth fl i in
 644               let body' =
 645                let counter = ref (List.length fl) in
 646                 List.fold_right
 647                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 648                  fl
 649                  body
 650               in
 651                (* the term is the result of a reduction; *)
 652                (* so it is already unwinded.             *)
 653                reduce (0,[],[],body',RS.to_stack_list tl)
 654           | t -> t
 655         in
 656          (match decofix (reduce (k,e,ens,term,[])) with
 657              C.MutConstruct (_,_,j,_) ->
 658               reduce (k, e, ens, (List.nth pl (j-1)), s)
 659            | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 660               let (arity, r) =
 661                 let o,_ =
 662                   CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind
 663                 in
 664                   match o with
 665                       C.InductiveDefinition (tl,ingredients,r,_) ->
 666                         let (_,_,arity,_) = List.nth tl i in
 667                           (arity,r)
 668                     | _ -> raise WrongUriToInductiveDefinition
 669               in
 670                let ts =
 671                 let num_to_eat = r in
 672                  let rec eat_first =
 673                   function
 674                      (0,l) -> l
 675                    | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 676                    | _ -> raise (Impossible 5)
 677                  in
 678                   eat_first (num_to_eat,tl)
 679                in
 680                 (* ts are already unwinded because they are a sublist of tl *)
 681                 reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
 682            | C.Cast _ | C.Implicit _ ->
 683               raise (Impossible 2) (* we don't trust our whd ;-) *)
 684            | _ ->
 685              let t' = unwind k e ens t in
 686               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 687          )
 688      | (k, e, ens, (C.Fix (i,fl) as t), s) ->
 689         let (_,recindex,_,body) = List.nth fl i in
 690          let recparam =
 691           try
 692            Some (RS.from_stack ~unwind (List.nth s recindex))
 693           with
 694            _ -> None
 695          in
 696           (match recparam with
 697               Some recparam ->
 698                (match reduce (0,[],[],recparam,[]) with
 699                    (* match recparam with *)
 700                    C.MutConstruct _
 701                  | C.Appl ((C.MutConstruct _)::_) ->
 702                     (* OLD
 703                     let body' =
 704                      let counter = ref (List.length fl) in
 705                       List.fold_right
 706                        (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 707                        fl
 708                        body
 709                     in
 710                      reduce (k, e, ens, body', s) *)
 711                     (* NEW *)
 712                     let leng = List.length fl in
 713                     let fl' =
 714                      let unwind_fl (name,recindex,typ,body) =
 715                       (name,recindex,unwind k e ens typ,
 716                         unwind' leng k e ens body)
 717                      in
 718                       List.map unwind_fl fl
 719                     in
 720                      let new_env =
 721                       let counter = ref 0 in
 722                       let rec build_env e =
 723                        if !counter = leng then e
 724                        else
 725                         (incr counter ;
 726                          build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e))
 727                       in
 728                        build_env e
 729                      in
 730                       reduce (k+leng, new_env, ens, body, s)
 731                  | _ ->
 732                    let t' = unwind k e ens t in
 733                     if s = [] then t' else
 734                      C.Appl (t'::(RS.from_stack_list ~unwind s))
 735                )
 736             | None ->
 737                let t' = unwind k e ens t in
 738                 if s = [] then t' else
 739                  C.Appl (t'::(RS.from_stack_list ~unwind s))
 740           )
 741      | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
 742         let t' = unwind k e ens t in
 743          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 744    and push_exp_named_subst k e ens =
 745     function
 746        [] -> ens
 747      | (uri,t)::tl ->
 748          push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
 749    in
 750      reduce
 751   ;;
 752   (*
 753   let rec whd context t =
 754     try
 755       reduce context (0, [], [], t, [])
 756     with Not_found ->
 757       prerr_endline (CicPp.ppterm t) ;
 758       raise Not_found
 759   ;;
 760   *)
 761
 762   let rec whd ?(subst=[]) context t =
 763     reduce ~subst context (0, [], [], t, [])
 764   ;;
 765
 766
 767 (* DEBUGGING ONLY
 768 let whd context t =
 769  let res = whd context t in
 770  let rescsc = CicReductionNaif.whd context t in
 771   if not (CicReductionNaif.are_convertible context res rescsc) then
 772    begin
 773     prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
 774     flush stderr ;
 775     prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
 776     flush stderr ;
 777     prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
 778     flush stderr ;
 779 CicReductionNaif.fdebug := 0 ;
 780 let _ =  CicReductionNaif.are_convertible context res rescsc in
 781     assert false ;
 782    end
 783   else
 784    res
 785 ;;
 786 *)
 787  end
 788 ;;
 789
 790
 791 (*
 792 module R = Reduction CallByNameStrategy;;
 793 module R = Reduction CallByValueStrategy;;
 794 module R = Reduction CallByValueStrategyByNameOnConstants;;
 795 module R = Reduction LazyCallByValueStrategy;;
 796 module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
 797 module R = Reduction LazyCallByNameStrategy;;
 798 module R = Reduction
 799  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
 800 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
 801 module R = Reduction
 802  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
 803 *)
 804 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
 805 module U = UriManager;;
 806
 807 let whd = R.whd;;
 808
 809   (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
 810     * fallbacks to structural equality *)
 811 let (===) x y = (Pervasives.compare x y = 0)
 812
 813 (* t1, t2 must be well-typed *)
 814 let are_convertible ?(subst=[]) ?(metasenv=[])  =
 815  let rec aux test_equality_only context t1 t2 ugraph =
 816   let aux2 test_equality_only t1 t2 ugraph =
 817
 818    (* this trivial euristic cuts down the total time of about five times ;-) *)
 819    (* this because most of the time t1 and t2 are "sintactically" the same   *)
 820    if t1 === t2 then
 821      true,ugraph
 822    else
 823     begin
 824      let module C = Cic in
 825        match (t1,t2) with
 826           (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph
 827         | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
 828             if U.eq uri1 uri2 then
 829              (try
 830                List.fold_right2
 831                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 832                   let b',ugraph' = aux test_equality_only context x y ugraph in
 833                   (U.eq uri1 uri2 && b' && b),ugraph'
 834                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 835               with
 836                Invalid_argument _ -> false,ugraph
 837              )
 838             else
 839               false,ugraph
 840         | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
 841             if n1 = n2 then
 842               let b2, ugraph1 =
 843                 let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
 844                 let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
 845                   List.fold_left2
 846                     (fun (b,ugraph) t1 t2 ->
 847                        if b then
 848                          match t1,t2 with
 849                              None,_
 850                            | _,None  -> true,ugraph
 851                            | Some t1',Some t2' ->
 852                                aux test_equality_only context t1' t2' ugraph
 853                        else
 854                          false,ugraph
 855                     ) (true,ugraph) l1 l2
 856               in
 857                 if b2 then true,ugraph1 else false,ugraph
 858             else
 859               false,ugraph
 860           (* TASSI: CONSTRAINTS *)
 861         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
 862             true,(CicUniv.add_eq t2 t1 ugraph)
 863           (* TASSI: CONSTRAINTS *)
 864         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 865             true,(CicUniv.add_ge t2 t1 ugraph)
 866           (* TASSI: CONSTRAINTS *)
 867         | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
 868           (* TASSI: CONSTRAINTS *)
 869         | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
 870         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 871             let b',ugraph' = aux true context s1 s2 ugraph in
 872             if b' then
 873               aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
 874                 t1 t2 ugraph'
 875             else
 876               false,ugraph
 877         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
 878            let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
 879            if b' then
 880              aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
 881                t1 t2 ugraph'
 882            else
 883              false,ugraph
 884         | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
 885            let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
 886            if b' then
 887             aux test_equality_only
 888              ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
 889            else
 890              false,ugraph
 891         | (C.Appl l1, C.Appl l2) ->
 892            (try
 893              List.fold_right2
 894                (fun  x y (b,ugraph) ->
 895                  if b then
 896                    aux test_equality_only context x y ugraph
 897                  else
 898                    false,ugraph) l1 l2 (true,ugraph)
 899             with
 900              Invalid_argument _ -> false,ugraph
 901            )
 902         | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
 903             let b' = U.eq uri1 uri2 in
 904             if b' then
 905              (try
 906                List.fold_right2
 907                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 908                   if b && U.eq uri1 uri2 then
 909                     aux test_equality_only context x y ugraph
 910                   else
 911                     false,ugraph
 912                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 913               with
 914                Invalid_argument _ -> false,ugraph
 915              )
 916             else
 917               false,ugraph
 918         | (C.MutInd (uri1,i1,exp_named_subst1),
 919            C.MutInd (uri2,i2,exp_named_subst2)
 920           ) ->
 921             let b' = U.eq uri1 uri2 && i1 = i2 in
 922             if b' then
 923              (try
 924                List.fold_right2
 925                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 926                   if b && U.eq uri1 uri2 then
 927                     aux test_equality_only context x y ugraph
 928                   else
 929                    false,ugraph
 930                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 931               with
 932                Invalid_argument _ -> false,ugraph
 933              )
 934             else
 935               false,ugraph
 936         | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 937            C.MutConstruct (uri2,i2,j2,exp_named_subst2)
 938           ) ->
 939             let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
 940             if b' then
 941              (try
 942                List.fold_right2
 943                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 944                   if b && U.eq uri1 uri2 then
 945                     aux test_equality_only context x y ugraph
 946                   else
 947                     false,ugraph
 948                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 949               with
 950                Invalid_argument _ -> false,ugraph
 951              )
 952             else
 953               false,ugraph
 954         | (C.MutCase (uri1,i1,outtype1,term1,pl1),
 955            C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
 956             let b' = U.eq uri1 uri2 && i1 = i2 in
 957             if b' then
 958              let b'',ugraph''=aux test_equality_only context
 959                  outtype1 outtype2 ugraph in
 960              if b'' then
 961                let b''',ugraph'''= aux test_equality_only context
 962                    term1 term2 ugraph'' in
 963                List.fold_right2
 964                  (fun x y (b,ugraph) ->
 965                    if b then
 966                      aux test_equality_only context x y ugraph
 967                    else
 968                      false,ugraph)
 969                  pl1 pl2 (true,ugraph''')
 970              else
 971                false,ugraph
 972             else
 973               false,ugraph
 974         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
 975             let tys =
 976               List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
 977             in
 978             if i1 = i2 then
 979              List.fold_right2
 980               (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
 981                 if b && recindex1 = recindex2 then
 982                   let b',ugraph' = aux test_equality_only context ty1 ty2
 983                       ugraph in
 984                   if b' then
 985                     aux test_equality_only (tys@context) bo1 bo2 ugraph'
 986                   else
 987                     false,ugraph
 988                 else
 989                   false,ugraph)
 990              fl1 fl2 (true,ugraph)
 991             else
 992               false,ugraph
 993         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
 994            let tys =
 995             List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
 996            in
 997             if i1 = i2 then
 998               List.fold_right2
 999               (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
1000                 if b then
1001                   let b',ugraph' = aux test_equality_only context ty1 ty2
1002                       ugraph in
1003                   if b' then
1004                     aux test_equality_only (tys@context) bo1 bo2 ugraph'
1005                   else
1006                     false,ugraph
1007                 else
1008                   false,ugraph)
1009              fl1 fl2 (true,ugraph)
1010             else
1011               false,ugraph
1012         | (C.Cast _, _) | (_, C.Cast _)
1013         | (C.Implicit _, _) | (_, C.Implicit _) ->
1014             assert false
1015         | (_,_) -> false,ugraph
1016     end
1017   in
1018      begin
1019      debug t1 [t2] "PREWHD";
1020      (*
1021      (match t1 with
1022          Cic.Meta _ ->
1023            prerr_endline (CicPp.ppterm t1);
1024            prerr_endline (CicPp.ppterm (whd ~subst context t1));
1025            prerr_endline (CicPp.ppterm t2);
1026            prerr_endline (CicPp.ppterm (whd ~subst context t2))
1027        | _ -> ()); *)
1028      let t1' = whd ~subst context t1 in
1029      let t2' = whd ~subst context t2 in
1030       debug t1' [t2'] "POSTWHD";
1031       aux2 test_equality_only t1' t2' ugraph
1032     end
1033  in
1034   aux false (*c t1 t2 ugraph *)
1035 ;;
1036