6f88ecd · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add syntax for transformation rules

%transform lhs ==> rhs Unbound names on the lhs are treated as patterns. Transformation behaviour not yet implemented.

commit6f88ecd9afb220a794397916df463187923938d6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 26 Jul 2013, 14:33 (13 years ago) parentadf646e

5 files changed+70−6

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+4 src/Idris/AbsSyntaxTree.hs+5−1 src/Idris/ElabDecls.hs+35 src/Idris/IBC.hs+12−4 src/Idris/Parser.hs+14−1

src/Idris/AbsSyntax.hs+4

@@ -61,6 +61,10 @@ addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = (tgt, f) : idris_

6161addLangExt :: LanguageExt -> Idris ()

6262addLangExt TypeProviders = do i <- getIState ; putIState $ i { idris_language_extensions = [TypeProviders] }

6363

64+addTrans :: (Term, Term) -> Idris ()

65+addTrans t = do i <- getIState

66+ putIState $ i { idris_transforms = t : idris_transforms i }

67+

6468totcheck :: (FC, Name) -> Idris ()

6569totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

6670

src/Idris/AbsSyntaxTree.hs+5−1

@@ -97,6 +97,7 @@ data IState = IState {

9797 idris_name :: Int,

9898 idris_metavars :: [Name], -- ^ The currently defined but not proven metavariables

9999 idris_coercions :: [Name],

100+ idris_transforms :: [(Term, Term)],

100101 syntax_rules :: [Syntax],

101102 syntax_keywords :: [String],

102103 imported :: [FilePath], -- ^ The imported modules

@@ -158,6 +159,7 @@ data IBCWrite = IBCFix FixDecl

158159 | IBCAccess Name Accessibility

159160 | IBCTotal Name Totality

160161 | IBCFlags Name [FnOpt]

162+ | IBCTrans (Term, Term)

161163 | IBCCG Name

162164 | IBCDoc Name

163165 | IBCCoercion Name

@@ -167,7 +169,7 @@ data IBCWrite = IBCFix FixDecl

167169idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

168170 emptyContext emptyContext emptyContext emptyContext

169171 emptyContext emptyContext emptyContext emptyContext

170− [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

172+ [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] []

171173 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

172174

173175-- | The monad for the main REPL - reading and processing files and updating

@@ -375,6 +377,8 @@ data PDecl' t

375377 | PMutual FC [PDecl' t] -- ^ Mutual block

376378 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

377379 | PProvider SyntaxInfo FC Name t t -- ^ Type provider. The first t is the type, the second is the term

380+ | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

381+ -- bool is True, lhs and rhs must be convertible

378382 | PReflection FC Name -- type to reflect to

379383 t -- type of variables

380384 [PClause' t] -- ^ Pattern clauses

src/Idris/ElabDecls.hs+35

@@ -298,6 +298,39 @@ elabProvider info syn fc n ty tm

298298 , tp == tp' = True

299299 isProviderOf _ _ = False

300300

301+-- | Elaborate a type provider

302+elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()

303+elabTransform info fc safe lhs_in rhs_in

304+ = do ctxt <- getContext

305+ i <- getIState

306+ let lhs = addImplPat i lhs_in

307+ ((lhs', dlhs, []), _) <-

308+ tclift $ elaborate ctxt (MN 0 "transLHS") infP []

309+ (erun fc (buildTC i info True False (UN "transform")

310+ (infTerm lhs)))

311+ let lhs_tm = orderPats (getInferTerm lhs')

312+ let lhs_ty = getInferType lhs'

313+ let newargs = pvars i lhs_tm

314+

315+ (clhs_tm, clhs_ty) <- recheckC fc [] lhs_tm

316+ logLvl 3 ("Transform LHS " ++ show clhs_tm)

317+ let rhs = addImplBound i (map fst newargs) rhs_in

318+ ((rhs', defer), _) <-

319+ tclift $ elaborate ctxt (MN 0 "transRHS") clhs_ty []

320+ (do pbinds lhs_tm

321+ erun fc (build i info False (UN "transform") rhs)

322+ erun fc $ psolve lhs_tm

323+ tt <- get_term

324+ let (tm, ds) = runState (collectDeferred tt) []

325+ return (tm, ds))

326+ (crhs_tm, crhs_ty) <- recheckC fc [] rhs'

327+ logLvl 3 ("Transform RHS " ++ show crhs_tm)

328+ when safe $ case converts ctxt [] clhs_tm crhs_tm of

329+ OK _ -> return ()

330+ Error e -> ierror (At fc (CantUnify False clhs_tm crhs_tm e [] 0))

331+ addTrans (clhs_tm, crhs_tm)

332+ addIBC (IBCTrans (clhs_tm, crhs_tm))

333+

301334

302335elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

303336 PTerm -> String -> Name -> PTerm -> Idris ()

@@ -1416,6 +1449,8 @@ elabDecl' what info (PProvider syn fc n tp tm)

14161449 | what /= EDefns

14171450 = do iLOG $ "Elaborating type provider " ++ show n

14181451 elabProvider info syn fc n tp tm

1452+elabDecl' what info (PTransform fc safety old new)

1453+ = elabTransform info fc safety old new

14191454elabDecl' _ _ _ = return () -- skipped this time

14201455

14211456elabCaseBlock info d@(PClauses f o n ps)

src/Idris/IBC.hs+12−4

@@ -24,7 +24,7 @@ import Debug.Trace

2424import Paths_idris

2525

2626ibcVersion :: Word8

27−ibcVersion = 31

27+ibcVersion = 32

2828

2929data IBCFile = IBCFile { ver :: Word8,

3030 sourcefile :: FilePath,

@@ -49,6 +49,7 @@ data IBCFile = IBCFile { ver :: Word8,

4949 ibc_cg :: [(Name, CGInfo)],

5050 ibc_defs :: [(Name, Def)],

5151 ibc_docstrings :: [(Name, String)],

52+ ibc_transforms :: [(Term, Term)],

5253 ibc_coercions :: [Name]

5354 }

5455 deriving Show

@@ -57,7 +58,7 @@ deriving instance Binary IBCFile

5758!-}

5859

5960initIBC :: IBCFile

60−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

61+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

6162

6263loadIBC :: FilePath -> Idris ()

6364loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -130,6 +131,7 @@ ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }

130131ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

131132ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

132133ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

134+ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }

133135

134136process :: IBCFile -> FilePath -> Idris ()

135137process i fn

@@ -162,6 +164,7 @@ process i fn

162164 pCG (ibc_cg i)

163165 pDocs (ibc_docstrings i)

164166 pCoercions (ibc_coercions i)

167+ pTrans (ibc_transforms i)

165168

166169timestampOlder :: FilePath -> FilePath -> IO ()

167170timestampOlder src ibc = do srct <- getModificationTime src

@@ -291,6 +294,9 @@ pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds

291294pCoercions :: [Name] -> Idris ()

292295pCoercions ns = mapM_ (\ n -> addCoercion n) ns

293296

297+pTrans :: [(Term, Term)] -> Idris ()

298+pTrans ts = mapM_ addTrans ts

299+

294300----- Generated by 'derive'

295301

296302instance Binary SizeChange where

@@ -781,7 +787,7 @@ instance Binary Totality where

781787 _ -> error "Corrupted binary data for Totality"

782788

783789instance Binary IBCFile where

784− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24)

790+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25)

785791 = {-# SCC "putIBCFile" #-}

786792 do put x1

787793 put x2

@@ -807,6 +813,7 @@ instance Binary IBCFile where

807813 put x22

808814 put x23

809815 put x24

816+ put x25

810817 get

811818 = do x1 <- get

812819 if x1 == ibcVersion then

@@ -833,7 +840,8 @@ instance Binary IBCFile where

833840 x22 <- get

834841 x23 <- get

835842 x24 <- get

836− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24)

843+ x25 <- get

844+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25)

837845 else return (initIBC { ver = x1 })

838846

839847instance Binary FnOpt where

src/Idris/Parser.hs+14−1

@@ -344,7 +344,8 @@ pDecl syn = do notEndBlock

344344 <|> pInstance syn

345345 <|> do d <- pDSL syn; return [d]

346346 <|> pDirective syn

347− <|> pProvider syn

347+ <|> try (pProvider syn)

348+ <|> pTransform syn

348349 <|> try (do reserved "import"; fp <- identifier

349350 fail "imports must be at the top of file")

350351

@@ -1604,6 +1605,18 @@ pProvider syn = do lchar '%'; reserved "provide";

16041605 e <- pExpr syn

16051606 return [PProvider syn fc n t e]

16061607

1608+pTransform :: SyntaxInfo -> IParser [PDecl]

1609+pTransform syn = do lchar '%'; reserved "transform";

1610+ -- leave it unchecked, until we work out what this should

1611+ -- actually mean...

1612+-- safety <- option True (do reserved "unsafe"

1613+-- return False)

1614+ lhs <- pExpr syn

1615+ fc <- pfc

1616+ symbol "==>"

1617+ rhs <- pExpr syn

1618+ return [PTransform fc False lhs rhs]

1619+

16071620pTactic :: SyntaxInfo -> IParser PTactic

16081621pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

16091622 return $ Intro ns