Compute.ConcreteNew: bug fix for indirectly defined pattern macros

More changes are probably needed to make pattern macros first class values.
Also includes minor changes related to variants and error messages.
This commit is contained in:
hallgren
2012-12-06 16:44:03 +00:00
parent 32f085a4b5
commit 81f843ac06

View File

@@ -60,7 +60,7 @@ value env t0 =
then let p = identC (BS.pack "P") then let p = identC (BS.pack "P")
in value0 (fst env) (mkProd [(Implicit,p,typeType)] (Vr p) []) in value0 (fst env) (mkProd [(Implicit,p,typeType)] (Vr p) [])
else VApp x [] else VApp x []
| otherwise -> err bug (value0 (fst env)) (lookupResDef (fst env) x) | otherwise -> valueResDef (fst env) x
QC x -> VCApp x [] QC x -> VCApp x []
App e1 e2 -> apply' env e1 [value env e2] App e1 e2 -> apply' env e1 [value env e2]
Let (x,(oty,t)) body -> value (ext (x,value env t) env) body Let (x,(oty,t)) body -> value (ext (x,value env t) env) body
@@ -90,8 +90,11 @@ value env t0 =
Strs ts -> VStrs (map (value env) ts) Strs ts -> VStrs (map (value env) ts)
Glue t1 t2 -> glue (both (value env) (t1,t2)) Glue t1 t2 -> glue (both (value env) (t1,t2))
ELin c r -> unlockVRec c (value env r) ELin c r -> unlockVRec c (value env r)
EPatt p -> VPatt p -- hmm
t -> ppbug (text "value"<+>ppTerm Unqualified 10 t $$ text (show t)) t -> ppbug (text "value"<+>ppTerm Unqualified 10 t $$ text (show t))
valueResDef gr = err bug (value0 gr) . lookupResDef gr
vconcat vv@(v1,v2) = vconcat vv@(v1,v2) =
case vv of case vv of
(VError _,_) -> v1 (VError _,_) -> v1
@@ -236,10 +239,13 @@ valueTable env@(gr,bs) i cs =
sts <- mapM (matchPattern cs') vs sts <- mapM (matchPattern cs') vs
return $ VV pty (map (valueMatch gr) sts) return $ VV pty (map (valueMatch gr) sts)
inlinePattMacro p = case p of inlinePattMacro p =
PM qc -> do EPatt p' <- lookupResDef gr qc case p of
inlinePattMacro p' PM qc -> case valueResDef gr qc of
_ -> composPattOp inlinePattMacro p VPatt p' -> inlinePattMacro p'
r -> ppbug $ hang (text "Expected pattern macro:") 4
(text (show r))
_ -> composPattOp inlinePattMacro p
apply' env t [] = value env t apply' env t [] = value env t
apply' env t vs = apply' env t vs =
@@ -268,7 +274,7 @@ vbeta bt f (v:vs) =
(Implicit,VImplArg v) -> ap v (Implicit,VImplArg v) -> ap v
(Explicit, v) -> ap v (Explicit, v) -> ap v
where where
ap (VFV avs) = VFV [vapply (f v) vs|v<-avs] ap (VFV avs) = vfv [vapply (f v) vs|v<-avs]
ap v = vapply (f v) vs ap v = vapply (f v) vs
{- {-
@@ -339,4 +345,4 @@ both = apBoth
bug msg = ppbug (text msg) bug msg = ppbug (text msg)
ppbug doc = error $ render $ ppbug doc = error $ render $
hang (text "Internal error in Compute.ConcreteNew2:") 4 doc hang (text "Internal error in Compute.ConcreteNew:") 4 doc