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