Removed thunk from Fun
authornipkow
Fri Jun 15 09:10:06 2007 +0200 (2007-06-15)
changeset 233972cc3352f6c3c
parent 23396 6d72ababc58f
child 23398 0b5a400c7595
Removed thunk from Fun
src/Pure/Tools/nbe_codegen.ML
src/Pure/Tools/nbe_eval.ML
     1.1 --- a/src/Pure/Tools/nbe_codegen.ML	Fri Jun 15 09:09:06 2007 +0200
     1.2 +++ b/src/Pure/Tools/nbe_codegen.ML	Fri Jun 15 09:10:06 2007 +0200
     1.3 @@ -74,11 +74,11 @@
     1.4  val tab_update = S.app "NBE.update";
     1.5  
     1.6  fun mk_nbeFUN(nm,e) =
     1.7 -  S.app Eval_Fun (S.tup [S.abs(S.list [MLvname nm])e,S.list [],"1",
     1.8 +  S.app Eval_Fun (S.tup [S.abs(S.list [MLvname nm])e,S.list [],"1" (*,
     1.9        S.abs(S.tup [])(S.Let 
    1.10          [S.Val (MLintern "var") (S.app Eval_new_name (S.tup [])),
    1.11           S.Val (MLvname nm) (S.app Eval_BVar (S.tup [(MLintern "var"), S.list []]))]
    1.12 -	(S.app Eval_AbsN(S.tup[MLintern "var",(S.app Eval_to_term e)])))]);
    1.13 +	(S.app Eval_AbsN(S.tup[MLintern "var",(S.app Eval_to_term e)])))*)]);
    1.14  
    1.15  fun take_last n xs = rev (Library.take(n, rev xs));
    1.16  fun drop_last n xs = rev (Library.drop(n, rev xs));
    1.17 @@ -87,10 +87,9 @@
    1.18  	if (ar <= length args) then 
    1.19  	  S.nbe_apps (S.app (MLname nm) (S.list (take_last ar args)))
    1.20  	             (drop_last ar args)
    1.21 -        else S.app Eval_Fun (S.tup [MLname nm,S.list args,
    1.22 +        else S.app Eval_Fun (S.tup [MLname nm,S.list args(*,
    1.23  	           string_of_int(ar - (length args)),
    1.24 -		   S.abs (S.tup []) (S.app Eval_C
    1.25 -	(S.quote nm))]);
    1.26 +		   S.abs (S.tup []) (S.app Eval_C (S.quote nm))*)]);
    1.27  
    1.28  fun mk_rexpr defined names ar =
    1.29    let
     2.1 --- a/src/Pure/Tools/nbe_eval.ML	Fri Jun 15 09:09:06 2007 +0200
     2.2 +++ b/src/Pure/Tools/nbe_eval.ML	Fri Jun 15 09:10:06 2007 +0200
     2.3 @@ -23,7 +23,7 @@
     2.4        Constr of string*(Univ list)       (*named constructors*)
     2.5      | Var of string*(Univ list)          (*free variables*)
     2.6      | BVar of int*(Univ list)            (*bound named variables*)
     2.7 -    | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm)
     2.8 +    | Fun of (Univ list -> Univ) * (Univ list) * int
     2.9                                           (*functions*);
    2.10  
    2.11    val eval: theory -> Univ Symtab.table -> term -> nterm
    2.12 @@ -87,12 +87,7 @@
    2.13      Constr of string*(Univ list)       (* Named Constructors *)
    2.14    | Var of string*(Univ list)          (* Free variables *)
    2.15    | BVar of int*(Univ list)         (* Bound named variables *)
    2.16 -  | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
    2.17 -
    2.18 -fun to_term (Constr(name, args))    = apps (C name) (map to_term args)
    2.19 -  | to_term (Var   (name, args))    = apps (V name) (map to_term args)
    2.20 -  | to_term (BVar  (name, args))    = apps (B name) (map to_term args)
    2.21 -  | to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args);
    2.22 +  | Fun of (Univ list -> Univ) * (Univ list) * int;
    2.23  
    2.24  (*
    2.25     A typical operation, why functions might be good for, is
    2.26 @@ -100,14 +95,14 @@
    2.27     reasonably we applied in a semantical way.
    2.28  *)
    2.29  
    2.30 -fun apply (Fun(f,xs,1,name))  x = f (x::xs)
    2.31 -  | apply (Fun(f,xs,n,name))  x = Fun(f,x::xs,n-1,name)
    2.32 +fun apply (Fun(f,xs,1))  x = f (x::xs)
    2.33 +  | apply (Fun(f,xs,n))  x = Fun(f,x::xs,n-1)
    2.34    | apply (Constr(name,args)) x = Constr(name,x::args)
    2.35    | apply (Var(name,args))    x = Var(name,x::args)
    2.36    | apply (BVar(name,args))   x = BVar(name,x::args);
    2.37  
    2.38  fun mk_Fun(name,v,0) = (name,v [])
    2.39 -  | mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name));
    2.40 +  | mk_Fun(name,v,n) = (name,Fun(v,[],n));
    2.41  
    2.42  
    2.43  (* ------------------ evaluation with greetings to Tarski ------------------ *)
    2.44 @@ -117,8 +112,7 @@
    2.45    | prep_term thy (Free v_ty) = Free v_ty
    2.46    | prep_term thy (s $ t) = prep_term thy s $ prep_term thy t
    2.47    | prep_term thy (Abs (raw_v, ty, raw_t)) =
    2.48 -      let
    2.49 -        val (v, t) = Syntax.variant_abs (raw_v, ty, raw_t);
    2.50 +      let val (v,t) = Syntax.variant_abs (raw_v, ty, raw_t);
    2.51        in Abs (v, ty, prep_term thy t) end;
    2.52  
    2.53  
    2.54 @@ -127,6 +121,13 @@
    2.55  val counter = ref 0;
    2.56  fun new_name () = (counter := !counter +1; !counter);
    2.57  
    2.58 +fun to_term (Constr(name, args))    = apps (C name) (map to_term args)
    2.59 +  | to_term (Var   (name, args))    = apps (V name) (map to_term args)
    2.60 +  | to_term (BVar  (name, args))    = apps (B name) (map to_term args)
    2.61 +  | to_term (F as Fun _) =
    2.62 +      let val var = new_name()
    2.63 +      in AbsN(var, to_term (apply F (BVar(var,[])))) end;
    2.64 +
    2.65  
    2.66  (* greetings to Tarski *)
    2.67  
    2.68 @@ -139,9 +140,7 @@
    2.69        | evl vars (s $ t) =
    2.70            apply (evl vars s) (evl vars t)
    2.71        | evl vars (Abs (v, _, t)) =
    2.72 -          Fun (fn [x] => evl (AList.update (op =) (v, x) vars) t, [], 1,
    2.73 -            fn () => let val var = new_name() in
    2.74 -              AbsN (var, to_term (evl (AList.update (op =) (v, BVar (var, [])) vars) t)) end)
    2.75 +          Fun (fn [x] => evl (AList.update (op =) (v, x) vars) t, [], 1)
    2.76    in (counter := 0; to_term (evl [] (prep_term thy t))) end;
    2.77  
    2.78  end;