Skip to content

Commit

Permalink
Merge pull request #666 from hacspec/type0-instead-of-type
Browse files Browse the repository at this point in the history
fix(F*): always use `Type0`, never `Type`
  • Loading branch information
karthikbhargavan authored May 14, 2024
2 parents 6a4509d + a4552b2 commit 6cce50e
Show file tree
Hide file tree
Showing 9 changed files with 38 additions and 34 deletions.
2 changes: 2 additions & 0 deletions engine/backends/fstar/fstar_ast.ml
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
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
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
'''
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
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
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
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
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
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

0 comments on commit 6cce50e

Please sign in to comment.