4ed9c1b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added %thaw directive

The opposite of %freeze, this allows a frozen definition to reduce again. Only names which have previously been frozen can be thawed. Fixes #3200, though it's really a workaround for the fact that the type checker reduces more than necessary in the conversion check and unification.

commit4ed9c1b6a2c7474881e89eafe462b2e6df0d4bff authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 4 Jun 2016, 13:04 (10 years ago) parentb1a42b3

3 files changed+12

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/Directives.hs+8 src/Idris/Parser.hs+3

src/Idris/AbsSyntaxTree.hs+1

@@ -831,6 +831,7 @@ data Directive = DLib Codegen String

831831 | DInclude Codegen String

832832 | DHide Name

833833 | DFreeze Name

834+ | DThaw Name

834835 | DInjective Name

835836 | DSetTotal Name -- assert totality after checking

836837 | DAccess Accessibility

src/Idris/Directives.hs+8

@@ -48,6 +48,14 @@ directiveAction (DFreeze n') = do

4848 mapM_ (\n -> do

4949 setAccessibility n Frozen

5050 addIBC (IBCAccess n Frozen)) ns

51+directiveAction (DThaw n') = do

52+ ns <- allNamespaces n'

53+ mapM_ (\n -> do

54+ ctxt <- getContext

55+ case lookupDefAccExact n False ctxt of

56+ Just (_, Frozen) -> do setAccessibility n Public

57+ addIBC (IBCAccess n Public)

58+ _ -> throwError (Msg (show n ++ " is not frozen"))) ns

5159directiveAction (DInjective n') = do

5260 ns <- allNamespaces n'

5361 mapM_ (\n -> do

src/Idris/Parser.hs+3

@@ -1353,6 +1353,7 @@ Directive' ::= 'lib' CodeGen String_t

13531353 | 'include' CodeGen String_t

13541354 | 'hide' Name

13551355 | 'freeze' Name

1356+ | 'thaw' Name

13561357 | 'access' Accessibility

13571358 | 'default' Totality

13581359 | 'logging' Natural

@@ -1385,6 +1386,8 @@ directive syn = do try (lchar '%' *> reserved "lib")

13851386 return [PDirective (DHide n)]

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

13871388 return [PDirective (DFreeze n)]

1389+ <|> do try (lchar '%' *> reserved "thaw"); n <- fst <$> iName []

1390+ return [PDirective (DThaw n)]

13881391 -- injectivity assertins are intended for debugging purposes

13891392 -- only, and won't be documented/could be removed at any point

13901393 <|> do try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName