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