1- {-# LANGUAGE LambdaCase #-}
2- {-# LANGUAGE TypeOperators #-}
31{-# LANGUAGE AllowAmbiguousTypes #-}
2+ {-# LANGUAGE DataKinds #-}
3+ {-# LANGUAGE DefaultSignatures #-}
4+ {-# LANGUAGE ExistentialQuantification #-}
45{-# LANGUAGE FlexibleContexts #-}
5- {-# LANGUAGE UndecidableSuperClasses #-}
6+ {-# LANGUAGE FlexibleInstances #-}
67{-# LANGUAGE FunctionalDependencies #-}
7- {-# LANGUAGE TypeFamilies #-}
88{-# LANGUAGE GADTs #-}
9- {-# LANGUAGE FlexibleInstances #-}
10- {-# LANGUAGE DefaultSignatures #-}
119{-# LANGUAGE KindSignatures #-}
12- {-# LANGUAGE TypeApplications #-}
10+ {-# LANGUAGE LambdaCase #-}
11+ {-# LANGUAGE OverloadedStrings #-}
12+ {-# LANGUAGE PatternSynonyms #-}
1313{-# LANGUAGE ScopedTypeVariables #-}
1414{-# LANGUAGE StandaloneDeriving #-}
15- {-# LANGUAGE DataKinds #-}
15+ {-# LANGUAGE TypeApplications #-}
16+ {-# LANGUAGE TypeFamilies #-}
17+ {-# LANGUAGE TypeOperators #-}
18+ {-# LANGUAGE UndecidableSuperClasses #-}
1619{-# LANGUAGE ViewPatterns #-}
17- {-# LANGUAGE ExistentialQuantification #-}
18- {-# LANGUAGE PatternSynonyms #-}
19- {-# LANGUAGE OverloadedStrings #-}
2020{-# OPTIONS_GHC -Wno-orphans #-}
2121
22- module Constrained.Spec.List
23- ( ListSpec (.. )
24- , ListW (.. )
25- , ElemW (.. )
26- , pattern Elem
27- , append_
28- , singletonList_
29- , elem_
30- , sum_
31- , foldMap_
32- , Foldy (.. )
33- , FoldSpec (.. )
34- , preMapFoldSpec
35- , toPredsFoldSpec
36- , adds
37- , conformsToFoldSpec
38- , combineFoldSpec
39- ) where
22+ module Constrained.Spec.List (
23+ ListSpec (.. ),
24+ ListW (.. ),
25+ ElemW (.. ),
26+ pattern Elem ,
27+ append_ ,
28+ singletonList_ ,
29+ elem_ ,
30+ sum_ ,
31+ foldMap_ ,
32+ Foldy (.. ),
33+ FoldSpec (.. ),
34+ preMapFoldSpec ,
35+ toPredsFoldSpec ,
36+ adds ,
37+ conformsToFoldSpec ,
38+ combineFoldSpec ,
39+ ) where
4040
41- import Constrained.TheKnot
4241import Constrained.AbstractSyntax
4342import Constrained.Base
4443import Constrained.Conformance
@@ -54,6 +53,7 @@ import Constrained.SumList
5453-- TODO: some strange things here, why is SolverStage in here?!
5554-- Because it is mutually recursive with something else in here.
5655import Constrained.Syntax
56+ import Constrained.TheKnot
5757import Control.Applicative
5858import Control.Monad
5959import Data.Foldable
@@ -135,7 +135,6 @@ guardListSpec msg l@(ListSpec _hint must size elemS _fold)
135135 )
136136 | otherwise = (typeSpec l)
137137
138-
139138data ElemW :: [Type ] -> Type -> Type where
140139 ElemW :: HasSpec a => ElemW '[a , [a ]] Bool
141140
@@ -265,7 +264,6 @@ instance Forallable [a] a where
265264 fromForAllSpec es = typeSpec (ListSpec Nothing [] mempty es NoFold )
266265 forAllToList = id
267266
268-
269267instance Logic ListW where
270268 propagateTypeSpec (FoldMapW f) (Unary HOLE ) ts cant =
271269 typeSpec (ListSpec Nothing [] TrueSpec TrueSpec $ FoldSpec f (TypeSpec ts cant))
@@ -341,7 +339,6 @@ instance Logic ListW where
341339 unsafeExists $ \ x' ->
342340 Assert (x ==. appFun (foldMapFn g) x') <> toPreds x' ts
343341
344-
345342data ListW (args :: [Type ]) (res :: Type ) where
346343 FoldMapW :: forall a b . (Foldy b , HasSpec a ) => Fun '[a ] b -> ListW '[[a ]] b
347344 SingletonListW :: HasSpec a => ListW '[a ] [a ]
@@ -624,4 +621,3 @@ instance Sized [a] where
624621 Just zs -> typeSpec (ListSpec Nothing mempty (MemberSpec zs) TrueSpec NoFold )
625622 sizeOfTypeSpec (ListSpec _ _ _ ErrorSpec {} _) = equalSpec 0
626623 sizeOfTypeSpec (ListSpec _ must sizespec _ _) = sizespec <> geqSpec (sizeOf must)
627-
0 commit comments