diff --git a/CONTRIBUTORS b/CONTRIBUTORS --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -3,3 +3,5 @@ * Anders Persson * Daniel Schoepe * Dmytro Lypai + * Johan Ankner + * Peter Jonsson diff --git a/examples/NanoFeldspar/Core.hs b/examples/NanoFeldspar/Core.hs --- a/examples/NanoFeldspar/Core.hs +++ b/examples/NanoFeldspar/Core.hs @@ -34,6 +34,7 @@ import Language.Syntactic.Constructs.Tuple import Language.Syntactic.Frontend.Tuple import Language.Syntactic.Sharing.SimpleCodeMotion +import Language.Syntactic.Sharing.CodeMotion2 @@ -157,8 +158,11 @@ canShareDict :: MkInjDict (FODomain FeldSyms Typeable Top) canShareDict = mkInjDictFO canShare canShareIn +canShareDict2 :: MkInjDict (FODomain FeldSyms Typeable Top) +canShareDict2 = mkInjDictFO canShare (const True) + -------------------------------------------------------------------------------- -- * Back ends -------------------------------------------------------------------------------- @@ -175,6 +179,9 @@ showAST :: (Syntactic a, Domain a ~ FeldDomainAll) => a -> String showAST = Syntactic.showAST . reifySmart (const True) canShareDict +showAST2 :: (Syntactic a, Domain a ~ FeldDomainAll) => a -> String +showAST2 = Syntactic.showAST . reifySmart2 (const True) canShareDict + -- | Draw the syntax tree on the terminal using Unicode art drawAST :: (Syntactic a, Domain a ~ FeldDomainAll) => a -> IO () drawAST = Syntactic.drawAST . reifySmart (const True) canShareDict @@ -186,6 +193,9 @@ -- | Evaluation eval :: (Syntactic a, Domain a ~ FeldDomainAll) => a -> Internal a eval = evalBind . reifySmart (const True) canShareDict + +eval2 :: (Syntactic a, Domain a ~ FeldDomainAll) => a -> Internal a +eval2 = evalBind . reifySmart2 (const True) canShareDict2 diff --git a/src/Language/Syntactic/Constructs/Tuple.hs b/src/Language/Syntactic/Constructs/Tuple.hs --- a/src/Language/Syntactic/Constructs/Tuple.hs +++ b/src/Language/Syntactic/Constructs/Tuple.hs @@ -25,6 +25,14 @@ Tup5 :: Tuple (a :-> b :-> c :-> d :-> e :-> Full (a,b,c,d,e)) Tup6 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> Full (a,b,c,d,e,f)) Tup7 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> g :-> Full (a,b,c,d,e,f,g)) + Tup8 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> Full (a,b,c,d,e,f,g,h)) + Tup9 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> Full (a,b,c,d,e,f,g,h,i)) + Tup10 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> Full (a,b,c,d,e,f,g,h,i,j)) + Tup11 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> Full (a,b,c,d,e,f,g,h,i,j,k)) + Tup12 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> l :-> Full (a,b,c,d,e,f,g,h,i,j,k,l)) + Tup13 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> l :-> m :-> Full (a,b,c,d,e,f,g,h,i,j,k,l,m)) + Tup14 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> l :-> m :-> n :-> Full (a,b,c,d,e,f,g,h,i,j,k,l,m,n)) + Tup15 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> l :-> m :-> n :-> o :-> Full (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o)) instance Constrained Tuple where @@ -33,12 +41,20 @@ instance Semantic Tuple where - semantics Tup2 = Sem "tup2" (,) - semantics Tup3 = Sem "tup3" (,,) - semantics Tup4 = Sem "tup4" (,,,) - semantics Tup5 = Sem "tup5" (,,,,) - semantics Tup6 = Sem "tup6" (,,,,,) - semantics Tup7 = Sem "tup7" (,,,,,,) + semantics Tup2 = Sem "tup2" (,) + semantics Tup3 = Sem "tup3" (,,) + semantics Tup4 = Sem "tup4" (,,,) + semantics Tup5 = Sem "tup5" (,,,,) + semantics Tup6 = Sem "tup6" (,,,,,) + semantics Tup7 = Sem "tup7" (,,,,,,) + semantics Tup8 = Sem "tup8" (,,,,,,,) + semantics Tup9 = Sem "tup9" (,,,,,,,,) + semantics Tup10 = Sem "tup10" (,,,,,,,,,) + semantics Tup11 = Sem "tup11" (,,,,,,,,,,) + semantics Tup12 = Sem "tup12" (,,,,,,,,,,,) + semantics Tup13 = Sem "tup13" (,,,,,,,,,,,,) + semantics Tup14 = Sem "tup14" (,,,,,,,,,,,,,) + semantics Tup15 = Sem "tup15" (,,,,,,,,,,,,,,) semanticInstances ''Tuple @@ -48,51 +64,159 @@ -- * Projection -------------------------------------------------------------------------------- --- | These families ('Sel1'' - 'Sel7'') are needed because of the problem +-- | These families ('Sel1'' - 'Sel15'') are needed because of the problem -- described in: -- -- type family Sel1' a -type instance Sel1' (a,b) = a -type instance Sel1' (a,b,c) = a -type instance Sel1' (a,b,c,d) = a -type instance Sel1' (a,b,c,d,e) = a -type instance Sel1' (a,b,c,d,e,f) = a -type instance Sel1' (a,b,c,d,e,f,g) = a +type instance Sel1' (a,b) = a +type instance Sel1' (a,b,c) = a +type instance Sel1' (a,b,c,d) = a +type instance Sel1' (a,b,c,d,e) = a +type instance Sel1' (a,b,c,d,e,f) = a +type instance Sel1' (a,b,c,d,e,f,g) = a +type instance Sel1' (a,b,c,d,e,f,g,h) = a +type instance Sel1' (a,b,c,d,e,f,g,h,i) = a +type instance Sel1' (a,b,c,d,e,f,g,h,i,j) = a +type instance Sel1' (a,b,c,d,e,f,g,h,i,j,k) = a +type instance Sel1' (a,b,c,d,e,f,g,h,i,j,k,l) = a +type instance Sel1' (a,b,c,d,e,f,g,h,i,j,k,l,m) = a +type instance Sel1' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = a +type instance Sel1' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = a type family Sel2' a -type instance Sel2' (a,b) = b -type instance Sel2' (a,b,c) = b -type instance Sel2' (a,b,c,d) = b -type instance Sel2' (a,b,c,d,e) = b -type instance Sel2' (a,b,c,d,e,f) = b -type instance Sel2' (a,b,c,d,e,f,g) = b +type instance Sel2' (a,b) = b +type instance Sel2' (a,b,c) = b +type instance Sel2' (a,b,c,d) = b +type instance Sel2' (a,b,c,d,e) = b +type instance Sel2' (a,b,c,d,e,f) = b +type instance Sel2' (a,b,c,d,e,f,g) = b +type instance Sel2' (a,b,c,d,e,f,g,h) = b +type instance Sel2' (a,b,c,d,e,f,g,h,i) = b +type instance Sel2' (a,b,c,d,e,f,g,h,i,j) = b +type instance Sel2' (a,b,c,d,e,f,g,h,i,j,k) = b +type instance Sel2' (a,b,c,d,e,f,g,h,i,j,k,l) = b +type instance Sel2' (a,b,c,d,e,f,g,h,i,j,k,l,m) = b +type instance Sel2' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = b +type instance Sel2' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = b type family Sel3' a -type instance Sel3' (a,b,c) = c -type instance Sel3' (a,b,c,d) = c -type instance Sel3' (a,b,c,d,e) = c -type instance Sel3' (a,b,c,d,e,f) = c -type instance Sel3' (a,b,c,d,e,f,g) = c +type instance Sel3' (a,b,c) = c +type instance Sel3' (a,b,c,d) = c +type instance Sel3' (a,b,c,d,e) = c +type instance Sel3' (a,b,c,d,e,f) = c +type instance Sel3' (a,b,c,d,e,f,g) = c +type instance Sel3' (a,b,c,d,e,f,g,h) = c +type instance Sel3' (a,b,c,d,e,f,g,h,i) = c +type instance Sel3' (a,b,c,d,e,f,g,h,i,j) = c +type instance Sel3' (a,b,c,d,e,f,g,h,i,j,k) = c +type instance Sel3' (a,b,c,d,e,f,g,h,i,j,k,l) = c +type instance Sel3' (a,b,c,d,e,f,g,h,i,j,k,l,m) = c +type instance Sel3' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = c +type instance Sel3' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = c type family Sel4' a -type instance Sel4' (a,b,c,d) = d -type instance Sel4' (a,b,c,d,e) = d -type instance Sel4' (a,b,c,d,e,f) = d -type instance Sel4' (a,b,c,d,e,f,g) = d +type instance Sel4' (a,b,c,d) = d +type instance Sel4' (a,b,c,d,e) = d +type instance Sel4' (a,b,c,d,e,f) = d +type instance Sel4' (a,b,c,d,e,f,g) = d +type instance Sel4' (a,b,c,d,e,f,g,h) = d +type instance Sel4' (a,b,c,d,e,f,g,h,i) = d +type instance Sel4' (a,b,c,d,e,f,g,h,i,j) = d +type instance Sel4' (a,b,c,d,e,f,g,h,i,j,k) = d +type instance Sel4' (a,b,c,d,e,f,g,h,i,j,k,l) = d +type instance Sel4' (a,b,c,d,e,f,g,h,i,j,k,l,m) = d +type instance Sel4' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = d +type instance Sel4' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = d type family Sel5' a -type instance Sel5' (a,b,c,d,e) = e -type instance Sel5' (a,b,c,d,e,f) = e -type instance Sel5' (a,b,c,d,e,f,g) = e +type instance Sel5' (a,b,c,d,e) = e +type instance Sel5' (a,b,c,d,e,f) = e +type instance Sel5' (a,b,c,d,e,f,g) = e +type instance Sel5' (a,b,c,d,e,f,g,h) = e +type instance Sel5' (a,b,c,d,e,f,g,h,i) = e +type instance Sel5' (a,b,c,d,e,f,g,h,i,j) = e +type instance Sel5' (a,b,c,d,e,f,g,h,i,j,k) = e +type instance Sel5' (a,b,c,d,e,f,g,h,i,j,k,l) = e +type instance Sel5' (a,b,c,d,e,f,g,h,i,j,k,l,m) = e +type instance Sel5' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = e +type instance Sel5' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = e type family Sel6' a -type instance Sel6' (a,b,c,d,e,f) = f -type instance Sel6' (a,b,c,d,e,f,g) = f +type instance Sel6' (a,b,c,d,e,f) = f +type instance Sel6' (a,b,c,d,e,f,g) = f +type instance Sel6' (a,b,c,d,e,f,g,h) = f +type instance Sel6' (a,b,c,d,e,f,g,h,i) = f +type instance Sel6' (a,b,c,d,e,f,g,h,i,j) = f +type instance Sel6' (a,b,c,d,e,f,g,h,i,j,k) = f +type instance Sel6' (a,b,c,d,e,f,g,h,i,j,k,l) = f +type instance Sel6' (a,b,c,d,e,f,g,h,i,j,k,l,m) = f +type instance Sel6' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = f +type instance Sel6' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = f type family Sel7' a -type instance Sel7' (a,b,c,d,e,f,g) = g +type instance Sel7' (a,b,c,d,e,f,g) = g +type instance Sel7' (a,b,c,d,e,f,g,h) = g +type instance Sel7' (a,b,c,d,e,f,g,h,i) = g +type instance Sel7' (a,b,c,d,e,f,g,h,i,j) = g +type instance Sel7' (a,b,c,d,e,f,g,h,i,j,k) = g +type instance Sel7' (a,b,c,d,e,f,g,h,i,j,k,l) = g +type instance Sel7' (a,b,c,d,e,f,g,h,i,j,k,l,m) = g +type instance Sel7' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = g +type instance Sel7' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = g +type family Sel8' a +type instance Sel8' (a,b,c,d,e,f,g,h) = h +type instance Sel8' (a,b,c,d,e,f,g,h,i) = h +type instance Sel8' (a,b,c,d,e,f,g,h,i,j) = h +type instance Sel8' (a,b,c,d,e,f,g,h,i,j,k) = h +type instance Sel8' (a,b,c,d,e,f,g,h,i,j,k,l) = h +type instance Sel8' (a,b,c,d,e,f,g,h,i,j,k,l,m) = h +type instance Sel8' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = h +type instance Sel8' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = h + +type family Sel9' a +type instance Sel9' (a,b,c,d,e,f,g,h,i) = i +type instance Sel9' (a,b,c,d,e,f,g,h,i,j) = i +type instance Sel9' (a,b,c,d,e,f,g,h,i,j,k) = i +type instance Sel9' (a,b,c,d,e,f,g,h,i,j,k,l) = i +type instance Sel9' (a,b,c,d,e,f,g,h,i,j,k,l,m) = i +type instance Sel9' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = i +type instance Sel9' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = i + +type family Sel10' a +type instance Sel10' (a,b,c,d,e,f,g,h,i,j) = j +type instance Sel10' (a,b,c,d,e,f,g,h,i,j,k) = j +type instance Sel10' (a,b,c,d,e,f,g,h,i,j,k,l) = j +type instance Sel10' (a,b,c,d,e,f,g,h,i,j,k,l,m) = j +type instance Sel10' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = j +type instance Sel10' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = j + +type family Sel11' a +type instance Sel11' (a,b,c,d,e,f,g,h,i,j,k) = k +type instance Sel11' (a,b,c,d,e,f,g,h,i,j,k,l) = k +type instance Sel11' (a,b,c,d,e,f,g,h,i,j,k,l,m) = k +type instance Sel11' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = k +type instance Sel11' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = k + +type family Sel12' a +type instance Sel12' (a,b,c,d,e,f,g,h,i,j,k,l) = l +type instance Sel12' (a,b,c,d,e,f,g,h,i,j,k,l,m) = l +type instance Sel12' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = l +type instance Sel12' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = l + +type family Sel13' a +type instance Sel13' (a,b,c,d,e,f,g,h,i,j,k,l,m) = m +type instance Sel13' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = m +type instance Sel13' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = m + +type family Sel14' a +type instance Sel14' (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = n +type instance Sel14' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = n + +type family Sel15' a +type instance Sel15' (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = o + -- | Expressions for selecting elements of a tuple data Select a where @@ -103,6 +227,14 @@ Sel5 :: (Sel5 a b, Sel5' a ~ b) => Select (a :-> Full b) Sel6 :: (Sel6 a b, Sel6' a ~ b) => Select (a :-> Full b) Sel7 :: (Sel7 a b, Sel7' a ~ b) => Select (a :-> Full b) + Sel8 :: (Sel8 a b, Sel8' a ~ b) => Select (a :-> Full b) + Sel9 :: (Sel9 a b, Sel9' a ~ b) => Select (a :-> Full b) + Sel10 :: (Sel10 a b, Sel10' a ~ b) => Select (a :-> Full b) + Sel11 :: (Sel11 a b, Sel11' a ~ b) => Select (a :-> Full b) + Sel12 :: (Sel12 a b, Sel12' a ~ b) => Select (a :-> Full b) + Sel13 :: (Sel13 a b, Sel13' a ~ b) => Select (a :-> Full b) + Sel14 :: (Sel14 a b, Sel14' a ~ b) => Select (a :-> Full b) + Sel15 :: (Sel15 a b, Sel15' a ~ b) => Select (a :-> Full b) instance Constrained Select where @@ -118,6 +250,14 @@ semantics Sel5 = Sem "sel5" sel5 semantics Sel6 = Sem "sel6" sel6 semantics Sel7 = Sem "sel7" sel7 + semantics Sel8 = Sem "sel8" sel8 + semantics Sel9 = Sem "sel9" sel9 + semantics Sel10 = Sem "sel10" sel10 + semantics Sel11 = Sem "sel11" sel11 + semantics Sel12 = Sem "sel12" sel12 + semantics Sel13 = Sem "sel13" sel13 + semantics Sel14 = Sem "sel14" sel14 + semantics Sel15 = Sem "sel15" sel15 semanticInstances ''Select @@ -132,4 +272,12 @@ selectPos Sel5 = 5 selectPos Sel6 = 6 selectPos Sel7 = 7 +selectPos Sel8 = 8 +selectPos Sel9 = 9 +selectPos Sel10 = 10 +selectPos Sel11 = 11 +selectPos Sel12 = 12 +selectPos Sel13 = 13 +selectPos Sel14 = 14 +selectPos Sel15 = 15 diff --git a/src/Language/Syntactic/Frontend/Tuple.hs b/src/Language/Syntactic/Frontend/Tuple.hs --- a/src/Language/Syntactic/Frontend/Tuple.hs +++ b/src/Language/Syntactic/Frontend/Tuple.hs @@ -231,3 +231,575 @@ , sugarSymC Sel7 a ) +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , InjectC Tuple dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + ) + , InjectC Select dom (Internal a) + , InjectC Select dom (Internal b) + , InjectC Select dom (Internal c) + , InjectC Select dom (Internal d) + , InjectC Select dom (Internal e) + , InjectC Select dom (Internal f) + , InjectC Select dom (Internal g) + , InjectC Select dom (Internal h) + ) => + Syntactic (a,b,c,d,e,f,g,h) + where + type Domain (a,b,c,d,e,f,g,h) = Domain a + type Internal (a,b,c,d,e,f,g,h) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + ) + + desugar = uncurryN $ sugarSymC Tup8 + sugar a = + ( sugarSymC Sel1 a + , sugarSymC Sel2 a + , sugarSymC Sel3 a + , sugarSymC Sel4 a + , sugarSymC Sel5 a + , sugarSymC Sel6 a + , sugarSymC Sel7 a + , sugarSymC Sel8 a + ) + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , InjectC Tuple dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + ) + , InjectC Select dom (Internal a) + , InjectC Select dom (Internal b) + , InjectC Select dom (Internal c) + , InjectC Select dom (Internal d) + , InjectC Select dom (Internal e) + , InjectC Select dom (Internal f) + , InjectC Select dom (Internal g) + , InjectC Select dom (Internal h) + , InjectC Select dom (Internal i) + ) => + Syntactic (a,b,c,d,e,f,g,h,i) + where + type Domain (a,b,c,d,e,f,g,h,i) = Domain a + type Internal (a,b,c,d,e,f,g,h,i) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + ) + + desugar = uncurryN $ sugarSymC Tup9 + sugar a = + ( sugarSymC Sel1 a + , sugarSymC Sel2 a + , sugarSymC Sel3 a + , sugarSymC Sel4 a + , sugarSymC Sel5 a + , sugarSymC Sel6 a + , sugarSymC Sel7 a + , sugarSymC Sel8 a + , sugarSymC Sel9 a + ) + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , Syntactic j, Domain j ~ dom + , InjectC Tuple dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + ) + , InjectC Select dom (Internal a) + , InjectC Select dom (Internal b) + , InjectC Select dom (Internal c) + , InjectC Select dom (Internal d) + , InjectC Select dom (Internal e) + , InjectC Select dom (Internal f) + , InjectC Select dom (Internal g) + , InjectC Select dom (Internal h) + , InjectC Select dom (Internal i) + , InjectC Select dom (Internal j) + ) => + Syntactic (a,b,c,d,e,f,g,h,i,j) + where + type Domain (a,b,c,d,e,f,g,h,i,j) = Domain a + type Internal (a,b,c,d,e,f,g,h,i,j) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + ) + + desugar = uncurryN $ sugarSymC Tup10 + sugar a = + ( sugarSymC Sel1 a + , sugarSymC Sel2 a + , sugarSymC Sel3 a + , sugarSymC Sel4 a + , sugarSymC Sel5 a + , sugarSymC Sel6 a + , sugarSymC Sel7 a + , sugarSymC Sel8 a + , sugarSymC Sel9 a + , sugarSymC Sel10 a + ) + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , Syntactic j, Domain j ~ dom + , Syntactic k, Domain k ~ dom + , InjectC Tuple dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + ) + , InjectC Select dom (Internal a) + , InjectC Select dom (Internal b) + , InjectC Select dom (Internal c) + , InjectC Select dom (Internal d) + , InjectC Select dom (Internal e) + , InjectC Select dom (Internal f) + , InjectC Select dom (Internal g) + , InjectC Select dom (Internal h) + , InjectC Select dom (Internal i) + , InjectC Select dom (Internal j) + , InjectC Select dom (Internal k) + ) => + Syntactic (a,b,c,d,e,f,g,h,i,j,k) + where + type Domain (a,b,c,d,e,f,g,h,i,j,k) = Domain a + type Internal (a,b,c,d,e,f,g,h,i,j,k) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + ) + + desugar = uncurryN $ sugarSymC Tup11 + sugar a = + ( sugarSymC Sel1 a + , sugarSymC Sel2 a + , sugarSymC Sel3 a + , sugarSymC Sel4 a + , sugarSymC Sel5 a + , sugarSymC Sel6 a + , sugarSymC Sel7 a + , sugarSymC Sel8 a + , sugarSymC Sel9 a + , sugarSymC Sel10 a + , sugarSymC Sel11 a + ) + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , Syntactic j, Domain j ~ dom + , Syntactic k, Domain k ~ dom + , Syntactic l, Domain l ~ dom + , InjectC Tuple dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + ) + , InjectC Select dom (Internal a) + , InjectC Select dom (Internal b) + , InjectC Select dom (Internal c) + , InjectC Select dom (Internal d) + , InjectC Select dom (Internal e) + , InjectC Select dom (Internal f) + , InjectC Select dom (Internal g) + , InjectC Select dom (Internal h) + , InjectC Select dom (Internal i) + , InjectC Select dom (Internal j) + , InjectC Select dom (Internal k) + , InjectC Select dom (Internal l) + ) => + Syntactic (a,b,c,d,e,f,g,h,i,j,k,l) + where + type Domain (a,b,c,d,e,f,g,h,i,j,k,l) = Domain a + type Internal (a,b,c,d,e,f,g,h,i,j,k,l) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + ) + + desugar = uncurryN $ sugarSymC Tup12 + sugar a = + ( sugarSymC Sel1 a + , sugarSymC Sel2 a + , sugarSymC Sel3 a + , sugarSymC Sel4 a + , sugarSymC Sel5 a + , sugarSymC Sel6 a + , sugarSymC Sel7 a + , sugarSymC Sel8 a + , sugarSymC Sel9 a + , sugarSymC Sel10 a + , sugarSymC Sel11 a + , sugarSymC Sel12 a + ) + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , Syntactic j, Domain j ~ dom + , Syntactic k, Domain k ~ dom + , Syntactic l, Domain l ~ dom + , Syntactic m, Domain m ~ dom + , InjectC Tuple dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + ) + , InjectC Select dom (Internal a) + , InjectC Select dom (Internal b) + , InjectC Select dom (Internal c) + , InjectC Select dom (Internal d) + , InjectC Select dom (Internal e) + , InjectC Select dom (Internal f) + , InjectC Select dom (Internal g) + , InjectC Select dom (Internal h) + , InjectC Select dom (Internal i) + , InjectC Select dom (Internal j) + , InjectC Select dom (Internal k) + , InjectC Select dom (Internal l) + , InjectC Select dom (Internal m) + ) => + Syntactic (a,b,c,d,e,f,g,h,i,j,k,l,m) + where + type Domain (a,b,c,d,e,f,g,h,i,j,k,l,m) = Domain a + type Internal (a,b,c,d,e,f,g,h,i,j,k,l,m) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + ) + + desugar = uncurryN $ sugarSymC Tup13 + sugar a = + ( sugarSymC Sel1 a + , sugarSymC Sel2 a + , sugarSymC Sel3 a + , sugarSymC Sel4 a + , sugarSymC Sel5 a + , sugarSymC Sel6 a + , sugarSymC Sel7 a + , sugarSymC Sel8 a + , sugarSymC Sel9 a + , sugarSymC Sel10 a + , sugarSymC Sel11 a + , sugarSymC Sel12 a + , sugarSymC Sel13 a + ) + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , Syntactic j, Domain j ~ dom + , Syntactic k, Domain k ~ dom + , Syntactic l, Domain l ~ dom + , Syntactic m, Domain m ~ dom + , Syntactic n, Domain n ~ dom + , InjectC Tuple dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + , Internal n + ) + , InjectC Select dom (Internal a) + , InjectC Select dom (Internal b) + , InjectC Select dom (Internal c) + , InjectC Select dom (Internal d) + , InjectC Select dom (Internal e) + , InjectC Select dom (Internal f) + , InjectC Select dom (Internal g) + , InjectC Select dom (Internal h) + , InjectC Select dom (Internal i) + , InjectC Select dom (Internal j) + , InjectC Select dom (Internal k) + , InjectC Select dom (Internal l) + , InjectC Select dom (Internal m) + , InjectC Select dom (Internal n) + ) => + Syntactic (a,b,c,d,e,f,g,h,i,j,k,l,m,n) + where + type Domain (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = Domain a + type Internal (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + , Internal n + ) + + desugar = uncurryN $ sugarSymC Tup14 + sugar a = + ( sugarSymC Sel1 a + , sugarSymC Sel2 a + , sugarSymC Sel3 a + , sugarSymC Sel4 a + , sugarSymC Sel5 a + , sugarSymC Sel6 a + , sugarSymC Sel7 a + , sugarSymC Sel8 a + , sugarSymC Sel9 a + , sugarSymC Sel10 a + , sugarSymC Sel11 a + , sugarSymC Sel12 a + , sugarSymC Sel13 a + , sugarSymC Sel14 a + ) + + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , Syntactic j, Domain j ~ dom + , Syntactic k, Domain k ~ dom + , Syntactic l, Domain l ~ dom + , Syntactic m, Domain m ~ dom + , Syntactic n, Domain n ~ dom + , Syntactic o, Domain o ~ dom + , InjectC Tuple dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + , Internal n + , Internal o + ) + , InjectC Select dom (Internal a) + , InjectC Select dom (Internal b) + , InjectC Select dom (Internal c) + , InjectC Select dom (Internal d) + , InjectC Select dom (Internal e) + , InjectC Select dom (Internal f) + , InjectC Select dom (Internal g) + , InjectC Select dom (Internal h) + , InjectC Select dom (Internal i) + , InjectC Select dom (Internal j) + , InjectC Select dom (Internal k) + , InjectC Select dom (Internal l) + , InjectC Select dom (Internal m) + , InjectC Select dom (Internal n) + , InjectC Select dom (Internal o) + ) => + Syntactic (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) + where + type Domain (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = Domain a + type Internal (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + , Internal n + , Internal o + ) + + desugar = uncurryN $ sugarSymC Tup15 + sugar a = + ( sugarSymC Sel1 a + , sugarSymC Sel2 a + , sugarSymC Sel3 a + , sugarSymC Sel4 a + , sugarSymC Sel5 a + , sugarSymC Sel6 a + , sugarSymC Sel7 a + , sugarSymC Sel8 a + , sugarSymC Sel9 a + , sugarSymC Sel10 a + , sugarSymC Sel11 a + , sugarSymC Sel12 a + , sugarSymC Sel13 a + , sugarSymC Sel14 a + , sugarSymC Sel15 a + ) diff --git a/src/Language/Syntactic/Frontend/TupleConstrained.hs b/src/Language/Syntactic/Frontend/TupleConstrained.hs --- a/src/Language/Syntactic/Frontend/TupleConstrained.hs +++ b/src/Language/Syntactic/Frontend/TupleConstrained.hs @@ -328,3 +328,783 @@ , sugarSymC' Sel7 a ) + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , TupleSat dom p + , p ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + ) + , p (Internal a) + , p (Internal b) + , p (Internal c) + , p (Internal d) + , p (Internal e) + , p (Internal f) + , p (Internal g) + , p (Internal h) + , InjectC (Tuple :|| p) dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + ) + , InjectC (Select :|| p) dom (Internal a) + , InjectC (Select :|| p) dom (Internal b) + , InjectC (Select :|| p) dom (Internal c) + , InjectC (Select :|| p) dom (Internal d) + , InjectC (Select :|| p) dom (Internal e) + , InjectC (Select :|| p) dom (Internal f) + , InjectC (Select :|| p) dom (Internal g) + , InjectC (Select :|| p) dom (Internal h) + ) => + Syntactic (a,b,c,d,e,f,g,h) + where + type Domain (a,b,c,d,e,f,g,h) = Domain a + type Internal (a,b,c,d,e,f,g,h) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + ) + + desugar = uncurryN $ sugarSymC' Tup8 + sugar a = + ( sugarSymC' Sel1 a + , sugarSymC' Sel2 a + , sugarSymC' Sel3 a + , sugarSymC' Sel4 a + , sugarSymC' Sel5 a + , sugarSymC' Sel6 a + , sugarSymC' Sel7 a + , sugarSymC' Sel8 a + ) + + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , TupleSat dom p + , p ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + ) + , p (Internal a) + , p (Internal b) + , p (Internal c) + , p (Internal d) + , p (Internal e) + , p (Internal f) + , p (Internal g) + , p (Internal h) + , p (Internal i) + , InjectC (Tuple :|| p) dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + ) + , InjectC (Select :|| p) dom (Internal a) + , InjectC (Select :|| p) dom (Internal b) + , InjectC (Select :|| p) dom (Internal c) + , InjectC (Select :|| p) dom (Internal d) + , InjectC (Select :|| p) dom (Internal e) + , InjectC (Select :|| p) dom (Internal f) + , InjectC (Select :|| p) dom (Internal g) + , InjectC (Select :|| p) dom (Internal h) + , InjectC (Select :|| p) dom (Internal i) + ) => + Syntactic (a,b,c,d,e,f,g,h,i) + where + type Domain (a,b,c,d,e,f,g,h,i) = Domain a + type Internal (a,b,c,d,e,f,g,h,i) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + ) + + desugar = uncurryN $ sugarSymC' Tup9 + sugar a = + ( sugarSymC' Sel1 a + , sugarSymC' Sel2 a + , sugarSymC' Sel3 a + , sugarSymC' Sel4 a + , sugarSymC' Sel5 a + , sugarSymC' Sel6 a + , sugarSymC' Sel7 a + , sugarSymC' Sel8 a + , sugarSymC' Sel9 a + ) + + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , Syntactic j, Domain j ~ dom + , TupleSat dom p + , p ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + ) + , p (Internal a) + , p (Internal b) + , p (Internal c) + , p (Internal d) + , p (Internal e) + , p (Internal f) + , p (Internal g) + , p (Internal h) + , p (Internal i) + , p (Internal j) + , InjectC (Tuple :|| p) dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + ) + , InjectC (Select :|| p) dom (Internal a) + , InjectC (Select :|| p) dom (Internal b) + , InjectC (Select :|| p) dom (Internal c) + , InjectC (Select :|| p) dom (Internal d) + , InjectC (Select :|| p) dom (Internal e) + , InjectC (Select :|| p) dom (Internal f) + , InjectC (Select :|| p) dom (Internal g) + , InjectC (Select :|| p) dom (Internal h) + , InjectC (Select :|| p) dom (Internal i) + , InjectC (Select :|| p) dom (Internal j) + ) => + Syntactic (a,b,c,d,e,f,g,h,i,j) + where + type Domain (a,b,c,d,e,f,g,h,i,j) = Domain a + type Internal (a,b,c,d,e,f,g,h,i,j) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + ) + + desugar = uncurryN $ sugarSymC' Tup10 + sugar a = + ( sugarSymC' Sel1 a + , sugarSymC' Sel2 a + , sugarSymC' Sel3 a + , sugarSymC' Sel4 a + , sugarSymC' Sel5 a + , sugarSymC' Sel6 a + , sugarSymC' Sel7 a + , sugarSymC' Sel8 a + , sugarSymC' Sel9 a + , sugarSymC' Sel10 a + ) + + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , Syntactic j, Domain j ~ dom + , Syntactic k, Domain k ~ dom + , TupleSat dom p + , p ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + ) + , p (Internal a) + , p (Internal b) + , p (Internal c) + , p (Internal d) + , p (Internal e) + , p (Internal f) + , p (Internal g) + , p (Internal h) + , p (Internal i) + , p (Internal j) + , p (Internal k) + , InjectC (Tuple :|| p) dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + ) + , InjectC (Select :|| p) dom (Internal a) + , InjectC (Select :|| p) dom (Internal b) + , InjectC (Select :|| p) dom (Internal c) + , InjectC (Select :|| p) dom (Internal d) + , InjectC (Select :|| p) dom (Internal e) + , InjectC (Select :|| p) dom (Internal f) + , InjectC (Select :|| p) dom (Internal g) + , InjectC (Select :|| p) dom (Internal h) + , InjectC (Select :|| p) dom (Internal i) + , InjectC (Select :|| p) dom (Internal j) + , InjectC (Select :|| p) dom (Internal k) + ) => + Syntactic (a,b,c,d,e,f,g,h,i,j,k) + where + type Domain (a,b,c,d,e,f,g,h,i,j,k) = Domain a + type Internal (a,b,c,d,e,f,g,h,i,j,k) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + ) + + desugar = uncurryN $ sugarSymC' Tup11 + sugar a = + ( sugarSymC' Sel1 a + , sugarSymC' Sel2 a + , sugarSymC' Sel3 a + , sugarSymC' Sel4 a + , sugarSymC' Sel5 a + , sugarSymC' Sel6 a + , sugarSymC' Sel7 a + , sugarSymC' Sel8 a + , sugarSymC' Sel9 a + , sugarSymC' Sel10 a + , sugarSymC' Sel11 a + ) + + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , Syntactic j, Domain j ~ dom + , Syntactic k, Domain k ~ dom + , Syntactic l, Domain l ~ dom + , TupleSat dom p + , p ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + ) + , p (Internal a) + , p (Internal b) + , p (Internal c) + , p (Internal d) + , p (Internal e) + , p (Internal f) + , p (Internal g) + , p (Internal h) + , p (Internal i) + , p (Internal j) + , p (Internal k) + , p (Internal l) + , InjectC (Tuple :|| p) dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + ) + , InjectC (Select :|| p) dom (Internal a) + , InjectC (Select :|| p) dom (Internal b) + , InjectC (Select :|| p) dom (Internal c) + , InjectC (Select :|| p) dom (Internal d) + , InjectC (Select :|| p) dom (Internal e) + , InjectC (Select :|| p) dom (Internal f) + , InjectC (Select :|| p) dom (Internal g) + , InjectC (Select :|| p) dom (Internal h) + , InjectC (Select :|| p) dom (Internal i) + , InjectC (Select :|| p) dom (Internal j) + , InjectC (Select :|| p) dom (Internal k) + , InjectC (Select :|| p) dom (Internal l) + ) => + Syntactic (a,b,c,d,e,f,g,h,i,j,k,l) + where + type Domain (a,b,c,d,e,f,g,h,i,j,k,l) = Domain a + type Internal (a,b,c,d,e,f,g,h,i,j,k,l) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + ) + + desugar = uncurryN $ sugarSymC' Tup12 + sugar a = + ( sugarSymC' Sel1 a + , sugarSymC' Sel2 a + , sugarSymC' Sel3 a + , sugarSymC' Sel4 a + , sugarSymC' Sel5 a + , sugarSymC' Sel6 a + , sugarSymC' Sel7 a + , sugarSymC' Sel8 a + , sugarSymC' Sel9 a + , sugarSymC' Sel10 a + , sugarSymC' Sel11 a + , sugarSymC' Sel12 a + ) + + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , Syntactic j, Domain j ~ dom + , Syntactic k, Domain k ~ dom + , Syntactic l, Domain l ~ dom + , Syntactic m, Domain m ~ dom + , TupleSat dom p + , p ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + ) + , p (Internal a) + , p (Internal b) + , p (Internal c) + , p (Internal d) + , p (Internal e) + , p (Internal f) + , p (Internal g) + , p (Internal h) + , p (Internal i) + , p (Internal j) + , p (Internal k) + , p (Internal l) + , p (Internal m) + , InjectC (Tuple :|| p) dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + ) + , InjectC (Select :|| p) dom (Internal a) + , InjectC (Select :|| p) dom (Internal b) + , InjectC (Select :|| p) dom (Internal c) + , InjectC (Select :|| p) dom (Internal d) + , InjectC (Select :|| p) dom (Internal e) + , InjectC (Select :|| p) dom (Internal f) + , InjectC (Select :|| p) dom (Internal g) + , InjectC (Select :|| p) dom (Internal h) + , InjectC (Select :|| p) dom (Internal i) + , InjectC (Select :|| p) dom (Internal j) + , InjectC (Select :|| p) dom (Internal k) + , InjectC (Select :|| p) dom (Internal l) + , InjectC (Select :|| p) dom (Internal m) + ) => + Syntactic (a,b,c,d,e,f,g,h,i,j,k,l,m) + where + type Domain (a,b,c,d,e,f,g,h,i,j,k,l,m) = Domain a + type Internal (a,b,c,d,e,f,g,h,i,j,k,l,m) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + ) + + desugar = uncurryN $ sugarSymC' Tup13 + sugar a = + ( sugarSymC' Sel1 a + , sugarSymC' Sel2 a + , sugarSymC' Sel3 a + , sugarSymC' Sel4 a + , sugarSymC' Sel5 a + , sugarSymC' Sel6 a + , sugarSymC' Sel7 a + , sugarSymC' Sel8 a + , sugarSymC' Sel9 a + , sugarSymC' Sel10 a + , sugarSymC' Sel11 a + , sugarSymC' Sel12 a + , sugarSymC' Sel13 a + ) + + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , Syntactic j, Domain j ~ dom + , Syntactic k, Domain k ~ dom + , Syntactic l, Domain l ~ dom + , Syntactic m, Domain m ~ dom + , Syntactic n, Domain n ~ dom + , TupleSat dom p + , p ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + , Internal n + ) + , p (Internal a) + , p (Internal b) + , p (Internal c) + , p (Internal d) + , p (Internal e) + , p (Internal f) + , p (Internal g) + , p (Internal h) + , p (Internal i) + , p (Internal j) + , p (Internal k) + , p (Internal l) + , p (Internal m) + , p (Internal n) + , InjectC (Tuple :|| p) dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + , Internal n + ) + , InjectC (Select :|| p) dom (Internal a) + , InjectC (Select :|| p) dom (Internal b) + , InjectC (Select :|| p) dom (Internal c) + , InjectC (Select :|| p) dom (Internal d) + , InjectC (Select :|| p) dom (Internal e) + , InjectC (Select :|| p) dom (Internal f) + , InjectC (Select :|| p) dom (Internal g) + , InjectC (Select :|| p) dom (Internal h) + , InjectC (Select :|| p) dom (Internal i) + , InjectC (Select :|| p) dom (Internal j) + , InjectC (Select :|| p) dom (Internal k) + , InjectC (Select :|| p) dom (Internal l) + , InjectC (Select :|| p) dom (Internal m) + , InjectC (Select :|| p) dom (Internal n) + ) => + Syntactic (a,b,c,d,e,f,g,h,i,j,k,l,m,n) + where + type Domain (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = Domain a + type Internal (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + , Internal n + ) + + desugar = uncurryN $ sugarSymC' Tup14 + sugar a = + ( sugarSymC' Sel1 a + , sugarSymC' Sel2 a + , sugarSymC' Sel3 a + , sugarSymC' Sel4 a + , sugarSymC' Sel5 a + , sugarSymC' Sel6 a + , sugarSymC' Sel7 a + , sugarSymC' Sel8 a + , sugarSymC' Sel9 a + , sugarSymC' Sel10 a + , sugarSymC' Sel11 a + , sugarSymC' Sel12 a + , sugarSymC' Sel13 a + , sugarSymC' Sel14 a + ) + + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Syntactic c, Domain c ~ dom + , Syntactic d, Domain d ~ dom + , Syntactic e, Domain e ~ dom + , Syntactic f, Domain f ~ dom + , Syntactic g, Domain g ~ dom + , Syntactic h, Domain h ~ dom + , Syntactic i, Domain i ~ dom + , Syntactic j, Domain j ~ dom + , Syntactic k, Domain k ~ dom + , Syntactic l, Domain l ~ dom + , Syntactic m, Domain m ~ dom + , Syntactic n, Domain n ~ dom + , Syntactic o, Domain o ~ dom + , TupleSat dom p + , p ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + , Internal n + , Internal o + ) + , p (Internal a) + , p (Internal b) + , p (Internal c) + , p (Internal d) + , p (Internal e) + , p (Internal f) + , p (Internal g) + , p (Internal h) + , p (Internal i) + , p (Internal j) + , p (Internal k) + , p (Internal l) + , p (Internal m) + , p (Internal n) + , p (Internal o) + , InjectC (Tuple :|| p) dom + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + , Internal n + , Internal o + ) + , InjectC (Select :|| p) dom (Internal a) + , InjectC (Select :|| p) dom (Internal b) + , InjectC (Select :|| p) dom (Internal c) + , InjectC (Select :|| p) dom (Internal d) + , InjectC (Select :|| p) dom (Internal e) + , InjectC (Select :|| p) dom (Internal f) + , InjectC (Select :|| p) dom (Internal g) + , InjectC (Select :|| p) dom (Internal h) + , InjectC (Select :|| p) dom (Internal i) + , InjectC (Select :|| p) dom (Internal j) + , InjectC (Select :|| p) dom (Internal k) + , InjectC (Select :|| p) dom (Internal l) + , InjectC (Select :|| p) dom (Internal m) + , InjectC (Select :|| p) dom (Internal n) + , InjectC (Select :|| p) dom (Internal o) + ) => + Syntactic (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) + where + type Domain (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = Domain a + type Internal (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + , Internal h + , Internal i + , Internal j + , Internal k + , Internal l + , Internal m + , Internal n + , Internal o + ) + + desugar = uncurryN $ sugarSymC' Tup15 + sugar a = + ( sugarSymC' Sel1 a + , sugarSymC' Sel2 a + , sugarSymC' Sel3 a + , sugarSymC' Sel4 a + , sugarSymC' Sel5 a + , sugarSymC' Sel6 a + , sugarSymC' Sel7 a + , sugarSymC' Sel8 a + , sugarSymC' Sel9 a + , sugarSymC' Sel10 a + , sugarSymC' Sel11 a + , sugarSymC' Sel12 a + , sugarSymC' Sel13 a + , sugarSymC' Sel14 a + , sugarSymC' Sel15 a + ) + diff --git a/src/Language/Syntactic/Sharing/CodeMotion2.hs b/src/Language/Syntactic/Sharing/CodeMotion2.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Sharing/CodeMotion2.hs @@ -0,0 +1,475 @@ +{-# LANGUAGE UndecidableInstances #-} +module Language.Syntactic.Sharing.CodeMotion2 + ( codeMotion2 + , reifySmart2 + ) where + +import Control.Monad.State +import Control.Monad.Reader +import qualified Data.Set as Set +import qualified Data.Map as Map +import Data.Array +import Data.List +import Data.Maybe (fromJust,fromMaybe) +import Data.Function +import Data.Hash +import Data.Typeable + +import Language.Syntactic +import Language.Syntactic.Constructs.Binding +import Language.Syntactic.Constructs.Binding.HigherOrder +import Language.Syntactic.Sharing.SimpleCodeMotion + + + +isVariable :: PrjDict dom -> ASTF (NodeDomain dom) a -> Bool +isVariable pd (Sym (C' (InjR (prjVariable pd -> Just _)))) = True +isVariable pd _ = False + +newtype NodeId = NodeId { nodeInteger :: Integer } + deriving (Eq, Ord, Num, Real, Integral, Enum, Ix) + +instance Show NodeId + where + show (NodeId i) = show i + +showNode :: NodeId -> String +showNode n = "node:" ++ show n + +instance AlphaEq dom dom dom env => AlphaEq Node Node dom env + where + alphaEqSym (Node n1) _ (Node n2) _ = return (n1 == n2) + +instance Constrained Node + where + type Sat Node = Top + exprDict _ = Dict + +instance Equality Node + where + equal (Node n1) (Node n2) = error "can't compare nodes for equality" + exprHash (Node n) = hash (nodeInteger n) + +-- | Placeholder for a syntax tree. Similar to Node from Graph, but with the +-- invariant that nodes with the same id are alpha-equivalent, given that they +-- come from the same expression. +data Node a + where + Node :: NodeId -> Node (Full a) + + +type NodeDomain dom = (Node :+: dom) :|| Sat dom + + +-- | A gathered sub-expression along with information used to decide where and +-- if it should be shared. +data Gathered dom = Gathered + { geExpr :: ASTSAT (NodeDomain dom) + -- ^ The gathered expression. + , geNodeId :: NodeId + -- ^ The node id of the expression. + , geInfo :: [(NodeId, GatherInfo)] + -- ^ A list of nodes which the gathered expression occurs in, which it + -- should not be hoisted out of, along with the number of times it occurs + -- in it and the union of all the scopes where the variable occurs. + } + +-- | An occurence count and a union of scopes for a gathered expression. Used +-- for the heuristic for when to share an expression. +data GatherInfo = GatherInfo + { giCount :: Int + , giScopes :: Set.Set VarId + } + deriving Show + +-- | A set of expressions used to keep track of gathered expression in `gather` +newtype GatherSet dom = GatherSet {unGatherSet :: Map.Map Hash [Gathered dom]} + + +lookupGS :: forall dom a + . ( AlphaEq dom dom (NodeDomain dom) [(VarId,VarId)] + , Equality dom) + => GatherSet dom + -> ASTF (NodeDomain dom) a + -> Maybe (Gathered dom) +lookupGS (GatherSet m) e = Map.lookup (exprHash e) m >>= look + where + look :: [Gathered dom] -> Maybe (Gathered dom) + look [] = Nothing + look (g:gs) | ASTB ge <- geExpr g + , alphaEq ge e + = Just g + look (g:gs) = look gs + +updateGS :: forall dom + . ( AlphaEq dom dom (NodeDomain dom) [(VarId,VarId)] + , Equality dom) + => GatherSet dom + -> Gathered dom + -> GatherSet dom +updateGS (GatherSet m) g + | ASTB ge <- geExpr g + = GatherSet $ Map.alter alt (exprHash ge) m + where + alt :: Maybe [Gathered dom] -> Maybe [Gathered dom] + alt (Just gs) = Just $ ins gs + alt Nothing = Just [g] + ins :: [Gathered dom] -> [Gathered dom] + ins [] = [g] + ins (x:xs) | ASTB xe <- geExpr x + , ASTB ge <- geExpr g + , alphaEq xe ge + = g : xs + ins (x:xs) = x : ins xs + +emptyGS = GatherSet $ Map.empty + +toListGS (GatherSet m) = concatMap snd (Map.toList m) + +type RebuildEnv dom = + ( Map.Map NodeId (ASTSAT dom) + -- associates node ids with the AST they should be substituted by + , Set.Set VarId + -- bound variables + , [NodeId] + -- nodes that have been encountered + ) + +type RebuildMonad dom a = ReaderT (RebuildEnv dom) (State VarId) a + + +runRebuild :: RebuildMonad dom a -> State VarId a +runRebuild m = runReaderT m (Map.empty, Set.empty, [0]) + +addBoundVar :: VarId -> RebuildMonad dom a -> RebuildMonad dom a +addBoundVar v = local (\(nm,vs,sn) -> (nm, Set.insert v vs, sn)) + +getBoundVars :: RebuildMonad dom (Set.Set VarId) +getBoundVars = do + (_,bv,_) <- ask + return bv + +addNodeExpr :: NodeId -> ASTSAT dom -> RebuildMonad dom a -> RebuildMonad dom a +addNodeExpr n a = local (\(nm,vs,sn) -> (Map.insert n a nm, vs, sn)) + +getNodeExprMap :: RebuildMonad dom (Map.Map NodeId (ASTSAT dom)) +getNodeExprMap = do + (nm,_,_) <- ask + return nm + +addSeenNode :: NodeId -> RebuildMonad dom a -> RebuildMonad dom a +addSeenNode n = local (\(nm,vs,sn) -> (nm, vs, n:sn)) + +getSeenNodes :: RebuildMonad dom [NodeId] +getSeenNodes = do + (_,_,sn) <- ask + return sn + + + +codeMotion2 :: forall dom a + . ( ConstrainedBy dom Typeable + , AlphaEq dom dom (NodeDomain dom) [(VarId,VarId)] + , Equality dom + ) + => (forall c. ASTF dom c -> Bool) -- ^ Control wether a sub-expression can be hoisted over the given expression + -> PrjDict dom + -> MkInjDict dom + -> ASTF dom a + -> State VarId (ASTF dom a) +codeMotion2 hoistOver pd mkId a = do + let (gm, a') = gather hoistOver pd a + rebuild pd mkId (toListGS gm) a' + +type ShareInfo dom = (NodeId, ASTSAT (NodeDomain dom), GatherInfo) + +data ShareMaybe dom a + where + Share :: Sat dom b => VarId -> InjDict dom b a -> ASTF dom b -> ShareMaybe dom a + Not :: Sat dom b => ASTF dom b -> ShareMaybe dom a + +rebuild :: forall dom a + . ( ConstrainedBy dom Typeable + , AlphaEq dom dom (NodeDomain dom) [(VarId,VarId)] + , Equality dom + ) + => PrjDict dom + -> MkInjDict dom + -> [Gathered dom] + -> ASTF (NodeDomain dom) a + -> State VarId (ASTF dom a) +rebuild pd mkId gs (Sym (C' (InjL _))) = error "" +rebuild pd mkId gs a = runRebuild $ rebuild' 0 a + where + nodes :: Array NodeId (Gathered dom) + nodes = array + (1, maximum (0:(Prelude.map geNodeId gs))) + (zip (Prelude.map geNodeId gs) gs) + + nodeExpr :: NodeId -> ASTSAT (NodeDomain dom) + nodeExpr n = geExpr (nodes ! n) + + freeVars :: Array NodeId (Set.Set VarId) + freeVars = nodesFreeVars pd nodes + + nodeDeps :: Array NodeId (Set.Set NodeId) + nodeDeps = nodeDepsArray + where + nodeDepsArray = array (0,snd (bounds nodes)) [(n, nodeDepsNode n) | n <- 0 : indices nodes] + + nodeDepsNode :: NodeId -> Set.Set NodeId + nodeDepsNode 0 = nodeDepsExp a + nodeDepsNode n = liftASTB nodeDepsExp $ geExpr (nodes ! n) + + nodeDepsExp :: AST (NodeDomain dom) b -> Set.Set NodeId + nodeDepsExp (Sym (C' (InjR _))) = Set.empty + nodeDepsExp (Sym (C' (InjL (Node n)))) = Set.insert n (nodeDepsArray ! n) + nodeDepsExp (s :$ b) = Set.union (nodeDepsExp s) (nodeDepsExp b) + + -- | Computes a list of nodes that should be considered for sharing at a + -- particular node. Must return a ShareInfo corresponding to any node + -- that might be encounter in direct sub-expression of the node that has + -- not already been considered at a parent node. Otherwise we will not know + -- what to do with that node. + -- Implementation is pretty bizarre right now, but it should be replaced anyway. + nodesToConsider :: (NodeId -> Bool) -> Set.Set VarId -> [NodeId] -> [ShareInfo dom] + nodesToConsider f bv seenNodes = concatMap mkShareInfo (assocs nodes) + where + maximumBy' f [] = [] + maximumBy' f xs = [maximumBy f xs] + mkShareInfo (n,g) = map snd $ maximumBy' (compare `on` fst) $ map (\(Just i,x) -> (i,x)) $ filter ((/=Nothing) . fst) + [ (elemIndex il seenNodes, (n, geExpr g, gi)) + | (il,gi) <- geInfo g + --, i <- elemIndex il seenNodes + -- must be shared inside `il` + , Set.null (freeVars ! n `Set.difference` bv) + -- any free variables in the sub-expression must be bound + , f n + ] + + rebuild' :: forall b + . NodeId + -> ASTF (NodeDomain dom) b + -> RebuildMonad dom (ASTF dom b) + rebuild' n (Sym (C' (InjR lam)) :$ ns@(Sym (C' (InjL (Node nb))))) + | Just v <- prjLambda pd lam + = case geExpr (nodes ! nb) of + ASTB a + | Dict <- exprDictSub pTypeable ns + , Dict <- exprDictSub pTypeable a + -> case gcast a of + Nothing -> error "rebuild: type mistmatch" + Just a -> do + a' <- addBoundVar v $ addSeenNode n $ rebuild' nb a + return (Sym lam :$ a') + rebuild' n (Sym (C' (InjR s))) = return $ Sym s + rebuild' n a = addSeenNode n $ shareExprsIn n a + + shareExprsIn :: forall b + . NodeId + -> ASTF (NodeDomain dom) b + -> RebuildMonad dom (ASTF dom b) + shareExprsIn n a = do + bv <- getBoundVars + seenNodes <- getSeenNodes + nodeMap <- getNodeExprMap + let considered = nodesToConsider (\n' -> n' /= n && not (Map.member n' nodeMap) && Set.member n' (nodeDeps ! n)) bv seenNodes + let sorted = sortBy (compare `on` (\(n,_,_) -> n)) considered + shareEm sorted a + + shareEm + :: [ShareInfo dom] + -> ASTF (NodeDomain dom) b + -> RebuildMonad dom (ASTF dom b) + shareEm [] a = fixNodeExprSub a + shareEm ((n, be@(ASTB b), gi) : sis) a = do + b' <- rebuild' n b + bv <- getBoundVars + case mkId b' (inlineAll nodeExpr a) of + Just id | heuristic bv gi a -> do + v <- get; put (v+1) + a' <- addNodeExpr n (ASTB (Sym (injVariable id v))) $ shareEm sis a + return $ Sym (injLet id) :$ b' :$ (Sym (injLambda id v) :$ a') + _ -> do + a' <- addNodeExpr n (ASTB b') $ shareEm sis a + return a' + + fixNodeExprSub :: forall b + . ( ConstrainedBy dom Typeable + , AlphaEq dom dom (NodeDomain dom) [(VarId,VarId)] + , Equality dom + ) + => AST (NodeDomain dom) b + -> RebuildMonad dom (AST dom b) + fixNodeExprSub (Sym (C' (InjR s))) = return (Sym s) + fixNodeExprSub (s :$ b) = do + b' <- fixNodeExpr b + s' <- fixNodeExprSub s + return (s' :$ b') + + fixNodeExpr :: forall b . ASTF (NodeDomain dom) b -> RebuildMonad dom (ASTF dom b) + fixNodeExpr (ns@(Sym (C' (InjL (Node n))))) = do + nodeMap <- getNodeExprMap + let a = lookNode nodeMap + return a + where + lookNode nodeMap = case Map.lookup n nodeMap of + Just (ASTB a) + | Dict <- exprDictSub pTypeable ns + , Dict <- exprDictSub pTypeable a + -> case gcast a of + Nothing -> error "rebuild: type mismatch" + Just a -> a + Nothing -> error "rebuild: lost node" + + heuristic :: Set.Set VarId -> GatherInfo -> ASTF (NodeDomain dom) b -> Bool + heuristic bv gi b = not (isVariable pd b) && (giCount gi > 1 || not (Set.null (giScopes gi `Set.difference` bv))) + +-- | Given a array of nodes calculates the set of free variables in the +-- sub-expression each +nodesFreeVars :: forall dom + . PrjDict dom + -> Array NodeId (Gathered dom) + -> Array NodeId (Set.Set VarId) +nodesFreeVars pd nodes = freeVars + where + freeVars = array (bounds nodes) [(n, freeVarsNode n) | n <- indices nodes] + + freeVarsNode :: NodeId -> Set.Set VarId + freeVarsNode n = liftASTB freeVarsExp $ geExpr (nodes ! n) + + freeVarsExp :: AST (NodeDomain dom) a -> Set.Set VarId + freeVarsExp (Sym (C' (InjR var))) | Just v <- prjVariable pd var = Set.singleton v + freeVarsExp (Sym (C' (InjR lam)) :$ b) | Just v <- prjLambda pd lam = Set.delete v (freeVarsExp b) + freeVarsExp (Sym (C' (InjR _))) = Set.empty + freeVarsExp (Sym (C' (InjL (Node n)))) = freeVars ! n + freeVarsExp (s :$ b) = Set.union (freeVarsExp s) (freeVarsExp b) + +inlineAll :: forall dom a + . ConstrainedBy dom Typeable + => (NodeId -> ASTSAT (NodeDomain dom)) + -> ASTF (NodeDomain dom) a + -> ASTF dom a +inlineAll nodes a = go a + where + go :: AST (NodeDomain dom) sig -> AST dom sig + go (s :$ a) = go s :$ go a + go (Sym (C' (InjR s))) = Sym s + go s@(Sym (C' (InjL (Node n)))) = case nodes n of + ASTB a + | Dict <- exprDictSub pTypeable s + , Dict <- exprDictSub pTypeable a + -> case gcast a of + Nothing -> error "inlineAll: type mismatch" + Just a -> go a + + +type GatherEnv = + ( [NodeId] + -- List of nodes upwards in the syntax tree that cannot be hoisted over + , Set.Set VarId + -- Varibles in scope + ) +type GatherState dom = + ( GatherSet dom -- Set of expressions that have been recorded + , NodeId -- Node counter. + ) + +type GatherMonad dom a = ReaderT GatherEnv (State (GatherState dom)) a + +runGather :: GatherSet dom -> GatherMonad dom a -> (GatherSet dom, a) +runGather s gather = (gm,a) + where + (a,(gm,n')) = runState (runReaderT gather ([0], Set.empty)) (s,1) + +getInnerLimit :: GatherMonad dom NodeId +getInnerLimit = liftM (head . fst) ask + +getScope :: GatherMonad dom (Set.Set VarId) +getScope = liftM snd ask + +addInnerLimit :: NodeId -> GatherMonad dom a -> GatherMonad dom a +addInnerLimit n = local (\(ns,vs) -> (n:ns,vs)) + +addScopeVar :: VarId -> GatherMonad dom a -> GatherMonad dom a +addScopeVar v = local (\(ns,vs) -> (ns, Set.insert v vs )) + +-- | Convert an expression to a graph representation where each set of +-- alpha-equivalent sub-expressions share a node. Occurence counts for the +-- sub-expressions, and other information is also recorded. +gather :: forall dom a + . ( ConstrainedBy dom Typeable + , AlphaEq dom dom (NodeDomain dom) [(VarId,VarId)] + , Equality dom + ) + => (forall c. ASTF dom c -> Bool) + -> PrjDict dom + -> ASTF dom a + -> (GatherSet dom, ASTF (NodeDomain dom) a) +gather hoistOver pd a@(Sym s) | Dict <- exprDict a = (emptyGS, Sym (C' (InjR s))) +gather hoistOver pd a | Dict <- exprDict a + = runGather emptyGS (gatherRec (hoistOver a) a) + where + gather' :: Bool -> ASTF dom b -> GatherMonad dom (ASTF (NodeDomain dom) b) + gather' h a | Dict <- exprDict a = do + (a',n) <- + mfix (\(~(a',n)) -> do + a' <- addInnerLimitIf (not h) n $ gatherRec (hoistOver a) a + n <- recordExpr a' + return (a',n) + ) + return $ Sym $ C' $ InjL $ Node n + + addInnerLimitIf True n m = addInnerLimit n m + addInnerLimitIf _ n m = m + + gatherRec + :: (Sat dom (DenResult b)) + => Bool + -> AST dom b + -> GatherMonad dom (AST (NodeDomain dom) b) + gatherRec h (Sym lam :$ b) | Just v <- prjLambda pd lam = do + b' <- addScopeVar v $ gather' h b + return ((Sym (C' (InjR lam))) :$ b') + gatherRec h (Sym s) = return $ Sym $ C' $ InjR s + gatherRec h (s :$ b) = do + b' <- gather' h b + s' <- gatherRec h s + return (s' :$ b') + + recordExpr :: ASTF (NodeDomain dom) b -> GatherMonad dom NodeId + recordExpr a | Dict <- exprDict a = do + (s,n) <- get + innerLimit <- getInnerLimit + scope <- getScope + case lookupGS s a of + Just ge -> do + let ge' = ge { geInfo = updateInfo scope (geInfo ge) innerLimit } + put (updateGS s ge', n) + return (geNodeId ge) + Nothing -> do + let ge = Gathered { geExpr = ASTB a , geNodeId = n , geInfo = [(innerLimit, GatherInfo { giCount = 1 , giScopes = scope })] } + put (updateGS s ge, n+1) + return n + +updateInfo :: Set.Set VarId -> [(NodeId, GatherInfo)] -> NodeId -> [(NodeId, GatherInfo)] +updateInfo scope [] n = [(n, GatherInfo { giCount = 1 , giScopes = scope })] +updateInfo scope ((n,gi):xs) n' | n == n' = (n, gi') : xs + where + gi' = gi { giCount = giCount gi + 1 , giScopes = Set.union (giScopes gi) scope } +updateInfo scope (x:xs) n' = x : updateInfo scope xs n' + + +-- | Like 'reify' but with common sub-expression elimination and variable hoisting +reifySmart2 :: forall dom p pVar a + . ( AlphaEq dom dom (NodeDomain (FODomain dom p pVar)) [(VarId,VarId)] + , Equality dom + , Syntactic a + , Domain a ~ HODomain dom p pVar + , p :< Typeable + ) + => (forall c. ASTF (FODomain dom p pVar) c -> Bool) + -> MkInjDict (FODomain dom p pVar) + -> a + -> ASTF (FODomain dom p pVar) (Internal a) +reifySmart2 hoistOver mkId = flip evalState 0 . (codeMotion2 hoistOver prjDictFO mkId <=< reifyM . desugar) diff --git a/src/Language/Syntactic/Sharing/SimpleCodeMotion.hs b/src/Language/Syntactic/Sharing/SimpleCodeMotion.hs --- a/src/Language/Syntactic/Sharing/SimpleCodeMotion.hs +++ b/src/Language/Syntactic/Sharing/SimpleCodeMotion.hs @@ -125,7 +125,7 @@ -> MkInjDict dom -> ASTF dom a -> Maybe (Chosen dom a) -choose hoistOver pd mkId a = chooseEnv initEnv a +choose hoistOver pd mkId a = chooseEnvSub initEnv a where initEnv = Env { inLambda = False diff --git a/syntactic.cabal b/syntactic.cabal --- a/syntactic.cabal +++ b/syntactic.cabal @@ -1,5 +1,5 @@ Name: syntactic -Version: 1.11 +Version: 1.12.1 Synopsis: Generic abstract syntax, and utilities for embedded languages Description: This library provides: . @@ -51,7 +51,7 @@ Category: Language Build-type: Simple Cabal-version: >=1.10 -Tested-with: GHC==7.6.1, GHC==7.4.2 +Tested-with: GHC==7.6.2, GHC==7.8.2 extra-source-files: CONTRIBUTORS @@ -89,6 +89,7 @@ Language.Syntactic.Frontend.Tuple Language.Syntactic.Frontend.TupleConstrained Language.Syntactic.Sharing.SimpleCodeMotion + Language.Syntactic.Sharing.CodeMotion2 Language.Syntactic.Sharing.Utils Language.Syntactic.Sharing.Graph Language.Syntactic.Sharing.StableName @@ -141,6 +142,40 @@ hs-source-dirs: tests examples main-is: NanoFeldsparEval.hs + + other-modules: + + default-language: Haskell2010 + + default-extensions: + FlexibleContexts + FlexibleInstances + GADTs + MultiParamTypeClasses + ScopedTypeVariables + TypeFamilies + TypeOperators + UndecidableInstances + ViewPatterns + + other-extensions: + TemplateHaskell + + build-depends: + syntactic, + base, + mtl >= 2 && < 3, + QuickCheck >= 2.4 && < 3, + tasty, + tasty-th, + tasty-quickcheck + +test-suite NanoFeldsparEval2 + type: exitcode-stdio-1.0 + + hs-source-dirs: tests examples + + main-is: NanoFeldsparEval2.hs other-modules: diff --git a/tests/NanoFeldsparEval2.hs b/tests/NanoFeldsparEval2.hs new file mode 100644 --- /dev/null +++ b/tests/NanoFeldsparEval2.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE TemplateHaskell #-} + +import Test.Tasty +import Test.Tasty.TH +import Test.Tasty.QuickCheck + +import NanoFeldspar.Core (eval2) +import NanoFeldspar.Test + + + +prop_scProd a b = eval2 scProd a' b' == ref a' b' + where + a' = take 20 a + b' = take 20 b + ref a b = sum (zipWith (*) a b) + +prop_1 a b = eval2 prog1 a' b == ref a' b + where + a' = a `mod` 20 + ref a b = [min (i+3) b | i <- [0..a-1]] + +prop_2 a = eval2 prog2 a == ref a + where + ref a = max (min a a) (min a a) + +prop_3 a b = eval2 prog3 a b' == ref a b' + where + b' = a - (b `mod` 20) + ref a b = sum [l .. u] + where + l = min a b + u = max a b + +prop_4 a = eval2 prog4 a' == ref a' + where + a' = a `mod` 20 + ref a = [(a+a)*i | i <- [0..a-1]] + +prop_5 a = eval2 prog5 a == ref a + where + ref a = let (b,c) = (a*2,a*3) in (b-c)*(c-b) + +prop_6 = eval2 prog6 == ref + where + ref = as!!1 + sum as + sum as + where + as = map (*2) [1..20] + +prop_8 a = eval2 prog8 a == ref a + where + ref a = [a .. a+9] + + + +main = $(defaultMainGenerator) +