git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2187 from david-christiansen/wip/tactical
1621052David Christiansen
idris.cabal+7
compare with master
unifiedsplit
@@ -512,6 +512,13 @@ Extra-source-files:
512 test/literate001/*.lidr
512 test/literate001/*.lidr
513 test/literate001/expected
513 test/literate001/expected
514
514
515+ test/meta001/run
516+ test/meta001/*.idr
517+ test/meta001/expected
518+ test/meta002/run
519+ test/meta002/*.idr
520+ test/meta002/expected
521+
515 test/primitives001/run
522 test/primitives001/run
516 test/primitives001/*.idr
523 test/primitives001/*.idr
517 test/primitives001/expected
524 test/primitives001/expected
libs/base/Language/Reflection/Utils.idr+9
@@ -297,3 +297,12 @@ instance Show Err where
297 show (ProviderError x) = "ProviderError \"" ++ show x ++ "\""
297 show (ProviderError x) = "ProviderError \"" ++ show x ++ "\""
298 show (LoadingFailed x err) = "LoadingFailed " ++ show x ++ " (" ++ show err ++ ")"
298 show (LoadingFailed x err) = "LoadingFailed " ++ show x ++ " (" ++ show err ++ ")"
299
299
300+-------------------------
301+-- Idiom brackets for Raw
302+-------------------------
303+
304+(<*>) : Raw -> Raw -> Raw
305+(<*>) = RApp
306+
307+pure : Raw -> Raw
308+pure = id
test/meta001/Finite.idrnew file+184
@@ -0,0 +1,184 @@
1+module Finite
2+
3+import Data.Fin
4+import Language.Reflection.Elab
5+import Language.Reflection.Utils
6+
7+-- Test various features of reflected elaboration, including looking
8+-- up datatypes, defining functions, and totality checking
9+
10+%default total
11+
12+||| A bijection between some type and bounded numbers
13+data Finite : Type -> Nat -> Type where
14+ IsFinite : (toFin : a -> Fin n) ->
15+ (fromFin : Fin n -> a) ->
16+ (ok1 : (x : a) -> fromFin (toFin x) = x) ->
17+ (ok2 : (y : Fin n) -> toFin (fromFin y) = y) ->
18+ Finite a n
19+
20+acceptableConstructor : Raw -> Bool
21+acceptableConstructor (Var _) = True
22+acceptableConstructor _ = False
23+
24+mkFin : Nat -> Nat -> Elab Raw
25+mkFin Z j = fail [TermPart `(Fin Z), TextPart "is uninhabitable!"]
26+mkFin (S k) Z = return `(FZ {k=~(quote k)})
27+mkFin (S k) (S j) = do i <- mkFin k j
28+ return `(FS {k=~(quote k)} ~i)
29+
30+mkToClause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
31+mkToClause fn size i (n, Var ty) =
32+ MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i
33+mkToClause fn size i (n, ty) =
34+ fail [TextPart "unsupported constructor", NamePart n]
35+
36+
37+mkFromClause : TTName -> (size, i : Nat) ->
38+ (constr : (TTName, Raw)) ->
39+ Elab FunClause
40+mkFromClause fn size i (n, Var ty) =
41+ return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)
42+mkFromClause fn size i (n, ty) =
43+ fail [TextPart "unsupported constructor", NamePart n]
44+
45+
46+mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
47+mkOk1Clause fn size i (n, Var ty) =
48+ return $ MkFunClause (RApp (Var fn) (Var n))
49+ [| (Var (UN "Refl")) (Var ty) (Var n) |]
50+mkOk1Clause fn size i (n, ty) =
51+ fail [TextPart "unsupported constructor", NamePart n]
52+
53+
54+mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
55+mkOk2Clause fn size i (n, Var ty) =
56+ return $ MkFunClause (RApp (Var fn) !(mkFin size i))
57+ [| (Var "Refl") `(Fin ~(quote size))
58+ !(mkFin size i) |]
59+mkOk2Clause fn size i (n, ty) =
60+ fail [TextPart "unsupported constructor", NamePart n]
61+
62+
63+mkToClauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)
64+mkToClauses fn size xs = mkToClauses' Z xs
65+ where mkToClauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
66+ mkToClauses' k [] = return []
67+ mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs
68+ clause <- mkToClause fn size k x
69+ return $ clause :: rest
70+
71+||| Generate a clause for the end of a pattern-match on Fins that
72+||| declares its own impossibility.
73+|||
74+||| This is to satisfy the totality checker, because `impossible`
75+||| clauses are still
76+mkAbsurdFinClause : (fn : TTName) -> (goal : Raw -> Raw) -> (size : Nat) ->
77+ Elab FunClause
78+mkAbsurdFinClause fn goal size =
79+ do pv <- gensym "badfin"
80+ lhsArg <- lhsBody pv size
81+ let lhs = RBind pv (PVar `(Fin Z : Type))
82+ (RApp (Var fn) lhsArg)
83+ let rhs = RBind pv (PVar `(Fin Z : Type))
84+ `(FinZElim {a=~(goal lhsArg)} ~(Var pv))
85+ return $ MkFunClause lhs rhs
86+ where lhsBody : TTName -> Nat -> Elab Raw
87+ lhsBody f Z = return $ Var f
88+ lhsBody f (S k) = do smaller <- lhsBody f k
89+ return `(FS {k=~(quote k)} ~smaller)
90+
91+
92+mkFromClauses : TTName -> TTName -> Nat ->
93+ List (TTName, Raw) -> Elab (List FunClause)
94+mkFromClauses fn ty size xs = mkFromClauses' Z xs
95+ where mkFromClauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
96+ mkFromClauses' k [] =
97+ return [!(mkAbsurdFinClause fn (const (Var ty)) size)]
98+ mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs
99+ clause <- mkFromClause fn size k x
100+ return $ clause :: rest
101+
102+mkOk1Clauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)
103+mkOk1Clauses fn size xs = mkOk1Clauses' Z xs
104+ where mkOk1Clauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
105+ mkOk1Clauses' k [] = return []
106+ mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs
107+ clause <- mkOk1Clause fn size k x
108+ return $ clause :: rest
109+
110+mkOk2Clauses : TTName -> Nat -> List (TTName, Raw) -> (Raw -> Raw) -> Elab (List FunClause)
111+mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs
112+ where mkOk2Clauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
113+ mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]
114+ mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs
115+ clause <- mkOk2Clause fn size k x
116+ return $ clause :: rest
117+
118+
119+genToFin : (to, from, ok1, ok2, ty : TTName) -> Elab ()
120+genToFin to from ok1 ok2 ty =
121+ do (MkDatatype famn tcargs tcres constrs) <- lookupDatatypeExact ty
122+ let size = length constrs
123+ argn <- gensym "arg"
124+ declareType $ Declare to [Explicit argn (Var ty)]
125+ `(Fin ~(quote size))
126+ toClauses <- mkToClauses to size constrs
127+ defineFunction $ DefineFun to toClauses
128+
129+ argn' <- gensym "arg"
130+ declareType $ Declare from [Explicit argn' `(Fin ~(quote size))]
131+ (Var ty)
132+ fromClauses <- mkFromClauses from ty size constrs
133+ defineFunction $ DefineFun from fromClauses
134+
135+ argn'' <- gensym "arg"
136+ declareType $ Declare ok1 [Explicit argn'' (Var ty)]
137+ `((=) {A=~(Var ty)} {B=~(Var ty)}
138+ ~(RApp (Var from) (RApp (Var to) (Var argn'')))
139+ ~(Var argn''))
140+ ok1Clauses <- mkOk1Clauses ok1 size constrs
141+ defineFunction $ DefineFun ok1 ok1Clauses
142+
143+ argn''' <- gensym "arg"
144+ let fty : Raw = `(Fin ~(quote size))
145+ let ok2ResTy = the (Raw -> Raw)
146+ (\n => `((=) {A=~fty} {B=~fty}
147+ ~(RApp (Var to) (RApp (Var from) n))
148+ ~n))
149+ declareType $ Declare ok2 [Explicit argn''' fty]
150+ (ok2ResTy (Var argn'''))
151+ ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy
152+ defineFunction $ DefineFun ok2 ok2Clauses
153+
154+ return ()
155+
156+
157+deriveFinite : Elab ()
158+deriveFinite =
159+ do (App (App (P _ `{Finite} _) (P _ tyn _)) _) <- snd <$> getGoal
160+ | ty => fail [TextPart "inapplicable goal type", TermPart ty]
161+ (MkDatatype _ _ _ constrs) <- lookupDatatypeExact tyn
162+ let size = length constrs
163+ let to = SN (MetaN tyn (UN "toFinite"))
164+ let from = SN (MetaN tyn (UN "fromFinite"))
165+ let ok1 = SN (MetaN tyn (UN "finiteOk1"))
166+ let ok2 = SN (MetaN tyn (UN "finiteOk2"))
167+ genToFin to from ok1 ok2 tyn
168+ fill `(IsFinite {a=~(Var tyn)} {n=~(quote size)}
169+ ~(Var to) ~(Var from)
170+ ~(Var ok1) ~(Var ok2))
171+ solve
172+
173+data TwoStateModel = Alive | Dead
174+data ThreeStateModel = Working | Disabled | Deceased
175+
176+
177+twoStateFinite : Finite TwoStateModel 2
178+twoStateFinite = %runElab deriveFinite
179+
180+threeStateFinite : Finite ThreeStateModel 3
181+threeStateFinite = %runElab deriveFinite
182+
183+boolFinite : Finite Bool 2
184+boolFinite = %runElab deriveFinite
test/meta001/expectednew file

No changes to the content.

test/meta001/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ --check --nocolour --consolewidth 70 Finite.idr
3+rm -f *.ibc
test/meta002/Tacs.idrnew file+252
@@ -0,0 +1,252 @@
1+||| A work-in-progress demonstration of Idris elaborator metaprogramming.
2+||| Goals:
3+||| * Let tactics query the environment, for things like type signatures
4+||| * Tactics expressions should be normal Idris expressions, and support
5+||| things like idiom brackets, Alternative, etc
6+||| * Make user-defined tactics just as easy to use as built-in ones
7+module Tacs
8+
9+import Data.Fin
10+import Data.Vect
11+
12+import Language.Reflection
13+import Language.Reflection.Errors
14+import Language.Reflection.Elab
15+import Language.Reflection.Utils
16+
17+%default total
18+
19+-- Tactics can now query the elaborator and bind variables
20+
21+--stuff : Nat -> Nat -> Nat
22+--stuff x y = %runElab (debugMessage "oh noes")
23+
24+intros : Elab ()
25+intros = do g <- getGoal
26+ case snd g of
27+ `(~_ -> ~_) => intro Nothing
28+ _ => return ()
29+
30+foo : Nat -> Nat
31+foo = %runElab (do intro (Just (UN "fnord"))
32+ fill `(plus ~(Var (UN "fnord")) ~(Var (UN "fnord")))
33+ solve)
34+
35+
36+
37+
38+-- Note that <|> is equivalent to "try" in the old tactics.
39+-- In these tactics, we use ordinary do notation and ordinary documentation strings!
40+||| Try to solve a goal with simple guesses of easy type
41+triv : Elab ()
42+triv = do fill `(Z) <|> fill `(() : ())
43+ solve
44+
45+
46+-- Solve both kinds of goal. The %runElab construction elaborates
47+-- to the result of running the tactic script that it contains.
48+
49+test1 : ()
50+test1 = %runElab triv
51+
52+test2 : Nat
53+test2 = %runElab triv
54+
55+
56+namespace STLC
57+
58+ data Ty = UNIT | ARR Ty Ty
59+
60+ %name Ty t,t',t''
61+
62+ instance Quotable Ty TT where
63+ quotedTy = `(Ty : Type)
64+ quote UNIT = `(UNIT : Ty)
65+ quote (ARR t t') = `(ARR ~(quote t) ~(quote t'))
66+
67+ elabTy : Ty -> Elab ()
68+ elabTy UNIT = do fill `(() : Type)
69+ solve
70+ elabTy (ARR t t') = do arg <- gensym "__stlc_arg"
71+ n1 <- mkTypeHole "t1"
72+ n2 <- mkTypeHole "t2"
73+ fill (RBind arg (Pi (Var n1) RType) (Var n2))
74+ focus n1; elabTy t
75+ focus n2; elabTy t'
76+ solve
77+ where mkTypeHole : String -> Elab TTName
78+ mkTypeHole hint = do holeName <- gensym hint
79+ claim holeName RType
80+ unfocus holeName
81+ return holeName
82+
83+ foo : %runElab (elabTy $ ARR (ARR UNIT UNIT) (ARR UNIT UNIT))
84+ foo = id
85+
86+ namespace Untyped
87+ ||| Completely untyped terms
88+ data UTm = Lam String UTm | App UTm UTm | Var String | UnitCon
89+ %name UTm tm,tm',tm''
90+
91+ namespace Scoped
92+ ||| Scope-checked terms - we'll use tactics to infer their types!
93+ data STm : Nat -> Type where
94+ Lam : String -> STm (S n) -> STm n
95+ App : STm n -> STm n -> STm n
96+ Var : Fin n -> STm n
97+ UnitCon : STm n
98+ %name STm tm,tm',tm''
99+
100+ ||| Find the de Bruijn index for a variable in a naming context
101+ findVar : Eq a => a -> Vect n a -> Maybe (Fin n)
102+ findVar x [] = Nothing
103+ findVar x (y :: xs) = if x == y then pure FZ else [| FS (findVar x xs) |]
104+
105+ ||| Resolve the names in a term to de Bruijn indices
106+ scopeCheck : Vect n String -> UTm -> Either String (STm n)
107+ scopeCheck vars (Lam x tm) = [| (Lam x) (scopeCheck (x::vars) tm) |]
108+ scopeCheck vars (App tm tm') = [| App (scopeCheck vars tm)
109+ (scopeCheck vars tm') |]
110+ scopeCheck vars (Var x) = case findVar x vars of
111+ Nothing => Left $ "Unknown var " ++ x
112+ Just i => pure $ Var i
113+ scopeCheck vars UnitCon = pure UnitCon
114+
115+ forgetScope : Vect n String -> STm n -> UTm
116+ forgetScope vars (Lam x tm) = Lam x (forgetScope (x::vars) tm)
117+ forgetScope vars (App tm tm') = App (forgetScope vars tm)
118+ (forgetScope vars tm')
119+ forgetScope vars (Var i) = Var $ index i vars
120+ forgetScope vars UnitCon = UnitCon
121+
122+ namespace Typed
123+
124+ Env : Type
125+ Env = List Ty
126+ %name Typed.Env env
127+
128+ ||| Well-typed de Bruijn indices
129+ data Ix : Env -> Ty -> Type where
130+ Z : Ix (t::env) t
131+ S : Ix env t -> Ix (t'::env) t
132+ %name Ix i,j,k
133+
134+ data Tm : List Ty -> Ty -> Type where
135+ Lam : {env : List Ty} -> {t, t' : Ty} ->
136+ Tm (t::env) t' -> Tm env (ARR t t')
137+ App : Tm env (ARR t t') -> Tm env t -> Tm env t'
138+ Var : Ix env t -> Tm env t
139+ UnitCon : Tm env UNIT
140+
141+ namespace Inference
142+ inNS : String -> TTName
143+ inNS n = NS (UN n) ["STLC", "Tacs"]
144+
145+ inTypedNS : String -> TTName
146+ inTypedNS n = NS (UN n) ["Typed", "STLC", "Tacs"]
147+
148+ elaborateSTLC : STm 0 -> Elab ()
149+ elaborateSTLC tm =
150+ do -- We're going to fill out a goal that wants a Sigma Ty (Tm [])
151+ -- First establish a hole for the type (inferred by side effect,
152+ -- similar to Idris implicit args)
153+ tH <- gensym "t"
154+ claim tH (Var (inNS "Ty"))
155+ unfocus tH
156+ -- Next we make a hole that wants a term in that type
157+ tmH <- gensym "tm"
158+ let p : Raw = `(Tm [])
159+ claim tmH (RApp p (Var tH))
160+ unfocus tmH
161+
162+ -- Now we put this hole variable into our sigma constructor
163+ -- prior to elaboration, so it doesn't disappear too soon
164+ fill `(MkSigma ~(Var tH) ~(Var tmH) : Sigma Ty (Tm []))
165+ solve
166+ focus tmH
167+ mkTerm [] tm
168+
169+ where mkEnvH : Elab TTName
170+ mkEnvH = do envH <- gensym "env"
171+ claim envH `(List Ty)
172+ unfocus envH
173+ return envH
174+
175+ mkTyH : Elab TTName
176+ mkTyH = do tyH <- gensym "ty"
177+ claim tyH `(Ty)
178+ unfocus tyH
179+ return tyH
180+
181+ mkIx : Fin n -> Elab ()
182+ mkIx FZ = do envH <- mkEnvH
183+ tH <- mkTyH
184+ fill `(Z {t=~(Var tH)} {env=~(Var envH)})
185+ solve
186+ mkIx (FS i) = do envH <- mkEnvH
187+ tH <- mkTyH
188+ vH <- mkTyH
189+ argH <- gensym "arg"
190+ claim argH `(Ix ~(Var envH) ~(Var tH))
191+ unfocus argH
192+ fill `(S {env=~(Var envH)} {t=~(Var tH)} {t'=~(Var vH)} ~(Var argH))
193+ solve
194+ focus argH
195+ mkIx i
196+
197+ mkTerm : Vect n TTName -> STm n -> Elab ()
198+ mkTerm xs (Lam x tm) = do tH <- mkTyH
199+ envH <- mkEnvH
200+ tH' <- mkTyH
201+ bodyH <- gensym "body"
202+ claim bodyH `(Tm ((::) ~(Var tH) ~(Var envH)) ~(Var tH'))
203+ fill `(Lam {env=~(Var envH)}
204+ {t=~(Var tH)} {t'=~(Var tH')}
205+ ~(Var bodyH))
206+
207+ solve
208+ focus bodyH
209+ mkTerm (tH::xs) tm
210+ mkTerm xs (App tm tm') = do envH <- mkEnvH
211+ tH <- mkTyH
212+ tH' <- mkTyH
213+ fH <- gensym "f"
214+ claim fH `(Tm ~(Var envH) (ARR ~(Var tH) ~(Var tH')))
215+ unfocus fH
216+ argH <- gensym "arg"
217+ claim argH `(Tm ~(Var envH) ~(Var tH))
218+ unfocus argH
219+ fill `(App {env=~(Var envH)}
220+ {t=~(Var tH)} {t'=~(Var tH')}
221+ ~(Var fH) ~(Var argH))
222+ solve
223+ focus fH
224+ mkTerm xs tm
225+ focus argH
226+ mkTerm xs tm'
227+ mkTerm xs (Var i) = do tH <- mkTyH
228+ envH <- mkEnvH
229+ ixH <- gensym "ix"
230+ claim ixH `(Ix ~(Var envH) ~(Var tH))
231+ unfocus ixH
232+ fill `(Var {env=~(Var envH)} {t=~(Var tH)} ~(Var ixH))
233+ solve
234+ focus ixH
235+ mkIx i
236+ mkTerm xs UnitCon = do envH <- mkEnvH
237+ fill `(UnitCon {env=~(Var envH)})
238+ solve
239+ testElab : Sigma Ty (Tm [])
240+ testElab = %runElab (elaborateSTLC (App (Lam "x" UnitCon) UnitCon))
241+
242+ testElab2 : Sigma Ty (Tm [])
243+ testElab2 = %runElab (elaborateSTLC (App (Lam "x" (Var 0)) UnitCon))
244+
245+ -- Doesn't work! :-)
246+ testElab3 : Sigma Ty (Tm [])
247+ testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))
248+ (Lam "x" (App (Var 0) (Var 0)))))
249+ -- Error is:
250+ -- Tacs.idr line 247 col 14:
251+ -- When elaborating right hand side of testElab3:
252+ -- Unifying ty and Tacs.STLC.ARR ty t would lead to infinite value
test/meta002/expectednew file+3
@@ -0,0 +1,3 @@
1+Tacs.idr:247:15:
2+When elaborating right hand side of testElab3:
3+Unifying ty and ARR ty t would lead to infinite value
test/meta002/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ --nocolour --check --consolewidth 70 Tacs.idr
3+rm -f *.ibc