git.iko.soy/Idris-dev
on master help sign in
Disable forcing and collapsibility (dirty hack).
eea9302Matus Tejiscak
src/IRTS/Compiler.hs+5−4
compare with master
unifiedsplit
@@ -324,10 +324,11 @@ instance ToIR (TT Name) where
324
324
325getFTypes :: TT Name -> Maybe [FType]
325getFTypes :: TT Name -> Maybe [FType]
326getFTypes tm = case unApply tm of
326getFTypes tm = case unApply tm of
327+ -- nil : {a : Type} -> List a
327− (nil, []) -> Just []
328+ (nil, [_]) -> Just []
328− (cons, [ty, xs]) ->
329+ -- cons : {a : Type} -> a -> List a -> List a
329− fmap (mkIty' ty :) (getFTypes xs)
330+ (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
330− _ -> Nothing
331+ _ -> Nothing
331
332
332mkIty' (P _ (UN ty) _) = mkIty (str ty)
333mkIty' (P _ (UN ty) _) = mkIty (str ty)
333mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
334mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
src/Idris/DataOpts.hs+2−2
@@ -33,7 +33,7 @@ forceArgs typeName n expforce t = do
33 iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++ show t
33 iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++ show t
34
34
35getForcedArgs :: IState -> Name -> Type -> ForceMap
35getForcedArgs :: IState -> Name -> Type -> ForceMap
36−getForcedArgs ist typeName t = addCollapsibleArgs 0 t $ forcedInTarget 0 t
36+getForcedArgs ist typeName t = M.empty -- addCollapsibleArgs 0 t $ forcedInTarget 0 t
37 where
37 where
38 maxUnion = M.unionWith max
38 maxUnion = M.unionWith max
39
39
@@ -91,7 +91,7 @@ collapseCons tn ctors = do
91 _
91 _
92 | all (ctorCollapsible ist) ctors
92 | all (ctorCollapsible ist) ctors
93 , disjointTerms ctorTargetArgs
93 , disjointTerms ctorTargetArgs
94− -> mapM_ setCollapsible (tn : map fst ctors)
94+ -> return () -- mapM_ setCollapsible (tn : map fst ctors)
95
95
96 [(cn, ct)]
96 [(cn, ct)]
97 -> checkNewType ist cn ct
97 -> checkNewType ist cn ct