let macro = Grammar.Entry.create grammar "macro"
let script = Grammar.Entry.create grammar "script"
let statement = Grammar.Entry.create grammar "statement"
+let statements = Grammar.Entry.create grammar "statements"
let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
vars body
EXTEND
- GLOBAL: term term0 statement;
+ GLOBAL: term term0 statement statements;
int: [
[ num = NUM ->
try
| com = comment -> TacticAst.Comment (loc, com)
]
];
+ statements: [
+ [ l = LIST0 [ statement ] -> l
+ ]
+ ];
END
let exc_located_wrapper f =
exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream))
let parse_statement stream =
exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
+let parse_statements stream =
+ exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream))
+
(**/**)
val parse_term: char Stream.t -> DisambiguateTypes.term
val parse_statement: char Stream.t -> (CicAst.term, string) TacticAst.statement
+val parse_statements:
+ char Stream.t -> (CicAst.term, string) TacticAst.statement list
(** {2 Grammar extensions} *)
Cic.MutConstruct (uri, i, j, mk_subst uris)
| Cic.Meta _ | Cic.Implicit _ as t ->
(*
- prerr_endline (sprintf
+ debug_print (sprintf
"Warning: %s must be instantiated with _[%s] but we do not enforce it"
(CicPp.ppterm t)
(String.concat "; "
try
CicUtil.term_of_uri uri
with exn ->
- prerr_endline uri;
- prerr_endline (Printexc.to_string exn);
+ debug_print uri;
+ debug_print (Printexc.to_string exn);
assert false
in
fun _ _ _ -> term))
(fun dom_item ->
try
let len = List.length (lookup_choices dom_item) in
- prerr_endline (sprintf "BENCHMARK %s: %d"
+ debug_print (sprintf "BENCHMARK %s: %d"
(string_of_domain_item dom_item) len);
len
with No_choices _ -> 0)
(*
(if benchmark then
let res_size = List.length res in
- prerr_endline (sprintf
+ debug_print (sprintf
("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
"BENCHMARK: estimated %.2f")
!actual_refinements !max_refinements !domain_size res_size
exception Elim_failure of string
exception Can_t_eliminate
+let debug_print = fun _ -> ()
+
let fresh_binder =
let counter = ref ~-1 in
function
add_params (fun b s t -> Cic.Lambda (b, s, t)) leftno ty cic
in
(*
-prerr_endline (CicPp.ppterm eliminator_type);
-prerr_endline (CicPp.ppterm eliminator_body);
+debug_print (CicPp.ppterm eliminator_type);
+debug_print (CicPp.ppterm eliminator_body);
*)
let (computed_type, ugraph) =
try
let trust = ref (fun _ -> true);;
let set_trust f = trust := f
let trust_obj uri = !trust uri
-
+let debug_print = fun _ -> ()
(* ************************************************************************** *
TYPES
frozen_list := List.remove_assoc uri !frozen_list;
frozen_list := (uri,(o,Some real_ugraph))::!frozen_list;
| Some g ->
- prerr_endline (
+ debug_print (
"You are probably hacking an object already hacked or an"^
" object that has the universe file but is not"^
" yet committed.");
assert false
with
Not_found ->
- prerr_endline (
+ debug_print (
"You are hacking an object that is not in the"^
" frozen_list, this means you are probably generating an"^
" universe file for an object that already"^
(Some (CicUniv.ugraph_of_xml filename_univ),Some filename_univ)
with Failure s ->
- prerr_endline (
+ debug_print (
"WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri));
Inix.unlink
None,None
let set_type_checking_info ?(replace_ugraph=None) uri =
(*
if not (Cache.can_be_cooked uri) && replace_ugraph <> None then begin
- prerr_endline (
+ debug_print (
"?replace_ugraph must be None if you are not committing an "^
"object that has a universe graph associated "^
"(can happen only in the fase of universes graphs generation).");
match Cache.can_be_cooked uri, replace_ugraph with
| true, Some _
| false, None ->
- prerr_endline (
+ debug_print (
"?replace_ugraph must be (Some ugraph) when committing an object that "^
"has no associated universe graph. If this is in make_univ phase you "^
"should drop this exception and let univ_make commit thi object with "^
else
(* we don't trust the uri, so we fail *)
begin
- prerr_endline ("CACHE MISS: " ^ (UriManager.string_of_uri uri));
+ debug_print ("CACHE MISS: " ^ (UriManager.string_of_uri uri));
raise Not_found
end
(list_uri ())
with
Not_found ->
- prerr_endline "Who has removed the uri in the meanwhile?";
+ debug_print "Who has removed the uri in the meanwhile?";
raise Not_found
;;
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
try
reduce context (0, [], [], t, [])
with Not_found ->
- prerr_endline (CicPp.ppterm t) ;
+ debug_print (CicPp.ppterm t) ;
raise Not_found
;;
*)
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
exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
+let debug_print = fun _ -> ()
+
let lift_from k n =
let rec liftaux k =
let module C = Cic in
(*CSC: per la roba che proviene da Coq questo non serve! *)
let subst_vars exp_named_subst =
(*
-prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
+debug_print ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
*)
let rec substaux k =
let module C = Cic in
)
in
(*
-prerr_endline "\n\n---- BEGIN " ;
-prerr_endline ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-prerr_endline ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst)) ;
-prerr_endline ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst')) ;
+debug_print "\n\n---- BEGIN " ;
+debug_print ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
+debug_print ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst)) ;
+debug_print ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst')) ;
*)
let exp_named_subst'' =
substaux_in_exp_named_subst uri k exp_named_subst' params
in
(*
-prerr_endline ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'')) ;
-prerr_endline "---- END\n\n " ;
+debug_print ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'')) ;
+debug_print "---- END\n\n " ;
*)
C.Var (uri,exp_named_subst'')
)
| _::tl -> filter_and_lift 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
raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
;;
-let debug_print = prerr_endline ;;
+let debug_print = fun _ -> () ;;
let rec split l n =
match (l,n) with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
with Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph_dust
in
match cobj,ugraph with
| CicEnvironment.CheckedObj _
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
with Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
ty,ugraph2)
| _ ->
raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
)
with
Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph1_dust
in
match cobj with
raise CicEnvironmentError)
with
Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph1_dust
in
match cobj with
(* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
match CicEnvironment.is_type_checked ~trust:false ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') ->
- (* prerr_endline ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
+ (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
cobj,ugraph'
| CicEnvironment.UncheckedObj uobj ->
(* let's typecheck the uncooked object *)
logger#log (`Start_type_checking uri) ;
- (* prerr_endline ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
+ (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
let ugraph1 =
(match uobj with
C.Constant (_,Some te,ty,_,_) ->
object.
*)
Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph1
;;
let tactical_terminator = "."
let tactic_terminator = tactical_terminator
+let command_terminator = tactical_terminator
let tactical_separator = ";"
let pp_term_ast term = CicAstPp.pp_term term
sprintf "alias num (instance %d) = \"%s\"" instance desc
let pp_command = function
- | Qed _ -> "Qed"
+ | Qed _ -> "qed"
| Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value
| Inductive (_, params, types) ->
let pp_params = function
let pp_tactical tac = pp_tactical tac ^ tactical_terminator
let pp_tactic tac = pp_tactic tac ^ tactic_terminator
+let pp_command tac = pp_command tac ^ command_terminator
let pp_executable = function
| Macro (_,x) -> pp_macro_ast x
metasenv_length := 0;
context_length := 0
let print_counters () =
- prerr_endline (Printf.sprintf
+ debug_print (Printf.sprintf
"apply_subst: %d
apply_subst_context: %d
apply_subst_metasenv: %d
exception Uncertain of string
exception AssertFailure of string
-let debug_print = prerr_endline
+let debug_print = fun _ -> ()
type substitution = (int * (Cic.context * Cic.term)) list
(ppterm subst term)
in
(* DEBUG
- prerr_endline error_msg;
- prerr_endline ("metasenv = \n" ^ (ppmetasenv metasenv subst));
- prerr_endline ("subst = \n" ^ (ppsubst subst));
- prerr_endline ("context = \n" ^ (ppcontext subst context)); *)
+ debug_print error_msg;
+ debug_print ("metasenv = \n" ^ (ppmetasenv metasenv subst));
+ debug_print ("subst = \n" ^ (ppsubst subst));
+ debug_print ("context = \n" ^ (ppcontext subst context)); *)
raise (MetaSubstFailure error_msg)))
subst ([], [])
in
otherwise the occur check does not make sense *)
(*
- prerr_endline ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
+ debug_print ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l))));
*)
(* order (in the sense of alpha-conversion). See comment above *)
(* related to the delift function. *)
(* debug_print "First Order UnificationFailure during delift" ;
-prerr_endline(sprintf
+debug_print(sprintf
"Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
(ppterm subst t)
(String.concat "; "
exception Uncertain of string;;
exception AssertFailure of string;;
-let debug_print = prerr_endline
+let debug_print = fun _ -> ()
let fo_unif_subst subst context metasenv t1 t2 ugraph =
try
(tgt = (CicUtil.term_of_uri "cic:/Coq/Reals/Rdefinitions/R.con"))
then
begin
- prerr_endline "TROVATA coercion";
+ debug_print "TROVATA coercion";
Some (CicUtil.term_of_uri "cic:/Coq/Reals/Raxioms/INR.con")
end
else
begin
- prerr_endline (sprintf "NON TROVATA la coercion %s %s" (CicPp.ppterm src)
+ debug_print (sprintf "NON TROVATA la coercion %s %s" (CicPp.ppterm src)
(CicPp.ppterm tgt));
None
end
try
fo_unif_subst subst context metasenv hetype hetype' ugraph
with exn ->
- prerr_endline (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
+ debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
(CicPp.ppterm hetype)
(CicPp.ppterm hetype')
(CicMetaSubst.ppmetasenv metasenv [])
exception Uncertain of string;;
exception AssertFailure of string;;
-let debug_print = prerr_endline
+let debug_print = fun _ -> ()
let type_of_aux' metasenv subst context term ugraph =
try
with
Uncertain _
| UnificationFailure _ ->
-prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j));
+debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j));
let metasenv, subst =
CicMetaSubst.restrict
subst [(n,j)] metasenv in
with
UnificationFailure msg
| Uncertain msg ->
- prerr_endline msg;raise (UnificationFailure msg)
+ (* debug_print msg; *)raise (UnificationFailure msg)
| AssertFailure _ ->
- prerr_endline "siamo allo huge hack";
+ debug_print "siamo allo huge hack";
(* TODO huge hack!!!!
* we keep on unifying/refining in the hope that
* the problem will be eventually solved.
C.Prod _ ->
fo_unif_subst test_equality_only
subst context metasenv t1' t2 ugraph
- | _ -> (* raise (UnificationFailure "9")) *)
- raise
+ | _ -> raise (UnificationFailure "9"))
+ (* raise
(UnificationFailure (sprintf
"Can't unify %s with %s because they are not convertible"
(CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+ (CicMetaSubst.ppterm subst t2))))*)
| (_,_) ->
let b,ugraph1 =
R.are_convertible ~subst ~metasenv context t1 t2 ugraph
open Printf;;
+let debug_print = fun _ -> ()
+
type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list
(* the list of known coercions (MUST be transitively closed) *)
UriManager.eq t tgt)
!coercions
in
- prerr_endline (sprintf ":) TROVATA la coercion %s %s"
+ debug_print (sprintf ":) TROVATA la coercion %s %s"
(UriManager.name_of_uri src)
(UriManager.name_of_uri tgt));
Some (CicUtil.term_of_uri (UriManager.string_of_uri u))
with
Not_found ->
- prerr_endline (sprintf ":( NON TROVATA la coercion %s %s"
+ debug_print (sprintf ":( NON TROVATA la coercion %s %s"
(UriManager.name_of_uri src) (UriManager.name_of_uri tgt));
None
;;
try
CicTypeChecker.type_of_aux' [] [] c univ
with CicTypeChecker.TypeCheckerFailure s as exn ->
- prerr_endline (sprintf "Generated composite coercion:\n%s\n%s"
+ debug_print (sprintf "Generated composite coercion:\n%s\n%s"
(CicPp.ppterm c) s);
raise exn
in
!coercions
-(* stupid case *)
-(*
-let l = close_coercion_graph
- (UriManager.uri_of_string
- "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)")
- (UriManager.uri_of_string
- "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind#xpointer(1/1)")
- (UriManager.uri_of_string
- "cic:/CoRN/algebra/CRings/cr_crr.con")
-in
- List.iter (fun (u,o,g) ->
- prerr_endline (CicPp.ppobj o);
- prerr_endline (UriManager.string_of_uri u);
- prerr_endline "")
- l
-*)
-
-
(* EOF *)
* http://cs.unibo.it/helm/.
*)
+let debug_print = fun _ -> ()
+
(* mk_fresh_name context name typ *)
(* returns an identifier which is fresh in the context *)
(* and that resembles [name] as much as possible. *)
C.Anonymous ->
if List.mem k rels2 then
(
- prerr_endline "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name" ;
+ debug_print "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name" ;
C.Anonymous
)
else
Helm_registry.get_opt_default Helm_registry.get_bool false "getter.prefetch"
in
if is_prefetch_set then
- ignore (Thread.create sync_with_map ())
+ (* ignore (Thread.create sync_with_map ()) *)
+ sync_with_map ()
* http://cs.unibo.it/helm/.
*)
+let debug_print = fun _ -> ()
+
(* Da rimuovere, solo per debug*)
let print_context ctx =
let print_name =
Some (ey, ty) ->
(* the goal is still there *)
(*
- prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
- prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
- prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
+ debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
+ debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p));
+ debug_print ("CURRENT HYP = " ^ (fst (print_context ey)));
*)
(* if the goal contains metavariables we use the input
signature for at_most constraints *)
let auto_tac ?num ~(dbd:Mysql.dbd) =
let auto_tac dbh (proof,goal) =
- prerr_endline "Entro in Auto";
+ debug_print "Entro in Auto";
match (auto dbd [(proof, [(goal,depth)],None)]) with
- [] -> prerr_endline("Auto failed");
+ [] -> debug_print("Auto failed");
raise (ProofEngineTypes.Fail "No Applicable theorem")
| (proof,[],_)::_ ->
- prerr_endline "AUTO_TAC HA FINITO";
+ debug_print "AUTO_TAC HA FINITO";
(proof,[])
| _ -> assert false
in
match exitus with
Yes (bo,_) ->
(*
- prerr_endline "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
- prerr_endline (CicPp.ppterm ty);
+ debug_print "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
+ debug_print (CicPp.ppterm ty);
*)
let subst_in =
(* if we just apply the subtitution, the type
proof goal subst_in metasenv in
[(subst_in,(proof,[],sign))]
| No d when (d >= depth) ->
- (* prerr_endline "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *)
+ (* debug_print "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *)
[] (* the empty list means no choices, i.e. failure *)
| No _
| NotYetInspected ->
(*
- prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
- prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
- prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
+ debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
+ debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p));
+ debug_print ("CURRENT HYP = " ^ (fst (print_context ey)));
*)
let sign, new_sign =
if is_meta_closed then
in
if not (cty = ty) then
begin
- prerr_endline ("ty = "^CicPp.ppterm ty);
- prerr_endline ("cty = "^CicPp.ppterm cty);
+ debug_print ("ty = "^CicPp.ppterm ty);
+ debug_print ("cty = "^CicPp.ppterm cty);
assert false
end
Hashtbl.add inspected_goals
let maxdepthgoals = reorder_goals dbd sign proof maxdepthgoals in
let len2 = List.length maxdepthgoals in
match maxdepthgoals with
- [] -> prerr_endline
+ [] -> debug_print
("caso sospetto " ^ (string_of_int (List.length othergoals)) ^ " " ^ string_of_int depth);
auto_new dbd
width already_seen_goals((subst,(proof, othergoals, sign))::tl)
auto_new dbd width already_seen_goals all_choices
| _ -> assert false
end
- | None -> prerr_endline "caso none";
+ | None -> debug_print "caso none";
auto_new
dbd width already_seen_goals ((subst,(proof, gtl, sign))::tl)
end
let auto_tac_new ~(dbd:Mysql.dbd) =
let auto_tac dbd (proof,goal) =
Hashtbl.clear inspected_goals;
- prerr_endline "Entro in Auto";
+ debug_print "Entro in Auto";
let id t = t in
match (auto_new dbd width [] [id,(proof, [(goal,depth)],None)]) with
- [] -> prerr_endline("Auto failed");
+ [] -> debug_print("Auto failed");
raise (ProofEngineTypes.Fail "No Applicable theorem")
| (_,(proof,[],_))::_ ->
- prerr_endline "AUTO_TAC HA FINITO";
+ debug_print "AUTO_TAC HA FINITO";
let _,_,p,_ = proof in
- prerr_endline (CicPp.ppterm p);
+ debug_print (CicPp.ppterm p);
(proof,[])
| _ -> assert false
in
open HelmLibraryObjects
+let debug_print = fun _ -> ()
+
let rec injection_tac ~term =
let injection_tac ~term status =
let (proof, goal) = status in
let (t1',t2',consno2') = (* bruuutto: uso un eccezione per terminare con successo! buuu!! :-/ *)
try
let rec traverse t1 t2 =
-prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ;
-prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ;
+debug_print ("XXXX t1 " ^ CicPp.ppterm t1) ;
+debug_print ("XXXX t2 " ^ CicPp.ppterm t2) ;
match t1,t2 with
((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
(C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
in traverse t1 t2
with (TwoDifferentSubtermsFound (t1,t2,consno2)) -> (t1,t2,consno2)
in
-prerr_endline ("XXXX consno2' " ^ (string_of_int consno2')) ;
+debug_print ("XXXX consno2' " ^ (string_of_int consno2')) ;
if consno2' = 0
then raise (ProofEngineTypes.Fail "Discriminate: Discriminating terms are structurally equal")
else
match fst(CicEnvironment.get_obj turi
CicUniv.empty_ugraph) with
C.InductiveDefinition (ind_type_list,_,nr_ind_params) ->
-prerr_endline ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno)) ;
+debug_print ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno)) ;
let _,_,_,constructor_list = (List.nth ind_type_list typeno) in
-prerr_endline ("XXXX nth " ^ (string_of_int (List.length constructor_list)) ^ " " ^ (string_of_int consno2')) ;
+debug_print ("XXXX nth " ^ (string_of_int (List.length constructor_list)) ^ " " ^ (string_of_int consno2')) ;
let false_constr_id,_ = List.nth constructor_list (consno2' - 1) in
-prerr_endline ("XXXX nth funzionano ") ;
+debug_print ("XXXX nth funzionano ") ;
List.map
(function (id,cty) ->
let red_ty = CicReduction.whd context cty in (* dubbio: e' corretto ridurre in questo context ??? *)
)
~continuation:
(
-prerr_endline ("XXXX rewrite<-: " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2'])));
-prerr_endline ("XXXX rewrite<-: " ^ CicPp.ppterm (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2'])) ;
-prerr_endline ("XXXX equri: " ^ U.string_of_uri equri) ;
-prerr_endline ("XXXX tty : " ^ CicPp.ppterm tty) ;
-prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1')) ;
-prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ;
-if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> tty then prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1')) ;
-if (CicTypeChecker.type_of_aux' metasenv' context' t2') <> tty then prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ;
+debug_print ("XXXX rewrite<-: " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2'])));
+debug_print ("XXXX rewrite<-: " ^ CicPp.ppterm (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2'])) ;
+debug_print ("XXXX equri: " ^ U.string_of_uri equri) ;
+debug_print ("XXXX tty : " ^ CicPp.ppterm tty) ;
+debug_print ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1')) ;
+debug_print ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ;
+if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> tty then debug_print ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1')) ;
+if (CicTypeChecker.type_of_aux' metasenv' context' t2') <> tty then debug_print ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ;
if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> (CicTypeChecker.type_of_aux' metasenv' context' t2')
- then prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1')) ; prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ;
+ then debug_print ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux'
+ metasenv' context' t1')) ; debug_print ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ;
let termty' = ProofEngineReduction.replace_lifting ~equality:(==) ~what:t1 ~with_what:t1' ~where:termty in
let termty'' = ProofEngineReduction.replace_lifting ~equality:(==) ~what:t2 ~with_what:t2' ~where:termty' in
-prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' term));
+debug_print ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' term));
T.then_
~start:(EqualityTactics.rewrite_back_simpl_tac ~term:term)
~continuation:(IntroductionTactics.constructor_tac ~n:1)
(** perform debugging output? *)
let debug = false
+let debug_print = fun _ -> ()
(** debugging print *)
let warn s =
if debug then
- prerr_endline ("DECOMPOSE: " ^ s)
+ debug_print ("DECOMPOSE: " ^ s)
(T.then_
~start:(
if (term'==term) (* if it's the first application of elim, there's no need to clear the hyp *)
- then begin prerr_endline ("%%%%%%% no clear"); T.id_tac end
- else begin prerr_endline ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end)
+ then begin debug_print ("%%%%%%% no clear"); T.id_tac end
+ else begin debug_print ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end)
~continuation:(ProofEngineTypes.mk_tactic (elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim)))
status
)))
module Constr = MetadataConstraints
module PET = ProofEngineTypes
+let debug_print = fun _ -> ()
+
(** maps a shell like pattern (which uses '*' and '?') to a sql pattern for
* the "like" operator (which uses '%' and '_'). Does not support escaping. *)
let sqlpat_of_shellglob =
(fun cols -> match cols.(0) with Some s -> s | _ -> assert false))
let match_term ~(dbd:Mysql.dbd) ty =
-(* prerr_endline (CicPp.ppterm ty); *)
+(* debug_print (CicPp.ppterm ty); *)
let metadata = MetadataExtractor.compute ~body:None ~ty in
let constants_no =
MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
let hyp_constants =
Constr.StringSet.diff (signature_of_hypothesis context) types_constants
in
-(* Constr.StringSet.iter prerr_endline hyp_constants; *)
+(* Constr.StringSet.iter debug_print hyp_constants; *)
let other_constants = Constr.StringSet.union sig_constants hyp_constants in
let uris =
let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
if ((List.length uris < pow) or (pow <= 0))
then begin
-(* prerr_endline "MetadataQuery: large sig, falling back to old method"; *)
+(* debug_print "MetadataQuery: large sig, falling back to old method"; *)
filter_uris_forward ~dbd (main, other_constants) uris
end else
filter_uris_backward ~dbd ~facts (main, other_constants) uris
(let status' =
try
let (proof, goal_list) =
-(* prerr_endline ("STO APPLICANDO " ^ uri); *)
+(* debug_print ("STO APPLICANDO " ^ uri); *)
PET.apply_tactic
(PrimitiveTactics.apply_tac
~term:(CicUtil.term_of_uri uri))
in
Constr.StringSet.union main hyp_and_sug
in
-(* Constr.StringSet.iter prerr_endline hyp_constants; *)
+(* Constr.StringSet.iter debug_print hyp_constants; *)
let all_constants_closed = close_with_types all_constants metasenv context in
let other_constants =
Constr.StringSet.diff all_constants_closed types_constants
in
- prerr_endline "all_constants_closed";
- Constr.StringSet.iter prerr_endline all_constants_closed;
- prerr_endline "other_constants";
- Constr.StringSet.iter prerr_endline other_constants;
+ debug_print "all_constants_closed";
+ Constr.StringSet.iter debug_print all_constants_closed;
+ debug_print "other_constants";
+ Constr.StringSet.iter debug_print other_constants;
let uris =
let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
if ((List.length uris < pow) or (pow <= 0))
then begin
- prerr_endline "MetadataQuery: large sig, falling back to old method";
+ debug_print "MetadataQuery: large sig, falling back to old method";
filter_uris_forward ~dbd (main, other_constants) uris
end else
filter_uris_backward ~dbd ~facts (main, other_constants) uris
(let status' =
try
let (subst,(proof, goal_list)) =
- (* prerr_endline ("STO APPLICANDO" ^ uri); *)
+ (* debug_print ("STO APPLICANDO" ^ uri); *)
PrimitiveTactics.apply_tac_verbose
~term:(CicUtil.term_of_uri uri)
status
let metadata = MetadataExtractor.compute ~body:None ~ty:t' in
(* List.iter
(fun x ->
- prerr_endline
+ debug_print
(MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x)))
metadata; *)
let no_concl = MetadataDb.count_distinct `Conclusion metadata in
in
match (look_for_dummy_main metadata) with
| None->
-(* prerr_endline "Caso None"; *)
+(* debug_print "Caso None"; *)
(* no dummy in main position *)
let metadata = List.filter is_dummy metadata in
let constraints = List.map MetadataTypes.constr_of_metadata metadata in
let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints
| Some (depth, dummy_type) ->
-(* prerr_endline
+(* debug_print
(sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type)); *)
(* a dummy in main position *)
let metadata_for_dummy_type =
(** perform debugging output? *)
let debug = false
+let debug_print = fun _ -> ()
(** debugging print *)
let warn s =
if debug then
- prerr_endline ("RING WARNING: " ^ s)
+ debug_print ("RING WARNING: " ^ s)
(** CIC URIS *)
(** perform debugging output? *)
let debug = false
+let debug_print = fun _ -> ()
(** debugging print *)
let warn s =
if debug then
- prerr_endline ("TACTICALS WARNING: " ^ s)
+ debug_print ("TACTICALS WARNING: " ^ s)
(** TACTIC{,AL}S *)
| (Some (Cic.Name name,_))::_ when name = "T" -> n
| _::tl -> find (n+1) tl
in
- prerr_endline ("eseguo find");
+ debug_print ("eseguo find");
find 1 context
in
- prerr_endline ("eseguo apply");
+ debug_print ("eseguo apply");
apply_tac ~term:(Cic.Rel rel) status
in
(* do_tactic ~n:2 *)
projects / helm.git / commitdiff