summaryrefslogtreecommitdiff
path: root/tests/fstar-split/traits
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/fstar-split/traits/Makefile49
-rw-r--r--tests/fstar-split/traits/Primitives.fst884
-rw-r--r--tests/fstar-split/traits/Traits.fst468
3 files changed, 0 insertions, 1401 deletions
diff --git a/tests/fstar-split/traits/Makefile b/tests/fstar-split/traits/Makefile
deleted file mode 100644
index fa7d1f36..00000000
--- a/tests/fstar-split/traits/Makefile
+++ /dev/null
@@ -1,49 +0,0 @@
-# This file was automatically generated - modify ../Makefile.template instead
-INCLUDE_DIRS = .
-
-FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
-
-FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
-
-FSTAR_OPTIONS = $(FSTAR_HINTS) \
- --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
- --warn_error '+241@247+285-274' \
-
-FSTAR_EXE ?= fstar.exe
-FSTAR_NO_FLAGS = $(FSTAR_EXE) --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
-
-FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
-
-# The F* roots are used to compute the dependency graph, and generate the .depend file
-FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
-
-# Build all the files
-all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
-
-# This is the right way to ensure the .depend file always gets re-built.
-ifeq (,$(filter %-in,$(MAKECMDGOALS)))
-ifndef NODEPEND
-ifndef MAKE_RESTARTS
-.depend: .FORCE
- $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@
-
-.PHONY: .FORCE
-.FORCE:
-endif
-endif
-
-include .depend
-endif
-
-# For the interactive mode
-%.fst-in %.fsti-in:
- @echo $(FSTAR_OPTIONS)
-
-# Generete the .checked files in batch mode
-%.checked:
- $(FSTAR) $(FSTAR_OPTIONS) $< && \
- touch -c $@
-
-.PHONY: clean
-clean:
- rm -f obj/*
diff --git a/tests/fstar-split/traits/Primitives.fst b/tests/fstar-split/traits/Primitives.fst
deleted file mode 100644
index a3ffbde4..00000000
--- a/tests/fstar-split/traits/Primitives.fst
+++ /dev/null
@@ -1,884 +0,0 @@
-/// This file lists primitive and assumed functions and types
-module Primitives
-open FStar.Mul
-open FStar.List.Tot
-
-#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
-
-(*** Utilities *)
-val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) :
- ls':list a{
- length ls' = length ls /\
- index ls' i == x
- }
-#push-options "--fuel 1"
-let rec list_update #a ls i x =
- match ls with
- | x' :: ls -> if i = 0 then x :: ls else x' :: list_update ls (i-1) x
-#pop-options
-
-(*** Result *)
-type error : Type0 =
-| Failure
-| OutOfFuel
-
-type result (a : Type0) : Type0 =
-| Return : v:a -> result a
-| Fail : e:error -> result a
-
-// Monadic return operator
-unfold let return (#a : Type0) (x : a) : result a = Return x
-
-// Monadic bind operator.
-// Allows to use the notation:
-// ```
-// let* x = y in
-// ...
-// ```
-unfold let (let*) (#a #b : Type0) (m: result a)
- (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) :
- result b =
- match m with
- | Return x -> f x
- | Fail e -> Fail e
-
-// Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail Failure
-
-// Normalize and unwrap a successful result (used for globals).
-let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
-
-(*** Misc *)
-type char = FStar.Char.char
-type string = string
-
-let is_zero (n: nat) : bool = n = 0
-let decrease (n: nat{n > 0}) : nat = n - 1
-
-let core_mem_replace (a : Type0) (x : a) (y : a) : a = x
-let core_mem_replace_back (a : Type0) (x : a) (y : a) : a = y
-
-// We don't really use raw pointers for now
-type mut_raw_ptr (t : Type0) = { v : t }
-type const_raw_ptr (t : Type0) = { v : t }
-
-(*** Scalars *)
-/// Rem.: most of the following code was partially generated
-
-assume val size_numbits : pos
-
-// TODO: we could use FStar.Int.int_t and FStar.UInt.int_t
-
-let isize_min : int = -9223372036854775808 // TODO: should be opaque
-let isize_max : int = 9223372036854775807 // TODO: should be opaque
-let i8_min : int = -128
-let i8_max : int = 127
-let i16_min : int = -32768
-let i16_max : int = 32767
-let i32_min : int = -2147483648
-let i32_max : int = 2147483647
-let i64_min : int = -9223372036854775808
-let i64_max : int = 9223372036854775807
-let i128_min : int = -170141183460469231731687303715884105728
-let i128_max : int = 170141183460469231731687303715884105727
-let usize_min : int = 0
-let usize_max : int = 4294967295 // TODO: should be opaque
-let u8_min : int = 0
-let u8_max : int = 255
-let u16_min : int = 0
-let u16_max : int = 65535
-let u32_min : int = 0
-let u32_max : int = 4294967295
-let u64_min : int = 0
-let u64_max : int = 18446744073709551615
-let u128_min : int = 0
-let u128_max : int = 340282366920938463463374607431768211455
-
-type scalar_ty =
-| Isize
-| I8
-| I16
-| I32
-| I64
-| I128
-| Usize
-| U8
-| U16
-| U32
-| U64
-| U128
-
-let is_unsigned = function
- | Isize | I8 | I16 | I32 | I64 | I128 -> false
- | Usize | U8 | U16 | U32 | U64 | U128 -> true
-
-let scalar_min (ty : scalar_ty) : int =
- match ty with
- | Isize -> isize_min
- | I8 -> i8_min
- | I16 -> i16_min
- | I32 -> i32_min
- | I64 -> i64_min
- | I128 -> i128_min
- | Usize -> usize_min
- | U8 -> u8_min
- | U16 -> u16_min
- | U32 -> u32_min
- | U64 -> u64_min
- | U128 -> u128_min
-
-let scalar_max (ty : scalar_ty) : int =
- match ty with
- | Isize -> isize_max
- | I8 -> i8_max
- | I16 -> i16_max
- | I32 -> i32_max
- | I64 -> i64_max
- | I128 -> i128_max
- | Usize -> usize_max
- | U8 -> u8_max
- | U16 -> u16_max
- | U32 -> u32_max
- | U64 -> u64_max
- | U128 -> u128_max
-
-type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
-
-let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
- if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
-
-let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
-
-let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
- if y <> 0 then mk_scalar ty (x / y) else Fail Failure
-
-/// The remainder operation
-let int_rem (x : int) (y : int{y <> 0}) : int =
- if x >= 0 then (x % y) else -(x % y)
-
-(* Checking consistency with Rust *)
-let _ = assert_norm(int_rem 1 2 = 1)
-let _ = assert_norm(int_rem (-1) 2 = -1)
-let _ = assert_norm(int_rem 1 (-2) = 1)
-let _ = assert_norm(int_rem (-1) (-2) = -1)
-
-let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
- if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
-
-let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
- mk_scalar ty (x + y)
-
-let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
- mk_scalar ty (x - y)
-
-let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
- mk_scalar ty (x * y)
-
-let scalar_xor (#ty : scalar_ty)
- (x : scalar ty) (y : scalar ty) : scalar ty =
- match ty with
- | U8 -> FStar.UInt.logxor #8 x y
- | U16 -> FStar.UInt.logxor #16 x y
- | U32 -> FStar.UInt.logxor #32 x y
- | U64 -> FStar.UInt.logxor #64 x y
- | U128 -> FStar.UInt.logxor #128 x y
- | Usize -> admit() // TODO
- | I8 ->
- // Encoding issues...
- normalize_spec (FStar.Int.int_t 8);
- normalize_spec (scalar I8);
- FStar.Int.logxor #8 x y
- | I16 ->
- // Encoding issues...
- normalize_spec (FStar.Int.int_t 16);
- normalize_spec (scalar I16);
- FStar.Int.logxor #16 x y
- | I32 -> FStar.Int.logxor #32 x y
- | I64 -> FStar.Int.logxor #64 x y
- | I128 ->
- // Encoding issues...
- normalize_spec (FStar.Int.int_t 128);
- normalize_spec (scalar I128);
- FStar.Int.logxor #128 x y
- | Isize -> admit() // TODO
-
-let scalar_or (#ty : scalar_ty)
- (x : scalar ty) (y : scalar ty) : scalar ty =
- match ty with
- | U8 -> FStar.UInt.logor #8 x y
- | U16 -> FStar.UInt.logor #16 x y
- | U32 -> FStar.UInt.logor #32 x y
- | U64 -> FStar.UInt.logor #64 x y
- | U128 -> FStar.UInt.logor #128 x y
- | Usize -> admit() // TODO
- | I8 ->
- // Encoding issues...
- normalize_spec (FStar.Int.int_t 8);
- normalize_spec (scalar I8);
- FStar.Int.logor #8 x y
- | I16 ->
- // Encoding issues...
- normalize_spec (FStar.Int.int_t 16);
- normalize_spec (scalar I16);
- FStar.Int.logor #16 x y
- | I32 -> FStar.Int.logor #32 x y
- | I64 -> FStar.Int.logor #64 x y
- | I128 ->
- // Encoding issues...
- normalize_spec (FStar.Int.int_t 128);
- normalize_spec (scalar I128);
- FStar.Int.logor #128 x y
- | Isize -> admit() // TODO
-
-let scalar_and (#ty : scalar_ty)
- (x : scalar ty) (y : scalar ty) : scalar ty =
- match ty with
- | U8 -> FStar.UInt.logand #8 x y
- | U16 -> FStar.UInt.logand #16 x y
- | U32 -> FStar.UInt.logand #32 x y
- | U64 -> FStar.UInt.logand #64 x y
- | U128 -> FStar.UInt.logand #128 x y
- | Usize -> admit() // TODO
- | I8 ->
- // Encoding issues...
- normalize_spec (FStar.Int.int_t 8);
- normalize_spec (scalar I8);
- FStar.Int.logand #8 x y
- | I16 ->
- // Encoding issues...
- normalize_spec (FStar.Int.int_t 16);
- normalize_spec (scalar I16);
- FStar.Int.logand #16 x y
- | I32 -> FStar.Int.logand #32 x y
- | I64 -> FStar.Int.logand #64 x y
- | I128 ->
- // Encoding issues...
- normalize_spec (FStar.Int.int_t 128);
- normalize_spec (scalar I128);
- FStar.Int.logand #128 x y
- | Isize -> admit() // TODO
-
-// Shift left
-let scalar_shl (#ty0 #ty1 : scalar_ty)
- (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) =
- admit()
-
-// Shift right
-let scalar_shr (#ty0 #ty1 : scalar_ty)
- (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) =
- admit()
-
-(** Cast an integer from a [src_ty] to a [tgt_ty] *)
-// TODO: check the semantics of casts in Rust
-let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
- mk_scalar tgt_ty x
-
-// This can't fail, but for now we make all casts faillible (easier for the translation)
-let scalar_cast_bool (tgt_ty : scalar_ty) (x : bool) : result (scalar tgt_ty) =
- mk_scalar tgt_ty (if x then 1 else 0)
-
-/// The scalar types
-type isize : eqtype = scalar Isize
-type i8 : eqtype = scalar I8
-type i16 : eqtype = scalar I16
-type i32 : eqtype = scalar I32
-type i64 : eqtype = scalar I64
-type i128 : eqtype = scalar I128
-type usize : eqtype = scalar Usize
-type u8 : eqtype = scalar U8
-type u16 : eqtype = scalar U16
-type u32 : eqtype = scalar U32
-type u64 : eqtype = scalar U64
-type u128 : eqtype = scalar U128
-
-
-let core_isize_min : isize = isize_min
-let core_isize_max : isize = isize_max
-let core_i8_min : i8 = i8_min
-let core_i8_max : i8 = i8_max
-let core_i16_min : i16 = i16_min
-let core_i16_max : i16 = i16_max
-let core_i32_min : i32 = i32_min
-let core_i32_max : i32 = i32_max
-let core_i64_min : i64 = i64_min
-let core_i64_max : i64 = i64_max
-let core_i128_min : i128 = i128_min
-let core_i128_max : i128 = i128_max
-
-let core_usize_min : usize = usize_min
-let core_usize_max : usize = usize_max
-let core_u8_min : u8 = u8_min
-let core_u8_max : u8 = u8_max
-let core_u16_min : u16 = u16_min
-let core_u16_max : u16 = u16_max
-let core_u32_min : u32 = u32_min
-let core_u32_max : u32 = u32_max
-let core_u64_min : u64 = u64_min
-let core_u64_max : u64 = u64_max
-let core_u128_min : u128 = u128_min
-let core_u128_max : u128 = u128_max
-
-/// Negation
-let isize_neg = scalar_neg #Isize
-let i8_neg = scalar_neg #I8
-let i16_neg = scalar_neg #I16
-let i32_neg = scalar_neg #I32
-let i64_neg = scalar_neg #I64
-let i128_neg = scalar_neg #I128
-
-/// Division
-let isize_div = scalar_div #Isize
-let i8_div = scalar_div #I8
-let i16_div = scalar_div #I16
-let i32_div = scalar_div #I32
-let i64_div = scalar_div #I64
-let i128_div = scalar_div #I128
-let usize_div = scalar_div #Usize
-let u8_div = scalar_div #U8
-let u16_div = scalar_div #U16
-let u32_div = scalar_div #U32
-let u64_div = scalar_div #U64
-let u128_div = scalar_div #U128
-
-/// Remainder
-let isize_rem = scalar_rem #Isize
-let i8_rem = scalar_rem #I8
-let i16_rem = scalar_rem #I16
-let i32_rem = scalar_rem #I32
-let i64_rem = scalar_rem #I64
-let i128_rem = scalar_rem #I128
-let usize_rem = scalar_rem #Usize
-let u8_rem = scalar_rem #U8
-let u16_rem = scalar_rem #U16
-let u32_rem = scalar_rem #U32
-let u64_rem = scalar_rem #U64
-let u128_rem = scalar_rem #U128
-
-/// Addition
-let isize_add = scalar_add #Isize
-let i8_add = scalar_add #I8
-let i16_add = scalar_add #I16
-let i32_add = scalar_add #I32
-let i64_add = scalar_add #I64
-let i128_add = scalar_add #I128
-let usize_add = scalar_add #Usize
-let u8_add = scalar_add #U8
-let u16_add = scalar_add #U16
-let u32_add = scalar_add #U32
-let u64_add = scalar_add #U64
-let u128_add = scalar_add #U128
-
-/// Subtraction
-let isize_sub = scalar_sub #Isize
-let i8_sub = scalar_sub #I8
-let i16_sub = scalar_sub #I16
-let i32_sub = scalar_sub #I32
-let i64_sub = scalar_sub #I64
-let i128_sub = scalar_sub #I128
-let usize_sub = scalar_sub #Usize
-let u8_sub = scalar_sub #U8
-let u16_sub = scalar_sub #U16
-let u32_sub = scalar_sub #U32
-let u64_sub = scalar_sub #U64
-let u128_sub = scalar_sub #U128
-
-/// Multiplication
-let isize_mul = scalar_mul #Isize
-let i8_mul = scalar_mul #I8
-let i16_mul = scalar_mul #I16
-let i32_mul = scalar_mul #I32
-let i64_mul = scalar_mul #I64
-let i128_mul = scalar_mul #I128
-let usize_mul = scalar_mul #Usize
-let u8_mul = scalar_mul #U8
-let u16_mul = scalar_mul #U16
-let u32_mul = scalar_mul #U32
-let u64_mul = scalar_mul #U64
-let u128_mul = scalar_mul #U128
-
-/// Xor
-let u8_xor = scalar_xor #U8
-let u16_xor = scalar_xor #U16
-let u32_xor = scalar_xor #U32
-let u64_xor = scalar_xor #U64
-let u128_xor = scalar_xor #U128
-let usize_xor = scalar_xor #Usize
-let i8_xor = scalar_xor #I8
-let i16_xor = scalar_xor #I16
-let i32_xor = scalar_xor #I32
-let i64_xor = scalar_xor #I64
-let i128_xor = scalar_xor #I128
-let isize_xor = scalar_xor #Isize
-
-/// Or
-let u8_or = scalar_or #U8
-let u16_or = scalar_or #U16
-let u32_or = scalar_or #U32
-let u64_or = scalar_or #U64
-let u128_or = scalar_or #U128
-let usize_or = scalar_or #Usize
-let i8_or = scalar_or #I8
-let i16_or = scalar_or #I16
-let i32_or = scalar_or #I32
-let i64_or = scalar_or #I64
-let i128_or = scalar_or #I128
-let isize_or = scalar_or #Isize
-
-/// And
-let u8_and = scalar_and #U8
-let u16_and = scalar_and #U16
-let u32_and = scalar_and #U32
-let u64_and = scalar_and #U64
-let u128_and = scalar_and #U128
-let usize_and = scalar_and #Usize
-let i8_and = scalar_and #I8
-let i16_and = scalar_and #I16
-let i32_and = scalar_and #I32
-let i64_and = scalar_and #I64
-let i128_and = scalar_and #I128
-let isize_and = scalar_and #Isize
-
-/// Shift left
-let u8_shl #ty = scalar_shl #U8 #ty
-let u16_shl #ty = scalar_shl #U16 #ty
-let u32_shl #ty = scalar_shl #U32 #ty
-let u64_shl #ty = scalar_shl #U64 #ty
-let u128_shl #ty = scalar_shl #U128 #ty
-let usize_shl #ty = scalar_shl #Usize #ty
-let i8_shl #ty = scalar_shl #I8 #ty
-let i16_shl #ty = scalar_shl #I16 #ty
-let i32_shl #ty = scalar_shl #I32 #ty
-let i64_shl #ty = scalar_shl #I64 #ty
-let i128_shl #ty = scalar_shl #I128 #ty
-let isize_shl #ty = scalar_shl #Isize #ty
-
-/// Shift right
-let u8_shr #ty = scalar_shr #U8 #ty
-let u16_shr #ty = scalar_shr #U16 #ty
-let u32_shr #ty = scalar_shr #U32 #ty
-let u64_shr #ty = scalar_shr #U64 #ty
-let u128_shr #ty = scalar_shr #U128 #ty
-let usize_shr #ty = scalar_shr #Usize #ty
-let i8_shr #ty = scalar_shr #I8 #ty
-let i16_shr #ty = scalar_shr #I16 #ty
-let i32_shr #ty = scalar_shr #I32 #ty
-let i64_shr #ty = scalar_shr #I64 #ty
-let i128_shr #ty = scalar_shr #I128 #ty
-let isize_shr #ty = scalar_shr #Isize #ty
-
-(*** core::ops *)
-
-// Trait declaration: [core::ops::index::Index]
-noeq type core_ops_index_Index (self idx : Type0) = {
- output : Type0;
- index : self → idx → result output
-}
-
-// Trait declaration: [core::ops::index::IndexMut]
-noeq type core_ops_index_IndexMut (self idx : Type0) = {
- indexInst : core_ops_index_Index self idx;
- index_mut : self → idx → result indexInst.output;
- index_mut_back : self → idx → indexInst.output → result self;
-}
-
-// Trait declaration [core::ops::deref::Deref]
-noeq type core_ops_deref_Deref (self : Type0) = {
- target : Type0;
- deref : self → result target;
-}
-
-// Trait declaration [core::ops::deref::DerefMut]
-noeq type core_ops_deref_DerefMut (self : Type0) = {
- derefInst : core_ops_deref_Deref self;
- deref_mut : self → result derefInst.target;
- deref_mut_back : self → derefInst.target → result self;
-}
-
-type core_ops_range_Range (a : Type0) = {
- start : a;
- end_ : a;
-}
-
-(*** [alloc] *)
-
-let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Return x
-let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result t = Return x
-let alloc_boxed_Box_deref_mut_back (t : Type) (_ : t) (x : t) : result t = Return x
-
-// Trait instance
-let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = {
- target = self;
- deref = alloc_boxed_Box_deref self;
-}
-
-// Trait instance
-let alloc_boxed_Box_coreopsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = {
- derefInst = alloc_boxed_Box_coreopsDerefInst self;
- deref_mut = alloc_boxed_Box_deref_mut self;
- deref_mut_back = alloc_boxed_Box_deref_mut_back self;
-}
-
-(*** Array *)
-type array (a : Type0) (n : usize) = s:list a{length s = n}
-
-// We tried putting the normalize_term condition as a refinement on the list
-// but it didn't work. It works with the requires clause.
-let mk_array (a : Type0) (n : usize)
- (l : list a) :
- Pure (array a n)
- (requires (normalize_term(FStar.List.Tot.length l) = n))
- (ensures (fun _ -> True)) =
- normalize_term_spec (FStar.List.Tot.length l);
- l
-
-let array_index_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : result a =
- if i < length x then Return (index x i)
- else Fail Failure
-
-let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) =
- if i < length x then Return (list_update x i nx)
- else Fail Failure
-
-(*** Slice *)
-type slice (a : Type0) = s:list a{length s <= usize_max}
-
-let slice_len (a : Type0) (s : slice a) : usize = length s
-
-let slice_index_usize (a : Type0) (x : slice a) (i : usize) : result a =
- if i < length x then Return (index x i)
- else Fail Failure
-
-let slice_update_usize (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) =
- if i < length x then Return (list_update x i nx)
- else Fail Failure
-
-(*** Subslices *)
-
-let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
-let array_from_slice (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) =
- if length s = n then Return s
- else Fail Failure
-
-// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *)
-let array_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) : result (slice a) =
- admit()
-
-let array_update_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) (ns : slice a) : result (array a n) =
- admit()
-
-let array_repeat (a : Type0) (n : usize) (x : a) : array a n =
- admit()
-
-let slice_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) : result (slice a) =
- admit()
-
-let slice_update_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) (ns : slice a) : result (slice a) =
- admit()
-
-(*** Vector *)
-type alloc_vec_Vec (a : Type0) = v:list a{length v <= usize_max}
-
-let alloc_vec_Vec_new (a : Type0) : alloc_vec_Vec a = assert_norm(length #a [] == 0); []
-let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v
-
-// Helper
-let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a =
- if i < length v then Return (index v i) else Fail Failure
-// Helper
-let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
- if i < length v then Return (list_update v i x) else Fail Failure
-
-// The **forward** function shouldn't be used
-let alloc_vec_Vec_push_fwd (a : Type0) (v : alloc_vec_Vec a) (x : a) : unit = ()
-let alloc_vec_Vec_push (a : Type0) (v : alloc_vec_Vec a) (x : a) :
- Pure (result (alloc_vec_Vec a))
- (requires True)
- (ensures (fun res ->
- match res with
- | Fail e -> e == Failure
- | Return v' -> length v' = length v + 1)) =
- if length v < usize_max then begin
- (**) assert_norm(length [x] == 1);
- (**) append_length v [x];
- (**) assert(length (append v [x]) = length v + 1);
- Return (append v [x])
- end
- else Fail Failure
-
-// The **forward** function shouldn't be used
-let alloc_vec_Vec_insert_fwd (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result unit =
- if i < length v then Return () else Fail Failure
-let alloc_vec_Vec_insert (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
- if i < length v then Return (list_update v i x) else Fail Failure
-
-// Trait declaration: [core::slice::index::private_slice_index::Sealed]
-type core_slice_index_private_slice_index_Sealed (self : Type0) = unit
-
-// Trait declaration: [core::slice::index::SliceIndex]
-noeq type core_slice_index_SliceIndex (self t : Type0) = {
- sealedInst : core_slice_index_private_slice_index_Sealed self;
- output : Type0;
- get : self → t → result (option output);
- get_mut : self → t → result (option output);
- get_mut_back : self → t → option output → result t;
- get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output);
- get_unchecked_mut : self → mut_raw_ptr t → result (mut_raw_ptr output);
- index : self → t → result output;
- index_mut : self → t → result output;
- index_mut_back : self → t → output → result t;
-}
-
-// [core::slice::index::[T]::index]: forward function
-let core_slice_index_Slice_index
- (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
- (s : slice t) (i : idx) : result inst.output =
- let* x = inst.get i s in
- match x with
- | None -> Fail Failure
- | Some x -> Return x
-
-// [core::slice::index::Range:::get]: forward function
-let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) :
- result (option (slice t)) =
- admit () // TODO
-
-// [core::slice::index::Range::get_mut]: forward function
-let core_slice_index_RangeUsize_get_mut
- (t : Type0) : core_ops_range_Range usize → slice t → result (option (slice t)) =
- admit () // TODO
-
-// [core::slice::index::Range::get_mut]: backward function 0
-let core_slice_index_RangeUsize_get_mut_back
- (t : Type0) :
- core_ops_range_Range usize → slice t → option (slice t) → result (slice t) =
- admit () // TODO
-
-// [core::slice::index::Range::get_unchecked]: forward function
-let core_slice_index_RangeUsize_get_unchecked
- (t : Type0) :
- core_ops_range_Range usize → const_raw_ptr (slice t) → result (const_raw_ptr (slice t)) =
- // Don't know what the model should be - for now we always fail to make
- // sure code which uses it fails
- fun _ _ -> Fail Failure
-
-// [core::slice::index::Range::get_unchecked_mut]: forward function
-let core_slice_index_RangeUsize_get_unchecked_mut
- (t : Type0) :
- core_ops_range_Range usize → mut_raw_ptr (slice t) → result (mut_raw_ptr (slice t)) =
- // Don't know what the model should be - for now we always fail to make
- // sure code which uses it fails
- fun _ _ -> Fail Failure
-
-// [core::slice::index::Range::index]: forward function
-let core_slice_index_RangeUsize_index
- (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) =
- admit () // TODO
-
-// [core::slice::index::Range::index_mut]: forward function
-let core_slice_index_RangeUsize_index_mut
- (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) =
- admit () // TODO
-
-// [core::slice::index::Range::index_mut]: backward function 0
-let core_slice_index_RangeUsize_index_mut_back
- (t : Type0) : core_ops_range_Range usize → slice t → slice t → result (slice t) =
- admit () // TODO
-
-// [core::slice::index::[T]::index_mut]: forward function
-let core_slice_index_Slice_index_mut
- (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
- slice t → idx → result inst.output =
- admit () //
-
-// [core::slice::index::[T]::index_mut]: backward function 0
-let core_slice_index_Slice_index_mut_back
- (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
- slice t → idx → inst.output → result (slice t) =
- admit () // TODO
-
-// [core::array::[T; N]::index]: forward function
-let core_array_Array_index
- (t idx : Type0) (n : usize) (inst : core_ops_index_Index (slice t) idx)
- (a : array t n) (i : idx) : result inst.output =
- admit () // TODO
-
-// [core::array::[T; N]::index_mut]: forward function
-let core_array_Array_index_mut
- (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
- (a : array t n) (i : idx) : result inst.indexInst.output =
- admit () // TODO
-
-// [core::array::[T; N]::index_mut]: backward function 0
-let core_array_Array_index_mut_back
- (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
- (a : array t n) (i : idx) (x : inst.indexInst.output) : result (array t n) =
- admit () // TODO
-
-// Trait implementation: [core::slice::index::private_slice_index::Range]
-let core_slice_index_private_slice_index_SealedRangeUsizeInst
- : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = ()
-
-// Trait implementation: [core::slice::index::Range]
-let core_slice_index_SliceIndexRangeUsizeSliceTInst (t : Type0) :
- core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) = {
- sealedInst = core_slice_index_private_slice_index_SealedRangeUsizeInst;
- output = slice t;
- get = core_slice_index_RangeUsize_get t;
- get_mut = core_slice_index_RangeUsize_get_mut t;
- get_mut_back = core_slice_index_RangeUsize_get_mut_back t;
- get_unchecked = core_slice_index_RangeUsize_get_unchecked t;
- get_unchecked_mut = core_slice_index_RangeUsize_get_unchecked_mut t;
- index = core_slice_index_RangeUsize_index t;
- index_mut = core_slice_index_RangeUsize_index_mut t;
- index_mut_back = core_slice_index_RangeUsize_index_mut_back t;
-}
-
-// Trait implementation: [core::slice::index::[T]]
-let core_ops_index_IndexSliceTIInst (t idx : Type0)
- (inst : core_slice_index_SliceIndex idx (slice t)) :
- core_ops_index_Index (slice t) idx = {
- output = inst.output;
- index = core_slice_index_Slice_index t idx inst;
-}
-
-// Trait implementation: [core::slice::index::[T]]
-let core_ops_index_IndexMutSliceTIInst (t idx : Type0)
- (inst : core_slice_index_SliceIndex idx (slice t)) :
- core_ops_index_IndexMut (slice t) idx = {
- indexInst = core_ops_index_IndexSliceTIInst t idx inst;
- index_mut = core_slice_index_Slice_index_mut t idx inst;
- index_mut_back = core_slice_index_Slice_index_mut_back t idx inst;
-}
-
-// Trait implementation: [core::array::[T; N]]
-let core_ops_index_IndexArrayInst (t idx : Type0) (n : usize)
- (inst : core_ops_index_Index (slice t) idx) :
- core_ops_index_Index (array t n) idx = {
- output = inst.output;
- index = core_array_Array_index t idx n inst;
-}
-
-// Trait implementation: [core::array::[T; N]]
-let core_ops_index_IndexMutArrayIInst (t idx : Type0) (n : usize)
- (inst : core_ops_index_IndexMut (slice t) idx) :
- core_ops_index_IndexMut (array t n) idx = {
- indexInst = core_ops_index_IndexArrayInst t idx n inst.indexInst;
- index_mut = core_array_Array_index_mut t idx n inst;
- index_mut_back = core_array_Array_index_mut_back t idx n inst;
-}
-
-// [core::slice::index::usize::get]: forward function
-let core_slice_index_usize_get
- (t : Type0) : usize → slice t → result (option t) =
- admit () // TODO
-
-// [core::slice::index::usize::get_mut]: forward function
-let core_slice_index_usize_get_mut
- (t : Type0) : usize → slice t → result (option t) =
- admit () // TODO
-
-// [core::slice::index::usize::get_mut]: backward function 0
-let core_slice_index_usize_get_mut_back
- (t : Type0) : usize → slice t → option t → result (slice t) =
- admit () // TODO
-
-// [core::slice::index::usize::get_unchecked]: forward function
-let core_slice_index_usize_get_unchecked
- (t : Type0) : usize → const_raw_ptr (slice t) → result (const_raw_ptr t) =
- admit () // TODO
-
-// [core::slice::index::usize::get_unchecked_mut]: forward function
-let core_slice_index_usize_get_unchecked_mut
- (t : Type0) : usize → mut_raw_ptr (slice t) → result (mut_raw_ptr t) =
- admit () // TODO
-
-// [core::slice::index::usize::index]: forward function
-let core_slice_index_usize_index (t : Type0) : usize → slice t → result t =
- admit () // TODO
-
-// [core::slice::index::usize::index_mut]: forward function
-let core_slice_index_usize_index_mut (t : Type0) : usize → slice t → result t =
- admit () // TODO
-
-// [core::slice::index::usize::index_mut]: backward function 0
-let core_slice_index_usize_index_mut_back
- (t : Type0) : usize → slice t → t → result (slice t) =
- admit () // TODO
-
-// Trait implementation: [core::slice::index::private_slice_index::usize]
-let core_slice_index_private_slice_index_SealedUsizeInst
- : core_slice_index_private_slice_index_Sealed usize = ()
-
-// Trait implementation: [core::slice::index::usize]
-let core_slice_index_SliceIndexUsizeSliceTInst (t : Type0) :
- core_slice_index_SliceIndex usize (slice t) = {
- sealedInst = core_slice_index_private_slice_index_SealedUsizeInst;
- output = t;
- get = core_slice_index_usize_get t;
- get_mut = core_slice_index_usize_get_mut t;
- get_mut_back = core_slice_index_usize_get_mut_back t;
- get_unchecked = core_slice_index_usize_get_unchecked t;
- get_unchecked_mut = core_slice_index_usize_get_unchecked_mut t;
- index = core_slice_index_usize_index t;
- index_mut = core_slice_index_usize_index_mut t;
- index_mut_back = core_slice_index_usize_index_mut_back t;
-}
-
-// [alloc::vec::Vec::index]: forward function
-let alloc_vec_Vec_index (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
- (self : alloc_vec_Vec t) (i : idx) : result inst.output =
- admit () // TODO
-
-// [alloc::vec::Vec::index_mut]: forward function
-let alloc_vec_Vec_index_mut (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
- (self : alloc_vec_Vec t) (i : idx) : result inst.output =
- admit () // TODO
-
-// [alloc::vec::Vec::index_mut]: backward function 0
-let alloc_vec_Vec_index_mut_back
- (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
- (self : alloc_vec_Vec t) (i : idx) (x : inst.output) : result (alloc_vec_Vec t) =
- admit () // TODO
-
-// Trait implementation: [alloc::vec::Vec]
-let alloc_vec_Vec_coreopsindexIndexInst (t idx : Type0)
- (inst : core_slice_index_SliceIndex idx (slice t)) :
- core_ops_index_Index (alloc_vec_Vec t) idx = {
- output = inst.output;
- index = alloc_vec_Vec_index t idx inst;
-}
-
-// Trait implementation: [alloc::vec::Vec]
-let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
- (inst : core_slice_index_SliceIndex idx (slice t)) :
- core_ops_index_IndexMut (alloc_vec_Vec t) idx = {
- indexInst = alloc_vec_Vec_coreopsindexIndexInst t idx inst;
- index_mut = alloc_vec_Vec_index_mut t idx inst;
- index_mut_back = alloc_vec_Vec_index_mut_back t idx inst;
-}
-
-(*** Theorems *)
-
-let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
- Lemma (
- alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
- alloc_vec_Vec_index_usize v i)
- [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
- =
- admit()
-
-let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
- Lemma (
- alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
- alloc_vec_Vec_index_usize v i)
- [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
- =
- admit()
-
-let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) :
- Lemma (
- alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x ==
- alloc_vec_Vec_update_usize v i x)
- [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x)]
- =
- admit()
diff --git a/tests/fstar-split/traits/Traits.fst b/tests/fstar-split/traits/Traits.fst
deleted file mode 100644
index a815406f..00000000
--- a/tests/fstar-split/traits/Traits.fst
+++ /dev/null
@@ -1,468 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [traits] *)
-module Traits
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** Trait declaration: [traits::BoolTrait]
- Source: 'src/traits.rs', lines 1:0-1:19 *)
-noeq type boolTrait_t (self : Type0) = { get_bool : self -> result bool; }
-
-(** [traits::{bool}::get_bool]: forward function
- Source: 'src/traits.rs', lines 12:4-12:30 *)
-let bool_get_bool (self : bool) : result bool =
- Return self
-
-(** Trait implementation: [traits::{bool}]
- Source: 'src/traits.rs', lines 11:0-11:23 *)
-let traits_BoolTraitBoolInst : boolTrait_t bool = { get_bool = bool_get_bool; }
-
-(** [traits::BoolTrait::ret_true]: forward function
- Source: 'src/traits.rs', lines 6:4-6:30 *)
-let boolTrait_ret_true
- (#self : Type0) (self_clause : boolTrait_t self) (self1 : self) :
- result bool
- =
- Return true
-
-(** [traits::test_bool_trait_bool]: forward function
- Source: 'src/traits.rs', lines 17:0-17:44 *)
-let test_bool_trait_bool (x : bool) : result bool =
- let* b = bool_get_bool x in
- if b then boolTrait_ret_true traits_BoolTraitBoolInst x else Return false
-
-(** [traits::{core::option::Option<T>#1}::get_bool]: forward function
- Source: 'src/traits.rs', lines 23:4-23:30 *)
-let option_get_bool (t : Type0) (self : option t) : result bool =
- begin match self with | None -> Return false | Some _ -> Return true end
-
-(** Trait implementation: [traits::{core::option::Option<T>#1}]
- Source: 'src/traits.rs', lines 22:0-22:31 *)
-let traits_BoolTraitcoreoptionOptionTInst (t : Type0) : boolTrait_t (option t)
- = {
- get_bool = option_get_bool t;
-}
-
-(** [traits::test_bool_trait_option]: forward function
- Source: 'src/traits.rs', lines 31:0-31:54 *)
-let test_bool_trait_option (t : Type0) (x : option t) : result bool =
- let* b = option_get_bool t x in
- if b
- then boolTrait_ret_true (traits_BoolTraitcoreoptionOptionTInst t) x
- else Return false
-
-(** [traits::test_bool_trait]: forward function
- Source: 'src/traits.rs', lines 35:0-35:50 *)
-let test_bool_trait
- (t : Type0) (boolTraitTInst : boolTrait_t t) (x : t) : result bool =
- boolTraitTInst.get_bool x
-
-(** Trait declaration: [traits::ToU64]
- Source: 'src/traits.rs', lines 39:0-39:15 *)
-noeq type toU64_t (self : Type0) = { to_u64 : self -> result u64; }
-
-(** [traits::{u64#2}::to_u64]: forward function
- Source: 'src/traits.rs', lines 44:4-44:26 *)
-let u64_to_u64 (self : u64) : result u64 =
- Return self
-
-(** Trait implementation: [traits::{u64#2}]
- Source: 'src/traits.rs', lines 43:0-43:18 *)
-let traits_ToU64U64Inst : toU64_t u64 = { to_u64 = u64_to_u64; }
-
-(** [traits::{(A, A)#3}::to_u64]: forward function
- Source: 'src/traits.rs', lines 50:4-50:26 *)
-let pair_to_u64
- (a : Type0) (toU64AInst : toU64_t a) (self : (a & a)) : result u64 =
- let (x, x1) = self in
- let* i = toU64AInst.to_u64 x in
- let* i1 = toU64AInst.to_u64 x1 in
- u64_add i i1
-
-(** Trait implementation: [traits::{(A, A)#3}]
- Source: 'src/traits.rs', lines 49:0-49:31 *)
-let traits_ToU64TupleAAInst (a : Type0) (toU64AInst : toU64_t a) : toU64_t (a &
- a) = {
- to_u64 = pair_to_u64 a toU64AInst;
-}
-
-(** [traits::f]: forward function
- Source: 'src/traits.rs', lines 55:0-55:36 *)
-let f (t : Type0) (toU64TInst : toU64_t t) (x : (t & t)) : result u64 =
- pair_to_u64 t toU64TInst x
-
-(** [traits::g]: forward function
- Source: 'src/traits.rs', lines 59:0-61:18 *)
-let g
- (t : Type0) (toU64TupleTTInst : toU64_t (t & t)) (x : (t & t)) : result u64 =
- toU64TupleTTInst.to_u64 x
-
-(** [traits::h0]: forward function
- Source: 'src/traits.rs', lines 66:0-66:24 *)
-let h0 (x : u64) : result u64 =
- u64_to_u64 x
-
-(** [traits::Wrapper]
- Source: 'src/traits.rs', lines 70:0-70:21 *)
-type wrapper_t (t : Type0) = { x : t; }
-
-(** [traits::{traits::Wrapper<T>#4}::to_u64]: forward function
- Source: 'src/traits.rs', lines 75:4-75:26 *)
-let wrapper_to_u64
- (t : Type0) (toU64TInst : toU64_t t) (self : wrapper_t t) : result u64 =
- toU64TInst.to_u64 self.x
-
-(** Trait implementation: [traits::{traits::Wrapper<T>#4}]
- Source: 'src/traits.rs', lines 74:0-74:35 *)
-let traits_ToU64traitsWrapperTInst (t : Type0) (toU64TInst : toU64_t t) :
- toU64_t (wrapper_t t) = {
- to_u64 = wrapper_to_u64 t toU64TInst;
-}
-
-(** [traits::h1]: forward function
- Source: 'src/traits.rs', lines 80:0-80:33 *)
-let h1 (x : wrapper_t u64) : result u64 =
- wrapper_to_u64 u64 traits_ToU64U64Inst x
-
-(** [traits::h2]: forward function
- Source: 'src/traits.rs', lines 84:0-84:41 *)
-let h2 (t : Type0) (toU64TInst : toU64_t t) (x : wrapper_t t) : result u64 =
- wrapper_to_u64 t toU64TInst x
-
-(** Trait declaration: [traits::ToType]
- Source: 'src/traits.rs', lines 88:0-88:19 *)
-noeq type toType_t (self t : Type0) = { to_type : self -> result t; }
-
-(** [traits::{u64#5}::to_type]: forward function
- Source: 'src/traits.rs', lines 93:4-93:28 *)
-let u64_to_type (self : u64) : result bool =
- Return (self > 0)
-
-(** Trait implementation: [traits::{u64#5}]
- Source: 'src/traits.rs', lines 92:0-92:25 *)
-let traits_ToTypeU64BoolInst : toType_t u64 bool = { to_type = u64_to_type; }
-
-(** Trait declaration: [traits::OfType]
- Source: 'src/traits.rs', lines 98:0-98:16 *)
-noeq type ofType_t (self : Type0) = {
- of_type : (t : Type0) -> (toTypeTSelfInst : toType_t t self) -> t -> result
- self;
-}
-
-(** [traits::h3]: forward function
- Source: 'src/traits.rs', lines 104:0-104:50 *)
-let h3
- (t1 t2 : Type0) (ofTypeT1Inst : ofType_t t1) (toTypeT2T1Inst : toType_t t2
- t1) (y : t2) :
- result t1
- =
- ofTypeT1Inst.of_type t2 toTypeT2T1Inst y
-
-(** Trait declaration: [traits::OfTypeBis]
- Source: 'src/traits.rs', lines 109:0-109:36 *)
-noeq type ofTypeBis_t (self t : Type0) = {
- toTypeTSelfInst : toType_t t self;
- of_type : t -> result self;
-}
-
-(** [traits::h4]: forward function
- Source: 'src/traits.rs', lines 118:0-118:57 *)
-let h4
- (t1 t2 : Type0) (ofTypeBisT1T2Inst : ofTypeBis_t t1 t2) (toTypeT2T1Inst :
- toType_t t2 t1) (y : t2) :
- result t1
- =
- ofTypeBisT1T2Inst.of_type y
-
-(** [traits::TestType]
- Source: 'src/traits.rs', lines 122:0-122:22 *)
-type testType_t (t : Type0) = t
-
-(** [traits::{traits::TestType<T>#6}::test::TestType1]
- Source: 'src/traits.rs', lines 127:8-127:24 *)
-type testType_test_TestType1_t = u64
-
-(** Trait declaration: [traits::{traits::TestType<T>#6}::test::TestTrait]
- Source: 'src/traits.rs', lines 128:8-128:23 *)
-noeq type testType_test_TestTrait_t (self : Type0) = {
- test : self -> result bool;
-}
-
-(** [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}::test]: forward function
- Source: 'src/traits.rs', lines 139:12-139:34 *)
-let testType_test_TestType1_test
- (self : testType_test_TestType1_t) : result bool =
- Return (self > 1)
-
-(** Trait implementation: [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}]
- Source: 'src/traits.rs', lines 138:8-138:36 *)
-let traits_TestType_test_TestTraittraitstraitsTestTypeTtestTestType1Inst :
- testType_test_TestTrait_t testType_test_TestType1_t = {
- test = testType_test_TestType1_test;
-}
-
-(** [traits::{traits::TestType<T>#6}::test]: forward function
- Source: 'src/traits.rs', lines 126:4-126:36 *)
-let testType_test
- (t : Type0) (toU64TInst : toU64_t t) (self : testType_t t) (x : t) :
- result bool
- =
- let* x1 = toU64TInst.to_u64 x in
- if x1 > 0 then testType_test_TestType1_test 0 else Return false
-
-(** [traits::BoolWrapper]
- Source: 'src/traits.rs', lines 150:0-150:22 *)
-type boolWrapper_t = bool
-
-(** [traits::{traits::BoolWrapper#7}::to_type]: forward function
- Source: 'src/traits.rs', lines 156:4-156:25 *)
-let boolWrapper_to_type
- (t : Type0) (toTypeBoolTInst : toType_t bool t) (self : boolWrapper_t) :
- result t
- =
- toTypeBoolTInst.to_type self
-
-(** Trait implementation: [traits::{traits::BoolWrapper#7}]
- Source: 'src/traits.rs', lines 152:0-152:33 *)
-let traits_ToTypetraitsBoolWrapperTInst (t : Type0) (toTypeBoolTInst : toType_t
- bool t) : toType_t boolWrapper_t t = {
- to_type = boolWrapper_to_type t toTypeBoolTInst;
-}
-
-(** [traits::WithConstTy::LEN2]
- Source: 'src/traits.rs', lines 164:4-164:21 *)
-let with_const_ty_len2_body : result usize = Return 32
-let with_const_ty_len2_c : usize = eval_global with_const_ty_len2_body
-
-(** Trait declaration: [traits::WithConstTy]
- Source: 'src/traits.rs', lines 161:0-161:39 *)
-noeq type withConstTy_t (self : Type0) (len : usize) = {
- cLEN1 : usize;
- cLEN2 : usize;
- tV : Type0;
- tW : Type0;
- tW_clause_0 : toU64_t tW;
- f : tW -> array u8 len -> result tW;
-}
-
-(** [traits::{bool#8}::LEN1]
- Source: 'src/traits.rs', lines 175:4-175:21 *)
-let bool_len1_body : result usize = Return 12
-let bool_len1_c : usize = eval_global bool_len1_body
-
-(** [traits::{bool#8}::f]: merged forward/backward function
- (there is a single backward function, and the forward function returns ())
- Source: 'src/traits.rs', lines 180:4-180:39 *)
-let bool_f (i : u64) (a : array u8 32) : result u64 =
- Return i
-
-(** Trait implementation: [traits::{bool#8}]
- Source: 'src/traits.rs', lines 174:0-174:29 *)
-let traits_WithConstTyBool32Inst : withConstTy_t bool 32 = {
- cLEN1 = bool_len1_c;
- cLEN2 = with_const_ty_len2_c;
- tV = u8;
- tW = u64;
- tW_clause_0 = traits_ToU64U64Inst;
- f = bool_f;
-}
-
-(** [traits::use_with_const_ty1]: forward function
- Source: 'src/traits.rs', lines 183:0-183:75 *)
-let use_with_const_ty1
- (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len) :
- result usize
- =
- Return withConstTyHLENInst.cLEN1
-
-(** [traits::use_with_const_ty2]: forward function
- Source: 'src/traits.rs', lines 187:0-187:73 *)
-let use_with_const_ty2
- (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len)
- (w : withConstTyHLENInst.tW) :
- result unit
- =
- Return ()
-
-(** [traits::use_with_const_ty3]: forward function
- Source: 'src/traits.rs', lines 189:0-189:80 *)
-let use_with_const_ty3
- (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len)
- (x : withConstTyHLENInst.tW) :
- result u64
- =
- withConstTyHLENInst.tW_clause_0.to_u64 x
-
-(** [traits::test_where1]: forward function
- Source: 'src/traits.rs', lines 193:0-193:40 *)
-let test_where1 (t : Type0) (_x : t) : result unit =
- Return ()
-
-(** [traits::test_where2]: forward function
- Source: 'src/traits.rs', lines 194:0-194:57 *)
-let test_where2
- (t : Type0) (withConstTyT32Inst : withConstTy_t t 32) (_x : u32) :
- result unit
- =
- Return ()
-
-(** Trait declaration: [traits::ParentTrait0]
- Source: 'src/traits.rs', lines 200:0-200:22 *)
-noeq type parentTrait0_t (self : Type0) = {
- tW : Type0;
- get_name : self -> result string;
- get_w : self -> result tW;
-}
-
-(** Trait declaration: [traits::ParentTrait1]
- Source: 'src/traits.rs', lines 205:0-205:22 *)
-type parentTrait1_t (self : Type0) = unit
-
-(** Trait declaration: [traits::ChildTrait]
- Source: 'src/traits.rs', lines 206:0-206:49 *)
-noeq type childTrait_t (self : Type0) = {
- parentTrait0SelfInst : parentTrait0_t self;
- parentTrait1SelfInst : parentTrait1_t self;
-}
-
-(** [traits::test_child_trait1]: forward function
- Source: 'src/traits.rs', lines 209:0-209:56 *)
-let test_child_trait1
- (t : Type0) (childTraitTInst : childTrait_t t) (x : t) : result string =
- childTraitTInst.parentTrait0SelfInst.get_name x
-
-(** [traits::test_child_trait2]: forward function
- Source: 'src/traits.rs', lines 213:0-213:54 *)
-let test_child_trait2
- (t : Type0) (childTraitTInst : childTrait_t t) (x : t) :
- result childTraitTInst.parentTrait0SelfInst.tW
- =
- childTraitTInst.parentTrait0SelfInst.get_w x
-
-(** [traits::order1]: forward function
- Source: 'src/traits.rs', lines 219:0-219:59 *)
-let order1
- (t u : Type0) (parentTrait0TInst : parentTrait0_t t) (parentTrait0UInst :
- parentTrait0_t u) :
- result unit
- =
- Return ()
-
-(** Trait declaration: [traits::ChildTrait1]
- Source: 'src/traits.rs', lines 222:0-222:35 *)
-noeq type childTrait1_t (self : Type0) = {
- parentTrait1SelfInst : parentTrait1_t self;
-}
-
-(** Trait implementation: [traits::{usize#9}]
- Source: 'src/traits.rs', lines 224:0-224:27 *)
-let traits_ParentTrait1UsizeInst : parentTrait1_t usize = ()
-
-(** Trait implementation: [traits::{usize#10}]
- Source: 'src/traits.rs', lines 225:0-225:26 *)
-let traits_ChildTrait1UsizeInst : childTrait1_t usize = {
- parentTrait1SelfInst = traits_ParentTrait1UsizeInst;
-}
-
-(** Trait declaration: [traits::Iterator]
- Source: 'src/traits.rs', lines 229:0-229:18 *)
-noeq type iterator_t (self : Type0) = { tItem : Type0; }
-
-(** Trait declaration: [traits::IntoIterator]
- Source: 'src/traits.rs', lines 233:0-233:22 *)
-noeq type intoIterator_t (self : Type0) = {
- tItem : Type0;
- tIntoIter : Type0;
- tIntoIter_clause_0 : iterator_t tIntoIter;
- into_iter : self -> result tIntoIter;
-}
-
-(** Trait declaration: [traits::FromResidual]
- Source: 'src/traits.rs', lines 250:0-250:21 *)
-type fromResidual_t (self t : Type0) = unit
-
-(** Trait declaration: [traits::Try]
- Source: 'src/traits.rs', lines 246:0-246:48 *)
-noeq type try_t (self : Type0) = {
- tResidual : Type0;
- fromResidualSelftraitsTrySelfResidualInst : fromResidual_t self tResidual;
-}
-
-(** Trait declaration: [traits::WithTarget]
- Source: 'src/traits.rs', lines 252:0-252:20 *)
-noeq type withTarget_t (self : Type0) = { tTarget : Type0; }
-
-(** Trait declaration: [traits::ParentTrait2]
- Source: 'src/traits.rs', lines 256:0-256:22 *)
-noeq type parentTrait2_t (self : Type0) = {
- tU : Type0;
- tU_clause_0 : withTarget_t tU;
-}
-
-(** Trait declaration: [traits::ChildTrait2]
- Source: 'src/traits.rs', lines 260:0-260:35 *)
-noeq type childTrait2_t (self : Type0) = {
- parentTrait2SelfInst : parentTrait2_t self;
- convert : parentTrait2SelfInst.tU -> result
- parentTrait2SelfInst.tU_clause_0.tTarget;
-}
-
-(** Trait implementation: [traits::{u32#11}]
- Source: 'src/traits.rs', lines 264:0-264:23 *)
-let traits_WithTargetU32Inst : withTarget_t u32 = { tTarget = u32; }
-
-(** Trait implementation: [traits::{u32#12}]
- Source: 'src/traits.rs', lines 268:0-268:25 *)
-let traits_ParentTrait2U32Inst : parentTrait2_t u32 = {
- tU = u32;
- tU_clause_0 = traits_WithTargetU32Inst;
-}
-
-(** [traits::{u32#13}::convert]: forward function
- Source: 'src/traits.rs', lines 273:4-273:29 *)
-let u32_convert (x : u32) : result u32 =
- Return x
-
-(** Trait implementation: [traits::{u32#13}]
- Source: 'src/traits.rs', lines 272:0-272:24 *)
-let traits_ChildTrait2U32Inst : childTrait2_t u32 = {
- parentTrait2SelfInst = traits_ParentTrait2U32Inst;
- convert = u32_convert;
-}
-
-(** Trait declaration: [traits::CFnOnce]
- Source: 'src/traits.rs', lines 286:0-286:23 *)
-noeq type cFnOnce_t (self args : Type0) = {
- tOutput : Type0;
- call_once : self -> args -> result tOutput;
-}
-
-(** Trait declaration: [traits::CFnMut]
- Source: 'src/traits.rs', lines 292:0-292:37 *)
-noeq type cFnMut_t (self args : Type0) = {
- cFnOnceSelfArgsInst : cFnOnce_t self args;
- call_mut : self -> args -> result cFnOnceSelfArgsInst.tOutput;
- call_mut_back : self -> args -> result self;
-}
-
-(** Trait declaration: [traits::CFn]
- Source: 'src/traits.rs', lines 296:0-296:33 *)
-noeq type cFn_t (self args : Type0) = {
- cFnMutSelfArgsInst : cFnMut_t self args;
- call : self -> args -> result cFnMutSelfArgsInst.cFnOnceSelfArgsInst.tOutput;
-}
-
-(** Trait declaration: [traits::GetTrait]
- Source: 'src/traits.rs', lines 300:0-300:18 *)
-noeq type getTrait_t (self : Type0) = { tW : Type0; get_w : self -> result tW;
-}
-
-(** [traits::test_get_trait]: forward function
- Source: 'src/traits.rs', lines 305:0-305:49 *)
-let test_get_trait
- (t : Type0) (getTraitTInst : getTrait_t t) (x : t) :
- result getTraitTInst.tW
- =
- getTraitTInst.get_w x
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 18:00:55 +0000