Generated names need to be unique in clauses

Otherwise we might think we've dealt with an erased name when we haven't
- given that clauses are compiled all together.
Fixes #186
This commit is contained in:
Edwin Brady 2020-01-19 16:36:30 +00:00
parent f81085cf67
commit 692bd8a547

View File

@ -927,20 +927,24 @@ getPMDef fc phase fn ty []
getArgs i _ = pure [] getArgs i _ = pure []
getPMDef fc phase fn ty clauses getPMDef fc phase fn ty clauses
= do defs <- get Ctxt = do defs <- get Ctxt
let cs = map (toClosed defs) clauses let cs = map (toClosed defs) (labelPat 0 clauses)
simpleCase fc phase fn ty Nothing cs simpleCase fc phase fn ty Nothing cs
where where
mkSubstEnv : Int -> Env Term vars -> SubstEnv vars [] labelPat : Int -> List a -> List (String, a)
mkSubstEnv i [] = Nil labelPat i [] = []
mkSubstEnv i (v :: vs) labelPat i (x :: xs) = ("pat" ++ show i ++ ":", x) :: labelPat (i + 1) xs
= Ref fc Bound (MN "pat" i) :: mkSubstEnv (i + 1) vs
close : Env Term vars -> Term vars -> ClosedTerm mkSubstEnv : Int -> String -> Env Term vars -> SubstEnv vars []
close {vars} env tm mkSubstEnv i pname [] = Nil
= substs (mkSubstEnv 0 env) mkSubstEnv i pname (v :: vs)
= Ref fc Bound (MN pname i) :: mkSubstEnv (i + 1) pname vs
close : Env Term vars -> String -> Term vars -> ClosedTerm
close {vars} env pname tm
= substs (mkSubstEnv 0 pname env)
(rewrite appendNilRightNeutral vars in tm) (rewrite appendNilRightNeutral vars in tm)
toClosed : Defs -> Clause -> (ClosedTerm, ClosedTerm) toClosed : Defs -> (String, Clause) -> (ClosedTerm, ClosedTerm)
toClosed defs (MkClause env lhs rhs) toClosed defs (pname, MkClause env lhs rhs)
= (close env lhs, close env rhs) = (close env pname lhs, close env pname rhs)