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

git.iko.soy/Idris-dev

Argument options (instead of just a Bool for lazy)

commit803194f5d7a4d2d3c835c34cf7b53ae34b6a3b0b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 24 Jan 2014, 22:22 (13 years ago) parent5080735

9 files changed+69−46

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+4−4 src/Idris/AbsSyntaxTree.hs+34−21 src/Idris/Coverage.hs+1−1 src/Idris/DeepSeq.hs+3 src/Idris/ElabDecls.hs+5−4 src/Idris/ElabTerm.hs−6 src/Idris/IBC.hs+12 src/Idris/ParseExpr.hs+9−9 src/Idris/Providers.hs+1−1

src/Idris/AbsSyntax.hs+4−4

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

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

10411041 doAdd (UConstraint c args : cs) ns t

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

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

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

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

10451045 | otherwise = doAdd cs ns t

10461046

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

10491049

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

10511051 = getcapp c ++ getConstraints sc

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

11751175 pibind using [] sc = sc

11761176 pibind using (n:ns) sc

11771177 = case lookup n using of

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

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

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

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

11801180 (pibind using ns sc)

11811181

11821182-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+34−21

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

352352!-}

353353

354354-- Mark bindings with their explicitness, and laziness

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

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

356356 pstatic :: Static,

357357 pdocstr :: String,

358358 pparam :: Bool }

359− | Exp { plazy :: Bool,

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

360360 pstatic :: Static,

361361 pdocstr :: String,

362362 pparam :: Bool }

363− | Constraint { plazy :: Bool,

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

364364 pstatic :: Static,

365365 pdocstr :: String }

366− | TacImp { plazy :: Bool,

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

367367 pstatic :: Static,

368368 pscript :: PTerm,

369369 pdocstr :: String }

370370 deriving (Show, Eq)

371371

372+plazy :: Plicity -> Bool

373+plazy tm = Lazy `elem` pargopts tm

374+

372375{-!

373376deriving instance Binary Plicity

374377deriving instance NFData Plicity

375378!-}

376379

377−impl = Imp False Dynamic "" False

378−expl = Exp False Dynamic "" False

379−expl_param = Exp False Dynamic "" True

380−constraint = Constraint False Dynamic ""

381−tacimpl t = TacImp False Dynamic t ""

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

381+expl = Exp [] Dynamic "" False

382+expl_param = Exp [] Dynamic "" True

383+constraint = Constraint [] Dynamic ""

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

382385

383386data FnOpt = Inlinable -- always evaluate when simplifying

384387 | TotalFn | PartialFn

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

724727

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

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

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

730+ argopts :: [ArgOpt],

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

728732 pargdoc :: String }

729733 | PExp { priority :: Int,

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

734+ argopts :: [ArgOpt],

735+ getTm :: t,

731736 pargdoc :: String }

732737 | PConstraint { priority :: Int,

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

738+ argopts :: [ArgOpt],

739+ getTm :: t,

734740 pargdoc :: String }

735741 | PTacImplicit { priority :: Int,

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

742+ argopts :: [ArgOpt],

743+ pname :: Name,

737744 getScript :: t,

738745 getTm :: t,

739746 pargdoc :: String }

740747 deriving (Show, Eq, Functor)

741748

749+data ArgOpt = Lazy | HideDisplay

750+ deriving (Show, Eq)

751+

752+lazyarg :: PArg' t -> Bool

753+lazyarg tm = Lazy `elem` argopts tm

754+

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

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

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

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

750763deriving instance NFData PArg'

751764!-}

752765

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

754−pexp t = PExp 1 False t ""

755−pconst t = PConstraint 1 False t ""

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

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

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

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

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

757770

758771type PArg = PArg' PTerm

759772

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

10031016 prettySe 10 sc

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

10051018 | 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

10071020 bracket p 2 $

10081021 if size sc > breakingSize then

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

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

10241037 _ -> empty

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

10261039 | 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

10281041 bracket p 2 $

10291042 if size sc > breakingSize then

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

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

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

12181231 | n `elem` allNamesIn sc || impl

12191232 = bracket p 2 $

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

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

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

12221235 ") " ++

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

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

12281241 Static -> "[static] "

12291242 _ -> ""

12301243 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 "{") ++

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

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

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

src/Idris/Coverage.hs+1−1

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

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

5757 -- suggests)

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

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

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

6060 _ -> repeat (pexp Placeholder)

6161 let tryclauses = mkClauses parg all_args

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

src/Idris/DeepSeq.hs+3

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

5353 rnf Static = ()

5454 rnf Dynamic = ()

5555

56+instance NFData ArgOpt where

57+ rnf _ = ()

58+

5659instance NFData Plicity where

5760 rnf (Imp x1 x2 x3 x4)

5861 = 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)

842842 else return ()

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

844844

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)

846847 mkLazy t = t

847848

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

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

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

19091910 lamBind i _ sc = sc

19101911 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

19121913 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

19141915 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

19161917 methArgs i _ = []

19171918

19181919 papp fc f [] = f

src/Idris/ElabTerm.hs−6

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

222222 ctxt <- get_context

223223 let (tc, _) = unApply ty

224224 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') $

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

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

233227 showHd x = show x

src/Idris/IBC.hs+12

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

11531153 return (Fix x1 x2)

11541154

11551155

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+

11561168instance Binary Static where

11571169 put x

11581170 = case x of

src/Idris/ParseExpr.hs+9−9

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

769769

770770pi :: SyntaxInfo -> IdrisParser PTerm

771771pi syn =

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

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

774− else return False

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

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

774+ else return []

775775 st <- static

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

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

778778 symbol "->"

779779 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

781781 lchar '{'

782782 (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"

784784 xt <- typeDeclList syn

785785 lchar '}'

786786 symbol "->"

787787 sc <- expr syn

788788 return (bindList (PPi

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

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

790790 <|> (do

791791 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"

793793 script <- simpleExpr syn

794794 xt <- typeDeclList syn

795795 lchar '}'

796796 symbol "->"

797797 sc <- expr syn

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

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

799799 <|> (if implicitAllowed syn then do

800800 xt <- typeDeclList syn

801801 lchar '}'

802802 symbol "->"

803803 sc <- expr syn

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

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

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

806806 <?> "dependent type signature"

807807

src/Idris/Providers.hs+1−1

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

1111

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

1313providerTy :: 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 ""]

1515

1616ioret = sUN "prim_io_return"

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