Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

Comparing changes

Choose two branches to see what's changed or to start a new pull request. If you need to, you can also compare across forks.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
...
Checking mergeability… Don't worry, you can still create the pull request.
  • 16 commits
  • 39 files changed
  • 0 commit comments
  • 1 contributor
Commits on Sep 03, 2007
@amiddelk amiddelk Branch for addition of GADTs to EHC. 0a6c9e0
Commits on Sep 11, 2007
@amiddelk amiddelk * Parser + abstract syntax for GADTs.
* Generation of the appropriate type signatures of constructor/deconstructor functions for GADTs.
* Static checks on GADT definition (kinds, cyclic definitions, etc)

Next step: introduction of assume-equality constraints during pattern matching.
b8e04bc
@amiddelk amiddelk Gathering of assume-equality constraints (from pattern matches) 96f46b3
@amiddelk amiddelk * Generates equality prove obligations when a match with a fixed type…
… variable fails (either a Ty_Var

Fixed or a TyCon "C_...")

Last step: add CHR rules to the CHR machinery to satisfy the generated prove equalities from the 
generated assume equalities.
8524c76
Commits on Sep 14, 2007
@amiddelk amiddelk GADTs + CHR ee79fb6
@amiddelk amiddelk First working GADT test:
-- Test2.eh -------------------------
let data Bool = True | False
    data D a = C1 a,a=Int
             | C2 a,a=Bool
 in let x1 = C1 3
        x2 = C2 True
     in let f :: D a -> a
            f = \z -> case z of
                        C1 _ -> 3
                        C2 _ -> True
         in let y1 = f x1
                y2 = f x2
             in (y1,y2)

(type signature is required)
a0677d3
@amiddelk amiddelk More work on the CHR part of the GADT implementation after obtaining …
…a lot of information about the CHR machinery from Atze.

Some tests:
* test/regress/16/gadt1.eh crashes (multiple reductions for the same prove-constraint, have to look into that)
* test/regress/16/gadt2.eh compiles (still have to check if the output is as expected)
* test/regress/16/gadt3.eh compiles after adding a required signature
d192178
@amiddelk amiddelk The three gadt examples in test/regress/16 now work.
  (changed the heuristics to select a scope rule above the symmetry rule)

Simplified the implementation a bit.
3895ecd
Commits on Sep 17, 2007
@amiddelk amiddelk * Fixed symmetry rule, with my previous implementation it could prove…
… any Prove equality constraint (for some reason)

* New implementation to bring Assume equality constraints in scope (based on fitsIn)

One issue, how to solve in combination with implicit variables:

Assume (c_bla = C_bla)
Prove (c_bla = i_bla -> C_bla)
796d765
Commits on Oct 17, 2007
@amiddelk amiddelk * Created a plain Haskell file to experiment with the CHR machinery (…
…src/chr-experiment)

    ** ambitions for later: turn it into an extensive test suite
* Created a reduction rule to deal with Impl_Tail constructs 
    ** it is a bit too ad-hoc at the moment, but can deal with that later (proof of concept)
    ** still have to adapt the heuristics to deal with this specific reduction
         (maybe the heuristic can also take in account that the assumption we made on the
          context still holds)
* Commited other changes as a precaution for changes I'm about to make.
fad447b
Commits on Oct 18, 2007
@amiddelk amiddelk CHR/GADT: Generic congruence rule (using fitsIn)
* did not have to modify the CHR machinery for that (higher-order predicates and a guard can be used as 'foreign function interface')

It now generates the proper reduction graph for:

Ass. A = B
Ass. B = C
Ass. C1 = (C2 -> A, Int)
Prv. (C2 -> ({! i !} -> C), Int) = C1

(using symmetry, transitivity, congruence, and a rule that assumes that left-over implicit vars can be removed)

Todo: adapt the graph heuristics because there are now new types of reductions in the graph.
b4b31f2
Commits on Oct 19, 2007
@amiddelk amiddelk * Adapted the heuristics to deal with the equality reductions.
* Direct cycles in the reduction graph are now properly handled in general; indirect cyles can only be created by the equality CHRs and are properly handled by the heuristic.
* Added an erasure for evidence resulting from an equality proof.
* Changed my set of rules to properly deal with scoping.
* Disassembled the entire CHR pipeline and reconstructed a simpler pipeline just for some tests (src/chr-experiment/Main.hs)
* Added a todo item on my whiteboard to document the CHR pipeline now I have some more knowledge of it ;-)

And last but not least:
* Changed the chr machinery of EH16 such that it now uses my new rules for equality proofs

Now *all* my gadt examples type check that should type check, and minor variations on them that shouldn't indeed fail with unresolved overloading.

So... it's finished?!

(well... I still need to integrate it with EH versions > 16 and also think about performance because the graphs can get huge...)
f565399
Commits on Nov 01, 2007
@amiddelk amiddelk Thanks to a change by Atze, forward and backward reasoning (needed fo…
…r an example in the left-corner paper of Atze and Doaitse) now seems to work (although slow :( )
3dad54f
Commits on Nov 06, 2007
@amiddelk amiddelk f4a4a8e
Commits on Nov 14, 2007
@amiddelk amiddelk Solved some performance issues with the GADT stuff. It is still not
fast: it takes 23 seconds to compile a derived version of the code of 
Arthur and Doaitse. But I'm not sure anymore if the time is in the CHR 
stuff because EHC itself takes quite some time on that kind of code as 
well (have to do some profiling again).
86bbb00
Commits on Dec 10, 2007
@amiddelk amiddelk Prepared gadt-branch for merge with trunk.
A.k.a. made sure that the gadt changes do not break the main pipeline of 
EHC.

(can take a while due to regression tests)
0f16ef1
Showing with 3,637 additions and 2,073 deletions.
  1. +2,664 −2,025 EHC/configure
  2. +2 −2 EHC/mk/shared.mk.in
  3. +134 −0 EHC/src/chr-experiment/Main.hs
  4. +13 −0 EHC/src/ehc/Base/Opts.chs
  5. +19 −8 EHC/src/ehc/CHR/Solve.chs
  6. +3 −0  EHC/src/ehc/EH.cag
  7. +19 −1 EHC/src/ehc/EH/AbsSyn.cag
  8. +8 −0 EHC/src/ehc/EH/GatherError.cag
  9. +93 −4 EHC/src/ehc/EH/Infer.cag
  10. +13 −0 EHC/src/ehc/EH/InferClassCHR.cag
  11. +102 −4 EHC/src/ehc/EH/InferData.cag
  12. +28 −8 EHC/src/ehc/EH/InferPatExpr.cag
  13. +6 −0 EHC/src/ehc/EH/MainAG.cag
  14. +3 −0  EHC/src/ehc/EH/Parser.chs
  15. +14 −0 EHC/src/ehc/EH/Pretty.cag
  16. +14 −0 EHC/src/ehc/EH/PrettyAST.cag
  17. +10 −0 EHC/src/ehc/EH/ResolvePredCHR.cag
  18. +5 −1 EHC/src/ehc/EH/Uniq.cag
  19. +3 −0  EHC/src/ehc/HS/ExtraChecks.cag
  20. +19 −2 EHC/src/ehc/HS/ToEH.cag
  21. +86 −0 EHC/src/ehc/Pred/CHR.chs
  22. +25 −0 EHC/src/ehc/Pred/CommonCHR.chs
  23. +10 −1 EHC/src/ehc/Pred/EvidenceToCore.chs
  24. +37 −1 EHC/src/ehc/Pred/Heuristics.chs
  25. +11 −5 EHC/src/ehc/Pred/RedGraph.chs
  26. +42 −3 EHC/src/ehc/Pred/ToCHR.chs
  27. +1 −1  EHC/src/ehc/Scanner/Common.chs
  28. +3 −0  EHC/src/ehc/Ty.cag
  29. +24 −0 EHC/src/ehc/Ty/AbsSyn.cag
  30. +100 −0 EHC/src/ehc/Ty/FitsIn.chs
  31. +5 −0 EHC/src/ehc/Ty/Ftv.cag
  32. +12 −0 EHC/src/ehc/Ty/Pretty.cag
  33. +10 −0 EHC/src/ehc/Ty/Trf/Canonic.cag
  34. +48 −5 EHC/src/ehc/Ty/Trf/Subst.cag
  35. +6 −0 EHC/src/ehc/Ty/TrieKey.cag
  36. +2 −1  EHC/src/libutil/EH/Util/AGraph.hs
  37. +2 −1  EHC/test/regress/16/gadt3.eh
  38. +27 −0 EHC/test/regress/16/gadt4.eh
  39. +14 −0 EHC/test/regress/16/gadt5.eh
View
4,689 EHC/configure
2,664 additions, 2,025 deletions not shown
View
4 EHC/mk/shared.mk.in
@@ -170,7 +170,7 @@ RULER2_OPTS := $(RULER2_OPTS_DFLT)
# order to shuffle (see ehc/src/files1.mk for a complete list)
# 4_99: interim for stuff from 4, needed for 4_2, because of ruler generated material uptil 4_2
-EHC_SHUFFLE_ORDER := 1 < 2 < 3 < 4 < 4_99 < 5 < 6 < 7 < 8 < 9 < 10 < 11 < 12 < 13 < 14 < 15 < 16 < 20 < 95 < 96 < 97 < 98 < $(EHC_UHC_VARIANT) < 100 < 101, 4_99 < 4_2, 6 < 6_4, 7 < 7_2, 10 < 50
+EHC_SHUFFLE_ORDER := 1 < 2 < 3 < 4 < 4_99 < 5 < 6 < 7 < 8 < 9 < 10 < 11 < 12 < 13 < 14 < 15 < 20 < 95 < 96 < 97 < 98 < $(EHC_UHC_VARIANT) < 100 < 101, 4_99 < 4_2, 6 < 6_4, 7 < 7_2, 10 < 50, 15 < 16
###########################################################################################
# Misc
@@ -212,7 +212,7 @@ GEN_CABAL = \
echo "Homepage: http://www.cs.uu.nl/wiki/Ehc/WebHome" ; \
echo "Category: Testing" ; \
echo "Build-Depends: $(subst $(space),$(comma),$(strip base haskell98 mtl fgl $(GHC_EHC_PKG_UULIB) $(3)))" ; \
- echo "Extensions: $(subst $(space),$(comma),$(strip RankNTypes MultiParamTypeClasses FunctionalDependencies $(4)))" ; \
+ echo "Extensions: $(subst $(space),$(comma),$(strip RankNTypes MultiParamTypeClasses FunctionalDependencies TypeSynonymInstances FlexibleContexts FlexibleInstances $(4)))" ; \
echo "Synopsis: $(strip $(5))" ; \
echo "Exposed-Modules: $(subst $(space),$(comma),$(strip $(6)))" ; \
echo "C-Sources: $(subst $(space),$(comma),$(strip $(7)))" ; \
View
134 EHC/src/chr-experiment/Main.hs
@@ -0,0 +1,134 @@
+{-# OPTIONS_GHC -fglasgow-exts -package EH16 #-}
+module Main where
+
+import EH16.CHR
+import EH16.Pred.ToCHR
+import EH16.CHR.Solve
+import EH16.Ty.FitsIn
+import EH16.Ty
+import EH16.Pred.CHR
+import EH16.Pred.CommonCHR
+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 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 :: PredScope -> Pred -> Constraint CHRPredOcc RedHowAnnotation
+ a s pr = Assume (mkCHRPredOcc pr s)
+
+ p :: PredScope -> Pred -> Constraint CHRPredOcc RedHowAnnotation
+ p s pr = Prove (mkCHRPredOcc pr s)
+
+ 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
+
+ ty1 = mkProdApp [tyK2 `mk1Arrow` tyA, tyInt]
+ 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 = initScopedPredStore
+{-
+ = chrStoreFromElems
+ $ [ -- symmetry (prove)
+ [Prove eqT1T2] ==> [Prove eqT2T1, Reduction eqT1T2 RedHow_ByEqSymmetry [eqT2T1]]
+ |> [UnequalTy ty1 ty2]
+ , -- transitivity (normal case)
+ [Prove eqT1T2, Assume eqT2T3] ==> [Prove eqT1T3, Reduction eqT1T2 RedHow_ByEqTrans [eqT1T3, eqT2T3]]
+ |> [UnequalTy ty2 ty3]
+ , -- transitivity (asymmetric case)
+ [Prove eqT1T2, Assume eqT3T2] ==> [Prove eqT1T3, Reduction eqT1T2 RedHow_ByEqTrans [eqT1T3, eqT3T2]]
+ |> [UnequalTy ty2 ty3]
+ , -- context to nil reduction on equality types
+ [Prove eqT1T2] ==> [Prove eqT1T3, Reduction eqT1T2 (RedHow_ByEqTyReduction ty2 ty3) [eqT1T3]]
+ |> [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]]
+ |> [EqsByCongruence ty1 ty2 ps]
+ , -- unpack predseq (cons)
+ [Prove psCons] ==> [Prove psHead, Prove psPred, Reduction psCons RedHow_ByPredSeqUnpack [psHead, psPred]]
+ , -- unpack predsec (nil)
+ [Prove psNil] ==> [Reduction psNil RedHow_ByPredSeqUnpack []]
+ ]
+ where
+ eqT1T2 = mkCHRPredOcc (Pred_Eq ty1 ty2) sc
+ eqT2T1 = mkCHRPredOcc (Pred_Eq ty2 ty1) sc
+ eqT2T3 = mkCHRPredOcc (Pred_Eq ty2 ty3) sc
+ eqT3T2 = mkCHRPredOcc (Pred_Eq ty3 ty2) sc
+ eqT1T3 = mkCHRPredOcc (Pred_Eq ty1 ty3) sc
+ psPred = mkCHRPredOcc (Pred_Preds ps) sc
+ psCons = mkCHRPredOcc (Pred_Preds (PredSeq_Cons pr ps)) sc
+ psNil = mkCHRPredOcc (Pred_Preds PredSeq_Nil) sc
+ psHead = mkCHRPredOcc pr sc
+
+ sc = PredScope_Var u1
+ [ty1,ty2,ty3] = map mkTyVar [u2,u3,u4]
+ 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]
+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 ]
+
+graph :: RedGraph CHRPredOcc RedHowAnnotation
+graph = addToRedGraphFromReductions producedCnstrs (addToRedGraphFromAssumes assumeMap emptyRedGraph)
+
+evid :: Evidence CHRPredOcc RedHowAnnotation
+evid = snd $ head $ (heurScopedEHC env) [RedHow_ProveObl uidNull (PredScope_Var uidNull)] $ redAlternatives graph p
+ where (Prove p) = last input
+
+res :: PP_Doc
+res = vlist (map pp producedCnstrs)
+
+main :: IO ()
+main = return ()
View
13 EHC/src/ehc/Base/Opts.chs
@@ -482,6 +482,11 @@ optsDiscrRecompileRepr opts
%%% Fitting options (should be in FitsIn, but here it avoids mut rec modules)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+Difference strong/weak:
+
+strong: in a context where information is known (i.e. type signature)
+strong allows impredicative binding whereas weak will instantiate quantifiers
+
%%[9 export(FIOBind(..),fioBindIsYes,fioBindNoSet)
data FIOBind = FIOBindYes | FIOBindNoBut TyVarIdS
@@ -506,6 +511,10 @@ data FIOpts = FIOpts { fioLeaveRInst :: Bool , fioBindR
, fioDontBind :: TyVarIdS
, fioBindLVars :: FIOBind , fioBindRVars :: FIOBind
%%]
+%%[16.FIOpts
+ , fioFitFailureToProveObl :: Bool
+ , fioFitVarFailureToProveObl :: Bool
+%%]
%%[50.FIOpts
, fioAllowEqOpen :: Bool , fioInstCoConst :: HowToInst
%%]
@@ -527,6 +536,10 @@ strongFIOpts = FIOpts { fioLeaveRInst = False , fioBindR
, fioDontBind = Set.empty
, fioBindLVars = FIOBindYes , fioBindRVars = FIOBindYes
%%]
+%%[16.FIOpts
+ , fioFitFailureToProveObl = False
+ , fioFitVarFailureToProveObl = False
+%%]
%%[50.FIOpts
, fioAllowEqOpen = False , fioInstCoConst = instCoConst
%%]
View
27 EHC/src/ehc/CHR/Solve.chs
@@ -24,7 +24,7 @@ Assumptions (to be documented further)
%%]
-- For debug
-%%[9 import(EH.Util.Utils)
+%%[9 import(EH.Util.Utils, Debug.Trace)
%%]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -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
View
3  EHC/src/ehc/EH.cag
@@ -58,6 +58,9 @@
%%[15 hs export(FuncDep(..), FuncDeps)
%%]
+%%[16 hs export(DataConstrEq(..), DataConstrEqs)
+%%]
+
%%[50 hs export(DataConstrEq(..), DataConstrEqs)
%%]
View
20 EHC/src/ehc/EH/AbsSyn.cag
@@ -439,6 +439,9 @@ DATA DataConstr
mbFixityPrio : {Maybe Int} -- Nothing: not infix
%%]]
fields : DataFields
+%%[[16
+ eqs : DataConstrEqs
+%%]]
%%]
%%[50.DataConstr
eqs : DataConstrEqs
@@ -456,6 +459,14 @@ DATA DataField
TYPE DataFields = [DataField]
%%]
+%%[16.Data
+DATA DataConstrEq
+ | Eq tyVar : TyVar
+ tyExpr : TyExpr
+
+TYPE DataConstrEqs = [DataConstrEq]
+%%]
+
%%[50.Data
DATA DataConstrEq
| Eq tyVar : TyVar
@@ -475,6 +486,13 @@ SET AllDataField = DataField DataFields
SET AllData = AllDataField AllDataConstr
%%]
+%%[16.SetsData -7.SetsData
+SET AllDataConstrEq = DataConstrEq DataConstrEqs
+SET AllDataConstr = DataConstr DataConstrs
+SET AllDataField = DataField DataFields
+SET AllData = AllDataField AllDataConstr AllDataConstrEq
+%%]
+
%%[50.SetsData -7.SetsData
SET AllDataConstrEq = DataConstrEq DataConstrEqs
SET AllDataConstr = DataConstr DataConstrs
@@ -537,7 +555,7 @@ SET AllNT = AllData AllCase AllTyExpr AllTyVar AllDecl AllPatExpr Al
AllFuncDep
%%]]
-SET NTPrf = AllDecl AllCase AllExpr AllPatExpr
+SET NTPrf = AllDecl AllCase AllExpr AllPatExpr AllData
%%]
View
8 EHC/src/ehc/EH/GatherError.cag
@@ -183,6 +183,14 @@ SEM PatExpr
| Expr lhs . errSq = rngLift @range mkNestErr' @pp [@expr.errSq, Seq.fromList @nmErrs, foErrSq @fo_]
%%]
+%%[16
+SEM DataConstr
+ | Constr lhs . errSq := rngLift @range mkNestErr' @pp [@fields.errSq, @eqs.errSq, foErrSq @fo_, Seq.fromList @loc.occErrL, @loc.undefVarsErrSq]
+
+SEM DataConstrEq
+ | Eq lhs . errSq = rngLift @range mkNestErr' @pp [foErrSq @loc.fo_, foErrSq @loc.foRhsTy, @tyVar.errSq, @tyExpr.errSq]
+%%]
+
%%[50
SEM DataConstr
| Constr lhs . errSq := rngLift @range mkNestErr' @pp [@fields.errSq, @eqs.errSq, foErrSq @fo_]
View
97 EHC/src/ehc/EH/Infer.cag
@@ -240,6 +240,14 @@ SEM Expr
ATTR AllDataField [ | tyGam: TyGam | ]
%%]
+%%[16
+ATTR AllDataConstrEq [ | tyGam: TyGam | ]
+
+-- tyvarid of .tyVar already present in @lhs.tyGam
+SEM DataConstrEq
+ | Eq tyExpr.tyGam = @lhs.tyGam
+%%]
+
%%[50
ATTR AllDataConstrEq [ | tyGam: TyGam | ]
%%]
@@ -251,6 +259,9 @@ ATTR
%%[[7
AllDataField
%%]]
+%%[[16
+ AllDataConstrEq
+%%]]
[ | tyKiGam: TyKiGam | ]
%%]
@@ -836,51 +847,95 @@ ATTR AllExpr AllPatExpr [ fiOpts: FIOpts | | ]
SEM AGItf
| AGItf expr . fiOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
%%]
-- generated from ruler rules into EHRulerRules, was/from 4.fiOpts.init
%%[5.fiOpts.init
SEM Expr
| AppImpred func . fiOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
loc . argFIOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
arg . fiOpts = @argFIOpts
-
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
%%]
-- generated from ruler rules into EHRulerRules, was 2.App
%%[5.fiOpts.init
SEM Decl
| Val expr . fiOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
patExpr . fiOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
%%]
-- generated from ruler rules into EHRulerRules, was 2.App
%%[5.fiOpts.init
SEM Expr
- | Lam loc . knFunFIOpts = @lhs.fiOpts {fioBindRFirst=True}
+ | Lam loc . knFunFIOpts = (@lhs.fiOpts {fioBindRFirst=True })
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
| App func . fiOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
loc . argFIOpts = instLFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
arg . fiOpts = @argFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
%%]
-- 20070205 - AD, should be generated from ruler rules, but not yet is
%%[5
SEM Expr
| TypeAs loc . asFiOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
expr . fiOpts = @asFiOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
%%]
%%[5
ATTR AllCase [ fiOpts: FIOpts | | ]
SEM Decl
- | Val expr . fiOpts := if @hasTySig then strongFIOpts else weakFIOpts
+ | Val expr . fiOpts := (if @hasTySig then strongFIOpts else weakFIOpts)
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
SEM CaseAlt
| Pat patExpr . fiOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
SEM Expr
- | Case expr . fiOpts = weakFIOpts
+ | Case expr . fiOpts = weakFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
%%]
%%[7
@@ -888,37 +943,70 @@ ATTR DataFieldExpr [ fldFIOpts: FIOpts | | ]
SEM RecExpr
| Ext loc . knFIOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
recExpr . fiOpts = @lhs.fiOpts {fioNoRLabElimFor = @nm : fioNoRLabElimFor @lhs.fiOpts}
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
| Upd loc . knFIOpts = strongFIOpts -- {fioNoRLabElimFor = [@nm]}
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
| Ext Upd expr . fiOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
SEM Expr
| DataFields loc . fldFIOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
SEM DataFieldExpr
| Upd expr . fiOpts = @lhs.fldFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
SEM Expr
| Rec loc . fiOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
%%]
%%[9
SEM Expr
| App func . fiOpts := implFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
SEM Decl
| InstanceIntro
expr . fiOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
%%]
%%[12
SEM Expr
| AppImpl arg . fiOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
%%]
%%[1010
SEM Decl
| DynVal expr . fiOpts = strongFIOpts
+%%[[16
+ {fioFitVarFailureToProveObl = True }
+%%]]
%%]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -982,6 +1070,7 @@ SEM PatExpr
%%]
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% The XX_App function name of a XX, if any
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
View
13 EHC/src/ehc/EH/InferClassCHR.cag
@@ -95,6 +95,19 @@ SEM Decl
SEM Expr
| LamImpl loc . implsIsEmpty = null @knPrL
+%%[16
+-- Each branch in a case expr has it's own predicate scope
+ATTR CaseAlts [ predScopeCounter : Int | | ]
+
+SEM Expr
+ | Case
+ alts.predScopeCounter = 0
+
+SEM CaseAlts
+ | Cons
+ (tl.predScopeCounter, hd.predScope) = pscpEnter @lhs.predScopeCounter @lhs.predScope
+%%]
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Scopes of introduced bindings
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
View
106 EHC/src/ehc/EH/InferData.cag
@@ -103,7 +103,8 @@ SEM DataConstr
loc . dataConProdTy : Ty
loc . dataQuUnConTy = let fvD = ftv @lhs.dataTy
fvU = ftv @dataConProdTy
- in mkTyQu TyQu_Forall fvD ([@lhs.dataTy] `mkArrow` mkTyQu TyQu_Exists (fvU \\ fvD) @dataConProdTy)
+ in (mkTyQu TyQu_Forall fvD ([@lhs.dataTy] `mkArrow` mkTyQu TyQu_Exists (fvU \\ fvD) @dataConProdTy))
+
lhs . patValGam = gamUnions
[ assocLToGam
[ (@conNm, ValGamInfo @dataConTy)
@@ -132,13 +133,18 @@ SEM Decl
]
%%]
+
%%[7
ATTR AllDataConstr [ | | dataAltTyL USE {++} {[]}: {AssocL HsName Ty} ]
SEM DataConstr
- | Constr loc . dataConTy := assocLElts @fields.fldTyL `mkArrow` @lhs.dataTy
- . dataConProdTy := let lbls = zipWith (\p (ml,_) -> maybe p id ml) positionalFldNames @fields.fldTyL
- in mkTyRec (zipWith (\l (_,t) -> (l,t)) lbls @fields.fldTyL)
+ | Constr loc . dataConTy2 = assocLElts @fields.fldTyL `mkArrow` @lhs.dataTy
+ loc . dataConProdTy2 = let lbls = zipWith (\p (ml,_) -> maybe p id ml) positionalFldNames @fields.fldTyL
+ in mkTyRec (zipWith (\l (_,t) -> (l,t)) lbls @fields.fldTyL)
+
+ loc . dataConTy := @loc.dataConTy1
+ loc . dataConProdTy := @loc.dataConProdTy1
+
loc . dataAltTyL = [(@conNm,@dataConProdTy)]
SEM Decl
@@ -146,6 +152,37 @@ SEM Decl
. dataTgi := mkTGIData (Ty_Con @tyNm) Ty_Any {- ([@dataTy] `mkArrow` @dataAltTy) -}
%%]
+%%[7.dataConXTy
+SEM DataConstr
+ | Constr
+ loc.dataConTy1 = @loc.dataConTy2
+ loc.dataConProdTy1 = @loc.dataConProdTy2
+%%]
+
+%%[16.dataConXTy -7.dataConXTy
+SEM DataConstr
+ | Constr
+ (loc.dataConTy1, loc.cycVarMp) = @loc.eqsVarMp `tyAppVarMp2_RhsOfEqOnly` @loc.dataConTy2
+ (loc.dataConProdTy1, _) = @loc.eqsVarMp `tyAppVarMp2_RhsOfEqOnly` appendEqPreds @eqs.prOccL @loc.dataConProdTy2 -- cyclic occurrences subsumed by @loc.cycVarMp
+ loc.occErrL = varmpOccurErr
+%%[[99
+ @range
+%%]]
+ @loc.cycVarMp
+%%]
+
+%%[16 hs
+-- assumption: Ty is a product
+-- this function is supposed to be applied to the RHS of the unquantified type of the deconstructor function, which
+-- is a product of the field types of the constructor. The equality constraints are encoded by adding them to the
+-- end of this product.
+appendEqPreds :: [PredOcc] -> Ty -> Ty
+appendEqPreds preds ty
+ = let predsTyL = map (Ty_Pred . poPr) preds
+ prodTyL = tyProdArgs ty
+ in mkProdApp (prodTyL ++ predsTyL)
+%%]
+
%%[8
ATTR AllDataConstr [ dataAltTy: Ty | | ]
%%]
@@ -338,6 +375,47 @@ SEM Expr
%%]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%% GADT
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+Kind of LHS of the DataConstrEq should match the kind of the RHS.
+
+%%[16
+SEM DataConstrEq
+ | Eq loc.fo_ = fitsIn weakFIOpts emptyFE @lUniq @tyExpr.kiVarMp @tyVar.ki @tyExpr.ki
+ lhs.kiVarMp = foVarMp @loc.fo_ |=> @tyExpr.kiVarMp
+
+ATTR AllDataConstrEq [ | | prOccL USE {++} {[]} : {[PredOcc]} ]
+
+SEM DataConstrEq
+ | Eq loc.pr = Pred_Eq @tyVar.ty @tyExpr.ty
+ loc.prOccId = mkPrIdCHR @loc.lUniq3
+ loc.prOcc = mkPredOcc @loc.pr @loc.prOccId @lhs.predScope
+ lhs.prOccL = [@loc.prOcc]
+%%]
+
+Construct a substitution from the additional equations. This subsitution is applied to the type of the constructor function to obtain
+the actual type of the constructor, i.e. the additional equations do not show up in the type of a constructor. The equations are required
+to be non-cyclic, and in case one equation is multiply defined, the right hand sides have to be equal modulo unification.
+
+%%[16
+SEM AllDataConstrEq [ | eqVarMp : {VarMp} | ]
+
+SEM DataConstr
+ | Constr
+ eqs.eqVarMp = emptyVarMp
+ loc.eqsVarMp = @eqs.eqVarMp
+
+SEM DataConstrEq
+ | Eq
+ loc.tv = tyVar @tyVar.ty
+ loc.knRhsTy = maybe Ty_Any id $ varmpTyLookup @loc.tv @lhs.eqVarMp
+ loc.foRhsTy = fitsIn strongFIOpts emptyFE @lUniq2 @lhs.eqVarMp @loc.knRhsTy @tyExpr.ty
+ loc.unitVarMp = @loc.tv `varmpTyUnit` foTy @loc.foRhsTy
+ lhs.eqVarMp = @loc.unitVarMp |=> foVarMp @loc.foRhsTy |=> @lhs.eqVarMp
+%%]
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Pattern: additional info for checks, codegen, etc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -358,4 +436,24 @@ SEM DataFieldPatExpr
| * - Ext lhs . fldL = []
%%]
+Check that LHS of equations is a tyvar in scope
+%%[16
+ATTR AllDataConstrEq TyVar [ | | tyvarNms USE {`Set.union`} {Set.empty} : {Set HsName} ]
+SEM TyVar
+ | Var lhs.tyvarNms = Set.singleton @nm
+
+SEM DataConstr
+ | Constr
+ loc.tyVarsInScope = Set.fromList (gamKeys @fields.tyGam)
+ loc.undefTyVarsInEqs = @eqs.tyvarNms `Set.difference` @loc.tyVarsInScope
+ loc.undefVarsErrSq = if Set.null @loc.undefTyVarsInEqs
+ then Seq.empty
+ else Seq.singleton $
+ Err_NamesNotIntrod
+%%[[99
+ @range
+%%]]
+ "" [(pp nm, Nothing) | nm <- Set.toList @loc.undefTyVarsInEqs]
+
+%%]
View
36 EHC/src/ehc/EH/InferPatExpr.cag
@@ -56,13 +56,21 @@ SEM PatExpr
%%[5.patFunTy
SEM PatExpr
| Con loc . (ty_g_,nmErrs) = valGamLookupTy (hsnUn @nm) @lhs.valGam
- . (tvarv1_,tvarv2_,fo_fitP_)
- = let [a,r] = mkNewTyVarL 2 @lUniq
- in (a,r,fitsIn instFIOpts @fe @lUniq2 emptyVarMp @ty_g_ ([a] `mkArrow` r))
+ . (tvarv1_,tvarv2_) = let [a,r] = mkNewTyVarL 2 @lUniq in (a,r)
+ . knTyShape = [@loc.tvarv1_] `mkArrow` @loc.tvarv2_
+ . fo_fitP_ = fitsIn instFIOpts @fe @lUniq2 emptyVarMp @ty_g_ @loc.knTyShape
. tyVarMp_p_ = foVarMp @fo_fitP_
. patFunTy := @tyVarMp_p_ |=> foTy @fo_fitP_
%%]
+GADT: deconstructor signature will be a function with a product (with possibly equality constraints) as value.
+ match with this additional information such that the equality constraints will be stripped off by the fitsIn function.
+%%[16.patFunTy
+SEM PatExpr
+ | Con
+ loc.knTyShape := [@loc.tvarv1_] `mkArrow` (hsnRec `mkConApp` [@loc.tvarv2_])
+%%]
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Distribution of known ty
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -74,11 +82,14 @@ ATTR PatExpr [ knTyL: TyL | | ]
-- generated from ruler rules into EHRulerRules, was 1.knTy.App
%%[5.knTy.App
+
+-- Note: knProdTy is later replaced by @loc.patFunTy which is based on the signature of the deconstructor
+
SEM PatExpr
- | AppTop loc . knProdTy
- = @lhs.knTy
+ | AppTop loc . knProdTy = @lhs.knTy
+ . prodTyL = tyProdArgs @knProdTy
. (knTyL,arityErrs)
- = case tyProdArgs @knProdTy of
+ = case @loc.prodTyL of
tL | @patExpr.arity == length tL
-> (reverse tL,[])
_ -> (repeat Ty_Any
@@ -224,12 +235,21 @@ SEM DataFieldPatExpr
patExpr . knTy = @knFldTy
loc . ty = @dataFieldPatExpr.ty
| Con loc . (gTy,nmErrs) = valGamLookupTy (hsnUn @nm) @lhs.valGam
- . fo_ = let [u] = mkNewTyVarL 1 @lUniq
- in fitsIn @lhs.fiOpts @fe @lUniq2 @lhs.tyVarMp @gTy ([@lhs.knTy] `mkArrow` u)
+ . tyvar = mkTyVar @lUniq
+ . knTyShape = [@lhs.knTy] `mkArrow` @knTyShape
+ . fo_ = fitsIn @lhs.fiOpts @fe @lUniq2 @lhs.tyVarMp @gTy @loc.knTyShape
. ty = @lhs.knTy
lhs . tyVarMp = foVarMp @fo_ |=> @lhs.tyVarMp
%%]
+GADT: deconstructor signature will be a function with a product (with possibly equality constraints) as value.
+ match with this additional information such that the equality constraints will be stripped off by the fitsIn function.
+%%[16
+SEM DataFieldPatExpr
+ | Con
+ loc.knTyShape := [@lhs.knTy] `mkArrow` (hsnRec `mkConApp` [@loc.tyvar])
+%%]
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Row based records
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
View
6 EHC/src/ehc/EH/MainAG.cag
@@ -55,6 +55,9 @@
%%[9 hs import({%{EH}Ty.Trf.Canonic})
%%]
+%%[16 hs import({%{EH}Ty.Trf.Subst})
+%%]
+
%%[50 hs import({%{EH}Ty.Trf.ElimEqual},{%{EH}Gam.Utils})
%%]
@@ -363,6 +366,9 @@ SEM *
loc.clMissNmS : {Set HsName}
loc.clKiNmErrs : ErrL
loc.foKnRec : FIOut
+ loc.eqsVarMp : VarMp
+ loc.dataConTy1 : Ty
+ loc.foRhsTy : FIOut
%%]
View
3  EHC/src/ehc/EH/Parser.chs
@@ -400,6 +400,9 @@ pDataConstr = mkEH DataConstr_Constr
pDataConstr = (\c f -> mkEH DataConstr_Constr c Nothing f)
%%]]
<$> pCon <*> (pDataFields <|> pCurly pDataLabFields)
+%%[[16
+ <*> pList (mkEH DataConstrEq_Eq <$ pComma <*> pTyVar <* pKey "=" <*> pTyExpr)
+%%]]
%%]
%%[50.DataConstr
<*> pList (mkEH DataConstrEq_Eq <$ pComma <*> pTyVar <* pKey "=" <*> pTyExpr)
View
14 EHC/src/ehc/EH/Pretty.cag
@@ -387,11 +387,25 @@ SEM DataConstr
>|< @ppExtra
. ppExtra = empty
%%]
+%%[16
+SEM DataConstr
+ | Constr loc . ppExtra := hlist . map ("," >#<) $ @eqs.ppL
+%%]
%%[50
SEM DataConstr
| Constr loc . ppExtra := hlist . map ("," >#<) $ @eqs.ppL
%%]
+%%[16
+ATTR DataConstrEqs [ | | ppL: {[PP_Doc]} ]
+
+SEM DataConstrEq
+ | Eq loc . pp = @tyVar.pp >|< "=" >|< @tyExpr.pp
+
+SEM DataConstrEqs
+ | Nil lhs . ppL = []
+ | Cons lhs . ppL = @hd.pp : @tl.ppL
+%%]
%%[50
ATTR DataConstrEqs [ | | ppL: {[PP_Doc]} ]
View
14 EHC/src/ehc/EH/PrettyAST.cag
@@ -648,6 +648,20 @@ SEM Decl
]
%%]
+%%[16
+SEM DataConstrEq
+ | Eq lhs . ppAST = ppNest ["DataConstrEq","Eq"] [] [@tyVar.ppAST,@tyExpr.ppAST]
+
+SEM DataConstrEqs
+ | Nil lhs . ppAST = ppNest ["DataConstrEqs","Nil"] [] []
+ | Cons lhs . ppAST = ppNest ["DataConstrEqs","Cons"] [] [@hd.ppAST,@tl.ppAST]
+
+SEM DataConstr
+ | Constr loc . ppAST := ppNestInfo @lhs.opts ["DataConstr","Constr"] [ppNm @conNm] [@fields.ppAST,@eqs.ppAST] @info
+ loc . info = [ -- mkInfo1 "eqs.eqTyVarMp" (pp @eqs.eqTyVarMp)
+ ]
+%%]
+
%%[50
SEM DataConstrEq
| Eq lhs . ppAST = ppNest ["DataConstrEq","Eq"] [] [@tyVar.ppAST,@tyExpr.ppAST]
View
10 EHC/src/ehc/EH/ResolvePredCHR.cag
@@ -40,6 +40,16 @@ SEM RecPatExpr
lhs . gathCnstrMp = cnstrMpUnions [@hereCnstrMp, @recPatExpr.gathCnstrMp, @patExpr.gathCnstrMp]
%%]
+%%[16
+SEM PatExpr
+ | Con loc . hereCnstrMp = foGathCnstrMp @fo_fitP_
+ lhs . gathCnstrMp = @loc.hereCnstrMp
+
+SEM DataFieldPatExpr
+ | Con loc . hereCnstrMp = foGathCnstrMp @fo_
+ lhs . gathCnstrMp = @loc.hereCnstrMp
+%%]
+
%%[97
SEM PatExpr
| Expr loc . hereCnstrMp = foGathCnstrMp @fo_
View
6 EHC/src/ehc/EH/Uniq.cag
@@ -207,7 +207,6 @@ SEM DataField
%%]
-
New unique-rules for 7_2: I just need a lot of unique numbers...
%%[7_2
@@ -379,6 +378,11 @@ SEM PatExpr
| Expr (expr.gUniq,loc.lUniq,loc.lUniq2,loc.lUniq3) = mkNewLevUID3 @lhs.gUniq
%%]
+%%[16
+SEM DataConstrEq
+ | Eq (tyVar.gUniq,loc.lUniq,loc.lUniq2,loc.lUniq3) = mkNewLevUID3 @lhs.gUniq
+%%]
+
%%[50
SEM DataConstrEq
| Eq (tyVar.gUniq,loc.lUniq) = mkNewLevUID @lhs.gUniq
View
3  EHC/src/ehc/HS/ExtraChecks.cag
@@ -49,6 +49,9 @@ SEM Declaration
_
%%]]
[_]
+%%[[16
+ _
+%%]]
-> []
_ -> [rngLift @range Err_Newtype @simpletype.name]
%%]
View
21 EHC/src/ehc/HS/ToEH.cag
@@ -330,9 +330,17 @@ ehPlainDataField r
%%[5.Constructor
SEM Constructor
| Constructor
- lhs . eh = rngLift @range EH.DataConstr_Constr @conrefname @types.eh
+ lhs . eh = rngLift @range EH.DataConstr_Constr @conrefname
+ @types.eh
+%%[[16
+ []
+%%]]
| Infix
- lhs . eh = rngLift @range EH.DataConstr_Constr @conrefname [@leftType.eh,@rightType.eh]
+ lhs . eh = rngLift @range EH.DataConstr_Constr @conrefname
+ [@leftType.eh,@rightType.eh]
+%%[[16
+ []
+%%]]
%%]
%%[7.Constructor -5.Constructor
SEM Constructor
@@ -342,18 +350,27 @@ SEM Constructor
Nothing
%%]]
(map (ehPlainDataField emptyRange) @types.eh)
+%%[[16
+ []
+%%]]
| Infix
lhs . eh = rngLift @range EH.DataConstr_Constr @conrefname
%%[[95
(Just $ fgiPrio $ fixityGamLookup @conrefname @lhs.fixityGam)
%%]]
(map (ehPlainDataField emptyRange) [@leftType.eh,@rightType.eh])
+%%[[16
+ []
+%%]]
| Record
lhs . eh = rngLift @range EH.DataConstr_Constr @conrefname
%%[[95
Nothing
%%]]
@fieldDeclarations.eh
+%%[[16
+ []
+%%]]
%%]
%%[9
| Contexted
View
86 EHC/src/ehc/Pred/CHR.chs
@@ -25,6 +25,9 @@ Derived from work by Gerrit vd Geest.
%%[10 import({%{EH}Base.Builtin})
%%]
+%%[16 import({%{EH}Ty.Trf.MergePreds}, {%{EH}Ty.FitsInCommon}, {%{EH}Base.Opts}, Debug.Trace)
+%%]
+
%%[20 import({%{EH}Base.CfgPP})
%%]
@@ -99,6 +102,11 @@ instance CHRSubstitutable Guard TyVarId VarMp where
%%[[10
chrFtv (NonEmptyRowLacksLabel r o t l ) = Set.unions [ftvSet r,ftvSet o,ftvSet t,ftvSet l]
%%]]
+%%[[16
+ chrFtv (IsCtxNilReduction t1 t2) = Set.unions [ftvSet t1, ftvSet t2]
+ chrFtv (EqsByCongruence t1 t2 ps) = Set.unions [ftvSet t1, ftvSet t2, ftvSet ps]
+ chrFtv (EqualModuloUnification t1 t2) = Set.unions [ftvSet t1, ftvSet t2]
+%%]]
chrAppSubst s (HasStrictCommonScope p1 p2 p3) = HasStrictCommonScope (s |=> p1) (s |=> p2) (s |=> p3)
chrAppSubst s (IsStrictParentScope p1 p2 p3) = IsStrictParentScope (s |=> p1) (s |=> p2) (s |=> p3)
@@ -108,6 +116,12 @@ instance CHRSubstitutable Guard TyVarId VarMp where
%%[[10
chrAppSubst s (NonEmptyRowLacksLabel r o t l ) = NonEmptyRowLacksLabel (s |=> r) (s |=> o) (s |=> t) (s |=> l)
%%]]
+%%[[16
+ chrAppSubst s (IsCtxNilReduction t1 t2) = IsCtxNilReduction (s |=> t1) (s |=> t2)
+ chrAppSubst s (EqsByCongruence t1 t2 ps) = EqsByCongruence (s |=> t1) (s |=> t2) (s |=> ps)
+ chrAppSubst s (UnequalTy t1 t2) = UnequalTy (s |=> t1) (s |=> t2)
+ chrAppSubst s (EqualModuloUnification t1 t2) = EqualModuloUnification (s |=> t1) (s |=> t2)
+%%]]
%%]
%%[9
@@ -129,6 +143,9 @@ instance CHRSubstitutable RedHowAnnotation TyVarId VarMp where
%%[[10
chrAppSubst s (RedHow_ByLabel l o sc) = RedHow_ByLabel (chrAppSubst s l) (chrAppSubst s o) (chrAppSubst s sc)
%%]]
+%%[[16
+ chrAppSubst s (RedHow_ByEqTyReduction ty1 ty2) = RedHow_ByEqTyReduction (s |=> ty1) (s |=> ty2)
+%%]]
chrAppSubst _ x = x
%%]
@@ -222,6 +239,12 @@ data Guard
%%[[10
| NonEmptyRowLacksLabel Ty LabelOffset Ty Label -- non empty row does not have label?, yielding its position + rest
%%]]
+%%[[16
+ | IsCtxNilReduction Ty Ty
+ | EqsByCongruence Ty Ty PredSeq
+ | UnequalTy Ty Ty
+ | EqualModuloUnification Ty Ty
+%%]]
%%]
%%[9
@@ -234,6 +257,12 @@ ppGuard (EqualScope sc1 sc2 ) = sc1 >#< "==" >#< sc2
%%[[10
ppGuard (NonEmptyRowLacksLabel r o t l ) = ppParens (t >#< "==" >#< ppParens (r >#< "| ...")) >#< "\\" >#< l >|< "@" >|< o
%%]]
+%%[[16
+ppGuard (IsCtxNilReduction t1 t2 ) = t1 >#< "~>" >#< t2
+ppGuard (EqsByCongruence t1 t2 ps ) = t1 >#< "~~" >#< t2 >#< "~>" >#< ps
+ppGuard (UnequalTy t1 t2 ) = t1 >#< "/=" >#< t2
+ppGuard (EqualModuloUnification t1 t2 ) = t1 >#< "==" >#< t2
+%%]]
%%]
ppGuard (IsStrictParentScope sc1 sc2 sc3) = ppParens (ppParens (sc1 >#< "==" >#< sc2 >#< "\\/" >#< sc1 >#< "==" >#< sc3 ) >#< "/\\" >#< sc2 >#< "/=" >#< sc3)
@@ -297,6 +326,63 @@ instance CHRCheckable FIIn Guard VarMp where
(offset,presence) = tyExtsOffset lab' $ tyRowCanonOrder exts
(Label_Lab lab') = chrAppSubst subst' lab
%%]]
+%%[[16
+ chk (IsCtxNilReduction t1 t2)
+ = if foHasErrs fo || tStart == tRes
+ then Nothing
+ else return varMp
+ where
+ tStart = subst' |=> t1
+ t1' = tmpoTy $ tyMergePreds [] tStart
+ t2' = subst' |=> t2
+ uid = fiUniq env
+ fiOpts = unifyFIOpts { fioUniq = uid, fioBindRVars = FIOBindNoBut (ftvSet t2), fioPredAsTy = True, fioLeaveRInst = True }
+ fo = fitsIn fiOpts (fiEnv env) uid subst' t1' t2'
+ varMp = foVarMp fo
+ tRes = varMp |=> foTy fo -- hum, I would assume that this substitution is already applied by fitsIn...?!
+
+ chk (EqsByCongruence t1 t2 obls)
+ = if foHasErrs fo || null preds
+ then Nothing
+ else return varMp
+ where
+ t1' = subst' |=> t1 -- todo: check if these substitutions a really needed (maybe its already done by the solver before calling chk)
+ t2' = subst' |=> t2
+ obls' = subst' |=> obls
+ uid = fiUniq env
+ fiOpts = unifyFIOpts { fioUniq = uid, fioFitFailureToProveObl = True, fioBindRVars = FIOBindNoBut Set.empty, fioDontBind = fioDontBind (fiFIOpts env), fioPredAsTy = True, fioLeaveRInst = True }
+ fo = fitsIn fiOpts (fiEnv env) uid subst' t1' t2'
+ cnstrs = Map.keys (foGathCnstrMp fo)
+ preds = [ cpoPr p | (Prove p) <- cnstrs ]
+ ps = foldr PredSeq_Cons PredSeq_Nil preds
+ (PredSeq_Var v) = obls
+ varMp = v `varmpPredSeqUnit` ps |=> foVarMp fo
+
+ chk (UnequalTy t1 t2)
+ = if (subst' |=> t1) == (subst' |=> t2)
+ then Nothing
+ else return emptyVarMp
+
+ chk (EqualModuloUnification t1 t2)
+ | isTyVar t1 = return emptyVarMp
+ | isTyVar t2 = return emptyVarMp
+ where
+ isTyVar t = case (subst' |=> t) of
+ Ty_Var _ TyVarCateg_Plain -> True
+ _ -> False
+ {-
+ chk (EqualModuloUnification t1 t2)
+ = if foHasErrs fo
+ then Nothing
+ else return emptyVarMp
+ where
+ t1' = subst' |=> t1
+ t2' = subst' |=> t2
+ uid = fiUniq env
+ fiOpts = unifyFIOpts { fioUniq = uid, fioPredAsTy = True, fioLeaveRInst = True }
+ fo = fitsIn fiOpts (fiEnv env) uid subst' t1' t2'
+ -}
+%%]]
chk _
= Nothing
%%]
View
25 EHC/src/ehc/Pred/CommonCHR.chs
@@ -44,6 +44,15 @@ data RedHowAnnotation
%%[[13
| RedHow_Lambda !UID !PredScope
%%]]
+%%[[16
+ | RedHow_ByEqSymmetry
+ | RedHow_ByEqTrans
+ | RedHow_ByEqCongr
+ | RedHow_ByEqTyReduction !Ty !Ty
+ | RedHow_ByPredSeqUnpack
+ | RedHow_ByEqFromAssume
+ | RedHow_ByEqIdentity
+%%]]
deriving (Eq, Ord)
%%]
@@ -65,6 +74,15 @@ instance PP RedHowAnnotation where
%%[[13
pp (RedHow_Lambda i sc) = "lambda" >#< i >#< sc
%%]]
+%%[[16
+ pp (RedHow_ByEqSymmetry) = pp "eqsym"
+ pp (RedHow_ByEqTrans ) = pp "eqtrans"
+ 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_ByEqIdentity) = pp "identity"
+%%]]
%%]
pp (RedHow_ByInstance s p sc) = "inst" >#< s >|< sc >#< "::" >#< p
@@ -141,6 +159,13 @@ instance ForceEval RedHowAnnotation where
fevCount (RedHow_ProveObl i sc) = cm1 "RedHow_ProveObl" `cmUnion` fevCount i `cmUnion` fevCount sc
fevCount (RedHow_Assumption vun sc) = cm1 "RedHow_Assumption" `cmUnion` fevCount vun `cmUnion` fevCount sc
fevCount (RedHow_ByScope ) = cm1 "RedHow_ByScope"
+ fevCount (RedHow_ByEqSymmetry ) = cm1 "RedHow_ByEqSymmetry"
+ fevCount (RedHow_ByEqTrans ) = cm1 "RedHow_ByEqTrans"
+ 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_ByEqIdentity ) = cm1 "RedHow_ByEqIdentity"
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
%%]]
View
11 EHC/src/ehc/Pred/EvidenceToCore.chs
@@ -86,7 +86,7 @@ evidMpToCore env evidMp
$ evidMp'
, concat ambigs
)
- where (evidMp',ambigs) = unzip [ ((i,ev3),as) | (i,ev) <- Map.toList evidMp, let (ev2,as) = splitAmbig ev ; ev3 = strip ev2 ]
+ where (evidMp',ambigs) = unzip [ ((i,ev3),as) | (i,ev) <- filter (not.ignore) (Map.toList evidMp), let (ev2,as) = splitAmbig ev ; ev3 = strip ev2 ]
mke (RedHow_ProveObl i _,ev) st = fst $ mk1 st (Just i) ev
mk1 st mbevk ev@(Evid_Proof p info evs)
= ins (insk || isJust mbevk) evk evnm ev c sc (Set.unions (uses : map tcrUsed rs)) (st' {tcsUniq=u'})
@@ -136,6 +136,15 @@ evidMpToCore env evidMp
%%[[13
ann (RedHow_Lambda i sc) [body] = ( [mkHNm i] `mkCExprLam` tcrCExpr body, sc )
%%]]
+%%[[16
+ ignore (_, (Evid_Proof _ red _))
+ | red `elem` [RedHow_ByEqSymmetry, RedHow_ByEqTrans, RedHow_ByEqCongr, RedHow_ByPredSeqUnpack, RedHow_ByEqFromAssume, RedHow_ByEqIdentity]
+ = True
+ ignore (_, (Evid_Proof _ (RedHow_ByEqTyReduction _ _) _))
+ = True
+%%]]
+ ignore _ = False
+
strip (Evid_Proof _ RedHow_ByScope [ev]) = strip ev
strip (Evid_Proof p i evs ) = Evid_Proof p i (map strip evs)
strip ev = ev
View
38 EHC/src/ehc/Pred/Heuristics.chs
@@ -264,9 +264,45 @@ anncmpEHCScoped env ann1 ann2
(HeurRed (RedHow_BySuperClass _ _ _) _, _ ) -> P_GT
(_ , HeurRed (RedHow_BySuperClass _ _ _) _) -> P_LT
(HeurRed RedHow_ByScope [HeurAlts p _], HeurRed RedHow_ByScope [HeurAlts q _]) -> toPartialOrdering $ pscpCmpByLen (cpoScope p) (cpoScope q)
+ (HeurRed RedHow_ByScope _ , _ ) -> P_LT
+ (_ , HeurRed RedHow_ByScope _ ) -> P_GT
+ _ -> error ("anncmpEHCScoped: don't know how to deal with:\n " ++ show (pp ann1) ++ "\n " ++ show (pp ann2))
+
+cmpEqReds :: RedHowAnnotation -> RedHowAnnotation -> PartialOrdering
+%%[[16
+cmpEqReds RedHow_ByEqIdentity _ = P_GT
+cmpEqReds _ RedHow_ByEqIdentity = P_LT
+cmpEqReds RedHow_ByPredSeqUnpack _ = P_GT
+cmpEqReds _ RedHow_ByPredSeqUnpack = P_LT
+cmpEqReds RedHow_ByEqFromAssume _ = P_GT
+cmpEqReds _ RedHow_ByEqFromAssume = P_LT
+cmpEqReds (RedHow_Assumption _ _) _ = P_GT
+cmpEqReds _ (RedHow_Assumption _ _) = P_LT
+cmpEqReds (RedHow_ByEqTyReduction _ _) _ = P_GT
+cmpEqReds _ (RedHow_ByEqTyReduction _ _) = P_LT
+cmpEqReds RedHow_ByEqCongr _ = P_GT
+cmpEqReds _ RedHow_ByEqCongr = P_LT
+cmpEqReds RedHow_ByEqTrans _ = P_GT
+cmpEqReds _ RedHow_ByEqTrans = P_LT
+cmpEqReds RedHow_ByEqSymmetry _ = P_GT
+cmpEqReds _ RedHow_ByEqSymmetry = P_LT
+%%]]
+cmpEqReds r1 r2 = error ("cmpEqReds: don't know how to deal with: " ++ show (pp r1) ++ " and " ++ show (pp r2))
heurScopedEHC :: FIIn -> Heuristic CHRPredOcc RedHowAnnotation
-heurScopedEHC env = toHeuristic $ contextBinChoice (anncmpEHCScoped env)
+heurScopedEHC env = toHeuristic $ ifthenelseSHeuristic isEqHeuristic eqHeuristic defaultHeuristic
+ where
+%%[[16
+ isEqHeuristic (CHRPredOcc (Pred_Eq _ _) _) = True
+%%]]
+ isEqHeuristic _ = False
+ eqHeuristic = binChoice cmpEqReds . solvable
+ defaultHeuristic = contextBinChoice (anncmpEHCScoped env)
+
+ifthenelseSHeuristic :: (p -> Bool) -> SHeuristic p info -> SHeuristic p info -> SHeuristic p info
+ifthenelseSHeuristic g t e alts
+ | g (redaltsPredicate alts) = t alts
+ | otherwise = e alts
%%]
%%[9
View
16 EHC/src/ehc/Pred/RedGraph.chs
@@ -4,7 +4,7 @@
Derived from work by Gerrit vd Geest.
-%%[9 module {%{EH}Pred.RedGraph} import({%{EH}Base.Common},{%{EH}Ty},{%{EH}VarMp})
+%%[9 module {%{EH}Pred.RedGraph} import({%{EH}Base.Common},{%{EH}Ty},{%{EH}VarMp}, Data.Maybe)
%%]
%%[9 import({%{EH}CHR.Constraint},{%{EH}CHR.Constraint})
@@ -13,7 +13,7 @@ Derived from work by Gerrit vd Geest.
%%[9 import({%{EH}Pred.Heuristics})
%%]
-%%[9 import(qualified Data.Map as Map)
+%%[9 import(qualified Data.Map as Map, Data.Map(Map), Data.Set(Set), qualified Data.Set as Set)
%%]
%%[9 import(EH.Util.AGraph,EH.Util.Pretty) export(module EH.Util.AGraph)
@@ -104,9 +104,15 @@ addReduction _ = id
%%[9 export(redAlternatives)
redAlternatives :: (Ord p {-, PP p, PP info debug -}) => RedGraph p info -> p -> HeurAlts p info
-redAlternatives gr = recOr
- where recOr p = HeurAlts p (map recAnd (successors gr (Red_Pred p)))
- recAnd (i, n) = HeurRed i (map recOr (preds n))
+redAlternatives gr = recOr Set.empty
+ where recOr visited p = HeurAlts p (mapMaybe (recAnd visited') (successors gr (Red_Pred p)))
+ where visited' = Set.insert p visited
+
+ recAnd visited (i, n)
+ | any (`Set.member` visited) qs = Nothing
+ | otherwise = return $ HeurRed i (map (recOr visited) qs)
+ where qs = preds n
+
preds n = case n of
Red_Pred q -> [q]
Red_And qs -> qs
View
45 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]
+ ,[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]
+ , map mkTyVar [u10,u11,u14,u15]
, map Label_Var [u12]
, map LabelOffset_Var [u13]
%%]]
@@ -100,10 +100,17 @@ 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] = mkNewLevUIDL 13 uidStart
+ where [u1,u2,u3,u4,u5,u6,u7,u8,u9,u10,u11,u12,u13,u14,u15] = mkNewLevUIDL 15 uidStart
%%]]
%%]
+CHR rules for proving constraints. These rules have to obey the invariant that
+the new proof obligations are individually weaker than the original proof
+obligations, i.e. that there is no sequence of reductions that can lead from the
+new proof obligations to the original ones.
+
+In terms of entailment: for a CHR rule H => B, B may not entail H.
+
%%[9 export(initScopedPredStore)
initScopedPredStore :: ScopedPredStore
initScopedPredStore
@@ -115,6 +122,10 @@ initScopedPredStore
%%[[13
++ [ instForall, predArrow, predSeq1, predSeq2 ]
%%]]
+%%[[16
+ -- comment out predSeq1 and predSeq2 above because they conflict with the unpack rules!
+ ++ [ {-rlEqScope,-} rlEqTrans, rlEqSym, rlEqCongr, rlUnpackCons , {- rlCtxToNil, -} rlEqSymPrv, rlEqTransPrv, rlEqCongrPrv, rlUnpackConsPrv, rlUnpackNilPrv, rlPrvByAssume, rlPrvByIdentity ]
+%%]]
where p1s1 = mkCHRPredOcc pr1 sc1
p1s2 = mkCHRPredOcc pr1 sc2
p1s3 = mkCHRPredOcc pr1 sc3
@@ -157,6 +168,34 @@ initScopedPredStore
predSeq2 = [Prove $ mkCHRPredOcc (Pred_Preds PredSeq_Nil) sc1]
<==> []
%%]]
+%%[[16
+ 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
+ eqT2T3s2 = mkCHRPredOcc (Pred_Eq ty2 ty3) sc2
+ 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
+
+ rlEqSym = [Assume eqT1T2s1] ==> [Assume eqT2T1s1] -- symmetry
+ rlEqTrans = [Assume eqT1T2s1, Assume eqT2T3s2] ==> [Assume eqT1T3s1] |> [IsVisibleInScope sc2 sc1] -- 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 eqT2T3s2] ==> [Prove eqT1T3s1, Reduction eqT1T2s1 RedHow_ByEqTrans [eqT1T3s1]] |> [IsVisibleInScope sc2 sc1, 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 eqT1T2s2] ==> [Reduction eqT1T2s1 RedHow_ByEqFromAssume []] |> [IsVisibleInScope sc2 sc1] -- dirty hack: generated assumptions by chr are not added to the graph, so made a reduction instead
+ rlPrvByIdentity = [Prove eqT1T2s1] ==> [Reduction eqT1T2s1 RedHow_ByEqIdentity []] |> [EqualModuloUnification ty1 ty2]
+
+%%]]
-- inclSc = ehcCfgCHRInclScope $ feEHCOpts $ fiEnv env
%%]
View
2  EHC/src/ehc/Scanner/Common.chs
@@ -262,7 +262,7 @@ hiScanOpts
, "Assume", "Prove", "Reduction"
, "scope"
, "HasStrictCommonScope", "IsStrictParentScope", "IsVisibleInScope", "EqualScope", "NotEqualScope"
- , "redhowinst", "redhowsuper", "redhowprove", "redhowassume", "redhowscope"
+ , "redhowinst", "redhowsuper", "redhowprove", "redhowassume", "redhowscope", "redhoweqsym", "redhoweqtrans", "redhoweqcongr"
, "varuidnmname", "varuidnmuid", "varuidnmvar"
%%]]
%%[[10
View
3  EHC/src/ehc/Ty.cag
@@ -984,6 +984,9 @@ predTy p
%%[10 hs
Pred_Lacks t _ -> t
%%]
+%%[16 hs
+ Pred_Eq t _ -> t -- does it matter if we return the left or the right type?
+%%]
%%[13 hs export(predSeqToList,predLFlatten)
predSeqToList :: PredSeq -> [Pred]
View
24 EHC/src/ehc/Ty/AbsSyn.cag
@@ -7,6 +7,24 @@
%%% Abstract syntax for Ty
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+There are some conventions/restrictions on the structure of types that are not enforced
+by the abstract syntax:
+
+Encoding of prove-constraints:
+ concrete syntax:
+ {! impls !} -> ty
+ abstract syntax:
+ Ty_App (Ty_App (Ty_Con "->") (Ty_Impls impls)) ty
+
+Encoding of assume-constraints:
+ concrete syntax:
+ (ty, {! pred1 !}, ..., {! predn !})
+ abstract syntax:
+ Ty_Ext (... (Ty_Ext ty (prod m+1) (Ty_Pred pred_1) ) ...) (prod m+n) (Ty_Pred pred_n)
+
+ In other words: the predicates are at the outset of a product, pred_n "more outermost"
+ than pred_{n-1}.
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Top level
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -223,6 +241,12 @@ DATA PredSeq
| Nil
%%]
+%%[16
+DATA Pred
+ | Eq tyL : Ty
+ tyR : Ty
+%%]
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% CHR specific
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
View
100 EHC/src/ehc/Ty/FitsIn.chs
@@ -56,6 +56,9 @@
%%[10 import({%{EH}Core.Utils})
%%]
+%%[16 import(Debug.Trace)
+%%]
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Coercion application
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -370,6 +373,36 @@ fitsInFI fi ty1 ty2
else id
%%]
+%%[16.fitsIn.eqProofAssume
+ eqAssume p fi t1 t2 isRec isSum
+ = out { foGathCnstrMp = foGathCnstrMp out `Map.union` mp }
+ where
+ mp = cnstrMpFromList [cnstr]
+ cnstr = mkAssumeConstraint p lUniq scope
+ scope = fePredScope $ fiEnv fi
+ (gUniq,lUniq) = mkNewLevUID (fiUniq fi)
+ fi' = fi { fiUniq = gUniq }
+ out = fRow fi' t1 t2 isRec isSum
+%%]
+
+%%[16.fitsIn.eqProofObligation
+ eqProofObligation tRes fi tL tR
+ = (res fi tRes) { foGathCnstrMp = mp }
+ where
+ mp = cnstrMpFromList [cnstr]
+ cnstr = mkProveConstraint (Pred_Eq tL tR) uid scope
+ scope = fePredScope $ fiEnv fi
+ uid = fiUniq fi
+%%]
+
+%%[16.fitsIn.isSkVar
+ -- is skolemnized tyvar?
+ isSkVar = isSkVar' . show
+
+ isSkVar' ('C':'_':_) = True
+ isSkVar' _ = False
+%%]
+
%%[4.fitsIn.FOUtils
foUpdVarMp c fo = fo {foVarMp = c |=> foVarMp fo}
foSetVarMp c fo = fo {foVarMp = c}
@@ -449,6 +482,12 @@ fitsInFI fi ty1 ty2
(zip tL1 tL2)
%%]
+GADT: when encountering a product with eq-constraints on the outset, remove them and bring them in scope as assume constraints
+%%[16.fitsIn.fRow.StripPreds
+ fRow fi (Ty_Ext t1 _ (Ty_Pred p)) t2 isRec isSum = eqAssume p fi t1 t2 isRec isSum
+ fRow fi t1 (Ty_Ext t2 _ (Ty_Pred p)) isRec isSum = eqAssume p fi t1 t2 isRec isSum
+%%]
+
%%[7.fitsIn.fRow.Base
fRow fi tr1 tr2 isRec isSum
= foR
@@ -930,6 +969,21 @@ fitsInFI fi ty1 ty2
= fRow fi t1 t2 False False
%%]
+FitsIn type clashes
+
+GADT: type clash between fixed type variable and some other type results in a equality proof constraint
+%%[16.fitsIn.EqProve
+ f fi t1@(Ty_Var v1 TyVarCateg_Fixed) t2 | fioFitVarFailureToProveObl (fiFIOpts fi) = eqProofObligation t2 fi t1 t2
+ f fi t1 t2@(Ty_Var v2 TyVarCateg_Fixed) | fioFitVarFailureToProveObl (fiFIOpts fi) = eqProofObligation t2 fi t2 t1
+ f fi t1@(Ty_Con cstr) t2 | isSkVar cstr && fioFitVarFailureToProveObl (fiFIOpts fi) = eqProofObligation t2 fi t1 t2
+ f fi t1 t2@(Ty_Con cstr) | isSkVar cstr && fioFitVarFailureToProveObl (fiFIOpts fi) = eqProofObligation t2 fi t2 t1
+
+ f fi t1 t2
+ | fioFitFailureToProveObl (fiFIOpts fi)
+ && t1 /= ty1 && t2 /= ty2 -- only generate proof obligations for type clashes when there is at least a partial match
+ = eqProofObligation t1 fi t1 t2
+%%]
+
%%[4.fitsIn.DefaultCase
f fi t1 t2 = errClash fi t1 t2
%%]
@@ -1005,6 +1059,52 @@ fitPredIntoPred fi pr1 pr2
| tyIsEmptyRow ty1 && tyIsEmptyRow ty2
= Just (Pred_Lacks ty2 l2, lv1 `varmpLabelUnit` l2)
%%]]
+%%[[13
+ -- assumption: a PredSeq_Var can only occur as a tail in a PredSeq
+ f (Pred_Preds ps1) (Pred_Preds ps2)
+ = do (ps, varMp) <- fPreds ps1 ps2
+ return (Pred_Preds ps, varMp)
+ where
+ fPreds ps@(PredSeq_Var v1) (PredSeq_Var v2)
+ | v1 == v2
+ = Just (ps, emptyVarMp)
+ fPreds (PredSeq_Var v1) ps
+ = Just (ps, v1 `varmpPredSeqUnit` ps)
+ fPreds ps (PredSeq_Var v1)
+ = Just (ps, v1 `varmpPredSeqUnit` ps)
+ fPreds (PredSeq_Cons pr1 ps1) (PredSeq_Cons pr2 ps2)
+ = do (pr', s1) <- f pr1 pr2
+ (ps', s2) <- fPreds (s1 |=> ps1) (s1 |=> ps2)
+ return (PredSeq_Cons pr' ps', s2 |=> s1)
+ fPreds PredSeq_Nil PredSeq_Nil
+ = Just (PredSeq_Nil, emptyVarMp)
+ fPreds _ _
+ = Nothing
+%%]]
+%%[[16
+ f (Pred_Eq tlA trA) (Pred_Eq tlB trB)
+ = if foHasErrs foL || foHasErrs foR
+ then Nothing
+ else Just $ (Pred_Eq tlOut trOut, varMpOut)
+ where
+ (u1, u2, u3, u4) = mkNewLevUID3 (fiUniq fi)
+
+ fiOptsL = unifyFIOpts { fioUniq = u3, fioBindRVars = FIOBindNoBut Set.empty, fioDontBind = fioDontBind (fiFIOpts fi), fioPredAsTy = True, fioLeaveRInst = True }
+ fiOptsR = unifyFIOpts { fioUniq = u4, fioBindRVars = FIOBindNoBut Set.empty, fioDontBind = fioDontBind (fiFIOpts fi), fioPredAsTy = True, fioLeaveRInst = True }
+
+ foL = fitsIn fiOptsL (fiEnv fi) u1 varMp1In tlA tlB
+ foR = fitsIn fiOptsR (fiEnv fi) u2 varMp2In trA trB
+
+ varMp1In = fiVarMp fi
+ varMp2In = varMp1Out |=> fiVarMp fi
+
+ varMp1Out = foVarMp foL
+ varMp2Out = foVarMp foR
+ varMpOut = varMp2Out |=> varMp1Out
+
+ tlOut = varMpOut |=> foTy foL
+ trOut = varMpOut |=> foTy foR
+%%]]
f pr1 pr2
= if foHasErrs fo
then Nothing
View
5 EHC/src/ehc/Ty/Ftv.cag
@@ -80,6 +80,11 @@ SEM PredSeq
| Var lhs . tvMp = @av `Map.singleton` TyVarCateg_Plain
%%]
+%%[16
+SEM Pred
+ | Eq lhs . tvMp = @tyL.tvMp `Map.union` @tyR.tvMp
+%%]
+
%%[50
SEM Ty
| Equal lhs . tvs = [@tv] `union` @ty.tvs
View
12 EHC/src/ehc/Ty/Pretty.cag
@@ -126,6 +126,13 @@ instance PP ImplsProveOcc where
pp o = ipoId o >|< "/" >|< ipoScope o
%%]
+%%[16 hs
+instance PP PredSeq where
+ pp (PredSeq_Cons hd tl) = pp hd >#< ":" >#< pp tl
+ pp (PredSeq_Nil ) = pp "[]"
+ pp (PredSeq_Var u ) = pp u
+%%]
+
%%[10 hs
instance PP LabelOffset where
pp = pp . show
@@ -574,6 +581,11 @@ SEM Ty
(cfgppAside @lhs.cfg ("\\" >|< @tnPP) ("->" >#< @ty.pp))
%%]
+%%[16
+SEM Pred
+ | Eq lhs . pp = ppParNeed @parNeed @lhs.parNeed (@tyL.pp >#< "=" >#< @tyR.pp)
+%%]
+
%%[50
SEM Ty
| Equal loc . pp = ppParens (maybe (cfgPPTyPPVarDflt @lhs.cfg @lhs.cfg "e" @tv) id (tnLookupPP @tv @lhs.tnMap) >|< "=" >|< @ty.pp)
View
10 EHC/src/ehc/Ty/Trf/Canonic.cag
@@ -23,6 +23,9 @@ This matters for:
%%[11 hs import({%{EH}Base.Opts})
%%]
+%%[16 hs import({%{EH}Ty.Trf.MergePreds})
+%%]
+
%%[9.WRAPPER ag import({Ty/AbsSyn},{Ty/CommonAG})
WRAPPER TyAGItf
%%]
@@ -51,6 +54,13 @@ tyCanonic fi ty
%%[9 hs export(predCanonic)
predCanonic :: FIIn -> Pred -> Pred
+%%[[16
+predCanonic fi (Pred_Eq t1 t2)
+ = Pred_Eq (tmpoTy $ tyMergePreds [] t1') (tmpoTy $ tyMergePreds [] t2')
+ where
+ t1' = tyCanonic fi t1
+ t2' = tyCanonic fi t2
+%%]]
predCanonic fi pr
= case tyCanonic fi $ Ty_Pred pr of
Ty_Pred pr' -> pr'
View
53 EHC/src/ehc/Ty/Trf/Subst.cag
@@ -27,21 +27,43 @@ tyAppVarMp varmp ty
%%]
%%[4 -2.tyAppVarMp hs export(tyAppVarMp,tyAppVarMp2)
-tyAppVarMp' :: VarMp -> TVUseMp -> Ty -> (Ty,VarMp)
-tyAppVarMp' varmp usemp ty
+tyAppVarMp' :: SubstOpts -> VarMp -> TVUseMp -> Ty -> (Ty,VarMp)
+tyAppVarMp' opts varmp usemp ty
= (repl_Syn_TyAGItf t,cycVarMp_Syn_TyAGItf t)
where t = wrap_TyAGItf
(sem_TyAGItf (TyAGItf_AGItf ty))
- (Inh_TyAGItf {varmp_Inh_TyAGItf = varmp, tvUseMp_Inh_TyAGItf = usemp})
+ (Inh_TyAGItf {varmp_Inh_TyAGItf = varmp, tvUseMp_Inh_TyAGItf = usemp, substOpts_Inh_TyAGItf = opts })
tyAppVarMp :: VarMp -> Ty -> Ty
tyAppVarMp varmp ty
= ty'
- where (ty',_) = tyAppVarMp' varmp Map.empty ty
+ where (ty',_) = tyAppVarMp' defaultOpts varmp Map.empty ty
tyAppVarMp2 :: VarMp -> Ty -> (Ty,VarMp)
tyAppVarMp2 varmp ty
- = tyAppVarMp' varmp Map.empty ty
+ = tyAppVarMp' defaultOpts varmp Map.empty ty
+%%]
+
+%%[4.substOpts hs
+data SubstOpts
+ = SubstOpts
+
+defaultOpts :: SubstOpts
+defaultOpts = SubstOpts
+%%]
+
+%%[16.substOpts -4.substOpts hs
+data SubstOpts
+ = SubstOpts { onlySubstRHSOfEq :: Bool }
+
+defaultOpts :: SubstOpts
+defaultOpts = SubstOpts { onlySubstRHSOfEq = False }
+%%]
+
+%%[16 hs export (tyAppVarMp2_RhsOfEqOnly)
+tyAppVarMp2_RhsOfEqOnly :: VarMp -> Ty -> (Ty, VarMp)
+tyAppVarMp2_RhsOfEqOnly varmp ty
+ = tyAppVarMp' (SubstOpts { onlySubstRHSOfEq = True }) varmp Map.empty ty
%%]
%%[4
@@ -207,6 +229,10 @@ ATTR AllTyAndFlds [ | | repl: SELF ]
ATTR TyAGItf [ | | repl: Ty ]
%%]
+%%[4 ag
+ATTR TyAGItf AllTy [ substOpts: SubstOpts | | ]
+%%]
+
%%[10
ATTR LabelAGItf Label [ varmp: VarMp | | ]
ATTR LabelAGItf [ | | repl: Label ]
@@ -260,6 +286,23 @@ SEM PredSeq
else (@repl,emptyVarMp)
%%]
+%%[16
+
+-- if "onlySubstRHSOfEq" is True, then tyL is either a Var or a Con and the orig attribute is used and defined.
+-- The orig attribute is not used if "onlySubstRHSOfEq" is False. This setting is almost always False.
+
+ATTR Ty [ | | orig: Ty ]
+SEM Ty
+ | Var Con loc.orig = @loc.repl
+ | * - Var Con loc.orig = undefined
+
+SEM Pred
+ | Eq
+ lhs.repl = if onlySubstRHSOfEq @lhs.substOpts
+ then Pred_Eq @tyL.orig @tyR.repl
+ else @loc.repl
+%%]
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Don't construct/return new structure when no changes occur: currently useless as changes are always (i.e. 99% :-)) present
View
6 EHC/src/ehc/Ty/TrieKey.cag
@@ -165,6 +165,12 @@ SEM Pred
| RowSplit lhs . trieKey = singleton $ TK_One TKK_Normal $ Key_Str "|"
. trieKeyNest = @ty.trieKey :++: @exts.trieKey
+%%[16
+SEM Pred
+ | Eq lhs . trieKey = (singleton $ TK_One TKK_Normal $ Key_Str "=")
+ . trieKeyNest = @tyL.trieKey :++: @tyR.trieKey :++: @tyL.trieKeyNest :++: @tyR.trieKeyNest
+%%]
+
%%[10
SEM Label
| Lab lhs . trieKey = singleton $ TK_One TKK_Normal $ Key_HNm @nm
View
3  EHC/src/libutil/EH/Util/AGraph.hs
@@ -19,6 +19,7 @@ import Data.Graph.Inductive.Tree (Gr)
import Data.Graph.Inductive.Graphviz (graphviz')
import Data.Maybe (fromJust)
+import Data.List(nub)
data AGraph a b = AGr { agraphNodeMap :: NodeMap a, agraphGraph :: Gr a b}
@@ -38,7 +39,7 @@ deleteEdge (p, q) (AGr nm gr) = AGr nm (delEdge (getId p, getId q) gr)
insMapNodes :: Ord a => [a] -> AGraph a b -> AGraph a b
insMapNodes as (AGr m g) =
- let (ns, m') = mkNodes m as
+ let (ns, m') = mkNodes m (nub as)
ns' = filter (\(i, _) -> not $ gelem i g) ns
in AGr m' (insNodes ns' g)
View
3  EHC/test/regress/16/gadt3.eh
@@ -2,7 +2,8 @@ let data Term a
= LitI a, a = Int
| LitC a, a = Char
in
-let eval = \x -> case x of
+let eval :: Term a -> a
+ eval = \x -> case x of
LitI i -> i
LitC j -> j
in 3
View
27 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
View
14 EHC/test/regress/16/gadt5.eh
@@ -0,0 +1,14 @@
+let
+
+data IntTupleRep t
+ = Tup, t = (Int, Int)
+
+in let
+
+tupId :: IntTupleRep t -> t -> t
+tupId = \g -> \t ->
+ case g of
+ Tup -> case t of
+ (a,b) -> (a,b)
+
+in 3

No commit comments for this range

Something went wrong with that request. Please try again.