Commit f88a55b6 authored by Benedikt Becker's avatar Benedikt Becker

Merge branch 'markers-everywhere' into 'master'

Markers everywhere, less todos, and tests for mlw_printer

See merge request !369
parents cb4241f1 6368b28c
......@@ -6,7 +6,7 @@ stages:
- deploy
variables:
BUILD_IMAGE: "$CI_REGISTRY_IMAGE:ci-master-2020-04-01"
BUILD_IMAGE: "$CI_REGISTRY_IMAGE:ci-master-2020-04-17"
SPHINX_IMAGE: "$CI_REGISTRY_IMAGE:ci-sphinx"
GIT_CLEAN_FLAGS: "-ffdxq"
......
......@@ -296,6 +296,12 @@ list_stuff () {
fi
}
test_mlw_printer () {
python3 -m sexpdata || return
bench/test_mlw_printer bench/valid/*.mlw
bench/test_mlw_printer bench/typing/good/*.mlw
}
echo "=== Checking stdlib ==="
goods stdlib
goods stdlib/mach
......@@ -467,3 +473,6 @@ echo ""
echo "=== Checking realizations ==="
exec bench/check_realizations.sh
echo "=== Checking mlw_printer ==="
test_mlw_printer
#!/usr/bin/env python3
import sys
import sexpdata
from subprocess import Popen, PIPE
# Read a whyml file as a s-exp
def read(filename):
p = Popen(["bin/why3pp", "--output=sexp", filename], stdout=PIPE, encoding='utf8')
return sexpdata.loads(''.join(p.stdout.readlines()))
# Pretty-print a whyml file and read the result as a s-exp
def print_and_read(filename):
p = Popen(["bin/why3pp", "--output=mlw", filename], stdout=PIPE, encoding='utf8')
p1 = Popen(["bin/why3pp", "--output=sexp", "-"], stdin=p.stdout, stdout=PIPE, encoding='utf8')
return sexpdata.loads(''.join(p1.stdout.readlines()))
class NotEqual(Exception):
def __init__(self, path, sexp0, sexp1):
self.path = path
self.sexp0 = sexp0
self.sexp1 = sexp1
def is_location(sexp):
return (type(sexp) == list and
[type(x) for x in sexp] == [str, int, int, int])
def assert_equal(path, sexp0, sexp1):
if is_location(sexp0) and is_location(sexp1):
return # Don't bother with locations
elif sexp1 == sexpdata.Symbol("__todo__"):
return # And accept todos
elif type(sexp0) == list and type(sexp1) == list:
for i, (s0, s1) in enumerate(zip(sexp0, sexp1)):
return assert_equal(path+[i], s0, s1)
if len(sexp0) > len(sexp1):
raise NotEqual(path+[len(sexp1)], sexp0[len(sexp1)], None)
if len(sexp1) > len(sexp0):
raise NotEqual(path+[len(sexp0)], None, sexp1[len(sexp0)])
elif sexp0 == sexp1:
return
else:
raise NotEqual(path, sexp0, sexp1)
def trace(path, sexp, sexp1):
if path == []:
return [sexpdata.Symbol("EXPECTED"), sexp,
sexpdata.Symbol("FOUND"), sexp1]
elif type(sexp) == list:
return [trace(path[1:], sexp[i], sexp1)
if i == path[0] else sexp[i]
for i, x in enumerate(sexp)]
return sexp
def test(filename):
sexp0 = read(filename)
try:
sexp1 = print_and_read(filename)
assert_equal([], sexp0, sexp1)
print("OK:", filename)
return True
except AssertionError:
print("CANT REPARSE:", filename)
return False
except NotEqual as e:
print("FAILED:", filename)
# sexpdata.dump(trace(e.path, sexp0, e.sexp1), sys.stdout)
return False
def main():
res = all(test(f) for f in sys.argv[1:])
exit(0 if res else 1)
if __name__ == "__main__":
main()
......@@ -310,7 +310,7 @@ let mods = Typing.type_mlw_file env [] "myfile.mlw" mlw_file
(* END{typemodules} *)
(* BEGIN{typemoduleserror} *)
let mods =
let _mods =
try
Typing.type_mlw_file env [] "myfile.mlw" mlw_file
with Loc.Located (loc, e) -> (* A located exception [e] *)
......
module M1
use int.Int
use int.Int
goal g: Int.(=) 4 (Int.(+) 2 2)
end
module M2
use int.Int
use int.Int
let f (x: int) requires { x = 6 } ensures { result = 42 } = Int.(*) x 7
let f (x : int)
requires { x = 6 }
ensures { result = 42 } =
Int.(*) x 7
end
module M3
use int.Int
use ref.Ref
use int.Int
use ref.Ref
let f (_: ())
let f (_ : ())
ensures { Int.(>=) result 0 } =
let x = Ref.ref 42 in (Ref.(!) x)
let x = Ref.ref 42 in Ref.(!) x
end
module M4
use int.Int
use array.Array
use int.Int
use array.Array
let f (a: Array.array int)
let f (a : Array.array int)
requires { Int.(>=) (Array.length a) 1 }
returns { _ -> ((Array.([]) a 0) = 42) } =
returns { _ -> (Array.([]) a 0) = 42 } =
Array.([]<-) a 0 42
end
Tasks are:
......
......@@ -8,7 +8,7 @@ USER root
ARG DEBIAN_FRONTEND=noninteractive
RUN apt-get update -yq && \
apt-get upgrade -yq --with-new-pkgs --auto-remove && \
apt-get install -yq --no-install-recommends wget libgmp-dev xvfb unzip build-essential autoconf ocaml-nox ca-certificates git xauth graphviz menhir libmenhir-ocaml-dev libzip-ocaml-dev liblablgtksourceview3-ocaml-dev libzarith-ocaml-dev && \
apt-get install -yq --no-install-recommends wget libgmp-dev xvfb unzip build-essential autoconf ocaml-nox ca-certificates git xauth graphviz menhir libmenhir-ocaml-dev libzip-ocaml-dev liblablgtksourceview3-ocaml-dev libzarith-ocaml-dev python3-sexpdata && \
apt-get clean
RUN wget --quiet https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/local/bin/opam && \
......
This diff is collapsed.
......@@ -9,20 +9,24 @@
(* *)
(********************************************************************)
(** {1 Pretty printing of Why3 parse trees as Why3 source code} *)
(** {1 Pretty printing of Why3 parse trees as WhyML source code} *)
(** {2 Printers} *)
val pp_pattern : Ptree.pattern Pp.pp
type 'a printers = { marked: 'a Pp.pp; closed: 'a Pp.pp }
(** The [marked] printer potentially adds the marker, the [closed] printer adds
parentheses to the potentially marked node *)
val pp_pattern : Ptree.pattern printers
(** Printer for patterns *)
val pp_expr : Ptree.expr Pp.pp
val pp_expr : Ptree.expr printers
(** Printer for expressions *)
val pp_term : Ptree.term Pp.pp
val pp_term : Ptree.term printers
(** Printer for terms *)
val pp_pty : Ptree.pty Pp.pp
val pp_pty : Ptree.pty printers
(** Printer for types *)
val pp_decl : Ptree.decl Pp.pp
......
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