exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
-let debug_print = fun _ -> ()
+let debug = false
+let profile = false
+let debug_print s = if debug then prerr_endline (Lazy.force s)
let fdebug = ref 1;;
let debug t env s =
CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
in
if !fdebug = 0 then
- debug_print (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
+ debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) ""))
;;
module type Strategy =
)
| C.Var (uri,exp_named_subst) ->
(*
-debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
+debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens))) ;
*)
if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
| _::tl -> filter_and_lift already_instantiated tl
(*
| (uri,_)::tl ->
-debug_print ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
+debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ;
if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
-exp_named_subst' then debug_print "---- OK1" ;
-debug_print ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-if List.mem uri params then debug_print "---- OK2" ;
+exp_named_subst' then debug_print (lazy "---- OK1") ;
+debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
+if List.mem uri params then debug_print (lazy "---- OK2") ;
filter_and_lift tl
*)
in
unwind_aux m t
;;
+ let unwind = unwind' 0;;
+
+(*
let unwind =
- unwind' 0
+ 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
try
reduce context (0, [], [], t, [])
with Not_found ->
- debug_print (CicPp.ppterm t) ;
+ debug_print (lazy (CicPp.ppterm t)) ;
raise Not_found
;;
*)
;;
-(* 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 ("PRIMA: " ^ CicPp.ppterm t) ;
- flush stderr ;
- debug_print ("DOPO: " ^ CicPp.ppterm res) ;
- flush stderr ;
- debug_print ("CSC: " ^ CicPp.ppterm rescsc) ;
- flush stderr ;
-CicReductionNaif.fdebug := 0 ;
-let _ = CicReductionNaif.are_convertible context res rescsc in
- assert false ;
- end
- else
- res
-;;
-*)
end
;;
-(*
-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
module R = Reduction
LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
-module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
+ OK 59.058s
+module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
module R = Reduction
- ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
+ ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
+module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
*)
module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
module U = UriManager;;
-let whd = R.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 = (Pervasives.compare x y = 0)
+let (===) x y =
+ Pervasives.compare x y = 0
(* t1, t2 must be well-typed *)
-let are_convertible ?(subst=[]) ?(metasenv=[]) =
+let are_convertible whd ?(subst=[]) ?(metasenv=[]) =
let rec aux test_equality_only context t1 t2 ugraph =
let aux2 test_equality_only t1 t2 ugraph =
else
false,ugraph
| (C.Cast _, _) | (_, C.Cast _)
- | (C.Implicit _, _) | (_, C.Implicit _) ->
- assert false
+ | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| (_,_) -> false,ugraph
end
in
(*
(match t1 with
Cic.Meta _ ->
- debug_print (CicPp.ppterm t1);
- debug_print (CicPp.ppterm (whd ~subst context t1));
- debug_print (CicPp.ppterm t2);
- debug_print (CicPp.ppterm (whd ~subst context t2))
+ debug_print (lazy (CicPp.ppterm t1));
+ debug_print (lazy (CicPp.ppterm (whd ~subst context t1)));
+ debug_print (lazy (CicPp.ppterm t2));
+ debug_print (lazy (CicPp.ppterm (whd ~subst context t2)))
| _ -> ()); *)
- 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
debug t1' [t2'] "POSTWHD";
aux2 test_equality_only t1' t2' ugraph
end
aux false (*c t1 t2 ugraph *)
;;
+(* 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 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) ->
let s' = aux ctx s in
C.Lambda (n, s', aux ((decl n s')::ctx) t)
| C.LetIn (n,s,t) ->
- let s' = aux ctx s in
- C.LetIn (n, s, aux ((def n s')::ctx) t)
+ (* the term is already in weak head normal form *)
+ assert false
| C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
| C.Appl [] -> assert false
| C.Const (uri,exp_named_subst) ->
List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
| C.MutCase (sp,i,outt,t,pl) ->
C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl)
+(*CSC: to be completed, I suppose *)
| C.Fix _ -> t
| C.CoFix _ -> t