]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/lib/log.ml
- new semantic log system
[helm.git] / helm / software / lambda-delta / lib / log.ml
index 667fef534253c4a0894eb5f74af7a2a08e8e1d9e..78e57fdfaf9433a115cf262fd5baa2172e803f73 100644 (file)
       V_______________________________________________________________ *)
 
 module P = Printf
+module F = Format
+module C = Cps
+
+type ('a, 'b) item = Term of 'a * 'b
+                   | Context of 'a
+                   | Warn of string
+                  | String of string
+
+type ('a, 'b) specs = {
+   pp_term   : F.formatter -> 'a -> 'b -> unit;
+   pp_context: F.formatter -> 'a -> unit
+}
+
+let level = ref 0
+
+(* Internal functions *******************************************************)
 
 let init =
    let started = ref false in
@@ -17,5 +33,28 @@ let init =
       if !started then () else 
       begin P.printf "\n"; started := true end
 
+let pp_items frm st l items =   
+   let pp_item = function
+      | Term (c, t) -> st.pp_context frm c; st.pp_term frm c t
+      | Context c   -> st.pp_context frm c
+      | Warn s      -> F.fprintf frm "@[%s\n@]" s
+      | String s    -> F.fprintf frm "@[%s @]" s
+   in
+   if !level >= l then List.iter pp_item items
+
+(* Interface functions ******************************************************)
+
 let warn msg = 
    init (); P.printf " %s\n" msg; flush stdout
+
+let log st l items = pp_items F.std_formatter st l items
+
+let error st items = pp_items F.err_formatter st 0 items
+
+let items1 s = [Warn s]
+
+let ct_items1 s c t =
+   [Warn s; Term (c, t)]
+
+let ct_items2 s1 c1 t1 s2 c2 t2 =
+   [Warn s1; Term (c1, t1); Warn s2; Term (c2, t2)]