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 44138ff8ce
commit 7d0f649f29

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