parsers are now registered (in Env), in preparation for plugins

bench/bench

@@ -94,10 +94,6 @@ echo "=== Type-checking theories ==="
 goods theories --type-only
 echo ""
 
-echo "=== Checking drivers ==="
-drivers drivers
-echo ""
-
 echo "=== Parsing programs ==="
 pgml_options=--parse-only
 programs bench/programs/bad-typing
@@ -116,3 +112,7 @@ programs bench/programs/good
 programs examples/programs
 echo ""
 
+echo "=== Checking drivers ==="
+drivers drivers
+echo ""
+

src/core/env.ml

@@ -63,3 +63,49 @@ let find_theory env sl s =
 
 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
+
+let parse_only_table   = Hashtbl.create 17 (* parser name -> parse_only *)
+let read_channel_table = Hashtbl.create 17 (* parser name -> read_channel *)
+let suffixes_table     = Hashtbl.create 17 (* suffix -> parser name *)
+
+let register_parser name suffixes po rc =
+  Hashtbl.add parse_only_table   name po;
+  Hashtbl.add read_channel_table name rc;
+  List.iter (fun s -> Hashtbl.add suffixes_table ("." ^ s) name) suffixes
+
+exception UnknownParser of string (* parser name *)
+
+let parser_for_file ?name file = match name with
+  | None -> 
+      begin try 
+	let ext = 
+	  let s = Filename.chop_extension file in
+	  let n = String.length s in
+	  String.sub file n (String.length file - n)
+	in
+	Hashtbl.find suffixes_table ext
+      with Invalid_argument _ | Not_found -> 
+	"why"
+      end
+  | Some n -> 
+      n
+
+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
+
+let read_channel ?name env file ic =
+  let n = parser_for_file ?name file in 
+  let rc = find_parser read_channel_table n in
+  rc env file ic
+

src/core/env.mli

@@ -34,3 +34,22 @@ val env_tag : env -> int
 
 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
+
+val register_parser :
+  string -> string list -> parse_only -> read_channel -> unit
+  (** [register_parser name extensions f1 f2] registers a new parser
+      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
+
+val read_channel : ?name:string -> read_channel
+
+exception UnknownParser of string (* parser name *)
+

src/ide/ide_main.ml

@@ -89,7 +89,7 @@ let env = Env.create_env (Typing.retrieve !loadpath)
 
 let theories = 
   let cin = open_in fname in
-  let m = Typing.read_channel env fname cin in
+  let m = Env.read_channel env fname cin in
   close_in cin;
   m
 

src/main.ml

@@ -385,12 +385,10 @@ let do_input env drv = function
         | f   -> f, open_in f
       in
       if !opt_parse_only then begin
-        let lb = Lexing.from_channel cin in
-        Loc.set_file fname lb;
-        ignore (Lexer.parse_logic_file lb);
-        close_in cin;
+	Env.parse_only env fname cin;
+        close_in cin
       end else begin
-        let m = Typing.read_channel env fname cin in
+        let m = Env.read_channel env fname cin in
         close_in cin;
         if !opt_type_only then ()
         else if Queue.is_empty tlist then

src/parser/typing.ml

@@ -1055,6 +1055,17 @@ let retrieve lp env sl =
   let file = locate_file lp sl in
   read_file env file
 
+
+(** 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 () = Env.register_parser "why" ["why"] parse_only read_channel
+
 (*
 Local Variables:
 compile-command: "unset LANG; make -C ../.. test"

src/parser/typing.mli

@@ -28,10 +28,6 @@ open Env
 val retrieve : string list -> retrieve_theory
   (** creates a new typing environment for a given loadpath *)
 
-val read_file : env -> string -> theory Mnm.t
-
-val read_channel : env -> string -> in_channel -> theory Mnm.t
-
 (** incremental parsing *)
 
 val add_decl : env -> theory Mnm.t -> theory_uc -> Ptree.decl -> theory_uc

src/programs/pgm_typing.mli

@@ -32,3 +32,4 @@ val file : Env.env -> theory_uc -> Pgm_ptree.file -> theory_uc * Pgm_ttree.file
 
 val print_type_v : Format.formatter -> Pgm_ttree.type_v -> unit
 
+val purify : theory_uc -> Pgm_ttree.type_v -> Ty.ty

src/programs/pgm_wp.ml

@@ -41,6 +41,7 @@ let empty_env uc = { uc = uc; globals = Mls.empty; locals = Mvs.empty }
 let add_local x v env = { env with locals = Mvs.add x v env.locals }
 let add_global x v env = { env with globals = Mls.add x v env.globals }
 
+let ts_arrow uc = ns_find_ts (get_namespace uc) ["arrow"]
 let ts_ref   env = ns_find_ts (get_namespace env.uc) ["ref"]
 let ts_label env = ns_find_ts (get_namespace env.uc) ["label"]
 
@@ -72,6 +73,40 @@ let post_effect env ef ((_,q),ql) =
 let add_binder env (x, v) = add_local x v env
 let add_binders = List.fold_left add_binder
 
+let v_result ty = create_vsymbol (id_fresh "result") ty
+
+let post_map f ((v, q), ql) = 
+  (v, f q), List.map (fun (e,(v,q)) -> e, (v, f q)) ql
+
+let type_c_of_type_v env = function
+  | Tarrow ([], c) ->
+      c
+  | v ->
+      let ty = purify env.uc v in
+      { c_result_type = v;
+	c_effect      = E.empty;
+	c_pre         = f_true;
+	c_post        = (v_result ty, f_true), []; }
+
+let subst1 vs1 vs2 = Mvs.add vs1 (t_var vs2) Mvs.empty
+
+let rec subst_type_c s c = 
+  { c_result_type = subst_type_v s c.c_result_type;
+    c_effect      = c.c_effect;
+    c_pre         = f_subst s c.c_pre;
+    c_post        = post_map (f_subst s) c.c_post; }
+
+and subst_type_v s = function
+  | Tpure _ as v -> v
+  | Tarrow (bl, c) -> Tarrow (bl, subst_type_c s c)
+
+let apply_type_v env v vs = match v with
+  | Tarrow ((x, _) :: bl, c) ->
+      let c = type_c_of_type_v env (Tarrow (bl, c)) in
+      subst_type_c (subst1 x vs) c
+  | Tarrow ([], _) | Tpure _ -> 
+      assert false
+
 let rec expr env e =
   let ty = e.Pgm_ttree.expr_type in
   let loc = e.Pgm_ttree.expr_loc in
@@ -89,8 +124,10 @@ and expr_desc env _loc ty = function
   | Pgm_ttree.Eglobal ls ->
       assert (Mls.mem ls env.globals);
       Eglobal ls, Mls.find ls env.globals, E.empty
-  | Pgm_ttree.Eapply _ ->
-      assert false (*TODO*)
+  | Pgm_ttree.Eapply (e1, vs) ->
+      let e1 = expr env e1 in
+      let c = apply_type_v env e1.expr_type_v vs in
+      Eany c, c.c_result_type, c.c_effect
   | Pgm_ttree.Eapply_ref _ ->
       assert false (*TODO*)
   | Pgm_ttree.Efun (bl, t) ->
@@ -137,10 +174,17 @@ and recfun _env _def =
 
 (* phase 4: weakest preconditions *******************************************)
 
-(* TODO: use simp forms / tag with label "WP" *)
-let wp_and     = f_and
-let wp_implies = f_implies
-let wp_forall  = f_forall
+(* smart constructors for building WPs
+   TODO: use simp forms / tag with label "WP" *)
+
+let wp_and ?(sym=false) f1 f2 = 
+  (* TODO: tag instead? *)
+  if sym then f_and_simp f1 f2 else f_and_simp f1 (f_implies_simp f1 f2) 
+
+let wp_implies = f_implies_simp
+let wp_forall  = f_forall_simp
+
+(* utility functions for building WPs *)
 
 let fresh_label env =
   let ty = ty_app (ts_label env) [] in
@@ -152,9 +196,6 @@ let wp_binder (x, tv) f = match tv with
 
 let wp_binders = List.fold_right wp_binder 
 
-let post_map f ((v, q), ql) = 
-  (v, f q), List.map (fun (e,(v,q)) -> e, (v, f q)) ql
-
 (* replace old(t) with at(t,lab) everywhere in formula f *)
 let rec old_label env lab f =
   f_map (old_label_term env lab) (old_label env lab) f
@@ -218,8 +259,6 @@ let rec ls_assoc ls = function
   | (ls', x) :: _ when ls_equal ls ls' -> x
   | _ :: r -> ls_assoc ls r
 
-let v_result ty = create_vsymbol (id_fresh "result") ty
-
 let exn_v_result ls = match ls.ls_args with
   | [] -> None
   | [ty] -> Some (v_result ty)
@@ -239,6 +278,8 @@ let saturate_post ty ef f (_, ql) =
   let xs = Sls.elements ef.E.raises in
   ((v_result ty, f), List.map set_post xs)
 
+(* Recursive computation of the weakest precondition *)
+
 let rec wp_expr env e q = 
   let lab = fresh_label env in
   let q = post_map (old_label env lab) q in
@@ -265,7 +306,7 @@ and wp_desc env e q = match e.expr_desc with
       wp_and f q
   | Eassert (Pgm_ptree.Acheck, f) ->
       let (_, q), _ = q in
-      f_and f q (* symetric conjunction instead *)
+      wp_and ~sym:true f q
   | Eassert (Pgm_ptree.Aassume, f) ->
       let (_, q), _ = q in
       wp_implies f q

tests/test-pgm-jcf.mlw

@@ -12,12 +12,12 @@ parameter imp_sub :
 
 parameter r : int ref
 
+parameter write : v:int -> {} unit writes r { !r = v }
+
 let ff () = 
-  { !r = 1 } 
-  label L:
-  assume { !r = 42 };
-  !r + 2
-  { old(!r) = 1 and result=3 }
+  { true } 
+  1+2
+  { result = 3 }
 
 
 (*