diff --git a/src/Conjure/Language/AbstractLiteral.hs b/src/Conjure/Language/AbstractLiteral.hs index 31c626e43..8c6e92d0e 100644 --- a/src/Conjure/Language/AbstractLiteral.hs +++ b/src/Conjure/Language/AbstractLiteral.hs @@ -50,6 +50,7 @@ instance (SimpleJSON x, Pretty x, ExpressionLike x) => SimpleJSON (AbstractLiter AbsLitVariant _ nm x -> do x' <- toSimpleJSON x return $ JSON.Object $ KM.fromList [(fromString (renderNormal nm), x')] + AbsLitSequence xs -> toSimpleJSON xs AbsLitMatrix index xs -> case index of DomainInt _ ranges -> do @@ -59,7 +60,6 @@ instance (SimpleJSON x, Pretty x, ExpressionLike x) => SimpleJSON (AbstractLiter AbsLitSet xs -> toSimpleJSON xs AbsLitMSet xs -> toSimpleJSON xs AbsLitFunction xs -> toSimpleJSON (AsDictionary xs) - AbsLitSequence xs -> toSimpleJSON xs AbsLitRelation xs -> toSimpleJSON xs AbsLitPartition xs -> toSimpleJSON xs fromSimpleJSON = noFromSimpleJSON "AbstractLiteral" diff --git a/src/Conjure/Language/AdHoc.hs b/src/Conjure/Language/AdHoc.hs index 3cf7ebcf0..574f8e5f1 100644 --- a/src/Conjure/Language/AdHoc.hs +++ b/src/Conjure/Language/AdHoc.hs @@ -115,7 +115,7 @@ instance SimpleJSON Integer where Nothing -> noFromSimpleJSON "Integer" t text _ -> noFromSimpleJSON "Integer" t x -data AsDictionary a b = AsDictionary [(a,b)] +newtype AsDictionary a b = AsDictionary [(a,b)] instance (Pretty x, SimpleJSON x, SimpleJSON y) => SimpleJSON (AsDictionary x y) where toSimpleJSON (AsDictionary xs) = do diff --git a/src/Conjure/Language/Constant.hs b/src/Conjure/Language/Constant.hs index 5b7cecbcd..5bd08c415 100644 --- a/src/Conjure/Language/Constant.hs +++ b/src/Conjure/Language/Constant.hs @@ -103,6 +103,9 @@ instance SimpleJSON Constant where fromSimpleJSON _ (JSON.Bool b) = return (ConstantBool b) + fromSimpleJSON (TypeInt (TagEnum enum_type_name)) (JSON.String value) = + return (ConstantEnum (Name enum_type_name) [] (Name value)) + fromSimpleJSON t@TypeInt{} x@JSON.Number{} = ConstantInt TagInt <$> fromSimpleJSON t x fromSimpleJSON t@TypeInt{} x@JSON.String{} = ConstantInt TagInt <$> fromSimpleJSON t x @@ -175,8 +178,7 @@ instance SimpleJSON Constant where return $ ConstantAbstract $ AbsLitFunction ys fromSimpleJSON ty@(TypeFunction fr to) value@(JSON.Array xs) = do - mys <- forM (V.toList xs) $ \ x -> - case x of + mys <- forM (V.toList xs) $ \case JSON.Array x' -> case V.toList x' of [a', b'] -> do @@ -190,6 +192,17 @@ instance SimpleJSON Constant where then return $ ConstantAbstract $ AbsLitFunction ys else noFromSimpleJSON "Constant" ty value + fromSimpleJSON (TypeSequence inner) (JSON.Object m) = do + ys :: [(Integer, Constant)] <- forM (KM.toList m) $ \ (toText->name, value) -> do + -- the name must be an integer + a <- fromSimpleJSON (TypeInt TagInt) (JSON.String name) + b <- fromSimpleJSON inner value + return (a, b) + + let ys_sorted = sort ys + + return $ ConstantAbstract $ AbsLitSequence (map snd ys_sorted) + fromSimpleJSON (TypeSequence t) (JSON.Array xs) = ConstantAbstract . AbsLitSequence <$> mapM (fromSimpleJSON t) (V.toList xs) @@ -456,7 +469,7 @@ viewConstantMatrix constant = indices_as_int = [ i | ConstantInt _ i <- indices ] if length indices == length indices_as_int then - if length indices > 0 + if not (null indices) then if maximum indices_as_int - minimum indices_as_int + 1 == genericLength indices then return (DomainInt TagInt [RangeBounded (fromInt (minimum indices_as_int)) (fromInt (maximum indices_as_int))], values) @@ -494,6 +507,7 @@ viewConstantFunction constant = do viewConstantSequence :: MonadFailDoc m => Constant -> m [Constant] viewConstantSequence (ConstantAbstract (AbsLitSequence xs)) = return xs +viewConstantSequence (ConstantAbstract (AbsLitMatrix _ xs)) = return xs viewConstantSequence (TypedConstant c _) = viewConstantSequence c viewConstantSequence constant = failDoc ("Expecting a sequence, but got:" <++> pretty constant) diff --git a/src/Conjure/Language/Definition.hs b/src/Conjure/Language/Definition.hs index a5752e47b..63d4662b3 100644 --- a/src/Conjure/Language/Definition.hs +++ b/src/Conjure/Language/Definition.hs @@ -105,20 +105,29 @@ fromSimpleJSONModel essence json = case json of JSON.Object inners -> do stmts <- forM (KM.toList inners) $ \ (toText->name, valueJSON) -> do - -- traceM $ show $ "name " <+> pretty name let mdomain = [ dom | Declaration (FindOrGiven Given (Name nm) dom) <- mStatements essence , nm == name ] - -- traceM $ show $ "mdomain " <+> vcat (map pretty mdomain) - case mdomain of - [domain] -> do - -- traceM $ show $ "domain " <+> pretty domain + let enums = [ nm + | Name nm <- essence |> mInfo |> miEnumGivens + , nm == name + ] + case (mdomain, enums) of + ([domain], _) -> do typ <- typeOfDomain domain - -- traceM $ show $ "typ " <+> pretty typ value <- fromSimpleJSON typ valueJSON - -- traceM $ show $ "value " <+> pretty value return $ Just $ Declaration (Letting (Name name) value) + (_, [enum]) -> do + case valueJSON of + JSON.Array v -> do + let vals = [ case str of + JSON.String t -> Name t + _ -> bug ("fromSimpleJSONModel not name: " <+> pretty (show str)) + | str <- V.toList v + ] + return $ Just $ Declaration (LettingDomainDefnEnum (Name enum) vals) + _ -> bug "fromSimpleJSONModel" _ -> do logWarn $ "Ignoring" <+> pretty name <+> "from the JSON file." return Nothing diff --git a/src/Conjure/Language/Expression.hs b/src/Conjure/Language/Expression.hs index 7d04952fd..a4b510138 100644 --- a/src/Conjure/Language/Expression.hs +++ b/src/Conjure/Language/Expression.hs @@ -164,6 +164,9 @@ instance SimpleJSON Declaration where Letting nm x -> do x' <- toSimpleJSON x return $ JSON.Object $ KM.fromList [(fromString (renderNormal nm), x')] + LettingDomainDefnEnum nm xs -> do + let xs' = map (fromString . renderNormal) xs + return $ JSON.Object $ KM.fromList [(fromString (renderNormal nm), JSON.Array (V.fromList xs'))] _ -> noToSimpleJSON d fromSimpleJSON = noFromSimpleJSON "Declaration" diff --git a/src/Conjure/Language/Expression/Op/TwoBars.hs b/src/Conjure/Language/Expression/Op/TwoBars.hs index 2ecf672e5..a71577fa6 100644 --- a/src/Conjure/Language/Expression/Op/TwoBars.hs +++ b/src/Conjure/Language/Expression/Op/TwoBars.hs @@ -29,6 +29,7 @@ instance (TypeOf x, Pretty x, Domain () x :< x) => TypeOf (OpTwoBars x) where case ty of TypeInt _ -> return () TypeList{} -> return () + TypeMatrix{} -> return () TypeSet{} -> return () TypeMSet{} -> return () TypeFunction{} -> return () diff --git a/src/Conjure/Process/Enums.hs b/src/Conjure/Process/Enums.hs index 80a22b155..c544c0852 100644 --- a/src/Conjure/Process/Enums.hs +++ b/src/Conjure/Process/Enums.hs @@ -194,6 +194,12 @@ removeEnumsFromParam model param = do = return (fromIntWithTag i (TagEnum ename)) onX p = return p + onC :: Monad m => Constant -> m Constant + onC (ConstantEnum _ _ nm) + | Just (Name ename, i) <- M.lookup nm nameToIntMapping + = return (fromIntWithTag i (TagEnum ename)) + onC p = return p + onD :: MonadFailDoc m => Domain () Expression -> m (Domain () Expression) onD (DomainEnum nm@(Name nmText) (Just ranges) _) | Just _ <- M.lookup nm enumDomainNames @@ -207,7 +213,7 @@ removeEnumsFromParam model param = do onD p = return p let param' = param { mStatements = catMaybes statements' } - let f = transformBiM onD >=> transformBiM onX + let f = transformBiM onD >=> transformBiM onX >=> transformBiM onC (,) <$> f model <*> f param' diff --git a/src/Conjure/Process/ValidateConstantForDomain.hs b/src/Conjure/Process/ValidateConstantForDomain.hs index 8fc7c40a7..7e8f804dd 100644 --- a/src/Conjure/Process/ValidateConstantForDomain.hs +++ b/src/Conjure/Process/ValidateConstantForDomain.hs @@ -4,41 +4,10 @@ module Conjure.Process.ValidateConstantForDomain ( validateConstantForDomain ) w import Conjure.Prelude import Conjure.Language.Constant - ( viewConstantBool, - viewConstantFunction, - viewConstantIntWithTag, - viewConstantMSet, - viewConstantMatrix, - viewConstantPartition, - viewConstantRecord, - viewConstantRelation, - viewConstantSequence, - viewConstantSet, - viewConstantTuple, - viewConstantVariant, - Constant(ConstantEnum, TypedConstant, ConstantInt, ConstantBool) ) import Conjure.Language.Definition - ( Name, - NameGen, forgetRepr ) import Conjure.Language.Domain - ( Domain(DomainBool, DomainUnnamed, DomainEnum, DomainPartition, - DomainTuple, DomainRecord, DomainVariant, DomainMatrix, DomainInt, - DomainSet, DomainMSet, DomainFunction, DomainSequence, - DomainRelation), - Range(RangeBounded, RangeOpen, RangeSingle, RangeLowerBounded, - RangeUpperBounded), - BinaryRelationAttrs(BinaryRelationAttrs), - RelationAttr(RelationAttr), - OccurAttr(OccurAttr_MinMaxOccur, OccurAttr_None, - OccurAttr_MinOccur, OccurAttr_MaxOccur), - MSetAttr(MSetAttr), - SizeAttr(SizeAttr_MinMaxSize, SizeAttr_None, SizeAttr_Size, - SizeAttr_MinSize, SizeAttr_MaxSize), - SetAttr(SetAttr), - binRelToAttrName, SequenceAttr (SequenceAttr), JectivityAttr (JectivityAttr_Surjective, JectivityAttr_Bijective) ) +import Conjure.Language.Type import Conjure.Language.Pretty -import Conjure.Language.Type ( TypeCheckerMode ) -import Conjure.Language.Expression import Conjure.Language.Instantiate ( instantiateExpression ) import Conjure.Process.AttributeAsConstraints ( mkAttributeToConstraint ) import Conjure.Process.Enumerate ( EnumerateDomain, enumerateDomain ) @@ -64,6 +33,9 @@ validateConstantForDomain _ (viewConstantBool -> Just _) DomainBool{} = return ( validateConstantForDomain _ _ (DomainInt _ []) = return () -- no restrictions +-- enums, always ok +validateConstantForDomain _ (ConstantEnum (Name ty1) _ _) (DomainInt (TagEnum ty2) _) | ty1 == ty2 = return () + validateConstantForDomain name c@(viewConstantIntWithTag -> Just (cTag, i)) d@(DomainInt dTag rs) | cTag == dTag = let intInRange RangeOpen = True diff --git a/src/Conjure/Rules/Transform.hs b/src/Conjure/Rules/Transform.hs index 5f6a71fe3..455b7fb96 100644 --- a/src/Conjure/Rules/Transform.hs +++ b/src/Conjure/Rules/Transform.hs @@ -1,532 +1,605 @@ {-# LANGUAGE QuasiQuotes #-} + module Conjure.Rules.Transform (rules_Transform) where -import Conjure.Rules.Vertical.Variant (onTagged) -import Conjure.Rules.Import +import Conjure.Rules.Import +import Conjure.Rules.Vertical.Variant (onTagged) rules_Transform :: [Rule] -rules_Transform = - [ rule_Transform_Sequence_Literal - , rule_Transform_Functorially - , rule_Transform_Comprehension - , rule_Transform_Product_Types - , rule_Transform_Matrix - , rule_Transform_Partition - , rule_Transform_Sequence - , rule_Transform_Sequence_Defined - , rule_Transformed_Indexing - , rule_Lift_Transformed_Indexing - , rule_Transform_Indexing - , rule_Transform_Unifying - - , rule_Transform_Variant_Literal - , rule_Transform_Variant_Eq - , rule_Transform_Variant_Neq - , rule_Transform_Variant_Lt - , rule_Transform_Variant_Leq - , rule_Transformed_Variant_Index - , rule_Transformed_Variant_Active +rules_Transform = + [ rule_Transform_Sequence_Literal, + rule_Transform_Functorially, + rule_Transform_Comprehension, + rule_Transform_Product_Types, + rule_Transform_Matrix, + rule_Transform_Partition, + rule_Transform_Sequence, + rule_Transform_Sequence_Defined, + rule_Transformed_Indexing, + rule_Lift_Transformed_Indexing, + rule_Transform_Indexing, + rule_Transform_Unifying, + rule_Transform_Variant_Literal, + rule_Transform_Variant_Eq, + rule_Transform_Variant_Neq, + rule_Transform_Variant_Lt, + rule_Transform_Variant_Leq, + rule_Transformed_Variant_Index, + rule_Transformed_Variant_Active ] - rule_Transform_Functorially :: Rule -rule_Transform_Functorially = "transform-functorially" `namedRule` theRule where - theRule (Comprehension body gensOrConds) = do - (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of - Generator (GenInExpr (Single pat) expr) -> - return (pat, matchDefs [opToSet, opToMSet] expr) - _ -> na "rule_Transform_Functorially" - (morphism, y) <- match opTransform x - ty <- typeOf y - inn <- morphing =<< typeOf morphism - if let ?typeCheckerMode = StronglyTyped in ty `containsTypeFunctorially` inn - then - return - ( "Horizontal rule for transform of functorially" - , do - (dPat, d) <- quantifiedVar - return (Comprehension body $ - gocBefore - ++ [Generator (GenInExpr dPat [essence| &y |])] - ++ ((ComprehensionLetting (Single pat) [essence| - transform(&morphism, &d) |] ):gocAfter) - ) - ) - else na "rule_Transform_Functorially" - theRule _ = na "rule_Transform_Functorially" - +rule_Transform_Functorially = "transform-functorially" `namedRule` theRule + where + theRule (Comprehension body gensOrConds) = do + (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of + Generator (GenInExpr (Single pat) expr) -> + return (pat, matchDefs [opToSet, opToMSet] expr) + _ -> na "rule_Transform_Functorially" + (morphism, y) <- match opTransform x + ty <- typeOf y + inn <- morphing =<< typeOf morphism + if let ?typeCheckerMode = StronglyTyped in ty `containsTypeFunctorially` inn + then + return + ( "Horizontal rule for transform of functorially", + do + (dPat, d) <- quantifiedVar + return + ( Comprehension body + $ gocBefore + ++ [Generator (GenInExpr dPat y)] + ++ ( ( ComprehensionLetting + (Single pat) + [essence| + transform(&morphism, &d) |] + ) + : gocAfter + ) + ) + ) + else na "rule_Transform_Functorially" + theRule _ = na "rule_Transform_Functorially" rule_Transform_Comprehension :: Rule -rule_Transform_Comprehension = "transform-comprehension" `namedRule` theRule where - theRule x = do - (morphism, cmp@(Comprehension body gensOrConds)) <- match opTransform x - ty <- typeOf cmp - inn <- morphing =<< typeOf morphism - if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn - then - return ( "Horizontal rule for transform comprehension" - , do - gox <- sequence (transformOverGenOrCond morphism <$> gensOrConds) - return $ Comprehension [essence| - transform(&morphism, &body) - |] (join gox) - ) - else na "rule_Transform_Comprehension" - transformOverGenOrCond m (Generator g) = transformOverGenerator m g - transformOverGenOrCond m (Condition e) = - return [Condition [essence| transform(&m,&e) |]] - transformOverGenOrCond m (ComprehensionLetting pat e) = - return [ComprehensionLetting pat [essence| transform(&m,&e) |]] - - transformOverGenerator m (GenDomainHasRepr a d) = do - (Single nm, n) <- quantifiedVarOverDomain $ forgetRepr d - return [Generator (GenDomainHasRepr nm d) - ,ComprehensionLetting (Single a) [essence| transform(&m, &n) |] - ] - transformOverGenerator m (GenInExpr a e) = - return [Generator (GenInExpr a [essence| transform(&m,&e) |])] - transformOverGenerator m (GenDomainNoRepr absPat d) = do - (rPat, ns) <- clonePattern absPat - return $ [Generator (GenDomainNoRepr rPat d)] - ++ ((\(pat,exp) -> - ComprehensionLetting (Single pat) [essence| transform(&m,&exp) |] - ) <$> ns) - - clonePattern (Single name) = do - (nPat, n) <- quantifiedVar - return (nPat,[(name, n)]) - clonePattern (AbsPatTuple pats) = do - rec <- sequence (clonePattern <$> pats) - return ( AbsPatTuple $ fst <$> rec - , join $ snd <$> rec) - clonePattern (AbsPatMatrix pats) = do - rec <- sequence (clonePattern <$> pats) - return ( AbsPatMatrix $ fst <$> rec - , join $ snd <$> rec) - clonePattern (AbsPatSet pats) = do - rec <- sequence (clonePattern <$> pats) - return ( AbsPatSet $ fst <$> rec - , join $ snd <$> rec) - clonePattern _ = - bug "rule_Transform_Comprehension: clonePattern: unsupported Abstract Pattern" +rule_Transform_Comprehension = "transform-comprehension" `namedRule` theRule + where + theRule x = do + (morphism, cmp@(Comprehension body gensOrConds)) <- match opTransform x + ty <- typeOf cmp + inn <- morphing =<< typeOf morphism + if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn + then + return + ( "Horizontal rule for transform comprehension", + do + gox <- sequence (transformOverGenOrCond morphism <$> gensOrConds) + return + $ Comprehension + [essence| transform(&morphism, &body) |] + (join gox) + ) + else na "rule_Transform_Comprehension" + transformOverGenOrCond m (Generator g) = transformOverGenerator m g + transformOverGenOrCond m (Condition e) = + return [Condition [essence| transform(&m,&e) |]] + transformOverGenOrCond m (ComprehensionLetting pat e) = + return [ComprehensionLetting pat [essence| transform(&m,&e) |]] + + transformOverGenerator m (GenDomainHasRepr a d) = do + (Single nm, n) <- quantifiedVarOverDomain $ forgetRepr d + return + [ Generator (GenDomainHasRepr nm d), + ComprehensionLetting (Single a) [essence| transform(&m, &n) |] + ] + transformOverGenerator m (GenInExpr a e) = + return [Generator (GenInExpr a [essence| transform(&m,&e) |])] + transformOverGenerator m (GenDomainNoRepr absPat d) = do + (rPat, ns) <- clonePattern absPat + return + $ [Generator (GenDomainNoRepr rPat d)] + ++ ( ( \(pat, exp) -> + ComprehensionLetting (Single pat) [essence| transform(&m,&exp) |] + ) + <$> ns + ) + clonePattern (Single name) = do + (nPat, n) <- quantifiedVar + return (nPat, [(name, n)]) + clonePattern (AbsPatTuple pats) = do + rec <- sequence (clonePattern <$> pats) + return + ( AbsPatTuple $ fst <$> rec, + join $ snd <$> rec + ) + clonePattern (AbsPatMatrix pats) = do + rec <- sequence (clonePattern <$> pats) + return + ( AbsPatMatrix $ fst <$> rec, + join $ snd <$> rec + ) + clonePattern (AbsPatSet pats) = do + rec <- sequence (clonePattern <$> pats) + return + ( AbsPatSet $ fst <$> rec, + join $ snd <$> rec + ) + clonePattern _ = + bug "rule_Transform_Comprehension: clonePattern: unsupported Abstract Pattern" rule_Transform_Product_Types :: Rule -rule_Transform_Product_Types = "transform-product-types" `namedRule` theRule where - theRule [essence| transform(&morphism, &i) |] = do - inn <- morphing =<< typeOf morphism - ti <- typeOf i - if let ?typeCheckerMode = StronglyTyped in ti `containsProductType` inn - then case ti of - (TypeTuple tint) -> do - let tupleIndexTransform indx = - let indexexpr = Constant (ConstantInt TagInt indx) - in [essence| transform(&morphism, &i[&indexexpr]) |] - tupleExpression = - AbstractLiteral $ AbsLitTuple - $ (tupleIndexTransform <$> [1..(fromIntegral $ length tint)]) - return - ( "Horizontal rule for transform of tuple" - , return tupleExpression - ) - (TypeRecord namet) -> do - let recordIndexTransform indx = - let indexexpr = Reference (fst indx) - $ Just $ RecordField (fst indx) (snd indx) - in (fst indx, [essence| transform(&morphism, &i[&indexexpr]) |]) - recordExpression = AbstractLiteral $ AbsLitRecord - $ (recordIndexTransform <$> namet) - return - ( "Horizontal rule for transform of record" - , return recordExpression - ) - _ -> bug "rule_Transform_Product_Types this is a bug" - else na "rule_Transform_Product_Types" - theRule _ = na "rule_Transform_Product_Types" - +rule_Transform_Product_Types = "transform-product-types" `namedRule` theRule + where + theRule [essence| transform(&morphism, &i) |] = do + inn <- morphing =<< typeOf morphism + ti <- typeOf i + if let ?typeCheckerMode = StronglyTyped in ti `containsProductType` inn + then case ti of + (TypeTuple tint) -> do + let tupleIndexTransform indx = + let indexexpr = Constant (ConstantInt TagInt indx) + in [essence| transform(&morphism, &i[&indexexpr]) |] + tupleExpression = + AbstractLiteral + $ AbsLitTuple + $ (tupleIndexTransform <$> [1 .. (fromIntegral $ length tint)]) + return + ( "Horizontal rule for transform of tuple", + return tupleExpression + ) + (TypeRecord namet) -> do + let recordIndexTransform indx = + let indexexpr = + Reference (fst indx) + $ Just + $ RecordField (fst indx) (snd indx) + in (fst indx, [essence| transform(&morphism, &i[&indexexpr]) |]) + recordExpression = + AbstractLiteral + $ AbsLitRecord + $ (recordIndexTransform <$> namet) + return + ( "Horizontal rule for transform of record", + return recordExpression + ) + _ -> bug "rule_Transform_Product_Types this is a bug" + else na "rule_Transform_Product_Types" + theRule _ = na "rule_Transform_Product_Types" rule_Transform_Matrix :: Rule -rule_Transform_Matrix = "transform-matrix" `namedRule` theRule where - theRule (Comprehension body gensOrConds) = do - (gocBefore, (pat, exp), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of - Generator (GenInExpr (Single pat) expr) -> return (pat, expr) - _ -> na "rule_Transform_Matrix" - (morphism, matexp) <- match opTransform exp - DomainMatrix domIndx _ <- domainOf matexp - ty <- typeOf matexp - inn <- morphing =<< typeOf morphism - if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn - then return - ( "Horizontal rule for transform matrix in comprehension generator" - , do - (dPat, d) <- quantifiedVar - (Single mName, m) <- quantifiedVar - (Single iName, i) <- quantifiedVar - return (Comprehension body $ - gocBefore - ++ [Generator (GenDomainNoRepr dPat (forgetRepr domIndx))] - ++ [ComprehensionLetting (Single iName) [essence| transform(&morphism, &d) |]] - ++ [ComprehensionLetting (Single mName) [essence| &matexp[&i] |]] - ++ [ComprehensionLetting (Single pat) [essence| transform(&morphism, &m) |]] - ++ gocAfter) - ) - else na "rule_Transform_Matrix" - theRule _ = na "rule_Transform_Matrix" - +rule_Transform_Matrix = "transform-matrix" `namedRule` theRule + where + theRule (Comprehension body gensOrConds) = do + (gocBefore, (pat, exp), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of + Generator (GenInExpr (Single pat) expr) -> return (pat, expr) + _ -> na "rule_Transform_Matrix" + (morphism, matexp) <- match opTransform exp + DomainMatrix domIndx _ <- domainOf matexp + ty <- typeOf matexp + inn <- morphing =<< typeOf morphism + if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn + then + return + ( "Horizontal rule for transform matrix in comprehension generator", + do + (dPat, d) <- quantifiedVar + (Single mName, m) <- quantifiedVar + (Single iName, i) <- quantifiedVar + return + ( Comprehension body + $ gocBefore + ++ [Generator (GenDomainNoRepr dPat (forgetRepr domIndx))] + ++ [ComprehensionLetting (Single iName) [essence| transform(&morphism, &d) |]] + ++ [ComprehensionLetting (Single mName) [essence| &matexp[&i] |]] + ++ [ComprehensionLetting (Single pat) [essence| transform(&morphism, &m) |]] + ++ gocAfter + ) + ) + else na "rule_Transform_Matrix" + theRule _ = na "rule_Transform_Matrix" rule_Transform_Partition :: Rule -rule_Transform_Partition = "transform-partition" `namedRule` theRule where - theRule (Comprehension body gensOrConds) = do - (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of - Generator (GenInExpr (Single pat) expr) -> return (pat, expr) - _ -> na "rule_Transform_Partition" - z <- match opParts x - (morphism, y) <- match opTransform z - ty <- typeOf y - case ty of TypePartition{} -> return () ; _ -> na "only applies to partitions" - inn <- morphing =<< typeOf morphism - if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn - then do - return - ( "Horizontal rule for transform of partition" - , do - (dPat, d) <- quantifiedVar - return (Comprehension body $ - gocBefore - ++ [Generator (GenInExpr dPat [essence| parts(&y) |])] - ++ ((ComprehensionLetting (Single pat) [essence| transform(&morphism, &d) |] ):gocAfter) - ) - ) - else na "rule_Transform_Partition" - theRule _ = na "rule_Transform_Partition" - +rule_Transform_Partition = "transform-partition" `namedRule` theRule + where + theRule (Comprehension body gensOrConds) = do + (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of + Generator (GenInExpr (Single pat) expr) -> return (pat, expr) + _ -> na "rule_Transform_Partition" + z <- match opParts x + (morphism, y) <- match opTransform z + ty <- typeOf y + case ty of TypePartition {} -> return (); _ -> na "only applies to partitions" + inn <- morphing =<< typeOf morphism + if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn + then do + return + ( "Horizontal rule for transform of partition", + do + (dPat, d) <- quantifiedVar + return + ( Comprehension body + $ gocBefore + ++ [Generator (GenInExpr dPat [essence| parts(&y) |])] + ++ ((ComprehensionLetting (Single pat) [essence| transform(&morphism, &d) |]) : gocAfter) + ) + ) + else na "rule_Transform_Partition" + theRule _ = na "rule_Transform_Partition" rule_Transform_Sequence :: Rule -rule_Transform_Sequence = "transform-sequence" `namedRule` theRule where - theRule (Comprehension body gensOrConds) = do - (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of - Generator (GenInExpr (Single pat) expr) -> - return (pat, matchDefs [opToSet, opToMSet] expr) - _ -> na "rule_Transform_Sequence" - (morphism, y) <- match opTransform x - ty <- typeOf y - case ty of TypeSequence{} -> return () ; _ -> na "only applies to sequences" - inn <- morphing =<< typeOf morphism - if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn - then do - return - ( "Horizontal rule for transform of sequence" - , do - (dPat, d) <- quantifiedVar - return (Comprehension body $ - gocBefore - ++ [Generator (GenInExpr dPat [essence| &y |])] - ++ ((ComprehensionLetting (Single pat) [essence| - (&d[1], transform(&morphism, &d[2])) |] ):gocAfter) - ) - - ) - else na "rule_Transform_Sequence" - theRule _ = na "rule_Transform_Sequence" - +rule_Transform_Sequence = "transform-sequence" `namedRule` theRule + where + theRule (Comprehension body gensOrConds) = do + (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of + Generator (GenInExpr (Single pat) expr) -> + return (pat, matchDefs [opToSet, opToMSet] expr) + _ -> na "rule_Transform_Sequence" + (morphism, y) <- match opTransform x + ty <- typeOf y + case ty of TypeSequence {} -> return (); _ -> na "only applies to sequences" + inn <- morphing =<< typeOf morphism + if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn + then do + return + ( "Horizontal rule for transform of sequence", + do + (dPat, d) <- quantifiedVar + return + ( Comprehension body + $ gocBefore + ++ [Generator (GenInExpr dPat y)] + ++ ( ( ComprehensionLetting + (Single pat) + [essence| + (&d[1], transform(&morphism, &d[2])) |] + ) + : gocAfter + ) + ) + ) + else na "rule_Transform_Sequence" + theRule _ = na "rule_Transform_Sequence" rule_Transform_Sequence_Defined :: Rule -rule_Transform_Sequence_Defined = "transform-sequence-defined" `namedRule` theRule where - theRule (Comprehension body gensOrConds) = do - (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of - Generator (GenInExpr pat@Single{} expr) -> - return (pat, matchDefs [opToSet, opToMSet] expr) - _ -> na "rule_Transform_Sequence_Defined" - defi <- match opDefined x - (morphism, y) <- match opTransform defi - ty <- typeOf y - case ty of TypeSequence{} -> return () ; _ -> na "only applies to sequences" - inn <- morphing =<< typeOf morphism - if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn - then do - return - ( "Horizontal rule for transform of sequence defined" - , do - return (Comprehension body $ - gocBefore - ++ [Generator (GenInExpr pat [essence| defined(&y) |])] - ++ gocAfter - ) - ) - else na "rule_Transform_Sequence_Defined" - theRule _ = na "rule_Transform_Sequence_Defined" - +rule_Transform_Sequence_Defined = "transform-sequence-defined" `namedRule` theRule + where + theRule (Comprehension body gensOrConds) = do + (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of + Generator (GenInExpr pat@Single {} expr) -> + return (pat, matchDefs [opToSet, opToMSet] expr) + _ -> na "rule_Transform_Sequence_Defined" + defi <- match opDefined x + (morphism, y) <- match opTransform defi + ty <- typeOf y + case ty of TypeSequence {} -> return (); _ -> na "only applies to sequences" + inn <- morphing =<< typeOf morphism + if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn + then do + return + ( "Horizontal rule for transform of sequence defined", + do + return + ( Comprehension body + $ gocBefore + ++ [Generator (GenInExpr pat [essence| defined(&y) |])] + ++ gocAfter + ) + ) + else na "rule_Transform_Sequence_Defined" + theRule _ = na "rule_Transform_Sequence_Defined" rule_Transformed_Indexing :: Rule -rule_Transformed_Indexing = "transformed-indexing" `namedRule` theRule where - theRule (Comprehension body gensOrConds) = do - (gocBefore, (pat, exp), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of - Generator (GenInExpr (Single pat) expr) -> return (pat, expr) - _ -> na "rule_Transformed_Indexing" - (matexp, indexer) <- match opIndexing exp - (morphism, mat) <- match opTransform matexp - ty <- typeOf mat - inn <- morphing =<< typeOf morphism - if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn - then do - return - ( "Horizontal rule for transformed indexing" - , do - (Single mName, m) <- quantifiedVar - return (Comprehension body $ - gocBefore - ++ [ComprehensionLetting (Single mName) [essence| &matexp[&indexer] |]] - - ++ [ComprehensionLetting (Single pat) [essence| transform(&morphism, &m) |]] - ++ gocAfter) - ) - else na "rule_Transformed_Indexing" - theRule _ = na "rule_Transformed_Indexing" - +rule_Transformed_Indexing = "transformed-indexing" `namedRule` theRule + where + theRule (Comprehension body gensOrConds) = do + (gocBefore, (pat, exp), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of + Generator (GenInExpr (Single pat) expr) -> return (pat, expr) + _ -> na "rule_Transformed_Indexing" + (matexp, indexer) <- match opIndexing exp + (morphism, mat) <- match opTransform matexp + ty <- typeOf mat + inn <- morphing =<< typeOf morphism + if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn + then do + return + ( "Horizontal rule for transformed indexing", + do + (Single mName, m) <- quantifiedVar + return + ( Comprehension body + $ gocBefore + ++ [ComprehensionLetting (Single mName) [essence| &matexp[&indexer] |]] + ++ [ComprehensionLetting (Single pat) [essence| transform(&morphism, &m) |]] + ++ gocAfter + ) + ) + else na "rule_Transformed_Indexing" + theRule _ = na "rule_Transformed_Indexing" rule_Lift_Transformed_Indexing :: Rule -rule_Lift_Transformed_Indexing = "lift-transformed-indexing" `namedRule` theRule where - matchIndexing :: (?typeCheckerMode :: TypeCheckerMode) - => Expression - -> Maybe (Expression, Expression, Expression, Expression) - matchIndexing exp = do - (matexp, indexer) <- match opIndexing exp - (morphism, mat) <- match opTransform matexp - return (exp, morphism, mat, indexer) - - liftIndexing (exp, morphism, mat, indexer) = do - (Single nm, m) <- quantifiedVar - return ( (exp, [essence| transform(&morphism, &m) |]) - , ComprehensionLetting (Single nm) [essence| &mat[&indexer] |]) - - transformBody bdy [] = bdy - transformBody bdy ((orig, repl):rest) = - let nbdy = transformBi (\e -> if e == orig - then repl - else e) bdy - in transformBody nbdy rest - - theRule (Comprehension body gensOrConds) = do - let matched = catMaybes [matchIndexing exp | exp <- universeBi body] - case matched of - [] -> na "rule_Lift_Transformed_Indexing: nothing to lift" - _ -> do - replacements <- sequence (liftIndexing <$> matched) - return ( "Horizontal rule for lift transformed indexing" - , return (Comprehension (transformBody body (fst <$> replacements)) $ - gensOrConds ++ (snd <$> replacements)) - ) - theRule _ = na "rule_Lift_Transformed_Indexing" +rule_Lift_Transformed_Indexing = "lift-transformed-indexing" `namedRule` theRule + where + matchIndexing :: + (?typeCheckerMode :: TypeCheckerMode) => + Expression -> + Maybe (Expression, Expression, Expression, Expression) + matchIndexing exp = do + (matexp, indexer) <- match opIndexing exp + (morphism, mat) <- match opTransform matexp + return (exp, morphism, mat, indexer) + + liftIndexing (exp, morphism, mat, indexer) = do + (Single nm, m) <- quantifiedVar + return + ( (exp, [essence| transform(&morphism, &m) |]), + ComprehensionLetting (Single nm) [essence| &mat[&indexer] |] + ) + transformBody bdy [] = bdy + transformBody bdy ((orig, repl) : rest) = + let nbdy = + transformBi + ( \e -> + if e == orig + then repl + else e + ) + bdy + in transformBody nbdy rest + + theRule (Comprehension body gensOrConds) = do + let matched = catMaybes [matchIndexing exp | exp <- universeBi body] + case matched of + [] -> na "rule_Lift_Transformed_Indexing: nothing to lift" + _ -> do + replacements <- sequence (liftIndexing <$> matched) + return + ( "Horizontal rule for lift transformed indexing", + return + ( Comprehension (transformBody body (fst <$> replacements)) + $ gensOrConds + ++ (snd <$> replacements) + ) + ) + theRule _ = na "rule_Lift_Transformed_Indexing" rule_Transform_Indexing :: Rule -rule_Transform_Indexing = "transform-indexing" `namedRule` theRule where - theRule (Comprehension body gensOrConds) = do - (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of - Generator (GenInExpr pat expr) -> return (pat, expr) - _ -> na "rule_Transform_Indexing" - (morphism, matexp) <- match opTransform expr - (mat, indexer) <- match opIndexing matexp - ty <- typeOf mat - inn <- morphing =<< typeOf morphism - if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn - then do - return - ( "Horizontal rule for transform indexing" - , do - (Single mName, m) <- quantifiedVar - (Single iName, i) <- quantifiedVar - return (Comprehension body $ - gocBefore - ++ [ComprehensionLetting (Single iName) [essence| transform(&morphism, &indexer) |]] - ++ [ComprehensionLetting (Single mName) [essence| &mat[&i] |]] - - ++ [Generator (GenInExpr pat [essence| transform(&morphism, &m) |])] - ++ gocAfter) - ) - else na "rule_Transform_Indexing" - theRule _ = na "rule_Transform_Indexing" - - -rule_Transform_Unifying :: Rule -rule_Transform_Unifying = "transform-unifying" `namedRule` theRule where - theRule [essence| transform(&morphism, &i) |] = do - inner <- morphing =<< typeOf morphism - typeI <- typeOf i - if let ?typeCheckerMode = StronglyTyped in typesUnify [inner, typeI] - then return ( "Horizontal rule for transform unifying" - , return [essence| image(&morphism, &i) |] +rule_Transform_Indexing = "transform-indexing" `namedRule` theRule + where + theRule (Comprehension body gensOrConds) = do + (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of + Generator (GenInExpr pat expr) -> return (pat, expr) + _ -> na "rule_Transform_Indexing" + (morphism, matexp) <- match opTransform expr + (mat, indexer) <- match opIndexing matexp + ty <- typeOf mat + inn <- morphing =<< typeOf morphism + if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn + then do + return + ( "Horizontal rule for transform indexing", + do + (Single mName, m) <- quantifiedVar + (Single iName, i) <- quantifiedVar + return + ( Comprehension body + $ gocBefore + ++ [ComprehensionLetting (Single iName) [essence| transform(&morphism, &indexer) |]] + ++ [ComprehensionLetting (Single mName) [essence| &mat[&i] |]] + ++ [Generator (GenInExpr pat [essence| transform(&morphism, &m) |])] + ++ gocAfter ) - else if let ?typeCheckerMode = StronglyTyped in typeI `containsType` inner - then na "rule_Transform_Unifying" - else return ( "Horizontal rule for transform shortcut" - , do - return [essence| &i |] - ) - theRule _ = na "rule_Transform_Unifying" + ) + else na "rule_Transform_Indexing" + theRule _ = na "rule_Transform_Indexing" +rule_Transform_Unifying :: Rule +rule_Transform_Unifying = "transform-unifying" `namedRule` theRule + where + theRule [essence| transform(&morphism, &i) |] = do + inner <- morphing =<< typeOf morphism + typeI <- typeOf i + if let ?typeCheckerMode = StronglyTyped in typesUnify [inner, typeI] + then + return + ( "Horizontal rule for transform unifying", + return [essence| image(&morphism, &i) |] + ) + else + if let ?typeCheckerMode = StronglyTyped in typeI `containsType` inner + then na "rule_Transform_Unifying" + else + return + ( "Horizontal rule for transform shortcut", + return i + ) + theRule _ = na "rule_Transform_Unifying" rule_Transform_Sequence_Literal :: Rule -rule_Transform_Sequence_Literal = "transform-sequence-literal" `namedRule` theRule where - theRule p = do - _ <- match opTransform p - let (x, rx) = matchManyTransforms p - (_, as) <- match sequenceLiteral x - return ( "Horizontal rule for transform sequence literal" - , return $ AbstractLiteral $ AbsLitSequence $ rx <$> as - ) +rule_Transform_Sequence_Literal = "transform-sequence-literal" `namedRule` theRule + where + theRule p = do + _ <- match opTransform p + let (x, rx) = matchManyTransforms p + TypeSequence {} <- typeOf x + (_, as) <- match sequenceLiteral x + return + ( "Horizontal rule for transform sequence literal", + return $ AbstractLiteral $ AbsLitSequence $ rx <$> as + ) rule_Transform_Variant_Literal :: Rule -rule_Transform_Variant_Literal = "transform-variant-literal" `namedRule` theRule where - theRule p = do - _ <- match opTransform p - let (x, rx) = matchManyTransforms p - case x of - AbstractLiteral (AbsLitVariant d n a) -> - return ( "Horizontal rule for transform variant literal" - , return $ AbstractLiteral $ AbsLitVariant d n $ rx a - ) - _ -> na "rule_Transform_Variant_Literal" - +rule_Transform_Variant_Literal = "transform-variant-literal" `namedRule` theRule + where + theRule p = do + _ <- match opTransform p + let (x, rx) = matchManyTransforms p + case x of + AbstractLiteral (AbsLitVariant d n a) -> + return + ( "Horizontal rule for transform variant literal", + return $ AbstractLiteral $ AbsLitVariant d n $ rx a + ) + _ -> na "rule_Transform_Variant_Literal" -atLeastOneTransform :: MonadFailDoc m => (Expression, Expression) -> m () -atLeastOneTransform (l,r) = do +atLeastOneTransform :: (MonadFailDoc m) => (Expression, Expression) -> m () +atLeastOneTransform (l, r) = do case (match opTransform l, match opTransform r) of (Nothing, Nothing) -> na "no transforms on either side" - _ -> return () + _ -> return () -matchManyTransforms :: Expression - -> (Expression, Expression -> Expression) +matchManyTransforms :: + Expression -> + (Expression, Expression -> Expression) matchManyTransforms exp = case match opTransform exp of Nothing -> (exp, id) Just (morphism, so) -> let (nexp, ntrans) = matchManyTransforms so - in ( nexp - , \x -> let nx = ntrans x in [essence| transform(&morphism, &nx) |]) + in ( nexp, + \x -> let nx = ntrans x in [essence| transform(&morphism, &nx) |] + ) rule_Transform_Variant_Eq :: Rule -rule_Transform_Variant_Eq = "transform-variant-eq" `namedRule` theRule where - theRule p = do - (l,r) <- match opEq p - atLeastOneTransform (l,r) - let (x, rx) = matchManyTransforms l - let (y, ry) = matchManyTransforms r - TypeVariant{} <- typeOf x - TypeVariant{} <- typeOf y - (xWhich:xs) <- downX1 x - (yWhich:ys) <- downX1 y - return ( "Vertical rule for right transformed variant equality" - , return $ make opAnd $ fromList - [ [essence| &xWhich = &yWhich |] - , onTagged (make opEq) xWhich (rx <$> xs) (ry<$> ys) - ] - ) - +rule_Transform_Variant_Eq = "transform-variant-eq" `namedRule` theRule + where + theRule p = do + (l, r) <- match opEq p + atLeastOneTransform (l, r) + let (x, rx) = matchManyTransforms l + let (y, ry) = matchManyTransforms r + TypeVariant {} <- typeOf x + TypeVariant {} <- typeOf y + (xWhich : xs) <- downX1 x + (yWhich : ys) <- downX1 y + return + ( "Vertical rule for right transformed variant equality", + return + $ make opAnd + $ fromList + [ [essence| &xWhich = &yWhich |], + onTagged (make opEq) xWhich (rx <$> xs) (ry <$> ys) + ] + ) rule_Transform_Variant_Neq :: Rule -rule_Transform_Variant_Neq = "transform-variant-neq" `namedRule` theRule where - theRule p = do - (l,r) <- match opNeq p - atLeastOneTransform (l,r) - let (x, rx) = matchManyTransforms l - let (y, ry) = matchManyTransforms r - TypeVariant{} <- typeOf x - TypeVariant{} <- typeOf y - (xWhich:xs) <- downX1 x - (yWhich:ys) <- downX1 y - return ( "Vertical rule for right transformed variant nequality" - , return $ make opOr $ fromList - [ [essence| &xWhich != &yWhich |] - , make opAnd $ fromList - [ [essence| &xWhich = &yWhich |] - , onTagged (make opNeq) xWhich (rx <$> xs) (ry<$> ys) - ] - ] - ) - +rule_Transform_Variant_Neq = "transform-variant-neq" `namedRule` theRule + where + theRule p = do + (l, r) <- match opNeq p + atLeastOneTransform (l, r) + let (x, rx) = matchManyTransforms l + let (y, ry) = matchManyTransforms r + TypeVariant {} <- typeOf x + TypeVariant {} <- typeOf y + (xWhich : xs) <- downX1 x + (yWhich : ys) <- downX1 y + return + ( "Vertical rule for right transformed variant nequality", + return + $ make opOr + $ fromList + [ [essence| &xWhich != &yWhich |], + make opAnd + $ fromList + [ [essence| &xWhich = &yWhich |], + onTagged (make opNeq) xWhich (rx <$> xs) (ry <$> ys) + ] + ] + ) rule_Transform_Variant_Lt :: Rule -rule_Transform_Variant_Lt = "transform-variant-lt" `namedRule` theRule where - theRule p = do - (l,r) <- match opLt p - atLeastOneTransform (l,r) - let (x, rx) = matchManyTransforms l - let (y, ry) = matchManyTransforms r - TypeVariant{} <- typeOf x - TypeVariant{} <- typeOf y - (xWhich:xs) <- downX1 x - (yWhich:ys) <- downX1 y - return ( "Vertical rule for right transformed variant less than" - , return $ make opOr $ fromList - [ [essence| &xWhich < &yWhich |] - , make opAnd $ fromList - [ [essence| &xWhich = &yWhich |] - , onTagged (make opLt) xWhich (rx <$> xs) (ry<$> ys) - ] - ] - ) +rule_Transform_Variant_Lt = "transform-variant-lt" `namedRule` theRule + where + theRule p = do + (l, r) <- match opLt p + atLeastOneTransform (l, r) + let (x, rx) = matchManyTransforms l + let (y, ry) = matchManyTransforms r + TypeVariant {} <- typeOf x + TypeVariant {} <- typeOf y + (xWhich : xs) <- downX1 x + (yWhich : ys) <- downX1 y + return + ( "Vertical rule for right transformed variant less than", + return + $ make opOr + $ fromList + [ [essence| &xWhich < &yWhich |], + make opAnd + $ fromList + [ [essence| &xWhich = &yWhich |], + onTagged (make opLt) xWhich (rx <$> xs) (ry <$> ys) + ] + ] + ) rule_Transform_Variant_Leq :: Rule -rule_Transform_Variant_Leq = "transform-variant-leq" `namedRule` theRule where - theRule p = do - (l,r) <- match opLeq p - atLeastOneTransform (l,r) - let (x, rx) = matchManyTransforms l - let (y, ry) = matchManyTransforms r - TypeVariant{} <- typeOf x - TypeVariant{} <- typeOf y - (xWhich:xs) <- downX1 x - (yWhich:ys) <- downX1 y - return ( "Vertical rule for right transformed variant less than eq" - , return $ make opOr $ fromList - [ [essence| &xWhich < &yWhich |] - , make opAnd $ fromList - [ [essence| &xWhich = &yWhich |] - , onTagged (make opLeq) xWhich (rx <$> xs) (ry<$> ys) - ] - ] - ) +rule_Transform_Variant_Leq = "transform-variant-leq" `namedRule` theRule + where + theRule p = do + (l, r) <- match opLeq p + atLeastOneTransform (l, r) + let (x, rx) = matchManyTransforms l + let (y, ry) = matchManyTransforms r + TypeVariant {} <- typeOf x + TypeVariant {} <- typeOf y + (xWhich : xs) <- downX1 x + (yWhich : ys) <- downX1 y + return + ( "Vertical rule for right transformed variant less than eq", + return + $ make opOr + $ fromList + [ [essence| &xWhich < &yWhich |], + make opAnd + $ fromList + [ [essence| &xWhich = &yWhich |], + onTagged (make opLeq) xWhich (rx <$> xs) (ry <$> ys) + ] + ] + ) rule_Transformed_Variant_Index :: Rule -rule_Transformed_Variant_Index = "transformed-variant-index" `namedRule` theRule where +rule_Transformed_Variant_Index = "transformed-variant-index" `namedRule` theRule + where theRule p = do - (l,arg) <- match opIndexing p - atLeastOneTransform (l,l) - let (x, rx) = matchManyTransforms l - TypeVariant ds <- typeOf x - (xWhich:xs) <- downX1 x - name <- nameOut arg - argInt <- - case elemIndex name (map fst ds) of - Nothing -> failDoc "Variant indexing, not a member of the type." - Just argInt -> return argInt - return - ( "Variant indexing on:" <+> pretty p - , return $ WithLocals - (rx (atNote "Variant indexing" xs argInt)) - (DefinednessConstraints - [ [essence| &xWhich = &argInt2 |] + (l, arg) <- match opIndexing p + atLeastOneTransform (l, l) + let (x, rx) = matchManyTransforms l + TypeVariant ds <- typeOf x + (xWhich : xs) <- downX1 x + name <- nameOut arg + argInt <- + case elemIndex name (map fst ds) of + Nothing -> failDoc "Variant indexing, not a member of the type." + Just argInt -> return argInt + return + ( "Variant indexing on:" <+> pretty p, + return + $ WithLocals + (rx (atNote "Variant indexing" xs argInt)) + ( DefinednessConstraints + [ [essence| &xWhich = &argInt2 |] | let argInt2 = fromInt (fromIntegral (argInt + 1)) - ]) - ) - + ] + ) + ) rule_Transformed_Variant_Active :: Rule -rule_Transformed_Variant_Active = "transformed-variant-active" `namedRule` theRule where +rule_Transformed_Variant_Active = "transformed-variant-active" `namedRule` theRule + where theRule p = do - (l,name) <- match opActive p - atLeastOneTransform (l,l) - let (x, _) = matchManyTransforms l - TypeVariant ds <- typeOf x - (xWhich:_) <- downX1 x - argInt <- case elemIndex name (map fst ds) of - Nothing -> failDoc "Variant indexing, not a member of the type." - Just argInt -> return $ fromInt $ fromIntegral $ argInt + 1 - return - ( "Variant active on:" <+> pretty p - , return $ [essence| &xWhich = &argInt |] - ) - - - + (l, name) <- match opActive p + atLeastOneTransform (l, l) + let (x, _) = matchManyTransforms l + TypeVariant ds <- typeOf x + (xWhich : _) <- downX1 x + argInt <- case elemIndex name (map fst ds) of + Nothing -> failDoc "Variant indexing, not a member of the type." + Just argInt -> return $ fromInt $ fromIntegral $ argInt + 1 + return + ( "Variant active on:" <+> pretty p, + return $ [essence| &xWhich = &argInt |] + ) diff --git a/src/Conjure/UI/TranslateParameter.hs b/src/Conjure/UI/TranslateParameter.hs index 6c5e23d13..e32e3f30f 100644 --- a/src/Conjure/UI/TranslateParameter.hs +++ b/src/Conjure/UI/TranslateParameter.hs @@ -30,7 +30,7 @@ translateParameter :: m Model -- eprime param translateParameter graphSolver eprimeModel0 essenceParam0 = do - logDebug $ "[eprimeModel 0]" <+-> pretty essenceParam0 + logDebug $ "[eprimeModel 0]" <+-> pretty eprimeModel0 logDebug $ "[essenceParam 0]" <+-> pretty essenceParam0 (eprimeModel, essenceParam1) <- removeEnumsFromParam eprimeModel0 essenceParam0 logDebug $ "[eprimeModel 1]" <+-> pretty eprimeModel