Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix(F*): always use Type0, never Type #666

Merged
merged 1 commit into from
May 14, 2024
Merged

fix(F*): always use Type0, never Type #666

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions engine/backends/fstar/fstar_ast.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,8 @@ let mk_refined (x : string) (typ : AST.term) (phi : x:AST.term -> AST.term) =
let x_bd = mk_e_binder @@ AST.Annotated (x, typ) in
term @@ AST.Refine (x_bd, phi (term @@ AST.Var (lid_of_id x)))

let type0_term = AST.Name (lid [ "Type0" ]) |> term

let parse_string f s =
let open FStar_Parser_ParseIt in
let frag_of_text s =
Expand Down
7 changes: 3 additions & 4 deletions engine/backends/fstar/fstar_backend.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -627,8 +627,7 @@ struct
let ident = plocal_ident p.ident in
match p.kind with
| GPLifetime _ -> Error.assertion_failure span "pgeneric_param:LIFETIME"
| GPType { default = _ } ->
{ kind; typ = F.term @@ F.AST.Name (F.lid [ "Type" ]); ident }
| GPType { default = _ } -> { kind; typ = F.type0_term; ident }
| GPConst { typ } -> { kind = Explicit; typ = pty span typ; ident }

let of_generic_constraint span (nth : int) (c : generic_constraint) =
Expand Down Expand Up @@ -987,7 +986,7 @@ struct
}
else
let generics = FStarBinder.of_generics e.span generics in
let ty = F.term @@ F.AST.Name (F.lid [ "Type" ]) in
let ty = F.type0_term in
let arrow_typ =
F.term
@@ F.AST.Product (List.map ~f:FStarBinder.to_binder generics, ty)
Expand Down Expand Up @@ -1169,7 +1168,7 @@ struct
let fields =
match i.ti_v with
| TIType bounds ->
let t = F.term @@ F.AST.Name (F.lid [ "Type" ]) in
let t = F.type0_term in
(* let constraints = *)
(* List.map *)
(* ~f:(fun implements -> *)
Expand Down
4 changes: 2 additions & 2 deletions test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ module Attribute_opaque
open Core
open FStar.Mul

val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type) : Type
val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0

val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type) : Type
val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0
'''
2 changes: 1 addition & 1 deletion test-harness/src/snapshots/toolchain__attributes into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_1 (#v_T: Type) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
{
f_Output = v_T;
f_index_pre = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> true);
Expand Down
15 changes: 9 additions & 6 deletions test-harness/src/snapshots/toolchain__generics into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ module Generics.Defaults_generics
open Core
open FStar.Mul

type t_Defaults (v_T: Type) (v_N: usize) = | Defaults : t_Array v_T v_N -> t_Defaults v_T v_N
type t_Defaults (v_T: Type0) (v_N: usize) = | Defaults : t_Array v_T v_N -> t_Defaults v_T v_N

let f (_: t_Defaults Prims.unit (sz 2)) : Prims.unit = ()
'''
Expand All @@ -45,10 +45,10 @@ module Generics
open Core
open FStar.Mul

let impl__Bar__inherent_impl_generics (#v_T: Type) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
()

class t_Foo (v_Self: Type) = {
class t_Foo (v_Self: Type0) = {
f_const_add_pre:v_N: usize -> v_Self -> bool;
f_const_add_post:v_N: usize -> v_Self -> usize -> bool;
f_const_add:v_N: usize -> x0: v_Self
Expand All @@ -63,7 +63,10 @@ let impl_Foo_for_usize: t_Foo usize =
f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
}

let dup (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T) (x: v_T)
let dup
(#v_T: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T)
(x: v_T)
: (v_T & v_T) = Core.Clone.f_clone x, Core.Clone.f_clone x <: (v_T & v_T)

let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x
Expand All @@ -72,7 +75,7 @@ let call_f (_: Prims.unit) : usize = (f (sz 10) (sz 3) <: usize) +! sz 3

let g
(v_N: usize)
(#v_T: Type)
(#v_T: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Convert.t_Into v_T (t_Array usize v_N))
(arr: v_T)
: usize =
Expand Down Expand Up @@ -117,7 +120,7 @@ let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =

let repeat
(v_LEN: usize)
(#v_T: Type)
(#v_T: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T)
(x: v_T)
: t_Array v_T v_LEN = Rust_primitives.Hax.repeat x v_LEN
Expand Down
4 changes: 2 additions & 2 deletions test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ module Include_flag
open Core
open FStar.Mul

class t_Trait (v_Self: Type) = { __marker_trait_t_Trait:Prims.unit }
class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }

/// Indirect dependencies
let main_a_a (_: Prims.unit) : Prims.unit = ()
Expand All @@ -42,7 +42,7 @@ let main_a_b (_: Prims.unit) : Prims.unit = ()
let main_a_c (_: Prims.unit) : Prims.unit = ()

/// Direct dependencies
let main_a (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T)
let main_a (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T)
: Prims.unit =
let _:Prims.unit = main_a_a () in
let _:Prims.unit = main_a_b () in
Expand Down
4 changes: 2 additions & 2 deletions test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ module Mut_ref_functionalization
open Core
open FStar.Mul

class t_FooTrait (v_Self: Type) = {
class t_FooTrait (v_Self: Type0) = {
f_z_pre:v_Self -> bool;
f_z_post:v_Self -> v_Self -> bool;
f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result)
Expand Down Expand Up @@ -230,7 +230,7 @@ let j (x: t_Bar) : (t_Bar & u8) =
let hax_temp_output:u8 = out1 +! out in
x, hax_temp_output <: (t_Bar & u8)

type t_Pair (v_T: Type) = {
type t_Pair (v_T: Type0) = {
f_a:v_T;
f_b:t_Foo
}
Expand Down
12 changes: 6 additions & 6 deletions test-harness/src/snapshots/toolchain__naming into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,27 +108,27 @@ type t_Foo2 =
| Foo2_A : t_Foo2
| Foo2_B { f_x:usize }: t_Foo2

class t_FooTrait (v_Self: Type) = { f_ASSOCIATED_CONSTANT:usize }
class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }

class t_T1 (v_Self: Type) = { __marker_trait_t_T1:Prims.unit }
class t_T1 (v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_T1_for_Foo: t_T1 t_Foo = { __marker_trait = () }

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_T1_for_tuple_Foo_u8: t_T1 (t_Foo & u8) = { __marker_trait = () }

class t_T2_for_a (v_Self: Type) = { __marker_trait_t_T2_for_a:Prims.unit }
class t_T2_for_a (v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit }

class t_T3_e_for_a (v_Self: Type) = { __marker_trait_t_T3_e_for_a:Prims.unit }
class t_T3_e_for_a (v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit }

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () }

let v_INHERENT_CONSTANT: usize = sz 3

let constants
(#v_T: Type)
(#v_T: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T)
(_: Prims.unit)
: usize = f_ASSOCIATED_CONSTANT +! v_INHERENT_CONSTANT
Expand All @@ -143,7 +143,7 @@ let ff__g__impl_1__g (self: t_Foo) : usize = sz 1

let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_of

type t_Arity1 (v_T: Type) = | Arity1 : v_T -> t_Arity1 v_T
type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_T2_e_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a (t_Arity1 (t_Foo & u8)) =
Expand Down
22 changes: 11 additions & 11 deletions test-harness/src/snapshots/toolchain__traits into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,13 +35,13 @@ module Traits
open Core
open FStar.Mul

class t_Bar (v_Self: Type) = {
class t_Bar (v_Self: Type0) = {
f_bar_pre:v_Self -> bool;
f_bar_post:v_Self -> Prims.unit -> bool;
f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result)
}

let impl_2__method (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T)
let impl_2__method (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T)
: Prims.unit = f_bar x

type t_Error = | Error_Fail : t_Error
Expand All @@ -53,15 +53,15 @@ let impl__Error__for_application_callback (_: Prims.unit) : Prims.unit -> t_Err

let t_Error_cast_to_repr (x: t_Error) : isize = match x with | Error_Fail -> isz 0

class t_Lang (v_Self: Type) = {
f_Var:Type;
class t_Lang (v_Self: Type0) = {
f_Var:Type0;
f_s_pre:v_Self -> i32 -> bool;
f_s_post:v_Self -> i32 -> (v_Self & f_Var) -> bool;
f_s:x0: v_Self -> x1: i32
-> Prims.Pure (v_Self & f_Var) (f_s_pre x0 x1) (fun result -> f_s_post x0 x1 result)
}

class t_SuperTrait (v_Self: Type) = {
class t_SuperTrait (v_Self: Type0) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_4075428158603710007:Core.Clone.t_Clone v_Self;
f_function_of_super_trait_pre:v_Self -> bool;
f_function_of_super_trait_post:v_Self -> u32 -> bool;
Expand All @@ -80,8 +80,8 @@ let impl_SuperTrait_for_i32: t_SuperTrait i32 =
f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32
}

class t_Foo (v_Self: Type) = {
f_AssocType:Type;
class t_Foo (v_Self: Type0) = {
f_AssocType:Type0;
f_AssocType_12975176671554111340:t_SuperTrait f_AssocType;
f_AssocType_15292246028710717365:Core.Clone.t_Clone f_AssocType;
f_N:usize;
Expand All @@ -100,7 +100,7 @@ class t_Foo (v_Self: Type) = {
}

let closure_impl_expr
(#v_I: Type)
(#v_I: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Iter.Traits.Iterator.t_Iterator v_I)
(it: v_I)
: Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global =
Expand All @@ -109,7 +109,7 @@ let closure_impl_expr
Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit))

let closure_impl_expr_fngen
(#v_I #v_F: Type)
(#v_I #v_F: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Core.Iter.Traits.Iterator.t_Iterator v_I)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i3: Core.Ops.Function.t_FnMut v_F Prims.unit)
(it: v_I)
Expand All @@ -119,11 +119,11 @@ let closure_impl_expr_fngen
<:
Core.Iter.Adapters.Map.t_Map v_I v_F)

let f (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit =
let f (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit =
let _:Prims.unit = f_assoc_f () in
f_method_f x

let g (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: i1.f_AssocType)
let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: i1.f_AssocType)
: u32 = f_function_of_super_trait x

[@@ FStar.Tactics.Typeclasses.tcinstance]
Expand Down
Loading