exception ReferenceToInductiveDefinition;;
let debug = false
+let profile = false
let debug_print s = if debug then prerr_endline (Lazy.force s)
let fdebug = ref 1;;
unwind_aux m t
;;
-let profiler_unwind = HExtlib.profile "are_convertible.unwind"
- let unwind k e ens t =
-let foo () =
- unwind' 0 k e ens t
-in
- profiler_unwind.HExtlib.profile foo ()
+ let unwind = unwind' 0;;
+
+(*
+ let unwind =
+ let profiler_unwind = HExtlib.profile ~enable:profile "are_convertible.unwind" in
+ fun k e ens t ->
+ profiler_unwind.HExtlib.profile (unwind k e ens) t
;;
+*)
let reduce ~delta ?(subst = []) context : config -> Cic.term =
let module C = Cic in
let module S = CicSubstitution in
let rec reduce =
function
- (k, e, _, (C.Rel n as t), s) ->
+ (k, e, _, C.Rel n, s) ->
let d =
try
Some (RS.from_env (List.nth e (n-1)))
if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
| (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
| (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
- | (k, e, ens, (C.Cast (te,ty) as t), s) ->
+ | (k, e, ens, C.Cast (te,ty), s) ->
reduce (k, e, ens, te, s) (* s should be empty *)
| (k, e, ens, (C.Prod _ as t), s) ->
unwind k e ens t (* s should be empty *)
| (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t'
| (k, e, ens, C.Lambda (_,_,t), p::s) ->
reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
- | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
+ | (k, e, ens, C.LetIn (_,m,t), s) ->
let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
reduce (k+1, m'::e, ens, t, s)
| (_, _, _, C.Appl [], _) -> assert false
| (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
let decofix =
function
- C.CoFix (i,fl) as t ->
+ C.CoFix (i,fl) ->
let (_,_,body) = List.nth fl i in
let body' =
let counter = ref (List.length fl) in
module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
module U = UriManager;;
-let profiler_whd = HExtlib.profile "are_convertible.whd"
let whd = R.whd
+(*
+let whd =
+ let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
+ fun ?(delta=true) ?(subst=[]) context t ->
+ profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
+*)
+
(* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
* fallbacks to structural equality *)
let (===) x y =
debug_print (lazy (CicPp.ppterm t2));
debug_print (lazy (CicPp.ppterm (whd ~subst context t2)))
| _ -> ()); *)
- let t1' =
- let foo () =
-whd ?delta:(Some true) ?subst:(Some subst) context t1
- in
- profiler_whd.HExtlib.profile foo ()
-in
- let t2' =
- let foo () =
-whd ?delta:(Some true) ?subst:(Some subst) context t2
- in
- profiler_whd.HExtlib.profile foo ()
-in
+ let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
+ let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
debug t1' [t2'] "POSTWHD";
aux2 test_equality_only t1' t2' ugraph
end
let are_convertible = are_convertible whd
-let profiler_other_whd = HExtlib.profile "~are_convertible.whd"
+let whd = R.whd
+
+(*
+let profiler_other_whd = HExtlib.profile ~enable:profile "~are_convertible.whd"
let whd ?(delta=true) ?(subst=[]) context t =
let foo () =
whd ~delta ~subst context t
in
profiler_other_whd.HExtlib.profile foo ()
+*)
let rec normalize ?(delta=true) ?(subst=[]) ctx term =
let module C = Cic in
let t = whd ~delta ~subst ctx term in
let aux = normalize ~delta ~subst in
let decl name t = Some (name, C.Decl t) in
- let def name t = Some (name, C.Def (t,None)) in
+ let def name t = Some (name, C.Def (t,None)) in
match t with
| C.Rel n -> t
| C.Var (uri,exp_named_subst) ->