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 (lazy (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 (lazy ("%%%%%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 (lazy ("---- 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 (lazy "---- OK1") ;
 501 debug_print (lazy ("++++ 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 (lazy "---- 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 ~delta ?(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) when delta=false->
 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.Const (uri,exp_named_subst) as t), s) ->
 609         (let o,_ =
 610            CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 611          in
 612           match o with
 613             C.Constant (_,Some body,_,_,_) ->
 614              let ens' = push_exp_named_subst k e ens exp_named_subst in
 615               (* constants are closed *)
 616               reduce (0, [], ens', body, s)
 617           | C.Constant (_,None,_,_,_) ->
 618              let t' = unwind k e ens t in
 619               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 620           | C.Variable _ -> raise ReferenceToVariable
 621           | C.CurrentProof (_,_,body,_,_,_) ->
 622              let ens' = push_exp_named_subst k e ens exp_named_subst in
 623               (* constants are closed *)
 624               reduce (0, [], ens', body, s)
 625           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 626         )
 627      | (k, e, ens, (C.MutInd _ 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.MutConstruct _ as t),s) ->
 631          let t' = unwind k e ens t in
 632           if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 633      | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
 634         let decofix =
 635          function
 636             C.CoFix (i,fl) as t ->
 637              let (_,_,body) = List.nth fl i in
 638               let body' =
 639                let counter = ref (List.length fl) in
 640                 List.fold_right
 641                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 642                  fl
 643                  body
 644               in
 645                (* the term is the result of a reduction; *)
 646                (* so it is already unwinded.             *)
 647                reduce (0,[],[],body',[])
 648           | C.Appl (C.CoFix (i,fl) :: tl) ->
 649              let (_,_,body) = List.nth fl i in
 650               let body' =
 651                let counter = ref (List.length fl) in
 652                 List.fold_right
 653                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 654                  fl
 655                  body
 656               in
 657                (* the term is the result of a reduction; *)
 658                (* so it is already unwinded.             *)
 659                reduce (0,[],[],body',RS.to_stack_list tl)
 660           | t -> t
 661         in
 662          (match decofix (reduce (k,e,ens,term,[])) with
 663              C.MutConstruct (_,_,j,_) ->
 664               reduce (k, e, ens, (List.nth pl (j-1)), s)
 665            | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 666               let (arity, r) =
 667                 let o,_ =
 668                   CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind
 669                 in
 670                   match o with
 671                       C.InductiveDefinition (tl,ingredients,r,_) ->
 672                         let (_,_,arity,_) = List.nth tl i in
 673                           (arity,r)
 674                     | _ -> raise WrongUriToInductiveDefinition
 675               in
 676                let ts =
 677                 let num_to_eat = r in
 678                  let rec eat_first =
 679                   function
 680                      (0,l) -> l
 681                    | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 682                    | _ -> raise (Impossible 5)
 683                  in
 684                   eat_first (num_to_eat,tl)
 685                in
 686                 (* ts are already unwinded because they are a sublist of tl *)
 687                 reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
 688            | C.Cast _ | C.Implicit _ ->
 689               raise (Impossible 2) (* we don't trust our whd ;-) *)
 690            | _ ->
 691              let t' = unwind k e ens t in
 692               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 693          )
 694      | (k, e, ens, (C.Fix (i,fl) as t), s) ->
 695         let (_,recindex,_,body) = List.nth fl i in
 696          let recparam =
 697           try
 698            Some (RS.from_stack ~unwind (List.nth s recindex))
 699           with
 700            _ -> None
 701          in
 702           (match recparam with
 703               Some recparam ->
 704                (match reduce (0,[],[],recparam,[]) with
 705                    (* match recparam with *)
 706                    C.MutConstruct _
 707                  | C.Appl ((C.MutConstruct _)::_) ->
 708                     (* OLD
 709                     let body' =
 710                      let counter = ref (List.length fl) in
 711                       List.fold_right
 712                        (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 713                        fl
 714                        body
 715                     in
 716                      reduce (k, e, ens, body', s) *)
 717                     (* NEW *)
 718                     let leng = List.length fl in
 719                     let fl' =
 720                      let unwind_fl (name,recindex,typ,body) =
 721                       (name,recindex,unwind k e ens typ,
 722                         unwind' leng k e ens body)
 723                      in
 724                       List.map unwind_fl fl
 725                     in
 726                      let new_env =
 727                       let counter = ref 0 in
 728                       let rec build_env e =
 729                        if !counter = leng then e
 730                        else
 731                         (incr counter ;
 732                          build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e))
 733                       in
 734                        build_env e
 735                      in
 736                       reduce (k+leng, new_env, ens, body, s)
 737                  | _ ->
 738                    let t' = unwind k e ens t in
 739                     if s = [] then t' else
 740                      C.Appl (t'::(RS.from_stack_list ~unwind s))
 741                )
 742             | None ->
 743                let t' = unwind k e ens t in
 744                 if s = [] then t' else
 745                  C.Appl (t'::(RS.from_stack_list ~unwind s))
 746           )
 747      | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
 748         let t' = unwind k e ens t in
 749          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 750    and push_exp_named_subst k e ens =
 751     function
 752        [] -> ens
 753      | (uri,t)::tl ->
 754          push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
 755    in
 756      reduce
 757   ;;
 758   (*
 759   let rec whd context t =
 760     try
 761       reduce context (0, [], [], t, [])
 762     with Not_found ->
 763       debug_print (lazy (CicPp.ppterm t)) ;
 764       raise Not_found
 765   ;;
 766   *)
 767
 768   let rec whd ?(delta=true) ?(subst=[]) context t =
 769     reduce ~delta ~subst context (0, [], [], t, [])
 770   ;;
 771
 772
 773 (* DEBUGGING ONLY
 774 let whd context t =
 775  let res = whd context t in
 776  let rescsc = CicReductionNaif.whd context t in
 777   if not (CicReductionNaif.are_convertible context res rescsc) then
 778    begin
 779     debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
 780     flush stderr ;
 781     debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
 782     flush stderr ;
 783     debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
 784     flush stderr ;
 785 CicReductionNaif.fdebug := 0 ;
 786 let _ =  CicReductionNaif.are_convertible context res rescsc in
 787     assert false ;
 788    end
 789   else
 790    res
 791 ;;
 792 *)
 793  end
 794 ;;
 795
 796
 797 (*
 798 module R = Reduction CallByNameStrategy;;
 799 module R = Reduction CallByValueStrategy;;
 800 module R = Reduction CallByValueStrategyByNameOnConstants;;
 801 module R = Reduction LazyCallByValueStrategy;;
 802 module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
 803 module R = Reduction LazyCallByNameStrategy;;
 804 module R = Reduction
 805  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
 806 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
 807 module R = Reduction
 808  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
 809 *)
 810 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
 811 module U = UriManager;;
 812
 813 let whd = R.whd;;
 814
 815   (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
 816     * fallbacks to structural equality *)
 817 let (===) x y = (Pervasives.compare x y = 0)
 818
 819 (* t1, t2 must be well-typed *)
 820 let are_convertible ?(subst=[]) ?(metasenv=[])  =
 821  let rec aux test_equality_only context t1 t2 ugraph =
 822   let aux2 test_equality_only t1 t2 ugraph =
 823
 824    (* this trivial euristic cuts down the total time of about five times ;-) *)
 825    (* this because most of the time t1 and t2 are "sintactically" the same   *)
 826    if t1 === t2 then
 827      true,ugraph
 828    else
 829     begin
 830      let module C = Cic in
 831        match (t1,t2) with
 832           (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph
 833         | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
 834             if U.eq uri1 uri2 then
 835              (try
 836                List.fold_right2
 837                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 838                   let b',ugraph' = aux test_equality_only context x y ugraph in
 839                   (U.eq uri1 uri2 && b' && b),ugraph'
 840                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 841               with
 842                Invalid_argument _ -> false,ugraph
 843              )
 844             else
 845               false,ugraph
 846         | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
 847             if n1 = n2 then
 848               let b2, ugraph1 =
 849                 let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
 850                 let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
 851                   List.fold_left2
 852                     (fun (b,ugraph) t1 t2 ->
 853                        if b then
 854                          match t1,t2 with
 855                              None,_
 856                            | _,None  -> true,ugraph
 857                            | Some t1',Some t2' ->
 858                                aux test_equality_only context t1' t2' ugraph
 859                        else
 860                          false,ugraph
 861                     ) (true,ugraph) l1 l2
 862               in
 863                 if b2 then true,ugraph1 else false,ugraph
 864             else
 865               false,ugraph
 866           (* TASSI: CONSTRAINTS *)
 867         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
 868             true,(CicUniv.add_eq t2 t1 ugraph)
 869           (* TASSI: CONSTRAINTS *)
 870         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 871             true,(CicUniv.add_ge t2 t1 ugraph)
 872           (* TASSI: CONSTRAINTS *)
 873         | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
 874           (* TASSI: CONSTRAINTS *)
 875         | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
 876         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 877             let b',ugraph' = aux true context s1 s2 ugraph in
 878             if b' then
 879               aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
 880                 t1 t2 ugraph'
 881             else
 882               false,ugraph
 883         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
 884            let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
 885            if b' then
 886              aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
 887                t1 t2 ugraph'
 888            else
 889              false,ugraph
 890         | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
 891            let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
 892            if b' then
 893             aux test_equality_only
 894              ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
 895            else
 896              false,ugraph
 897         | (C.Appl l1, C.Appl l2) ->
 898            (try
 899              List.fold_right2
 900                (fun  x y (b,ugraph) ->
 901                  if b then
 902                    aux test_equality_only context x y ugraph
 903                  else
 904                    false,ugraph) l1 l2 (true,ugraph)
 905             with
 906              Invalid_argument _ -> false,ugraph
 907            )
 908         | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
 909             let b' = U.eq uri1 uri2 in
 910             if b' then
 911              (try
 912                List.fold_right2
 913                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 914                   if b && U.eq uri1 uri2 then
 915                     aux test_equality_only context x y ugraph
 916                   else
 917                     false,ugraph
 918                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 919               with
 920                Invalid_argument _ -> false,ugraph
 921              )
 922             else
 923               false,ugraph
 924         | (C.MutInd (uri1,i1,exp_named_subst1),
 925            C.MutInd (uri2,i2,exp_named_subst2)
 926           ) ->
 927             let b' = U.eq uri1 uri2 && i1 = i2 in
 928             if b' then
 929              (try
 930                List.fold_right2
 931                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 932                   if b && U.eq uri1 uri2 then
 933                     aux test_equality_only context x y ugraph
 934                   else
 935                    false,ugraph
 936                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 937               with
 938                Invalid_argument _ -> false,ugraph
 939              )
 940             else
 941               false,ugraph
 942         | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 943            C.MutConstruct (uri2,i2,j2,exp_named_subst2)
 944           ) ->
 945             let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
 946             if b' then
 947              (try
 948                List.fold_right2
 949                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 950                   if b && U.eq uri1 uri2 then
 951                     aux test_equality_only context x y ugraph
 952                   else
 953                     false,ugraph
 954                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 955               with
 956                Invalid_argument _ -> false,ugraph
 957              )
 958             else
 959               false,ugraph
 960         | (C.MutCase (uri1,i1,outtype1,term1,pl1),
 961            C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
 962             let b' = U.eq uri1 uri2 && i1 = i2 in
 963             if b' then
 964              let b'',ugraph''=aux test_equality_only context
 965                  outtype1 outtype2 ugraph in
 966              if b'' then
 967                let b''',ugraph'''= aux test_equality_only context
 968                    term1 term2 ugraph'' in
 969                List.fold_right2
 970                  (fun x y (b,ugraph) ->
 971                    if b then
 972                      aux test_equality_only context x y ugraph
 973                    else
 974                      false,ugraph)
 975                  pl1 pl2 (b''',ugraph''')
 976              else
 977                false,ugraph
 978             else
 979               false,ugraph
 980         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
 981             let tys =
 982               List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
 983             in
 984             if i1 = i2 then
 985              List.fold_right2
 986               (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
 987                 if b && recindex1 = recindex2 then
 988                   let b',ugraph' = aux test_equality_only context ty1 ty2
 989                       ugraph in
 990                   if b' then
 991                     aux test_equality_only (tys@context) bo1 bo2 ugraph'
 992                   else
 993                     false,ugraph
 994                 else
 995                   false,ugraph)
 996              fl1 fl2 (true,ugraph)
 997             else
 998               false,ugraph
 999         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
1000            let tys =
1001             List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
1002            in
1003             if i1 = i2 then
1004               List.fold_right2
1005               (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
1006                 if b then
1007                   let b',ugraph' = aux test_equality_only context ty1 ty2
1008                       ugraph in
1009                   if b' then
1010                     aux test_equality_only (tys@context) bo1 bo2 ugraph'
1011                   else
1012                     false,ugraph
1013                 else
1014                   false,ugraph)
1015              fl1 fl2 (true,ugraph)
1016             else
1017               false,ugraph
1018         | (C.Cast _, _) | (_, C.Cast _)
1019         | (C.Implicit _, _) | (_, C.Implicit _) ->
1020             assert false
1021         | (_,_) -> false,ugraph
1022     end
1023   in
1024      begin
1025      debug t1 [t2] "PREWHD";
1026      (*
1027      (match t1 with
1028          Cic.Meta _ ->
1029            debug_print (lazy (CicPp.ppterm t1));
1030            debug_print (lazy (CicPp.ppterm (whd ~subst context t1)));
1031            debug_print (lazy (CicPp.ppterm t2));
1032            debug_print (lazy (CicPp.ppterm (whd ~subst context t2)))
1033        | _ -> ()); *)
1034      let t1' = whd ~subst context t1 in
1035      let t2' = whd ~subst context t2 in
1036       debug t1' [t2'] "POSTWHD";
1037       aux2 test_equality_only t1' t2' ugraph
1038     end
1039  in
1040   aux false (*c t1 t2 ugraph *)
1041 ;;
1042
1043
1044 let rec normalize ?(delta=true) ?(subst=[]) ctx term =
1045   let module C = Cic in
1046   let t = whd ~delta ~subst ctx term in
1047   let aux = normalize ~delta ~subst in
1048   let decl name t = Some (name, C.Decl t) in
1049   let def  name t = Some (name, C.Def (t,None)) in
1050   match t with
1051   | C.Rel n -> t
1052   | C.Var (uri,exp_named_subst) ->
1053       C.Var (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
1054   | C.Meta (i,l) ->
1055       C.Meta (i,List.map (function Some t -> Some (aux ctx t) | None -> None) l)
1056   | C.Sort _ -> t
1057   | C.Implicit _ -> t
1058   | C.Cast (te,ty) -> C.Cast (aux ctx te, aux ctx ty)
1059   | C.Prod (n,s,t) ->
1060       let s' = aux ctx s in
1061       C.Prod (n, s', aux ((decl n s')::ctx) t)
1062   | C.Lambda (n,s,t) ->
1063       let s' = aux ctx s in
1064       C.Lambda (n, s', aux ((decl n s')::ctx) t)
1065   | C.LetIn (n,s,t) ->
1066       (* the term is already in weak head normal form *)
1067       assert false
1068   | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
1069   | C.Appl [] -> assert false
1070   | C.Const (uri,exp_named_subst) ->
1071       C.Const (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
1072   | C.MutInd (uri,typeno,exp_named_subst) ->
1073       C.MutInd (uri,typeno, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
1074   | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
1075       C.MutConstruct (uri, typeno, consno,
1076         List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
1077   | C.MutCase (sp,i,outt,t,pl) ->
1078       C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl)
1079 (*CSC: to be completed, I suppose *)
1080   | C.Fix _ -> t
1081   | C.CoFix _ -> t
1082
1083 let normalize ?delta ?subst ctx term =
1084 (*  prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); *)
1085   let t = normalize ?delta ?subst ctx term in
1086 (*  prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); *)
1087   t
1088
1089
1090 (* performs an head beta/cast reduction *)
1091 let rec head_beta_reduce =
1092  function
1093     (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
1094       let he'' = CicSubstitution.subst he' t in
1095        if tl' = [] then
1096         he''
1097        else
1098         let he''' =
1099          match he'' with
1100             Cic.Appl l -> Cic.Appl (l@tl')
1101           | _ -> Cic.Appl (he''::tl')
1102         in
1103          head_beta_reduce he'''
1104   | Cic.Cast (te,_) -> head_beta_reduce te
1105   | t -> t