d7f4e11 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Induction now works on types with parameters

d7f4e11Ahmad Salim Al-Sibahi13 years ago

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

@@ -177,6 +177,7 @@ data IBCWrite = IBCFix FixDecl

177 | IBCDyLib String

178 | IBCHeader Codegen String

179 | IBCAccess Name Accessibility

180+ | IBCMetaInformation Name MetaInformation

180 | IBCTotal Name Totality

181 | IBCTotal Name Totality

181 | IBCFlags Name [FnOpt]

182 | IBCFlags Name [FnOpt]

182 | IBCTrans (Term, Term)

183 | IBCTrans (Term, Term)

src/Idris/Core/Evaluate.hs+44−28

@@ -4,12 +4,12 @@

4module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

5 rt_simplify, simplify, specialise, hnf, convEq, convEq',

6 Def(..), CaseInfo(..), CaseDefs(..),

7− Accessibility(..), Totality(..), PReason(..),

7+ Accessibility(..), Totality(..), PReason(..), MetaInformation(..),

8 Context, initContext, ctxtAlist, uconstraints, next_tvar,

9− addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,

9+ addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11 lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,

12− lookupTotal, lookupNameTotal, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

12+ lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

13 Value(..), Quote(..), initEval) where

15import Debug.Trace

@@ -678,12 +678,18 @@ deriving instance Binary Totality

678deriving instance Binary PReason

679!-}

680

681+-- Possible attached meta-information for a definition in context

682+data MetaInformation =

683+ EmptyMI -- ^ No meta-information

684+ | DataMI [Int] -- ^ Meta information for a data declaration with position of parameters

685+ deriving (Eq, Show)

686+

681-- | Contexts used for global definitions and for proof state. They contain

687-- | Contexts used for global definitions and for proof state. They contain

682-- universe constraints and existing definitions.

688-- universe constraints and existing definitions.

683data Context = MkContext {

689data Context = MkContext {

684− uconstraints :: [UConstraint],

690+ uconstraints :: [UConstraint],

685− next_tvar :: Int,

691+ next_tvar :: Int,

686− definitions :: Ctxt (Def, Accessibility, Totality)

692+ definitions :: Ctxt (Def, Accessibility, Totality, MetaInformation)

687 } deriving Show

693 } deriving Show

688

694

689-- | The initial empty context

695-- | The initial empty context

@@ -691,37 +697,43 @@ initContext = MkContext [] 0 emptyContext

691

697

692-- | Get the definitions from a context

698-- | Get the definitions from a context

693ctxtAlist :: Context -> [(Name, Def)]

699ctxtAlist :: Context -> [(Name, Def)]

694−ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)

700+ctxtAlist ctxt = map (\(n, (d, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)

695

701

696veval ctxt env t = evalState (eval False ctxt [] env t []) initEval

702veval ctxt env t = evalState (eval False ctxt [] env t []) initEval

697

703

698addToCtxt :: Name -> Term -> Type -> Context -> Context

704addToCtxt :: Name -> Term -> Type -> Context -> Context

699addToCtxt n tm ty uctxt

705addToCtxt n tm ty uctxt

700 = let ctxt = definitions uctxt

706 = let ctxt = definitions uctxt

701− ctxt' = addDef n (Function ty tm, Public, Unchecked) ctxt in

707+ ctxt' = addDef n (Function ty tm, Public, Unchecked, EmptyMI) ctxt in

702 uctxt { definitions = ctxt' }

708 uctxt { definitions = ctxt' }

703

709

704setAccess :: Name -> Accessibility -> Context -> Context

710setAccess :: Name -> Accessibility -> Context -> Context

705setAccess n a uctxt

711setAccess n a uctxt

706 = let ctxt = definitions uctxt

712 = let ctxt = definitions uctxt

707− ctxt' = updateDef n (\ (d, _, t) -> (d, a, t)) ctxt in

713+ ctxt' = updateDef n (\ (d, _, t, m) -> (d, a, t, m)) ctxt in

708 uctxt { definitions = ctxt' }

714 uctxt { definitions = ctxt' }

709

715

710setTotal :: Name -> Totality -> Context -> Context

716setTotal :: Name -> Totality -> Context -> Context

711setTotal n t uctxt

717setTotal n t uctxt

712 = let ctxt = definitions uctxt

718 = let ctxt = definitions uctxt

713− ctxt' = updateDef n (\ (d, a, _) -> (d, a, t)) ctxt in

719+ ctxt' = updateDef n (\ (d, a, _, m) -> (d, a, t, m)) ctxt in

720+ uctxt { definitions = ctxt' }

721+

722+setMetaInformation :: Name -> MetaInformation -> Context -> Context

723+setMetaInformation n m uctxt

724+ = let ctxt = definitions uctxt

725+ ctxt' = updateDef n (\ (d, a, t, _) -> (d, a, t, m)) ctxt in

714 uctxt { definitions = ctxt' }

726 uctxt { definitions = ctxt' }

715

727

716addCtxtDef :: Name -> Def -> Context -> Context

728addCtxtDef :: Name -> Def -> Context -> Context

717addCtxtDef n d c = let ctxt = definitions c

729addCtxtDef n d c = let ctxt = definitions c

718− ctxt' = addDef n (d, Public, Unchecked) $! ctxt in

730+ ctxt' = addDef n (d, Public, Unchecked, EmptyMI) $! ctxt in

719 c { definitions = ctxt' }

731 c { definitions = ctxt' }

720

732

721addTyDecl :: Name -> NameType -> Type -> Context -> Context

733addTyDecl :: Name -> NameType -> Type -> Context -> Context

722addTyDecl n nt ty uctxt

734addTyDecl n nt ty uctxt

723 = let ctxt = definitions uctxt

735 = let ctxt = definitions uctxt

724− ctxt' = addDef n (TyDecl nt ty, Public, Unchecked) ctxt in

736+ ctxt' = addDef n (TyDecl nt ty, Public, Unchecked, EmptyMI) ctxt in

725 uctxt { definitions = ctxt' }

737 uctxt { definitions = ctxt' }

726

738

727addDatatype :: Datatype Name -> Context -> Context

739addDatatype :: Datatype Name -> Context -> Context

@@ -729,14 +741,14 @@ addDatatype (Data n tag ty cons) uctxt

729 = let ctxt = definitions uctxt

741 = let ctxt = definitions uctxt

730 ty' = normalise uctxt [] ty

742 ty' = normalise uctxt [] ty

731 ctxt' = addCons 0 cons (addDef n

743 ctxt' = addCons 0 cons (addDef n

732− (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked) ctxt) in

744+ (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt) in

733 uctxt { definitions = ctxt' }

745 uctxt { definitions = ctxt' }

734 where

746 where

735 addCons tag [] ctxt = ctxt

747 addCons tag [] ctxt = ctxt

736 addCons tag ((n, ty) : cons) ctxt

748 addCons tag ((n, ty) : cons) ctxt

737 = let ty' = normalise uctxt [] ty in

749 = let ty' = normalise uctxt [] ty in

738 addCons (tag+1) cons (addDef n

750 addCons (tag+1) cons (addDef n

739− (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt)

751+ (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt)

740

752

741-- FIXME: Too many arguments! Refactor all these Bools.

753-- FIXME: Too many arguments! Refactor all these Bools.

742addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

754addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

@@ -770,7 +782,7 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)

770 (args_rt, sc_rt) in

782 (args_rt, sc_rt) in

771 addDef n (CaseOp (ci { case_inlinable = inlc })

783 addDef n (CaseOp (ci { case_inlinable = inlc })

772 ty ps_in ps_tot cdef,

784 ty ps_in ps_tot cdef,

773− access, Unchecked) ctxt in

785+ access, Unchecked, EmptyMI) ctxt in

774 uctxt { definitions = ctxt' }

786 uctxt { definitions = ctxt' }

775

787

776-- simplify a definition for totality checking

788-- simplify a definition for totality checking

@@ -778,16 +790,16 @@ simplifyCasedef :: Name -> Context -> Context

778simplifyCasedef n uctxt

790simplifyCasedef n uctxt

779 = let ctxt = definitions uctxt

791 = let ctxt = definitions uctxt

780 ctxt' = case lookupCtxt n ctxt of

792 ctxt' = case lookupCtxt n ctxt of

781− [(CaseOp ci ty [] ps _, acc, tot)] ->

793+ [(CaseOp ci ty [] ps _, acc, tot, metainf)] ->

782 ctxt -- nothing to simplify (or already done...)

794 ctxt -- nothing to simplify (or already done...)

783− [(CaseOp ci ty ps_in ps cd, acc, tot)] ->

795+ [(CaseOp ci ty ps_in ps cd, acc, tot, metainf)] ->

784 let ps_in' = map simpl ps_in

796 let ps_in' = map simpl ps_in

785 pdef = map debind ps_in' in

797 pdef = map debind ps_in' in

786 case simpleCase False True False CompileTime emptyFC pdef of

798 case simpleCase False True False CompileTime emptyFC pdef of

787 OK (CaseDef args sc _) ->

799 OK (CaseDef args sc _) ->

788 addDef n (CaseOp ci

800 addDef n (CaseOp ci

789 ty ps_in' ps (cd { cases_totcheck = (args, sc) }),

801 ty ps_in' ps (cd { cases_totcheck = (args, sc) }),

790− acc, tot) ctxt

802+ acc, tot, metainf) ctxt

791 Error err -> error (show err)

803 Error err -> error (show err)

792 _ -> ctxt in

804 _ -> ctxt in

793 uctxt { definitions = ctxt' }

805 uctxt { definitions = ctxt' }

@@ -807,10 +819,10 @@ addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->

807 Context -> Context

819 Context -> Context

808addOperator n ty a op uctxt

820addOperator n ty a op uctxt

809 = let ctxt = definitions uctxt

821 = let ctxt = definitions uctxt

810− ctxt' = addDef n (Operator ty a op, Public, Unchecked) ctxt in

822+ ctxt' = addDef n (Operator ty a op, Public, Unchecked, EmptyMI) ctxt in

811 uctxt { definitions = ctxt' }

823 uctxt { definitions = ctxt' }

812

824

813−tfst (a, _, _) = a

825+tfst (a, _, _, _) = a

814

826

815lookupNames :: Name -> Context -> [Name]

827lookupNames :: Name -> Context -> [Name]

816lookupNames n ctxt

828lookupNames n ctxt

@@ -856,10 +868,10 @@ lookupP :: Name -> Context -> [Term]

856lookupP n ctxt

868lookupP n ctxt

857 = do def <- lookupCtxt n (definitions ctxt)

869 = do def <- lookupCtxt n (definitions ctxt)

858 p <- case def of

870 p <- case def of

859− (Function ty tm, a, _) -> return (P Ref n ty, a)

871+ (Function ty tm, a, _, _) -> return (P Ref n ty, a)

860− (TyDecl nt ty, a, _) -> return (P nt n ty, a)

872+ (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)

861− (CaseOp _ ty _ _ _, a, _) -> return (P Ref n ty, a)

873+ (CaseOp _ ty _ _ _, a, _, _) -> return (P Ref n ty, a)

862− (Operator ty _ _, a, _) -> return (P Ref n ty, a)

874+ (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

863 case snd p of

875 case snd p of

864 Hidden -> []

876 Hidden -> []

865 _ -> return (fst p)

877 _ -> return (fst p)

@@ -872,15 +884,19 @@ lookupDefAcc :: Name -> Bool -> Context ->

872lookupDefAcc n mkpublic ctxt

884lookupDefAcc n mkpublic ctxt

873 = map mkp $ lookupCtxt n (definitions ctxt)

885 = map mkp $ lookupCtxt n (definitions ctxt)

874 -- io_bind a special case for REPL prettiness

886 -- io_bind a special case for REPL prettiness

875− where mkp (d, a, _) = if mkpublic && (not (n == UN "io_bind" || n == UN "io_return"))

887+ where mkp (d, a, _, _) = if mkpublic && (not (n == UN "io_bind" || n == UN "io_return"))

876− then (d, Public) else (d, a)

888+ then (d, Public) else (d, a)

877

889

878lookupTotal :: Name -> Context -> [Totality]

890lookupTotal :: Name -> Context -> [Totality]

879lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

891lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

880− where mkt (d, a, t) = t

892+ where mkt (d, a, t, m) = t

893+

894+lookupMetaInformation :: Name -> Context -> [MetaInformation]

895+lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)

896+ where mkm (d, a, t, m) = m

881

897

882lookupNameTotal :: Name -> Context -> [(Name, Totality)]

898lookupNameTotal :: Name -> Context -> [(Name, Totality)]

883−lookupNameTotal n = map (\(n, (_, _, t)) -> (n, t)) . lookupCtxtName n . definitions

899+lookupNameTotal n = map (\(n, (_, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions

884

900

885

901

886lookupVal :: Name -> Context -> [Value]

902lookupVal :: Name -> Context -> [Value]

src/Idris/Core/ProofState.hs+18−9

@@ -602,26 +602,32 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

602 (tmv, tmt) <- lift $ check ctxt env (Var nm)

603 let tmt' = normalise ctxt env tmt

604 case unApply tmt' of

605− (P _ tnm _, pms@[]) -> do

605+ (P _ tnm _, tyargs) -> do

606 case lookupTy (SN (ElimN tnm)) ctxt of

607 [elimTy] -> do

608+ param_pos <- case lookupMetaInformation tnm ctxt of

609+ [DataMI param_pos] -> return param_pos

610+ m | length tyargs > 0 -> fail $ "Invalid meta information for " ++ show tnm ++ " where the metainformation is " ++ show m ++ " and definition is" ++ show (lookupDef tnm ctxt)

611+ _ -> return []

612+ let (params, indicies) = splitTyArgs param_pos tyargs

608 let args = getArgTys elimTy

613 let args = getArgTys elimTy

609− let pmargs = take (length pms) args -- TODO: Fill these correctly when having multiple parameters working

614+ let pmargs = take (length tyargs) args

610− let args' = drop (length pms) args

615+ let args' = drop (length tyargs) args

611 let propTy = head args'

616 let propTy = head args'

612− let consargs = init $ tail args -- TODO: This is incorrect when type has indicies, get indicies and use the correct count

617+ let restargs = init $ tail args'

618+ let consargs = take (length restargs - length indicies) $ restargs

619+ let indxargs = drop (length restargs - length indicies) $ restargs

613− let scr = last $ tail args

620+ let scr = last $ tail args'

614 let prop = Bind nm (Lam tmt') t -- TODO: Make this work for types with indicies

621 let prop = Bind nm (Lam tmt') t -- TODO: Make this work for types with indicies

615− let res = substV prop $ bindConsArgs consargs (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0))) ([prop] ++ map makeConsArg consargs ++ [tmv]))

622+ let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0))) (params ++ [prop] ++ map makeConsArg consargs ++ [tmv])))

616 action (\ps -> ps {holes = holes ps \\ [x]})

623 action (\ps -> ps {holes = holes ps \\ [x]})

617 mapM_ addConsHole (reverse consargs)

624 mapM_ addConsHole (reverse consargs)

618 let res' = forget $ res

625 let res' = forget $ res

619 (scv, sct) <- lift $ check ctxt env res'

626 (scv, sct) <- lift $ check ctxt env res'

620 let scv' = specialise ctxt env [] scv

627 let scv' = specialise ctxt env [] scv

621 return scv'

628 return scv'

622− [] -> fail $ "Induction needs an eliminator for " ++ show nm

629+ [] -> fail $ "Induction needs an eliminator for " ++ show tnm

623− xs -> fail $ "Multiple definitions found when searching for the eliminator of " ++ show nm

630+ xs -> fail $ "Multiple definitions found when searching for the eliminator of " ++ show tnm

624− (P _ nm _, _) -> fail "Induction not yet supported for types with arguments"

625 _ -> fail "Unkown type for induction"

631 _ -> fail "Unkown type for induction"

626 where scname = MN 0 "scarg"

632 where scname = MN 0 "scarg"

627 makeConsArg (nm, ty) = P Bound nm ty

633 makeConsArg (nm, ty) = P Bound nm ty

@@ -629,6 +635,9 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

629 bindConsArgs [] v = v

635 bindConsArgs [] v = v

630 addConsHole (nm, ty) =

636 addConsHole (nm, ty) =

631 action (\ps -> ps { holes = nm : holes ps })

637 action (\ps -> ps { holes = nm : holes ps })

638+ splitTyArgs param_pos tyargs =

639+ let (params, indicies) = partition (flip elem param_pos . fst) . zip [0..] $ tyargs

640+ in (map snd params, map snd indicies)

632induction tm ctxt env _ = do fail "Can't do induction here"

641induction tm ctxt env _ = do fail "Can't do induction here"

633

642

634

643

src/Idris/Core/TT.hs−15

@@ -515,21 +515,6 @@ raw_unapply t = ua [] t where

515 ua args (RApp f a) = ua (a:args) f

516 ua args t = (t, args)

517

518−data RawFun = RawFun { rtype :: Raw,

519− rval :: Raw

520− }

521− deriving Show

522−

523−data RawDatatype = RDatatype Name Raw [(Name, Raw)]

524− deriving Show

525−

526−data RDef = RFunction RawFun

527− | RConst Raw

528− | RData RawDatatype

529− deriving Show

530−

531−type RProgram = [(Name, RDef)]

532−

533-- WELL TYPED TERMS ---------------------------------------------------------

518-- WELL TYPED TERMS ---------------------------------------------------------

534

519

535-- | Universe expressions for universe checking

520-- | Universe expressions for universe checking

src/Idris/Core/Typecheck.hs−25

@@ -214,28 +214,3 @@ check' holes ctxt env top = chk env top where

214 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)

215 discharge n (PVTy t) scv sct

216 = return (Bind n (PVTy t) scv, sct)

217−

218−

219−checkProgram :: Context -> RProgram -> TC Context

220−checkProgram ctxt [] = return ctxt

221−checkProgram ctxt ((n, RConst t) : xs)

222− = do (t', tt') <- trace (show n) $ check ctxt [] t

223− isType ctxt [] tt'

224− checkProgram (addTyDecl n Ref t' ctxt) xs

225−checkProgram ctxt ((n, RFunction (RawFun ty val)) : xs)

226− = do (ty', tyt') <- trace (show n) $ check ctxt [] ty

227− (val', valt') <- check ctxt [] val

228− isType ctxt [] tyt'

229− converts ctxt [] ty' valt'

230− checkProgram (addToCtxt n val' ty' ctxt) xs

231−checkProgram ctxt ((n, RData (RDatatype _ ty cons)) : xs)

232− = do (ty', tyt') <- trace (show n) $ check ctxt [] ty

233− isType ctxt [] tyt'

234− -- add the tycon temporarily so we can check constructors

235− let ctxt' = addDatatype (Data n 0 ty' []) ctxt

236− cons' <- mapM (checkCon ctxt') cons

237− checkProgram (addDatatype (Data n 0 ty' cons') ctxt) xs

238− where checkCon ctxt (n, cty) = do (cty', ctyt') <- check ctxt [] cty

239− return (n, cty')

240−

241−

src/Idris/ElabDecls.hs+3

@@ -202,8 +202,11 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

202 addIBC (IBCData n)

203 addDocStr n doc

204 addIBC (IBCDoc n)

205+ let metainf = DataMI params

206+ addIBC (IBCMetaInformation n metainf)

205 collapseCons n cons

207 collapseCons n cons

206 updateContext (addDatatype (Data n ttag cty cons))

208 updateContext (addDatatype (Data n ttag cty cons))

209+ updateContext (setMetaInformation n metainf)

207 mapM_ (checkPositive n) cons

210 mapM_ (checkPositive n) cons

208 if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty

211 if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty

209 else return ()

212 else return ()

src/Idris/IBC.hs+28−5

@@ -23,7 +23,7 @@ import Debug.Trace

23import Paths_idris

25ibcVersion :: Word8

26−ibcVersion = 48

26+ibcVersion = 49

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

@@ -52,7 +52,8 @@ data IBCFile = IBCFile { ver :: Word8,

52 ibc_transforms :: [(Term, Term)],

53 ibc_coercions :: [Name],

54 ibc_lineapps :: [(FilePath, Int, PTerm)],

55− ibc_namehints :: [(Name, Name)]

55+ ibc_namehints :: [(Name, Name)],

56+ ibc_metainformation :: [(Name, MetaInformation)]

56 }

57 }

57 deriving Show

58 deriving Show

58{-!

59{-!

@@ -60,7 +61,7 @@ deriving instance Binary IBCFile

60!-}

61!-}

62initIBC :: IBCFile

63initIBC :: IBCFile

63−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

64+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

65loadIBC :: FilePath -> Idris ()

66loadIBC :: FilePath -> Idris ()

66loadIBC fp = do iLOG $ "Loading ibc " ++ fp

67loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -140,6 +141,7 @@ ibc i (IBCLineApp fp l t) f

140 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }

141 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }

141ibc i (IBCNameHint (n, ty)) f

142ibc i (IBCNameHint (n, ty)) f

142 = return f { ibc_namehints = (n, ty) : ibc_namehints f }

143 = return f { ibc_namehints = (n, ty) : ibc_namehints f }

144+ibc i (IBCMetaInformation n m) f = return f { ibc_metainformation = (n,m) : ibc_metainformation f }

143

145

144process :: IBCFile -> FilePath -> Idris ()

146process :: IBCFile -> FilePath -> Idris ()

145process i fn

147process i fn

@@ -176,6 +178,7 @@ process i fn

176 pTrans (ibc_transforms i)

178 pTrans (ibc_transforms i)

177 pLineApps (ibc_lineapps i)

179 pLineApps (ibc_lineapps i)

178 pNameHints (ibc_namehints i)

180 pNameHints (ibc_namehints i)

181+ pMetaInformation (ibc_metainformation i)

179

182

180timestampOlder :: FilePath -> FilePath -> IO ()

183timestampOlder :: FilePath -> FilePath -> IO ()

181timestampOlder src ibc = do srct <- getModificationTime src

184timestampOlder src ibc = do srct <- getModificationTime src

@@ -326,6 +329,12 @@ pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls

326pNameHints :: [(Name, Name)] -> Idris ()

329pNameHints :: [(Name, Name)] -> Idris ()

327pNameHints ns = mapM_ (\ (n, ty) -> addNameHint n ty) ns

330pNameHints ns = mapM_ (\ (n, ty) -> addNameHint n ty) ns

328

331

332+pMetaInformation :: [(Name, MetaInformation)] -> Idris ()

333+pMetaInformation ds = mapM_ (\ (n, m) ->

334+ do i <- getIState

335+ putIState (i { tt_ctxt = setMetaInformation n m (tt_ctxt i) }))

336+ ds

337+

329----- Generated by 'derive'

338----- Generated by 'derive'

330

339

331instance Binary SizeChange where

340instance Binary SizeChange where

@@ -890,8 +899,20 @@ instance Binary Totality where

890 3 -> return Productive

899 3 -> return Productive

891 _ -> error "Corrupted binary data for Totality"

900 _ -> error "Corrupted binary data for Totality"

892

901

902+instance Binary MetaInformation where

903+ put x

904+ = case x of

905+ EmptyMI -> do putWord8 0

906+ DataMI x1 -> do putWord8 1

907+ put x1

908+ get = do i <- getWord8

909+ case i of

910+ 0 -> return EmptyMI

911+ 1 -> do x1 <- get

912+ return (DataMI x1)

913+

893instance Binary IBCFile where

914instance Binary IBCFile where

894− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28)

915+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29)

895 = {-# SCC "putIBCFile" #-}

916 = {-# SCC "putIBCFile" #-}

896 do put x1

917 do put x1

897 put x2

918 put x2

@@ -921,6 +942,7 @@ instance Binary IBCFile where

921 put x26

942 put x26

922 put x27

943 put x27

923 put x28

944 put x28

945+ put x29

924 get

946 get

925 = do x1 <- get

947 = do x1 <- get

926 if x1 == ibcVersion then

948 if x1 == ibcVersion then

@@ -951,7 +973,8 @@ instance Binary IBCFile where

951 x26 <- get

973 x26 <- get

952 x27 <- get

974 x27 <- get

953 x28 <- get

975 x28 <- get

976+ x29 <- get

954− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28)

977+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29)

955 else return (initIBC { ver = x1 })

978 else return (initIBC { ver = x1 })

956

979

957instance Binary DataOpt where

980instance Binary DataOpt where