4e6adeb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Separate Core NFData instances

4e6adebEdwin Brady13 years ago

idris.cabal+1

compare with master

unifiedsplit

@@ -341,6 +341,7 @@ Library

341 Exposed-modules:

342 Idris.Core.CaseTree

343 , Idris.Core.Constraints

344+ , Idris.Core.DeepSeq

344 , Idris.Core.Elaborate

345 , Idris.Core.Elaborate

345 , Idris.Core.Evaluate

346 , Idris.Core.Evaluate

346 , Idris.Core.Execute

347 , Idris.Core.Execute

src/Idris/Core/DeepSeq.hsnew file+99

@@ -0,0 +1,99 @@

1+module Idris.Core.DeepSeq where

3+import Idris.Core.TT

5+import Control.DeepSeq

7+instance NFData Name where

8+ rnf (UN x1) = rnf x1 `seq` ()

9+ rnf (NS x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

10+ rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

11+ rnf NErased = ()

12+ rnf (SN x1) = rnf x1 `seq` ()

13+

14+instance NFData SpecialName where

15+ rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

16+ rnf (InstanceN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

17+ rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

18+ rnf (MethodN x1) = rnf x1 `seq` ()

19+ rnf (CaseN x1) = rnf x1 `seq` ()

20+ rnf (ElimN x1) = rnf x1 `seq` ()

21+

22+instance NFData Raw where

23+ rnf (Var x1) = rnf x1 `seq` ()

24+ rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

25+ rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

26+ rnf RType = ()

27+ rnf (RForce x1) = rnf x1 `seq` ()

28+ rnf (RConstant x1) = x1 `seq` ()

29+

30+instance NFData FC where

31+ rnf (FC x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

32+

33+instance NFData Err where

34+ rnf (Msg x1) = rnf x1 `seq` ()

35+ rnf (InternalMsg x1) = rnf x1 `seq` ()

36+ rnf (CantUnify x1 x2 x3 x4 x5 x6)

37+ = rnf x1 `seq`

38+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

39+ rnf (InfiniteUnify x1 x2 x3)

40+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

41+ rnf (CantConvert x1 x2 x3)

42+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

43+ rnf (UnifyScope x1 x2 x3 x4)

44+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

45+ rnf (CantInferType x1) = rnf x1 `seq` ()

46+ rnf (NonFunctionType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

47+ rnf (CantIntroduce x1) = rnf x1 `seq` ()

48+ rnf (NoSuchVariable x1) = rnf x1 `seq` ()

49+ rnf (NoTypeDecl x1) = rnf x1 `seq` ()

50+ rnf (NotInjective x1 x2 x3)

51+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

52+ rnf (CantResolve x1) = rnf x1 `seq` ()

53+ rnf (CantResolveAlts x1) = rnf x1 `seq` ()

54+ rnf (IncompleteTerm x1) = rnf x1 `seq` ()

55+ rnf UniverseError = ()

56+ rnf ProgramLineComment = ()

57+ rnf (Inaccessible x1) = rnf x1 `seq` ()

58+ rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()

59+ rnf (AlreadyDefined x1) = rnf x1 `seq` ()

60+ rnf (ProofSearchFail x1) = rnf x1 `seq` ()

61+ rnf (NoRewriting x1) = rnf x1 `seq` ()

62+ rnf (At x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

63+ rnf (Elaborating x1 x2 x3)

64+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

65+ rnf (ProviderError x1) = rnf x1 `seq` ()

66+ rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

67+

68+instance (NFData b) => NFData (Binder b) where

69+ rnf (Lam x1) = rnf x1 `seq` ()

70+ rnf (Pi x1) = rnf x1 `seq` ()

71+ rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

72+ rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

73+ rnf (Hole x1) = rnf x1 `seq` ()

74+ rnf (GHole x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

75+ rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

76+ rnf (PVar x1) = rnf x1 `seq` ()

77+ rnf (PVTy x1) = rnf x1 `seq` ()

78+

79+instance NFData UExp where

80+ rnf (UVar x1) = rnf x1 `seq` ()

81+ rnf (UVal x1) = rnf x1 `seq` ()

82+

83+instance NFData NameType where

84+ rnf Bound = ()

85+ rnf Ref = ()

86+ rnf (DCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

87+ rnf (TCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

88+

89+instance (NFData n) => NFData (TT n) where

90+ rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

91+ rnf (V x1) = rnf x1 `seq` ()

92+ rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

93+ rnf (App x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

94+ rnf (Constant x1) = x1 `seq` ()

95+ rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

96+ rnf Erased = ()

97+ rnf Impossible = ()

98+ rnf (TType x1) = rnf x1 `seq` ()

99+

src/Idris/Core/ProofState.hs+7−7

@@ -487,7 +487,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

487 -- dontunify = dontunify ps \\ [x],

488 -- unified = (uh, uns ++ [(x, val)]),

489 instances = instances ps \\ [x] })

490− let tm' = instantiate val (pToV x sc) in

490+ let tm' = subst x val sc in

491 return tm'

492 | otherwise = lift $ tfail $ IncompleteTerm val

493solve _ _ h@(Bind x t sc)

@@ -513,7 +513,7 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

513 (tyv, tyt) <- lift $ check ctxt env ty

514-- ns <- lift $ unify ctxt env tyv t'

515 case t' of

516− Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

516+ Bind y (Pi s) t -> let t' = subst y (P Bound n s) t in

517 do ns <- unify' ctxt env s tyv

518 ps <- get

519 let (uh, uns) = unified ps

@@ -532,7 +532,7 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

532 _ -> hnf ctxt env t

533 case t' of

534 Bind y (Pi s) t -> -- trace ("in type " ++ show t') $

535− let t' = instantiate (P Bound n s) (pToV y t) in

535+ let t' = subst y (P Bound n s) t in

536 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

537 _ -> lift $ tfail $ CantIntroduce t'

538intro n ctxt env _ = fail "Can't introduce here."

@@ -548,7 +548,7 @@ forall n ty ctxt env _ = fail "Can't pi bind here"

548patvar :: Name -> RunTactic

549patvar n ctxt env (Bind x (Hole t) sc) =

550 do action (\ps -> ps { holes = holes ps \\ [x] })

551− return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))

551+ return $ Bind n (PVar t) (subst x (P Bound n t) sc)

552patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm

553

554letbind :: Name -> Raw -> Raw -> RunTactic

@@ -662,7 +662,7 @@ patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

662 x@(Bind y (PVTy s) t) -> x

663 _ -> hnf ctxt env t

664 case t' of

665− Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

665+ Bind y (PVTy s) t -> let t' = subst y (P Bound n s) t in

666 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))

667 _ -> fail "Nothing to pattern bind"

668patbind n ctxt env _ = fail "Can't pattern bind here"

@@ -742,7 +742,7 @@ keepGiven du (u : us) hs = keepGiven du us hs

742updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $

743 updateSolved' xs x

744updateSolved' xs (Bind n (Hole ty) t)

745− | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t))

745+ | Just v <- lookup n xs = psubst n v (updateSolved' xs t)

746updateSolved' xs (Bind n b t)

747 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)

748updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)

@@ -759,7 +759,7 @@ updateError ns e = e

759

760solveInProblems x val [] = []

761solveInProblems x val ((l, r, env, err) : ps)

762− = ((instantiate val (pToV x l), instantiate val (pToV x r),

762+ = ((psubst x val l, psubst x val r,

763 updateEnv [(x, val)] env, err) : solveInProblems x val ps)

764

765updateNotunified ns nu = up nu where

src/Idris/Core/TT.hs+10

@@ -757,6 +757,16 @@ finalise t = t

757subst :: Eq n => n -> TT n -> TT n -> TT n

758subst n v tm = instantiate v (pToV n tm)

759

760+-- If there are no Vs in the term (i.e. in proof state)

761+psubst :: Eq n => n -> TT n -> TT n -> TT n

762+psubst n v tm = s' tm where

763+ s' (P _ x _) | n == x = v

764+ s' (Bind x b sc) | n == x = Bind x (fmap s' b) sc

765+ | otherwise = Bind x (fmap s' b) (s' sc)

766+ s' (App f a) = App (s' f) (s' a)

767+ s' (Proj t idx) = Proj (s' t) idx

768+ s' t = t

769+

760substNames :: Eq n => [(n, TT n)] -> TT n -> TT n

770substNames :: Eq n => [(n, TT n)] -> TT n -> TT n

761substNames [] t = t

771substNames [] t = t

762substNames ((n, tm) : xs) t = subst n tm (substNames xs t)

772substNames ((n, tm) : xs) t = subst n tm (substNames xs t)

src/Idris/DeepSeq.hs+2−96

@@ -1,5 +1,6 @@

1−module Idris.DeepSeq where

1+module Idris.DeepSeq(module Idris.DeepSeq, module Idris.Core.DeepSeq) where

3+import Idris.Core.DeepSeq

3import Idris.Core.TT

4import Idris.Core.TT

4import Idris.AbsSyntax

5import Idris.AbsSyntax

5import Idris.AbsSyntaxTree

6import Idris.AbsSyntaxTree

@@ -12,32 +13,6 @@ instance NFData Forceability where

12 rnf Conditional = ()

13 rnf Conditional = ()

13 rnf Unconditional = ()

14 rnf Unconditional = ()

15−instance NFData Raw where

16− rnf (Var x1) = rnf x1 `seq` ()

17− rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

18− rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

19− rnf RType = ()

20− rnf (RForce x1) = rnf x1 `seq` ()

21− rnf (RConstant x1) = x1 `seq` ()

22−

23−instance NFData FC where

24− rnf (FC x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

25−

26−instance NFData Name where

27− rnf (UN x1) = rnf x1 `seq` ()

28− rnf (NS x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

29− rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

30− rnf NErased = ()

31− rnf (SN x1) = rnf x1 `seq` ()

32−

33−instance NFData SpecialName where

34− rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

35− rnf (InstanceN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

36− rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

37− rnf (MethodN x1) = rnf x1 `seq` ()

38− rnf (CaseN x1) = rnf x1 `seq` ()

39− rnf (ElimN x1) = rnf x1 `seq` ()

40−

41instance NFData IntTy where

16instance NFData IntTy where

42 rnf (ITFixed x1) = rnf x1 `seq` ()

17 rnf (ITFixed x1) = rnf x1 `seq` ()

43 rnf ITNative = ()

18 rnf ITNative = ()

@@ -45,85 +20,16 @@ instance NFData IntTy where

45 rnf ITChar = ()

20 rnf ITChar = ()

46 rnf (ITVec x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

21 rnf (ITVec x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

48−

49instance NFData NativeTy where

23instance NFData NativeTy where

50 rnf IT8 = ()

24 rnf IT8 = ()

51 rnf IT16 = ()

25 rnf IT16 = ()

52 rnf IT32 = ()

26 rnf IT32 = ()

53 rnf IT64 = ()

27 rnf IT64 = ()

54−

56instance NFData ArithTy where

29instance NFData ArithTy where

57 rnf (ATInt x1) = rnf x1 `seq` ()

30 rnf (ATInt x1) = rnf x1 `seq` ()

58 rnf ATFloat = ()

31 rnf ATFloat = ()

60−instance NFData Err where

61− rnf (Msg x1) = rnf x1 `seq` ()

62− rnf (InternalMsg x1) = rnf x1 `seq` ()

63− rnf (CantUnify x1 x2 x3 x4 x5 x6)

64− = rnf x1 `seq`

65− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

66− rnf (InfiniteUnify x1 x2 x3)

67− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

68− rnf (CantConvert x1 x2 x3)

69− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

70− rnf (UnifyScope x1 x2 x3 x4)

71− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

72− rnf (CantInferType x1) = rnf x1 `seq` ()

73− rnf (NonFunctionType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

74− rnf (CantIntroduce x1) = rnf x1 `seq` ()

75− rnf (NoSuchVariable x1) = rnf x1 `seq` ()

76− rnf (NoTypeDecl x1) = rnf x1 `seq` ()

77− rnf (NotInjective x1 x2 x3)

78− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

79− rnf (CantResolve x1) = rnf x1 `seq` ()

80− rnf (CantResolveAlts x1) = rnf x1 `seq` ()

81− rnf (IncompleteTerm x1) = rnf x1 `seq` ()

82− rnf UniverseError = ()

83− rnf ProgramLineComment = ()

84− rnf (Inaccessible x1) = rnf x1 `seq` ()

85− rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()

86− rnf (AlreadyDefined x1) = rnf x1 `seq` ()

87− rnf (ProofSearchFail x1) = rnf x1 `seq` ()

88− rnf (NoRewriting x1) = rnf x1 `seq` ()

89− rnf (At x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

90− rnf (Elaborating x1 x2 x3)

91− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

92− rnf (ProviderError x1) = rnf x1 `seq` ()

93− rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

94−

95−instance (NFData b) => NFData (Binder b) where

96− rnf (Lam x1) = rnf x1 `seq` ()

97− rnf (Pi x1) = rnf x1 `seq` ()

98− rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

99− rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

100− rnf (Hole x1) = rnf x1 `seq` ()

101− rnf (GHole x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

102− rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

103− rnf (PVar x1) = rnf x1 `seq` ()

104− rnf (PVTy x1) = rnf x1 `seq` ()

105−

106−instance NFData UExp where

107− rnf (UVar x1) = rnf x1 `seq` ()

108− rnf (UVal x1) = rnf x1 `seq` ()

109−

110−instance NFData NameType where

111− rnf Bound = ()

112− rnf Ref = ()

113− rnf (DCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

114− rnf (TCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

115−

116−instance (NFData n) => NFData (TT n) where

117− rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

118− rnf (V x1) = rnf x1 `seq` ()

119− rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

120− rnf (App x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

121− rnf (Constant x1) = x1 `seq` ()

122− rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

123− rnf Erased = ()

124− rnf Impossible = ()

125− rnf (TType x1) = rnf x1 `seq` ()

126−

127instance NFData SizeChange where

33instance NFData SizeChange where

128 rnf Smaller = ()

34 rnf Smaller = ()

129 rnf Same = ()

35 rnf Same = ()