- (k, e, _, (C.Rel n as t), s) ->
+ (k, e, _, C.Rel n, s) ->
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 *)
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)
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
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
| (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
let decofix =
function
let (_,_,body) = List.nth fl i in
let body' =
let counter = ref (List.length fl) in
let (_,_,body) = List.nth fl i in
let body' =
let counter = ref (List.length fl) in
-(* DEBUGGING ONLY
-let whd context t =
- let res = whd context t in
- let rescsc = CicReductionNaif.whd context t in
- if not (CicReductionNaif.are_convertible context res rescsc) then
- begin
- debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
- flush stderr ;
- debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
- flush stderr ;
- debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
- flush stderr ;
-CicReductionNaif.fdebug := 0 ;
-let _ = CicReductionNaif.are_convertible context res rescsc in
- assert false ;
- end
- else
- res
-;;
-*)
-(*
-module R = Reduction CallByNameStrategy;;
-module R = Reduction CallByValueStrategy;;
-module R = Reduction CallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByValueStrategy;;
-module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByNameStrategy;;
+(* ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
+ senza ridurre la testa
+module R = Reduction CallByNameStrategy;; OK 56.368s
+module R = Reduction CallByValueStrategy;; ROTTO
+module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
+module R = Reduction LazyCallByValueStrategy;; ROTTO
+module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
+module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
(* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
* fallbacks to structural equality *)
(* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
* fallbacks to structural equality *)
- let t1' = whd ~subst context t1 in
- let t2' = whd ~subst context t2 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
+(* DEBUGGING ONLY
+let whd ?(delta=true) ?(subst=[]) context t =
+ let res = whd ~delta ~subst context t in
+ let rescsc = CicReductionNaif.whd ~delta ~subst context t in
+ if not (fst (are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph)) then
+ begin
+ debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
+ flush stderr ;
+ debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
+ flush stderr ;
+ debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
+ flush stderr ;
+fdebug := 0 ;
+let _ = are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph in
+ assert false ;
+ end
+ else
+ res
+;;
+*)
+
+let are_convertible = 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 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