diff --git a/Makefile.in b/Makefile.in index a10dcd1a5e3fac6208de45d398b20dafefd57a96..7ce1063ecf7c1ab9d9d2147a2a84eeb356ea9b58 100644 --- a/Makefile.in +++ b/Makefile.in @@ -178,8 +178,8 @@ LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer dri collect_data_model parse_smtv2_model_lexer parse_smtv2_model \ parse_smtv2_model -LIB_MLW = ity expr dexpr pdecl eval_match typeinv vc pmodule \ - pinterp compile pdriver cprinter ocaml_printer +LIB_MLW = ity expr pdecl eval_match typeinv vc pmodule dexpr \ + pinterp mltree compile pdriver cprinter ocaml_printer LIB_PARSER = ptree glob typing parser lexer @@ -1601,8 +1601,9 @@ CLEANDIRS += src/trywhy3 .PHONY: bench test bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \ - share/Makefile.config -# temporarily disabled dependency: bin/why3extract + share/Makefile.config bin/why3extract.@OCAMLBEST@ + bash bench/bench ".@OCAMLBEST@" + @echo "=== Checking Why3 API ===" $(MAKE) test-api-logic.@OCAMLBEST@ # $(MAKE) test-api-mlw-tree.@OCAMLBEST@ # $(MAKE) test-api-mlw.@OCAMLBEST@ @@ -1611,9 +1612,9 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \ # desactivé car requiert findlib # if test -d examples/runstrat ; then \ # $(MAKE) test-runstrat.@OCAMLBEST@ ; fi - bash bench/bench ".@OCAMLBEST@" @if test "@enable_coq_tactic@" = "yes"; then \ - echo "=== checking the Coq tactic ==="; \ + echo ; \ + echo "=== Checking the Coq tactic ==="; \ $(MAKE) test-coq-tactic.@OCAMLBEST@; fi ############### diff --git a/bench/bench b/bench/bench index 6f285fab81517027d2a66199346ca4a6549bb476..17243460d5eaf9af27cc62ce184fcf441c756ac6 100755 --- a/bench/bench +++ b/bench/bench @@ -169,10 +169,6 @@ list_stuff () { fi } -echo "=== Checking invalid goals ===" -invalid_goals bench/invalid -echo "" - echo "=== Checking theories ===" goods theories --type-only # FIXME remove --type-only echo "" @@ -193,6 +189,33 @@ bads bench/typing/bad --type-only bads bench/programs/bad-typing --type-only echo "" +echo "=== Checking good files ===" +goods bench/typing/good +goods bench/programs/good +goods examples/bts +goods examples/tests +goods examples/tests-provers +goods examples/check-builtin +goods examples/logic +goods examples +goods examples/foveoos11-cm +goods examples/WP_revisited +goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps" +goods examples/bitvectors "-L examples/bitvectors" +goods examples/avl "-L examples/avl" +goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication" +goods examples/double_wp "-L examples/double_wp" +goods examples/in_progress +echo "" + +echo "=== Checking valid goals ===" +valid_goals bench/valid +echo "" + +echo "=== Checking invalid goals ===" +invalid_goals bench/invalid +echo "" + echo "=== Checking execution ===" execute examples/euler001.mlw Euler001.bench execute examples/euler002.mlw Solve.bench @@ -225,7 +248,7 @@ execute examples/vstte10_queens.mlw NQueens.test8 echo "" -echo "=== Extraction to Ocaml ===" +echo "=== Checking extraction to OCaml ===" extract_and_run examples/euler001 euler001.ml 1000000 extract_and_run examples/gcd gcd.ml 6 15 extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml @@ -234,31 +257,6 @@ extract_and_run examples/defunctionalization defunctionalization.ml extract_and_run examples/sudoku sudoku.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6 echo "" - - -echo "=== Checking good files ===" -goods bench/typing/good -goods bench/programs/good -goods examples/bts -goods examples/tests -goods examples/tests-provers -goods examples/check-builtin -goods examples/logic -goods examples -goods examples/foveoos11-cm -goods examples/WP_revisited -goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps" -goods examples/bitvectors "-L examples/bitvectors" -goods examples/avl "-L examples/avl" -goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication" -goods examples/double_wp "-L examples/double_wp" -goods examples/in_progress -echo "" - -echo "=== Checking valid goals ===" -valid_goals bench/valid -echo "" - echo "=== Checking --list-* ===" list_stuff --list-transforms list_stuff --list-printers diff --git a/doc/exec.tex b/doc/exec.tex index 247eb2cd94a544d81990f954ec7786507024dc6c..62bf644dbcd679d0355e0dbe25014d2a7935a383 100644 --- a/doc/exec.tex +++ b/doc/exec.tex @@ -127,14 +127,14 @@ we invoke \texttt{extract} from the directory where this file is stored. File \texttt{aqueue.ml} now contains the following OCaml code: \begin{whycode} let enqueue (x: 'a) (q: 'a queue) : 'a queue = -create (q.front) (q.lenf) (x :: (q.rear)) - (Z.add (q.lenr) (Z.of_string "1")) + create (q.front) (q.lenf) (x :: (q.rear)) + (Z.add (q.lenr) (Z.of_string "1")) \end{whycode} Choosing a function symbol as the entry point of extraction allows us to focus only on specific parts of the program. However, the generated code cannot be type-checked by the OCaml compiler, as it depends on function \texttt{create} and on type \texttt{'a queue}, whose definitions are not given. In order to -obtain a \emph{correct} OCaml implementation, we can perform a recursive +obtain a \emph{complete} OCaml implementation, we can perform a recursive extraction: \begin{verbatim} > why3 extraction --recursive -D ocaml64 -L . \ @@ -162,6 +162,9 @@ let enqueue (x: 'a) (q: 'a queue) : 'a queue = create (q.front) (q.lenf) (x :: (q.rear)) (Z.add (q.lenr) (Z.of_string "1")) \end{whycode} +This new version of the code is now accepted by the OCaml compiler. + +Let us now consider the % \label{fig:extract-queens} % \caption{Recursive extraction of \texttt{queens} function.} % \end{figure} diff --git a/examples/add_list.mlw b/examples/add_list.mlw index 999c944049840d4ae81c75d0d06f45ecb73e6938..1accfd87aaf24c983955c43c80c57a88cae65917 100644 --- a/examples/add_list.mlw +++ b/examples/add_list.mlw @@ -59,30 +59,24 @@ module AddListImp use import SumList use import ref.Ref -exception Break - let sum (l: list or_integer_float) : (int, real) = returns { si, sf -> si = add_int l /\ sf = add_real l } let si = ref 0 in let sf = ref 0.0 in let ll = ref l in - try - while True do + while True do invariant { !si + add_int !ll = add_int l /\ - !sf +. add_real !ll = add_real l - } + !sf +. add_real !ll = add_real l } variant { !ll } match !ll with - | Nil -> raise Break + | Nil -> return (!si, !sf) | Cons (Integer n) t -> si := !si + n; ll := t | Cons (Real x) t -> sf := !sf +. x; ll := t end - done; - absurd - with Break -> (!si, !sf) - end + done; + absurd let main () = diff --git a/examples/algo63_fastwp/why3session.xml b/examples/algo63_fastwp/why3session.xml index aa0c8c8385d5723eda05db92ee160fb5f17bc56d..d8124c2bd7cc3f3345539a9d5ffd82707900a4a4 100644 --- a/examples/algo63_fastwp/why3session.xml +++ b/examples/algo63_fastwp/why3session.xml @@ -2,176 +2,223 @@ - - - + + - + - + - + - + - + - + - + - + - + - + - + - + - - + + - + - - + + - + - + - + - - + + - + - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - + - - + + - - + + - - - + + - - - + + - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - + - + diff --git a/examples/algo63_fastwp/why3shapes.gz b/examples/algo63_fastwp/why3shapes.gz index 1a620014d8d52ee8580baa2ec30186f701b00465..cba1b41a481e45fb67be7aee3048682deb58c1e3 100644 Binary files a/examples/algo63_fastwp/why3shapes.gz and b/examples/algo63_fastwp/why3shapes.gz differ diff --git a/examples/bag.mlw b/examples/bag.mlw index 58d53f8f9b9771a82efa05a2f32598e9f1e2352a..97bca7e6b5cc3caa3724f2f02551c617936e1b19 100644 --- a/examples/bag.mlw +++ b/examples/bag.mlw @@ -1,7 +1,6 @@ module Bag - use BuiltIn use import int.Int type bag 'a = 'a -> int @@ -13,10 +12,10 @@ module Bag fun _ -> 0 let ghost function add (e: 'a) (b: bag 'a): bag 'a = - fun x -> if BuiltIn.(=) x e then b x + 1 else b x + fun x -> if pure {x = e} then b x + 1 else b x let ghost function remove (e: 'a) (b: bag 'a): bag 'a = - fun x -> if BuiltIn.(=) x e then b x - 1 else b x + fun x -> if pure {x = e} then b x - 1 else b x end diff --git a/examples/binary_search.mlw b/examples/binary_search.mlw index 6d3ce8c7551ea6de4fdad172db16f9227b989de5..372a2346dab1a310a0e414aa26f0f59fce6b568e 100644 --- a/examples/binary_search.mlw +++ b/examples/binary_search.mlw @@ -11,34 +11,30 @@ module BinarySearch (* the code and its specification *) - exception Break int (* raised to exit the loop *) exception Not_found (* raised to signal a search failure *) let binary_search (a : array int) (v : int) : int requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] } ensures { 0 <= result < length a /\ a[result] = v } raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v } - = try - let l = ref 0 in - let u = ref (length a - 1) in - while !l <= !u do - invariant { 0 <= !l /\ !u < length a } - invariant { - forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u } - variant { !u - !l } - let m = !l + div (!u - !l) 2 in - assert { !l <= m <= !u }; - if a[m] < v then - l := m + 1 - else if a[m] > v then - u := m - 1 - else - raise (Break m) - done; - raise Not_found - with Break i -> - i - end + = + let l = ref 0 in + let u = ref (length a - 1) in + while !l <= !u do + invariant { 0 <= !l /\ !u < length a } + invariant { + forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u } + variant { !u - !l } + let m = !l + div (!u - !l) 2 in + assert { !l <= m <= !u }; + if a[m] < v then + l := m + 1 + else if a[m] > v then + u := m - 1 + else + return m + done; + raise Not_found end @@ -51,7 +47,6 @@ module BinarySearchAnyMidPoint use import ref.Ref use import array.Array - exception Break int (* raised to exit the loop *) exception Not_found (* raised to signal a search failure *) val midpoint (l:int) (u:int) : int @@ -61,26 +56,23 @@ module BinarySearchAnyMidPoint requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] } ensures { 0 <= result < length a /\ a[result] = v } raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v } - = try - let l = ref 0 in - let u = ref (length a - 1) in - while !l <= !u do - invariant { 0 <= !l /\ !u < length a } - invariant { - forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u } - variant { !u - !l } - let m = midpoint !l !u in - if a[m] < v then - l := m + 1 - else if a[m] > v then - u := m - 1 - else - raise (Break m) - done; - raise Not_found - with Break i -> - i - end + = + let l = ref 0 in + let u = ref (length a - 1) in + while !l <= !u do + invariant { 0 <= !l /\ !u < length a } + invariant { + forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u } + variant { !u - !l } + let m = midpoint !l !u in + if a[m] < v then + l := m + 1 + else if a[m] > v then + u := m - 1 + else + return m + done; + raise Not_found end @@ -95,7 +87,6 @@ module BinarySearchInt32 (* the code and its specification *) - exception Break int32 (* raised to exit the loop *) exception Not_found (* raised to signal a search failure *) let binary_search (a : array int32) (v : int32) : int32 @@ -104,27 +95,24 @@ module BinarySearchInt32 ensures { 0 <= to_int result < to_int a.length /\ a[to_int result] = v } raises { Not_found -> forall i:int. 0 <= i < to_int a.length -> a[i] <> v } - = try - let l = ref (of_int 0) in - let u = ref (length a - of_int 1) in - while !l <= !u do - invariant { 0 <= to_int !l /\ to_int !u < to_int a.length } - invariant { forall i : int. 0 <= i < to_int a.length -> - a[i] = v -> to_int !l <= i <= to_int !u } - variant { to_int !u - to_int !l } - let m = !l + (!u - !l) / of_int 2 in - assert { to_int !l <= to_int m <= to_int !u }; - if a[m] < v then - l := m + of_int 1 - else if a[m] > v then - u := m - of_int 1 - else - raise (Break m) - done; - raise Not_found - with Break i -> - i - end + = + let l = ref (of_int 0) in + let u = ref (length a - of_int 1) in + while !l <= !u do + invariant { 0 <= to_int !l /\ to_int !u < to_int a.length } + invariant { forall i : int. 0 <= i < to_int a.length -> + a[i] = v -> to_int !l <= i <= to_int !u } + variant { to_int !u - to_int !l } + let m = !l + (!u - !l) / of_int 2 in + assert { to_int !l <= to_int m <= to_int !u }; + if a[m] < v then + l := m + of_int 1 + else if a[m] > v then + u := m - of_int 1 + else + return m + done; + raise Not_found end diff --git a/examples/binomial_heap/why3session.xml b/examples/binomial_heap/why3session.xml index 82a396f3483b37d34978d1af146449df847d54e1..21c7efefd723a5c2bd43a2f3e4a8c29e20f1fbe8 100644 --- a/examples/binomial_heap/why3session.xml +++ b/examples/binomial_heap/why3session.xml @@ -7,7 +7,7 @@ - + diff --git a/examples/binomial_heap/why3shapes.gz b/examples/binomial_heap/why3shapes.gz index 28e2eacf8255564cc51079b26d2098838bedcf2f..5950210f70a61642168ffe933986f43d40692630 100644 Binary files a/examples/binomial_heap/why3shapes.gz and b/examples/binomial_heap/why3shapes.gz differ diff --git a/examples/bitvector_examples/why3session.xml b/examples/bitvector_examples/why3session.xml index f66e689c4c2f0cf8baa6c147384b90fde126004b..89a77a8286d209324fd65fd889cb1b99204b3948 100644 --- a/examples/bitvector_examples/why3session.xml +++ b/examples/bitvector_examples/why3session.xml @@ -6,7 +6,7 @@ - + diff --git a/examples/bitvector_examples/why3shapes.gz b/examples/bitvector_examples/why3shapes.gz index 7faa1649ba773db20d22ab11f50c346e45864345..eceb148251ee83229da1728216da12f20a1cef36 100644 Binary files a/examples/bitvector_examples/why3shapes.gz and b/examples/bitvector_examples/why3shapes.gz differ diff --git a/examples/braun_trees/why3session.xml b/examples/braun_trees/why3session.xml index b588caeac8425a7706399ebd6c69fe636f27e68c..6bd105a89bf9fab191469274e5399aacf460c958 100644 --- a/examples/braun_trees/why3session.xml +++ b/examples/braun_trees/why3session.xml @@ -2,9 +2,10 @@ + - + @@ -23,8 +24,8 @@ - - + + @@ -75,8 +76,8 @@ - - + + @@ -134,27 +135,27 @@ - + - - + + - + - + - + - + - + - + diff --git a/examples/braun_trees/why3shapes.gz b/examples/braun_trees/why3shapes.gz index cf38acdd8100500046c9d7fba7aeb0853668ee95..99d17858b29d93866a89e7afbb7dccab01444f3b 100644 Binary files a/examples/braun_trees/why3shapes.gz and b/examples/braun_trees/why3shapes.gz differ diff --git a/examples/check-builtin/real/why3session.xml b/examples/check-builtin/real/why3session.xml index fd8a3e59527f80f6e901e0ee8f82d07746e08651..5896c780dbbc58d622391a131c99c6c96d75dec2 100644 --- a/examples/check-builtin/real/why3session.xml +++ b/examples/check-builtin/real/why3session.xml @@ -106,7 +106,7 @@ - + diff --git a/examples/check-builtin/real/why3shapes.gz b/examples/check-builtin/real/why3shapes.gz index af58c6f7f9cf559c17d3db7ba8f574607281bc4a..0130a3baa6b12946057b00ea4957e743984f3b8a 100644 Binary files a/examples/check-builtin/real/why3shapes.gz and b/examples/check-builtin/real/why3shapes.gz differ diff --git a/examples/decrease1.mlw b/examples/decrease1.mlw index a6ca10d134d9ca2340cf2ce1fc400f0de6699a73..164c0a5bfeb1474646312f9b20838fd6b4840f1b 100644 --- a/examples/decrease1.mlw +++ b/examples/decrease1.mlw @@ -21,8 +21,6 @@ module Decrease1 variant { j - i } = if i < j then decrease1_induction a (i+1) j - exception Found - let search (a: array int) requires { decrease1 a } ensures { @@ -30,18 +28,14 @@ module Decrease1 \/ (0 <= result < length a /\ a[result] = 0 /\ forall j: int. 0 <= j < result -> a[j] <> 0) } = let i = ref 0 in - try - while !i < length a do - invariant { 0 <= !i } - invariant { forall j: int. 0 <= j < !i -> j < length a -> a[j] <> 0 } - variant { length a - !i } - if a[!i] = 0 then raise Found; - if a[!i] > 0 then i := !i + a[!i] else i := !i + 1 - done; - -1 - with Found -> - !i - end + while !i < length a do + invariant { 0 <= !i } + invariant { forall j: int. 0 <= j < !i -> j < length a -> a[j] <> 0 } + variant { length a - !i } + if a[!i] = 0 then return !i; + if a[!i] > 0 then i := !i + a[!i] else i := !i + 1 + done; + -1 let rec search_rec (a: array int) (i : int) requires { decrease1 a /\ 0 <= i } diff --git a/examples/dfs.mlw b/examples/dfs.mlw index 6d9521ba5d209472066160a7391725f0b4fbf2a8..106cac72dcc517a1d4031df9cc3b16ad60b8bdb1 100644 --- a/examples/dfs.mlw +++ b/examples/dfs.mlw @@ -105,4 +105,4 @@ module DFS assert { well_colored !marked !busy }; dfs root -end \ No newline at end of file +end diff --git a/examples/double_wp/compiler.mlw b/examples/double_wp/compiler.mlw index 1f1d4722efdc04e8beedb0efe9c27bc9b38682d0..85e871f211e7e5142681b9df6dd4bf4c751c5b33 100644 --- a/examples/double_wp/compiler.mlw +++ b/examples/double_wp/compiler.mlw @@ -24,8 +24,8 @@ module Compile_aexpr meta rewrite_def function aexpr_post let rec compile_aexpr (a:aexpr) : hl 'a - ensures { result <% (trivial_pre,aexpr_post a result.code.length) } - ensures { hl_correctness result } + ensures { result.pre --> trivial_pre } + ensures { result.post --> aexpr_post a result.code.length } variant { a } = let c = match a with | Anum n -> $ iconstf n @@ -74,9 +74,9 @@ module Compile_bexpr meta rewrite_def function exec_cond let rec compile_bexpr (b:bexpr) (cond:bool) (ofs:ofs) : hl 'a - ensures { let len = result.code.length in - result <% (trivial_pre,bexpr_post b cond (len + ofs) len) } - ensures { hl_correctness result } + ensures { result.pre --> trivial_pre } + ensures { result.post --> let len = result.code.length in + bexpr_post b cond (len + ofs) len } variant { b } = let c = match b with | Btrue -> $ if cond then ibranchf ofs else inil () @@ -164,9 +164,8 @@ module Compile_com (forall pk sk mk. var (VMS pk sk mk) (VMS pi si mi) -> mk = mj) let rec compile_com (cmd: com) : hl 'a - ensures { hl_correctness result } - ensures { let len = result.code.length in - result <% (com_pre cmd,com_post cmd len) } + ensures { result.pre --> com_pre cmd } + ensures { result.post --> let len = result.code.length in com_post cmd len } variant { cmd } = let res = match cmd with | Cskip -> $ inil () diff --git a/examples/double_wp/compiler/why3session.xml b/examples/double_wp/compiler/why3session.xml index 58c52735164bd11e83ecf1e3711fee884fdbae8f..61d942682e923765beaaae0cacbb6b568ea0d3e9 100644 --- a/examples/double_wp/compiler/why3session.xml +++ b/examples/double_wp/compiler/why3session.xml @@ -5,91 +5,37 @@ - + - - + + - - + + - - + + - + - - + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - + - + - - + + @@ -97,14 +43,14 @@ - + - + - + - - + + @@ -112,14 +58,14 @@ - + - + - + - - + + @@ -127,14 +73,14 @@ - + - + - + - - + + @@ -142,14 +88,14 @@ - + - + - + - - + + @@ -159,115 +105,59 @@ - - + + - - + + - + - + - - + + - - + + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + - - - - - - - - - - + + + + + + + + + + @@ -275,29 +165,33 @@ - - - - - - - - + + + + + + + + + + + + - - - - - - - - - - + + + + + + + + + + @@ -305,14 +199,14 @@ - + - + - + - - + + @@ -320,29 +214,33 @@ - - - - - - - - + + + + + + + + + + + + - - - - - - - - - - + + + + + + + + + + @@ -350,29 +248,33 @@ - - - - - - - - + + + + + + + + + + + + - - - - - - - - - - + + + + + + + + + + @@ -380,14 +282,33 @@ - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -397,78 +318,78 @@ - - + + - - + + - + - + - + - + - + - + - + - + - + - + - + - + @@ -478,109 +399,31 @@ - - + + - - + + - - + + - - + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - + - + - - + + @@ -588,14 +431,14 @@ - + - + - + - - + + @@ -603,14 +446,36 @@ - + - + - + - - + + + + + + + + + + + + + + + + + + + + + + + + @@ -618,14 +483,14 @@ - + - + - + - - + + @@ -633,100 +498,100 @@ - + - + - + - + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + @@ -738,11 +603,11 @@ - - + + - - + + @@ -755,7 +620,7 @@ - + @@ -764,7 +629,7 @@ - + @@ -772,10 +637,10 @@ - + - + diff --git a/examples/double_wp/compiler/why3shapes.gz b/examples/double_wp/compiler/why3shapes.gz index 36f9cb97b559d0b81fe0224890d5e53b89cbf632..ddb38efc64181092c7ffa1cc54a942b1e8024d76 100644 Binary files a/examples/double_wp/compiler/why3shapes.gz and b/examples/double_wp/compiler/why3shapes.gz differ diff --git a/examples/double_wp/imp/why3session.xml b/examples/double_wp/imp/why3session.xml index 75c074c55a7755ea40a3ff022fac218dd90a583d..6435d459490b6e927cbb7706db1b91930840288e 100644 --- a/examples/double_wp/imp/why3session.xml +++ b/examples/double_wp/imp/why3session.xml @@ -4,62 +4,62 @@ - + - + - + - + - + - + - + - + - + diff --git a/examples/double_wp/imp/why3shapes.gz b/examples/double_wp/imp/why3shapes.gz index 6ec1fc1b2dda116a6fe5e57d2f7997185de40ec0..94eeb379bb90bb17bc6df366198236bc7a590b6e 100644 Binary files a/examples/double_wp/imp/why3shapes.gz and b/examples/double_wp/imp/why3shapes.gz differ diff --git a/examples/double_wp/logic.mlw b/examples/double_wp/logic.mlw index be410aaa7316c464042ddc1e3fd517e441d741b5..06d7c40c5a97ecf442c00d4384f96fdadf80500b 100644 --- a/examples/double_wp/logic.mlw +++ b/examples/double_wp/logic.mlw @@ -32,19 +32,15 @@ module Compiler_logic type pre 'a = 'a -> pos -> pred type post 'a = 'a -> pos -> rel + (* Machine transition valid whatever the global code is. *) + predicate contextual_irrelevance (c:code) (p:pos) (ms1 ms2:machine_state) = + forall c_glob. codeseq_at c_glob p c -> transition_star c_glob ms1 ms2 + (* Hoare triples with explicit pre & post *) type hl 'a = { code: code; ghost pre : pre {'a}; ghost post: post {'a} } - - (* (<%): pack the pre/post rewriting. - lock is an artifact to prevent unrolling of - h's definition recursively. *) - let function lock () : (int,int) = - ensures { result = (0,0) } - while false do variant { 0 } () done; (0,0) - predicate (<%) (h:hl 'a) (x:(pre 'a,post 'a)) = - let (pr,ps) = x in - h --> { code = let (_,_) = lock () in h.code; pre = pr; post = ps } - meta rewrite_def predicate (<%) + (* (Total) correctness for hoare triple. *) + invariant { forall x:'a,p ms. pre x p ms -> + exists ms'. post x p ms ms' /\ contextual_irrelevance code p ms ms' } (* Predicate transformer type. Same auxiliary variables as for Hoare triples. *) @@ -52,20 +48,9 @@ module Compiler_logic (* Code with backward predicate transformer. *) type wp 'a = { wcode : code; ghost wp : wp_trans {'a} } - - (* Machine transition valid whatever the global code is. *) - predicate contextual_irrelevance (c:code) (p:pos) (ms1 ms2:machine_state) = - forall c_glob. codeseq_at c_glob p c -> transition_star c_glob ms1 ms2 - - (* (Total) correctness for hoare triple. *) - predicate hl_correctness (cs:hl 'a) = - forall x:'a,p ms. cs.pre x p ms -> - exists ms'. cs.post x p ms ms' /\ contextual_irrelevance cs.code p ms ms' - - (* Similar definition for backward predicate transformers *) - predicate wp_correctness (code:wp 'a) = - forall x:'a,p post ms. (code.wp x p post) ms -> - exists ms'. post ms' /\ contextual_irrelevance code.wcode p ms ms' + (* Similar invariant for backward predicate transformers *) + invariant { forall x:'a,p post ms. wp x p post ms -> + exists ms'. post ms' /\ contextual_irrelevance wcode p ms ms' } (* WP combinator for sequence. Similar to the standard WP calculus for sequence. The initial machine state is memorized in auxiliary @@ -81,10 +66,8 @@ module Compiler_logic (* Code combinator for sequence, with wp. *) let (--) (s1 : wp 'a) (s2 : wp ('a, machine_state)) : wp 'a - requires { wp_correctness s1 /\ wp_correctness s2 } - ensures { result.wcode.length = s1.wcode.length + s2.wcode.length } + ensures { result.wcode.length --> s1.wcode.length + s2.wcode.length } ensures { result.wp --> seq_wp s1.wcode.length s1.wp s2.wp } - ensures { wp_correctness result } = let code = s1.wcode ++ s2.wcode in let res = { wcode = code; wp = seq_wp s1.wcode.length s1.wp s2.wp } in assert { forall x: 'a, p post ms. res.wp x p post ms -> @@ -106,9 +89,8 @@ module Compiler_logic Similar to WP calculus for (if cond then s). *) let (%) (s:wp 'a) (ghost cond:pre {'a}) : wp 'a - requires { wp_correctness s } ensures { result.wp --> fork_wp s.wp cond } - ensures { result.wcode.length = s.wcode.length /\ wp_correctness result } + ensures { result.wcode.length --> s.wcode.length } = { wcode = s.wcode; wp = fork_wp s.wp cond } (* WP transformer for hoare triples. *) @@ -118,26 +100,23 @@ module Compiler_logic lemma towp_wp_lemma: forall pr ps, x:'a, p q ms. towp_wp pr ps x p q ms = (pr x p ms && (forall ms'. ps x p ms ms' -> q ms')) - meta rewrite lemma towp_wp_lemma (* Unwrap code with hoare triple into code with wp. Analogous to procedure call/abstract block. *) let ($_) (c:hl 'a) : wp 'a - requires { hl_correctness c } - ensures { result.wcode.length = c.code.length } + ensures { result.wcode.length --> c.code.length } ensures { result.wp --> towp_wp c.pre c.post } - ensures { wp_correctness result } = { wcode = c.code; wp = towp_wp c.pre c.post } (* Equip code with pre/post-condition. That is here that proof happen. (P -> wp (c,Q)). Anologous to checking function/abstract block specification. *) let hoare (ghost pre:pre {'a}) (c:wp 'a) (ghost post:post {'a}) : hl 'a - requires { wp_correctness c } requires { forall x p ms. pre x p ms -> (c.wp x p (post x p ms)) ms } - ensures { result <% (pre,post) } - ensures { result.code.length = c.wcode.length /\ hl_correctness result} + ensures { result.pre --> pre } + ensures { result.post --> post } + ensures { result.code.length --> c.wcode.length } = { code = c.wcode ; pre = pre; post = post } function trivial_pre : pre 'a = fun _ p ms -> let VMS p' _ _ = ms in p = p' @@ -175,15 +154,13 @@ module Compiler_logic (* Code combinator for looping construct. *) let make_loop (c:wp 'a) (ghost inv cont:pre {'a}) (ghost var:post {'a}) : wp 'a - requires { wp_correctness c } ensures { result.wp --> loop_wp c.wp inv cont var } - ensures { wp_correctness result } - ensures { result.wcode.length = c.wcode.length } - = let res = { wcode = c.wcode; wp = loop_wp c.wp inv cont var } in - assert { forall x p q ms0. res.wp x p q ms0 -> + ensures { result.wcode.length --> c.wcode.length } + = let wpt = loop_wp c.wp inv cont var in + assert { forall x p q ms0. wpt x p q ms0 -> forall ms. inv x p ms -> acc (var x p) ms -> - exists ms'. contextual_irrelevance res.wcode p ms ms' /\ q ms' + exists ms'. contextual_irrelevance c.wcode p ms ms' /\ q ms' }; - res + { wcode = c.wcode; wp = wpt } end diff --git a/examples/double_wp/logic/why3session.xml b/examples/double_wp/logic/why3session.xml index 2e159a90e9ee3e4878674db8da9b26aaca824803..0cfdd32f934f57885b37b90ae73d575816d6c41b 100644 --- a/examples/double_wp/logic/why3session.xml +++ b/examples/double_wp/logic/why3session.xml @@ -4,27 +4,25 @@ + - - - - + - - + + - - + + - + - + @@ -38,7 +36,7 @@ - + @@ -58,7 +56,7 @@ - + @@ -66,14 +64,14 @@ - - + + - + - + diff --git a/examples/double_wp/logic/why3shapes.gz b/examples/double_wp/logic/why3shapes.gz index 1105c0cc2f0a30df3a70464c590e7171bd600353..bc33d9d41142a872e7a7902b992903ea7e553bde 100644 Binary files a/examples/double_wp/logic/why3shapes.gz and b/examples/double_wp/logic/why3shapes.gz differ diff --git a/examples/double_wp/specs.mlw b/examples/double_wp/specs.mlw index cff0cc1ae73b8ed88f9748e4744b65d3d98b043f..5c60280a098120b0cc73a14fcc9d8580bcc9c828 100644 --- a/examples/double_wp/specs.mlw +++ b/examples/double_wp/specs.mlw @@ -20,8 +20,9 @@ module VM_instr_spec (ghost f:machine_state -> machine_state) : hl 'a requires { forall c p. codeseq_at c p code_f -> forall x ms. pre x p ms -> transition c ms (f ms) } - ensures { result <% (pre,ifun_post f) } - ensures { result.code = code_f /\ hl_correctness result } + ensures { result.pre --> pre } + ensures { result.post --> ifun_post f } + ensures { result.code --> code_f } = let res = { pre = pre; code = code_f; post = ifun_post f } in assert { forall x p ms. res.pre x p ms -> not (exists ms' : machine_state. res.post x p ms ms' /\ @@ -39,8 +40,9 @@ module VM_instr_spec meta rewrite_def function iconst_fun let iconstf (n: int) : hl 'a - ensures { result <% (trivial_pre,iconst_post n) } - ensures { result.code.length = 1 /\ hl_correctness result } + ensures { result.pre --> trivial_pre } + ensures { result.post --> iconst_post n } + ensures { result.code.length --> 1 } = hoare trivial_pre ($ ifunf trivial_pre n.iconst n.iconst_fun) n.iconst_post (* Ivar spec *) @@ -53,8 +55,9 @@ module VM_instr_spec meta rewrite_def function ivar_fun let ivarf (x: id) : hl 'a - ensures { result <% (trivial_pre,ivar_post x) } - ensures { result.code.length = 1 /\ hl_correctness result } + ensures { result.pre --> trivial_pre } + ensures { result.post --> ivar_post x } + ensures { result.code.length --> 1 } = hoare trivial_pre ($ ifunf trivial_pre x.ivar x.ivar_fun) x.ivar_post (* Binary arithmetic operators specification (Iadd, Isub, Imul) @@ -81,8 +84,9 @@ module VM_instr_spec requires { forall c p. codeseq_at c p code_b -> forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m) (VMS (p+1) (push (op n1 n2) s) m) } - ensures { result <% (ibinop_pre,ibinop_post op) } - ensures { result.code.length = code_b.length /\ hl_correctness result } + ensures { result.pre --> ibinop_pre } + ensures { result.post --> ibinop_post op } + ensures { result.code.length --> code_b.length } = hoare ibinop_pre ($ ifunf ibinop_pre code_b op.ibinop_fun) op.ibinop_post constant plus : binop = fun x y -> x + y @@ -95,18 +99,21 @@ module VM_instr_spec meta rewrite_def function mul let iaddf () : hl 'a - ensures { result <% (ibinop_pre,ibinop_post plus) } - ensures { result.code.length = 1 /\ hl_correctness result } + ensures { result.pre --> ibinop_pre } + ensures { result.post --> ibinop_post plus } + ensures { result.code.length --> 1 } = create_binop iadd plus let isubf () : hl 'a - ensures { result <% (ibinop_pre,ibinop_post sub) } - ensures { result.code.length = 1 /\ hl_correctness result } + ensures { result.pre --> ibinop_pre } + ensures { result.post --> ibinop_post sub } + ensures { result.code.length --> 1 } = create_binop isub sub let imulf () : hl 'a - ensures { result <% (ibinop_pre,ibinop_post mul) } - ensures { result.code.length = 1 /\ hl_correctness result } + ensures { result.pre --> ibinop_pre } + ensures { result.post --> ibinop_post mul } + ensures { result.code.length --> 1 } = create_binop imul mul (* Inil spec *) @@ -115,8 +122,9 @@ module VM_instr_spec meta rewrite_def function inil_post let inil () : hl 'a - ensures { result <% (trivial_pre,inil_post) } - ensures { result.code.length = 0 /\ hl_correctness result } + ensures { result.pre --> trivial_pre } + ensures { result.post --> inil_post } + ensures { result.code.length --> 0 } = { pre = trivial_pre; code = Nil; post = inil_post } (* Ibranch specification *) @@ -129,8 +137,9 @@ module VM_instr_spec meta rewrite_def function ibranch_fun let ibranchf (ofs:ofs) : hl 'a - ensures { result <% (trivial_pre,ibranch_post ofs) } - ensures { result.code.length = 1 /\ hl_correctness result } + ensures { result.pre --> trivial_pre } + ensures { result.post --> ibranch_post ofs } + ensures { result.code.length --> 1 } = let cf = $ ifunf trivial_pre (ibranch ofs) (ibranch_fun ofs) in hoare trivial_pre cf (ibranch_post ofs) @@ -155,8 +164,9 @@ module VM_instr_spec requires { forall c p1 n1 n2 s m. codeseq_at c p1 code_cd -> let p2 = (if cond n1 n2 then p1 + ofs + 1 else p1 + 1) in transition c (VMS p1 (push n2 (push n1 s)) m) (VMS p2 s m) } - ensures { result <% (ibinop_pre,icjump_post cond ofs) } - ensures { result.code.length = code_cd.length /\ hl_correctness result } + ensures { result.pre --> ibinop_pre } + ensures { result.post --> icjump_post cond ofs } + ensures { result.code.length --> code_cd.length } = let c = $ ifunf ibinop_pre code_cd (icjump_fun cond ofs) in hoare ibinop_pre c (icjump_post cond ofs) @@ -174,23 +184,27 @@ module VM_instr_spec meta rewrite_def function bgt let ibeqf (ofs:ofs) : hl 'a - ensures { result <% (ibinop_pre,icjump_post beq ofs) } - ensures { result.code.length = 1 /\ hl_correctness result } + ensures { result.pre --> ibinop_pre } + ensures { result.post --> icjump_post beq ofs } + ensures { result.code.length --> 1 } = create_cjump (ibeq ofs) beq ofs let ibnef (ofs:ofs) : hl 'a - ensures { result <% (ibinop_pre,icjump_post bne ofs) } - ensures { result.code.length = 1 /\ hl_correctness result } + ensures { result.pre --> ibinop_pre } + ensures { result.post --> icjump_post bne ofs } + ensures { result.code.length --> 1 } = create_cjump (ibne ofs) bne ofs let iblef (ofs:ofs) : hl 'a - ensures { result <% (ibinop_pre,icjump_post ble ofs) } - ensures { result.code.length = 1 /\ hl_correctness result } + ensures { result.pre --> ibinop_pre } + ensures { result.post --> icjump_post ble ofs } + ensures { result.code.length --> 1 } = create_cjump (ible ofs) ble ofs let ibgtf (ofs:ofs) : hl 'a - ensures { result <% (ibinop_pre,icjump_post bgt ofs) } - ensures { result.code.length = 1 /\ hl_correctness result } + ensures { result.pre --> ibinop_pre } + ensures { result.post --> icjump_post bgt ofs } + ensures { result.code.length --> 1 } = create_cjump (ibgt ofs) bgt ofs (* Isetvar specification *) @@ -211,8 +225,9 @@ module VM_instr_spec meta rewrite_def function isetvar_fun let isetvarf (x: id) : hl 'a - ensures { result <% (isetvar_pre,isetvar_post x) } - ensures { result.code.length = 1 /\ hl_correctness result } + ensures { result.pre --> isetvar_pre } + ensures { result.post --> isetvar_post x } + ensures { result.code.length --> 1 } = let c = $ ifunf isetvar_pre (isetvar x) (isetvar_fun x) in hoare isetvar_pre c (isetvar_post x) diff --git a/examples/double_wp/specs/why3session.xml b/examples/double_wp/specs/why3session.xml index 29d833f2f359880ecea80b1e0f5c2a1463f5ad85..3ef5207627f216a011d52ea0289d5b3e77c576bd 100644 --- a/examples/double_wp/specs/why3session.xml +++ b/examples/double_wp/specs/why3session.xml @@ -5,68 +5,68 @@ - + - + + + + - - + + - - + + - - - - + + + + + + + - + - + - - + + - - + + - - - - + - + - + - - + + - - + + - - - - + @@ -84,19 +84,13 @@ - - - - - - - + - + - - + + @@ -104,11 +98,14 @@ - - + + + + + - - + + @@ -123,24 +120,19 @@ - - + + + + + + + + - - - - - - - - - - - - - + + @@ -149,27 +141,24 @@ - + - + - - + + - - + + - - - - + - + @@ -184,7 +173,7 @@ - + diff --git a/examples/double_wp/specs/why3shapes.gz b/examples/double_wp/specs/why3shapes.gz index 17fefa43dc0643da4f8574d7b91f82ec80b1e53f..c236391e11c2bd6e408e1e9c087d88bc5d77087e 100644 Binary files a/examples/double_wp/specs/why3shapes.gz and b/examples/double_wp/specs/why3shapes.gz differ diff --git a/examples/double_wp/state.why b/examples/double_wp/state.why index e3b3d7f9c80d848b8283b082fe06f6181ef51477..b3866fb5f4c570d8a694a8ab0d50c249102f7016 100644 --- a/examples/double_wp/state.why +++ b/examples/double_wp/state.why @@ -1,6 +1,6 @@ theory State - clone export map.Map + use export map.Map type id = Id int type state = map id int diff --git a/examples/double_wp/state/why3session.xml b/examples/double_wp/state/why3session.xml index 0ce89cecf9dc04951d80d58e0a042f080c8eb4a5..1a85ba367b5b7fbe7a6c45800076290c278f8e81 100644 --- a/examples/double_wp/state/why3session.xml +++ b/examples/double_wp/state/why3session.xml @@ -2,8 +2,8 @@ - - + + diff --git a/examples/double_wp/vm/why3session.xml b/examples/double_wp/vm/why3session.xml index 7f8ca70d7b5d9c4f66847ff944c6056f7499d3bd..43821cf93ada980b446e2dec9235a70315196724 100644 --- a/examples/double_wp/vm/why3session.xml +++ b/examples/double_wp/vm/why3session.xml @@ -28,7 +28,7 @@ - + diff --git a/examples/double_wp/vm/why3shapes.gz b/examples/double_wp/vm/why3shapes.gz index 8e094f252073e84830a7a704399cead937862fed..bf4b8b1ee3c8976ea2e8855ad06efb21ae9f5e26 100644 Binary files a/examples/double_wp/vm/why3shapes.gz and b/examples/double_wp/vm/why3shapes.gz differ diff --git a/examples/dyck/why3session.xml b/examples/dyck/why3session.xml index fc7c31885c03752e81590d48efc55fd68bb5a212..71b4450602ad5cef32c78b4f91cd1698ec08c972 100644 --- a/examples/dyck/why3session.xml +++ b/examples/dyck/why3session.xml @@ -2,17 +2,19 @@ - + + + - + @@ -48,11 +50,12 @@ - - - - - + + + + + + @@ -75,12 +78,9 @@ - + - - - diff --git a/examples/dyck/why3shapes.gz b/examples/dyck/why3shapes.gz index e90309da03cb98d85497558876c253b2ea87a965..b10af4cd60852b7299a4df8c35442dbfcba6daba 100644 Binary files a/examples/dyck/why3shapes.gz and b/examples/dyck/why3shapes.gz differ diff --git a/examples/euler002/why3session.xml b/examples/euler002/why3session.xml index 378976115edba2749f21368b8488c4d85222da73..1fd6597013fc68452dd91986a8339080ac9f2d68 100644 --- a/examples/euler002/why3session.xml +++ b/examples/euler002/why3session.xml @@ -394,7 +394,7 @@ - + @@ -444,7 +444,7 @@ - + diff --git a/examples/euler002/why3shapes.gz b/examples/euler002/why3shapes.gz index e5a9d670b722e3b9aad6a68d428f7244307192e7..b1f9d4a7419a2282692e2fc613ef5a18c97039d9 100644 Binary files a/examples/euler002/why3shapes.gz and b/examples/euler002/why3shapes.gz differ diff --git a/examples/fibonacci/why3session.xml b/examples/fibonacci/why3session.xml index 221953b7398ba6636e2f367f7b96647cce5f01c8..b0fa44e157ffb6968489a4a77104a16b569ca699 100644 --- a/examples/fibonacci/why3session.xml +++ b/examples/fibonacci/why3session.xml @@ -164,7 +164,7 @@ - + @@ -192,7 +192,7 @@ - + diff --git a/examples/fibonacci/why3shapes.gz b/examples/fibonacci/why3shapes.gz index 225d1874d879b3c29b13c2ef631d714db997c519..4708375242adc4bdc09a1d17f7f65a0c6aa190ca 100644 Binary files a/examples/fibonacci/why3shapes.gz and b/examples/fibonacci/why3shapes.gz differ diff --git a/examples/hackers-delight.mlw b/examples/hackers-delight.mlw index 7a41daa42b4b58ad7bd22c1729cfe0ac2e2c996b..c6b80950df99d570f2dc1e1e128657c7a30281ab 100644 --- a/examples/hackers-delight.mlw +++ b/examples/hackers-delight.mlw @@ -43,7 +43,6 @@ end *) module Utils_Spec - use BuiltIn use import int.Int use import int.NumOf use import bv.BV32 @@ -79,8 +78,7 @@ module Utils_Spec variant {bv with ult} ensures {t'int (count bv) = NumOf.numof (nth bv) 0 32} = - if BuiltIn.(=) bv zeros then () - else + if pure { bv <> zeros } then begin countSpec_Aux (lsr_bv bv one); assert { @@ -92,7 +90,7 @@ module Utils_Spec NumOf.numof f 0 32 - x = NumOf.numof f (0+1) 32 && NumOf.numof f (0+1) (31+1) = NumOf.numof h 0 31 && NumOf.numof g 0 (32-1) = NumOf.numof g 0 32 - } + } end (** With these lemmas, we can now prove the correctness property of diff --git a/examples/in_progress/bit_reversal.mlw b/examples/in_progress/bit_reversal.mlw index 4036f94a6a48757ed451716e0918b5d782d4f809..7bd8ebf67a2a8f7003a5a35a107be5ec60eec3d9 100644 --- a/examples/in_progress/bit_reversal.mlw +++ b/examples/in_progress/bit_reversal.mlw @@ -5,14 +5,15 @@ module BitReversal use import bv.BV32 use import array.Init + let swap (a:array 'a) (i j : t) - requires { 0 <= to_uint i < a.length } - requires { 0 <= to_uint j < a.length } + requires { 0 <= t'int i < a.length } + requires { 0 <= t'int j < a.length } writes { a } - ensures { a[to_uint i] = old a[to_uint j] } - ensures { a[to_uint j] = old a[to_uint i] } + ensures { a[t'int i] = old a[t'int j] } + ensures { a[t'int j] = old a[t'int i] } ensures { forall k. 0 <= k < a.length -> - k <> to_uint i /\ k <> to_uint j -> a[k] = (old a)[k] } + k <> t'int i /\ k <> t'int j -> a[k] = (old a)[k] } = let tmp = a[to_uint i] in a[to_uint i] <- a[to_uint j]; @@ -24,21 +25,21 @@ module BitReversal (ghost loglen masklen logdi loghi:t) requires { ult loglen (of_int 32) } requires { masklen = lsl_bv ones loglen } - requires { a.length = to_uint (lsl_bv (of_int 1) loglen) } + requires { a.length = t'int (lsl_bv (of_int 1) loglen) } requires { ult logdi (of_int 32) && di = lsl_bv (of_int 1) logdi } requires { ult loghi (of_int 32) && hi = lsl_bv (of_int 1) loghi } - requires { to_uint logdi + to_uint loghi = to_uint loglen } - requires { to_uint i < a.length } - requires { to_uint di <= a.length } - requires { to_uint h < a.length } + requires { t'int logdi + t'int loghi = t'int loglen } + requires { t'int i < a.length } + requires { t'int di <= a.length } + requires { t'int h < a.length } requires { di <> of_int 0 } writes { a } - variant { to_uint di } + variant { t'int di } = if eq di (of_int 1) then (if ult i h then swap a i h) else let dj = lsr_bv di (of_int 1) in let hj = lsl_bv hi (of_int 1) in - assert { to_uint logdi >= 1 }; + assert { t'int logdi >= 1 }; assert { ule dj (lsl_bv (of_int 1) (BV32.sub logdi (of_int 1))) }; assert { bw_and dj masklen = zeros }; assert { ult i (lsl_bv (of_int 1) loglen) }; @@ -51,7 +52,7 @@ module BitReversal (BV32.sub logdi (of_int 1)) (BV32.add loghi (of_int 1)) let bit_rev (a:array t) (ghost loglen:t) - requires { ult loglen (of_int 32) && a.length = to_uint (lsl_bv (of_int 1) loglen) } + requires { ult loglen (of_int 32) && a.length = t'int (lsl_bv (of_int 1) loglen) } = aux a (of_int 0) (of_int a.length) (of_int 0) (of_int 1) loglen (lsl_bv ones loglen) loglen (of_int 0) diff --git a/examples/maximum_subarray.mlw b/examples/maximum_subarray.mlw index 7f4ac65f6570fb384950b3aa8423d7938865a05e..36c9cac3971d41090768d20d35596f198d3e15ac 100644 --- a/examples/maximum_subarray.mlw +++ b/examples/maximum_subarray.mlw @@ -236,3 +236,49 @@ module Algo5 !maxsum end + +(* Kadane's algorithm with 63-bit integers + + Interestingly, we only have to require all sums to be no greater + than max_int. There is no need to require the sums to be no + smaller than min_int, since whenever the sum becomes negative it is + replaced by the next element. *) + +module BoundedIntegers + + use import int.Int + use import mach.int.Int63 + use import mach.int.Refint63 + use import mach.array.Array63 + use int.Sum + + function sum (a: array int63) (lo hi: int) : int = + Sum.sum (fun i -> (a[i] : int)) lo hi + + let maximum_subarray (a: array int63) (ghost lo hi: ref int): int63 + requires { "no overflow" forall l h. 0 <= l <= h <= length a -> + sum a l h <= max_int } + ensures { 0 <= !lo <= !hi <= length a && result = sum a !lo !hi } + ensures { forall l h. 0 <= l <= h <= length a -> result >= sum a !lo !hi } + = lo := 0; + hi := 0; + let n = length a in + let ms = ref zero in + let ghost l = ref 0 in + let s = ref zero in + let i = ref zero in + while !i < n do + invariant { 0 <= !lo <= !hi <= !i <= n && 0 <= !ms = sum a !lo !hi } + invariant { forall l' h': int. 0 <= l' <= h' <= !i -> sum a l' h' <= !ms } + invariant { 0 <= !l <= !i && !s = sum a !l !i } + invariant { forall l': int. 0 <= l' < !i -> sum a l' !i <= !s } + variant { n - !i } + if !s < zero then begin s := a[!i]; l := to_int !i end + else begin assert { sum a !l (!i + 1) <= max_int }; s += a[!i] end; + if !s > !ms then begin + ms := !s; lo := !l; hi := to_int !i + 1 end; + incr i + done; + !ms + +end diff --git a/examples/maximum_subarray/why3session.xml b/examples/maximum_subarray/why3session.xml index 6767c16501b3d55acf2ed9dbb785fb9dc66d5bdc..24b6d705e606ca072e9e81fce4d45f15b94c4db0 100644 --- a/examples/maximum_subarray/why3session.xml +++ b/examples/maximum_subarray/why3session.xml @@ -4,8 +4,9 @@ + - + @@ -17,9 +18,9 @@ - - - + + + @@ -86,9 +87,9 @@ - - - + + + @@ -99,9 +100,9 @@ - - - + + + @@ -159,7 +160,7 @@ - + @@ -173,5 +174,114 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/maximum_subarray/why3shapes.gz b/examples/maximum_subarray/why3shapes.gz index 58f70e74474e3d82571ab364843fce3d65905403..ffe4c63fda9ce49db0f25f52b400bf0ced262600 100644 Binary files a/examples/maximum_subarray/why3shapes.gz and b/examples/maximum_subarray/why3shapes.gz differ diff --git a/examples/mccarthy_vc_sp/why3session.xml b/examples/mccarthy_vc_sp/why3session.xml index 3d9dfe5866b20296e30ba7f39803c24a21147ec2..1d10aee854bb83c6347ac8981e6f1dfc1ccd68b0 100644 --- a/examples/mccarthy_vc_sp/why3session.xml +++ b/examples/mccarthy_vc_sp/why3session.xml @@ -2,38 +2,47 @@ - + - + - + - + - + - + - - + + - - + + - - + + + + + + + + + + + diff --git a/examples/mccarthy_vc_sp/why3shapes.gz b/examples/mccarthy_vc_sp/why3shapes.gz index f99e0f8db752b7d7b9787a955f17b992065f9181..434115a08b0066aaa3a57cd2999ef521209e88bf 100644 Binary files a/examples/mccarthy_vc_sp/why3shapes.gz and b/examples/mccarthy_vc_sp/why3shapes.gz differ diff --git a/examples/mergesort_array.mlw b/examples/mergesort_array.mlw index 56e7385f9848c2166835732734396eb88d991e24..89aaf9a0f19b159cb871f82202146cc687ca8e52 100644 --- a/examples/mergesort_array.mlw +++ b/examples/mergesort_array.mlw @@ -102,16 +102,15 @@ module TopDownMergesort ensures { sorted_sub a l r } ensures { permut_sub (old a) a l r } variant { r - l } - = if l < r-1 then begin - let m = l + (r - l) / 2 in - assert { l <= m < r }; - mergesort_rec a tmp l m; - assert { permut_sub (old a) a l r }; - label M in - mergesort_rec a tmp m r; - assert { permut_sub (a at M) a l r }; - merge_using tmp a l m r; - end + = if l >= r-1 then return; + let m = l + (r - l) / 2 in + assert { l <= m < r }; + mergesort_rec a tmp l m; + assert { permut_sub (old a) a l r }; + label M in + mergesort_rec a tmp m r; + assert { permut_sub (a at M) a l r }; + merge_using tmp a l m r let mergesort (a: array elt) : unit ensures { sorted a } @@ -228,24 +227,19 @@ module NaturalMergesort done; !i - exception Break - exception Return - let natural_mergesort (a: array elt) : unit ensures { sorted a } ensures { permut_all (old a) a } = let n = length a in - if n >= 2 then + if n <= 1 then return; let tmp = Array.copy a in let ghost first_run = ref 0 in - try while true do invariant { 0 <= !first_run <= n && sorted_sub a 0 !first_run } invariant { permut_all (old a) a } variant { n - !first_run } label L in let lo = ref 0 in - try while !lo < n - 1 do invariant { 0 <= !lo <= n } invariant { !first_run at L <= !first_run <= n } @@ -254,7 +248,7 @@ module NaturalMergesort invariant { permut_all (a at L) a } variant { n - !lo } let mid = find_run a !lo in - if mid = n then begin if !lo = 0 then raise Return; raise Break end; + if mid = n then begin if !lo = 0 then return; raise L end; let hi = find_run a mid in label M in merge_using tmp a !lo mid hi; @@ -263,9 +257,7 @@ module NaturalMergesort ghost if !lo = 0 then first_run := hi; lo := hi; done - with Break -> () end done - with Return -> () end (** an alternative implementation suggested by Martin Clochard, @@ -283,26 +275,24 @@ module NaturalMergesort ensures { forall j: int. 0 <= j < lo -> a[j] = (old a)[j] } variant { k } = let n = length a in - if lo >= n-1 then n else - try - let mid = ref (find_run a lo) in - if !mid = n then raise Break; - for i = 0 to k-1 do - invariant { lo + i < !mid < n } - invariant { sorted_sub a lo !mid } - invariant { permut_sub (old a) a lo (length a) } - invariant { forall j: int. 0 <= j < lo -> a[j] = (old a)[j] } - let hi = naturalrec tmp a !mid i in - assert { permut_sub (old a) a lo (length a) }; - label M in - merge_using tmp a lo !mid hi; - assert { permut_sub (a at M) a lo hi }; - assert { permut_sub (a at M) a lo (length a) }; - mid := hi; - if !mid = n then raise Break - done; - !mid - with Break -> n end + if lo >= n-1 then return n; + let mid = ref (find_run a lo) in + if !mid = n then return n; + for i = 0 to k-1 do + invariant { lo + i < !mid < n } + invariant { sorted_sub a lo !mid } + invariant { permut_sub (old a) a lo (length a) } + invariant { forall j: int. 0 <= j < lo -> a[j] = (old a)[j] } + let hi = naturalrec tmp a !mid i in + assert { permut_sub (old a) a lo (length a) }; + label M in + merge_using tmp a lo !mid hi; + assert { permut_sub (a at M) a lo hi }; + assert { permut_sub (a at M) a lo (length a) }; + mid := hi; + if !mid = n then return n + done; + !mid let natural_mergesort2 (a: array elt) : unit ensures { sorted a } @@ -312,4 +302,4 @@ module NaturalMergesort let _ = naturalrec tmp a 0 (length a) in () -end \ No newline at end of file +end diff --git a/examples/mergesort_array/why3session.xml b/examples/mergesort_array/why3session.xml index a6004ca3dcd5716f010bc720076ea5c06b7bab85..1f94dba716485d33e800c89985d4fb2652442261 100644 --- a/examples/mergesort_array/why3session.xml +++ b/examples/mergesort_array/why3session.xml @@ -3,129 +3,129 @@ "http://why3.lri.fr/why3session.dtd"> - + - + - + - - + + - + - + - + - + - + - - - + + + - + - + - - + + - + - + - + - + - + - - - + + + - + - - + + - + - + - + - + - + - + - - + + - - - - + - + - + - - + + - - + + - + - - + + - - + + + + + @@ -141,10 +141,10 @@ - + - + @@ -153,21 +153,21 @@ - + - + - + - + @@ -178,13 +178,13 @@ - + - + @@ -192,7 +192,7 @@ - + @@ -200,29 +200,29 @@ - - - + + + - + - + - + - + - + @@ -237,10 +237,10 @@ - + - + @@ -248,7 +248,7 @@ - + @@ -290,13 +290,13 @@ - + - + - + @@ -308,10 +308,10 @@ - + - - + + @@ -320,141 +320,141 @@ - + - + - - + + - - + + - + - + - + - + - + + + + + + + - + - + - - + + - + - + - - + + - + - + - - + + - - + + - + - + - + - - + + - - + + - + - - - - - - - + - + - + - - + + - + - + - + - + - + - - + + - + - - + + - - + + - - + + - + - + @@ -467,7 +467,7 @@ - + @@ -482,92 +482,92 @@ - + - - + + - + - + - - - - - + + - - + + - - + + - + - - + + + + + - + - + - - + + - + - - + + - + - + - + - - + + - + - + - + - - + + - + - + - + - - + + diff --git a/examples/mergesort_array/why3shapes.gz b/examples/mergesort_array/why3shapes.gz index db43c9b04d9cac57f04f7e2371fc174223983142..4eab24b1ef46b5fe8b901ead530e1155495175d6 100644 Binary files a/examples/mergesort_array/why3shapes.gz and b/examples/mergesort_array/why3shapes.gz differ diff --git a/examples/mjrty.mlw b/examples/mjrty.mlw index d7265c5867eeb4c046f14f3a70046b433bf6d04c..462e498a6727598936701a04987c1769f0b46ce6 100644 --- a/examples/mjrty.mlw +++ b/examples/mjrty.mlw @@ -16,8 +16,7 @@ - arrays are 0-based - we assume the input array to have at least one element - we use 2x <= y instead of x <= floor(y/2), which is equivalent - - we do not consider arithmetic overflows (easy, but requires the - extra hypothesis length a <= max_int) + *) module Mjrty @@ -28,48 +27,41 @@ module Mjrty use import array.NumOfEq exception Not_found - exception Found type candidate - val eq (x y: candidate) : bool + val (=) (x y: candidate) : bool ensures { result <-> x = y } - (* FIXME: call it (=) when we have overloading *) let mjrty (a: array candidate) : candidate requires { 1 <= length a } ensures { 2 * numof a result 0 (length a) > length a } - raises { Not_found -> - forall c: candidate. 2 * numof a c 0 (length a) <= length a } + raises { Not_found -> forall c. 2 * numof a c 0 (length a) <= length a } = let n = length a in let cand = ref a[0] in let k = ref 0 in - for i = 0 to n-1 do (* could start at 1 with k initialized to 1 *) + for i = 0 to n - 1 do (* could start at 1 with k initialized to 1 *) invariant { 0 <= !k <= numof a !cand 0 i } - invariant {2 * (numof a !cand 0 i - !k) <= i - !k } - invariant {forall c:candidate. c <> !cand -> 2 * numof a c 0 i <= i - !k } + invariant { 2 * (numof a !cand 0 i - !k) <= i - !k } + invariant { forall c. c <> !cand -> 2 * numof a c 0 i <= i - !k } if !k = 0 then begin cand := a[i]; k := 1 - end else if eq !cand a[i] then + end else if !cand = a[i] then incr k else decr k done; if !k = 0 then raise Not_found; - try - if 2 * !k > n then raise Found; - k := 0; - for i = 0 to n-1 do - invariant { !k = numof a !cand 0 i /\ 2 * !k <= n } - if eq a[i] !cand then begin - incr k; - if 2 * !k > n then raise Found - end - done; - raise Not_found - with Found -> - !cand - end + if 2 * !k > n then return !cand; + k := 0; + for i = 0 to n - 1 do + invariant { !k = numof a !cand 0 i /\ 2 * !k <= n } + if a[i] = !cand then begin + incr k; + if 2 * !k > n then return !cand + end + done; + raise Not_found end diff --git a/examples/patience.mlw b/examples/patience.mlw index fb13300a3b6f6da075a2561b4002a2cfc880a682..200a3b8f4a4ba635b751602b29a8e7099532745b 100644 --- a/examples/patience.mlw +++ b/examples/patience.mlw @@ -85,30 +85,26 @@ module PigeonHole requires { n > m >= 0 } variant { m } ensures { not (injective f n m) } - = try + = for i = 0 to n-1 do invariant { forall k. 0 <= k < i -> f k <> m-1 } - if f i = m-1 then - begin + if f i = m-1 then begin (* we have found index i such that f i = m-1 *) for j = i+1 to n-1 do invariant { forall k. i < k < j -> f k <> m-1 } - if f j = m-1 then raise Found + (* we know that f i = f j = m-1 hence we are done *) + if f j = m-1 then return done; (* we know that for all k <> i, f k <> m-1 *) let g = shift f i in assert { range g (n-1) (m-1) }; pigeon_hole (n-1) (m-1) g; - raise Found; - end + return + end done; (* we know that for all k, f k <> m-1 *) assert { range f n (m-1) }; pigeon_hole n (m-1) f - with Found -> - (* we know that f i = f j = m-1 hence we are done *) - () - end end @@ -328,7 +324,7 @@ module PatienceAbstract ensures { s.values = (old s).values[(old s).num_elts <- c] } = let ghost pred = ref (-1) in - try + try for i = 0 to s.num_stacks - 1 do invariant { if i=0 then !pred = -1 else let stack_im1 = s.stacks[i-1] in @@ -343,19 +339,15 @@ module PatienceAbstract let stack_i = s.stacks[i] in let stack_i_size = s.stack_sizes[i] in let top_stack_i = stack_i[stack_i_size - 1] in - if c <= s.values[top_stack_i] then - raise (Return i) - else - begin - assert { 0 <= top_stack_i < s.num_elts }; - assert { let (is,ip) = s.positions[top_stack_i] in - 0 <= is < s.num_stacks && - 0 <= ip < s.stack_sizes[is] && - s.stacks[is][ip] = top_stack_i && - is = i /\ ip = stack_i_size - 1 - }; - pred := top_stack_i - end + if c <= s.values[top_stack_i] then raise (Return i); + assert { 0 <= top_stack_i < s.num_elts }; + assert { let (is,ip) = s.positions[top_stack_i] in + 0 <= is < s.num_stacks && + 0 <= ip < s.stack_sizes[is] && + s.stacks[is][ip] = top_stack_i && + is = i /\ ip = stack_i_size - 1 + }; + pred := top_stack_i done; (* we add a new stack *) let idx = s.num_elts in diff --git a/examples/pigeonhole.mlw b/examples/pigeonhole.mlw index 4b771545c327f9122be8256b8a3eec7c483bf263..a56a8d3cddf88bc95f160219e7fefab71d4f5c81 100644 --- a/examples/pigeonhole.mlw +++ b/examples/pigeonhole.mlw @@ -9,8 +9,6 @@ module Pigeonhole use import set.Fset use import ref.Ref - exception Exit - let rec below (n: int) : set int requires { 0 <= n } ensures { forall i. mem i result <-> 0 <= i < n } @@ -24,15 +22,13 @@ module Pigeonhole ensures { exists i1, i2. 0 <= i1 < i2 < n /\ f i1 = f i2 } = let s = ref empty in - try for i = 0 to n-1 do invariant { cardinal !s = i } invariant { forall x. mem x !s <-> (exists j. 0 <= j < i /\ x = f j) } - if mem (f i) !s then raise Exit; + if mem (f i) !s then return; s := add (f i) !s done; let b = below m in assert { subset !s b }; absurd - with Exit -> () end end diff --git a/examples/power/why3session.xml b/examples/power/why3session.xml index 12ea68d445159a3fea0af34b708afe5b4ab7a2bb..031c1d550fecf781157078815bf98c10b3e7206b 100644 --- a/examples/power/why3session.xml +++ b/examples/power/why3session.xml @@ -2,9 +2,10 @@ + - + @@ -20,7 +21,7 @@ - + @@ -32,7 +33,7 @@ - + diff --git a/examples/power/why3shapes.gz b/examples/power/why3shapes.gz index 1536a47ab888efaac46cb950fca4969611e3ed7f..3ec5517fa9dbe6fb2739285348ec31df76b98794 100644 Binary files a/examples/power/why3shapes.gz and b/examples/power/why3shapes.gz differ diff --git a/examples/sum_of_digits/why3session.xml b/examples/sum_of_digits/why3session.xml index 8007c75453773c8968f5e0d956edc4447890b79c..ed6270329997acfacf82a05017aff9db024a993e 100644 --- a/examples/sum_of_digits/why3session.xml +++ b/examples/sum_of_digits/why3session.xml @@ -8,7 +8,7 @@ - + @@ -32,7 +32,7 @@ - + diff --git a/examples/sum_of_digits/why3shapes.gz b/examples/sum_of_digits/why3shapes.gz index 72437a60029d300725988da65de550fde5fc7634..41624151d073e41d520fecacffcd6106ee3c7c55 100644 Binary files a/examples/sum_of_digits/why3shapes.gz and b/examples/sum_of_digits/why3shapes.gz differ diff --git a/examples/tests-provers/coq-interval/why3session.xml b/examples/tests-provers/coq-interval/why3session.xml index ced293b89bc60a95bc0dd693471a9fcea963baa1..d114d0a268be853599c9285c38251ae3679bd623 100644 --- a/examples/tests-provers/coq-interval/why3session.xml +++ b/examples/tests-provers/coq-interval/why3session.xml @@ -4,7 +4,7 @@ - + diff --git a/examples/tests-provers/coq-interval/why3shapes.gz b/examples/tests-provers/coq-interval/why3shapes.gz index a1f8b57d3b191b68eb4081d773b6ab060f00b61f..c835a92af5948e7d3d911bf5f39bb8944ba98acd 100644 Binary files a/examples/tests-provers/coq-interval/why3shapes.gz and b/examples/tests-provers/coq-interval/why3shapes.gz differ diff --git a/examples/toy_compiler/why3session.xml b/examples/toy_compiler/why3session.xml index 9e154327fc16ed098b0c8d32e919e9d801dd1b0c..ed94a229c1d52ba62fdf7d202f8843e9372cfb2f 100644 --- a/examples/toy_compiler/why3session.xml +++ b/examples/toy_compiler/why3session.xml @@ -2,14 +2,15 @@ + - + - + @@ -33,17 +34,21 @@ - - - - - - - - - - - + + + + + + + + + + + + + + + diff --git a/examples/toy_compiler/why3shapes.gz b/examples/toy_compiler/why3shapes.gz index abe78117ed1d8cc4640325fe741ca3e05e2946eb..556aefa759f6c82fb8a4d82567fd71a5a92df487 100644 Binary files a/examples/toy_compiler/why3shapes.gz and b/examples/toy_compiler/why3shapes.gz differ diff --git a/examples/tree_of_array/why3session.xml b/examples/tree_of_array/why3session.xml index 7088256aed554d7cd125035fe8c5e50a438a72ef..a1490fb7a2d84a936c35d6e26c882ac1b147c5c3 100644 --- a/examples/tree_of_array/why3session.xml +++ b/examples/tree_of_array/why3session.xml @@ -4,9 +4,9 @@ - + - + diff --git a/examples/tree_of_array/why3shapes.gz b/examples/tree_of_array/why3shapes.gz index 7cb01d2e65812ecd77a303497fa664e33cbfbc89..74cc1fa99bec2adb05ed5ba04776827ec2003dad 100644 Binary files a/examples/tree_of_array/why3shapes.gz and b/examples/tree_of_array/why3shapes.gz differ diff --git a/examples/tree_of_list/why3session.xml b/examples/tree_of_list/why3session.xml index c18f8637cefe77205b283ac2201965edbdabebd8..ea2d9b0c786bd6dab4bfd1e29288cba79f5f02ae 100644 --- a/examples/tree_of_list/why3session.xml +++ b/examples/tree_of_list/why3session.xml @@ -4,9 +4,9 @@ - + - + diff --git a/examples/tree_of_list/why3shapes.gz b/examples/tree_of_list/why3shapes.gz index 7867d85fa5c85c5e26c96adf7f8bb2a82012a7ed..59ec5aa3783968b036ac738c58794cc82da7ef47 100644 Binary files a/examples/tree_of_list/why3shapes.gz and b/examples/tree_of_list/why3shapes.gz differ diff --git a/examples/vacid_0_build_maze/why3session.xml b/examples/vacid_0_build_maze/why3session.xml index 2c6fdb2240c735ebf10358a76a7255097bbf7ea4..4f84a978e2eb39066eb5093548228e363d59a1fc 100644 --- a/examples/vacid_0_build_maze/why3session.xml +++ b/examples/vacid_0_build_maze/why3session.xml @@ -346,7 +346,7 @@ - + diff --git a/examples/vacid_0_sparse_array/why3session.xml b/examples/vacid_0_sparse_array/why3session.xml index 657963d1c9c8a4509af1c22ca689016d16f98e8a..31a2ea1e5388f9889fb1d2e75b45cce0b51e7d3d 100644 --- a/examples/vacid_0_sparse_array/why3session.xml +++ b/examples/vacid_0_sparse_array/why3session.xml @@ -78,7 +78,7 @@ - + diff --git a/examples/verifythis_fm2012_treedel.mlw b/examples/verifythis_fm2012_treedel.mlw index d0b4df69323505e33f4229bb0186a799ccca4638..6a71b86daa97cd278370c010e6ad33189143c773 100644 --- a/examples/verifythis_fm2012_treedel.mlw +++ b/examples/verifythis_fm2012_treedel.mlw @@ -105,10 +105,11 @@ module Treedel | Top | Left (zipper 'a) 'a (tree 'a) - function zip (t: tree 'a) (z: zipper 'a) : tree 'a = match z with + let rec function zip (t: tree 'a) (z: zipper 'a) : tree 'a + = match z with | Top -> t | Left z x r -> zip (Node t x r) z - end + end lemma inorder_zip: forall z "induction": zipper 'a, x: 'a, l r: tree 'a. diff --git a/examples/vstte12_tree_reconstruction.mlw b/examples/vstte12_tree_reconstruction.mlw index 043a6bcf9656971985b75c7e12778107a30dacc1..729a06e41b7493cdbb3273fcbb389e271a2ebd12 100644 --- a/examples/vstte12_tree_reconstruction.mlw +++ b/examples/vstte12_tree_reconstruction.mlw @@ -18,10 +18,11 @@ module Tree type tree = Leaf | Node tree tree (* the list of leaf depths for tree t, if root is at depth d *) - function depths (d: int) (t: tree) : list int = match t with + let rec function depths (d: int) (t: tree) : list int = + match t with | Leaf -> Cons d Nil | Node l r -> depths (d+1) l ++ depths (d+1) r - end + end (* lemmas on depths *) diff --git a/examples/vstte12_two_way_sort/why3session.xml b/examples/vstte12_two_way_sort/why3session.xml index 3ee6715c542cef377519d79366986e6e1f513466..4fee880798ce77dd736db843a46f5f7bdf4b93a4 100644 --- a/examples/vstte12_two_way_sort/why3session.xml +++ b/examples/vstte12_two_way_sort/why3session.xml @@ -4,9 +4,9 @@ - + - + diff --git a/examples/vstte12_two_way_sort/why3shapes.gz b/examples/vstte12_two_way_sort/why3shapes.gz index 9d351d16fc6e0a020ee6b1b3777961f89ffabc28..74650e212050bebcb6368cdde0e8e0d7dcb61e1c 100644 Binary files a/examples/vstte12_two_way_sort/why3shapes.gz and b/examples/vstte12_two_way_sort/why3shapes.gz differ diff --git a/examples/zeros/why3session.xml b/examples/zeros/why3session.xml index 9542391ea43b3fc17092a263f87efc2f57360526..b9b3a30340257a8377812faf813ad56236a3e108 100644 --- a/examples/zeros/why3session.xml +++ b/examples/zeros/why3session.xml @@ -4,17 +4,17 @@ - + - + - + - + diff --git a/examples/zeros/why3shapes.gz b/examples/zeros/why3shapes.gz index fb757eb5d9cfa3b4f1adc5636e39e9ac4ca9ab6a..0e60b17d0dd3030559fe32bdd137a1b9424428d0 100644 Binary files a/examples/zeros/why3shapes.gz and b/examples/zeros/why3shapes.gz differ diff --git a/lib/coq/int/Exponentiation.v b/lib/coq/int/Exponentiation.v index e70511e29863542e35c703c87002931248ab79d5..3f9e14cc31385c1877b7f2f43a34d0c4f79402f2 100644 --- a/lib/coq/int/Exponentiation.v +++ b/lib/coq/int/Exponentiation.v @@ -38,9 +38,6 @@ Hypothesis Unit_def_l : forall (x:t), ((infix_as one x) = x). (* Why3 goal *) Hypothesis Unit_def_r : forall (x:t), ((infix_as x one) = x). -(* Why3 goal *) -Hypothesis Comm : forall (x:t) (y:t), ((infix_as x y) = (infix_as y x)). - (* Why3 goal *) Definition power: t -> Z -> t. intros x n. @@ -66,6 +63,7 @@ Qed. (* Why3 goal *) Lemma Power_s_alt : forall (x:t) (n:Z), (0%Z < n)%Z -> ((power x n) = (infix_as x (power x (n - 1%Z)%Z))). +Proof. intros x n h1. rewrite <- Power_s; auto with zarith. f_equal; omega. @@ -109,19 +107,40 @@ now rewrite Power_1. Qed. (* Why3 goal *) -Lemma Power_mult2 : forall (x:t) (y:t) (n:Z), (0%Z <= n)%Z -> - ((power (infix_as x y) n) = (infix_as (power x n) (power y n))). +Lemma Power_comm1 : forall (x:t) (y:t), ((infix_as x y) = (infix_as y x)) -> + forall (n:Z), (0%Z <= n)%Z -> ((infix_as (power x n) y) = (infix_as y + (power x n))). +Proof. +intros x y comm. +apply natlike_ind. +now rewrite Power_0, Unit_def_r, Unit_def_l. +intros n Hn IHn. +unfold Zsucc. +rewrite (Power_s _ _ Hn). +rewrite Assoc. +rewrite IHn. +rewrite <- Assoc. +rewrite <- Assoc. +now rewrite comm. +Qed. + +(* Why3 goal *) +Lemma Power_comm2 : forall (x:t) (y:t), ((infix_as x y) = (infix_as y x)) -> + forall (n:Z), (0%Z <= n)%Z -> ((power (infix_as x y) + n) = (infix_as (power x n) (power y n))). Proof. -intros x y. +intros x y comm. apply natlike_ind. -apply sym_eq. rewrite 3!Power_0. -apply Unit_def_r. +now rewrite Unit_def_r. intros n Hn IHn. unfold Zsucc. rewrite 3!(Power_s _ _ Hn). rewrite IHn. -now rewrite Assoc, <- (Assoc y), (Comm y), 2!Assoc. +rewrite <- Assoc. +rewrite (Assoc x). +rewrite <- (Power_comm1 _ _ comm _ Hn). +now rewrite <- 2!Assoc. Qed. End Exponentiation. diff --git a/lib/coq/int/Power.v b/lib/coq/int/Power.v index 11f2185fa86642786a3fffb9fa986a41a8121545..65ef76c2f4f680da0136d9609e90f6bfbf78d87b 100644 --- a/lib/coq/int/Power.v +++ b/lib/coq/int/Power.v @@ -82,12 +82,21 @@ apply Power_mult ; auto with zarith. Qed. (* Why3 goal *) -Lemma Power_mult2 : forall (x:Z) (y:Z) (n:Z), (0%Z <= n)%Z -> - ((power (x * y)%Z n) = ((power x n) * (power y n))%Z). +Lemma Power_comm1 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z) -> + forall (n:Z), (0%Z <= n)%Z -> (((power x n) * y)%Z = (y * (power x n))%Z). Proof. -intros x y n Hn. +intros x y h1 n h2. +auto with zarith. +Qed. + +(* Why3 goal *) +Lemma Power_comm2 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z) -> + forall (n:Z), (0%Z <= n)%Z -> ((power (x * y)%Z n) = ((power x + n) * (power y n))%Z). +Proof. +intros x y h1 n h2. rewrite 3!power_is_exponentiation ; auto with zarith. -apply Power_mult2 ; auto with zarith. +apply Power_comm2 ; auto with zarith. Qed. (* Why3 goal *) diff --git a/lib/coq/real/PowerInt.v b/lib/coq/real/PowerInt.v index c9c9a85e6961e8c417c79941b163adbfe8bc8bd2..cbe145e75b23e5a95f51466102869a81ab2ec2a4 100644 --- a/lib/coq/real/PowerInt.v +++ b/lib/coq/real/PowerInt.v @@ -88,12 +88,21 @@ apply Power_mult ; auto with real. Qed. (* Why3 goal *) -Lemma Power_mult2 : forall (x:R) (y:R) (n:Z), (0%Z <= n)%Z -> +Lemma Power_comm1 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R) -> + forall (n:Z), (0%Z <= n)%Z -> + (((Reals.Rfunctions.powerRZ x n) * y)%R = (y * (Reals.Rfunctions.powerRZ x n))%R). +intros x y h1 n h2. +apply Rmult_comm. +Qed. + +(* Why3 goal *) +Lemma Power_comm2 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R) -> + forall (n:Z), (0%Z <= n)%Z -> ((Reals.Rfunctions.powerRZ (x * y)%R n) = ((Reals.Rfunctions.powerRZ x n) * (Reals.Rfunctions.powerRZ y n))%R). Proof. -intros x y n h1. +intros x y h1 n h2. rewrite 3!power_is_exponentiation by auto with zarith. -apply Power_mult2 ; auto with real. +apply Power_comm2 ; auto with real. Qed. (* Why3 goal *) diff --git a/modules/mach/array.mlw b/modules/mach/array.mlw index 7ca74d1dc5cb2de0957bc5f42798d78b032c6177..faa4c6f8fa124402999bc8c3d5e95fbbab1eeeeb 100644 --- a/modules/mach/array.mlw +++ b/modules/mach/array.mlw @@ -15,91 +15,91 @@ module Array32 type array 'a = private { mutable ghost elts : int -> 'a; length : int32; - } invariant { 0 <= to_int length } + } invariant { 0 <= length } function ([]) (a: array 'a) (i: int) : 'a = a.elts i val ([]) (a: array 'a) (i: int32) : 'a - requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length } - ensures { result = a[to_int i] } + requires { "expl:index in array bounds" 0 <= i < a.length } + ensures { result = a[i] } val ([]<-) (a: array 'a) (i: int32) (v: 'a) : unit writes {a} - requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length } - ensures { a.elts = (old a.elts)[to_int i <- v] } + requires { "expl:index in array bounds" 0 <= i < a.length } + ensures { a.elts = (old a.elts)[i <- v] } (** unsafe get/set operations with no precondition *) exception OutOfBounds let defensive_get (a: array 'a) (i: int32) - ensures { 0 <= to_int i < to_int a.length } - ensures { result = a[to_int i] } - raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length } + ensures { 0 <= i < a.length } + ensures { result = a[i] } + raises { OutOfBounds -> i < 0 \/ i >= a.length } = if i < of_int 0 || i >= length a then raise OutOfBounds; a[i] let defensive_set (a: array 'a) (i: int32) (v: 'a) - ensures { 0 <= to_int i < to_int a.length } - ensures { a.elts = (old a.elts)[to_int i <- v] } - raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length } + ensures { 0 <= i < a.length } + ensures { a.elts = (old a.elts)[i <- v] } + raises { OutOfBounds -> i < 0 \/ i >= a.length } = if i < of_int 0 || i >= length a then raise OutOfBounds; a[i] <- v val make (n: int32) (v: 'a) : array 'a - requires { "expl:array creation size" to_int n >= 0 } - ensures { forall i:int. 0 <= i < to_int n -> result[i] = v } + requires { "expl:array creation size" n >= 0 } + ensures { forall i:int. 0 <= i < n -> result[i] = v } ensures { result.length = n } val append (a1: array 'a) (a2: array 'a) : array 'a - ensures { to_int result.length = to_int a1.length + to_int a2.length } - ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] } - ensures { forall i:int. 0 <= i < to_int a2.length -> - result[to_int a1.length + i] = a2[i] } + ensures { result.length = a1.length + a2.length } + ensures { forall i:int. 0 <= i < a1.length -> result[i] = a1[i] } + ensures { forall i:int. 0 <= i < a2.length -> + result[a1.length + i] = a2[i] } val sub (a: array 'a) (ofs: int32) (len: int32) : array 'a - requires { 0 <= to_int ofs /\ 0 <= to_int len } - requires { to_int ofs + to_int len <= to_int a.length } + requires { 0 <= ofs /\ 0 <= len } + requires { ofs + len <= a.length } ensures { result.length = len } - ensures { forall i:int. 0 <= i < to_int len -> - result[i] = a[to_int ofs + i] } + ensures { forall i:int. 0 <= i < len -> + result[i] = a[ofs + i] } val copy (a: array 'a) : array 'a ensures { result.length = a.length } - ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] } + ensures { forall i:int. 0 <= i < result.length -> result[i] = a[i] } val fill (a: array 'a) (ofs: int32) (len: int32) (v: 'a) : unit writes {a} - requires { 0 <= to_int ofs /\ 0 <= to_int len } - requires { to_int ofs + to_int len <= to_int a.length } + requires { 0 <= ofs /\ 0 <= len } + requires { ofs + len <= a.length } ensures { forall i:int. - (0 <= i < to_int ofs \/ - to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] } - ensures { forall i:int. to_int ofs <= i < to_int ofs + to_int len -> + (0 <= i < ofs \/ + ofs + len <= i < a.length) -> a[i] = (old a)[i] } + ensures { forall i:int. ofs <= i < ofs + len -> a[i] = v } val blit (a1: array 'a) (ofs1: int32) (a2: array 'a) (ofs2: int32) (len: int32) : unit writes {a2} - requires { 0 <= to_int ofs1 /\ 0 <= to_int len } - requires { to_int ofs1 + to_int len <= to_int a1.length } - requires { 0 <= to_int ofs2 /\ - to_int ofs2 + to_int len <= to_int a2.length } + requires { 0 <= ofs1 /\ 0 <= len } + requires { ofs1 + len <= a1.length } + requires { 0 <= ofs2 /\ + ofs2 + len <= a2.length } ensures { forall i:int. - (0 <= i < to_int ofs2 \/ - to_int ofs2 + to_int len <= i < to_int a2.length) -> + (0 <= i < ofs2 \/ + ofs2 + len <= i < a2.length) -> a2[i] = (old a2)[i] } ensures { forall i:int. - to_int ofs2 <= i < to_int ofs2 + to_int len -> - a2[i] = a1[to_int ofs1 + i - to_int ofs2] } + ofs2 <= i < ofs2 + len -> + a2[i] = a1[ofs1 + i - ofs2] } val self_blit (a: array 'a) (ofs1: int32) (ofs2: int32) (len: int32) : unit writes {a} - requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\ - to_int ofs1 + to_int len <= to_int a.length } - requires { 0 <= to_int ofs2 /\ to_int ofs2 + to_int len <= to_int a.length } + requires { 0 <= ofs1 /\ 0 <= len /\ + ofs1 + len <= a.length } + requires { 0 <= ofs2 /\ ofs2 + len <= a.length } ensures { forall i:int. - (0 <= i < to_int ofs2 \/ - to_int ofs2 + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] } + (0 <= i < ofs2 \/ + ofs2 + len <= i < a.length) -> a[i] = (old a)[i] } ensures { forall i:int. - to_int ofs2 <= i < to_int ofs2 + to_int len -> - a[i] = (old a)[to_int ofs1 + i - to_int ofs2] } + ofs2 <= i < ofs2 + len -> + a[i] = (old a)[ofs1 + i - ofs2] } end @@ -114,91 +114,91 @@ module Array31 type array 'a = private { mutable ghost elts : int -> 'a; length : int31; - } invariant { 0 <= to_int length } + } invariant { 0 <= length } function ([]) (a: array 'a) (i: int) : 'a = a.elts i val ([]) (a: array 'a) (i: int31) : 'a - requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length } - ensures { result = a[to_int i] } + requires { "expl:index in array bounds" 0 <= i < a.length } + ensures { result = a[i] } val ([]<-) (a: array 'a) (i: int31) (v: 'a) : unit writes {a} - requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length } - ensures { a.elts = (old a.elts)[to_int i <- v] } + requires { "expl:index in array bounds" 0 <= i < a.length } + ensures { a.elts = (old a.elts)[i <- v] } (** unsafe get/set operations with no precondition *) exception OutOfBounds let defensive_get (a: array 'a) (i: int31) - ensures { 0 <= to_int i < to_int a.length } - ensures { result = a[to_int i] } - raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length } + ensures { 0 <= i < a.length } + ensures { result = a[i] } + raises { OutOfBounds -> i < 0 \/ i >= a.length } = if i < of_int 0 || i >= length a then raise OutOfBounds; a[i] let defensive_set (a: array 'a) (i: int31) (v: 'a) - ensures { 0 <= to_int i < to_int a.length } - ensures { a.elts = (old a.elts)[to_int i <- v] } - raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length } + ensures { 0 <= i < a.length } + ensures { a.elts = (old a.elts)[i <- v] } + raises { OutOfBounds -> i < 0 \/ i >= a.length } = if i < of_int 0 || i >= length a then raise OutOfBounds; a[i] <- v val make (n: int31) (v: 'a) : array 'a - requires { "expl:array creation size" to_int n >= 0 } - ensures { forall i:int. 0 <= i < to_int n -> result[i] = v } + requires { "expl:array creation size" n >= 0 } + ensures { forall i:int. 0 <= i < n -> result[i] = v } ensures { result.length = n } val append (a1: array 'a) (a2: array 'a) : array 'a - ensures { to_int result.length = to_int a1.length + to_int a2.length } - ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] } - ensures { forall i:int. 0 <= i < to_int a2.length -> - result[to_int a1.length + i] = a2[i] } + ensures { result.length = a1.length + a2.length } + ensures { forall i:int. 0 <= i < a1.length -> result[i] = a1[i] } + ensures { forall i:int. 0 <= i < a2.length -> + result[a1.length + i] = a2[i] } val sub (a: array 'a) (ofs: int31) (len: int31) : array 'a - requires { 0 <= to_int ofs /\ 0 <= to_int len } - requires { to_int ofs + to_int len <= to_int a.length } + requires { 0 <= ofs /\ 0 <= len } + requires { ofs + len <= a.length } ensures { result.length = len } - ensures { forall i:int. 0 <= i < to_int len -> - result[i] = a[to_int ofs + i] } + ensures { forall i:int. 0 <= i < len -> + result[i] = a[ofs + i] } val copy (a: array 'a) : array 'a ensures { result.length = a.length } - ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] } + ensures { forall i:int. 0 <= i < result.length -> result[i] = a[i] } val fill (a: array 'a) (ofs: int31) (len: int31) (v: 'a) : unit - requires { 0 <= to_int ofs /\ 0 <= to_int len } - requires { to_int ofs + to_int len <= to_int a.length } + requires { 0 <= ofs /\ 0 <= len } + requires { ofs + len <= a.length } ensures { forall i:int. - (0 <= i < to_int ofs \/ - to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] } - ensures { forall i:int. to_int ofs <= i < to_int ofs + to_int len -> + (0 <= i < ofs \/ + ofs + len <= i < a.length) -> a[i] = (old a)[i] } + ensures { forall i:int. ofs <= i < ofs + len -> a[i] = v } val blit (a1: array 'a) (ofs1: int31) (a2: array 'a) (ofs2: int31) (len: int31) : unit writes {a2} - requires { 0 <= to_int ofs1 /\ 0 <= to_int len } - requires { to_int ofs1 + to_int len <= to_int a1.length } - requires { 0 <= to_int ofs2 /\ - to_int ofs2 + to_int len <= to_int a2.length } + requires { 0 <= ofs1 /\ 0 <= len } + requires { ofs1 + len <= a1.length } + requires { 0 <= ofs2 /\ + ofs2 + len <= a2.length } ensures { forall i:int. - (0 <= i < to_int ofs2 \/ - to_int ofs2 + to_int len <= i < to_int a2.length) -> + (0 <= i < ofs2 \/ + ofs2 + len <= i < a2.length) -> a2[i] = (old a2)[i] } ensures { forall i:int. - to_int ofs2 <= i < to_int ofs2 + to_int len -> - a2[i] = a1[to_int ofs1 + i - to_int ofs2] } + ofs2 <= i < ofs2 + len -> + a2[i] = a1[ofs1 + i - ofs2] } val self_blit (a: array 'a) (ofs1: int31) (ofs2: int31) (len: int31) : unit writes {a} - requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\ - to_int ofs1 + to_int len <= to_int a.length } - requires { 0 <= to_int ofs2 /\ to_int ofs2 + to_int len <= to_int a.length } + requires { 0 <= ofs1 /\ 0 <= len /\ + ofs1 + len <= a.length } + requires { 0 <= ofs2 /\ ofs2 + len <= a.length } ensures { forall i:int. - (0 <= i < to_int ofs2 \/ - to_int ofs2 + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] } + (0 <= i < ofs2 \/ + ofs2 + len <= i < a.length) -> a[i] = (old a)[i] } ensures { forall i:int. - to_int ofs2 <= i < to_int ofs2 + to_int len -> - a[i] = (old a)[to_int ofs1 + i - to_int ofs2] } + ofs2 <= i < ofs2 + len -> + a[i] = (old a)[ofs1 + i - ofs2] } end @@ -213,92 +213,92 @@ module Array63 type array 'a = private { mutable ghost elts : int -> 'a; length : int63; - } invariant { 0 <= to_int length } + } invariant { 0 <= length } function ([]) (a: array 'a) (i: int) : 'a = a.elts i val ([]) (a: array 'a) (i: int63) : 'a - requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length } - ensures { result = a[to_int i] } + requires { "expl:index in array bounds" 0 <= i < a.length } + ensures { result = a[i] } val ([]<-) (a: array 'a) (i: int63) (v: 'a) : unit writes {a} - requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length } - ensures { a.elts = (old a.elts)[to_int i <- v] } + requires { "expl:index in array bounds" 0 <= i < a.length } + ensures { a.elts = (old a.elts)[i <- v] } (** unsafe get/set operations with no precondition *) exception OutOfBounds let defensive_get (a: array 'a) (i: int63) - ensures { 0 <= to_int i < to_int a.length } - ensures { result = a[to_int i] } - raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length } + ensures { 0 <= i < a.length } + ensures { result = a[i] } + raises { OutOfBounds -> i < 0 \/ i >= a.length } = if i < of_int 0 || i >= length a then raise OutOfBounds; a[i] let defensive_set (a: array 'a) (i: int63) (v: 'a) - ensures { 0 <= to_int i < to_int a.length } - ensures { a.elts = (old a.elts)[to_int i <- v] } - raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length } + ensures { 0 <= i < a.length } + ensures { a.elts = (old a.elts)[i <- v] } + raises { OutOfBounds -> i < 0 \/ i >= a.length } = if i < of_int 0 || i >= length a then raise OutOfBounds; a[i] <- v val make (n: int63) (v: 'a) : array 'a - requires { "expl:array creation size" to_int n >= 0 } - ensures { forall i:int. 0 <= i < to_int n -> result[i] = v } + requires { "expl:array creation size" n >= 0 } + ensures { forall i:int. 0 <= i < n -> result[i] = v } ensures { result.length = n } val append (a1: array 'a) (a2: array 'a) : array 'a - ensures { to_int result.length = to_int a1.length + to_int a2.length } - ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] } - ensures { forall i:int. 0 <= i < to_int a2.length -> - result[to_int a1.length + i] = a2[i] } + ensures { result.length = a1.length + a2.length } + ensures { forall i:int. 0 <= i < a1.length -> result[i] = a1[i] } + ensures { forall i:int. 0 <= i < a2.length -> + result[a1.length + i] = a2[i] } val sub (a: array 'a) (ofs: int63) (len: int63) : array 'a - requires { 0 <= to_int ofs /\ 0 <= to_int len } - requires { to_int ofs + to_int len <= to_int a.length } + requires { 0 <= ofs /\ 0 <= len } + requires { ofs + len <= a.length } ensures { result.length = len } - ensures { forall i:int. 0 <= i < to_int len -> - result[i] = a[to_int ofs + i] } + ensures { forall i:int. 0 <= i < len -> + result[i] = a[ofs + i] } val copy (a: array 'a) : array 'a ensures { result.length = a.length } - ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] } + ensures { forall i:int. 0 <= i < result.length -> result[i] = a[i] } val fill (a: array 'a) (ofs: int63) (len: int63) (v: 'a) : unit writes { a } - requires { 0 <= to_int ofs /\ 0 <= to_int len } - requires { to_int ofs + to_int len <= to_int a.length } + requires { 0 <= ofs /\ 0 <= len } + requires { ofs + len <= a.length } ensures { forall i:int. - (0 <= i < to_int ofs \/ - to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] } - ensures { forall i:int. to_int ofs <= i < to_int ofs + to_int len -> + (0 <= i < ofs \/ + ofs + len <= i < a.length) -> a[i] = (old a)[i] } + ensures { forall i:int. ofs <= i < ofs + len -> a[i] = v } val blit (a1: array 'a) (ofs1: int63) (a2: array 'a) (ofs2: int63) (len: int63) : unit writes {a2} - requires { 0 <= to_int ofs1 /\ 0 <= to_int len } - requires { to_int ofs1 + to_int len <= to_int a1.length } - requires { 0 <= to_int ofs2 /\ - to_int ofs2 + to_int len <= to_int a2.length } + requires { 0 <= ofs1 /\ 0 <= len } + requires { ofs1 + len <= a1.length } + requires { 0 <= ofs2 /\ + ofs2 + len <= a2.length } ensures { forall i:int. - (0 <= i < to_int ofs2 \/ - to_int ofs2 + to_int len <= i < to_int a2.length) -> + (0 <= i < ofs2 \/ + ofs2 + len <= i < a2.length) -> a2[i] = (old a2)[i] } ensures { forall i:int. - to_int ofs2 <= i < to_int ofs2 + to_int len -> - a2[i] = a1[to_int ofs1 + i - to_int ofs2] } + ofs2 <= i < ofs2 + len -> + a2[i] = a1[ofs1 + i - ofs2] } val self_blit (a: array 'a) (ofs1: int63) (ofs2: int63) (len: int63) : unit writes {a} - requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\ - to_int ofs1 + to_int len <= to_int a.length } - requires { 0 <= to_int ofs2 /\ to_int ofs2 + to_int len <= to_int a.length } + requires { 0 <= ofs1 /\ 0 <= len /\ + ofs1 + len <= a.length } + requires { 0 <= ofs2 /\ ofs2 + len <= a.length } ensures { forall i:int. - (0 <= i < to_int ofs2 \/ - to_int ofs2 + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] } + (0 <= i < ofs2 \/ + ofs2 + len <= i < a.length) -> a[i] = (old a)[i] } ensures { forall i:int. - to_int ofs2 <= i < to_int ofs2 + to_int len -> - a[i] = (old a)[to_int ofs1 + i - to_int ofs2] } + ofs2 <= i < ofs2 + len -> + a[i] = (old a)[ofs1 + i - ofs2] } end diff --git a/modules/mach/int.mlw b/modules/mach/int.mlw index 4b28e95ee527e69332268681258e7efc31dd60a6..7ef4012c1fec13ed995f2374dbb7c87c2d71cea0 100644 --- a/modules/mach/int.mlw +++ b/modules/mach/int.mlw @@ -99,14 +99,14 @@ module Bounded_int use import int.ComputerDivision val (/) (a:t) (b:t) : t - requires { "expl:division by zero" to_int b <> 0 } - requires { "expl:integer overflow" in_bounds (div (to_int a) (to_int b)) } - ensures { to_int result = div (to_int a) (to_int b) } + requires { "expl:division by zero" b <> 0 } + requires { "expl:integer overflow" in_bounds (div a b) } + ensures { result = div a b } val (%) (a:t) (b:t) : t - requires { "expl:division by zero" to_int b <> 0 } - requires { "expl:integer overflow" in_bounds (mod (to_int a) (to_int b)) } - ensures { to_int result = mod (to_int a) (to_int b) } + requires { "expl:division by zero" b <> 0 } + requires { "expl:integer overflow" in_bounds (mod a b) } + ensures { result = mod a b } end diff --git a/share/emacs/why3.el b/share/emacs/why3.el index 03426e0eb8d9efd23f5a792b029f3f219b2774fe..dfb9864dffbb56667f156be9605bfc5157cef2b4 100644 --- a/share/emacs/why3.el +++ b/share/emacs/why3.el @@ -28,8 +28,8 @@ ;; Note: comment font-lock is guaranteed by suitable syntax entries '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face) ; '("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face) - `(,(why3-regexp-opt '("invariant" "variant" "diverges" "requires" "ensures" "returns" "raises" "reads" "writes" "alias" "assert" "assume" "check")) . font-lock-type-face) - `(,(why3-regexp-opt '("use" "clone" "scope" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "raise" "try" "with" "theory" "uses" "module" "converter" "fun" "at" "old" "true" "false" "forall" "exists" "label" "by" "so" "meta")) . font-lock-keyword-face) + `(,(why3-regexp-opt '("invariant" "variant" "diverges" "requires" "ensures" "pure" "returns" "raises" "reads" "writes" "alias" "assert" "assume" "check")) . font-lock-type-face) + `(,(why3-regexp-opt '("use" "clone" "scope" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "raise" "return" "try" "with" "theory" "uses" "module" "converter" "fun" "at" "old" "true" "false" "forall" "exists" "label" "by" "so" "meta")) . font-lock-keyword-face) ) "Minimal highlighting for Why3 mode") diff --git a/share/lang/why3.lang b/share/lang/why3.lang index 607bcbe4126f1dae9346fbcce950ab77ec798b9e..1033d7cb8b6bebbbb10fcea07e58788ab263f534 100644 --- a/share/lang/why3.lang +++ b/share/lang/why3.lang @@ -204,6 +204,7 @@ on linking described in file LICENSE. not raise rec + return so then to @@ -223,6 +224,7 @@ on linking described in file LICENSE. check invariant old + pure raises reads requires diff --git a/share/latex/why3lang.log b/share/latex/why3lang.log new file mode 100644 index 0000000000000000000000000000000000000000..4721fc5ff2bd1d1cd4f80c960d42ca9ac5522a7d --- /dev/null +++ b/share/latex/why3lang.log @@ -0,0 +1,66 @@ +This is pdfTeX, Version 3.14159265-2.6-1.40.15 (TeX Live 2015/dev/Debian) (preloaded format=pdflatex 2017.3.26) 16 MAY 2017 14:32 +entering extended mode + restricted \write18 enabled. + %&-line parsing enabled. +**/home/rrieu/why3/share/latex/why3lang.sty +(/home/rrieu/why3/share/latex/why3lang.sty +LaTeX2e <2014/05/01> +Babel <3.9l> and hyphenation patterns for 79 languages loaded. +(/usr/share/texlive/texmf-dist/tex/latex/listings/listings.sty +(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty +Package: keyval 2014/05/08 v1.15 key=value parser (DPC) +\KV@toks@=\toks14 +) +\lst@mode=\count79 +\lst@gtempboxa=\box26 +\lst@token=\toks15 +\lst@length=\count80 +\lst@currlwidth=\dimen102 +\lst@column=\count81 +\lst@pos=\count82 +\lst@lostspace=\dimen103 +\lst@width=\dimen104 +\lst@newlines=\count83 +\lst@lineno=\count84 +\abovecaptionskip=\skip41 +\belowcaptionskip=\skip42 +\lst@maxwidth=\dimen105 + +(/usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty +File: lstmisc.sty 2014/09/06 1.5e (Carsten Heinz) +\c@lstnumber=\count85 +\lst@skipnumbers=\count86 +\lst@framebox=\box27 +) +(/usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg +File: listings.cfg 2014/09/06 1.5e listings configuration +)) +Package: listings 2014/09/06 1.5e (Carsten Heinz) + +(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty +Package: amssymb 2013/01/14 v3.01 AMS font symbols + +(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty +Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support +\@emptytoks=\toks16 +\symAMSa=\mathgroup4 +\symAMSb=\mathgroup5 +LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold' +(Font) U/euf/m/n --> U/euf/b/n on input line 106. +))) +* +! Emergency stop. +<*> /home/rrieu/why3/share/latex/why3lang.sty + +End of file on the terminal! + + +Here is how much of TeX's memory you used: + 1497 strings out of 493105 + 20991 string characters out of 6137072 + 69587 words of memory out of 5000000 + 5037 multiletter control sequences out of 15000+600000 + 3640 words of font info for 14 fonts, out of 8000000 for 9000 + 1141 hyphenation exceptions out of 8191 + 26i,0n,32p,208b,219s stack positions out of 5000i,500n,10000p,200000b,80000s +! ==> Fatal error occurred, no output PDF file produced! diff --git a/share/latex/why3lang.sty b/share/latex/why3lang.sty index 4972334decf1325601e6849731206f96c8abf45b..e33ce46cc330e1349c4cdf5985db6819e2744343 100644 --- a/share/latex/why3lang.sty +++ b/share/latex/why3lang.sty @@ -10,7 +10,7 @@ check,clone,coinductive,constant,diverges,do,done,downto,% else,end,ensures,exception,exists,export,false,for,forall,fun,% function,ghost,goal,if,import,in,inductive,invariant,label,lemma,% let,loop,match,meta,module,mutable,not,old,% -predicate,private,raise,raises,reads,rec,requires,result,% +predicate,private,pure,raise,raises,reads,rec,requires,result,return,% returns,scope,so,then,theory,to,true,try,type,use,val,variant,while,% with,writes},% string=[b]",% diff --git a/share/vim/syntax/why3.vim b/share/vim/syntax/why3.vim index 643250a2c7ec48ec4511a31cf36113a3035bbd45..074a5761c1cfe4a28ad9e3188d253a8600bb70c9 100644 --- a/share/vim/syntax/why3.vim +++ b/share/vim/syntax/why3.vim @@ -92,16 +92,15 @@ syn keyword whyKeyword then type with syn keyword whyKeyword abstract any syn keyword whyKeyword exception fun ghost label syn keyword whyKeyword model mutable private -syn keyword whyKeyword raise rec val while +syn keyword whyKeyword raise rec return val while syn keyword whyBoolean true false syn keyword whyType bool int list map option real syn keyword whyType array ref unit -syn keyword whySpec absurd alias assert assume check diverges ensures -syn keyword whySpec invariant raises reads requires returns variant writes -syn keyword whySpec at old +syn keyword whySpec absurd alias assert assume check diverges ensures invariant +syn keyword whySpec pure raises reads requires returns variant writes at old syn match whyConstructor "(\s*)" syn match whyConstructor "\u\(\w\|'\)*\>" diff --git a/src/core/dterm.ml b/src/core/dterm.ml index 0aaf53ce55111a54f6799b2e44d4492f751b73b5..c728cab58fcb43520e0400bf48effa7d227cb157 100644 --- a/src/core/dterm.ml +++ b/src/core/dterm.ml @@ -103,6 +103,8 @@ let rec dty_unify dty1 dty2 = match dty1,dty2 with List.iter2 dty_unify dl1 dl2 | _ -> raise Exit +let dty_int = Duty ty_int +let dty_real = Duty ty_real let dty_bool = Duty ty_bool let protect_on x s = if x then "(" ^^ s ^^ ")" else s @@ -184,7 +186,7 @@ and dpattern_node = | DPapp of lsymbol * dpattern list | DPor of dpattern * dpattern | DPas of dpattern * preid - | DPcast of dpattern * ty + | DPcast of dpattern * dty type dbinop = | DTand | DTand_asym | DTor | DTor_asym | DTimplies | DTiff | DTby | DTso @@ -203,7 +205,7 @@ type dterm = { and dterm_node = | DTvar of string * dty | DTgvar of vsymbol - | DTconst of Number.constant * ty + | DTconst of Number.constant * dty | DTapp of lsymbol * dterm list | DTfapp of dterm * dterm | DTif of dterm * dterm * dterm @@ -215,7 +217,7 @@ and dterm_node = | DTnot of dterm | DTtrue | DTfalse - | DTcast of dterm * ty + | DTcast of dterm * dty | DTuloc of dterm * Loc.position | DTlabel of dterm * Slab.t @@ -317,8 +319,7 @@ let dpattern ?loc node = dp1.dp_dty, Mstr.union join dp1.dp_vars dp2.dp_vars | DPas (dp,{pre_name = n}) -> dp.dp_dty, Mstr.add_new (DuplicateVar n) n dp.dp_dty dp.dp_vars - | DPcast (dp,ty) -> - let dty = dty_of_ty ty in + | DPcast (dp,dty) -> dpat_expected_type dp dty; dty, dp.dp_vars in let dty, vars = Loc.try1 ?loc get_dty node in @@ -395,8 +396,8 @@ let dterm tuc ?loc node = mk_dty (Some dty) | DTgvar vs -> mk_dty (Some (dty_of_ty vs.vs_ty)) - | DTconst (_,ty) -> - mk_dty (Some (dty_of_ty ty)) + | DTconst (_,dty) -> + mk_dty (Some dty) | DTapp (ls, dtl) when ls_equal ls ps_equ -> let swap, dtl = match dtl with @@ -490,8 +491,7 @@ let dterm tuc ?loc node = there is no need to count these constructs as "formulas" which require explicit if-then-else conversion to bool *) mk_dty (Some dty_bool) - | DTcast (dt,ty) -> - let dty = dty_of_ty ty in + | DTcast (dt,dty) -> dterm_expected_dterm tuc dt dty | DTuloc (dt,_) | DTlabel (dt,_) -> @@ -606,8 +606,8 @@ and try_term strict keep_loc uloc env prop dty node = t_var (Mstr.find_exn (UnboundVar n) n env) | DTgvar vs -> t_var vs - | DTconst (c,ty) -> - t_const c ty + | DTconst (c,dty) -> + t_const c (term_ty_of_dty ~strict dty) | DTapp (ls,[]) when ls_equal ls fs_bool_true -> if prop then t_true else t_bool_true | DTapp (ls,[]) when ls_equal ls fs_bool_false -> diff --git a/src/core/dterm.mli b/src/core/dterm.mli index b242ad59a4a9f38ab70a4c76b02eec902f12f977..c6c2edd13337667ba66dd8ac0253aa792d3893a3 100644 --- a/src/core/dterm.mli +++ b/src/core/dterm.mli @@ -28,6 +28,8 @@ val dty_app : tysymbol -> dty list -> dty val dty_match : dty -> ty -> unit (* raises Exit on failure *) val dty_unify : dty -> dty -> unit (* raises Exit on failure *) +val dty_int : dty +val dty_real : dty val dty_bool : dty val dty_fold : (tysymbol -> 'a list -> 'a) -> @@ -48,7 +50,7 @@ and dpattern_node = | DPapp of lsymbol * dpattern list | DPor of dpattern * dpattern | DPas of dpattern * preid - | DPcast of dpattern * ty + | DPcast of dpattern * dty type dbinop = | DTand | DTand_asym | DTor | DTor_asym | DTimplies | DTiff | DTby | DTso @@ -67,7 +69,7 @@ type dterm = private { and dterm_node = | DTvar of string * dty | DTgvar of vsymbol - | DTconst of Number.constant * ty + | DTconst of Number.constant * dty | DTapp of lsymbol * dterm list | DTfapp of dterm * dterm | DTif of dterm * dterm * dterm @@ -79,7 +81,7 @@ and dterm_node = | DTnot of dterm | DTtrue | DTfalse - | DTcast of dterm * ty + | DTcast of dterm * dty | DTuloc of dterm * Loc.position | DTlabel of dterm * Slab.t diff --git a/src/core/pretty.ml b/src/core/pretty.ml index 68f91b15a5e8ec1d526b7e2dd5fc797dc17feebf..5c0017efd3001f4fdc1916f0d6df5847168664b8 100644 --- a/src/core/pretty.ml +++ b/src/core/pretty.ml @@ -296,12 +296,12 @@ and print_tnode pri fmt t = match t.t_node with fprintf fmt "false" | Tbinop (Tand,f1,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) }) when Slab.mem Term.asym_split f2.t_label -> - fprintf fmt (protect_on (pri > 2) "@[%a so@ %a@]") - (print_lterm 3) f1 (print_lterm 2) f2 + fprintf fmt (protect_on (pri > 1) "@[%a so@ %a@]") + (print_lterm 2) f1 (print_lterm 1) f2 | Tbinop (Timplies,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) },f1) when Slab.mem Term.asym_split f2.t_label -> - fprintf fmt (protect_on (pri > 2) "@[%a by@ %a@]") - (print_lterm 3) f1 (print_lterm 2) f2 + fprintf fmt (protect_on (pri > 1) "@[%a by@ %a@]") + (print_lterm 2) f1 (print_lterm 1) f2 | Tbinop (b,f1,f2) -> let asym = Slab.mem Term.asym_split f1.t_label in let p = prio_binop b in diff --git a/src/core/theory.ml b/src/core/theory.ml index 12771a3f24d68e4c5117e7e84b2f85c0464c3750..b91cec4475812652da3fc8c5ef5d01eb9209a6b5 100644 --- a/src/core/theory.ml +++ b/src/core/theory.ml @@ -39,29 +39,30 @@ let ns_replace eq chk x vo vn = if eq vo vn then vo else raise (ClashSymbol x) -let rec merge_ns chk ns1 ns2 = - if ns1 == ns2 then ns1 else - let join eq x n o = Some (ns_replace eq chk x o n) in - let ns_union eq m1 m2 = - if m1 == m2 then m1 else Mstr.union (join eq) m1 m2 in - let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in - { ns_ts = ns_union ts_equal ns1.ns_ts ns2.ns_ts; - ns_ls = ns_union ls_equal ns1.ns_ls ns2.ns_ls; - ns_pr = ns_union pr_equal ns1.ns_pr ns2.ns_pr; - ns_ns = Mstr.union fusion ns1.ns_ns ns2.ns_ns; } - -let add_ns chk x ns m = Mstr.change (function - | Some os -> Some (merge_ns chk ns os) - | None -> Some ns) x m - -let ns_add eq chk x vn m = Mstr.change (function - | Some vo -> Some (ns_replace eq chk x vo vn) +let merge_ts = ns_replace ts_equal +let merge_ls = ns_replace ls_equal +let merge_pr = ns_replace pr_equal + +let rec merge_ns chk _ no nn = + if no == nn then no else + let union merge o n = + let merge x vo vn = Some (merge chk x vo vn) in + if o == n then o else Mstr.union merge o n in + { ns_ts = union merge_ts no.ns_ts nn.ns_ts; + ns_ls = union merge_ls no.ns_ls nn.ns_ls; + ns_pr = union merge_pr no.ns_pr nn.ns_pr; + ns_ns = union merge_ns no.ns_ns nn.ns_ns } + +let ns_add merge chk x vn m = Mstr.change (function + | Some vo -> Some (merge chk x vo vn) | None -> Some vn) x m -let add_ts chk x ts ns = { ns with ns_ts = ns_add ts_equal chk x ts ns.ns_ts } -let add_ls chk x ls ns = { ns with ns_ls = ns_add ls_equal chk x ls ns.ns_ls } -let add_pr chk x pf ns = { ns with ns_pr = ns_add pr_equal chk x pf ns.ns_pr } -let add_ns chk x nn ns = { ns with ns_ns = add_ns chk x nn ns.ns_ns } +let add_ts chk x ts ns = { ns with ns_ts = ns_add merge_ts chk x ts ns.ns_ts } +let add_ls chk x ps ns = { ns with ns_ls = ns_add merge_ls chk x ps ns.ns_ls } +let add_pr chk x xs ns = { ns with ns_pr = ns_add merge_pr chk x xs ns.ns_pr } +let add_ns chk x nn ns = { ns with ns_ns = ns_add merge_ns chk x nn ns.ns_ns } + +let merge_ns chk nn no = merge_ns chk "" no nn (* swap arguments *) let rec ns_find get_map ns = function | [] -> assert false @@ -156,14 +157,15 @@ let meta_float = register_meta "float_type" [MTtysymbol; MTlsymbol; MTlsymbol] (** Theory *) type theory = { - th_name : ident; (* theory name *) - th_path : string list; (* environment qualifiers *) - th_decls : tdecl list; (* theory declarations *) - th_crcmap : Coercion.t; (* implicit coercions *) - th_export : namespace; (* exported namespace *) - th_known : known_map; (* known identifiers *) - th_local : Sid.t; (* locally declared idents *) - th_used : Sid.t; (* used theories *) + th_name : ident; (* theory name *) + th_path : string list; (* environment qualifiers *) + th_decls : tdecl list; (* theory declarations *) + th_ranges : lsymbol Mts.t; (* range type projections *) + th_crcmap : Coercion.t; (* implicit coercions *) + th_export : namespace; (* exported namespace *) + th_known : known_map; (* known identifiers *) + th_local : Sid.t; (* locally declared idents *) + th_used : Sid.t; (* used theories *) } and tdecl = { @@ -263,6 +265,7 @@ type theory_uc = { uc_name : ident; uc_path : string list; uc_decls : tdecl list; + uc_ranges : lsymbol Mts.t; uc_crcmap : Coercion.t; uc_prefix : string list; uc_import : namespace list; @@ -279,6 +282,7 @@ let empty_theory n p = { uc_name = id_register n; uc_path = p; uc_decls = []; + uc_ranges = Mts.empty; uc_crcmap = Coercion.empty; uc_prefix = []; uc_import = [empty_ns]; @@ -293,6 +297,7 @@ let close_theory uc = match uc.uc_export with { th_name = uc.uc_name; th_path = uc.uc_path; th_decls = List.rev uc.uc_decls; + th_ranges = uc.uc_ranges; th_crcmap = uc.uc_crcmap; th_export = e; th_known = uc.uc_known; @@ -319,6 +324,13 @@ let close_scope uc ~import = | [], [_], [_] -> raise NoOpenedNamespace | _ -> assert false +let import_scope uc ql = match uc.uc_import with + | i1 :: sti -> + let e0 = ns_find_ns i1 ql in + let i1 = merge_ns false e0 i1 in + { uc with uc_import = i1::sti } + | _ -> assert false + (* Base constructors *) let known_ty kn ty = @@ -340,8 +352,11 @@ let known_meta kn al = in List.iter check al +(* FIXME: proper description *) let meta_coercion = register_meta ~desc:"coercion" "coercion" [MTlsymbol] +exception RangeConflict of tysymbol + let add_tdecl uc td = match td.td_node with | Decl d -> { uc with uc_decls = td :: uc.uc_decls; @@ -354,11 +369,20 @@ let add_tdecl uc td = match td.td_node with uc_used = Sid.union uc.uc_used (Sid.add th.th_name th.th_used) } | Clone (_,sm) -> known_clone uc.uc_known sm; { uc with uc_decls = td :: uc.uc_decls } + | Meta (m,([MAts ts; MAls ls] as al)) when meta_equal m meta_range -> + known_meta uc.uc_known al; + let add b = match b with + | None -> Some ls + | Some s when ls_equal s ls -> b + | _ -> raise (RangeConflict ts) in + { uc with uc_ranges = Mts.change add ts uc.uc_ranges; + uc_decls = td :: uc.uc_decls } | Meta (m,([MAls ls] as al)) when meta_equal m meta_coercion -> known_meta uc.uc_known al; - (* FIXME: shouldn't we add the meta to the theory? *) - { uc with uc_crcmap = Coercion.add uc.uc_crcmap ls } - | Meta (_,al) -> known_meta uc.uc_known al; + { uc with uc_crcmap = Coercion.add uc.uc_crcmap ls; + uc_decls = td :: uc.uc_decls } + | Meta (_,al) -> + known_meta uc.uc_known al; { uc with uc_decls = td :: uc.uc_decls } (** Declarations *) @@ -479,10 +503,13 @@ let create_use th = mk_tdecl (Use th) let use_export uc th = let uc = add_tdecl uc (create_use th) in + let comb ts s1 s2 = if ls_equal s1 s2 then Some s1 + else raise (RangeConflict ts) in match uc.uc_import, uc.uc_export with | i0 :: sti, e0 :: ste -> { uc with uc_import = merge_ns false th.th_export i0 :: sti; uc_export = merge_ns true th.th_export e0 :: ste; + uc_ranges = Mts.union comb uc.uc_ranges th.th_ranges; uc_crcmap = Coercion.union uc.uc_crcmap th.th_crcmap } | _ -> assert false @@ -934,5 +961,8 @@ let () = Exn_printer.register Format.fprintf fmt "Metaproperty %s expects a %a argument but \ is applied to %a" m.meta_name print_meta_arg_type t1 print_meta_arg_type t2 + | RangeConflict ts -> + Format.fprintf fmt "Conflicting definitions for range type %s" + ts.ts_name.id_string | _ -> raise exn end diff --git a/src/core/theory.mli b/src/core/theory.mli index 38e9de69e0740ee2bb992fa02296e56fd0bc4cff..4788ce960acfd2b89edbb4db44b5889f17d56fb4 100644 --- a/src/core/theory.mli +++ b/src/core/theory.mli @@ -84,14 +84,15 @@ val meta_float : meta (** {2 Theories} *) type theory = private { - th_name : ident; (* theory name *) - th_path : string list; (* environment qualifiers *) - th_decls : tdecl list; (* theory declarations *) - th_crcmap : Coercion.t; (* implicit coercions *) - th_export : namespace; (* exported namespace *) - th_known : known_map; (* known identifiers *) - th_local : Sid.t; (* locally declared idents *) - th_used : Sid.t; (* used theories *) + th_name : ident; (* theory name *) + th_path : string list; (* environment qualifiers *) + th_decls : tdecl list; (* theory declarations *) + th_ranges : lsymbol Mts.t; (* range type projections *) + th_crcmap : Coercion.t; (* implicit coercions *) + th_export : namespace; (* exported namespace *) + th_known : known_map; (* known identifiers *) + th_local : Sid.t; (* locally declared idents *) + th_used : Sid.t; (* used theories *) } and tdecl = private { @@ -125,6 +126,7 @@ type theory_uc = private { uc_name : ident; uc_path : string list; uc_decls : tdecl list; + uc_ranges : lsymbol Mts.t; uc_crcmap : Coercion.t; uc_prefix : string list; uc_import : namespace list; @@ -137,8 +139,9 @@ type theory_uc = private { val create_theory : ?path:string list -> preid -> theory_uc val close_theory : theory_uc -> theory -val open_scope : theory_uc -> string -> theory_uc -val close_scope : theory_uc -> import:bool -> theory_uc +val open_scope : theory_uc -> string -> theory_uc +val close_scope : theory_uc -> import:bool -> theory_uc +val import_scope : theory_uc -> string list -> theory_uc val get_namespace : theory_uc -> namespace @@ -230,3 +233,5 @@ exception KnownMeta of meta exception UnknownMeta of string exception BadMetaArity of meta * int exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type + +exception RangeConflict of tysymbol diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml index 147bd15a7eeaab2171d60c2399c35e6b2f067b92..5a71ee3ed3a3273b093b7bc7e2c4dabff636d302 100644 --- a/src/ide/gmain.ml +++ b/src/ide/gmain.ml @@ -863,14 +863,6 @@ let project_dir = else fname -let () = - if not (Sys.file_exists project_dir) then - begin - Debug.dprintf debug "[GUI] '%s' does not exist. \ - Creating directory of that name for the project@." project_dir; - Unix.mkdir project_dir 0o777 - end - let info_window ?(callback=(fun () -> ())) mt s = let buttons = match mt with | `INFO -> GWindow.Buttons.close @@ -1338,13 +1330,20 @@ let save_session () = session_needs_saving := false; end +let quit_save () = + save_session (); GMain.quit () + +(* override GMain.quit to remove an empty session directory *) +let quit_no_save () = + begin try Unix.rmdir project_dir with _ -> () end; + GMain.quit () let exit_function ~destroy () = (* do not save automatically anymore Gconfig.save_config (); *) - if not !session_needs_saving then GMain.quit () else + if not !session_needs_saving then quit_no_save () else match (Gconfig.config ()).saving_policy with - | 0 -> save_session (); GMain.quit () - | 1 -> GMain.quit () + | 0 -> quit_save () + | 1 -> quit_no_save () | 2 -> let answer = GToolbox.question_box @@ -1354,13 +1353,13 @@ let exit_function ~destroy () = in begin match answer with - | 1 -> save_session (); GMain.quit () - | 2 -> GMain.quit () - | _ -> if destroy then GMain.quit () else () + | 1 -> quit_save () + | 2 -> quit_no_save () + | _ -> if destroy then quit_no_save () end | _ -> eprintf "unexpected value for saving_policy@."; - GMain.quit () + quit_no_save () (*************) (* View menu *) diff --git a/src/jessie/ACSLtoWhy3.ml b/src/jessie/ACSLtoWhy3.ml index 16a0470eb70fa719720f53320df0734d5d916dea..59402d5f69680ef1ceef2afc53ea9644cc422496 100644 --- a/src/jessie/ACSLtoWhy3.ml +++ b/src/jessie/ACSLtoWhy3.ml @@ -499,7 +499,7 @@ let get_var denv v = ev, is_mutable with Not_found -> let l = - Stdlib.Mstr.fold (fun s (_a,_b) acc -> s :: acc) (Dexpr.denv_contents denv) [] + Stdlib.Sstr.fold (fun s acc -> s :: acc) (Dexpr.denv_names denv) [] in Self.result "denv contains @[[%a]@]" (Pp.print_list Pp.semi Format.pp_print_string) l; @@ -1135,7 +1135,7 @@ and lval denv (host,offset) = get_var denv v with e -> let l = - Stdlib.Mstr.fold (fun s (_a,_b) acc -> s :: acc) (Dexpr.denv_contents denv) [] + Stdlib.Sstr.fold (fun s acc -> s :: acc) (Dexpr.denv_names denv) [] in Self.result "denv contains @[[%a]@]" (Pp.print_list Pp.semi Format.pp_print_string) l; @@ -1474,7 +1474,7 @@ let fundecl denv_global fdec = *) (* let l = - Stdlib.Mstr.fold (fun s (_a,_b) acc -> s :: acc) (Dexpr.denv_contents denv_global) [] + Stdlib.Sstr.fold (fun s acc -> s :: acc) (Dexpr.denv_names denv_global) [] in Self.result "denv_global contains @[[%a]@]" (Pp.print_list Pp.semi Format.pp_print_string) l; @@ -1482,7 +1482,7 @@ let fundecl denv_global fdec = let denv,def = Dexpr.drec_defn denv_global [predef] in (* let l = - Stdlib.Mstr.fold (fun s (_a,_b) acc -> s :: acc) (Dexpr.denv_contents denv) [] + Stdlib.Sstr.fold (fun s acc -> s :: acc) (Dexpr.denv_names denv) [] in Self.result "denv contains @[[%a]@]" (Pp.print_list Pp.semi Format.pp_print_string) l; @@ -1558,7 +1558,7 @@ let global (theories,lemmas,denv,functions) g = let denv = Dexpr.denv_add_let denv dlet_defn in Self.result "global var %s done" vi.vname; let l = - Stdlib.Mstr.fold (fun s (_a,_b) acc -> s :: acc) (Dexpr.denv_contents denv) [] + Stdlib.Sstr.fold (fun s acc -> s :: acc) (Dexpr.denv_names denv) [] in Self.result "denv contains @[[%a]@]" (Pp.print_list Pp.semi Format.pp_print_string) l; diff --git a/src/mlw/compile.ml b/src/mlw/compile.ml index 5bc2f2e60597fda355ec0ea7917578b7552321ba..939fc0d5ed4c7d3e422a957d2f163715b4a5d1fb 100644 --- a/src/mlw/compile.ml +++ b/src/mlw/compile.ml @@ -10,9 +10,6 @@ (********************************************************************) (* - - suggest a command line to compile the extracted code - (for instance in a comment) - - extract file f.mlw into OCaml file f.ml, with sub-modules - "use (im|ex)port" -> "open" @@ -45,108 +42,8 @@ let module_name ?fname path t = fname ^ "__" ^ t module ML = struct - open Expr - - type ty = - | Tvar of tvsymbol - | Tapp of ident * ty list - | Ttuple of ty list - - type is_ghost = bool - - type var = ident * ty * is_ghost - - type for_direction = To | DownTo - - type pat = - | Pwild - | Pvar of vsymbol - | Papp of lsymbol * pat list - | Ptuple of pat list - | Por of pat * pat - | Pas of pat * ident - - type is_rec = bool - - type binop = Band | Bor | Beq - - type ity = I of Ity.ity | C of Ity.cty (* TODO: keep it like this? *) - - type expr = { - e_node : expr_node; - e_ity : ity; - e_effect : effect; - } - - and expr_node = - | Econst of Number.integer_constant - | Evar of pvsymbol - | Eapp of rsymbol * expr list - | Efun of var list * expr - | Elet of let_def * expr - | Eif of expr * expr * expr - | Eassign of (pvsymbol * rsymbol * pvsymbol) list - | Ematch of expr * (pat * expr) list - | Eblock of expr list - | Ewhile of expr * expr - (* For loop for Why3's type int *) - | Efor of pvsymbol * pvsymbol * for_direction * pvsymbol * expr - | Eraise of xsymbol * expr option - | Etry of expr * (xsymbol * pvsymbol list * expr) list - | Eignore of expr - | Eabsurd - | Ehole - - and let_def = - | Lvar of pvsymbol * expr - | Lsym of rsymbol * ty * var list * expr - | Lrec of rdef list - - and rdef = { - rec_sym : rsymbol; (* exported *) - rec_rsym : rsymbol; (* internal *) - rec_args : var list; - rec_exp : expr; - rec_res : ty; - rec_svar : Stv.t; (* set of type variables *) - } - - type is_mutable = bool - - type typedef = - | Ddata of (ident * ty list) list - | Drecord of (is_mutable * ident * ty) list - | Dalias of ty - - type its_defn = { - its_name : ident; - its_args : tvsymbol list; - its_private : bool; - its_def : typedef option; - } - - type decl = - | Dtype of its_defn list - | Dlet of let_def - | Dexn of xsymbol * ty option - | Dclone of ident * decl list -(* - | Dfunctor of ident * (ident * decl list) list * decl list -*) - - type known_map = decl Mid.t - - type from_module = { - from_mod: Pmodule.pmodule option; - from_km : Pdecl.known_map; - } - - type pmodule = { - mod_from : from_module; - mod_decl : decl list; - mod_known : known_map; - } + open Mltree let get_decl_name = function | Dtype itdefl -> List.map (fun {its_name = id} -> id) itdefl @@ -234,6 +131,11 @@ module ML = struct | Eraise (xs, Some e) -> f xs.xs_name; iter_deps_expr f e + | Eexn (_xs, None, e) -> (* FIXME? How come we never do binding here? *) + iter_deps_expr f e + | Eexn (_xs, Some ty, e) -> (* FIXME? How come we never do binding here? *) + iter_deps_ty f ty; + iter_deps_expr f e | Etry (e, xbranchl) -> iter_deps_expr f e; List.iter (iter_deps_xbranch f) xbranchl @@ -304,6 +206,7 @@ module ML = struct end + (** Translation from Mlw to ML *) module Translate = struct @@ -319,35 +222,21 @@ module Translate = struct let rec type_ ty = match ty.ty_node with | Tyvar tvs -> - ML.Tvar tvs + Mltree.Tvar tvs | Tyapp (ts, tyl) when is_ts_tuple ts -> - ML.Ttuple (List.map type_ tyl) + Mltree.Ttuple (List.map type_ tyl) | Tyapp (ts, tyl) -> - ML.Tapp (ts.ts_name, List.map type_ tyl) + Mltree.Tapp (ts.ts_name, List.map type_ tyl) let vsty vs = vs.vs_name, type_ vs.vs_ty - let type_args = (* point-free *) - List.map (fun x -> x.tv_name) - let rec filter_ghost_params p def = function | [] -> [] | pv :: l -> if p pv then def pv :: (filter_ghost_params p def l) else filter_ghost_params p def l - let filter2_ghost_params p def al l = - let rec filter2_ghost_params_cps l k = - match l with - | [] -> k [] - | [e] -> k (if p e then [def e] else [al e]) - | e :: r -> - filter2_ghost_params_cps r - (fun fr -> k (if p e then (def e) :: fr else fr)) - in - filter2_ghost_params_cps l (fun x -> x) - let rec filter_out_ghost_rdef = function | [] -> [] | { rec_sym = rs; rec_rsym = rrs } :: l @@ -357,25 +246,25 @@ module Translate = struct let rec pat p = match p.pat_node with | Pwild -> - ML.Pwild + Mltree.Pwild | Pvar vs when (restore_pv vs).pv_ghost -> - ML.Pwild + Mltree.Pwild | Pvar vs -> - ML.Pvar vs + Mltree.Pvar vs | Por (p1, p2) -> - ML.Por (pat p1, pat p2) + Mltree.Por (pat p1, pat p2) | Pas (p, vs) when (restore_pv vs).pv_ghost -> pat p | Pas (p, vs) -> - ML.Pas (pat p, vs.vs_name) + Mltree.Pas (pat p, vs) | Papp (ls, pl) when is_fs_tuple ls -> - ML.Ptuple (List.map pat pl) + Mltree.Ptuple (List.map pat pl) | Papp (ls, pl) -> let rs = restore_rs ls in let args = rs.rs_cty.cty_args in let mk acc pv pp = if not pv.pv_ghost then pat pp :: acc else acc in let pat_pl = List.fold_left2 mk [] args pl in - ML.Papp (ls, List.rev pat_pl) + Mltree.Papp (ls, List.rev pat_pl) (** programs *) @@ -385,26 +274,26 @@ module Translate = struct let rec ity t = match t.ity_node with | Ityvar (tvs, _) -> - ML.Tvar tvs + Mltree.Tvar tvs | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts -> - ML.Ttuple (List.map ity itl) + Mltree.Ttuple (List.map ity itl) | Ityapp ({its_ts = ts}, itl, _) -> - ML.Tapp (ts.ts_name, List.map ity itl) + Mltree.Tapp (ts.ts_name, List.map ity itl) | Ityreg {reg_its = its; reg_args = args} -> let args = List.map ity args in - ML.Tapp (its.its_ts.ts_name, args) + Mltree.Tapp (its.its_ts.ts_name, args) let pvty pv = if pv.pv_ghost then ML.mk_var (pv_name pv) ML.tunit true else let (vs, vs_ty) = vsty pv.pv_vs in ML.mk_var vs vs_ty false - let for_direction = function - | To -> ML.To - | DownTo -> ML.DownTo + (* let for_direction = function *) + (* | To -> Mltree.To *) + (* | DownTo -> Mltree.DownTo *) let isconstructor info rs = - match Mid.find_opt rs.rs_name info.ML.from_km with + match Mid.find_opt rs.rs_name info.Mltree.from_km with | Some {pd_node = PDtype its} -> let is_constructor its = List.exists (rs_equal rs) its.itd_constructors in @@ -422,7 +311,7 @@ module Translate = struct | _ -> false let get_record_itd info rs = - match Mid.find_opt rs.rs_name info.ML.from_km with + match Mid.find_opt rs.rs_name info.Mltree.from_km with | Some {pd_node = PDtype itdl} -> let f pjl_constr = List.exists (rs_equal rs) pjl_constr in let itd = match rs.rs_field with @@ -450,15 +339,15 @@ module Translate = struct let def pv = pv_name pv, ity pv.pv_ity, pv.pv_ghost in filter_ghost_params pv_not_ghost def cty_app.cty_args in let args = - let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in + let def pv = ML.mk_expr (Mltree.Evar pv) (Mltree.I pv.pv_ity) eff_empty in let args = filter_ghost_params pv_not_ghost def pvl in let extra_args = (* FIXME : ghost status in this extra arguments *) List.map def cty_app.cty_args in args @ extra_args in - let eapp = - ML.mk_expr (ML.Eapp (rsc, args)) (ML.C cty_app) cty_app.cty_effect in - ML.mk_expr (ML.Efun (args_f, eapp)) (ML.C cty_app) cty_app.cty_effect + let eapp = ML.mk_expr (Mltree.Eapp (rsc, args)) (Mltree.C cty_app) + cty_app.cty_effect in + ML.mk_expr (Mltree.Efun (args_f, eapp)) (Mltree.C cty_app) cty_app.cty_effect (* function arguments *) let filter_params args = @@ -481,67 +370,67 @@ module Translate = struct in loop (pvl, cty_args) let app pvl cty_args = - let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in + let def pv = ML.mk_expr (Mltree.Evar pv) (Mltree.I pv.pv_ity) eff_empty in filter_params_cty pv_not_ghost def pvl cty_args let mk_for op_b_rs op_a_rs i_pv from_pv to_pv body_expr eff = let i_expr, from_expr, to_expr = let int_ity = ML.ity_int in let eff_e = eff_empty in - ML.mk_expr (ML.Evar i_pv) int_ity eff_e, - ML.mk_expr (ML.Evar from_pv) int_ity eff_e, - ML.mk_expr (ML.Evar to_pv) int_ity eff_e in + ML.mk_expr (Mltree.Evar i_pv) int_ity eff_e, + ML.mk_expr (Mltree.Evar from_pv) int_ity eff_e, + ML.mk_expr (Mltree.Evar to_pv) int_ity eff_e in let for_rs = let for_id = id_fresh "for_loop_to" in let for_cty = create_cty [i_pv] [] [] Mxs.empty Mpv.empty eff ity_unit in create_rsymbol for_id for_cty in let for_expr = - let test = ML.mk_expr (ML.Eapp (op_b_rs, [i_expr; to_expr])) - (ML.I ity_bool) eff_empty in + let test = ML.mk_expr (Mltree.Eapp (op_b_rs, [i_expr; to_expr])) + (Mltree.I ity_bool) eff_empty in let next_expr = let one_const = Number.int_const_dec "1" in let one_expr = - ML.mk_expr (ML.Econst one_const) ML.ity_int eff_empty in - let i_op_one = ML.Eapp (op_a_rs, [i_expr; one_expr]) in + ML.mk_expr (Mltree.Econst one_const) ML.ity_int eff_empty in + let i_op_one = Mltree.Eapp (op_a_rs, [i_expr; one_expr]) in ML.mk_expr i_op_one ML.ity_int eff_empty in let rec_call = - ML.mk_expr (ML.Eapp (for_rs, [next_expr])) + ML.mk_expr (Mltree.Eapp (for_rs, [next_expr])) ML.ity_unit eff in let seq_expr = ML.mk_expr (ML.eseq body_expr rec_call) ML.ity_unit eff in - ML.mk_expr (ML.Eif (test, seq_expr, ML.mk_unit)) ML.ity_unit eff in + ML.mk_expr (Mltree.Eif (test, seq_expr, ML.mk_unit)) ML.ity_unit eff in let ty_int = ity ity_int in let for_call_expr = - let for_call = ML.Eapp (for_rs, [from_expr]) in + let for_call = Mltree.Eapp (for_rs, [from_expr]) in ML.mk_expr for_call ML.ity_unit eff in let pv_name pv = pv.pv_vs.vs_name in let args = [ pv_name i_pv, ty_int, false ] in let for_rec_def = { - ML.rec_sym = for_rs; ML.rec_args = args; - ML.rec_rsym = for_rs; ML.rec_exp = for_expr; - ML.rec_res = ML.tunit; ML.rec_svar = Stv.empty; + Mltree.rec_sym = for_rs; Mltree.rec_args = args; + Mltree.rec_rsym = for_rs; Mltree.rec_exp = for_expr; + Mltree.rec_res = ML.tunit; Mltree.rec_svar = Stv.empty; } in - let for_let = ML.Elet (ML.Lrec [for_rec_def], for_call_expr) in + let for_let = Mltree.Elet (Mltree.Lrec [for_rec_def], for_call_expr) in ML.mk_expr for_let ML.ity_unit eff let mk_for_downto info i_pv from_pv to_pv body eff = let ge_rs, minus_rs = - let ns = (Opt.get info.ML.from_mod).mod_export in + let ns = (Opt.get info.Mltree.from_mod).mod_export in ns_find_rs ns ["Int"; "infix >="], ns_find_rs ns ["Int"; "infix -"] in mk_for ge_rs minus_rs i_pv from_pv to_pv body eff let mk_for_to info i_pv from_pv to_pv body eff = let le_rs, plus_rs = - let ns = (Opt.get info.ML.from_mod).mod_export in + let ns = (Opt.get info.Mltree.from_mod).mod_export in ns_find_rs ns ["Int"; "infix <="], ns_find_rs ns ["Int"; "infix +"] in mk_for le_rs plus_rs i_pv from_pv to_pv body eff - exception ExtractionAny + (* exception ExtractionAny *) (* build the set of type variables from functions arguments *) let rec add_tvar acc = function - | ML.Tvar tv -> Stv.add tv acc - | ML.Tapp (_, tyl) | ML.Ttuple tyl -> + | Mltree.Tvar tv -> Stv.add tv acc + | Mltree.Tapp (_, tyl) | Mltree.Ttuple tyl -> List.fold_left add_tvar acc tyl (* expressions *) @@ -550,9 +439,9 @@ module Translate = struct match e.e_node with | Econst c -> let c = match c with Number.ConstInt c -> c | _ -> assert false in - ML.mk_expr (ML.Econst c) (ML.I e.e_ity) eff + ML.mk_expr (Mltree.Econst c) (Mltree.I e.e_ity) eff | Evar pv -> - ML.mk_expr (ML.Evar pv) (ML.I e.e_ity) eff + ML.mk_expr (Mltree.Evar pv) (Mltree.I e.e_ity) eff | Elet (LDvar (_, e1), e2) when e_ghost e1 -> expr info e2 | Elet (LDvar (_, e1), e2) when e_ghost e2 -> @@ -561,10 +450,10 @@ module Translate = struct when pv.pv_ghost || not (Mpv.mem pv e2.e_effect.eff_reads) -> if eff_pure e1.e_effect then expr info e2 else let e1 = ML.mk_ignore (expr info e1) in - ML.mk_expr (ML.eseq e1 (expr info e2)) (ML.I e.e_ity) eff + ML.mk_expr (ML.eseq e1 (expr info e2)) (Mltree.I e.e_ity) eff | Elet (LDvar (pv, e1), e2) -> let ml_let = ML.mk_let_var pv (expr info e1) (expr info e2) in - ML.mk_expr ml_let (ML.I e.e_ity) eff + ML.mk_expr ml_let (Mltree.I e.e_ity) eff | Elet (LDsym (rs, _), ein) when rs_ghost rs -> expr info ein | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) -> @@ -572,8 +461,8 @@ module Translate = struct let ef = expr info ef in let ein = expr info ein in let res = ity cty.cty_result in - let ml_letrec = ML.Elet (ML.Lsym (rs, res, args, ef), ein) in - ML.mk_expr ml_letrec (ML.I e.e_ity) eff + let ml_letrec = Mltree.Elet (Mltree.Lsym (rs, res, args, ef), ein) in + ML.mk_expr ml_letrec (Mltree.I e.e_ity) eff | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) when isconstructor info rs_app -> (* partial application of constructor *) @@ -582,18 +471,18 @@ module Translate = struct let mk_func pv f = ity_func pv.pv_ity f in let func = List.fold_right mk_func cty.cty_args cty.cty_result in let res = ity func in - let ml_letrec = ML.Elet (ML.Lsym (rsf, res, [], eta_app), ein) in - ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect + let ml_letrec = Mltree.Elet (Mltree.Lsym (rsf, res, [], eta_app), ein) in + ML.mk_expr ml_letrec (Mltree.I e.e_ity) e.e_effect | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) -> (* partial application *) let pvl = app pvl rs_app.rs_cty.cty_args in let eapp = - ML.mk_expr (ML.Eapp (rs_app, pvl)) (ML.C cty) cty.cty_effect in + ML.mk_expr (Mltree.Eapp (rs_app, pvl)) (Mltree.C cty) cty.cty_effect in let ein = expr info ein in let res = ity cty.cty_result in let args = params cty.cty_args in - let ml_letrec = ML.Elet (ML.Lsym (rsf, res, args, eapp), ein) in - ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect + let ml_letrec = Mltree.Elet (Mltree.Lsym (rsf, res, args, eapp), ein) in + ML.mk_expr ml_letrec (Mltree.I e.e_ity) e.e_effect | Elet (LDrec rdefl, ein) -> let rdefl = filter_out_ghost_rdef rdefl in let def = function @@ -606,14 +495,14 @@ module Translate = struct let svar = List.fold_left add_tvar Stv.empty args' in add_tvar svar res in let ef = expr info ef in - { ML.rec_sym = rs1; ML.rec_rsym = rs2; - ML.rec_args = args; ML.rec_exp = ef ; - ML.rec_res = res; ML.rec_svar = svar; } + { Mltree.rec_sym = rs1; Mltree.rec_rsym = rs2; + Mltree.rec_args = args; Mltree.rec_exp = ef ; + Mltree.rec_res = res; Mltree.rec_svar = svar; } | _ -> assert false in let rdefl = List.map def rdefl in if rdefl <> [] then - let ml_letrec = ML.Elet (ML.Lrec rdefl, expr info ein) in - ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect + let ml_letrec = Mltree.Elet (Mltree.Lrec rdefl, expr info ein) in + ML.mk_expr ml_letrec (Mltree.I e.e_ity) e.e_effect else expr info ein | Eexec ({c_node = Capp (rs, [])}, _) when is_rs_tuple rs -> ML.mk_unit @@ -629,64 +518,69 @@ module Translate = struct let pvl = app pvl rs.rs_cty.cty_args in begin match pvl with | [pv_expr] when is_optimizable_record_rs info rs -> pv_expr - | _ -> ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff end + | _ -> ML.mk_expr (Mltree.Eapp (rs, pvl)) (Mltree.I e.e_ity) eff end | Eexec ({c_node = Cfun e; c_cty = {cty_args = []}}, _) -> (* abstract block *) expr info e | Eexec ({c_node = Cfun e; c_cty = cty}, _) -> let args = params cty.cty_args in - ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff + ML.mk_expr (Mltree.Efun (args, expr info e)) (Mltree.I e.e_ity) eff | Eexec ({c_node = Cany}, _) -> (* raise ExtractionAny *) ML.mk_hole | Eabsurd -> - ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff + ML.mk_expr Mltree.Eabsurd (Mltree.I e.e_ity) eff | Ecase (e1, _) when e_ghost e1 -> ML.mk_unit | Ecase (e1, pl) -> let e1 = expr info e1 in let pl = List.map (ebranch info) pl in - ML.mk_expr (ML.Ematch (e1, pl)) (ML.I e.e_ity) eff + ML.mk_expr (Mltree.Ematch (e1, pl)) (Mltree.I e.e_ity) eff | Eassert _ -> ML.mk_unit | Eif (e1, e2, e3) when e_ghost e3 -> let e1 = expr info e1 in let e2 = expr info e2 in - ML.mk_expr (ML.Eif (e1, e2, ML.mk_unit)) (ML.I e.e_ity) eff + ML.mk_expr (Mltree.Eif (e1, e2, ML.mk_unit)) (Mltree.I e.e_ity) eff | Eif (e1, e2, e3) when e_ghost e2 -> let e1 = expr info e1 in let e3 = expr info e3 in - ML.mk_expr (ML.Eif (e1, ML.mk_unit, e3)) (ML.I e.e_ity) eff + ML.mk_expr (Mltree.Eif (e1, ML.mk_unit, e3)) (Mltree.I e.e_ity) eff | Eif (e1, e2, e3) -> let e1 = expr info e1 in let e2 = expr info e2 in let e3 = expr info e3 in - ML.mk_expr (ML.Eif (e1, e2, e3)) (ML.I e.e_ity) eff + ML.mk_expr (Mltree.Eif (e1, e2, e3)) (Mltree.I e.e_ity) eff | Ewhile (e1, _, _, e2) -> let e1 = expr info e1 in let e2 = expr info e2 in - ML.mk_expr (ML.Ewhile (e1, e2)) (ML.I e.e_ity) eff - | Efor (pv1, (pv2, To, pv3), _, efor) -> + ML.mk_expr (Mltree.Ewhile (e1, e2)) (Mltree.I e.e_ity) eff + | Efor (pv1, (pv2, To, pv3), _, _, efor) -> let efor = expr info efor in mk_for_to info pv1 pv2 pv3 efor eff - | Efor (pv1, (pv2, DownTo, pv3), _, efor) -> + | Efor (pv1, (pv2, DownTo, pv3), _, _, efor) -> let efor = expr info efor in mk_for_downto info pv1 pv2 pv3 efor eff | Eghost _ -> assert false | Eassign al -> - ML.mk_expr (ML.Eassign al) (ML.I e.e_ity) eff + ML.mk_expr (Mltree.Eassign al) (Mltree.I e.e_ity) eff | Epure _ -> (* assert false (\*TODO*\) *) ML.mk_hole | Etry (etry, pvl_e_map) -> let etry = expr info etry in let bl = let bl_map = Mxs.bindings pvl_e_map in List.map (fun (xs, (pvl, e)) -> xs, pvl, expr info e) bl_map in - ML.mk_expr (ML.Etry (etry, bl)) (ML.I e.e_ity) eff + ML.mk_expr (Mltree.Etry (etry, bl)) (Mltree.I e.e_ity) eff | Eraise (xs, ex) -> let ex = match expr info ex with - | {ML.e_node = ML.Eblock []} -> None + | {Mltree.e_node = Mltree.Eblock []} -> None | e -> Some e in - ML.mk_expr (ML.Eraise (xs, ex)) (ML.I e.e_ity) eff + ML.mk_expr (Mltree.Eraise (xs, ex)) (Mltree.I e.e_ity) eff + | Eexn (xs, e1) -> + let e1 = expr info e1 in + let ty = if ity_equal xs.xs_ity ity_unit + then None else Some (ity xs.xs_ity) in + ML.mk_expr (Mltree.Eexn (xs, ty, e1)) (Mltree.I e.e_ity) eff | Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _) (* assert false (\*TODO*\) *) | Eexec ({c_node=Cpur (_, _); _ }, _) -> ML.mk_hole @@ -695,9 +589,6 @@ module Translate = struct and ebranch info ({pp_pat = p}, e) = (pat p, expr info e) - let its_args ts = ts.its_ts.ts_args - let itd_name td = td.itd_its.its_ts.ts_name - (* type declarations/definitions *) let tdef itd = let s = itd.itd_its in @@ -720,23 +611,24 @@ module Translate = struct ML.mk_its_defn id args is_private None | NoDef, cl, [] -> let cl = ddata_constructs cl in - ML.mk_its_defn id args is_private (Some (ML.Ddata cl)) + ML.mk_its_defn id args is_private (Some (Mltree.Ddata cl)) | NoDef, _, pjl -> let p e = not (rs_ghost e) in let pjl = filter_ghost_params p drecord_fields pjl in begin match pjl with - | [] -> ML.mk_its_defn id args is_private (Some (ML.Dalias ML.tunit)) + | [] -> ML.mk_its_defn id args is_private + (Some (Mltree.Dalias ML.tunit)) | [_, _, ty_pj] when is_optimizable_record_itd itd -> - ML.mk_its_defn id args is_private (Some (ML.Dalias ty_pj)) - | pjl -> ML.mk_its_defn id args is_private (Some (ML.Drecord pjl)) + ML.mk_its_defn id args is_private (Some (Mltree.Dalias ty_pj)) + | pjl -> ML.mk_its_defn id args is_private (Some (Mltree.Drecord pjl)) end | Alias t, _, _ -> - ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t))) + ML.mk_its_defn id args is_private (Some (Mltree.Dalias (ity t))) | Range _, _, _ -> assert false (* TODO *) | Float _, _, _ -> assert false (* TODO *) end - exception ExtractionVal of rsymbol + (* exception ExtractionVal of rsymbol *) let is_val = function | Eexec ({c_node = Cany}, _) -> true @@ -755,7 +647,7 @@ module Translate = struct | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) -> let args = params cty.cty_args in let res = ity cty.cty_result in - [ML.Dlet (ML.Lsym (rs, res, args, expr info e))] + [Mltree.Dlet (Mltree.Lsym (rs, res, args, expr info e))] | PDlet (LDrec rl) -> let rl = filter_out_ghost_rdef rl in let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} = @@ -766,27 +658,27 @@ module Translate = struct let args' = List.map (fun (_, ty, _) -> ty) args in let svar = List.fold_left add_tvar Stv.empty args' in add_tvar svar res in - { ML.rec_sym = rs1; ML.rec_rsym = rs2; - ML.rec_args = args; ML.rec_exp = expr info e; - ML.rec_res = res; ML.rec_svar = svar; } in - if rl = [] then [] else [ML.Dlet (ML.Lrec (List.map def rl))] + { Mltree.rec_sym = rs1; Mltree.rec_rsym = rs2; + Mltree.rec_args = args; Mltree.rec_exp = expr info e; + Mltree.rec_res = res; Mltree.rec_svar = svar; } in + if rl = [] then [] else [Mltree.Dlet (Mltree.Lrec (List.map def rl))] | PDlet (LDsym _) | PDpure | PDlet (LDvar _) -> [] | PDtype itl -> let itsd = List.map tdef itl in - [ML.Dtype itsd] + [Mltree.Dtype itsd] | PDexn xs -> - if ity_equal xs.xs_ity ity_unit then [ML.Dexn (xs, None)] - else [ML.Dexn (xs, Some (ity xs.xs_ity))] + if ity_equal xs.xs_ity ity_unit then [Mltree.Dexn (xs, None)] + else [Mltree.Dexn (xs, Some (ity xs.xs_ity))] let pdecl_m m pd = - let info = { ML.from_mod = Some m; ML.from_km = m.mod_known; } in + let info = { Mltree.from_mod = Some m; Mltree.from_km = m.mod_known; } in pdecl Sid.empty info pd (* unit module declarations *) let rec mdecl pids info = function | Udecl pd -> pdecl pids info pd - | Uscope (_, _, l) -> List.concat (List.map (mdecl pids info) l) + | Uscope (_, l) -> List.concat (List.map (mdecl pids info) l) | Uuse _ | Uclone _ | Umeta _ -> [] let abstract_or_alias_type itd = @@ -800,7 +692,7 @@ module Translate = struct let rec empty_munit = function | Udecl pd -> empty_pdecl pd | Uclone mi -> List.for_all empty_munit mi.mi_mod.mod_units - | Uscope (_, _, l) -> List.for_all empty_munit l + | Uscope (_, l) -> List.for_all empty_munit l | Uuse _ | Umeta _ -> true let is_empty_clone mi = @@ -825,14 +717,14 @@ module Translate = struct Format.printf "param %s@." id.id_string; let dl = List.concat (List.map (mdecl Sid.empty from) mi.mi_mod.mod_units) in - ML.Dclone (id, dl) + Mltree.Dclone (id, dl) let ids_of_params pids mi = Mid.fold (fun id _ pids -> Sid.add id pids) mi.mi_mod.mod_known pids (* modules *) let module_ m = - let from = { ML.from_mod = Some m; ML.from_km = m.mod_known; } in + let from = { Mltree.from_mod = Some m; Mltree.from_km = m.mod_known; } in let params = find_params m.mod_units in let pids = List.fold_left ids_of_params Sid.empty params in let mod_decl = List.concat (List.map (mdecl pids from) m.mod_units) in @@ -840,16 +732,19 @@ module Translate = struct let add known_map decl = let idl = ML.get_decl_name decl in List.fold_left (ML.add_known_decl decl) known_map idl in - let mod_known = List.fold_left add Mid.empty mod_decl in - { ML.mod_from = from; ML.mod_decl = mod_decl; ML.mod_known = mod_known } - - let () = Exn_printer.register (fun fmt e -> match e with - | ExtractionAny -> - Format.fprintf fmt "Cannot extract an undefined node" - | ExtractionVal rs -> - Format.fprintf fmt "Function %a cannot be extracted" - print_rs rs - | _ -> raise e) + let mod_known = List.fold_left add Mid.empty mod_decl in { + Mltree.mod_from = from; + Mltree.mod_decl = mod_decl; + Mltree.mod_known = mod_known + } + + (* let () = Exn_printer.register (fun fmt e -> match e with *) + (* | ExtractionAny -> *) + (* Format.fprintf fmt "Cannot extract an undefined node" *) + (* | ExtractionVal rs -> *) + (* Format.fprintf fmt "Function %a cannot be extracted" *) + (* print_rs rs *) + (* | _ -> raise e) *) end @@ -857,7 +752,7 @@ end module Transform = struct - open ML + open Mltree let no_reads_writes_conflict spv spv_mreg = let is_not_write {pv_ity = ity} = match ity.ity_node with @@ -865,7 +760,7 @@ module Transform = struct | _ -> true in Spv.for_all is_not_write spv - type subst = expr Mpv.t + (* type subst = expr Mpv.t *) let mk_list_eb ebl f = let mk_acc e (e_acc, s_acc) = @@ -913,6 +808,9 @@ module Transform = struct let e2, s2 = expr info subst e2 in let e3, s3 = expr info subst e3 in mk (Eif (e1, e2, e3)), Spv.union (Spv.union s1 s2) s3 + | Eexn (xs, ty, e1) -> + let e1, s1 = expr info subst e1 in + mk (Eexn (xs, ty, e1)), s1 | Ematch (e, bl) -> let e, spv = expr info subst e in let e_bl, spv_bl = mk_list_eb bl (branch info subst) in @@ -981,15 +879,9 @@ module Transform = struct let module_ m = let mod_decl = List.map (pdecl m.mod_from) m.mod_decl in let add known_map decl = - let idl = get_decl_name decl in + let idl = ML.get_decl_name decl in List.fold_left (ML.add_known_decl decl) known_map idl in let mod_known = List.fold_left add Mid.empty mod_decl in { m with mod_decl = mod_decl; mod_known = mod_known } end - -(* - * Local Variables: - * compile-command: "make -C ../.. -j3 bin/why3extract.opt" - * End: - *) diff --git a/src/mlw/compile.mli b/src/mlw/compile.mli new file mode 100644 index 0000000000000000000000000000000000000000..ef9e7f0a6e7ef57a547dd807fb9318476d50d510 --- /dev/null +++ b/src/mlw/compile.mli @@ -0,0 +1,21 @@ +open Ident + +val clean_name : string -> string + +val module_name : ?fname:string -> string list -> string -> string + +module ML : sig + val get_decl_name : Mltree.decl -> ident list + + val iter_deps : (Ident.ident -> unit) -> Mltree.decl -> unit +end + +module Translate : sig + val module_ : Pmodule.pmodule -> Mltree.pmodule + + val pdecl_m : Pmodule.pmodule -> Pdecl.pdecl -> Mltree.decl list +end + +module Transform : sig + val module_ : Mltree.pmodule -> Mltree.pmodule +end diff --git a/src/mlw/cprinter.ml b/src/mlw/cprinter.ml index 8da9060a42686d1899c888afc90c783754b210cf..819c8595ba57c56beaee772b2b69c7cbc0b94e79 100644 --- a/src/mlw/cprinter.ml +++ b/src/mlw/cprinter.ml @@ -872,7 +872,7 @@ module MLToC = struct open Term open Printer open Pmodule - open Compile.ML + open Mltree open C let rec ty_of_mlty info = function @@ -935,7 +935,7 @@ module MLToC = struct then Sreturn e else Sexpr e - let rec expr info env (e:Compile.ML.expr) : C.body = + let rec expr info env (e:Mltree.expr) : C.body = assert (not e.e_effect.eff_ghost); match e.e_node with | Eblock [] -> @@ -959,10 +959,10 @@ module MLToC = struct ([],return_or_expr env (C.Econst (Cint "1"))) | Eapp (rs, []) when rs_equal rs rs_false -> ([],return_or_expr env (C.Econst (Cint "0"))) - | Compile.ML.Evar pv -> + | Evar pv -> let e = C.Evar (pv_name pv) in ([], return_or_expr env e) - | Compile.ML.Econst ic -> + | Econst ic -> let n = Number.compute_int ic in let e = C.(Econst (Cint (BigInt.to_string n))) in ([], return_or_expr env e) @@ -1072,7 +1072,7 @@ module MLToC = struct | Lvar (pv,le) -> (* not a block *) begin match le.e_node with - | Compile.ML.Econst ic -> + | Econst ic -> let n = Number.compute_int ic in let ce = C.(Econst (Cint (BigInt.to_string n))) in if debug then Format.printf "propagate constant %s for var %s@." @@ -1150,7 +1150,7 @@ module MLToC = struct (fun (bs,rs) (xs, pvsl, r) -> let id = xs.xs_name in match pvsl, r.e_node with - | [pv], Compile.ML.Evar pv' + | [pv], Evar pv' when pv_equal pv pv' && env.computes_return_value -> (bs, Sid.add id rs) | [], (Eblock []) when is_unit r.e_ity && is_while -> @@ -1194,6 +1194,7 @@ module MLToC = struct | Eabsurd -> assert false | Eassign _ -> raise (Unsupported "assign") | Ehole -> assert false + | Eexn _ -> raise (Unsupported "exception") | Eignore e -> [], C.Sseq(C.Sblock(expr info {env with computes_return_value = false} e), if env.computes_return_value @@ -1278,18 +1279,25 @@ module MLToC = struct begin match idef with | Some (Dalias ty) -> Some (C.Dtypedef (ty_of_mlty info ty, id)) - | Some _ -> raise (Unsupported "Ddata/Drecord") + | Some _ -> if debug then Format.printf "Ddata/Drecord@."; + None (*FIXME unsupported*) | None -> begin match query_syntax info.syntax id with | Some _ -> None | None -> - raise (Unsupported "type declaration without syntax or alias") + if debug + then + Format.printf + "type declaration without syntax or alias: %s@." + id.id_string; + None (*FIXME*) + (* raise (Unsupported ("type declaration without syntax or alias: "^id.id_string)) *) end end | _ -> None (*TODO exn ? *) - let translate_decl (info:info) (d:Compile.ML.decl) : C.definition option + let translate_decl (info:info) (d:Mltree.decl) : C.definition option = let decide_print id = query_syntax info.syntax id = None in match Compile.ML.get_decl_name d with diff --git a/src/mlw/dexpr.ml b/src/mlw/dexpr.ml index 14ef8fdfc8970144a4b33fe47b5ae60655b0fb2a..8c178852d7f3d612f4c6921f8c2c63fcc8072521 100644 --- a/src/mlw/dexpr.ml +++ b/src/mlw/dexpr.ml @@ -15,6 +15,7 @@ open Ty open Term open Ity open Expr +open Pmodule (** Program types *) @@ -361,7 +362,7 @@ type dpattern_node = | DPapp of rsymbol * dpattern list | DPas of dpattern * preid * bool | DPor of dpattern * dpattern - | DPcast of dpattern * ity + | DPcast of dpattern * dity (** Specifications *) @@ -371,7 +372,7 @@ type dbinder = preid option * ghost * dity type register_old = pvsymbol -> string -> pvsymbol -type 'a later = pvsymbol Mstr.t -> register_old -> 'a +type 'a later = pvsymbol Mstr.t -> xsymbol Mstr.t -> register_old -> 'a (* specification terms are parsed and typechecked after the program expressions, when the types of locally bound program variables are already established. *) @@ -393,10 +394,17 @@ type dspec = ity -> dspec_final must have this type. All vsymbols in the exceptional postcondition clauses must have the type of the corresponding exception. *) +let old_mark = "'Old" +let old_mark_id = id_fresh old_mark + (** Expressions *) type dinvariant = term list +type dxsymbol = + | DElexn of string * dity + | DEgexn of xsymbol + type dexpr = { de_node : dexpr_node; de_dvty : dvty; @@ -405,13 +413,12 @@ type dexpr = { and dexpr_node = | DEvar of string * dvty - | DEpv of pvsymbol - | DErs of rsymbol + | DEsym of prog_symbol | DEls of lsymbol | DEconst of Number.constant * dity | DEapp of dexpr * dexpr - | DEfun of dbinder list * mask * dspec later * dexpr - | DEany of dbinder list * mask * dspec later * dity + | DEfun of dbinder list * dity * mask * dspec later * dexpr + | DEany of dbinder list * dity * mask * dspec later | DElet of dlet_defn * dexpr | DErec of drec_defn * dexpr | DEnot of dexpr @@ -422,16 +429,17 @@ and dexpr_node = | DEassign of (dexpr * rsymbol * dexpr) list | DEwhile of dexpr * dinvariant later * variant list later * dexpr | DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr - | DEtry of dexpr * (xsymbol * dpattern * dexpr) list - | DEraise of xsymbol * dexpr + | DEtry of dexpr * (dxsymbol * dpattern * dexpr) list + | DEraise of dxsymbol * dexpr | DEghost of dexpr + | DEexn of preid * dity * mask * dexpr | DEassert of assertion_kind * term later | DEpure of term later * dity | DEabsurd | DEtrue | DEfalse - | DEmark of preid * dexpr - | DEcast of dexpr * ity + | DEcast of dexpr * dity + | DEmark of preid * dity * dexpr | DEuloc of dexpr * Loc.position | DElabel of dexpr * Slab.t @@ -439,19 +447,20 @@ and dlet_defn = preid * ghost * rs_kind * dexpr and drec_defn = { fds : dfun_defn list } -and dfun_defn = preid * ghost * rs_kind * - dbinder list * mask * dspec later * variant list later * dexpr +and dfun_defn = preid * ghost * rs_kind * dbinder list * + dity * mask * dspec later * variant list later * dexpr (** Environment *) type denv = { frozen : dity list; - locals : (Stv.t option * dvty) Mstr.t; + locals : (bool * Stv.t option * dvty) Mstr.t; + excpts : dxsymbol Mstr.t } -let denv_contents d = d.locals +let denv_names d = Mstr.domain d.locals -let denv_empty = { frozen = []; locals = Mstr.empty } +let denv_empty = { frozen = []; locals = Mstr.empty; excpts = Mstr.empty } let is_frozen frozen v = try List.iter (occur_check v) frozen; false with Exit -> true @@ -474,25 +483,27 @@ let free_vars frozen (argl,res) = | Dapp (_,tl,_) -> List.fold_left add s tl in List.fold_left add (add Stv.empty res) argl -let denv_add_mono { frozen = frozen; locals = locals } id dvty = - let locals = Mstr.add id.pre_name (None, dvty) locals in - { frozen = freeze_dvty frozen dvty; locals = locals } +let denv_add_exn { frozen = fz; locals = ls; excpts = xs } id dity = + let xs = Mstr.add id.pre_name (DElexn (id.pre_name, dity)) xs in + { frozen = freeze_dvty fz ([], dity); locals = ls; excpts = xs } -let denv_add_poly { frozen = frozen; locals = locals } id dvty = - let ftvs = free_vars frozen dvty in - let locals = Mstr.add id.pre_name (Some ftvs, dvty) locals in - { frozen = frozen; locals = locals } +let denv_add_mono { frozen = fz; locals = ls; excpts = xs } id dvty = + let ls = Mstr.add id.pre_name (false, None, dvty) ls in + { frozen = freeze_dvty fz dvty; locals = ls; excpts = xs } -let denv_add_rec_mono { frozen = frozen; locals = locals } id dvty = - let locals = Mstr.add id.pre_name (Some Stv.empty, dvty) locals in - { frozen = freeze_dvty frozen dvty; locals = locals } +let denv_add_poly { frozen = fz; locals = ls; excpts = xs } id dvty = + let ls = Mstr.add id.pre_name (false, Some (free_vars fz dvty), dvty) ls in + { frozen = fz; locals = ls; excpts = xs } -let denv_add_rec_poly { frozen = frozen; locals = locals } frozen0 id dvty = - let ftvs = free_vars frozen0 dvty in - let locals = Mstr.add id.pre_name (Some ftvs, dvty) locals in - { frozen = frozen; locals = locals } +let denv_add_rec_mono { frozen = fz; locals = ls; excpts = xs } id dvty = + let ls = Mstr.add id.pre_name (false, Some Stv.empty, dvty) ls in + { frozen = freeze_dvty fz dvty; locals = ls; excpts = xs } -let denv_add_rec denv frozen0 id ((argl,res) as dvty) = +let denv_add_rec_poly { frozen = fz; locals = ls; excpts = xs } fz0 id dvty = + let ls = Mstr.add id.pre_name (false, Some (free_vars fz0 dvty), dvty) ls in + { frozen = fz; locals = ls; excpts = xs } + +let denv_add_rec denv fz0 id ((argl,res) as dvty) = let rec is_explicit = function | Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))} | Durg (d,_) -> is_explicit d @@ -500,38 +511,44 @@ let denv_add_rec denv frozen0 id ((argl,res) as dvty) = | Dutv _ -> true | Dapp (_,tl,_) -> List.for_all is_explicit tl in if List.for_all is_explicit argl && is_explicit res - then denv_add_rec_poly denv frozen0 id dvty + then denv_add_rec_poly denv fz0 id dvty else denv_add_rec_mono denv id dvty let denv_add_var denv id dity = denv_add_mono denv id ([], dity) +let denv_add_for_index denv id dvty = + let dvty = [], dity_of_dvty dvty in + let { frozen = fz; locals = ls; excpts = xs } = denv in + let ls = Mstr.add id.pre_name (true, None, dvty) ls in + { frozen = freeze_dvty fz dvty; locals = ls; excpts = xs } + let denv_add_let denv (id,_,_,({de_dvty = dvty} as de)) = if fst dvty = [] then denv_add_mono denv id dvty else let rec is_value de = match de.de_node with | DEghost de | DEuloc (de,_) | DElabel (de,_) -> is_value de - | DEvar _ | DErs _ | DEls _ | DEfun _ | DEany _ -> true + | DEvar _ | DEsym _ | DEls _ | DEfun _ | DEany _ -> true | _ -> false in if is_value de then denv_add_poly denv id dvty else denv_add_mono denv id dvty -let denv_add_args { frozen = frozen; locals = locals } bl = - let l = List.fold_left (fun l (_,_,t) -> t::l) frozen bl in +let denv_add_args { frozen = fz; locals = ls; excpts = xs } bl = + let l = List.fold_left (fun l (_,_,t) -> t::l) fz bl in let add s (id,_,t) = match id with | Some {pre_name = n} -> - Mstr.add_new (Dterm.DuplicateVar n) n (None, ([],t)) s + Mstr.add_new (Dterm.DuplicateVar n) n (false, None, ([],t)) s | None -> s in let s = List.fold_left add Mstr.empty bl in - { frozen = l; locals = Mstr.set_union s locals } + { frozen = l; locals = Mstr.set_union s ls; excpts = xs } -let denv_add_pat { frozen = frozen; locals = locals } dp = - let l = Mstr.fold (fun _ t l -> t::l) dp.dp_vars frozen in - let s = Mstr.map (fun t -> None, ([], t)) dp.dp_vars in - { frozen = l; locals = Mstr.set_union s locals } +let denv_add_pat { frozen = fz; locals = ls; excpts = xs } dp = + let l = Mstr.fold (fun _ t l -> t::l) dp.dp_vars fz in + let s = Mstr.map (fun t -> false, None, ([], t)) dp.dp_vars in + { frozen = l; locals = Mstr.set_union s ls; excpts = xs } let mk_node n = function - | Some tvs, dvty -> DEvar (n, specialize_scheme tvs dvty) - | None, dvty -> DEvar (n, dvty) + | _, Some tvs, dvty -> DEvar (n, specialize_scheme tvs dvty) + | _, None, dvty -> DEvar (n, dvty) let denv_get denv n = mk_node n (Mstr.find_exn (Dterm.UnboundVar n) n denv.locals) @@ -539,6 +556,12 @@ let denv_get denv n = let denv_get_opt denv n = Opt.map (mk_node n) (Mstr.find_opt n denv.locals) +exception UnboundExn of string + +let denv_get_exn denv n = Mstr.find_exn (UnboundExn n) n denv.excpts + +let denv_get_exn_opt denv n = Mstr.find_opt n denv.excpts + let denv_pure denv get_dty = let ht = Htv.create 3 in let hi = Hint.create 3 in @@ -550,9 +573,10 @@ let denv_pure denv get_dty = let f = Dterm.dty_fresh () in Htv.add ht v (f,d); f end | Dapp (s,dl,_) -> Dterm.dty_app s.its_ts (List.map fold dl) | Dutv v -> Dterm.dty_var v in - let pure_denv = Mstr.mapi (fun n (_, dvty) -> - Dterm.DTvar (n, fold (dity_of_dvty dvty))) denv.locals in - let dty = get_dty pure_denv in + let add n (idx, _, dvty) = + let dity = if idx then dity_int else dity_of_dvty dvty in + Dterm.DTvar (n, fold dity) in + let dty = get_dty (Mstr.mapi add denv.locals) in Htv.iter (fun v (f,_) -> try Dterm.dty_match f (ty_var v) with Exit -> ()) ht; let fnS s dl = dity_app_fresh (restore_its s) dl in @@ -602,21 +626,21 @@ let drec_defn denv0 prel = denv_add_rec denv denv0.frozen id (argl,res) in let denv1 = List.fold_left add denv0 prel in let parse (id,gh,pk,bl,res,msk,pre) = - let dsp, dvl, de = pre (denv_add_args denv1 bl) in + let dsp, dvl, de = pre denv1 in dexpr_expected_type de res; - (id,gh,pk,bl,msk,dsp,dvl,de) in + (id,gh,pk,bl,res,msk,dsp,dvl,de) in let fdl = List.map parse prel in - let add denv (id,_,_,bl,_,_,_,{de_dvty = dvty}) = + let add denv (id,_,_,bl,res,_,_,_,_) = (* just in case we linked some polymorphic type var to the outer context *) let check tv = if is_frozen denv0.frozen tv then Loc.errorm ?loc:id.pre_loc "This function is expected to be polymorphic in type variable %a" Pretty.print_tv tv in begin match Mstr.find_opt id.pre_name denv1.locals with - | Some (Some tvs, _) -> Stv.iter check tvs - | Some (None, _) | None -> assert false + | Some (_, Some tvs, _) -> Stv.iter check tvs + | Some (_, None, _) | None -> assert false end; let argl = List.map (fun (_,_,t) -> t) bl in - denv_add_poly denv id (argl, dity_of_dvty dvty) in + denv_add_poly denv id (argl, res) in List.fold_left add denv0 fdl, { fds = fdl } (** Constructors *) @@ -652,20 +676,32 @@ let dpattern ?loc node = let { dp_pat = pat; dp_dity = dity; dp_vars = vars } = dp in let vars = Mstr.add_new (Dterm.DuplicateVar n) n dity vars in mk_dpat (PPas (pat, id, gh)) dity vars - | DPcast (dp, ity) -> - dpat_expected_type dp (dity_of_ity ity); + | DPcast (dp, dity) -> + dpat_expected_type dp dity; dp in Loc.try1 ?loc dpat node +let specialize_dxs = function + | DEgexn xs -> specialize_xs xs + | DElexn (_,dity) -> dity + let dexpr ?loc node = let get_dvty = function | DEvar (_,dvty) -> dvty - | DEpv pv -> + | DEsym (PV pv) -> [], specialize_pv pv - | DErs rs -> + | DEsym (RS rs) -> specialize_rs rs + | DEsym (OO ss) -> + let dt = dity_fresh () in + let ot = overload_of_rs (Srs.choose ss) in + begin match ot with + | UnOp -> [dt], dt + | BinOp -> [dt;dt], dt + | BinRel -> [dt;dt], dity_bool + | NoOver -> assert false end | DEls ls -> specialize_ls ls | DEconst (_, ity) -> [],ity @@ -688,9 +724,10 @@ let dexpr ?loc node = end; dexpr_expected_type de2 a; [], r - | DEfun (bl,_,_,de) -> - List.map (fun (_,_,t) -> t) bl, dity_of_dvty de.de_dvty - | DEany (bl,_,_,res) -> + | DEfun (bl,res,_,_,de) -> + dexpr_expected_type de res; + List.map (fun (_,_,t) -> t) bl, res + | DEany (bl,res,_,_) -> List.map (fun (_,_,t) -> t) bl, res | DElet (_,de) | DErec (_,de) -> @@ -732,8 +769,9 @@ let dexpr ?loc node = dexpr_expected_type de2 dity_unit; dvty_unit | DEfor (_,de_from,_,de_to,_,de) -> - dexpr_expected_type de_from dity_int; - dexpr_expected_type de_to dity_int; + let bty = dity_fresh () in + dexpr_expected_type de_from bty; + dexpr_expected_type de_to bty; dexpr_expected_type de dity_unit; dvty_unit | DEtry (_,[]) -> @@ -742,12 +780,13 @@ let dexpr ?loc node = let res = dity_fresh () in dexpr_expected_type de res; List.iter (fun (xs,dp,de) -> - dpat_expected_type dp (specialize_xs xs); + dpat_expected_type dp (specialize_dxs xs); dexpr_expected_type de res) bl; [], res | DEraise (xs,de) -> - dexpr_expected_type de (specialize_xs xs); + dexpr_expected_type de (specialize_dxs xs); [], dity_fresh () + | DEexn (_,_,_,de) | DEghost de -> de.de_dvty | DEassert _ -> @@ -759,10 +798,10 @@ let dexpr ?loc node = | DEtrue | DEfalse -> dvty_bool - | DEcast (de,ity) -> - dexpr_expected_type de (dity_of_ity ity); + | DEcast (de,dity) + | DEmark (_,dity,de) -> + dexpr_expected_type de dity; de.de_dvty - | DEmark (_,de) | DEuloc (de,_) | DElabel (de,_) -> de.de_dvty in @@ -936,10 +975,17 @@ let check_spec inr dsp ecty ({e_loc = loc} as e) = let check_aliases recu c = let rds_regs = c.cty_freeze.isb_reg in let report r _ _ = - if Mreg.mem r rds_regs then let spv = Spv.filter + if Mreg.mem r rds_regs then + let spv = Spv.filter (fun v -> ity_r_occurs r v.pv_ity) (cty_reads c) in - Loc.errorm "The type of this function contains an alias with \ - external variable %a" print_pv (Spv.choose spv) + if not (Spv.is_empty spv) then Loc.errorm + "The type of this function contains an alias with \ + external variable %a" print_pv (Spv.choose spv); + let sxs = Sxs.filter + (fun xs -> ity_r_occurs r xs.xs_ity) (c.cty_effect.eff_raises) in + Loc.errorm + "The type of this function contains an alias with \ + external local exception %a" print_xs (Sxs.choose sxs) else Loc.errorm "The type of this function contains an alias" in (* we allow the value in a non-recursive function to contain regions coming the function's arguments, but not from the @@ -972,7 +1018,9 @@ let check_fun inr rsym dsp e = type env = { rsm : rsymbol Mstr.t; pvm : pvsymbol Mstr.t; + xsm : xsymbol Mstr.t; old : (pvsymbol Mstr.t * (let_defn * pvsymbol) Hpv.t) Mstr.t; + idx : pvsymbol Mpv.t; (* external-to-internal loop indexes *) ghs : bool; (* we are under DEghost or in a ghost function *) lgh : bool; (* we are under let ghost c = *) cgh : bool; (* we are under DEghost in a cexp *) @@ -982,7 +1030,9 @@ type env = { let env_empty = { rsm = Mstr.empty; pvm = Mstr.empty; + xsm = Mstr.empty; old = Mstr.empty; + idx = Mpv.empty; ghs = false; lgh = false; cgh = false; @@ -1012,7 +1062,10 @@ let find_old pvm (ovm,old) v = let register_old env v l = find_old env.pvm (Mstr.find_exn (UnboundLabel l) l env.old) v -let get_later env later = later env.pvm (register_old env) +let get_later env later = + let pvm = if Mpv.is_empty env.idx then env.pvm else + Mstr.map (fun v -> Mpv.find_def v v env.idx) env.pvm in + later pvm env.xsm (register_old env) let add_label ({pvm = pvm; old = old} as env) l = let ht = Hpv.create 3 in @@ -1023,7 +1076,7 @@ let rebase_old {pvm = pvm} preold old fvs = if not (Mvs.mem o fvs) then sbs else match preold with | Some preold -> Mvs.add o (t_var (find_old pvm preold v).pv_vs) sbs - | None -> raise (UnboundLabel "0") in + | None -> raise (UnboundLabel old_mark) in Hpv.fold rebase old Mvs.empty let rebase_pre env preold old pl = @@ -1058,14 +1111,17 @@ let add_pv_map ({pvm = pvm} as env) vm = let add_binders env pvl = List.fold_left add_pvsymbol env pvl +let add_xsymbol ({xsm = xsm} as env) xs = + { env with xsm = Mstr.add xs.xs_name.id_string xs xsm } + (** Abstract values *) let cty_of_spec env bl mask dspl dity = let ity = ity_of_dity dity in let bl = binders env.ghs bl in let env = add_binders env bl in - let preold = Mstr.find_opt "0" env.old in - let env, old = add_label env "0" in + let preold = Mstr.find_opt old_mark env.old in + let env, old = add_label env old_mark in let dsp = get_later env dspl ity in let ity, regs = alias_of_dspec dsp ity in let dsp = get_later env dspl ity in (* FIXME ? *) @@ -1101,12 +1157,31 @@ let rec strip uloc labs de = match de.de_node with let get_pv env n = Mstr.find_exn (Dterm.UnboundVar n) n env.pvm let get_rs env n = Mstr.find_exn (Dterm.UnboundVar n) n env.rsm +let get_xs env = function + | DElexn (n,_) -> Mstr.find_exn (UnboundExn n) n env.xsm + | DEgexn xs -> xs + let proxy_labels = Slab.singleton proxy_label type let_prexix = | LD of let_defn | EA of expr +let vl_of_mask id mask ity = + let mk_res m t = create_pvsymbol id ~ghost:(mask_ghost m) t in + if ity_equal ity ity_unit then [] else + match mask, ity.ity_node with + | MaskTuple ml, Ityapp (_,tl,_) -> List.map2 mk_res ml tl + | _ -> [mk_res mask ity] + +let t_of_vl = function + | [] -> t_void | [v] -> t_var v.pv_vs + | vl -> t_tuple (List.map (fun v -> t_var v.pv_vs) vl) + +let e_of_vl = function + | [] -> e_void | [v] -> e_var v + | vl -> e_tuple (List.map e_var vl) + let rec expr uloc env ({de_loc = loc} as de) = let uloc, labs, de = strip uloc Slab.empty de in let env = {env with lgh = false; cgh = false} in @@ -1154,6 +1229,21 @@ and try_cexp uloc env ({de_dvty = argl,res} as de0) lpl = let al = List.map (fun v -> v.pv_ghost) s.rs_cty.cty_args in let gh = env.ghs || env.lgh || rs_ghost s || all_ghost al lpl in apply c_app gh s al lpl in + let c_oop s lpl = + let al = (Srs.choose s).rs_cty.cty_args in + let al = List.map (fun _ -> false) al in + let gh = env.ghs || env.lgh || all_ghost al lpl in + let loc = Opt.get_def de0.de_loc uloc in + let app s vl al res = + let app s cl = try Expr.c_app s vl al res :: cl with + (* TODO: are there other valid exceptions here? *) + | TypeMismatch _ -> cl in + match Srs.fold app s [] with + | [c] -> c + | [] -> Loc.errorm ?loc "No suitable symbol found" + (* TODO: show types or locations for ambiguity *) + | _cl -> Loc.errorm ?loc "Ambiguous notation" in + apply app gh s al lpl in let c_pur s lpl = apply c_pur true s (List.map Util.ttrue s.ls_args) lpl in let proxy c = @@ -1167,7 +1257,8 @@ and try_cexp uloc env ({de_dvty = argl,res} as de0) lpl = c_app s (LD ld :: lpl) in match de0.de_node with | DEvar (n,_) -> c_app (get_rs env n) lpl - | DErs s -> c_app s lpl + | DEsym (RS s) -> c_app s lpl + | DEsym (OO s) -> c_oop s lpl | DEls s -> c_pur s lpl | DEapp (de1,de2) -> let e2 = e_ghostify env.cgh (expr uloc env de2) in @@ -1176,13 +1267,13 @@ and try_cexp uloc env ({de_dvty = argl,res} as de0) lpl = (* if we were not in the ghost context until now, then we must ghostify the let-definitions down from here *) cexp uloc {env with ghs = true; cgh = env.cgh || not env.ghs} de lpl - | DEfun (bl,msk,dsp,de) -> - let dvl _ _ = [] in + | DEfun (bl,_,msk,dsp,de) -> + let dvl _ _ _ = [] in let env = {env with ghs = env.ghs || env.lgh} in let c, dsp, _ = lambda uloc env (binders env.ghs bl) msk dsp dvl de in check_fun env.inr None dsp c; proxy c - | DEany (bl,msk,dsp,dity) -> + | DEany (bl,dity,msk,dsp) -> let env = {env with ghs = env.ghs || env.lgh} in proxy (c_any (cty_of_spec env bl msk dsp dity)) | DElet ((_,_,_,{de_dvty = ([],_)}) as dldf,de) -> @@ -1195,9 +1286,13 @@ and try_cexp uloc env ({de_dvty = argl,res} as de0) lpl = | DErec (drdf,de) -> let ld, env = rec_defn uloc env drdf in cexp uloc env de (LD ld :: lpl) + | DEexn _ -> + Loc.errorm "Local exception declarations are not allowed \ + over higher-order expressions" | DEmark _ -> - Loc.errorm "Marks are not allowed over higher-order expressions" - | DEpv _ | DEconst _ | DEnot _ | DEand _ | DEor _ | DEif _ | DEcase _ + Loc.errorm "Label declarations are not allowed \ + over higher-order expressions" + | DEsym _ | DEconst _ | DEnot _ | DEand _ | DEor _ | DEif _ | DEcase _ | DEassign _ | DEwhile _ | DEfor _ | DEtry _ | DEraise _ | DEassert _ | DEpure _ | DEabsurd | DEtrue | DEfalse -> assert false (* expr-only *) | DEcast _ | DEuloc _ | DElabel _ -> assert false (* already stripped *) @@ -1206,15 +1301,15 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) = match de0.de_node with | DEvar (n,_) when argl = [] -> e_var (get_pv env n) - | DEpv v -> + | DEsym (PV v) -> e_var v - | DEconst(c,dity) -> - e_const c (ity_of_dity dity) + | DEconst (c,dity) -> + e_const c (ity_of_dity dity) | DEapp ({de_dvty = ([],_)} as de1, de2) -> let e1 = expr uloc env de1 in let e2 = expr uloc env de2 in e_app rs_func_app [e1; e2] [] (ity_of_dity res) - | DEvar _ | DErs _ | DEls _ | DEapp _ | DEfun _ | DEany _ -> + | DEvar _ | DEsym _ | DEls _ | DEapp _ | DEfun _ | DEany _ -> let cgh,ldl,c = try_cexp uloc env de0 [] in let e = e_ghostify cgh (e_exec c) in List.fold_left e_let_check e ldl @@ -1267,14 +1362,19 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) = | DEfor (id,de_from,dir,de_to,dinv,de) -> let e_from = expr uloc env de_from in let e_to = expr uloc env de_to in - let v = create_pvsymbol id ity_int in + let v = create_pvsymbol id e_from.e_ity in let env = add_pvsymbol env v in + let i = if ity_equal v.pv_ity ity_int then v else + create_pvsymbol id ~ghost:true ity_int in + let env = if pv_equal i v then env else + { env with idx = Mpv.add v i env.idx } in let e = expr uloc env de in let inv = get_later env dinv in - e_for v e_from dir e_to (create_invariant inv) e + e_for v e_from dir e_to i (create_invariant inv) e | DEtry (de1,bl) -> let e1 = expr uloc env de1 in let add_branch m (xs,dp,de) = + let xs = get_xs env xs in let mask = if env.ghs then MaskGhost else xs.xs_mask in let vm, pat = create_prog_pattern dp.dp_pat xs.xs_ity mask in let e = expr uloc (add_pv_map env vm) de in @@ -1308,21 +1408,8 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) = List.map2 conv_simple pl (List.combine tyl ghl), e | bl -> let mask = if env.ghs then MaskGhost else xs.xs_mask in - let id = id_fresh "q" in - let vl = match mask with - | _ when ity_equal xs.xs_ity ity_unit -> [] - | MaskGhost -> [create_pvsymbol id ~ghost:true xs.xs_ity] - | MaskVisible -> [create_pvsymbol id ~ghost:false xs.xs_ity] - | MaskTuple ml -> - let mk_var ity m = - create_pvsymbol id ~ghost:(mask_ghost m) ity in - let tyl = match xs.xs_ity.ity_node with (* tuple *) - | Ityapp (_,tyl,_) -> tyl | _ -> assert false in - List.map2 mk_var tyl ml in - let t, e = match vl with - | [] -> t_void, e_void | [v] -> t_var v.pv_vs, e_var v - | vl -> t_tuple (List.map (fun v -> t_var v.pv_vs) vl), - e_tuple (List.map e_var vl) in + let vl = vl_of_mask (id_fresh "q") mask xs.xs_ity in + let t = t_of_vl vl and e = e_of_vl vl in let pl = List.rev_map (fun (p,_) -> [p.pp_pat]) bl in let bl = if Pattern.is_exhaustive [t] pl then bl else let _,pp = create_prog_pattern PPwild xs.xs_ity mask in @@ -1330,7 +1417,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) = vl, e_case e (List.rev bl) in e_try e1 (Mxs.mapi mk_branch xsm) | DEraise (xs,de) -> - e_raise xs (expr uloc env de) (ity_of_dity res) + e_raise (get_xs env xs) (expr uloc env de) (ity_of_dity res) | DEghost de -> e_ghostify true (expr uloc {env with ghs = true} de) | DEassert (ak,f) -> @@ -1343,10 +1430,21 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) = e_true | DEfalse -> e_false - | DEmark ({pre_name = l},de) -> - let env, old = add_label env l in + | DEexn (id,dity,mask,de) -> + let xs = create_xsymbol id ~mask (ity_of_dity dity) in + e_exn xs (expr uloc (add_xsymbol env xs) de) + | DEmark (id,dity,de) -> + let xs = create_xsymbol id (ity_of_dity dity) in + let env, old = add_label env id.pre_name in + let e = expr uloc (add_xsymbol env xs) de in + let e = if Sxs.mem xs e.e_effect.eff_raises then + let v = create_pvsymbol (id_fresh "result") xs.xs_ity in + (* FIXME? We assume that the generated exception will not + be catched inside e. Otherwise, it will not appear in + the effect and we will not declare the exception here. *) + e_exn xs (e_try e (Mxs.singleton xs ([v], e_var v))) else e in let put _ (ld,_) e = e_let ld e in - Hpv.fold put old (expr uloc env de) + Hpv.fold put old e | DEcast _ | DEuloc _ | DElabel _ -> assert false (* already stripped *) @@ -1366,10 +1464,10 @@ and sym_defn uloc env (id,gh,kind,de) = ld::ldl, add_rsymbol env s and rec_defn uloc ({inr = inr} as env) {fds = dfdl} = - let step1 env (id, gh, kind, bl, mask, dsp, dvl, ({de_dvty = dvty} as de)) = + let step1 env (id, gh, kind, bl, res, mask, dsp, dvl, de) = let ghost = env.ghs || gh || kind = RKlemma in let pvl = binders ghost bl in - let ity = Loc.try1 ?loc:de.de_loc ity_of_dity (dity_of_dvty dvty) in + let ity = Loc.try1 ?loc:de.de_loc ity_of_dity res in let cty = create_cty ~mask pvl [] [] Mxs.empty Mpv.empty eff_empty ity in let rs = create_rsymbol id ~ghost ~kind:RKnone cty in add_rsymbol env rs, (rs, kind, mask, dsp, dvl, de) in @@ -1401,9 +1499,16 @@ and rec_defn uloc ({inr = inr} as env) {fds = dfdl} = and lambda uloc env pvl mask dsp dvl de = let env = add_binders env pvl in - let preold = Mstr.find_opt "0" env.old in - let env, old = add_label env "0" in - let e = expr uloc env de in + let preold = Mstr.find_opt old_mark env.old in + let env, old = add_label env old_mark in + let e = if pvl = [] then expr uloc env de else + let ity = ity_of_dity (dity_of_dvty de.de_dvty) in + let xs = create_xsymbol old_mark_id ~mask ity in + let e = expr uloc (add_xsymbol env xs) de in + if not (Sxs.mem xs e.e_effect.eff_raises) then e else + let vl = vl_of_mask (id_fresh "r") mask xs.xs_ity in + let branches = Mxs.singleton xs (vl, e_of_vl vl) in + e_exn xs (e_try e branches) in let dsp = get_later env dsp e.e_ity in let dvl = get_later env dvl in let dvl = rebase_variant env preold old dvl in @@ -1417,7 +1522,7 @@ let rec_defn ?(keep_loc=true) drdf = fst (rec_defn uloc env_empty drdf) let rec mask_of_fun de = match de.de_node with - | DEfun (_,msk,_,_) -> msk + | DEfun (_,_,msk,_,_) -> msk | DEghost de | DEcast (de,_) | DEuloc (de,_) | DElabel (de,_) -> mask_of_fun de | _ -> MaskGhost (* a safe default for checking *) @@ -1470,4 +1575,6 @@ let expr ?(keep_loc=true) de = let () = Exn_printer.register (fun fmt e -> match e with | UnboundLabel s -> Format.fprintf fmt "unbound label %s" s + | UnboundExn s -> + Format.fprintf fmt "unbound exception %s" s | _ -> raise e) diff --git a/src/mlw/dexpr.mli b/src/mlw/dexpr.mli index dfbf5ec1ad8dfaf39706efece7037f51a6cfc0d8..87b760bfedd40dde7c7634e6fab7af6a4c45423a 100644 --- a/src/mlw/dexpr.mli +++ b/src/mlw/dexpr.mli @@ -14,6 +14,7 @@ open Ident open Term open Ity open Expr +open Pmodule (** Program types *) @@ -45,7 +46,7 @@ type dpattern_node = | DPapp of rsymbol * dpattern list | DPas of dpattern * preid * bool | DPor of dpattern * dpattern - | DPcast of dpattern * ity + | DPcast of dpattern * dity (** Binders *) @@ -57,11 +58,14 @@ type dbinder = preid option * ghost * dity exception UnboundLabel of string +val old_mark : string +val old_mark_id : preid + type register_old = pvsymbol -> string -> pvsymbol (** Program variables occurring under [old] or [at] are passed to a registrar function. The label string must be ["0"] for [old]. *) -type 'a later = pvsymbol Mstr.t -> register_old -> 'a +type 'a later = pvsymbol Mstr.t -> xsymbol Mstr.t -> register_old -> 'a (** Specification terms are parsed and typechecked after the program expressions, when the types of locally bound program variables are already established. *) @@ -87,6 +91,10 @@ type dspec = ity -> dspec_final type dinvariant = term list +type dxsymbol = + | DElexn of string * dity + | DEgexn of xsymbol + type dexpr = private { de_node : dexpr_node; de_dvty : dvty; @@ -95,13 +103,12 @@ type dexpr = private { and dexpr_node = | DEvar of string * dvty - | DEpv of pvsymbol - | DErs of rsymbol + | DEsym of prog_symbol | DEls of lsymbol | DEconst of Number.constant * dity | DEapp of dexpr * dexpr - | DEfun of dbinder list * mask * dspec later * dexpr - | DEany of dbinder list * mask * dspec later * dity + | DEfun of dbinder list * dity * mask * dspec later * dexpr + | DEany of dbinder list * dity * mask * dspec later | DElet of dlet_defn * dexpr | DErec of drec_defn * dexpr | DEnot of dexpr @@ -112,16 +119,17 @@ and dexpr_node = | DEassign of (dexpr * rsymbol * dexpr) list | DEwhile of dexpr * dinvariant later * variant list later * dexpr | DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr - | DEtry of dexpr * (xsymbol * dpattern * dexpr) list - | DEraise of xsymbol * dexpr + | DEtry of dexpr * (dxsymbol * dpattern * dexpr) list + | DEraise of dxsymbol * dexpr | DEghost of dexpr + | DEexn of preid * dity * mask * dexpr | DEassert of assertion_kind * term later | DEpure of term later * dity | DEabsurd | DEtrue | DEfalse - | DEmark of preid * dexpr - | DEcast of dexpr * ity + | DEcast of dexpr * dity + | DEmark of preid * dity * dexpr | DEuloc of dexpr * Loc.position | DElabel of dexpr * Slab.t @@ -129,8 +137,8 @@ and dlet_defn = preid * ghost * rs_kind * dexpr and drec_defn = private { fds : dfun_defn list } -and dfun_defn = preid * ghost * rs_kind * - dbinder list * mask * dspec later * variant list later * dexpr +and dfun_defn = preid * ghost * rs_kind * dbinder list * + dity * mask * dspec later * variant list later * dexpr (** Environment *) @@ -146,11 +154,19 @@ val denv_add_args : denv -> dbinder list -> denv val denv_add_pat : denv -> dpattern -> denv +val denv_add_for_index : denv -> preid -> dvty -> denv + +val denv_add_exn : denv -> preid -> dity -> denv + val denv_get : denv -> string -> dexpr_node (** raises UnboundVar *) val denv_get_opt : denv -> string -> dexpr_node option -val denv_contents : denv -> (Ty.Stv.t option * dvty) Mstr.t +val denv_get_exn : denv -> string -> dxsymbol (** raises Not_found *) + +val denv_get_exn_opt : denv -> string -> dxsymbol option + +val denv_names : denv -> Sstr.t val denv_pure : denv -> (Dterm.denv -> Dterm.dty) -> dity diff --git a/src/mlw/expr.ml b/src/mlw/expr.ml index 1007c84996f9f776f580dff5779584131e16216e..e16567b4c54b17e4f325732c7a0abd8061e62b2e 100644 --- a/src/mlw/expr.ml +++ b/src/mlw/expr.ml @@ -323,9 +323,10 @@ and expr_node = | Eif of expr * expr * expr | Ecase of expr * (prog_pattern * expr) list | Ewhile of expr * invariant list * variant list * expr - | Efor of pvsymbol * for_bounds * invariant list * expr + | Efor of pvsymbol * for_bounds * pvsymbol * invariant list * expr | Etry of expr * (pvsymbol list * expr) Mxs.t | Eraise of xsymbol * expr + | Eexn of xsymbol * expr | Eassert of assertion_kind * term | Eghost of expr | Epure of term @@ -384,8 +385,8 @@ let c_ghost c = c.c_cty.cty_effect.eff_ghost let e_fold fn acc e = match e.e_node with | Evar _ | Econst _ | Eexec _ | Eassign _ | Eassert _ | Epure _ | Eabsurd -> acc - | Eraise (_,e) | Efor (_,_,_,e) | Eghost e - | Elet ((LDsym _|LDrec _), e) -> fn acc e + | Eraise (_,e) | Efor (_,_,_,_,e) | Eghost e + | Elet ((LDsym _|LDrec _), e) | Eexn (_,e) -> fn acc e | Elet (LDvar (_,d), e) | Ewhile (d,_,_,e) -> fn (fn acc d) e | Eif (c,d,e) -> fn (fn (fn acc c) d) e | Ecase (d,bl) -> List.fold_left (fun acc (_,e) -> fn acc e) (fn acc d) bl @@ -564,7 +565,7 @@ let rec raw_of_expr prop e = match e.e_node with | Evar v -> t_var v.pv_vs | Econst c -> t_const c (ty_of_ity e.e_ity) | Epure t -> t - | Eghost e -> pure_of_expr prop e + | Eghost e | Eexn (_,e) -> pure_of_expr prop e | Eexec (_,{cty_post = []}) -> raise Exit | Eexec (_,{cty_post = q::_}) -> let v, h = open_post q in @@ -626,7 +627,7 @@ let rec post_of_expr res e = match e.e_node with | Econst (Number.ConstReal _ as c)-> post_of_term res (t_const c ty_real) | Epure t -> post_of_term res t - | Eghost e -> post_of_expr res e + | Eghost e | Eexn (_,e) -> post_of_expr res e | Eexec (_,c) -> let conv q = open_post_with res q in copy_labels e (t_and_l (List.map conv c.cty_post)) @@ -859,25 +860,37 @@ let e_not e = e_if e e_false e_true (* loops *) -let e_for_raw v ((f,_,t) as bounds) inv e = - ity_equal_check v.pv_ity ity_int; - ity_equal_check f.pv_ity ity_int; - ity_equal_check t.pv_ity ity_int; +let e_for_raw v ((f,_,t) as bounds) i inv e = + ity_equal_check f.pv_ity v.pv_ity; + ity_equal_check t.pv_ity v.pv_ity; + ity_equal_check i.pv_ity ity_int; ity_equal_check e.e_ity ity_unit; + if not (pv_equal v i) then begin + if not i.pv_ghost then Loc.errorm + "The internal for-loop index mush be ghost"; + let check f = if t_v_occurs v.pv_vs f > 0 then Loc.errorm + "The external for-loop index cannot occur in the invariant" in + List.iter check inv; + match v.pv_ity.ity_node with + | Ityapp ({its_def = Range _},_,_) -> () + | _ when ity_equal v.pv_ity ity_int -> () + | _ -> Loc.errorm "For-loop bounds must have an integer type" + end; let vars = List.fold_left t_freepvs Spv.empty inv in let ghost = v.pv_ghost || f.pv_ghost || t.pv_ghost in let eff = try_effect [e] eff_read_pre vars e.e_effect in let eff = try_effect [e] eff_ghostify ghost eff in ignore (try_effect [e] eff_union_seq eff eff); let eff = eff_bind_single v eff in + let eff = eff_bind_single i eff in let eff = eff_read_single_pre t eff in let eff = eff_read_single_pre f eff in - mk_expr (Efor (v,bounds,inv,e)) e.e_ity MaskVisible eff + mk_expr (Efor (v,bounds,i,inv,e)) e.e_ity MaskVisible eff -let e_for v f dir t inv e = +let e_for v f dir t i inv e = let hd, t = mk_proxy false t [] in let hd, f = mk_proxy false f hd in - let_head hd (e_for_raw v (f,dir,t) inv e) + let_head hd (e_for_raw v (f,dir,t) i inv e) let e_while d inv vl e = ity_equal_check d.e_ity ity_bool; @@ -957,6 +970,12 @@ let e_raise xs e ity = let eff = try_effect [e] eff_union_seq e.e_effect eff in mk_expr (Eraise (xs,e)) ity MaskVisible eff +exception ExceptionLeak of xsymbol + +let e_exn xs e = + if Sxs.mem xs e.e_effect.eff_raises then raise (ExceptionLeak xs); + mk_expr (Eexn (xs,e)) e.e_ity e.e_mask e.e_effect + (* snapshots, assertions, "any" *) let e_pure t = @@ -977,6 +996,7 @@ let cty_add_variant d varl = let add s (t,_) = t_freepvs s t in let rec e_rs_subst sm e = e_label_copy e (match e.e_node with | Evar _ | Econst _ | Eassign _ | Eassert _ | Epure _ | Eabsurd -> e + | Eexn (xs,e) -> e_exn xs (e_rs_subst sm e) | Eghost e -> e_ghostify true (e_rs_subst sm e) | Eexec (c,_) -> e_exec (c_rs_subst sm c) | Elet (LDvar (v,d),e) -> @@ -1003,7 +1023,7 @@ let rec e_rs_subst sm e = e_label_copy e (match e.e_node with let sm = List.fold_left2 add sm fdl nfdl in e_let (LDrec nfdl) (e_rs_subst sm e) | Eif (c,d,e) -> e_if (e_rs_subst sm c) (e_rs_subst sm d) (e_rs_subst sm e) - | Efor (v,b,inv,e) -> e_for_raw v b inv (e_rs_subst sm e) + | Efor (v,b,i,inv,e) -> e_for_raw v b i inv (e_rs_subst sm e) | Ewhile (d,inv,vl,e) -> e_while (e_rs_subst sm d) inv vl (e_rs_subst sm e) | Eraise (xs,d) -> e_raise xs (e_rs_subst sm d) e.e_ity | Ecase (d,bl) -> e_case (e_rs_subst sm d) @@ -1142,10 +1162,12 @@ let print_rs fmt ({rs_name = {id_string = nm}} as s) = if nm = "mixfix [.._]" then pp_print_string fmt "([.._])" else if nm = "mixfix [_.._]" then pp_print_string fmt "([_.._])" else match extract_op s.rs_name, s.rs_logic with - | Some s, _ -> - let s = if Strings.has_prefix "*" s then " " ^ s else s in - let s = if Strings.has_suffix "*" s then s ^ " " else s in - fprintf fmt "(%s)" s + | Some x, _ -> + fprintf fmt "(%s%s%s)" + (if Strings.has_prefix "*" x then " " else "") + x + (if List.length s.rs_cty.cty_args = 1 then "_" else + if Strings.has_suffix "*" x then " " else "") | _, RLnone | _, RLlemma -> pp_print_string fmt (id_unique sprinter s.rs_name) | _, RLpv v -> print_pv fmt v @@ -1326,11 +1348,17 @@ and print_enode pri fmt e = match e.e_node with | Ewhile (d,inv,varl,e) -> fprintf fmt "@[while %a do%a%a@\n%a@]@\ndone" print_expr d print_invariant inv print_variant varl print_expr e - | Efor (pv,(pvfrom,dir,pvto),inv,e) -> - fprintf fmt "@[for %a =@ %a@ %s@ %a@ %ado@\n%a@]@\ndone" - print_pv pv print_pv pvfrom + | Efor (pv,(pvfrom,dir,pvto),i,inv,e) -> + let print_i fmt i = + if not (pv_equal pv i) then fprintf fmt "(%a)" print_pv i in + fprintf fmt "@[for %a%a =@ %a@ %s@ %a@ %ado@\n%a@]@\ndone" + print_pv pv print_i i print_pv pvfrom (if dir = To then "to" else "downto") print_pv pvto print_invariant inv print_expr e + | Eexn (xs, e) -> + fprintf fmt (protect_on (pri > 0) "exception %a@ in@\n%a") + print_xs xs print_expr e; + forget_xs xs | Eraise (xs,e) when is_e_void e -> fprintf fmt "raise %a" print_xs xs | Eraise (xs,e) -> @@ -1407,4 +1435,6 @@ let () = Exn_printer.register (fun fmt e -> match e with "Function %a is not a constructor" print_rs s | FieldExpected s -> fprintf fmt "Function %a is not a mutable field" print_rs s + | ExceptionLeak xs -> fprintf fmt + "Uncatched local exception %a" print_xs xs | _ -> raise e) diff --git a/src/mlw/expr.mli b/src/mlw/expr.mli index 055919442d79e536084ec0fc487c75031539b42c..55a4f4c6543f1973c5a8377cb9246c73e68cc3a7 100644 --- a/src/mlw/expr.mli +++ b/src/mlw/expr.mli @@ -131,9 +131,10 @@ and expr_node = | Eif of expr * expr * expr | Ecase of expr * (prog_pattern * expr) list | Ewhile of expr * invariant list * variant list * expr - | Efor of pvsymbol * for_bounds * invariant list * expr + | Efor of pvsymbol * for_bounds * pvsymbol * invariant list * expr | Etry of expr * (pvsymbol list * expr) Mxs.t | Eraise of xsymbol * expr + | Eexn of xsymbol * expr | Eassert of assertion_kind * term | Eghost of expr | Epure of term @@ -224,6 +225,10 @@ val e_false : expr val is_e_true : expr -> bool val is_e_false : expr -> bool +exception ExceptionLeak of xsymbol + +val e_exn : xsymbol -> expr -> expr + val e_raise : xsymbol -> expr -> ity -> expr val e_try : expr -> (pvsymbol list * expr) Mxs.t -> expr @@ -232,8 +237,8 @@ val e_case : expr -> (prog_pattern * expr) list -> expr val e_while : expr -> invariant list -> variant list -> expr -> expr -val e_for : pvsymbol -> - expr -> for_direction -> expr -> invariant list -> expr -> expr +val e_for : pvsymbol -> expr -> for_direction -> expr -> + pvsymbol -> invariant list -> expr -> expr val e_assert : assertion_kind -> term -> expr diff --git a/src/mlw/ity.ml b/src/mlw/ity.ml index 724cdf091191670b64b8b7a3efcccfcd05c3bc29..6efac966e93238358061cb837c6b01f0608bba95 100644 --- a/src/mlw/ity.ml +++ b/src/mlw/ity.ml @@ -873,11 +873,9 @@ let xs_equal : xsymbol -> xsymbol -> bool = (==) let xs_hash xs = id_hash xs.xs_name let xs_compare xs1 xs2 = id_compare xs1.xs_name xs2.xs_name +let freeze_xs xs s = ity_freeze s xs.xs_ity + let create_xsymbol id ?(mask=MaskVisible) ity = - if not (ity_closed ity) then Loc.errorm ?loc:id.pre_loc - "Exception %s has a polymorphic type" id.pre_name; - if not ity.ity_imm then Loc.errorm ?loc:id.pre_loc - "The type of exception %s has mutable components" id.pre_name; mask_check (Invalid_argument "Ity.create_xsymbol") ity mask; { xs_name = id_register id; xs_ity = ity; xs_mask = mask_reduce mask } @@ -1284,13 +1282,16 @@ let spec_t_fold fn_t acc pre post xpost = let acc = fn_l (fn_l acc pre) post in Mxs.fold (fun _ l a -> fn_l a l) xpost acc -let check_tvs reads result pre post xpost = - (* every type variable in spec comes either from a known vsymbol - or from the result type. We need this to ensure that we always - can do a full instantiation. TODO: do we really need this? *) +let check_tvs reads raises result pre post xpost = + (* each type variable in spec comes either from a known vsymbol + or from the external exception, or from the result type. + We need this to ensure that we can do a full instantiation. + TODO: do we really need this? *) let add_pv v s = ity_freevars s v.pv_ity in let tvs = ity_freevars Stv.empty result in let tvs = Spv.fold add_pv reads tvs in + let add_xs xs s = ity_freevars s xs.xs_ity in + let tvs = Sxs.fold add_xs raises tvs in let check_tvs () t = let ttv = t_ty_freevars Stv.empty t in if not (Stv.subset ttv tvs) then Loc.error ?loc:t.t_loc @@ -1331,7 +1332,8 @@ let create_cty ?(mask=MaskVisible) args pre post xpost oldies effect result = let effect = eff_read_pre preads effect in let xreads = Spv.diff effect.eff_reads sarg in let freeze = Spv.fold freeze_pv xreads isb_empty in - check_tvs effect.eff_reads result pre post xpost; + let freeze = Sxs.fold freeze_xs effect.eff_raises freeze in + check_tvs effect.eff_reads effect.eff_raises result pre post xpost; (* remove exceptions whose postcondition is False *) let is_false q = match open_post q with | _, {t_node = Tfalse} -> true | _ -> false in @@ -1354,6 +1356,8 @@ let create_cty ?(mask=MaskVisible) args pre post xpost oldies effect result = as ghost, to keep the type signature consistent. *) let rknown = read_regs effect.eff_reads in let vknown = ity_rch_regs rknown result in + let add_xs xs s = ity_rch_regs s xs.xs_ity in + let vknown = Sxs.fold add_xs raises vknown in let effect = reset_taints { effect with eff_writes = Mreg.set_inter effect.eff_writes rknown; eff_covers = Mreg.set_inter effect.eff_covers rknown; @@ -1511,14 +1515,14 @@ let cty_read_post c pvs = let cty_add_pre pre c = if pre = [] then c else begin check_pre pre; let c = cty_read_pre (List.fold_left t_freepvs Spv.empty pre) c in let rd = List.fold_right Spv.add c.cty_args c.cty_effect.eff_reads in - check_tvs rd c.cty_result pre [] Mxs.empty; + check_tvs rd c.cty_effect.eff_raises c.cty_result pre [] Mxs.empty; { c with cty_pre = pre @ c.cty_pre } end let cty_add_post c post = if post = [] then c else begin check_post (Invalid_argument "Ity.cty_add_post") c.cty_result post; let c = cty_read_post c (List.fold_left t_freepvs Spv.empty post) in let rd = List.fold_right Spv.add c.cty_args c.cty_effect.eff_reads in - check_tvs rd c.cty_result [] post Mxs.empty; + check_tvs rd c.cty_effect.eff_raises c.cty_result [] post Mxs.empty; { c with cty_post = post @ c.cty_post } end (** pretty-printing *) @@ -1627,6 +1631,8 @@ let forget_pv v = forget_var v.pv_vs let print_xs fmt xs = pp_print_string fmt (id_unique xprinter xs.xs_name) +let forget_xs xs = forget_id xprinter xs.xs_name + exception FoundPrefix of pvsymbol list let unknown = create_pvsymbol (id_fresh "?") ity_unit diff --git a/src/mlw/ity.mli b/src/mlw/ity.mli index 23cba3cdc59b935affd3b0f10ff133b06418ee26..72c1b012e2624dac29ccd225e631c5b60c840f1e 100644 --- a/src/mlw/ity.mli +++ b/src/mlw/ity.mli @@ -491,6 +491,7 @@ val cty_add_post : cty -> post list -> cty val forget_reg : region -> unit (* flush id_unique for a region *) val forget_pv : pvsymbol -> unit (* flush for a program variable *) +val forget_xs : xsymbol -> unit (* flush for a local exception *) val forget_cty : cty -> unit (* forget arguments and oldies *) val print_its : Format.formatter -> itysymbol -> unit (* type symbol *) diff --git a/src/mlw/mltree.ml b/src/mlw/mltree.ml new file mode 100644 index 0000000000000000000000000000000000000000..a4753e523c8ef09c8bc5596dbc86ba5469b7fa66 --- /dev/null +++ b/src/mlw/mltree.ml @@ -0,0 +1,106 @@ +open Expr +open Ident +open Ty +open Ity +open Term + +type ty = + | Tvar of tvsymbol + | Tapp of ident * ty list + | Ttuple of ty list + +type is_ghost = bool + +type var = ident * ty * is_ghost + +type for_direction = To | DownTo + +type pat = + | Pwild + | Pvar of vsymbol + | Papp of lsymbol * pat list + | Ptuple of pat list + | Por of pat * pat + | Pas of pat * vsymbol + +type is_rec = bool + +type binop = Band | Bor | Beq + +type ity = I of Ity.ity | C of Ity.cty (* TODO: keep it like this? *) + +type expr = { + e_node : expr_node; + e_ity : ity; + e_effect : effect; +} + +and expr_node = + | Econst of Number.integer_constant + | Evar of pvsymbol + | Eapp of rsymbol * expr list + | Efun of var list * expr + | Elet of let_def * expr + | Eif of expr * expr * expr + | Eassign of (pvsymbol * rsymbol * pvsymbol) list + | Ematch of expr * (pat * expr) list + | Eblock of expr list + | Ewhile of expr * expr + (* For loop for Why3's type int *) + | Efor of pvsymbol * pvsymbol * for_direction * pvsymbol * expr + | Eraise of xsymbol * expr option + | Eexn of xsymbol * ty option * expr + | Etry of expr * (xsymbol * pvsymbol list * expr) list + | Eignore of expr + | Eabsurd + | Ehole + +and let_def = + | Lvar of pvsymbol * expr + | Lsym of rsymbol * ty * var list * expr + | Lrec of rdef list + +and rdef = { + rec_sym : rsymbol; (* exported *) + rec_rsym : rsymbol; (* internal *) + rec_args : var list; + rec_exp : expr; + rec_res : ty; + rec_svar : Stv.t; (* set of type variables *) +} + +type is_mutable = bool + +type typedef = + | Ddata of (ident * ty list) list + | Drecord of (is_mutable * ident * ty) list + | Dalias of ty + +type its_defn = { + its_name : ident; + its_args : tvsymbol list; + its_private : bool; + its_def : typedef option; +} + +type decl = + | Dtype of its_defn list + | Dlet of let_def + | Dexn of xsymbol * ty option + | Dclone of ident * decl list +(* + | Dfunctor of ident * (ident * decl list) list * decl list +*) + +type known_map = decl Mid.t + +type from_module = { + from_mod: Pmodule.pmodule option; + from_km : Pdecl.known_map; +} + +type pmodule = { + mod_from : from_module; + mod_decl : decl list; + mod_known : known_map; +} diff --git a/src/mlw/ocaml_printer.ml b/src/mlw/ocaml_printer.ml index f74175c8389ca726d51e1f2a460d96b353ec020e..030918689ef42541193a4c5f4d04c194529f5ff8 100644 --- a/src/mlw/ocaml_printer.ml +++ b/src/mlw/ocaml_printer.ml @@ -38,7 +38,8 @@ type info = { module Print = struct - open ML + open Mltree + open Compile.ML let ocaml_keywords = ["and"; "as"; "assert"; "asr"; "begin"; @@ -208,7 +209,7 @@ module Print = struct fprintf fmt "_" | Pvar {vs_name=id} -> (print_lident info) fmt id - | Pas (p, id) -> + | Pas (p, {vs_name=id}) -> fprintf fmt "%a as %a" (print_pat info) p (print_lident info) id | Por (p1, p2) -> fprintf fmt "%a | %a" (print_pat info) p1 (print_pat info) p2 @@ -326,7 +327,7 @@ module Print = struct else let ty_args = List.map (fun (_, ty, _) -> ty) args in let id_args = List.map (fun (id, _, _) -> id) args in - fprintf fmt ": @[%a@]. @[%a@] ->@ %a@ =@ fun @[%a@]@ ->" + fprintf fmt ": @[@[%a@]. @[%a@] ->@ %a@ =@ @[fun @[%a@]@ ->@]@]" print_svar s (print_list arrow (print_ty ~paren:true info)) ty_args (print_ty ~paren:true info) res @@ -417,7 +418,7 @@ module Print = struct (print_expr info) e1 (print_expr info) e2 | Eif (e1, e2, e3) -> fprintf fmt (protect_on paren - "@[@[if@ %a@]@ then@;<1 2>@[%a@]@;<1 0>else@;<1 2>@[%a@]@]") + "@[@[if@ %a@ then@ @[%a@]@]@;<1 0>else@;<1 2>@[%a@]@]") (print_expr info) e1 (print_expr info) e2 (print_expr info) e3 | Eblock [] -> fprintf fmt "()" @@ -448,6 +449,13 @@ module Print = struct fprintf fmt "@[@[begin@ try@ %a@] with@]@\n@[%a@]@\nend" (print_expr info) e (print_list newline (print_xbranch info)) bl + | Eexn (xs, None, e) -> + fprintf fmt "@[let exception %a in@\n%a@]" + (print_uident info) xs.xs_name (print_expr info) e + | Eexn (xs, Some t, e) -> + fprintf fmt "@[let exception %a of %a in@\n%a@]" + (print_uident info) xs.xs_name (print_ty ~paren:true info) t + (print_expr info) e | Eignore e -> fprintf fmt "ignore (%a)" (print_expr info) e (* | Enot _ -> (\* TODO *\) assert false *) (* | Ebinop _ -> (\* TODO *\) assert false *) @@ -527,28 +535,34 @@ module Print = struct assert false (*TODO*) let print_decl info fmt decl = + (* avoids printing the same decl for mutually recursive decls *) + let memo = Hashtbl.create 64 in let decl_name = get_decl_name decl in let decide_print id = - if query_syntax info.info_syn id = None then begin - print_decl info fmt decl; + if query_syntax info.info_syn id = None && + not (Hashtbl.mem memo decl) then begin + Hashtbl.add memo decl (); print_decl info fmt decl; fprintf fmt "@." end in List.iter decide_print decl_name end -let print_decl pargs ?old ?fname ~flat ({mod_theory = th} as m) fmt d = - ignore (old); - let info = { - info_syn = pargs.Pdriver.syntax; - info_convert = pargs.Pdriver.converter; - info_current_th = th; - info_current_mo = Some m; - info_th_known_map = th.th_known; - info_mo_known_map = m.mod_known; - info_fname = Opt.map Compile.clean_name fname; - flat = flat; - } in - Print.print_decl info fmt d +let print_decl = + let memo = Hashtbl.create 16 in + fun pargs ?old ?fname ~flat ({mod_theory = th} as m) fmt d -> + ignore (old); + let info = { + info_syn = pargs.Pdriver.syntax; + info_convert = pargs.Pdriver.converter; + info_current_th = th; + info_current_mo = Some m; + info_th_known_map = th.th_known; + info_mo_known_map = m.mod_known; + info_fname = Opt.map Compile.clean_name fname; + flat = flat; + } in + if not (Hashtbl.mem memo d) then begin + Hashtbl.add memo d (); Print.print_decl info fmt d end let fg ?fname m = let mod_name = m.mod_theory.th_name.id_string in @@ -557,9 +571,3 @@ let fg ?fname m = let () = Pdriver.register_printer "ocaml" ~desc:"printer for OCaml code" fg print_decl - -(* - * Local Variables: - * compile-command: "make -C ../.. -j3 bin/why3extract.opt" - * End: - *) diff --git a/src/mlw/pdecl.ml b/src/mlw/pdecl.ml index 498da4ae005b136c9a9d3373be97f5076778dd73..2c843fe462ed68c02eea6a380d4cd4233602a65a 100644 --- a/src/mlw/pdecl.ml +++ b/src/mlw/pdecl.ml @@ -215,8 +215,11 @@ let get_syms node pure = let del_rd syms rd = Sid.remove rd.rec_sym.rs_name syms in List.fold_left del_rd esms rdl in syms_let_defn (Sid.union syms esms) ld - | Efor (i,_,invl,e) -> - syms_pv (syms_tl (syms_expr syms e) invl) i + | Eexn (xs, e) -> + let esms = syms_expr Sid.empty e in + Sid.union syms (Sid.remove xs.xs_name esms) + | Efor (v,_,i,invl,e) -> + syms_pv (syms_pv (syms_tl (syms_expr syms e) invl) i) v | Ewhile (d,invl,varl,e) -> let syms = syms_varl (syms_expr syms e) varl in syms_tl (syms_eity syms d) invl diff --git a/src/mlw/pdriver.ml b/src/mlw/pdriver.ml index fecbd1ff519f5c17b9e8e1308b135efc5717ba21..bc7788dc996c1d7059d146fd17df60234e20a915 100644 --- a/src/mlw/pdriver.ml +++ b/src/mlw/pdriver.ml @@ -164,11 +164,12 @@ let load_driver env file extra_files = try match ns_find_prog_symbol m.mod_export q with | PV pv -> pv.Ity.pv_vs.vs_name | RS rs -> rs.Expr.rs_name - with Not_found -> raise (Loc.Located (loc, UnknownVal (!qualid,q))) + | OO _ -> raise Not_found (* TODO: proper error message *) + with Not_found -> Loc.error ~loc (UnknownVal (!qualid,q)) in let find_xs m (loc,q) = try ns_find_xs m.mod_export q - with Not_found -> raise (Loc.Located (loc, UnknownExn (!qualid,q))) + with Not_found -> Loc.error ~loc (UnknownExn (!qualid,q)) in let add_local_module loc m = function | MRexception (q,s) -> @@ -223,7 +224,7 @@ type filename_generator = ?fname:string -> Pmodule.pmodule -> string type printer = printer_args -> ?old:in_channel -> ?fname:string -> flat:bool -> - Pmodule.pmodule -> Compile.ML.decl Pp.pp + Pmodule.pmodule -> Mltree.decl Pp.pp type reg_printer = Pp.formatted * filename_generator * printer diff --git a/src/mlw/pdriver.mli b/src/mlw/pdriver.mli index b8e93c9d6fa9e015f58008b26755896a45e830d2..f04e12d2e862f0c905caec031af1addf6661e33b 100644 --- a/src/mlw/pdriver.mli +++ b/src/mlw/pdriver.mli @@ -39,7 +39,7 @@ val load_driver : Env.env -> string -> string list -> driver type printer = printer_args -> ?old:in_channel -> ?fname:string -> flat:bool -> - Pmodule.pmodule -> Compile.ML.decl Pp.pp + Pmodule.pmodule -> Mltree.decl Pp.pp type filename_generator = ?fname:string -> Pmodule.pmodule -> string diff --git a/src/mlw/pinterp.ml b/src/mlw/pinterp.ml index bb40fc0b51169fc8be0c15cecae244852c8a2b43..8ce170f5e991ef8968a4482339b7d39fccc30524 100644 --- a/src/mlw/pinterp.ml +++ b/src/mlw/pinterp.ml @@ -594,7 +594,7 @@ let rec eval_expr env (e : expr) : result = end | r -> r end - | Efor(pvs,(pvs1,dir,pvs2),_inv,e1) -> + | Efor(pvs,(pvs1,dir,pvs2),_i,_inv,e1) -> begin try let a = big_int_of_value (get_pvs env pvs1) in @@ -642,6 +642,7 @@ let rec eval_expr env (e : expr) : result = | Normal t -> Excep(xs,t) | _ -> r end + | Eexn(_,e1) -> eval_expr env e1 | Eassert(_,_t) -> Normal Vvoid (* TODO *) (* TODO: do not eval t if no assertion check *) (* @@ -816,10 +817,3 @@ let eval_global_symbol env m fmt rs = with Not_found -> eprintf "Symbol '%s' has no definition.@." rs.rs_name.Ident.id_string; exit 1 - - -(* -Local Variables: -compile-command: "unset LANG; make -C ../.. bin/why3execute.byte" -End: -*) diff --git a/src/mlw/pmodule.ml b/src/mlw/pmodule.ml index e28fb273874d1c3ee426798a339fff48cd372c90..aee4fffa99d19cd1bd026f94879d6e6fa180d2d5 100644 --- a/src/mlw/pmodule.ml +++ b/src/mlw/pmodule.ml @@ -24,6 +24,7 @@ open Pdecl type prog_symbol = | PV of pvsymbol | RS of rsymbol + | OO of Srs.t type namespace = { ns_ts : itysymbol Mstr.t; (* type symbols *) @@ -41,47 +42,102 @@ let empty_ns = { let ns_replace eq chk x vo vn = if not chk then vn else - if eq vo vn then vn else + if eq vo vn then vo else raise (ClashSymbol x) -let psym_equal p1 p2 = match p1,p2 with - | PV p1, PV p2 -> pv_equal p1 p2 - | RS p1, RS p2 -> rs_equal p1 p2 - | _, _ -> false - -let rec merge_ns chk ns1 ns2 = - if ns1 == ns2 then ns1 else - let join eq x n o = Some (ns_replace eq chk x o n) in - let ns_union eq m1 m2 = - if m1 == m2 then m1 else Mstr.union (join eq) m1 m2 in - let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in - { ns_ts = ns_union its_equal ns1.ns_ts ns2.ns_ts; - ns_ps = ns_union psym_equal ns1.ns_ps ns2.ns_ps; - ns_xs = ns_union xs_equal ns1.ns_xs ns2.ns_xs; - ns_ns = Mstr.union fusion ns1.ns_ns ns2.ns_ns; } - -let add_ns chk x ns m = Mstr.change (function - | Some os -> Some (merge_ns chk ns os) - | None -> Some ns) x m - -let ns_add eq chk x vn m = Mstr.change (function - | Some vo -> Some (ns_replace eq chk x vo vn) +let merge_ts = ns_replace its_equal +let merge_xs = ns_replace xs_equal + +type overload = + | UnOp (* t -> t *) + | BinOp (* t -> t -> t *) + | BinRel (* t -> t -> bool *) + | NoOver (* none of the above *) + +let overload_of_rs {rs_cty = cty} = + if cty.cty_effect.eff_ghost then NoOver else + if cty.cty_mask <> MaskVisible then NoOver else + match cty.cty_args with + | [a;b] when ity_equal a.pv_ity b.pv_ity && + ity_equal cty.cty_result ity_bool && + not a.pv_ghost && not b.pv_ghost -> BinRel + | [a;b] when ity_equal a.pv_ity b.pv_ity && + ity_equal cty.cty_result a.pv_ity && + not a.pv_ghost && not b.pv_ghost -> BinOp + | [a] when ity_equal cty.cty_result a.pv_ity && + not a.pv_ghost -> UnOp + | _ -> NoOver + +exception IncompatibleNotation of string + +let merge_ps chk x vo vn = + let fsty rs = (List.hd rs.rs_cty.cty_args).pv_ity in + if chk then match vo, vn with (* export namespace *) + (* currently, we have no way to export notation *) + | _, OO _ | OO _, _ -> assert false + | PV v1, PV v2 when pv_equal v1 v2 -> vo + | RS r1, RS r2 when rs_equal r1 r2 -> vo + | _ -> raise (ClashSymbol x) + else match vo, vn with (* import namespace *) + (* once again, no way to export notation *) + | _, OO _ -> assert false + (* but we can merge two compatible symbols *) + | RS r1, RS r2 when not (rs_equal r1 r2) -> + let o1 = overload_of_rs r1 in + let o2 = overload_of_rs r2 in + if o1 <> o2 || o2 = NoOver then vn else + if fsty r1 == fsty r2 then vn else + OO (Srs.add r2 (Srs.singleton r1)) + (* or add a compatible symbol to notation *) + | OO s1, RS r2 -> + let o1 = overload_of_rs (Srs.choose s1) in + let o2 = overload_of_rs r2 in + if o1 <> o2 || o2 = NoOver then vn else + let ty = fsty r2 in + let confl r = fsty r != ty in + let s1 = Srs.filter confl s1 in + if Srs.is_empty s1 then vn else + OO (Srs.add r2 s1) + | _ -> vn + +let rec merge_ns chk _ no nn = + if no == nn then no else + let union merge o n = + let merge x vo vn = Some (merge chk x vo vn) in + if o == n then o else Mstr.union merge o n in + { ns_ts = union merge_ts no.ns_ts nn.ns_ts; + ns_ps = union merge_ps no.ns_ps nn.ns_ps; + ns_xs = union merge_xs no.ns_xs nn.ns_xs; + ns_ns = union merge_ns no.ns_ns nn.ns_ns } + +let ns_add merge chk x vn m = Mstr.change (function + | Some vo -> Some (merge chk x vo vn) | None -> Some vn) x m -let add_xs chk x xs ns = { ns with ns_xs = ns_add xs_equal chk x xs ns.ns_xs } -let add_ts chk x ts ns = { ns with ns_ts = ns_add its_equal chk x ts ns.ns_ts } -let add_ps chk x ps ns = { ns with ns_ps = ns_add psym_equal chk x ps ns.ns_ps } -let add_ns chk x nn ns = { ns with ns_ns = add_ns chk x nn ns.ns_ns } +let add_ts chk x ts ns = { ns with ns_ts = ns_add merge_ts chk x ts ns.ns_ts } +let add_ps chk x ps ns = { ns with ns_ps = ns_add merge_ps chk x ps ns.ns_ps } +let add_xs chk x xs ns = { ns with ns_xs = ns_add merge_xs chk x xs ns.ns_xs } +let add_ns chk x nn ns = { ns with ns_ns = ns_add merge_ns chk x nn ns.ns_ns } + +let merge_ns chk nn no = merge_ns chk "" no nn (* swap arguments *) let rec ns_find get_map ns = function | [] -> assert false | [a] -> Mstr.find a (get_map ns) | a::l -> ns_find get_map (Mstr.find a ns.ns_ns) l -let ns_find_prog_symbol = ns_find (fun ns -> ns.ns_ps) -let ns_find_ns = ns_find (fun ns -> ns.ns_ns) -let ns_find_xs = ns_find (fun ns -> ns.ns_xs) -let ns_find_its = ns_find (fun ns -> ns.ns_ts) +let ns_find_its = ns_find (fun ns -> ns.ns_ts) +let ns_find_xs = ns_find (fun ns -> ns.ns_xs) +let ns_find_ns = ns_find (fun ns -> ns.ns_ns) + +let ns_find_prog_symbol ns s = + let ps = ns_find (fun ns -> ns.ns_ps) ns s in + match ps with + | RS _ | PV _ -> ps + | OO ss -> + let rs1 = Expr.Srs.min_elt ss in + let rs2 = Expr.Srs.max_elt ss in + if Expr.rs_equal rs1 rs2 then RS rs1 else ps let ns_find_pv ns s = match ns_find_prog_symbol ns s with | PV pv -> pv | _ -> raise Not_found @@ -105,7 +161,7 @@ and mod_unit = | Uuse of pmodule | Uclone of mod_inst | Umeta of meta * meta_arg list - | Uscope of string * bool * mod_unit list + | Uscope of string * mod_unit list and mod_inst = { mi_mod : pmodule; @@ -172,7 +228,7 @@ let close_module, restore_module = let open_scope uc s = match uc.muc_import with | ns :: _ -> { uc with muc_theory = Theory.open_scope uc.muc_theory s; - muc_units = [Uscope (s, false, uc.muc_units)]; + muc_units = [Uscope (s, uc.muc_units)]; muc_import = ns :: uc.muc_import; muc_export = empty_ns :: uc.muc_export; } | [] -> assert false @@ -180,20 +236,27 @@ let open_scope uc s = match uc.muc_import with let close_scope uc ~import = let th = Theory.close_scope uc.muc_theory ~import in match List.rev uc.muc_units, uc.muc_import, uc.muc_export with - | [Uscope (_,_,ul1)], _ :: sti, _ :: ste -> (* empty scope *) + | [Uscope (_,ul1)], _ :: sti, _ :: ste -> (* empty scope *) { uc with muc_theory = th; muc_units = ul1; muc_import = sti; muc_export = ste; } - | Uscope (s,_,ul1) :: ul0, _ :: i1 :: sti, e0 :: e1 :: ste -> + | Uscope (s,ul1) :: ul0, _ :: i1 :: sti, e0 :: e1 :: ste -> let i1 = if import then merge_ns false e0 i1 else i1 in let i1 = add_ns false s e0 i1 in let e1 = add_ns true s e0 e1 in { uc with muc_theory = th; - muc_units = Uscope (s, import, ul0) :: ul1; + muc_units = Uscope (s,ul0) :: ul1; muc_import = i1 :: sti; muc_export = e1 :: ste; } | _ -> assert false +let import_scope uc ql = match uc.muc_import with + | i1 :: sti -> + let th = Theory.import_scope uc.muc_theory ql in + let i1 = merge_ns false (ns_find_ns i1 ql) i1 in + { uc with muc_theory = th; muc_import = i1::sti } + | _ -> assert false + let use_export uc ({mod_theory = mth} as m) = let th = Theory.use_export uc.muc_theory mth in let uc = if Sid.mem mth.th_name uc.muc_used then uc @@ -345,9 +408,11 @@ let add_use uc d = Sid.fold (fun id uc -> | Some n -> use_export uc (tuple_module n) | None -> uc) (Mid.set_diff d.pd_syms uc.muc_known) uc +let mk_vc uc d = Vc.vc uc.muc_env uc.muc_known uc.muc_theory d + let add_pdecl ?(warn=true) ~vc uc d = let uc = add_use uc d in - let dl = if vc then Vc.vc uc.muc_env uc.muc_known d else [] in + let dl = if vc then mk_vc uc d else [] in (* verification conditions must not add additional dependencies on built-in theories like TupleN or HighOrd. Also, we expect int.Int or any other library theory to be in the context: @@ -580,24 +645,31 @@ let cl_save_rs cl s s' = type smap = { sm_vs : vsymbol Mvs.t; sm_pv : pvsymbol Mvs.t; + sm_xs : xsymbol Mxs.t; sm_rs : rsymbol Mrs.t; } let sm_of_cl cl = { sm_vs = Mvs.map (fun v -> v.pv_vs) cl.pv_table; sm_pv = cl.pv_table; + sm_xs = cl.xs_table; sm_rs = cl.rs_table } let sm_save_vs sm v v' = { sm_vs = Mvs.add v v'.pv_vs sm.sm_vs; sm_pv = Mvs.add v v' sm.sm_pv; + sm_xs = sm.sm_xs; sm_rs = sm.sm_rs } let sm_save_pv sm v v' = { sm_vs = Mvs.add v.pv_vs v'.pv_vs sm.sm_vs; sm_pv = Mvs.add v.pv_vs v' sm.sm_pv; + sm_xs = sm.sm_xs; sm_rs = sm.sm_rs } +let sm_save_xs sm s s' = + { sm with sm_xs = Mxs.add s s' sm.sm_xs } + let sm_save_rs cl sm s s' = let sm = { sm with sm_rs = Mrs.add s s' sm.sm_rs } in match s.rs_logic, s'.rs_logic with @@ -608,6 +680,10 @@ let sm_save_rs cl sm s s' = let sm_find_pv sm v = Mvs.find_def v v.pv_vs sm.sm_pv (* non-instantiated global variables are not in sm *) +let sm_find_xs sm xs = Mxs.find_def xs xs sm.sm_xs + +let sm_find_rs sm rs = Mrs.find_def rs rs sm.sm_rs + let clone_pv cl {pv_vs = vs; pv_ity = ity; pv_ghost = ghost} = create_pvsymbol (id_clone vs.vs_name) ~ghost (clone_ity cl ity) @@ -768,7 +844,7 @@ let clone_cty cl sm ?(drop_decr=false) cty = let pre = clone_invl cl sm_args pre in let post = clone_invl cl sm_olds cty.cty_post in let xpost = Mxs.fold (fun xs fl q -> - let xs = cl_find_xs cl xs in + let xs = sm_find_xs sm xs in let fl = clone_invl cl sm_olds fl in Mxs.add xs fl q) cty.cty_xpost Mxs.empty in let add_read v s = Spv.add (sm_find_pv sm_args v) s in @@ -788,7 +864,7 @@ let clone_cty cl sm ?(drop_decr=false) cty = let add_reset reg s = Sreg.add (clone_reg cl reg) s in let resets = Sreg.fold add_reset cty.cty_effect.eff_resets Sreg.empty in let eff = eff_reset (eff_write reads writes) resets in - let add_raise xs eff = eff_raise eff (cl_find_xs cl xs) in + let add_raise xs eff = eff_raise eff (sm_find_xs sm xs) in let eff = Sxs.fold add_raise cty.cty_effect.eff_raises eff in let eff = if cty.cty_effect.eff_oneway then eff_diverge eff else eff in let cty = create_cty ~mask:cty.cty_mask args pre post xpost olds eff res in @@ -838,20 +914,25 @@ let rec clone_expr cl sm e = e_label_copy e (match e.e_node with | Ewhile (c,invl,varl,e) -> e_while (clone_expr cl sm c) (clone_invl cl sm invl) (clone_varl cl sm varl) (clone_expr cl sm e) - | Efor (i, (f,dir,t), invl, e) -> - let i' = clone_pv cl i in - let ism = sm_save_pv sm i i' in - e_for i' + | Efor (v, (f,dir,t), i, invl, e) -> + let v' = clone_pv cl v in + let ism = sm_save_pv sm v v' in + let i' = if pv_equal v i then v' else clone_pv cl i in + let ism = if pv_equal v i then ism else sm_save_pv ism i i' in + e_for v' (e_var (sm_find_pv sm f)) dir (e_var (sm_find_pv sm t)) - (clone_invl cl ism invl) (clone_expr cl ism e) + i' (clone_invl cl ism invl) (clone_expr cl ism e) | Etry (d, xl) -> let conv_br xs (vl, e) m = let vl' = List.map (clone_pv cl) vl in let sm = List.fold_left2 sm_save_pv sm vl vl' in - Mxs.add (cl_find_xs cl xs) (vl', clone_expr cl sm e) m in + Mxs.add (sm_find_xs sm xs) (vl', clone_expr cl sm e) m in e_try (clone_expr cl sm d) (Mxs.fold conv_br xl Mxs.empty) | Eraise (xs, e) -> - e_raise (cl_find_xs cl xs) (clone_expr cl sm e) (clone_ity cl e.e_ity) + e_raise (sm_find_xs sm xs) (clone_expr cl sm e) (clone_ity cl e.e_ity) + | Eexn ({xs_name = id; xs_mask = mask; xs_ity = ity} as xs, e) -> + let xs' = create_xsymbol (id_clone id) ~mask (clone_ity cl ity) in + e_exn xs' (clone_expr cl (sm_save_xs sm xs xs') e) | Eassert (k, f) -> e_assert k (clone_term cl sm.sm_vs f) | Eghost e -> @@ -865,7 +946,7 @@ and clone_cexp cl sm c = match c.c_node with let vl = List.map (fun v -> sm_find_pv sm v) vl in let al = List.map (fun v -> clone_ity cl v.pv_ity) c.c_cty.cty_args in let res = clone_ity cl c.c_cty.cty_result in - c_app (Mrs.find_def s s sm.sm_rs) vl al res + c_app (sm_find_rs sm s) vl al res | Cpur (s,vl) -> let vl = List.map (fun v -> sm_find_pv sm v) vl in let al = List.map (fun v -> clone_ity cl v.pv_ity) c.c_cty.cty_args in @@ -955,7 +1036,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with (* FIXME check ghost status and mask of cexp/ld wrt rs *) (* FIXME check effects of cexp/ld wrt rs *) (* FIXME add correspondance for "let lemma" to cl.pr_table *) - let dl = Vc.vc uc.muc_env uc.muc_known (create_let_decl ld) in + let dl = mk_vc uc (create_let_decl ld) in List.fold_left (add_pdecl_raw ~warn:false) uc dl | PDlet ld -> begin match ld with @@ -1035,7 +1116,7 @@ let clone_export uc m inst = | MApr pr -> MApr (cl_find_pr cl pr) | a -> a) al) with Not_found -> uc end - | Uscope (n,_import,ul) -> + | Uscope (n,ul) -> let uc = open_scope uc n in let uc = List.fold_left add_unit uc ul in close_scope ~import:false uc in @@ -1113,20 +1194,32 @@ let rec print_unit fmt = function print_mname mi.mi_mod | Umeta (m,al) -> Format.fprintf fmt "@[meta %s %a@]" m.meta_name (Pp.print_list Pp.comma Pretty.print_meta_arg) al - | Uscope (s,i,[Uuse m]) -> Format.fprintf fmt "use%s %a%s" - (if i then " import" else "") print_mname m + | Uscope (s,[Uuse m]) -> Format.fprintf fmt "use %a%s" print_mname m (if s = m.mod_theory.th_name.id_string then "" else " as " ^ s) - | Uscope (s,i,[Uclone mi]) -> Format.fprintf fmt "clone%s %a%s with ..." - (if i then " import" else "") print_mname mi.mi_mod + | Uscope (s,[Uclone mi]) -> Format.fprintf fmt "clone %a%s with ..." + print_mname mi.mi_mod (if s = mi.mi_mod.mod_theory.th_name.id_string then "" else " as " ^ s) - | Uscope (s,i,ul) -> Format.fprintf fmt "@[scope%s %s@\n%a@]@\nend" - (if i then " import" else "") s (Pp.print_list Pp.newline2 print_unit) ul + | Uscope (s,ul) -> Format.fprintf fmt "@[scope %s@\n%a@]@\nend" + s (Pp.print_list Pp.newline2 print_unit) ul let print_module fmt m = Format.fprintf fmt "@[module %s@\n%a@]@\nend" m.mod_theory.th_name.id_string (Pp.print_list Pp.newline2 print_unit) m.mod_units +let get_rs_name nm = + if nm = "mixfix []" then "([])" else + if nm = "mixfix []<-" then "([]<-)" else + if nm = "mixfix [<-]" then "([<-])" else + if nm = "mixfix [_..]" then "([_..])" else + if nm = "mixfix [.._]" then "([.._])" else + if nm = "mixfix [_.._]" then "([_.._])" else + try "(" ^ Strings.remove_prefix "infix " nm ^ ")" with Not_found -> + try "(" ^ Strings.remove_prefix "prefix " nm ^ "_)" with Not_found -> + nm + let () = Exn_printer.register (fun fmt e -> match e with + | IncompatibleNotation nm -> Format.fprintf fmt + "Incombatible type signatures for notation '%s'" (get_rs_name nm) | ModuleNotFound (sl,s) -> Format.fprintf fmt "Module %s not found in library %a" s print_path sl | _ -> raise e) diff --git a/src/mlw/pmodule.mli b/src/mlw/pmodule.mli index a02726a113585b7d9912d118271437a9aa56ef0a..c8627c0cbf56f082a801408adfb05e1a4c64b8a1 100644 --- a/src/mlw/pmodule.mli +++ b/src/mlw/pmodule.mli @@ -24,6 +24,7 @@ open Pdecl type prog_symbol = | PV of pvsymbol | RS of rsymbol + | OO of Srs.t type namespace = { ns_ts : itysymbol Mstr.t; (* type symbols *) @@ -32,16 +33,24 @@ type namespace = { ns_ns : namespace Mstr.t; (* inner namespaces *) } -val ns_find_its : namespace -> string list -> itysymbol - val ns_find_prog_symbol : namespace -> string list -> prog_symbol +val ns_find_its : namespace -> string list -> itysymbol val ns_find_pv : namespace -> string list -> pvsymbol val ns_find_rs : namespace -> string list -> rsymbol val ns_find_xs : namespace -> string list -> xsymbol - val ns_find_ns : namespace -> string list -> namespace +type overload = + | UnOp (* t -> t *) + | BinOp (* t -> t -> t *) + | BinRel (* t -> t -> bool *) + | NoOver (* none of the above *) + +val overload_of_rs : rsymbol -> overload + +exception IncompatibleNotation of string + (** {2 Module} *) type pmodule = private { @@ -58,7 +67,7 @@ and mod_unit = | Uuse of pmodule | Uclone of mod_inst | Umeta of meta * meta_arg list - | Uscope of string * bool * mod_unit list + | Uscope of string * mod_unit list and mod_inst = { mi_mod : pmodule; @@ -90,8 +99,9 @@ type pmodule_uc = private { val create_module : Env.env -> ?path:string list -> preid -> pmodule_uc val close_module : pmodule_uc -> pmodule -val open_scope : pmodule_uc -> string -> pmodule_uc -val close_scope : pmodule_uc -> import:bool -> pmodule_uc +val open_scope : pmodule_uc -> string -> pmodule_uc +val close_scope : pmodule_uc -> import:bool -> pmodule_uc +val import_scope : pmodule_uc -> string list -> pmodule_uc val restore_path : ident -> string list * string * string list (** [restore_path id] returns the triple (library path, module, diff --git a/src/mlw/vc.ml b/src/mlw/vc.ml index c39f8064e88b13bb0dae1a9907be7021d25de9d4..45c77abf2042e990cfcdb039135e4ba968ac9ae7 100644 --- a/src/mlw/vc.ml +++ b/src/mlw/vc.ml @@ -61,6 +61,7 @@ let vc_labels = Slab.add kp_label type vc_env = { known_map : Pdecl.known_map; + ts_ranges : lsymbol Mts.t; ps_int_le : lsymbol; ps_int_ge : lsymbol; ps_int_lt : lsymbol; @@ -70,8 +71,9 @@ type vc_env = { exn_count : int ref; } -let mk_env {Theory.th_export = ns} kn = { +let mk_env {Theory.th_export = ns} kn tuc = { known_map = kn; + ts_ranges = tuc.Theory.uc_ranges; ps_int_le = Theory.ns_find_ls ns ["infix <="]; ps_int_ge = Theory.ns_find_ls ns ["infix >="]; ps_int_lt = Theory.ns_find_ls ns ["infix <"]; @@ -89,7 +91,7 @@ let new_exn env = incr env.exn_count; !(env.exn_count) (* FIXME: cannot verify int.why because of a cyclic dependency. int.Int is used for the "for" loops and for integer variants. We should be able to extract the necessary lsymbols from kn. *) -let mk_env env kn = mk_env (Env.read_theory env ["int"] "Int") kn +let mk_env env kn tuc = mk_env (Env.read_theory env ["int"] "Int") kn tuc (* explanation labels *) @@ -706,7 +708,8 @@ let rec k_expr env lps ({e_loc = loc} as e) res xmap = let f = vc_expl None lab expl_check f in let k = Kpar (Kstop f, k_unit res) in inv_of_pure env e.e_loc [f] k - | Eghost e0 -> + | Eghost e0 + | Eexn (_,e0) -> k_expr env lps e0 res xmap | Epure t -> let t = if t.t_ty <> None then t_lab t else @@ -735,9 +738,16 @@ let rec k_expr env lps ({e_loc = loc} as e) res xmap = let k = Kseq (Kval ([], prev), 0, bind_oldies oldies k) in let k = List.fold_right assume_inv iinv k in Kpar (j, k_havoc e.e_effect k) - | Efor (v, ({pv_vs = a}, d, {pv_vs = b}), invl, e1) -> - let a = t_var a and b = t_var b in - let i = t_var v.pv_vs and one = t_nat_const 1 in + | Efor (vx, (a, d, b), vi, invl, e1) -> + let int_of_pv = match vx.pv_vs.vs_ty.ty_node with + | Tyapp (s,_) when ts_equal s ts_int -> + fun v -> t_var v.pv_vs + | Tyapp (s,_) -> + let s = Mts.find s env.ts_ranges in + fun v -> fs_app s [t_var v.pv_vs] ty_int + | Tyvar _ -> assert false (* never *) in + let a = int_of_pv a and i = t_var vi.pv_vs in + let b = int_of_pv b and one = t_nat_const 1 in let init = wp_of_inv None lab expl_loop_init invl in let prev = sp_of_inv None lab expl_loop_init invl in let keep = wp_of_inv None lab expl_loop_keep invl in @@ -748,14 +758,20 @@ let rec k_expr env lps ({e_loc = loc} as e) res xmap = let expl_bounds f = vc_expl loc lab expl_for_bound f in let i_pl_1 = fs_app pl [i; one] ty_int in let b_pl_1 = fs_app pl [b; one] ty_int in - let init = t_subst_single v.pv_vs a init in - let keep = t_subst_single v.pv_vs i_pl_1 keep in - let last = t_subst_single v.pv_vs b_pl_1 prev in + let init = t_subst_single vi.pv_vs a init in + let keep = t_subst_single vi.pv_vs i_pl_1 keep in + let last = t_subst_single vi.pv_vs b_pl_1 prev in let iinv = inv_of_loop env e.e_loc invl [] in let j = List.fold_right assert_inv iinv (Kstop init) in let k = List.fold_right assert_inv iinv (Kstop keep) in let k = Kseq (k_expr env lps e1 res xmap, 0, k) in - let k = Kseq (Kval ([v], sp_and bounds prev), 0, k) in + let k = + if pv_equal vx vi then + Kseq (Kval ([vx], sp_and bounds prev), 0, k) + else + Kseq (Kval ([vx], t_true), 0, + Kseq (Klet (vi, int_of_pv vx, sp_and bounds prev), 0, k)) + in let k = Kpar (k, Kval ([res], last)) in let k = List.fold_right assume_inv iinv k in let k = Kpar (j, k_havoc e.e_effect k) in @@ -1368,13 +1384,13 @@ let mk_vc_decl kn id f = Eval_match.eval_match kn f in create_pure_decl (create_prop_decl Pgoal pr f) -let vc env kn d = match d.pd_node with +let vc env kn tuc d = match d.pd_node with | PDlet (LDsym (s, {c_node = Cfun e; c_cty = cty})) -> - let env = mk_env env kn in + let env = mk_env env kn tuc in let f = vc_fun env (Debug.test_noflag debug_sp) cty e in [mk_vc_decl kn s.rs_name f] | PDlet (LDrec rdl) -> - let env = mk_env env kn in + let env = mk_env env kn tuc in let fl = vc_rec env (Debug.test_noflag debug_sp) rdl in List.map2 (fun rd f -> mk_vc_decl kn rd.rec_sym.rs_name f) rdl fl | _ -> [] diff --git a/src/mlw/vc.mli b/src/mlw/vc.mli index 257f7867f1aa5693af00bfe6d8572040ca48ad06..4be2c03c2377bdc5240dccecec6e50b4815b4a93 100644 --- a/src/mlw/vc.mli +++ b/src/mlw/vc.mli @@ -11,4 +11,4 @@ open Pdecl -val vc : Env.env -> known_map -> pdecl -> pdecl list +val vc : Env.env -> known_map -> Theory.theory_uc -> pdecl -> pdecl list diff --git a/src/parser/lexer.mll b/src/parser/lexer.mll index ea5af1a4ccabd758493b38be7ae1d90ae3c22761..886fbc8420350b9cd0afeb77b0911fd2758750a8 100644 --- a/src/parser/lexer.mll +++ b/src/parser/lexer.mll @@ -84,11 +84,13 @@ "mutable", MUTABLE; "old", OLD; "private", PRIVATE; + "pure", PURE; "raise", RAISE; "raises", RAISES; "reads", READS; "rec", REC; "requires", REQUIRES; + "return", RETURN; "returns", RETURNS; "to", TO; "try", TRY; @@ -183,10 +185,6 @@ rule token = parse { LEFTBRC } | "}" { RIGHTBRC } - | "{|" - { LEFTPURE } - | "|}" - { RIGHTPURE } | ":" { COLON } | ";" @@ -221,6 +219,8 @@ rule token = parse { TILDE } | "=" { EQUAL } + | "-" + { MINUS } | "[" { LEFTSQ } | "]" diff --git a/src/parser/parser.mly b/src/parser/parser.mly index 5c32d283d0aeb9d2f0253427f1d2a23e49373f2d..2f068ae323b14a2c9dfc0bd497af615bdbd2a7f6 100644 --- a/src/parser/parser.mly +++ b/src/parser/parser.mly @@ -137,15 +137,15 @@ %token ABSTRACT ABSURD ANY ASSERT ASSUME AT BEGIN CHECK %token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR %token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD -%token PRIVATE RAISE RAISES READS REC REQUIRES RETURNS -%token TO TRY VAL VARIANT WHILE WRITES ALIAS +%token PRIVATE PURE RAISE RAISES READS REC REQUIRES +%token RETURN RETURNS TO TRY VAL VARIANT WHILE WRITES ALIAS (* symbols *) %token AND ARROW %token BAR %token COLON COMMA -%token DOT DOTDOT EQUAL LT GT LTGT +%token DOT DOTDOT EQUAL LT GT LTGT MINUS %token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ %token LARROW LRARROW OR %token RIGHTPAR RIGHTSQ @@ -156,21 +156,19 @@ (* program symbols *) -%token AMPAMP BARBAR LEFTBRC RIGHTBRC LEFTPURE RIGHTPURE SEMICOLON +%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON (* Precedences *) %nonassoc IN %nonassoc below_SEMI %nonassoc SEMICOLON -%nonassoc LET VAL +%nonassoc LET VAL EXCEPTION %nonassoc prec_no_else %nonassoc DOT ELSE GHOST %nonassoc prec_named -%nonassoc COLON - -%right ARROW LRARROW -%right BY SO +%nonassoc COLON (* weaker than -> because of t: a -> b *) +%right ARROW LRARROW BY SO %right OR BARBAR %right AND AMPAMP %nonassoc NOT @@ -178,10 +176,11 @@ %nonassoc AT OLD %nonassoc LARROW %nonassoc RIGHTSQ (* stronger than <- for e1[e2 <- e3] *) -%left OP2 +%left OP2 MINUS %left OP3 %left OP4 %nonassoc prec_prefix_op +%nonassoc INTEGER REAL %nonassoc LEFTSQ %nonassoc OPPREF @@ -512,11 +511,17 @@ term_: | NOT term { Tnot $2 } | OLD term - { Tat ($2, mk_id "0" $startpos($1) $endpos($1)) } + { Tat ($2, mk_id Dexpr.old_mark $startpos($1) $endpos($1)) } | term AT uident { Tat ($1, $3) } | prefix_op term %prec prec_prefix_op { Tidapp (Qident $1, [$2]) } +| MINUS INTEGER + { Tidapp (Qident (mk_id (prefix "-") $startpos($1) $endpos($1)), + [mk_term (Tconst (Number.ConstInt $2)) $startpos($2) $endpos($2)]) } +| MINUS REAL + { Tidapp (Qident (mk_id (prefix "-") $startpos($1) $endpos($1)), + [mk_term (Tconst (Number.ConstReal $2)) $startpos($2) $endpos($2)]) } | l = term ; o = bin_op ; r = term { Tbinop (l, o, r) } | l = term ; o = infix_op_1 ; r = term @@ -578,13 +583,17 @@ term_dot_: | o = oppref ; a = term_dot { Tidapp (Qident o, [a]) } | term_sub_ { $1 } -term_sub_: -| term_dot DOT lqualid_rich { Tidapp ($3,[$1]) } +term_block: | LEFTPAR term RIGHTPAR { $2.term_desc } | LEFTPAR RIGHTPAR { Ttuple [] } | LEFTPAR comma_list2(term) RIGHTPAR { Ttuple $2 } | LEFTBRC field_list1(term) RIGHTBRC { Trecord $2 } | LEFTBRC term_arg WITH field_list1(term) RIGHTBRC { Tupdate ($2,$4) } + +term_sub_: +| term_block { $1 } +| uqualid DOT mk_term(term_block) { Tscope ($1, $3) } +| term_dot DOT lqualid_rich { Tidapp ($3,[$1]) } | term_arg LEFTSQ term RIGHTSQ { Tidapp (get_op $startpos($2) $endpos($2), [$1;$3]) } | term_arg LEFTSQ term LARROW term RIGHTSQ @@ -689,6 +698,12 @@ expr_: { Enot $2 } | prefix_op expr %prec prec_prefix_op { Eidapp (Qident $1, [$2]) } +| MINUS INTEGER + { Eidapp (Qident (mk_id (prefix "-") $startpos($1) $endpos($1)), + [mk_expr (Econst (Number.ConstInt $2)) $startpos($2) $endpos($2)]) } +| MINUS REAL + { Eidapp (Qident (mk_id (prefix "-") $startpos($1) $endpos($1)), + [mk_expr (Econst (Number.ConstReal $2)) $startpos($2) $endpos($2)]) } | l = expr ; o = infix_op_1 ; r = expr { Einfix (l,o,r) } | l = expr ; o = infix_op_234 ; r = expr @@ -762,6 +777,10 @@ expr_: { Ematch ($2, $4) } | MATCH comma_list2(expr) WITH match_cases(seq_expr) END { Ematch (mk_expr (Etuple $2) $startpos($2) $endpos($2), $4) } +| EXCEPTION labels(uident) IN seq_expr + { Eexn ($2, PTtuple [], Ity.MaskVisible, $4) } +| EXCEPTION labels(uident) return IN seq_expr + { Eexn ($2, fst $3, snd $3, $5) } | LABEL labels(uident) IN seq_expr { Emark ($2, $4) } | WHILE seq_expr DO loop_annotation seq_expr DONE @@ -774,6 +793,8 @@ expr_: { Eraise ($2, $3) } | RAISE LEFTPAR uqualid expr_arg? RIGHTPAR { Eraise ($3, $4) } +| RETURN expr_arg? + { Eraise (Qident (mk_id Dexpr.old_mark $startpos($1) $endpos($1)), $2) } | TRY seq_expr WITH bar_list1(exn_handler) END { Etry ($2, $4) } | GHOST expr @@ -801,7 +822,7 @@ expr_dot_: | o = oppref ; a = expr_dot { Eidapp (Qident o, [a]) } | expr_sub { $1 } -expr_sub: +expr_block: | BEGIN single_spec spec seq_expr END { Efun ([], None, Ity.MaskVisible, spec_union $2 $3, $4) } | BEGIN single_spec spec END @@ -814,8 +835,12 @@ expr_sub: | LEFTPAR comma_list2(expr) RIGHTPAR { Etuple $2 } | LEFTBRC field_list1(expr) RIGHTBRC { Erecord $2 } | LEFTBRC expr_arg WITH field_list1(expr) RIGHTBRC { Eupdate ($2, $4) } -| LEFTPURE term RIGHTPURE { Epure $2 } + +expr_sub: +| expr_block { $1 } +| uqualid DOT mk_expr(expr_block) { Escope ($1, $3) } | expr_dot DOT lqualid_rich { Eidapp ($3, [$1]) } +| PURE LEFTBRC term RIGHTBRC { Epure $3 } | expr_arg LEFTSQ expr RIGHTSQ { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) } | expr_arg LEFTSQ expr LARROW expr RIGHTSQ @@ -1033,7 +1058,9 @@ lident_op_id: lident_op: | op_symbol { infix $1 } | op_symbol UNDERSCORE { prefix $1 } +| MINUS UNDERSCORE { prefix "-" } | EQUAL { infix "=" } +| MINUS { infix "-" } | OPPREF { prefix $1 } | LEFTSQ RIGHTSQ { mixfix "[]" } | LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" } @@ -1055,6 +1082,7 @@ op_symbol: prefix_op: | op_symbol { mk_id (prefix $1) $startpos $endpos } +| MINUS { mk_id (prefix "-") $startpos $endpos } %inline infix_op_1: | o = OP1 { mk_id (infix o) $startpos $endpos } @@ -1067,6 +1095,7 @@ prefix_op: | o = OP2 { mk_id (infix o) $startpos $endpos } | o = OP3 { mk_id (infix o) $startpos $endpos } | o = OP4 { mk_id (infix o) $startpos $endpos } +| MINUS { mk_id (infix "-") $startpos $endpos } (* Qualified idents *) diff --git a/src/parser/ptree.ml b/src/parser/ptree.ml index 9c21d4c2b0c308ca7790e286b6f1a27e8f6b8b84..f87775ec13c17d6de0792c63174d7061bc915e6c 100644 --- a/src/parser/ptree.ml +++ b/src/parser/ptree.ml @@ -85,6 +85,7 @@ and term_desc = | Ttuple of term list | Trecord of (qualid * term) list | Tupdate of term * (qualid * term) list + | Tscope of qualid * term | Tat of term * ident (*s Program expressions *) @@ -142,6 +143,7 @@ and expr_desc = | Eabsurd | Epure of term | Eraise of qualid * expr option + | Eexn of ident * pty * Ity.mask * expr | Etry of expr * (qualid * pattern option * expr) list | Efor of ident * expr * Expr.for_direction * expr * invariant * expr (* annotations *) @@ -150,6 +152,7 @@ and expr_desc = | Ecast of expr * pty | Eghost of expr | Enamed of label * expr + | Escope of qualid * expr and fundef = ident * ghost * Expr.rs_kind * binder list * pty option * Ity.mask * spec * expr diff --git a/src/parser/typing.ml b/src/parser/typing.ml index 1bb7a7cc0ff2c7d5588b81874f477ecaf47fa9f3..beb0df6a548fae8a88e3166637d36c5feba4c9fe 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -96,7 +96,10 @@ let find_xsymbol_ns ns q = let find_prog_symbol_ns ns p = let get_id_ps = function | PV pv -> pv.pv_vs.vs_name - | RS rs -> rs.rs_name in + | RS rs -> rs.rs_name + (* FIXME: this is incorrect, but we cannot + know the correct symbol at this stage *) + | OO ss -> (Srs.choose ss).rs_name in find_qualid get_id_ps ns_find_prog_symbol ns p let get_namespace muc = List.hd muc.Pmodule.muc_import @@ -128,6 +131,13 @@ let ty_of_pty tuc pty = in get_ty pty +let dty_of_pty tuc pty = + Dterm.dty_of_ty (ty_of_pty tuc pty) + +let dty_of_opt tuc = function + | Some pty -> dty_of_pty tuc pty + | None -> Dterm.dty_fresh () + let ity_of_pty muc pty = let rec get_ity = function | PTtyvar {id_str = x} -> @@ -147,6 +157,13 @@ let ity_of_pty muc pty = in get_ity pty +let dity_of_pty muc pty = + Dexpr.dity_of_ity (ity_of_pty muc pty) + +let dity_of_opt muc = function + | Some pty -> dity_of_pty muc pty + | None -> Dexpr.dity_fresh () + (** typing using destructive type variables parsed trees intermediate trees typed trees @@ -188,16 +205,13 @@ let rec dpattern tuc { pat_desc = desc; pat_loc = loc } = DPapp (cs,fl) | Ptree.Pas (p, x, false) -> DPas (dpattern tuc p, create_user_id x) | Ptree.Por (p, q) -> DPor (dpattern tuc p, dpattern tuc q) - | Ptree.Pcast (p, ty) -> DPcast (dpattern tuc p, ty_of_pty tuc ty) + | Ptree.Pcast (p, ty) -> DPcast (dpattern tuc p, dty_of_pty tuc ty) | Ptree.Pvar (_, true) | Ptree.Pas (_, _, true) -> Loc.errorm ~loc "ghost variables are only allowed in programs") let quant_var tuc (loc, id, gh, ty) = if gh then Loc.errorm ~loc "ghost variables are only allowed in programs"; - let ty = match ty with - | Some ty -> dty_of_ty (ty_of_pty tuc ty) - | None -> dty_fresh () in - Opt.map create_user_id id, ty, Some loc + Opt.map create_user_id id, dty_of_opt tuc ty, Some loc let loc_cutoff loc13 loc23 loc2 = let f,l,b,e = Loc.get loc13 in @@ -290,9 +304,9 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} = apply loc de1 op1 (dterm tuc gvars at denv e23) in chain loc (dterm tuc gvars at denv e1) op1 e23 | Ptree.Tconst (Number.ConstInt _ as c) -> - DTconst (c, ty_int) + DTconst (c, dty_int) | Ptree.Tconst (Number.ConstReal _ as c) -> - DTconst (c, ty_real) + DTconst (c, dty_real) | Ptree.Tlet (x, e1, e2) -> let id = create_user_id x in let e1 = dterm tuc gvars at denv e1 in @@ -362,17 +376,19 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} = if re then d else mk_let tuc ~loc "q " e1 d | Ptree.Tat (e1, l) -> DTlabel (dterm tuc gvars (Some l.id_str) denv e1, Slab.empty) + | Ptree.Tscope (q, e1) -> + let tuc = Theory.open_scope tuc "dummy" in + let tuc = Theory.import_scope tuc (string_list_of_qualid q) in + DTlabel (dterm tuc gvars at denv e1, Slab.empty) | Ptree.Tnamed (Lpos uloc, e1) -> DTuloc (dterm tuc gvars at denv e1, uloc) | Ptree.Tnamed (Lstr lab, e1) -> DTlabel (dterm tuc gvars at denv e1, Slab.singleton lab) | Ptree.Tcast ({term_desc = Ptree.Tconst c}, pty) -> - let ty = ty_of_pty tuc pty in - DTconst (c, ty) + DTconst (c, dty_of_pty tuc pty) | Ptree.Tcast (e1, pty) -> let d1 = dterm tuc gvars at denv e1 in - let ty = ty_of_pty tuc pty in - DTcast (d1, ty)) + DTcast (d1, dty_of_pty tuc pty)) (** typing program expressions *) @@ -432,7 +448,7 @@ let rec dpattern muc { pat_desc = desc; pat_loc = loc } = DPapp (cs,fl) | Ptree.Ptuple pl -> DPapp (rs_tuple (List.length pl), List.map (dpattern muc) pl) - | Ptree.Pcast (p, pty) -> DPcast (dpattern muc p, ity_of_pty muc pty) + | Ptree.Pcast (p, pty) -> DPcast (dpattern muc p, dity_of_pty muc pty) | Ptree.Pas (p, x, gh) -> DPas (dpattern muc p, create_user_id x, gh) | Ptree.Por (p, q) -> DPor (dpattern muc p, dpattern muc q)) @@ -483,9 +499,13 @@ let dpost muc ql lvm old ity = v, Loc.try3 ~loc type_fmla muc lvm old f in List.map dpost ql -let dxpost muc ql lvm old = +let dxpost muc ql lvm xsm old = let add_exn (q,pf) m = - let xs = find_xsymbol muc q in + let xs = match q with + | Qident i -> + begin try Mstr.find i.id_str xsm with + | Not_found -> find_xsymbol muc q end + | _ -> find_xsymbol muc q in Mxs.change (fun l -> match pf, l with | Some pf, Some l -> Some (pf :: l) | Some pf, None -> Some (pf :: []) @@ -528,42 +548,37 @@ let find_variant_ls muc q = match find_lsymbol muc.muc_theory q with | { ls_args = [u;v]; ls_value = None } as ls when ty_equal u v -> ls | s -> Loc.errorm ~loc:(qloc q) "Not an order relation: %a" Pretty.print_ls s -let dvariant muc varl lvm old = +let dvariant muc varl lvm _xsm old = let dvar t = type_term muc lvm old t in let dvar (t,q) = dvar t, Opt.map (find_variant_ls muc) q in List.map dvar varl -let dspec muc sp lvm old ity = { +let dspec muc sp lvm xsm old ity = { ds_pre = dpre muc sp.sp_pre lvm old; ds_post = dpost muc sp.sp_post lvm old ity; - ds_xpost = dxpost muc sp.sp_xpost lvm old; + ds_xpost = dxpost muc sp.sp_xpost lvm xsm old; ds_reads = dreads muc sp.sp_reads lvm; ds_writes = dwrites muc sp.sp_writes lvm; ds_alias = dalias muc sp.sp_alias lvm ity; ds_checkrw = sp.sp_checkrw; ds_diverge = sp.sp_diverge; } -let dassert muc f lvm old = type_fmla muc lvm old f +let dassert muc f lvm _xsm old = type_fmla muc lvm old f -let dinvariant muc f lvm old = dpre muc f lvm old +let dinvariant muc f lvm _xsm old = dpre muc f lvm old (* abstract values *) -let dbinder muc id gh pty = - let id = Opt.map create_user_id id in - let dity = match pty with - | Some pty -> dity_of_ity (ity_of_pty muc pty) - | None -> dity_fresh () in - id, gh, dity - -let dparam muc (_,id,gh,pty) = dbinder muc id gh (Some pty) +let dparam muc (_,id,gh,pty) = + Opt.map create_user_id id, gh, dity_of_pty muc pty -let dbinder muc (_,id,gh,pty) = dbinder muc id gh pty +let dbinder muc (_,id,gh,opt) = + Opt.map create_user_id id, gh, dity_of_opt muc opt (* expressions *) let is_reusable de = match de.de_node with - | DEvar _ | DEpv _ -> true | _ -> false + | DEvar _ | DEsym _ -> true | _ -> false let mk_var n de = Dexpr.dexpr ?loc:de.de_loc (DEvar (n, de.de_dvty)) @@ -587,8 +602,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = DEapp (Dexpr.dexpr ~loc e1, e2)) e el in let qualid_app loc q el = - let e = try match find_prog_symbol muc q with - | PV pv -> DEpv pv | RS rs -> DErs rs with + let e = try DEsym (find_prog_symbol muc q) with | _ -> DEls (find_lsymbol muc.muc_theory q) in expr_app loc e el in @@ -599,6 +613,12 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = | None -> qualid_app loc q el) | _ -> qualid_app loc q el in + let find_dxsymbol q = match q with + | Qident {id_str = n} -> + (try denv_get_exn denv n with _ + -> DEgexn (find_xsymbol muc q)) + | _ -> DEgexn (find_xsymbol muc q) + in Dexpr.dexpr ~loc begin match desc with | Ptree.Eident q -> qualid_app loc q [] @@ -607,7 +627,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = | Ptree.Eapply (e1, e2) -> DEapp (dexpr muc denv e1, dexpr muc denv e2) | Ptree.Etuple el -> - let e = DErs (rs_tuple (List.length el)) in + let e = DEsym (RS (rs_tuple (List.length el))) in expr_app loc e (List.map (dexpr muc denv) el) | Ptree.Einfix (e1, op1, e23) | Ptree.Einnfix (e1, op1, e23) -> @@ -640,18 +660,18 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = | None -> Loc.error ~loc (Decl.RecordFieldMissing (ls_of_rs pj)) | Some e -> dexpr muc denv e in let cs,fl = parse_record ~loc muc get_val fl in - expr_app loc (DErs cs) fl + expr_app loc (DEsym (RS cs)) fl | Ptree.Eupdate (e1, fl) -> let e1 = dexpr muc denv e1 in let re = is_reusable e1 in let v = if re then e1 else mk_var "q " e1 in let get_val _ pj = function | None -> - let pj = Dexpr.dexpr ~loc (DErs pj) in + let pj = Dexpr.dexpr ~loc (DEsym (RS pj)) in Dexpr.dexpr ~loc (DEapp (pj, v)) | Some e -> dexpr muc denv e in let cs,fl = parse_record ~loc muc get_val fl in - let d = expr_app loc (DErs cs) fl in + let d = expr_app loc (DEsym (RS cs)) fl in if re then d else mk_let ~loc "q " e1 d | Ptree.Elet (id, gh, kind, e1, e2) -> let e1 = update_any kind e1 in @@ -666,16 +686,17 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = DErec (rd, dexpr muc denv e1) | Ptree.Efun (bl, pty, msk, sp, e) -> let bl = List.map (dbinder muc) bl in - let e = match pty with - | Some pty -> { e with expr_desc = Ecast (e, pty) } - | None -> e in let ds = match (sp.sp_variant, sp.sp_alias) with | (({term_loc = loc},_)::_,_) -> Loc.errorm ~loc "unexpected 'variant' clause" | (_,({term_loc = loc},_)::_) -> Loc.errorm ~loc "unexpected 'alias' clause" | _ -> dspec muc sp in - DEfun (bl, msk, ds, dexpr muc (denv_add_args denv bl) e) + let dity = dity_of_opt muc pty in + let denv = denv_add_args denv bl in + let denv = if bl = [] then denv else + denv_add_exn denv old_mark_id dity in + DEfun (bl, dity, msk, ds, dexpr muc denv e) | Ptree.Eany (pl, kind, pty, msk, sp) -> let pl = List.map (dparam muc) pl in let ds = match sp.sp_variant with @@ -687,7 +708,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = | RKlemma, None -> ity_unit | RKpred, None -> ity_bool | _ -> Loc.errorm ~loc "cannot determine the type of the result" in - DEany (pl, msk, ds, dity_of_ity ity) + DEany (pl, dity_of_ity ity, msk, ds) | Ptree.Ematch (e1, bl) -> let e1 = dexpr muc denv e1 in let branch (pp, e) = @@ -724,28 +745,32 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = let eto = dexpr muc denv eto in let inv = dinvariant muc inv in let id = create_user_id id in - let denv = denv_add_var denv id (dity_of_ity ity_int) in + let denv = denv_add_for_index denv id efrom.de_dvty in DEfor (id, efrom, dir, eto, inv, dexpr muc denv e1) | Ptree.Eassign asl -> let mk_assign (e1,q,e2) = dexpr muc denv e1, find_record_field muc q, dexpr muc denv e2 in DEassign (List.map mk_assign asl) | Ptree.Eraise (q, e1) -> - let xs = find_xsymbol muc q in + let xs = find_dxsymbol q in + let mb_unit = match xs with + | DEgexn xs -> ity_equal xs.xs_ity ity_unit + | DElexn _ -> true in let e1 = match e1 with | Some e1 -> dexpr muc denv e1 - | None when ity_equal xs.xs_ity ity_unit -> - Dexpr.dexpr ~loc (DErs rs_void) + | None when mb_unit -> Dexpr.dexpr ~loc (DEsym (RS rs_void)) | _ -> Loc.errorm ~loc "exception argument expected" in DEraise (xs, e1) | Ptree.Etry (e1, cl) -> let e1 = dexpr muc denv e1 in let branch (q, pp, e) = - let xs = find_xsymbol muc q in + let xs = find_dxsymbol q in + let mb_unit = match xs with + | DEgexn xs -> ity_equal xs.xs_ity ity_unit + | DElexn _ -> true in let pp = match pp with | Some pp -> dpattern muc pp - | None when ity_equal xs.xs_ity ity_unit -> - Dexpr.dpattern ~loc (DPapp (rs_void, [])) + | None when mb_unit -> Dexpr.dpattern ~loc (DPapp (rs_void, [])) | _ -> Loc.errorm ~loc "exception argument expected" in let denv = denv_add_pat denv pp in let e = dexpr muc denv e in @@ -753,9 +778,15 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = DEtry (e1, List.map branch cl) | Ptree.Eghost e1 -> DEghost (dexpr muc denv e1) - | Ptree.Eabsurd -> DEabsurd + | Ptree.Eexn (id, pty, mask, e1) -> + let id = create_user_id id in + let dity = dity_of_pty muc pty in + let denv = denv_add_exn denv id dity in + DEexn (id, dity, mask, dexpr muc denv e1) + | Ptree.Eabsurd -> + DEabsurd | Ptree.Epure t -> - let get_term lvm old = type_term muc lvm old t in + let get_term lvm _xsm old = type_term muc lvm old t in let gvars _at q = try match find_prog_symbol muc q with | PV v -> Some v | _ -> None with _ -> None in let get_dty pure_denv = @@ -765,27 +796,32 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = | Ptree.Eassert (ak, f) -> DEassert (ak, dassert muc f) | Ptree.Emark (id, e1) -> - DEmark (create_user_id id, dexpr muc denv e1) + let dity = dity_fresh () in + let id = create_user_id id in + let denv = denv_add_exn denv id dity in + DEmark (id, dity, dexpr muc denv e1) + | Ptree.Escope (q, e1) -> + let muc = open_scope muc "dummy" in + let muc = import_scope muc (string_list_of_qualid q) in + DElabel (dexpr muc denv e1, Slab.empty) | Ptree.Enamed (Lpos uloc, e1) -> DEuloc (dexpr muc denv e1, uloc) | Ptree.Enamed (Lstr lab, e1) -> DElabel (dexpr muc denv e1, Slab.singleton lab) - | Ptree.Ecast ({expr_desc = Ptree.Econst c},pty) -> - let ity = ity_of_pty muc pty in - DEconst (c, dity_of_ity ity) - | Ptree.Ecast (e1,pty) -> + | Ptree.Ecast ({expr_desc = Ptree.Econst c}, pty) -> + DEconst (c, dity_of_pty muc pty) + | Ptree.Ecast (e1, pty) -> let d1 = dexpr muc denv e1 in - let ity = ity_of_pty muc pty in - DEcast (d1, ity) + DEcast (d1, dity_of_pty muc pty) end and drec_defn muc denv fdl = let prep (id, gh, kind, bl, pty, msk, sp, e) = let bl = List.map (dbinder muc) bl in - let dity = match pty with - | Some pty -> dity_of_ity (ity_of_pty muc pty) - | None -> dity_fresh () in + let dity = dity_of_opt muc pty in let pre denv = + let denv = denv_add_args denv bl in + let denv = denv_add_exn denv old_mark_id dity in let dv = dvariant muc sp.sp_variant in dspec muc sp, dv, dexpr muc denv e in create_user_id id, gh, kind, bl, dity, msk, pre in @@ -1100,6 +1136,8 @@ let type_inst ({muc_theory = tuc} as muc) ({mod_theory = t} as m) s = Loc.errorm ~loc:(qloc q) "program constant expected" | RS _, PV _ -> Loc.errorm ~loc:(qloc q) "program function expected" + | OO _, _ | _, OO _ -> + Loc.errorm ~loc:(qloc q) "ambiguous notation" end | CSxsym (p,q) -> let xs1 = find_xsymbol_ns m.mod_export p in diff --git a/src/tools/why3extract.ml b/src/tools/why3extract.ml index 9ea7d6dc1261c0f30b6d83653df9d748e2c583e5..191d6532c19caeec1b321f43b56f9e213151de20 100644 --- a/src/tools/why3extract.ml +++ b/src/tools/why3extract.ml @@ -153,15 +153,12 @@ let print_mdecls ?fname m mdecls = if cout <> stdout then close_out cout end let find_module_path mm path m = match path with - | [] -> - Mstr.find m mm - | path -> - let mm = Env.read_library Pmodule.mlw_language env path in + | [] -> Mstr.find m mm + | path -> let mm = Env.read_library Pmodule.mlw_language env path in Mstr.find m mm let find_module_id mm id = - let (path, m, _) = Pmodule.restore_path id in - find_module_path mm path m + let (path, m, _) = Pmodule.restore_path id in find_module_path mm path m let translate_module = let memo = Ident.Hid.create 16 in @@ -189,14 +186,14 @@ let extract_to = if not (Ident.Hid.mem memo name) then begin Ident.Hid.add memo name (); let mdecls = match decl with - | None -> (translate_module m).ML.mod_decl + | None -> (translate_module m).Mltree.mod_decl | Some d -> Translate.pdecl_m m d in print_mdecls ?fname m mdecls end let rec use_iter f l = List.iter - (function Uuse t -> f t | Uscope (_,_,l) -> use_iter f l | _ -> ()) l + (function Uuse t -> f t | Uscope (_,l) -> use_iter f l | _ -> ()) l let rec do_extract_module ?fname m = let extract_use m' = @@ -277,7 +274,7 @@ let toextract = ref [] let find_decl mm id = let m = find_module_id mm id in let m = translate_module m in - Ident.Mid.find id m.ML.mod_known + Ident.Mid.find id m.Mltree.mod_known let rec visit mm id = if not (Ident.Hid.mem visited id) then begin @@ -289,9 +286,9 @@ let rec visit mm id = with Not_found -> () end -let visit mm id = - if opt_rec_single = Recursive then visit mm id - else toextract := id :: !toextract +(* let visit mm id = *) +(* if opt_rec_single = Recursive then visit mm id *) +(* else toextract := id :: !toextract *) let flat_extraction mm = function | File fname -> @@ -302,14 +299,12 @@ let flat_extraction mm = function eprintf "multiple module '%s'; use -L . instead@." s; exit 1 end; - let tm = translate_module m in - Ident.Mid.iter (fun id _ -> visit mm id) tm.ML.mod_known; Mstr.add s m mm in Mstr.fold do_m mmf mm | Module (path, m) -> let m = find_module_path mm path m in (* FIXME: catch Not_found here *) let m = translate_module m in - Ident.Mid.iter (fun id _ -> visit mm id) m.ML.mod_known; + Ident.Mid.iter (fun id _ -> visit mm id) m.Mltree.mod_known; mm | Symbol (path, m, s) -> let m = find_module_path mm path m in @@ -325,6 +320,9 @@ let () = Queue.iter do_modular opt_queue | Flat -> let mm = Queue.fold flat_extraction Mstr.empty opt_queue in + let visit_m _ m = let tm = translate_module m in + Ident.Mid.iter (fun id _ -> visit mm id) tm.Mltree.mod_known in + Mstr.iter visit_m mm; let (_fg, pargs, pr) = Pdriver.lookup_printer opt_driver in let cout = match opt_output with | None -> stdout @@ -337,7 +335,7 @@ let () = let extract fmt id = let pm = find_module_id mm id in let m = translate_module pm in - let d = Ident.Mid.find id m.ML.mod_known in + let d = Ident.Mid.find id m.Mltree.mod_known in pr pargs ~flat:true pm fmt d in List.iter (extract fmt) (List.rev !toextract); if cout <> stdout then close_out cout diff --git a/src/transform/encoding.ml b/src/transform/encoding.ml index 9273b085675f36d63d73e1b4e30ee6abb77722fc..f5477cdda449ad75002de2ecfcbe3922ece4b621 100644 --- a/src/transform/encoding.ml +++ b/src/transform/encoding.ml @@ -31,7 +31,7 @@ let meta_enco_kept = register_meta_excl "enco_kept" [MTstring] ~desc:"Specify@ the@ type@ protection@ transformation:@; \ @[\ - @[twin: use@ conversion@ functions@ between@ the@ kept@ types@ \ - and@ the@ universal@ type@]@\ + and@ the@ universal@ type@]\ @]" let meta_enco_poly = register_meta_excl "enco_poly" [MTstring] diff --git a/theories/int.why b/theories/int.why index 199a1798a6f24f056a39438cc1609c5070f5b594..671b0f8ea270c90e192b2aa10c108a50edb19a3f 100644 --- a/theories/int.why +++ b/theories/int.why @@ -265,7 +265,12 @@ theory Exponentiation lemma Power_mult : forall x:t, n m : int. 0 <= n -> 0 <= m -> power x (Int.(*) n m) = power (power x n) m - lemma Power_mult2 : forall x y: t, n: int. 0 <= n -> + lemma Power_comm1 : forall x y: t. x * y = y * x -> + forall n:int. 0 <= n -> + power x n * y = y * power x n + + lemma Power_comm2 : forall x y: t. x * y = y * x -> + forall n:int. 0 <= n -> power (x * y) n = power x n * power y n (* TODO diff --git a/theories/map.why b/theories/map.why index 31a95c28681c5c164d827c16b074247ba9a1122a..be50968b2d3dab5785e991a37dd2b636953874d0 100644 --- a/theories/map.why +++ b/theories/map.why @@ -11,7 +11,7 @@ theory Map let function get (f: map 'a 'b) (x: 'a) : 'b = f x let ghost function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b = - fun y -> if y = x then v else f y + fun y -> if pure {y = x} then v else f y (** syntactic sugar *) let function ([]) (f: map 'a 'b) (x: 'a) : 'b = f x