From 032740de9fb9f9448a7b008815a216c6312cf739 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 15 Feb 2022 22:20:04 -0800 Subject: [PATCH 1/9] working towards making the basic logical connectives in prims based on the standard types currently defined in Pervasives etc. --- examples/layeredeffects/RunST.fst | 4 +- .../InjectiveTypeFormers.Explicit.fst | 4 +- examples/paradoxes/InjectiveTypeFormers.fst | 108 ------------------ src/basic/boot/FStar.Compiler.Util.fsi | 6 +- src/ocaml-output/FStar_Parser_Const.ml | 6 +- src/ocaml-output/FStar_Syntax_Util.ml | 2 +- .../FStar_TypeChecker_TcInductive.ml | 2 +- src/parser/FStar.Parser.Const.fs | 10 +- src/smtencoding/FStar.SMTEncoding.Encode.fs | 2 +- src/smtencoding/FStar.SMTEncoding.Encode.fsi | 1 - .../FStar.SMTEncoding.EncodeTerm.fs | 2 +- .../FStar.SMTEncoding.EncodeTerm.fsi | 2 +- src/smtencoding/FStar.SMTEncoding.Env.fs | 3 +- src/syntax/FStar.Syntax.Free.fs | 2 +- src/syntax/FStar.Syntax.Syntax.fs | 4 +- src/syntax/FStar.Syntax.Syntax.fsi | 7 +- src/syntax/FStar.Syntax.Util.fs | 4 +- .../FStar.TypeChecker.TcInductive.fs | 2 +- ulib/FStar.Classical.fst | 14 +-- ulib/FStar.IndefiniteDescription.fst | 6 +- ulib/FStar.SquashProperties.fst | 22 ++-- ulib/experimental/Steel.Effect.Common.fsti | 2 +- ulib/fs/prims.fs | 20 ++-- ulib/ml/prims.ml | 38 +++--- ulib/prims.fst | 25 ++-- 25 files changed, 95 insertions(+), 203 deletions(-) delete mode 100644 examples/paradoxes/InjectiveTypeFormers.fst diff --git a/examples/layeredeffects/RunST.fst b/examples/layeredeffects/RunST.fst index 77c1acff4d1..2c102d90807 100644 --- a/examples/layeredeffects/RunST.fst +++ b/examples/layeredeffects/RunST.fst @@ -27,7 +27,7 @@ noeq type action : inp:Type0 -> out:Type0 -> st0:Type0 -> st1:Type0 -> Type u#1 = | Read : #st0:Type -> action unit st0 st0 st0 | Write : #st0:Type -> #st1:Type -> action st1 unit st0 st1 - | Raise : #st0:Type -> #st1:Type -> action exn c_False st0 st1 + | Raise : #st0:Type -> #st1:Type -> action exn Prims.empty st0 st1 // alternative: exceptions do not change state // | Raise : #a:Type -> #st0:Type -> action exn a st0 st0 @@ -294,7 +294,7 @@ let rec _catchST (#a:Type0) #labs #si #sf | Op Read _i k -> _catchST #a #labs stt (k s0) s0 | Op Write s k -> _catchST #a #labs stt (k ()) s | Op Raise e k -> - let k' (o : c_False) : repr (a & sf) stt stt labs = + let k' (o : Prims.empty) : repr (a & sf) stt stt labs = unreachable () in Op Raise e k' diff --git a/examples/paradoxes/InjectiveTypeFormers.Explicit.fst b/examples/paradoxes/InjectiveTypeFormers.Explicit.fst index a616756e6cf..45a9078f34e 100644 --- a/examples/paradoxes/InjectiveTypeFormers.Explicit.fst +++ b/examples/paradoxes/InjectiveTypeFormers.Explicit.fst @@ -32,7 +32,7 @@ val false_of_pq : p q -> Lemma False let false_of_pq pq = FStar.Classical.( exists_elim - c_False + Prims.empty (give_witness pq) (fun (a:(Type u#1 -> Type u#0){i a == q /\ ~(a q)}) -> isInj_admit p a w)) @@ -40,7 +40,7 @@ let false_of_pq pq = let false_of_pq_squash (pq: p q) : GTot False = false_of_pq pq; - coerce (FStar.Squash.return_squash #c_False (match () with)) + coerce (FStar.Squash.return_squash #Prims.empty (match () with)) let not_pq : ~ (p q) = FStar.Classical.give_witness diff --git a/examples/paradoxes/InjectiveTypeFormers.fst b/examples/paradoxes/InjectiveTypeFormers.fst deleted file mode 100644 index 0cb7d22915c..00000000000 --- a/examples/paradoxes/InjectiveTypeFormers.fst +++ /dev/null @@ -1,108 +0,0 @@ -(* - 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 InjectiveTypeFormers -// We need the --__temp_no_proj flag to workaround an F* bug related to generating code for projectors - -// F* unfortunately still includes injective type formers; -// these are known to be inconsistent; -// ported inconsistency proof from Lean: -// https://gist.github.com/leodemoura/0c88341bb585bf9a72e6 -open FStar.Constructive - -(* this file relies on a violation of the cardinality constraints of Type*) -#set-options "--cardinality warn --print_universes --print_bound_var_types" - -noeq type i: (Type u#a -> Type u#b) -> Type u#(max (a + 1) (b + 1)) = -| Mk: f:(Type -> Type) -> i f - -val injI : x:(Type->Type) -> y:(Type->Type) -> - Lemma (requires (i x == i y)) (ensures (x == y)) -let injI (x:Type->Type) (y:Type->Type) = () - -// Another way to prove injectivity, that doesn't rely on -// projectors for i in the SMT encoding, but does rely -// on inversion and "typing elimination" for Mk -// Namely: that if x : i f then x = Mk e for some e -// and: that if Mk e : i f then e = f -(* -val injI_ : x:(Type->Type) -> y:(Type->Type) -> i x -> - Lemma (requires (i x == i y)) (ensures (x == y)) -let injI_ (x:Type->Type) (y:Type->Type) ix = () - -val injI : x:(Type->Type) -> y:(Type->Type) -> - Lemma (requires (i x == i y)) (ensures (x == y)) -let injI (x:Type->Type) (y:Type->Type) = injI_ x y (Mk x) -*) - -// P in SMT logic -- accepted but hard to use for the rest of the proof -// (the SMT solver doesn't prove false_of_Pp automatically) -// type P (x:Type) = (exists (a:Type->Type). i a == x /\ ~(a x)) - -// P in constructive logic -- not accepted, for no good reason (filed as #350)! -noeq type cexists_type_to_type : ((Type->Type) -> Type) -> Type = - | ExTypeToTypeIntro : #p:((Type->Type) -> Type) -> t:(Type -> Type) -> - h:(p t) -> cexists_type_to_type p - -val exInd : #p:((Type->Type) -> Type) -> p0:Type -> - (x:(Type->Type) -> p x -> Tot p0) -> cexists_type_to_type p -> Tot p0 -let exInd (#p:((Type->Type) -> Type)) (p0:Type) - (f: (x:(Type->Type) -> p x -> Tot p0)) (h:cexists_type_to_type p) = - match h with - | ExTypeToTypeIntro #q #t h -> f t h - - -#set-options "--log_types" - -(** Hitting non-cumulativity: -(Error) Expected expression of type "Type((S n'ua))"; -got expression "x" of type "Type(n'ua)" -*) -type r (x:Type u#a) = - cexists_type_to_type - (fun (a:Type u#a -> Type0) -> cand (ceq_type (i a) x) (cnot (a x))) - - -val aux : h:r p -> - a:(Type->Type) -> - h12:(cand (ceq_type (i a) p) (cnot (a p))) -> - Tot cfalse -let aux h (a:(Type->Type)) h12 = - let Conj h1 h2 = h12 in - injI a r; // h2 h -- this should finish the proof but causes bogus error - // Subtyping check failed; - // expected type (a (i (fun x -> (cexists_type_to_type - // (fun a -> (cand (ceq_type (i a) x) ((a x) -> Tot cfalse))))))); - // got type (r p) - assert(a == r); -// let h2' : cnot (a p) = magic() in h2' h -- this does not work, -// F* doesn't seem to replace equals by equals in types (filed as #351) - let h2' : cnot (r p) = magic() in h2' h // this does work - -val false_of_rp : r p -> Tot cfalse -let false_of_rp h = - // Using the match directly does not seem to work - // match h with - // | ExTypeToTypeIntro 'p 'a h -> aux h 'a h - exInd // #(fun (a:Type->Type) -> cand (ceq_type (i a) p) (cnot (a p))) - cfalse - (fun (a:(Type->Type)) -> aux h a) // needed an eta expansion - h - -val have_rp : unit -> Tot (r p) -let have_rp () = ExTypeToTypeIntro r (Conj ReflType false_of_rp) - -val contradiction : unit -> Tot cfalse -let contradiction () = false_of_rp (have_rp ()) diff --git a/src/basic/boot/FStar.Compiler.Util.fsi b/src/basic/boot/FStar.Compiler.Util.fsi index b7d464003a0..d79053a5a24 100644 --- a/src/basic/boot/FStar.Compiler.Util.fsi +++ b/src/basic/boot/FStar.Compiler.Util.fsi @@ -15,9 +15,10 @@ *) #light "off" module FStar.Compiler.Util +open Prims open FStar.Pervasives -open FStar.Compiler.Effect module List = FStar.Compiler.List -open FStar.Compiler.Effect module List = FStar.Compiler.List +open FStar.Compiler.Effect +module List = FStar.Compiler.List open FStar.BaseTypes @@ -251,7 +252,6 @@ val getcwd: unit -> string val readdir: string -> list val paths_to_same_file: string -> string -> bool -open Prims val file_exists: string -> Tot val is_directory: string -> Tot diff --git a/src/ocaml-output/FStar_Parser_Const.ml b/src/ocaml-output/FStar_Parser_Const.ml index a06f1a0b0f5..853a5c075ab 100644 --- a/src/ocaml-output/FStar_Parser_Const.ml +++ b/src/ocaml-output/FStar_Parser_Const.ml @@ -68,9 +68,9 @@ let (admit_lid : FStar_Ident.lident) = pconst "admit" let (magic_lid : FStar_Ident.lident) = pconst "magic" let (has_type_lid : FStar_Ident.lident) = pconst "has_type" let (c_true_lid : FStar_Ident.lident) = pconst "c_True" -let (c_false_lid : FStar_Ident.lident) = pconst "c_False" -let (c_and_lid : FStar_Ident.lident) = pconst "c_and" -let (c_or_lid : FStar_Ident.lident) = pconst "c_or" +let (empty_type_lid : FStar_Ident.lident) = pconst "empty" +let (c_and_lid : FStar_Ident.lident) = pconst "tuple2" +let (c_or_lid : FStar_Ident.lident) = pconst "either" let (dtuple2_lid : FStar_Ident.lident) = pconst "dtuple2" let (eq2_lid : FStar_Ident.lident) = pconst "eq2" let (eq3_lid : FStar_Ident.lident) = pconst "op_Equals_Equals_Equals" diff --git a/src/ocaml-output/FStar_Syntax_Util.ml b/src/ocaml-output/FStar_Syntax_Util.ml index 459767b9035..4ea8e4ce731 100644 --- a/src/ocaml-output/FStar_Syntax_Util.ml +++ b/src/ocaml-output/FStar_Syntax_Util.ml @@ -3036,7 +3036,7 @@ let (destruct_sq_base_table : [(FStar_Parser_Const.c_eq2_lid, FStar_Parser_Const.c_eq2_lid)]); (Prims.int_zero, [(FStar_Parser_Const.c_true_lid, FStar_Parser_Const.true_lid); - (FStar_Parser_Const.c_false_lid, FStar_Parser_Const.false_lid)])] + (FStar_Parser_Const.empty_type_lid, FStar_Parser_Const.false_lid)])] let (destruct_typ_as_formula : FStar_Syntax_Syntax.term -> connective FStar_Pervasives_Native.option) = fun f -> diff --git a/src/ocaml-output/FStar_TypeChecker_TcInductive.ml b/src/ocaml-output/FStar_TypeChecker_TcInductive.ml index a21b06e5418..c03606fe4e1 100644 --- a/src/ocaml-output/FStar_TypeChecker_TcInductive.ml +++ b/src/ocaml-output/FStar_TypeChecker_TcInductive.ml @@ -1884,7 +1884,7 @@ let (check_inductive_well_typedness : | uu___6 -> ())); (sig_bndle, tcs1, datas2)))))) let (early_prims_inductives : Prims.string Prims.list) = - ["c_False"; "c_True"; "equals"; "c_and"; "c_or"] + ["empty"; "c_True"; "equals"; "tuple2"; "either"] let (mk_discriminator_and_indexed_projectors : FStar_Syntax_Syntax.qualifier Prims.list -> FStar_Syntax_Syntax.attribute Prims.list -> diff --git a/src/parser/FStar.Parser.Const.fs b/src/parser/FStar.Parser.Const.fs index b62753ace8a..de8c7416069 100644 --- a/src/parser/FStar.Parser.Const.fs +++ b/src/parser/FStar.Parser.Const.fs @@ -104,11 +104,11 @@ let magic_lid = pconst "magic" let has_type_lid = pconst "has_type" (* Constructive variants *) -let c_true_lid = pconst "c_True" -let c_false_lid = pconst "c_False" -let c_and_lid = pconst "c_and" -let c_or_lid = pconst "c_or" -let dtuple2_lid = pconst "dtuple2" // for l_Exists +let c_true_lid = pconst "c_True" +let empty_type_lid = pconst "empty" +let c_and_lid = pconst "tuple2" +let c_or_lid = pconst "either" +let dtuple2_lid = pconst "dtuple2" // for l_Exists (* Various equality predicates *) let eq2_lid = pconst "eq2" diff --git a/src/smtencoding/FStar.SMTEncoding.Encode.fs b/src/smtencoding/FStar.SMTEncoding.Encode.fs index 4dadb4cb285..7f66af7c86e 100644 --- a/src/smtencoding/FStar.SMTEncoding.Encode.fs +++ b/src/smtencoding/FStar.SMTEncoding.Encode.fs @@ -16,10 +16,10 @@ #light "off" module FStar.SMTEncoding.Encode +open Prims open FStar.Pervasives open FStar.Compiler.Effect open FStar.Compiler.List -open Prims open FStar open FStar.Compiler open FStar.TypeChecker.Env diff --git a/src/smtencoding/FStar.SMTEncoding.Encode.fsi b/src/smtencoding/FStar.SMTEncoding.Encode.fsi index c109a1f04f7..430f409d1cd 100644 --- a/src/smtencoding/FStar.SMTEncoding.Encode.fsi +++ b/src/smtencoding/FStar.SMTEncoding.Encode.fsi @@ -17,7 +17,6 @@ module FStar.SMTEncoding.Encode open FStar.Compiler.Effect -open FStar.Compiler.Effect open FStar.SMTEncoding.Term module ErrorReporting = FStar.SMTEncoding.ErrorReporting module S = FStar.Syntax.Syntax diff --git a/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fs b/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fs index d500181a9f6..1fc9cf730b0 100644 --- a/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fs +++ b/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fs @@ -16,10 +16,10 @@ #light "off" module FStar.SMTEncoding.EncodeTerm +open Prims open FStar.Pervasives open FStar.Compiler.Effect open FStar.Compiler.List -open Prims open FStar open FStar.Compiler open FStar.TypeChecker.Env diff --git a/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fsi b/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fsi index bad9bb9c8d0..759ae28b476 100644 --- a/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fsi +++ b/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fsi @@ -16,10 +16,10 @@ #light "off" module FStar.SMTEncoding.EncodeTerm +open Prims open FStar.Pervasives open FStar.Compiler.Effect open FStar.Compiler.Effect -open Prims open FStar open FStar.Compiler open FStar.TypeChecker.Env diff --git a/src/smtencoding/FStar.SMTEncoding.Env.fs b/src/smtencoding/FStar.SMTEncoding.Env.fs index 1ec533b845a..4cf3373257a 100644 --- a/src/smtencoding/FStar.SMTEncoding.Env.fs +++ b/src/smtencoding/FStar.SMTEncoding.Env.fs @@ -16,10 +16,9 @@ #light "off" module FStar.SMTEncoding.Env +open Prims open FStar.Pervasives open FStar.Compiler.Effect -open FStar.Compiler.Effect -open Prims open FStar open FStar.Compiler open FStar.TypeChecker.Env diff --git a/src/syntax/FStar.Syntax.Free.fs b/src/syntax/FStar.Syntax.Free.fs index 4d3d8c716b3..322ca9d6846 100644 --- a/src/syntax/FStar.Syntax.Free.fs +++ b/src/syntax/FStar.Syntax.Free.fs @@ -16,11 +16,11 @@ #light "off" // (c) Microsoft Corporation. All rights reserved module FStar.Syntax.Free +open Prims open FStar.Pervasives open FStar.Compiler.Effect open FStar.Compiler.List -open Prims open FStar open FStar.Compiler open FStar.Compiler.Util diff --git a/src/syntax/FStar.Syntax.Syntax.fs b/src/syntax/FStar.Syntax.Syntax.fs index ad0811befe7..db708d21353 100644 --- a/src/syntax/FStar.Syntax.Syntax.fs +++ b/src/syntax/FStar.Syntax.Syntax.fs @@ -15,13 +15,13 @@ *) #light "off" module FStar.Syntax.Syntax +(* Prims is used for bootstrapping *) +open Prims open FStar.Pervasives open FStar.Compiler.Effect open FStar.Compiler.List (* Type definitions for the core AST *) -(* Prims is used for bootstrapping *) -open Prims open FStar open FStar.Compiler open FStar.Compiler.Util diff --git a/src/syntax/FStar.Syntax.Syntax.fsi b/src/syntax/FStar.Syntax.Syntax.fsi index e6b3703af96..382e5415736 100644 --- a/src/syntax/FStar.Syntax.Syntax.fsi +++ b/src/syntax/FStar.Syntax.Syntax.fsi @@ -15,14 +15,15 @@ *) #light "off" module FStar.Syntax.Syntax +(* Prims is used for bootstrapping *) +open Prims open FStar.Pervasives open FStar.Compiler.Effect open FStar.Compiler.Effect (* Type definitions for the core AST *) -(* Prims is used for bootstrapping *) -open Prims -open FStar open FStar.Compiler +open FStar +open FStar.Compiler open FStar.Compiler.Util open FStar.Compiler.Range open FStar.Ident diff --git a/src/syntax/FStar.Syntax.Util.fs b/src/syntax/FStar.Syntax.Util.fs index 2254d877b15..0b728a5a170 100644 --- a/src/syntax/FStar.Syntax.Util.fs +++ b/src/syntax/FStar.Syntax.Util.fs @@ -16,11 +16,11 @@ #light "off" // (c) Microsoft Corporation. All rights reserved module FStar.Syntax.Util +open Prims open FStar.Pervasives open FStar.Compiler.Effect open FStar.Compiler.List -open Prims open FStar open FStar.Compiler open FStar.Compiler.Util @@ -1496,7 +1496,7 @@ let destruct_sq_base_table = (PC.c_or_lid, PC.or_lid); (PC.c_eq2_lid, PC.c_eq2_lid)]); (3, [(PC.c_eq2_lid, PC.c_eq2_lid)]); - (0, [(PC.c_true_lid, PC.true_lid); (PC.c_false_lid, PC.false_lid)]) + (0, [(PC.c_true_lid, PC.true_lid); (PC.empty_type_lid, PC.false_lid)]) ] let destruct_typ_as_formula f : option = diff --git a/src/typechecker/FStar.TypeChecker.TcInductive.fs b/src/typechecker/FStar.TypeChecker.TcInductive.fs index 46989d5567a..7826ab3670a 100644 --- a/src/typechecker/FStar.TypeChecker.TcInductive.fs +++ b/src/typechecker/FStar.TypeChecker.TcInductive.fs @@ -780,7 +780,7 @@ let check_inductive_well_typedness (env:env_t) (ses:list) (quals:list) (* Attributes of the envelopping bundle *) diff --git a/ulib/FStar.Classical.fst b/ulib/FStar.Classical.fst index c67e33cddd6..abfb0797026 100644 --- a/ulib/FStar.Classical.fst +++ b/ulib/FStar.Classical.fst @@ -51,13 +51,13 @@ let move_requires #a #p #q f x = give_proof (bind_squash (get_proof (l_or (p x) (~(p x)))) (fun (b: l_or (p x) (~(p x))) -> bind_squash b - (fun (b': c_or (p x) (~(p x))) -> + (fun (b': Prims.either (p x) (~(p x))) -> match b' with - | Left hp -> + | Prims.Inl hp -> give_witness hp; f x; get_proof (p x ==> q x) - | Right hnp -> give_witness hnp))) + | Prims.Inr hnp -> give_witness hnp))) let move_requires_2 #a #b #p #q f x y = move_requires (f x) y @@ -133,13 +133,13 @@ let ghost_lemma #a #p #q f = give_proof (bind_squash (get_proof (l_or (p x) (~(p x)))) (fun (b: l_or (p x) (~(p x))) -> bind_squash b - (fun (b': c_or (p x) (~(p x))) -> + (fun (b': Prims.either (p x) (~(p x))) -> match b' with - | Left hp -> + | Prims.Inl hp -> give_witness hp; f x; get_proof (p x ==> q x ()) - | Right hnp -> give_witness hnp)))) + | Prims.Inr hnp -> give_witness hnp)))) in forall_intro lem @@ -158,7 +158,7 @@ let exists_intro_not_all_not (#a:Type) (#p:a -> Type) = bind_squash (get_proof (forall x. ~ (p x))) (fun (g: (forall x. ~ (p x))) -> - bind_squash #(x:a -> GTot (~(p x))) #c_False g + bind_squash #(x:a -> GTot (~(p x))) #Prims.empty g (fun (h:(x:a -> GTot (~(p x)))) -> f h)) in () diff --git a/ulib/FStar.IndefiniteDescription.fst b/ulib/FStar.IndefiniteDescription.fst index 61959b7eae0..6e5a4be4e0f 100644 --- a/ulib/FStar.IndefiniteDescription.fst +++ b/ulib/FStar.IndefiniteDescription.fst @@ -68,13 +68,13 @@ let strong_excluded_middle (p: Type0) : GTot (b: bool{b = true <==> p}) = give_proof (bind_squash (get_proof (l_or p (~p))) (fun (b: l_or p (~p)) -> bind_squash b - (fun (b': c_or p (~p)) -> + (fun (b': Prims.either p (~p)) -> match b' with - | Left hp -> + | Prims.Inl hp -> give_witness hp; exists_intro (fun b -> b = true <==> p) true; get_proof (exists b. b = true <==> p) - | Right hnp -> + | Prims.Inr hnp -> give_witness hnp; exists_intro (fun b -> b = true <==> p) false; get_proof (exists b. b = true <==> p)))) diff --git a/ulib/FStar.SquashProperties.fst b/ulib/FStar.SquashProperties.fst index df975ee408a..1f0a48fe0c5 100644 --- a/ulib/FStar.SquashProperties.fst +++ b/ulib/FStar.SquashProperties.fst @@ -49,12 +49,12 @@ let forall_intro #a #p f = (* The whole point of defining squash is to soundly allow define excluded_middle; here this follows from get_proof and give_proof *) -val bool_of_or : #p:Type -> #q:Type -> c_or p q -> +val bool_of_or : #p:Type -> #q:Type -> Prims.either p q -> Tot (b:bool{(b ==> p) /\ (not(b) ==> q)}) let bool_of_or #p #q t = match t with - | Left _ -> true - | Right _ -> false + | Prims.Inl _ -> true + | Prims.Inr _ -> false val excluded_middle : p:Type -> GTot (squash (b:bool{b <==> p})) let excluded_middle (p:Type) = map_squash (join_squash (get_proof (p \/ (~p)))) bool_of_or @@ -64,9 +64,9 @@ val excluded_middle_squash : p:Type0 -> GTot (p \/ ~p) let excluded_middle_squash p = bind_squash (excluded_middle p) (fun x -> if x then - map_squash (get_proof p) (Left #p) + map_squash (get_proof p) (Prims.Inl #p) else - return_squash (Right #_ #(~p) (return_squash (fun (h:p) -> + return_squash (Prims.Inr #_ #(~p) (return_squash (fun (h:p) -> give_proof (return_squash h); false_elim #False ())))) @@ -76,10 +76,10 @@ let excluded_middle_squash p = val ifProp: #p:Type0 -> b:Type0 -> e1:squash p -> e2:squash p -> GTot (squash p) let ifProp #p b e1 e2 = bind_squash (excluded_middle_squash b) - (fun (x:c_or b (~ b)) -> + (fun (x:Prims.either b (~ b)) -> match x with - | Left _ -> e1 - | Right _ -> e2) + | Prims.Inl _ -> e1 + | Prims.Inr _ -> e2) (* The powerset operator *) type pow (p:Type) = p -> GTot bool @@ -107,11 +107,11 @@ let false_elim (#a:Type) (f:False) : Tot a val l1: (a:Type0) -> (b:Type0) -> GTot (squash (retract_cond (pow a) (pow b))) let l1 (a:Type) (b:Type) = bind_squash (excluded_middle_squash (retract (pow a) (pow b))) - (fun (x:c_or (retract (pow a) (pow b)) (~ (retract (pow a) (pow b)))) -> + (fun (x:Prims.either (retract (pow a) (pow b)) (~ (retract (pow a) (pow b)))) -> match x with - | Left (MkR f0 g0 e) -> + | Prims.Inl (MkR f0 g0 e) -> return_squash (MkC f0 g0 (fun _ -> e)) - | Right nr -> + | Prims.Inr nr -> let f0 (x:pow a) (y:b) = false in let g0 (x:pow b) (y:a) = false in map_squash nr (fun (f:(retract (pow a) (pow b) -> GTot False)) -> diff --git a/ulib/experimental/Steel.Effect.Common.fsti b/ulib/experimental/Steel.Effect.Common.fsti index 4d027d3319d..b28d060633d 100644 --- a/ulib/experimental/Steel.Effect.Common.fsti +++ b/ulib/experimental/Steel.Effect.Common.fsti @@ -2350,7 +2350,7 @@ let init_resolve_tac () : Tac unit = (* AF: There probably is a simpler way to get from p to squash p in a tactic, so that we can use apply_lemma *) let squash_and p (x:squash (p /\ True)) : (p /\ True) = - let x : squash (p `c_and` True) = FStar.Squash.join_squash x in + let x : squash (p `Prims.tuple2` True) = FStar.Squash.join_squash x in x /// Calling into the framing tactic to ensure that the vprop whose selector we are trying to access is in the context diff --git a/ulib/fs/prims.fs b/ulib/fs/prims.fs index 51cb6e1db37..a05d0f8a964 100644 --- a/ulib/fs/prims.fs +++ b/ulib/fs/prims.fs @@ -59,22 +59,22 @@ type 'd b2t = B2t of unit type 'a squash = Squash of unit -type (' p, ' q) c_or = - | Left of ' p - | Right of ' q +type (' p, ' q) either = + | Inl of ' p + | Inr of ' q -type (' p, ' q) l_or = ('p, 'q) c_or squash +type (' p, ' q) l_or = ('p, 'q) either squash -let uu___is_Left = function Left _ -> true | Right _ -> false +let uu___is_Inl = function Inl _ -> true | Inr _ -> false -let uu___is_Right = function Left _ -> false | Right _ -> true +let uu___is_Inr = function Inl _ -> false | Inr _ -> true -type (' p, ' q) c_and = -| And of ' p * ' q +type (' p, ' q) tuple2 = +| Mktuple2 of ' p * ' q -type (' p, ' q) l_and = ('p, 'q) c_and squash +type (' p, ' q) l_and = ('p, 'q) tuple2 squash -let uu___is_And _ = true +let uu___is_Mktuple2 _ = true type c_True = diff --git a/ulib/ml/prims.ml b/ulib/ml/prims.ml index 4f671418940..3e6f6a3cea3 100644 --- a/ulib/ml/prims.ml +++ b/ulib/ml/prims.ml @@ -20,7 +20,7 @@ type bool' = bool [@@deriving yojson,show] type bool = bool' [@@deriving yojson,show] -type c_False = unit +type empty = unit (*This is how Coq extracts Inductive void := . Our extraction needs to be fixed to recognize when there are no constructors and generate this type abbreviation*) type c_True = @@ -38,30 +38,30 @@ let uu___is_Refl : 'Aa . 'Aa -> 'Aa -> ('Aa,unit,unit) equals -> bool = type ('Aa,'Ax,'Ay) eq2 = unit type ('Aa,'Ab,'Ax,'Ay) op_Equals_Equals_Equals = unit type 'Ab b2t = unit -type ('Ap,'Aq) c_and = - | And of 'Ap * 'Aq -let uu___is_And : 'Ap 'Aq . ('Ap,'Aq) c_and -> bool = +type ('Ap,'Aq) tuple2 = + | Mktuple2 of 'Ap * 'Aq +let uu___is_Mktuple2 : 'Ap 'Aq . ('Ap,'Aq) tuple2 -> bool = fun projectee -> true -let __proj__And__item___0 : 'Ap 'Aq . ('Ap,'Aq) c_and -> 'Ap = - fun projectee -> match projectee with | And (_0,_1) -> _0 -let __proj__And__item___1 : 'Ap 'Aq . ('Ap,'Aq) c_and -> 'Aq = - fun projectee -> match projectee with | And (_0,_1) -> _1 +let __proj__Mktuple2__item___1 : 'Ap 'Aq . ('Ap,'Aq) tuple2 -> 'Ap = + fun projectee -> match projectee with | Mktuple2 (_0,_1) -> _0 +let __proj__Mktuple2__item___2 : 'Ap 'Aq . ('Ap,'Aq) tuple2 -> 'Aq = + fun projectee -> match projectee with | Mktuple2 (_0,_1) -> _1 type ('Ap,'Aq) l_and = unit -type ('Ap,'Aq) c_or = - | Left of 'Ap - | Right of 'Aq -let uu___is_Left : 'Ap 'Aq . ('Ap,'Aq) c_or -> bool = +type ('Ap,'Aq) either = + | Inl of 'Ap + | Inr of 'Aq +let uu___is_Inl : 'Ap 'Aq . ('Ap,'Aq) either -> bool = fun projectee -> - match projectee with | Left _0 -> true | uu____344 -> false + match projectee with | Inl _0 -> true | uu____344 -> false -let __proj__Left__item___0 : 'Ap 'Aq . ('Ap,'Aq) c_or -> 'Ap = - fun projectee -> match projectee with | Left _0 -> _0 -let uu___is_Right : 'Ap 'Aq . ('Ap,'Aq) c_or -> bool = +let __proj__Inl__item___0 : 'Ap 'Aq . ('Ap,'Aq) either -> 'Ap = + fun projectee -> match projectee with | Inl _0 -> _0 +let uu___is_Inr : 'Ap 'Aq . ('Ap,'Aq) either -> bool = fun projectee -> - match projectee with | Right _0 -> true | uu____404 -> false + match projectee with | Inr _0 -> true | uu____404 -> false -let __proj__Right__item___0 : 'Ap 'Aq . ('Ap,'Aq) c_or -> 'Aq = - fun projectee -> match projectee with | Right _0 -> _0 +let __proj__Inr__item___0 : 'Ap 'Aq . ('Ap,'Aq) either -> 'Aq = + fun projectee -> match projectee with | Inr _0 -> _0 type ('Ap,'Aq) l_or = unit type ('Ap,'Aq) l_imp = unit type ('Ap,'Aq) l_iff = unit diff --git a/ulib/prims.fst b/ulib/prims.fst index 4d1dfae8149..92252f2aa45 100644 --- a/ulib/prims.fst +++ b/ulib/prims.fst @@ -58,14 +58,14 @@ type eqtype = a: Type0{hasEq a} assume new type bool : eqtype -(** [c_False] is the empty inductive type. The type with no - inhabitants represents logical falsehood. Note, [c_False] is +(** [empty] is the empty inductive type. The type with no + inhabitants represents logical falsehood. Note, [empty] is seldom used directly in F*. We instead use its "squashed" variant, [False], see below. *) -type c_False = +type empty = (** [c_True] is the singleton inductive type---it is trivially - inhabited. Like [c_False], [c_True] is seldom used. We instead use + inhabited. Like [empty], [c_True] is seldom used. We instead use its "squashed" variants, [True] *) type c_True = | T @@ -135,7 +135,7 @@ let l_True:logical = squash c_True as "False" and rendered in the ide as [Falsee]. It is a squashed version of constructive truth, [c_True]. *) [@@ "tac_opaque"; smt_theory_symbol] -let l_False:logical = squash c_False +let l_False:logical = squash empty (** The type of provable equalities, defined as the usual inductive type with a single constructor for reflexivity. As with the other @@ -159,22 +159,22 @@ type eq2 (#a: Type) (x: a) (y: a) : logical = squash (equals x y) type b2t (b: bool) : logical = (b == true) (** constructive conjunction *) -type c_and (p: Type) (q: Type) = | And : p -> q -> c_and p q +type tuple2 (p: Type) (q: Type) = | Mktuple2 : _1:p -> _2:q -> tuple2 p q (** squashed conjunction, specialized to [Type0], written with an infix binary [/\] *) [@@ "tac_opaque"; smt_theory_symbol] -type l_and (p: logical) (q: logical) : logical = squash (c_and p q) +type l_and (p: logical) (q: logical) : logical = squash (tuple2 p q) (** constructive disjunction *) -type c_or (p: Type) (q: Type) = - | Left : p -> c_or p q - | Right : q -> c_or p q +type either (p: Type) (q: Type) = + | Inl : v:p -> either p q + | Inr : v:q -> either p q (** squashed disjunction, specialized to [Type0], written with an infix binary [\/] *) [@@ "tac_opaque"; smt_theory_symbol] -type l_or (p: logical) (q: logical) : logical = squash (c_or p q) +type l_or (p: logical) (q: logical) : logical = squash (either p q) (** squashed (non-dependent) implication, specialized to [Type0], written with an infix binary [==>]. Note, [==>] binds weaker than @@ -485,7 +485,8 @@ let ( === ) (#a #b: Type) (x: a) (y: b) : logical = a == b /\ x == y (** Dependent pairs [dtuple2] in concrete syntax is [x:a & b x]. Its values can be constructed with the concrete syntax [(| x, y |)] *) unopteq -type dtuple2 (a: Type) (b: (a -> GTot Type)) = | Mkdtuple2 : _1: a -> _2: b _1 -> dtuple2 a b +type dtuple2 (a: Type) (b: (a -> GTot Type)) = + | Mkdtuple2 : _1: a -> _2: b _1 -> dtuple2 a b (** Squashed existential quantification, or dependent sums, are written [exists (x:a). p x] : specialized to Type0 *) From cfa8547a5903ee22f62850aca1fae1bbc5a1f6c5 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 16 Feb 2022 09:09:34 -0800 Subject: [PATCH 2/9] fix up a unit test --- src/tests/FStar.Tests.Unif.fs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tests/FStar.Tests.Unif.fs b/src/tests/FStar.Tests.Unif.fs index 424902b2252..d47fa0525bb 100644 --- a/src/tests/FStar.Tests.Unif.fs +++ b/src/tests/FStar.Tests.Unif.fs @@ -136,7 +136,7 @@ let run_all () = //imitation: unifies u to a constant FStar.Main.process_args () |> ignore; //set options let tm, us = inst 1 (tc "fun u x -> u x") in - let sol = tc "fun x -> c_and x x" in + let sol = tc "fun x -> Prims.tuple2 x x" in unify_check 9 tm sol Trivial From 5a06a94c6e342e8ef09c4cfec514900d44214a5d Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 16 Feb 2022 09:31:58 -0800 Subject: [PATCH 3/9] fix up a couple of refs to old constructors --- ulib/FStar.Classical.Sugar.fst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/ulib/FStar.Classical.Sugar.fst b/ulib/FStar.Classical.Sugar.fst index bfecbb887df..67da905b954 100644 --- a/ulib/FStar.Classical.Sugar.fst +++ b/ulib/FStar.Classical.Sugar.fst @@ -45,9 +45,9 @@ let or_elim_simple bind_squash x (fun p_or_q -> bind_squash p_or_q (fun p_cor_q -> match p_cor_q with - | Left p -> + | Prims.Inl p -> f (return_squash p) - | Right q -> + | Prims.Inr q -> g (return_squash q))) let or_elim @@ -73,7 +73,7 @@ let and_elim (p:Type) : Tot (squash r) = let open FStar.Squash in bind_squash x (fun p_and_q -> - bind_squash p_and_q (fun (And p q) -> + bind_squash p_and_q (fun (Prims.Mktuple2 p q) -> f (return_squash p) (return_squash q))) let forall_intro From b4d7382b35fb774745c9edd2f959cc9aeb71d23c Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 16 Feb 2022 10:42:40 -0800 Subject: [PATCH 4/9] another fixup --- ulib/FStar.LexicographicOrdering.fst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/ulib/FStar.LexicographicOrdering.fst b/ulib/FStar.LexicographicOrdering.fst index 99d11e37a65..0ecd634b06f 100644 --- a/ulib/FStar.LexicographicOrdering.fst +++ b/ulib/FStar.LexicographicOrdering.fst @@ -105,14 +105,14 @@ let lex_to_lex_t #a #b r_a r_b t1 t2 p = : squash (lex_t r_a r_b t1 t2) = bind_squash p (fun p -> match p with - | And (_:dfst t1 == dfst t2) p2 -> + | Prims.Mktuple2 (_:dfst t1 == dfst t2) p2 -> bind_squash p2 (fun p2 -> return_squash (Right_lex #a #b #r_a #r_b (dfst t1) (dsnd t1) (dsnd t2) p2))) in bind_squash p (fun p -> match p with - | Left p1 -> left p1 - | Right p2 -> right p2) + | Prims.Inl p1 -> left p1 + | Prims.Inr p2 -> right p2) let lex_t_non_dep_wf #a #b #r_a #r_b wf_a wf_b = From 470032a547ec532be1ac11d8ef4147c0132e6fe0 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 16 Feb 2022 22:41:15 +0000 Subject: [PATCH 5/9] fixing some test cases --- .../data_structures/BinaryTreesEnumeration.fsti | 4 ++-- examples/hello/TestSeq/TestSeq.fst.hints | 4 ++-- examples/misc/WorkingWithSquashedProofs.fst | 16 ++++++++-------- src/Makefile | 2 +- src/ocaml-output/FStar_Tests_Unif.ml | 2 +- tests/bug-reports/Bug844.fst | 6 +++--- tests/error-messages/Coercions.fst.expected | 10 +++++----- tests/error-messages/NegativeTests.False.fst | 2 +- .../NegativeTests.False.fst.expected | 8 ++++---- .../NegativeTests.Neg.fst.expected | 6 +++--- tests/error-messages/PatAnnot.fst.expected | 4 ++-- .../Test.FunctionalExtensionality.fst.expected | 2 +- .../integration.push-pop.out.expected | 8 ++++---- 13 files changed, 37 insertions(+), 37 deletions(-) diff --git a/examples/data_structures/BinaryTreesEnumeration.fsti b/examples/data_structures/BinaryTreesEnumeration.fsti index 4bab8273cb7..9809a0fdafd 100644 --- a/examples/data_structures/BinaryTreesEnumeration.fsti +++ b/examples/data_structures/BinaryTreesEnumeration.fsti @@ -115,10 +115,10 @@ let rec memP_append_aux #a (x: a) (l: list a) : let pf : squash (x == h \/ List.memP x t) = () in p <-- FStar.Squash.join_squash pf ; match p with - | Left x_eq_h -> + | Prims.Inl x_eq_h -> let l12 = [], t in assert (l == (fst l12) @ (x :: snd l12)) //trigger - | Right mem_x_t -> + | Prims.Inr mem_x_t -> FStar.Classical.exists_elim goal (pure_as_squash (memP_append_aux x) t) diff --git a/examples/hello/TestSeq/TestSeq.fst.hints b/examples/hello/TestSeq/TestSeq.fst.hints index 41acfa2be81..87d6d210052 100755 --- a/examples/hello/TestSeq/TestSeq.fst.hints +++ b/examples/hello/TestSeq/TestSeq.fst.hints @@ -23,7 +23,7 @@ "typing_FStar.Seq.Base.length", "unit_typing" ], 0, - "25cc2c939eb461a1f762a9753136eb31" + "601ee9bf5aa72f07eff6aff22259563b" ], [ "TestSeq.main", @@ -47,7 +47,7 @@ "typing_Tm_abs_f8b7175ad4f28c0bc3c11371abe1d18d" ], 0, - "baa43cd91f4e8cd1710ad84558bac52a" + "4c43b60034e8b75a02622e388be51622" ] ] ] \ No newline at end of file diff --git a/examples/misc/WorkingWithSquashedProofs.fst b/examples/misc/WorkingWithSquashedProofs.fst index 78fe8b8f8e6..c104e8e6a87 100644 --- a/examples/misc/WorkingWithSquashedProofs.fst +++ b/examples/misc/WorkingWithSquashedProofs.fst @@ -83,13 +83,13 @@ let valid_baz (a:Type) (x:a) : Lemma (baz a x) = let s_fb : squash (foo a x \/ bar a x) = foo_or_bar x in FStar.Squash.bind_squash s_fb (fun (fb:(foo a x \/ bar a x)) -> - FStar.Squash.bind_squash fb (fun (c_fb:c_or (foo a x) (bar a x)) -> + FStar.Squash.bind_squash fb (fun (c_fb:Prims.either (foo a x) (bar a x)) -> let s_baz : squash (baz a x) = match c_fb with - | Left f -> + | Prims.Inl f -> // let sf = FStar.Squash.return_squash f in foo_baz x - | Right b -> + | Prims.Inr b -> // let sg = FStar.Squash.return_squash b in bar_baz x in @@ -112,12 +112,12 @@ let valid_baz_alt (a:Type) (x:a) : Lemma (baz a x) = let s_fb : squash (foo a x \/ bar a x) = foo_or_bar x in FStar.Squash.bind_squash s_fb (fun (fb:(foo a x \/ bar a x)) -> - FStar.Squash.bind_squash fb (fun (c_fb:c_or (foo a x) (bar a x)) -> + FStar.Squash.bind_squash fb (fun (c_fb:Prims.either (foo a x) (bar a x)) -> let s_baz : squash (baz a x) = match c_fb with - | Left f -> + | Prims.Inl f -> c_foo_baz x f - | Right b -> + | Prims.Inr b -> c_bar_baz x b in s_baz)) @@ -129,8 +129,8 @@ let elim_squash_or (#r:_) (#p #q:_) (f:squash (p \/ q)) (left: p -> GTot r) (rig = FStar.Squash.bind_squash #_ #r f (fun pq -> FStar.Squash.bind_squash pq (fun c -> match c with - | Left x -> FStar.Squash.return_squash (left x) - | Right x -> FStar.Squash.return_squash (right x))) + | Prims.Inl x -> FStar.Squash.return_squash (left x) + | Prims.Inr x -> FStar.Squash.return_squash (right x))) let valid_baz_alt_alt (a:Type) (x:a) : GTot (squash (baz a x)) diff --git a/src/Makefile b/src/Makefile index e88174efc4d..3d8604e158b 100644 --- a/src/Makefile +++ b/src/Makefile @@ -146,7 +146,7 @@ utest: # The first tests have to be performed sequentially (but each one may use some parallelism) # Adding the F# build and F# tests also here # since in the uregressions target it may not be a good idea to override the fstar.exe binary? -utest-prelude: fsharp-build-and-test +utest-prelude: +$(MAKE) boot-ocaml #build the ocaml-snapshot +$(MAKE) clean_extracted #ensures that there is no leftover from previous extraction +$(MAKE) fstar-ocaml #extract the compiler again and build the result diff --git a/src/ocaml-output/FStar_Tests_Unif.ml b/src/ocaml-output/FStar_Tests_Unif.ml index 48e91ebc255..4ef0966e641 100644 --- a/src/ocaml-output/FStar_Tests_Unif.ml +++ b/src/ocaml-output/FStar_Tests_Unif.ml @@ -235,7 +235,7 @@ let (run_all : unit -> Prims.bool) = inst Prims.int_one uu___14 in match uu___13 with | (tm, us) -> - let sol = FStar_Tests_Pars.tc "fun x -> c_and x x" in + let sol = FStar_Tests_Pars.tc "fun x -> Prims.tuple2 x x" in (unify_check (Prims.of_int (9)) tm sol FStar_TypeChecker_Common.Trivial (fun uu___15 -> diff --git a/tests/bug-reports/Bug844.fst b/tests/bug-reports/Bug844.fst index 7f5ee0eb77e..bb694ab63a1 100644 --- a/tests/bug-reports/Bug844.fst +++ b/tests/bug-reports/Bug844.fst @@ -37,9 +37,9 @@ noeq type retract_cond 'a 'b : Type = val l1: (a:Type0) -> (b:Type0) -> GTot (squash (retract_cond (pow a) (pow b))) let l1 (a:Type) (b:Type) = bind_squash (excluded_middle_squash (retract (pow a) (pow b))) - (fun (x:c_or (retract (pow a) (pow b)) (~ (retract (pow a) (pow b)))) -> + (fun (x:Prims.either (retract (pow a) (pow b)) (~ (retract (pow a) (pow b)))) -> match x with - | Left (MkR f0 g0 e) -> + | Prims.Inl (MkR f0 g0 e) -> return_squash (MkC f0 g0 (fun _ -> e) (* <- this lambda causes the problem *)) - | Right nr -> + | Prims.Inr nr -> magic()) diff --git a/tests/error-messages/Coercions.fst.expected b/tests/error-messages/Coercions.fst.expected index d25d28c0296..4f8af6e4fa7 100644 --- a/tests/error-messages/Coercions.fst.expected +++ b/tests/error-messages/Coercions.fst.expected @@ -5,19 +5,19 @@ Coercions.fst(6,38-6,39): (Error 34) Computed type "Prims.int" and effect "GTot" Coercions.fst(19,37-19,38): (Error 34) Computed type "'a" and effect "GTot" is not compatible with the annotated type "'a" effect "Tot" >>] >> Got issues: [ -Coercions.fst(71,4-71,8): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(672,18-672,24)) +Coercions.fst(71,4-71,8): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(673,18-673,24)) >>] >> Got issues: [ -Coercions.fst(74,49-74,57): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(672,18-672,24)) +Coercions.fst(74,49-74,57): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(673,18-673,24)) >>] >> Got issues: [ -Coercions.fst(76,55-76,56): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(672,18-672,24)) +Coercions.fst(76,55-76,56): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(673,18-673,24)) >>] >> Got issues: [ -Coercions.fst(78,50-78,51): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(672,18-672,24)) +Coercions.fst(78,50-78,51): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(673,18-673,24)) >>] >> Got issues: [ -Coercions.fst(80,51-80,52): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(672,18-672,24)) +Coercions.fst(80,51-80,52): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(673,18-673,24)) >>] Verified module: Coercions All verification conditions discharged successfully diff --git a/tests/error-messages/NegativeTests.False.fst b/tests/error-messages/NegativeTests.False.fst index 7f59724ac05..730590eac2f 100644 --- a/tests/error-messages/NegativeTests.False.fst +++ b/tests/error-messages/NegativeTests.False.fst @@ -27,4 +27,4 @@ val f : p1:(True \/ True) -> p2:(True \/ True) -> Lemma (p1 = p2) let f p1 p2 = () val absurd : unit -> Lemma False [@@expect_failure] // this raises 2 errors on 1-phase, and 4 on 2-phases -let absurd () = f (Left #_ #True T) (Right #True #_ T) //adding implicits to get 2 typing errors +let absurd () = f (Prims.Inl #_ #True T) (Prims.Inr #True #_ T) //adding implicits to get 2 typing errors diff --git a/tests/error-messages/NegativeTests.False.fst.expected b/tests/error-messages/NegativeTests.False.fst.expected index 82ec223275b..1e978a2a949 100644 --- a/tests/error-messages/NegativeTests.False.fst.expected +++ b/tests/error-messages/NegativeTests.False.fst.expected @@ -2,10 +2,10 @@ NegativeTests.False.fst(23,13-23,33): (Error 19) assertion failed; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(444,55-444,67)) >>] >> Got issues: [ -NegativeTests.False.fst(30,18-30,35): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.c_or (*?u1*) _ Prims.l_True" -NegativeTests.False.fst(30,18-30,35): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.c_or Prims.c_True Prims.l_True" -NegativeTests.False.fst(30,36-30,54): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.c_or Prims.l_True (*?u6*) _" -NegativeTests.False.fst(30,36-30,54): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.c_or Prims.l_True Prims.c_True" +NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Inl (Prims.T)" has type "Prims.either (*?u1*) _ Prims.l_True" +NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Inl (Prims.T)" has type "Prims.either Prims.c_True Prims.l_True" +NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Inr (Prims.T)" has type "Prims.either Prims.l_True (*?u6*) _" +NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Inr (Prims.T)" has type "Prims.either Prims.l_True Prims.c_True" >>] NegativeTests.False.fst(21,4-21,7): (Warning 240) Admitting NegativeTests.False.bar without a definition NegativeTests.False.fst(28,4-28,10): (Warning 240) Admitting NegativeTests.False.absurd without a definition diff --git a/tests/error-messages/NegativeTests.Neg.fst.expected b/tests/error-messages/NegativeTests.Neg.fst.expected index 58ce6d6524d..124956923fc 100644 --- a/tests/error-messages/NegativeTests.Neg.fst.expected +++ b/tests/error-messages/NegativeTests.Neg.fst.expected @@ -1,8 +1,8 @@ >> Got issues: [ -NegativeTests.Neg.fst(20,8-20,10): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(672,18-672,24)) +NegativeTests.Neg.fst(20,8-20,10): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(673,18-673,24)) >>] >> Got issues: [ -NegativeTests.Neg.fst(24,8-24,10): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(672,18-672,24)) +NegativeTests.Neg.fst(24,8-24,10): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(673,18-673,24)) >>] >> Got issues: [ NegativeTests.Neg.fst(27,30-27,35): (Error 19) assertion failed; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel @@ -23,7 +23,7 @@ NegativeTests.Neg.fst(46,30-46,31): (Error 19) Subtyping check failed; expected NegativeTests.Neg.fst(50,45-50,47): (Error 19) Subtyping check failed; expected type _: FStar.Pervasives.result Prims.int {V? _}; got type FStar.Pervasives.result Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also FStar.Pervasives.fsti(478,4-478,5)) >>] >> Got issues: [ -NegativeTests.Neg.fst(55,25-55,26): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(672,18-672,24)) +NegativeTests.Neg.fst(55,25-55,26): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(673,18-673,24)) >>] >> Got issues: [ NegativeTests.Neg.fst(59,0-60,17): (Error 309) Type annotation _: Type0{NegativeTests.Neg.phi_1510} for inductive NegativeTests.Neg.t is not Type or eqtype, or it is eqtype but contains unopteq qualifier diff --git a/tests/error-messages/PatAnnot.fst.expected b/tests/error-messages/PatAnnot.fst.expected index 4f6268ea620..d16d07a2a06 100644 --- a/tests/error-messages/PatAnnot.fst.expected +++ b/tests/error-messages/PatAnnot.fst.expected @@ -11,10 +11,10 @@ PatAnnot.fst(33,0-35,14): (Error 19) assertion failed (Also see: prims.fst(444,5 PatAnnot.fst(39,10-39,12): (Error 19) Subtyping check failed; expected type Prims.squash Prims.l_False; got type Prims.unit; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also PatAnnot.fst(40,26-40,31)) >>] >> Got issues: [ -PatAnnot.fst(46,10-46,11): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(672,18-672,24)) +PatAnnot.fst(46,10-46,11): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(673,18-673,24)) >>] >> Got issues: [ -PatAnnot.fst(55,36-55,39): (Error 19) Type annotation on parameter incompatible with the expected type; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(672,18-672,24)) +PatAnnot.fst(55,36-55,39): (Error 19) Type annotation on parameter incompatible with the expected type; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(673,18-673,24)) >>] Verified module: PatAnnot All verification conditions discharged successfully diff --git a/tests/error-messages/Test.FunctionalExtensionality.fst.expected b/tests/error-messages/Test.FunctionalExtensionality.fst.expected index dda6dc4b428..3a69ad51cbe 100644 --- a/tests/error-messages/Test.FunctionalExtensionality.fst.expected +++ b/tests/error-messages/Test.FunctionalExtensionality.fst.expected @@ -5,7 +5,7 @@ Test.FunctionalExtensionality.fst(36,49-36,50): (Error 19) Subtyping check faile Test.FunctionalExtensionality.fst(80,2-80,8): (Error 19) assertion failed; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also Test.FunctionalExtensionality.fst(80,9-80,43)) >>] >> Got issues: [ -Test.FunctionalExtensionality.fst(92,36-92,47): (Error 19) Subtyping check failed; expected type _: Prims.int -> Prims.Tot Prims.int; got type Prims.nat ^-> Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(672,18-672,24)) +Test.FunctionalExtensionality.fst(92,36-92,47): (Error 19) Subtyping check failed; expected type _: Prims.int -> Prims.Tot Prims.int; got type Prims.nat ^-> Prims.int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(673,18-673,24)) >>] >> Got issues: [ Test.FunctionalExtensionality.fst(142,57-142,58): (Error 19) Subtyping check failed; expected type Prims.int ^-> Prims.int; got type Prims.int ^-> Prims.nat; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also FStar.FunctionalExtensionality.fsti(102,60-102,77)) diff --git a/tests/interactive/integration.push-pop.out.expected b/tests/interactive/integration.push-pop.out.expected index d55db898f0e..f313b9e9d1b 100644 --- a/tests/interactive/integration.push-pop.out.expected +++ b/tests/interactive/integration.push-pop.out.expected @@ -78,17 +78,17 @@ {"kind": "response", "query-id": "80", "response": [], "status": "success"} {"kind": "response", "query-id": "91", "response": [{"level": "error", "message": "Syntax error: Parsing.Parse_error", "number": 168, "ranges": [{"beg": [12, 0], "end": [12, 0], "fname": ""}]}], "status": "success"} {"kind": "response", "query-id": "98", "response": [], "status": "success"} -{"kind": "response", "query-id": "101", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; got type int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [672, 18], "end": [672, 24], "fname": "prims.fst"}]}], "status": "failure"} +{"kind": "response", "query-id": "101", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; got type int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [673, 18], "end": [673, 24], "fname": "prims.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "107", "response": [], "status": "success"} {"kind": "response", "query-id": "108", "response": [], "status": "success"} {"kind": "response", "query-id": "112", "response": null, "status": "success"} {"kind": "response", "query-id": "114", "response": [], "status": "success"} -{"kind": "response", "query-id": "116", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; got type int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [672, 18], "end": [672, 24], "fname": "prims.fst"}]}], "status": "failure"} +{"kind": "response", "query-id": "116", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; got type int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [673, 18], "end": [673, 24], "fname": "prims.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "118", "response": [], "status": "success"} {"kind": "response", "query-id": "119", "response": [], "status": "success"} {"kind": "response", "query-id": "122", "response": null, "status": "success"} {"kind": "response", "query-id": "124", "response": [], "status": "success"} -{"kind": "response", "query-id": "126", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; got type int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [672, 18], "end": [672, 24], "fname": "prims.fst"}]}], "status": "failure"} +{"kind": "response", "query-id": "126", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; got type int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [673, 18], "end": [673, 24], "fname": "prims.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "128", "response": [], "status": "success"} {"kind": "response", "query-id": "130", "response": [], "status": "success"} {"kind": "response", "query-id": "133", "response": [], "status": "success"} @@ -106,7 +106,7 @@ {"kind": "response", "query-id": "191", "response": null, "status": "success"} {"kind": "response", "query-id": "192", "response": null, "status": "success"} {"kind": "response", "query-id": "194", "response": [], "status": "success"} -{"kind": "response", "query-id": "198", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; got type int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [672, 18], "end": [672, 24], "fname": "prims.fst"}]}], "status": "failure"} +{"kind": "response", "query-id": "198", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; got type int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [673, 18], "end": [673, 24], "fname": "prims.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "200", "response": [], "status": "success"} {"kind": "response", "query-id": "204", "response": [], "status": "success"} {"kind": "response", "query-id": "205", "response": [{"level": "error", "message": "assertion failed; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel", "number": 19, "ranges": [{"beg": [13, 8], "end": [13, 14], "fname": ""}, {"beg": [13, 15], "end": [13, 23], "fname": ""}]}], "status": "failure"} From 9d1a04f6755b239b9dbc99fe6644b0227cf93d34 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 16 Feb 2022 22:50:04 +0000 Subject: [PATCH 6/9] revert Makefile change --- src/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Makefile b/src/Makefile index 3d8604e158b..e88174efc4d 100644 --- a/src/Makefile +++ b/src/Makefile @@ -146,7 +146,7 @@ utest: # The first tests have to be performed sequentially (but each one may use some parallelism) # Adding the F# build and F# tests also here # since in the uregressions target it may not be a good idea to override the fstar.exe binary? -utest-prelude: +utest-prelude: fsharp-build-and-test +$(MAKE) boot-ocaml #build the ocaml-snapshot +$(MAKE) clean_extracted #ensures that there is no leftover from previous extraction +$(MAKE) fstar-ocaml #extract the compiler again and build the result From 8191b3e5454de16f9c924eee58092a6f89ddf659 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 17 Feb 2022 11:24:43 -0800 Subject: [PATCH 7/9] c_and is pair; c_or is sum --- .../BinaryTreesEnumeration.fsti | 4 ++-- examples/misc/WorkingWithSquashedProofs.fst | 14 ++++++------ src/parser/FStar.Parser.Const.fs | 4 ++-- src/tests/FStar.Tests.Unif.fs | 2 +- .../FStar.TypeChecker.TcInductive.fs | 2 +- tests/bug-reports/Bug844.fst | 6 ++--- tests/error-messages/NegativeTests.False.fst | 2 +- .../NegativeTests.False.fst.expected | 8 +++---- ulib/FStar.Classical.Sugar.fst | 6 ++--- ulib/FStar.Classical.fst | 12 +++++----- ulib/FStar.IndefiniteDescription.fst | 6 ++--- ulib/FStar.LexicographicOrdering.fst | 6 ++--- ulib/FStar.SquashProperties.fst | 22 +++++++++---------- ulib/experimental/Steel.Effect.Common.fsti | 2 +- ulib/fs/prims.fs | 12 +++++----- ulib/ml/prims.ml | 22 +++++++++---------- ulib/prims.fst | 12 +++++----- 17 files changed, 71 insertions(+), 71 deletions(-) diff --git a/examples/data_structures/BinaryTreesEnumeration.fsti b/examples/data_structures/BinaryTreesEnumeration.fsti index 9809a0fdafd..ce5204b51ad 100644 --- a/examples/data_structures/BinaryTreesEnumeration.fsti +++ b/examples/data_structures/BinaryTreesEnumeration.fsti @@ -115,10 +115,10 @@ let rec memP_append_aux #a (x: a) (l: list a) : let pf : squash (x == h \/ List.memP x t) = () in p <-- FStar.Squash.join_squash pf ; match p with - | Prims.Inl x_eq_h -> + | Prims.Left x_eq_h -> let l12 = [], t in assert (l == (fst l12) @ (x :: snd l12)) //trigger - | Prims.Inr mem_x_t -> + | Prims.Right mem_x_t -> FStar.Classical.exists_elim goal (pure_as_squash (memP_append_aux x) t) diff --git a/examples/misc/WorkingWithSquashedProofs.fst b/examples/misc/WorkingWithSquashedProofs.fst index c104e8e6a87..0e3ea5e5dfd 100644 --- a/examples/misc/WorkingWithSquashedProofs.fst +++ b/examples/misc/WorkingWithSquashedProofs.fst @@ -83,13 +83,13 @@ let valid_baz (a:Type) (x:a) : Lemma (baz a x) = let s_fb : squash (foo a x \/ bar a x) = foo_or_bar x in FStar.Squash.bind_squash s_fb (fun (fb:(foo a x \/ bar a x)) -> - FStar.Squash.bind_squash fb (fun (c_fb:Prims.either (foo a x) (bar a x)) -> + FStar.Squash.bind_squash fb (fun (c_fb:Prims.sum (foo a x) (bar a x)) -> let s_baz : squash (baz a x) = match c_fb with - | Prims.Inl f -> + | Prims.Left f -> // let sf = FStar.Squash.return_squash f in foo_baz x - | Prims.Inr b -> + | Prims.Right b -> // let sg = FStar.Squash.return_squash b in bar_baz x in @@ -115,9 +115,9 @@ let valid_baz_alt (a:Type) (x:a) FStar.Squash.bind_squash fb (fun (c_fb:Prims.either (foo a x) (bar a x)) -> let s_baz : squash (baz a x) = match c_fb with - | Prims.Inl f -> + | Prims.Left f -> c_foo_baz x f - | Prims.Inr b -> + | Prims.Right b -> c_bar_baz x b in s_baz)) @@ -129,8 +129,8 @@ let elim_squash_or (#r:_) (#p #q:_) (f:squash (p \/ q)) (left: p -> GTot r) (rig = FStar.Squash.bind_squash #_ #r f (fun pq -> FStar.Squash.bind_squash pq (fun c -> match c with - | Prims.Inl x -> FStar.Squash.return_squash (left x) - | Prims.Inr x -> FStar.Squash.return_squash (right x))) + | Prims.Left x -> FStar.Squash.return_squash (left x) + | Prims.Right x -> FStar.Squash.return_squash (right x))) let valid_baz_alt_alt (a:Type) (x:a) : GTot (squash (baz a x)) diff --git a/src/parser/FStar.Parser.Const.fs b/src/parser/FStar.Parser.Const.fs index de8c7416069..47b9707bd37 100644 --- a/src/parser/FStar.Parser.Const.fs +++ b/src/parser/FStar.Parser.Const.fs @@ -106,8 +106,8 @@ let has_type_lid = pconst "has_type" (* Constructive variants *) let c_true_lid = pconst "c_True" let empty_type_lid = pconst "empty" -let c_and_lid = pconst "tuple2" -let c_or_lid = pconst "either" +let c_and_lid = pconst "pair" +let c_or_lid = pconst "sum" let dtuple2_lid = pconst "dtuple2" // for l_Exists (* Various equality predicates *) diff --git a/src/tests/FStar.Tests.Unif.fs b/src/tests/FStar.Tests.Unif.fs index d47fa0525bb..40814411dfa 100644 --- a/src/tests/FStar.Tests.Unif.fs +++ b/src/tests/FStar.Tests.Unif.fs @@ -136,7 +136,7 @@ let run_all () = //imitation: unifies u to a constant FStar.Main.process_args () |> ignore; //set options let tm, us = inst 1 (tc "fun u x -> u x") in - let sol = tc "fun x -> Prims.tuple2 x x" in + let sol = tc "fun x -> Prims.pair x x" in unify_check 9 tm sol Trivial diff --git a/src/typechecker/FStar.TypeChecker.TcInductive.fs b/src/typechecker/FStar.TypeChecker.TcInductive.fs index 7826ab3670a..06ce4afa05a 100644 --- a/src/typechecker/FStar.TypeChecker.TcInductive.fs +++ b/src/typechecker/FStar.TypeChecker.TcInductive.fs @@ -780,7 +780,7 @@ let check_inductive_well_typedness (env:env_t) (ses:list) (quals:list) (* Attributes of the envelopping bundle *) diff --git a/tests/bug-reports/Bug844.fst b/tests/bug-reports/Bug844.fst index bb694ab63a1..9021f1b421d 100644 --- a/tests/bug-reports/Bug844.fst +++ b/tests/bug-reports/Bug844.fst @@ -37,9 +37,9 @@ noeq type retract_cond 'a 'b : Type = val l1: (a:Type0) -> (b:Type0) -> GTot (squash (retract_cond (pow a) (pow b))) let l1 (a:Type) (b:Type) = bind_squash (excluded_middle_squash (retract (pow a) (pow b))) - (fun (x:Prims.either (retract (pow a) (pow b)) (~ (retract (pow a) (pow b)))) -> + (fun (x:Prims.sum (retract (pow a) (pow b)) (~ (retract (pow a) (pow b)))) -> match x with - | Prims.Inl (MkR f0 g0 e) -> + | Prims.Left (MkR f0 g0 e) -> return_squash (MkC f0 g0 (fun _ -> e) (* <- this lambda causes the problem *)) - | Prims.Inr nr -> + | Prims.Right nr -> magic()) diff --git a/tests/error-messages/NegativeTests.False.fst b/tests/error-messages/NegativeTests.False.fst index 730590eac2f..f991e062f18 100644 --- a/tests/error-messages/NegativeTests.False.fst +++ b/tests/error-messages/NegativeTests.False.fst @@ -27,4 +27,4 @@ val f : p1:(True \/ True) -> p2:(True \/ True) -> Lemma (p1 = p2) let f p1 p2 = () val absurd : unit -> Lemma False [@@expect_failure] // this raises 2 errors on 1-phase, and 4 on 2-phases -let absurd () = f (Prims.Inl #_ #True T) (Prims.Inr #True #_ T) //adding implicits to get 2 typing errors +let absurd () = f (Prims.Left #_ #True T) (Prims.Right #True #_ T) //adding implicits to get 2 typing errors diff --git a/tests/error-messages/NegativeTests.False.fst.expected b/tests/error-messages/NegativeTests.False.fst.expected index 1e978a2a949..47d16b90207 100644 --- a/tests/error-messages/NegativeTests.False.fst.expected +++ b/tests/error-messages/NegativeTests.False.fst.expected @@ -2,10 +2,10 @@ NegativeTests.False.fst(23,13-23,33): (Error 19) assertion failed; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(444,55-444,67)) >>] >> Got issues: [ -NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Inl (Prims.T)" has type "Prims.either (*?u1*) _ Prims.l_True" -NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Inl (Prims.T)" has type "Prims.either Prims.c_True Prims.l_True" -NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Inr (Prims.T)" has type "Prims.either Prims.l_True (*?u6*) _" -NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Inr (Prims.T)" has type "Prims.either Prims.l_True Prims.c_True" +NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.sum (*?u1*) _ Prims.l_True" +NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.sum Prims.c_True Prims.l_True" +NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.sum Prims.l_True (*?u6*) _" +NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.sum Prims.l_True Prims.c_True" >>] NegativeTests.False.fst(21,4-21,7): (Warning 240) Admitting NegativeTests.False.bar without a definition NegativeTests.False.fst(28,4-28,10): (Warning 240) Admitting NegativeTests.False.absurd without a definition diff --git a/ulib/FStar.Classical.Sugar.fst b/ulib/FStar.Classical.Sugar.fst index 67da905b954..fab73510859 100644 --- a/ulib/FStar.Classical.Sugar.fst +++ b/ulib/FStar.Classical.Sugar.fst @@ -45,9 +45,9 @@ let or_elim_simple bind_squash x (fun p_or_q -> bind_squash p_or_q (fun p_cor_q -> match p_cor_q with - | Prims.Inl p -> + | Prims.Left p -> f (return_squash p) - | Prims.Inr q -> + | Prims.Right q -> g (return_squash q))) let or_elim @@ -73,7 +73,7 @@ let and_elim (p:Type) : Tot (squash r) = let open FStar.Squash in bind_squash x (fun p_and_q -> - bind_squash p_and_q (fun (Prims.Mktuple2 p q) -> + bind_squash p_and_q (fun (Prims.Pair p q) -> f (return_squash p) (return_squash q))) let forall_intro diff --git a/ulib/FStar.Classical.fst b/ulib/FStar.Classical.fst index abfb0797026..9760280c128 100644 --- a/ulib/FStar.Classical.fst +++ b/ulib/FStar.Classical.fst @@ -51,13 +51,13 @@ let move_requires #a #p #q f x = give_proof (bind_squash (get_proof (l_or (p x) (~(p x)))) (fun (b: l_or (p x) (~(p x))) -> bind_squash b - (fun (b': Prims.either (p x) (~(p x))) -> + (fun (b': Prims.sum (p x) (~(p x))) -> match b' with - | Prims.Inl hp -> + | Prims.Left hp -> give_witness hp; f x; get_proof (p x ==> q x) - | Prims.Inr hnp -> give_witness hnp))) + | Prims.Right hnp -> give_witness hnp))) let move_requires_2 #a #b #p #q f x y = move_requires (f x) y @@ -133,13 +133,13 @@ let ghost_lemma #a #p #q f = give_proof (bind_squash (get_proof (l_or (p x) (~(p x)))) (fun (b: l_or (p x) (~(p x))) -> bind_squash b - (fun (b': Prims.either (p x) (~(p x))) -> + (fun (b': Prims.sum (p x) (~(p x))) -> match b' with - | Prims.Inl hp -> + | Prims.Left hp -> give_witness hp; f x; get_proof (p x ==> q x ()) - | Prims.Inr hnp -> give_witness hnp)))) + | Prims.Right hnp -> give_witness hnp)))) in forall_intro lem diff --git a/ulib/FStar.IndefiniteDescription.fst b/ulib/FStar.IndefiniteDescription.fst index 6e5a4be4e0f..c369ff0f03d 100644 --- a/ulib/FStar.IndefiniteDescription.fst +++ b/ulib/FStar.IndefiniteDescription.fst @@ -68,13 +68,13 @@ let strong_excluded_middle (p: Type0) : GTot (b: bool{b = true <==> p}) = give_proof (bind_squash (get_proof (l_or p (~p))) (fun (b: l_or p (~p)) -> bind_squash b - (fun (b': Prims.either p (~p)) -> + (fun (b': Prims.sum p (~p)) -> match b' with - | Prims.Inl hp -> + | Prims.Left hp -> give_witness hp; exists_intro (fun b -> b = true <==> p) true; get_proof (exists b. b = true <==> p) - | Prims.Inr hnp -> + | Prims.Right hnp -> give_witness hnp; exists_intro (fun b -> b = true <==> p) false; get_proof (exists b. b = true <==> p)))) diff --git a/ulib/FStar.LexicographicOrdering.fst b/ulib/FStar.LexicographicOrdering.fst index 0ecd634b06f..40303f79df7 100644 --- a/ulib/FStar.LexicographicOrdering.fst +++ b/ulib/FStar.LexicographicOrdering.fst @@ -105,14 +105,14 @@ let lex_to_lex_t #a #b r_a r_b t1 t2 p = : squash (lex_t r_a r_b t1 t2) = bind_squash p (fun p -> match p with - | Prims.Mktuple2 (_:dfst t1 == dfst t2) p2 -> + | Prims.Pair (_:dfst t1 == dfst t2) p2 -> bind_squash p2 (fun p2 -> return_squash (Right_lex #a #b #r_a #r_b (dfst t1) (dsnd t1) (dsnd t2) p2))) in bind_squash p (fun p -> match p with - | Prims.Inl p1 -> left p1 - | Prims.Inr p2 -> right p2) + | Prims.Left p1 -> left p1 + | Prims.Right p2 -> right p2) let lex_t_non_dep_wf #a #b #r_a #r_b wf_a wf_b = diff --git a/ulib/FStar.SquashProperties.fst b/ulib/FStar.SquashProperties.fst index 1f0a48fe0c5..d8b9e6664f6 100644 --- a/ulib/FStar.SquashProperties.fst +++ b/ulib/FStar.SquashProperties.fst @@ -49,12 +49,12 @@ let forall_intro #a #p f = (* The whole point of defining squash is to soundly allow define excluded_middle; here this follows from get_proof and give_proof *) -val bool_of_or : #p:Type -> #q:Type -> Prims.either p q -> +val bool_of_or : #p:Type -> #q:Type -> Prims.sum p q -> Tot (b:bool{(b ==> p) /\ (not(b) ==> q)}) let bool_of_or #p #q t = match t with - | Prims.Inl _ -> true - | Prims.Inr _ -> false + | Prims.Left _ -> true + | Prims.Right _ -> false val excluded_middle : p:Type -> GTot (squash (b:bool{b <==> p})) let excluded_middle (p:Type) = map_squash (join_squash (get_proof (p \/ (~p)))) bool_of_or @@ -64,9 +64,9 @@ val excluded_middle_squash : p:Type0 -> GTot (p \/ ~p) let excluded_middle_squash p = bind_squash (excluded_middle p) (fun x -> if x then - map_squash (get_proof p) (Prims.Inl #p) + map_squash (get_proof p) (Prims.Left #p) else - return_squash (Prims.Inr #_ #(~p) (return_squash (fun (h:p) -> + return_squash (Prims.Right #_ #(~p) (return_squash (fun (h:p) -> give_proof (return_squash h); false_elim #False ())))) @@ -76,10 +76,10 @@ let excluded_middle_squash p = val ifProp: #p:Type0 -> b:Type0 -> e1:squash p -> e2:squash p -> GTot (squash p) let ifProp #p b e1 e2 = bind_squash (excluded_middle_squash b) - (fun (x:Prims.either b (~ b)) -> + (fun (x:Prims.sum b (~ b)) -> match x with - | Prims.Inl _ -> e1 - | Prims.Inr _ -> e2) + | Prims.Left _ -> e1 + | Prims.Right _ -> e2) (* The powerset operator *) type pow (p:Type) = p -> GTot bool @@ -107,11 +107,11 @@ let false_elim (#a:Type) (f:False) : Tot a val l1: (a:Type0) -> (b:Type0) -> GTot (squash (retract_cond (pow a) (pow b))) let l1 (a:Type) (b:Type) = bind_squash (excluded_middle_squash (retract (pow a) (pow b))) - (fun (x:Prims.either (retract (pow a) (pow b)) (~ (retract (pow a) (pow b)))) -> + (fun (x:Prims.sum (retract (pow a) (pow b)) (~ (retract (pow a) (pow b)))) -> match x with - | Prims.Inl (MkR f0 g0 e) -> + | Prims.Left (MkR f0 g0 e) -> return_squash (MkC f0 g0 (fun _ -> e)) - | Prims.Inr nr -> + | Prims.Right nr -> let f0 (x:pow a) (y:b) = false in let g0 (x:pow b) (y:a) = false in map_squash nr (fun (f:(retract (pow a) (pow b) -> GTot False)) -> diff --git a/ulib/experimental/Steel.Effect.Common.fsti b/ulib/experimental/Steel.Effect.Common.fsti index b28d060633d..69759babdc3 100644 --- a/ulib/experimental/Steel.Effect.Common.fsti +++ b/ulib/experimental/Steel.Effect.Common.fsti @@ -2350,7 +2350,7 @@ let init_resolve_tac () : Tac unit = (* AF: There probably is a simpler way to get from p to squash p in a tactic, so that we can use apply_lemma *) let squash_and p (x:squash (p /\ True)) : (p /\ True) = - let x : squash (p `Prims.tuple2` True) = FStar.Squash.join_squash x in + let x : squash (p `Prims.pair` True) = FStar.Squash.join_squash x in x /// Calling into the framing tactic to ensure that the vprop whose selector we are trying to access is in the context diff --git a/ulib/fs/prims.fs b/ulib/fs/prims.fs index a05d0f8a964..4e9eef163a9 100644 --- a/ulib/fs/prims.fs +++ b/ulib/fs/prims.fs @@ -59,15 +59,15 @@ type 'd b2t = B2t of unit type 'a squash = Squash of unit -type (' p, ' q) either = - | Inl of ' p - | Inr of ' q +type (' p, ' q) sum = + | Left of ' p + | Right of ' q -type (' p, ' q) l_or = ('p, 'q) either squash +type (' p, ' q) l_or = ('p, 'q) sum squash -let uu___is_Inl = function Inl _ -> true | Inr _ -> false +let uu___is_Left = function Left _ -> true | Right _ -> false -let uu___is_Inr = function Inl _ -> false | Inr _ -> true +let uu___is_Right = function Left _ -> false | Right _ -> true type (' p, ' q) tuple2 = | Mktuple2 of ' p * ' q diff --git a/ulib/ml/prims.ml b/ulib/ml/prims.ml index 3e6f6a3cea3..d77838fc4c6 100644 --- a/ulib/ml/prims.ml +++ b/ulib/ml/prims.ml @@ -47,21 +47,21 @@ let __proj__Mktuple2__item___1 : 'Ap 'Aq . ('Ap,'Aq) tuple2 -> 'Ap = let __proj__Mktuple2__item___2 : 'Ap 'Aq . ('Ap,'Aq) tuple2 -> 'Aq = fun projectee -> match projectee with | Mktuple2 (_0,_1) -> _1 type ('Ap,'Aq) l_and = unit -type ('Ap,'Aq) either = - | Inl of 'Ap - | Inr of 'Aq -let uu___is_Inl : 'Ap 'Aq . ('Ap,'Aq) either -> bool = +type ('Ap,'Aq) sum = + | Left of 'Ap + | Right of 'Aq +let uu___is_Left : 'Ap 'Aq . ('Ap,'Aq) either -> bool = fun projectee -> - match projectee with | Inl _0 -> true | uu____344 -> false + match projectee with | Left _0 -> true | uu____344 -> false -let __proj__Inl__item___0 : 'Ap 'Aq . ('Ap,'Aq) either -> 'Ap = - fun projectee -> match projectee with | Inl _0 -> _0 -let uu___is_Inr : 'Ap 'Aq . ('Ap,'Aq) either -> bool = +let __proj__Left__item___0 : 'Ap 'Aq . ('Ap,'Aq) either -> 'Ap = + fun projectee -> match projectee with | Left _0 -> _0 +let uu___is_Right : 'Ap 'Aq . ('Ap,'Aq) either -> bool = fun projectee -> - match projectee with | Inr _0 -> true | uu____404 -> false + match projectee with | Right _0 -> true | uu____404 -> false -let __proj__Inr__item___0 : 'Ap 'Aq . ('Ap,'Aq) either -> 'Aq = - fun projectee -> match projectee with | Inr _0 -> _0 +let __proj__Right__item___0 : 'Ap 'Aq . ('Ap,'Aq) either -> 'Aq = + fun projectee -> match projectee with | Right _0 -> _0 type ('Ap,'Aq) l_or = unit type ('Ap,'Aq) l_imp = unit type ('Ap,'Aq) l_iff = unit diff --git a/ulib/prims.fst b/ulib/prims.fst index 92252f2aa45..e71f221c9f1 100644 --- a/ulib/prims.fst +++ b/ulib/prims.fst @@ -159,22 +159,22 @@ type eq2 (#a: Type) (x: a) (y: a) : logical = squash (equals x y) type b2t (b: bool) : logical = (b == true) (** constructive conjunction *) -type tuple2 (p: Type) (q: Type) = | Mktuple2 : _1:p -> _2:q -> tuple2 p q +type pair (p: Type) (q: Type) = | Pair : _1:p -> _2:q -> pair p q (** squashed conjunction, specialized to [Type0], written with an infix binary [/\] *) [@@ "tac_opaque"; smt_theory_symbol] -type l_and (p: logical) (q: logical) : logical = squash (tuple2 p q) +type l_and (p: logical) (q: logical) : logical = squash (pair p q) (** constructive disjunction *) -type either (p: Type) (q: Type) = - | Inl : v:p -> either p q - | Inr : v:q -> either p q +type sum (p: Type) (q: Type) = + | Left : v:p -> sum p q + | Right : v:q -> sum p q (** squashed disjunction, specialized to [Type0], written with an infix binary [\/] *) [@@ "tac_opaque"; smt_theory_symbol] -type l_or (p: logical) (q: logical) : logical = squash (either p q) +type l_or (p: logical) (q: logical) : logical = squash (sum p q) (** squashed (non-dependent) implication, specialized to [Type0], written with an infix binary [==>]. Note, [==>] binds weaker than From a5cb4ee0d7e0a82ef85712f967fbdf95cb5354a5 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 17 Feb 2022 20:06:59 +0000 Subject: [PATCH 8/9] c_True is trivial; c_and is pair; c_or is sum --- examples/native_tactics/Tutorial.fst | 2 +- ...ropositionalExtensionalityInconsistent.fst | 4 +-- examples/tactics/Tutorial.fst | 2 +- src/ocaml-output/FStar_Parser_Const.ml | 6 ++--- src/ocaml-output/FStar_Tests_Unif.ml | 2 +- .../FStar_TypeChecker_TcInductive.ml | 2 +- src/parser/FStar.Parser.Const.fs | 2 +- .../FStar.TypeChecker.TcInductive.fs | 2 +- .../NegativeTests.False.fst.expected | 4 +-- tests/micro-benchmarks/NormVsSMT.fst | 4 +-- ulib/FStar.IndefiniteDescription.fst | 4 +-- ulib/fs/prims.fs | 16 ++++++------ ulib/ml/prims.ml | 26 +++++++++---------- ulib/prims.fst | 12 ++++----- 14 files changed, 44 insertions(+), 44 deletions(-) diff --git a/examples/native_tactics/Tutorial.fst b/examples/native_tactics/Tutorial.fst index 89ea5f9b74b..07f905d8edd 100644 --- a/examples/native_tactics/Tutorial.fst +++ b/examples/native_tactics/Tutorial.fst @@ -102,7 +102,7 @@ and you can simply think of the type `squash phi` as the type of irrelevant proofs of `phi`. We call goals that are squashed ``irrelevant''. > For experts: You might notice that `True` is already a squash (of -> `c_True`), so this seems useless. In this case it is, but we squash +> `trivial`), so this seems useless. In this case it is, but we squash > nevertheless for consistency since this might be not so. A tactic is not required to completely prove an assertion, and can leave diff --git a/examples/paradoxes/PropositionalExtensionalityInconsistent.fst b/examples/paradoxes/PropositionalExtensionalityInconsistent.fst index 040f54009e0..5e34fa98669 100644 --- a/examples/paradoxes/PropositionalExtensionalityInconsistent.fst +++ b/examples/paradoxes/PropositionalExtensionalityInconsistent.fst @@ -61,7 +61,7 @@ let predExt_Type = (ensures (p1 == p2)) let predExt_Type_inconsistent (ax:predExt_Type) : Lemma False - = let p1 : predicate int = fun n -> c_True in + = let p1 : predicate int = fun n -> trivial in let p2 : predicate int = fun n -> unit in ax int p1 p2 @@ -78,6 +78,6 @@ let predExt_ss = (ensures (p1 == p2)) let predExt_ss_inconsistent (ax:predExt_ss) : Lemma False - = let p1 : predicate_ss int = fun n -> c_True in + = let p1 : predicate_ss int = fun n -> trivial in let p2 : predicate_ss int = fun n -> unit in ax int p1 p2 diff --git a/examples/tactics/Tutorial.fst b/examples/tactics/Tutorial.fst index 307e43ad743..d2bc7567a22 100644 --- a/examples/tactics/Tutorial.fst +++ b/examples/tactics/Tutorial.fst @@ -93,7 +93,7 @@ let ex2 () = /// .. note:: /// /// For experts: You might notice that ``True`` is already a squash (of -/// ``c_True``), so this seems useless. In this case it is, but we squash +/// ``trivial``), so this seems useless. In this case it is, but we squash /// nevertheless for consistency since this might be not so. /// A tactic is not required to completely prove an assertion, and can leave diff --git a/src/ocaml-output/FStar_Parser_Const.ml b/src/ocaml-output/FStar_Parser_Const.ml index 853a5c075ab..f0ab3fd287c 100644 --- a/src/ocaml-output/FStar_Parser_Const.ml +++ b/src/ocaml-output/FStar_Parser_Const.ml @@ -67,10 +67,10 @@ let (b2t_lid : FStar_Ident.lident) = pconst "b2t" let (admit_lid : FStar_Ident.lident) = pconst "admit" let (magic_lid : FStar_Ident.lident) = pconst "magic" let (has_type_lid : FStar_Ident.lident) = pconst "has_type" -let (c_true_lid : FStar_Ident.lident) = pconst "c_True" +let (c_true_lid : FStar_Ident.lident) = pconst "trivial" let (empty_type_lid : FStar_Ident.lident) = pconst "empty" -let (c_and_lid : FStar_Ident.lident) = pconst "tuple2" -let (c_or_lid : FStar_Ident.lident) = pconst "either" +let (c_and_lid : FStar_Ident.lident) = pconst "pair" +let (c_or_lid : FStar_Ident.lident) = pconst "sum" let (dtuple2_lid : FStar_Ident.lident) = pconst "dtuple2" let (eq2_lid : FStar_Ident.lident) = pconst "eq2" let (eq3_lid : FStar_Ident.lident) = pconst "op_Equals_Equals_Equals" diff --git a/src/ocaml-output/FStar_Tests_Unif.ml b/src/ocaml-output/FStar_Tests_Unif.ml index 4ef0966e641..832d36c1b1b 100644 --- a/src/ocaml-output/FStar_Tests_Unif.ml +++ b/src/ocaml-output/FStar_Tests_Unif.ml @@ -235,7 +235,7 @@ let (run_all : unit -> Prims.bool) = inst Prims.int_one uu___14 in match uu___13 with | (tm, us) -> - let sol = FStar_Tests_Pars.tc "fun x -> Prims.tuple2 x x" in + let sol = FStar_Tests_Pars.tc "fun x -> Prims.pair x x" in (unify_check (Prims.of_int (9)) tm sol FStar_TypeChecker_Common.Trivial (fun uu___15 -> diff --git a/src/ocaml-output/FStar_TypeChecker_TcInductive.ml b/src/ocaml-output/FStar_TypeChecker_TcInductive.ml index c03606fe4e1..8e2cd4d1e17 100644 --- a/src/ocaml-output/FStar_TypeChecker_TcInductive.ml +++ b/src/ocaml-output/FStar_TypeChecker_TcInductive.ml @@ -1884,7 +1884,7 @@ let (check_inductive_well_typedness : | uu___6 -> ())); (sig_bndle, tcs1, datas2)))))) let (early_prims_inductives : Prims.string Prims.list) = - ["empty"; "c_True"; "equals"; "tuple2"; "either"] + ["empty"; "trivial"; "equals"; "pair"; "sum"] let (mk_discriminator_and_indexed_projectors : FStar_Syntax_Syntax.qualifier Prims.list -> FStar_Syntax_Syntax.attribute Prims.list -> diff --git a/src/parser/FStar.Parser.Const.fs b/src/parser/FStar.Parser.Const.fs index 47b9707bd37..11d8528ce85 100644 --- a/src/parser/FStar.Parser.Const.fs +++ b/src/parser/FStar.Parser.Const.fs @@ -104,7 +104,7 @@ let magic_lid = pconst "magic" let has_type_lid = pconst "has_type" (* Constructive variants *) -let c_true_lid = pconst "c_True" +let c_true_lid = pconst "trivial" let empty_type_lid = pconst "empty" let c_and_lid = pconst "pair" let c_or_lid = pconst "sum" diff --git a/src/typechecker/FStar.TypeChecker.TcInductive.fs b/src/typechecker/FStar.TypeChecker.TcInductive.fs index 06ce4afa05a..fe742b0a1c0 100644 --- a/src/typechecker/FStar.TypeChecker.TcInductive.fs +++ b/src/typechecker/FStar.TypeChecker.TcInductive.fs @@ -780,7 +780,7 @@ let check_inductive_well_typedness (env:env_t) (ses:list) (quals:list) (* Attributes of the envelopping bundle *) diff --git a/tests/error-messages/NegativeTests.False.fst.expected b/tests/error-messages/NegativeTests.False.fst.expected index 47d16b90207..a630a44098d 100644 --- a/tests/error-messages/NegativeTests.False.fst.expected +++ b/tests/error-messages/NegativeTests.False.fst.expected @@ -3,9 +3,9 @@ NegativeTests.False.fst(23,13-23,33): (Error 19) assertion failed; The SMT solve >>] >> Got issues: [ NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.sum (*?u1*) _ Prims.l_True" -NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.sum Prims.c_True Prims.l_True" +NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.sum Prims.trivial Prims.l_True" NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.sum Prims.l_True (*?u6*) _" -NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.sum Prims.l_True Prims.c_True" +NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.sum Prims.l_True Prims.trivial" >>] NegativeTests.False.fst(21,4-21,7): (Warning 240) Admitting NegativeTests.False.bar without a definition NegativeTests.False.fst(28,4-28,10): (Warning 240) Admitting NegativeTests.False.absurd without a definition diff --git a/tests/micro-benchmarks/NormVsSMT.fst b/tests/micro-benchmarks/NormVsSMT.fst index b767d0baf77..988ad7a922f 100644 --- a/tests/micro-benchmarks/NormVsSMT.fst +++ b/tests/micro-benchmarks/NormVsSMT.fst @@ -19,8 +19,8 @@ let _ = assert_norm (True /\ True) let _ = assert_norm (True \/ True) (* These fail, and probably shouldn't, but it's not too worrysome *) -(* let _ = assert (c_and True True) *) -(* let _ = assert (c_and c_True c_True) *) +(* let _ = assert (pair True True) *) +(* let _ = assert (pair trivial trivial) *) (* This fails after removing t_valid, c.f. 5ac0bd96d *) (* val l1 : (a : Type) -> Lemma (a ==> squash a) *) diff --git a/ulib/FStar.IndefiniteDescription.fst b/ulib/FStar.IndefiniteDescription.fst index c369ff0f03d..1998b346347 100644 --- a/ulib/FStar.IndefiniteDescription.fst +++ b/ulib/FStar.IndefiniteDescription.fst @@ -102,7 +102,7 @@ let stronger_markovs_principle_prop (p: (nat -> GTot prop)) (** A proof for squash p can be eliminated to get p in the Ghost effect *) let elim_squash (#p:Type u#a) (s:squash p) : GTot p = - let uu : squash (x:p & squash c_True) = + let uu : squash (x:p & squash trivial) = bind_squash s (fun x -> return_squash (| x, return_squash T |)) in give_proof (return_squash uu); - indefinite_description_ghost p (fun _ -> squash c_True) + indefinite_description_ghost p (fun _ -> squash trivial) diff --git a/ulib/fs/prims.fs b/ulib/fs/prims.fs index 4e9eef163a9..92e5dbb34da 100644 --- a/ulib/fs/prims.fs +++ b/ulib/fs/prims.fs @@ -69,25 +69,25 @@ let uu___is_Left = function Left _ -> true | Right _ -> false let uu___is_Right = function Left _ -> false | Right _ -> true -type (' p, ' q) tuple2 = -| Mktuple2 of ' p * ' q +type (' p, ' q) pair = +| Pair of ' p * ' q -type (' p, ' q) l_and = ('p, 'q) tuple2 squash +type (' p, ' q) l_and = ('p, 'q) pair squash -let uu___is_Mktuple2 _ = true +let uu___is_Pair _ = true -type c_True = +type trivial = | T -type l_True = c_True squash +type l_True = trivial squash let uu___is_T _ = true -type c_False = unit +type empty = unit (*This is how Coq extracts Inductive void := . Our extraction needs to be fixed to recognize when there are no constructors and generate this type abbreviation*) -type l_False = c_False squash +type l_False = empty squash type (' p, ' q) l_imp = ('p -> 'q) squash diff --git a/ulib/ml/prims.ml b/ulib/ml/prims.ml index d77838fc4c6..d8348a1eafd 100644 --- a/ulib/ml/prims.ml +++ b/ulib/ml/prims.ml @@ -23,9 +23,9 @@ type bool = bool' type empty = unit (*This is how Coq extracts Inductive void := . Our extraction needs to be fixed to recognize when there are no constructors and generate this type abbreviation*) -type c_True = +type trivial = | T -let (uu___is_T : c_True -> bool) = fun projectee -> true +let (uu___is_T : trivial -> bool) = fun projectee -> true type nonrec unit = unit type 'Ap squash = unit type 'Ap auto_squash = unit @@ -38,29 +38,29 @@ let uu___is_Refl : 'Aa . 'Aa -> 'Aa -> ('Aa,unit,unit) equals -> bool = type ('Aa,'Ax,'Ay) eq2 = unit type ('Aa,'Ab,'Ax,'Ay) op_Equals_Equals_Equals = unit type 'Ab b2t = unit -type ('Ap,'Aq) tuple2 = - | Mktuple2 of 'Ap * 'Aq -let uu___is_Mktuple2 : 'Ap 'Aq . ('Ap,'Aq) tuple2 -> bool = +type ('Ap,'Aq) pair = + | Pair of 'Ap * 'Aq +let uu___is_Pair : 'Ap 'Aq . ('Ap,'Aq) pair -> bool = fun projectee -> true -let __proj__Mktuple2__item___1 : 'Ap 'Aq . ('Ap,'Aq) tuple2 -> 'Ap = - fun projectee -> match projectee with | Mktuple2 (_0,_1) -> _0 -let __proj__Mktuple2__item___2 : 'Ap 'Aq . ('Ap,'Aq) tuple2 -> 'Aq = - fun projectee -> match projectee with | Mktuple2 (_0,_1) -> _1 +let __proj__Pair__item___1 : 'Ap 'Aq . ('Ap,'Aq) pair -> 'Ap = + fun projectee -> match projectee with | Pair (_0,_1) -> _0 +let __proj__Pair__item___2 : 'Ap 'Aq . ('Ap,'Aq) pair -> 'Aq = + fun projectee -> match projectee with | Pair (_0,_1) -> _1 type ('Ap,'Aq) l_and = unit type ('Ap,'Aq) sum = | Left of 'Ap | Right of 'Aq -let uu___is_Left : 'Ap 'Aq . ('Ap,'Aq) either -> bool = +let uu___is_Left : 'Ap 'Aq . ('Ap,'Aq) sum -> bool = fun projectee -> match projectee with | Left _0 -> true | uu____344 -> false -let __proj__Left__item___0 : 'Ap 'Aq . ('Ap,'Aq) either -> 'Ap = +let __proj__Left__item___0 : 'Ap 'Aq . ('Ap,'Aq) sum -> 'Ap = fun projectee -> match projectee with | Left _0 -> _0 -let uu___is_Right : 'Ap 'Aq . ('Ap,'Aq) either -> bool = +let uu___is_Right : 'Ap 'Aq . ('Ap,'Aq) sum -> bool = fun projectee -> match projectee with | Right _0 -> true | uu____404 -> false -let __proj__Right__item___0 : 'Ap 'Aq . ('Ap,'Aq) either -> 'Aq = +let __proj__Right__item___0 : 'Ap 'Aq . ('Ap,'Aq) sum -> 'Aq = fun projectee -> match projectee with | Right _0 -> _0 type ('Ap,'Aq) l_or = unit type ('Ap,'Aq) l_imp = unit diff --git a/ulib/prims.fst b/ulib/prims.fst index e71f221c9f1..f53196b403c 100644 --- a/ulib/prims.fst +++ b/ulib/prims.fst @@ -64,10 +64,10 @@ type bool : eqtype [False], see below. *) type empty = -(** [c_True] is the singleton inductive type---it is trivially - inhabited. Like [empty], [c_True] is seldom used. We instead use +(** [trivial] is the singleton inductive type---it is trivially + inhabited. Like [empty], [trivial] is seldom used. We instead use its "squashed" variants, [True] *) -type c_True = | T +type trivial = | T (** [unit]: another singleton type, with its only inhabitant written [()] we assume it is primitive, for convenient interop with other languages *) @@ -127,13 +127,13 @@ val smt_theory_symbol:attribute (** [l_True] has a special bit of syntactic sugar. It is written just as "True" and rendered in the ide as [True]. It is a squashed version - of constructive truth, [c_True]. *) + of constructive truth, [trivial]. *) [@@ "tac_opaque"; smt_theory_symbol] -let l_True:logical = squash c_True +let l_True:logical = squash trivial (** [l_False] has a special bit of syntactic sugar. It is written just as "False" and rendered in the ide as [Falsee]. It is a squashed version - of constructive truth, [c_True]. *) + of constructive falsehood, the empty type. *) [@@ "tac_opaque"; smt_theory_symbol] let l_False:logical = squash empty From 1edc5d0ae120e64a4588c23beafd04f39889bd20 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 17 Feb 2022 21:25:16 +0000 Subject: [PATCH 9/9] remove a couple of uses of old names --- examples/hello/TestSeq/TestSeq.fst.hints | 4 ++-- examples/misc/WorkingWithSquashedProofs.fst | 2 +- tests/error-messages/NegativeTests.False.fst.expected | 8 ++++---- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/examples/hello/TestSeq/TestSeq.fst.hints b/examples/hello/TestSeq/TestSeq.fst.hints index 87d6d210052..f3d3823b4de 100755 --- a/examples/hello/TestSeq/TestSeq.fst.hints +++ b/examples/hello/TestSeq/TestSeq.fst.hints @@ -23,7 +23,7 @@ "typing_FStar.Seq.Base.length", "unit_typing" ], 0, - "601ee9bf5aa72f07eff6aff22259563b" + "ec536a8e37d4ba8494e2ac0c633975d7" ], [ "TestSeq.main", @@ -47,7 +47,7 @@ "typing_Tm_abs_f8b7175ad4f28c0bc3c11371abe1d18d" ], 0, - "4c43b60034e8b75a02622e388be51622" + "be769d4a10a07b4c0591a4b7284c9419" ] ] ] \ No newline at end of file diff --git a/examples/misc/WorkingWithSquashedProofs.fst b/examples/misc/WorkingWithSquashedProofs.fst index 0e3ea5e5dfd..aeaaa2faf60 100644 --- a/examples/misc/WorkingWithSquashedProofs.fst +++ b/examples/misc/WorkingWithSquashedProofs.fst @@ -112,7 +112,7 @@ let valid_baz_alt (a:Type) (x:a) : Lemma (baz a x) = let s_fb : squash (foo a x \/ bar a x) = foo_or_bar x in FStar.Squash.bind_squash s_fb (fun (fb:(foo a x \/ bar a x)) -> - FStar.Squash.bind_squash fb (fun (c_fb:Prims.either (foo a x) (bar a x)) -> + FStar.Squash.bind_squash fb (fun (c_fb:Prims.sum (foo a x) (bar a x)) -> let s_baz : squash (baz a x) = match c_fb with | Prims.Left f -> diff --git a/tests/error-messages/NegativeTests.False.fst.expected b/tests/error-messages/NegativeTests.False.fst.expected index a630a44098d..85acaefe5d2 100644 --- a/tests/error-messages/NegativeTests.False.fst.expected +++ b/tests/error-messages/NegativeTests.False.fst.expected @@ -2,10 +2,10 @@ NegativeTests.False.fst(23,13-23,33): (Error 19) assertion failed; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(444,55-444,67)) >>] >> Got issues: [ -NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.sum (*?u1*) _ Prims.l_True" -NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.sum Prims.trivial Prims.l_True" -NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.sum Prims.l_True (*?u6*) _" -NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.sum Prims.l_True Prims.trivial" +NegativeTests.False.fst(30,18-30,41): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.sum (*?u1*) _ Prims.l_True" +NegativeTests.False.fst(30,18-30,41): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.sum Prims.trivial Prims.l_True" +NegativeTests.False.fst(30,42-30,66): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.sum Prims.l_True (*?u6*) _" +NegativeTests.False.fst(30,42-30,66): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.sum Prims.l_True Prims.trivial" >>] NegativeTests.False.fst(21,4-21,7): (Warning 240) Admitting NegativeTests.False.bar without a definition NegativeTests.False.fst(28,4-28,10): (Warning 240) Admitting NegativeTests.False.absurd without a definition