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

git.iko.soy/Idris-dev

Added "partial" keyword and "%default" directive

commit7b2bf5e64651465e65945599b489b6c9efda74e1 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 22 Oct 2012, 15:11 (14 years ago) parent792deaf

5 files changed+33−14

compare with master

unifiedsplit

CHANGELOG+3 src/Core/CoreParser.hs+1−1 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/ElabDecls.hs+1−1 src/Idris/Parser.hs+26−11

CHANGELOG+3

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

66* Added 'parameters' blocks

77* 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.

811

912Internal changes:

1013

src/Core/CoreParser.hs+1−1

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

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

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

2424 "do", "dsl", "import", "impossible",

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

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

2626 "infix", "infixl", "infixr",

2727 "where", "with", "syntax", "proof", "postulate",

2828 "using", "namespace", "class", "instance",

src/Idris/AbsSyntaxTree.hs+2−1

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

7676 brace_stack :: [Maybe Int],

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

7878 default_access :: Accessibility,

79+ default_total :: Bool,

7980 ibc_write :: [IBCWrite],

8081 compiled_so :: Maybe String

8182 }

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

117118 emptyContext emptyContext emptyContext emptyContext

118119 emptyContext emptyContext emptyContext

119120 [] "" defaultOpts 6 [] [] [] [] [] [] [] []

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

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

121122

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

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

src/Idris/ElabDecls.hs+1−1

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

897897

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

899899elabDecl' 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

901901 elabType info s f o n ty

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

903903 elabData info s f d

src/Idris/Parser.hs+26−11

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

405405

406406pFunDecl' :: SyntaxInfo -> IParser PDecl

407407pFunDecl' syn = try (do pushIndent

408− opts <- pFnOpts

408+ ist <- getState

409+ let initOpts = if default_total ist

410+ then [TotalFn]

411+ else []

412+ opts <- pFnOpts initOpts

409413 acc <- pAccessibility

410− opts' <- pFnOpts

414+ opts' <- pFnOpts opts

411415 n_in <- pfName

412416 let n = expandNS syn n_in

413417 ty <- pTSig (impOK syn)

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

415419 pTerminator

416420-- ty' <- implicit syn n ty

417421 addAcc n acc

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

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

419423 <|> try (pPattern syn)

420424 <|> try (pCAF syn)

421425

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

612616pfName = try pOpFront

613617 <|> pName

614618

619+pTotality :: IParser Bool

620+pTotality

621+ = do reserved "total"; return True

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

623+

615624pAccessibility' :: IParser Accessibility

616625pAccessibility'

617626 = do reserved "public"; return Public

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

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

624633 <|> return Nothing

625634

626−pFnOpts :: IParser [FnOpt]

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

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

629− return (CExport c : xs))

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

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

636+pFnOpts opts

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

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

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

640+ pFnOpts (CExport c : opts))

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

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

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

633− xs <- pFnOpts

634− return (Specialise ns : xs)

635− <|> return []

644+ pFnOpts (Specialise ns : opts)

645+ <|> return opts

636646

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

638648addAcc n a = do i <- getState

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

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

13641374 return [PDirective (do i <- getIState

13651375 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 }))])

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

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

13681383