quelques tests

parent b7dd1446
......@@ -150,10 +150,8 @@ bin/gwhy.byte: $(GCMO)
WHYVO=lib/coq/Why.vo
bench:: $(BINARY) $(WHYVO)
bench:: $(BINARY)
cd bench; sh ./bench "../$(BINARY)"
make -C bench fastwp.bench.ergo
make -C examples ergo
# installation
##############
......
#!/bin/sh
# auto bench for why
export WHYLIB=../lib
pgm=$1
option=$2
coqc="coqc -I ../lib/coq"
pvstc () {
context=`dirname $1`
theory=`basename $1`
cd $context
echo "(typecheck "'"'$theory'"'")" > pvstc.el
pvs -q -batch -l pvstc.el
cd ..
}
provers () {
file=$1
base=$2
dir=`dirname $1`
# running Coq
if ! $coqc "$base"_why.v > /dev/null 2>&1; then
echo "coq FAILED"
$coqc "$base"_why.v
exit 1
fi
# if ! $coqc -I $dir "$base"_valid.v > /dev/null 2>&1; then
# echo "coq validation FAILED"
# $coqc -I $dir "$base"_valid.v
# exit 1
# fi
echo -n "coq ok... "
# running PVS
if ! $pgm --pvs $f > /dev/null 2>&1; then
echo "pvs generation FAILED"
$pgm --pvs $f
exit 1
fi
if test "$option" = "pvs"; then
if ! pvstc "$base"_why > /dev/null 2>&1; then
echo "pvs typecheck FAILED"
pvs -q -v 3 -batch -l pvstc.el
exit 1
fi
echo "pvs ok"
else
echo
fi
}
goods () {
for f in $1/*.why; do
echo -n " "$f"... "
base=$1/`basename $f .why`
# running Why
if ! $pgm $2 $f > /dev/null 2>&1; then
echo "why FAILED"
$pgm $2 $f
exit 1
fi
echo "why ok... "
done
}
good_ml () {
for f in $1/*.why; do
echo -n " "$f"... "
base=$1/`basename $f .why`
# running Why
if ! $pgm --coq-@COQVER@ $f > /dev/null 2>&1; then
echo "why FAILED"
$pgm --coq-@COQVER@ $f
exit 1
fi
echo -n "why ok... "
provers $f $base
# echo -n "coq ok..."
# $pgm --ocaml --ocaml-ext $f > $base.ml 2>/dev/null
# if ocamlc -c $base.ml > /dev/null 2>&1; then
# echo "ocaml ok"
# else
# echo "ocaml FAILED"
# fi
done
}
bads () {
for f in $1/*.why; do
echo -n " "$f"... "
if $pgm $2 $f > /dev/null 2>&1; then
echo "$pgm $2 $f"
echo "FAILED!"
exit 1
else
echo "ok"
fi
done
}
# 1. Syntax
echo "=== Parsing good files ==="
goods typing/bad --parse-only
echo ""
# 2. Typing
echo "=== Type-checking bad files ==="
bads typing/bad --type-only
echo ""
echo "=== Type-checking good files ==="
goods typing/good --type-only
echo ""
theory A end
theory B uses A, A end
theory A end
theory B end
theory C uses A, A:B end
theory A end
theory A end
theory A
end
theory B
uses A
end
......@@ -471,10 +471,10 @@ AC_SUBST(MIZARLIB)
AC_SUBST(FORPACK)
# Finally create the Makefile from Makefile.in
AC_OUTPUT(Makefile)
dnl AC_OUTPUT(Makefile bench/bench)
dnl AC_OUTPUT(Makefile)
AC_OUTPUT(Makefile bench/bench)
chmod a-w Makefile
dnl chmod a+x bench/bench
chmod a+x bench/bench
# Summary
......
......@@ -71,6 +71,7 @@
"match", MATCH;
"not", NOT;
"of", OF;
"open", OPEN;
"or", OR;
"parameter", PARAMETER;
"predicate", PREDICATE;
......
......@@ -16,7 +16,17 @@
open Format
let file = Sys.argv.(1)
let files = ref []
let parse_only = ref false
let type_only = ref false
let () =
Arg.parse
["--parse-only", Arg.Set parse_only, "stops after parsing";
"--type-only", Arg.Set type_only, "stops after type-checking";
]
(fun f -> files := f :: !files)
"usage: why [options] files..."
let rec report fmt = function
| Lexer.Error e ->
......@@ -30,14 +40,17 @@ let rec report fmt = function
| e ->
fprintf fmt "anomaly: %s" (Printexc.to_string e)
let type_file env file =
let c = open_in file in
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let f = Lexer.parse_logic_file lb in
close_in c;
if !parse_only then env else Typing.add_decls env f
let () =
try
let c = open_in file in
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let f = Lexer.parse_logic_file lb in
close_in c;
ignore (Typing.add_decls Typing.empty f)
ignore (List.fold_left type_file Typing.empty !files)
with e ->
eprintf "%a@." report e;
exit 1
......
......@@ -97,7 +97,7 @@
%token EXCEPTION EXISTS EXTERNAL FALSE FOR FORALL FPI FUN FUNCTION GE GOAL GT
%token IF IN INCLUDE INDUCTIVE INT INVARIANT
%token LE LEFTB LEFTBLEFTB LEFTPAR LEFTSQ LET LOGIC LRARROW LT MATCH MINUS
%token NOT NOTEQ OF OR PARAMETER PERCENT PLUS PREDICATE PROP
%token NOT NOTEQ OF OPEN OR PARAMETER PERCENT PLUS PREDICATE PROP
%token QUOTE RAISE RAISES READS REAL REC REF RETURNS RIGHTB RIGHTBRIGHTB
%token RIGHTPAR RIGHTSQ
%token SEMICOLON SLASH
......@@ -205,12 +205,12 @@ decl:
{ Function_def (loc (), $2, $4, $7, $9) }
| GOAL ident COLON lexpr
{ Goal (loc (), $2, $4) }
| TYPE typedecl
{ let loc, vl, id = $2 in TypeDecl (loc, vl, id) }
| TYPE typedecl typedefn
{ let loc, vl, id = $2 in $3 loc vl id }
| USES list1_uident_sep_comma
| USES list1_uses_sep_comma
{ Uses (loc (), $2) }
| OPEN uident
{ Open $2 }
;
list1_theory:
......@@ -491,9 +491,14 @@ list1_lident_sep_comma:
| lident COMMA list1_lident_sep_comma { $1 :: $3 }
;
list1_uident_sep_comma:
| uident { [$1] }
| uident COMMA list1_uident_sep_comma { $1 :: $3 }
list1_uses_sep_comma:
| uses { [$1] }
| uses COMMA list1_uses_sep_comma { $1 :: $3 }
;
uses:
| uqualid { None, $1 }
| uident COLON uqualid { Some $1, $3 }
;
/******* programs **************************************************
......
......@@ -70,7 +70,7 @@ type plogic_type =
| PPredicate of pty list
| PFunction of pty list * pty
type uses = ident
type uses = ident option * qualid
type theory = {
th_loc : loc;
......@@ -89,6 +89,6 @@ and logic_decl =
| AlgType of (loc * ident list * ident * (loc * ident * pty list) list) list
| Theory of theory
| Uses of loc * uses list
| Open of ident
type logic_file = logic_decl list
......@@ -9,18 +9,15 @@ theory A
end
theory B
uses A
logic d : A.t
logic p : A.t -> prop
end
theory C
uses B
uses B, T:B.A
logic e : B.A.t
axiom test : B.p(B.A.c)
axiom test : B.p(T.c)
end
theory Int
......@@ -74,9 +71,9 @@ end
theory Test
uses Eq, List
uses Eq, L : List
axiom a : forall x : 'a. not Eq.eq(List.nil, List.cons(List.nil, List.nil))
axiom a : forall x : 'a. not Eq.eq(L.nil, L.cons(L.nil, L.nil))
end
......@@ -37,6 +37,7 @@ type error =
| BadNumberOfArguments of Name.t * int * int
| ClashTheory of string
| UnboundTheory of string
| AlreadyTheory of string
exception Error of error
......@@ -78,6 +79,8 @@ let report fmt = function
fprintf fmt "clash with previous theory %s" s
| UnboundTheory s ->
fprintf fmt "unbound theory %s" s
| AlreadyTheory s ->
fprintf fmt "already using a theory with name %s" s
(** typing environments *)
......@@ -87,7 +90,7 @@ type env = {
tysymbols : tysymbol M.t; (* type symbols *)
fsymbols : fsymbol M.t; (* function symbols *)
psymbols : psymbol M.t; (* predicate symbols *)
theories : env M.t; (* theories introduced with uses *)
theories : env M.t; (* theories introduced *)
}
let empty = {
......@@ -110,13 +113,6 @@ let add_tysymbol x ty env = { env with tysymbols = M.add x ty env.tysymbols }
let loaded_theories = Hashtbl.create 17
let add_global_theory env t =
try
let th = Hashtbl.find loaded_theories t.id in
{ env with theories = M.add t.id th env.theories }
with Not_found ->
error ~loc:t.id_loc (UnboundTheory t.id)
(** typing using destructive type variables
parsed trees intermediate trees typed trees
......@@ -233,6 +229,10 @@ let find_local_theory t env =
try M.find t.id env.theories
with Not_found -> error ~loc:t.id_loc (UnboundTheory t.id)
let find_global_theory t =
try Hashtbl.find loaded_theories t.id
with Not_found -> error ~loc:t.id_loc (UnboundTheory t.id)
let rec find_theory q env = match q with
| Qident t -> find_local_theory t env
| Qdot (q, t) -> let env = find_theory q env in find_local_theory t env
......@@ -472,6 +472,24 @@ let axiom loc s f env =
ignore (fmla env f);
env
let uses_theory env (as_t, q) =
let loc = qloc q in
let rec find_theory q = match q with
| Qident t ->
t.id, find_global_theory t
| Qdot (q, t) ->
let _, env = find_theory q in t.id, find_local_theory t env
in
let id, th = find_theory q in
let id = match as_t with None -> id | Some x -> x.id in
if M.mem id env.theories then error ~loc (AlreadyTheory id);
{ env with theories = M.add id th env.theories }
let open_theory t env =
let loc = t.id_loc and id = t.id in
if not (M.mem id env.theories) then error ~loc (UnboundTheory id);
assert false (*TODO*)
let rec add_decl env = function
| TypeDecl (loc, sl, s) ->
add_type loc sl s env
......@@ -484,15 +502,22 @@ let rec add_decl env = function
| Theory th ->
add_theory th env
| Uses (loc, uses) ->
List.fold_left add_global_theory env uses
| _ ->
List.fold_left uses_theory env uses
| Open id ->
open_theory id env
| AlgType _
| Goal _
| Function_def _
| Predicate_def _
| Inductive_def _ ->
assert false (*TODO*)
and add_decls env = List.fold_left add_decl env
and add_theory th env =
let id = th.th_name.id in
if M.mem id env.theories then error ~loc:th.th_loc (ClashTheory id);
if Hashtbl.mem loaded_theories id then error ~loc:th.th_loc (ClashTheory id);
let th_env = add_decls empty th.th_decl in
Hashtbl.add loaded_theories id th_env;
env
......
......@@ -16,7 +16,7 @@
open Term
(** typing environments *)
(** Typing environments *)
type env
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment