From 8370fee1e97e665ec10100edbddb03906b2da563 Mon Sep 17 00:00:00 2001
From: Jon Sterling <jon@jonmsterling.com>
Date: Mon, 26 Feb 2018 09:41:07 -0500
Subject: [PATCH] performance tuning: when to check free-vars?

---
 lib/sml-typed-abts         |  2 +-
 src/redprl/refiner.fun     |  2 ++
 src/redprl/refiner_kit.fun | 16 ++++++----------
 3 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/lib/sml-typed-abts b/lib/sml-typed-abts
index c437e0879..343bd461a 160000
--- a/lib/sml-typed-abts
+++ b/lib/sml-typed-abts
@@ -1 +1 @@
-Subproject commit c437e08791330fa96eb72fc0af151688ee5ba9db
+Subproject commit 343bd461a183b1e7510de02cd88c087d0837e2e4
diff --git a/src/redprl/refiner.fun b/src/redprl/refiner.fun
index fc361efb7..34aa0a3a8 100644
--- a/src/redprl/refiner.fun
+++ b/src/redprl/refiner.fun
@@ -152,6 +152,7 @@ struct
       let
         val tr = ["True.Witness"]
         val H >> AJ.TRUE ty = jdg
+        val () = assertWellScoped H tm
         val goal = makeMem tr H (tm, ty)
       in
         |>: goal #> (H, tm)
@@ -166,6 +167,7 @@ struct
       let
         val tr = ["Term.Exact"]
         val H >> AJ.TERM tau = jdg
+        val () = assertWellScoped H tm
         val tau' = Abt.sort tm
         val _ = Assert.sortEq (tau, tau')
       in
diff --git a/src/redprl/refiner_kit.fun b/src/redprl/refiner_kit.fun
index b23cb214b..9688cd5e2 100644
--- a/src/redprl/refiner_kit.fun
+++ b/src/redprl/refiner_kit.fun
@@ -35,24 +35,21 @@ struct
       end
   end
 
-  (* assert that the term 'm' has only free variables 'us' and free variables 'xs' at most. *)
-  fun assertWellScoped xs m = 
+  (* assert that the term 'm' has only free variables from 'H' at most. *)
+  fun assertWellScoped H m = 
     let
-      val vars = List.foldl (fn (x, vars) => Var.Ctx.remove vars x) (Abt.varctx m) xs
-      fun ppVars us = Fpp.Atomic.squares @@ Fpp.hsep @@ List.map TermPrinter.ppVar us
+      val vars = Hyps.foldl (fn (x, tau, vars) => Var.Ctx.remove vars x) (Abt.varctx m) H
+      fun ppVars xs = Fpp.Atomic.squares @@ Fpp.hsep @@ List.map TermPrinter.ppVar xs
       val varsOk = Var.Ctx.isEmpty vars
     in
       if varsOk then
         ()
       else
         raise E.error
-          [Fpp.text "Internal Error:",
-           Fpp.text "Validation term",
+          [Fpp.text "Term",
            TermPrinter.ppTerm m,
            Fpp.text "had unbound variables",
-           ppVars (Var.Ctx.domain vars),
-           Fpp.text "whereas we expected only",
-           ppVars xs]
+           ppVars (Var.Ctx.domain vars)]
     end
 
   (* hypotheses *)
@@ -67,7 +64,6 @@ struct
     let
       val (xs, taus) = Hyps.foldr (fn (x, jdg, (xs, taus)) => (x::xs, AJ.synthesis jdg::taus)) ([],[]) H
     in
-      assertWellScoped xs m;
       Abt.checkb (Abt.\ (xs, m), (taus, Abt.sort m))
     end