97e28f7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Export tactic-implicit arguments properly

commit97e28f7542ead56fe6328b839fe0281cc48ce36c authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 17 Feb 2012, 13:24 (15 years ago) parentc887611

3 files changed+23−1

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2 src/Idris/Coverage.hs+1−1 src/Idris/IBC.hs+20

src/Idris/AbsSyntax.hs+2

@@ -797,6 +797,8 @@ showImp impl tm = se 10 tm where

797797 _ -> ""

798798 se p (PPi (Constraint _ _) n ty sc)

799799 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc

800+ se p (PPi (TacImp _ _ s) n ty sc)

801+ = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc

800802 se p (PApp _ (PRef _ f) [])

801803 | not impl = show f

802804 se p (PApp _ (PRef _ op@(UN (f:_))) args)

src/Idris/Coverage.hs+1−1

@@ -280,7 +280,7 @@ checkTotality path fc n

280280 i <- getIState

281281 let opts = case lookupCtxt Nothing n (idris_flags i) of

282282 [fs] -> fs

283− [] -> []

283+ _ -> []

284284 t' <- case t of

285285 Unchecked ->

286286 case lookupDef Nothing n ctxt of

src/Idris/IBC.hs+20

@@ -777,6 +777,10 @@ instance Binary Plicity where

777777 Constraint x1 x2 -> do putWord8 2

778778 put x1

779779 put x2

780+ TacImp x1 x2 x3 -> do putWord8 3

781+ put x1

782+ put x2

783+ put x3

780784 get

781785 = do i <- getWord8

782786 case i of

@@ -789,6 +793,10 @@ instance Binary Plicity where

789793 2 -> do x1 <- get

790794 x2 <- get

791795 return (Constraint x1 x2)

796+ 3 -> do x1 <- get

797+ x2 <- get

798+ x3 <- get

799+ return (TacImp x1 x2 x3)

792800 _ -> error "Corrupted binary data for Plicity"

793801

794802

@@ -1061,6 +1069,12 @@ instance (Binary t) => Binary (PArg' t) where

10611069 put x1

10621070 put x2

10631071 put x3

1072+ PTacImplicit x1 x2 x3 x4 x5 -> do putWord8 3

1073+ put x1

1074+ put x2

1075+ put x3

1076+ put x4

1077+ put x5

10641078 get

10651079 = do i <- getWord8

10661080 case i of

@@ -1077,6 +1091,12 @@ instance (Binary t) => Binary (PArg' t) where

10771091 x2 <- get

10781092 x3 <- get

10791093 return (PConstraint x1 x2 x3)

1094+ 3 -> do x1 <- get

1095+ x2 <- get

1096+ x3 <- get

1097+ x4 <- get

1098+ x5 <- get

1099+ return (PTacImplicit x1 x2 x3 x4 x5)

10801100 _ -> error "Corrupted binary data for PArg'"

10811101

10821102