mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-13 07:26:59 +03:00
Add reasonable tests for elaborator reflection
This commit is contained in:
David Raymond Christiansen
parent
2ea89613c0
commit
28e2668206
@ -512,6 +512,13 @@ Extra-source-files:
|
||||
test/literate001/*.lidr
|
||||
test/literate001/expected
|
||||
|
||||
test/meta001/run
|
||||
test/meta001/*.idr
|
||||
test/meta001/expected
|
||||
test/meta002/run
|
||||
test/meta002/*.idr
|
||||
test/meta002/expected
|
||||
|
||||
test/primitives001/run
|
||||
test/primitives001/*.idr
|
||||
test/primitives001/expected
|
||||
|
||||
184
test/meta001/Finite.idr
Normal file
184
test/meta001/Finite.idr
Normal file
@ -0,0 +1,184 @@
|
||||
module Finite
|
||||
|
||||
import Data.Fin
|
||||
import Language.Reflection.Elab
|
||||
import Language.Reflection.Utils
|
||||
|
||||
-- Test various features of reflected elaboration, including looking
|
||||
-- up datatypes, defining functions, and totality checking
|
||||
|
||||
%default total
|
||||
|
||||
||| A bijection between some type and bounded numbers
|
||||
data Finite : Type -> Nat -> Type where
|
||||
IsFinite : (toFin : a -> Fin n) ->
|
||||
(fromFin : Fin n -> a) ->
|
||||
(ok1 : (x : a) -> fromFin (toFin x) = x) ->
|
||||
(ok2 : (y : Fin n) -> toFin (fromFin y) = y) ->
|
||||
Finite a n
|
||||
|
||||
acceptableConstructor : Raw -> Bool
|
||||
acceptableConstructor (Var _) = True
|
||||
acceptableConstructor _ = False
|
||||
|
||||
mkFin : Nat -> Nat -> Elab Raw
|
||||
mkFin Z j = fail [TermPart `(Fin Z), TextPart "is uninhabitable!"]
|
||||
mkFin (S k) Z = return `(FZ {k=~(quote k)})
|
||||
mkFin (S k) (S j) = do i <- mkFin k j
|
||||
return `(FS {k=~(quote k)} ~i)
|
||||
|
||||
mkToClause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
|
||||
mkToClause fn size i (n, Var ty) =
|
||||
MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i
|
||||
mkToClause fn size i (n, ty) =
|
||||
fail [TextPart "unsupported constructor", NamePart n]
|
||||
|
||||
|
||||
mkFromClause : TTName -> (size, i : Nat) ->
|
||||
(constr : (TTName, Raw)) ->
|
||||
Elab FunClause
|
||||
mkFromClause fn size i (n, Var ty) =
|
||||
return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)
|
||||
mkFromClause fn size i (n, ty) =
|
||||
fail [TextPart "unsupported constructor", NamePart n]
|
||||
|
||||
|
||||
mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
|
||||
mkOk1Clause fn size i (n, Var ty) =
|
||||
return $ MkFunClause (RApp (Var fn) (Var n))
|
||||
[| (Var (UN "Refl")) (Var ty) (Var n) |]
|
||||
mkOk1Clause fn size i (n, ty) =
|
||||
fail [TextPart "unsupported constructor", NamePart n]
|
||||
|
||||
|
||||
mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
|
||||
mkOk2Clause fn size i (n, Var ty) =
|
||||
return $ MkFunClause (RApp (Var fn) !(mkFin size i))
|
||||
[| (Var "Refl") `(Fin ~(quote size))
|
||||
!(mkFin size i) |]
|
||||
mkOk2Clause fn size i (n, ty) =
|
||||
fail [TextPart "unsupported constructor", NamePart n]
|
||||
|
||||
|
||||
mkToClauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)
|
||||
mkToClauses fn size xs = mkToClauses' Z xs
|
||||
where mkToClauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
|
||||
mkToClauses' k [] = return []
|
||||
mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs
|
||||
clause <- mkToClause fn size k x
|
||||
return $ clause :: rest
|
||||
|
||||
||| Generate a clause for the end of a pattern-match on Fins that
|
||||
||| declares its own impossibility.
|
||||
|||
|
||||
||| This is to satisfy the totality checker, because `impossible`
|
||||
||| clauses are still
|
||||
mkAbsurdFinClause : (fn : TTName) -> (goal : Raw -> Raw) -> (size : Nat) ->
|
||||
Elab FunClause
|
||||
mkAbsurdFinClause fn goal size =
|
||||
do pv <- gensym "badfin"
|
||||
lhsArg <- lhsBody pv size
|
||||
let lhs = RBind pv (PVar `(Fin Z : Type))
|
||||
(RApp (Var fn) lhsArg)
|
||||
let rhs = RBind pv (PVar `(Fin Z : Type))
|
||||
`(FinZElim {a=~(goal lhsArg)} ~(Var pv))
|
||||
return $ MkFunClause lhs rhs
|
||||
where lhsBody : TTName -> Nat -> Elab Raw
|
||||
lhsBody f Z = return $ Var f
|
||||
lhsBody f (S k) = do smaller <- lhsBody f k
|
||||
return `(FS {k=~(quote k)} ~smaller)
|
||||
|
||||
|
||||
mkFromClauses : TTName -> TTName -> Nat ->
|
||||
List (TTName, Raw) -> Elab (List FunClause)
|
||||
mkFromClauses fn ty size xs = mkFromClauses' Z xs
|
||||
where mkFromClauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
|
||||
mkFromClauses' k [] =
|
||||
return [!(mkAbsurdFinClause fn (const (Var ty)) size)]
|
||||
mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs
|
||||
clause <- mkFromClause fn size k x
|
||||
return $ clause :: rest
|
||||
|
||||
mkOk1Clauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)
|
||||
mkOk1Clauses fn size xs = mkOk1Clauses' Z xs
|
||||
where mkOk1Clauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
|
||||
mkOk1Clauses' k [] = return []
|
||||
mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs
|
||||
clause <- mkOk1Clause fn size k x
|
||||
return $ clause :: rest
|
||||
|
||||
mkOk2Clauses : TTName -> Nat -> List (TTName, Raw) -> (Raw -> Raw) -> Elab (List FunClause)
|
||||
mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs
|
||||
where mkOk2Clauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
|
||||
mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]
|
||||
mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs
|
||||
clause <- mkOk2Clause fn size k x
|
||||
return $ clause :: rest
|
||||
|
||||
|
||||
genToFin : (to, from, ok1, ok2, ty : TTName) -> Elab ()
|
||||
genToFin to from ok1 ok2 ty =
|
||||
do (MkDatatype famn tcargs tcres constrs) <- lookupDatatypeExact ty
|
||||
let size = length constrs
|
||||
argn <- gensym "arg"
|
||||
declareType $ Declare to [Explicit argn (Var ty)]
|
||||
`(Fin ~(quote size))
|
||||
toClauses <- mkToClauses to size constrs
|
||||
defineFunction $ DefineFun to toClauses
|
||||
|
||||
argn' <- gensym "arg"
|
||||
declareType $ Declare from [Explicit argn' `(Fin ~(quote size))]
|
||||
(Var ty)
|
||||
fromClauses <- mkFromClauses from ty size constrs
|
||||
defineFunction $ DefineFun from fromClauses
|
||||
|
||||
argn'' <- gensym "arg"
|
||||
declareType $ Declare ok1 [Explicit argn'' (Var ty)]
|
||||
`((=) {A=~(Var ty)} {B=~(Var ty)}
|
||||
~(RApp (Var from) (RApp (Var to) (Var argn'')))
|
||||
~(Var argn''))
|
||||
ok1Clauses <- mkOk1Clauses ok1 size constrs
|
||||
defineFunction $ DefineFun ok1 ok1Clauses
|
||||
|
||||
argn''' <- gensym "arg"
|
||||
let fty : Raw = `(Fin ~(quote size))
|
||||
let ok2ResTy = the (Raw -> Raw)
|
||||
(\n => `((=) {A=~fty} {B=~fty}
|
||||
~(RApp (Var to) (RApp (Var from) n))
|
||||
~n))
|
||||
declareType $ Declare ok2 [Explicit argn''' fty]
|
||||
(ok2ResTy (Var argn'''))
|
||||
ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy
|
||||
defineFunction $ DefineFun ok2 ok2Clauses
|
||||
|
||||
return ()
|
||||
|
||||
|
||||
deriveFinite : Elab ()
|
||||
deriveFinite =
|
||||
do (App (App (P _ `{Finite} _) (P _ tyn _)) _) <- snd <$> getGoal
|
||||
| ty => fail [TextPart "inapplicable goal type", TermPart ty]
|
||||
(MkDatatype _ _ _ constrs) <- lookupDatatypeExact tyn
|
||||
let size = length constrs
|
||||
let to = SN (MetaN tyn (UN "toFinite"))
|
||||
let from = SN (MetaN tyn (UN "fromFinite"))
|
||||
let ok1 = SN (MetaN tyn (UN "finiteOk1"))
|
||||
let ok2 = SN (MetaN tyn (UN "finiteOk2"))
|
||||
genToFin to from ok1 ok2 tyn
|
||||
fill `(IsFinite {a=~(Var tyn)} {n=~(quote size)}
|
||||
~(Var to) ~(Var from)
|
||||
~(Var ok1) ~(Var ok2))
|
||||
solve
|
||||
|
||||
data TwoStateModel = Alive | Dead
|
||||
data ThreeStateModel = Working | Disabled | Deceased
|
||||
|
||||
|
||||
twoStateFinite : Finite TwoStateModel 2
|
||||
twoStateFinite = %runElab deriveFinite
|
||||
|
||||
threeStateFinite : Finite ThreeStateModel 3
|
||||
threeStateFinite = %runElab deriveFinite
|
||||
|
||||
boolFinite : Finite Bool 2
|
||||
boolFinite = %runElab deriveFinite
|
||||
0
test/meta001/expected
Normal file
0
test/meta001/expected
Normal file
3
test/meta001/run
Executable file
3
test/meta001/run
Executable file
@ -0,0 +1,3 @@
|
||||
#!/usr/bin/env bash
|
||||
idris $@ --check --nocolour --consolewidth 70 Finite.idr
|
||||
rm -f *.ibc
|
||||
252
test/meta002/Tacs.idr
Normal file
252
test/meta002/Tacs.idr
Normal file
@ -0,0 +1,252 @@
|
||||
||| A work-in-progress demonstration of Idris elaborator metaprogramming.
|
||||
||| Goals:
|
||||
||| * Let tactics query the environment, for things like type signatures
|
||||
||| * Tactics expressions should be normal Idris expressions, and support
|
||||
||| things like idiom brackets, Alternative, etc
|
||||
||| * Make user-defined tactics just as easy to use as built-in ones
|
||||
module Tacs
|
||||
|
||||
import Data.Fin
|
||||
import Data.Vect
|
||||
|
||||
import Language.Reflection
|
||||
import Language.Reflection.Errors
|
||||
import Language.Reflection.Elab
|
||||
import Language.Reflection.Utils
|
||||
|
||||
%default total
|
||||
|
||||
-- Tactics can now query the elaborator and bind variables
|
||||
|
||||
--stuff : Nat -> Nat -> Nat
|
||||
--stuff x y = %runElab (debugMessage "oh noes")
|
||||
|
||||
intros : Elab ()
|
||||
intros = do g <- getGoal
|
||||
case snd g of
|
||||
`(~_ -> ~_) => intro Nothing
|
||||
_ => return ()
|
||||
|
||||
foo : Nat -> Nat
|
||||
foo = %runElab (do intro (Just (UN "fnord"))
|
||||
fill `(plus ~(Var (UN "fnord")) ~(Var (UN "fnord")))
|
||||
solve)
|
||||
|
||||
|
||||
|
||||
|
||||
-- Note that <|> is equivalent to "try" in the old tactics.
|
||||
-- In these tactics, we use ordinary do notation and ordinary documentation strings!
|
||||
||| Try to solve a goal with simple guesses of easy type
|
||||
triv : Elab ()
|
||||
triv = do fill `(Z) <|> fill `(() : ())
|
||||
solve
|
||||
|
||||
|
||||
-- Solve both kinds of goal. The %runElab construction elaborates
|
||||
-- to the result of running the tactic script that it contains.
|
||||
|
||||
test1 : ()
|
||||
test1 = %runElab triv
|
||||
|
||||
test2 : Nat
|
||||
test2 = %runElab triv
|
||||
|
||||
|
||||
namespace STLC
|
||||
|
||||
data Ty = UNIT | ARR Ty Ty
|
||||
|
||||
%name Ty t,t',t''
|
||||
|
||||
instance Quotable Ty TT where
|
||||
quotedTy = `(Ty : Type)
|
||||
quote UNIT = `(UNIT : Ty)
|
||||
quote (ARR t t') = `(ARR ~(quote t) ~(quote t'))
|
||||
|
||||
elabTy : Ty -> Elab ()
|
||||
elabTy UNIT = do fill `(() : Type)
|
||||
solve
|
||||
elabTy (ARR t t') = do arg <- gensym "__stlc_arg"
|
||||
n1 <- mkTypeHole "t1"
|
||||
n2 <- mkTypeHole "t2"
|
||||
fill (RBind arg (Pi (Var n1) RType) (Var n2))
|
||||
focus n1; elabTy t
|
||||
focus n2; elabTy t'
|
||||
solve
|
||||
where mkTypeHole : String -> Elab TTName
|
||||
mkTypeHole hint = do holeName <- gensym hint
|
||||
claim holeName RType
|
||||
unfocus holeName
|
||||
return holeName
|
||||
|
||||
foo : %runElab (elabTy $ ARR (ARR UNIT UNIT) (ARR UNIT UNIT))
|
||||
foo = id
|
||||
|
||||
namespace Untyped
|
||||
||| Completely untyped terms
|
||||
data UTm = Lam String UTm | App UTm UTm | Var String | UnitCon
|
||||
%name UTm tm,tm',tm''
|
||||
|
||||
namespace Scoped
|
||||
||| Scope-checked terms - we'll use tactics to infer their types!
|
||||
data STm : Nat -> Type where
|
||||
Lam : String -> STm (S n) -> STm n
|
||||
App : STm n -> STm n -> STm n
|
||||
Var : Fin n -> STm n
|
||||
UnitCon : STm n
|
||||
%name STm tm,tm',tm''
|
||||
|
||||
||| Find the de Bruijn index for a variable in a naming context
|
||||
findVar : Eq a => a -> Vect n a -> Maybe (Fin n)
|
||||
findVar x [] = Nothing
|
||||
findVar x (y :: xs) = if x == y then pure FZ else [| FS (findVar x xs) |]
|
||||
|
||||
||| Resolve the names in a term to de Bruijn indices
|
||||
scopeCheck : Vect n String -> UTm -> Either String (STm n)
|
||||
scopeCheck vars (Lam x tm) = [| (Lam x) (scopeCheck (x::vars) tm) |]
|
||||
scopeCheck vars (App tm tm') = [| App (scopeCheck vars tm)
|
||||
(scopeCheck vars tm') |]
|
||||
scopeCheck vars (Var x) = case findVar x vars of
|
||||
Nothing => Left $ "Unknown var " ++ x
|
||||
Just i => pure $ Var i
|
||||
scopeCheck vars UnitCon = pure UnitCon
|
||||
|
||||
forgetScope : Vect n String -> STm n -> UTm
|
||||
forgetScope vars (Lam x tm) = Lam x (forgetScope (x::vars) tm)
|
||||
forgetScope vars (App tm tm') = App (forgetScope vars tm)
|
||||
(forgetScope vars tm')
|
||||
forgetScope vars (Var i) = Var $ index i vars
|
||||
forgetScope vars UnitCon = UnitCon
|
||||
|
||||
namespace Typed
|
||||
|
||||
Env : Type
|
||||
Env = List Ty
|
||||
%name Typed.Env env
|
||||
|
||||
||| Well-typed de Bruijn indices
|
||||
data Ix : Env -> Ty -> Type where
|
||||
Z : Ix (t::env) t
|
||||
S : Ix env t -> Ix (t'::env) t
|
||||
%name Ix i,j,k
|
||||
|
||||
data Tm : List Ty -> Ty -> Type where
|
||||
Lam : {env : List Ty} -> {t, t' : Ty} ->
|
||||
Tm (t::env) t' -> Tm env (ARR t t')
|
||||
App : Tm env (ARR t t') -> Tm env t -> Tm env t'
|
||||
Var : Ix env t -> Tm env t
|
||||
UnitCon : Tm env UNIT
|
||||
|
||||
namespace Inference
|
||||
inNS : String -> TTName
|
||||
inNS n = NS (UN n) ["STLC", "Tacs"]
|
||||
|
||||
inTypedNS : String -> TTName
|
||||
inTypedNS n = NS (UN n) ["Typed", "STLC", "Tacs"]
|
||||
|
||||
elaborateSTLC : STm 0 -> Elab ()
|
||||
elaborateSTLC tm =
|
||||
do -- We're going to fill out a goal that wants a Sigma Ty (Tm [])
|
||||
-- First establish a hole for the type (inferred by side effect,
|
||||
-- similar to Idris implicit args)
|
||||
tH <- gensym "t"
|
||||
claim tH (Var (inNS "Ty"))
|
||||
unfocus tH
|
||||
-- Next we make a hole that wants a term in that type
|
||||
tmH <- gensym "tm"
|
||||
let p : Raw = `(Tm [])
|
||||
claim tmH (RApp p (Var tH))
|
||||
unfocus tmH
|
||||
|
||||
-- Now we put this hole variable into our sigma constructor
|
||||
-- prior to elaboration, so it doesn't disappear too soon
|
||||
fill `(MkSigma ~(Var tH) ~(Var tmH) : Sigma Ty (Tm []))
|
||||
solve
|
||||
focus tmH
|
||||
mkTerm [] tm
|
||||
|
||||
where mkEnvH : Elab TTName
|
||||
mkEnvH = do envH <- gensym "env"
|
||||
claim envH `(List Ty)
|
||||
unfocus envH
|
||||
return envH
|
||||
|
||||
mkTyH : Elab TTName
|
||||
mkTyH = do tyH <- gensym "ty"
|
||||
claim tyH `(Ty)
|
||||
unfocus tyH
|
||||
return tyH
|
||||
|
||||
mkIx : Fin n -> Elab ()
|
||||
mkIx FZ = do envH <- mkEnvH
|
||||
tH <- mkTyH
|
||||
fill `(Z {t=~(Var tH)} {env=~(Var envH)})
|
||||
solve
|
||||
mkIx (FS i) = do envH <- mkEnvH
|
||||
tH <- mkTyH
|
||||
vH <- mkTyH
|
||||
argH <- gensym "arg"
|
||||
claim argH `(Ix ~(Var envH) ~(Var tH))
|
||||
unfocus argH
|
||||
fill `(S {env=~(Var envH)} {t=~(Var tH)} {t'=~(Var vH)} ~(Var argH))
|
||||
solve
|
||||
focus argH
|
||||
mkIx i
|
||||
|
||||
mkTerm : Vect n TTName -> STm n -> Elab ()
|
||||
mkTerm xs (Lam x tm) = do tH <- mkTyH
|
||||
envH <- mkEnvH
|
||||
tH' <- mkTyH
|
||||
bodyH <- gensym "body"
|
||||
claim bodyH `(Tm ((::) ~(Var tH) ~(Var envH)) ~(Var tH'))
|
||||
fill `(Lam {env=~(Var envH)}
|
||||
{t=~(Var tH)} {t'=~(Var tH')}
|
||||
~(Var bodyH))
|
||||
|
||||
solve
|
||||
focus bodyH
|
||||
mkTerm (tH::xs) tm
|
||||
mkTerm xs (App tm tm') = do envH <- mkEnvH
|
||||
tH <- mkTyH
|
||||
tH' <- mkTyH
|
||||
fH <- gensym "f"
|
||||
claim fH `(Tm ~(Var envH) (ARR ~(Var tH) ~(Var tH')))
|
||||
unfocus fH
|
||||
argH <- gensym "arg"
|
||||
claim argH `(Tm ~(Var envH) ~(Var tH))
|
||||
unfocus argH
|
||||
fill `(App {env=~(Var envH)}
|
||||
{t=~(Var tH)} {t'=~(Var tH')}
|
||||
~(Var fH) ~(Var argH))
|
||||
solve
|
||||
focus fH
|
||||
mkTerm xs tm
|
||||
focus argH
|
||||
mkTerm xs tm'
|
||||
mkTerm xs (Var i) = do tH <- mkTyH
|
||||
envH <- mkEnvH
|
||||
ixH <- gensym "ix"
|
||||
claim ixH `(Ix ~(Var envH) ~(Var tH))
|
||||
unfocus ixH
|
||||
fill `(Var {env=~(Var envH)} {t=~(Var tH)} ~(Var ixH))
|
||||
solve
|
||||
focus ixH
|
||||
mkIx i
|
||||
mkTerm xs UnitCon = do envH <- mkEnvH
|
||||
fill `(UnitCon {env=~(Var envH)})
|
||||
solve
|
||||
testElab : Sigma Ty (Tm [])
|
||||
testElab = %runElab (elaborateSTLC (App (Lam "x" UnitCon) UnitCon))
|
||||
|
||||
testElab2 : Sigma Ty (Tm [])
|
||||
testElab2 = %runElab (elaborateSTLC (App (Lam "x" (Var 0)) UnitCon))
|
||||
|
||||
-- Doesn't work! :-)
|
||||
testElab3 : Sigma Ty (Tm [])
|
||||
testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))
|
||||
(Lam "x" (App (Var 0) (Var 0)))))
|
||||
-- Error is:
|
||||
-- Tacs.idr line 247 col 14:
|
||||
-- When elaborating right hand side of testElab3:
|
||||
-- Unifying ty and Tacs.STLC.ARR ty t would lead to infinite value
|
||||
3
test/meta002/expected
Normal file
3
test/meta002/expected
Normal file
@ -0,0 +1,3 @@
|
||||
Tacs.idr:247:15:
|
||||
When elaborating right hand side of testElab3:
|
||||
Unifying ty and ARR ty t would lead to infinite value
|
||||
3
test/meta002/run
Executable file
3
test/meta002/run
Executable file
@ -0,0 +1,3 @@
|
||||
#!/usr/bin/env bash
|
||||
idris $@ --nocolour --check --consolewidth 70 Tacs.idr
|
||||
rm -f *.ibc
|
||||
Loading…
Reference in New Issue
Block a user