From 7682980b78512b831562c3ec396bc501d3394d6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 15 Oct 2024 15:19:09 -0700 Subject: [PATCH 01/10] FStarC.Compiler.Util: implement pimap_remove --- ocaml/fstar-lib/FStarC_Compiler_Util.ml | 1 + src/basic/FStarC.Compiler.Util.fsti | 1 + 2 files changed, 2 insertions(+) diff --git a/ocaml/fstar-lib/FStarC_Compiler_Util.ml b/ocaml/fstar-lib/FStarC_Compiler_Util.ml index 8538e705878..9f3cee6eca1 100644 --- a/ocaml/fstar-lib/FStarC_Compiler_Util.ml +++ b/ocaml/fstar-lib/FStarC_Compiler_Util.ml @@ -468,6 +468,7 @@ let pimap_find_default (map: 'value pimap) (key: Z.t) (dflt: 'value) = let pimap_try_find (map: 'value pimap) (key: Z.t) = ZMap.Exceptionless.find key map let pimap_fold (m:'value pimap) f a = ZMap.fold f m a +let pimap_remove (m:'value pimap) k = ZMap.remove k m (* restore pre-2.11 BatString.nsplit behavior, see https://github.com/ocaml-batteries-team/batteries-included/issues/845 *) diff --git a/src/basic/FStarC.Compiler.Util.fsti b/src/basic/FStarC.Compiler.Util.fsti index e4a08c66911..62da14e5102 100644 --- a/src/basic/FStarC.Compiler.Util.fsti +++ b/src/basic/FStarC.Compiler.Util.fsti @@ -80,6 +80,7 @@ val pimap_add: pimap 'value -> int -> 'value -> pimap 'value val pimap_find_default: pimap 'value -> int -> 'value -> 'value val pimap_try_find: pimap 'value -> int -> option 'value val pimap_fold: pimap 'value -> (int -> 'value -> 'a -> 'a) -> 'a -> 'a +val pimap_remove: pimap 'value -> int -> pimap 'value val format: string -> list string -> string val format1: string -> string -> string From e807f1677e02775a5b4b21bb25e7f1eb7b99af9d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 15 Oct 2024 15:19:30 -0700 Subject: [PATCH 02/10] FStarC.Hash: expose a to_int operation --- ocaml/fstar-lib/FStarC_Hash.ml | 2 ++ src/basic/FStarC.Hash.fsti | 4 ++++ 2 files changed, 6 insertions(+) diff --git a/ocaml/fstar-lib/FStarC_Hash.ml b/ocaml/fstar-lib/FStarC_Hash.ml index 4a6947e7364..4ece1088b4a 100644 --- a/ocaml/fstar-lib/FStarC_Hash.ml +++ b/ocaml/fstar-lib/FStarC_Hash.ml @@ -5,6 +5,8 @@ type hash_code = int let cmp_hash (x:hash_code) (y:hash_code) : Z.t = Z.of_int (x-y) +let to_int (i:int) = Z.of_int i + let of_int (i:Z.t) = Z.to_int i let of_string (s:string) = BatHashtbl.hash s diff --git a/src/basic/FStarC.Hash.fsti b/src/basic/FStarC.Hash.fsti index 287932e35c7..cba5dc5b576 100644 --- a/src/basic/FStarC.Hash.fsti +++ b/src/basic/FStarC.Hash.fsti @@ -3,6 +3,10 @@ open FStarC.Compiler.Effect type hash_code +(* Unsure whether to expose this. Try not to use it. It's +useful in hashmap to use zarith imaps. *) +val to_int : hash_code -> int + val cmp_hash (_ _ : hash_code) : int val of_int : int -> hash_code From 068baa3961f5b2a1f3a50a00d6b568a4abffce03 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 15 Oct 2024 15:20:29 -0700 Subject: [PATCH 03/10] Introduce FStarC.Compiler.HashMap --- src/data/FStarC.Compiler.HashMap.fst | 72 +++++++++++++++++++++++++++ src/data/FStarC.Compiler.HashMap.fsti | 55 ++++++++++++++++++++ 2 files changed, 127 insertions(+) create mode 100644 src/data/FStarC.Compiler.HashMap.fst create mode 100644 src/data/FStarC.Compiler.HashMap.fsti diff --git a/src/data/FStarC.Compiler.HashMap.fst b/src/data/FStarC.Compiler.HashMap.fst new file mode 100644 index 00000000000..1de46a5e02e --- /dev/null +++ b/src/data/FStarC.Compiler.HashMap.fst @@ -0,0 +1,72 @@ +module FStarC.Compiler.HashMap + +(* This is implemented with a red black tree. We should use an actual hash table *) + +open FStarC +open FStarC.Compiler.Effect +open FStarC.Class.Hashable +module BU = FStarC.Compiler.Util + +let hashmap (k v : Type) : Tot Type0 = + BU.pimap (k & v) + +let empty (#k #v : _) : hashmap k v + = BU.pimap_empty () + +let add (#k #v : _) + {| deq k |} + {| hashable k |} + (key : k) + (value : v) + (m : hashmap k v) + : hashmap k v + = BU.pimap_add m (Hash.to_int <| hash key) (key, value) + +let remove (#k #v : _) + {| deq k |} + {| hashable k |} + (key : k) + (m : hashmap k v) + : hashmap k v + = BU.pimap_remove m (Hash.to_int <| hash key) // coarse + +let lookup (#k #v : _) + {| deq k |} + {| hashable k |} + (key : k) + (m : hashmap k v) + : option v + = match BU.pimap_try_find m (Hash.to_int <| hash key) with + | Some (key', v) when key =? key' -> Some v + | _ -> None + +(* lookup |> Some?.v *) +let get (#k #v : _) + {| deq k |} + {| hashable k |} + (key : k) + (m : hashmap k v) + : v + = Some?.v (lookup key m) + +let mem (#k #v : _) + {| deq k |} + {| hashable k |} + (key : k) + (m : hashmap k v) + : bool + = Some? (lookup key m) + +let cached_fun (#a #b : Type) {| hashable a |} {| deq a |} (f : a -> b) = + let cache = BU.mk_ref (empty #a #b) in + let f_cached = + fun x -> + match lookup x (!cache) with + | Some y -> y + | None -> + let y = f x in + cache := add x y !cache; + y + in + f_cached, (fun () -> cache := empty #a #b) + diff --git a/src/data/FStarC.Compiler.HashMap.fsti b/src/data/FStarC.Compiler.HashMap.fsti new file mode 100644 index 00000000000..f5801a15890 --- /dev/null +++ b/src/data/FStarC.Compiler.HashMap.fsti @@ -0,0 +1,55 @@ +module FStarC.Compiler.HashMap + +(* NOTE: THIS IS A CACHE. COLLISIONS WILL BE DROPPED/OVERWRITTEN. + +However you should not get a wrong value from lookup/get as we store the key +in the map too and compare it before returning the value. *) + +open FStarC.Class.Deq +open FStarC.Class.Hashable + +val hashmap (k v : Type) : Type0 + +type t = hashmap + +val empty (#k #v : _) : hashmap k v + +val add (#k #v : _) + {| deq k |} + {| hashable k |} + (key : k) + (value : v) + (m : hashmap k v) +: hashmap k v + +val remove (#k #v : _) + {| deq k |} + {| hashable k |} + (key : k) + (m : hashmap k v) + : hashmap k v + +val lookup (#k #v : _) + {| deq k |} + {| hashable k |} + (key : k) + (m : hashmap k v) + : option v + +(* lookup |> Some?.v *) +val get (#k #v : _) + {| deq k |} + {| hashable k |} + (key : k) + (m : hashmap k v) + : v + +val mem (#k #v : _) + {| deq k |} + {| hashable k |} + (key : k) + (m : hashmap k v) + : bool + +val cached_fun (#a #b : Type) {| hashable a |} {| deq a |} (f : a -> b) + : (a -> b) & (unit -> unit) // along with a reset fun From 5f5b8950775571b563ac74d0c1a54f277fb2b7a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 15 Oct 2024 13:39:41 -0700 Subject: [PATCH 04/10] Desugaring: some improvements Trying to make it faster, though not much luck. The bottleneck is name resolution. --- src/tosyntax/FStarC.ToSyntax.ToSyntax.fst | 29 +++++++++++++---------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst index 07f8fabff13..cdd89c4bb92 100644 --- a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst +++ b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst @@ -3650,11 +3650,13 @@ and desugar_decl_maybe_fail_attr env (d: decl): (env_t & sigelts) = let env0 = Env.snapshot env |> snd in (* we need the snapshot since pushing the let * will shadow a previous val *) + (* If this is an expect_failure, check to see if it fails. * If it does, check that the errors match as we normally do. * If it doesn't fail, leave it alone! The typechecker will check the failure. *) let env, sigelts = - let attrs = U.deduplicate_terms (List.map (desugar_term env) d.attrs) in + let attrs = List.map (desugar_term env) d.attrs in + let attrs = U.deduplicate_terms attrs in match get_fail_attr false attrs with | Some (expected_errs, lax) -> let d = { d with attrs = [] } in @@ -3900,6 +3902,7 @@ and desugar_decl_core env (d_attrs:list S.term) (d:decl) : (env_t & sigelts) = in if not expand_toplevel_pattern then begin + (* Usual case *) let lets = List.map (fun x -> None, x) lets in let as_inner_let = mk_term (Let(isrec, lets, mk_term (Const Const_unit) d.drange Expr)) d.drange Expr @@ -3912,16 +3915,16 @@ and desugar_decl_core env (d_attrs:list S.term) (d:decl) : (env_t & sigelts) = let val_quals, val_attrs = List.fold_right (fun fv (qs, ats) -> let qs', ats' = Env.lookup_letbinding_quals_and_attrs env fv.fv_name.v in - (qs'@qs, ats'@ats)) + (List.rev_append qs' qs, List.rev_append ats' ats)) fvs ([], []) in (* Propagate top-level attrs to each lb. The lb.lbattrs field should be empty, * but just being safe here. *) - let top_attrs = d_attrs in + let top_attrs = U.deduplicate_terms <| List.rev_append val_attrs d_attrs in let lbs = let (isrec, lbs0) = lbs in - let lbs0 = lbs0 |> List.map (fun lb -> { lb with lbattrs = U.deduplicate_terms (lb.lbattrs @ val_attrs @ top_attrs) }) in + let lbs0 = lbs0 |> List.map (fun lb -> { lb with lbattrs = U.deduplicate_terms (List.rev_append lb.lbattrs top_attrs) }) in (isrec, lbs0) in // BU.print3 "Desugaring %s, val_quals are %s, val_attrs are %s\n" @@ -3930,29 +3933,29 @@ and desugar_decl_core env (d_attrs:list S.term) (d:decl) : (env_t & sigelts) = // (List.map show val_attrs |> String.concat ", "); let quals = match quals with - | _::_ -> - List.map (trans_qual None) quals - | _ -> - val_quals + | _::_ -> List.map (trans_qual None) quals + | _ -> val_quals in let quals = if lets |> BU.for_some (fun (_, (_, t)) -> t.level=Formula) then S.Logic::quals - else quals in + else quals + in let names = fvs |> List.map (fun fv -> fv.fv_name.v) in let s = { sigel = Sig_let {lbs; lids=names}; sigquals = quals; sigrng = d.drange; sigmeta = default_sigmeta; - sigattrs = U.deduplicate_terms (val_attrs @ top_attrs); + sigattrs = top_attrs; sigopts = None; - sigopens_and_abbrevs = opens_and_abbrevs env + sigopens_and_abbrevs = opens_and_abbrevs env; } in let env = push_sigelt env s in env, [s] | _ -> failwith "Desugaring a let did not produce a let" end else + (* Need to expand the toplevel pattern into more toplevel lets *) (* If there is a top-level pattern we first bind the result of the body *) (* to some private anonymous name then we gather each idents bounded in *) (* the pattern and introduce one toplevel binding for each of them *) @@ -4285,9 +4288,9 @@ let desugar_decls env decls = let env, sigelts = List.fold_left (fun (env, sigelts) d -> let env, se = desugar_decl env d in - env, sigelts@se) (env, []) decls + env, List.rev_append se sigelts) (env, []) decls in - env, sigelts + env, List.rev sigelts (* Top-level functionality: from AST to a module Keeps track of the name of variables and so on (in the context) From 8c5d94ccac3c1dcb41c75a8895e4d3fb8a0535dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 15 Oct 2024 15:32:54 -0700 Subject: [PATCH 05/10] snap --- .../generated/FStarC_ToSyntax_ToSyntax.ml | 48 +++++++++---------- 1 file changed, 23 insertions(+), 25 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml index 0488b062bb7..712b6a29d93 100644 --- a/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml +++ b/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml @@ -9182,11 +9182,10 @@ and (desugar_decl_maybe_fail_attr : FStar_Pervasives_Native.snd uu___ in let uu___ = let attrs = - let uu___1 = - FStarC_Compiler_List.map (desugar_term env) - d.FStarC_Parser_AST.attrs in - FStarC_Syntax_Util.deduplicate_terms uu___1 in - let uu___1 = get_fail_attr false attrs in + FStarC_Compiler_List.map (desugar_term env) + d.FStarC_Parser_AST.attrs in + let attrs1 = FStarC_Syntax_Util.deduplicate_terms attrs in + let uu___1 = get_fail_attr false attrs1 in match uu___1 with | FStar_Pervasives_Native.Some (expected_errs, lax) -> let d1 = @@ -9202,7 +9201,7 @@ and (desugar_decl_maybe_fail_attr : FStarC_Errors.catch_errors (fun uu___3 -> FStarC_Options.with_saved_options - (fun uu___4 -> desugar_decl_core env attrs d1)) in + (fun uu___4 -> desugar_decl_core env attrs1 d1)) in (match uu___2 with | (errs, r) -> (match (errs, r) with @@ -9210,7 +9209,7 @@ and (desugar_decl_maybe_fail_attr : let ses1 = FStarC_Compiler_List.map (fun se -> - let uu___3 = no_fail_attrs attrs in + let uu___3 = no_fail_attrs attrs1 in { FStarC_Syntax_Syntax.sigel = (se.FStarC_Syntax_Syntax.sigel); @@ -9242,7 +9241,7 @@ and (desugar_decl_maybe_fail_attr : FStarC_Syntax_Syntax.sigquals = []; FStarC_Syntax_Syntax.sigmeta = FStarC_Syntax_Syntax.default_sigmeta; - FStarC_Syntax_Syntax.sigattrs = attrs; + FStarC_Syntax_Syntax.sigattrs = attrs1; FStarC_Syntax_Syntax.sigopens_and_abbrevs = uu___3; FStarC_Syntax_Syntax.sigopts = FStar_Pervasives_Native.None @@ -9335,7 +9334,7 @@ and (desugar_decl_maybe_fail_attr : FStarC_Errors_Msg.is_error_message_list_doc) (Obj.magic uu___8)); (env0, [])))))) - | FStar_Pervasives_Native.None -> desugar_decl_core env attrs d in + | FStar_Pervasives_Native.None -> desugar_decl_core env attrs1 d in match uu___ with | (env1, sigelts) -> (env1, sigelts) and (desugar_decl : env_t -> FStarC_Parser_AST.decl -> (env_t * FStarC_Syntax_Syntax.sigelts)) @@ -9821,13 +9820,16 @@ and (desugar_decl_core : (fv.FStarC_Syntax_Syntax.fv_name).FStarC_Syntax_Syntax.v in (match uu___6 with | (qs', ats') -> - ((FStarC_Compiler_List.op_At qs' - qs), - (FStarC_Compiler_List.op_At ats' - ats)))) fvs ([], []) in + ((FStarC_Compiler_List.rev_append + qs' qs), + (FStarC_Compiler_List.rev_append + ats' ats)))) fvs ([], []) in (match uu___4 with | (val_quals, val_attrs) -> - let top_attrs = d_attrs in + let top_attrs = + FStarC_Syntax_Util.deduplicate_terms + (FStarC_Compiler_List.rev_append val_attrs + d_attrs) in let lbs1 = let uu___5 = lbs in match uu___5 with @@ -9837,10 +9839,9 @@ and (desugar_decl_core : (fun lb -> let uu___6 = FStarC_Syntax_Util.deduplicate_terms - (FStarC_Compiler_List.op_At + (FStarC_Compiler_List.rev_append lb.FStarC_Syntax_Syntax.lbattrs - (FStarC_Compiler_List.op_At - val_attrs top_attrs)) in + top_attrs) in { FStarC_Syntax_Syntax.lbname = (lb.FStarC_Syntax_Syntax.lbname); @@ -9883,10 +9884,6 @@ and (desugar_decl_core : fvs in let s = let uu___5 = - FStarC_Syntax_Util.deduplicate_terms - (FStarC_Compiler_List.op_At val_attrs - top_attrs) in - let uu___6 = FStarC_Syntax_DsEnv.opens_and_abbrevs env in { FStarC_Syntax_Syntax.sigel = @@ -9900,9 +9897,9 @@ and (desugar_decl_core : FStarC_Syntax_Syntax.sigquals = quals2; FStarC_Syntax_Syntax.sigmeta = FStarC_Syntax_Syntax.default_sigmeta; - FStarC_Syntax_Syntax.sigattrs = uu___5; + FStarC_Syntax_Syntax.sigattrs = top_attrs; FStarC_Syntax_Syntax.sigopens_and_abbrevs = - uu___6; + uu___5; FStarC_Syntax_Syntax.sigopts = FStar_Pervasives_Native.None } in @@ -10572,9 +10569,10 @@ let (desugar_decls : let uu___2 = desugar_decl env1 d in (match uu___2 with | (env2, se) -> - (env2, (FStarC_Compiler_List.op_At sigelts se)))) + (env2, (FStarC_Compiler_List.rev_append se sigelts)))) (env, []) decls in - match uu___ with | (env1, sigelts) -> (env1, sigelts) + match uu___ with + | (env1, sigelts) -> (env1, (FStarC_Compiler_List.rev sigelts)) let (desugar_modul_common : FStarC_Syntax_Syntax.modul FStar_Pervasives_Native.option -> FStarC_Syntax_DsEnv.env -> From ae5ed1156aeccbcdeb097e711827e70e9ee315a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 15 Oct 2024 16:08:10 -0700 Subject: [PATCH 06/10] Syntax: more ord instances --- src/basic/FStarC.Ident.fst | 10 +++++ src/basic/FStarC.Ident.fsti | 3 ++ src/syntax/FStarC.Syntax.Syntax.fst | 62 ++++++++++++++++++++++++++++ src/syntax/FStarC.Syntax.Syntax.fsti | 2 + 4 files changed, 77 insertions(+) diff --git a/src/basic/FStarC.Ident.fst b/src/basic/FStarC.Ident.fst index d9c92fc8db6..daf8661d7c1 100644 --- a/src/basic/FStarC.Ident.fst +++ b/src/basic/FStarC.Ident.fst @@ -96,3 +96,13 @@ instance deq_ident = { instance deq_lident = { (=?) = lid_equals; } + +instance ord_ident = { + super = deq_ident; + cmp = (fun x y -> cmp (string_of_id x) (string_of_id y)); +} + +instance ord_lident = { + super = deq_lident; + cmp = (fun x y -> cmp (string_of_lid x) (string_of_lid y)); +} diff --git a/src/basic/FStarC.Ident.fsti b/src/basic/FStarC.Ident.fsti index 58614c5aaeb..f98fd55641b 100644 --- a/src/basic/FStarC.Ident.fsti +++ b/src/basic/FStarC.Ident.fsti @@ -19,6 +19,7 @@ open FStarC.Compiler.Range open FStarC.Class.Show open FStarC.Class.HasRange open FStarC.Class.Deq +open FStarC.Class.Ord open FStarC.Class.PP (** A (short) identifier for a local name. @@ -144,3 +145,5 @@ instance val hasrange_ident : hasRange ident instance val hasrange_lident : hasRange lident instance val deq_ident : deq ident instance val deq_lident : deq lident +instance val ord_ident : ord ident +instance val ord_lident : ord lident diff --git a/src/syntax/FStarC.Syntax.Syntax.fst b/src/syntax/FStarC.Syntax.Syntax.fst index d2cd26c8ab8..8c45901d78a 100644 --- a/src/syntax/FStarC.Syntax.Syntax.fst +++ b/src/syntax/FStarC.Syntax.Syntax.fst @@ -30,6 +30,7 @@ open FStarC.VConfig open FStarC.Class.Ord open FStarC.Class.HasRange open FStarC.Class.Setlike +open FStarC.Compiler.Order module O = FStarC.Options module PC = FStarC.Parser.Const @@ -85,6 +86,67 @@ instance showable_should_check_uvar = { // This is set in FStarC.Main.main, where all modules are in-scope. let lazy_chooser : ref (option (lazy_kind -> lazyinfo -> term)) = mk_ref None +let cmp_qualifier (q1 q2 : qualifier) : FStarC.Compiler.Order.order = + match q1, q2 with + | Assumption, Assumption -> Eq + | New, New -> Eq + | Private, Private -> Eq + | Unfold_for_unification_and_vcgen, Unfold_for_unification_and_vcgen -> Eq + | Irreducible, Irreducible -> Eq + | Inline_for_extraction, Inline_for_extraction -> Eq + | NoExtract, NoExtract -> Eq + | Noeq, Noeq -> Eq + | Unopteq, Unopteq -> Eq + | TotalEffect, TotalEffect -> Eq + | Logic, Logic -> Eq + | Reifiable, Reifiable -> Eq + | Reflectable l1, Reflectable l2 -> cmp l1 l2 + | Visible_default, Visible_default -> Eq + | Discriminator l1, Discriminator l2 -> cmp l1 l2 + | Projector (l1, i1), Projector (l2, i2) -> cmp (l1, i1) (l2, i2) + | RecordType (l1, i1), RecordType (l2, i2) -> cmp (l1, i1) (l2, i2) + | RecordConstructor (l1, i1), RecordConstructor (l2, i2) -> cmp (l1, i1) (l2, i2) + | Action l1, Action l2 -> cmp l1 l2 + | ExceptionConstructor, ExceptionConstructor -> Eq + | HasMaskedEffect, HasMaskedEffect -> Eq + | Effect, Effect -> Eq + | OnlyName, OnlyName -> Eq + | InternalAssumption, InternalAssumption -> Eq + + | Assumption, _ -> Lt | _, Assumption -> Gt + | New, _ -> Lt | _, New -> Gt + | Private, _ -> Lt | _, Private -> Gt + | Unfold_for_unification_and_vcgen, _ -> Lt | _, Unfold_for_unification_and_vcgen -> Gt + | Irreducible, _ -> Lt | _, Irreducible -> Gt + | Inline_for_extraction, _ -> Lt | _, Inline_for_extraction -> Gt + | NoExtract, _ -> Lt | _, NoExtract -> Gt + | Noeq, _ -> Lt | _, Noeq -> Gt + | Unopteq, _ -> Lt | _, Unopteq -> Gt + | TotalEffect, _ -> Lt | _, TotalEffect -> Gt + | Logic, _ -> Lt | _, Logic -> Gt + | Reifiable, _ -> Lt | _, Reifiable -> Gt + | Reflectable _, _ -> Lt | _, Reflectable _ -> Gt + | Visible_default, _ -> Lt | _, Visible_default -> Gt + | Discriminator _, _ -> Lt | _, Discriminator _ -> Gt + | Projector _, _ -> Lt | _, Projector _ -> Gt + | RecordType _, _ -> Lt | _, RecordType _ -> Gt + | RecordConstructor _, _ -> Lt | _, RecordConstructor _ -> Gt + | Action _, _ -> Lt | _, Action _ -> Gt + | ExceptionConstructor, _ -> Lt | _, ExceptionConstructor -> Gt + | HasMaskedEffect, _ -> Lt | _, HasMaskedEffect -> Gt + | Effect, _ -> Lt | _, Effect -> Gt + | OnlyName, _ -> Lt | _, OnlyName -> Gt + | InternalAssumption, _ -> Lt | _, InternalAssumption -> Gt + +instance deq_qualifier : deq qualifier = { + (=?) = (fun q1 q2 -> cmp_qualifier q1 q2 = Eq); +} + +instance ord_qualifier : ord qualifier = { + super = deq_qualifier; + cmp = cmp_qualifier; +} + let is_internal_qualifier (q:qualifier) : bool = match q with | Visible_default diff --git a/src/syntax/FStarC.Syntax.Syntax.fsti b/src/syntax/FStarC.Syntax.Syntax.fsti index e49545faad4..6677964d180 100644 --- a/src/syntax/FStarC.Syntax.Syntax.fsti +++ b/src/syntax/FStarC.Syntax.Syntax.fsti @@ -485,6 +485,8 @@ type qualifier = //is present only for name resolution and will be elaborated at typechecking | InternalAssumption //an assumption internally generated by F*, e.g. hasEq axioms, not to be reported with --report_assumes +instance val ord_qualifier : ord qualifier + (* Checks if the qualifer is internal, and should not be written by users. *) val is_internal_qualifier (q:qualifier) : bool From c454d61de6e9a4f64b043a5fafbcd3e84d0fc461 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 15 Oct 2024 16:10:15 -0700 Subject: [PATCH 07/10] Class.Ord: introduce sort_dedup and ord_list_diff --- src/class/FStarC.Class.Ord.fst | 43 ++++++++++++++++++++++++++++----- src/class/FStarC.Class.Ord.fsti | 11 +++++++++ 2 files changed, 48 insertions(+), 6 deletions(-) diff --git a/src/class/FStarC.Class.Ord.fst b/src/class/FStarC.Class.Ord.fst index 3890ecfcc48..3973e89cee0 100644 --- a/src/class/FStarC.Class.Ord.fst +++ b/src/class/FStarC.Class.Ord.fst @@ -14,12 +14,12 @@ let max x y = if x >=? y then x else y instance ord_eq (a:Type) (d : ord a) : Tot (deq a) = d.super -let rec insert (#a:Type) {| ord a |} (x:a) (xs:list a) : list a = - match xs with - | [] -> [x] - | y::ys -> if x <=? y then x :: y :: ys else y :: insert x ys - -let rec sort xs = +let rec sort #a xs = + let rec insert (x:a) (xs:list a) : list a = + match xs with + | [] -> [x] + | y::ys -> if x <=? y then x :: y :: ys else y :: insert x ys + in match xs with | [] -> [] | x::xs -> insert x (sort xs) @@ -29,6 +29,37 @@ let dedup #a xs = let out = fold_left (fun out x -> if existsb (fun y -> x =? y) out then out else x :: out) [] xs in List.rev out +let rec sort_dedup #a xs = + let rec insert (x:a) (xs:list a) : list a = + match xs with + | [] -> [x] + | y::ys -> + match cmp x y with + | Eq -> ys + | Lt -> x :: y :: ys + | Gt -> y :: insert x ys + in + match xs with + | [] -> [] + | x::xs -> insert x (sort_dedup xs) + +let ord_list_diff (#a:Type) {| ord a |} (xs ys : list a) : list a & list a = + let open FStarC.Compiler.Order in + let xs = xs |> sort_dedup in + let ys = ys |> sort_dedup in + let rec go (xd, yd) xs ys : list a & list a = + match xs, ys with + | x::xs, y::ys -> ( + match cmp x y with + | Lt -> go (x::xd, yd) xs (y::ys) + | Eq -> go (xd, yd) xs ys + | Gt -> go (xd, y::yd) (x::xs) ys + ) + (* One of the two is empty, that's it *) + | xs, ys -> (List.rev_append xd xs, List.rev_append yd ys) + in + go ([], []) xs ys + instance ord_int : ord int = { super = solve; cmp = compare_int; diff --git a/src/class/FStarC.Class.Ord.fsti b/src/class/FStarC.Class.Ord.fsti index 111d8ae38f0..990ed4be0cd 100644 --- a/src/class/FStarC.Class.Ord.fsti +++ b/src/class/FStarC.Class.Ord.fsti @@ -22,6 +22,17 @@ val dedup (xs : list a) : list a +(* Sort and deduplicate at once *) +val sort_dedup + (#a:Type) {| ord a |} + (xs : list a) + : list a + +(* Returns the difference of two lists, modulo order and duplication. +The first component is the elements only present in xs, and the second +is the elements only present in ys. *) +val ord_list_diff (#a:Type) {| ord a |} (xs ys : list a) : list a & list a + instance val ord_eq (a:Type) (d : ord a) : Tot (deq a) val ( {| ord a |} -> a -> a -> bool From 3a7e84e8606b88f1e4c3d808ab4730df3df184c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 15 Oct 2024 16:10:42 -0700 Subject: [PATCH 08/10] Tc: compare qualifiers modulo order and repetition Fixes #3232 --- src/class/FStarC.Class.Ord.fst | 2 +- src/class/FStarC.Class.Ord.fsti | 2 +- src/typechecker/FStarC.TypeChecker.Tc.fst | 27 ++++++++++++++++------- 3 files changed, 21 insertions(+), 10 deletions(-) diff --git a/src/class/FStarC.Class.Ord.fst b/src/class/FStarC.Class.Ord.fst index 3973e89cee0..01ee370a539 100644 --- a/src/class/FStarC.Class.Ord.fst +++ b/src/class/FStarC.Class.Ord.fst @@ -43,7 +43,7 @@ let rec sort_dedup #a xs = | [] -> [] | x::xs -> insert x (sort_dedup xs) -let ord_list_diff (#a:Type) {| ord a |} (xs ys : list a) : list a & list a = +let ord_list_diff (#a:Type0) {| ord a |} (xs ys : list a) : list a & list a = let open FStarC.Compiler.Order in let xs = xs |> sort_dedup in let ys = ys |> sort_dedup in diff --git a/src/class/FStarC.Class.Ord.fsti b/src/class/FStarC.Class.Ord.fsti index 990ed4be0cd..fc6b03031dc 100644 --- a/src/class/FStarC.Class.Ord.fsti +++ b/src/class/FStarC.Class.Ord.fsti @@ -31,7 +31,7 @@ val sort_dedup (* Returns the difference of two lists, modulo order and duplication. The first component is the elements only present in xs, and the second is the elements only present in ys. *) -val ord_list_diff (#a:Type) {| ord a |} (xs ys : list a) : list a & list a +val ord_list_diff (#a:Type0) {| ord a |} (xs ys : list a) : list a & list a instance val ord_eq (a:Type) (d : ord a) : Tot (deq a) diff --git a/src/typechecker/FStarC.TypeChecker.Tc.fst b/src/typechecker/FStarC.TypeChecker.Tc.fst index f14ec8743dc..fb673b295bf 100644 --- a/src/typechecker/FStarC.TypeChecker.Tc.fst +++ b/src/typechecker/FStarC.TypeChecker.Tc.fst @@ -37,6 +37,7 @@ open FStarC.Class.Show open FStarC.Class.Tagged open FStarC.Class.PP open FStarC.Class.Setlike +open FStarC.Class.Ord module S = FStarC.Syntax.Syntax module SP = FStarC.Syntax.Print @@ -284,23 +285,33 @@ let run_phase1 (f:unit -> 'a) = let tc_sig_let env r se lbs lids : list sigelt & list sigelt & Env.env = let env0 = env in let env = Env.set_range env r in - let check_quals_eq l qopt val_q = match qopt with + let check_quals_eq (l:lident) (qopt : option (list qualifier)) (val_q : list qualifier) : option (list qualifier) = + match qopt with | None -> Some val_q | Some q' -> //logic is now a deprecated qualifier, so discard it from the checking //AR: 05/19: drop irreducible also // irreducible is not allowed on val, but one could add it on let - let drop_logic_and_irreducible = List.filter (fun x -> not (x = Logic || x = Irreducible)) in - if (let val_q, q' = drop_logic_and_irreducible val_q, drop_logic_and_irreducible q' in - List.length val_q = List.length q' - && List.forall2 U.qualifier_equal val_q q') - then Some q' //but retain it in the returned list of qualifiers, some code may still add type annotations of Type0, which will hinder `logical` inference - else + let drop_logic_and_irreducible = List.filter (fun x -> not (Logic? x || Irreducible? x)) in + let val_q = drop_logic_and_irreducible val_q in + //but we retain it in the returned list of qualifiers, some code may still add type annotations of Type0, which will hinder `logical` inference + let q'0 = q' in + let q' = drop_logic_and_irreducible q' in + match Class.Ord.ord_list_diff val_q q' with + | [], [] -> Some q'0 + | d1, d2 -> let open FStarC.Pprint in raise_error r Errors.Fatal_InconsistentQualifierAnnotation [ text "Inconsistent qualifier annotations on" ^/^ doc_of_string (show l); prefix 4 1 (text "Expected") (squotes (arbitrary_string (show val_q))) ^/^ - prefix 4 1 (text "got") (squotes (arbitrary_string (show q'))) + prefix 4 1 (text "got") (squotes (arbitrary_string (show q'))); + + if Cons? d1 then + prefix 2 1 (text "Only in declaration: ") (squotes (arbitrary_string (show d1))) + else empty; + if Cons? d2 then + prefix 2 1 (text "Only in definition: ") (squotes (arbitrary_string (show d2))) + else empty; ] in From bd4767060c04a6bd8a17d3ccaf5b4803c979296a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 15 Oct 2024 16:12:44 -0700 Subject: [PATCH 09/10] snap --- ocaml/fstar-lib/generated/FStarC_Class_Ord.ml | 57 +++++- ocaml/fstar-lib/generated/FStarC_Ident.ml | 22 ++- .../generated/FStarC_Syntax_Syntax.ml | 108 ++++++++++++ .../generated/FStarC_TypeChecker_Tc.ml | 163 +++++++++++------- 4 files changed, 276 insertions(+), 74 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_Class_Ord.ml b/ocaml/fstar-lib/generated/FStarC_Class_Ord.ml index 9faa8a487bb..a0ddf556624 100644 --- a/ocaml/fstar-lib/generated/FStarC_Class_Ord.ml +++ b/ocaml/fstar-lib/generated/FStarC_Class_Ord.ml @@ -46,23 +46,20 @@ let max : 'a . 'a ord -> 'a -> 'a -> 'a = let uu___1 = op_Greater_Equals_Question uu___ x y in if uu___1 then x else y let ord_eq : 'a . 'a ord -> 'a FStarC_Class_Deq.deq = fun d -> d.super -let rec insert : 'a . 'a ord -> 'a -> 'a Prims.list -> 'a Prims.list = +let rec sort : 'a . 'a ord -> 'a Prims.list -> 'a Prims.list = fun uu___ -> - fun x -> - fun xs -> - match xs with + fun xs -> + let rec insert x xs1 = + match xs1 with | [] -> [x] | y::ys -> let uu___1 = op_Less_Equals_Question uu___ x y in if uu___1 then x :: y :: ys - else (let uu___3 = insert uu___ x ys in y :: uu___3) -let rec sort : 'a . 'a ord -> 'a Prims.list -> 'a Prims.list = - fun uu___ -> - fun xs -> + else (let uu___3 = insert x ys in y :: uu___3) in match xs with | [] -> [] - | x::xs1 -> let uu___1 = sort uu___ xs1 in insert uu___ x uu___1 + | x::xs1 -> let uu___1 = sort uu___ xs1 in insert x uu___1 let dedup : 'a . 'a ord -> 'a Prims.list -> 'a Prims.list = fun uu___ -> fun xs -> @@ -77,6 +74,48 @@ let dedup : 'a . 'a ord -> 'a Prims.list -> 'a Prims.list = out1 in if uu___1 then out1 else x :: out1) [] xs in FStarC_Compiler_List.rev out +let rec sort_dedup : 'a . 'a ord -> 'a Prims.list -> 'a Prims.list = + fun uu___ -> + fun xs -> + let rec insert x xs1 = + match xs1 with + | [] -> [x] + | y::ys -> + let uu___1 = cmp uu___ x y in + (match uu___1 with + | FStarC_Compiler_Order.Eq -> ys + | FStarC_Compiler_Order.Lt -> x :: y :: ys + | FStarC_Compiler_Order.Gt -> + let uu___2 = insert x ys in y :: uu___2) in + match xs with + | [] -> [] + | x::xs1 -> let uu___1 = sort_dedup uu___ xs1 in insert x uu___1 +let ord_list_diff : + 'a . + 'a ord -> + 'a Prims.list -> 'a Prims.list -> ('a Prims.list * 'a Prims.list) + = + fun uu___ -> + fun xs -> + fun ys -> + let xs1 = sort_dedup uu___ xs in + let ys1 = sort_dedup uu___ ys in + let rec go uu___1 xs2 ys2 = + match uu___1 with + | (xd, yd) -> + (match (xs2, ys2) with + | (x::xs3, y::ys3) -> + let uu___2 = cmp uu___ x y in + (match uu___2 with + | FStarC_Compiler_Order.Lt -> + go ((x :: xd), yd) xs3 (y :: ys3) + | FStarC_Compiler_Order.Eq -> go (xd, yd) xs3 ys3 + | FStarC_Compiler_Order.Gt -> + go (xd, (y :: yd)) (x :: xs3) ys3) + | (xs3, ys3) -> + ((FStarC_Compiler_List.rev_append xd xs3), + (FStarC_Compiler_List.rev_append yd ys3))) in + go ([], []) xs1 ys1 let (ord_int : Prims.int ord) = { super = FStarC_Class_Deq.deq_int; cmp = FStarC_Compiler_Order.compare_int } diff --git a/ocaml/fstar-lib/generated/FStarC_Ident.ml b/ocaml/fstar-lib/generated/FStarC_Ident.ml index 078307e82b0..fb08fc9782c 100644 --- a/ocaml/fstar-lib/generated/FStarC_Ident.ml +++ b/ocaml/fstar-lib/generated/FStarC_Ident.ml @@ -158,4 +158,24 @@ let (hasrange_lident : lident FStarC_Class_HasRange.hasRange) = let (deq_ident : ident FStarC_Class_Deq.deq) = { FStarC_Class_Deq.op_Equals_Question = ident_equals } let (deq_lident : lident FStarC_Class_Deq.deq) = - { FStarC_Class_Deq.op_Equals_Question = lid_equals } \ No newline at end of file + { FStarC_Class_Deq.op_Equals_Question = lid_equals } +let (ord_ident : ident FStarC_Class_Ord.ord) = + { + FStarC_Class_Ord.super = deq_ident; + FStarC_Class_Ord.cmp = + (fun x -> + fun y -> + let uu___ = string_of_id x in + let uu___1 = string_of_id y in + FStarC_Class_Ord.cmp FStarC_Class_Ord.ord_string uu___ uu___1) + } +let (ord_lident : lident FStarC_Class_Ord.ord) = + { + FStarC_Class_Ord.super = deq_lident; + FStarC_Class_Ord.cmp = + (fun x -> + fun y -> + let uu___ = string_of_lid x in + let uu___1 = string_of_lid y in + FStarC_Class_Ord.cmp FStarC_Class_Ord.ord_string uu___ uu___1) + } \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_Syntax.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_Syntax.ml index 93219e96e90..dbc45fd882b 100644 --- a/ocaml/fstar-lib/generated/FStarC_Syntax_Syntax.ml +++ b/ocaml/fstar-lib/generated/FStarC_Syntax_Syntax.ml @@ -1345,6 +1345,114 @@ let (lazy_chooser : (lazy_kind -> lazyinfo -> term) FStar_Pervasives_Native.option FStarC_Compiler_Effect.ref) = FStarC_Compiler_Util.mk_ref FStar_Pervasives_Native.None +let (cmp_qualifier : qualifier -> qualifier -> FStarC_Compiler_Order.order) = + fun q1 -> + fun q2 -> + match (q1, q2) with + | (Assumption, Assumption) -> FStarC_Compiler_Order.Eq + | (New, New) -> FStarC_Compiler_Order.Eq + | (Private, Private) -> FStarC_Compiler_Order.Eq + | (Unfold_for_unification_and_vcgen, Unfold_for_unification_and_vcgen) + -> FStarC_Compiler_Order.Eq + | (Irreducible, Irreducible) -> FStarC_Compiler_Order.Eq + | (Inline_for_extraction, Inline_for_extraction) -> + FStarC_Compiler_Order.Eq + | (NoExtract, NoExtract) -> FStarC_Compiler_Order.Eq + | (Noeq, Noeq) -> FStarC_Compiler_Order.Eq + | (Unopteq, Unopteq) -> FStarC_Compiler_Order.Eq + | (TotalEffect, TotalEffect) -> FStarC_Compiler_Order.Eq + | (Logic, Logic) -> FStarC_Compiler_Order.Eq + | (Reifiable, Reifiable) -> FStarC_Compiler_Order.Eq + | (Reflectable l1, Reflectable l2) -> + FStarC_Class_Ord.cmp FStarC_Ident.ord_lident l1 l2 + | (Visible_default, Visible_default) -> FStarC_Compiler_Order.Eq + | (Discriminator l1, Discriminator l2) -> + FStarC_Class_Ord.cmp FStarC_Ident.ord_lident l1 l2 + | (Projector (l1, i1), Projector (l2, i2)) -> + FStarC_Class_Ord.cmp + (FStarC_Class_Ord.ord_tuple2 FStarC_Ident.ord_lident + FStarC_Ident.ord_ident) (l1, i1) (l2, i2) + | (RecordType (l1, i1), RecordType (l2, i2)) -> + FStarC_Class_Ord.cmp + (FStarC_Class_Ord.ord_tuple2 + (FStarC_Class_Ord.ord_list FStarC_Ident.ord_ident) + (FStarC_Class_Ord.ord_list FStarC_Ident.ord_ident)) (l1, i1) + (l2, i2) + | (RecordConstructor (l1, i1), RecordConstructor (l2, i2)) -> + FStarC_Class_Ord.cmp + (FStarC_Class_Ord.ord_tuple2 + (FStarC_Class_Ord.ord_list FStarC_Ident.ord_ident) + (FStarC_Class_Ord.ord_list FStarC_Ident.ord_ident)) (l1, i1) + (l2, i2) + | (Action l1, Action l2) -> + FStarC_Class_Ord.cmp FStarC_Ident.ord_lident l1 l2 + | (ExceptionConstructor, ExceptionConstructor) -> + FStarC_Compiler_Order.Eq + | (HasMaskedEffect, HasMaskedEffect) -> FStarC_Compiler_Order.Eq + | (Effect, Effect) -> FStarC_Compiler_Order.Eq + | (OnlyName, OnlyName) -> FStarC_Compiler_Order.Eq + | (InternalAssumption, InternalAssumption) -> FStarC_Compiler_Order.Eq + | (Assumption, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, Assumption) -> FStarC_Compiler_Order.Gt + | (New, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, New) -> FStarC_Compiler_Order.Gt + | (Private, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, Private) -> FStarC_Compiler_Order.Gt + | (Unfold_for_unification_and_vcgen, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, Unfold_for_unification_and_vcgen) -> FStarC_Compiler_Order.Gt + | (Irreducible, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, Irreducible) -> FStarC_Compiler_Order.Gt + | (Inline_for_extraction, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, Inline_for_extraction) -> FStarC_Compiler_Order.Gt + | (NoExtract, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, NoExtract) -> FStarC_Compiler_Order.Gt + | (Noeq, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, Noeq) -> FStarC_Compiler_Order.Gt + | (Unopteq, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, Unopteq) -> FStarC_Compiler_Order.Gt + | (TotalEffect, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, TotalEffect) -> FStarC_Compiler_Order.Gt + | (Logic, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, Logic) -> FStarC_Compiler_Order.Gt + | (Reifiable, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, Reifiable) -> FStarC_Compiler_Order.Gt + | (Reflectable uu___, uu___1) -> FStarC_Compiler_Order.Lt + | (uu___, Reflectable uu___1) -> FStarC_Compiler_Order.Gt + | (Visible_default, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, Visible_default) -> FStarC_Compiler_Order.Gt + | (Discriminator uu___, uu___1) -> FStarC_Compiler_Order.Lt + | (uu___, Discriminator uu___1) -> FStarC_Compiler_Order.Gt + | (Projector uu___, uu___1) -> FStarC_Compiler_Order.Lt + | (uu___, Projector uu___1) -> FStarC_Compiler_Order.Gt + | (RecordType uu___, uu___1) -> FStarC_Compiler_Order.Lt + | (uu___, RecordType uu___1) -> FStarC_Compiler_Order.Gt + | (RecordConstructor uu___, uu___1) -> FStarC_Compiler_Order.Lt + | (uu___, RecordConstructor uu___1) -> FStarC_Compiler_Order.Gt + | (Action uu___, uu___1) -> FStarC_Compiler_Order.Lt + | (uu___, Action uu___1) -> FStarC_Compiler_Order.Gt + | (ExceptionConstructor, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, ExceptionConstructor) -> FStarC_Compiler_Order.Gt + | (HasMaskedEffect, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, HasMaskedEffect) -> FStarC_Compiler_Order.Gt + | (Effect, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, Effect) -> FStarC_Compiler_Order.Gt + | (OnlyName, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, OnlyName) -> FStarC_Compiler_Order.Gt + | (InternalAssumption, uu___) -> FStarC_Compiler_Order.Lt + | (uu___, InternalAssumption) -> FStarC_Compiler_Order.Gt +let (deq_qualifier : qualifier FStarC_Class_Deq.deq) = + { + FStarC_Class_Deq.op_Equals_Question = + (fun q1 -> + fun q2 -> + let uu___ = cmp_qualifier q1 q2 in + uu___ = FStarC_Compiler_Order.Eq) + } +let (ord_qualifier : qualifier FStarC_Class_Ord.ord) = + { + FStarC_Class_Ord.super = deq_qualifier; + FStarC_Class_Ord.cmp = cmp_qualifier + } let (is_internal_qualifier : qualifier -> Prims.bool) = fun q -> match q with diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Tc.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Tc.ml index 7987a9c6fc0..1fa9c884454 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Tc.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Tc.ml @@ -720,71 +720,106 @@ let (tc_sig_let : FStarC_Compiler_List.filter (fun x -> Prims.op_Negation - ((x = FStarC_Syntax_Syntax.Logic) || - (x = FStarC_Syntax_Syntax.Irreducible))) in + ((FStarC_Syntax_Syntax.uu___is_Logic x) || + (FStarC_Syntax_Syntax.uu___is_Irreducible x))) in + let val_q1 = drop_logic_and_irreducible val_q in + let q'0 = q' in + let q'1 = drop_logic_and_irreducible q' in let uu___ = - let uu___1 = - let uu___2 = drop_logic_and_irreducible val_q in - let uu___3 = drop_logic_and_irreducible q' in - (uu___2, uu___3) in - match uu___1 with - | (val_q1, q'1) -> - ((FStarC_Compiler_List.length val_q1) = - (FStarC_Compiler_List.length q'1)) - && - (FStarC_Compiler_List.forall2 - FStarC_Syntax_Util.qualifier_equal val_q1 q'1) in - if uu___ - then FStar_Pervasives_Native.Some q' - else - (let uu___2 = - let uu___3 = - let uu___4 = - FStarC_Errors_Msg.text - "Inconsistent qualifier annotations on" in - let uu___5 = - let uu___6 = - FStarC_Class_Show.show - FStarC_Ident.showable_lident l in - FStarC_Pprint.doc_of_string uu___6 in - FStarC_Pprint.op_Hat_Slash_Hat uu___4 uu___5 in - let uu___4 = - let uu___5 = - let uu___6 = - let uu___7 = FStarC_Errors_Msg.text "Expected" in - let uu___8 = - let uu___9 = - let uu___10 = - FStarC_Class_Show.show - (FStarC_Class_Show.show_list - FStarC_Syntax_Print.showable_qualifier) - val_q in - FStarC_Pprint.arbitrary_string uu___10 in - FStarC_Pprint.squotes uu___9 in - FStarC_Pprint.prefix (Prims.of_int (4)) - Prims.int_one uu___7 uu___8 in - let uu___7 = - let uu___8 = FStarC_Errors_Msg.text "got" in - let uu___9 = - let uu___10 = - let uu___11 = - FStarC_Class_Show.show - (FStarC_Class_Show.show_list - FStarC_Syntax_Print.showable_qualifier) - q' in - FStarC_Pprint.arbitrary_string uu___11 in - FStarC_Pprint.squotes uu___10 in - FStarC_Pprint.prefix (Prims.of_int (4)) - Prims.int_one uu___8 uu___9 in - FStarC_Pprint.op_Hat_Slash_Hat uu___6 uu___7 in - [uu___5] in - uu___3 :: uu___4 in - FStarC_Errors.raise_error - FStarC_Class_HasRange.hasRange_range r - FStarC_Errors_Codes.Fatal_InconsistentQualifierAnnotation - () - (Obj.magic FStarC_Errors_Msg.is_error_message_list_doc) - (Obj.magic uu___2)) in + FStarC_Class_Ord.ord_list_diff + FStarC_Syntax_Syntax.ord_qualifier val_q1 q'1 in + (match uu___ with + | ([], []) -> FStar_Pervasives_Native.Some q'0 + | (d1, d2) -> + let uu___1 = + let uu___2 = + let uu___3 = + FStarC_Errors_Msg.text + "Inconsistent qualifier annotations on" in + let uu___4 = + let uu___5 = + FStarC_Class_Show.show + FStarC_Ident.showable_lident l in + FStarC_Pprint.doc_of_string uu___5 in + FStarC_Pprint.op_Hat_Slash_Hat uu___3 uu___4 in + let uu___3 = + let uu___4 = + let uu___5 = + let uu___6 = FStarC_Errors_Msg.text "Expected" in + let uu___7 = + let uu___8 = + let uu___9 = + FStarC_Class_Show.show + (FStarC_Class_Show.show_list + FStarC_Syntax_Print.showable_qualifier) + val_q1 in + FStarC_Pprint.arbitrary_string uu___9 in + FStarC_Pprint.squotes uu___8 in + FStarC_Pprint.prefix (Prims.of_int (4)) + Prims.int_one uu___6 uu___7 in + let uu___6 = + let uu___7 = FStarC_Errors_Msg.text "got" in + let uu___8 = + let uu___9 = + let uu___10 = + FStarC_Class_Show.show + (FStarC_Class_Show.show_list + FStarC_Syntax_Print.showable_qualifier) + q'1 in + FStarC_Pprint.arbitrary_string uu___10 in + FStarC_Pprint.squotes uu___9 in + FStarC_Pprint.prefix (Prims.of_int (4)) + Prims.int_one uu___7 uu___8 in + FStarC_Pprint.op_Hat_Slash_Hat uu___5 uu___6 in + let uu___5 = + let uu___6 = + if Prims.uu___is_Cons d1 + then + let uu___7 = + FStarC_Errors_Msg.text + "Only in declaration: " in + let uu___8 = + let uu___9 = + let uu___10 = + FStarC_Class_Show.show + (FStarC_Class_Show.show_list + FStarC_Syntax_Print.showable_qualifier) + d1 in + FStarC_Pprint.arbitrary_string uu___10 in + FStarC_Pprint.squotes uu___9 in + FStarC_Pprint.prefix (Prims.of_int (2)) + Prims.int_one uu___7 uu___8 + else FStarC_Pprint.empty in + let uu___7 = + let uu___8 = + if Prims.uu___is_Cons d2 + then + let uu___9 = + FStarC_Errors_Msg.text + "Only in definition: " in + let uu___10 = + let uu___11 = + let uu___12 = + FStarC_Class_Show.show + (FStarC_Class_Show.show_list + FStarC_Syntax_Print.showable_qualifier) + d2 in + FStarC_Pprint.arbitrary_string uu___12 in + FStarC_Pprint.squotes uu___11 in + FStarC_Pprint.prefix (Prims.of_int (2)) + Prims.int_one uu___9 uu___10 + else FStarC_Pprint.empty in + [uu___8] in + uu___6 :: uu___7 in + uu___4 :: uu___5 in + uu___2 :: uu___3 in + FStarC_Errors.raise_error + FStarC_Class_HasRange.hasRange_range r + FStarC_Errors_Codes.Fatal_InconsistentQualifierAnnotation + () + (Obj.magic + FStarC_Errors_Msg.is_error_message_list_doc) + (Obj.magic uu___1)) in let rename_parameters lb = let rename_in_typ def typ = let typ1 = FStarC_Syntax_Subst.compress typ in From 1fd7fea65d959622d244a859bea72bcb5c48554e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 15 Oct 2024 16:16:19 -0700 Subject: [PATCH 10/10] Add some tests --- tests/bug-reports/Bug3232a.fst | 7 +++++++ tests/error-messages/Bug3232b.fst | 8 ++++++++ tests/error-messages/Bug3232b.fst.expected | 16 ++++++++++++++++ tests/error-messages/Bug3232b.fst.json_expected | 7 +++++++ tests/error-messages/Bug3232c.fst | 8 ++++++++ tests/error-messages/Bug3232c.fst.expected | 16 ++++++++++++++++ tests/error-messages/Bug3232c.fst.json_expected | 7 +++++++ tests/error-messages/Bug3232d.fst | 8 ++++++++ tests/error-messages/Bug3232d.fst.expected | 17 +++++++++++++++++ tests/error-messages/Bug3232d.fst.json_expected | 7 +++++++ 10 files changed, 101 insertions(+) create mode 100644 tests/bug-reports/Bug3232a.fst create mode 100644 tests/error-messages/Bug3232b.fst create mode 100644 tests/error-messages/Bug3232b.fst.expected create mode 100644 tests/error-messages/Bug3232b.fst.json_expected create mode 100644 tests/error-messages/Bug3232c.fst create mode 100644 tests/error-messages/Bug3232c.fst.expected create mode 100644 tests/error-messages/Bug3232c.fst.json_expected create mode 100644 tests/error-messages/Bug3232d.fst create mode 100644 tests/error-messages/Bug3232d.fst.expected create mode 100644 tests/error-messages/Bug3232d.fst.json_expected diff --git a/tests/bug-reports/Bug3232a.fst b/tests/bug-reports/Bug3232a.fst new file mode 100644 index 00000000000..fe64d11455b --- /dev/null +++ b/tests/bug-reports/Bug3232a.fst @@ -0,0 +1,7 @@ +module Bug3232a + +inline_for_extraction noextract +val f (x:int) : unit + +noextract inline_for_extraction +let f x = () diff --git a/tests/error-messages/Bug3232b.fst b/tests/error-messages/Bug3232b.fst new file mode 100644 index 00000000000..2e4027052bb --- /dev/null +++ b/tests/error-messages/Bug3232b.fst @@ -0,0 +1,8 @@ +module Bug3232b + +inline_for_extraction +val f (x:int) : unit + +[@@expect_failure] +noextract inline_for_extraction +let f x = () diff --git a/tests/error-messages/Bug3232b.fst.expected b/tests/error-messages/Bug3232b.fst.expected new file mode 100644 index 00000000000..da85bc8a39e --- /dev/null +++ b/tests/error-messages/Bug3232b.fst.expected @@ -0,0 +1,16 @@ +>> Got issues: [ +* Error 93 at Bug3232b.fst(8,0-8,12): + - Inconsistent qualifier annotations on Bug3232b.f + - Expected '[inline_for_extraction]' got '[noextract, inline_for_extraction]' + - Only in definition: '[noextract]' + +>>] +* Warning 240 at Bug3232b.fst(4,4-4,5): + - Bug3232b.f is declared but no definition was found + - Add an 'assume' if this is intentional + +* Warning 240 at Bug3232b.fst(8,0-8,12): + - Missing definitions in module Bug3232b: f + +Verified module: Bug3232b +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug3232b.fst.json_expected b/tests/error-messages/Bug3232b.fst.json_expected new file mode 100644 index 00000000000..bef17601f1c --- /dev/null +++ b/tests/error-messages/Bug3232b.fst.json_expected @@ -0,0 +1,7 @@ +>> Got issues: [ +{"msg":["Inconsistent qualifier annotations on\nBug3232b.f","Expected '[inline_for_extraction]'\ngot '[noextract, inline_for_extraction]'","","Only in definition: '[noextract]'"],"level":"Error","range":{"def":{"file_name":"Bug3232b.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}},"use":{"file_name":"Bug3232b.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":93,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]} +>>] +{"msg":["Bug3232b.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Bug3232b.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}},"use":{"file_name":"Bug3232b.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}}},"number":240,"ctx":["While desugaring module Bug3232b"]} +{"msg":["Missing definitions in module Bug3232b: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"Bug3232b.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":240,"ctx":[]} +Verified module: Bug3232b +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug3232c.fst b/tests/error-messages/Bug3232c.fst new file mode 100644 index 00000000000..0f11f6b4244 --- /dev/null +++ b/tests/error-messages/Bug3232c.fst @@ -0,0 +1,8 @@ +module Bug3232c + +inline_for_extraction noextract +val f (x:int) : unit + +[@@expect_failure] +noextract +let f x = () diff --git a/tests/error-messages/Bug3232c.fst.expected b/tests/error-messages/Bug3232c.fst.expected new file mode 100644 index 00000000000..73b9f6acc1a --- /dev/null +++ b/tests/error-messages/Bug3232c.fst.expected @@ -0,0 +1,16 @@ +>> Got issues: [ +* Error 93 at Bug3232c.fst(8,0-8,12): + - Inconsistent qualifier annotations on Bug3232c.f + - Expected '[inline_for_extraction, noextract]' got '[noextract]' + - Only in declaration: '[inline_for_extraction]' + +>>] +* Warning 240 at Bug3232c.fst(4,4-4,5): + - Bug3232c.f is declared but no definition was found + - Add an 'assume' if this is intentional + +* Warning 240 at Bug3232c.fst(8,0-8,12): + - Missing definitions in module Bug3232c: f + +Verified module: Bug3232c +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug3232c.fst.json_expected b/tests/error-messages/Bug3232c.fst.json_expected new file mode 100644 index 00000000000..d7c581d8a67 --- /dev/null +++ b/tests/error-messages/Bug3232c.fst.json_expected @@ -0,0 +1,7 @@ +>> Got issues: [ +{"msg":["Inconsistent qualifier annotations on\nBug3232c.f","Expected '[inline_for_extraction, noextract]'\ngot '[noextract]'","Only in declaration: '[inline_for_extraction]'",""],"level":"Error","range":{"def":{"file_name":"Bug3232c.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}},"use":{"file_name":"Bug3232c.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":93,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]} +>>] +{"msg":["Bug3232c.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Bug3232c.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}},"use":{"file_name":"Bug3232c.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}}},"number":240,"ctx":["While desugaring module Bug3232c"]} +{"msg":["Missing definitions in module Bug3232c: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"Bug3232c.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":240,"ctx":[]} +Verified module: Bug3232c +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug3232d.fst b/tests/error-messages/Bug3232d.fst new file mode 100644 index 00000000000..e74235dce41 --- /dev/null +++ b/tests/error-messages/Bug3232d.fst @@ -0,0 +1,8 @@ +module Bug3232d + +inline_for_extraction +val f (x:int) : unit + +[@@expect_failure] +noextract +let f x = () diff --git a/tests/error-messages/Bug3232d.fst.expected b/tests/error-messages/Bug3232d.fst.expected new file mode 100644 index 00000000000..539c6ed6000 --- /dev/null +++ b/tests/error-messages/Bug3232d.fst.expected @@ -0,0 +1,17 @@ +>> Got issues: [ +* Error 93 at Bug3232d.fst(8,0-8,12): + - Inconsistent qualifier annotations on Bug3232d.f + - Expected '[inline_for_extraction]' got '[noextract]' + - Only in declaration: '[inline_for_extraction]' + - Only in definition: '[noextract]' + +>>] +* Warning 240 at Bug3232d.fst(4,4-4,5): + - Bug3232d.f is declared but no definition was found + - Add an 'assume' if this is intentional + +* Warning 240 at Bug3232d.fst(8,0-8,12): + - Missing definitions in module Bug3232d: f + +Verified module: Bug3232d +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug3232d.fst.json_expected b/tests/error-messages/Bug3232d.fst.json_expected new file mode 100644 index 00000000000..9ea9b56781a --- /dev/null +++ b/tests/error-messages/Bug3232d.fst.json_expected @@ -0,0 +1,7 @@ +>> Got issues: [ +{"msg":["Inconsistent qualifier annotations on\nBug3232d.f","Expected '[inline_for_extraction]'\ngot '[noextract]'","Only in declaration: '[inline_for_extraction]'","Only in definition: '[noextract]'"],"level":"Error","range":{"def":{"file_name":"Bug3232d.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}},"use":{"file_name":"Bug3232d.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":93,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]} +>>] +{"msg":["Bug3232d.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Bug3232d.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}},"use":{"file_name":"Bug3232d.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}}},"number":240,"ctx":["While desugaring module Bug3232d"]} +{"msg":["Missing definitions in module Bug3232d: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"Bug3232d.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":240,"ctx":[]} +Verified module: Bug3232d +All verification conditions discharged successfully