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

git.iko.soy/Idris-dev

on master help sign in

Add syntax for transformation rules

6f88ecdEdwin Brady13 years ago

src/Idris/AbsSyntax.hs+4

compare with master

unifiedsplit

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

61addLangExt :: LanguageExt -> Idris ()

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

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

65+addTrans t = do i <- getIState

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

67+

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

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

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

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

src/Idris/AbsSyntaxTree.hs+5−1

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

97 idris_name :: Int,

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

99 idris_coercions :: [Name],

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

100 syntax_rules :: [Syntax],

101 syntax_rules :: [Syntax],

101 syntax_keywords :: [String],

102 syntax_keywords :: [String],

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

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

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

158 | IBCAccess Name Accessibility

159 | IBCAccess Name Accessibility

159 | IBCTotal Name Totality

160 | IBCTotal Name Totality

160 | IBCFlags Name [FnOpt]

161 | IBCFlags Name [FnOpt]

162+ | IBCTrans (Term, Term)

161 | IBCCG Name

163 | IBCCG Name

162 | IBCDoc Name

164 | IBCDoc Name

163 | IBCCoercion Name

165 | IBCCoercion Name

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

167idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

169idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

168 emptyContext emptyContext emptyContext emptyContext

170 emptyContext emptyContext emptyContext emptyContext

169 emptyContext emptyContext emptyContext emptyContext

171 emptyContext emptyContext emptyContext emptyContext

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

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

171 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

173 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

172

174

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

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

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

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

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

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

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

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

379 | 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

378 | PReflection FC Name -- type to reflect to

382 | PReflection FC Name -- type to reflect to

379 t -- type of variables

383 t -- type of variables

380 [PClause' t] -- ^ Pattern clauses

384 [PClause' t] -- ^ Pattern clauses

src/Idris/ElabDecls.hs+35

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

298 , tp == tp' = True

299 isProviderOf _ _ = False

300

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+

301

334

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

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

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

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

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

1416 | what /= EDefns

1449 | what /= EDefns

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

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

1418 elabProvider info syn fc n tp tm

1451 elabProvider info syn fc n tp tm

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

1453+ = elabTransform info fc safety old new

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

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

1420

1455

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

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

src/Idris/IBC.hs+12−4

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

24import Paths_idris

26ibcVersion :: Word8

27−ibcVersion = 31

27+ibcVersion = 32

29data IBCFile = IBCFile { ver :: Word8,

30 sourcefile :: FilePath,

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

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

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

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

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

52 ibc_coercions :: [Name]

53 ibc_coercions :: [Name]

53 }

54 }

54 deriving Show

55 deriving Show

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

57!-}

58!-}

59initIBC :: IBCFile

60initIBC :: IBCFile

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

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

62loadIBC :: FilePath -> Idris ()

63loadIBC :: FilePath -> Idris ()

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

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

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

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

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

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

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

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

133ibc 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 }

133

135

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

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

135process i fn

137process i fn

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

162 pCG (ibc_cg i)

164 pCG (ibc_cg i)

163 pDocs (ibc_docstrings i)

165 pDocs (ibc_docstrings i)

164 pCoercions (ibc_coercions i)

166 pCoercions (ibc_coercions i)

167+ pTrans (ibc_transforms i)

165

168

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

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

167timestampOlder src ibc = do srct <- getModificationTime src

170timestampOlder src ibc = do srct <- getModificationTime src

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

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

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

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

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

293

296

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

298+pTrans ts = mapM_ addTrans ts

299+

294----- Generated by 'derive'

300----- Generated by 'derive'

295

301

296instance Binary SizeChange where

302instance Binary SizeChange where

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

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

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

782

788

783instance Binary IBCFile where

789instance 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)

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

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

786 do put x1

792 do put x1

787 put x2

793 put x2

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

807 put x22

813 put x22

808 put x23

814 put x23

809 put x24

815 put x24

816+ put x25

810 get

817 get

811 = do x1 <- get

818 = do x1 <- get

812 if x1 == ibcVersion then

819 if x1 == ibcVersion then

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

833 x22 <- get

840 x22 <- get

834 x23 <- get

841 x23 <- get

835 x24 <- get

842 x24 <- get

843+ x25 <- 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)

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)

837 else return (initIBC { ver = x1 })

845 else return (initIBC { ver = x1 })

838

846

839instance Binary FnOpt where

847instance Binary FnOpt where

src/Idris/Parser.hs+14−1

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

344 <|> pInstance syn

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

346 <|> pDirective syn

347− <|> pProvider syn

347+ <|> try (pProvider syn)

348+ <|> pTransform syn

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

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

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

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

350

351

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

1604 e <- pExpr syn

1605 e <- pExpr syn

1605 return [PProvider syn fc n t e]

1606 return [PProvider syn fc n t e]

1606

1607

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+

1607pTactic :: SyntaxInfo -> IParser PTactic

1620pTactic :: SyntaxInfo -> IParser PTactic

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

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

1609 return $ Intro ns

1622 return $ Intro ns