--- a/src/HOL/IsaMakefile Sat Jul 31 23:58:05 2010 +0200
+++ b/src/HOL/IsaMakefile Sun Aug 01 10:26:55 2010 +0200
@@ -401,7 +401,8 @@
Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \
Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \
Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
- Library/Code_Integer.thy Library/Code_Natural.thy \
+ Library/Code_Integer.thy Library/Code_Natural.thy \
+ Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML \
Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy \
Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \
Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Prolog.thy Sun Aug 01 10:26:55 2010 +0200
@@ -0,0 +1,13 @@
+(* Title: HOL/Library/Code_Prolog.thy
+ Author: Lukas Bulwahn, TUM 2010
+*)
+
+header {* Code generation of prolog programs *}
+
+theory Code_Prolog
+imports Main
+uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
+begin
+
+end
+
--- a/src/HOL/Library/HOL_Library_ROOT.ML Sat Jul 31 23:58:05 2010 +0200
+++ b/src/HOL/Library/HOL_Library_ROOT.ML Sun Aug 01 10:26:55 2010 +0200
@@ -2,4 +2,4 @@
(* Classical Higher-order Logic -- batteries included *)
use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
- "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set"];
+ "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"];
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Sat Jul 31 23:58:05 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Sun Aug 01 10:26:55 2010 +0200
@@ -1,6 +1,5 @@
theory Code_Prolog_Examples
-imports Predicate_Compile_Alternative_Defs
-uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
+imports Code_Prolog
begin
section {* Example append *}
@@ -12,6 +11,166 @@
code_pred append .
-values 3 "{((x::'b list), y, z). append x y z}"
+values 3 "{(x, y, z). append x y z}"
+
+
+section {* Example queens *}
+
+inductive nodiag :: "int => int => int list => bool"
+where
+ "nodiag B D []"
+| "D \<noteq> N - B ==> D \<noteq> B - N ==> Da = D + 1 ==> nodiag B Da L ==> nodiag B D (N # L)"
+
+text {*
+qdelete(A, [A|L], L).
+qdelete(X, [A|Z], [A|R]) :-
+ qdelete(X, Z, R).
+*}
+
+inductive qdelete :: "int => int list => int list => bool"
+where
+ "qdelete A (A # L) L"
+| "qdelete X Z R ==> qdelete X (A # Z) (A # R)"
+
+text {*
+qperm([], []).
+qperm([X|Y], K) :-
+ qdelete(U, [X|Y], Z),
+ K = [U|V],
+ qperm(Z, V).
+*}
+
+inductive qperm :: "int list => int list => bool"
+where
+ "qperm [] []"
+| "qdelete U (X # Y) Z ==> qperm Z V ==> qperm (X # Y) (U # V)"
+
+text {*
+safe([]).
+safe([N|L]) :-
+ nodiag(N, 1, L),
+ safe(L).
+*}
+
+inductive safe :: "int list => bool"
+where
+ "safe []"
+| "nodiag N 1 L ==> safe L ==> safe (N # L)"
+
+text {*
+queen(Data, Out) :-
+ qperm(Data, Out),
+ safe(Out)
+*}
+
+inductive queen :: "int list => int list => bool"
+where
+ "qperm Data Out ==> safe Out ==> queen Data Out"
+
+inductive queen_9
+where
+ "queen [1,2,3,4,5,6,7,8,9] ys ==> queen_9 ys"
+
+code_pred queen_9 .
+
+values 150 "{ys. queen_9 ys}"
+
+
+section {* Example symbolic derivation *}
+
+hide_const Plus Pow
+
+datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
+ | Minus expr expr | Uminus expr | Pow expr int | Exp expr
+
+text {*
+
+d(U + V, X, DU + DV) :-
+ cut,
+ d(U, X, DU),
+ d(V, X, DV).
+d(U - V, X, DU - DV) :-
+ cut,
+ d(U, X, DU),
+ d(V, X, DV).
+d(U * V, X, DU * V + U * DV) :-
+ cut,
+ d(U, X, DU),
+ d(V, X, DV).
+d(U / V, X, (DU * V - U * DV) / ^(V, 2)) :-
+ cut,
+ d(U, X, DU),
+ d(V, X, DV).
+d(^(U, N), X, DU * num(N) * ^(U, N1)) :-
+ cut,
+ N1 is N - 1,
+ d(U, X, DU).
+d(-U, X, -DU) :-
+ cut,
+ d(U, X, DU).
+d(exp(U), X, exp(U) * DU) :-
+ cut,
+ d(U, X, DU).
+d(log(U), X, DU / U) :-
+ cut,
+ d(U, X, DU).
+d(x, X, num(1)) :-
+ cut.
+d(num(_), _, num(0)).
+
+*}
+
+inductive d :: "expr => expr => expr => bool"
+where
+ "d U X DU ==> d V X DV ==> d (Plus U V) X (Plus DU DV)"
+| "d U X DU ==> d V X DV ==> d (Minus U V) X (Minus DU DV)"
+| "d U X DU ==> d V X DV ==> d (Mult U V) X (Plus (Mult DU V) (Mult U DV))"
+| "d U X DU ==> d V X DV ==> d (Div U V) X (Div (Minus (Mult DU V) (Mult U DV)) (Pow V 2))"
+| "d U X DU ==> N1 = N - 1 ==> d (Pow U N) X (Mult DU (Mult (Num N) (Pow U N1)))"
+| "d U X DU ==> d (Uminus U) X (Uminus DU)"
+| "d U X DU ==> d (Exp U) X (Mult (Exp U) DU)"
+| "d U X DU ==> d (Log U) X (Div DU U)"
+| "d x X (Num 1)"
+| "d (Num n) X (Num 0)"
+
+text {*
+ops8(E) :-
+ d((x + num(1)) * ((^(x, 2) + num(2)) * (^(x, 3) + num(3))), x, E).
+
+divide10(E) :-
+ d(((((((((x / x) / x) / x) / x) / x) / x) / x) / x) / x, x, E).
+
+log10(E) :-
+ d(log(log(log(log(log(log(log(log(log(log(x)))))))))), x, E).
+
+times10(E) :-
+ d(((((((((x * x) * x) * x) * x) * x) * x) * x) * x) * x, x, E)
+*}
+
+inductive ops8 :: "expr => bool"
+where
+ "d (Mult (Plus x (Num 1)) (Mult (Plus (Pow x 2) (Num 2)) (Plus (Pow x 3) (Num 3)))) x e ==> ops8 e"
+
+inductive divide10
+where
+ "d (Div (Div (Div (Div (Div (Div (Div (Div (Div x x) x) x) x) x) x) x) x) x) x e ==> divide10 e"
+
+inductive log10
+where
+ "d (Log (Log (Log (Log (Log (Log (Log (Log (Log (Log x)))))))))) x e ==> log10 e"
+
+inductive times10
+where
+ "d (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult x x) x) x) x) x) x) x) x) x) x e ==> times10 e"
+
+code_pred ops8 .
+code_pred divide10 .
+code_pred log10 .
+code_pred times10 .
+
+values "{e. ops8 e}"
+values "{e. divide10 e}"
+values "{e. log10 e}"
+values "{e. times10 e}"
end
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Sat Jul 31 23:58:05 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Sun Aug 01 10:26:55 2010 +0200
@@ -1,1 +1,2 @@
use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
+use_thys ["Code_Prolog_Examples"];
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Jul 31 23:58:05 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sun Aug 01 10:26:55 2010 +0200
@@ -6,9 +6,14 @@
signature CODE_PROLOG =
sig
- datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list;
- datatype prem = Conj of prem list | NotRel of string * prol_term list
- | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term;
+ datatype arith_op = Plus | Minus
+ datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
+ | Number of int | ArithOp of arith_op * prol_term list;
+ datatype prem = Conj of prem list
+ | Rel of string * prol_term list | NotRel of string * prol_term list
+ | Eq of prol_term * prol_term | NotEq of prol_term * prol_term
+ | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term;
+
type clause = ((string * prol_term list) * prem);
type logic_program = clause list;
type constant_table = (string * string) list
@@ -35,15 +40,29 @@
(* internal program representation *)
-datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list;
+datatype arith_op = Plus | Minus
+
+datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
+ | Number of int | ArithOp of arith_op * prol_term list;
+
+fun is_Var (Var _) = true
+ | is_Var _ = false
+
+fun is_arith_term (Var _) = true
+ | is_arith_term (Number _) = true
+ | is_arith_term (ArithOp (_, operands)) = forall is_arith_term operands
+ | is_arith_term _ = false
fun string_of_prol_term (Var s) = "Var " ^ s
| string_of_prol_term (Cons s) = "Cons " ^ s
| string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")"
+ | string_of_prol_term (Number n) = "Number " ^ string_of_int n
-datatype prem = Conj of prem list | NotRel of string * prol_term list
- | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term;
-
+datatype prem = Conj of prem list
+ | Rel of string * prol_term list | NotRel of string * prol_term list
+ | Eq of prol_term * prol_term | NotEq of prol_term * prol_term
+ | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term;
+
fun dest_Rel (Rel (c, ts)) = (c, ts)
type clause = ((string * prol_term list) * prem);
@@ -80,33 +99,66 @@
(** translation of terms, literals, premises, and clauses **)
+fun translate_arith_const @{const_name "Groups.plus_class.plus"} = SOME Plus
+ | translate_arith_const @{const_name "Groups.minus_class.minus"} = SOME Minus
+ | translate_arith_const _ = NONE
+
fun translate_term ctxt constant_table t =
- case strip_comb t of
- (Free (v, T), []) => Var v
- | (Const (c, _), []) => Cons (translate_const constant_table c)
- | (Const (c, _), args) =>
- AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args)
- | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t)
+ case try HOLogic.dest_number t of
+ SOME (@{typ "int"}, n) => Number n
+ | NONE =>
+ (case strip_comb t of
+ (Free (v, T), []) => Var v
+ | (Const (c, _), []) => Cons (translate_const constant_table c)
+ | (Const (c, _), args) =>
+ (case translate_arith_const c of
+ SOME aop => ArithOp (aop, map (translate_term ctxt constant_table) args)
+ | NONE =>
+ AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args))
+ | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t))
fun translate_literal ctxt constant_table t =
case strip_comb t of
(Const (@{const_name "op ="}, _), [l, r]) =>
- Eq (pairself (translate_term ctxt constant_table) (l, r))
+ let
+ val l' = translate_term ctxt constant_table l
+ val r' = translate_term ctxt constant_table r
+ in
+ (if is_Var l' andalso is_arith_term r' then ArithEq else Eq) (l', r')
+ end
| (Const (c, _), args) =>
Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args)
| _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t)
fun NegRel_of (Rel lit) = NotRel lit
| NegRel_of (Eq eq) = NotEq eq
-
+ | NegRel_of (ArithEq eq) = NotArithEq eq
+
fun translate_prem ctxt constant_table t =
case try HOLogic.dest_not t of
SOME t => NegRel_of (translate_literal ctxt constant_table t)
| NONE => translate_literal ctxt constant_table t
+
+fun imp_prems_conv cv ct =
+ case Thm.term_of ct of
+ Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
+ | _ => Conv.all_conv ct
+
+fun Trueprop_conv cv ct =
+ case Thm.term_of ct of
+ Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct
+ | _ => raise Fail "Trueprop_conv"
+
+fun preprocess_intro thy rule =
+ Conv.fconv_rule
+ (imp_prems_conv
+ (Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq}))))
+ (Thm.transfer thy rule)
+
fun translate_intros ctxt gr const constant_table =
let
- val intros = Graph.get_node gr const
+ val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const)
val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table
fun translate_intro intro =
@@ -158,9 +210,14 @@
(* code printer *)
+fun write_arith_op Plus = "+"
+ | write_arith_op Minus = "-"
+
fun write_term (Var v) = first_upper v
| write_term (Cons c) = c
- | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
+ | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
+ | write_term (ArithOp (oper, [a1, a2])) = write_term a1 ^ " " ^ write_arith_op oper ^ " " ^ write_term a2
+ | write_term (Number n) = string_of_int n
fun write_rel (pred, args) =
pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
@@ -170,6 +227,8 @@
| write_prem (NotRel p) = "not(" ^ write_rel p ^ ")"
| write_prem (Eq (l, r)) = write_term l ^ " = " ^ write_term r
| write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r
+ | write_prem (ArithEq (l, r)) = write_term l ^ " is " ^ write_term r
+ | write_prem (NotArithEq (l, r)) = write_term l ^ " =\\= " ^ write_term r
fun write_clause (head, prem) =
write_rel head ^ (if prem = Conj [] then "." else " :- " ^ write_prem prem ^ ".")
@@ -200,6 +259,8 @@
"main :- halt(1).\n"
(* parsing prolog solution *)
+val scan_number =
+ Scan.many1 Symbol.is_ascii_digit
val scan_atom =
Scan.many1 (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_quasi s)
@@ -221,10 +282,13 @@
val is_var_ident =
forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
+fun int_of_symbol_list xs = fold (fn x => fn s => s * 10 + (ord x - ord "0")) xs 0
+
fun scan_terms xs = (((scan_term --| $$ ",") ::: scan_terms)
|| (scan_term >> single)) xs
and scan_term xs =
- ((scan_var >> (Var o string_of))
+ ((scan_number >> (Number o int_of_symbol_list))
+ || (scan_var >> (Var o string_of))
|| ((scan_atom -- ($$ "(" |-- scan_terms --| $$ ")"))
>> (fn (f, ts) => AppF (string_of f, ts)))
|| (scan_atom >> (Cons o string_of))) xs
@@ -263,6 +327,8 @@
(* values command *)
fun restore_term ctxt constant_table (Var s, T) = Free (s, T)
+ | restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n
+ | restore_term ctxt constant_table (Number n, _) = raise (Fail "unexpected type for number")
| restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T)
| restore_term ctxt constant_table (AppF (f, args), T) =
let
@@ -299,16 +365,31 @@
val _ = tracing "Running prolog program..."
val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
val _ = tracing "Restoring terms..."
- fun mk_set_comprehension t =
- let
- val frees = Term.add_frees t []
- val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt [t]) ("uu", fastype_of t)
- in HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
- frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"}))) end
- val set_comprs = map (fn ts =>
- mk_set_comprehension (HOLogic.mk_tuple (map (restore_term ctxt constant_table) (ts ~~ Ts)))) tss
+ val empty = Const("Orderings.bot_class.bot", fastype_of t_compr)
+ fun mk_insert x S =
+ Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S
+ fun mk_set_compr in_insert [] xs =
+ rev ((Free ("...", fastype_of t_compr)) ::
+ (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))
+ | mk_set_compr in_insert (t :: ts) xs =
+ let
+ val frees = Term.add_frees t []
+ in
+ if null frees then
+ mk_set_compr (t :: in_insert) ts xs
+ else
+ let
+ val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt [t]) ("uu", fastype_of t)
+ val set_compr =
+ HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
+ frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"})))
+ in
+ set_compr :: (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs)
+ end
+ end
in
- foldl1 (HOLogic.mk_binop @{const_name sup}) (set_comprs @ [Free ("...", fastype_of t_compr)])
+ foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr []
+ (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt constant_table) (ts ~~ Ts))) tss) [])
end
fun values_cmd print_modes soln raw_t state =
@@ -318,6 +399,7 @@
val t' = values ctxt soln t
val ty' = Term.type_of t'
val ctxt' = Variable.auto_fixes t' ctxt
+ val _ = tracing "Printing terms..."
val p = Print_Mode.with_modes print_modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
--- a/src/HOL/Tools/inductive.ML Sat Jul 31 23:58:05 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Sun Aug 01 10:26:55 2010 +0200
@@ -548,15 +548,18 @@
fun mk_simp_eq ctxt prop =
let
- val (c, args) = strip_comb (HOLogic.dest_Trueprop prop)
val ctxt' = Variable.auto_fixes prop ctxt
- val cname = fst (dest_Const c)
+ val cname = fst (dest_Const (fst (strip_comb (HOLogic.dest_Trueprop prop))))
val info = the_inductive ctxt cname
val eq = nth (#eqs (snd info)) (find_index (fn c => c = cname) (#names (fst info)))
- val (_, args') = strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq))))
+ val lhs_eq = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq)))
+ val subst = Pattern.match (ProofContext.theory_of ctxt) (lhs_eq, HOLogic.dest_Trueprop prop)
+ (Vartab.empty, Vartab.empty)
val certify = cterm_of (ProofContext.theory_of ctxt)
- in
- cterm_instantiate (map (pairself certify) (args' ~~ args)) eq
+ val inst = map (fn v => (certify (Var v), certify (Envir.subst_term subst (Var v))))
+ (Term.add_vars lhs_eq [])
+ in
+ cterm_instantiate inst eq
|> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv
(Simplifier.full_rewrite (simpset_of ctxt))))
|> singleton (Variable.export ctxt' ctxt)