edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-10-26 17:33:47 +03:00
Code Issues Projects Releases Wiki Activity

Begin elaboration of quoting terms

Browse Source
This commit is contained in:
Edwin Brady 2019-11-30 15:26:17 +00:00
parent aae3d0f718
commit 07509f6103
10 changed files with 125 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
idris2.ipkg
View File

@ -95,6 +95,7 @@ modules =
TTImp.Elab.Lazy,
TTImp.Elab.Local,
TTImp.Elab.Prim,
TTImp.Elab.Quote,
TTImp.Elab.Record,
TTImp.Elab.Rewrite,
TTImp.Elab.Term,

5
libs/base/Language/Reflection/TTImp.idr
View File

@ -51,6 +51,11 @@ mutual
IDelay : FC -> TTImp -> TTImp -- delay constructor
IForce : FC -> TTImp -> TTImp
-- Quasiquotation
IQuote : FC -> TTImp -> TTImp
IQuoteDecl : FC -> TTImp -> TTImp
IUnquote : FC -> TTImp -> TTImp
IPrimVal : FC -> (c : Constant) -> TTImp
IType : FC -> TTImp
IHole : FC -> String -> TTImp

2
src/Core/Binary.idr
View File

@ -27,7 +27,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 10
ttcVersion = 11
export
checkTTCVersion : Int -> Int -> Core ()

14
src/Idris/Desugar.idr
View File

@ -203,12 +203,14 @@ mutual
Just f => pure $ IApp fc (IVar fc f)
(IPrimVal fc (Ch x))
desugar side ps (PPrimVal fc x) = pure $ IPrimVal fc x
desugar side ps (PQuote fc x)
= throw (GenericMsg fc "Reflection not implemeted yet")
-- = pure $ IQuote fc !(desugar side ps x)
desugar side ps (PUnquote fc x)
= throw (GenericMsg fc "Reflection not implemeted yet")
-- = pure $ IUnquote fc !(desugar side ps x)
desugar side ps (PQuote fc tm)
= pure $ IQuote fc !(desugar side ps tm)
desugar side ps (PQuoteDecl fc x)
= do [x'] <- desugarDecl ps x
| _ => throw (GenericMsg fc "Can't quote this declaration")
pure $ IQuoteDecl fc x'
desugar side ps (PUnquote fc tm)
= pure $ IUnquote fc !(desugar side ps tm)
desugar side ps (PHole fc br holename)
= do when br $
do syn <- get Syn

7
src/Idris/Resugar.idr
View File

@ -214,6 +214,13 @@ mutual
toPTerm p (IDelayed fc r ty) = pure (PDelayed fc r !(toPTerm argPrec ty))
toPTerm p (IDelay fc tm) = pure (PDelay fc !(toPTerm argPrec tm))
toPTerm p (IForce fc tm) = pure (PForce fc !(toPTerm argPrec tm))
toPTerm p (IQuote fc tm) = pure (PQuote fc !(toPTerm argPrec tm))
toPTerm p (IQuoteDecl fc d)
= do md <- toPDecl d
case md of
Nothing => throw (InternalError "Can't resugar log or pragma")
Just d' => pure (PQuoteDecl fc d')
toPTerm p (IUnquote fc tm) = pure (PUnquote fc !(toPTerm argPrec tm))
toPTerm p (Implicit fc True) = pure (PImplicit fc)
toPTerm p (Implicit fc False) = pure (PInfer fc)

2
src/Idris/Syntax.idr
View File

@ -55,6 +55,7 @@ mutual
PSearch : FC -> (depth : Nat) -> PTerm
PPrimVal : FC -> Constant -> PTerm
PQuote : FC -> PTerm -> PTerm
PQuoteDecl : FC -> PDecl -> PTerm
PUnquote : FC -> PTerm -> PTerm
PHole : FC -> (bracket : Bool) -> (holename : String) -> PTerm
PType : FC -> PTerm
@ -394,6 +395,7 @@ mutual
= showPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d a ++ "}"
showPrec _ (PSearch _ _) = "%search"
showPrec d (PQuote _ tm) = "`(" ++ showPrec d tm ++ ")"
showPrec d (PQuoteDecl _ tm) = "`( <<declaration>> )"
showPrec d (PUnquote _ tm) = "~(" ++ showPrec d tm ++ ")"
showPrec d (PPrimVal _ c) = showPrec d c
showPrec _ (PHole _ _ n) = "?" ++ n

33
src/TTImp/Elab/Quote.idr Normal file
View File

@ -0,0 +1,33 @@
module TTImp.Elab.Quote
import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.Reflect
import Core.Unify
import Core.TT
import Core.Value
import TTImp.Elab.Check
import TTImp.Reflect
import TTImp.TTImp
%default covering
export
checkQuote : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
{auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> RawImp -> Maybe (Glued vars) ->
Core (Term vars, Glued vars)
checkQuote rig elabinfo nest env fc tm exp
= do defs <- get Ctxt
tm <- reflect fc defs env tm
ty <- getCon fc defs (reflectionttimp "TTImp")
checkExp rig elabinfo env fc tm (gnf env ty) exp

7
src/TTImp/Elab/Term.idr
View File

@ -22,6 +22,7 @@ import TTImp.Elab.ImplicitBind
import TTImp.Elab.Lazy
import TTImp.Elab.Local
import TTImp.Elab.Prim
import TTImp.Elab.Quote
import TTImp.Elab.Record
import TTImp.Elab.Rewrite
import TTImp.Reflect
@ -151,6 +152,12 @@ checkTerm rig elabinfo nest env (IDelay fc tm) exp
= checkDelay rig elabinfo nest env fc tm exp
checkTerm rig elabinfo nest env (IForce fc tm) exp
= checkForce rig elabinfo nest env fc tm exp
checkTerm rig elabinfo nest env (IQuote fc tm) exp
= checkQuote rig elabinfo nest env fc tm exp
checkTerm rig elabinfo nest env (IQuoteDecl fc tm) exp
= throw (GenericMsg fc "Reflection not implemented yet")
checkTerm rig elabinfo nest env (IUnquote fc tm) exp
= throw (InternalError "Unquote should have been resolved")
checkTerm {vars} rig elabinfo nest env (IPrimVal fc c) exp
= do let (cval, cty) = checkPrim {vars} fc c
checkExp rig elabinfo env fc cval (gnf env cty) exp

24
src/TTImp/Reflect.idr
View File

@ -157,6 +157,18 @@ mutual
= do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
pure (IForce fc' t')
reify defs (NDCon _ (NS _ (UN "IQuote")) _ _ [fc, t])
= do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
pure (IQuote fc' t')
reify defs (NDCon _ (NS _ (UN "IQuoteDecl")) _ _ [fc, t])
= do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
pure (IQuoteDecl fc' t')
reify defs (NDCon _ (NS _ (UN "IUnquote")) _ _ [fc, t])
= do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
pure (IUnquote fc' t')
reify defs (NDCon _ (NS _ (UN "IPrimVal")) _ _ [fc, t])
= do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
@ -455,6 +467,18 @@ mutual
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t
appCon fc defs (reflectionttimp "IForce") [fc', t']
reflect fc defs env (IQuote tfc t)
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t
appCon fc defs (reflectionttimp "IQuote") [fc', t']
reflect fc defs env (IQuoteDecl tfc t)
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t
appCon fc defs (reflectionttimp "IQuoteDecl") [fc', t']
reflect fc defs env (IUnquote tfc t)
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t
appCon fc defs (reflectionttimp "IUnquote") [fc', t']
reflect fc defs env (IPrimVal tfc t)
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t

45
src/TTImp/TTImp.idr
View File

@ -82,6 +82,11 @@ mutual
IDelay : FC -> RawImp -> RawImp -- delay constructor
IForce : FC -> RawImp -> RawImp
-- Quasiquoting
IQuote : FC -> RawImp -> RawImp
IQuoteDecl : FC -> ImpDecl -> RawImp
IUnquote : FC -> RawImp -> RawImp
IPrimVal : FC -> (c : Constant) -> RawImp
IType : FC -> RawImp
IHole : FC -> String -> RawImp
@ -143,6 +148,9 @@ mutual
show (IDelayed fc r tm) = "(%delayed " ++ show tm ++ ")"
show (IDelay fc tm) = "(%delay " ++ show tm ++ ")"
show (IForce fc tm) = "(%force " ++ show tm ++ ")"
show (IQuote fc tm) = "(%quote " ++ show tm ++ ")"
show (IQuoteDecl fc tm) = "(%quotedecl " ++ show tm ++ ")"
show (IUnquote fc tm) = "(%unquote " ++ show tm ++ ")"
show (IPrimVal fc c) = show c
show (IHole _ x) = "?" ++ x
show (IType fc) = "%type"
@ -369,6 +377,8 @@ findIBinds (IAlternative fc u alts)
findIBinds (IDelayed fc _ ty) = findIBinds ty
findIBinds (IDelay fc tm) = findIBinds tm
findIBinds (IForce fc tm) = findIBinds tm
findIBinds (IQuote fc tm) = findIBinds tm
findIBinds (IUnquote fc tm) = findIBinds tm
findIBinds (IBindHere _ _ tm) = findIBinds tm
findIBinds (IBindVar _ n) = [n]
-- We've skipped lambda, case, let and local - rather than guess where the
@ -398,6 +408,8 @@ findImplicits (IAlternative fc u alts)
findImplicits (IDelayed fc _ ty) = findImplicits ty
findImplicits (IDelay fc tm) = findImplicits tm
findImplicits (IForce fc tm) = findImplicits tm
findImplicits (IQuote fc tm) = findImplicits tm
findImplicits (IUnquote fc tm) = findImplicits tm
findImplicits (IBindVar _ n) = [n]
findImplicits tm = []
@ -514,6 +526,9 @@ getFC (IMustUnify x _ _) = x
getFC (IDelayed x _ _) = x
getFC (IDelay x _) = x
getFC (IForce x _) = x
getFC (IQuote x _) = x
getFC (IQuoteDecl x _) = x
getFC (IUnquote x _) = x
getFC (IAs x _ _ _) = x
getFC (Implicit x _) = x
@ -582,15 +597,22 @@ mutual
toBuf b (IForce fc t)
= do tag 20; toBuf b fc; toBuf b t
toBuf b (IQuote fc t)
= do tag 21; toBuf b fc; toBuf b t
toBuf b (IQuoteDecl fc t)
= do tag 22; toBuf b fc; toBuf b t
toBuf b (IUnquote fc t)
= do tag 23; toBuf b fc; toBuf b t
toBuf b (IPrimVal fc y)
= do tag 21; toBuf b fc; toBuf b y
= do tag 24; toBuf b fc; toBuf b y
toBuf b (IType fc)
= do tag 22; toBuf b fc
= do tag 25; toBuf b fc
toBuf b (IHole fc y)
= do tag 23; toBuf b fc; toBuf b y
= do tag 26; toBuf b fc; toBuf b y
toBuf b (Implicit fc i)
= do tag 24; toBuf b fc; toBuf b i
= do tag 27; toBuf b fc; toBuf b i
fromBuf b
= case !getTag of
@ -658,12 +680,19 @@ mutual
pure (IForce fc y)
21 => do fc <- fromBuf b; y <- fromBuf b
pure (IPrimVal fc y)
22 => do fc <- fromBuf b
pure (IType fc)
pure (IQuote fc y)
22 => do fc <- fromBuf b; y <- fromBuf b
pure (IQuoteDecl fc y)
23 => do fc <- fromBuf b; y <- fromBuf b
pure (IUnquote fc y)
24 => do fc <- fromBuf b; y <- fromBuf b
pure (IPrimVal fc y)
25 => do fc <- fromBuf b
pure (IType fc)
26 => do fc <- fromBuf b; y <- fromBuf b
pure (IHole fc y)
24 => do fc <- fromBuf b
27 => do fc <- fromBuf b
i <- fromBuf b
pure (Implicit fc i)
_ => corrupt "RawImp"