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.

Sign up for GitHub

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

don't cache varctx (rare operation) #110

Closed
wants to merge 1 commit into from
Closed

don't cache varctx (rare operation) #110

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
57 changes: 37 additions & 20 deletions src/core/abt.fun
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ struct

type system_annotation =
{varIdxBound: int,
freeVars: varctx,
hasVars: bool,
hasMetas: bool}

type annotation = annotation
Expand All @@ -51,7 +51,7 @@ struct

fun systemAnnLub (ann1 : system_annotation, ann2 : system_annotation) : system_annotation =
{varIdxBound = Int.max (#varIdxBound ann1, #varIdxBound ann2),
freeVars = VarCtxUtil.union (#freeVars ann1, #freeVars ann2),
hasVars = #hasVars ann1 orelse #hasVars ann2,
hasMetas = #hasMetas ann1 orelse #hasMetas ann2}

datatype 'a annotated = <: of 'a * internal_annotation
Expand Down Expand Up @@ -129,28 +129,28 @@ struct
fun scopeReadAnn scope =
let
val Sc.\ (xs, body <: ann) = Sc.unsafeRead scope
val {varIdxBound, freeVars, hasMetas} = #system ann
val {varIdxBound, hasVars, hasMetas} = #system ann
val varIdxBound' = varIdxBound - List.length xs
in
{user = #user ann,
system = {varIdxBound = varIdxBound', freeVars = freeVars, hasMetas = hasMetas}}
system = {varIdxBound = varIdxBound', hasVars = hasVars, hasMetas = hasMetas}}
end

fun makeVarTerm (var, tau) userAnn =
case var of
FREE x =>
V (var, tau) <:
{user = userAnn,
system = {varIdxBound = 0, freeVars = Var.Ctx.singleton x tau, hasMetas = false}}
system = {varIdxBound = 0, hasVars = true, hasMetas = false}}

| BOUND i =>
V (var, tau) <:
{user = userAnn,
system = {varIdxBound = i + 1, freeVars = Var.Ctx.empty, hasMetas = false}}
system = {varIdxBound = i + 1, hasVars = false, hasMetas = false}}

fun makeAppTerm (theta, scopes) userAnn =
let
val operatorAnn = {varIdxBound = 0, freeVars = Var.Ctx.empty, hasMetas = false}
val operatorAnn = {varIdxBound = 0, hasVars = false, hasMetas = false}
val systemAnn =
List.foldl
(fn (ABS (_, scope), ann) => systemAnnLub (ann, #system (scopeReadAnn scope)))
Expand All @@ -162,7 +162,7 @@ struct

fun makeMetaTerm (((X, tau), ms) : meta_term) userAnn =
let
val metaSystemAnn = {varIdxBound = 0, freeVars = Var.Ctx.empty, hasMetas = true}
val metaSystemAnn = {varIdxBound = 0, hasVars = false, hasMetas = true}
val systemAnn =
List.foldl
(fn (_ <: termAnn, ann) => systemAnnLub (ann, #system termAnn))
Expand Down Expand Up @@ -256,8 +256,8 @@ struct

fun abstractAbt (ix : int) xs =
let
fun shouldTraverse ix ({freeVars, hasMetas, ...} : system_annotation) =
case xs of [] => false | _ => not (Var.Ctx.isEmpty freeVars)
fun shouldTraverse ix ({hasVars, hasMetas, ...} : system_annotation) =
case xs of [] => false | _ => hasVars

fun abstractVar j =
fn (vt as (FREE x, tau)) <: ann =>
Expand All @@ -282,9 +282,6 @@ struct
freeVariable = fn (x, tau) => makeVarTerm (FREE x, tau) NONE}


fun varctx (_ <: {system = {freeVars, ...}, ...}) =
freeVars

val metactx : abt -> metactx =
let
val monoid : (metactx -> metactx) monoid =
Expand All @@ -300,6 +297,26 @@ struct
fn tm => abtAccum monoid alg 0 tm Metavar.Ctx.empty
end

val varctx : abt -> varctx =
let
val monoid : (varctx -> varctx) monoid =
{unit = fn ctx => ctx,
mul = op o}

fun handleVar _ ((var, tau) <: _) =
case var of
FREE x => (fn ctx => Var.Ctx.insert ctx x tau)
| _ => #unit monoid

val alg =
{debug = "varctx",
handleVar = handleVar,
handleMeta = fn _ => #unit monoid,
shouldTraverse = fn _ => fn ({hasVars, ...} : system_annotation) => hasVars}
in
fn tm => abtAccum monoid alg 0 tm Var.Ctx.empty
end

val varOccurrences =
let
type occurrences = annotation list Var.Ctx.dict
Expand All @@ -316,7 +333,7 @@ struct
{debug = "varOccurrences",
handleVar = handleVar,
handleMeta = fn _ => #unit monoid,
shouldTraverse = fn _ => fn ({freeVars, ...} : system_annotation) => not (Var.Ctx.isEmpty freeVars)}
shouldTraverse = fn _ => fn ({hasVars, ...} : system_annotation) => hasVars}
in
fn tm => abtAccum monoid alg 0 tm Var.Ctx.empty
end
Expand All @@ -335,9 +352,9 @@ struct
{debug = "renameVars",
handleVar = handleVar,
handleMeta = fn (X, _) => X,
shouldTraverse = fn _ => fn ({freeVars, ...} : system_annotation) => not (Var.Ctx.isEmpty freeVars)}
shouldTraverse = fn _ => fn ({hasVars, ...} : system_annotation) => hasVars}
in
abtRec alg 0
if Var.Ctx.isEmpty vrho then (fn x => x) else abtRec alg 0
end

fun renameMetavars mrho =
Expand All @@ -353,13 +370,13 @@ struct
handleMeta = handleMeta,
shouldTraverse = fn _ => fn ({hasMetas, ...} : system_annotation) => hasMetas}
in
abtRec alg 0
if Metavar.Ctx.isEmpty mrho then (fn x => x) else abtRec alg 0
end

fun substVarenv (vrho : varenv) =
let
fun shouldTraverse _ ({freeVars, ...} : system_annotation) =
not (Var.Ctx.isEmpty freeVars orelse Var.Ctx.isEmpty vrho)
fun shouldTraverse _ ({hasVars, ...} : system_annotation) =
hasVars

fun handleVar _ ((vt as (var, tau)) <: ann) =
case var of
Expand All @@ -375,7 +392,7 @@ struct
handleMeta = fn (X, _) => X,
shouldTraverse = shouldTraverse}
in
abtRec alg 0
if Var.Ctx.isEmpty vrho then (fn x => x) else abtRec alg 0
end
end

Expand Down