improving translation to prolog; restoring terms from prolog output; adding tracing support
1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Jul 29 17:27:57 2010 +0200
1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Jul 29 17:27:57 2010 +0200
1.3 @@ -6,20 +6,28 @@
1.4
1.5 signature CODE_PROLOG =
1.6 sig
1.7 - datatype term = Var of string * typ | Cons of string | AppF of string * term list;
1.8 - datatype prem = Conj of prem list | NotRel of string * term list | Rel of string * term list | Eq of term * term | NotEq of term * term;
1.9 - type clause = ((string * term list) * prem);
1.10 + datatype prol_term = Var of string * typ | Cons of string | AppF of string * prol_term list;
1.11 + datatype prem = Conj of prem list | NotRel of string * prol_term list
1.12 + | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term;
1.13 + type clause = ((string * prol_term list) * prem);
1.14 type logic_program = clause list;
1.15 + type constant_table = (string * string) list
1.16 +
1.17 + val generate : Proof.context -> string list -> (logic_program * constant_table)
1.18 + val write_program : logic_program -> string
1.19 + val run : logic_program -> string -> string list -> int option -> prol_term list list
1.20
1.21 - val generate : Proof.context -> string list -> logic_program
1.22 - val write_program : logic_program -> string
1.23 - val run : logic_program -> string -> string list -> int option -> term list
1.24 -
1.25 + val trace : bool Unsynchronized.ref
1.26 end;
1.27
1.28 structure Code_Prolog : CODE_PROLOG =
1.29 struct
1.30
1.31 +(* diagnostic tracing *)
1.32 +
1.33 +val trace = Unsynchronized.ref false
1.34 +
1.35 +fun tracing s = if !trace then Output.tracing s else ()
1.36 (* general string functions *)
1.37
1.38 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
1.39 @@ -27,59 +35,88 @@
1.40
1.41 (* internal program representation *)
1.42
1.43 -datatype term = Var of string * typ | Cons of string | AppF of string * term list;
1.44 +datatype prol_term = Var of string * typ | Cons of string | AppF of string * prol_term list;
1.45
1.46 fun string_of_prol_term (Var (s, T)) = "Var " ^ s
1.47 | string_of_prol_term (Cons s) = "Cons " ^ s
1.48 | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")"
1.49
1.50 -datatype prem = Conj of prem list | NotRel of string * term list | Rel of string * term list | Eq of term * term | NotEq of term * term;
1.51 +datatype prem = Conj of prem list | NotRel of string * prol_term list
1.52 + | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term;
1.53
1.54 fun dest_Rel (Rel (c, ts)) = (c, ts)
1.55
1.56 -type clause = ((string * term list) * prem);
1.57 +type clause = ((string * prol_term list) * prem);
1.58
1.59 type logic_program = clause list;
1.60
1.61 (* translation from introduction rules to internal representation *)
1.62
1.63 +(** constant table **)
1.64 +
1.65 +type constant_table = (string * string) list
1.66 +
1.67 (* assuming no clashing *)
1.68 -fun translate_const c = Long_Name.base_name c
1.69 +fun mk_constant_table consts =
1.70 + AList.make (first_lower o Long_Name.base_name) consts
1.71
1.72 -fun translate_term ctxt t =
1.73 +fun declare_consts consts constant_table =
1.74 + fold (fn c => AList.update (op =) (c, first_lower (Long_Name.base_name c))) consts constant_table
1.75 +
1.76 +fun translate_const constant_table c =
1.77 + case AList.lookup (op =) constant_table c of
1.78 + SOME c' => c'
1.79 + | NONE => error ("No such constant: " ^ c)
1.80 +
1.81 +fun inv_lookup _ [] _ = NONE
1.82 + | inv_lookup eq ((key, value)::xs) value' =
1.83 + if eq (value', value) then SOME key
1.84 + else inv_lookup eq xs value';
1.85 +
1.86 +fun restore_const constant_table c =
1.87 + case inv_lookup (op =) constant_table c of
1.88 + SOME c' => c'
1.89 + | NONE => error ("No constant corresponding to " ^ c)
1.90 +
1.91 +(** translation of terms, literals, premises, and clauses **)
1.92 +
1.93 +fun translate_term ctxt constant_table t =
1.94 case strip_comb t of
1.95 (Free (v, T), []) => Var (v, T)
1.96 - | (Const (c, _), []) => Cons (translate_const c)
1.97 - | (Const (c, _), args) => AppF (translate_const c, map (translate_term ctxt) args)
1.98 + | (Const (c, _), []) => Cons (translate_const constant_table c)
1.99 + | (Const (c, _), args) =>
1.100 + AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args)
1.101 | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t)
1.102
1.103 -
1.104 -fun translate_literal ctxt t =
1.105 +fun translate_literal ctxt constant_table t =
1.106 case strip_comb t of
1.107 - (Const (@{const_name "op ="}, _), [l, r]) => Eq (pairself (translate_term ctxt) (l, r))
1.108 - | (Const (c, _), args) => Rel (translate_const c, map (translate_term ctxt) args)
1.109 + (Const (@{const_name "op ="}, _), [l, r]) =>
1.110 + Eq (pairself (translate_term ctxt constant_table) (l, r))
1.111 + | (Const (c, _), args) =>
1.112 + Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args)
1.113 | _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t)
1.114
1.115 fun NegRel_of (Rel lit) = NotRel lit
1.116 | NegRel_of (Eq eq) = NotEq eq
1.117
1.118 -fun translate_prem ctxt t =
1.119 +fun translate_prem ctxt constant_table t =
1.120 case try HOLogic.dest_not t of
1.121 - SOME t => NegRel_of (translate_literal ctxt t)
1.122 - | NONE => translate_literal ctxt t
1.123 + SOME t => NegRel_of (translate_literal ctxt constant_table t)
1.124 + | NONE => translate_literal ctxt constant_table t
1.125
1.126 -fun translate_intros ctxt gr const =
1.127 +fun translate_intros ctxt gr const constant_table =
1.128 let
1.129 val intros = Graph.get_node gr const
1.130 val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
1.131 + val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table
1.132 fun translate_intro intro =
1.133 let
1.134 val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro)
1.135 val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems intro)
1.136 - val prems' = Conj (map (translate_prem ctxt') prems)
1.137 - val clause = (dest_Rel (translate_literal ctxt' head), prems')
1.138 + val prems' = Conj (map (translate_prem ctxt' constant_table') prems)
1.139 + val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
1.140 in clause end
1.141 - in map translate_intro intros' end
1.142 + in (map translate_intro intros', constant_table') end
1.143
1.144 fun generate ctxt const =
1.145 let
1.146 @@ -87,8 +124,9 @@
1.147 Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
1.148 val gr = Predicate_Compile_Core.intros_graph_of ctxt
1.149 val scc = strong_conn_of gr const
1.150 + val constant_table = mk_constant_table (flat scc)
1.151 in
1.152 - maps (translate_intros ctxt gr) (flat scc)
1.153 + apfst flat (fold_map (translate_intros ctxt gr) (flat scc) constant_table)
1.154 end
1.155
1.156 (* transform logic program *)
1.157 @@ -121,8 +159,8 @@
1.158 (* code printer *)
1.159
1.160 fun write_term (Var (v, _)) = first_upper v
1.161 - | write_term (Cons c) = first_lower c
1.162 - | write_term (AppF (f, args)) = first_lower f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
1.163 + | write_term (Cons c) = c
1.164 + | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
1.165
1.166 fun write_rel (pred, args) =
1.167 pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
1.168 @@ -143,15 +181,15 @@
1.169
1.170 fun query_first rel vnames =
1.171 "eval :- once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
1.172 - "writef('" ^ implode (map (fn v => v ^ " = %w\\n") vnames) ^"', [" ^ space_implode ", " vnames ^ "]).\n"
1.173 + "writef('" ^ implode (map (fn v => v ^ " = %w; ") vnames) ^"\\n', [" ^ space_implode ", " vnames ^ "]).\n"
1.174
1.175 fun query_firstn n rel vnames =
1.176 "eval :- findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^
1.177 rel ^ "(" ^ space_implode ", " vnames ^ "), Sols), writelist(Sols).\n" ^
1.178 "writelist([]).\n" ^
1.179 "writelist([(" ^ space_implode ", " vnames ^ ")|T]) :- " ^
1.180 - "writef('" ^ implode (map (fn v => v ^ " = %w\\n") vnames) ^
1.181 - "', [" ^ space_implode ", " vnames ^ "]), writelist(T).\n"
1.182 + "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
1.183 + "\\n', [" ^ space_implode ", " vnames ^ "]), writelist(T).\n"
1.184
1.185 val prelude =
1.186 "#!/usr/bin/swipl -q -t main -f\n\n" ^
1.187 @@ -181,47 +219,27 @@
1.188
1.189 val is_var_ident =
1.190 forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
1.191 -(*
1.192 -fun repeat_sep sep scan =
1.193 - let
1.194 - fun rep ys xs =
1.195 - (case (SOME (scan xs) handle FAIL _ => NONE) of
1.196 - NONE => (rev ys, xs)
1.197 - | SOME (y, xs') =>
1.198 - case (SOME (scan sep) handle FAIL _ => NONE) of
1.199 - NONE => (rev (y :: ys), xs')
1.200 - | SOME (_, xs'') => rep (y :: ys) xs'')
1.201 - in rep [] end;
1.202 -
1.203 -fun repeat_sep1 sep scan = (scan --| sep) ::: repeat_sep sep scan;
1.204 -*)
1.205
1.206 fun scan_terms xs = (((scan_term --| $$ ",") ::: scan_terms)
1.207 || (scan_term >> single)) xs
1.208 and scan_term xs =
1.209 ((scan_var >> (fn s => Var (string_of s, dummyT)))
1.210 || ((scan_atom -- ($$ "(" |-- scan_terms --| $$ ")"))
1.211 - >> (fn (f, ts) => AppF (string_of f, rev ts)))
1.212 + >> (fn (f, ts) => AppF (string_of f, ts)))
1.213 || (scan_atom >> (Cons o string_of))) xs
1.214 -(*
1.215 -val scan_term =
1.216 - scan_ident >> (fn s =>
1.217 - if is_var_ident s then (Var (string_of s, dummyT))
1.218 - else if is_atom_ident s then
1.219 - else Cons (string_of s)
1.220 - else raise Fail "unexpected")
1.221 -*)
1.222 +
1.223 val parse_term = fst o Scan.finite Symbol.stopper
1.224 (Scan.error (!! (fn _ => raise Fail "parsing prolog output failed")) scan_term)
1.225 o explode
1.226
1.227 -fun parse_solution sol =
1.228 +fun parse_solutions sol =
1.229 let
1.230 fun dest_eq s = case space_explode "=" s of
1.231 (l :: r :: []) => parse_term (unprefix " " r)
1.232 | _ => raise Fail "unexpected equation in prolog output"
1.233 + fun parse_solution s = map dest_eq (space_explode ";" s)
1.234 in
1.235 - map dest_eq (fst (split_last (space_explode "\n" sol)))
1.236 + map parse_solution (fst (split_last (space_explode "\n" sol)))
1.237 end
1.238
1.239 (* calling external interpreter and getting results *)
1.240 @@ -231,20 +249,33 @@
1.241 val cmd = Path.named_root
1.242 val query = case nsols of NONE => query_first | SOME n => query_firstn n
1.243 val prog = prelude ^ query query_rel vnames ^ write_program p
1.244 + val _ = tracing ("Generated prolog program:\n" ^ prog)
1.245 val prolog_file = File.tmp_path (Path.basic "prolog_file")
1.246 val _ = File.write prolog_file prog
1.247 val (solution, _) = bash_output ("/usr/local/bin/swipl -f " ^ File.shell_path prolog_file)
1.248 - val ts = parse_solution solution
1.249 + val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
1.250 + val tss = parse_solutions solution
1.251 in
1.252 - ts
1.253 + tss
1.254 end
1.255
1.256 (* values command *)
1.257
1.258 -fun mk_term (Var (s, T)) = Free (s, T)
1.259 - | mk_term (Cons s) = Const (s, dummyT)
1.260 - | mk_term (AppF (f, args)) = list_comb (Const (f, dummyT), map mk_term args)
1.261 -
1.262 +fun restore_term ctxt constant_table (Var (s, _), T) = Free (s, T)
1.263 + | restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T)
1.264 + | restore_term ctxt constant_table (AppF (f, args), T) =
1.265 + let
1.266 + val thy = ProofContext.theory_of ctxt
1.267 + val c = restore_const constant_table f
1.268 + val cT = Sign.the_const_type thy c
1.269 + val (argsT, resT) = strip_type cT
1.270 + val subst = Sign.typ_match thy (resT, T) Vartab.empty
1.271 + val argsT' = map (Envir.subst_type subst) argsT
1.272 + in
1.273 + list_comb (Const (c, Envir.subst_type subst cT),
1.274 + map (restore_term ctxt constant_table) (args ~~ argsT'))
1.275 + end
1.276 +
1.277 fun values ctxt soln t_compr =
1.278 let
1.279 val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
1.280 @@ -262,9 +293,21 @@
1.281 case try (map (fst o dest_Free)) all_args of
1.282 SOME vs => vs
1.283 | NONE => error ("Not only free variables in " ^ commas (map (Syntax.string_of_term ctxt) all_args))
1.284 - val ts = run (generate ctxt [name]) (translate_const name) (map first_upper vnames) soln
1.285 + val _ = tracing "Generating prolog program..."
1.286 + val (p, constant_table) = generate ctxt [name]
1.287 + val _ = tracing "Running prolog program..."
1.288 + val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
1.289 + val _ = tracing "Restoring terms..."
1.290 + fun mk_set_comprehension t =
1.291 + let
1.292 + val frees = Term.add_frees t []
1.293 + val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt [t]) ("uu", fastype_of t)
1.294 + in HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
1.295 + frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"}))) end
1.296 + val set_comprs = map (fn ts =>
1.297 + mk_set_comprehension (HOLogic.mk_tuple (map (restore_term ctxt constant_table) (ts ~~ Ts)))) tss
1.298 in
1.299 - HOLogic.mk_tuple (map mk_term ts)
1.300 + foldl1 (HOLogic.mk_binop @{const_name sup}) (set_comprs @ [Free ("...", fastype_of t_compr)])
1.301 end
1.302
1.303 fun values_cmd print_modes soln raw_t state =