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

git.iko.soy/Idris-dev

Separate Core NFData instances

commit4e6adeb1922e7e29f0e09d60f960ea9fda8e8567 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 15 Jan 2014, 18:23 (13 years ago) parentf24ae1d

5 files changed+119−103

compare with master

unifiedsplit

idris.cabal+1 src/Idris/Core/DeepSeq.hs+99 src/Idris/Core/ProofState.hs+7−7 src/Idris/Core/TT.hs+10 src/Idris/DeepSeq.hs+2−96

idris.cabal+1

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

341341 Exposed-modules:

342342 Idris.Core.CaseTree

343343 , Idris.Core.Constraints

344+ , Idris.Core.DeepSeq

344345 , Idris.Core.Elaborate

345346 , Idris.Core.Evaluate

346347 , 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)

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

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

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

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

490+ let tm' = subst x val sc in

491491 return tm'

492492 | otherwise = lift $ tfail $ IncompleteTerm val

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

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

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

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

515515 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

517517 do ns <- unify' ctxt env s tyv

518518 ps <- get

519519 let (uh, uns) = unified ps

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

532532 _ -> hnf ctxt env t

533533 case t' of

534534 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

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

537537 _ -> lift $ tfail $ CantIntroduce t'

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

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

548548patvar :: Name -> RunTactic

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

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

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

553553

554554letbind :: Name -> Raw -> Raw -> RunTactic

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

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

663663 _ -> hnf ctxt env t

664664 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

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

667667 _ -> fail "Nothing to pattern bind"

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

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

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

743743 updateSolved' xs x

744744updateSolved' 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)

746746updateSolved' xs (Bind n b t)

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

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

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

759759

760760solveInProblems x val [] = []

761761solveInProblems 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,

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

764764

765765updateNotunified ns nu = up nu where

src/Idris/Core/TT.hs+10

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

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

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

759759

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+

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

761771substNames [] t = t

762772substNames ((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

34import Idris.Core.TT

45import Idris.AbsSyntax

56import Idris.AbsSyntaxTree

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

1213 rnf Conditional = ()

1314 rnf Unconditional = ()

1415

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−

4116instance NFData IntTy where

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

4318 rnf ITNative = ()

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

4520 rnf ITChar = ()

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

4722

48−

4923instance NFData NativeTy where

5024 rnf IT8 = ()

5125 rnf IT16 = ()

5226 rnf IT32 = ()

5327 rnf IT64 = ()

54−

5528

5629instance NFData ArithTy where

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

5831 rnf ATFloat = ()

5932

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−

12733instance NFData SizeChange where

12834 rnf Smaller = ()

12935 rnf Same = ()