git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/meta002/DataDef.idr
75 lines 3.0 kB history raw
1module DataDef
3%language ElabReflection
5foo : Elab ()
6foo = do declareDatatype $ Declare `{{DataDef.N}} [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type)
7 defineDatatype $ DefineDatatype `{{DataDef.N}} [
8 Constructor `{{MkN}} [MkFunArg `{{x}} `(Nat) Implicit NotErased] (RApp (Var `{{DataDef.N}}) (Var `{{x}})),
9 Constructor `{{MkN'}} [MkFunArg `{{x}} `(Nat) Explicit NotErased] (RApp (Var `{{DataDef.N}}) (RApp (Var `{S}) (Var `{{x}})))
10 ]
11%runElab foo
13one : N 1
14one = MkN
16two : N 2
17two = MkN' 1
20-- mutual
21-- data U : Type where
22-- Base : U
23-- Pi : (code : U) -> (el code -> U) -> U
24-- el : U -> Type
25-- el Base = Bool
26-- el (Pi code body) = (x : el code) -> el (body x)
30mkU : Elab ()
31mkU = do let U = `{{DataDef.U}}
32 let el = `{{DataDef.el}}
33 declareDatatype $ Declare U [] `(Type)
34 declareType $ Declare el [MkFunArg `{{code}} (Var U) Explicit NotErased] `(Type)
35 defineDatatype $ DefineDatatype U [
36 Constructor `{{Base}} [] (Var U),
37 Constructor `{{Pi}}
38 [MkFunArg `{{code}} (Var U) Explicit NotErased,
39 MkFunArg `{{body}} `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)) Explicit NotErased]
40 (Var U)
41 ]
42 defineFunction $ DefineFun el [
43 MkFunClause (RBind `{{code}} (PVar (Var U))
44 (RBind `{{body}} (PVar `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)))
45 (RApp (Var el)
46 (RApp (RApp (Var `{{DataDef.Pi}})
47 (Var `{{code}}))
48 (Var `{{body}})))))
49 (RBind `{{code}} (PVar (Var U))
50 (RBind `{{body}} (PVar `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)))
51 (RBind `{{x}} (Pi (RApp (Var el) (Var `{{code}})) `(Type))
52 (RApp (Var el) (RApp (Var `{{body}}) (Var `{{x}})))))),
53 MkFunClause (RApp (Var el) (Var `{{DataDef.Base}})) `(Bool)
55 ]
57%runElab mkU
59tt : el Base
60tt = True
62fun : el (Pi Base (\x => if x then Base else Pi Base (const Base)))
63fun = \x => (case x of
64 False => \y => False
65 True => False)
68nope : Elab ()
69nope = defineDatatype $ DefineDatatype `{Either} [
70 Constructor `{{Middle}} [ MkFunArg `{{x}} `(Type) Implicit NotErased
71 , MkFunArg `{{y}} `(Type) Implicit NotErased
72 ] `(Either ~(Var `{{x}}) ~(Var `{{y}}))
73 ]
74%runElab nope