23174

1 
(* Title: Tools/Compute_Oracle/compute.ML


2 
ID: $Id$


3 
Author: Steven Obua


4 
*)


5 


6 
signature COMPUTE = sig


7 


8 
type computer


9 


10 
exception Make of string


11 


12 
val basic_make : theory > thm list > computer


13 
val make : theory > thm list > computer


14 


15 
val compute : computer > (int > string) > cterm > term


16 
val theory_of : computer > theory


17 


18 
val default_naming: int > string


19 
val oracle_fn: theory > computer * (int > string) * cterm > term


20 
end


21 


22 
structure Compute: COMPUTE = struct


23 


24 
exception Make of string;


25 


26 
fun is_mono_typ (Type (_, list)) = forall is_mono_typ list


27 
 is_mono_typ _ = false


28 


29 
fun is_mono_term (Const (_, t)) = is_mono_typ t


30 
 is_mono_term (Var (_, t)) = is_mono_typ t


31 
 is_mono_term (Free (_, t)) = is_mono_typ t


32 
 is_mono_term (Bound _) = true


33 
 is_mono_term (a $ b) = is_mono_term a andalso is_mono_term b


34 
 is_mono_term (Abs (_, ty, t)) = is_mono_typ ty andalso is_mono_term t


35 


36 
structure AMTermTab = TableFun (type key = AbstractMachine.term val ord = AM_Util.term_ord)


37 


38 
fun add x y = x + y : int;


39 
fun inc x = x + 1;


40 


41 
exception Mono of term;


42 


43 
val remove_types =


44 
let


45 
fun remove_types_var table invtable ccount vcount ldepth t =


46 
(case Termtab.lookup table t of


47 
NONE =>


48 
let


49 
val a = AbstractMachine.Var vcount


50 
in


51 
(Termtab.update (t, a) table,


52 
AMTermTab.update (a, t) invtable,


53 
ccount,


54 
inc vcount,


55 
AbstractMachine.Var (add vcount ldepth))


56 
end


57 
 SOME (AbstractMachine.Var v) =>


58 
(table, invtable, ccount, vcount, AbstractMachine.Var (add v ldepth))


59 
 SOME _ => sys_error "remove_types_var: lookup should be a var")


60 


61 
fun remove_types_const table invtable ccount vcount ldepth t =


62 
(case Termtab.lookup table t of


63 
NONE =>


64 
let


65 
val a = AbstractMachine.Const ccount


66 
in


67 
(Termtab.update (t, a) table,


68 
AMTermTab.update (a, t) invtable,


69 
inc ccount,


70 
vcount,


71 
a)


72 
end


73 
 SOME (c as AbstractMachine.Const _) =>


74 
(table, invtable, ccount, vcount, c)


75 
 SOME _ => sys_error "remove_types_const: lookup should be a const")


76 


77 
fun remove_types table invtable ccount vcount ldepth t =


78 
case t of


79 
Var (_, ty) =>


80 
if is_mono_typ ty then remove_types_var table invtable ccount vcount ldepth t


81 
else raise (Mono t)


82 
 Free (_, ty) =>


83 
if is_mono_typ ty then remove_types_var table invtable ccount vcount ldepth t


84 
else raise (Mono t)


85 
 Const (_, ty) =>


86 
if is_mono_typ ty then remove_types_const table invtable ccount vcount ldepth t


87 
else raise (Mono t)


88 
 Abs (_, ty, t') =>


89 
if is_mono_typ ty then


90 
let


91 
val (table, invtable, ccount, vcount, t') =


92 
remove_types table invtable ccount vcount (inc ldepth) t'


93 
in


94 
(table, invtable, ccount, vcount, AbstractMachine.Abs t')


95 
end


96 
else


97 
raise (Mono t)


98 
 a $ b =>


99 
let


100 
val (table, invtable, ccount, vcount, a) =


101 
remove_types table invtable ccount vcount ldepth a


102 
val (table, invtable, ccount, vcount, b) =


103 
remove_types table invtable ccount vcount ldepth b


104 
in


105 
(table, invtable, ccount, vcount, AbstractMachine.App (a,b))


106 
end


107 
 Bound b => (table, invtable, ccount, vcount, AbstractMachine.Var b)


108 
in


109 
fn (table, invtable, ccount, vcount) => remove_types table invtable ccount vcount 0


110 
end


111 


112 
fun infer_types naming =


113 
let


114 
fun infer_types invtable ldepth bounds ty (AbstractMachine.Var v) =


115 
if v < ldepth then (Bound v, List.nth (bounds, v)) else


116 
(case AMTermTab.lookup invtable (AbstractMachine.Var (vldepth)) of


117 
SOME (t as Var (_, ty)) => (t, ty)


118 
 SOME (t as Free (_, ty)) => (t, ty)


119 
 _ => sys_error "infer_types: lookup should deliver Var or Free")


120 
 infer_types invtable ldepth _ ty (c as AbstractMachine.Const _) =


121 
(case AMTermTab.lookup invtable c of


122 
SOME (c as Const (_, ty)) => (c, ty)


123 
 _ => sys_error "infer_types: lookup should deliver Const")


124 
 infer_types invtable ldepth bounds (n,ty) (AbstractMachine.App (a, b)) =


125 
let


126 
val (a, aty) = infer_types invtable ldepth bounds (n+1, ty) a


127 
val (adom, arange) =


128 
case aty of


129 
Type ("fun", [dom, range]) => (dom, range)


130 
 _ => sys_error "infer_types: function type expected"


131 
val (b, bty) = infer_types invtable ldepth bounds (0, adom) b


132 
in


133 
(a $ b, arange)


134 
end


135 
 infer_types invtable ldepth bounds (0, ty as Type ("fun", [dom, range]))


136 
(AbstractMachine.Abs m) =


137 
let


138 
val (m, _) = infer_types invtable (ldepth+1) (dom::bounds) (0, range) m


139 
in


140 
(Abs (naming ldepth, dom, m), ty)


141 
end


142 
 infer_types invtable ldepth bounds ty (AbstractMachine.Abs m) =


143 
sys_error "infer_types: cannot infer type of abstraction"


144 


145 
fun infer invtable ty term =


146 
let


147 
val (term', _) = infer_types invtable 0 [] (0, ty) term


148 
in


149 
term'


150 
end


151 
in


152 
infer


153 
end


154 


155 
datatype computer =


156 
Computer of theory_ref *


157 
(AbstractMachine.term Termtab.table * term AMTermTab.table * int * AbstractMachine.program)


158 


159 
fun basic_make thy raw_ths =


160 
let


161 
val ths = map (Thm.transfer thy) raw_ths;


162 


163 
fun thm2rule table invtable ccount th =


164 
let


165 
val prop = Thm.plain_prop_of th


166 
handle THM _ => raise (Make "theorems must be plain propositions")


167 
val (a, b) = Logic.dest_equals prop


168 
handle TERM _ => raise (Make "theorems must be metalevel equations")


169 


170 
val (table, invtable, ccount, vcount, prop) =


171 
remove_types (table, invtable, ccount, 0) (a$b)


172 
handle Mono _ => raise (Make "no type variables allowed")


173 
val (left, right) =


174 
(case prop of AbstractMachine.App x => x  _ =>


175 
sys_error "make: remove_types should deliver application")


176 


177 
fun make_pattern table invtable n vars (var as AbstractMachine.Var v) =


178 
let


179 
val var' = the (AMTermTab.lookup invtable var)


180 
val table = Termtab.delete var' table


181 
val invtable = AMTermTab.delete var invtable


182 
val vars = Inttab.update_new (v, n) vars handle Inttab.DUP _ =>


183 
raise (Make "no duplicate variable in pattern allowed")


184 
in


185 
(table, invtable, n+1, vars, AbstractMachine.PVar)


186 
end


187 
 make_pattern table invtable n vars (AbstractMachine.Abs _) =


188 
raise (Make "no lambda abstractions allowed in pattern")


189 
 make_pattern table invtable n vars (AbstractMachine.Const c) =


190 
(table, invtable, n, vars, AbstractMachine.PConst (c, []))


191 
 make_pattern table invtable n vars (AbstractMachine.App (a, b)) =


192 
let


193 
val (table, invtable, n, vars, pa) =


194 
make_pattern table invtable n vars a


195 
val (table, invtable, n, vars, pb) =


196 
make_pattern table invtable n vars b


197 
in


198 
case pa of


199 
AbstractMachine.PVar =>


200 
raise (Make "patterns may not start with a variable")


201 
 AbstractMachine.PConst (c, args) =>


202 
(table, invtable, n, vars, AbstractMachine.PConst (c, args@[pb]))


203 
end


204 


205 
val (table, invtable, vcount, vars, pattern) =


206 
make_pattern table invtable 0 Inttab.empty left


207 
val _ = (case pattern of


208 
AbstractMachine.PVar =>


209 
raise (Make "patterns may not start with a variable")


210 
 _ => ())


211 


212 
(* at this point, there shouldn't be any variables


213 
left in table or invtable, only constants *)


214 


215 
(* finally, provide a function for renaming the


216 
pattern bound variables on the right hand side *)


217 


218 
fun rename ldepth vars (var as AbstractMachine.Var v) =


219 
if v < ldepth then var


220 
else (case Inttab.lookup vars (v  ldepth) of


221 
NONE => raise (Make "new variable on right hand side")


222 
 SOME n => AbstractMachine.Var ((vcountn1)+ldepth))


223 
 rename ldepth vars (c as AbstractMachine.Const _) = c


224 
 rename ldepth vars (AbstractMachine.App (a, b)) =


225 
AbstractMachine.App (rename ldepth vars a, rename ldepth vars b)


226 
 rename ldepth vars (AbstractMachine.Abs m) =


227 
AbstractMachine.Abs (rename (ldepth+1) vars m)


228 


229 
in


230 
(table, invtable, ccount, (pattern, rename 0 vars right))


231 
end


232 


233 
val (table, invtable, ccount, rules) =


234 
fold_rev (fn th => fn (table, invtable, ccount, rules) =>


235 
let


236 
val (table, invtable, ccount, rule) =


237 
thm2rule table invtable ccount th


238 
in (table, invtable, ccount, rule::rules) end)


239 
ths (Termtab.empty, AMTermTab.empty, 0, [])


240 


241 
val prog = AbstractMachine.compile rules


242 


243 
in Computer (Theory.self_ref thy, (table, invtable, ccount, prog)) end


244 


245 
fun make thy ths =


246 
let


247 
val (_, {mk_rews={mk=mk,mk_eq_True=emk, ...},...}) = rep_ss (simpset_of thy)


248 
fun mk_eq_True th = (case emk th of NONE => [th]  SOME th' => [th, th'])


249 
in


250 
basic_make thy (maps mk (maps mk_eq_True ths))


251 
end


252 


253 
fun compute (Computer r) naming ct =


254 
let


255 
val {t=t, T=ty, thy=ctthy, ...} = rep_cterm ct


256 
val (rthy, (table, invtable, ccount, prog)) = r


257 
val thy = Theory.merge (Theory.deref rthy, ctthy)


258 
val (table, invtable, ccount, vcount, t) = remove_types (table, invtable, ccount, 0) t


259 
val t = AbstractMachine.run prog t


260 
val t = infer_types naming invtable ty t


261 
in


262 
t


263 
end


264 


265 
fun theory_of (Computer (rthy, _)) = Theory.deref rthy


266 


267 
fun default_naming i = "v_" ^ Int.toString i


268 


269 


270 
fun oracle_fn thy (r, naming, ct) =


271 
let


272 
val _ = Theory.assert_super (theory_of r) thy


273 
val t' = compute r naming ct


274 
in


275 
Logic.mk_equals (term_of ct, t')


276 
end


277 


278 
end
