registered formats: simplification: no more parse_only function, but boolean...

registered formats: simplification: no more parse_only function, but boolean optional argument instead

Makefile.in

@@ -214,12 +214,12 @@ $(PGMCMO) $(PGMCMX): INCLUDES = -I src/programs
 byte: bin/whyml.byte
 opt:  bin/whyml.opt
 
-bin/whyml.opt: src/why.cmxa $(PGMCMX)
+bin/whyml.opt: src/why.cmxa $(PGMCMX) src/main.cmx
 	$(if $(QUIET), @echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
 	$(STRIP) $@
 
-bin/whyml.byte: src/why.cma $(PGMCMO)
+bin/whyml.byte: src/why.cma $(PGMCMO) src/main.cmo
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
 
@@ -242,7 +242,7 @@ clean::
 # test target
 
 %: %.mlw bin/whyml.byte
-	bin/whyml.byte -L theories $*.mlw
+	bin/whyml.byte $*.mlw
 
 ###############
 # proof manager
@@ -475,7 +475,7 @@ clean::
 bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@
 	sh bench/bench \
 	    "bin/why.@OCAMLBEST@" \
-	    "bin/whyml.@OCAMLBEST@ -L theories"
+	    "bin/whyml.@OCAMLBEST@"
 
 BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
 BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
@@ -516,10 +516,10 @@ test: bin/why.byte $(TOOLS)
 	@for i in output_coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done
 
 testl: bin/whyml.byte
-	ocamlrun -bt bin/whyml.byte -L theories/ tests/test-pgm-jcf.mlw
+	ocamlrun -bt bin/whyml.byte tests/test-pgm-jcf.mlw
 
 testl-type: bin/whyml.byte
-	ocamlrun -bt bin/whyml.byte --type-only -L theories/ tests/test-pgm-jcf.mlw
+	ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
 
 ###############
 # installation

src/core/env.ml

@@ -66,22 +66,22 @@ let env_tag env = env.env_tag
 
 (** Parsers *)
 
-type parse_only   = env -> string -> in_channel -> unit
-type read_channel = env -> string -> in_channel -> theory Mnm.t
+type read_channel = 
+  ?debug:bool -> ?parse_only:bool -> ?type_only:bool ->
+  env -> string -> in_channel -> theory Mnm.t
+
 type error_report = Format.formatter -> exn -> unit
 
-let parse_only_table   = Hashtbl.create 17 (* parser name -> parse_only *)
 let read_channel_table = Hashtbl.create 17 (* parser name -> read_channel *)
 let error_report_table = Hashtbl.create 17 (* parser name -> error_report *)
 let suffixes_table     = Hashtbl.create 17 (* suffix -> parser name *)
 
-let register_parser name suffixes po rc er =
-  Hashtbl.add parse_only_table   name po;
+let register_format name suffixes rc er =
   Hashtbl.add read_channel_table name rc;
   Hashtbl.add error_report_table name er;
   List.iter (fun s -> Hashtbl.add suffixes_table ("." ^ s) name) suffixes
 
-exception UnknownParser of string (* parser name *)
+exception UnknownFormat of string (* parser name *)
 
 let parser_for_file ?name file = match name with
   | None -> 
@@ -100,17 +100,12 @@ let parser_for_file ?name file = match name with
 
 let find_parser table n =
   try Hashtbl.find table n
-  with Not_found -> raise (UnknownParser n)
-
-let parse_only ?name env file ic =
-  let n = parser_for_file ?name file in 
-  let po = find_parser parse_only_table n in
-  po env file ic
+  with Not_found -> raise (UnknownFormat n)
 
-let read_channel ?name env file ic =
+let read_channel ?name ?debug ?parse_only ?type_only env file ic =
   let n = parser_for_file ?name file in 
   let rc = find_parser read_channel_table n in
-  rc env file ic
+  rc ?debug ?parse_only ?type_only env file ic
 
 let report ?name file fmt e =
   let n = parser_for_file ?name file in 

src/core/env.mli

@@ -37,24 +37,24 @@ exception TheoryNotFound of string list * string
 
 (** Parsers *)
 
-type parse_only   = env -> string -> in_channel -> unit
-type read_channel = env -> string -> in_channel -> theory Mnm.t
+type read_channel = 
+  ?debug:bool -> ?parse_only:bool -> ?type_only:bool ->
+  env -> string -> in_channel -> theory Mnm.t
+
 type error_report = Format.formatter -> exn -> unit
 
-val register_parser :
-  string -> string list -> parse_only -> read_channel -> error_report -> unit
-  (** [register_parser name extensions f1 f2] registers a new parser
+val register_format :
+  string -> string list -> read_channel -> error_report -> unit
+  (** [register_format name extensions f1 f2] registers a new format
       under name [name], for files with extensions in list [extensions];
-      [f1] is the function to perform parsing only;
-      [f2] is the function to retrieve a list of theories from a channel *)
-
-val parse_only   : ?name:string -> parse_only
+      [f1] is the function to perform parsing;
+      [f2] is the function to report errors *)
 
 val read_channel : ?name:string -> read_channel
 
 val report : ?name:string -> string -> error_report
 
-exception UnknownParser of string (* parser name *)
+exception UnknownFormat of string (* format name *)
 
 val list_formats : unit -> (string * string list) list
 

src/main.ml

@@ -27,8 +27,10 @@ open Driver
 open Trans
 
 let usage_msg =
-  "Usage: why [options] [[file|-] \
+  sprintf
+  "Usage: %s [options] [[file|-] \
    [-a <transform> -t <theory> [-g <goal>]...]...]..."
+  (Filename.basename Sys.argv.(0))
 
 let opt_queue = Queue.create ()
 
@@ -291,7 +293,7 @@ let rec report fmt = function
       Prover.report fmt e
   | Register.Error e ->
       Register.report fmt e
-  | Env.UnknownParser p ->
+  | Env.UnknownFormat p ->
       fprintf fmt "unknown format '%s'" p
   | e -> 
       fprintf fmt "anomaly: %s" (Printexc.to_string e)
@@ -408,21 +410,21 @@ let do_input env drv = function
       in
       let report = Env.report ?name:!opt_parser fname in
       try
-	if !opt_parse_only then begin
-	  Env.parse_only ?name:!opt_parser env fname cin;
-          close_in cin
-	end else begin
-          let m = Env.read_channel ?name:!opt_parser env fname cin in
-          close_in cin;
-          if !opt_type_only then ()
-          else if Queue.is_empty tlist then
-            let glist = Queue.create () in
-            let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
-            let do_th _ (t,th) = do_theory drv fname t th trans glist in
-            Ident.Mid.iter do_th (Mnm.fold add_th m Ident.Mid.empty)
-          else
-            Queue.iter (do_local_theory drv fname m) tlist
-	end
+	let m = 
+	  Env.read_channel ?name:!opt_parser ~debug:!opt_debug 
+	    ~parse_only:!opt_parse_only ~type_only:!opt_type_only
+	    env fname cin 
+	in
+        close_in cin;
+        if !opt_type_only then 
+	  ()
+        else if Queue.is_empty tlist then
+          let glist = Queue.create () in
+          let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
+          let do_th _ (t,th) = do_theory drv fname t th trans glist in
+          Ident.Mid.iter do_th (Mnm.fold add_th m Ident.Mid.empty)
+        else
+          Queue.iter (do_local_theory drv fname m) tlist
       with 
 	| Loc.Located (loc, e) ->
 	    eprintf "%a%a" Loc.report_position loc report e; exit 1

src/parser/typing.ml

@@ -1039,9 +1039,11 @@ let read_file env file =
   let tl = load_file file in
   type_theories env tl
 
-let read_channel env file ic =
+let read_channel 
+    ?(debug=false) ?(parse_only=false) ?(type_only=false) env file ic =
+  ignore (debug, type_only);
   let tl = load_channel file ic in
-  type_theories env tl
+  if parse_only then Mnm.empty else type_theories env tl
 
 let locate_file lp sl =
   let f = List.fold_left Filename.concat "" sl ^ ".why" in
@@ -1058,12 +1060,6 @@ let retrieve lp env sl =
 
 (** register Why parser *)
 
-let parse_only _env fname cin =
-  let lb = Lexing.from_channel cin in
-  Loc.set_file fname lb;
-  ignore (Lexer.parse_logic_file lb);
-  close_in cin
-
 let error_report fmt = function
   | Lexer.Error e ->
       fprintf fmt "lexical error: %a" Lexer.report e;
@@ -1076,7 +1072,7 @@ let error_report fmt = function
   | e -> 
       raise e
 
-let () = Env.register_parser "why" ["why"] parse_only read_channel error_report
+let () = Env.register_format "why" ["why"] read_channel error_report
 
 (*
 Local Variables:

src/programs/pgm_main.ml

@@ -22,6 +22,7 @@
 open Format
 open Why
 
+(****
 let files = ref []
 let parse_only = ref false
 let type_only = ref false
@@ -41,6 +42,7 @@ let () =
     ]
     (fun f -> files := f :: !files)
     "usage: whyl [options] files..."
+***)
 
 let rec report fmt = function
   | Lexer.Error e ->
@@ -59,41 +61,37 @@ let rec report fmt = function
       Denv.report fmt e
   | e ->
       raise e
-(*       fprintf fmt "anomaly: %s" (Printexc.to_string e) *)
 
 open Pgm_ptree
-open Theory
 
-let env = Env.create_env (Typing.retrieve !loadpath)
+let parse_only _env file c =
+  let lb = Lexing.from_channel c in
+  Loc.set_file file lb;
+  ignore (Pgm_lexer.parse_file lb)
 
-let type_file file =
-  let c = open_in file in
+let read_channel 
+    ?(debug=false) ?(parse_only=false) ?(type_only=false) env file c =
+  ignore (debug);
   let lb = Lexing.from_channel c in
   Loc.set_file file lb;
   let p = Pgm_lexer.parse_file lb in 
-  close_in c;
-  if !parse_only then raise Exit;
-  let uc = Theory.create_theory (Ident.id_fresh "Pgm") in
-  let th = Env.find_theory env ["programs"] "Prelude" in
-  let uc = Theory.use_export uc th in
-  let uc, dl = Pgm_typing.file env uc p in
-  if !type_only then raise Exit;
-  let th = Pgm_wp.file uc dl in
-  printf "%a@." Pretty.print_theory th;
-  ()
-
-let handle_file file =
-  try
-    type_file file
-  with Exit -> 
-    ()
+  if parse_only then 
+    Theory.Mnm.empty
+  else begin
+    let uc = Theory.create_theory (Ident.id_fresh "Pgm") in
+    let th = Env.find_theory env ["programs"] "Prelude" in
+    let uc = Theory.use_export uc th in
+    let uc, dl = Pgm_typing.file env uc p in
+    if type_only then 
+      Theory.Mnm.empty
+    else begin
+      let th = Pgm_wp.file uc dl in
+      Theory.Mnm.add "Pgm" th Theory.Mnm.empty
+    end
+  end
 
 let () =
-  try
-    List.iter handle_file !files
-  with e when not !debug ->
-    eprintf "%a@." report e;
-    exit 1
+  Env.register_format "whyml" ["mlw"] read_channel report
 
 (*
 Local Variables: 

src/programs/pgm_typing.ml

@@ -823,8 +823,7 @@ let file env uc dl =
 	 | Pgm_ptree.Dlet (id, e) -> 
 	     let e = type_expr uc e in
 	     (*DEBUG*)
-	     eprintf "@[--typing %s-----@\n  %a@]@." 
-	       id.id print_expr e;
+	     (* eprintf "@[--typing %s-----@\n  %a@]@." id.id print_expr e; *)
 	     let tyl, ty = uncurrying uc e.expr_type in
 	     let ls = create_lsymbol (id_user id.id id.id_loc) tyl (Some ty) in
 	     add_global ls;

src/programs/pgm_wp.ml

@@ -336,10 +336,10 @@ let decl env = function
   | Pgm_ttree.Dlet (ls, e) ->
       let e = expr env e in
       (* DEBUG *)
-      eprintf "@[--effect %a-----@\n  %a@]@\n----------------@." 
-	Pretty.print_ls ls print_type_v e.expr_type_v;
+      (* eprintf "@[--effect %a-----@\n  %a@]@\n----------------@."  *)
+	(* Pretty.print_ls ls print_type_v e.expr_type_v; *)
       let f = wp env e in
-      eprintf "wp = %a@\n----------------@." Pretty.print_fmla f;
+      (* eprintf "wp = %a@\n----------------@." Pretty.print_fmla f; *)
       let env = add_wp_decl ls f env in
       let env = add_global ls e.expr_type_v env in
       env

tests/test-pgm-jcf.mlw

@@ -19,6 +19,11 @@ let ff () =
   1+2
   { result = 3 }
 
+let gg () =
+  { true } 
+  3-1
+  { result = 2 }
+
 
 (*
 Local Variables: