803194f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Argument options (instead of just a Bool for lazy)

803194fEdwin Brady13 years ago

src/Idris/AbsSyntax.hs+4−4

compare with master

unifiedsplit

@@ -1040,12 +1040,12 @@ addUsingConstraints syn fc t

1040 -- if all of args in ns, then add it

1041 doAdd (UConstraint c args : cs) ns t

1042 | all (\n -> elem n ns) args

1043− = PPi (Constraint False Dynamic "") (sMN 0 "cu")

1043+ = PPi (Constraint [] Dynamic "") (sMN 0 "cu")

1044 (mkConst c args) (doAdd cs ns t)

1045 | otherwise = doAdd cs ns t

1046

1047 mkConst c args = PApp fc (PRef fc c)

1048− (map (\n -> PExp 0 False (PRef fc n) "") args)

1048+ (map (\n -> PExp 0 [] (PRef fc n) "") args)

1049

1050 getConstraints (PPi (Constraint _ _ _) _ c sc)

1051 = getcapp c ++ getConstraints sc

@@ -1175,8 +1175,8 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1175 pibind using [] sc = sc

1176 pibind using (n:ns) sc

1177 = case lookup n using of

1178− Just ty -> PPi (Imp False Dynamic "" False) n ty (pibind using ns sc)

1178+ Just ty -> PPi (Imp [] Dynamic "" False) n ty (pibind using ns sc)

1179− Nothing -> PPi (Imp False Dynamic "" False) n Placeholder

1179+ Nothing -> PPi (Imp [] Dynamic "" False) n Placeholder

1180 (pibind using ns sc)

1181

1182-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+34−21

@@ -352,33 +352,36 @@ deriving instance NFData Static

352!-}

353

354-- Mark bindings with their explicitness, and laziness

355−data Plicity = Imp { plazy :: Bool,

355+data Plicity = Imp { pargopts :: [ArgOpt],

356 pstatic :: Static,

357 pdocstr :: String,

358 pparam :: Bool }

359− | Exp { plazy :: Bool,

359+ | Exp { pargopts :: [ArgOpt],

360 pstatic :: Static,

361 pdocstr :: String,

362 pparam :: Bool }

363− | Constraint { plazy :: Bool,

363+ | Constraint { pargopts :: [ArgOpt],

364 pstatic :: Static,

365 pdocstr :: String }

366− | TacImp { plazy :: Bool,

366+ | TacImp { pargopts :: [ArgOpt],

367 pstatic :: Static,

368 pscript :: PTerm,

369 pdocstr :: String }

370 deriving (Show, Eq)

371

372+plazy :: Plicity -> Bool

373+plazy tm = Lazy `elem` pargopts tm

374+

372{-!

375{-!

373deriving instance Binary Plicity

376deriving instance Binary Plicity

374deriving instance NFData Plicity

377deriving instance NFData Plicity

375!-}

378!-}

376

379

377−impl = Imp False Dynamic "" False

380+impl = Imp [Lazy] Dynamic "" False

378−expl = Exp False Dynamic "" False

381+expl = Exp [] Dynamic "" False

379−expl_param = Exp False Dynamic "" True

382+expl_param = Exp [] Dynamic "" True

380−constraint = Constraint False Dynamic ""

383+constraint = Constraint [] Dynamic ""

381−tacimpl t = TacImp False Dynamic t ""

384+tacimpl t = TacImp [] Dynamic t ""

382

385

383data FnOpt = Inlinable -- always evaluate when simplifying

386data FnOpt = Inlinable -- always evaluate when simplifying

384 | TotalFn | PartialFn

387 | TotalFn | PartialFn

@@ -724,21 +727,31 @@ type PDo = PDo' PTerm

724

727

725data PArg' t = PImp { priority :: Int,

728data PArg' t = PImp { priority :: Int,

726 machine_inf :: Bool, -- true if the machine inferred it

729 machine_inf :: Bool, -- true if the machine inferred it

730+ argopts :: [ArgOpt],

727− lazyarg :: Bool, pname :: Name, getTm :: t,

731+ pname :: Name, getTm :: t,

728 pargdoc :: String }

732 pargdoc :: String }

729 | PExp { priority :: Int,

733 | PExp { priority :: Int,

734+ argopts :: [ArgOpt],

730− lazyarg :: Bool, getTm :: t,

735+ getTm :: t,

731 pargdoc :: String }

736 pargdoc :: String }

732 | PConstraint { priority :: Int,

737 | PConstraint { priority :: Int,

738+ argopts :: [ArgOpt],

733− lazyarg :: Bool, getTm :: t,

739+ getTm :: t,

734 pargdoc :: String }

740 pargdoc :: String }

735 | PTacImplicit { priority :: Int,

741 | PTacImplicit { priority :: Int,

742+ argopts :: [ArgOpt],

736− lazyarg :: Bool, pname :: Name,

743+ pname :: Name,

737 getScript :: t,

744 getScript :: t,

738 getTm :: t,

745 getTm :: t,

739 pargdoc :: String }

746 pargdoc :: String }

740 deriving (Show, Eq, Functor)

747 deriving (Show, Eq, Functor)

741

748

749+data ArgOpt = Lazy | HideDisplay

750+ deriving (Show, Eq)

751+

752+lazyarg :: PArg' t -> Bool

753+lazyarg tm = Lazy `elem` argopts tm

754+

742instance Sized a => Sized (PArg' a) where

755instance Sized a => Sized (PArg' a) where

743 size (PImp p _ l nm trm _) = 1 + size nm + size trm

756 size (PImp p _ l nm trm _) = 1 + size nm + size trm

744 size (PExp p l trm _) = 1 + size trm

757 size (PExp p l trm _) = 1 + size trm

@@ -750,10 +763,10 @@ deriving instance Binary PArg'

750deriving instance NFData PArg'

763deriving instance NFData PArg'

751!-}

764!-}

752

765

753−pimp n t mach = PImp 1 mach True n t ""

766+pimp n t mach = PImp 1 mach [Lazy] n t ""

754−pexp t = PExp 1 False t ""

767+pexp t = PExp 1 [] t ""

755−pconst t = PConstraint 1 False t ""

768+pconst t = PConstraint 1 [] t ""

756−ptacimp n s t = PTacImplicit 2 True n s t ""

769+ptacimp n s t = PTacImplicit 2 [Lazy] n s t ""

757

770

758type PArg = PArg' PTerm

771type PArg = PArg' PTerm

759

772

@@ -1003,7 +1016,7 @@ prettyImp impl = prettySe 10

1003 prettySe 10 sc

1016 prettySe 10 sc

1004 prettySe p (PPi (Exp l s _ _) n ty sc)

1017 prettySe p (PPi (Exp l s _ _) n ty sc)

1005 | n `elem` allNamesIn sc || impl =

1018 | n `elem` allNamesIn sc || impl =

1006− let open = if l then text "|" <> lparen else lparen in

1019+ let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1007 bracket p 2 $

1020 bracket p 2 $

1008 if size sc > breakingSize then

1021 if size sc > breakingSize then

1009 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>

1022 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>

@@ -1024,7 +1037,7 @@ prettyImp impl = prettySe 10

1024 _ -> empty

1037 _ -> empty

1025 prettySe p (PPi (Imp l s _ _) n ty sc)

1038 prettySe p (PPi (Imp l s _ _) n ty sc)

1026 | impl =

1039 | impl =

1027− let open = if l then text "|" <> lbrace else lbrace in

1040+ let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

1028 bracket p 2 $

1041 bracket p 2 $

1029 if size sc > breakingSize then

1042 if size sc > breakingSize then

1030 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>

1043 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>

@@ -1217,7 +1230,7 @@ showImp ist impl colour tm = se 10 [] tm where

1217 se p bnd (PPi (Exp l s _ param) n ty sc)

1230 se p bnd (PPi (Exp l s _ param) n ty sc)

1218 | n `elem` allNamesIn sc || impl

1231 | n `elem` allNamesIn sc || impl

1219 = bracket p 2 $

1232 = bracket p 2 $

1220− (if l then "|(" else "(") ++

1233+ (if Lazy `elem` l then "|(" else "(") ++

1221 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1234 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1222 ") " ++

1235 ") " ++

1223 (if (impl && param) then "P" else "") ++

1236 (if (impl && param) then "P" else "") ++

@@ -1228,7 +1241,7 @@ showImp ist impl colour tm = se 10 [] tm where

1228 Static -> "[static] "

1241 Static -> "[static] "

1229 _ -> ""

1242 _ -> ""

1230 se p bnd (PPi (Imp l s _ _) n ty sc)

1243 se p bnd (PPi (Imp l s _ _) n ty sc)

1231− | impl = bracket p 2 $ (if l then "|{" else "{") ++

1244+ | impl = bracket p 2 $ (if Lazy `elem` l then "|{" else "{") ++

1232 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1245 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1233 "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc

1246 "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc

1234 | otherwise = se 10 ((n, True):bnd) sc

1247 | otherwise = se 10 ((n, True):bnd) sc

src/Idris/Coverage.hs+1−1

@@ -56,7 +56,7 @@ genClauses fc n xs given

56 -- there may be more case splitting that the idris_implicits record

57 -- suggests)

58 let parg = case lookupCtxt n (idris_implicits i) of

59− (p : _) -> p ++ repeat (PExp 0 False Placeholder "")

59+ (p : _) -> p ++ repeat (PExp 0 [] Placeholder "")

60 _ -> repeat (pexp Placeholder)

61 let tryclauses = mkClauses parg all_args

62 logLvl 2 $ show (length tryclauses) ++ " initially to check"

src/Idris/DeepSeq.hs+3

@@ -53,6 +53,9 @@ instance NFData Static where

53 rnf Static = ()

54 rnf Dynamic = ()

56+instance NFData ArgOpt where

57+ rnf _ = ()

58+

56instance NFData Plicity where

59instance NFData Plicity where

57 rnf (Imp x1 x2 x3 x4)

60 rnf (Imp x1 x2 x3 x4)

58 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

61 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

src/Idris/ElabDecls.hs+5−4

@@ -842,7 +842,8 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

842 else return ()

843 tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))

844

845− mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)

845+ mkLazy (PPi pl n ty sc)

846+ = PPi (pl { pargopts = nub (Lazy : pargopts pl) }) n ty (mkLazy sc)

846 mkLazy t = t

847 mkLazy t = t

847

848

848 getNamePos :: Int -> PTerm -> Name -> Maybe Int

849 getNamePos :: Int -> PTerm -> Name -> Maybe Int

@@ -1908,11 +1909,11 @@ elabInstance info syn what fc cs n ps t expn ds = do

1908 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

1909 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

1909 lamBind i _ sc = sc

1910 lamBind i _ sc = sc

1910 methArgs i (PPi (Imp _ _ _ _) n ty sc)

1911 methArgs i (PPi (Imp _ _ _ _) n ty sc)

1911− = PImp 0 True False n (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

1912+ = PImp 0 True [] n (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

1912 methArgs i (PPi (Exp _ _ _ _) n ty sc)

1913 methArgs i (PPi (Exp _ _ _ _) n ty sc)

1913− = PExp 0 False (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

1914+ = PExp 0 [] (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

1914 methArgs i (PPi (Constraint _ _ _) n ty sc)

1915 methArgs i (PPi (Constraint _ _ _) n ty sc)

1915− = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc

1916+ = PConstraint 0 [] (PResolveTC fc) "" : methArgs (i+1) sc

1916 methArgs i _ = []

1917 methArgs i _ = []

1917

1918

1918 papp fc f [] = f

1919 papp fc f [] = f

src/Idris/ElabTerm.hs−6

@@ -222,12 +222,6 @@ elab ist info pattern opts fn tm

222 ctxt <- get_context

223 let (tc, _) = unApply ty

224 let as' = pruneByType tc ctxt as

225−-- case as' of

226−-- [a] -> elab' ina a

227−-- as -> lift $ tfail $ CantResolveAlts (map showHd as)

228−-- trace ("Original " ++ show (length as, as) ++ "\n" ++

229−-- "New " ++ show (length as', as)) $

230−-- traceWhen (length as' > 1) (show as') $

231 tryAll (zip (map (elab' ina) as') (map showHd as'))

225 tryAll (zip (map (elab' ina) as') (map showHd as'))

232 where showHd (PApp _ h _) = show h

226 where showHd (PApp _ h _) = show h

233 showHd x = show x

227 showHd x = show x

src/Idris/IBC.hs+12

@@ -1153,6 +1153,18 @@ instance Binary FixDecl where

1153 return (Fix x1 x2)

1154

1155

1156+instance Binary ArgOpt where

1157+ put x

1158+ = case x of

1159+ Lazy -> putWord8 0

1160+ HideDisplay -> putWord8 1

1161+ get

1162+ = do i <- getWord8

1163+ case i of

1164+ 0 -> return Lazy

1165+ 1 -> return HideDisplay

1166+ _ -> error "Corrupted binary data for Static"

1167+

1156instance Binary Static where

1168instance Binary Static where

1157 put x

1169 put x

1158 = case x of

1170 = case x of

src/Idris/ParseExpr.hs+9−9

@@ -769,39 +769,39 @@ Pi ::=

769

770pi :: SyntaxInfo -> IdrisParser PTerm

771pi syn =

772− do lazy <- if implicitAllowed syn -- laziness is top level only

772+ do opts <- if implicitAllowed syn -- laziness is top level only

773− then option False (do lchar '|'; return True)

773+ then option [] (do lchar '|'; return [Lazy])

774− else return False

774+ else return []

775 st <- static

776 (do try(lchar '('); xt <- typeDeclList syn; lchar ')'

777 doc <- option "" (docComment '^')

778 symbol "->"

779 sc <- expr syn

780− return (bindList (PPi (Exp lazy st doc False)) xt sc)) <|> (do

780+ return (bindList (PPi (Exp opts st doc False)) xt sc)) <|> (do

781 lchar '{'

782 (do reserved "auto"

783− when (lazy || (st == Static)) $ fail "auto type constraints can not be lazy or static"

783+ when (Lazy `elem` opts || (st == Static)) $ fail "auto type constraints can not be lazy or static"

784 xt <- typeDeclList syn

785 lchar '}'

786 symbol "->"

787 sc <- expr syn

788 return (bindList (PPi

789− (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))

789+ (TacImp [] Dynamic (PTactics [Trivial]) "")) xt sc))

790 <|> (do

791 reserved "default"

792− when (lazy || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

792+ when (Lazy `elem` opts || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

793 script <- simpleExpr syn

794 xt <- typeDeclList syn

795 lchar '}'

796 symbol "->"

797 sc <- expr syn

798− return (bindList (PPi (TacImp False Dynamic script "")) xt sc))

798+ return (bindList (PPi (TacImp [] Dynamic script "")) xt sc))

799 <|> (if implicitAllowed syn then do

800 xt <- typeDeclList syn

801 lchar '}'

802 symbol "->"

803 sc <- expr syn

804− return (bindList (PPi (Imp lazy st "" False)) xt sc)

804+ return (bindList (PPi (Imp opts st "" False)) xt sc)

805 else do fail "no implicit arguments allowed here"))

806 <?> "dependent type signature"

807

src/Idris/Providers.hs+1−1

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

12-- | Wrap a type provider in the type of type providers

13providerTy :: FC -> PTerm -> PTerm

14−providerTy fc tm = PApp fc (PRef fc $ sUN "Provider") [PExp 0 False tm ""]

14+providerTy fc tm = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] tm ""]

16ioret = sUN "prim_io_return"

17ermod = sNS (sUN "Error") ["Providers"]