make bench verifie aussi les programmes dans examples/programs/

Makefile.in

@@ -244,8 +244,8 @@ WHYVO=lib/coq/Why.vo
 bench/bench : bench/bench.in config.status
 	./config.status --file bench/bench
 
-bench:: $(BINARY) bench/bench $(TOOLS)
-	sh bench/bench "$(BINARY) -I theories/"
+bench:: $(BINARY) $(BINARYL) bench/bench $(TOOLS)
+	sh bench/bench "$(BINARY) -I theories/" "$(BINARYL) -I theories"
 
 BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
 BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))

bench/bench.in

@@ -5,7 +5,7 @@
 export WHYLIB=../lib
 
 pgm=$1
-option=$2
+pgml=$2
 
 goods () {
     for f in $1/*.why; do
@@ -47,6 +47,19 @@ drivers () {
     done
 }
 
+programs () {
+    for f in $1/*.mlw; do
+	echo -n "  "$f"... "
+	if ! $pgml $f > /dev/null 2>&1; then 
+	    echo "$pgml $2 $f"
+	    echo "FAILED!"
+	    exit 1 
+        else 
+	    echo "ok"
+	fi
+    done
+}
+
 # 1. Syntax
 echo "=== Parsing good files  ==="
 goods bench/typing/bad --parse-only
@@ -69,3 +82,7 @@ echo "=== Checking drivers ==="
 drivers drivers
 echo ""
 
+echo "=== Type-checking programs ==="
+programs examples/programs
+echo ""
+

src/parser/typing.ml

@@ -787,22 +787,17 @@ let add_logics dl th =
   let dl = List.map type_decl dl in
   List.fold_left add_decl th (create_logic_decls dl)
 
-let env_of_denv denv =
-  Mstr.mapi 
-    (fun x dty -> create_vsymbol (id_fresh x) (ty_of_dty dty))
-    denv.dvars
-
-let type_term denv t =
+let type_term denv env t =
   let t = dterm denv t in
-  term (env_of_denv denv) t
+  term env t
 
-let term uc = type_term (create_denv uc)
+let term uc = type_term (create_denv uc) Mstr.empty
 
-let type_fmla denv f =
+let type_fmla denv env f =
   let f = dfmla denv f in
-  fmla (env_of_denv denv) f
+  fmla env f
 
-let fmla uc = type_fmla (create_denv uc)
+let fmla uc = type_fmla (create_denv uc) Mstr.empty
 
 let add_prop k loc s f th =
   let f = fmla th f in

src/parser/typing.mli

@@ -19,6 +19,7 @@
 
 (** Typing environments *)
 
+open Util
 open Ty
 open Term
 open Theory
@@ -35,19 +36,6 @@ val read_channel : env -> string -> in_channel -> theory Mnm.t
 
 val add_decl : env -> theory Mnm.t -> theory_uc -> Ptree.decl -> theory_uc
 
-type denv
-
-val create_denv : theory_uc -> denv
-
-val find_user_type_var : string -> denv -> Denv.type_var
-
-val mem_var : string -> denv -> bool
-val find_var : string -> denv -> Denv.dty
-val add_var : string -> Denv.dty -> denv -> denv
-
-val type_term : denv -> Ptree.lexpr -> term
-val type_fmla : denv -> Ptree.lexpr -> fmla
-
 (** error reporting *)
 
 type error
@@ -61,3 +49,16 @@ val report : Format.formatter -> error -> unit
 val specialize_fsymbol : 
   Ptree.qualid -> theory_uc -> lsymbol * Denv.dty list * Denv.dty
 
+type denv
+
+val create_denv : theory_uc -> denv
+
+val find_user_type_var : string -> denv -> Denv.type_var
+
+val mem_var : string -> denv -> bool
+val find_var : string -> denv -> Denv.dty
+val add_var : string -> Denv.dty -> denv -> denv
+
+val type_term : denv -> vsymbol Mstr.t -> Ptree.lexpr -> term
+val type_fmla : denv -> vsymbol Mstr.t -> Ptree.lexpr -> fmla
+

src/programs/pgm_ttree.mli

@@ -66,10 +66,10 @@ type expr = {
 
 and expr_desc =
   | Econstant of constant
-  | Elocal of string
+  | Elocal of Term.vsymbol
   | Eglobal of Term.lsymbol
   | Eapply of expr * expr
-  | Elet of string * expr * expr
+  | Elet of Term.vsymbol * expr * expr
 
   | Esequence of expr * expr
   | Eif of expr * expr * expr

src/programs/pgm_typing.ml

@@ -19,6 +19,7 @@
 
 open Format
 open Util
+open Ident
 open Term
 open Theory
 open Denv
@@ -154,52 +155,55 @@ and expr_desc env loc = function
 
 (* phase 2: typing annotations *)
 
-let rec expr e =
-  let d = expr_desc e.dexpr_denv e.dexpr_desc in
+let rec expr env e =
+  let d = expr_desc env e.dexpr_denv e.dexpr_desc in
   let ty = Denv.ty_of_dty e.dexpr_type in
   { expr_desc = d; expr_type = ty; expr_loc = e.dexpr_loc }
 
-and expr_desc denv = function
+and expr_desc env denv = function
   | DEconstant c ->
       Econstant c
   | DElocal x ->
-      Elocal x
+      Elocal (Mstr.find x env)
   | DEglobal ls ->
       Eglobal ls
   | DEapply (e1, e2) ->
-      Eapply (expr e1, expr e2)
+      Eapply (expr env e1, expr env e2)
   | DElet (x, e1, e2) ->
-      Elet (x, expr e1, expr e2)
+      let e1 = expr env e1 in
+      let v = create_vsymbol (id_fresh x) e1.expr_type in
+      let env = Mstr.add x v env in
+      Elet (v, e1, expr env e2)
 
   | DEsequence (e1, e2) ->
-      Esequence (expr e1, expr e2)
+      Esequence (expr env e1, expr env e2)
   | DEif (e1, e2, e3) ->
-      Eif (expr e1, expr e2, expr e3)
+      Eif (expr env e1, expr env e2, expr env e3)
   | DEwhile (e1, la, e2) ->
       let la = 
 	{ loop_invariant = 
-	    option_map (Typing.type_fmla denv) la.Pgm_ptree.loop_invariant;
+	    option_map (Typing.type_fmla denv env) la.Pgm_ptree.loop_invariant;
 	  loop_variant   = 
-	    option_map (Typing.type_term denv) la.Pgm_ptree.loop_variant; }
+	    option_map (Typing.type_term denv env) la.Pgm_ptree.loop_variant; }
       in
-      Ewhile (expr e1, la, expr e2)
+      Ewhile (expr env e1, la, expr env e2)
   | DElazy (op, e1, e2) ->
-      Elazy (op, expr e1, expr e2)
+      Elazy (op, expr env e1, expr env e2)
   | DEskip ->
       Eskip
 
   | DEassert (k, f) ->
-      let f = Typing.type_fmla denv f in
+      let f = Typing.type_fmla denv env f in
       Eassert (k, f)
   | DEghost e1 -> 
-      Eghost (expr e1)
+      Eghost (expr env e1)
   | DElabel (s, e1) ->
-      Elabel (s, expr e1)
+      Elabel (s, expr env e1)
 
 let code uc id e =
   let env = create_denv uc in
   let e = dexpr env e in
-  ignore (expr e)
+  ignore (expr Mstr.empty e)
 
 (*
 Local Variables: