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