src/Tools/nbe.ML
changeset 27499 150558266831
parent 27264 843472ae2116
child 27609 b23c9ad0fe7d
     1.1 --- a/src/Tools/nbe.ML	Tue Jul 08 18:13:11 2008 +0200
     1.2 +++ b/src/Tools/nbe.ML	Tue Jul 08 18:13:12 2008 +0200
     1.3 @@ -59,22 +59,22 @@
     1.4      Const of int * Univ list           (*named (uninterpreted) constants*)
     1.5    | Free of string * Univ list         (*free variables*)
     1.6    | DFree of string * int              (*free (uninterpreted) dictionary parameters*)
     1.7 -  | BVar of int * Univ list            (*bound named variables*)
     1.8 +  | BVar of int * Univ list            (*bound variables, named*)
     1.9    | Abs of (int * (Univ list -> Univ)) * Univ list
    1.10 -                                      (*abstractions as closures*);
    1.11 +                                       (*abstractions as closures*);
    1.12  
    1.13  (* constructor functions *)
    1.14  
    1.15  fun abss n f = Abs ((n, f), []);
    1.16  fun apps (Abs ((n, f), xs)) ys = let val k = n - length ys in
    1.17 -      if k = 0 then f (ys @ xs)
    1.18 -      else if k < 0 then
    1.19 -        let val (zs, ws) = chop (~ k) ys
    1.20 -        in apps (f (ws @ xs)) zs end
    1.21 -      else Abs ((k, f), ys @ xs) end (*note: reverse convention also for apps!*)
    1.22 +      case int_ord (k, 0)
    1.23 +       of EQUAL => f (ys @ xs)
    1.24 +        | LESS => let val (zs, ws) = chop (~ k) ys in apps (f (ws @ xs)) zs end
    1.25 +        | GREATER => Abs ((k, f), ys @ xs) (*note: reverse convention also for apps!*)
    1.26 +      end
    1.27    | apps (Const (name, xs)) ys = Const (name, ys @ xs)
    1.28    | apps (Free (name, xs)) ys = Free (name, ys @ xs)
    1.29 -  | apps (BVar (name, xs)) ys = BVar (name, ys @ xs);
    1.30 +  | apps (BVar (n, xs)) ys = BVar (n, ys @ xs);
    1.31  
    1.32  
    1.33  (** assembling and compiling ML code from terms **)
    1.34 @@ -332,8 +332,8 @@
    1.35            in of_apps bounds (Term.Const (c, T'), ts') typidx' end
    1.36        | of_univ bounds (Free (name, ts)) typidx =
    1.37            of_apps bounds (Term.Free (name, dummyT), ts) typidx
    1.38 -      | of_univ bounds (BVar (name, ts)) typidx =
    1.39 -          of_apps bounds (Bound (bounds - name - 1), ts) typidx
    1.40 +      | of_univ bounds (BVar (n, ts)) typidx =
    1.41 +          of_apps bounds (Bound (bounds - n - 1), ts) typidx
    1.42        | of_univ bounds (t as Abs _) typidx =
    1.43            typidx
    1.44            |> of_univ (bounds + 1) (apps t [BVar (bounds, [])])