git.iko.soy/Idris-dev
on master help sign in
Idris-dev/samples/misc/reflection.idr
151 lines 4.0 kB history raw
1module ReflectionExamples
3import Language.Reflection
5||| The reflected term for (\ x => reverse "bba")
6reflectVal : TT
7reflectVal = ?valPrf
9||| intEq for the integers 3 and 3
10applyTac1 : Int
11applyTac1 = ?tacPrf1
13||| intEq for the integers 3 and 42
14applyTac0 : Int
15applyTac0 = ?tacPrf0
17||| intEq for the two arguments
18applyTacDyn : Int -> Int -> Int
19applyTacDyn x y = ?tacPrfDyn
21||| Restored version for RConstant (I 42)
22fill : Int
23fill = ?fillPrf
25||| The type (TTName, TT) computed from its reflected raw rep.
26envTuple : Type
27envTuple = ?envTuplePrf
29||| The type List (TTName, TT) computed from its reflected raw rep.
30envList : List (TTName, TT)
31envList = ?envListPrf
33||| Reflected raw rep. for the type (TTName, TT)
34tupleType : Raw
35tupleType = RApp (RApp (Var (UN "Pair"))
36 (Var (NS (UN "TTName") ["Reflection", "Language"])))
37 (Var (NS (UN "TT") ["Reflection", "Language"]))
39||| Reflected raw rep for the type List (TTName, TT)
40mkTuple : Raw
41mkTuple = RApp (RApp (Var (UN "MkPair"))
42 (Var (NS (UN "TTName") ["Reflection", "Language"])))
43 (Var (NS (UN "TT") ["Reflection", "Language"]))
45||| Reflected raw rep for Prelude.List.Nil
46nil : Raw
47nil = (Var (NS (UN "Nil") ["List", "Prelude"]))
49||| Reflected raw rep for Prelude.List.::
50cons : Raw
51cons = (Var (NS (UN "::") ["List", "Prelude"]))
53||| 1 if the two arguments are equal, 0 otherwise
54||| This function is chosen as simple as possible for
55||| demo purposes.
56intEq : Int -> Int -> Int
57intEq x y = case x == y of
58 True => 1
59 False => 0
61||| A tactic script to run intEq on two let-bound or introduced
62||| arguments of the current (otherwise empty) proof context
63firstEq : List (TTName, Binder TT) -> TT -> Tactic
64firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) _ = Exact (App (App f x) y)
65firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) _ = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))
66firstEq xs _ = Exact (TConst (I 0))
68||| Skip 1 argument of the proof context and return the second one which
69||| has to be introduced. Used for the tactical dispatch example, which
70||| will push dispatch, as first env agrument.
71innerTac : List (TTName, Binder TT) -> TT -> Tactic
72innerTac (_::(x, Lam xt)::_) _ = Exact (P Bound x xt)
74||| Returns the reflected representation of innerTac
75innerTacTT : TT
76innerTacTT = ?innerTacTTPrf
78||| Dispatch to the reflected rep. of innerTac
79dispatch : List (TTName, Binder TT) -> TT -> Tactic
80dispatch xs _ = ApplyTactic (innerTacTT)
82||| Call dispatch which will then dispatch to innerTac.
83tacticalDispatch : Int -> Int
84tacticalDispatch = ?tacticalDispatchPrf
86||| A tactic to get the representation of its goal
87studyGoalTac : List (TTName, Binder TT) -> TT -> Tactic
88studyGoalTac _ goal = Reflect goal
90||| Returns the representation of its goal, TT
91||| (so this is reflect on the type TT)
92studyGoal : TT
93studyGoal = ?studyGoalPrf
95---------- Proofs ----------
97ReflectionExamples.studyGoalPrf = proof {
98 applyTactic studyGoalTac;
101ReflectionExamples.envTuplePrf = proof {
102 let x = tupleType;
103 fill x;
106ReflectionExamples.envListPrf = proof {
107 let x : Raw = RApp nil tupleType;
108 fill x;
112ReflectionExamples.valPrf = proof {
113 let x : (List String -> String) = (\ x => reverse "bba");
114 reflect x;
118ReflectionExamples.tacPrf1 = proof {
119 let f : (Int -> Int -> Int) = intEq;
120 let x : Int = 3;
121 let y : Int = 3;
122 applyTactic firstEq;
125ReflectionExamples.tacPrf0 = proof {
126 let f : (Int -> Int -> Int) = intEq;
127 let x : Int = 3;
128 let y : Int = 42;
129 applyTactic firstEq;
132ReflectionExamples.tacPrfDyn = proof {
133 let f : (Int -> Int -> Int) = intEq;
134 intros;
135 applyTactic firstEq;
138ReflectionExamples.fillPrf = proof {
139 let x : Raw = RConstant (I 42);
140 fill x;
143ReflectionExamples.innerTacTTPrf = proof {
144 reflect innerTac;
147ReflectionExamples.tacticalDispatchPrf = proof {
148 intros;
149 applyTactic dispatch;