helm/software/components/ng_kernel/nCicReduction.ml

   1 (*  ||M||  This file is part of HELM, an Hypertextual, Electronic
   2     ||A||  Library of Mathematics, developed at the Computer Science
   3     ||T||  Department, University of Bologna, Italy.
   4     ||I||
   5     ||T||  HELM is free software; you can redistribute it and/or
   6     ||A||  modify it under the terms of the GNU General Public License
   7     \   /  version 2 or (at your option) any later version.
   8      \ /   This software is distributed as is, NO WARRANTY.
   9       V_______________________________________________________________ *)
  10
  11 (* $Id$ *)
  12
  13 (* TODO unify exceptions *)
  14
  15 exception WrongUriToInductiveDefinition;;
  16 exception Impossible of int;;
  17 exception ReferenceToConstant;;
  18 exception ReferenceToVariable;;
  19 exception ReferenceToCurrentProof;;
  20 exception ReferenceToInductiveDefinition;;
  21
  22 let debug = false
  23 let profile = false
  24 let debug_print s = if debug then prerr_endline (Lazy.force s)
  25
  26 let fdebug = ref 1;;
  27 let debug t env s =
  28  let rec debug_aux t i =
  29   let module C = Cic in
  30   let module U = UriManager in
  31    CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  32  in
  33   if !fdebug = 0 then
  34    debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) ""))
  35 ;;
  36
  37 module type Strategy =
  38  sig
  39   type stack_term
  40   type env_term
  41   type config = int * env_term list * NCic.term * stack_term list
  42   val to_env :
  43    reduce: (config -> config) ->
  44    unwind: (config -> NCic.term) ->
  45    config -> env_term
  46   val from_stack : stack_term -> config
  47   val from_stack_list_for_unwind :
  48    unwind: (config -> NCic.term) ->
  49    stack_term list -> NCic.term list
  50   val from_env : env_term -> config
  51   val from_env_for_unwind :
  52    unwind: (config -> NCic.term) ->
  53    env_term -> NCic.term
  54   val stack_to_env :
  55    reduce: (config -> config) ->
  56    unwind: (config -> NCic.term) ->
  57    stack_term -> env_term
  58   val compute_to_env :
  59    reduce: (config -> config) ->
  60    unwind: (config -> NCic.term) ->
  61    int -> env_term list ->
  62     NCic.term -> env_term
  63   val compute_to_stack :
  64    reduce: (config -> config) ->
  65    unwind: (config -> NCic.term) ->
  66    config -> stack_term
  67  end
  68 ;;
  69
  70 module CallByValueByNameForUnwind' =
  71  struct
  72   type config = int * env_term list * NCic.term * stack_term list
  73   and stack_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
  74   and env_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
  75   let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c)
  76   let from_stack (c,_) = Lazy.force c
  77   let from_stack_list_for_unwind ~unwind:_ l =
  78    List.map (function (_,c) -> Lazy.force c) l
  79   let from_env (c,_) = Lazy.force c
  80   let from_env_for_unwind ~unwind:_ (_,c) = Lazy.force c
  81   let stack_to_env ~reduce:_ ~unwind:_ config = config
  82   let compute_to_env ~reduce ~unwind k e t =
  83    lazy (reduce (k,e,t,[])), lazy (unwind (k,e,t,[]))
  84   let compute_to_stack ~reduce ~unwind config =
  85    lazy (reduce config), lazy (unwind config)
  86  end
  87 ;;
  88
  89
  90 (* {{{ module CallByValueByNameForUnwind =
  91  struct
  92   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
  93   and stack_term = config
  94   and env_term = config * config (* cbv, cbn *)
  95   and ens_term = config * config (* cbv, cbn *)
  96
  97   let to_env c = c,c
  98   let to_ens c = c,c
  99   let from_stack config = config
 100   let from_stack_list_for_unwind ~unwind l = List.map unwind l
 101   let from_env (c,_) = c
 102   let from_ens (c,_) = c
 103   let from_env_for_unwind ~unwind (_,c) = unwind c
 104   let from_ens_for_unwind ~unwind (_,c) = unwind c
 105   let stack_to_env ~reduce ~unwind config = reduce config, (0,[],[],unwind config,[])
 106   let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[]), (k,e,ens,t,[])
 107   let compute_to_stack ~reduce ~unwind config = config
 108  end
 109 ;;
 110
 111
 112 (* Old Machine *)
 113 module CallByNameStrategy =
 114  struct
 115   type stack_term = Cic.term
 116   type env_term = Cic.term
 117   type ens_term = Cic.term
 118   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 119   let to_env v = v
 120   let to_ens v = v
 121   let from_stack ~unwind v = v
 122   let from_stack_list ~unwind l = l
 123   let from_env v = v
 124   let from_ens v = v
 125   let from_env_for_unwind ~unwind v = v
 126   let from_ens_for_unwind ~unwind v = v
 127   let stack_to_env ~reduce ~unwind v = v
 128   let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
 129   let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
 130  end
 131 ;;
 132
 133 module CallByNameStrategy =
 134  struct
 135   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 136   and stack_term = config
 137   and env_term = config
 138   and ens_term = config
 139
 140   let to_env c = c
 141   let to_ens c = c
 142   let from_stack config = config
 143   let from_stack_list_for_unwind ~unwind l = List.map unwind l
 144   let from_env c = c
 145   let from_ens c = c
 146   let from_env_for_unwind ~unwind c = unwind c
 147   let from_ens_for_unwind ~unwind c = unwind c
 148   let stack_to_env ~reduce ~unwind config = 0,[],[],unwind config,[]
 149   let compute_to_env ~reduce ~unwind k e ens t = k,e,ens,t,[]
 150   let compute_to_stack ~reduce ~unwind config = config
 151  end
 152 ;;
 153
 154 module CallByValueStrategy =
 155  struct
 156   type stack_term = Cic.term
 157   type env_term = Cic.term
 158   type ens_term = Cic.term
 159   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 160   let to_env v = v
 161   let to_ens v = v
 162   let from_stack ~unwind v = v
 163   let from_stack_list ~unwind l = l
 164   let from_env v = v
 165   let from_ens v = v
 166   let from_env_for_unwind ~unwind v = v
 167   let from_ens_for_unwind ~unwind v = v
 168   let stack_to_env ~reduce ~unwind v = v
 169   let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
 170   let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
 171  end
 172 ;;
 173
 174 module CallByValueStrategyByNameOnConstants =
 175  struct
 176   type stack_term = Cic.term
 177   type env_term = Cic.term
 178   type ens_term = Cic.term
 179   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 180   let to_env v = v
 181   let to_ens v = v
 182   let from_stack ~unwind v = v
 183   let from_stack_list ~unwind l = l
 184   let from_env v = v
 185   let from_ens v = v
 186   let from_env_for_unwind ~unwind v = v
 187   let from_ens_for_unwind ~unwind v = v
 188   let stack_to_env ~reduce ~unwind v = v
 189   let compute_to_stack ~reduce ~unwind k e ens =
 190    function
 191       Cic.Const _ as t -> unwind k e ens t
 192     | t -> reduce (k,e,ens,t,[])
 193   let compute_to_env ~reduce ~unwind k e ens =
 194    function
 195       Cic.Const _ as t -> unwind k e ens t
 196     | t -> reduce (k,e,ens,t,[])
 197  end
 198 ;;
 199
 200 module LazyCallByValueStrategy =
 201  struct
 202   type stack_term = Cic.term lazy_t
 203   type env_term = Cic.term lazy_t
 204   type ens_term = Cic.term lazy_t
 205   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 206   let to_env v = lazy v
 207   let to_ens v = lazy v
 208   let from_stack ~unwind v = Lazy.force v
 209   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 210   let from_env v = Lazy.force v
 211   let from_ens v = Lazy.force v
 212   let from_env_for_unwind ~unwind v = Lazy.force v
 213   let from_ens_for_unwind ~unwind v = Lazy.force v
 214   let stack_to_env ~reduce ~unwind v = v
 215   let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
 216   let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
 217  end
 218 ;;
 219
 220 module LazyCallByValueStrategyByNameOnConstants =
 221  struct
 222   type stack_term = Cic.term lazy_t
 223   type env_term = Cic.term lazy_t
 224   type ens_term = Cic.term lazy_t
 225   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 226   let to_env v = lazy v
 227   let to_ens v = lazy v
 228   let from_stack ~unwind v = Lazy.force v
 229   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 230   let from_env v = Lazy.force v
 231   let from_ens v = Lazy.force v
 232   let from_env_for_unwind ~unwind v = Lazy.force v
 233   let from_ens_for_unwind ~unwind v = Lazy.force v
 234   let stack_to_env ~reduce ~unwind v = v
 235   let compute_to_stack ~reduce ~unwind k e ens t =
 236    lazy (
 237     match t with
 238        Cic.Const _ as t -> unwind k e ens t
 239      | t -> reduce (k,e,ens,t,[]))
 240   let compute_to_env ~reduce ~unwind k e ens t =
 241    lazy (
 242     match t with
 243        Cic.Const _ as t -> unwind k e ens t
 244      | t -> reduce (k,e,ens,t,[]))
 245  end
 246 ;;
 247
 248 module LazyCallByNameStrategy =
 249  struct
 250   type stack_term = Cic.term lazy_t
 251   type env_term = Cic.term lazy_t
 252   type ens_term = Cic.term lazy_t
 253   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 254   let to_env v = lazy v
 255   let to_ens v = lazy v
 256   let from_stack ~unwind v = Lazy.force v
 257   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 258   let from_env v = Lazy.force v
 259   let from_ens v = Lazy.force v
 260   let from_env_for_unwind ~unwind v = Lazy.force v
 261   let from_ens_for_unwind ~unwind v = Lazy.force v
 262   let stack_to_env ~reduce ~unwind v = v
 263   let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
 264   let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
 265  end
 266 ;;
 267
 268 module
 269  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
 270 =
 271  struct
 272   type stack_term = reduce:bool -> Cic.term
 273   type env_term = reduce:bool -> Cic.term
 274   type ens_term = reduce:bool -> Cic.term
 275   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 276   let to_env v =
 277    let value = lazy v in
 278     fun ~reduce -> Lazy.force value
 279   let to_ens v =
 280    let value = lazy v in
 281     fun ~reduce -> Lazy.force value
 282   let from_stack ~unwind v = (v ~reduce:false)
 283   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 284   let from_env v = (v ~reduce:true)
 285   let from_ens v = (v ~reduce:true)
 286   let from_env_for_unwind ~unwind v = (v ~reduce:true)
 287   let from_ens_for_unwind ~unwind v = (v ~reduce:true)
 288   let stack_to_env ~reduce ~unwind v = v
 289   let compute_to_stack ~reduce ~unwind k e ens t =
 290    let svalue =
 291      lazy (
 292       match t with
 293          Cic.Const _ as t -> unwind k e ens t
 294        | t -> reduce (k,e,ens,t,[])
 295      ) in
 296    let lvalue =
 297     lazy (unwind k e ens t)
 298    in
 299     fun ~reduce ->
 300      if reduce then Lazy.force svalue else Lazy.force lvalue
 301   let compute_to_env ~reduce ~unwind k e ens t =
 302    let svalue =
 303      lazy (
 304       match t with
 305          Cic.Const _ as t -> unwind k e ens t
 306        | t -> reduce (k,e,ens,t,[])
 307      ) in
 308    let lvalue =
 309     lazy (unwind k e ens t)
 310    in
 311     fun ~reduce ->
 312      if reduce then Lazy.force svalue else Lazy.force lvalue
 313  end
 314 ;;
 315
 316 module ClosuresOnStackByValueFromEnvOrEnsStrategy =
 317  struct
 318   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 319   and stack_term = config
 320   and env_term = config
 321   and ens_term = config
 322
 323   let to_env config = config
 324   let to_ens config = config
 325   let from_stack config = config
 326   let from_stack_list_for_unwind ~unwind l = List.map unwind l
 327   let from_env v = v
 328   let from_ens v = v
 329   let from_env_for_unwind ~unwind config = unwind config
 330   let from_ens_for_unwind ~unwind config = unwind config
 331   let stack_to_env ~reduce ~unwind config = reduce config
 332   let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[])
 333   let compute_to_stack ~reduce ~unwind config = config
 334  end
 335 ;;
 336
 337 module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
 338  struct
 339   type stack_term =
 340    int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
 341   type env_term = Cic.term
 342   type ens_term = Cic.term
 343   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 344   let to_env v = v
 345   let to_ens v = v
 346   let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
 347   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 348   let from_env v = v
 349   let from_ens v = v
 350   let from_env_for_unwind ~unwind v = v
 351   let from_ens_for_unwind ~unwind v = v
 352   let stack_to_env ~reduce ~unwind (k,e,ens,t) =
 353    match t with
 354       Cic.Const _ as t -> unwind k e ens t
 355     | t -> reduce (k,e,ens,t,[])
 356   let compute_to_env ~reduce ~unwind k e ens t =
 357    unwind k e ens t
 358   let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
 359  end
 360 ;;
 361
 362 }}} *)
 363
 364 module Reduction(RS : Strategy) =
 365  struct
 366   type env = RS.env_term list
 367   type stack = RS.stack_term list
 368   type config = int * env * NCic.term * stack
 369
 370   let rec unwind (k,e,t,s) =
 371     let t =
 372       if k = 0 then t
 373       else
 374         NCicSubstitution.psubst ~avoid_beta_redexes:true
 375           true 0 (RS.from_env_for_unwind ~unwind) e t
 376     in
 377     if s = [] then t
 378     else NCic.Appl(t::(RS.from_stack_list_for_unwind ~unwind s))
 379   ;;
 380
 381   let list_nth l n = try List.nth l n with Failure _ -> assert false;;
 382   let rec replace i s t =
 383     match i,s with
 384     |  0,_::tl -> t::tl
 385     | n,he::tl -> he::(replace (n - 1) tl t)
 386     | _,_ -> assert false
 387   ;;
 388
 389   let rec reduce ~delta ?(subst = []) context : config -> config =
 390    let rec aux = function
 391      | k, e, NCic.Rel n, s when n <= k ->
 392         let k',e',t',s' = RS.from_env (list_nth e (n-1)) in
 393         aux (k',e',t',s'@s)
 394      | k, _, NCic.Rel n, s as config (* when n > k *) ->
 395         (match List.nth context (n - 1 - k) with
 396         | (_,NCic.Decl _) -> config
 397         | (_,NCic.Def (x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s))
 398      | (k, e, NCic.Meta (n,l), s) as config ->
 399         (try
 400            let _,_, term,_ = NCicUtils.lookup_subst n subst in
 401            aux (k, e, NCicSubstitution.subst_meta l term,s)
 402          with  NCicUtils.Subst_not_found _ -> config)
 403      | (_, _, NCic.Sort _, _) as config -> config
 404      | (_, _, NCic.Implicit _, _) -> assert false
 405      | (_, _, NCic.Prod _, _) as config -> config
 406      | (_, _, NCic.Lambda _, []) as config -> config
 407      | (k, e, NCic.Lambda (_,_,t), p::s) ->
 408          aux (k+1, (RS.stack_to_env ~reduce:aux ~unwind p)::e, t,s)
 409      | (k, e, NCic.LetIn (_,_,m,t), s) ->
 410         let m' = RS.compute_to_env ~reduce:aux ~unwind k e m in
 411          aux (k+1, m'::e, t, s)
 412      | (_, _, NCic.Appl [], _) -> assert false
 413      | (k, e, NCic.Appl (he::tl), s) ->
 414         let tl' =
 415          List.map (fun t->RS.compute_to_stack ~reduce:aux ~unwind (k,e,t,[])) tl
 416         in
 417          aux (k, e, he, tl' @ s)
 418      | (_, _, NCic.Const
 419             (NReference.Ref (_,_,NReference.Def) as refer), s) as config ->
 420          let _,_,body,_,_,height = NCicEnvironment.get_checked_def refer in
 421          if delta >= height then config else aux (0, [], body, s)
 422      | (_, _, NCic.Const (NReference.Ref
 423                (_,_,NReference.Fix (_,recindex)) as refer),s) as config ->
 424         let _,_,body,_, _, height = NCicEnvironment.get_checked_fix refer in
 425         if delta >= height then config else
 426         (match
 427           try Some (RS.from_stack (List.nth s recindex))
 428           with Failure _ -> None
 429         with
 430         | None -> config
 431         | Some recparam ->
 432            match reduce ~delta:0 ~subst context recparam with
 433            | (_,_,NCic.Const (NReference.Ref (_,_,NReference.Con _)), _) as c ->
 434                let new_s =
 435                  replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c)
 436                in
 437                aux (0, [], body, new_s)
 438            | _ -> config)
 439      | (_, _, NCic.Const _, _) as config -> config
 440      | (k, e, NCic.Match (_,_,term,pl),s) as config ->
 441         let decofix = function
 442           | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix _)as refer),s)->
 443              let _,_,body,_,_,_ = NCicEnvironment.get_checked_cofix refer in
 444              reduce ~delta:0 ~subst context (0,[],body,s)
 445           | config -> config
 446         in
 447         (match decofix (reduce ~delta:0 ~subst context (k,e,term,[])) with
 448         | (_, _, NCic.Const (NReference.Ref (_,_,NReference.Con (_,j))),[]) ->
 449             aux (k, e, List.nth pl (j-1), s)
 450         | (_, _, NCic.Const
 451              (NReference.Ref (_,_,NReference.Con (_,j)) as refer), s') ->
 452           let leftno = NCicEnvironment.get_indty_leftno refer in
 453           let _,params = HExtlib.split_nth leftno s' in
 454           aux (k, e, List.nth pl (j-1), params@s)
 455         | _ -> config)
 456    in
 457     aux
 458   ;;
 459
 460   let whd ?(delta=0) ?(subst=[]) context t =
 461    unwind (reduce ~delta ~subst context (0, [], t, []))
 462   ;;
 463
 464  end
 465 ;;
 466
 467
 468 (* {{{ ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
 469            senza ridurre la testa
 470 module R = Reduction CallByNameStrategy;; OK 56.368s
 471 module R = Reduction CallByValueStrategy;; ROTTO
 472 module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
 473 module R = Reduction LazyCallByValueStrategy;; ROTTO
 474 module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
 475 module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
 476 module R = Reduction
 477  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
 478  OK 59.058s
 479 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
 480 module R = Reduction
 481  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
 482 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 483 module R = Reduction(CallByValueByNameForUnwind);;
 484 module R = Reduction(CallByNameStrategy);;
 485 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;}}} *)
 486 module RS = CallByValueByNameForUnwind';;
 487
 488 module R = Reduction(RS);;
 489 module U = UriManager;;
 490
 491 let whd = R.whd
 492
 493 (*
 494 let whd =
 495  let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
 496   fun ?(delta=true) ?(subst=[]) context t ->
 497    profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
 498 *)
 499
 500 (*
 501
 502  (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
 503   * fallbacks to structural equality *)
 504 let (===) x y = Pervasives.compare x y = 0 ;;
 505
 506 module C = NCic
 507
 508 (* t1, t2 must be well-typed *)
 509 let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
 510  let heuristic = ref true in
 511  let rec aux test_equality_only context t1 t2 =
 512    let rec aux2 test_equality_only t1 t2 =
 513      if t1 === t2 then
 514        true
 515      else
 516        match (t1,t2) with
 517        | (C.Rel n1, C.Rel n2) -> n1 = n2
 518
 519        | (C.Sort (C.Type a), C.Sort (C.Type b)) -> a <= b
 520        | (C.Sort (C.Type a), C.Sort (C.Type b)) when test_equality_only -> a=b
 521        | (C.Sort s1,C.Sort (C.Type _)) -> (not test_equality_only)
 522        | (C.Sort s1, C.Sort s2) -> s1 = s2
 523
 524        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 525            aux true context s1 s2 &&
 526            aux test_equality_only ((name1, C.Decl s1)::context) t1 t2
 527        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
 528           aux test_equality_only context s1 s2 && (* sure?! *)
 529           aux test_equality_only ((name1, C.Decl s1)::context) t1 t2
 530
 531        | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
 532             if n1 = n2 then
 533               let b2, ugraph1 =
 534                 let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
 535                 let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
 536                   List.fold_left2
 537                     (fun (b,ugraph) t1 t2 ->
 538                        if b then
 539                          match t1,t2 with
 540                              None,_
 541                            | _,None  -> true,ugraph
 542                            | Some t1',Some t2' ->
 543                                aux test_equality_only context t1' t2' ugraph
 544                        else
 545                          false,ugraph
 546                     ) (true,ugraph) l1 l2
 547               in
 548                 if b2 then true,ugraph1 else false,ugraph
 549             else
 550               false,ugraph
 551         | C.Meta (n1,l1), _ ->
 552            (try
 553               let _,term,_ = NCicUtils.lookup_subst n1 subst in
 554               let term' = CicSubstitution.subst_meta l1 term in
 555                aux test_equality_only context term' t2 ugraph
 556             with  CicUtil.Subst_not_found _ -> false,ugraph)
 557         | _, C.Meta (n2,l2) ->
 558            (try
 559               let _,term,_ = CicUtil.lookup_subst n2 subst in
 560               let term' = CicSubstitution.subst_meta l2 term in
 561                aux test_equality_only context t1 term' ugraph
 562             with  CicUtil.Subst_not_found _ -> false,ugraph)
 563         | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
 564            let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
 565            if b' then
 566             aux test_equality_only
 567              ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
 568            else
 569              false,ugraph
 570         | (C.Appl l1, C.Appl l2) ->
 571            (try
 572              List.fold_right2
 573                (fun  x y (b,ugraph) ->
 574                  if b then
 575                    aux test_equality_only context x y ugraph
 576                  else
 577                    false,ugraph) l1 l2 (true,ugraph)
 578             with
 579              Invalid_argument _ -> false,ugraph
 580            )
 581         | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
 582             let b' = U.eq uri1 uri2 in
 583             if b' then
 584              (try
 585                List.fold_right2
 586                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 587                   if b && U.eq uri1 uri2 then
 588                     aux test_equality_only context x y ugraph
 589                   else
 590                     false,ugraph
 591                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 592               with
 593                Invalid_argument _ -> false,ugraph
 594              )
 595             else
 596               false,ugraph
 597         | (C.MutInd (uri1,i1,exp_named_subst1),
 598            C.MutInd (uri2,i2,exp_named_subst2)
 599           ) ->
 600             let b' = U.eq uri1 uri2 && i1 = i2 in
 601             if b' then
 602              (try
 603                List.fold_right2
 604                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 605                   if b && U.eq uri1 uri2 then
 606                     aux test_equality_only context x y ugraph
 607                   else
 608                    false,ugraph
 609                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 610               with
 611                Invalid_argument _ -> false,ugraph
 612              )
 613             else
 614               false,ugraph
 615         | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 616            C.MutConstruct (uri2,i2,j2,exp_named_subst2)
 617           ) ->
 618             let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
 619             if b' then
 620              (try
 621                List.fold_right2
 622                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 623                   if b && U.eq uri1 uri2 then
 624                     aux test_equality_only context x y ugraph
 625                   else
 626                     false,ugraph
 627                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 628               with
 629                Invalid_argument _ -> false,ugraph
 630              )
 631             else
 632               false,ugraph
 633         | (C.MutCase (uri1,i1,outtype1,term1,pl1),
 634            C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
 635             let b' = U.eq uri1 uri2 && i1 = i2 in
 636             if b' then
 637              let b'',ugraph''=aux test_equality_only context
 638                  outtype1 outtype2 ugraph in
 639              if b'' then
 640                let b''',ugraph'''= aux test_equality_only context
 641                    term1 term2 ugraph'' in
 642                List.fold_right2
 643                  (fun x y (b,ugraph) ->
 644                    if b then
 645                      aux test_equality_only context x y ugraph
 646                    else
 647                      false,ugraph)
 648                  pl1 pl2 (b''',ugraph''')
 649              else
 650                false,ugraph
 651             else
 652               false,ugraph
 653         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
 654             let tys,_ =
 655               List.fold_left
 656                 (fun (types,len) (n,_,ty,_) ->
 657                    (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 658                     len+1)
 659                 ) ([],0) fl1
 660             in
 661             if i1 = i2 then
 662              List.fold_right2
 663               (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
 664                 if b && recindex1 = recindex2 then
 665                   let b',ugraph' = aux test_equality_only context ty1 ty2
 666                       ugraph in
 667                   if b' then
 668                     aux test_equality_only (tys@context) bo1 bo2 ugraph'
 669                   else
 670                     false,ugraph
 671                 else
 672                   false,ugraph)
 673              fl1 fl2 (true,ugraph)
 674             else
 675               false,ugraph
 676         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
 677             let tys,_ =
 678               List.fold_left
 679                 (fun (types,len) (n,ty,_) ->
 680                    (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 681                     len+1)
 682                 ) ([],0) fl1
 683             in
 684             if i1 = i2 then
 685               List.fold_right2
 686               (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
 687                 if b then
 688                   let b',ugraph' = aux test_equality_only context ty1 ty2
 689                       ugraph in
 690                   if b' then
 691                     aux test_equality_only (tys@context) bo1 bo2 ugraph'
 692                   else
 693                     false,ugraph
 694                 else
 695                   false,ugraph)
 696              fl1 fl2 (true,ugraph)
 697             else
 698               false,ugraph
 699         | C.Cast (bo,_),t -> aux2 test_equality_only bo t ugraph
 700         | t,C.Cast (bo,_) -> aux2 test_equality_only t bo ugraph
 701         | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
 702         | (_,_) -> false,ugraph
 703   in
 704    let res =
 705     if !heuristic then
 706      aux2 test_equality_only t1 t2 ugraph
 707     else
 708      false,ugraph
 709    in
 710     if fst res = true then
 711      res
 712     else
 713 begin
 714 (*if !heuristic then prerr_endline ("NON FACILE: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*)
 715    (* heuristic := false; *)
 716    debug t1 [t2] "PREWHD";
 717 (*prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*)
 718 (*
 719 prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);
 720    let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
 721    let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
 722     debug t1' [t2'] "POSTWHD";
 723 *)
 724 let rec convert_machines ugraph =
 725  function
 726     [] -> true,ugraph
 727   | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl ->
 728      let (b,ugraph) as res =
 729       aux2 test_equality_only
 730        (R.unwind (k1,env1,ens1,h1,[])) (R.unwind (k2,env2,ens2,h2,[])) ugraph
 731      in
 732       if b then
 733        let problems =
 734         try
 735          Some
 736           (List.combine
 737             (List.map
 738               (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
 739               s1)
 740             (List.map
 741               (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
 742               s2)
 743           @ tl)
 744         with
 745          Invalid_argument _ -> None
 746        in
 747         match problems with
 748            None -> false,ugraph
 749          | Some problems -> convert_machines ugraph problems
 750       else
 751        res
 752 in
 753  convert_machines ugraph
 754   [R.reduce ~delta:true ~subst context (0,[],[],t1,[]),
 755    R.reduce ~delta:true ~subst context (0,[],[],t2,[])]
 756 (*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*)
 757 (*
 758     aux2 test_equality_only t1' t2' ugraph
 759 *)
 760 end
 761  in
 762   aux false (*c t1 t2 ugraph *)
 763 ;;
 764 *)
 765
 766 (* {{{ DEBUGGING ONLY
 767 let whd ?(delta=true) ?(subst=[]) context t =
 768  let res = whd ~delta ~subst context t in
 769  let rescsc = CicReductionNaif.whd ~delta ~subst context t in
 770   if not (fst (are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph)) then
 771    begin
 772     debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
 773     flush stderr ;
 774     debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
 775     flush stderr ;
 776     debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
 777     flush stderr ;
 778 fdebug := 0 ;
 779 let _ =  are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph in
 780     assert false ;
 781    end
 782   else
 783    res
 784 ;;
 785  }}} *)
 786
 787 (*let are_convertible = are_convertible whd*)
 788
 789 (* {{{ let profiler_other_whd = HExtlib.profile ~enable:profile "~are_convertible.whd"
 790 let whd ?(delta=true) ?(subst=[]) context t =
 791  let foo () =
 792   whd ~delta ~subst context t
 793  in
 794   profiler_other_whd.HExtlib.profile foo ()
 795  }}} *)
 796
 797 (* {{{ let rec normalize ?(delta=true) ?(subst=[]) ctx term =
 798   let module C = Cic in
 799   let t = whd ~delta ~subst ctx term in
 800   let aux = normalize ~delta ~subst in
 801   let decl name t = Some (name, C.Decl t) in
 802   match t with
 803   | C.Rel n -> t
 804   | C.Var (uri,exp_named_subst) ->
 805       C.Var (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
 806   | C.Meta (i,l) ->
 807       C.Meta (i,List.map (function Some t -> Some (aux ctx t) | None -> None) l)
 808   | C.Sort _ -> t
 809   | C.Implicit _ -> t
 810   | C.Cast (te,ty) -> C.Cast (aux ctx te, aux ctx ty)
 811   | C.Prod (n,s,t) ->
 812       let s' = aux ctx s in
 813       C.Prod (n, s', aux ((decl n s')::ctx) t)
 814   | C.Lambda (n,s,t) ->
 815       let s' = aux ctx s in
 816       C.Lambda (n, s', aux ((decl n s')::ctx) t)
 817   | C.LetIn (n,s,t) ->
 818       (* the term is already in weak head normal form *)
 819       assert false
 820   | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
 821   | C.Appl [] -> assert false
 822   | C.Const (uri,exp_named_subst) ->
 823       C.Const (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
 824   | C.MutInd (uri,typeno,exp_named_subst) ->
 825       C.MutInd (uri,typeno, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
 826   | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 827       C.MutConstruct (uri, typeno, consno,
 828         List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
 829   | C.MutCase (sp,i,outt,t,pl) ->
 830       C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl)
 831 (*CSC: to be completed, I suppose *)
 832   | C.Fix _ -> t
 833   | C.CoFix _ -> t
 834
 835 let normalize ?delta ?subst ctx term =
 836 (*  prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); *)
 837   let t = normalize ?delta ?subst ctx term in
 838 (*  prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); *)
 839   t
 840  }}} *)
 841
 842 (* {{{ performs an head beta/cast reduction
 843 let rec head_beta_reduce ?(delta=false) ?(upto=(-1)) t =
 844  match upto with
 845     0 -> t
 846   | n ->
 847     match t with
 848        (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
 849          let he'' = CicSubstitution.subst he' t in
 850           if tl' = [] then
 851            he''
 852           else
 853            let he''' =
 854             match he'' with
 855                Cic.Appl l -> Cic.Appl (l@tl')
 856              | _ -> Cic.Appl (he''::tl')
 857            in
 858             head_beta_reduce ~delta ~upto:(upto - 1) he'''
 859      | Cic.Cast (te,_) -> head_beta_reduce ~delta ~upto te
 860      | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true ->
 861         let bo =
 862          match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
 863             Cic.Constant (_,bo,_,_,_) -> bo
 864           | Cic.Variable _ -> raise ReferenceToVariable
 865           | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
 866           | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 867         in
 868          (match bo with
 869              None -> t
 870            | Some bo ->
 871               head_beta_reduce ~upto
 872                ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl)))
 873      | Cic.Const (uri,ens) as t when delta=true ->
 874         let bo =
 875          match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
 876             Cic.Constant (_,bo,_,_,_) -> bo
 877           | Cic.Variable _ -> raise ReferenceToVariable
 878           | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
 879           | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 880         in
 881          (match bo with
 882              None -> t
 883            | Some bo ->
 884               head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo))
 885      | t -> t
 886  }}} *)
 887
 888 (* {{{
 889 let are_convertible ?subst ?metasenv context t1 t2 ugraph =
 890  let before = Unix.gettimeofday () in
 891  let res = are_convertible ?subst ?metasenv context t1 t2 ugraph in
 892  let after = Unix.gettimeofday () in
 893  let diff = after -. before in
 894   if diff > 0.1 then
 895    begin
 896     let nc = List.map (function None -> None | Some (n,_) -> Some n) context in
 897      prerr_endline
 898       ("\n#(" ^ string_of_float diff ^ "):\n" ^ CicPp.pp t1 nc ^ "\n<=>\n" ^ CicPp.pp t2 nc);
 899    end;
 900   res
 901  }}} *)
 902
 903 (* vim:set foldmethod=marker: *)