exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
+let debug_print = fun _ -> ()
+
let fdebug = ref 1;;
let debug t env s =
let rec debug_aux t i =
CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
in
if !fdebug = 0 then
- prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
+ debug_print (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
;;
module type Strategy =
)
| C.Var (uri,exp_named_subst) ->
(*
-prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
+debug_print ("%%%%%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 ->
-prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
-if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
-prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-if List.mem uri params then prerr_endline "---- OK2" ;
+debug_print ("---- 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" ;
filter_and_lift tl
*)
in
unwind' 0
;;
- let reduce ?(subst = []) context : config -> Cic.term =
+ let reduce ~delta ?(subst = []) context : config -> Cic.term =
let module C = Cic in
let module S = CicSubstitution in
let rec reduce =
| (k, e, ens, C.Appl l, s) ->
C.Appl (List.append (List.map (unwind k e ens) l) s)
*)
+ | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) when delta=false->
+ let t' = unwind k e ens t in
+ if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
| (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
(let o,_ =
CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
try
reduce context (0, [], [], t, [])
with Not_found ->
- prerr_endline (CicPp.ppterm t) ;
+ debug_print (CicPp.ppterm t) ;
raise Not_found
;;
*)
- let rec whd ?(subst=[]) context t =
- reduce ~subst context (0, [], [], t, [])
+ let rec whd ?(delta=true) ?(subst=[]) context t =
+ reduce ~delta ~subst context (0, [], [], t, [])
;;
let rescsc = CicReductionNaif.whd context t in
if not (CicReductionNaif.are_convertible context res rescsc) then
begin
- prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
+ debug_print ("PRIMA: " ^ CicPp.ppterm t) ;
flush stderr ;
- prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
+ debug_print ("DOPO: " ^ CicPp.ppterm res) ;
flush stderr ;
- prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
+ debug_print ("CSC: " ^ CicPp.ppterm rescsc) ;
flush stderr ;
CicReductionNaif.fdebug := 0 ;
let _ = CicReductionNaif.are_convertible context res rescsc in
(*
(match t1 with
Cic.Meta _ ->
- prerr_endline (CicPp.ppterm t1);
- prerr_endline (CicPp.ppterm (whd ~subst context t1));
- prerr_endline (CicPp.ppterm t2);
- prerr_endline (CicPp.ppterm (whd ~subst context t2))
+ 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))
| _ -> ()); *)
let t1' = whd ~subst context t1 in
let t2' = whd ~subst context t2 in
aux false (*c t1 t2 ugraph *)
;;
+
+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
+ match t with
+ | C.Rel n -> t
+ | C.Var (uri,exp_named_subst) ->
+ C.Var (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
+ | C.Meta (i,l) ->
+ C.Meta (i,List.map (function Some t -> Some (aux ctx t) | None -> None) l)
+ | C.Sort _ -> t
+ | C.Implicit _ -> t
+ | C.Cast (te,ty) -> C.Cast (aux ctx te, aux ctx ty)
+ | C.Prod (n,s,t) ->
+ let s' = aux ctx s in
+ C.Prod (n, s', aux ((decl n s')::ctx) t)
+ | C.Lambda (n,s,t) ->
+ 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)
+ | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
+ | C.Appl [] -> assert false
+ | C.Const (uri,exp_named_subst) ->
+ C.Const (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
+ | C.MutInd (uri,typeno,exp_named_subst) ->
+ C.MutInd (uri,typeno, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
+ | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+ C.MutConstruct (uri, typeno, consno,
+ 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)
+ | C.Fix _ -> t
+ | C.CoFix _ -> t
+
+let normalize ?delta ?subst ctx term =
+(* prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); *)
+ let t = normalize ?delta ?subst ctx term in
+(* prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); *)
+ t
+
+