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

git.iko.soy/Idris-dev

on master help sign in

Export tactic-implicit arguments properly

97e28f7Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+2

compare with master

unifiedsplit

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

797 _ -> ""

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

799 = 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

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

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

801 | not impl = show f

803 | not impl = show f

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

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

src/Idris/Coverage.hs+1−1

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

280 i <- getIState

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

282 [fs] -> fs

283− [] -> []

283+ _ -> []

284 t' <- case t of

285 Unchecked ->

286 case lookupDef Nothing n ctxt of

src/Idris/IBC.hs+20

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

777 Constraint x1 x2 -> do putWord8 2

778 put x1

779 put x2

780+ TacImp x1 x2 x3 -> do putWord8 3

781+ put x1

782+ put x2

783+ put x3

780 get

784 get

781 = do i <- getWord8

785 = do i <- getWord8

782 case i of

786 case i of

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

789 2 -> do x1 <- get

793 2 -> do x1 <- get

790 x2 <- get

794 x2 <- get

791 return (Constraint x1 x2)

795 return (Constraint x1 x2)

796+ 3 -> do x1 <- get

797+ x2 <- get

798+ x3 <- get

799+ return (TacImp x1 x2 x3)

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

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

793

801

794

802

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

1061 put x1

1069 put x1

1062 put x2

1070 put x2

1063 put x3

1071 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

1064 get

1078 get

1065 = do i <- getWord8

1079 = do i <- getWord8

1066 case i of

1080 case i of

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

1077 x2 <- get

1091 x2 <- get

1078 x3 <- get

1092 x3 <- get

1079 return (PConstraint x1 x2 x3)

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

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

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

1081

1101

1082

1102