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 after nominal-mlang #1

Merged
merged 1 commit into from
Dec 15, 2023
Merged
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
4 changes: 2 additions & 2 deletions src/compiler/ast.mc
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ lang OpaqueOCamlAst = Ast
(acc, PatOpaqueOCamlCon {x with arg = arg})
end

lang OCamlStringAst = Ast
lang OCamlStringAst = Ast + ConstAst + TyConst
-- Constant
syn Const =
| COString {val : String}
Expand Down Expand Up @@ -76,7 +76,7 @@ lang OCamlStringAst = Ast
| PatOString x -> PatOString {x with ty = ty}
end

lang OCamlListAst = Ast
lang OCamlListAst = Ast + ConstAst + TyConst
-- Constant
syn Const =
| CONil ()
Expand Down
4 changes: 2 additions & 2 deletions src/compiler/cost.mc
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ let costEvalEnv /- : Ref EvalEnv (defined in lang frag) -/ = use Eval in ref (ev
let costSymEnv : Ref SymEnv = ref symEnvEmpty

let costSetVar
: Name -> Expr -> ()
: Name -> use Ast in Expr -> ()
= lam n. lam c.
let n = if nameHasSym n then n else nameSetNewSym n in
modref costSymEnv (
Expand All @@ -33,7 +33,7 @@ lang EvalCost = Eval + FloatAst + PrettyPrint
end
end

lang LogfBuiltin = Ast + Eval + PrettyPrint + ConstArity + FloatAst
lang LogfBuiltin = Ast + Eval + PrettyPrint + ConstArity + FloatAst + ConstDelta + ConstPrettyPrint
syn Const =
| CLogf ()

Expand Down
2 changes: 0 additions & 2 deletions src/compiler/main.mc
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,6 @@ lang RepAnalysis
+ RepTypesPrettyPrint
+ OCamlExtrasTypeCheck
+ OCamlExtrasPprint
sem typeCheckExpr env =
| tm -> errorSingle [infoTm tm] "Missing typeCheckExpr"
end

lang MExprRepTypesComposedSolver
Expand Down
4 changes: 2 additions & 2 deletions src/compiler/pprint.mc
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ include "mexpr/pprint.mc"

include "ast.mc"

lang OCamlStringPprint = PrettyPrint + OCamlStringAst
lang OCamlStringPprint = PrettyPrint + OCamlStringAst + ConstPrettyPrint
sem getConstStringCode indent =
| COString x -> join ["\"", escapeString x.val, "\""]

Expand Down Expand Up @@ -35,7 +35,7 @@ lang OCamlOpaquePprint = PrettyPrint + OpaqueOCamlAst
(env, join [x.content, match arg with Some arg then concat " " arg else ""])
end

lang OCamlListPprint = PrettyPrint + OCamlListAst
lang OCamlListPprint = PrettyPrint + OCamlListAst + ConstPrettyPrint
sem getConstStringCode indent =
| CONil _ -> "[]"
| COCons _ -> "(::)"
Expand Down
6 changes: 3 additions & 3 deletions src/compiler/type-check.mc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
include "mexpr/type-check.mc"

lang OpaqueOCamlTypeCheck = TypeCheck + OpaqueOCamlAst + CompatibleType
lang OpaqueOCamlTypeCheck = TypeCheck + OpaqueOCamlAst + CompatibleType + TypeAnnot + MatchTypeAnnot + PatTypeCheck
sem typeCheckExpr env =
| TmOpaqueOCaml x ->
TmOpaqueOCaml {x with ty = newmonovar env.currentLvl x.info}
Expand Down Expand Up @@ -29,7 +29,7 @@ lang OpaqueOCamlTypeCheck = TypeCheck + OpaqueOCamlAst + CompatibleType
| pat & PatOpaqueOCamlCon _ -> (env, pat)
end

lang OCamlStringTypeCheck = TypeCheck + Unify + OCamlStringAst + CompatibleType
lang OCamlStringTypeCheck = TypeCheck + Unify + OCamlStringAst + CompatibleType + MatchTypeAnnot + PatTypeCheck
sem typeCheckPat env patEnv =
| PatOString x ->
(patEnv, PatOString {x with ty = TyOString {info = x.info}})
Expand All @@ -44,7 +44,7 @@ lang OCamlStringTypeCheck = TypeCheck + Unify + OCamlStringAst + CompatibleType
| pat & PatOString _ -> (env, pat)
end

lang OCamlListTypeCheck = TypeCheck + Unify + OCamlListAst + CompatibleType
lang OCamlListTypeCheck = TypeCheck + Unify + OCamlListAst + CompatibleType + MatchTypeAnnot + PatTypeCheck
sem typeCheckPat env patEnv =
| PatOCons x ->
match typeCheckPat env patEnv x.head with (patEnv, head) in
Expand Down