xml parsing + dtd

Makefile.in

@@ -441,8 +441,8 @@ install_local: bin/why3config
 
 ifeq (@enable_ide@,yes)
 
-IDE_FILES = session gconfig db gmain
-# IDE_FILES = session gconfig newmain
+IDE_FILES = xml session gconfig db gmain
+# IDE_FILES = xml session gconfig newmain
 
 IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
 
@@ -478,7 +478,7 @@ bin/why3ide: bin/why3ide.@OCAMLBEST@
 
 include .depend.ide
 
-.depend.ide:
+.depend.ide: src/ide/xml.ml
 	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
 
 depend: .depend.ide

share/why3session.dtd

+<!ELEMENT file (theory*)>
+<!ATTLIST file name CDATA #REQUIRED>
+<!ATTLIST file verified CDATA #REQUIRED>
+
+<!ELEMENT theory (goal*)>
+<!ATTLIST theory name CDATA #REQUIRED>
+<!ATTLIST theory verified CDATA #REQUIRED>
+
+<!ELEMENT goal (proof*, transf*)>
+<!ATTLIST goal name CDATA #REQUIRED>
+<!ATTLIST goal expl CDATA #IMPLIED>
+<!ATTLIST goal proved CDATA #REQUIRED>
+
+<!ELEMENT proof (result)>
+<!ATTLIST proof prover CDATA #REQUIRED>
+
+<!ELEMENT result EMPTY>
+<!ATTLIST result status (valid|invalid|unknown|timeout|failure) #REQUIRED>
+<!ATTLIST result time CDATA #IMPLIED>
+
+<!ELEMENT transf (goal*)>
+<!ATTLIST transf name CDATA #REQUIRED>
+<!ATTLIST transf proved CDATA #REQUIRED>
+

src/ide/newmain.ml

@@ -165,7 +165,7 @@ let w = GWindow.window
   ~allow_grow:true ~allow_shrink:true
   ~width:gconfig.window_width
   ~height:gconfig.window_height
-  ~title:"Why3: graphical session manager" ()
+  ~title:"Why3 Interactive Proof Session" ()
 
 let (_ : GtkSignal.id) =
   w#misc#connect#size_allocate
@@ -673,8 +673,23 @@ let (_ : GMenu.image_menu_item) =
 let exit_function () =
   eprintf "saving IDE config file@.";
   save_config ();
-  eprintf "saving session@.";
-  M.test_save ();
+  eprintf "saving session (testing only)@.";
+  begin
+    M.test_save ();
+    try
+      let l = M.test_load () in
+      eprintf "reloaded successfully %d elements@." (List.length l);
+      match l with
+	| [] -> ()
+	| f :: _ ->
+	    eprintf "first element is a '%s' with %d sub-elements@." 
+	      f.Xml.name (List.length f.Xml.elements);
+	    
+    with e -> eprintf "test reloading failed with exception %s@."
+      (Printexc.to_string e)
+  end;
+  let ret = Sys.command "xmllint --noout --dtdvalid share/why3session.dtd essai.xml" in
+  if ret = 0 then eprintf "DTD validation succeeded, good!@."; 
   GMain.quit ()
 
 let (_ : GtkSignal.id) = w#connect#destroy ~callback:exit_function

src/ide/session.ml

@@ -210,11 +210,14 @@ let rec save_goal fmt g =
   fprintf fmt "@[<v 1><goal name=\"%s\" %aproved=\"%b\">@\n" 
     g.goal_name (opt "expl") g.goal_expl g.proved;
   Hashtbl.iter (save_proof_attempt fmt) g.external_proofs;
+  Hashtbl.iter (save_trans fmt) g.transformations;
   fprintf fmt "</goal>@]@\n"
 
-(*
-and save_trans fmt t =
-*)
+and save_trans fmt _ t =
+  fprintf fmt "<transf name=\"%s\" proved=\"%b\">@\n" 
+    t.transf.transformation_name t.transf_proved;
+  List.iter (save_goal fmt) t.subgoals;
+  fprintf fmt "</transf>@\n"
 
 let save_theory fmt t =
   fprintf fmt "@[<v 1><theory name=\"%s\" verified=\"%b\">@\n" "todo" t.verified;
@@ -230,13 +233,19 @@ let save fname =
   let ch = open_out fname in
   let fmt = formatter_of_out_channel ch in
   fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
+(*
   fprintf fmt "@[<v 1><project name=\"%s\">@\n" (Filename.basename fname);
+*)
   List.iter (save_file fmt) (get_all_files());
+(*
   fprintf fmt "</project>@]@.";
+*)
   close_out ch
 
 let test_save () = save "essai.xml"
 
+let test_load () = Xml.from_file "essai.xml"
+
 (****************************)
 (*     session opening      *)
 (****************************)

src/ide/session.mli

@@ -147,6 +147,8 @@ module Make(O: OBSERVER) : sig
   val maximum_running_proofs : int ref
 
   val test_save : unit -> unit
+  val test_load : unit -> Xml.element list
+
     (* 
   val save_session : unit -> unit
     (** enforces to save the session state on disk. *)

src/ide/xml.mli

+
+
+type element =
+    { name : string;
+      attributes : (string * Why.Rc.rc_value) list;
+      elements : element list;
+    }
+
+val from_file : string -> element list
+
+

src/ide/xml.mll

+
+
+{
+
+  open Lexing
+
+  open Why.Rc
+
+  type element =
+    { name : string;
+      attributes : (string * rc_value) list;
+      elements : element list;
+    }
+
+  let buf = Buffer.create 17
+
+  let rec pop_all group_stack element_stack =
+    match group_stack with
+      | [] -> element_stack
+      | (elem,att,elems)::g ->
+	  let e = {
+	    name = elem;
+	    attributes = att;
+	    elements = List.rev element_stack;
+	  }
+	  in pop_all g (e::elems)
+}
+
+let space = [' ' '\t' '\r' '\n']
+let digit = ['0'-'9']
+let letter = ['a'-'z' 'A'-'Z']
+let ident = (letter | digit | '_') + 
+let sign = '-' | '+' 
+let integer = sign? digit+
+let mantissa = ['e''E'] sign? digit+
+let real = sign? digit* '.' digit* mantissa?
+let escape = ['\\''"''n''t''r'] 
+
+rule xml_header = parse
+| "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" 
+    { elements [] [] lexbuf }
+| _ 
+    { failwith "[Xml error] wrong header" }
+      
+and elements group_stack element_stack = parse
+  | space+ 
+      { elements group_stack element_stack lexbuf }
+  | '<' (ident as elem)   
+      { attributes group_stack element_stack elem [] lexbuf }
+  | "</" (ident as celem) space* '>'
+      { match group_stack with
+         | [] -> 
+             Format.eprintf "[Xml warning] unexpected closing Xml element `%s'@." celem;
+             elements group_stack element_stack lexbuf
+         | (elem,att,stack)::g ->
+             if celem <> elem then
+               Format.eprintf "[Xml warning] Xml element `%s' closed by `%s'@." elem celem;
+	     let e = {
+	        name = elem;
+	        attributes = att;
+	        elements = List.rev element_stack;
+	     }
+             in elements g (e::stack) lexbuf            
+       }
+  | '<'
+      { Format.eprintf "[Xml warning] unexpected '<'@.";
+        elements group_stack element_stack lexbuf }      
+  | eof 
+      { match group_stack with
+         | [] -> element_stack
+         | (elem,_,_)::_ ->
+             Format.eprintf "[Xml warning] unclosed Xml element `%s'@." elem;
+             pop_all group_stack element_stack
+      }
+  | _ as c
+      { failwith ("[Xml error] invalid element starting with " ^ String.make 1 c) }
+
+and attributes groupe_stack element_stack elem acc = parse
+  | space+
+      { attributes groupe_stack element_stack elem acc lexbuf }
+  | (ident as key) space* '=' 
+      { let v = value lexbuf in
+        attributes groupe_stack element_stack elem ((key,v)::acc) lexbuf }
+  | '>' 
+      { elements ((elem,acc,element_stack)::groupe_stack) [] lexbuf }
+  | "/>"
+      { let e = { name = elem ; 
+                  attributes = acc;
+                  elements = [] }
+        in
+        elements groupe_stack (e::element_stack) lexbuf }
+  | _ as c
+      { failwith ("[Xml error] `>' expected, got " ^ String.make 1 c) }
+  | eof
+      { failwith ("[Xml error] unclosed element, `>' expected") }
+
+and value = parse
+  | space+ 
+      { value lexbuf }
+  | integer as i
+      { RCint (int_of_string i) }
+  | real as r
+      { RCfloat (float_of_string r) }
+  | '"' 
+      { Buffer.clear buf;
+	string_val lexbuf } 
+  | "true"
+      { RCbool true }
+  | "false"
+      { RCbool false }
+  | ident as id
+      { RCident id }
+  | _ as c
+      { failwith ("[Xml error] invalid value starting with " ^ String.make 1 c) }
+  | eof
+      { failwith "[Xml error] unterminated keyval pair" }
+
+and string_val = parse 
+  | '"' 
+      { RCstring (Buffer.contents buf) }
+  | [^ '\\' '"'] as c
+      { Buffer.add_char buf c;
+        string_val lexbuf }
+  | '\\' (['\\''\"'] as c)   
+      { Buffer.add_char buf c;
+        string_val lexbuf }
+  | '\\' 'n'
+      { Buffer.add_char buf '\n';
+        string_val lexbuf }
+  | '\\' (_ as c)
+      { Buffer.add_char buf '\\';
+        Buffer.add_char buf c;
+        string_val lexbuf }
+  | eof
+      { failwith "[Xml error] unterminated string" }
+
+
+{
+
+  let from_file f =
+      let c = 
+(*
+	try 
+*)
+	open_in f 
+(*
+	with Sys_error _ -> 
+	  Format.eprintf "Cannot open file %s@." f;
+	  exit 1
+*)
+      in
+      let lb = Lexing.from_channel c in
+      let l = xml_header lb in
+      close_in c;
+      List.rev l
+
+}