fe6b072 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2192 from melted/directive

fe6b072Niklas Larsson12 years ago

idris.cabal+1

compare with master

unifiedsplit

@@ -771,6 +771,7 @@ Library

771 , Idris.DataOpts

772 , Idris.DeepSeq

773 , Idris.Delaborate

774+ , Idris.Directives

774 , Idris.Docs

775 , Idris.Docs

775 , Idris.Docstrings

776 , Idris.Docstrings

776 , Idris.ElabDecls

777 , Idris.ElabDecls

src/Idris/AbsSyntaxTree.hs+17−1

@@ -628,7 +628,7 @@ data PDecl' t

628 | PDSL Name (DSL' t) -- ^ DSL declaration

629 | PSyntax FC Syntax -- ^ Syntax definition

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

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

631+ | PDirective Directive -- ^ Compiler directive.

632 | PProvider (Docstring (Either Err PTerm)) SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term

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

634 -- bool is True, lhs and rhs must be convertible

@@ -638,6 +638,22 @@ deriving instance Binary PDecl'

638deriving instance NFData PDecl'

639!-}

640

641+-- | The set of source directives

642+data Directive = DLib Codegen String |

643+ DLink Codegen String |

644+ DFlag Codegen String |

645+ DInclude Codegen String |

646+ DHide Name |

647+ DFreeze Name |

648+ DAccess Accessibility |

649+ DDefault Bool |

650+ DLogging Integer |

651+ DDynamicLibs [String] |

652+ DNameHint Name [Name] |

653+ DErrorHandlers Name Name [Name] |

654+ DLanguage LanguageExt |

655+ DUsed FC Name Name

656+

641-- | A set of instructions for things that need to happen in IState

657-- | A set of instructions for things that need to happen in IState

642-- after a term elaboration when there's been reflected elaboration.

658-- after a term elaboration when there's been reflected elaboration.

643data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

659data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

src/Idris/Directives.hsnew file+65

@@ -0,0 +1,65 @@

2+module Idris.Directives where

4+import Idris.AbsSyntax

5+import Idris.ASTUtils

6+import Idris.Imports

8+import Idris.Core.Evaluate

9+import Idris.Core.TT

10+

11+import Util.DynamicLinker

12+

13+-- | Run the action corresponding to a directive

14+directiveAction :: Directive -> Idris ()

15+directiveAction (DLib cgn lib) = do addLib cgn lib

16+ addIBC (IBCLib cgn lib)

17+

18+directiveAction (DLink cgn obj) = do dirs <- allImportDirs

19+ o <- runIO $ findInPath dirs obj

20+ addIBC (IBCObj cgn obj) -- just name, search on loading ibc

21+ addObjectFile cgn o

22+

23+directiveAction (DFlag cgn flag) = do addIBC (IBCCGFlag cgn flag)

24+ addFlag cgn flag

25+

26+directiveAction (DInclude cgn hdr) = do addHdr cgn hdr

27+ addIBC (IBCHeader cgn hdr)

28+

29+directiveAction (DHide n) = do setAccessibility n Hidden

30+ addIBC (IBCAccess n Hidden)

31+

32+directiveAction (DFreeze n) = do setAccessibility n Frozen

33+ addIBC (IBCAccess n Frozen)

34+

35+directiveAction (DAccess acc) = do updateIState (\i -> i { default_access = acc })

36+

37+directiveAction (DDefault tot) = do updateIState (\i -> i { default_total = tot })

38+

39+directiveAction (DLogging lvl) = setLogLevel (fromInteger lvl)

40+

41+directiveAction (DDynamicLibs libs) = do added <- addDyLib libs

42+ case added of

43+ Left lib -> addIBC (IBCDyLib (lib_name lib))

44+ Right msg -> fail $ msg

45+

46+directiveAction (DNameHint ty ns) = do ty' <- disambiguate ty

47+ mapM_ (addNameHint ty') ns

48+ mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns

49+

50+directiveAction (DErrorHandlers fn arg ns) = do fn' <- disambiguate fn

51+ ns' <- mapM disambiguate ns

52+ addFunctionErrorHandlers fn' arg ns'

53+ mapM_ (addIBC .

54+ IBCFunctionErrorHandler fn' arg) ns'

55+

56+directiveAction (DLanguage ext) = addLangExt ext

57+

58+directiveAction (DUsed fc fn arg) = addUsedName fc fn arg

59+

60+disambiguate :: Name -> Idris Name

61+disambiguate n = do i <- getIState

62+ case lookupCtxtName n (idris_implicits i) of

63+ [(n', _)] -> return n'

64+ [] -> throwError (NoSuchVariable n)

65+ more -> throwError (CantResolveAlts (map fst more))

src/Idris/ElabDecls.hs+2−1

@@ -8,6 +8,7 @@ import Idris.ASTUtils

8import Idris.DSL

9import Idris.Error

10import Idris.Delaborate

11+import Idris.Directives

11import Idris.Imports

12import Idris.Imports

12import Idris.Elab.Term

13import Idris.Elab.Term

13import Idris.Coverage

14import Idris.Coverage

@@ -250,7 +251,7 @@ elabDecl' _ info (PDSL n dsl)

250 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

251 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

251 addIBC (IBCDSL n)

252 addIBC (IBCDSL n)

252elabDecl' what info (PDirective i)

253elabDecl' what info (PDirective i)

253− | what /= EDefns = i

254+ | what /= EDefns = directiveAction i

254elabDecl' what info (PProvider doc syn fc provWhat n)

255elabDecl' what info (PProvider doc syn fc provWhat n)

255 | what /= EDefns

256 | what /= EDefns

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

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

src/Idris/Parser.hs+15−42

@@ -1077,71 +1077,44 @@ Directive' ::= 'lib' CodeGen String_t

1077-}

1078directive :: SyntaxInfo -> IdrisParser [PDecl]

1079directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;

1080− return [PDirective (do addLib cgn lib

1080+ return [PDirective (DLib cgn lib)]

1081− addIBC (IBCLib cgn lib))]

1082 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;

1081 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;

1083− return [PDirective (do dirs <- allImportDirs

1082+ return [PDirective (DLink cgn obj)]

1084− o <- liftIO $ findInPath dirs obj

1085− addIBC (IBCObj cgn obj) -- just name, search on loading ibc

1086− addObjectFile cgn o)]

1087− <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;

1083+ <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_; flag <- stringLiteral

1088− flag <- stringLiteral

1089− return [PDirective (do addIBC (IBCCGFlag cgn flag)

1084+ return [PDirective (DFlag cgn flag)]

1090− addFlag cgn flag)]

1091 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;

1085 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;

1092− return [PDirective (do addHdr cgn hdr

1086+ return [PDirective (DInclude cgn hdr)]

1093− addIBC (IBCHeader cgn hdr))]

1094 <|> do try (lchar '%' *> reserved "hide"); n <- fnName

1087 <|> do try (lchar '%' *> reserved "hide"); n <- fnName

1095− return [PDirective (do setAccessibility n Hidden

1088+ return [PDirective (DHide n)]

1096− addIBC (IBCAccess n Hidden))]

1097 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []

1089 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []

1098− return [PDirective (do setAccessibility n Frozen

1090+ return [PDirective (DFreeze n)]

1099− addIBC (IBCAccess n Frozen))]

1100 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility

1091 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility

1101− return [PDirective (do i <- get

1092+ return [PDirective (DAccess acc)]

1102− put(i { default_access = acc }))]

1103 <|> do try (lchar '%' *> reserved "default"); tot <- totality

1093 <|> do try (lchar '%' *> reserved "default"); tot <- totality

1104 i <- get

1094 i <- get

1105 put (i { default_total = tot } )

1095 put (i { default_total = tot } )

1106− return [PDirective (do i <- get

1096+ return [PDirective (DDefault tot)]

1107− put(i { default_total = tot }))]

1108 <|> do try (lchar '%' *> reserved "logging"); i <- natural;

1097 <|> do try (lchar '%' *> reserved "logging"); i <- natural;

1109− return [PDirective (setLogLevel (fromInteger i))]

1098+ return [PDirective (DLogging i)]

1110 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');

1099 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');

1111− return [PDirective (do added <- addDyLib libs

1100+ return [PDirective (DDynamicLibs libs)]

1112− case added of

1113− Left lib -> addIBC (IBCDyLib (lib_name lib))

1114− Right msg ->

1115− fail $ msg)]

1116 <|> do try (lchar '%' *> reserved "name")

1101 <|> do try (lchar '%' *> reserved "name")

1117 ty <- fnName

1102 ty <- fnName

1118 ns <- sepBy1 name (lchar ',')

1103 ns <- sepBy1 name (lchar ',')

1119− return [PDirective (do ty' <- disambiguate ty

1104+ return [PDirective (DNameHint ty ns)]

1120− mapM_ (addNameHint ty') ns

1121− mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]

1122 <|> do try (lchar '%' *> reserved "error_handlers")

1105 <|> do try (lchar '%' *> reserved "error_handlers")

1123 fn <- fnName

1106 fn <- fnName

1124 arg <- fnName

1107 arg <- fnName

1125 ns <- sepBy1 name (lchar ',')

1108 ns <- sepBy1 name (lchar ',')

1126− return [PDirective (do fn' <- disambiguate fn

1109+ return [PDirective (DErrorHandlers fn arg ns) ]

1127− ns' <- mapM disambiguate ns

1128− addFunctionErrorHandlers fn' arg ns'

1129− mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')]

1130 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

1110 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

1131− return [PDirective (addLangExt ext)]

1111+ return [PDirective (DLanguage ext)]

1132 <|> do fc <- getFC

1112 <|> do fc <- getFC

1133 try (lchar '%' *> reserved "used")

1113 try (lchar '%' *> reserved "used")

1134 fn <- fnName

1114 fn <- fnName

1135 arg <- iName []

1115 arg <- iName []

1136− return [PDirective (addUsedName fc fn arg)]

1116+ return [PDirective (DUsed fc fn arg)]

1137−

1138 <?> "directive"

1117 <?> "directive"

1139− where disambiguate :: Name -> Idris Name

1140− disambiguate n = do i <- getIState

1141− case lookupCtxtName n (idris_implicits i) of

1142− [(n', _)] -> return n'

1143− [] -> throwError (NoSuchVariable n)

1144− more -> throwError (CantResolveAlts (map fst more))

1145

1118

1146pLangExt :: IdrisParser LanguageExt

1119pLangExt :: IdrisParser LanguageExt

1147pLangExt = (reserved "TypeProviders" >> return TypeProviders)

1120pLangExt = (reserved "TypeProviders" >> return TypeProviders)