# HG changeset patch # User paulson # Date 935068397 -7200 # Node ID 52ea6848b908529229aa741d7f352f23f94320bd # Parent 29105299799c413969dae1a2817a80ec788c7d21 removed all unnecessary code diff -r 29105299799c -r 52ea6848b908 src/HOL/Tools/svc_funcs.ML --- a/src/HOL/Tools/svc_funcs.ML Thu Aug 19 15:12:51 1999 +0200 +++ b/src/HOL/Tools/svc_funcs.ML Thu Aug 19 15:13:17 1999 +0200 @@ -3,7 +3,7 @@ Author: Lawrence C Paulson Copyright 1999 University of Cambridge -Translation and abstraction functions for the interface to SVC +Translation functions for the interface to SVC Based upon the work of Søren T. Heilmann @@ -22,51 +22,37 @@ val trace = ref false; datatype expr = - bracketed_expr of expr - | ref_def_expr of string * expr - | ref_expr of string - | typed_expr of Type * expr - | buildin_expr of string * expr list - | interp_expr of string * expr list - | uninterp_expr of string * expr list - | false_expr - | true_expr - | distinct_expr of string - | int_expr of int - | rat_expr of int * int - and Type = - simple_type of string - | array_type of Type * Type - | record_type of (expr * Type) list - | bitvec_type of int; + Buildin of string * expr list + | Interp of string * expr list + | UnInterp of string * expr list + | FalseExpr + | TrueExpr + | Int of int + | Rat of int * int; open BasisLibrary + fun signedInt i = + if i < 0 then "-" ^ Int.toString (~i) + else Int.toString i; + + fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT; + + fun is_numeric T = is_intnat T orelse T = HOLogic.realT; + + fun is_numeric_op T = is_numeric (domain_type T); + fun toString t = - let fun signedInt i = - if i < 0 then "-" ^ Int.toString (~i) - else Int.toString i - fun ut(simple_type s) = s ^ " " - | ut(array_type(t1, t2)) = "ARRAY " ^ (ut t1) ^ (ut t2) - | ut(record_type fl) = - "RECORD" ^ - (foldl (fn (a, (d, t)) => a ^ (ue d) ^ (ut t)) (" ", fl)) - | ut(bitvec_type n) = "BITVEC " ^ (Int.toString n) ^ " " - and ue(bracketed_expr e) = "(" ^ (ue e) ^ ") " - | ue(ref_def_expr(r, e)) = "$" ^ r ^ ":" ^ (ue e) - | ue(ref_expr r) = "$" ^ r ^ " " - | ue(typed_expr(t, e)) = (ut t) ^ (ue e) - | ue(buildin_expr(s, l)) = + let fun ue (Buildin(s, l)) = "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") " - | ue(interp_expr(s, l)) = + | ue (Interp(s, l)) = "{" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} " - | ue(uninterp_expr(s, l)) = + | ue (UnInterp(s, l)) = "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") " - | ue(false_expr) = "FALSE " - | ue(true_expr) = "TRUE " - | ue(distinct_expr s) = "@" ^ s ^ " " - | ue(int_expr i) = (signedInt i) ^ " " - | ue(rat_expr(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " " + | ue (FalseExpr) = "FALSE " + | ue (TrueExpr) = "TRUE " + | ue (Int i) = (signedInt i) ^ " " + | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " " in ue t end; @@ -91,8 +77,8 @@ val svc_output = File.read svc_output_file handle _ => error "SVC returned no output" in - if ! trace then writeln ("SVC Returns:\n" ^ svc_output) else (); - if not (! trace) then (File.rm svc_input_file; File.rm svc_output_file) else (); + if ! trace then writeln ("SVC Returns:\n" ^ svc_output) + else (File.rm svc_input_file; File.rm svc_output_file); String.isPrefix "VALID" svc_output end @@ -103,9 +89,7 @@ let val (ts, bs) = ListPair.unzip args in (list_comb(c,ts), exists I bs) end; - fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT; - - (*Determining whether the biconditionals must be unfoled: if there are + (*Determining whether the biconditionals must be unfolded: if there are int or nat comparisons below*) val iff_tag = let fun tag t = @@ -128,19 +112,17 @@ (Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2, b1 orelse b2) end - else (*numeric equality*) (t, is_intnat T) + else (*might be numeric equality*) (t, is_intnat T) | Const("op <", Type ("fun", [T,_])) => (t, is_intnat T) | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T) | _ => (t, false) end in #1 o tag end; - (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*) fun add_nat_var (a, e) = - buildin_expr("=>", [buildin_expr("<=", [int_expr 0, - uninterp_expr (a, [])]), - e]); + Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]), + e]); (*Translate an Isabelle formula into an SVC expression pos ["positive"]: true if an assumption, false if a goal*) @@ -153,7 +135,7 @@ fun trans_var (a,T) = (if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars)) else (); - uninterp_expr (a, [])) + UnInterp (a, [])) fun var (Free(a,T)) = trans_var ("F_" ^ a, T) | var (Var((a, 0), T)) = trans_var (a, T) | var (Bound i) = @@ -167,70 +149,88 @@ | lit (Const("RealDef.0r", _)) = 0 | lit (Const("RealDef.1r", _)) = 1 (*translation of a literal expression [no variables]*) - fun litExp (Const("op +", T) $ x $ y) = (litExp x) + (litExp y) - | litExp (Const("op -", T) $ x $ y) = (litExp x) - (litExp y) - | litExp (Const("op *", T) $ x $ y) = (litExp x) * (litExp y) - | litExp (Const("uminus", _) $ x) = ~(litExp x) + fun litExp (Const("op +", T) $ x $ y) = + if is_numeric_op T then (litExp x) + (litExp y) + else raise OracleExn t + | litExp (Const("op -", T) $ x $ y) = + if is_numeric_op T then (litExp x) - (litExp y) + else raise OracleExn t + | litExp (Const("op *", T) $ x $ y) = + if is_numeric_op T then (litExp x) * (litExp y) + else raise OracleExn t + | litExp (Const("uminus", T) $ x) = + if is_numeric_op T then ~(litExp x) + else raise OracleExn t | litExp t = lit t - handle Match => raise OracleExn t + handle Match => raise OracleExn t (*translation of a real/rational expression*) - fun suc t = interp_expr("+", [int_expr 1, t]) + fun suc t = Interp("+", [Int 1, t]) fun tm (Const("Suc", T) $ x) = suc (tm x) - | tm (Const("op +", T) $ x $ y) = interp_expr("+", [tm x, tm y]) - | tm (Const("op -", _) $ x $ y) = - interp_expr("+", [tm x, interp_expr("*", [int_expr ~1, tm y])]) - | tm (Const("op *", _) $ x $ y) = interp_expr("*", [tm x, tm y]) - | tm (Const("op /", _) $ x $ y) = - interp_expr("*", [tm x, rat_expr(1, litExp y)]) - | tm (Const("uminus", _) $ x) = interp_expr("*", [int_expr ~1, tm x]) - | tm t = int_expr (lit t) + | tm (Const("op +", T) $ x $ y) = + if is_numeric_op T then Interp("+", [tm x, tm y]) + else raise OracleExn t + | tm (Const("op -", T) $ x $ y) = + if is_numeric_op T then + Interp("+", [tm x, Interp("*", [Int ~1, tm y])]) + else raise OracleExn t + | tm (Const("op *", T) $ x $ y) = + if is_numeric_op T then Interp("*", [tm x, tm y]) + else raise OracleExn t + | tm (Const("RealDef.rinv", T) $ x) = + if domain_type T = HOLogic.realT then + Rat(1, litExp x) + else raise OracleExn t + | tm (Const("uminus", T) $ x) = + if is_numeric_op T then Interp("*", [Int ~1, tm x]) + else raise OracleExn t + | tm t = Int (lit t) handle Match => var t (*translation of a formula*) and fm pos (Const("op &", _) $ p $ q) = - buildin_expr("AND", [fm pos p, fm pos q]) + Buildin("AND", [fm pos p, fm pos q]) | fm pos (Const("op |", _) $ p $ q) = - buildin_expr("OR", [fm pos p, fm pos q]) + Buildin("OR", [fm pos p, fm pos q]) | fm pos (Const("op -->", _) $ p $ q) = - buildin_expr("=>", [fm (not pos) p, fm pos q]) + Buildin("=>", [fm (not pos) p, fm pos q]) | fm pos (Const("Not", _) $ p) = - buildin_expr("NOT", [fm (not pos) p]) - | fm pos (Const("True", _)) = true_expr - | fm pos (Const("False", _)) = false_expr + Buildin("NOT", [fm (not pos) p]) + | fm pos (Const("True", _)) = TrueExpr + | fm pos (Const("False", _)) = FalseExpr | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) = (*polarity doesn't matter*) - buildin_expr("=", [fm pos p, fm pos q]) + Buildin("=", [fm pos p, fm pos q]) | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) = - buildin_expr("AND", (*unfolding uses both polarities*) - [buildin_expr("=>", [fm (not pos) p, fm pos q]), - buildin_expr("=>", [fm (not pos) q, fm pos p])]) + Buildin("AND", (*unfolding uses both polarities*) + [Buildin("=>", [fm (not pos) p, fm pos q]), + Buildin("=>", [fm (not pos) q, fm pos p])]) | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = let val tx = tm x and ty = tm y in if pos orelse T = HOLogic.realT then - buildin_expr("=", [tx, ty]) + Buildin("=", [tx, ty]) else if is_intnat T then - buildin_expr("AND", - [buildin_expr("<", [tx, suc ty]), - buildin_expr("<", [ty, suc tx])]) + Buildin("AND", + [Buildin("<", [tx, suc ty]), + Buildin("<", [ty, suc tx])]) else raise OracleExn t end (*inequalities: possible types are nat, int, real*) | fm pos (t as Const("op <", Type ("fun", [T,_])) $ x $ y) = if not pos orelse T = HOLogic.realT then - buildin_expr("<", [tm x, tm y]) + Buildin("<", [tm x, tm y]) else if is_intnat T then - buildin_expr("<=", [suc (tm x), tm y]) + Buildin("<=", [suc (tm x), tm y]) else raise OracleExn t | fm pos (t as Const("op <=", Type ("fun", [T,_])) $ x $ y) = if pos orelse T = HOLogic.realT then - buildin_expr("<=", [tm x, tm y]) + Buildin("<=", [tm x, tm y]) else if is_intnat T then - buildin_expr("<", [tm x, suc (tm y)]) + Buildin("<", [tm x, suc (tm y)]) else raise OracleExn t | fm pos t = var t; (*entry point, and translation of a meta-formula*) fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p) | mt pos ((c as Const("==>", _)) $ p $ q) = - buildin_expr("=>", [mt (not pos) p, mt pos q]) + Buildin("=>", [mt (not pos) p, mt pos q]) | mt pos t = fm pos (iff_tag t) (*it might be a formula*) val body_e = mt pos body (*evaluate now to assign into !nat_vars*) @@ -239,89 +239,14 @@ end; - (*Generalize an Isabelle formula, replacing by Vars - all subterms not intelligible to SVC. - Do not present "raw" terms to expr_of; the translation could be unsound!*) - fun abstract t = - let - val params = Term.strip_all_vars t - and body = Term.strip_all_body t - val Us = map #2 params - val nPar = length params - val vname = ref "V_a" - val pairs = ref ([] : (term*term) list) - fun insert t = - let val T = fastype_of t - val v = Unify.combound (Var ((!vname,0), Us--->T), - 0, nPar) - in vname := bump_string (!vname); - pairs := (t, v) :: !pairs; - v - end; - fun replace t = - case t of - Free _ => t (*but not existing Vars, lest the names clash*) - | Bound _ => t - | _ => (case gen_assoc (op aconv) (!pairs, t) of - Some v => v - | None => insert t) - (*abstraction of a real/rational expression*) - fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const("uminus", _)) $ x) = c $ (rat x) - | rat ((c as Const("RealDef.0r", _))) = c - | rat ((c as Const("RealDef.1r", _))) = c - | rat (t as Const("Numeral.number_of", _) $ w) = t - | rat t = replace t - (*abstraction of an integer expression: no div, mod*) - fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y) - | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y) - | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y) - | int ((c as Const("uminus", _)) $ x) = c $ (int x) - | int (t as Const("Numeral.number_of", _) $ w) = t - | int t = replace t - (*abstraction of a natural number expression: no minus*) - fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y) - | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y) - | nat ((c as Const("Suc", _)) $ x) = c $ (nat x) - | nat (t as Const("0", _)) = t - | nat (t as Const("Numeral.number_of", _) $ w) = t - | nat t = replace t - (*abstraction of a relation: =, <, <=*) - fun rel (T, c $ x $ y) = - if T = HOLogic.realT then c $ (rat x) $ (rat y) - else if T = HOLogic.intT then c $ (int x) $ (int y) - else if T = HOLogic.natT then c $ (nat x) $ (nat y) - else if T = HOLogic.boolT then c $ (fm x) $ (fm y) - else replace (c $ x $ y) (*non-numeric comparison*) - (*abstraction of a formula*) - and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q) - | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q) - | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q) - | fm ((c as Const("Not", _)) $ p) = c $ (fm p) - | fm ((c as Const("True", _))) = c - | fm ((c as Const("False", _))) = c - | fm (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = rel (T, t) - | fm (t as Const("op <", Type ("fun", [T,_])) $ x $ y) = rel (T, t) - | fm (t as Const("op <=", Type ("fun", [T,_])) $ x $ y) = rel (T, t) - | fm t = replace t - (*entry point, and abstraction of a meta-formula*) - fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p) - | mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q) - | mt t = fm t (*it might be a formula*) - in (list_all (params, mt body), !pairs) end; - - (*The oracle proves not the original formula but the abstracted version*) - fun oracle (sign, OracleExn P) = - let val (absP, _) = abstract P - val dummy = if !trace then writeln ("Subgoal abstracted to\n" ^ - Sign.string_of_term sign absP) + (*The oracle proves the given formula t, if possible*) + fun oracle (sign, OracleExn t) = + let val dummy = if !trace then writeln ("Subgoal abstracted to\n" ^ + Sign.string_of_term sign t) else () in - if valid (expr_of false absP) then absP - else raise OracleExn P + if valid (expr_of false t) then t + else raise OracleExn t end; end;