eea9302 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Disable forcing and collapsibility (dirty hack).

commiteea9302ec663a761febfb842e237c1607af02542 authorMatus Tejiscak <ziman@functor.sk> dateThu 13 Feb 2014, 14:18 (13 years ago) parenteeade97

2 files changed+7−6

unifiedsplit

src/IRTS/Compiler.hs+5−4

@@ -324,10 +324,11 @@ instance ToIR (TT Name) where

324324

325325getFTypes :: TT Name -> Maybe [FType]

326326getFTypes tm = case unApply tm of

327− (nil, []) -> Just []

328− (cons, [ty, xs]) ->

329− fmap (mkIty' ty :) (getFTypes xs)

330− _ -> Nothing

327+ -- nil : {a : Type} -> List a

328+ (nil, [_]) -> Just []

329+ -- cons : {a : Type} -> a -> List a -> List a

330+ (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs

331+ _ -> Nothing

331332

332333mkIty' (P _ (UN ty) _) = mkIty (str ty)

333334mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))

src/Idris/DataOpts.hs+2−2

@@ -33,7 +33,7 @@ forceArgs typeName n expforce t = do

3333 iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++ show t

3434

3535getForcedArgs :: 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

3737 where

3838 maxUnion = M.unionWith max

3939

@@ -91,7 +91,7 @@ collapseCons tn ctors = do

9191 _

9292 | all (ctorCollapsible ist) ctors

9393 , disjointTerms ctorTargetArgs

94− -> mapM_ setCollapsible (tn : map fst ctors)

94+ -> return () -- mapM_ setCollapsible (tn : map fst ctors)

9595

9696 [(cn, ct)]

9797 -> checkNewType ist cn ct