0679225 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Tweak match compilation (right to left, rather than l to r)

0679225Edwin Brady14 years ago

src/Core/CaseTree.hs+6−5

compare with master

unifiedsplit

@@ -66,14 +66,15 @@ simpleCase :: Bool -> Bool -> FC -> [([Name], Term, Term)] -> TC CaseDef

66simpleCase tc cover fc []

67 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []

68simpleCase tc cover fc cs

69− = let pats = map (\ (avs, l, r) -> (avs, toPats tc l, (l, r))) cs

69+ = let pats = map (\ (avs, l, r) ->

70+ (avs, reverse (toPats tc l), (l, r))) cs

70 chkPats = mapM chkAccessible pats in

71 chkPats = mapM chkAccessible pats in

71 case chkPats of

72 case chkPats of

72 OK pats ->

73 OK pats ->

73 let numargs = length (fst (head pats))

74 let numargs = length (fst (head pats))

74 ns = take numargs args

75 ns = take numargs args

75 (tree, st) = runState

76 (tree, st) = runState

76− (match ns pats (defaultCase cover)) ([], numargs) in

77+ (match (reverse ns) pats (defaultCase cover)) ([], numargs) in

77 return $ CaseDef ns (prune tree) (fst st)

78 return $ CaseDef ns (prune tree) (fst st)

78 Error err -> Error (At fc err)

79 Error err -> Error (At fc err)

79 where args = map (\i -> MN i "e") [0..]

80 where args = map (\i -> MN i "e") [0..]

@@ -123,9 +124,9 @@ toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []

123 then return PAny

124 then return PAny

124 else do put (n : ns)

125 else do put (n : ns)

125 return (PV n)

126 return (PV n)

126− toPat' (App f a) args = toPat' f (a : args)

127+ toPat' (App f a) args = toPat' f (a : args)

127− toPat' (Constant (I c)) [] = return $ PConst (I c)

128+ toPat' (Constant x@(I _)) [] = return $ PConst x

128− toPat' _ _ = return PAny

129+ toPat' _ _ = return PAny

129

130

131

131data Partition = Cons [Clause]

132data Partition = Cons [Clause]

src/Idris/REPLParser.hs+2−2

@@ -38,8 +38,8 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

38 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))

39 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

40 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

41− <|> try (do cmd ["d", "def"]; n <- pName; eof; return (Defn n))

41+ <|> try (do cmd ["d", "def"]; n <- pfName; eof; return (Defn n))

42− <|> try (do cmd ["total"]; do n <- pName; eof; return (TotCheck n))

42+ <|> try (do cmd ["total"]; do n <- pfName; eof; return (TotCheck n))

43 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))

44 <|> try (do cmd ["u", "universes"]; eof; return Universes)

45 <|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n))