Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Updates to built-in types interface, fixes to problematic dependencies, and improved matching in peval #806

Closed
wants to merge 4 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/main/accelerate.mc
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ lang MExprCudaCompile =
end

let keywordsSymEnv =
{symEnvEmpty with varEnv =
{symEnvDefault with varEnv =
mapFromSeq
cmpString
(map (lam s. (s, nameSym s)) mexprExtendedKeywords)}
Expand Down
2 changes: 1 addition & 1 deletion stdlib/c/compile.mc
Original file line number Diff line number Diff line change
Expand Up @@ -1387,7 +1387,7 @@ use Test in
let compile: CompileCOptions -> Expr -> CProg = lam opts. lam prog.

-- Symbolize with empty environment
let prog = symbolizeExpr symEnvEmpty prog in
let prog = symbolizeExpr symEnvDefault prog in

-- Type check and annotate
let prog = typeCheck prog in
Expand Down
3 changes: 1 addition & 2 deletions stdlib/mexpr/keyword-maker.mc
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@
include "ast.mc"
include "info.mc"
include "error.mc"
include "mexpr.mc"
include "ast-builder.mc"
include "eq.mc"

Expand Down Expand Up @@ -163,7 +162,7 @@ end

-- A test fragment that is used to test the approach. This
-- fragment can be used as a template when using the keyword maker.
lang _testKeywordMaker = KeywordMaker + MExpr + MExprEq
lang _testKeywordMaker = KeywordMaker + MExprEq

-- Example terms that will be used to represent the values of the
-- the keyword expressions (the new language constructs). The term
Expand Down
28 changes: 19 additions & 9 deletions stdlib/mexpr/symbolize.mc
Original file line number Diff line number Diff line change
Expand Up @@ -31,19 +31,29 @@ type SymEnv = {
ignoreExternals: Bool
}

let symEnvEmpty = {
let _symEnvEmpty = {
varEnv = mapEmpty cmpString,
conEnv = mapEmpty cmpString,
tyVarEnv = mapEmpty cmpString,

-- Built-in type constructors
tyConEnv =
mapFromSeq cmpString (map (lam t. (t.0, nameNoSym t.0)) builtinTypes),

tyConEnv = mapEmpty cmpString,
allowFree = false,
ignoreExternals = false
}

let symEnvAddBuiltinTypes : all a. SymEnv -> [(String, a)] -> SymEnv
= lam env. lam tys. {
env with tyConEnv =
foldl (lam env. lam t. mapInsert t.0 (nameNoSym t.0) env) env.tyConEnv tys
}

let symEnvDefault =
symEnvAddBuiltinTypes _symEnvEmpty builtinTypes

-- TODO(oerikss, 2023-11-14): Change all DSLs that use this name for the
-- symbolize environment to instead point to `symEnvDefault` and then
-- remove this alias and rename `_symEnvEmpty` to `symEnvEmpty`.
let symEnvEmpty = symEnvDefault

lang SymLookup
type LookupParams = {kind : String, info : [Info], allowFree : Bool}

Expand Down Expand Up @@ -125,13 +135,13 @@ lang Sym = Ast + SymLookup
-- Symbolize with builtin environment
sem symbolize =
| expr ->
let env = symEnvEmpty in
let env = symEnvDefault in
symbolizeExpr env expr

-- Symbolize with builtin environment and ignore errors
sem symbolizeAllowFree =
| expr ->
let env = { symEnvEmpty with allowFree = true } in
let env = { symEnvDefault with allowFree = true } in
symbolizeExpr env expr

-- Add top-level identifiers (along the spine of the program) in `t`
Expand Down Expand Up @@ -509,7 +519,7 @@ utest isFullySymbolized (nulam_ x (nvar_ x)) with true in
let testSymbolize = lam ast. lam testEqStr.
let symbolizeCalls =
[ symbolize
, symbolizeExpr {symEnvEmpty with allowFree = true}] in
, symbolizeExpr {symEnvDefault with allowFree = true}] in
foldl
(lam acc. lam symb.
if acc then
Expand Down
32 changes: 23 additions & 9 deletions stdlib/mexpr/type-check.mc
Original file line number Diff line number Diff line change
Expand Up @@ -38,19 +38,33 @@ type TCEnv = {
disableRecordPolymorphism: Bool
}

let _tcEnvEmpty = {
let typcheckEnvEmpty = {
varEnv = mapEmpty nameCmp,
conEnv = mapEmpty nameCmp,
tyVarEnv = mapEmpty nameCmp,
tyConEnv =
mapFromSeq nameCmp
(map (lam t: (String, [String]).
(nameNoSym t.0, (0, map nameSym t.1, tyvariant_ []))) builtinTypes),

tyConEnv = mapEmpty nameCmp,
currentLvl = 0,
disableRecordPolymorphism = true
}

let typecheckEnvAddBuiltinTypes : TCEnv -> [(String, [String])] -> TCEnv
= lam env. lam tys. {
env with
tyConEnv =
foldl
(lam env. lam t.
mapInsert (nameNoSym t.0) (0, map nameSym t.1, tyvariant_ []) env)
env.tyConEnv tys
}

let typcheckEnvDefault =
typecheckEnvAddBuiltinTypes typcheckEnvEmpty builtinTypes

-- TODO(oerikss, 2023-11-14): Change all DSLs that use this name for the
-- type-check environment to instead point to `typcheckEnvDefault` and then
-- remove this alias.
let _tcEnvEmpty = typcheckEnvDefault

let _insertVar = lam name. lam ty. lam env : TCEnv.
{env with varEnv = mapInsert name ty env.varEnv}

Expand Down Expand Up @@ -444,7 +458,7 @@ lang TypeCheck = TCUnify + Generalize + RemoveMetaVar
sem typeCheck : Expr -> Expr
sem typeCheck =
| tm ->
removeMetaVarExpr (typeCheckExpr _tcEnvEmpty tm)
removeMetaVarExpr (typeCheckExpr typcheckEnvDefault tm)

-- Type check `expr' under the type environment `env'. The resulting
-- type may contain unification variables and links.
Expand Down Expand Up @@ -994,8 +1008,8 @@ let typeOf = lam test : TypeTest.
let tyEnv = mapFromSeq nameCmp bindings in
unwrapTypes
(tyTm
(typeCheckExpr {_tcEnvEmpty with varEnv = tyEnv}
(symbolizeExpr {symEnvEmpty with varEnv = symEnv} test.tm)))
(typeCheckExpr {typcheckEnvDefault with varEnv = tyEnv}
(symbolizeExpr {symEnvDefault with varEnv = symEnv} test.tm)))
in

let runTest =
Expand Down
1 change: 1 addition & 0 deletions stdlib/peval/ast.mc
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ include "mexpr/type-check.mc"
include "mexpr/eval.mc"
include "mexpr/info.mc"
include "mexpr/eq.mc"
include "mexpr/mexpr.mc"

include "peval/peval.mc"
include "error.mc"
Expand Down
42 changes: 28 additions & 14 deletions stdlib/peval/peval.mc
Original file line number Diff line number Diff line change
Expand Up @@ -434,7 +434,8 @@ lang ConstPEval = PEval + ConstEvalNoDefault
end

lang MatchPEval =
PEval + MatchEval + RecordAst + ConstAst + DataAst + SeqAst + NeverAst + VarAst
PEval + MatchEval + RecordAst + ConstAst + DataAst + SeqAst + NeverAst +
VarAst + NamedPat

sem pevalBindThis =
| TmMatch _ -> true
Expand All @@ -443,23 +444,36 @@ lang MatchPEval =
| TmMatch r ->
pevalBind ctx
(lam target.
switch target
case t & TmNever _ then k t
-- TODO(oerikss, 2023-07-07): This check is not exhaustive, we must
-- probably redefine tryMatch and handle each particular pattern type.
case TmRecord _ | TmConst _ | TmConApp _ | TmSeq _ then
match tryMatch ctx.env target r.pat with Some env then
pevalBind { ctx with env = env } k r.thn
else pevalBind ctx k r.els
switch (target, tryMatch ctx.env target r.pat)
case (TmNever r, _) then TmNever r
case (_, Some env) then
pevalBind { ctx with env = env } k r.thn
case (!TmVar _, None _) then
pevalBind ctx k r.els
case _ then
match freshPattern ctx.env r.pat with (env, pat) in
let ctx = { ctx with recFlag = false } in
k (TmMatch {r with
target = target,
thn = pevalBind ctx (lam x. x) r.thn,
els = pevalBind ctx (lam x. x) r.els
})
k (TmMatch { r with
target = target,
pat = pat,
thn = pevalBind { ctx with env = env } (lam x. x) r.thn,
els = pevalBind ctx (lam x. x) r.els })
end)
r.target

sem freshPattern : EvalEnv -> Pat -> (EvalEnv, Pat)
sem freshPattern env =
| PatNamed (r & {ident = PName name}) ->
let newname = nameSetNewSym name in
let newvar = TmVar {
ident = newname,
ty = r.ty,
info = r.info,
frozen = false
} in
(evalEnvInsert name newvar env,
PatNamed { r with ident = PName newname })
| p -> smapAccumL_Pat_Pat freshPattern env p
end

lang UtestPEval = PEval + UtestAst
Expand Down
2 changes: 1 addition & 1 deletion stdlib/pmexpr/utils.mc
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ let typeCheckEnv = lam env : [(Name, Type)]. lam expr.
(lam env. lam x : (Name, Type).
match x with (id, ty) in
_insertVar id ty env)
_tcEnvEmpty env in
typcheckEnvDefault env in
removeMetaVarExpr (typeCheckExpr tcEnv expr)
in

Expand Down
Loading