Documentation update. Test cleanup.

lukstafi · Feb 18, 2015 · c2bdb6a · c2bdb6a
1 parent 4ae36de
commit c2bdb6a
Show file tree

Hide file tree

Showing 30 changed files with 355 additions and 206 deletions.
diff --git a/README.md b/README.md
@@ -21,6 +21,21 @@ I decided to implement a new domain / sort. It will be an order domain, with bot
 Milestones: [x] - completed, [#] - finishing (75%-95%), [+] - in the middle (25%-75%), [-] - just started (5%-25%), [_] - not started.
 
 Goals -- version targets may be reassigned:
+- [-] New sort: order. (v2.1)
+- [#] Order sort example: binomial heap. (v2.1)
+- [ ] Datatype-level invariants shared by all constructors of a datatype. (v2.1)
+- [ ] Solver directives in .gadt source code -- exposing the options available from the command-line interface. (v2.1)
+- [ ] Or-patterns `p1 | p2` introducing disjunctions in premises, either eliminated by disjunction elimination or expanded by implication clause duplication -- depending on user-level option; preserved in exported code. (v2.1)
+- [ ] Meta-automatic mode: retry with modified user-level parameter settings if inference fails. (v2.2)
+- [ ] Improve error reporting (likely culprit). (v2.2)
+- [ ] Ability to parse `.gadti` and `.mli` files, and use them with the module access `open M`, `let open M in ...`, `M.(...)` and `M.x` syntaxes. (v2.3)
+- [ ] 'Update' and 'verify' modes of inference: use an existing `.gadti` file to provide a type annotation on the toplevel `.gadt` expressions. (v2.3)
+- [ ] Optimize, paying attention to the speed of the update mode. (v2.3)
+- [ ] Support OCaml-style records, with some desambiguation roughly as in OCaml. (v2.4)
+- [ ] More general `when` clauses for patterns. Factorize `Num` and `NumAdd` out of the `expr` type. (v2.4)
+- [ ] Add a new "promising" sort. Candidates: proper integer numbers, ring of polynomials... (v2.4)
+
+Version 2.0 milestones are now completed:
 - [x] Export to OCaml using built-in or pervasives OCaml types, in particular `bool` instead of `boolean`. (v1.1)
 - [x] Support source code comments preserved in the AST. (v1.1)
 - [x] Factorize to make extending and adding sorts easier. (v1.2)
@@ -32,21 +47,8 @@ Goals -- version targets may be reassigned:
 - [x] Flagship example: AVL tree from OCaml standard library (height imbalance limited by 2). (v1.2)
 - [x] Option to detect all dead code. (v1.2.1)
 - [x] Improve coverage for examples from Chuan-kai Lin's PhD thesis. (v2.0)
-- [#] Improve coverage for DML / Liquid Types examples. (v2.0)
+- [x] Improve coverage for DML / Liquid Types examples. (v2.0)
 - [x] if-then-else syntax. (v2.0)
-- [-] New sort: order. (v2.1)
-- [#] Order sort example: binomial heap. (v2.1)
-- [ ] Datatype-level invariants shared by all constructors of a datatype. (v2.1)
-- [ ] Solver directives in .gadt source code -- exposing the options available from the command-line interface. (v2.1)
-- [ ] Or-patterns `p1 | p2` introducing disjunctions in premises, either eliminated by disjunction elimination or expanded by implication clause duplication -- depending on user-level option; preserved in exported code. (v2.1)
-- [ ] Meta-automatic mode: retry with modified user-level parameter settings if inference fails. (v2.1)
-- [ ] Ability to parse `.gadti` and `.mli` files, and use them with the module access `open M`, `let open M in ...`, `M.(...)` and `M.x` syntaxes. (v2.2)
-- [ ] Improve error reporting (likely culprit). (v2.2)
-- [ ] 'Update' and 'verify' modes of inference: use an existing `.gadti` file to provide a type annotation on the toplevel `.gadt` expressions. (v2.2)
-- [ ] Optimize, paying attention to the speed of the update mode. (v2.2)
-- [ ] Support OCaml-style records, with some desambiguation roughly as in OCaml. (v2.2)
-- [ ] More general `when` clauses for patterns. Factorize `Num` and `NumAdd` out of the `expr` type. (v2.3)
-- [ ] Add a new "promising" sort. Candidates: proper integer numbers, ring of polynomials... (v2.4)
 
 Version 1.0 milestones are now completed:
 - [x] Setup project. Parse and pretty-print.

diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf
diff --git a/doc/invargent-manual.tm b/doc/invargent-manual.tm
diff --git a/examples/avl_delmin-simpler.gadt → examples/avl_delmin_simpler.gadt b/examples/avl_delmin-simpler.gadt → examples/avl_delmin_simpler.gadt
diff --git a/examples/avl_delmin-simpler.gadti.target → examples/avl_delmin_simpler.gadti.target b/examples/avl_delmin-simpler.gadti.target → examples/avl_delmin_simpler.gadti.target
diff --git a/examples/binary_plus-harder.gadt → examples/binary_plus_harder.gadt b/examples/binary_plus-harder.gadt → examples/binary_plus_harder.gadt
diff --git a/examples/binary_plus-harder.gadti.target → examples/binary_plus_harder.gadti.target b/examples/binary_plus-harder.gadti.target → examples/binary_plus_harder.gadti.target
diff --git a/examples/non_outsidein-rx.gadt → examples/non_outsidein_rx.gadt b/examples/non_outsidein-rx.gadt → examples/non_outsidein_rx.gadt
diff --git a/examples/non_outsidein-rx.gadti.target → examples/non_outsidein_rx.gadti.target b/examples/non_outsidein-rx.gadti.target → examples/non_outsidein_rx.gadti.target
diff --git a/...es/non_pointwise_avl_delmin-modified.gadt → ...es/non_pointwise_avl_delmin_modified.gadt b/...es/non_pointwise_avl_delmin-modified.gadt → ...es/non_pointwise_avl_delmin_modified.gadt
diff --git a/...ointwise_avl_delmin-modified.gadti.target → ...ointwise_avl_delmin_modified.gadti.target b/...ointwise_avl_delmin-modified.gadti.target → ...ointwise_avl_delmin_modified.gadti.target
diff --git a/examples/non_pointwise_fd_comp-harder.gadt → examples/non_pointwise_fd_comp_harder.gadt b/examples/non_pointwise_fd_comp-harder.gadt → examples/non_pointwise_fd_comp_harder.gadt
diff --git a/...non_pointwise_fd_comp-harder.gadti.target → ...non_pointwise_fd_comp_harder.gadti.target b/...non_pointwise_fd_comp-harder.gadti.target → ...non_pointwise_fd_comp_harder.gadti.target
diff --git a/examples/non_pointwise_zip1-modified.gadt → examples/non_pointwise_zip1_modified.gadt b/examples/non_pointwise_zip1-modified.gadt → examples/non_pointwise_zip1_modified.gadt
diff --git a/.../non_pointwise_zip1-modified.gadti.target → .../non_pointwise_zip1_modified.gadti.target b/.../non_pointwise_zip1-modified.gadti.target → .../non_pointwise_zip1_modified.gadti.target
diff --git a/examples/non_pointwise_zip1-simpler.gadt → examples/non_pointwise_zip1_simpler.gadt b/examples/non_pointwise_zip1-simpler.gadt → examples/non_pointwise_zip1_simpler.gadt
diff --git a/...s/non_pointwise_zip1-simpler.gadti.target → ...s/non_pointwise_zip1_simpler.gadti.target b/...s/non_pointwise_zip1-simpler.gadti.target → ...s/non_pointwise_zip1_simpler.gadti.target
diff --git a/examples/non_pointwise_zip1-simpler2.gadt → examples/non_pointwise_zip1_simpler2.gadt b/examples/non_pointwise_zip1-simpler2.gadt → examples/non_pointwise_zip1_simpler2.gadt
diff --git a/.../non_pointwise_zip1-simpler2.gadti.target → .../non_pointwise_zip1_simpler2.gadti.target b/.../non_pointwise_zip1-simpler2.gadti.target → .../non_pointwise_zip1_simpler2.gadti.target
diff --git a/examples/pointwise_zip2-harder.gadt → examples/pointwise_zip2_harder.gadt b/examples/pointwise_zip2-harder.gadt → examples/pointwise_zip2_harder.gadt
diff --git a/examples/pointwise_zip2-harder.gadti.target → examples/pointwise_zip2_harder.gadti.target b/examples/pointwise_zip2-harder.gadti.target → examples/pointwise_zip2_harder.gadti.target
@@ -1,10 +1,13 @@
 datatype List : type
+
 datacons N : ∀a. List a
-datacons C : ∀a. a * List a ⟶ List a
+
+datacons C : ∀a.a * List a ⟶ List a
 
 datatype Zip2 : type * type
+
 datacons Zero2 : ∀a. Zip2 (a, List a)
-datacons Succ2 :
-  ∀a, b, c. Zip2 (a, b) ⟶ Zip2 ((c → a), (List c → b))
+
+datacons Succ2 : ∀a, b, c.Zip2 (a, b) ⟶ Zip2 (c → a, List c → b)
 
 val zip2 : ∀a, b. Zip2 (a, b) → a → b
diff --git a/examples/pointwise_zip2-simpler1.gadt → examples/pointwise_zip2_simpler1.gadt b/examples/pointwise_zip2-simpler1.gadt → examples/pointwise_zip2_simpler1.gadt
diff --git a/...ples/pointwise_zip2-simpler1.gadti.target → ...ples/pointwise_zip2_simpler1.gadti.target b/...ples/pointwise_zip2-simpler1.gadti.target → ...ples/pointwise_zip2_simpler1.gadti.target
diff --git a/examples/pointwise_zip2-simpler2.gadt → examples/pointwise_zip2_simpler2.gadt b/examples/pointwise_zip2-simpler2.gadt → examples/pointwise_zip2_simpler2.gadt
diff --git a/...ples/pointwise_zip2-simpler2.gadti.target → ...ples/pointwise_zip2_simpler2.gadti.target b/...ples/pointwise_zip2-simpler2.gadti.target → ...ples/pointwise_zip2_simpler2.gadti.target
diff --git a/examples/pointwise_zip2-simpler3.gadt → examples/pointwise_zip2_simpler3.gadt b/examples/pointwise_zip2-simpler3.gadt → examples/pointwise_zip2_simpler3.gadt
diff --git a/...ples/pointwise_zip2-simpler3.gadti.target → ...ples/pointwise_zip2_simpler3.gadti.target b/...ples/pointwise_zip2-simpler3.gadti.target → ...ples/pointwise_zip2_simpler3.gadti.target
diff --git a/examples/pointwise_zip2-simpler4.gadt → examples/pointwise_zip2_simpler4.gadt b/examples/pointwise_zip2-simpler4.gadt → examples/pointwise_zip2_simpler4.gadt
diff --git a/...ples/pointwise_zip2-simpler4.gadti.target → ...ples/pointwise_zip2_simpler4.gadti.target b/...ples/pointwise_zip2-simpler4.gadti.target → ...ples/pointwise_zip2_simpler4.gadti.target
diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml
@@ -17,7 +17,8 @@ let input_file file =
    with End_of_file -> ());
   Buffer.contents buf
 
-let test_case ?(test_annot=false) ?richer_answers ?more_general_num
+let test_case ?(test_annot=false) ?(do_ml=true)
+    ?richer_answers ?more_general_num
     ?prefer_guess ?prefer_bound_to_local ?prefer_bound_to_outer
     ?abd_rotations ?num_abd_timeout
     ?num_abd_fail_timeout ?nodeadcode file () =
@@ -76,7 +77,7 @@ let test_case ?(test_annot=false) ?richer_answers ?more_general_num
   (try
      let verif_res =
        (*[* Format.printf "test_case: file=%s@\n%!" file; *]*)
-       InvarGenT.process_file ~do_sig:true ~do_ml:true
+       InvarGenT.process_file ~do_sig:true ~do_ml
          ~full_annot:test_annot (file^".gadt") in
      assert_equal ~printer:(fun x->x)
        (input_file (file^".gadti.target"))
@@ -160,15 +161,15 @@ let tests = "InvarGenT" >::: [
         (fun () ->
            todo "currently requiring expanded arguments";
            skip_if !debug "debug";
-           test_case "binary_plus-harder" ());
+           test_case "binary_plus_harder" ());
       "flatten_pairs" >::
         (fun () ->
            skip_if !debug "debug";
            test_case "flatten_pairs" ());
       "flatten_quadrs" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~abd_rotations:4 "flatten_quadrs" ());
+           test_case "flatten_quadrs" ());
       "equational_reas" >::
         (fun () ->
            skip_if !debug "debug";
@@ -241,29 +242,27 @@ let tests = "InvarGenT" >::: [
       "pointwise-zip2-simpler1" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "pointwise_zip2-simpler1" ());
+           test_case "pointwise_zip2_simpler1" ());
       "pointwise-zip2-simpler2" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "pointwise_zip2-simpler2" ());
+           test_case "pointwise_zip2_simpler2" ());
       "pointwise-zip2-simpler3" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "pointwise_zip2-simpler3" ());
+           test_case "pointwise_zip2_simpler3" ());
       "pointwise-zip2-simpler4" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "pointwise_zip2-simpler4" ());
+           test_case "pointwise_zip2_simpler4" ());
       "pointwise-zip2" >::
         (fun () ->
-           (* This test is close enough. *)
            skip_if !debug "debug";
            test_case "pointwise_zip2" ());
       "pointwise-zip2-harder" >::
         (fun () ->
-           todo "too hard but not call-by-value";
            skip_if !debug "debug";
-           test_case "pointwise_zip2-harder" ());
+           test_case ~do_ml:false "pointwise_zip2_harder" ());
       "pointwise-avl_rotl" >::
         (fun () ->
            skip_if !debug "debug";
@@ -295,7 +294,7 @@ let tests = "InvarGenT" >::: [
       "non_outsidein-rx" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "non_outsidein-rx" ());
+           test_case "non_outsidein_rx" ());
       "non_pointwise-split" >::
         (fun () ->
            skip_if !debug "debug";
@@ -319,11 +318,11 @@ let tests = "InvarGenT" >::: [
       "avl_delmin-simpler" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "avl_delmin-simpler" ());
+           test_case "avl_delmin_simpler" ());
       "non_pointwise-avl_delmin-modified" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "non_pointwise_avl_delmin-modified" ());
+           test_case "non_pointwise_avl_delmin_modified" ());
       "non_pointwise-avl_delmin" >::
         (fun () ->
            skip_if !debug "debug";
@@ -344,19 +343,19 @@ let tests = "InvarGenT" >::: [
         (fun () ->
            todo "currently requiring expanded arguments";
            skip_if !debug "debug";
-           test_case "non_pointwise_fd_comp-harder" ());
+           test_case "non_pointwise_fd_comp_harder" ());
       "non_pointwise-zip1-simpler" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~prefer_guess:true "non_pointwise_zip1-simpler" ());
+           test_case ~prefer_guess:true "non_pointwise_zip1_simpler" ());
       "non_pointwise-zip1-simpler2" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~prefer_guess:true "non_pointwise_zip1-simpler2" ());
+           test_case ~prefer_guess:true "non_pointwise_zip1_simpler2" ());
       "non_pointwise-zip1-modified" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~prefer_guess:true "non_pointwise_zip1-modified" ());
+           test_case ~prefer_guess:true "non_pointwise_zip1_modified" ());
       "non_pointwise-zip1" >::
         (fun () ->
            skip_if !debug "debug";
@@ -377,16 +376,6 @@ let tests = "InvarGenT" >::: [
         (fun () ->
            skip_if !debug "debug";
            test_case "avl_tree" ());
-      "binomial_heap-ins_tree" >::
-        (fun () ->
-           todo "TODO";
-           skip_if !debug "debug";
-           test_case "binomial_heap-ins_tree" ());
-      "binomial_heap-merge" >::
-        (fun () ->
-           todo "TODO";
-           skip_if !debug "debug";
-           test_case "binomial_heap-merge" ());
       "binomial_heap" >::
         (fun () ->
            todo "TODO";
@@ -468,7 +457,7 @@ let tests = "InvarGenT" >::: [
       "liquid_isort-simpler3" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~more_general_num:true "liquid_isort_simpler3" ());
+           test_case "liquid_isort_simpler3" ());
       "liquid_isort-simpler" >::
         (fun () ->
            skip_if !debug "debug";
@@ -567,7 +556,7 @@ let tests = "InvarGenT" >::: [
            test_case ~prefer_bound_to_local:true "liquid_simplex_step_3a" ());
       "liquid_simplex_step_4" >::
         (fun () ->
-           todo "FIXME"; (* "too hard for current InvarGenT"; ? *)
+           todo "too hard for current InvarGenT";
            skip_if !debug "debug";
            test_case "liquid_simplex_step_4" ());
       "liquid_simplex_step_4a" >::
@@ -637,7 +626,7 @@ let tests = "InvarGenT" >::: [
       "liquid_gauss_simpler" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~prefer_bound_to_outer:true "liquid_gauss_simpler" ());
+           test_case "liquid_gauss_simpler" ());
       "liquid_gauss" >::
         (fun () ->
            skip_if !debug "debug";