git.iko.soy/Idris-dev
on master help sign in
Merge branch 'ImprovedReflection'
commit5d22c3e6b52bec38782380b1ec0c6c8320f2e2e7 authorJan Bessai <Jan.Bessai@tu-dortmund.de> dateSun 24 Mar 2013, 17:13 (14 years ago) parent7308d26c1a4eac
10 files changed+780−63
compare with master
unifiedsplit
Setup.hs+25−14 config.mk+4−1 idris.cabal+4−1 lib/Language/Reflection.idr+166−9 samples/reflection.idr+140 src/Idris/AbsSyntaxTree.hs+6−1 src/Idris/Completion.hs+2 src/Idris/ElabTerm.hs+415−33 src/Idris/IBC.hs+11−3 src/Idris/Parser.hs+7−1
Setup.hs+25−14
@@ -44,7 +44,7 @@ cleanJavaLib verbosity
4444 execPomExists <- doesFileExist ("java" </> "executable_pom.xml")
4545 when pomExists $ removeFile ("java" </> "executable_pom.xml")
4646
47−installStdLib pkg local verbosity copy
47+installStdLib pkg local withoutEffects verbosity copy
4848 = do let dirs = L.absoluteInstallDirs pkg local copy
4949 let idir = datadir dirs
5050 let icmd = idrisCmd local
@@ -54,11 +54,12 @@ installStdLib pkg local verbosity copy
5454 , "TARGET=" ++ idir
5555 , "IDRIS=" ++ icmd
5656 ]
57− make verbosity
58− [ "-C", "effects", "install"
59− , "TARGET=" ++ idir
60− , "IDRIS=" ++ icmd
61− ]
57+ unless withoutEffects $
58+ make verbosity
59+ [ "-C", "effects", "install"
60+ , "TARGET=" ++ idir
61+ , "IDRIS=" ++ icmd
62+ ]
6263 let idirRts = idir </> "rts"
6364 putStrLn $ "Installing run time system in " ++ idirRts
6465 make verbosity
@@ -93,17 +94,18 @@ removeLibIdris local verbosity
9394 , "IDRIS=" ++ icmd
9495 ]
9596
96−checkStdLib local verbosity
97+checkStdLib local withoutEffects verbosity
9798 = do let icmd = idrisCmd local
9899 putStrLn $ "Building libraries..."
99100 make verbosity
100101 [ "-C", "lib", "check"
101102 , "IDRIS=" ++ icmd
102103 ]
103− make verbosity
104− [ "-C", "effects", "check"
105− , "IDRIS=" ++ icmd
106− ]
104+ unless withoutEffects $
105+ make verbosity
106+ [ "-C", "effects", "check"
107+ , "IDRIS=" ++ icmd
108+ ]
107109 make verbosity
108110 [ "-C", "rts", "check"
109111 , "IDRIS=" ++ icmd
@@ -117,6 +119,12 @@ javaFlag flags =
117119 Just False -> False
118120 Nothing -> False
119121
122+noEffectsFlag flags =
123+ case lookup (FlagName "noeffects") (S.configConfigurationsFlags flags) of
124+ Just True -> True
125+ Just False -> False
126+ Nothing -> False
127+
120128preparePoms version
121129 = do pomTemplate <- TIO.readFile ("java" </> "pom_template.xml")
122130 TIO.writeFile ("java" </> "pom.xml") (insertVersion pomTemplate)
@@ -132,11 +140,13 @@ main = do
132140 defaultMainWithHooks $ simpleUserHooks
133141 { postCopy = \ _ flags pkg lbi -> do
134142 let verb = S.fromFlag $ S.copyVerbosity flags
135− installStdLib pkg lbi verb
143+ let withoutEffects = noEffectsFlag $ configFlags lbi
144+ installStdLib pkg lbi withoutEffects verb
136145 (S.fromFlag $ S.copyDest flags)
137146 , postInst = \ _ flags pkg lbi -> do
138147 let verb = (S.fromFlag $ S.installVerbosity flags)
139− installStdLib pkg lbi verb
148+ let withoutEffects = noEffectsFlag $ configFlags lbi
149+ installStdLib pkg lbi withoutEffects verb
140150 NoCopyDest
141151 when (javaFlag $ configFlags lbi)
142152 (installJavaLib pkg
@@ -155,6 +165,7 @@ main = do
155165 cleanJavaLib verb
156166 , postBuild = \ _ flags _ lbi -> do
157167 let verb = S.fromFlag $ S.buildVerbosity flags
158− checkStdLib lbi verb
168+ let withoutEffects = noEffectsFlag $ configFlags lbi
169+ checkStdLib lbi withoutEffects verb
159170 when (javaFlag $ configFlags lbi) (checkJavaLib verb)
160171 }
config.mk+4−1
@@ -1,6 +1,9 @@
11GMP_INCLUDE_DIR :=
22CC :=gcc
33CABAL :=cabal
4−CABALFLAGS :=
4+#CABALFLAGS :=
55## Enable Java RTS:
66#CABALFLAGS :=-f Java
7+## Disable building of Effects
8+CABALFLAGS :=-f NoEffects
9+
idris.cabal+4−1
@@ -65,7 +65,7 @@ Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr
6565 config.mk
6666 rts/*.c rts/*.h rts/Makefile
6767 js/*.js
68− java/org/idris/rts/*.java
68+ java/org/idris/rts/*.java
6969
7070source-repository head
7171 type: git
@@ -75,6 +75,9 @@ Flag Java
7575 Description: Build the Java RTS
7676 Default: False
7777
78+Flag NoEffects
79+ Description: Do not build the effects package
80+ Default: False
7881
7982Executable idris
8083 Main-is: Main.hs
lib/Language/Reflection.idr+166−9
@@ -1,19 +1,176 @@
11module Language.Reflection
22
3−TTName : Type
4−TTName = String -- needs to capture namespaces too...
3+%access public
54
6−data TT = Var TTName
7− | Lam TTName TT TT
8− | Pi TTName TT TT
9− | Let TTName TT TT TT
10− | App TTName TT TT
5+data TTName = UN String
6+ -- ^ User-provided name
7+ | NS TTName (List String)
8+ -- ^ Root, namespaces
9+ | MN Int String
10+ -- ^ Machine chosen names
11+ | NErased
12+ -- ^ Name of somethng which is never used in scope
13+
14+implicit
15+userSuppliedName : String -> TTName
16+userSuppliedName = UN
17+
18+data TTUExp = UVar Int
19+ -- ^ universe variable
20+ | UVal Int
21+ -- ^ explicit universe variable
22+
23+-- | Primitive constants
24+data Const = I Int | BI Nat | Fl Float | Ch Char | Str String
25+ | IType | BIType | FlType | ChType | StrType
26+ | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64
27+ | B8Type | B16Type | B32Type | B64Type
28+ | PtrType | VoidType | Forgot
29+
30+abstract class ReflConst (a : Type) where
31+ toConst : a -> Const
32+
33+instance ReflConst Int where
34+ toConst x = I x
35+
36+instance ReflConst Nat where
37+ toConst = BI
38+
39+instance ReflConst Float where
40+ toConst = Fl
41+
42+instance ReflConst Char where
43+ toConst = Ch
44+
45+instance ReflConst String where
46+ toConst = Str
47+
48+instance ReflConst Bits8 where
49+ toConst = B8
50+
51+instance ReflConst Bits16 where
52+ toConst = B16
53+
54+instance ReflConst Bits32 where
55+ toConst = B32
56+
57+instance ReflConst Bits64 where
58+ toConst = B64
59+
60+implicit
61+reflectConstant: (ReflConst a) => a -> Const
62+reflectConstant = toConst
63+
64+
65+-- | Types of named references
66+data NameType = Bound
67+ -- ^ reference which is just bound, e.g. by intro
68+ | Ref
69+ -- ^ reference to a variable
70+ | DCon Int Int
71+ -- ^ constructor with tag and number
72+ | TCon Int Int
73+ -- ^ type constructor with tag and number
74+
75+-- | Types annotations for bound variables in different
76+-- binding contexts
77+data Binder a = Lam a
78+ | Pi a
79+ | Let a a
80+ | NLet a a
81+ | Hole a
82+ | GHole a
83+ | Guess a a
84+ | PVar a
85+ | PVTy a
86+
87+
88+instance Functor Binder where
89+ fmap f (Lam x) = Lam (f x)
90+ fmap f (Pi x) = Pi (f x)
91+ fmap f (Let x y) = Let (f x) (f y)
92+ fmap f (NLet x y) = NLet (f x) (f y)
93+ fmap f (Hole x) = Hole (f x)
94+ fmap f (GHole x) = GHole (f x)
95+ fmap f (Guess x y) = Guess (f x) (f y)
96+ fmap f (PVar x) = PVar (f x)
97+ fmap f (PVTy x) = PVTy (f x)
98+
99+total
100+traverse : (Applicative f) => (a -> f b) -> Binder a -> f (Binder b)
101+traverse f (Lam x) = [| Lam (f x) |]
102+traverse f (Pi x) = [| Pi (f x) |]
103+traverse f (Let x y) = [| Let (f x) (f y) |]
104+traverse f (NLet x y) = [| NLet (f x) (f y) |]
105+traverse f (Hole x) = [| Hole (f x) |]
106+traverse f (GHole x) = [| GHole (f x) |]
107+traverse f (Guess x y) = [| Guess (f x) (f y) |]
108+traverse f (PVar x) = [| PVar (f x) |]
109+traverse f (PVTy x) = [| PVTy (f x) |]
110+
111+
112+-- | Reflection of the well typed core language
113+data TT = P NameType TTName TT
114+ -- ^ named binders
115+ | V Int
116+ -- ^ variables
117+ | Bind TTName (Binder TT) TT
118+ -- ^ type annotated named bindings
119+ | App TT TT
120+ -- ^ (named) application of a function to a value
121+ | TConst Const
122+ -- ^ constants
123+ | Proj TT Int
124+ -- ^ argument projection; runtime only
125+ | Erased
126+ -- ^ erased terms
127+ | Impossible
128+ -- ^ impossible terms
129+ | TType TTUExp
130+ -- ^ types
131+
132+-- | Raw terms without types
133+data Raw = Var TTName
134+ | RBind TTName (Binder Raw) Raw
135+ | RApp Raw Raw
136+ | RType
137+ | RForce Raw
138+ | RConstant Const
11139
12140data Tactic = Try Tactic Tactic
13− | GoalType TTName Tactic -- only run if the goal has the right type
141+ -- ^ try the first tactic and resort to the second one on failure
142+ | GoalType String Tactic
143+ -- ^ only run if the goal has the right type
14144 | Refine TTName
145+ -- ^ resolve function name, find matching arguments in the
146+ -- context and compute the proof target
15147 | Seq Tactic Tactic
148+ -- ^ apply both tactics in sequence
16149 | Trivial
150+ -- ^ intelligently construct the proof target from the context
17151 | Solve
18− | Exact TT -- not yet implemented
152+ -- ^ infer the proof target from the context
153+ | Intros
154+ -- ^ introduce all variables into the context
155+ | Intro TTName
156+ -- ^ introduce a named variable into the context, use the
157+ -- first one if the given name is not found
158+ | ApplyTactic TT
159+ -- ^ invoke the reflected rep. of another tactic
160+ | Reflect TT
161+ -- ^ turn a value into its reflected representation
162+ | Fill Raw
163+ -- ^ turn a raw value back into a term
164+ | Exact TT
165+ -- ^ use the given value to conclude the proof
166+ | Focus TTName
167+ -- ^ focus a named hole
168+ | Rewrite TT
169+ -- ^ rewrite using the reflected rep. of a equality proof
170+ | LetTac TTName TT
171+ -- ^ name a reflected term
172+ | LetTacTy TTName TT TT
173+ -- ^ name a reflected term and type it
174+ | Compute
175+ -- ^ normalise the context
19176
samples/reflection.idrnew file+140
@@ -0,0 +1,140 @@
1+module ReflectionExamples
2+
3+import Language.Reflection
4+
5+-- | The reflected term for (\ x => reverse "bba")
6+reflectVal : TT
7+reflectVal = ?valPrf
8+
9+-- | intEq for the integers 3 and 3
10+applyTac1 : Int
11+applyTac1 = ?tacPrf1
12+
13+-- | intEq for the integers 3 and 42
14+applyTac0 : Int
15+applyTac0 = ?tacPrf0
16+
17+-- | intEq for the two arguments
18+applyTacDyn : Int -> Int -> Int
19+applyTacDyn x y = ?tacPrfDyn
20+
21+-- | Restored version for RConstant (I 42)
22+fill : Int
23+fill = ?fillPrf
24+
25+-- | The type (TTName, TT) computed from its reflected raw rep.
26+envTuple : Type
27+envTuple = ?envTuplePrf
28+
29+-- | The type List (TTName, TT) computed from its reflected raw rep.
30+envList : List (TTName, TT)
31+envList = ?envListPrf
32+
33+-- | Reflected raw rep. for the type (TTName, TT)
34+tupleType : Raw
35+tupleType = RApp (RApp (Var (MN 0 "__Pair"))
36+ (Var (NS (UN "TTName") ["Reflection", "Language"])))
37+ (Var (NS (UN "TT") ["Reflection", "Language"]))
38+
39+-- | Reflected raw rep for the type List (TTName, TT)
40+mkTuple : Raw
41+mkTuple = RApp (RApp (Var (MN 0 "__MkPair"))
42+ (Var (NS (UN "TTName") ["Reflection", "Language"])))
43+ (Var (NS (UN "TT") ["Reflection", "Language"]))
44+
45+-- | Reflected raw rep for Prelude.List.Nil
46+nil : Raw
47+nil = (Var (NS (UN "Nil") ["List", "Prelude"]))
48+
49+-- | Reflected raw rep for Prelude.List.::
50+cons : Raw
51+cons = (Var (NS (UN "::") ["List", "Prelude"]))
52+
53+-- | 1 if the two arguments are equal, 0 otherwise
54+-- This function is chosen as simple as possible for
55+-- demo purposes.
56+intEq : Int -> Int -> Int
57+intEq x y = case x == y of
58+ True => 1
59+ False => 0
60+
61+-- | A tactic script to run intEq on two let-bound or introduced
62+-- arguments of the current (otherwise empty) proof context
63+firstEq : List (TTName, Binder TT) -> Tactic
64+firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) = Exact (App (App f x) y)
65+firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))
66+firstEq xs = Exact (TConst (I 0))
67+
68+-- | Skip 3 arguments of the proof context and return the fourth one which
69+-- has to be introduced.
70+-- Used for the tactical dispatch example, which will push dispatch,
71+-- its current proof context and the result of dispatch applied to it
72+-- first.
73+innerTac : List (TTName, Binder TT) -> Tactic
74+innerTac (_::_::_::(x, Lam xt)::_) = Exact (P Bound x xt)
75+
76+-- | Returns the reflected representation of innerTac
77+innerTacTT : TT
78+innerTacTT = ?innerTacTTPrf
79+
80+-- | Dispatch to the reflected rep. of innerTac
81+dispatch : List (TTName, Binder TT) -> Tactic
82+dispatch xs = ApplyTactic (innerTacTT)
83+
84+-- | Call dispatch which will then dispatch to innerTac.
85+tacticalDispatch : Int -> Int
86+tacticalDispatch = ?tacticalDispatchPrf
87+
88+---------- Proofs ----------
89+
90+ReflectionExamples.envTuplePrf = proof {
91+ let x = tupleType;
92+ fill x;
93+}
94+
95+ReflectionExamples.envListPrf = proof {
96+ let x : Raw = RApp nil tupleType;
97+ fill x;
98+}
99+
100+
101+ReflectionExamples.valPrf = proof {
102+ let x : (List String -> String) = (\ x => reverse "bba");
103+ reflect x;
104+}
105+
106+
107+ReflectionExamples.tacPrf1 = proof {
108+ let f : (Int -> Int -> Int) = intEq;
109+ let x : Int = 3;
110+ let y : Int = 3;
111+ applyTactic firstEq;
112+}
113+
114+ReflectionExamples.tacPrf0 = proof {
115+ let f : (Int -> Int -> Int) = intEq;
116+ let x : Int = 3;
117+ let y : Int = 42;
118+ applyTactic firstEq;
119+}
120+
121+ReflectionExamples.tacPrfDyn = proof {
122+ let f : (Int -> Int -> Int) = intEq;
123+ intros;
124+ applyTactic firstEq;
125+}
126+
127+ReflectionExamples.fillPrf = proof {
128+ let x : Raw = RConstant (I 42);
129+ fill x;
130+}
131+
132+ReflectionExamples.innerTacTTPrf = proof {
133+ reflect innerTac;
134+}
135+
136+ReflectionExamples.tacticalDispatchPrf = proof {
137+ intros;
138+ applyTactic dispatch;
139+}
140+
src/Idris/AbsSyntaxTree.hs+6−1
@@ -528,7 +528,9 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
528528 | ProofState | ProofTerm | Undo
529529 | Try (PTactic' t) (PTactic' t)
530530 | TSeq (PTactic' t) (PTactic' t)
531− | ReflectTac t -- see Language.Reflection module
531+ | ApplyTactic t -- see Language.Reflection module
532+ | Reflect t
533+ | Fill t
532534 | GoalType String (PTactic' t)
533535 | Qed | Abandon
534536 deriving (Show, Eq, Functor)
@@ -553,6 +555,9 @@ instance Sized a => Sized (PTactic' a) where
553555 size Undo = 1
554556 size (Try l r) = 1 + size l + size r
555557 size (TSeq l r) = 1 + size l + size r
558+ size (ApplyTactic t) = 1 + size t
559+ size (Reflect t) = 1 + size t
560+ size (Fill t) = 1 + size t
556561 size Qed = 1
557562 size Abandon = 1
558563
src/Idris/Completion.hs+2
@@ -35,7 +35,9 @@ tacticArgs = [ ("intro", Nothing)
3535 , ("let", Nothing) -- FIXME syntax for let
3636 , ("focus", Just ExprTArg)
3737 , ("exact", Just ExprTArg)
38+ , ("applyTactic", Just ExprTArg)
3839 , ("reflect", Just ExprTArg)
40+ , ("fill", Just ExprTArg)
3941 , ("try", Just AltsTArg)
4042 ] ++ map (\x -> (x, Nothing)) [
4143 "intro", "intros", "compute", "trivial", "solve", "attack",
src/Idris/ElabTerm.hs+415−33
@@ -13,6 +13,7 @@ import Core.Evaluate
1313import Control.Monad
1414import Control.Monad.State
1515import Data.List
16+
1617import Debug.Trace
1718
1819-- Data to pass to recursively called elaborators; e.g. for where blocks,
@@ -772,22 +773,76 @@ runTac autoSolve ist tac = do env <- get_env
772773 runT Solve = solve
773774 runT (Try l r) = do try' (runT l) (runT r) True
774775 runT (TSeq l r) = do runT l; runT r
775− runT (ReflectTac tm) = do attack -- let x : Tactic = tm in ...
776− valn <- unique_hole (MN 0 "tacval")
777− claim valn (Var tacticTy)
778− tacn <- unique_hole (MN 0 "tacn")
779− letbind tacn (Var tacticTy) (Var valn)
780− focus valn
781− elab ist toplevel False False (MN 0 "tac") tm
782− (tm', ty') <- get_type_val (Var tacn)
783− ctxt <- get_context
784− env <- get_env
785− let tactic = normalise ctxt env tm'
786− runReflected tactic
787−-- p <- get_term
788−-- trace (show p ++ "\n\n") $
789− return ()
790− where tacticTy = tacm "Tactic"
776+ runT (ApplyTactic tm) = do tenv <- get_env -- store the environment before it is loaded with junk
777+ attack -- let f : List (TTName, Binder TT) -> Tactic = tm in ...
778+ valn <- unique_hole (MN 0 "tacval")
779+ claim valn (RBind (UN "__pi_arg")
780+ (Pi (RApp listTy envTupleType)) tacticTy)
781+ tacn <- unique_hole (MN 0 "tacn")
782+ letbind tacn (RBind (UN "__pi_arg")
783+ (Pi (RApp listTy envTupleType)) tacticTy)
784+ (Var valn)
785+ focus valn
786+ elab ist toplevel False False (MN 0 "tac") tm
787+ (tm', ty') <- get_type_val (Var tacn)
788+ ctxt <- get_context
789+ env <- get_env
790+ let tm'' = normalise ctxt env tm'
791+ attack -- let x : List (TTName, Binder TT) = reflectEnv in ...
792+ envval <- unique_hole (MN 0 "letval")
793+ claim envval (RApp listTy envTupleType)
794+ letn <- unique_hole (MN 0 "letvar")
795+ letbind letn (RApp listTy envTupleType) (Var envval)
796+ focus envval
797+ env <- get_env
798+ elab ist toplevel False False (MN 0 "tac") (PQuote (reflectEnv tenv))
799+ (env', _) <- get_type_val (Var letn)
800+ ctxt <- get_context
801+ env <- get_env
802+ let env'' = normalise ctxt env env'
803+ attack -- let z : Tactic = f x
804+ restac <- unique_hole (MN 0 "letval")
805+ claim restac tacticTy
806+ letn <- unique_hole (MN 0 "letvar")
807+ letbind letn tacticTy (Var restac)
808+ focus restac
809+ elab ist toplevel False False (MN 0 "tac") (PQuote (RApp (forget tm'') (forget env'')))
810+ (res, _) <- get_type_val (Var letn)
811+ ctxt <- get_context
812+ env <- get_env
813+ let tactic = normalise ctxt env res
814+ runReflected tactic
815+ where tacticTy = Var (reflm "Tactic")
816+ listTy = Var (NS (UN "List") ["List", "Prelude"])
817+ runT (Reflect v) = do attack -- let x = reflect v in ...
818+ tyn <- unique_hole (MN 0 "letty")
819+ claim tyn RType
820+ valn <- unique_hole (MN 0 "letval")
821+ claim valn (Var tyn)
822+ letn <- unique_hole (MN 0 "letvar")
823+ letbind letn (Var tyn) (Var valn)
824+ focus valn
825+ elab ist toplevel False False (MN 0 "tac") v
826+ (value, _) <- get_type_val (Var letn)
827+ ctxt <- get_context
828+ env <- get_env
829+ let value' = hnf ctxt env value
830+ runTac autoSolve ist (Exact $ PQuote (reflect value'))
831+ runT (Fill v) = do attack -- let x = fill x in ...
832+ tyn <- unique_hole (MN 0 "letty")
833+ claim tyn RType
834+ valn <- unique_hole (MN 0 "letval")
835+ claim valn (Var tyn)
836+ letn <- unique_hole (MN 0 "letvar")
837+ letbind letn (Var tyn) (Var valn)
838+ focus valn
839+ elab ist toplevel False False (MN 0 "tac") v
840+ (value, _) <- get_type_val (Var letn)
841+ ctxt <- get_context
842+ env <- get_env
843+ let value' = normalise ctxt env value
844+ rawValue <- reifyRaw value'
845+ runTac autoSolve ist (Exact $ PQuote rawValue)
791846 runT (GoalType n tac) = do g <- goal
792847 case unApply g of
793848 (P _ n' _, _) ->
@@ -797,24 +852,351 @@ runTac autoSolve ist tac = do env <- get_env
797852 _ -> fail "Wrong goal type"
798853 runT x = fail $ "Not implemented " ++ show x
799854
800− runReflected t = do t' <- reify t
855+ runReflected t = do t' <- reify ist t
801856 runTac autoSolve ist t'
802− tacm n = NS (UN n) ["Reflection", "Language"]
803−
804− reify :: Term -> ElabD PTactic
805− reify (P _ n _) | n == tacm "Trivial" = return Trivial
806− reify (P _ n _) | n == tacm "Solve" = return Solve
807− reify f@(App _ _)
808− | (P _ f _, args) <- unApply f = reifyAp f args
809− reify t = fail ("Unknown tactic " ++ show t)
810−
811− reifyAp t [l, r] | t == tacm "Try" = liftM2 Try (reify l) (reify r)
812− reifyAp t [Constant (Str x)]
813− | t == tacm "Refine" = return $ Refine (UN x) []
814− reifyAp t [l, r] | t == tacm "Seq" = liftM2 TSeq (reify l) (reify r)
815− reifyAp t [Constant (Str n), x]
816− | t == tacm "GoalType" = liftM (GoalType n) (reify x)
817− reifyAp f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
857+
858+-- | Prefix a name with the "Reflection.Language" namespace
859+reflm :: String -> Name
860+reflm n = NS (UN n) ["Reflection", "Language"]
861+
862+
863+-- | Reify tactics from their reflected representation
864+reify :: IState -> Term -> ElabD PTactic
865+reify _ (P _ n _) | n == reflm "Intros" = return Intros
866+reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
867+reify _ (P _ n _) | n == reflm "Solve" = return Solve
868+reify _ (P _ n _) | n == reflm "Compute" = return Compute
869+reify ist t@(App _ _)
870+ | (P _ f _, args) <- unApply t = reifyApp ist f args
871+reify _ t = fail ("Unknown tactic " ++ show t)
872+
873+reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
874+reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
875+reifyApp _ t [x]
876+ | t == reflm "Refine" = do n <- reifyTTName x
877+ return $ Refine n []
878+reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
879+reifyApp ist t [Constant (Str n), x]
880+ | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
881+reifyApp _ t [Constant (Str n)]
882+ | t == reflm "Intro" = return $ Intro [UN n]
883+reifyApp ist t [t']
884+ | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
885+reifyApp ist t [t']
886+ | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
887+reifyApp _ t [t']
888+ | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
889+reifyApp ist t [t']
890+ | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
891+reifyApp ist t [x]
892+ | t == reflm "Focus" = liftM Focus (reifyTTName x)
893+reifyApp ist t [t']
894+ | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
895+reifyApp ist t [n, t']
896+ | t == reflm "LetTac" = do n' <- reifyTTName n
897+ t'' <- reifyTT t'
898+ return $ LetTac n' (delab ist t')
899+reifyApp ist t [n, tt', t']
900+ | t == reflm "LetTacTy" = do n' <- reifyTTName n
901+ tt'' <- reifyTT tt'
902+ t'' <- reifyTT t'
903+ return $ LetTacTy n' (delab ist tt'') (delab ist t'')
904+reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
905+
906+-- | Reify terms from their reflected representation
907+reifyTT :: Term -> ElabD Term
908+reifyTT t@(App _ _)
909+ | (P _ f _, args) <- unApply t = reifyTTApp f args
910+reifyTT t@(P _ n _)
911+ | n == reflm "Erased" = return $ Erased
912+reifyTT t@(P _ n _)
913+ | n == reflm "Impossible" = return $ Impossible
914+reifyTT t = fail ("Unknown reflection term: " ++ show t)
915+
916+reifyTTApp :: Name -> [Term] -> ElabD Term
917+reifyTTApp t [nt, n, x]
918+ | t == reflm "P" = do nt' <- reifyTTNameType nt
919+ n' <- reifyTTName n
920+ x' <- reifyTT x
921+ return $ P nt' n' x'
922+reifyTTApp t [Constant (I i)]
923+ | t == reflm "V" = return $ V i
924+reifyTTApp t [n, b, x]
925+ | t == reflm "Bind" = do n' <- reifyTTName n
926+ b' <- reifyTTBinder reifyTT (reflm "TT") b
927+ x' <- reifyTT x
928+ return $ Bind n' b' x'
929+reifyTTApp t [f, x]
930+ | t == reflm "App" = do f' <- reifyTT f
931+ x' <- reifyTT x
932+ return $ App f' x'
933+reifyTTApp t [c]
934+ | t == reflm "TConst" = liftM Constant (reifyTTConst c)
935+reifyTTApp t [t', Constant (I i)]
936+ | t == reflm "Proj" = do t'' <- reifyTT t'
937+ return $ Proj t'' i
938+reifyTTApp t [tt]
939+ | t == reflm "TType" = liftM TType (reifyTTUExp tt)
940+reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
941+
942+-- | Reify raw terms from their reflected representation
943+reifyRaw :: Term -> ElabD Raw
944+reifyRaw t@(App _ _)
945+ | (P _ f _, args) <- unApply t = reifyRawApp f args
946+reifyRaw t@(P _ n _)
947+ | n == reflm "RType" = return $ RType
948+reifyRaw t = fail ("Unknown reflection raw term: " ++ show t)
949+
950+reifyRawApp :: Name -> [Term] -> ElabD Raw
951+reifyRawApp t [n]
952+ | t == reflm "Var" = liftM Var (reifyTTName n)
953+reifyRawApp t [n, b, x]
954+ | t == reflm "RBind" = do n' <- reifyTTName n
955+ b' <- reifyTTBinder reifyRaw (reflm "Raw") b
956+ x' <- reifyRaw x
957+ return $ RBind n' b' x'
958+reifyRawApp t [f, x]
959+ | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
960+reifyRawApp t [t']
961+ | t == reflm "RForce" = liftM RForce (reifyRaw t')
962+reifyRawApp t [c]
963+ | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
964+reifyRawApp t args = fail ("Unknown reflection raw term: " ++ show (t, args))
965+
966+reifyTTName :: Term -> ElabD Name
967+reifyTTName t@(App _ _)
968+ | (P _ f _, args) <- unApply t = reifyTTNameApp f args
969+reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
970+
971+reifyTTNameApp :: Name -> [Term] -> ElabD Name
972+reifyTTNameApp t [Constant (Str n)]
973+ | t == reflm "UN" = return $ UN n
974+reifyTTNameApp t [n, ns]
975+ | t == reflm "NS" = do n' <- reifyTTName n
976+ ns' <- reifyTTNamespace ns
977+ return $ NS n' ns'
978+reifyTTNameApp t [Constant (I i), Constant (Str n)]
979+ | t == reflm "MN" = return $ MN i n
980+reifyTTNameApp t []
981+ | t == reflm "NErased" = return NErased
982+reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
983+
984+reifyTTNamespace :: Term -> ElabD [String]
985+reifyTTNamespace t@(App _ _)
986+ = case unApply t of
987+ (P _ f _, [Constant StrType])
988+ | f == NS (UN "Nil") ["List", "Prelude"] -> return []
989+ (P _ f _, [Constant StrType, Constant (Str n), ns])
990+ | f == NS (UN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
991+ _ -> fail ("Unknown reflection namespace arg: " ++ show t)
992+reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
993+
994+reifyTTNameType :: Term -> ElabD NameType
995+reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
996+reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
997+reifyTTNameType t@(App _ _)
998+ = case unApply t of
999+ (P _ f _, [Constant (I tag), Constant (I num)])
1000+ | f == reflm "DCon" -> return $ DCon tag num
1001+ | f == reflm "TCon" -> return $ TCon tag num
1002+ _ -> fail ("Unknown reflection name type: " ++ show t)
1003+reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)
1004+
1005+reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
1006+reifyTTBinder reificator binderType t@(App _ _)
1007+ = case unApply t of
1008+ (P _ f _, bt:args) | forget bt == Var binderType
1009+ -> reifyTTBinderApp reificator f args
1010+ _ -> fail ("Mismatching binder reflection: " ++ show t)
1011+reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)
1012+
1013+reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
1014+reifyTTBinderApp reif f [t]
1015+ | f == reflm "Lam" = liftM Lam (reif t)
1016+reifyTTBinderApp reif f [t]
1017+ | f == reflm "Pi" = liftM Pi (reif t)
1018+reifyTTBinderApp reif f [x, y]
1019+ | f == reflm "Let" = liftM2 Let (reif x) (reif y)
1020+reifyTTBinderApp reif f [x, y]
1021+ | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
1022+reifyTTBinderApp reif f [t]
1023+ | f == reflm "Hole" = liftM Hole (reif t)
1024+reifyTTBinderApp reif f [t]
1025+ | f == reflm "GHole" = liftM GHole (reif t)
1026+reifyTTBinderApp reif f [x, y]
1027+ | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
1028+reifyTTBinderApp reif f [t]
1029+ | f == reflm "PVar" = liftM PVar (reif t)
1030+reifyTTBinderApp reif f [t]
1031+ | f == reflm "PVTy" = liftM PVTy (reif t)
1032+reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
1033+
1034+reifyTTConst :: Term -> ElabD Const
1035+reifyTTConst (P _ n _) | n == reflm "IType" = return $ IType
1036+reifyTTConst (P _ n _) | n == reflm "BIType" = return $ BIType
1037+reifyTTConst (P _ n _) | n == reflm "FlType" = return $ FlType
1038+reifyTTConst (P _ n _) | n == reflm "ChType" = return $ ChType
1039+reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
1040+reifyTTConst (P _ n _) | n == reflm "B8Type" = return $ B8Type
1041+reifyTTConst (P _ n _) | n == reflm "B16Type" = return $ B16Type
1042+reifyTTConst (P _ n _) | n == reflm "B32Type" = return $ B32Type
1043+reifyTTConst (P _ n _) | n == reflm "B64Type" = return $ B64Type
1044+reifyTTConst (P _ n _) | n == reflm "PtrType" = return $ PtrType
1045+reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
1046+reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
1047+reifyTTConst t@(App _ _)
1048+ | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg
1049+reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
1050+
1051+reifyTTConstApp :: Name -> Term -> ElabD Const
1052+reifyTTConstApp f (Constant c@(I _))
1053+ | f == reflm "I" = return $ c
1054+reifyTTConstApp f (Constant c@(BI _))
1055+ | f == reflm "BI" = return $ c
1056+reifyTTConstApp f (Constant c@(Fl _))
1057+ | f == reflm "Fl" = return $ c
1058+reifyTTConstApp f (Constant c@(I _))
1059+ | f == reflm "Ch" = return $ c
1060+reifyTTConstApp f (Constant c@(Str _))
1061+ | f == reflm "Str" = return $ c
1062+reifyTTConstApp f (Constant c@(B8 _))
1063+ | f == reflm "B8" = return $ c
1064+reifyTTConstApp f (Constant c@(B16 _))
1065+ | f == reflm "B16" = return $ c
1066+reifyTTConstApp f (Constant c@(B32 _))
1067+ | f == reflm "B32" = return $ c
1068+reifyTTConstApp f (Constant c@(B64 _))
1069+ | f == reflm "B64" = return $ c
1070+reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
1071+
1072+reifyTTUExp :: Term -> ElabD UExp
1073+reifyTTUExp t@(App _ _)
1074+ = case unApply t of
1075+ (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
1076+ (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
1077+ _ -> fail ("Unknown reflection type universe expression: " ++ show t)
1078+reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)
1079+
1080+-- | Create a reflected call to a named function/constructor
1081+reflCall :: String -> [Raw] -> Raw
1082+reflCall funName args
1083+ = raw_apply (Var (reflm funName)) args
1084+
1085+-- | Lift a term into its Language.Reflection.TT representation
1086+reflect :: Term -> Raw
1087+reflect (P nt n t)
1088+ = reflCall "P" [reflectNameType nt, reflectName n, reflect t]
1089+reflect (V n)
1090+ = reflCall "V" [RConstant (I n)]
1091+reflect (Bind n b x)
1092+ = reflCall "Bind" [reflectName n, reflectBinder b, reflect x]
1093+reflect (App f x)
1094+ = reflCall "App" [reflect f, reflect x]
1095+reflect (Constant c)
1096+ = reflCall "TConst" [reflectConstant c]
1097+reflect (Proj t i)
1098+ = reflCall "Proj" [reflect t, RConstant (I i)]
1099+reflect (Erased) = Var (reflm "Erased")
1100+reflect (Impossible) = Var (reflm "Impossible")
1101+reflect (TType exp) = reflCall "TType" [reflectUExp exp]
1102+
1103+reflectNameType :: NameType -> Raw
1104+reflectNameType (Bound) = Var (reflm "Bound")
1105+reflectNameType (Ref) = Var (reflm "Ref")
1106+reflectNameType (DCon x y)
1107+ = reflCall "DCon" [RConstant (I x), RConstant (I y)]
1108+reflectNameType (TCon x y)
1109+ = reflCall "TCon" [RConstant (I x), RConstant (I y)]
1110+
1111+reflectName :: Name -> Raw
1112+reflectName (UN str)
1113+ = reflCall "UN" [RConstant (Str str)]
1114+reflectName (NS n ns)
1115+ = reflCall "NS" [ reflectName n
1116+ , foldr (\ n s ->
1117+ raw_apply ( Var $ NS (UN "::") ["List", "Prelude"] )
1118+ [ RConstant StrType, RConstant (Str n), s ])
1119+ ( raw_apply ( Var $ NS (UN "Nil") ["List", "Prelude"] )
1120+ [ RConstant StrType ])
1121+ ns
1122+ ]
1123+reflectName (MN i n)
1124+ = reflCall "MN" [RConstant (I i), RConstant (Str n)]
1125+reflectName (NErased) = Var (reflm "NErased")
1126+
1127+reflectBinder :: Binder Term -> Raw
1128+reflectBinder (Lam t)
1129+ = reflCall "Lam" [Var (reflm "TT"), reflect t]
1130+reflectBinder (Pi t)
1131+ = reflCall "Pi" [Var (reflm "TT"), reflect t]
1132+reflectBinder (Let x y)
1133+ = reflCall "Let" [Var (reflm "TT"), reflect x, reflect y]
1134+reflectBinder (NLet x y)
1135+ = reflCall "NLet" [Var (reflm "TT"), reflect x, reflect y]
1136+reflectBinder (Hole t)
1137+ = reflCall "Hole" [Var (reflm "TT"), reflect t]
1138+reflectBinder (GHole t)
1139+ = reflCall "GHole" [Var (reflm "TT"), reflect t]
1140+reflectBinder (Guess x y)
1141+ = reflCall "Guess" [Var (reflm "TT"), reflect x, reflect y]
1142+reflectBinder (PVar t)
1143+ = reflCall "PVar" [Var (reflm "TT"), reflect t]
1144+reflectBinder (PVTy t)
1145+ = reflCall "PVTy" [Var (reflm "TT"), reflect t]
1146+
1147+reflectConstant :: Const -> Raw
1148+reflectConstant c@(I _) = reflCall "I" [RConstant c]
1149+reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
1150+reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
1151+reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
1152+reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
1153+reflectConstant (IType) = Var (reflm "IType")
1154+reflectConstant (BIType) = Var (reflm "BIType")
1155+reflectConstant (FlType) = Var (reflm "FlType")
1156+reflectConstant (ChType) = Var (reflm "ChType")
1157+reflectConstant (StrType) = Var (reflm "StrType")
1158+reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
1159+reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
1160+reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
1161+reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
1162+reflectConstant (B8Type) = Var (reflm "B8Type")
1163+reflectConstant (B16Type) = Var (reflm "B16Type")
1164+reflectConstant (B32Type) = Var (reflm "B32Type")
1165+reflectConstant (B64Type) = Var (reflm "B64Type")
1166+reflectConstant (PtrType) = Var (reflm "PtrType")
1167+reflectConstant (VoidType) = Var (reflm "VoidType")
1168+reflectConstant (Forgot) = Var (reflm "Forgot")
1169+
1170+reflectUExp :: UExp -> Raw
1171+reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
1172+reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
1173+
1174+-- | Reflect the environment of a proof into a List (TTName, Binder TT)
1175+reflectEnv :: Env -> Raw
1176+reflectEnv = foldr consToEnvList emptyEnvList
1177+ where
1178+ consToEnvList :: (Name, Binder Term) -> Raw -> Raw
1179+ consToEnvList (n, b) l
1180+ = raw_apply (Var (NS (UN "::") ["List", "Prelude"]))
1181+ [ envTupleType
1182+ , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
1183+ , (RApp (Var $ reflm "Binder")
1184+ (Var $ reflm "TT"))
1185+ , reflectName n
1186+ , reflectBinder b
1187+ ]
1188+ , l
1189+ ]
1190+
1191+ emptyEnvList :: Raw
1192+ emptyEnvList = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"]))
1193+ [envTupleType]
1194+
1195+envTupleType :: Raw
1196+envTupleType
1197+ = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
1198+ , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
1199+ ]
8181200
8191201solveAll = try (do solve; solveAll) (return ())
8201202
src/Idris/IBC.hs+11−3
@@ -1390,8 +1390,12 @@ instance (Binary t) => Binary (PTactic' t) where
13901390 put x1
13911391 put x2
13921392 Qed -> putWord8 15
1393− ReflectTac x1 -> do putWord8 16
1394− put x1
1393+ ApplyTactic x1 -> do putWord8 16
1394+ put x1
1395+ Reflect x1 -> do putWord8 17
1396+ put x1
1397+ Fill x1 -> do putWord8 18
1398+ put x1
13951399 get
13961400 = do i <- getWord8
13971401 case i of
@@ -1424,7 +1428,11 @@ instance (Binary t) => Binary (PTactic' t) where
14241428 return (TSeq x1 x2)
14251429 15 -> return Qed
14261430 16 -> do x1 <- get
1427− return (ReflectTac x1)
1431+ return (ApplyTactic x1)
1432+ 17 -> do x1 <- get
1433+ return (Reflect x1)
1434+ 18 -> do x1 <- get
1435+ return (Fill x1)
14281436 _ -> error "Corrupted binary data for PTactic'"
14291437
14301438
src/Idris/Parser.hs+7−1
@@ -1537,9 +1537,15 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
15371537 <|> do reserved "exact"; t <- pExpr syn;
15381538 i <- getState
15391539 return $ Exact (desugar syn i t)
1540+ <|> do reserved "applyTactic"; t <- pExpr syn;
1541+ i <- getState
1542+ return $ ApplyTactic (desugar syn i t)
15401543 <|> do reserved "reflect"; t <- pExpr syn;
15411544 i <- getState
1542− return $ ReflectTac (desugar syn i t)
1545+ return $ Reflect (desugar syn i t)
1546+ <|> do reserved "fill"; t <- pExpr syn;
1547+ i <- getState
1548+ return $ Fill (desugar syn i t)
15431549 <|> do reserved "try"; t <- pTactic syn;
15441550 lchar '|';
15451551 t1 <- pTactic syn