From 3dad54fb1eeefa35a7c4a37bdb619850a6eb5b0d Mon Sep 17 00:00:00 2001 From: amiddelk Date: Thu, 1 Nov 2007 10:31:28 +0000 Subject: [PATCH] Thanks to a change by Atze, forward and backward reasoning (needed for an example in the left-corner paper of Atze and Doaitse) now seems to work (although slow :( ) --- EHC/src/chr-experiment/Main.hs | 46 ++++++++++++++++++++----- EHC/src/ehc/CHR/Solve.chs | 25 ++++++++++---- EHC/src/ehc/Pred/CHR.chs | 14 ++++---- EHC/src/ehc/Pred/CommonCHR.chs | 3 ++ EHC/src/ehc/Pred/EvidenceToCore.chs | 2 +- EHC/src/ehc/Pred/Heuristics.chs | 2 ++ EHC/src/ehc/Pred/ToCHR.chs | 53 +++++++++++++++-------------- EHC/test/regress/16/gadt4.eh | 27 +++++++++++++++ 8 files changed, 123 insertions(+), 49 deletions(-) create mode 100644 EHC/test/regress/16/gadt4.eh diff --git a/EHC/src/chr-experiment/Main.hs b/EHC/src/chr-experiment/Main.hs index e43916013..073855300 100644 --- a/EHC/src/chr-experiment/Main.hs +++ b/EHC/src/chr-experiment/Main.hs @@ -12,25 +12,38 @@ import EH16.Pred.RedGraph import EH16.Base.Common import EH16.Pred.Heuristics import EH16.Pred.Evidence +import EH16.VarMp import EH.Util.Pretty -- list of constraints input :: [Constraint CHRPredOcc RedHowAnnotation] input - = [ eq a tyA tyB + = {-[ eq a tyA tyB , eq a tyB tyC , eq a tyK1 ty1 , eq p ty2 tyK1 + ]-} + {- + [ eq a s1 tyC (mkProdApp [tyA, tyInt]) + , eq a s2 tyC (mkProdApp [tyB, tyInt]) + , eq p s3 tyA tyB + ] + -} + [ eq a s0 tyA tyB + , eq a s0 tyB tyC + -- , eq a s0 tyB tyA + , eq a s0 tyC tyB +-- , eq p s0 tyInt tyInt ] where - a :: Pred -> Constraint CHRPredOcc RedHowAnnotation - a pr = Assume (mkCHRPredOcc pr initPredScope) + a :: PredScope -> Pred -> Constraint CHRPredOcc RedHowAnnotation + a s pr = Assume (mkCHRPredOcc pr s) - p :: Pred -> Constraint CHRPredOcc RedHowAnnotation - p pr = Prove (mkCHRPredOcc pr initPredScope) + p :: PredScope -> Pred -> Constraint CHRPredOcc RedHowAnnotation + p s pr = Prove (mkCHRPredOcc pr s) - eq f t1 t2 = f (Pred_Eq t1 t2) + eq f s t1 t2 = f s (Pred_Eq t1 t2) [tyA, tyB, tyC, tyK1, tyK2, tyInt] = map (Ty_Con . HNm) ["A", "B", "C", "K1", "K2", "Int"] tyCI = Ty_Impls (Impls_Tail u1 []) `mk1Arrow` tyC @@ -39,11 +52,17 @@ input ty2 = mkProdApp [tyK2 `mk1Arrow` tyCI, tyInt] [u1] = drop 7 (mkNewLevUIDL 8 uidStart) + + s0 = PredScope_Lev [] + s1 = PredScope_Lev [0] + s2 = PredScope_Lev [0,0] + s3 = PredScope_Lev [0,0,0] -- CHR rules store :: ScopedPredStore -store +store = initScopedPredStore +{- = chrStoreFromElems $ [ -- symmetry (prove) [Prove eqT1T2] ==> [Prove eqT2T1, Reduction eqT1T2 RedHow_ByEqSymmetry [eqT2T1]] @@ -59,7 +78,7 @@ store |> [IsCtxNilReduction ty2 ty3] , -- congruence (results in new proof obligations, discarding the old by the congruence reduction) [Prove eqT1T2] ==> [Prove psPred, Reduction eqT1T2 RedHow_ByEqCongr [psPred]] - |> [AreOblsByCongruence ty1 ty2 ps] + |> [EqsByCongruence ty1 ty2 ps] , -- unpack predseq (cons) [Prove psCons] ==> [Prove psHead, Prove psPred, Reduction psCons RedHow_ByPredSeqUnpack [psHead, psPred]] , -- unpack predsec (nil) @@ -81,13 +100,22 @@ store ps = PredSeq_Var u5 pr = Pred_Var u6 [u1,u2,u3,u4,u5,u6] = mkNewLevUIDL 6 uidStart +-} env :: FIIn env = emptyFI { fiUniq = last $ mkNewLevUIDL 7 uidStart } producedCnstrs :: [Constraint CHRPredOcc RedHowAnnotation] -producedCnstrs = chrSolve env store input +tr :: SolveTrace CHRPredOcc RedHowAnnotation Guard VarMp +(producedCnstrs,_,tr) = chrSolve' env store input + +steps :: PP_Doc +steps = vlist tr + +dump :: IO () +dump = do writeFile "output.txt" (show steps) + putStrLn "dumped to output.txt" assumeMap :: CHRPredOccCnstrMp assumeMap = cnstrMpFromList [ (c, RedHow_Assumption (VarUIDHs_UID uidNull) (PredScope_Var uidNull)) | c <- producedCnstrs ] diff --git a/EHC/src/ehc/CHR/Solve.chs b/EHC/src/ehc/CHR/Solve.chs index 5bcb035ab..78adc3c56 100644 --- a/EHC/src/ehc/CHR/Solve.chs +++ b/EHC/src/ehc/CHR/Solve.chs @@ -137,7 +137,8 @@ ppCHRStore' = ppCurlysCommasBlock . map (\(k,v) -> ppTrieKey k >-< indent 2 (":" %%[9 type WorkKey = CHRKey -type WorkUsedInMap = Map.Map CHRKey (Set.Set UsedByKey) +-- type WorkUsedInMap = Map.Map CHRKey (Set.Set UsedByKey) +type WorkUsedInMap = Map.Map (Set.Set CHRKey) (Set.Set UsedByKey) data Work p i = Work @@ -298,12 +299,18 @@ chrSolve'' env chrStore cnstrs prevState (_:_) -> expandMatch st matches where expandMatch st@(SolveState {stWorkList = wl}) - (((schr@(StoredCHR {storedIdent = chrId, storedChr = chr@(CHR {chrBody = b, chrSimpSz = simpSz})}),(keys,works)),subst) : tlMatch) + ( ( ( schr@(StoredCHR {storedIdent = chrId, storedChr = chr@(CHR {chrBody = b, chrSimpSz = simpSz})}) + , (keys,works) + ) + , subst + ) : tlMatch + ) = expandMatch (st') $ filter (\(r@(_,(ks,_)),_) -> not (any (`elem` keysSimp) ks || isUsedByPropPart (wlUsedIn wl') r)) $ tlMatch where (keysSimp,keysProp) = splitAt simpSz keys - usedIn = Map.fromListWith Set.union $ zip keysProp (repeat $ Set.singleton chrId) + usedIn = Map.singleton (Set.fromList keysProp) (Set.singleton chrId) + -- usedIn = Map.fromListWith Set.union $ zip keysProp (repeat $ Set.singleton chrId) (bTodo,bDone) = splitDone $ map (chrAppSubst subst) b wl' = wlInsert bTodo $ wlDeleteByKey keysSimp @@ -322,8 +329,8 @@ chrSolve'' env chrStore cnstrs prevState >-< "workkeys" >#< ppBracketsCommas (map ppTrieKey keys) >-< "worktrie" >#< wlTrie wl >-< "schr" >#< schr - >-< "usedin" >#< (ppBracketsCommasV $ map (\(k,s) -> ppTrieKey k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl) - >-< "usedin'" >#< (ppBracketsCommasV $ map (\(k,s) -> ppTrieKey k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl') + >-< "usedin" -- >#< (ppBracketsCommasV $ map (\(k,s) -> ppTrieKey k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl) + >-< "usedin'" -- >#< (ppBracketsCommasV $ map (\(k,s) -> ppTrieKey k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl') %%][100 %%]] expandMatch st _ @@ -380,12 +387,16 @@ chrSolve'' env chrStore cnstrs prevState cmb (Just s) next = fmap (`chrAppSubst` s) $ next s cmb _ _ = Nothing isUsedByPropPart wlUsedIn (chr,(keys,_)) - = all fnd $ drop (storedSimpSz chr) keys - where fnd k = maybe False (storedIdent chr `Set.member`) $ Map.lookup k wlUsedIn + = fnd $ drop (storedSimpSz chr) keys + where fnd k = maybe False (storedIdent chr `Set.member`) $ Map.lookup (Set.fromList k) wlUsedIn initState st = st { stWorkList = wlInsert wlnew $ stWorkList st, stDoneCnstrSet = Set.unions [Set.fromList done, stDoneCnstrSet st] } where (wlnew,done) = splitDone cnstrs splitDone = partition (\x -> cnstrRequiresSolve x) %%] + isUsedByPropPart wlUsedIn (chr,(keys,_)) + = all fnd $ drop (storedSimpSz chr) keys + where fnd k = maybe False (storedIdent chr `Set.member`) $ Map.lookup k wlUsedIn + -> iter {- $ trp "YY" ("chr" >#< schr >-< ppwork) $ -} st' r4 = foldr first Nothing $ r3 -- r5 = foldr first Nothing r4 diff --git a/EHC/src/ehc/Pred/CHR.chs b/EHC/src/ehc/Pred/CHR.chs index cd2c0731f..8e2d0c76a 100644 --- a/EHC/src/ehc/Pred/CHR.chs +++ b/EHC/src/ehc/Pred/CHR.chs @@ -104,7 +104,7 @@ instance CHRSubstitutable Guard TyVarId VarMp where %%]] %%[[16 chrFtv (IsCtxNilReduction t1 t2) = Set.unions [ftvSet t1, ftvSet t2] - chrFtv (AreOblsByCongruence t1 t2 ps) = Set.unions [ftvSet t1, ftvSet t2, ftvSet ps] + chrFtv (EqsByCongruence t1 t2 ps) = Set.unions [ftvSet t1, ftvSet t2, ftvSet ps] %%]] chrAppSubst s (HasStrictCommonScope p1 p2 p3) = HasStrictCommonScope (s |=> p1) (s |=> p2) (s |=> p3) @@ -117,7 +117,7 @@ instance CHRSubstitutable Guard TyVarId VarMp where %%]] %%[[16 chrAppSubst s (IsCtxNilReduction t1 t2) = IsCtxNilReduction (s |=> t1) (s |=> t2) - chrAppSubst s (AreOblsByCongruence t1 t2 ps) = AreOblsByCongruence (s |=> t1) (s |=> t2) (s |=> ps) + chrAppSubst s (EqsByCongruence t1 t2 ps) = EqsByCongruence (s |=> t1) (s |=> t2) (s |=> ps) chrAppSubst s (UnequalTy t1 t2) = UnequalTy (s |=> t1) (s |=> t2) %%]] %%] @@ -239,7 +239,7 @@ data Guard %%]] %%[[16 | IsCtxNilReduction Ty Ty - | AreOblsByCongruence Ty Ty PredSeq + | EqsByCongruence Ty Ty PredSeq | UnequalTy Ty Ty %%]] %%] @@ -256,7 +256,7 @@ ppGuard (NonEmptyRowLacksLabel r o t l ) = ppParens (t >#< "==" >#< ppParens %%]] %%[[16 ppGuard (IsCtxNilReduction t1 t2 ) = t1 >#< "~>" >#< t2 -ppGuard (AreOblsByCongruence t1 t2 ps ) = t1 >#< "~~" >#< t2 >#< "~>" >#< ps +ppGuard (EqsByCongruence t1 t2 ps ) = t1 >#< "~~" >#< t2 >#< "~>" >#< ps ppGuard (UnequalTy t1 t2 ) = t1 >#< "/=" >#< t2 %%]] %%] @@ -337,7 +337,7 @@ instance CHRCheckable FIIn Guard VarMp where varMp = foVarMp fo tRes = varMp |=> foTy fo -- hum, I would assume that this substitution is already applied by fitsIn...?! - chk (AreOblsByCongruence t1 t2 obls) + chk (EqsByCongruence t1 t2 obls) = if foHasErrs fo || null preds then Nothing else return varMp @@ -392,7 +392,7 @@ instance ForceEval Guard where forceEval x@(EqualScope sc1 sc2 ) | forceEval sc1 `seq` forceEval sc2 `seq` True = x forceEval x@(NonEmptyRowLacksLabel r o t l ) | forceEval r `seq` forceEval o `seq` forceEval t `seq` forceEval l `seq` True = x forceEval x@(IsCtxNilReduction t1 t2 ) | forceEval t1 `seq` forceEval t2 `seq` True = x - forceEval x@(AreOblsByCongruence t1 t2 ps ) | forceEval t1 `seq` forceEval t2 `seq` forceEval ps `seq` True = x + forceEval x@(EqsByCongruence t1 t2 ps ) | forceEval t1 `seq` forceEval t2 `seq` forceEval ps `seq` True = x %%[[101 fevCount (HasStrictCommonScope sc1 sc2 sc3) = cm1 "HasStrictCommonScope" `cmUnion` fevCount sc1 `cmUnion` fevCount sc2 `cmUnion` fevCount sc3 fevCount (IsStrictParentScope sc1 sc2 sc3) = cm1 "IsStrictParentScope" `cmUnion` fevCount sc1 `cmUnion` fevCount sc2 `cmUnion` fevCount sc3 @@ -401,7 +401,7 @@ instance ForceEval Guard where fevCount (EqualScope sc1 sc2 ) = cm1 "EqualScope" `cmUnion` fevCount sc1 `cmUnion` fevCount sc2 fevCount (NonEmptyRowLacksLabel r o t l ) = cm1 "NonEmptyRowLacksLabel" `cmUnion` fevCount r `cmUnion` fevCount o `cmUnion` fevCount t `cmUnion` fevCount l fevCount (IsCtxNilReduction t1 t2 ) = cm1 "IsCtxNilReduction" `cmUnion` fevCount t1 `cmUnion` fevCount t2 - fevCount (AreOblsByCongruence t1 t2 ps ) = cm1 "AreOblByCongruence" `cmUnion` fevCount t1 `cmUnion` fevCount t2 `cmUnion` fevCount ps + fevCount (EqsByCongruence t1 t2 ps ) = cm1 "EqsByCongruence" `cmUnion` fevCount t1 `cmUnion` fevCount t2 `cmUnion` fevCount ps %%]] %%] diff --git a/EHC/src/ehc/Pred/CommonCHR.chs b/EHC/src/ehc/Pred/CommonCHR.chs index f46b2df19..355844817 100644 --- a/EHC/src/ehc/Pred/CommonCHR.chs +++ b/EHC/src/ehc/Pred/CommonCHR.chs @@ -50,6 +50,7 @@ data RedHowAnnotation | RedHow_ByEqCongr | RedHow_ByEqTyReduction !Ty !Ty | RedHow_ByPredSeqUnpack + | RedHow_ByEqFromAssume %%]] deriving (Eq, Ord) %%] @@ -78,6 +79,7 @@ instance PP RedHowAnnotation where pp (RedHow_ByEqCongr ) = pp "eqcongr" pp (RedHow_ByEqTyReduction ty1 ty2) = "eqtyred" >#< ty1 >#< "~>" >#< ty2 pp (RedHow_ByPredSeqUnpack) = pp "unpack" + pp (RedHow_ByEqFromAssume) = pp "eqassume" %%]] %%] pp (RedHow_ByInstance s p sc) = "inst" >#< s >|< sc >#< "::" >#< p @@ -160,6 +162,7 @@ instance ForceEval RedHowAnnotation where fevCount (RedHow_ByEqCongr ) = cm1 "RedHow_ByEqCongr" fevCount (RedHow_ByEqTyReduction ty1 ty2) = cm1 "RedHow_ByEqTyReduction" `cmUnion` fevCount ty1 `cmUnion` fevCount ty2 fevCount (RedHow_ByPredSeqUnpack ) = cm1 "RedHow_ByPredSeqUnpack" + fevCount (RedHow_ByEqFromAssume ) = cm1 "RedHow_ByEqFromAssume" fevCount (RedHow_ByLabel l o sc) = cm1 "RedHow_ByLabel" `cmUnion` fevCount l `cmUnion` fevCount o `cmUnion` fevCount sc fevCount (RedHow_Lambda i sc) = cm1 "RedHow_Lambda" `cmUnion` fevCount i `cmUnion` fevCount sc %%]] diff --git a/EHC/src/ehc/Pred/EvidenceToCore.chs b/EHC/src/ehc/Pred/EvidenceToCore.chs index 1898c599d..0352ef124 100644 --- a/EHC/src/ehc/Pred/EvidenceToCore.chs +++ b/EHC/src/ehc/Pred/EvidenceToCore.chs @@ -138,7 +138,7 @@ evidMpToCore env evidMp %%]] %%[[16 ignore (_, (Evid_Proof _ red _)) - | red `elem` [RedHow_ByEqSymmetry, RedHow_ByEqTrans, RedHow_ByEqCongr, RedHow_ByPredSeqUnpack] + | red `elem` [RedHow_ByEqSymmetry, RedHow_ByEqTrans, RedHow_ByEqCongr, RedHow_ByPredSeqUnpack, RedHow_ByEqFromAssume] = True ignore (_, (Evid_Proof _ (RedHow_ByEqTyReduction _ _) _)) = True diff --git a/EHC/src/ehc/Pred/Heuristics.chs b/EHC/src/ehc/Pred/Heuristics.chs index 99a3b83d1..5a3c59c6a 100644 --- a/EHC/src/ehc/Pred/Heuristics.chs +++ b/EHC/src/ehc/Pred/Heuristics.chs @@ -270,6 +270,8 @@ anncmpEHCScoped env ann1 ann2 cmpEqReds :: RedHowAnnotation -> RedHowAnnotation -> PartialOrdering %%[[16 +cmpEqReds RedHow_ByEqFromAssume _ = P_GT +cmpEqReds _ RedHow_ByEqFromAssume = P_LT cmpEqReds (RedHow_Assumption _ _) _ = P_GT cmpEqReds _ (RedHow_Assumption _ _) = P_LT cmpEqReds RedHow_ByPredSeqUnpack _ = P_GT diff --git a/EHC/src/ehc/Pred/ToCHR.chs b/EHC/src/ehc/Pred/ToCHR.chs index 11fe7d070..9011cd958 100644 --- a/EHC/src/ehc/Pred/ToCHR.chs +++ b/EHC/src/ehc/Pred/ToCHR.chs @@ -76,7 +76,7 @@ Hence we can safely use non-unique variables. ([sc1,sc2,sc3] ,[pr1,pr2,pr3] %%[[10 - ,[ty1,ty2,ty3] + ,[ty1,ty2,ty3,ty4] ,[lab1] ,[off1] %%]] @@ -88,7 +88,7 @@ Hence we can safely use non-unique variables. = ( map PredScope_Var [u1,u2,u3] , map Pred_Var [u7,u8,u9] %%[[10 - , map mkTyVar [u10,u11,u14] + , map mkTyVar [u10,u11,u14,u15] , map Label_Var [u12] , map LabelOffset_Var [u13] %%]] @@ -100,7 +100,7 @@ Hence we can safely use non-unique variables. %%[[9 where [u1,u2,u3,u4,u5,u6,u7,u8,u9] = mkNewLevUIDL 9 uidStart %%][10 - where [u1,u2,u3,u4,u5,u6,u7,u8,u9,u10,u11,u12,u13,u14] = mkNewLevUIDL 14 uidStart + where [u1,u2,u3,u4,u5,u6,u7,u8,u9,u10,u11,u12,u13,u14,u15] = mkNewLevUIDL 15 uidStart %%]] %%] @@ -123,7 +123,7 @@ initScopedPredStore ++ [ instForall, predArrow, predSeq1, predSeq2 ] %%]] %%[[16 - ++ [ rlEqSym, rlEqTrans1, rlEqTrans2, rlEqCongr, rlCtxToNil, rlUnpackCons, rlUnpackNil ] + ++ [ rlEqScope, rlEqTrans, rlEqSym, rlEqCongr, rlUnpackCons, rlCtxToNil, rlEqSymPrv, rlEqTransPrv, rlEqCongrPrv, rlUnpackConsPrv, rlUnpackNilPrv, rlPrvByAssume ] %%]] where p1s1 = mkCHRPredOcc pr1 sc1 p1s2 = mkCHRPredOcc pr1 sc2 @@ -168,28 +168,31 @@ initScopedPredStore <==> [] %%]] %%[[16 - eqT1T2 = mkCHRPredOcc (Pred_Eq ty1 ty2) sc1 - eqT2T1 = mkCHRPredOcc (Pred_Eq ty2 ty1) sc1 - eqT2T3 = mkCHRPredOcc (Pred_Eq ty2 ty3) sc2 - eqT3T2 = mkCHRPredOcc (Pred_Eq ty3 ty2) sc2 - eqT1T3 = mkCHRPredOcc (Pred_Eq ty1 ty3) sc1 - psPred = mkCHRPredOcc (Pred_Preds pa1) sc1 - psCons = mkCHRPredOcc (Pred_Preds (PredSeq_Cons pr1 pa1)) sc1 - psNil = mkCHRPredOcc (Pred_Preds PredSeq_Nil) sc1 - psHead = mkCHRPredOcc pr1 sc1 + eqT1T2s1 = mkCHRPredOcc (Pred_Eq ty1 ty2) sc1 + eqT1T2s2 = mkCHRPredOcc (Pred_Eq ty1 ty2) sc2 + eqT2T1s1 = mkCHRPredOcc (Pred_Eq ty2 ty1) sc1 + eqT2T3s1 = mkCHRPredOcc (Pred_Eq ty2 ty3) sc1 + eqT1T3s1 = mkCHRPredOcc (Pred_Eq ty1 ty3) sc1 + eqT3T4s2 = mkCHRPredOcc (Pred_Eq ty3 ty4) sc2 + psPreds1 = mkCHRPredOcc (Pred_Preds pa1) sc1 + psConss1 = mkCHRPredOcc (Pred_Preds (PredSeq_Cons pr1 pa1)) sc1 + psNils1 = mkCHRPredOcc (Pred_Preds PredSeq_Nil) sc1 + psHeads1 = mkCHRPredOcc pr1 sc1 + + rlEqScope = [Assume eqT1T2s1, Prove eqT3T4s2] ==> [Assume eqT1T2s2] |> [IsVisibleInScope sc1 sc2] -- push equality assumption downwards + rlEqSym = [Assume eqT1T2s1] ==> [Assume eqT2T1s1] -- symmetry + rlEqTrans = [Assume eqT1T2s1, Assume eqT2T3s1] ==> [Assume eqT1T3s1] -- transitivity + rlEqCongr = [Assume eqT1T2s1] ==> [Assume psPreds1] |> [EqsByCongruence ty1 ty2 pa1] -- congruence + rlUnpackCons = [Assume psConss1] ==> [Assume psHeads1, Assume psPreds1] -- unpack a list of assumptions + + rlCtxToNil = [Prove eqT1T2s1] ==> [Prove eqT1T3s1, Reduction eqT1T2s1 (RedHow_ByEqTyReduction ty2 ty3) [eqT1T3s1]] |> [IsCtxNilReduction ty2 ty3] + rlEqSymPrv = [Prove eqT1T2s1] ==> [Prove eqT2T1s1, Reduction eqT1T2s1 RedHow_ByEqSymmetry [eqT2T1s1]] |> [UnequalTy ty1 ty2] + rlEqTransPrv = [Prove eqT1T2s1, Assume eqT2T3s1] ==> [Prove eqT1T3s1, Reduction eqT1T2s1 RedHow_ByEqTrans [eqT1T3s1, eqT2T3s1]] |> [UnequalTy ty2 ty3] + rlEqCongrPrv = [Prove eqT1T2s1] ==> [Prove psPreds1, Reduction eqT1T2s1 RedHow_ByEqCongr [psPreds1]] |> [EqsByCongruence ty1 ty2 pa1] + rlUnpackConsPrv = [Prove psConss1] ==> [Prove psHeads1, Prove psPreds1, Reduction psConss1 RedHow_ByPredSeqUnpack [psHeads1, psPreds1]] + rlUnpackNilPrv = [Prove psNils1] ==> [Reduction psNils1 RedHow_ByPredSeqUnpack []] + rlPrvByAssume = [Prove eqT1T2s1, Assume eqT1T2s1] ==> [Reduction eqT1T2s1 RedHow_ByEqFromAssume []] -- dirty hack: generated assumptions by chr are not added to the graph, so made a reduction instead - rlEqSym = [Prove eqT1T2] ==> [Prove eqT2T1, Reduction eqT1T2 RedHow_ByEqSymmetry [eqT2T1]] - |> [UnequalTy ty1 ty2] - rlEqTrans1 = [Prove eqT1T2, Assume eqT2T3] ==> [Prove eqT1T3, Reduction eqT1T2 RedHow_ByEqTrans [eqT1T3, eqT2T3]] - |> [UnequalTy ty2 ty3, IsVisibleInScope sc2 sc1] - rlEqTrans2 = [Prove eqT1T2, Assume eqT3T2] ==> [Prove eqT1T3, Reduction eqT1T2 RedHow_ByEqTrans [eqT1T3, eqT3T2]] - |> [UnequalTy ty2 ty3, IsVisibleInScope sc2 sc1] - rlEqCongr = [Prove eqT1T2] ==> [Prove psPred, Reduction eqT1T2 RedHow_ByEqCongr [psPred]] - |> [AreOblsByCongruence ty1 ty2 pa1] - rlCtxToNil = [Prove eqT1T2] ==> [Prove eqT1T3, Reduction eqT1T2 (RedHow_ByEqTyReduction ty2 ty3) [eqT1T3]] - |> [IsCtxNilReduction ty2 ty3] - rlUnpackCons = [Prove psCons] ==> [Prove psHead, Prove psPred, Reduction psCons RedHow_ByPredSeqUnpack [psHead, psPred]] - rlUnpackNil = [Prove psNil] ==> [Reduction psNil RedHow_ByPredSeqUnpack []] %%]] -- inclSc = ehcCfgCHRInclScope $ feEHCOpts $ fiEnv env %%] diff --git a/EHC/test/regress/16/gadt4.eh b/EHC/test/regress/16/gadt4.eh new file mode 100644 index 000000000..f18ff6ab5 --- /dev/null +++ b/EHC/test/regress/16/gadt4.eh @@ -0,0 +1,27 @@ +let + +data Ref a env + = Zero , env = (a, env') + | Succ (Ref a env') , env = (x, env') + +in let + +data Equal a b + = Eq, a = b + +in let + +data Maybe a + = Nothing + | Just a + +in let + +match :: Ref a env -> Ref b env -> Maybe (Equal a b) +match = \r1 -> \r2 -> + case (r1, r2) of + (Zero, Zero) -> Just Eq + (Succ x, Succ y) -> match x y + (_, _) -> Nothing + +in 3