Skip to content

Commit

Permalink
Merge pull request #127 from GaloisInc/faster-typechecker
Browse files Browse the repository at this point in the history
Avoid calling slow `typeInferComplete` on already-typechecked terms.
  • Loading branch information
brianhuffman authored Jan 21, 2021
2 parents db41a9b + 317550f commit 2109f18
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 2109f18

Please sign in to comment.