From c8fce0c24f2f5331f2f1135cc17d45192f2b30e3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 6 Nov 2023 18:49:27 +0100
Subject: Regenerate part of the trait tests for Lean

---
 tests/lean/Traits/Funs.lean  | 35 ++++++++++++++++++++-------------
 tests/lean/Traits/Types.lean | 46 +++++++++++++++++++++++++++++++++++++++++---
 2 files changed, 65 insertions(+), 16 deletions(-)

(limited to 'tests/lean/Traits')

diff --git a/tests/lean/Traits/Funs.lean b/tests/lean/Traits/Funs.lean
index 52ff0c0a..156ef1e0 100644
--- a/tests/lean/Traits/Funs.lean
+++ b/tests/lean/Traits/Funs.lean
@@ -31,8 +31,8 @@ def test_bool_trait_bool (x : Bool) : Result Bool :=
 /- [traits::Option::{1}::get_bool]: forward function -/
 def Option.get_bool (T : Type) (self : Option T) : Result Bool :=
   match self with
-  | Option.none => Result.ret false
-  | Option.some t => Result.ret true
+  | none => Result.ret false
+  | some t => Result.ret true
 
 /- Trait implementation: [traits::Option::{1}] -/
 def Option.BoolTraitInst (T : Type) : BoolTrait (Option T) := {
@@ -105,7 +105,7 @@ def h2 (T : Type) (inst : ToU64 T) (x : Wrapper T) : Result U64 :=
 
 /- [traits::u64::{5}::to_type]: forward function -/
 def u64.to_type (self : U64) : Result Bool :=
-  Result.ret (self > (U64.ofInt 0))
+  Result.ret (self > 0#u64)
 
 /- Trait implementation: [traits::u64::{5}] -/
 def u64.ToTypeInst : ToType U64 Bool := {
@@ -129,7 +129,7 @@ def h4
 /- [traits::TestType::{6}::test::TestType1::{0}::test]: forward function -/
 def TestType.test.TestType1.test
   (self : TestType.test.TestType1) : Result Bool :=
-  Result.ret (self._0 > (U64.ofInt 1))
+  Result.ret (self._0 > 1#u64)
 
 /- Trait implementation: [traits::TestType::{6}::test::TestType1::{0}] -/
 def TestType.test.TestType1.TestTypetestTestTraitInst : TestType.test.TestTrait
@@ -142,8 +142,8 @@ def TestType.test
   (T : Type) (inst : ToU64 T) (self : TestType T) (x : T) : Result Bool :=
   do
     let x0 ← inst.to_u64 x
-    if x0 > (U64.ofInt 0)
-    then TestType.test.TestType1.test { _0 := (U64.ofInt 0) }
+    if x0 > 0#u64
+    then TestType.test.TestType1.test { _0 := 0#u64 }
     else Result.ret false
 
 /- [traits::BoolWrapper::{7}::to_type]: forward function -/
@@ -158,21 +158,21 @@ def BoolWrapper.ToTypeInst (T : Type) (inst : ToType Bool T) : ToType
 }
 
 /- [traits::WithConstTy::LEN2] -/
-def with_const_ty_len2_body : Result Usize := Result.ret (Usize.ofInt 32)
+def with_const_ty_len2_body : Result Usize := Result.ret 32#usize
 def with_const_ty_len2_c : Usize :=
   eval_global with_const_ty_len2_body (by simp)
 
 /- [traits::Bool::{8}::LEN1] -/
-def bool_len1_body : Result Usize := Result.ret (Usize.ofInt 12)
+def bool_len1_body : Result Usize := Result.ret 12#usize
 def bool_len1_c : Usize := eval_global bool_len1_body (by simp)
 
 /- [traits::Bool::{8}::f]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
-def Bool.f (i : U64) (a : Array U8 (Usize.ofInt 32)) : Result U64 :=
+def Bool.f (i : U64) (a : Array U8 32#usize) : Result U64 :=
   Result.ret i
 
 /- Trait implementation: [traits::Bool::{8}] -/
-def Bool.WithConstTyInst : WithConstTy Bool (Usize.ofInt 32) := {
+def Bool.WithConstTyInst : WithConstTy Bool 32#usize := {
   LEN1 := bool_len1_c
   LEN2 := with_const_ty_len2_c
   V := U8
@@ -207,9 +207,7 @@ def test_where1 (T : Type) (_x : T) : Result Unit :=
 
 /- [traits::test_where2]: forward function -/
 def test_where2
-  (T : Type) (inst : WithConstTy T (Usize.ofInt 32)) (_x : U32) :
-  Result Unit
-  :=
+  (T : Type) (inst : WithConstTy T 32#usize) (_x : U32) : Result Unit :=
   Result.ret ()
 
 /- [traits::test_child_trait1]: forward function -/
@@ -229,4 +227,15 @@ def order1
   :=
   Result.ret ()
 
+/- [traits::map_option]: forward function -/
+def map_option
+  (T F : Type) (inst : core.ops.function.Fn F T) (x : Option T) (f0 : F) :
+  Result (Option T)
+  :=
+  match x with
+  | none => Result.ret none
+  | some x0 => do
+                 let t ← inst.call f0 x0
+                 Result.ret (some t)
+
 end traits
diff --git a/tests/lean/Traits/Types.lean b/tests/lean/Traits/Types.lean
index a8c12fe5..e325da6f 100644
--- a/tests/lean/Traits/Types.lean
+++ b/tests/lean/Traits/Types.lean
@@ -27,7 +27,7 @@ structure OfType (Self : Type) where
 
 /- Trait declaration: [traits::OfTypeBis] -/
 structure OfTypeBis (Self T : Type) where
-  parent_clause_0 :ToType T Self
+  parent_clause_0 : ToType T Self
   of_type : T → Result Self
 
 /- [traits::TestType] -/
@@ -69,8 +69,8 @@ structure ParentTrait1 (Self : Type) where
 
 /- Trait declaration: [traits::ChildTrait] -/
 structure ChildTrait (Self : Type) where
-  parent_clause_0 :ParentTrait0 Self
-  parent_clause_1 :ParentTrait1 Self
+  parent_clause_0 : ParentTrait0 Self
+  parent_clause_1 : ParentTrait1 Self
 
 /- Trait declaration: [traits::Iterator] -/
 structure Iterator (Self : Type) where
@@ -83,4 +83,44 @@ structure IntoIterator (Self : Type) where
   IntoIter_clause_0 : Iterator IntoIter
   into_iter : Self → Result IntoIter
 
+/- Trait declaration: [traits::FromResidual] -/
+structure FromResidual (Self T : Type) where
+
+/- Trait declaration: [traits::Try] -/
+structure Try (Self : Type) where
+  parent_clause_0 : FromResidual Self Residual
+  Residual : Type
+
+/- Trait declaration: [traits::CFnOnce] -/
+structure CFnOnce (Self Args : Type) where
+  Output : Type
+  call_once : Self → Args → Result Output
+
+/- Trait declaration: [traits::CFnMut] -/
+structure CFnMut (Self Args : Type) where
+  parent_clause_0 : CFnOnce Self Args
+  call_mut : Self → Args → Result parent_clause_0.Output
+  call_mut_back : Self → Args → parent_clause_0.Output → Result Self
+
+/- Trait declaration: [traits::CFn] -/
+structure CFn (Self Args : Type) where
+  parent_clause_0 : CFnMut Self Args
+  call_mut : Self → Args → Result parent_clause_0.parent_clause_0.Output
+
+/- Trait declaration: [core::ops::function::FnOnce] -/
+structure core.ops.function.FnOnce (Self Args : Type) where
+  Output : Type
+  call_once : Self → Args → Result Output
+
+/- Trait declaration: [core::ops::function::FnMut] -/
+structure core.ops.function.FnMut (Self Args : Type) where
+  parent_clause_0 : core.ops.function.FnOnce Self Args
+  call_mut : Self → Args → Result parent_clause_0.Output
+  call_mut_back : Self → Args → parent_clause_0.Output → Result Self
+
+/- Trait declaration: [core::ops::function::Fn] -/
+structure core.ops.function.Fn (Self Args : Type) where
+  parent_clause_0 : core.ops.function.FnMut Self Args
+  call : Self → Args → Result parent_clause_0.parent_clause_0.Output
+
 end traits
-- 
cgit v1.2.3