b5f219e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Remove the Lazy flag entirely.

commitb5f219eb2e00abff6ca4f9e40d13eee68f44a8b3 authorMatus Tejiscak <ziman@functor.sk> dateTue 18 Feb 2014, 16:18 (13 years ago) parentc1f89fa

5 files changed+17−28

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+10−18 src/Idris/Core/Execute.hs−1 src/Idris/ElabTerm.hs+1−1 src/Idris/IBC.hs+4−6 src/Idris/ParseExpr.hs+2−2

src/Idris/AbsSyntaxTree.hs+10−18

@@ -407,15 +407,12 @@ data Plicity = Imp { pargopts :: [ArgOpt],

407407 pscript :: PTerm }

408408 deriving (Show, Eq)

409409

410−plazy :: Plicity -> Bool

411−plazy tm = Lazy `elem` pargopts tm

412−

413410{-!

414411deriving instance Binary Plicity

415412deriving instance NFData Plicity

416413!-}

417414

418−impl = Imp [Lazy] Dynamic False

415+impl = Imp [] Dynamic False

419416expl = Exp [] Dynamic False

420417expl_param = Exp [] Dynamic True

421418constraint = Constraint [] Dynamic

@@ -793,12 +790,9 @@ data PArg' t = PImp { priority :: Int,

793790 getTm :: t }

794791 deriving (Show, Eq, Functor)

795792

796−data ArgOpt = Lazy | HideDisplay | InaccessibleArg

793+data ArgOpt = HideDisplay | InaccessibleArg

797794 deriving (Show, Eq)

798795

799−lazyarg :: PArg' t -> Bool

800−lazyarg tm = Lazy `elem` argopts tm

801−

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

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

804798 size (PExp p l nm trm) = 1 + size nm + size trm

@@ -810,10 +804,10 @@ deriving instance Binary PArg'

810804deriving instance NFData PArg'

811805!-}

812806

813−pimp n t mach = PImp 1 mach [Lazy] n t

807+pimp n t mach = PImp 1 mach [] n t

814808pexp t = PExp 1 [] (sMN 0 "arg") t

815809pconst t = PConstraint 1 [] (sMN 0 "carg") t

816−ptacimp n s t = PTacImplicit 2 [Lazy] n s t

810+ptacimp n s t = PTacImplicit 2 [] n s t

817811

818812type PArg = PArg' PTerm

819813

@@ -1126,10 +1120,9 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

11261120 prettySe 10 ((n, False):bnd) sc

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

11281122 | n `elem` allNamesIn sc || impl || n `elem` docArgs =

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

1130− bracket p 2 . group $

1131− enclose open rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1132− st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1123+ bracket p 2 . group $

1124+ enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1125+ st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

11331126 | otherwise =

11341127 bracket p 2 . group $

11351128 group (prettySe 0 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)

@@ -1140,10 +1133,9 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

11401133 _ -> empty

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

11421135 | impl =

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

1144− bracket p 2 $

1145− open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1146− st <> text "->" </> prettySe 10 ((n, True):bnd) sc

1136+ bracket p 2 $

1137+ lparen <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1138+ st <> text "->" </> prettySe 10 ((n, True):bnd) sc

11471139 | otherwise = prettySe 10 ((n, True):bnd) sc

11481140 where

11491141 st =

src/Idris/Core/Execute.hs−1

@@ -195,7 +195,6 @@ doExec env ctxt Erased = return EErased

195195doExec env ctxt Impossible = fail "Tried to execute an impossible case"

196196doExec env ctxt (TType u) = return (EType u)

197197

198−

199198execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

200199execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls

201200execApp env ctxt (EP _ f _) (t:a:delayed:rest)

src/Idris/ElabTerm.hs+1−1

@@ -465,7 +465,7 @@ elab ist info pattern opts fn tm

465465 elabArgs ist (ina || not isinf, guarded, inty)

466466 [] fc False f ns'

467467 (f == sUN "Force")

468− (map (\x -> (lazyarg x, getTm x)) eargs)

468+ (map (\x -> (False, getTm x)) eargs) -- TODO: remove this False arg

469469 solve

470470 ivs' <- get_instances

471471 -- Attempt to resolve any type classes which have 'complete' types,

src/Idris/IBC.hs+4−6

@@ -1317,15 +1317,13 @@ instance Binary FixDecl where

13171317instance Binary ArgOpt where

13181318 put x

13191319 = case x of

1320− Lazy -> putWord8 0

1321− HideDisplay -> putWord8 1

1322− InaccessibleArg -> putWord8 2

1320+ HideDisplay -> putWord8 0

1321+ InaccessibleArg -> putWord8 1

13231322 get

13241323 = do i <- getWord8

13251324 case i of

1326− 0 -> return Lazy

1327− 1 -> return HideDisplay

1328− 2 -> return InaccessibleArg

1325+ 0 -> return HideDisplay

1326+ 1 -> return InaccessibleArg

13291327 _ -> error "Corrupted binary data for Static"

13301328

13311329instance Binary Static where

src/Idris/ParseExpr.hs+2−2

@@ -807,7 +807,7 @@ pi syn =

807807 return (bindList (PPi (Exp opts st False)) xt sc)) <|> (do

808808 lchar '{'

809809 (do reserved "auto"

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

810+ when (st == Static) $ fail "auto type constraints can not be lazy or static"

811811 xt <- typeDeclList syn

812812 lchar '}'

813813 symbol "->"

@@ -816,7 +816,7 @@ pi syn =

816816 (TacImp [] Dynamic (PTactics [Trivial]))) xt sc))

817817 <|> (do

818818 reserved "default"

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

819+ when (st == Static) $ fail "default tactic constraints can not be lazy or static"

820820 script <- simpleExpr syn

821821 xt <- typeDeclList syn

822822 lchar '}'