--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/svc_funcs.ML Mon Aug 02 11:29:13 1999 +0200
@@ -0,0 +1,256 @@
+(* Title: HOL/Tools/svc_funcs.ML
+ ID: $Id$
+ Author: Lawrence C Paulson
+ Copyright 1999 University of Cambridge
+
+Translation and abstraction functions for the interface to SVC
+
+Based upon the work of Søren T. Heilmann
+*)
+
+(**TODO
+ change Path.pack to File.sysify_path
+ move realT to hologic.ML**)
+
+val realT = Type("RealDef.real",[]);
+
+
+
+structure Svc =
+struct
+ 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;
+
+ open BasisLibrary
+
+ 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)) =
+ "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
+ | ue(interp_expr(s, l)) =
+ "{" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
+ | ue(uninterp_expr(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) ^ " "
+ in
+ ue t
+ end;
+
+ fun valid e =
+ let val svc_home = getenv "SVC_HOME"
+ val svc_machine = getenv "SVC_MACHINE"
+ val check_valid = if svc_home = ""
+ then error "Environment variable SVC_HOME not set"
+ else if svc_machine = ""
+ then error "Environment variable SVC_MACHINE not set"
+ else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
+ val svc_input = toString e
+ val _ = if !trace then writeln ("Calling SVC:\n" ^ svc_input) else ()
+ val svc_input_file = File.tmp_path (Path.basic "SVM_in");
+ val svc_output_file = File.tmp_path (Path.basic "SVM_out");
+ val _ = (File.write svc_input_file svc_input;
+ execute (check_valid ^ " -dump-result " ^
+ Path.pack svc_output_file ^
+ " " ^ Path.pack svc_input_file ^
+ "> /dev/null 2>&1"))
+ val svc_output = File.read svc_output_file
+ handle _ => error "SVC returned no output"
+ val _ = if !trace then writeln ("SVC Returns:\n" ^ svc_output) else ()
+ in
+ String.isPrefix "VALID" svc_output
+ end
+
+ (*New exception constructor for passing arguments to the oracle*)
+ exception OracleExn of term;
+
+ (*Translate an Isabelle formula into an SVC expression
+ pos ["positive"]: true if an assumption, false if a goal*)
+ fun expr_of pos t =
+ let
+ val params = rename_wrt_term t (Term.strip_all_vars t)
+ and body = Term.strip_all_body t
+ val parNames = rev (map #1 params)
+ (*translation of a variable*)
+ fun var (Free(a, _)) = uninterp_expr("F_" ^ a, [])
+ | var (Var((a, 0), _)) = uninterp_expr(a, [])
+ | var (Bound i) = uninterp_expr("B_" ^ List.nth (parNames,i), [])
+ | var (t $ Bound _) = var t (*removing a parameter from a Var*)
+ | var t = raise OracleExn t;
+ (*translation of a literal*)
+ fun lit (Const("Numeral.number_of", _) $ w) = NumeralSyntax.dest_bin w
+ | lit (Const("0", _)) = 0
+ | lit (Const("0r", _)) = 0
+ | lit (Const("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)
+ | litExp t = lit t
+ handle Match => raise OracleExn t
+ (*translation of a real/rational expression*)
+ fun suc t = interp_expr("+", [int_expr 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)
+ handle Match => var t
+ (*translation of a formula*)
+ and fm pos (Const("op &", _) $ p $ q) =
+ buildin_expr("AND", [fm pos p, fm pos q])
+ | fm pos (Const("op |", _) $ p $ q) =
+ buildin_expr("OR", [fm pos p, fm pos q])
+ | fm pos (Const("op -->", _) $ p $ q) =
+ buildin_expr("=>", [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
+ | fm pos (Const("op =", Type ("fun", [T,_])) $ x $ y) =
+ if T = HOLogic.boolT then buildin_expr("=", [fm pos x, fm pos y])
+ else
+ let val tx = tm x and ty = tm y
+ in if pos orelse T = realT then
+ buildin_expr("=", [tx, ty])
+ else
+ buildin_expr("AND",
+ [buildin_expr("<", [tx, suc ty]),
+ buildin_expr("<", [ty, suc tx])])
+ end
+ (*inequalities: possible types are nat, int, real*)
+ | fm pos (Const("op <", Type ("fun", [T,_])) $ x $ y) =
+ if not pos orelse T = realT then
+ buildin_expr("<", [tm x, tm y])
+ else buildin_expr("<=", [suc (tm x), tm y])
+ | fm pos (Const("op <=", Type ("fun", [T,_])) $ x $ y) =
+ if pos orelse T = realT then
+ buildin_expr("<=", [tm x, tm y])
+ else buildin_expr("<", [tm x, suc (tm y)])
+ | fm pos t = var t;
+ (*entry point, and translation of a meta-formula*)
+ fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos p
+ | mt pos ((c as Const("==>", _)) $ p $ q) =
+ buildin_expr("=>", [mt (not pos) p, mt pos q])
+ | mt pos t = fm pos t (*it might be a formula*)
+ in
+ mt pos body
+ end;
+
+
+ (*Generalize an Isabelle formula, replacing by Vars
+ all subterms not intelligible to SVC. *)
+ 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("0r", _))) = c
+ | rat ((c as Const("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 = 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;
+
+ fun oracle (sign, OracleExn svc_form) =
+ if valid (expr_of false svc_form) then svc_form
+ else raise OracleExn svc_form;
+
+end;