From aade7de19cb0595bdc1a52f096584044a432b2dc Mon Sep 17 00:00:00 2001 From: Atze Dijkstra Date: Thu, 27 Feb 2014 14:01:26 +0100 Subject: [PATCH] fix for issue #18, faulty defaulting inside instance decl --- EHC/src/ehc/EH/Infer.cag | 63 +++++++++++++++++++++++------- EHC/src/ehc/EH/ResolvePredCHR.cag | 2 +- EHC/test/regress/99/Defaulting1.hs | 30 ++++++++++++++ 3 files changed, 79 insertions(+), 16 deletions(-) create mode 100644 EHC/test/regress/99/Defaulting1.hs diff --git a/EHC/src/ehc/EH/Infer.cag b/EHC/src/ehc/EH/Infer.cag index 184bfd441..f4fb1d2f9 100755 --- a/EHC/src/ehc/EH/Infer.cag +++ b/EHC/src/ehc/EH/Infer.cag @@ -109,25 +109,17 @@ SEM Expr decls . patTyVarMp := @exTyVarMp1b %%[(9 hmtyinfer) hs --- | split a list of predicates into non-ambiguous & ambiguous, using quantifications results tqoGam, --- which (a.o.) administers which predicates could be merged for quantification, those not are then ambiguous -doPredAmbigSplit :: (x -> PredOcc) -> TQOGam -> [x] -> ([x],[x]) -doPredAmbigSplit get tqoGam prOccL - = partition (\o -> poPoi (get o) `Set.member` assumedByQuant) prOccL - where assumedByQuant = Set.unions $ map tmpoInsPrIdSet $ gamElts tqoGam +-- | Construct a function which does quantification given some fixed environmental info +mkDoValGamQuantify + :: TyKiGam -> VarMp -> TyVarIdS -> ValGam + -> (Bool -> VarMp -> [PredOcc] -> (ValGam, VarMp, (VarMp, TQOGam))) +mkDoValGamQuantify valQuTyKiGam quTvKiVarMp noLetQuantTyVarIdS valGam_l_ + = \doQuant tyVarMp prOccL -> valGamQuantifyWithVarMp doQuant valQuTyKiGam quTvKiVarMp tyVarMp noLetQuantTyVarIdS prOccL valGam_l_ %%] %%[(9 hmtyinfer) SEM Expr - | Let loc . doValGamQuantify = \doQuant tyVarMp prOccL -> valGamQuantifyWithVarMp doQuant @valQuTyKiGam @quTvKiVarMp tyVarMp @noLetQuantTyVarIdS prOccL @valGam_l_ - . doPredAmbigSplitForSimplify - = \chrPrOccL - -> let us = mkNewLevUIDL (length chrPrOccL) uidStart - -- couple with arbitrary id's to make quantify & split work - prOccL = zipWith (\u (o,_) -> cpo2PredOcc (mkPrId u) o) us chrPrOccL - (_,_, (_,tqoGam)) = @doValGamQuantify False @tyVarMpDeclsL01 prOccL - (namb,amb) = doPredAmbigSplit fst tqoGam $ zip prOccL chrPrOccL - in (map snd amb, map snd namb) + | Let loc . doValGamQuantify = mkDoValGamQuantify @valQuTyKiGam @quTvKiVarMp @noLetQuantTyVarIdS @valGam_l_ . (quValGam_qu_,quTyVarMp, (cycTyVarMp_l,tqoGam)) := @doValGamQuantify True @tyVarMpDeclsQuant @toQuantOverPrOccL . tmpoTyVarMp = foldr (\tmpo c -> tmpoImplsVarMp tmpo `varUpd` c) emptyVarMp (gamElts @tqoGam) @@ -147,6 +139,47 @@ SEM Expr @bodyVarMp2 `varUpd` @lhs.tyVarMp +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%% Split for ambiguity check, required for defaulting +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%[(9 hmtyinfer) hs +-- | split a list of predicates into non-ambiguous & ambiguous, using quantifications results tqoGam, +-- which (a.o.) administers which predicates could be merged for quantification, those not are then ambiguous +doPredAmbigSplit :: (x -> PredOcc) -> TQOGam -> [x] -> ([x],[x]) +doPredAmbigSplit get tqoGam prOccL + = partition (\o -> poPoi (get o) `Set.member` assumedByQuant) prOccL + where assumedByQuant = Set.unions $ map tmpoInsPrIdSet $ gamElts tqoGam + +-- | Split predicates according to whether the predicate combining part of quantification can be done +mkDoPredAmbigSplitForSimplify :: (Bool -> vm -> [PredOcc] -> (dum1,dum2,(dum3,TQOGam))) -> vm -> [(CHRPredOcc, x)] -> ([(CHRPredOcc, x)],[(CHRPredOcc, x)]) +mkDoPredAmbigSplitForSimplify doValGamQuantify tyVarMpDeclsL01 + = \chrPrOccL + -> let us = mkNewLevUIDL (length chrPrOccL) uidStart + -- couple with arbitrary id's to make quantify & split work + prOccL = zipWith (\u (o,_) -> cpo2PredOcc (mkPrId u) o) us chrPrOccL + (_,_, (_,tqoGam)) = doValGamQuantify False tyVarMpDeclsL01 prOccL + (namb,amb) = doPredAmbigSplit fst tqoGam $ zip prOccL chrPrOccL + in (map snd amb, map snd namb) +%%] + +%%[(9 hmtyinfer) +SEM Expr + | Let loc . doPredAmbigSplitForSimplify + = mkDoPredAmbigSplitForSimplify @doValGamQuantify @tyVarMpDeclsL01 +%%] + +%%[(9 hmtyinfer) +SEM Decl + | Instance loc . doPredAmbigSplitForSimplify + = mkDoPredAmbigSplitForSimplify + (mkDoValGamQuantify + @lhs.finTyKiGam @lhs.tvKiVarMp + (setSubst @tyVarMpDeclsL0 @decls.noLetQuantTyVarIdS) + (gamTop @decls.patValGam)) + @tyVarMpDeclsL01 +%%] + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Restriction of @decls.tyVarMp to meta level 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/EHC/src/ehc/EH/ResolvePredCHR.cag b/EHC/src/ehc/EH/ResolvePredCHR.cag index 543aed1bb..20202dad5 100644 --- a/EHC/src/ehc/EH/ResolvePredCHR.cag +++ b/EHC/src/ehc/EH/ResolvePredCHR.cag @@ -510,7 +510,7 @@ SEM Decl %%]] ) = ehcOptTrace @lhs.opts "Decl.Instance.simplify1" $ - simplify [SimplifyHow_Canonicalize] (@chrProveFIIn {fiUniq = @lUniq7}) @lhs.chrStore @lhs.clDfGam (heurScopedEHC @chrProveFIIn) ((,) []) Map.empty @toProveDeclsCnstrMp emptySimplifyResult + simplify [SimplifyHow_Canonicalize] (@chrProveFIIn {fiUniq = @lUniq7}) @lhs.chrStore @lhs.clDfGam (heurScopedEHC @chrProveFIIn) @doPredAmbigSplitForSimplify Map.empty @toProveDeclsCnstrMp emptySimplifyResult . (chrSolveDeclsState,chrSolveDeclsRedGraph,chrSolveDeclsDoneConstraints,chrSolveDeclsTrace,_,_,_) = debugInfo @chrDeclsSimplifyResult diff --git a/EHC/test/regress/99/Defaulting1.hs b/EHC/test/regress/99/Defaulting1.hs new file mode 100644 index 000000000..6ee980881 --- /dev/null +++ b/EHC/test/regress/99/Defaulting1.hs @@ -0,0 +1,30 @@ +{- ---------------------------------------------------------------------------------------- + what : correct defaulting to Integer in instance decl, due to bug not doing so + expected: ok +---------------------------------------------------------------------------------------- -} + +module Defaulting1 where + +f :: Num a => a -> () +f _ = () + +class C a where + it :: a + + +-- fix of previous bug: +-- Here I get a type error: +-- Test.hs:14-15: +-- Predicates remain unproven: +-- preds: UHC.Base.Num v_3_190_2 +-- at : +-- trace: (UHC.Base.Num v_3_190_2,<4,0>,Test.hs:15:8): FAIL +-- (UHC.Base.Num v_3_190_2,<4,0>,Test.hs:15:8): FAIL +instance C () where + it = f 0 + +-- This one compiles fine. +it' :: () +it' = f 0 + +main = print (it :: ())