Updating: minor modification.

xlq · Mar 16, 2012 · 7970f1a · 7970f1a
1 parent 8b1942e
commit 7970f1a
Show file tree

Hide file tree

Showing 3 changed files with 25 additions and 15 deletions.
diff --git a/src/ats_trans3_env.dats b/src/ats_trans3_env.dats
@@ -1518,9 +1518,11 @@ funarg_varfin_check (loc0) = let
       end // end of [list_cons]
     | list_nil () => ()
   end // end of [auxpatlst]
+  val opt = the_lamloop_env_arg_get ()
 in
-  case+ the_lamloop_env_arg_get loc0 of
-  | ~Some_vt p3ts => auxpatlst (loc0, p3ts) | ~None_vt () => begin
+  case+ opt of
+  | ~Some_vt p3ts => auxpatlst (loc0, p3ts)
+  | ~None_vt () => begin
       prerr_loc_interror loc0;
       prerr ": funarg_varfin_check: no argument(s)."; prerr_newline ();
       $Err.abort {void} ()
@@ -1596,9 +1598,11 @@ s2exp_wth_instantiate (loc0, s2e0) = let
 in
   case+ s2e0.s2exp_node of
   | S2Ewth (s2e, wths2es) => let
+      val opt = the_lamloop_env_arg_get () 
       val p3ts = (
-        case+ the_lamloop_env_arg_get (loc0) of
-        | ~Some_vt p3ts => p3ts | ~None_vt () => begin
+        case+ opt of
+        | ~Some_vt p3ts => p3ts
+        | ~None_vt () => begin
             prerr_loc_interror loc0;
             prerr ": s2exp_wth_instantiate"; prerr_newline ();
             $Err.abort {p3atlst} ()

diff --git a/src/ats_trans3_env.sats b/src/ats_trans3_env.sats
@@ -501,7 +501,7 @@ fun the_lamloop_env_push_loop1 {n:nat} (
   lamloop_env_token | void
 ) // end of [the_lamloop_env_push_loop1]
 
-fun the_lamloop_env_arg_get (loc0: loc_t): Option_vt (p3atlst)
+fun the_lamloop_env_arg_get (): Option_vt (p3atlst)
 
 (* ****** ****** *)
 

diff --git a/src/ats_trans3_env_loop.dats b/src/ats_trans3_env_loop.dats
@@ -97,17 +97,23 @@ end // end of [the_lamloop_env_push_loop1]
 
 (* ****** ****** *)
 
-implement the_lamloop_env_arg_get (loc0) = begin
+implement
+the_lamloop_env_arg_get () = let
+//
+fun aux (
+  lmlps: lamlooplst
+) : Option_vt p3atlst = (
+  case+ lmlps of
+  | list_cons (lmlp, lmlps) => (
+    case+ lmlp of
+    | LMLPlam p3ts => Some_vt (p3ts) | _ => aux lmlps
+    )
+  | list_nil () => None_vt ()
+) // end of [aux]
+//
+in
   case+ !the_lamloop of
-  | LMLPlam p3ts => Some_vt (p3ts)
-  | _ => aux !the_lamloops where {
-      fun aux (lmlps: lamlooplst): Option_vt p3atlst =
-        case+ lmlps of
-        | list_cons (lmlp, lmlps) => begin case+ lmlp of
-          | LMLPlam p3ts => Some_vt (p3ts) | _ => aux lmlps
-          end
-        | list_nil () => None_vt ()
-    } // end of [where]
+  | LMLPlam p3ts => Some_vt (p3ts) | _ => aux !the_lamloops
 end // end of [the_lamloop_env_arg_get]
 
 (* ****** ******* *)