Add more defs and comments into the test file

tests/idris2/basic048/Fld.idr

@@ -3,26 +3,28 @@ import Data.Maybe
 import Data.Nat
 
 namespace SuperDog
-   public export
-   record SuperDog where
-      constructor MkDog
-      supername : String
-      age : Int
-      weight : Int
+  public export
+  record SuperDog where
+     constructor MkDog
+     supername : String
+     age : Int
+     weight : Int
 
 namespace OrdinaryDog
-   public export
-   record OrdinaryDog where
-      constructor MkDog
-      name : String
-      age : Int
-      weight : Int
+  public export
+  record OrdinaryDog where
+    constructor MkDog
+    name : String
+    age : Int
+    weight : Int
 
 record Other a where
-   constructor MkOther
-   {imp : String}
-   fieldA : a
-   fieldB : b
+  constructor MkOther
+  {imp : String}
+  fieldA : a
+  fieldB : b
+
+------ Using new application syntax as sugar for data instantiation (be it data/record/interface) -------
 
 myDog : OrdinaryDog
 myDog = MkDog { age = 4
@@ -63,35 +65,23 @@ namespace R2
     constructor MkR
     {auto field : a}
 
-r1 : R1
+r1 : R1 -- explicit fields access
 r1 = MkR {field = "string"}
 
 r2_shouldNotTypecheck1 : ?
 r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
 
-onlyName : OrdinaryDog -> String
-onlyName (MkDog {name, _}) = name
-
-mapName : (String -> String) -> OrdinaryDog -> OrdinaryDog
-mapName f = {name $= f}
-
-setName : String -> OrdinaryDog -> OrdinaryDog
-setName name' = {name := name'}
-
-setNameOld : String -> OrdinaryDog -> OrdinaryDog
-setNameOld name' = record {name = name'}
-
 interface Show a => (num : Num a) => MyIface a where -- Some interface with
-   constructor MkIface
+  constructor MkIface
                                              -- constraints
-   data MyData : a -> Type                   -- and a data declaration.
-   someFunc : a -> a                         -- Constraints are now elaborated as auto implicits (as one would expect)
-   giveBack : {x : a} -> MyData x -> a       -- (previously as explicit arguments of the interface
+  data MyData : a -> Type                    -- and a data declaration.
+  someFunc : a -> a                          -- Constraints are now elaborated as auto implicits (as one would expect)
+  giveBack : {x : a} -> MyData x -> a        -- (previously as explicit arguments of the interface
                                              -- constructor)
 
 
 data MyDataImpl : a -> Type where            -- implementation of MyData
-     MkMyData : (x : a) -> MyDataImpl x
+  MkMyData : (x : a) -> MyDataImpl x
 
 -- implementation MyIface Int where
 --    MyData = MyDataImpl
@@ -100,7 +90,7 @@ data MyDataImpl : a -> Type where            -- implementation of MyData
 
 %hint
 instanceMyIfaceInt : MyIface Integer -- this def, roughly speaking, is the 'same thing' as the above implementation
-                                     -- Show Int, Num Int are auto implicits vvv
+                                     -- Show Int, Num Int are auto implicits of MkIface
 instanceMyIfaceInt = MkIface { MyData = MyDataImpl
                              , someFunc = id
                              , giveBack = \(MkMyData x) => x
@@ -109,11 +99,10 @@ instanceMyIfaceInt = MkIface { MyData = MyDataImpl
 instanceOk : giveBack (MkMyData 22) = 22
 instanceOk = Refl
 
-interface Show' a where -- can be used in types
+interface Show' a where -- unlike Show, Show' reduces in types
    constructor MkShow'
    show' : a -> String
 
-
 Show' String where
    show' = id
 
@@ -133,41 +122,108 @@ record AllFieldTypes a where
 testAllFieldTypesOk : MkAllFieldTypes { aut = "aut"
                                       , exp = "exp"
                                       , imp = "imp" }
-                      = MkAllFieldTypes "exp" {imp = "imp"} @{"aut"}
+                       = MkAllFieldTypes "exp" {imp = "imp"} @{"aut"}
 testAllFieldTypesOk = Refl
 
-test4 : {auto a : String} -> {auto a : String} -> String
-test4 @{a} @{a'} = show' a ++ ":" ++ show' a'
+-------------------------------------
 
--- unnamed explicit takes priority
-test5 : (a : String) -> (a : String) -> String
-test5 {a = a2} {-snd-} a1 {-fst-} = a1 ++ a2
+------  The Update syntax --------
 
-test5Ok : Main.test5 "abc" "def" = "abcdef"
-test5Ok = Refl
+mapName : (String -> String) -> OrdinaryDog -> OrdinaryDog
+mapName f = {name $= f}
 
--- unnamed auto takes priority
-testAutoPriorityOk : Main.test4 {a = "2"} @{"1"} = "1:2"
+setName : String -> OrdinaryDog -> OrdinaryDog
+setName name' = {name := name'}
+
+data Three : Type -> Type -> Type -> Type where
+  MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c
+
+mapSetMap : (a -> a') -> b' -> (c -> c') -> Three a b c -> Three a' b' c'
+mapSetMap f y' g = {x $= f, y := y', z $= g}
+
+setNameOld : String -> OrdinaryDog -> OrdinaryDog
+setNameOld name' = record {name = name'}
+
+-------------------------------------
+
+--------- Applications in presence of duplicate names ----------
+
+-- Duplicate names are ok and treated sequentially
+testDuplicateNames : {auto a : String} -> {auto a : String} -> String
+testDuplicateNames @{a} @{a'} = show' a ++ ":" ++ show' a'
+
+-- When binding arguments on LHS or listing arguments to
+-- a function on RHS
+-- unnamed arguments always take priority over named,
+-- i.e they are bound/applied first,
+-- regardless of their relative positions to named ones
+testOrder1 : (a : String) -> (a : String) -> String
+testOrder1 {a = a2} {-snd-} a1 {-fst-} = a1 ++ a2
+
+testOrder1Ok : Main.testOrder1 "abc" "def" = "abcdef"
+testOrder1Ok = Refl
+
+-- unnamed explicit "1" is passed first, followed by named {a = "2"}
+testAutoPriorityOk : Main.testOrder1 {a = "2"} "1" = "12"
 testAutoPriorityOk = Refl
 
+-- Two arguments with the same name can be successfully bound
+-- if one of them is renamed in patterns.
+-- As both arguments are requested by name
+-- They are bound in the same order they are given
 sameNamesOk : (a : String) -> (a : Nat) -> (String, Nat)
-sameNamesOk {a, a = b} = (a, b)
+sameNamesOk {a {- = a-}, a = b} = (a, b)
 
+-- All arguments are named and are of different `plicities`. Binds occur sequentially.
+-- Arguments are renamed on LHS
 eachArgType : (a : String) -> {a : String} -> {auto a : String} -> String
 eachArgType {a = a1, a = a2, a = a3} = a1 ++ a2 ++ a3
 
 eachArgTypeOk : eachArgType @{"3"} "1" {a = "2"} = "123"
 eachArgTypeOk = Refl
 
+-- Arguments with the same names are provided on RHS
+-- which is ok, they are passed sequentially.
 eachArgTypeOk2 : eachArgType {a = "1", a = "2", a = "3"} = "123"
 eachArgTypeOk2 = Refl
 
+----------------------------------------
+
+--------- Bind-all-explicits pattern ----------
+
+-- This pattern works like inexhaustible supply of
+-- `_` (Match-any patterns).
+
+-- Here to complete the definition we only
+-- need to know the name of the OrdinaryDog.
+-- We bind it with `{name, _}` also stating that
+-- any extra explicits should be disregarded,
+-- by inserting `_` into the braces.
+onlyName : OrdinaryDog -> String
+onlyName (MkDog {name, _ {-age, weight-} }) = name
+
 dontCare : (x : String) -> (y : String) -> (z : String) -> String
 dontCare {x, z, _} = x ++ z
 
 dontCareOk : Main.dontCare "a" "b" "c" = "ac"
 dontCareOk = Refl
 
+-- If none of the explicit arguments are wanted
+-- one `{}` can be used instead of writing an underscore for each.
 dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
 dontCare2 {} = plusCommutative {}
 -- dontCare2 _ _ _ _ _ = plusCommutative _ _
+
+data Tree a = Leaf a | Node (Tree a) a (Tree a)
+
+isNode : Tree a -> Bool
+isNode (Node {}) = True
+isNode _ = False
+
+data IsNode : Tree a -> Type where
+  Is : IsNode (Node {})
+
+decIsNode : (x : Tree a) -> Dec (IsNode x)
+decIsNode (Node {}) = Yes Is
+decIsNode (Leaf {}) = No (\case Is impossible)
+------------------------------------------------

tests/idris2/basic048/expected

@@ -1,11 +1,11 @@
 1/1: Building Fld (Fld.idr)
 Error: While processing right hand side of r2_shouldNotTypecheck1. Ambiguous elaboration. Possible results:
     Main.R2.MkR
-    Main.R1.MkR (Main.OrdinaryDog.MkDog ?name ?_ ?_)
+    Main.R1.MkR Type
 
-Fld.idr:70:26--70:29
+Fld.idr:72:26--72:29
     |
- 70 | r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
+ 72 | r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
     |                          ^^^
 
 Main> Main.myDog : OrdinaryDog