mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 12:42:02 +03:00
232 lines
6.8 KiB
Idris
232 lines
6.8 KiB
Idris
|
|
import Data.Maybe
|
|
import Data.Nat
|
|
|
|
namespace SuperDog
|
|
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
|
|
|
|
record Other a where
|
|
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
|
|
, weight = 12
|
|
, name = "Sam" }
|
|
|
|
mySuperDog : SuperDog
|
|
mySuperDog = MkDog { age = 3
|
|
, weight = 10
|
|
, supername = "Super-Sam" }
|
|
|
|
other : ?
|
|
other = MkOther {fieldB = the Int 1, fieldA = "hi", imp = "Secret string"}
|
|
|
|
otherOk1 : Main.other.fieldB = (the Int 1)
|
|
otherOk1 = Refl
|
|
|
|
otherOk2 : Main.other.fieldA = "hi"
|
|
otherOk2 = Refl
|
|
|
|
otherOk3 : Main.other.imp = "Secret string"
|
|
otherOk3 = Refl
|
|
|
|
same : MkDog {age = 2, name = "Rex", weight = 10} = (the OrdinaryDog $ MkDog "Rex" 2 10)
|
|
same = Refl
|
|
|
|
namespace R1
|
|
|
|
public export
|
|
record R1 where
|
|
constructor MkR
|
|
-- `a` is out of scope here so
|
|
-- this silently declares an implicit field `0 a : Type`
|
|
field : a
|
|
|
|
namespace R2
|
|
|
|
public export
|
|
record R2 where
|
|
constructor MkR
|
|
{auto field : a}
|
|
|
|
r1 : R1 -- explicit fields access
|
|
r1 = MkR {field = "string"}
|
|
|
|
r2_shouldNotTypecheck1 : ?
|
|
r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
|
|
|
|
interface Show a => (num : Num a) => MyIface a where -- Some interface with
|
|
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
|
|
-- constructor)
|
|
|
|
|
|
data MyDataImpl : a -> Type where -- implementation of MyData
|
|
MkMyData : (x : a) -> MyDataImpl x
|
|
|
|
-- implementation MyIface Int where
|
|
-- MyData = MyDataImpl
|
|
-- someFunc = id
|
|
-- giveBack (MkMyData x) = x
|
|
|
|
%hint
|
|
instanceMyIfaceInt : MyIface Integer -- this def, roughly speaking, is the 'same thing' as the above implementation
|
|
-- Show Int, Num Int are auto implicits of MkIface
|
|
instanceMyIfaceInt = MkIface { MyData = MyDataImpl
|
|
, someFunc = id
|
|
, giveBack = \(MkMyData x) => x
|
|
, num = %search } -- auto implicit names are preserved
|
|
|
|
instanceOk : giveBack (MkMyData 22) = 22
|
|
instanceOk = Refl
|
|
|
|
interface Show' a where -- unlike Show, Show' reduces in types
|
|
constructor MkShow'
|
|
show' : a -> String
|
|
|
|
Show' String where
|
|
show' = id
|
|
|
|
%hint
|
|
showMaybe' : Show' a => Show' (Maybe a)
|
|
showMaybe' = MkShow' { show' = fromMaybe "Nothing" . (("Just " ++ ) . show' <$>) }
|
|
|
|
showMaybe'Ok : show' (Just "nice") = "Just nice"
|
|
showMaybe'Ok = Refl
|
|
|
|
record AllFieldTypes a where
|
|
constructor MkAllFieldTypes
|
|
exp : a
|
|
{imp : a}
|
|
{auto aut : a}
|
|
|
|
testAllFieldTypesOk : MkAllFieldTypes { aut = "aut"
|
|
, exp = "exp"
|
|
, imp = "imp" }
|
|
= MkAllFieldTypes "exp" {imp = "imp"} @{"aut"}
|
|
testAllFieldTypesOk = Refl
|
|
|
|
-------------------------------------
|
|
|
|
------ The Update syntax --------
|
|
|
|
mapName : (String -> String) -> OrdinaryDog -> OrdinaryDog
|
|
mapName f = {name $= f}
|
|
|
|
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' = {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-}, 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)
|
|
------------------------------------------------
|