b1cdd04 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added postulate declarations

b1cdd04Edwin Brady14 years ago

src/Core/TT.hs+1

compare with master

unifiedsplit

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

59 | UniverseError

60 | ProgramLineComment

61 | Inaccessible Name

62+ | NonCollapsiblePostulate Name

62 | At FC Err

63 | At FC Err

63 deriving Eq

64 deriving Eq

src/Idris/AbsSyntaxTree.hs+30−25

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

289inlinable :: FnOpts -> Bool

290inlinable = elem Inlinable

291

292+data PDecl' t

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

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

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

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

295+ | PPostulate String SyntaxInfo FC FnOpts Name t

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

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

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

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

296− | PData String SyntaxInfo FC Bool -- codata

298+ | PData String SyntaxInfo FC Bool -- codata

297− (PData' t) -- data declaration

299+ (PData' t) -- data declaration

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

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

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

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

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

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

301− | PClass String SyntaxInfo FC

303+ | PClass String SyntaxInfo FC

302− [t] -- constraints

304+ [t] -- constraints

303− Name

305+ Name

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

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

305− [PDecl' t] -- declarations

307+ [PDecl' t] -- declarations

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

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

307− Name -- class

309+ Name -- class

308− [t] -- parameters

310+ [t] -- parameters

309− t -- full instance type

311+ t -- full instance type

310− (Maybe Name) -- explicit name

312+ (Maybe Name) -- explicit name

311− [PDecl' t]

313+ [PDecl' t]

312− | PDSL Name (DSL' t)

314+ | PDSL Name (DSL' t)

313− | PSyntax FC Syntax

315+ | PSyntax FC Syntax

314− | PMutual FC [PDecl' t]

316+ | PMutual FC [PDecl' t]

315− | PDirective (Idris ())

317+ | PDirective (Idris ())

316− deriving Functor

318+ deriving Functor

317{-!

319{-!

318deriving instance Binary PDecl'

320deriving instance Binary PDecl'

319!-}

321!-}

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

348declared :: PDecl -> [Name]

350declared :: PDecl -> [Name]

349declared (PFix _ _ _) = []

351declared (PFix _ _ _) = []

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

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

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

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

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

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

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

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

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

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

360defined :: PDecl -> [Name]

363defined :: PDecl -> [Name]

361defined (PFix _ _ _) = []

364defined (PFix _ _ _) = []

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

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

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

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

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

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

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

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

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

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

657

661

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

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

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

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

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

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

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

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

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

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

667showDeclImp _ (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)

102pshow i UniverseError = "Universe inconsistency"

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

104pshow 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"

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

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

106

108

107showSc i [] = ""

109showSc 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

80 when corec $ do setAccessibility n Frozen

81 addIBC (IBCAccess n Frozen)

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+

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

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

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

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

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

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

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

999 | what /= EDefns

1023 | what /= EDefns

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

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

1001 elabType info s doc f o n ty

1025 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

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

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

1003 | what /= ETypes

1031 | what /= ETypes

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

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

src/Idris/IBC.hs+15

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

959 PMutual x1 x2 -> do putWord8 11

960 put x1

961 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

962 get

970 get

963 = do i <- getWord8

971 = do i <- getWord8

964 case i of

972 case i of

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

1027 11 -> do x1 <- get

1035 11 -> do x1 <- get

1028 x2 <- get

1036 x2 <- get

1029 return (PMutual x1 x2)

1037 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)

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

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

1031

1046

1032instance Binary SyntaxInfo where

1047instance Binary SyntaxInfo where

src/Idris/Parser.hs+21−2

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

417

418pFunDecl' :: SyntaxInfo -> IParser PDecl

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

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

421−-- let doc = ""

422 pushIndent

420 pushIndent

423 ist <- getState

421 ist <- getState

424 let initOpts = if default_total ist

422 let initOpts = if default_total ist

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

435-- ty' <- implicit syn n ty

433-- ty' <- implicit syn n ty

436 addAcc n acc

434 addAcc n acc

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

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

436+ <|> try (pPostulate syn)

438 <|> try (pPattern syn)

437 <|> try (pPattern syn)

439 <|> try (pCAF syn)

438 <|> try (pCAF syn)

440

439

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+

441pUsing :: SyntaxInfo -> IParser [PDecl]

460pUsing :: SyntaxInfo -> IParser [PDecl]

442pUsing syn =

461pUsing syn =

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

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