Commit fd87a342 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

switch to the new implementation of WhyML

parent 8ebe7bb5
...@@ -655,11 +655,11 @@ $(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide ...@@ -655,11 +655,11 @@ $(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
byte: bin/why3replayer.byte byte: bin/why3replayer.byte
opt: bin/why3replayer.opt opt: bin/why3replayer.opt
bin/why3replayer.opt: src/why3.cmxa $(PGMCMX) $(REPLAYERCMX) bin/why3replayer.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) $(REPLAYERCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^ $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3replayer.byte: src/why3.cma $(PGMCMO) $(REPLAYERCMO) bin/why3replayer.byte: src/why3.cma $(PGMCMO) $(MLWCMO) $(REPLAYERCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^ $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
...@@ -705,11 +705,11 @@ $(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session ...@@ -705,11 +705,11 @@ $(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session
byte: bin/why3session.byte byte: bin/why3session.byte
opt: bin/why3session.opt opt: bin/why3session.opt
bin/why3session.opt: src/why3.cmxa $(PGMCMX) $(SESSIONCMX) bin/why3session.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) $(SESSIONCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^ $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3session.byte: src/why3.cma $(PGMCMO) $(SESSIONCMO) bin/why3session.byte: src/why3.cma $(PGMCMO) $(MLWCMO) $(SESSIONCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^ $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
...@@ -760,11 +760,11 @@ opt: bin/why3bench.opt ...@@ -760,11 +760,11 @@ opt: bin/why3bench.opt
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I @SQLITE3LIB@ bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I @SQLITE3LIB@
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3 bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(BENCHCMX) bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) $(BENCHCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^ $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3bench.byte: src/why3.cma $(PGMCMO) $(BENCHCMO) bin/why3bench.byte: src/why3.cma $(PGMCMO) $(MLWCMO) $(BENCHCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^ $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
...@@ -1074,11 +1074,11 @@ $(WHY3DOCDEP): $(WHY3DOCGENERATED) ...@@ -1074,11 +1074,11 @@ $(WHY3DOCDEP): $(WHY3DOCGENERATED)
byte: bin/why3doc.byte byte: bin/why3doc.byte
opt: bin/why3doc.opt opt: bin/why3doc.opt
bin/why3doc.opt: src/why3.cmxa $(PGMCMX) $(WHY3DOCCMX) bin/why3doc.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) $(WHY3DOCCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^ $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3doc.byte: src/why3.cma $(PGMCMO) $(WHY3DOCCMO) bin/why3doc.byte: src/why3.cma $(PGMCMO) $(MLWCMO) $(WHY3DOCCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^ $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
......
module M
type t = {| mutable a : int; mutable b : int |}
val f : x:t -> {} unit writes x {}
end
...@@ -6,6 +6,6 @@ module M ...@@ -6,6 +6,6 @@ module M
let test () = let test () =
let x = ref 0 in let x = ref 0 in
fun y -> x := y; !x fun y -> { } x := y; !x { result = !x }
end end
(* missing int.Int *)
module M
let foo () = for i = 1 to 3 do () done
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/bad-typing/for1"
End:
*)
module P
use import module ref.Ref
let f (a : ref int) = a
end
(* a module is not a theory *)
module M
end
module M1
use import M
end
...@@ -15,7 +15,7 @@ let f () = ...@@ -15,7 +15,7 @@ let f () =
let k () = let k () =
{} {}
begin begin
b := 0; (* b := 1 for the right-to-left evaluation *) b := 1; (* b := 0 for the left-to-right evaluation *)
b1 := (1 - (f ())) + (f ()); b1 := (1 - (f ())) + (f ());
b2 := (f ()) * (1 - (f ())) b2 := (f ()) * (1 - (f ()))
end end
......
...@@ -150,7 +150,20 @@ let read_channel env path file c = ...@@ -150,7 +150,20 @@ let read_channel env path file c =
let tm, mm = retrieve env path file c in let tm, mm = retrieve env path file c in
mm, tm mm, tm
let library_of_env = Env.register_format "whyml" ["mlw"] read_channel let read_channel =
let one_time_hack = ref true in
fun env path file c ->
let env =
if !one_time_hack then begin
one_time_hack := false;
let genv = Env.env_of_library env in
Env.register_format "whyml-old-library" ["mlw"] read_channel genv
end
else env
in
read_channel env path file c
let library_of_env = Env.register_format "whyml-old" [] read_channel
(* (*
Local Variables: Local Variables:
......
...@@ -38,18 +38,4 @@ let read_channel env path file c = ...@@ -38,18 +38,4 @@ let read_channel env path file c =
Format.pp_print_newline Format.err_formatter ()) mm; Format.pp_print_newline Format.err_formatter ()) mm;
mm, tm mm, tm
(* TODO: remove this function once whyml becomes the default *) let library_of_env = Env.register_format "whyml" ["mlw"] read_channel
let read_channel =
let one_time_hack = ref true in
fun env path file c ->
let env =
if !one_time_hack then begin
one_time_hack := false;
let genv = Env.env_of_library env in
Env.register_format "whyml-library" ["mlw"] read_channel genv
end
else env
in
read_channel env path file c
let library_of_env = Env.register_format "whyml-exp" ["mlx"] read_channel
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