From 5858c6b8895010b580b6d7be26a962e7ed74cce4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Oct 2009 13:37:01 +0000 Subject: [PATCH] unification pps can be activated by the menu debug --- .../components/ng_refiner/nCicRefiner.ml | 9 +- .../components/ng_refiner/nCicRefiner.mli | 1 + .../components/ng_refiner/nCicUnification.ml | 14 +-- .../components/ng_refiner/nCicUnification.mli | 2 + helm/software/matita/matita.ml | 109 +----------------- 5 files changed, 19 insertions(+), 116 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index b84c23aae..757fceea2 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -22,13 +22,14 @@ let indent = ref "";; let inside c = indent := !indent ^ String.make 1 c;; let outside () = indent := String.sub !indent 0 (String.length !indent -1);; - +let debug = ref false;; let pp s = - prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) + if !debug then + prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) + else + () ;; -let pp _ = ();; - let wrap_exc msg = function | NCicUnification.Uncertain _ -> Uncertain msg | NCicUnification.UnificationFailure _ -> RefineFailure msg diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli index b75ee3a81..1a04d2abd 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.mli +++ b/helm/software/components/ng_refiner/nCicRefiner.mli @@ -28,3 +28,4 @@ val typeof_obj : ?localise:(NCic.term -> Stdpp.location) -> NCic.obj -> NCic.obj +val debug : bool ref diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index b91585fbe..5353363d5 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -78,20 +78,20 @@ let eta_reduce subst t = module C = NCic;; module Ref = NReference;; -let debug = false;; +let debug = ref false;; let indent = ref "";; -let pp = - if debug then - fun s -> prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) +let pp s = + if !debug then + prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) else - fun _ -> () + () ;; let inside c = indent := !indent ^ String.make 1 c; - if debug then prerr_endline ("{{{" ^ !indent ^ " ") + if !debug then prerr_endline ("{{{" ^ !indent ^ " ") ;; let outside ok = - if debug then prerr_endline "}}}"; + if !debug then prerr_endline "}}}"; if not ok then pp (lazy "exception raised!"); try indent := String.sub !indent 0 (String.length !indent -1) diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli index 86f5fae1a..83a59b64c 100644 --- a/helm/software/components/ng_refiner/nCicUnification.mli +++ b/helm/software/components/ng_refiner/nCicUnification.mli @@ -35,3 +35,5 @@ val delift_type_wrt_terms: NCic.term -> NCic.term list -> NCic.metasenv * NCic.substitution * NCic.term + +val debug : bool ref diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 1bfdf8ce3..5abd0139c 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -154,43 +154,6 @@ let _ = (fun x l -> (LexiconAstPp.pp_command x)::l) (filter status.LexiconEngine.lexicon_content_rev) []))); *) - addDebugItem "dump environment to \"env.dump\"" (fun _ -> - let oc = open_out "env.dump" in - CicEnvironment.dump_to_channel oc; - close_out oc); - addDebugItem "load environment from \"env.dump\"" (fun _ -> - let ic = open_in "env.dump" in - CicEnvironment.restore_from_channel ic; - close_in ic); - addDebugItem "dump universes" (fun _ -> - List.iter (fun (u,_,g) -> - prerr_endline (UriManager.string_of_uri u); - CicUniv.print_ugraph g) (CicEnvironment.list_obj ()) - ); - addDebugItem "dump environment content" (fun _ -> - List.iter (fun (u,_,_) -> - prerr_endline (UriManager.string_of_uri u)) - (CicEnvironment.list_obj ())); - addDebugItem "dump script status" script#dump; - addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ -> - Helm_registry.save_to "./foo.conf.xml"); - addDebugItem "dump metasenv" - (fun _ -> - if script#onGoingProof () then - HLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv)); - addDebugItem "print top-level grammar entries" - CicNotationParser.print_l2_pattern; - addDebugItem "dump moo to stderr" (fun _ -> - let grafite_status = (MatitaScript.current ())#grafite_status in - let moo = grafite_status#moo_content_rev in - List.iter - (fun cmd -> - prerr_endline - (GrafiteAstPp.pp_command - ~term_pp:(fun t -> CicPp.ppterm t) - ~obj_pp:(fun _ -> assert false) - cmd)) - (List.rev moo)); addDebugItem "print metasenv goals and stack to stderr" (fun _ -> prerr_endline ("metasenv goals: " ^ String.concat " " @@ -227,48 +190,11 @@ let _ = | Proof (_,m,_subst,p,ty, attrs) -> Cic.CurrentProof ("current proof",m,Lazy.force p,ty,[],attrs) | Intermediate _ -> assert false))); -(* addDebugItem "ask record choice" - (fun _ -> - HLog.debug (string_of_int - (MatitaGtkMisc.ask_record_choice ~gui ~title:"title" ~message:"msg" - ~fields:["a"; "b"; "c"] - ~records:[ - ["0"; "0"; "0"]; ["0"; "0"; "1"]; ["0"; "1"; "0"]; ["0"; "1"; "1"]; - ["1"; "0"; "0"]; ["1"; "0"; "1"]; ["1"; "1"; "0"]; ["1"; "1"; "1"]] - ()))); *) -(* addDebugItem "rotate light bulbs" - (fun _ -> - let nb = gui#main#hintNotebook in - nb#goto_page ((nb#current_page + 1) mod 3)); *) addDebugSeparator (); -(* - addDebugItem "meets between L and R" - (fun _ -> - let l = CoercDb.coerc_carr_of_term (CicUtil.term_of_uri - (UriManager.uri_of_string "cic:/matita/test/L.ind#xpointer(1/1)" )) - in - let r = CoercDb.coerc_carr_of_term (CicUtil.term_of_uri - (UriManager.uri_of_string "cic:/matita/test/R.ind#xpointer(1/1)" )) - in - let meets = CoercGraph.meets l r in - prerr_endline "MEETS:"; - List.iter (fun carr -> prerr_endline (CicPp.ppterm (CoercDb.term_of_carr - carr))) meets - ); - addDebugSeparator (); -*) addDebugItem "disable high level pretty printer" (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := true); addDebugItem "enable high level pretty printer" (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := false); -(* ZACK moved to the View menu - addDebugItem "disable all (pretty printing) notations" - (fun _ -> CicNotation.set_active_notations []); - addDebugItem "enable all (pretty printing) notations" - (fun _ -> - CicNotation.set_active_notations - (List.map fst (CicNotation.get_all_notations ()))); -*) addDebugSeparator (); addDebugItem "enable multiple disambiguation passes (default)" (fun _ -> MultiPassDisambiguator.only_one_pass := false); @@ -279,37 +205,10 @@ let _ = addDebugItem "prune disambiguation errors" (fun _ -> MatitaGui.all_disambiguation_passes := false); addDebugSeparator (); -(* ZACK moved to the View menu - addDebugItem "enable coercions hiding" - (fun _ -> Acic2content.hide_coercions := true); - addDebugItem "disable coercions hiding" - (fun _ -> Acic2content.hide_coercions := false); -*) - addDebugItem "show coercions graph" (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `Coercions)); - addDebugItem "show coercions graph (full)" (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `CoercionsFull)); - addDebugItem "dump coercions Db" (fun _ -> - List.iter - (fun (s,t,ul) -> - HLog.debug - ((String.concat "," - (List.map - (fun u,saturations,_ -> - UriManager.name_of_uri u ^ - "(" ^ string_of_int saturations ^ ")") - ul)) ^ ":" - ^ CoercDb.string_of_carr s ^ " -> " ^ CoercDb.string_of_carr t)) - (CoercDb.to_list (CoercDb.dump ()))); - addDebugSeparator (); - let mview () = (MatitaMathView.sequentsViewer_instance ())#cicMathView in -(* addDebugItem "save (sequent) MathML to matita.xml" - (fun _ -> ignore ((Gdome.domImplementation ())#saveDocumentToFile - ~doc:(HExtlib.unopt (mview ())#get_document) ~name:"matita.xml" ())); *) - addDebugItem "load (sequent) MathML from matita.xml" - (fun _ -> (mview ())#load_uri ~filename:"matita.xml"); + addDebugItem "enable refiner/unification logging" + (fun _ -> NCicRefiner.debug := true; NCicUnification.debug := true;); + addDebugItem "disable refiner/unification logging" + (fun _ -> NCicRefiner.debug := false; NCicUnification.debug := false;); addDebugSeparator (); addDebugItem "Expand virtuals" (fun _ -> (MatitaScript.current ())#expandAllVirtuals); -- 2.39.2