b5f219e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remove the Lazy flag entirely.

b5f219eMatus Tejiscak13 years ago

src/Idris/AbsSyntaxTree.hs+10−18

compare with master

unifiedsplit

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

407 pscript :: PTerm }

408 deriving (Show, Eq)

409

410−plazy :: Plicity -> Bool

411−plazy tm = Lazy `elem` pargopts tm

412−

413{-!

410{-!

414deriving instance Binary Plicity

411deriving instance Binary Plicity

415deriving instance NFData Plicity

412deriving instance NFData Plicity

416!-}

413!-}

417

414

418−impl = Imp [Lazy] Dynamic False

415+impl = Imp [] Dynamic False

419expl = Exp [] Dynamic False

416expl = Exp [] Dynamic False

420expl_param = Exp [] Dynamic True

417expl_param = Exp [] Dynamic True

421constraint = Constraint [] Dynamic

418constraint = Constraint [] Dynamic

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

793 getTm :: t }

790 getTm :: t }

794 deriving (Show, Eq, Functor)

791 deriving (Show, Eq, Functor)

795

792

796−data ArgOpt = Lazy | HideDisplay | InaccessibleArg

793+data ArgOpt = HideDisplay | InaccessibleArg

797 deriving (Show, Eq)

794 deriving (Show, Eq)

798

795

799−lazyarg :: PArg' t -> Bool

800−lazyarg tm = Lazy `elem` argopts tm

801−

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

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

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

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

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

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

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

810deriving instance NFData PArg'

804deriving instance NFData PArg'

811!-}

805!-}

812

806

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

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

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

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

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

809pconst 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

817

811

818type PArg = PArg' PTerm

812type PArg = PArg' PTerm

819

813

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

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

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

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

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

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

1122 | 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 $

1123+ bracket p 2 . group $

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

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

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

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

1133 | otherwise =

1126 | otherwise =

1134 bracket p 2 . group $

1127 bracket p 2 . group $

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

1128 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

1140 _ -> empty

1133 _ -> empty

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

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

1142 | impl =

1135 | impl =

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

1144− bracket p 2 $

1136+ bracket p 2 $

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

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

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

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

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

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

1148 where

1140 where

1149 st =

1141 st =

src/Idris/Core/Execute.hs−1

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

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

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

197

198−

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

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

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

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

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

200execApp 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

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

466 [] fc False f ns'

467 (f == sUN "Force")

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

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

469 solve

470 ivs' <- get_instances

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

src/Idris/IBC.hs+4−6

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

1317instance Binary ArgOpt where

1318 put x

1319 = case x of

1320− Lazy -> putWord8 0

1320+ HideDisplay -> putWord8 0

1321− HideDisplay -> putWord8 1

1322− InaccessibleArg -> putWord8 2

1321+ InaccessibleArg -> putWord8 1

1323 get

1322 get

1324 = do i <- getWord8

1323 = do i <- getWord8

1325 case i of

1324 case i of

1326− 0 -> return Lazy

1327− 1 -> return HideDisplay

1325+ 0 -> return HideDisplay

1328− 2 -> return InaccessibleArg

1326+ 1 -> return InaccessibleArg

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

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

1330

1328

1331instance Binary Static where

1329instance Binary Static where

src/Idris/ParseExpr.hs+2−2

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

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

808 lchar '{'

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

811 xt <- typeDeclList syn

812 lchar '}'

813 symbol "->"

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

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

817 <|> (do

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

820 script <- simpleExpr syn

821 xt <- typeDeclList syn

822 lchar '}'