# HG changeset patch # User haftmann # Date 1215533592 -7200 # Node ID 1505582668314a04dc083a1a971281aa49bf4a4b # Parent 80d0de398339274c0161705f3f5502aa1f61cd24 clarified code diff -r 80d0de398339 -r 150558266831 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Tue Jul 08 18:13:11 2008 +0200 +++ b/src/Tools/nbe.ML Tue Jul 08 18:13:12 2008 +0200 @@ -59,22 +59,22 @@ Const of int * Univ list (*named (uninterpreted) constants*) | Free of string * Univ list (*free variables*) | DFree of string * int (*free (uninterpreted) dictionary parameters*) - | BVar of int * Univ list (*bound named variables*) + | BVar of int * Univ list (*bound variables, named*) | Abs of (int * (Univ list -> Univ)) * Univ list - (*abstractions as closures*); + (*abstractions as closures*); (* constructor functions *) fun abss n f = Abs ((n, f), []); fun apps (Abs ((n, f), xs)) ys = let val k = n - length ys in - if k = 0 then f (ys @ xs) - else if k < 0 then - let val (zs, ws) = chop (~ k) ys - in apps (f (ws @ xs)) zs end - else Abs ((k, f), ys @ xs) end (*note: reverse convention also for apps!*) + case int_ord (k, 0) + of EQUAL => f (ys @ xs) + | LESS => let val (zs, ws) = chop (~ k) ys in apps (f (ws @ xs)) zs end + | GREATER => Abs ((k, f), ys @ xs) (*note: reverse convention also for apps!*) + end | apps (Const (name, xs)) ys = Const (name, ys @ xs) | apps (Free (name, xs)) ys = Free (name, ys @ xs) - | apps (BVar (name, xs)) ys = BVar (name, ys @ xs); + | apps (BVar (n, xs)) ys = BVar (n, ys @ xs); (** assembling and compiling ML code from terms **) @@ -332,8 +332,8 @@ in of_apps bounds (Term.Const (c, T'), ts') typidx' end | of_univ bounds (Free (name, ts)) typidx = of_apps bounds (Term.Free (name, dummyT), ts) typidx - | of_univ bounds (BVar (name, ts)) typidx = - of_apps bounds (Bound (bounds - name - 1), ts) typidx + | of_univ bounds (BVar (n, ts)) typidx = + of_apps bounds (Bound (bounds - n - 1), ts) typidx | of_univ bounds (t as Abs _) typidx = typidx |> of_univ (bounds + 1) (apps t [BVar (bounds, [])])