From: Enrico Tassi Date: Fri, 27 May 2005 16:31:47 +0000 (+0000) Subject: removed debug prerr_endline X-Git-Tag: PRE_INDEX_1~111 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=46f19eadce5f3a11c0ae26934fd8d1b597906416;p=helm.git removed debug prerr_endline --- diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index bfc535a3c..9f5fd193e 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -69,6 +69,7 @@ let alias_spec = Grammar.Entry.create grammar "alias_spec" 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) @@ -116,7 +117,7 @@ let mk_binder_ast binder typ vars body = vars body EXTEND - GLOBAL: term term0 statement; + GLOBAL: term term0 statement statements; int: [ [ num = NUM -> try @@ -586,6 +587,10 @@ EXTEND | com = comment -> TacticAst.Comment (loc, com) ] ]; + statements: [ + [ l = LIST0 [ statement ] -> l + ] + ]; END let exc_located_wrapper f = @@ -601,6 +606,9 @@ let parse_term stream = 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)) + (**/**) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli index f7510a9bd..9e3f442d8 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -29,6 +29,8 @@ exception Parse_error of Token.flocation * string 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} *) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index bd7b33440..4f8f8e78a 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -250,7 +250,7 @@ let interpretate ~context ~env ast = 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 "; " @@ -460,8 +460,8 @@ module Make (C: Callbacks) = 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)) @@ -514,7 +514,7 @@ module Make (C: Callbacks) = (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) @@ -615,7 +615,7 @@ module Make (C: Callbacks) = (* (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 diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index b85a4a519..e47b48d5d 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -28,6 +28,8 @@ open Printf exception Elim_failure of string exception Can_t_eliminate +let debug_print = fun _ -> () + let fresh_binder = let counter = ref ~-1 in function @@ -337,8 +339,8 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = 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 diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index ad61bcd04..695e0cffd 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -44,7 +44,7 @@ let cleanup_tmp = true;; let trust = ref (fun _ -> true);; let set_trust f = trust := f let trust_obj uri = !trust uri - +let debug_print = fun _ -> () (* ************************************************************************** * TYPES @@ -430,14 +430,14 @@ module Cache : 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"^ @@ -538,7 +538,7 @@ let get_object_to_add uri = (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 @@ -567,7 +567,7 @@ let find_or_add_to_unchecked uri = 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)."); @@ -577,7 +577,7 @@ let set_type_checking_info ?(replace_ugraph=None) uri = 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 "^ @@ -617,7 +617,7 @@ let get_cooked_obj ?(trust=true) base_univ uri = 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 @@ -705,6 +705,6 @@ let list_obj () = (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 ;; diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index 687a46549..35c89ae33 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -33,6 +33,8 @@ exception ReferenceToVariable;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; +let debug_print = fun _ -> () + let fdebug = ref 1;; let debug t env s = let rec debug_aux t i = @@ -41,7 +43,7 @@ let debug t env s = 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 = @@ -347,7 +349,7 @@ module Reduction(RS : 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)) @@ -493,10 +495,11 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - | _::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 @@ -754,7 +757,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; try reduce context (0, [], [], t, []) with Not_found -> - prerr_endline (CicPp.ppterm t) ; + debug_print (CicPp.ppterm t) ; raise Not_found ;; *) @@ -770,11 +773,11 @@ let whd context 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 @@ -1020,10 +1023,10 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = (* (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 diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index 30a24c13a..3ff3e4570 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -30,6 +30,8 @@ exception ReferenceToConstant;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; +let debug_print = fun _ -> () + let lift_from k n = let rec liftaux k = let module C = Cic in @@ -264,7 +266,7 @@ let subst arg = (*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 @@ -289,17 +291,17 @@ prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ; ) 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'') ) @@ -404,10 +406,11 @@ prerr_endline "---- END\n\n " ; | _::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 diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index fe46e4748..74542a226 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -42,7 +42,7 @@ let debug t context = 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 @@ -184,7 +184,7 @@ let rec type_of_constant ~logger uri ugraph = 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 @@ -225,7 +225,7 @@ and type_of_variable ~logger uri ugraph = | 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)) @@ -574,7 +574,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph = ) with Invalid_argument s -> - (*prerr_endline s;*) + (*debug_print s;*) uobj,ugraph1_dust in match cobj with @@ -609,7 +609,7 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph = raise CicEnvironmentError) with Invalid_argument s -> - (*prerr_endline s;*) + (*debug_print s;*) uobj,ugraph1_dust in match cobj with @@ -2037,12 +2037,12 @@ let typecheck uri ugraph = (* ??? 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,_,_) -> @@ -2111,7 +2111,7 @@ let typecheck uri ugraph = object. *) Invalid_argument s -> - (*prerr_endline s;*) + (*debug_print s;*) uobj,ugraph1 ;; diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index f10443c2d..eebc73c89 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -29,6 +29,7 @@ open TacticAst 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 @@ -145,7 +146,7 @@ let pp_alias = function 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 @@ -204,6 +205,7 @@ and pp_tacticals tacs = 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 diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index b8784d717..eaa094fdc 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -47,7 +47,7 @@ let reset_counters () = 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 @@ -72,7 +72,7 @@ exception MetaSubstFailure of string 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 @@ -594,10 +594,10 @@ let rec restrict subst to_be_restricted metasenv = (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 @@ -613,7 +613,7 @@ let delift n subst context metasenv l t = 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)))); *) @@ -738,7 +738,7 @@ let delift n subst context metasenv l t = (* 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 "; " diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 4a6e6cadf..fbde6a820 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -29,7 +29,7 @@ exception RefineFailure of string;; 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 @@ -53,12 +53,12 @@ let look_for_coercion src tgt = (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 @@ -787,7 +787,7 @@ and type_of_aux' metasenv context t ugraph = 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 []) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 25db7d915..3545f6c0e 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -29,7 +29,7 @@ exception UnificationFailure of string;; 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 @@ -305,7 +305,7 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph = 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 @@ -359,9 +359,9 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str 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. @@ -607,12 +607,12 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str 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 diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index 6aad3676d..00cfa90da 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -25,6 +25,8 @@ open Printf;; +let debug_print = fun _ -> () + type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list (* the list of known coercions (MUST be transitively closed) *) @@ -58,13 +60,13 @@ let look_for_coercion src tgt = 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 ;; @@ -122,7 +124,7 @@ let generate_composite_closure c1 c2 univ = 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 @@ -196,22 +198,4 @@ let get_coercions_list () = !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 *) diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml index fbb90552a..0dc5dadae 100644 --- a/helm/ocaml/cic_unification/freshNamesGenerator.ml +++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml @@ -23,6 +23,8 @@ * 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. *) @@ -111,7 +113,7 @@ let clean_dummy_dependent_types t = 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 diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml index 0251c548f..d0ecf9ba2 100644 --- a/helm/ocaml/getter/http_getter.ml +++ b/helm/ocaml/getter/http_getter.ml @@ -656,5 +656,6 @@ let init () = 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 () diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index 88f72ffa0..6afef50e0 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +let debug_print = fun _ -> () + (* Da rimuovere, solo per debug*) let print_context ctx = let print_name = @@ -106,9 +108,9 @@ let rec auto dbd = function 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 *) @@ -156,12 +158,12 @@ let rec auto dbd = function 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 @@ -335,8 +337,8 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals 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 @@ -349,14 +351,14 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals 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 @@ -409,8 +411,8 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals 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 @@ -456,7 +458,7 @@ and auto_new_aux dbd width already_seen_goals = function 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) @@ -492,7 +494,7 @@ and auto_new_aux dbd width already_seen_goals = function 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 @@ -502,15 +504,15 @@ and auto_new_aux dbd width already_seen_goals = function 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 diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index cfed56c95..96822d8e8 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -25,6 +25,8 @@ open HelmLibraryObjects +let debug_print = fun _ -> () + let rec injection_tac ~term = let injection_tac ~term status = let (proof, goal) = status in @@ -427,8 +429,8 @@ let discriminate_tac ~term status = 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))) @@ -458,7 +460,7 @@ prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ; 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 @@ -468,11 +470,11 @@ prerr_endline ("XXXX consno2' " ^ (string_of_int consno2')) ; 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 ??? *) @@ -522,21 +524,22 @@ prerr_endline ("XXXX nth funzionano ") ; ) ~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) diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index 15645951e..d018dc52c 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -27,11 +27,12 @@ (** 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) @@ -161,8 +162,8 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term = (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 ))) diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index fc5328e9f..962aad8e7 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -28,6 +28,8 @@ open Printf 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 = @@ -60,7 +62,7 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) pat = (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) @@ -188,13 +190,13 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = 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 @@ -205,7 +207,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = (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)) @@ -284,20 +286,20 @@ let experimental_hint 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 @@ -308,7 +310,7 @@ let experimental_hint (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 @@ -357,7 +359,7 @@ let instance ~dbd t = 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 @@ -379,7 +381,7 @@ let instance ~dbd t = 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 @@ -388,7 +390,7 @@ let instance ~dbd t = 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 = diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index 4691239f4..cebb4cf91 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -34,11 +34,12 @@ open HelmLibraryObjects (** 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 *) diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index 0479264d4..4e0e04914 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -31,11 +31,12 @@ open UriManager (** 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 *) @@ -255,10 +256,10 @@ let prova_tac = | (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 *)