0679225 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

Now matches on values before indices, to give a chance of erasing indices.

commit0679225fff224624ae50e549e8085c8a0040d7d8 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 8 Oct 2012, 17:00 (14 years ago) parent20d5a61

2 files changed+8−7

compare with master

unifiedsplit

src/Core/CaseTree.hs+6−5 src/Idris/REPLParser.hs+2−2

src/Core/CaseTree.hs+6−5

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

6666simpleCase tc cover fc []

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

6868simpleCase 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

7071 chkPats = mapM chkAccessible pats in

7172 case chkPats of

7273 OK pats ->

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

7475 ns = take numargs args

7576 (tree, st) = runState

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

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

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

7879 Error err -> Error (At fc err)

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

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

123124 then return PAny

124125 else do put (n : ns)

125126 return (PV n)

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

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

128− toPat' _ _ = return PAny

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

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

129+ toPat' _ _ = return PAny

129130

130131

131132data Partition = Cons [Clause]

src/Idris/REPLParser.hs+2−2

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

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

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

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

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

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

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

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

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

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

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