programs: Pgm_types renamed into Pgm_env; the main control flow is now in Pgm_main.type_and_wp

Makefile.in

@@ -208,7 +208,7 @@ PGMGENERATED = src/programs/pgm_parser.mli    src/programs/pgm_parser.ml \
 	       src/programs/pgm_parser.output src/programs/pgm_lexer.ml
 
 PGM_FILES = pgm_ttree pgm_ptree  pgm_parser pgm_lexer pgm_effect \
-	    pgm_types pgm_typing pgm_wp pgm_main
+	    pgm_env   pgm_typing pgm_wp pgm_main
 
 PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
 

src/programs/pgm_main.ml

@@ -21,28 +21,7 @@
 
 open Format
 open Why
-
-(****
-let files = ref []
-let parse_only = ref false
-let type_only = ref false
-let debug = ref false
-let loadpath = ref []
-let prover = ref None
-
-let () = 
-  Arg.parse 
-    ["--parse-only", Arg.Set parse_only, "stops after parsing";
-     "--type-only", Arg.Set type_only, "stops after type-checking";
-     "--debug", Arg.Set debug, "sets the debug flag";
-     "-L", Arg.String (fun s -> loadpath := s :: !loadpath), 
-       "<dir>  adds dir to the loadpath";
-     "-P", Arg.String (fun s -> prover := Some s),
-       "<prover> proves the verification conditions";
-    ]
-    (fun f -> files := f :: !files)
-    "usage: whyl [options] files..."
-***)
+open Pgm_env
 
 let rec report fmt = function
   | Lexer.Error e ->
@@ -66,31 +45,38 @@ let rec report fmt = function
   | e ->
       raise e
 
-open Pgm_ptree
-
 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_and_wp ?(type_only=false) env gl dl =
+  let decl gl d = if type_only then gl else Pgm_wp.decl gl d in
+  let add gl d = 
+    let gl, dl = Pgm_typing.decl env gl d in
+    List.fold_left decl gl dl
+  in
+  List.fold_left add gl dl
+
 let read_channel 
     ?(debug=false) ?(parse_only=false) ?(type_only=false) env file c =
   Pgm_typing.debug := debug;
   Pgm_wp.debug := debug;
   let lb = Lexing.from_channel c in
   Loc.set_file file lb;
-  let p = Pgm_lexer.parse_file lb in 
+  let dl = Pgm_lexer.parse_file lb in 
   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
+    let gl = empty_env uc in
+    let gl = type_and_wp ~type_only env gl dl in
     if type_only then 
       Theory.Mnm.empty
     else begin
-      let th = Pgm_wp.file uc dl in
+      let th = Theory.close_theory gl.uc in
       Theory.Mnm.add "Pgm" th Theory.Mnm.empty
     end
   end

src/programs/pgm_ttree.ml

@@ -105,15 +105,15 @@ type variant = Term.term * Term.lsymbol
 
 type reference = Pgm_effect.reference
 
-type pre = Pgm_types.pre
+type pre = Pgm_env.pre
 
-type post = Pgm_types.post
+type post = Pgm_env.post
 
-type type_v = Pgm_types.type_v
+type type_v = Pgm_env.type_v
 
-type type_c = Pgm_types.type_c
+type type_c = Pgm_env.type_c
 
-type binder = Pgm_types.binder
+type binder = Pgm_env.binder
 
 type loop_annotation = {
   loop_invariant : Term.fmla option;

src/programs/pgm_typing.ml

@@ -28,7 +28,7 @@ open Denv
 open Ptree
 open Pgm_effect
 open Pgm_ttree
-open Pgm_types
+open Pgm_env
 module E = Pgm_effect
 
 let debug = ref false
@@ -963,51 +963,43 @@ let add_exception loc x ty gl =
     errorm ~loc "clash with previous exception %s" x;
   add_exception (id_user x loc) ty gl
 
-let file env uc dl =
-  let gl = empty_env uc in
-  let gl, dl =
-    List.fold_left
-      (fun (gl, acc) d -> match d with
-	 | Pgm_ptree.Dlogic dl -> 
-	     let dl = logic_list0_decl dl in
-	     let add1 gl d = Pgm_types.add_pdecl env d gl in
-	     let gl = List.fold_left add1 gl dl in
-	     gl, acc
-	 | Pgm_ptree.Dlet (id, e) -> 
-	     let e = type_expr gl e in
-(* 	     if !debug then *)
-(* 	       eprintf "@[--typing %s-----@\n  %a@]@." id.id print_expr e; *)
-	     let ls, gl = add_global id.id_loc id.id e.expr_type_v gl in
-	     gl, Dlet (ls, e) :: acc
-	 | Pgm_ptree.Dletrec dl -> 
-	     let denv = create_denv gl in
-	     let _, dl = dletrec denv dl in
-	     let _, dl = iletrec gl Mstr.empty dl in
-	     let one gl (v, bl, var, t) =
-	       let loc = loc_of_id v.vs_name in
-	       let id = v.vs_name.id_string in
-	       let t, c = triple gl t in
-	       let tyv = Tarrow (bl, c) in
-	       let ls, gl = add_global loc id tyv gl in
-	       gl, (ls, (v, bl, var, t))
-	     in
-	     let gl, dl = map_fold_left one gl dl in
-	     gl, Dletrec dl :: acc
-	 | Pgm_ptree.Dparam (id, tyv) ->
-	     let denv = create_denv gl in
-	     let tyv = dtype_v denv tyv in
-	     let tyv = type_v gl Mstr.empty tyv in
-	     let ls, gl = add_global id.id_loc id.id tyv gl in
-	     let gl = add_global_if_pure gl ls in
-	     gl, Dparam (ls, tyv) :: acc
-	 | Pgm_ptree.Dexn (id, ty) ->
-	     let ty = option_map (type_type gl) ty in
-	     let _, gl = add_exception id.id_loc id.id ty gl in
-	     gl, acc
-      )
-      (gl, []) dl
-  in
-  gl.uc, List.rev dl
+let decl env gl = function
+  | Pgm_ptree.Dlogic dl -> 
+      let dl = logic_list0_decl dl in
+      let add1 gl d = Pgm_env.add_pdecl env d gl in
+      let gl = List.fold_left add1 gl dl in
+      gl, []
+  | Pgm_ptree.Dlet (id, e) -> 
+      let e = type_expr gl e in
+      (* if !debug then *)
+      (*   eprintf "@[--typing %s-----@\n  %a@]@." id.id print_expr e; *)
+      let ls, gl = add_global id.id_loc id.id e.expr_type_v gl in
+      gl, [Dlet (ls, e)]
+  | Pgm_ptree.Dletrec dl -> 
+      let denv = create_denv gl in
+      let _, dl = dletrec denv dl in
+      let _, dl = iletrec gl Mstr.empty dl in
+      let one gl (v, bl, var, t) =
+	let loc = loc_of_id v.vs_name in
+	let id = v.vs_name.id_string in
+	let t, c = triple gl t in
+	let tyv = Tarrow (bl, c) in
+	let ls, gl = add_global loc id tyv gl in
+	gl, (ls, (v, bl, var, t))
+      in
+      let gl, dl = map_fold_left one gl dl in
+      gl, [Dletrec dl]
+  | Pgm_ptree.Dparam (id, tyv) ->
+      let denv = create_denv gl in
+      let tyv = dtype_v denv tyv in
+      let tyv = type_v gl Mstr.empty tyv in
+      let ls, gl = add_global id.id_loc id.id tyv gl in
+      let gl = add_global_if_pure gl ls in
+      gl, [Dparam (ls, tyv)]
+  | Pgm_ptree.Dexn (id, ty) ->
+      let ty = option_map (type_type gl) ty in
+      let _, gl = add_exception id.id_loc id.id ty gl in
+      gl, []
 
 (*
 Local Variables: 

src/programs/pgm_typing.mli

@@ -26,11 +26,12 @@ type error
 
 exception Error of error
 
-val errorm : ?loc:Loc.position -> ('a, Format.formatter, unit, 'b) format4 -> 'a
-
 val report : Format.formatter -> error -> unit
 
-val file : Env.env -> theory_uc -> Pgm_ptree.file -> theory_uc * Pgm_ttree.file
+(* val errorm : ?loc:Loc.position -> ('a, Format.formatter, unit, 'b) format4 -> 'a *)
 
+val decl : 
+  Env.env -> Pgm_env.env -> Pgm_ptree.decl -> Pgm_env.env * Pgm_ttree.decl list
 
+(* TODO: move elsewhere? *)
 val reference_of_term : Term.term -> Pgm_effect.reference

src/programs/pgm_wp.ml

@@ -28,7 +28,7 @@ open Theory
 open Pretty
 open Pgm_ttree
 open Pgm_typing
-open Pgm_types
+open Pgm_env
 
 module E = Pgm_effect
 
@@ -388,13 +388,9 @@ let decl env = function
 	env
       in
       List.fold_left add_one env dl
-  | Pgm_ttree.Dparam (_ls, _v) ->
+  | Pgm_ttree.Dparam _ ->
       env
 
-let file uc dl =
-  let env = List.fold_left decl (empty_env uc) dl in
-  Theory.close_theory env.uc
-
 (*
 Local Variables: 
 compile-command: "unset LANG; make -C ../.. testl"

src/programs/pgm_wp.mli

@@ -22,7 +22,7 @@ open Theory
 
 val debug : bool ref
 
-val file : theory_uc -> Pgm_ttree.file -> theory
+val decl : Pgm_env.env -> Pgm_ttree.decl -> Pgm_env.env
   (** takes as input the result of [Pgm_typing.file] and produces
       a theory containing the verification conditions as goals,
       one for each function *)