Merge pull request #3325 from mtzguido/misc

Misc tactics cleanup

Makefile

@@ -40,6 +40,8 @@ clean-snapshot: clean-intermediate
 	$(call msg, "CLEAN SNAPSHOT")
 	$(Q)cd $(DUNE_SNAPSHOT) && { dune clean || true ; }
 	$(Q)rm -rf $(DUNE_SNAPSHOT)/fstar-lib/generated/*
+	$(Q)rm -f src/ocaml-output/fstarc/*
+	$(Q)rm -f src/ocaml-output/fstarlib/*
 
 .PHONY: dune-snapshot
 dune-snapshot:

tests/ide/emacs/fstarmode_gh73.out.expected

@@ -1,5 +1,5 @@
 {"kind": "protocol-info", "rest": "[...]"}
-{"kind": "response", "query-id": "1", "response": [{"level": "warning", "message": "- In the decreases clause for this function, the SMT solver may not be able to\n  prove that the types of\n    s (bound in FStar.Reflection.V2.Compare.fst(77,22-77,23))\n  and b1 (bound in FStar.Reflection.V2.Compare.fst(235,20-235,22))\n  are equal.\n- The type of the first term is: FStar.Stubs.Reflection.Types.term\n- The type of the second term is: FStar.Stubs.Reflection.Types.binder\n- If the proof fails, try annotating these with the same type.\n- See also FStar.Reflection.V2.Compare.fst(77,22-77,23)\n", "number": 290, "ranges": [{"beg": [77, 59], "end": [77, 60], "fname": "FStar.Reflection.V2.Compare.fst"}, {"beg": [77, 22], "end": [77, 23], "fname": "FStar.Reflection.V2.Compare.fst"}]}, {"level": "warning", "message": "- In the decreases clause for this function, the SMT solver may not be able to\n  prove that the types of\n    FStar.Ghost.reveal b1\n    (bound in\n    FStar.Reflection.V2.Compare.fst(182,25-182,40))\n  and b1 (bound in FStar.Reflection.V2.Compare.fst(235,20-235,22))\n  are equal.\n- The type of the first term is: FStar.Stubs.Reflection.Types.term\n- The type of the second term is: FStar.Stubs.Reflection.Types.binder\n- If the proof fails, try annotating these with the same type.\n", "number": 290, "ranges": [{"beg": [182, 25], "end": [182, 40], "fname": "FStar.Reflection.V2.Compare.fst"}]}, {"level": "warning", "message": "- In the decreases clause for this function, the SMT solver may not be able to\n  prove that the types of\n    FStar.Ghost.reveal b1\n    (bound in\n    FStar.Reflection.V2.Compare.fst(199,25-199,40))\n  and b1 (bound in FStar.Reflection.V2.Compare.fst(235,20-235,22))\n  are equal.\n- The type of the first term is: FStar.Stubs.Reflection.Types.term\n- The type of the second term is: FStar.Stubs.Reflection.Types.binder\n- If the proof fails, try annotating these with the same type.\n", "number": 290, "ranges": [{"beg": [199, 25], "end": [199, 40], "fname": "FStar.Reflection.V2.Compare.fst"}]}, {"level": "warning", "message": "- In the decreases clause for this function, the SMT solver may not be able to\n  prove that the types of\n    b1 (bound in FStar.Reflection.V2.Compare.fst(235,20-235,22))\n  and s (bound in FStar.Reflection.V2.Compare.fst(77,22-77,23))\n  are equal.\n- The type of the first term is: FStar.Stubs.Reflection.Types.binder\n- The type of the second term is: FStar.Stubs.Reflection.Types.term\n- If the proof fails, try annotating these with the same type.\n", "number": 290, "ranges": [{"beg": [235, 20], "end": [235, 22], "fname": "FStar.Reflection.V2.Compare.fst"}]}, {"level": "warning", "message": "- In the decreases clause for this function, the SMT solver may not be able to\n  prove that the types of\n    b1 (bound in FStar.Reflection.V2.Compare.fst(235,20-235,22))\n  and\n    FStar.Ghost.reveal b1\n    (bound in\n    FStar.Reflection.V2.Compare.fst(182,25-182,40))\n  are equal.\n- The type of the first term is: FStar.Stubs.Reflection.Types.binder\n- The type of the second term is: FStar.Stubs.Reflection.Types.term\n- If the proof fails, try annotating these with the same type.\n", "number": 290, "ranges": [{"beg": [235, 20], "end": [235, 22], "fname": "FStar.Reflection.V2.Compare.fst"}]}, {"level": "warning", "message": "- In the decreases clause for this function, the SMT solver may not be able to\n  prove that the types of\n    b1 (bound in FStar.Reflection.V2.Compare.fst(235,20-235,22))\n  and\n    FStar.Ghost.reveal b1\n    (bound in\n    FStar.Reflection.V2.Compare.fst(199,25-199,40))\n  are equal.\n- The type of the first term is: FStar.Stubs.Reflection.Types.binder\n- The type of the second term is: FStar.Stubs.Reflection.Types.term\n- If the proof fails, try annotating these with the same type.\n", "number": 290, "ranges": [{"beg": [235, 20], "end": [235, 22], "fname": "FStar.Reflection.V2.Compare.fst"}]}, {"level": "warning", "message": "- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n- Use FStar.Reflection.V2.TermEq.term_eq\n- See also FStar.Stubs.Reflection.V2.Builtins.fsti(167,0-167,48)\n", "number": 288, "ranges": [{"beg": [135, 17], "end": [135, 24], "fname": "FStar.Reflection.V2.Formula.fst"}, {"beg": [167, 0], "end": [167, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n- Use FStar.Reflection.V2.TermEq.term_eq\n- See also FStar.Stubs.Reflection.V2.Builtins.fsti(167,0-167,48)\n", "number": 288, "ranges": [{"beg": [136, 22], "end": [136, 29], "fname": "FStar.Reflection.V2.Formula.fst"}, {"beg": [167, 0], "end": [167, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "- Adding an implicit 'assume new' qualifier on document\n", "number": 239, "ranges": [{"beg": [36, 5], "end": [36, 13], "fname": "FStar.Stubs.Pprint.fsti"}]}, {"level": "warning", "message": "- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n- Use FStar.Reflection.V2.TermEq.term_eq\n- See also FStar.Stubs.Reflection.V2.Builtins.fsti(167,0-167,48)\n", "number": 288, "ranges": [{"beg": [623, 15], "end": [623, 22], "fname": "FStar.Tactics.V2.Derived.fst"}, {"beg": [167, 0], "end": [167, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n- Use FStar.Reflection.V2.TermEq.term_eq\n- See also FStar.Stubs.Reflection.V2.Builtins.fsti(167,0-167,48)\n", "number": 288, "ranges": [{"beg": [176, 11], "end": [176, 18], "fname": "FStar.Tactics.V2.Logic.fst"}, {"beg": [167, 0], "end": [167, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "- Pattern uses these theory symbols or terms that should not be in an SMT\n  pattern:\n    Prims.op_Subtraction\n", "number": 271, "ranges": [{"beg": [434, 8], "end": [434, 51], "fname": "FStar.UInt.fsti"}]}], "status": "success"}
+{"kind": "response", "query-id": "1", "response": [{"level": "warning", "message": "- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n- Use FStar.Reflection.V2.TermEq.term_eq\n- See also FStar.Stubs.Reflection.V2.Builtins.fsti(167,0-167,48)\n", "number": 288, "ranges": [{"beg": [135, 17], "end": [135, 24], "fname": "FStar.Reflection.V2.Formula.fst"}, {"beg": [167, 0], "end": [167, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n- Use FStar.Reflection.V2.TermEq.term_eq\n- See also FStar.Stubs.Reflection.V2.Builtins.fsti(167,0-167,48)\n", "number": 288, "ranges": [{"beg": [136, 22], "end": [136, 29], "fname": "FStar.Reflection.V2.Formula.fst"}, {"beg": [167, 0], "end": [167, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "- Adding an implicit 'assume new' qualifier on document\n", "number": 239, "ranges": [{"beg": [36, 5], "end": [36, 13], "fname": "FStar.Stubs.Pprint.fsti"}]}, {"level": "warning", "message": "- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n- Use FStar.Reflection.V2.TermEq.term_eq\n- See also FStar.Stubs.Reflection.V2.Builtins.fsti(167,0-167,48)\n", "number": 288, "ranges": [{"beg": [623, 15], "end": [623, 22], "fname": "FStar.Tactics.V2.Derived.fst"}, {"beg": [167, 0], "end": [167, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n- Use FStar.Reflection.V2.TermEq.term_eq\n- See also FStar.Stubs.Reflection.V2.Builtins.fsti(167,0-167,48)\n", "number": 288, "ranges": [{"beg": [176, 11], "end": [176, 18], "fname": "FStar.Tactics.V2.Logic.fst"}, {"beg": [167, 0], "end": [167, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "- Pattern uses these theory symbols or terms that should not be in an SMT\n  pattern:\n    Prims.op_Subtraction\n", "number": 271, "ranges": [{"beg": [434, 8], "end": [434, 51], "fname": "FStar.UInt.fsti"}]}], "status": "success"}
 {"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "- Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "success"}
 {"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "failure"}
 {"kind": "response", "query-id": "4", "response": [], "status": "success"}

ulib/FStar.Order.fst

@@ -15,6 +15,7 @@
 *)
 module FStar.Order
 
+[@@plugin]
 type order = | Lt | Eq | Gt
 
 // Some derived checks

ulib/FStar.Reflection.V1.Compare.fsti

@@ -0,0 +1,19 @@
+(*
+   Copyright 2008-2018 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module FStar.Reflection.V1.Compare
+
+(* The V2 module is generic already, and does not make any V1/V2 distinction. *)
+include FStar.Reflection.V2.Compare