b1cdd04 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added postulate declarations

postulate foo : type -- 'type' must return something of a collapsible type, i.e. a type with at most one instancei determined entirely by the indices, to ensure that it is unused at run-time.

commitb1cdd04021d9998bcbcd152ad66aff9b76b0183c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 26 Nov 2012, 21:05 (14 years ago) parenta6f8de5

6 files changed+97−27

compare with master

unifiedsplit

src/Core/TT.hs+1 src/Idris/AbsSyntaxTree.hs+30−25 src/Idris/Delaborate.hs+2 src/Idris/ElabDecls.hs+28 src/Idris/IBC.hs+15 src/Idris/Parser.hs+21−2

src/Core/TT.hs+1

@@ -59,6 +59,7 @@ data Err = Msg String

5959 | UniverseError

6060 | ProgramLineComment

6161 | Inaccessible Name

62+ | NonCollapsiblePostulate Name

6263 | At FC Err

6364 deriving Eq

6465

src/Idris/AbsSyntaxTree.hs+30−25

@@ -289,31 +289,33 @@ type FnOpts = [FnOpt]

289289inlinable :: FnOpts -> Bool

290290inlinable = elem Inlinable

291291

292−data PDecl' t = PFix FC Fixity [String] -- fixity declaration

293− | PTy String SyntaxInfo FC FnOpts Name t -- type declaration

294− | PClauses FC FnOpts Name [PClause' t] -- pattern clause

295− | PCAF FC Name t -- top level constant

296− | PData String SyntaxInfo FC Bool -- codata

297− (PData' t) -- data declaration

298− | PParams FC [(Name, t)] [PDecl' t] -- params block

299− | PNamespace String [PDecl' t] -- new namespace

300− | PRecord String SyntaxInfo FC Name t String Name t -- record declaration

301− | PClass String SyntaxInfo FC

302− [t] -- constraints

303− Name

304− [(Name, t)] -- parameters

305− [PDecl' t] -- declarations

306− | PInstance SyntaxInfo FC [t] -- constraints

307− Name -- class

308− [t] -- parameters

309− t -- full instance type

310− (Maybe Name) -- explicit name

311− [PDecl' t]

312− | PDSL Name (DSL' t)

313− | PSyntax FC Syntax

314− | PMutual FC [PDecl' t]

315− | PDirective (Idris ())

316− deriving Functor

292+data PDecl' t

293+ = PFix FC Fixity [String] -- fixity declaration

294+ | PTy String SyntaxInfo FC FnOpts Name t -- type declaration

295+ | PPostulate String SyntaxInfo FC FnOpts Name t

296+ | PClauses FC FnOpts Name [PClause' t] -- pattern clause

297+ | PCAF FC Name t -- top level constant

298+ | PData String SyntaxInfo FC Bool -- codata

299+ (PData' t) -- data declaration

300+ | PParams FC [(Name, t)] [PDecl' t] -- params block

301+ | PNamespace String [PDecl' t] -- new namespace

302+ | PRecord String SyntaxInfo FC Name t String Name t -- record declaration

303+ | PClass String SyntaxInfo FC

304+ [t] -- constraints

305+ Name

306+ [(Name, t)] -- parameters

307+ [PDecl' t] -- declarations

308+ | PInstance SyntaxInfo FC [t] -- constraints

309+ Name -- class

310+ [t] -- parameters

311+ t -- full instance type

312+ (Maybe Name) -- explicit name

313+ [PDecl' t]

314+ | PDSL Name (DSL' t)

315+ | PSyntax FC Syntax

316+ | PMutual FC [PDecl' t]

317+ | PDirective (Idris ())

318+ deriving Functor

317319{-!

318320deriving instance Binary PDecl'

319321!-}

@@ -348,6 +350,7 @@ type PClause = PClause' PTerm

348350declared :: PDecl -> [Name]

349351declared (PFix _ _ _) = []

350352declared (PTy _ _ _ _ n t) = [n]

353+declared (PPostulate _ _ _ _ n t) = [n]

351354declared (PClauses _ _ n _) = [] -- not a declaration

352355declared (PRecord _ _ _ n _ _ c _) = [n, c]

353356declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

@@ -360,6 +363,7 @@ declared (PNamespace _ ds) = concatMap declared ds

360363defined :: PDecl -> [Name]

361364defined (PFix _ _ _) = []

362365defined (PTy _ _ _ _ n t) = []

366+defined (PPostulate _ _ _ _ n t) = []

363367defined (PClauses _ _ n _) = [n] -- not a declaration

364368defined (PRecord _ _ _ n _ _ c _) = [n, c]

365369defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

@@ -657,6 +661,7 @@ instance Show PData where

657661

658662showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

659663showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty

664+showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty

660665showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)

661666showDeclImp _ (PData _ _ _ _ d) = show d

662667showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++

src/Idris/Delaborate.hs+2

@@ -102,6 +102,8 @@ pshow i (IncompleteTerm t) = "Incomplete term " ++ showImp True (delab i t)

102102pshow i UniverseError = "Universe inconsistency"

103103pshow i ProgramLineComment = "Program line next to comment"

104104pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

105+pshow i (NonCollapsiblePostulate n)

106+ = "The return type of postulate " ++ show n ++ " is not collapsible"

105107pshow i (At f e) = show f ++ ":" ++ pshow i e

106108

107109showSc i [] = ""

src/Idris/ElabDecls.hs+28

@@ -80,6 +80,30 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

8080 when corec $ do setAccessibility n Frozen

8181 addIBC (IBCAccess n Frozen)

8282

83+elabPostulate :: ElabInfo -> SyntaxInfo -> String ->

84+ FC -> FnOpts -> Name -> PTerm -> Idris ()

85+elabPostulate info syn doc fc opts n ty

86+ = do elabType info syn doc fc opts n ty

87+ -- make sure it's collapsible, so it is never needed at run time

88+ -- start by getting the elaborated type

89+ ctxt <- getContext

90+ fty <- case lookupTy Nothing n ctxt of

91+ [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!

92+ [ty] -> return ty

93+ ist <- get

94+ let (ap, _) = unApply (getRetTy fty)

95+ logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

96+ let postOK = case ap of

97+ P _ tn _ -> case lookupCtxt Nothing tn

98+ (idris_optimisation ist) of

99+ [oi] -> collapsible oi

100+ _ -> False

101+ _ -> False

102+ when (not postOK)

103+ $ tclift $ tfail (At fc (NonCollapsiblePostulate n))

104+ -- remove it from the deferred definitions list

105+ solveDeferred n

106+

83107elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> Bool -> PData -> Idris ()

84108elabData info syn doc fc codata (PLaterdecl n t_in)

85109 = do iLOG (show (fc, doc))

@@ -999,6 +1023,10 @@ elabDecl' what info (PTy doc s f o n ty)

9991023 | what /= EDefns

10001024 = do iLOG $ "Elaborating type decl " ++ show n ++ show o

10011025 elabType info s doc f o n ty

1026+elabDecl' what info (PPostulate doc s f o n ty)

1027+ | what /= EDefns

1028+ = do iLOG $ "Elaborating postulate " ++ show n ++ show o

1029+ elabPostulate info s doc f o n ty

10021030elabDecl' what info (PData doc s f co d)

10031031 | what /= ETypes

10041032 = do iLOG $ "Elaborating " ++ show (d_name d)

src/Idris/IBC.hs+15

@@ -959,6 +959,14 @@ instance (Binary t) => Binary (PDecl' t) where

959959 PMutual x1 x2 -> do putWord8 11

960960 put x1

961961 put x2

962+ PPostulate x1 x2 x3 x4 x5 x6

963+ -> do putWord8 12

964+ put x1

965+ put x2

966+ put x3

967+ put x4

968+ put x5

969+ put x6

962970 get

963971 = do i <- getWord8

964972 case i of

@@ -1027,6 +1035,13 @@ instance (Binary t) => Binary (PDecl' t) where

10271035 11 -> do x1 <- get

10281036 x2 <- get

10291037 return (PMutual x1 x2)

1038+ 12 -> do x1 <- get

1039+ x2 <- get

1040+ x3 <- get

1041+ x4 <- get

1042+ x5 <- get

1043+ x6 <- get

1044+ return (PPostulate x1 x2 x3 x4 x5 x6)

10301045 _ -> error "Corrupted binary data for PDecl'"

10311046

10321047instance Binary SyntaxInfo where

src/Idris/Parser.hs+21−2

@@ -417,8 +417,6 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'

417417

418418pFunDecl' :: SyntaxInfo -> IParser PDecl

419419pFunDecl' syn = try (do doc <- option "" (pDocComment '|')

420− -- trace ("Doc: " ++ show doc) $

421−-- let doc = ""

422420 pushIndent

423421 ist <- getState

424422 let initOpts = if default_total ist

@@ -435,9 +433,30 @@ pFunDecl' syn = try (do doc <- option "" (pDocComment '|')

435433-- ty' <- implicit syn n ty

436434 addAcc n acc

437435 return (PTy doc syn fc opts' n ty))

436+ <|> try (pPostulate syn)

438437 <|> try (pPattern syn)

439438 <|> try (pCAF syn)

440439

440+pPostulate :: SyntaxInfo -> IParser PDecl

441+pPostulate syn = do doc <- option "" (pDocComment '|')

442+ pushIndent

443+ reserved "postulate"

444+ ist <- getState

445+ let initOpts = if default_total ist

446+ then [TotalFn]

447+ else []

448+ opts <- pFnOpts initOpts

449+ acc <- pAccessibility

450+ opts' <- pFnOpts opts

451+ n_in <- pfName

452+ let n = expandNS syn n_in

453+ ty <- pTSig (impOK syn)

454+ fc <- pfc

455+ pTerminator

456+ addAcc n acc

457+ return (PPostulate doc syn fc opts' n ty)

458+

459+

441460pUsing :: SyntaxInfo -> IParser [PDecl]

442461pUsing syn =

443462 do reserved "using"; lchar '('; ns <- tyDeclList syn; lchar ')'