23 | Var of string*(Univ list) (*free variables*) |
23 | Var of string*(Univ list) (*free variables*) |
24 | BVar of int*(Univ list) (*bound named variables*) |
24 | BVar of int*(Univ list) (*bound named variables*) |
25 | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm) |
25 | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm) |
26 (*functions*); |
26 (*functions*); |
27 |
27 |
28 val nbe: Univ Symtab.table -> CodegenThingol.iterm -> nterm |
28 val nbe: theory -> Univ Symtab.table -> term -> nterm |
29 val apply: Univ -> Univ -> Univ |
29 val apply: Univ -> Univ -> Univ |
|
30 val prep_term: theory -> term -> term |
30 |
31 |
31 val to_term: Univ -> nterm |
32 val to_term: Univ -> nterm |
32 |
33 |
33 val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ |
34 val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ |
34 val new_name: unit -> int |
35 val new_name: unit -> int |
105 | apply (BVar(name,args)) x = BVar(name,x::args); |
106 | apply (BVar(name,args)) x = BVar(name,x::args); |
106 |
107 |
107 fun mk_Fun(name,v,0) = (name,v []) |
108 fun mk_Fun(name,v,0) = (name,v []) |
108 | mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name)); |
109 | mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name)); |
109 |
110 |
110 (* ---------------- table with the meaning of constants -------------------- *) |
|
111 |
|
112 val xfun_tab: Univ Symtab.table ref = ref Symtab.empty; |
|
113 |
|
114 fun lookup s = case Symtab.lookup (!xfun_tab) s of |
|
115 SOME x => x |
|
116 | NONE => Constr(s,[]); |
|
117 |
111 |
118 (* ------------------ evaluation with greetings to Tarski ------------------ *) |
112 (* ------------------ evaluation with greetings to Tarski ------------------ *) |
|
113 |
|
114 fun prep_term thy (Const c) = Const (CodegenNames.const thy (CodegenConsts.norm_of_typ thy c), dummyT) |
|
115 | prep_term thy (Free v_ty) = Free v_ty |
|
116 | prep_term thy (s $ t) = prep_term thy s $ prep_term thy t |
|
117 | prep_term thy (Abs (raw_v, ty, raw_t)) = |
|
118 let |
|
119 val (v, t) = Syntax.variant_abs (CodegenNames.purify_var raw_v, ty, raw_t); |
|
120 in Abs (v, ty, prep_term thy t) end; |
|
121 |
119 |
122 |
120 (* generation of fresh names *) |
123 (* generation of fresh names *) |
121 |
124 |
122 val counter = ref 0; |
125 val counter = ref 0; |
123 |
126 |
124 fun new_name () = (counter := !counter +1; !counter); |
127 fun new_name () = (counter := !counter +1; !counter); |
125 |
128 |
126 (* greetings to Tarski *) |
129 (* greetings to Tarski *) |
127 |
130 |
128 open BasicCodegenThingol; |
131 fun eval lookup = |
|
132 let |
|
133 fun evl vars (Const (s, _)) = lookup s |
|
134 | evl vars (Free (v, _)) = |
|
135 AList.lookup (op =) vars v |
|
136 |> the_default (Var (v, [])) |
|
137 | evl vars (s $ t) = apply (evl vars s) (evl vars t) |
|
138 | evl vars (Abs (v, _, t)) = |
|
139 Fun (fn [x] => evl (AList.update (op =) (v, x) vars) t, |
|
140 [], 1, |
|
141 fn () => let val var = new_name() in |
|
142 AbsN (var, to_term (evl (AList.update (op =) (v, BVar (var, [])) vars) t)) end) |
|
143 in evl end; |
129 |
144 |
130 fun eval xs = |
|
131 let |
|
132 fun evl (IConst (c, _)) = lookup c |
|
133 | evl (IVar n) = |
|
134 AList.lookup (op =) xs n |
|
135 |> the_default (Var (n, [])) |
|
136 | evl (s `$ t) = apply (eval xs s) (eval xs t) |
|
137 | evl ((n, _) `|-> t) = |
|
138 Fun (fn [x] => eval (AList.update (op =) (n, x) xs) t, |
|
139 [], 1, |
|
140 fn () => let val var = new_name() in |
|
141 AbsN (var, to_term (eval (AList.update (op =) (n, BVar (var, [])) xs) t)) end) |
|
142 in CodegenThingol.map_pure evl end; |
|
143 |
145 |
144 (* finally... *) |
146 (* finally... *) |
145 |
147 |
146 fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval [] t)); |
148 fun nbe thy tab t = |
|
149 let |
|
150 fun lookup s = case Symtab.lookup tab s |
|
151 of SOME x => x |
|
152 | NONE => Constr (s, []); |
|
153 in (counter := 0; to_term (eval lookup [] (prep_term thy t))) end; |
147 |
154 |
148 end; |
155 end; |