7b2bf5e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added "partial" keyword and "%default" directive

7b2bf5eEdwin Brady14 years ago

CHANGELOG+3

compare with master

unifiedsplit

@@ -5,6 +5,9 @@ User visible changes:

6* Added 'parameters' blocks

7* Allow local data definitions in where blocks

8+* Added '%default' directive to declare total-by-default or partial-by-default

9+ for functions, and a corresponding "partial" reserved words to mark functions as

10+ allowed to be partial.

9Internal changes:

12Internal changes:

src/Core/CoreParser.hs+1−1

@@ -22,7 +22,7 @@ idrisDef = haskellDef {

22 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

23 reservedNames = ["let", "in", "data", "record", "Set",

24 "do", "dsl", "import", "impossible",

25− "case", "of", "total",

25+ "case", "of", "total", "partial",

26 "infix", "infixl", "infixr",

27 "where", "with", "syntax", "proof", "postulate",

28 "using", "namespace", "class", "instance",

src/Idris/AbsSyntaxTree.hs+2−1

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

76 brace_stack :: [Maybe Int],

77 hide_list :: [(Name, Maybe Accessibility)],

78 default_access :: Accessibility,

79+ default_total :: Bool,

79 ibc_write :: [IBCWrite],

80 ibc_write :: [IBCWrite],

80 compiled_so :: Maybe String

81 compiled_so :: Maybe String

81 }

82 }

@@ -117,7 +118,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

117 emptyContext emptyContext emptyContext emptyContext

118 emptyContext emptyContext emptyContext emptyContext

118 emptyContext emptyContext emptyContext

119 emptyContext emptyContext emptyContext

119 [] "" defaultOpts 6 [] [] [] [] [] [] [] []

120 [] "" defaultOpts 6 [] [] [] [] [] [] [] []

120− [] Nothing Nothing [] [] [] Hidden [] Nothing

121+ [] Nothing Nothing [] [] [] Hidden False [] Nothing

121

122

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

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

123-- global state (hence the IO inner monad).

124-- global state (hence the IO inner monad).

src/Idris/ElabDecls.hs+1−1

@@ -897,7 +897,7 @@ elabDecl info d = idrisCatch (elabDecl' info d)

897

898elabDecl' info (PFix _ _ _) = return () -- nothing to elaborate

899elabDecl' info (PSyntax _ p) = return () -- nothing to elaborate

900−elabDecl' info (PTy s f o n ty) = do iLOG $ "Elaborating type decl " ++ show n

900+elabDecl' info (PTy s f o n ty) = do iLOG $ "Elaborating type decl " ++ show n ++ show o

901 elabType info s f o n ty

902elabDecl' info (PData s f d) = do iLOG $ "Elaborating " ++ show (d_name d)

903 elabData info s f d

src/Idris/Parser.hs+26−11

@@ -405,9 +405,13 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'

405

406pFunDecl' :: SyntaxInfo -> IParser PDecl

407pFunDecl' syn = try (do pushIndent

408+ ist <- getState

409+ let initOpts = if default_total ist

410+ then [TotalFn]

411+ else []

408− opts <- pFnOpts

412+ opts <- pFnOpts initOpts

409 acc <- pAccessibility

413 acc <- pAccessibility

410− opts' <- pFnOpts

414+ opts' <- pFnOpts opts

411 n_in <- pfName

415 n_in <- pfName

412 let n = expandNS syn n_in

416 let n = expandNS syn n_in

413 ty <- pTSig (impOK syn)

417 ty <- pTSig (impOK syn)

@@ -415,7 +419,7 @@ pFunDecl' syn = try (do pushIndent

415 pTerminator

419 pTerminator

416-- ty' <- implicit syn n ty

420-- ty' <- implicit syn n ty

417 addAcc n acc

421 addAcc n acc

418− return (PTy syn fc (opts ++ opts') n ty))

422+ return (PTy syn fc opts' n ty))

419 <|> try (pPattern syn)

423 <|> try (pPattern syn)

420 <|> try (pCAF syn)

424 <|> try (pCAF syn)

421

425

@@ -612,6 +616,11 @@ pOpFront = maybeWithNS pOpFrontNoNS False []

612pfName = try pOpFront

616pfName = try pOpFront

613 <|> pName

617 <|> pName

614

618

619+pTotality :: IParser Bool

620+pTotality

621+ = do reserved "total"; return True

622+ <|> do reserved "partial"; return False

623+

615pAccessibility' :: IParser Accessibility

624pAccessibility' :: IParser Accessibility

616pAccessibility'

625pAccessibility'

617 = do reserved "public"; return Public

626 = do reserved "public"; return Public

@@ -623,16 +632,17 @@ pAccessibility

623 = do acc <- pAccessibility'; return (Just acc)

632 = do acc <- pAccessibility'; return (Just acc)

624 <|> return Nothing

633 <|> return Nothing

625

634

626−pFnOpts :: IParser [FnOpt]

635+pFnOpts :: [FnOpt] -> IParser [FnOpt]

627−pFnOpts = do reserved "total"; xs <- pFnOpts; return (TotalFn : xs)

636+pFnOpts opts

637+ = do reserved "total"; pFnOpts (TotalFn : opts)

638+ <|> do reserved "partial"; pFnOpts (opts \\ [TotalFn])

628− <|> try (do lchar '%'; reserved "export"; c <- strlit; xs <- pFnOpts

639+ <|> try (do lchar '%'; reserved "export"; c <- strlit;

629− return (CExport c : xs))

640+ pFnOpts (CExport c : opts))

630− <|> do lchar '%'; reserved "assert_total"; xs <- pFnOpts; return (AssertTotal : xs)

641+ <|> do lchar '%'; reserved "assert_total"; pFnOpts (AssertTotal : opts)

631 <|> do lchar '%'; reserved "specialise";

642 <|> do lchar '%'; reserved "specialise";

632 lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'

643 lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'

633− xs <- pFnOpts

634− return (Specialise ns : xs)

644+ pFnOpts (Specialise ns : opts)

635− <|> return []

645+ <|> return opts

636

646

637addAcc :: Name -> Maybe Accessibility -> IParser ()

647addAcc :: Name -> Maybe Accessibility -> IParser ()

638addAcc n a = do i <- getState

648addAcc n a = do i <- getState

@@ -1363,6 +1373,11 @@ pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

1363 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'

1373 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'

1364 return [PDirective (do i <- getIState

1374 return [PDirective (do i <- getIState

1365 putIState (i { default_access = acc }))])

1375 putIState (i { default_access = acc }))])

1376+ <|> try (do lchar '%'; reserved "default"; tot <- pTotality

1377+ i <- getState

1378+ setState (i { default_total = tot } )

1379+ return [PDirective (do i <- getIState

1380+ putIState (i { default_total = tot }))])

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

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

1367 return [PDirective (setLogLevel (fromInteger i))])

1382 return [PDirective (setLogLevel (fromInteger i))])

1368

1383