helm/software/components/ng_kernel/nCicReduction.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id$ *)
  13
  14 (* TODO unify exceptions *)
  15
  16 module type Strategy =
  17  sig
  18   type stack_term
  19   type env_term
  20   type config = int * env_term list * NCic.term * stack_term list
  21   val to_env :
  22    reduce: (config -> config) ->
  23    unwind: (config -> NCic.term) ->
  24    config -> env_term
  25   val from_stack : stack_term -> config
  26   val from_stack_list_for_unwind :
  27    unwind: (config -> NCic.term) ->
  28    stack_term list -> NCic.term list
  29   val from_env : env_term -> config
  30   val from_env_for_unwind :
  31    unwind: (config -> NCic.term) ->
  32    env_term -> NCic.term
  33   val stack_to_env :
  34    reduce: (config -> config) ->
  35    unwind: (config -> NCic.term) ->
  36    stack_term -> env_term
  37   val compute_to_env :
  38    reduce: (config -> config) ->
  39    unwind: (config -> NCic.term) ->
  40    int -> env_term list ->
  41     NCic.term -> env_term
  42   val compute_to_stack :
  43    reduce: (config -> config) ->
  44    unwind: (config -> NCic.term) ->
  45    config -> stack_term
  46  end
  47 ;;
  48
  49 module CallByValueByNameForUnwind' =
  50  struct
  51   type config = int * env_term list * NCic.term * stack_term list
  52   and stack_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
  53   and env_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
  54   let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c)
  55   let from_stack (c,_) = Lazy.force c
  56   let from_stack_list_for_unwind ~unwind:_ l =
  57    List.map (function (_,c) -> Lazy.force c) l
  58   let from_env (c,_) = Lazy.force c
  59   let from_env_for_unwind ~unwind:_ (_,c) = Lazy.force c
  60   let stack_to_env ~reduce:_ ~unwind:_ config = config
  61   let compute_to_env ~reduce ~unwind k e t =
  62    lazy (reduce (k,e,t,[])), lazy (unwind (k,e,t,[]))
  63   let compute_to_stack ~reduce ~unwind config =
  64    lazy (reduce config), lazy (unwind config)
  65  end
  66 ;;
  67
  68
  69 (* {{{ module CallByValueByNameForUnwind =
  70  struct
  71   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
  72   and stack_term = config
  73   and env_term = config * config (* cbv, cbn *)
  74   and ens_term = config * config (* cbv, cbn *)
  75
  76   let to_env c = c,c
  77   let to_ens c = c,c
  78   let from_stack config = config
  79   let from_stack_list_for_unwind ~unwind l = List.map unwind l
  80   let from_env (c,_) = c
  81   let from_ens (c,_) = c
  82   let from_env_for_unwind ~unwind (_,c) = unwind c
  83   let from_ens_for_unwind ~unwind (_,c) = unwind c
  84   let stack_to_env ~reduce ~unwind config = reduce config, (0,[],[],unwind config,[])
  85   let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[]), (k,e,ens,t,[])
  86   let compute_to_stack ~reduce ~unwind config = config
  87  end
  88 ;;
  89
  90
  91 (* Old Machine *)
  92 module CallByNameStrategy =
  93  struct
  94   type stack_term = Cic.term
  95   type env_term = Cic.term
  96   type ens_term = Cic.term
  97   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
  98   let to_env v = v
  99   let to_ens v = v
 100   let from_stack ~unwind v = v
 101   let from_stack_list ~unwind l = l
 102   let from_env v = v
 103   let from_ens v = v
 104   let from_env_for_unwind ~unwind v = v
 105   let from_ens_for_unwind ~unwind v = v
 106   let stack_to_env ~reduce ~unwind v = v
 107   let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
 108   let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
 109  end
 110 ;;
 111
 112 module CallByNameStrategy =
 113  struct
 114   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 115   and stack_term = config
 116   and env_term = config
 117   and ens_term = config
 118
 119   let to_env c = c
 120   let to_ens c = c
 121   let from_stack config = config
 122   let from_stack_list_for_unwind ~unwind l = List.map unwind l
 123   let from_env c = c
 124   let from_ens c = c
 125   let from_env_for_unwind ~unwind c = unwind c
 126   let from_ens_for_unwind ~unwind c = unwind c
 127   let stack_to_env ~reduce ~unwind config = 0,[],[],unwind config,[]
 128   let compute_to_env ~reduce ~unwind k e ens t = k,e,ens,t,[]
 129   let compute_to_stack ~reduce ~unwind config = config
 130  end
 131 ;;
 132
 133 module CallByValueStrategy =
 134  struct
 135   type stack_term = Cic.term
 136   type env_term = Cic.term
 137   type ens_term = Cic.term
 138   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 139   let to_env v = v
 140   let to_ens v = v
 141   let from_stack ~unwind v = v
 142   let from_stack_list ~unwind l = l
 143   let from_env v = v
 144   let from_ens v = v
 145   let from_env_for_unwind ~unwind v = v
 146   let from_ens_for_unwind ~unwind v = v
 147   let stack_to_env ~reduce ~unwind v = v
 148   let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
 149   let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
 150  end
 151 ;;
 152
 153 module CallByValueStrategyByNameOnConstants =
 154  struct
 155   type stack_term = Cic.term
 156   type env_term = Cic.term
 157   type ens_term = Cic.term
 158   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 159   let to_env v = v
 160   let to_ens v = v
 161   let from_stack ~unwind v = v
 162   let from_stack_list ~unwind l = l
 163   let from_env v = v
 164   let from_ens v = v
 165   let from_env_for_unwind ~unwind v = v
 166   let from_ens_for_unwind ~unwind v = v
 167   let stack_to_env ~reduce ~unwind v = v
 168   let compute_to_stack ~reduce ~unwind k e ens =
 169    function
 170       Cic.Const _ as t -> unwind k e ens t
 171     | t -> reduce (k,e,ens,t,[])
 172   let compute_to_env ~reduce ~unwind k e ens =
 173    function
 174       Cic.Const _ as t -> unwind k e ens t
 175     | t -> reduce (k,e,ens,t,[])
 176  end
 177 ;;
 178
 179 module LazyCallByValueStrategy =
 180  struct
 181   type stack_term = Cic.term lazy_t
 182   type env_term = Cic.term lazy_t
 183   type ens_term = Cic.term lazy_t
 184   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 185   let to_env v = lazy v
 186   let to_ens v = lazy v
 187   let from_stack ~unwind v = Lazy.force v
 188   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 189   let from_env v = Lazy.force v
 190   let from_ens v = Lazy.force v
 191   let from_env_for_unwind ~unwind v = Lazy.force v
 192   let from_ens_for_unwind ~unwind v = Lazy.force v
 193   let stack_to_env ~reduce ~unwind v = v
 194   let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
 195   let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
 196  end
 197 ;;
 198
 199 module LazyCallByValueStrategyByNameOnConstants =
 200  struct
 201   type stack_term = Cic.term lazy_t
 202   type env_term = Cic.term lazy_t
 203   type ens_term = Cic.term lazy_t
 204   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 205   let to_env v = lazy v
 206   let to_ens v = lazy v
 207   let from_stack ~unwind v = Lazy.force v
 208   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 209   let from_env v = Lazy.force v
 210   let from_ens v = Lazy.force v
 211   let from_env_for_unwind ~unwind v = Lazy.force v
 212   let from_ens_for_unwind ~unwind v = Lazy.force v
 213   let stack_to_env ~reduce ~unwind v = v
 214   let compute_to_stack ~reduce ~unwind k e ens t =
 215    lazy (
 216     match t with
 217        Cic.Const _ as t -> unwind k e ens t
 218      | t -> reduce (k,e,ens,t,[]))
 219   let compute_to_env ~reduce ~unwind k e ens t =
 220    lazy (
 221     match t with
 222        Cic.Const _ as t -> unwind k e ens t
 223      | t -> reduce (k,e,ens,t,[]))
 224  end
 225 ;;
 226
 227 module LazyCallByNameStrategy =
 228  struct
 229   type stack_term = Cic.term lazy_t
 230   type env_term = Cic.term lazy_t
 231   type ens_term = Cic.term lazy_t
 232   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 233   let to_env v = lazy v
 234   let to_ens v = lazy v
 235   let from_stack ~unwind v = Lazy.force v
 236   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 237   let from_env v = Lazy.force v
 238   let from_ens v = Lazy.force v
 239   let from_env_for_unwind ~unwind v = Lazy.force v
 240   let from_ens_for_unwind ~unwind v = Lazy.force v
 241   let stack_to_env ~reduce ~unwind v = v
 242   let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
 243   let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
 244  end
 245 ;;
 246
 247 module
 248  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
 249 =
 250  struct
 251   type stack_term = reduce:bool -> Cic.term
 252   type env_term = reduce:bool -> Cic.term
 253   type ens_term = reduce:bool -> Cic.term
 254   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 255   let to_env v =
 256    let value = lazy v in
 257     fun ~reduce -> Lazy.force value
 258   let to_ens v =
 259    let value = lazy v in
 260     fun ~reduce -> Lazy.force value
 261   let from_stack ~unwind v = (v ~reduce:false)
 262   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 263   let from_env v = (v ~reduce:true)
 264   let from_ens v = (v ~reduce:true)
 265   let from_env_for_unwind ~unwind v = (v ~reduce:true)
 266   let from_ens_for_unwind ~unwind v = (v ~reduce:true)
 267   let stack_to_env ~reduce ~unwind v = v
 268   let compute_to_stack ~reduce ~unwind k e ens t =
 269    let svalue =
 270      lazy (
 271       match t with
 272          Cic.Const _ as t -> unwind k e ens t
 273        | t -> reduce (k,e,ens,t,[])
 274      ) in
 275    let lvalue =
 276     lazy (unwind k e ens t)
 277    in
 278     fun ~reduce ->
 279      if reduce then Lazy.force svalue else Lazy.force lvalue
 280   let compute_to_env ~reduce ~unwind k e ens t =
 281    let svalue =
 282      lazy (
 283       match t with
 284          Cic.Const _ as t -> unwind k e ens t
 285        | t -> reduce (k,e,ens,t,[])
 286      ) in
 287    let lvalue =
 288     lazy (unwind k e ens t)
 289    in
 290     fun ~reduce ->
 291      if reduce then Lazy.force svalue else Lazy.force lvalue
 292  end
 293 ;;
 294
 295 module ClosuresOnStackByValueFromEnvOrEnsStrategy =
 296  struct
 297   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 298   and stack_term = config
 299   and env_term = config
 300   and ens_term = config
 301
 302   let to_env config = config
 303   let to_ens config = config
 304   let from_stack config = config
 305   let from_stack_list_for_unwind ~unwind l = List.map unwind l
 306   let from_env v = v
 307   let from_ens v = v
 308   let from_env_for_unwind ~unwind config = unwind config
 309   let from_ens_for_unwind ~unwind config = unwind config
 310   let stack_to_env ~reduce ~unwind config = reduce config
 311   let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[])
 312   let compute_to_stack ~reduce ~unwind config = config
 313  end
 314 ;;
 315
 316 module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
 317  struct
 318   type stack_term =
 319    int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
 320   type env_term = Cic.term
 321   type ens_term = Cic.term
 322   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
 323   let to_env v = v
 324   let to_ens v = v
 325   let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
 326   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 327   let from_env v = v
 328   let from_ens v = v
 329   let from_env_for_unwind ~unwind v = v
 330   let from_ens_for_unwind ~unwind v = v
 331   let stack_to_env ~reduce ~unwind (k,e,ens,t) =
 332    match t with
 333       Cic.Const _ as t -> unwind k e ens t
 334     | t -> reduce (k,e,ens,t,[])
 335   let compute_to_env ~reduce ~unwind k e ens t =
 336    unwind k e ens t
 337   let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
 338  end
 339 ;;
 340
 341 }}} *)
 342
 343 module Reduction(RS : Strategy) =
 344  struct
 345   type env = RS.env_term list
 346   type stack = RS.stack_term list
 347   type config = int * env * NCic.term * stack
 348
 349   let rec unwind (k,e,t,s) =
 350     let t =
 351       if k = 0 then t
 352       else
 353         NCicSubstitution.psubst ~avoid_beta_redexes:true
 354           (RS.from_env_for_unwind ~unwind) e t
 355     in
 356     if s = [] then t
 357     else NCic.Appl(t::(RS.from_stack_list_for_unwind ~unwind s))
 358   ;;
 359
 360   let list_nth l n = try List.nth l n with Failure _ -> assert false;;
 361   let rec replace i s t =
 362     match i,s with
 363     |  0,_::tl -> t::tl
 364     | n,he::tl -> he::(replace (n - 1) tl t)
 365     | _,_ -> assert false
 366   ;;
 367
 368   let rec reduce ~delta ?(subst = []) context : config -> config =
 369    let rec aux = function
 370      | k, e, NCic.Rel n, s when n <= k ->
 371         let k',e',t',s' = RS.from_env (list_nth e (n-1)) in
 372         aux (k',e',t',s'@s)
 373      | k, _, NCic.Rel n, s as config (* when n > k *) ->
 374         let x= try Some (List.nth context (n - 1 - k)) with Failure _ -> None in
 375          (match x with
 376          | Some(_,NCic.Def(x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s)
 377          | _ -> config)
 378      | (k, e, NCic.Meta (n,l), s) as config ->
 379         (try
 380            let _,_, term,_ = NCicUtils.lookup_subst n subst in
 381            aux (k, e, NCicSubstitution.subst_meta l term,s)
 382          with  NCicUtils.Subst_not_found _ -> config)
 383      | (_, _, NCic.Sort _, _) as config -> config
 384      | (_, _, NCic.Implicit _, _) -> assert false
 385      | (_, _, NCic.Prod _, _) as config -> config
 386      | (_, _, NCic.Lambda _, []) as config -> config
 387      | (k, e, NCic.Lambda (_,_,t), p::s) ->
 388          aux (k+1, (RS.stack_to_env ~reduce:aux ~unwind p)::e, t,s)
 389      | (k, e, NCic.LetIn (_,_,m,t), s) ->
 390         let m' = RS.compute_to_env ~reduce:aux ~unwind k e m in
 391          aux (k+1, m'::e, t, s)
 392      | (_, _, NCic.Appl [], _) -> assert false
 393      | (k, e, NCic.Appl (he::tl), s) ->
 394         let tl' =
 395          List.map (fun t->RS.compute_to_stack ~reduce:aux ~unwind (k,e,t,[])) tl
 396         in
 397          aux (k, e, he, tl' @ s)
 398      | (_, _, NCic.Const
 399             (NReference.Ref (_,NReference.Def height) as refer), s) as config ->
 400          if delta >= height then config else
 401            let _,_,body,_,_,_ = NCicEnvironment.get_checked_def refer in
 402            aux (0, [], body, s)
 403      | (_, _, NCic.Const (NReference.Ref (_,
 404             (NReference.Decl|NReference.Ind _|NReference.Con _|NReference.CoFix _))), _) as config -> config
 405      | (_, _, NCic.Const (NReference.Ref
 406            (_,NReference.Fix (fixno,recindex,height)) as refer),s) as config ->
 407         if delta >= height then config else
 408         (match
 409           try Some (RS.from_stack (List.nth s recindex))
 410           with Failure _ -> None
 411         with
 412         | None -> config
 413         | Some recparam ->
 414            let fixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
 415            match reduce ~delta:0 ~subst context recparam with
 416            | (_,_,NCic.Const (NReference.Ref (_,NReference.Con _)), _) as c ->
 417                let new_s =
 418                  replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c)
 419                in
 420                let _,_,_,_,body = List.nth fixes fixno in
 421                aux (0, [], body, new_s)
 422            | _ -> config)
 423      | (k, e, NCic.Match (_,_,term,pl),s) as config ->
 424         let decofix = function
 425           | (_,_,NCic.Const(NReference.Ref(_,NReference.CoFix c)as refer),s)->
 426              let cofixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
 427              let _,_,_,_,body = List.nth cofixes c in
 428              reduce ~delta:0 ~subst context (0,[],body,s)
 429           | config -> config
 430         in
 431         (match decofix (reduce ~delta:0 ~subst context (k,e,term,[])) with
 432         | (_, _, NCic.Const (NReference.Ref (_,NReference.Con (_,j))),[]) ->
 433             aux (k, e, List.nth pl (j-1), s)
 434         | (_, _, NCic.Const
 435              (NReference.Ref (_,NReference.Con (_,j)) as refer), s') ->
 436           let leftno = NCicEnvironment.get_indty_leftno refer in
 437           let _,params = HExtlib.split_nth leftno s' in
 438           aux (k, e, List.nth pl (j-1), params@s)
 439         | _ -> config)
 440    in
 441     aux
 442   ;;
 443
 444   let whd ?(delta=0) ?(subst=[]) context t =
 445    unwind (reduce ~delta ~subst context (0, [], t, []))
 446   ;;
 447
 448  end
 449 ;;
 450
 451
 452 (* {{{ ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
 453            senza ridurre la testa
 454 module R = Reduction CallByNameStrategy;; OK 56.368s
 455 module R = Reduction CallByValueStrategy;; ROTTO
 456 module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
 457 module R = Reduction LazyCallByValueStrategy;; ROTTO
 458 module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
 459 module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
 460 module R = Reduction
 461  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
 462  OK 59.058s
 463 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
 464 module R = Reduction
 465  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
 466 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 467 module R = Reduction(CallByValueByNameForUnwind);;
 468 module R = Reduction(CallByNameStrategy);;
 469 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;}}} *)
 470 module RS = CallByValueByNameForUnwind';;
 471
 472 module R = Reduction(RS);;
 473 module U = UriManager;;
 474
 475 let whd = R.whd
 476
 477 (*
 478 let whd =
 479  let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
 480   fun ?(delta=true) ?(subst=[]) context t ->
 481    profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
 482 *)
 483
 484 (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
 485  * fallbacks to structural equality *)
 486 let (===) x y = Pervasives.compare x y = 0 ;;
 487
 488 module C = NCic
 489
 490 (* t1, t2 must be well-typed *)
 491 let are_convertible whd ?(subst=[])  =
 492  let rec aux test_eq_only context t1 t2 =
 493    let rec alpha_eq test_eq_only t1 t2 =
 494      if t1 === t2 then
 495        true
 496      else
 497        match (t1,t2) with
 498        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> a <= b
 499        | (C.Sort s1,C.Sort (C.Type _)) -> (not test_eq_only)
 500        | (C.Sort s1, C.Sort s2) -> s1 = s2
 501
 502        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 503            aux true context s1 s2 &&
 504            aux test_eq_only ((name1, C.Decl s1)::context) t1 t2
 505        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
 506           aux true context s1 s2 &&
 507           aux test_eq_only ((name1, C.Decl s1)::context) t1 t2
 508        | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
 509           aux test_eq_only context ty1 ty2 &&
 510           aux test_eq_only context s1 s2 &&
 511           aux test_eq_only ((name1, C.Def (s1,ty1))::context) t1 t2
 512
 513        | (C.Meta (n1,(s1, C.Irl i1)), C.Meta (n2,(s2, C.Irl i2)))
 514           when n1 = n2 && s1 = s2 -> true
 515        | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 &&
 516           let l1 = NCicUtils.expand_local_context l1 in
 517           let l2 = NCicUtils.expand_local_context l2 in
 518           (try List.for_all2
 519             (fun t1 t2 -> aux test_eq_only context
 520               (NCicSubstitution.lift s1 t1)
 521               (NCicSubstitution.lift s2 t2))
 522             l1 l2
 523           with Invalid_argument _ -> assert false) -> true
 524
 525        | C.Meta (n1,l1), _ ->
 526           (try
 527              let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
 528              let term = NCicSubstitution.subst_meta l1 term in
 529               aux test_eq_only context term t2
 530            with NCicUtils.Subst_not_found _ -> false)
 531        | _, C.Meta (n2,l2) ->
 532           (try
 533              let _,_,term,_ = NCicUtils.lookup_subst n2 subst in
 534              let term = NCicSubstitution.subst_meta l2 term in
 535               aux test_eq_only context t1 term
 536            with NCicUtils.Subst_not_found _ -> false)
 537
 538        | (C.Appl (C.Const r1::tl1), C.Appl (C.Const r2::tl2)) ->
 539           r1 = r2 &&
 540            let relevance = NCicEnvironment.get_relevance r1 in
 541            (try
 542              HExtlib.list_forall_default3
 543               (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
 544               tl1 tl2 true relevance
 545             with Invalid_argument _ -> false)
 546
 547        | (C.Appl l1, C.Appl l2) ->
 548           (try List.for_all2 (aux test_eq_only context) l1 l2
 549            with Invalid_argument _ -> false)
 550
 551        | (C.Match (ref1,outtype1,term1,pl1),
 552           C.Match (ref2,outtype2,term2,pl2)) ->
 553            NReference.eq ref1 ref2 &&
 554            aux test_eq_only context outtype1 outtype2 &&
 555            aux test_eq_only context term1 term2 &&
 556            (try List.for_all2 (aux test_eq_only context) pl1 pl2
 557             with Invalid_argument _ -> false)
 558
 559        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
 560        | (_,_) -> false
 561   in
 562    if alpha_eq test_eq_only t1 t2 then
 563      true
 564    else
 565      let height_of = function
 566       | NCic.Const (NReference.Ref (_,NReference.Def h))
 567       | NCic.Const (NReference.Ref (_,NReference.Fix (_,_,h)))
 568       | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Def h))::_)
 569       | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Fix (_,_,h)))::_) -> h
 570       | _ -> 0
 571      in
 572      let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
 573        let h1 = height_of t1 in
 574        let h2 = height_of t2 in
 575        let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
 576        R.reduce ~delta ~subst context m1,
 577        R.reduce ~delta ~subst context m2,
 578        delta
 579      in
 580      let rec convert_machines ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) =
 581        (alpha_eq test_eq_only
 582          (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[])) &&
 583         let relevance =
 584           match t1 with
 585               C.Const r -> NCicEnvironment.get_relevance r
 586             | _ -> [] in
 587         try
 588          HExtlib.list_forall_default3
 589            (fun t1 t2 b  ->
 590              not b ||
 591              let t1 = RS.from_stack t1 in
 592              let t2 = RS.from_stack t2 in
 593              convert_machines (small_delta_step t1 t2)) s1 s2 true relevance
 594         with Invalid_argument _ -> false) ||
 595        (delta > 0 &&
 596           let delta = delta - 1 in
 597           let red = R.reduce ~delta ~subst context in
 598           convert_machines (red m1,red m2,delta))
 599      in
 600      convert_machines (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
 601  in
 602   aux false
 603 ;;
 604
 605 let are_convertible = are_convertible whd
 606
 607 let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l =
 608  match upto, t, l with
 609   | 0, C.Appl l1, _ -> C.Appl (l1 @ l)
 610   | 0, t, [] -> t
 611   | 0, t, _ -> C.Appl (t::l)
 612   | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto hd (tl @ l)
 613   | _, C.Lambda(_,_,bo), arg::tl ->
 614      let bo = NCicSubstitution.subst arg bo in
 615      head_beta_reduce ~delta ~upto:(upto - 1) bo tl
 616   | _, C.Const (NReference.Ref (_, NReference.Def height) as re), _
 617     when delta <= height ->
 618       let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in
 619       head_beta_reduce ~upto ~delta bo l
 620   | _, t, [] -> t
 621   | _, t, _ -> C.Appl (t::l)
 622 ;;
 623
 624 let head_beta_reduce ?delta ?upto t = head_beta_reduce ?delta ?upto t [];;
 625
 626 (* vim:set foldmethod=marker: *)