| -- | |
| -- Module : Minigent.TC.Simplify |
| -- Copyright : (c) Data61 2018-2019 |
| -- Commonwealth Science and Research Organisation (CSIRO) |
| -- ABN 41 687 119 230 |
| -- License : BSD3 |
| -- |
| -- The simplify phase of the solver. |
| -- |
| -- May be used qualified or unqualified. |
| module Minigent.TC.Simplify where |
| |
| import Minigent.Syntax |
| import Minigent.Syntax.Utils |
| import qualified Minigent.Syntax.Utils.Row as Row |
| import qualified Minigent.Syntax.Utils.Rewrite as Rewrite |
| |
| import Control.Monad |
| import Data.Maybe (mapMaybe) |
| import qualified Data.Set as S |
| import qualified Data.Map as M |
| import Data.Foldable (toList) |
| |
| import Minigent.Syntax.PrettyPrint |
| import Debug.Trace |
| |
| -- | Rewrite a set of constraints, removing all trivially satisfiable constraints |
| -- and breaking down large constraints into smaller ones. |
| simplify :: [Constraint] -> Rewrite.Rewrite [Constraint] |
| simplify axs = Rewrite.pickOne $ \c -> -- trace ("About to simpliy:\n" ++ debugPrettyConstraints [c]) $ |
| case c of |
| c | c `elem` axs -> Just [] |
| Sat -> Just [] |
| c1 :&: c2 -> Just [c1,c2] |
| Drop (PrimType _) -> Just [] |
| Share (PrimType _) -> Just [] |
| Escape (PrimType _) -> Just [] |
| Drop (Function _ _) -> Just [] |
| Share (Function _ _) -> Just [] |
| Escape (Function _ _) -> Just [] |
| Drop (TypeVarBang _) -> Just [] |
| Share (TypeVarBang _) -> Just [] |
| Drop (RecParBang _ _) -> Just [] |
| Share (RecParBang _ _) -> Just [] |
| Share (Variant es) -> guard (rowVar es == Nothing) |
| >> Just (map Share (Row.untakenTypes es)) |
| Drop (Variant es) -> guard (rowVar es == Nothing) |
| >> Just (map Drop (Row.untakenTypes es)) |
| Escape (Variant es) -> guard (rowVar es == Nothing) |
| >> Just (map Escape (Row.untakenTypes es)) |
| Share (AbsType n s ts) -> guard (s == ReadOnly || s == Unboxed) |
| >> Just (map Share ts) |
| Drop (AbsType n s ts) -> guard (s == ReadOnly || s == Unboxed) |
| >> Just (map Drop ts) |
| Escape (AbsType n s ts) -> guard (s == Writable || s == Unboxed) |
| >> Just (map Escape ts) |
| Share (Record n es s) -> guard (s == ReadOnly || s == Unboxed) |
| >> guard (rowVar es == Nothing) |
| >> Just (map Share (Row.untakenTypes es)) |
| Drop (Record n es s) -> guard (s == ReadOnly || s == Unboxed) |
| >> guard (rowVar es == Nothing) |
| >> Just (map Drop (Row.untakenTypes es)) |
| Escape (Record n es s) -> guard (s == Writable || s == Unboxed) |
| >> guard (rowVar es == Nothing) |
| >> Just (map Escape (Row.untakenTypes es)) |
| Exhausted (Variant es) -> guard (null (Row.untakenTypes es) && rowVar es == Nothing) |
| >> Just [] |
| i :<=: PrimType t -> guard (fits i t) >> Just [] |
| |
| Function t1 t2 :< Function r1 r2 -> Just [r1 :< t1, t2 :< r2] |
| Function t1 t2 :=: Function r1 r2 -> Just [r1 :=: t1, t2 :=: r2] |
| |
| Variant r1 :< Variant r2 -> |
| if Row.null r1 && Row.null r2 then Just [] |
| else if Row.null r1 && null (Row.entries r2) |
| || Row.null r2 && null (Row.entries r1) |
| then Just [Variant r1 :=: Variant r2] |
| else do |
| let commons = Row.common r1 r2 |
| (ls, rs) = unzip commons |
| guard (not (null commons)) |
| guard (untakenLabels ls `S.isSubsetOf` untakenLabels rs) |
| let (r1',r2') = Row.withoutCommon r1 r2 |
| cs = map (\(Entry _ t _, Entry _ t' _) -> t :< t') commons |
| c = Variant r1' :< Variant r2' |
| Just (c:cs) |
| |
| Record n1 r1 s1 :< Record n2 r2 s2 -> |
| if Row.null r1 && Row.null r2 && s1 == s2 && n1 == n2 then Just [] |
| else if Row.null r1 && null (Row.entries r2) |
| || Row.null r2 && null (Row.entries r1) |
| then Just [Record n1 r1 s1 :=: Record n2 r2 s2] |
| else do |
| let commons = Row.common r1 r2 |
| (ls, rs) = unzip commons |
| guard (not (null commons)) |
| guard (untakenLabels rs `S.isSubsetOf` untakenLabels ls) |
| let (r1',r2') = Row.withoutCommon r1 r2 |
| cs = map (\(Entry _ t _, Entry _ t' _) -> t :< t') commons |
| ds = map Drop (Row.typesFor (untakenLabels ls S.\\ untakenLabels rs) r1) |
| c = Record n1 r1' s1 :< Record n2 r2' s2 |
| Just (c:cs ++ ds) |
| |
| {- |
| - Recursive Parameters: |
| - If we are reasoning about two recursive parameters, check if their context references |
| - are equal. We *do not* unroll here, and if we arrive at the same position where the contexts |
| - are both `Nothing', then the RecPars are truly equal. |
| - |
| - N.B. recursive parameters need only be *alpha* equivalent, hence we do not check if the names are equal |
| -} |
| RecPar n (Just ctxt) :< RecPar n' (Just ctxt') -> Just [(ctxt M.! n) :< (ctxt M.! n')] |
| RecPar n (Just ctxt) :=: RecPar n' (Just ctxt') -> Just [(ctxt M.! n) :=: (ctxt M.! n')] |
| RecParBang n (Just ctxt) :< RecParBang n' (Just ctxt') -> Just [(ctxt M.! n) :< (ctxt M.! n')] |
| RecParBang n (Just ctxt) :=: RecParBang n' (Just ctxt') -> Just [(ctxt M.! n) :=: (ctxt M.! n')] |
| |
| RecPar n Nothing :< RecPar n' Nothing -> Just [] |
| RecPar n Nothing :=: RecPar n' Nothing -> Just [] |
| RecParBang n Nothing :< RecParBang n' Nothing -> Just [] |
| RecParBang n Nothing :=: RecParBang n' Nothing -> Just [] |
| |
| |
| -- We need this here as otherwise it triggers the cases below |
| RecParBang n ctxt :< RecPar n' ctxt' -> Nothing |
| RecPar n ctxt :< RecParBang n' ctxt' -> Nothing |
| RecParBang n ctxt :=: RecPar n' ctxt' -> Nothing |
| RecPar n ctxt :=: RecParBang n' ctxt' -> Nothing |
| |
| {- |
| - otherwise: |
| - If we are reasoning about a recursive parameter and a type, unroll the parameter |
| - and reason about the type and the unrolled parameter |
| -} |
| RecPar n ctxt :< t@Record{} -> Just [unroll n ctxt :< t] |
| t@Record{} :< RecPar n ctxt -> Just [t :< unroll n ctxt] |
| RecPar n ctxt :=: t@Record{} -> Just [unroll n ctxt :=: t] |
| t@Record{} :=: RecPar n ctxt -> Just [t :=: unroll n ctxt] |
| |
| RecParBang n ctxt :< t@Record{} -> Just [Bang (unroll n ctxt) :< t] |
| t@Record{} :< RecParBang n ctxt -> Just [t :< Bang (unroll n ctxt)] |
| RecParBang n ctxt :=: t@Record{} -> Just [Bang (unroll n ctxt) :=: t] |
| t@Record{} :=: RecParBang n ctxt -> Just [t :=: Bang (unroll n ctxt)] |
| |
| t :< t' -> guard (unorderedType t || unorderedType t') >> Just [t :=: t'] |
| |
| AbsType n s ts :=: AbsType n' s' ts' -> guard (n == n' && s == s') >> Just (zipWith (:=:) ts ts') |
| |
| Variant r1 :=: Variant r2 -> |
| if Row.null r1 && Row.null r2 then Just [] |
| else if Row.justVar r1 && Row.justVar r2 && r1 == r2 |
| then Just [Solved (Variant r1)] |
| else do |
| let commons = Row.common r1 r2 |
| (ls, rs) = unzip commons |
| guard (not (null commons)) |
| guard (untakenLabels ls == untakenLabels rs) |
| let (r1',r2') = Row.withoutCommon r1 r2 |
| cs = map (\(Entry _ t _, Entry _ t' _) -> t :=: t') commons |
| c = Variant r1' :=: Variant r2' |
| Just (c:cs) |
| |
| Record rp1 r1 s1 :=: Record rp2 r2 s2 -> |
| if Row.null r1 && Row.null r2 && s1 == s2 && sameRecursive rp1 rp2 then Just [] |
| else if Row.justVar r1 && Row.justVar r2 && s1 == s2 && r1 == r2 && sameRecursive rp1 rp2 |
| then Just [Solved (Record rp1 r1 s1)] |
| else do |
| let commons = Row.common r1 r2 |
| (ls, rs) = unzip commons |
| guard (not (null commons)) |
| guard (untakenLabels rs == untakenLabels ls) |
| let (r1',r2') = Row.withoutCommon r1 r2 |
| cs = map (\(Entry _ t _, Entry _ t' _) -> t :=: t') commons |
| c = Record rp1 r1' s1 :=: Record rp2 r2' s2 |
| Just (c:cs) |
| |
| t :=: t' -> guard (t == t') >> if typeUVs t == [] then Just [] |
| else Just [Solved t] |
| Solved t -> guard (typeUVs t == []) >> Just [] |
| |
| -- If an unboxed record has no recursive parameter, sat |
| UnboxedNoRecurse None Unboxed -> Just [] |
| -- If a boxed record, sat |
| UnboxedNoRecurse _ c | (c == ReadOnly || c == Writable) -> Just [] |
| |
| _ -> Nothing |
| |
| |
| |
| where |
| |
| untakenLabels :: [Entry] -> S.Set FieldName |
| untakenLabels = S.fromList . mapMaybe (\(Entry l _ t) -> guard (not t) >> pure l) |
