Skip to content

Commit

Permalink
Avoid calling slow typeInferComplete on already-typechecked terms.
Browse files Browse the repository at this point in the history
This fixes a performance problem that was exposed by #118:
`typeInferComplete` is actually very slow when called on
`Constant` terms, because instead of using the cached type,
it rechecks the well-formedness of the constant's definition.
Furthermore, its memoization for observable sharing is mostly
ineffective, because it resets the memo table whenever it
looks under a binder.

Switching from `typeInferComplete` to `scTypeOf` brings the
saw-script start-up time back to where it was before #118.
  • Loading branch information
Brian Huffman committed Jan 21, 2021
1 parent db41a9b commit 317550f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion saw-core/src/Verifier/SAW/Typechecker.hs
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,7 @@ inferResolveNameApp n args =
typeInferComplete (DataTypeApp (dtName dt) params ixs)
(_, Just (ResolvedDef d)) ->
do t <- liftTCM scGlobalDef (defIdent d)
f <- typeInferComplete t
f <- TypedTerm t <$> liftTCM scTypeOf t
inferApplyAll f args
(Nothing, Nothing) ->
throwTCError $ UnboundName n
Expand Down

0 comments on commit 317550f

Please sign in to comment.