forked from GitHub/gf-core
Merge pull request #87 from anka-213/make-it-fast
Remove the `Either Int` from value2term
This commit is contained in:
4
.github/workflows/build-all-versions.yml
vendored
4
.github/workflows/build-all-versions.yml
vendored
@@ -14,7 +14,7 @@ jobs:
|
|||||||
strategy:
|
strategy:
|
||||||
matrix:
|
matrix:
|
||||||
os: [ubuntu-latest, macos-latest, windows-latest]
|
os: [ubuntu-latest, macos-latest, windows-latest]
|
||||||
cabal: ["3.2"]
|
cabal: ["latest"]
|
||||||
ghc:
|
ghc:
|
||||||
- "8.6.5"
|
- "8.6.5"
|
||||||
- "8.8.3"
|
- "8.8.3"
|
||||||
@@ -65,7 +65,7 @@ jobs:
|
|||||||
runs-on: ubuntu-latest
|
runs-on: ubuntu-latest
|
||||||
strategy:
|
strategy:
|
||||||
matrix:
|
matrix:
|
||||||
stack: ["2.3.3"]
|
stack: ["latest"]
|
||||||
ghc: ["7.10.3","8.0.2", "8.2.2", "8.4.4", "8.6.5", "8.8.4"]
|
ghc: ["7.10.3","8.0.2", "8.2.2", "8.4.4", "8.6.5", "8.8.4"]
|
||||||
# ghc: ["8.8.3"]
|
# ghc: ["8.8.3"]
|
||||||
|
|
||||||
|
|||||||
@@ -30,11 +30,12 @@ import Debug.Trace(trace)
|
|||||||
normalForm :: GlobalEnv -> L Ident -> Term -> Term
|
normalForm :: GlobalEnv -> L Ident -> Term -> Term
|
||||||
normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc)
|
normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc)
|
||||||
|
|
||||||
|
nfx :: GlobalEnv -> Term -> Err Term
|
||||||
nfx env@(GE _ _ _ loc) t = do
|
nfx env@(GE _ _ _ loc) t = do
|
||||||
v <- eval env [] t
|
v <- eval env [] t
|
||||||
case value2term loc [] v of
|
return (value2term loc [] v)
|
||||||
Left i -> fail ("variable #"++show i++" is out of scope")
|
-- Old value2term error message:
|
||||||
Right t -> return t
|
-- Left i -> fail ("variable #"++show i++" is out of scope")
|
||||||
|
|
||||||
eval :: GlobalEnv -> Env -> Term -> Err Value
|
eval :: GlobalEnv -> Env -> Term -> Err Value
|
||||||
eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t
|
eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t
|
||||||
@@ -288,9 +289,9 @@ glue env (v1,v2) = glu v1 v2
|
|||||||
(v1,v2) -> if flag optPlusAsBind (opts env)
|
(v1,v2) -> if flag optPlusAsBind (opts env)
|
||||||
then VC v1 (VC (VApp BIND []) v2)
|
then VC v1 (VC (VApp BIND []) v2)
|
||||||
else let loc = gloc env
|
else let loc = gloc env
|
||||||
vt v = case value2term loc (local env) v of
|
vt v = value2term loc (local env) v
|
||||||
Left i -> Error ('#':show i)
|
-- Old value2term error message:
|
||||||
Right t -> t
|
-- Left i -> Error ('#':show i)
|
||||||
originalMsg = render $ ppL loc (hang "unsupported token gluing" 4
|
originalMsg = render $ ppL loc (hang "unsupported token gluing" 4
|
||||||
(Glue (vt v1) (vt v2)))
|
(Glue (vt v1) (vt v2)))
|
||||||
term = render $ pp $ Glue (vt v1) (vt v2)
|
term = render $ pp $ Glue (vt v1) (vt v2)
|
||||||
@@ -355,9 +356,9 @@ select env vv =
|
|||||||
(v1,v2) -> ok2 VS v1 v2
|
(v1,v2) -> ok2 VS v1 v2
|
||||||
|
|
||||||
match loc cs v =
|
match loc cs v =
|
||||||
case value2term loc [] v of
|
err bad return (matchPattern cs (value2term loc [] v))
|
||||||
Left i -> bad ("variable #"++show i++" is out of scope")
|
-- Old value2term error message:
|
||||||
Right t -> err bad return (matchPattern cs t)
|
-- Left i -> bad ("variable #"++show i++" is out of scope")
|
||||||
where
|
where
|
||||||
bad = fail . ("In pattern matching: "++)
|
bad = fail . ("In pattern matching: "++)
|
||||||
|
|
||||||
@@ -383,9 +384,8 @@ valueTable env i cs =
|
|||||||
wild = case i of TWild _ -> True; _ -> False
|
wild = case i of TWild _ -> True; _ -> False
|
||||||
|
|
||||||
convertv cs' vty =
|
convertv cs' vty =
|
||||||
case value2term (gloc env) [] vty of
|
convert' cs' =<< paramValues'' env (value2term (gloc env) [] vty)
|
||||||
Left i -> fail ("variable #"++show i++" is out of scope")
|
-- Old value2term error message: Left i -> fail ("variable #"++show i++" is out of scope")
|
||||||
Right pty -> convert' cs' =<< paramValues'' env pty
|
|
||||||
|
|
||||||
convert cs' ty = convert' cs' =<< paramValues' env ty
|
convert cs' ty = convert' cs' =<< paramValues' env ty
|
||||||
|
|
||||||
@@ -492,58 +492,60 @@ vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res
|
|||||||
pf (_,VString n) = pp n
|
pf (_,VString n) = pp n
|
||||||
pf (_,v) = ppV v
|
pf (_,v) = ppV v
|
||||||
pa (_,v) = ppV v
|
pa (_,v) = ppV v
|
||||||
ppV v = case value2term' True loc [] v of
|
ppV v = ppTerm Unqualified 10 (value2term' True loc [] v)
|
||||||
Left i -> "variable #" <> pp i <+> "is out of scope"
|
-- Old value2term error message:
|
||||||
Right t -> ppTerm Unqualified 10 t
|
-- Left i -> "variable #" <> pp i <+> "is out of scope"
|
||||||
|
|
||||||
-- | Convert a value back to a term
|
-- | Convert a value back to a term
|
||||||
value2term :: GLocation -> [Ident] -> Value -> Either Int Term
|
value2term :: GLocation -> [Ident] -> Value -> Term
|
||||||
value2term = value2term' False
|
value2term = value2term' False
|
||||||
|
|
||||||
|
value2term' :: Bool -> p -> [Ident] -> Value -> Term
|
||||||
value2term' stop loc xs v0 =
|
value2term' stop loc xs v0 =
|
||||||
case v0 of
|
case v0 of
|
||||||
VApp pre vs -> liftM (foldl App (Q (cPredef,predefName pre))) (mapM v2t vs)
|
VApp pre vs -> applyMany (Q (cPredef,predefName pre)) vs
|
||||||
VCApp f vs -> liftM (foldl App (QC f)) (mapM v2t vs)
|
VCApp f vs -> applyMany (QC f) vs
|
||||||
VGen j vs -> liftM2 (foldl App) (var j) (mapM v2t vs)
|
VGen j vs -> applyMany (var j) vs
|
||||||
VMeta j env vs -> liftM (foldl App (Meta j)) (mapM v2t vs)
|
VMeta j env vs -> applyMany (Meta j) vs
|
||||||
VProd bt v x f -> liftM2 (Prod bt x) (v2t v) (v2t' x f)
|
VProd bt v x f -> Prod bt x (v2t v) (v2t' x f)
|
||||||
VAbs bt x f -> liftM (Abs bt x) (v2t' x f)
|
VAbs bt x f -> Abs bt x (v2t' x f)
|
||||||
VInt n -> return (EInt n)
|
VInt n -> EInt n
|
||||||
VFloat f -> return (EFloat f)
|
VFloat f -> EFloat f
|
||||||
VString s -> return (if null s then Empty else K s)
|
VString s -> if null s then Empty else K s
|
||||||
VSort s -> return (Sort s)
|
VSort s -> Sort s
|
||||||
VImplArg v -> liftM ImplArg (v2t v)
|
VImplArg v -> ImplArg (v2t v)
|
||||||
VTblType p res -> liftM2 Table (v2t p) (v2t res)
|
VTblType p res -> Table (v2t p) (v2t res)
|
||||||
VRecType rs -> liftM RecType (mapM (\(l,v) -> fmap ((,) l) (v2t v)) rs)
|
VRecType rs -> RecType [(l, v2t v) | (l,v) <- rs]
|
||||||
VRec as -> liftM R (mapM (\(l,v) -> v2t v >>= \t -> return (l,(Nothing,t))) as)
|
VRec as -> R [(l, (Nothing, v2t v)) | (l,v) <- as]
|
||||||
VV t _ vs -> liftM (V t) (mapM v2t vs)
|
VV t _ vs -> V t (map v2t vs)
|
||||||
VT wild v cs -> v2t v >>= \t -> liftM (T ((if wild then TWild else TTyped) t)) (mapM nfcase cs)
|
VT wild v cs -> T ((if wild then TWild else TTyped) (v2t v)) (map nfcase cs)
|
||||||
VFV vs -> liftM FV (mapM v2t vs)
|
VFV vs -> FV (map v2t vs)
|
||||||
VC v1 v2 -> liftM2 C (v2t v1) (v2t v2)
|
VC v1 v2 -> C (v2t v1) (v2t v2)
|
||||||
VS v1 v2 -> liftM2 S (v2t v1) (v2t v2)
|
VS v1 v2 -> S (v2t v1) (v2t v2)
|
||||||
VP v l -> v2t v >>= \t -> return (P t l)
|
VP v l -> P (v2t v) l
|
||||||
VPatt p -> return (EPatt p)
|
VPatt p -> EPatt p
|
||||||
VPattType v -> v2t v >>= return . EPattType
|
VPattType v -> EPattType $ v2t v
|
||||||
VAlts v vvs -> liftM2 Alts (v2t v) (mapM (\(x,y) -> liftM2 (,) (v2t x) (v2t y)) vvs)
|
VAlts v vvs -> Alts (v2t v) [(v2t x, v2t y) | (x,y) <- vvs]
|
||||||
VStrs vs -> liftM Strs (mapM v2t vs)
|
VStrs vs -> Strs (map v2t vs)
|
||||||
-- VGlue v1 v2 -> Glue (v2t v1) (v2t v2)
|
-- VGlue v1 v2 -> Glue (v2t v1) (v2t v2)
|
||||||
-- VExtR v1 v2 -> ExtR (v2t v1) (v2t v2)
|
-- VExtR v1 v2 -> ExtR (v2t v1) (v2t v2)
|
||||||
VError err -> return (Error err)
|
VError err -> Error err
|
||||||
|
|
||||||
where
|
where
|
||||||
|
applyMany f vs = foldl App f (map v2t vs)
|
||||||
v2t = v2txs xs
|
v2t = v2txs xs
|
||||||
v2txs = value2term' stop loc
|
v2txs = value2term' stop loc
|
||||||
v2t' x f = v2txs (x:xs) (bind f (gen xs))
|
v2t' x f = v2txs (x:xs) (bind f (gen xs))
|
||||||
|
|
||||||
var j
|
var j
|
||||||
| j<length xs = Right (Vr (reverse xs !! j))
|
| j<length xs = Vr (reverse xs !! j)
|
||||||
| otherwise = Left j
|
| otherwise = error ("variable #"++show j++" is out of scope")
|
||||||
|
|
||||||
|
|
||||||
pushs xs e = foldr push e xs
|
pushs xs e = foldr push e xs
|
||||||
push x (env,xs) = ((x,gen xs):env,x:xs)
|
push x (env,xs) = ((x,gen xs):env,x:xs)
|
||||||
gen xs = VGen (length xs) []
|
gen xs = VGen (length xs) []
|
||||||
|
|
||||||
nfcase (p,f) = liftM ((,) p) (v2txs xs' (bind f env'))
|
nfcase (p,f) = (,) p (v2txs xs' (bind f env'))
|
||||||
where (env',xs') = pushs (pattVars p) ([],xs)
|
where (env',xs') = pushs (pattVars p) ([],xs)
|
||||||
|
|
||||||
bind (Bind f) x = if stop
|
bind (Bind f) x = if stop
|
||||||
|
|||||||
@@ -568,9 +568,9 @@ unifyVar ge scope i env vs ty2 = do -- Check whether i is bound
|
|||||||
Bound ty1 -> do v <- liftErr (eval ge env ty1)
|
Bound ty1 -> do v <- liftErr (eval ge env ty1)
|
||||||
unify ge scope (vapply (geLoc ge) v vs) ty2
|
unify ge scope (vapply (geLoc ge) v vs) ty2
|
||||||
Unbound scope' _ -> case value2term (geLoc ge) (scopeVars scope') ty2 of
|
Unbound scope' _ -> case value2term (geLoc ge) (scopeVars scope') ty2 of
|
||||||
Left i -> let (v,_) = reverse scope !! i
|
-- Left i -> let (v,_) = reverse scope !! i
|
||||||
in tcError ("Variable" <+> pp v <+> "has escaped")
|
-- in tcError ("Variable" <+> pp v <+> "has escaped")
|
||||||
Right ty2' -> do ms2 <- getMetaVars (geLoc ge) [(scope,ty2)]
|
ty2' -> do ms2 <- getMetaVars (geLoc ge) [(scope,ty2)]
|
||||||
if i `elem` ms2
|
if i `elem` ms2
|
||||||
then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$
|
then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$
|
||||||
nest 2 (ppTerm Unqualified 0 ty2'))
|
nest 2 (ppTerm Unqualified 0 ty2'))
|
||||||
@@ -765,9 +765,9 @@ zonkTerm (Meta i) = do
|
|||||||
zonkTerm t = composOp zonkTerm t
|
zonkTerm t = composOp zonkTerm t
|
||||||
|
|
||||||
tc_value2term loc xs v =
|
tc_value2term loc xs v =
|
||||||
case value2term loc xs v of
|
return $ value2term loc xs v
|
||||||
Left i -> tcError ("Variable #" <+> pp i <+> "has escaped")
|
-- Old value2term error message:
|
||||||
Right t -> return t
|
-- Left i -> tcError ("Variable #" <+> pp i <+> "has escaped")
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user