--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 31 23:46:49 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Sep 01 13:45:58 2010 +0200
@@ -447,7 +447,7 @@
\label{relevance-filter}
\begin{enum}
-\opdefault{relevance\_thresholds}{int\_pair}{45~95}
+\opdefault{relevance\_thresholds}{int\_pair}{45~85}
Specifies the thresholds above which facts are considered relevant by the
relevance filter. The first threshold is used for the first iteration of the
relevance filter and the second threshold is used for the last iteration (if it
--- a/doc-src/more_antiquote.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/doc-src/more_antiquote.ML Wed Sep 01 13:45:58 2010 +0200
@@ -124,12 +124,13 @@
in
val _ = Thy_Output.antiquotation "code_stmts"
- (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
- (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
+ (parse_const_terms -- Scan.repeat parse_names
+ -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
+ (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
let val thy = ProofContext.theory_of ctxt in
- Code_Target.code_of thy
- target NONE "Example" (mk_cs thy)
+ Code_Target.present_code thy (mk_cs thy)
(fn naming => maps (fn f => f thy naming) mk_stmtss)
+ target some_width "Example" []
|> typewriter
end);
--- a/etc/isar-keywords.el Tue Aug 31 23:46:49 2010 +0200
+++ b/etc/isar-keywords.el Wed Sep 01 13:45:58 2010 +0200
@@ -245,6 +245,7 @@
"thus"
"thy_deps"
"translations"
+ "try"
"txt"
"txt_raw"
"typ"
@@ -398,6 +399,7 @@
"thm"
"thm_deps"
"thy_deps"
+ "try"
"typ"
"unused_thms"
"value"
--- a/src/HOL/Auth/Event.thy Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Auth/Event.thy Wed Sep 01 13:45:58 2010 +0200
@@ -22,14 +22,6 @@
consts
bad :: "agent set" -- {* compromised agents *}
- knows :: "agent => event list => msg set"
-
-
-text{*The constant "spies" is retained for compatibility's sake*}
-
-abbreviation (input)
- spies :: "event list => msg set" where
- "spies == knows Spy"
text{*Spy has access to his own key for spoof messages, but Server is secure*}
specification (bad)
@@ -37,9 +29,10 @@
Server_not_bad [iff]: "Server \<notin> bad"
by (rule exI [of _ "{Spy}"], simp)
-primrec
+primrec knows :: "agent => event list => msg set"
+where
knows_Nil: "knows A [] = initState A"
- knows_Cons:
+| knows_Cons:
"knows A (ev # evs) =
(if A = Spy then
(case ev of
@@ -62,14 +55,20 @@
therefore the oops case must use Notes
*)
-consts
- (*Set of items that might be visible to somebody:
+text{*The constant "spies" is retained for compatibility's sake*}
+
+abbreviation (input)
+ spies :: "event list => msg set" where
+ "spies == knows Spy"
+
+
+(*Set of items that might be visible to somebody:
complement of the set of fresh items*)
- used :: "event list => msg set"
-primrec
+primrec used :: "event list => msg set"
+where
used_Nil: "used [] = (UN B. parts (initState B))"
- used_Cons: "used (ev # evs) =
+| used_Cons: "used (ev # evs) =
(case ev of
Says A B X => parts {X} \<union> used evs
| Gets A X => used evs
--- a/src/HOL/Auth/NS_Public_Bad.thy Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Wed Sep 01 13:45:58 2010 +0200
@@ -203,7 +203,7 @@
apply clarify
apply (frule_tac A' = A in
Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto)
-apply (rename_tac C B' evs3)
+apply (rename_tac evs3 B' C)
txt{*This is the attack!
@{subgoals[display,indent=0,margin=65]}
*}
--- a/src/HOL/HOL.thy Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/HOL.thy Wed Sep 01 13:45:58 2010 +0200
@@ -30,6 +30,7 @@
"~~/src/Tools/induct.ML"
("~~/src/Tools/induct_tacs.ML")
("Tools/recfun_codegen.ML")
+ "Tools/try.ML"
begin
setup {* Intuitionistic.method_setup @{binding iprover} *}
--- a/src/HOL/Imperative_HOL/Array.thy Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Wed Sep 01 13:45:58 2010 +0200
@@ -484,11 +484,11 @@
code_type array (Scala "!collection.mutable.ArraySeq[_]")
code_const Array (Scala "!error(\"bare Array\")")
-code_const Array.new' (Scala "('_: Unit)/ => / Heap.Array.alloc((_))((_))")
-code_const Array.make' (Scala "('_: Unit)/ =>/ Heap.Array.make((_))((_))")
-code_const Array.len' (Scala "('_: Unit)/ =>/ Heap.Array.len((_))")
-code_const Array.nth' (Scala "('_: Unit)/ =>/ Heap.Array.nth((_), (_))")
-code_const Array.upd' (Scala "('_: Unit)/ =>/ Heap.Array.upd((_), (_), (_))")
-code_const Array.freeze (Scala "('_: Unit)/ =>/ Heap.Array.freeze((_))")
+code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
+code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
+code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
+code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
+code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
+code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
end
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Sep 01 13:45:58 2010 +0200
@@ -477,9 +477,9 @@
subsubsection {* Scala *}
code_include Scala "Heap"
-{*import collection.mutable.ArraySeq
-
-def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
+{*object Heap {
+ def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
+}
class Ref[A](x: A) {
var value = x
@@ -495,21 +495,23 @@
}
object Array {
- def alloc[A](n: Natural.Nat)(x: A): ArraySeq[A] =
+ import collection.mutable.ArraySeq
+ def alloc[A](n: Natural)(x: A): ArraySeq[A] =
ArraySeq.fill(n.as_Int)(x)
- def make[A](n: Natural.Nat)(f: Natural.Nat => A): ArraySeq[A] =
- ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural.Nat(k)))
- def len[A](a: ArraySeq[A]): Natural.Nat =
- Natural.Nat(a.length)
- def nth[A](a: ArraySeq[A], n: Natural.Nat): A =
+ def make[A](n: Natural)(f: Natural => A): ArraySeq[A] =
+ ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k)))
+ def len[A](a: ArraySeq[A]): Natural =
+ Natural(a.length)
+ def nth[A](a: ArraySeq[A], n: Natural): A =
a(n.as_Int)
- def upd[A](a: ArraySeq[A], n: Natural.Nat, x: A): Unit =
+ def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit =
a.update(n.as_Int, x)
def freeze[A](a: ArraySeq[A]): List[A] =
a.toList
-}*}
+}
+*}
-code_reserved Scala bind Ref Array
+code_reserved Scala Heap Ref Array
code_type Heap (Scala "Unit/ =>/ _")
code_const bind (Scala "Heap.bind")
--- a/src/HOL/Imperative_HOL/Ref.thy Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Wed Sep 01 13:45:58 2010 +0200
@@ -306,10 +306,10 @@
text {* Scala *}
-code_type ref (Scala "!Heap.Ref[_]")
+code_type ref (Scala "!Ref[_]")
code_const Ref (Scala "!error(\"bare Ref\")")
-code_const ref' (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
-code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.Ref.lookup((_))")
-code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.Ref.update((_), (_))")
+code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
end
--- a/src/HOL/IsaMakefile Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Sep 01 13:45:58 2010 +0200
@@ -213,6 +213,7 @@
Tools/sat_funcs.ML \
Tools/sat_solver.ML \
Tools/split_rule.ML \
+ Tools/try.ML \
Tools/typedef.ML \
Transitive_Closure.thy \
Typedef.thy \
@@ -1322,7 +1323,8 @@
Predicate_Compile_Examples/Predicate_Compile_Examples.thy \
Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy \
Predicate_Compile_Examples/Code_Prolog_Examples.thy \
- Predicate_Compile_Examples/Hotel_Example.thy
+ Predicate_Compile_Examples/Hotel_Example.thy \
+ Predicate_Compile_Examples/Lambda_Example.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
--- a/src/HOL/Library/Code_Natural.thy Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy Wed Sep 01 13:45:58 2010 +0200
@@ -56,47 +56,45 @@
code_reserved Haskell Natural
code_include Scala "Natural"
-{*import scala.Math
-
-object Nat {
+{*object Natural {
- def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
- def apply(numeral: Int): Nat = Nat(BigInt(numeral))
- def apply(numeral: String): Nat = Nat(BigInt(numeral))
+ def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
+ def apply(numeral: Int): Natural = Natural(BigInt(numeral))
+ def apply(numeral: String): Natural = Natural(BigInt(numeral))
}
-class Nat private(private val value: BigInt) {
+class Natural private(private val value: BigInt) {
override def hashCode(): Int = this.value.hashCode()
override def equals(that: Any): Boolean = that match {
- case that: Nat => this equals that
+ case that: Natural => this equals that
case _ => false
}
override def toString(): String = this.value.toString
- def equals(that: Nat): Boolean = this.value == that.value
+ def equals(that: Natural): Boolean = this.value == that.value
def as_BigInt: BigInt = this.value
def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
this.value.intValue
else error("Int value out of range: " + this.value.toString)
- def +(that: Nat): Nat = new Nat(this.value + that.value)
- def -(that: Nat): Nat = Nat(this.value - that.value)
- def *(that: Nat): Nat = new Nat(this.value * that.value)
+ def +(that: Natural): Natural = new Natural(this.value + that.value)
+ def -(that: Natural): Natural = Natural(this.value - that.value)
+ def *(that: Natural): Natural = new Natural(this.value * that.value)
- def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
+ def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
else {
val (k, l) = this.value /% that.value
- (new Nat(k), new Nat(l))
+ (new Natural(k), new Natural(l))
}
- def <=(that: Nat): Boolean = this.value <= that.value
+ def <=(that: Natural): Boolean = this.value <= that.value
- def <(that: Nat): Boolean = this.value < that.value
+ def <(that: Natural): Boolean = this.value < that.value
}
*}
@@ -105,7 +103,7 @@
code_type code_numeral
(Haskell "Natural.Natural")
- (Scala "Natural.Nat")
+ (Scala "Natural")
setup {*
fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
--- a/src/HOL/Library/Efficient_Nat.thy Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Wed Sep 01 13:45:58 2010 +0200
@@ -281,9 +281,7 @@
code_reserved Haskell Nat
code_include Scala "Nat"
-{*import scala.Math
-
-object Nat {
+{*object Nat {
def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
def apply(numeral: Int): Nat = Nat(BigInt(numeral))
@@ -330,7 +328,7 @@
code_type nat
(Haskell "Nat.Nat")
- (Scala "Nat.Nat")
+ (Scala "Nat")
code_instance nat :: equal
(Haskell -)
@@ -397,7 +395,7 @@
code_const int and nat
(Haskell "toInteger" and "fromInteger")
- (Scala "!_.as'_BigInt" and "Nat.Nat")
+ (Scala "!_.as'_BigInt" and "Nat")
text {* Conversion from and to code numerals. *}
@@ -405,14 +403,14 @@
(SML "IntInf.toInt")
(OCaml "_")
(Haskell "!(fromInteger/ ./ toInteger)")
- (Scala "!Natural.Nat(_.as'_BigInt)")
+ (Scala "!Natural(_.as'_BigInt)")
(Eval "_")
code_const Code_Numeral.nat_of
(SML "IntInf.fromInt")
(OCaml "_")
(Haskell "!(fromInteger/ ./ toInteger)")
- (Scala "!Nat.Nat(_.as'_BigInt)")
+ (Scala "!Nat(_.as'_BigInt)")
(Eval "_")
text {* Using target language arithmetic operations whenever appropriate *}
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Wed Sep 01 13:45:58 2010 +0200
@@ -12,6 +12,7 @@
"Tools/mirabelle_quickcheck.ML"
"Tools/mirabelle_refute.ML"
"Tools/mirabelle_sledgehammer.ML"
+ "Tools/mirabelle_sledgehammer_filter.ML"
begin
text {*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Sep 01 13:45:58 2010 +0200
@@ -0,0 +1,169 @@
+(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
+ Author: Jasmin Blanchette, TU Munich
+*)
+
+structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION =
+struct
+
+val relevance_filter_args =
+ [("worse_irrel_freq", Sledgehammer_Fact_Filter.worse_irrel_freq),
+ ("higher_order_irrel_weight",
+ Sledgehammer_Fact_Filter.higher_order_irrel_weight),
+ ("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
+ ("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight),
+ ("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight),
+ ("intro_bonus", Sledgehammer_Fact_Filter.intro_bonus),
+ ("elim_bonus", Sledgehammer_Fact_Filter.elim_bonus),
+ ("simp_bonus", Sledgehammer_Fact_Filter.simp_bonus),
+ ("local_bonus", Sledgehammer_Fact_Filter.local_bonus),
+ ("chained_bonus", Sledgehammer_Fact_Filter.chained_bonus),
+ ("max_imperfect", Sledgehammer_Fact_Filter.max_imperfect),
+ ("max_imperfect_exp", Sledgehammer_Fact_Filter.max_imperfect_exp),
+ ("threshold_divisor", Sledgehammer_Fact_Filter.threshold_divisor),
+ ("ridiculous_threshold", Sledgehammer_Fact_Filter.ridiculous_threshold)]
+
+structure Prooftab =
+ Table(type key = int * int val ord = prod_ord int_ord int_ord);
+
+val proof_table = Unsynchronized.ref Prooftab.empty
+
+val num_successes = Unsynchronized.ref ([] : (int * int) list)
+val num_failures = Unsynchronized.ref ([] : (int * int) list)
+val num_found_proofs = Unsynchronized.ref ([] : (int * int) list)
+val num_lost_proofs = Unsynchronized.ref ([] : (int * int) list)
+val num_found_facts = Unsynchronized.ref ([] : (int * int) list)
+val num_lost_facts = Unsynchronized.ref ([] : (int * int) list)
+
+fun get id c = the_default 0 (AList.lookup (op =) (!c) id)
+fun add id c n =
+ c := (case AList.lookup (op =) (!c) id of
+ SOME m => AList.update (op =) (id, m + n) (!c)
+ | NONE => (id, n) :: !c)
+
+fun init proof_file _ thy =
+ let
+ fun do_line line =
+ case line |> space_explode ":" of
+ [line_num, col_num, proof] =>
+ SOME (pairself (the o Int.fromString) (line_num, col_num),
+ proof |> space_explode " " |> filter_out (curry (op =) ""))
+ | _ => NONE
+ val proofs = File.read (Path.explode proof_file)
+ val proof_tab =
+ proofs |> space_explode "\n"
+ |> map_filter do_line
+ |> AList.coalesce (op =)
+ |> Prooftab.make
+ in proof_table := proof_tab; thy end
+
+fun percentage a b = if b = 0 then "N/A" else string_of_int (a * 100 div b)
+fun percentage_alt a b = percentage a (a + b)
+
+fun done id ({log, ...} : Mirabelle.done_args) =
+ if get id num_successes + get id num_failures > 0 then
+ (log "";
+ log ("Number of overall successes: " ^
+ string_of_int (get id num_successes));
+ log ("Number of overall failures: " ^ string_of_int (get id num_failures));
+ log ("Overall success rate: " ^
+ percentage_alt (get id num_successes) (get id num_failures) ^ "%");
+ log ("Number of found proofs: " ^ string_of_int (get id num_found_proofs));
+ log ("Number of lost proofs: " ^ string_of_int (get id num_lost_proofs));
+ log ("Proof found rate: " ^
+ percentage_alt (get id num_found_proofs) (get id num_lost_proofs) ^
+ "%");
+ log ("Number of found facts: " ^ string_of_int (get id num_found_facts));
+ log ("Number of lost facts: " ^ string_of_int (get id num_lost_facts));
+ log ("Fact found rate: " ^
+ percentage_alt (get id num_found_facts) (get id num_lost_facts) ^
+ "%"))
+ else
+ ()
+
+val default_max_relevant = 300
+
+fun with_index (i, s) = s ^ "@" ^ string_of_int i
+
+fun action args id ({pre, pos, log, ...} : Mirabelle.run_args) =
+ case (Position.line_of pos, Position.column_of pos) of
+ (SOME line_num, SOME col_num) =>
+ (case Prooftab.lookup (!proof_table) (line_num, col_num) of
+ SOME proofs =>
+ let
+ val {context = ctxt, facts, goal} = Proof.goal pre
+ val thy = ProofContext.theory_of ctxt
+ val args =
+ args
+ |> filter (fn (key, value) =>
+ case AList.lookup (op =) relevance_filter_args key of
+ SOME rf => (rf := the (Real.fromString value); false)
+ | NONE => true)
+
+ val {relevance_thresholds, full_types, max_relevant, theory_relevant,
+ ...} = Sledgehammer_Isar.default_params thy args
+ val subgoal = 1
+ val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
+ val facts =
+ Sledgehammer_Fact_Filter.relevant_facts ctxt full_types
+ relevance_thresholds
+ (the_default default_max_relevant max_relevant)
+ (the_default false theory_relevant)
+ {add = [], del = [], only = false} facts hyp_ts concl_t
+ |> map (fst o fst)
+ val (found_facts, lost_facts) =
+ List.concat proofs |> sort_distinct string_ord
+ |> map (fn fact => (find_index (curry (op =) fact) facts, fact))
+ |> List.partition (curry (op <=) 0 o fst)
+ |>> sort (prod_ord int_ord string_ord) ||> map snd
+ val found_proofs = filter (forall (member (op =) facts)) proofs
+ val n = length found_proofs
+ val _ =
+ if n = 0 then
+ (add id num_failures 1; log "Failure")
+ else
+ (add id num_successes 1;
+ add id num_found_proofs n;
+ log ("Success (" ^ string_of_int n ^ " of " ^
+ string_of_int (length proofs) ^ " proofs)"))
+ val _ = add id num_lost_proofs (length proofs - n)
+ val _ = add id num_found_facts (length found_facts)
+ val _ = add id num_lost_facts (length lost_facts)
+ val _ =
+ if null found_facts then
+ ()
+ else
+ let
+ val found_weight =
+ Real.fromInt (fold (fn (n, _) =>
+ Integer.add (n * n)) found_facts 0)
+ / Real.fromInt (length found_facts)
+ |> Math.sqrt |> Real.ceil
+ in
+ log ("Found facts (among " ^ string_of_int (length facts) ^
+ ", weight " ^ string_of_int found_weight ^ "): " ^
+ commas (map with_index found_facts))
+ end
+ val _ = if null lost_facts then
+ ()
+ else
+ log ("Lost facts (among " ^ string_of_int (length facts) ^
+ "): " ^ commas lost_facts)
+ in () end
+ | NONE => log "No known proof")
+ | _ => ()
+
+val proof_fileK = "proof_file"
+
+fun invoke args =
+ let
+ val (pf_args, other_args) =
+ args |> List.partition (curry (op =) proof_fileK o fst)
+ val proof_file = case pf_args of
+ [] => error "No \"proof_file\" specified"
+ | (_, s) :: _ => s
+ in Mirabelle.register (init proof_file, action other_args, done) end
+
+end;
+
+(* Workaround to keep the "mirabelle.pl" script happy *)
+structure Mirabelle_Sledgehammer_filter = Mirabelle_Sledgehammer_Filter;
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Sep 01 13:45:58 2010 +0200
@@ -51,7 +51,11 @@
}
my $tools = "";
if ($#action_files >= 0) {
- $tools = "uses " . join(" ", @action_files);
+ # uniquify
+ my $s = join ("\n", @action_files);
+ my @action_files = split(/\n/, $s . "\n" . $s);
+ %action_files = sort(@action_files);
+ $tools = "uses " . join(" ", sort(keys(%action_files)));
}
open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
@@ -71,7 +75,7 @@
END
-foreach (split(/:/, $actions)) {
+foreach (reverse(split(/:/, $actions))) {
if (m/([^[]*)(?:\[(.*)\])?/) {
my ($name, $settings_str) = ($1, $2 || "");
$name =~ s/^([a-z])/\U$1/;
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Wed Sep 01 13:45:58 2010 +0200
@@ -10,17 +10,35 @@
"append [] ys ys"
| "append xs ys zs ==> append (x # xs) ys (x # zs)"
-ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = false,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
values "{(x, y, z). append x y z}"
values 3 "{(x, y, z). append x y z}"
-ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.YAP} *}
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = false,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.YAP}) *}
values "{(x, y, z). append x y z}"
-ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = false,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
section {* Example queens *}
@@ -183,7 +201,13 @@
where
"y \<noteq> B \<Longrightarrow> notB y"
-ML {* Code_Prolog.options := {ensure_groundness = true, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
values 2 "{y. notB y}"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Wed Sep 01 13:45:58 2010 +0200
@@ -0,0 +1,169 @@
+theory Context_Free_Grammar_Example
+imports Code_Prolog
+begin
+
+declare mem_def[code_pred_inline]
+
+
+subsection {* Alternative rules for length *}
+
+definition size_list :: "'a list => nat"
+where "size_list = size"
+
+lemma size_list_simps:
+ "size_list [] = 0"
+ "size_list (x # xs) = Suc (size_list xs)"
+by (auto simp add: size_list_def)
+
+declare size_list_simps[code_pred_def]
+declare size_list_def[symmetric, code_pred_inline]
+
+
+setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+
+datatype alphabet = a | b
+
+inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
+ "[] \<in> S\<^isub>1"
+| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
+| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
+| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
+| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
+| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
+
+lemma
+ "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
+quickcheck[generator = prolog, iterations=1, expect = counterexample]
+oops
+
+definition "filter_a = filter (\<lambda>x. x = a)"
+
+lemma [code_pred_def]: "filter_a [] = []"
+unfolding filter_a_def by simp
+
+lemma [code_pred_def]: "filter_a (x#xs) = (if x = a then x # filter_a xs else filter_a xs)"
+unfolding filter_a_def by simp
+
+declare filter_a_def[symmetric, code_pred_inline]
+
+definition "filter_b = filter (\<lambda>x. x = b)"
+
+lemma [code_pred_def]: "filter_b [] = []"
+unfolding filter_b_def by simp
+
+lemma [code_pred_def]: "filter_b (x#xs) = (if x = b then x # filter_b xs else filter_b xs)"
+unfolding filter_b_def by simp
+
+declare filter_b_def[symmetric, code_pred_inline]
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [(["s1", "a1", "b1"], 2)],
+ replacing = [(("s1", "limited_s1"), "quickcheck")],
+ manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+
+theorem S\<^isub>1_sound:
+"w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator = prolog, iterations=1, expect = counterexample]
+oops
+
+
+inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
+ "[] \<in> S\<^isub>2"
+| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
+| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
+| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
+| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
+| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
+
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [(["s2", "a2", "b2"], 3)],
+ replacing = [(("s2", "limited_s2"), "quickcheck")],
+ manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+
+theorem S\<^isub>2_sound:
+"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator=prolog, iterations=1, expect = counterexample]
+oops
+
+inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
+ "[] \<in> S\<^isub>3"
+| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
+| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
+| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
+| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
+| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
+
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [(["s3", "a3", "b3"], 6)],
+ replacing = [(("s3", "limited_s3"), "quickcheck")],
+ manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+lemma S\<^isub>3_sound:
+"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator=prolog, iterations=1, size=1, expect = no_counterexample]
+oops
+
+
+(*
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+
+theorem S\<^isub>3_complete:
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
+quickcheck[generator = prolog, size=1, iterations=1]
+oops
+*)
+
+inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
+ "[] \<in> S\<^isub>4"
+| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
+| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
+| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
+| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
+| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
+| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
+
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [(["s4", "a4", "b4"], 6)],
+ replacing = [(("s4", "limited_s4"), "quickcheck")],
+ manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+
+theorem S\<^isub>4_sound:
+"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator = prolog, size=1, iterations=1, expect = no_counterexample]
+oops
+
+(*
+theorem S\<^isub>4_complete:
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
+oops
+*)
+
+hide_const a b
+
+
+end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Wed Sep 01 13:45:58 2010 +0200
@@ -84,18 +84,46 @@
lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
-ML {* Code_Prolog.options := {ensure_groundness = true} *}
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
values 40 "{s. hotel s}"
setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
-ML {* set Code_Prolog.trace *}
lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
quickcheck[generator = code, iterations = 100000, report]
-quickcheck[generator = prolog, iterations = 1]
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
oops
+definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
+[code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
+
+
+definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
+where
+ "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
+ s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
+ no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [],
+ limited_predicates = [(["hotel"], 5)],
+ replacing = [(("hotel", "limited_hotel"), "quickcheck")],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Wed Sep 01 13:45:58 2010 +0200
@@ -0,0 +1,126 @@
+theory Lambda_Example
+imports Code_Prolog
+begin
+
+subsection {* Lambda *}
+
+datatype type =
+ Atom nat
+ | Fun type type (infixr "\<Rightarrow>" 200)
+
+datatype dB =
+ Var nat
+ | App dB dB (infixl "\<degree>" 200)
+ | Abs type dB
+
+primrec
+ nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
+where
+ "[]\<langle>i\<rangle> = None"
+| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
+
+inductive nth_el1 :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ "nth_el1 (x # xs) 0 x"
+| "nth_el1 xs i y \<Longrightarrow> nth_el1 (x # xs) (Suc i) y"
+
+inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
+ where
+ Var [intro!]: "nth_el1 env x T \<Longrightarrow> env \<turnstile> Var x : T"
+ | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
+ | App [intro!]: "env \<turnstile> s : U \<Rightarrow> T \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
+
+primrec
+ lift :: "[dB, nat] => dB"
+where
+ "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
+ | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
+ | "lift (Abs T s) k = Abs T (lift s (k + 1))"
+
+primrec pred :: "nat => nat"
+where
+ "pred (Suc i) = i"
+
+primrec
+ subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300)
+where
+ subst_Var: "(Var i)[s/k] =
+ (if k < i then Var (pred i) else if i = k then s else Var i)"
+ | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
+ | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"
+
+inductive beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+ where
+ beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
+ | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
+ | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
+ | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
+
+subsection {* Inductive definitions for ordering on naturals *}
+
+inductive less_nat
+where
+ "less_nat 0 (Suc y)"
+| "less_nat x y ==> less_nat (Suc x) (Suc y)"
+
+lemma less_nat[code_pred_inline]:
+ "x < y = less_nat x y"
+apply (rule iffI)
+apply (induct x arbitrary: y)
+apply (case_tac y) apply (auto intro: less_nat.intros)
+apply (case_tac y)
+apply (auto intro: less_nat.intros)
+apply (induct rule: less_nat.induct)
+apply auto
+done
+
+lemma [code_pred_inline]: "(x::nat) + 1 = Suc x"
+by simp
+
+section {* Manual setup to find counterexample *}
+
+setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+
+setup {* Code_Prolog.map_code_options (K
+ { ensure_groundness = true,
+ limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
+ limited_predicates = [(["typing"], 2), (["nthel1"], 2)],
+ replacing = [(("typing", "limited_typing"), "quickcheck"),
+ (("nthel1", "limited_nthel1"), "lim_typing")],
+ manual_reorder = [],
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+lemma
+ "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
+text {* Verifying that the found counterexample really is one by means of a proof *}
+
+lemma
+assumes
+ "t' = Var 0"
+ "U = Atom 0"
+ "\<Gamma> = [Atom 1]"
+ "t = App (Abs (Atom 0) (Var 1)) (Var 0)"
+shows
+ "\<Gamma> \<turnstile> t : U"
+ "t \<rightarrow>\<^sub>\<beta> t'"
+ "\<not> \<Gamma> \<turnstile> t' : U"
+proof -
+ from assms show "\<Gamma> \<turnstile> t : U"
+ by (auto intro!: typing.intros nth_el1.intros)
+next
+ from assms have "t \<rightarrow>\<^sub>\<beta> (Var 1)[Var 0/0]"
+ by (auto simp only: intro: beta.intros)
+ moreover
+ from assms have "(Var 1)[Var 0/0] = t'" by simp
+ ultimately show "t \<rightarrow>\<^sub>\<beta> t'" by simp
+next
+ from assms show "\<not> \<Gamma> \<turnstile> t' : U"
+ by (auto elim: typing.cases nth_el1.cases)
+qed
+
+
+end
+
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Wed Sep 01 13:45:58 2010 +0200
@@ -1,2 +1,2 @@
use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
-if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example"];
+if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example", "Lambda_Example"];
--- a/src/HOL/Tools/Function/function_core.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Wed Sep 01 13:45:58 2010 +0200
@@ -860,9 +860,9 @@
rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
THEN (simp_default_tac (simpset_of ctxt) 1)
- THEN (etac not_acc_down 1)
- THEN ((etac R_cases)
- THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
+ THEN TRY ((etac not_acc_down 1)
+ THEN ((etac R_cases)
+ THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1))
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
in
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Sep 01 13:45:58 2010 +0200
@@ -8,8 +8,14 @@
sig
datatype prolog_system = SWI_PROLOG | YAP
type code_options =
- {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
- val options : code_options ref
+ {ensure_groundness : bool,
+ limited_types : (typ * int) list,
+ limited_predicates : (string list * int) list,
+ replacing : ((string * string) * string) list,
+ manual_reorder : ((string * int) * int list) list,
+ prolog_system : prolog_system}
+ val code_options_of : theory -> code_options
+ val map_code_options : (code_options -> code_options) -> theory -> theory
datatype arith_op = Plus | Minus
datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
@@ -31,6 +37,8 @@
val quickcheck : Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
val trace : bool Unsynchronized.ref
+
+ val replace : ((string * string) * string) -> logic_program -> logic_program
end;
structure Code_Prolog : CODE_PROLOG =
@@ -47,10 +55,38 @@
datatype prolog_system = SWI_PROLOG | YAP
type code_options =
- {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
+ {ensure_groundness : bool,
+ limited_types : (typ * int) list,
+ limited_predicates : (string list * int) list,
+ replacing : ((string * string) * string) list,
+ manual_reorder : ((string * int) * int list) list,
+ prolog_system : prolog_system}
-val options = Unsynchronized.ref {ensure_groundness = false, limited_types = [],
- prolog_system = SWI_PROLOG};
+structure Options = Theory_Data
+(
+ type T = code_options
+ val empty = {ensure_groundness = false,
+ limited_types = [], limited_predicates = [], replacing = [], manual_reorder = [],
+ prolog_system = SWI_PROLOG}
+ val extend = I;
+ fun merge
+ ({ensure_groundness = ensure_groundness1, limited_types = limited_types1,
+ limited_predicates = limited_predicates1, replacing = replacing1,
+ manual_reorder = manual_reorder1, prolog_system = prolog_system1},
+ {ensure_groundness = ensure_groundness2, limited_types = limited_types2,
+ limited_predicates = limited_predicates2, replacing = replacing2,
+ manual_reorder = manual_reorder2, prolog_system = prolog_system2}) =
+ {ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
+ limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2),
+ limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2),
+ manual_reorder = AList.merge (op =) (K true) (manual_reorder1, manual_reorder2),
+ replacing = Library.merge (op =) (replacing1, replacing2),
+ prolog_system = prolog_system1};
+);
+
+val code_options_of = Options.get
+
+val map_code_options = Options.map
(* general string functions *)
@@ -124,16 +160,32 @@
(* translation from introduction rules to internal representation *)
+fun mk_conform f empty avoid name =
+ let
+ fun dest_Char (Symbol.Char c) = c
+ val name' = space_implode "" (map (dest_Char o Symbol.decode)
+ (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
+ (Symbol.explode name)))
+ val name'' = f (if name' = "" then empty else name')
+ in (if member (op =) avoid name'' then Name.variant avoid name'' else name'') end
+
(** constant table **)
type constant_table = (string * string) list
(* assuming no clashing *)
-fun mk_constant_table consts =
- AList.make (first_lower o Long_Name.base_name) consts
-
fun declare_consts consts constant_table =
- fold (fn c => AList.update (op =) (c, first_lower (Long_Name.base_name c))) consts constant_table
+ let
+ fun update' c table =
+ if AList.defined (op =) table c then table else
+ let
+ val c' = mk_conform first_lower "pred" (map snd table) (Long_Name.base_name c)
+ in
+ AList.update (op =) (c, c') table
+ end
+ in
+ fold update' consts constant_table
+ end
fun translate_const constant_table c =
case AList.lookup (op =) constant_table c of
@@ -234,7 +286,8 @@
val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems)
val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
in clause end
- in (map translate_intro intros', constant_table') end
+ val res = (map translate_intro intros', constant_table')
+ in res end
fun depending_preds_of (key, intros) =
fold Term.add_const_names (map Thm.prop_of intros) []
@@ -263,7 +316,7 @@
val gr = Predicate_Compile_Core.intros_graph_of ctxt
val gr' = add_edges depending_preds_of const gr
val scc = strong_conn_of gr' [const]
- val constant_table = mk_constant_table (flat scc)
+ val constant_table = declare_consts (flat scc) []
in
apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
end
@@ -347,28 +400,88 @@
((flat grs) @ p', constant_table')
end
+(* make depth-limited version of predicate *)
+
+fun mk_lim_rel_name rel_name = "lim_" ^ rel_name
+
+fun mk_depth_limited rel_names ((rel_name, ts), prem) =
+ let
+ fun has_positive_recursive_prems (Conj prems) = exists has_positive_recursive_prems prems
+ | has_positive_recursive_prems (Rel (rel, ts)) = member (op =) rel_names rel
+ | has_positive_recursive_prems _ = false
+ fun mk_lim_prem (Conj prems) = Conj (map mk_lim_prem prems)
+ | mk_lim_prem (p as Rel (rel, ts)) =
+ if member (op =) rel_names rel then Rel (mk_lim_rel_name rel, Var "Lim" :: ts) else p
+ | mk_lim_prem p = p
+ in
+ if has_positive_recursive_prems prem then
+ ((mk_lim_rel_name rel_name, (AppF ("suc", [Var "Lim"])) :: ts), mk_lim_prem prem)
+ else
+ ((mk_lim_rel_name rel_name, (Var "Lim") :: ts), prem)
+ end
+
+fun add_limited_predicates limited_predicates =
+ let
+ fun add (rel_names, limit) (p, constant_table) =
+ let
+ val clauses = filter (fn ((rel, _), _) => member (op =) rel_names rel) p
+ val clauses' = map (mk_depth_limited rel_names) clauses
+ fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero")
+ fun mk_entry_clause rel_name =
+ let
+ val nargs = length (snd (fst
+ (the (find_first (fn ((rel, _), _) => rel = rel_name) clauses))))
+ val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs)
+ in
+ (("limited_" ^ rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars))
+ end
+ in (p @ (map mk_entry_clause rel_names) @ clauses', constant_table) end
+ in
+ fold add limited_predicates
+ end
+
+
+(* replace predicates in clauses *)
+
+(* replace (A, B, C) p = replace A by B in clauses of C *)
+fun replace ((from, to), location) p =
+ let
+ fun replace_prem (Conj prems) = Conj (map replace_prem prems)
+ | replace_prem (r as Rel (rel, ts)) =
+ if rel = from then Rel (to, ts) else r
+ | replace_prem r = r
+ in
+ map (fn ((rel, args), prem) => ((rel, args), (if rel = location then replace_prem else I) prem)) p
+ end
+
+(* reorder manually : reorder premises of ith clause of predicate p by a permutation perm *)
+
+fun reorder_manually reorder p =
+ let
+ fun reorder' (clause as ((rel, args), prem)) seen =
+ let
+ val seen' = AList.map_default (op =) (rel, 0) (fn x => x + 1) seen
+ val i = the (AList.lookup (op =) seen' rel)
+ val perm = AList.lookup (op =) reorder (rel, i)
+ val prem' = (case perm of
+ SOME p => (case prem of Conj prems => Conj (map (nth prems) p) | _ => prem)
+ | NONE => prem)
+ in (((rel, args), prem'), seen') end
+ in
+ fst (fold_map reorder' p [])
+ end
(* rename variables to prolog-friendly names *)
fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v))
fun rename_vars_prem renaming = map_term_prem (rename_vars_term renaming)
-fun dest_Char (Symbol.Char c) = c
-
fun is_prolog_conform v =
forall (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) (Symbol.explode v)
-
-fun mk_conform avoid v =
- let
- val v' = space_implode "" (map (dest_Char o Symbol.decode)
- (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
- (Symbol.explode v)))
- val v' = if v' = "" then "var" else v'
- in Name.variant avoid (first_upper v') end
fun mk_renaming v renaming =
- (v, mk_conform (map snd renaming) v) :: renaming
+ (v, mk_conform first_upper "Var" (map snd renaming) v) :: renaming
fun rename_vars_clause ((rel, args), prem) =
let
@@ -377,7 +490,7 @@
in ((rel, map (rename_vars_term renaming) args), rename_vars_prem renaming prem) end
val rename_vars_program = map rename_vars_clause
-
+
(* code printer *)
fun write_arith_op Plus = "+"
@@ -460,7 +573,7 @@
let
val cmd =
case system of SWI_PROLOG => "/usr/local/bin/swipl -f " | YAP => "/usr/local/bin/yap -L "
- in bash_output (cmd ^ file_name) end
+ in fst (bash_output (cmd ^ file_name)) end
(* parsing prolog solution *)
@@ -508,24 +621,23 @@
(l :: r :: []) => parse_term (unprefix " " r)
| _ => raise Fail "unexpected equation in prolog output"
fun parse_solution s = map dest_eq (space_explode ";" s)
+ val sols = case space_explode "\n" sol of [] => [] | s => fst (split_last s)
in
- map parse_solution (fst (split_last (space_explode "\n" sol)))
+ map parse_solution sols
end
(* calling external interpreter and getting results *)
fun run system p query_rel vnames nsols =
let
- val cmd = Path.named_root
val p' = rename_vars_program p
val _ = tracing "Renaming variable names..."
val renaming = fold mk_renaming vnames []
val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
val prog = prelude system ^ query system nsols query_rel vnames' ^ write_program p'
val _ = tracing ("Generated prolog program:\n" ^ prog)
- val prolog_file = File.tmp_path (Path.basic "prolog_file")
- val _ = File.write prolog_file prog
- val (solution, _) = invoke system (File.shell_path prolog_file)
+ val solution = Cache_IO.with_tmp_file "prolog_file" (fn prolog_file =>
+ (File.write prolog_file prog; invoke system (Path.implode prolog_file)))
val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
val tss = parse_solutions solution
in
@@ -577,7 +689,7 @@
fun values ctxt soln t_compr =
let
- val options = !options
+ val options = code_options_of (ProofContext.theory_of ctxt)
val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
| _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
val (body, Ts, fp) = HOLogic.strip_psplits split;
@@ -605,6 +717,9 @@
|> (if #ensure_groundness options then
add_ground_predicates ctxt' (#limited_types options)
else I)
+ |> add_limited_predicates (#limited_predicates options)
+ |> apfst (fold replace (#replacing options))
+ |> apfst (reorder_manually (#manual_reorder options))
val _ = tracing "Running prolog program..."
val tss = run (#prolog_system options)
p (translate_const constant_table name) (map first_upper vnames) soln
@@ -675,6 +790,7 @@
fun quickcheck ctxt report t size =
let
+ val options = code_options_of (ProofContext.theory_of ctxt)
val thy = Theory.copy (ProofContext.theory_of ctxt)
val (vs, t') = strip_abs t
val vs' = Variable.variant_frees ctxt [] vs
@@ -696,12 +812,18 @@
val ctxt' = ProofContext.init_global thy3
val _ = tracing "Generating prolog program..."
val (p, constant_table) = generate true ctxt' full_constname
- |> add_ground_predicates ctxt' (#limited_types (!options))
+ |> add_ground_predicates ctxt' (#limited_types options)
+ |> add_limited_predicates (#limited_predicates options)
+ |> apfst (fold replace (#replacing options))
+ |> apfst (reorder_manually (#manual_reorder options))
val _ = tracing "Running prolog program..."
- val [ts] = run (#prolog_system (!options))
+ val tss = run (#prolog_system options)
p (translate_const constant_table full_constname) (map fst vs') (SOME 1)
val _ = tracing "Restoring terms..."
- val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
+ val res =
+ case tss of
+ [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
+ | _ => NONE
val empty_report = ([], false)
in
(res, empty_report)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 01 13:45:58 2010 +0200
@@ -63,6 +63,19 @@
val add_random_dseq_equations : options -> string list -> theory -> theory
val add_new_random_dseq_equations : options -> string list -> theory -> theory
val mk_tracing : string -> term -> term
+ val prepare_intrs : options -> compilation -> theory -> string list -> thm list ->
+ ((string * typ) list * string list * string list * (string * mode list) list *
+ (string * (Term.term list * Predicate_Compile_Aux.indprem list) list) list)
+ type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool}
+ datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
+ | Mode_Pair of mode_derivation * mode_derivation | Term of mode
+ type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list
+ type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
+
+ val infer_modes :
+ mode_analysis_options -> options -> compilation -> (string * typ) list -> (string * mode list) list ->
+ string list -> (string * (Term.term list * Predicate_Compile_Aux.indprem list) list) list ->
+ theory -> ((moded_clause list pred_mode_table * string list) * theory)
end;
structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Sep 01 13:45:58 2010 +0200
@@ -351,13 +351,17 @@
|> map (fn (resargs, (names', prems')) =>
let
val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))
- in (prem'::prems', names') end)
+ in (prems' @ [prem'], names') end)
end
val intro_ts' = folds_map rewrite prems frees
|> maps (fn (prems', frees') =>
rewrite concl frees'
- |> map (fn (concl'::conclprems, _) =>
- Logic.list_implies ((flat prems') @ conclprems, concl')))
+ |> map (fn (conclprems, _) =>
+ let
+ val (conclprems', concl') = split_last conclprems
+ in
+ Logic.list_implies ((flat prems') @ conclprems', concl')
+ end))
(*val _ = tracing ("Rewritten intro to " ^
commas (map (Syntax.string_of_term_global thy) intro_ts'))*)
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Sep 01 13:45:58 2010 +0200
@@ -259,7 +259,8 @@
fun rewrite_intros thy =
Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
- #> Simplifier.full_simplify (HOL_basic_ss addsimps @{thms bool_simps} addsimps @{thms nnf_simps})
+ #> Simplifier.full_simplify
+ (HOL_basic_ss addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps})
#> map_term thy (maps_premises (split_conjs thy))
fun print_specs options thy msg ths =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Sep 01 13:45:58 2010 +0200
@@ -216,11 +216,10 @@
relevance_thresholds, max_relevant, theory_relevant, isar_proof,
isar_shrink_factor, timeout, ...} : params)
minimize_command
- ({subgoal, goal, relevance_override, axioms} : problem) =
+ ({subgoal, goal = (ctxt, (chained_ths, th)), relevance_override,
+ axioms} : problem) =
let
- val (ctxt, (_, th)) = goal;
- val thy = ProofContext.theory_of ctxt
- val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
+ val (_, hyp_ts, concl_t) = strip_subgoal th subgoal
val print = priority
fun print_v f = () |> verbose ? print o f
@@ -230,10 +229,10 @@
case axioms of
SOME axioms => axioms
| NONE =>
- (relevant_facts full_types relevance_thresholds
+ (relevant_facts ctxt full_types relevance_thresholds
(the_default default_max_relevant max_relevant)
(the_default default_theory_relevant theory_relevant)
- relevance_override goal hyp_ts concl_t
+ relevance_override chained_ths hyp_ts concl_t
|> tap ((fn n => print_v (fn () =>
"Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
" for " ^ quote atp_name ^ ".")) o length))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Sep 01 13:45:58 2010 +0200
@@ -5,7 +5,7 @@
signature SLEDGEHAMMER_FACT_FILTER =
sig
- datatype locality = General | Theory | Local | Chained
+ datatype locality = General | Intro | Elim | Simp | Local | Chained
type relevance_override =
{add: Facts.ref list,
@@ -13,14 +13,26 @@
only: bool}
val trace : bool Unsynchronized.ref
- val term_patterns : bool Unsynchronized.ref
+ val worse_irrel_freq : real Unsynchronized.ref
+ val higher_order_irrel_weight : real Unsynchronized.ref
+ val abs_rel_weight : real Unsynchronized.ref
+ val abs_irrel_weight : real Unsynchronized.ref
+ val skolem_irrel_weight : real Unsynchronized.ref
+ val intro_bonus : real Unsynchronized.ref
+ val elim_bonus : real Unsynchronized.ref
+ val simp_bonus : real Unsynchronized.ref
+ val local_bonus : real Unsynchronized.ref
+ val chained_bonus : real Unsynchronized.ref
+ val max_imperfect : real Unsynchronized.ref
+ val max_imperfect_exp : real Unsynchronized.ref
+ val threshold_divisor : real Unsynchronized.ref
+ val ridiculous_threshold : real Unsynchronized.ref
val name_thm_pairs_from_ref :
Proof.context -> unit Symtab.table -> thm list -> Facts.ref
-> ((string * locality) * thm) list
val relevant_facts :
- bool -> real * real -> int -> bool -> relevance_override
- -> Proof.context * (thm list * 'a) -> term list -> term
- -> ((string * locality) * thm) list
+ Proof.context -> bool -> real * real -> int -> bool -> relevance_override
+ -> thm list -> term list -> term -> ((string * locality) * thm) list
end;
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
@@ -32,11 +44,11 @@
fun trace_msg msg = if !trace then tracing (msg ()) else ()
(* experimental feature *)
-val term_patterns = Unsynchronized.ref false
+val term_patterns = false
val respect_no_atp = true
-datatype locality = General | Theory | Local | Chained
+datatype locality = General | Intro | Elim | Simp | Local | Chained
type relevance_override =
{add: Facts.ref list,
@@ -69,13 +81,22 @@
(*** constants with types ***)
+fun order_of_type (Type (@{type_name fun}, [T1, @{typ bool}])) =
+ order_of_type T1 (* cheat: pretend sets are first-order *)
+ | order_of_type (Type (@{type_name fun}, [T1, T2])) =
+ Int.max (order_of_type T1 + 1, order_of_type T2)
+ | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
+ | order_of_type _ = 0
+
(* An abstraction of Isabelle types and first-order terms *)
datatype pattern = PVar | PApp of string * pattern list
+datatype ptype = PType of int * pattern list
fun string_for_pattern PVar = "_"
| string_for_pattern (PApp (s, ps)) =
if null ps then s else s ^ string_for_patterns ps
and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
+fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
(*Is the second type an instance of the first one?*)
fun match_pattern (PVar, _) = true
@@ -86,17 +107,18 @@
| match_patterns ([], _) = false
| match_patterns (p :: ps, q :: qs) =
match_pattern (p, q) andalso match_patterns (ps, qs)
+fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
(* Is there a unifiable constant? *)
fun pconst_mem f consts (s, ps) =
- exists (curry (match_patterns o f) ps)
+ exists (curry (match_ptype o f) ps)
(map snd (filter (curry (op =) s o fst) consts))
fun pconst_hyper_mem f const_tab (s, ps) =
- exists (curry (match_patterns o f) ps) (these (Symtab.lookup const_tab s))
+ exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
-fun ptype (Type (s, Ts)) = PApp (s, map ptype Ts)
- | ptype (TFree (s, _)) = PApp (s, [])
- | ptype (TVar _) = PVar
+fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
+ | pattern_for_type (TFree (s, _)) = PApp (s, [])
+ | pattern_for_type (TVar _) = PVar
fun pterm thy t =
case strip_comb t of
@@ -105,14 +127,17 @@
| (Var x, []) => PVar
| _ => PApp ("?", []) (* equivalence class of higher-order constructs *)
(* Pairs a constant with the list of its type instantiations. *)
-and pconst_args thy const (s, T) ts =
- (if const then map ptype (these (try (Sign.const_typargs thy) (s, T)))
+and ptype thy const x ts =
+ (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
else []) @
- (if !term_patterns then map (pterm thy) ts else [])
-and pconst thy const (s, T) ts = (s, pconst_args thy const (s, T) ts)
+ (if term_patterns then map (pterm thy) ts else [])
+and pconst thy const (s, T) ts = (s, ptype thy const (s, T) ts)
+and rich_ptype thy const (s, T) ts =
+ PType (order_of_type T, ptype thy const (s, T) ts)
+and rich_pconst thy const (s, T) ts = (s, rich_ptype thy const (s, T) ts)
-fun string_for_hyper_pconst (s, pss) =
- s ^ "{" ^ commas (map string_for_patterns pss) ^ "}"
+fun string_for_hyper_pconst (s, ps) =
+ s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
val abs_name = "Sledgehammer.abs"
val skolem_prefix = "Sledgehammer.sko"
@@ -125,54 +150,56 @@
(* Add a pconstant to the table, but a [] entry means a standard
connective, which we ignore.*)
-fun add_pconst_to_table also_skolem (c, ps) =
+fun add_pconst_to_table also_skolem (c, p) =
if member (op =) boring_consts c orelse
(not also_skolem andalso String.isPrefix skolem_prefix c) then
I
else
- Symtab.map_default (c, [ps]) (insert (op =) ps)
+ Symtab.map_default (c, [p]) (insert (op =) p)
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-fun get_pconsts thy also_skolems pos ts =
+fun pconsts_in_terms thy also_skolems pos ts =
let
val flip = Option.map not
(* We include free variables, as well as constants, to handle locales. For
each quantifiers that must necessarily be skolemized by the ATP, we
introduce a fresh constant to simulate the effect of Skolemization. *)
fun do_const const (s, T) ts =
- add_pconst_to_table also_skolems (pconst thy const (s, T) ts)
+ add_pconst_to_table also_skolems (rich_pconst thy const (s, T) ts)
#> fold do_term ts
and do_term t =
case strip_comb t of
(Const x, ts) => do_const true x ts
| (Free x, ts) => do_const false x ts
- | (Abs (_, _, t'), ts) =>
- null ts ? add_pconst_to_table true (abs_name, [])
+ | (Abs (_, T, t'), ts) =>
+ (null ts
+ ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, [])))
#> fold do_term (t' :: ts)
| (_, ts) => fold do_term ts
- fun do_quantifier will_surely_be_skolemized body_t =
+ fun do_quantifier will_surely_be_skolemized abs_T body_t =
do_formula pos body_t
#> (if also_skolems andalso will_surely_be_skolemized then
- add_pconst_to_table true (gensym skolem_prefix, [])
+ add_pconst_to_table true
+ (gensym skolem_prefix, PType (order_of_type abs_T, []))
else
I)
and do_term_or_formula T =
if is_formula_type T then do_formula NONE else do_term
and do_formula pos t =
case t of
- Const (@{const_name all}, _) $ Abs (_, _, body_t) =>
- do_quantifier (pos = SOME false) body_t
+ Const (@{const_name all}, _) $ Abs (_, T, t') =>
+ do_quantifier (pos = SOME false) T t'
| @{const "==>"} $ t1 $ t2 =>
do_formula (flip pos) t1 #> do_formula pos t2
| Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
fold (do_term_or_formula T) [t1, t2]
| @{const Trueprop} $ t1 => do_formula pos t1
| @{const Not} $ t1 => do_formula (flip pos) t1
- | Const (@{const_name All}, _) $ Abs (_, _, body_t) =>
- do_quantifier (pos = SOME false) body_t
- | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
- do_quantifier (pos = SOME true) body_t
+ | Const (@{const_name All}, _) $ Abs (_, T, t') =>
+ do_quantifier (pos = SOME false) T t'
+ | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
+ do_quantifier (pos = SOME true) T t'
| @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
| @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
| @{const HOL.implies} $ t1 $ t2 =>
@@ -182,14 +209,14 @@
| Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
$ t1 $ t2 $ t3 =>
do_formula NONE t1 #> fold (do_term_or_formula T) [t2, t3]
- | Const (@{const_name Ex1}, _) $ Abs (_, _, body_t) =>
- do_quantifier (is_some pos) body_t
- | Const (@{const_name Ball}, _) $ t1 $ Abs (_, _, body_t) =>
- do_quantifier (pos = SOME false)
- (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, body_t))
- | Const (@{const_name Bex}, _) $ t1 $ Abs (_, _, body_t) =>
- do_quantifier (pos = SOME true)
- (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, body_t))
+ | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
+ do_quantifier (is_some pos) T t'
+ | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
+ do_quantifier (pos = SOME false) T
+ (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
+ | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
+ do_quantifier (pos = SOME true) T
+ (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
| (t0 as Const (_, @{typ bool})) $ t1 =>
do_term t0 #> do_formula pos t1 (* theory constant *)
| _ => do_term t
@@ -219,16 +246,17 @@
| (PApp _, PVar) => GREATER
| (PApp q1, PApp q2) =>
prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
+fun ptype_ord (PType p, PType q) =
+ prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
-structure CTtab =
- Table(type key = pattern list val ord = dict_ord pattern_ord)
+structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
fun count_axiom_consts theory_relevant thy =
let
fun do_const const (s, T) ts =
(* Two-dimensional table update. Constant maps to types maps to count. *)
- CTtab.map_default (pconst_args thy const (s, T) ts, 0) (Integer.add 1)
- |> Symtab.map_default (s, CTtab.empty)
+ PType_Tab.map_default (rich_ptype thy const (s, T) ts, 0) (Integer.add 1)
+ |> Symtab.map_default (s, PType_Tab.empty)
#> fold do_term ts
and do_term t =
case strip_comb t of
@@ -241,62 +269,108 @@
(**** Actual Filtering Code ****)
+fun pow_int x 0 = 1.0
+ | pow_int x 1 = x
+ | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
+
(*The frequency of a constant is the sum of those of all instances of its type.*)
fun pconst_freq match const_tab (c, ps) =
- CTtab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
- (the (Symtab.lookup const_tab c)) 0
+ PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
+ (the (Symtab.lookup const_tab c)) 0
(* A surprising number of theorems contain only a few significant constants.
These include all induction rules, and other general theorems. *)
(* "log" seems best in practice. A constant function of one ignores the constant
- frequencies. *)
-fun rel_log n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0)
-fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
+ frequencies. Rare constants give more points if they are relevant than less
+ rare ones. *)
+fun rel_weight_for order freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
(* FUDGE *)
-val abs_rel_weight = 0.5
-val abs_irrel_weight = 2.0
-val skolem_rel_weight = 2.0 (* impossible *)
-val skolem_irrel_weight = 0.5
+val worse_irrel_freq = Unsynchronized.ref 100.0
+val higher_order_irrel_weight = Unsynchronized.ref 1.05
+
+(* Irrelevant constants are treated differently. We associate lower penalties to
+ very rare constants and very common ones -- the former because they can't
+ lead to the inclusion of too many new facts, and the latter because they are
+ so common as to be of little interest. *)
+fun irrel_weight_for order freq =
+ let val (k, x) = !worse_irrel_freq |> `Real.ceil in
+ (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
+ else rel_weight_for order freq / rel_weight_for order k)
+ * pow_int (!higher_order_irrel_weight) (order - 1)
+ end
+
+(* FUDGE *)
+val abs_rel_weight = Unsynchronized.ref 0.5
+val abs_irrel_weight = Unsynchronized.ref 2.0
+val skolem_irrel_weight = Unsynchronized.ref 0.75
(* Computes a constant's weight, as determined by its frequency. *)
-fun generic_weight abs_weight skolem_weight logx f const_tab (c as (s, _)) =
+fun generic_pconst_weight abs_weight skolem_weight weight_for f const_tab
+ (c as (s, PType (m, _))) =
if s = abs_name then abs_weight
else if String.isPrefix skolem_prefix s then skolem_weight
- else logx (pconst_freq (match_patterns o f) const_tab c)
+ else weight_for m (pconst_freq (match_ptype o f) const_tab c)
-val rel_weight = generic_weight abs_rel_weight skolem_rel_weight rel_log I
-val irrel_weight = generic_weight abs_irrel_weight skolem_irrel_weight irrel_log
- swap
+fun rel_pconst_weight const_tab =
+ generic_pconst_weight (!abs_rel_weight) 0.0 rel_weight_for I const_tab
+fun irrel_pconst_weight const_tab =
+ generic_pconst_weight (!abs_irrel_weight) (!skolem_irrel_weight)
+ irrel_weight_for swap const_tab
(* FUDGE *)
-fun locality_multiplier General = 1.0
- | locality_multiplier Theory = 1.1
- | locality_multiplier Local = 1.3
- | locality_multiplier Chained = 2.0
+val intro_bonus = Unsynchronized.ref 0.15
+val elim_bonus = Unsynchronized.ref 0.15
+val simp_bonus = Unsynchronized.ref 0.15
+val local_bonus = Unsynchronized.ref 0.55
+val chained_bonus = Unsynchronized.ref 1.5
+
+fun locality_bonus General = 0.0
+ | locality_bonus Intro = !intro_bonus
+ | locality_bonus Elim = !elim_bonus
+ | locality_bonus Simp = !simp_bonus
+ | locality_bonus Local = !local_bonus
+ | locality_bonus Chained = !chained_bonus
fun axiom_weight loc const_tab relevant_consts axiom_consts =
case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
||> filter_out (pconst_hyper_mem swap relevant_consts) of
([], _) => 0.0
| (rel, irrel) =>
- case irrel |> filter_out (pconst_mem swap rel) of
- [] => 1.0
- | irrel =>
- let
- val rel_weight =
- fold (curry Real.+ o rel_weight const_tab) rel 0.0
- |> curry Real.* (locality_multiplier loc)
- val irrel_weight =
- fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
- val res = rel_weight / (rel_weight + irrel_weight)
- in if Real.isFinite res then res else 0.0 end
+ let
+ val irrel = irrel |> filter_out (pconst_mem swap rel)
+ val rel_weight =
+ 0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
+ val irrel_weight =
+ ~ (locality_bonus loc)
+ |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
+ val res = rel_weight / (rel_weight + irrel_weight)
+ in if Real.isFinite res then res else 0.0 end
+
+(* FIXME: experiment
+fun debug_axiom_weight loc const_tab relevant_consts axiom_consts =
+ case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
+ ||> filter_out (pconst_hyper_mem swap relevant_consts) of
+ ([], _) => 0.0
+ | (rel, irrel) =>
+ let
+ val irrel = irrel |> filter_out (pconst_mem swap rel)
+ val rels_weight =
+ 0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
+ val irrels_weight =
+ ~ (locality_bonus loc)
+ |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
+val _ = tracing (PolyML.makestring ("REL: ", map (`(rel_pconst_weight const_tab)) rel))
+val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight const_tab)) irrel))
+ val res = rels_weight / (rels_weight + irrels_weight)
+ in if Real.isFinite res then res else 0.0 end
+*)
fun pconsts_in_axiom thy t =
Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
- (get_pconsts thy true (SOME true) [t]) []
+ (pconsts_in_terms thy true (SOME true) [t]) []
fun pair_consts_axiom theory_relevant thy axiom =
case axiom |> snd |> theory_const_prop_of theory_relevant
|> pconsts_in_axiom thy of
@@ -304,24 +378,29 @@
| consts => SOME ((axiom, consts), NONE)
type annotated_thm =
- (((unit -> string) * locality) * thm) * (string * pattern list) list
+ (((unit -> string) * locality) * thm) * (string * ptype) list
-fun take_most_relevant max_max_imperfect max_relevant remaining_max
+(* FUDGE *)
+val max_imperfect = Unsynchronized.ref 11.5
+val max_imperfect_exp = Unsynchronized.ref 1.0
+
+fun take_most_relevant max_relevant remaining_max
(candidates : (annotated_thm * real) list) =
let
val max_imperfect =
- Real.ceil (Math.pow (max_max_imperfect,
- Real.fromInt remaining_max
- / Real.fromInt max_relevant))
+ Real.ceil (Math.pow (!max_imperfect,
+ Math.pow (Real.fromInt remaining_max
+ / Real.fromInt max_relevant, !max_imperfect_exp)))
val (perfect, imperfect) =
- candidates |> List.partition (fn (_, w) => w > 0.99999)
- ||> sort (Real.compare o swap o pairself snd)
+ candidates |> sort (Real.compare o swap o pairself snd)
+ |> take_prefix (fn (_, w) => w > 0.99999)
val ((accepts, more_rejects), rejects) =
chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
in
- trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^
- " of " ^ Int.toString (length candidates) ^ "): " ^ (accepts
- |> map (fn ((((name, _), _), _), weight) =>
+ trace_msg (fn () =>
+ "Actually passed (" ^ Int.toString (length accepts) ^ " of " ^
+ Int.toString (length candidates) ^ "): " ^
+ (accepts |> map (fn ((((name, _), _), _), weight) =>
name () ^ " [" ^ Real.toString weight ^ "]")
|> commas));
(accepts, more_rejects @ rejects)
@@ -329,16 +408,15 @@
fun if_empty_replace_with_locality thy axioms loc tab =
if Symtab.is_empty tab then
- get_pconsts thy false (SOME false)
+ pconsts_in_terms thy false (SOME false)
(map_filter (fn ((_, loc'), th) =>
if loc' = loc then SOME (prop_of th) else NONE) axioms)
else
tab
(* FUDGE *)
-val threshold_divisor = 2.0
-val ridiculous_threshold = 0.1
-val max_max_imperfect_fudge_factor = 0.66
+val threshold_divisor = Unsynchronized.ref 2.0
+val ridiculous_threshold = Unsynchronized.ref 0.1
fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
({add, del, ...} : relevance_override) axioms goal_ts =
@@ -347,13 +425,10 @@
val const_tab =
fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty
val goal_const_tab =
- get_pconsts thy false (SOME false) goal_ts
- |> fold (if_empty_replace_with_locality thy axioms)
- [Chained, Local, Theory]
+ pconsts_in_terms thy false (SOME false) goal_ts
+ |> fold (if_empty_replace_with_locality thy axioms) [Chained, Local]
val add_thms = maps (ProofContext.get_fact ctxt) add
val del_thms = maps (ProofContext.get_fact ctxt) del
- val max_max_imperfect =
- Math.sqrt (Real.fromInt max_relevant * max_max_imperfect_fudge_factor)
fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
let
fun game_over rejects =
@@ -364,23 +439,21 @@
map_filter (fn ((p as (_, th), _), _) =>
if member Thm.eq_thm add_thms th then SOME p
else NONE) rejects
- fun relevant [] rejects hopeless [] =
+ fun relevant [] rejects [] =
(* Nothing has been added this iteration. *)
- if j = 0 andalso threshold >= ridiculous_threshold then
+ if j = 0 andalso threshold >= !ridiculous_threshold then
(* First iteration? Try again. *)
- iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
+ iter 0 max_relevant (threshold / !threshold_divisor) rel_const_tab
hopeless hopeful
else
game_over (rejects @ hopeless)
- | relevant candidates rejects hopeless [] =
+ | relevant candidates rejects [] =
let
val (accepts, more_rejects) =
- take_most_relevant max_max_imperfect max_relevant remaining_max
- candidates
+ take_most_relevant max_relevant remaining_max candidates
val rel_const_tab' =
rel_const_tab
- |> fold (add_pconst_to_table false)
- (maps (snd o fst) accepts)
+ |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
fun is_dirty (c, _) =
Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
val (hopeful_rejects, hopeless_rejects) =
@@ -410,7 +483,7 @@
iter (j + 1) remaining_max threshold rel_const_tab'
hopeless_rejects hopeful_rejects)
end
- | relevant candidates rejects hopeless
+ | relevant candidates rejects
(((ax as (((_, loc), th), axiom_consts)), cached_weight)
:: hopeful) =
let
@@ -418,18 +491,18 @@
case cached_weight of
SOME w => w
| NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
-(* TODO: experiment
+(* FIXME: experiment
val name = fst (fst (fst ax)) ()
-val _ = if String.isPrefix "lift.simps(3" name then
-tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))
+val _ = if String.isSubstring "positive_minus" name orelse String.isSubstring "not_exp_le_zero" name then
+tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight loc const_tab rel_const_tab axiom_consts))
else
()
*)
in
if weight >= threshold then
- relevant ((ax, weight) :: candidates) rejects hopeless hopeful
+ relevant ((ax, weight) :: candidates) rejects hopeful
else
- relevant candidates ((ax, weight) :: rejects) hopeless hopeful
+ relevant candidates ((ax, weight) :: rejects) hopeful
end
in
trace_msg (fn () =>
@@ -438,7 +511,7 @@
commas (rel_const_tab |> Symtab.dest
|> filter (curry (op <>) [] o snd)
|> map string_for_hyper_pconst));
- relevant [] [] hopeless hopeful
+ relevant [] [] hopeful
end
in
axioms |> filter_out (member Thm.eq_thm del_thms o snd)
@@ -465,9 +538,9 @@
String.isSuffix "_def" a orelse String.isSuffix "_defs" a
end;
-fun make_fact_table xs =
- fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
-fun make_unique xs = Termtab.fold (cons o snd) (make_fact_table xs) []
+fun mk_fact_table f xs =
+ fold (Termtab.update o `(prop_of o f)) xs Termtab.empty
+fun uniquify xs = Termtab.fold (cons o snd) (mk_fact_table snd xs) []
(* FIXME: put other record thms here, or declare as "no_atp" *)
val multi_base_blacklist =
@@ -508,6 +581,11 @@
val exists_sledgehammer_const =
exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
+(* FIXME: make more reliable *)
+val exists_low_level_class_const =
+ exists_Const (fn (s, _) =>
+ String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
+
fun is_metastrange_theorem th =
case head_of (concl_of th) of
Const (a, _) => (a <> @{const_name Trueprop} andalso
@@ -588,17 +666,30 @@
let val t = prop_of thm in
is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse
- is_metastrange_theorem thm orelse is_that_fact thm
+ exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
+ is_that_fact thm
end
+fun clasimpset_rules_of ctxt =
+ let
+ val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> rep_cs
+ val intros = safeIs @ hazIs
+ val elims = map Classical.classical_rule (safeEs @ hazEs)
+ val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
+ in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
+
fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
let
val thy = ProofContext.theory_of ctxt
- val thy_prefix = Context.theory_name thy ^ Long_Name.separator
val global_facts = PureThy.facts_of thy
val local_facts = ProofContext.facts_of ctxt
val named_locals = local_facts |> Facts.dest_static []
val is_chained = member Thm.eq_thm chained_ths
+ val (intros, elims, simps) =
+ if exists (curry (op <) 0.0) [!intro_bonus, !elim_bonus, !simp_bonus] then
+ clasimpset_rules_of ctxt
+ else
+ (Termtab.empty, Termtab.empty, Termtab.empty)
(* Unnamed nonchained formulas with schematic variables are omitted, because
they are rejected by the backticks (`...`) parser for some reason. *)
fun is_good_unnamed_local th =
@@ -621,10 +712,6 @@
I
else
let
- val base_loc =
- if not global then Local
- else if String.isPrefix thy_prefix name0 then Theory
- else General
val multi = length ths > 1
fun backquotify th =
"`" ^ Print_Mode.setmp [Print_Mode.input]
@@ -654,7 +741,15 @@
case find_first check_thms [name1, name2, name0] of
SOME name => repair_name reserved multi j name
| NONE => ""
- end), if is_chained th then Chained else base_loc),
+ end),
+ let val t = prop_of th in
+ if is_chained th then Chained
+ else if not global then Local
+ else if Termtab.defined intros t then Intro
+ else if Termtab.defined elims t then Elim
+ else if Termtab.defined simps t then Simp
+ else General
+ end),
(multi, th)) :: rest)) ths
#> snd
end)
@@ -673,9 +768,9 @@
(* ATP invocation methods setup *)
(***************************************************************)
-fun relevant_facts full_types (threshold0, threshold1) max_relevant
+fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant
theory_relevant (relevance_override as {add, del, only})
- (ctxt, (chained_ths, _)) hyp_ts concl_t =
+ chained_ths hyp_ts concl_t =
let
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
1.0 / Real.fromInt (max_relevant + 1))
@@ -688,7 +783,7 @@
else
all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
|> name_thm_pairs ctxt (respect_no_atp andalso not only)
- |> make_unique
+ |> uniquify
in
trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
" theorems");
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 01 13:45:58 2010 +0200
@@ -67,7 +67,7 @@
("verbose", "false"),
("overlord", "false"),
("explicit_apply", "false"),
- ("relevance_thresholds", "45 95"),
+ ("relevance_thresholds", "45 85"),
("max_relevant", "smart"),
("theory_relevant", "smart"),
("isar_proof", "false"),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Sep 01 13:45:58 2010 +0200
@@ -218,8 +218,10 @@
count_combformula combformula
val optional_helpers =
- [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
- (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
+ [(["c_COMBI"], @{thms COMBI_def}),
+ (["c_COMBK"], @{thms COMBK_def}),
+ (["c_COMBB"], @{thms COMBB_def}),
+ (["c_COMBC"], @{thms COMBC_def}),
(["c_COMBS"], @{thms COMBS_def})]
val optional_typed_helpers =
[(["c_True", "c_False", "c_If"], @{thms True_or_False}),
--- a/src/HOL/Tools/list_code.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Tools/list_code.ML Wed Sep 01 13:45:58 2010 +0200
@@ -46,7 +46,7 @@
Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
| NONE =>
default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
- in Code_Target.add_syntax_const target @{const_name Cons}
+ in Code_Target.add_const_syntax target @{const_name Cons}
(SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
end
--- a/src/HOL/Tools/numeral.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Tools/numeral.ML Wed Sep 01 13:45:58 2010 +0200
@@ -76,7 +76,7 @@
fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
(Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
in
- thy |> Code_Target.add_syntax_const target number_of
+ thy |> Code_Target.add_const_syntax target number_of
(SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
@{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))))
end;
--- a/src/HOL/Tools/string_code.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/Tools/string_code.ML Wed Sep 01 13:45:58 2010 +0200
@@ -59,7 +59,7 @@
Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
| NONE =>
List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
- in Code_Target.add_syntax_const target
+ in Code_Target.add_const_syntax target
@{const_name Cons} (SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))
end;
@@ -69,7 +69,7 @@
case decode_char nibbles' (t1, t2)
of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
| NONE => Code_Printer.eqn_error thm "Illegal character expression";
- in Code_Target.add_syntax_const target
+ in Code_Target.add_const_syntax target
@{const_name Char} (SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))
end;
@@ -82,7 +82,7 @@
of SOME p => p
| NONE => Code_Printer.eqn_error thm "Illegal message expression")
| NONE => Code_Printer.eqn_error thm "Illegal message expression";
- in Code_Target.add_syntax_const target
+ in Code_Target.add_const_syntax target
@{const_name STR} (SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/try.ML Wed Sep 01 13:45:58 2010 +0200
@@ -0,0 +1,81 @@
+(* Title: HOL/Tools/try.ML
+ Author: Jasmin Blanchette, TU Muenchen
+
+Try a combination of proof methods.
+*)
+
+signature TRY =
+sig
+ val invoke_try : Proof.state -> unit
+end;
+
+structure Try : TRY =
+struct
+
+val timeout = Time.fromSeconds 5
+
+fun can_apply pre post tac st =
+ let val {goal, ...} = Proof.goal st in
+ case TimeLimit.timeLimit timeout (Seq.pull o tac) (pre st) of
+ SOME (x, _) => nprems_of (post x) < nprems_of goal
+ | NONE => false
+ end
+
+fun do_generic command pre post apply st =
+ let val timer = Timer.startRealTimer () in
+ if can_apply pre post apply st then
+ SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
+ else
+ NONE
+ end
+
+fun named_method thy name =
+ Method.method thy (Args.src ((name, []), Position.none))
+
+fun apply_named_method name ctxt =
+ let val thy = ProofContext.theory_of ctxt in
+ Method.apply (named_method thy name) ctxt []
+ end
+
+fun do_named_method name st =
+ do_generic name (#goal o Proof.goal) snd
+ (apply_named_method name (Proof.context_of st)) st
+
+fun apply_named_method_on_first_goal name ctxt =
+ let val thy = ProofContext.theory_of ctxt in
+ Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
+ end
+
+fun do_named_method_on_first_goal name st =
+ do_generic (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
+ else "")) I (#goal o Proof.goal)
+ (apply_named_method_on_first_goal name (Proof.context_of st)) st
+
+val all_goals_named_methods = ["auto", "safe"]
+val first_goal_named_methods =
+ ["simp", "fast", "fastsimp", "force", "best", "blast"]
+val do_methods =
+ map do_named_method_on_first_goal all_goals_named_methods @
+ map do_named_method first_goal_named_methods
+
+fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
+
+fun invoke_try st =
+ case do_methods |> Par_List.map (fn f => f st)
+ |> map_filter I |> sort (int_ord o pairself snd) of
+ [] => writeln "No proof found."
+ | xs as (s, _) :: _ =>
+ priority ("Try this command: " ^
+ Markup.markup Markup.sendback
+ ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^
+ " " ^ s) ^
+ ".\n(" ^ space_implode "; " (map time_string xs) ^ ")\n")
+
+val tryN = "try"
+
+val _ =
+ Outer_Syntax.improper_command tryN
+ "try a combination of proof methods" Keyword.diag
+ (Scan.succeed (Toplevel.keep (invoke_try o Toplevel.proof_of)))
+
+end;
--- a/src/HOL/ex/Numeral.thy Tue Aug 31 23:46:49 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Wed Sep 01 13:45:58 2010 +0200
@@ -989,7 +989,7 @@
in dest_num end;
fun pretty sgn literals [one', dig0', dig1'] _ thm _ _ [(t, _)] =
(Code_Printer.str o print literals o sgn o dest_num one' dig0' dig1' thm) t
- fun add_syntax (c, sgn) = Code_Target.add_syntax_const target c
+ fun add_syntax (c, sgn) = Code_Target.add_const_syntax target c
(SOME (Code_Printer.complex_const_syntax
(1, ([@{const_name One}, @{const_name Dig0}, @{const_name Dig1}],
pretty sgn))));
--- a/src/Pure/ML/ml_context.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/Pure/ML/ml_context.ML Wed Sep 01 13:45:58 2010 +0200
@@ -35,8 +35,8 @@
val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
Context.generic -> Context.generic
- val evaluate:
- Proof.context -> bool -> string * (unit -> 'a) option Unsynchronized.ref -> string -> 'a
+ val evaluate: Proof.context -> bool ->
+ string * (unit -> 'a) option Unsynchronized.ref -> string * string -> 'a
end
structure ML_Context: ML_CONTEXT =
@@ -203,10 +203,10 @@
(* FIXME not thread-safe -- reference can be accessed directly *)
-fun evaluate ctxt verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
+fun evaluate ctxt verbose (ref_name, r) (prelude, txt) = NAMED_CRITICAL "ML" (fn () =>
let
- val ants =
- ML_Lex.read Position.none ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))");
+ val s = prelude ^ "val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))"
+ val ants = ML_Lex.read Position.none s;
val _ = r := NONE;
val _ =
Context.setmp_thread_data (SOME (Context.Proof ctxt))
--- a/src/Tools/Code/code_eval.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Wed Sep 01 13:45:58 2010 +0200
@@ -9,8 +9,6 @@
val target: string
val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
-> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
- val evaluation_code: theory -> string -> string list -> string list
- -> string * ((string * string) list * (string * string) list)
val setup: theory -> theory
end;
@@ -21,16 +19,12 @@
val target = "Eval";
-val eval_struct_name = "Code";
-
-fun evaluation_code thy struct_name_hint tycos consts =
+fun evaluation_code thy module_name tycos consts =
let
val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
- val struct_name = if struct_name_hint = "" then eval_struct_name
- else struct_name_hint;
- val (ml_code, target_names) = Code_ML.evaluation_code_of thy target
- struct_name naming program (consts' @ tycos');
+ val (ml_code, target_names) = Code_Target.produce_code_for thy
+ target NONE module_name [] naming program (consts' @ tycos');
val (consts'', tycos'') = chop (length consts') target_names;
val consts_map = map2 (fn const => fn NONE =>
error ("Constant " ^ (quote o Code.string_of_const thy) const
@@ -57,11 +51,11 @@
|> Graph.new_node (value_name,
Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
|> fold (curry Graph.add_edge value_name) deps;
- val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
- (the_default target some_target) "" naming program' [value_name];
- val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
- ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
- in ML_Context.evaluate ctxt false reff sml_code end;
+ val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
+ (the_default target some_target) NONE "Code" [] naming program' [value_name];
+ val value_code = space_implode " "
+ (value_name' :: map (enclose "(" ")") args);
+ in ML_Context.evaluate ctxt false reff (program_code, value_code) end;
in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
@@ -69,26 +63,23 @@
local
-structure CodeAntiqData = Proof_Data
+structure Code_Antiq_Data = Proof_Data
(
- type T = (string list * string list) * (bool * (string
- * (string * ((string * string) list * (string * string) list)) lazy));
- fun init _ = (([], []), (true, ("", Lazy.value ("", ([], [])))));
+ type T = (string list * string list) * (bool
+ * (string * ((string * string) list * (string * string) list)) lazy);
+ fun init _ = (([], []), (true, (Lazy.value ("", ([], [])))));
);
-val is_first_occ = fst o snd o CodeAntiqData.get;
+val is_first_occ = fst o snd o Code_Antiq_Data.get;
fun register_code new_tycos new_consts ctxt =
let
- val ((tycos, consts), (_, (struct_name, _))) = CodeAntiqData.get ctxt;
+ val ((tycos, consts), _) = Code_Antiq_Data.get ctxt;
val tycos' = fold (insert (op =)) new_tycos tycos;
val consts' = fold (insert (op =)) new_consts consts;
- val (struct_name', ctxt') = if struct_name = ""
- then ML_Antiquote.variant eval_struct_name ctxt
- else (struct_name, ctxt);
- val acc_code = Lazy.lazy
- (fn () => evaluation_code (ProofContext.theory_of ctxt) eval_struct_name tycos' consts');
- in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end;
+ val acc_code = Lazy.lazy (fn () =>
+ evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts');
+ in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
fun register_const const = register_code [] [const];
@@ -99,11 +90,11 @@
fun print_code is_first print_it ctxt =
let
- val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
+ val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
val ml_code = if is_first then ml_code
else "";
- val all_struct_name = "Isabelle." ^ struct_code_name;
+ val all_struct_name = "Isabelle";
in (ml_code, print_it all_struct_name tycos_map consts_map) end;
in
@@ -143,34 +134,30 @@
Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
in
thy
- |> Code_Target.add_syntax_tyco target tyco (SOME (k, pr))
+ |> Code_Target.add_tyco_syntax target tyco (SOME (k, pr))
end;
fun add_eval_constr (const, const') thy =
let
val k = Code.args_number thy const;
fun pr pr' fxy ts = Code_Printer.brackify fxy
- (const' :: the_list (Code_ML.print_tuple pr' Code_Printer.BR (map fst ts)));
+ (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
in
thy
- |> Code_Target.add_syntax_const target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
+ |> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
end;
-fun add_eval_const (const, const') = Code_Target.add_syntax_const target
+fun add_eval_const (const, const') = Code_Target.add_const_syntax target
const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
- let
- val pr = Code_Printer.str o Long_Name.append module_name;
- in
- thy
- |> Code_Target.add_reserved target module_name
- |> Context.theory_map
- (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
- |> fold (add_eval_tyco o apsnd pr) tyco_map
- |> fold (add_eval_constr o apsnd pr) constr_map
- |> fold (add_eval_const o apsnd pr) const_map
- end
+ thy
+ |> Code_Target.add_reserved target module_name
+ |> Context.theory_map
+ (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
+ |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
+ |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
+ |> fold (add_eval_const o apsnd Code_Printer.str) const_map
| process (code_body, _) _ (SOME file_name) thy =
let
val preamble =
--- a/src/Tools/Code/code_haskell.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Wed Sep 01 13:45:58 2010 +0200
@@ -24,11 +24,11 @@
(** Haskell serializer **)
-fun print_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
+fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
reserved deresolve contr_classparam_typs deriving_show =
let
val deresolve_base = Long_Name.base_name o deresolve;
- fun class_name class = case syntax_class class
+ fun class_name class = case class_syntax class
of NONE => deresolve class
| SOME class => class;
fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
@@ -43,7 +43,7 @@
(map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
fun print_tyco_expr tyvars fxy (tyco, tys) =
brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
- and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
+ and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco
of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
| SOME (i, print) => print (print_typ tyvars) fxy tys)
| print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
@@ -72,7 +72,7 @@
in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
| print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
+ of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
then print_case tyvars some_thm vars fxy cases
else print_app tyvars some_thm vars fxy c_ts
| NONE => print_case tyvars some_thm vars fxy cases)
@@ -90,7 +90,7 @@
(str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs)
else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
end
- and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const
+ and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
let
@@ -133,7 +133,7 @@
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
|> intro_base_names
- (is_none o syntax_const) deresolve consts
+ (is_none o const_syntax) deresolve consts
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in
@@ -218,7 +218,7 @@
| print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
let
val tyvars = intro_vars (map fst vs) reserved;
- fun requires_args classparam = case syntax_const classparam
+ fun requires_args classparam = case const_syntax classparam
of NONE => 0
| SOME (Code_Printer.Plain_const_syntax _) => 0
| SOME (Code_Printer.Complex_const_syntax (k,_ )) => k;
@@ -234,7 +234,7 @@
val (c, (_, tys)) = const;
val (vs, rhs) = (apfst o map) fst
(Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
- val s = if (is_some o syntax_const) c
+ val s = if (is_some o const_syntax) c
then NONE else (SOME o Long_Name.base_name o deresolve) c;
val vars = reserved
|> intro_vars (map_filter I (s :: vs));
@@ -313,12 +313,12 @@
handle Option => error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, hs_program) end;
-fun serialize_haskell module_prefix module_name string_classes labelled_name
- raw_reserved includes module_alias
- syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program
- (stmt_names, presentation_stmt_names) destination =
+fun serialize_haskell module_prefix string_classes { labelled_name,
+ reserved_syms, includes, module_alias,
+ class_syntax, tyco_syntax, const_syntax, program,
+ names, presentation_names } =
let
- val reserved = fold (insert (op =) o fst) includes raw_reserved;
+ val reserved = fold (insert (op =) o fst) includes reserved_syms;
val (deresolver, hs_program) = haskell_program_of_program labelled_name
module_prefix reserved module_alias program;
val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
@@ -337,7 +337,7 @@
in deriv [] tyco end;
val reserved = make_vars reserved;
fun print_stmt qualified = print_haskell_stmt labelled_name
- syntax_class syntax_tyco syntax_const reserved
+ class_syntax tyco_syntax const_syntax reserved
(if qualified then deresolver else Long_Name.base_name o deresolver)
contr_classparam_typs
(if string_classes then deriving_show else K false);
@@ -350,7 +350,7 @@
fun serialize_module1 (module_name', (deps, (stmts, _))) =
let
val stmt_names = map fst stmts;
- val qualified = is_none module_name;
+ val qualified = null presentation_names;
val imports = subtract (op =) stmt_names deps
|> distinct (op =)
|> map_filter (try deresolver)
@@ -368,37 +368,41 @@
);
in print_module module_name' content end;
fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks2 (map_filter
- (fn (name, (_, SOME stmt)) => if null presentation_stmt_names
- orelse member (op =) presentation_stmt_names name
+ (fn (name, (_, SOME stmt)) => if null presentation_names
+ orelse member (op =) presentation_names name
then SOME (print_stmt false (name, stmt))
else NONE
| (_, (_, NONE)) => NONE) stmts);
val serialize_module =
- if null presentation_stmt_names then serialize_module1 else pair "" o serialize_module2;
- fun check_destination destination =
- (File.check destination; destination);
- fun write_module destination (modlname, content) =
- let
- val filename = case modlname
- of "" => Path.explode "Main.hs"
- | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
- o Long_Name.explode) modlname;
- val pathname = Path.append destination filename;
- val _ = File.mkdir_leaf (Path.dir pathname);
- in File.write pathname
- ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
- ^ code_of_pretty content)
- end
+ if null presentation_names then serialize_module1 else pair "" o serialize_module2;
+ fun write_module width (SOME destination) (modlname, content) =
+ let
+ val _ = File.check destination;
+ val filename = case modlname
+ of "" => Path.explode "Main.hs"
+ | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
+ o Long_Name.explode) modlname;
+ val pathname = Path.append destination filename;
+ val _ = File.mkdir_leaf (Path.dir pathname);
+ in File.write pathname
+ ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
+ ^ string_of_pretty width content)
+ end
+ | write_module width NONE (_, content) = writeln_pretty width content;
in
- Code_Target.mk_serialization target
- (fn NONE => K () o map (code_writeln o (fn p => Pretty.block [p, Pretty.fbrk]) o snd)
- | SOME file => K () o map (write_module (check_destination file)))
- (rpair [] o cat_lines o map (code_of_pretty o snd))
+ Code_Target.serialization
+ (fn width => fn destination => K () o map (write_module width destination))
+ (fn width => rpair [] o cat_lines o map (string_of_pretty width o snd))
(map (uncurry print_module) includes
@ map serialize_module (Symtab.dest hs_program))
- destination
end;
+val serializer : Code_Target.serializer =
+ Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
+ -- Scan.optional (Args.$$$ "string_classes" >> K true) false
+ >> (fn (module_prefix, string_classes) =>
+ serialize_haskell module_prefix string_classes));
+
val literals = let
fun char_haskell c =
let
@@ -460,19 +464,13 @@
val c_bind = Code.read_const thy raw_c_bind;
in if target = target' then
thy
- |> Code_Target.add_syntax_const target c_bind
+ |> Code_Target.add_const_syntax target c_bind
(SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
else error "Only Haskell target allows for monad syntax" end;
(** Isar setup **)
-fun isar_serializer module_name =
- Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
- -- Scan.optional (Args.$$$ "string_classes" >> K true) false
- >> (fn (module_prefix, string_classes) =>
- serialize_haskell module_prefix module_name string_classes));
-
val _ =
Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
@@ -481,11 +479,11 @@
val setup =
Code_Target.add_target
- (target, { serializer = isar_serializer, literals = literals,
+ (target, { serializer = serializer, literals = literals,
check = { env_var = "EXEC_GHC", make_destination = I,
make_command = fn ghc => fn module_name =>
ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
- #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
+ #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
str "->",
--- a/src/Tools/Code/code_ml.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Wed Sep 01 13:45:58 2010 +0200
@@ -8,10 +8,6 @@
sig
val target_SML: string
val target_OCaml: string
- val evaluation_code_of: theory -> string -> string
- -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
- val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
- -> Code_Printer.fixity -> 'a list -> Pretty.T option
val setup: theory -> theory
end;
@@ -56,21 +52,21 @@
| print_product print [x] = SOME (print x)
| print_product print xs = (SOME o enum " *" "" "") (map print xs);
-fun print_tuple _ _ [] = NONE
- | print_tuple print fxy [x] = SOME (print fxy x)
- | print_tuple print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
+fun tuplify _ _ [] = NONE
+ | tuplify print fxy [x] = SOME (print fxy x)
+ | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
(** SML serializer **)
-fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
+fun print_sml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =
let
fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
| print_tyco_expr fxy (tyco, [ty]) =
concat [print_typ BR ty, (str o deresolve) tyco]
| print_tyco_expr fxy (tyco, tys) =
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
- and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
+ and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
of NONE => print_tyco_expr fxy (tyco, tys)
| SOME (i, print) => print print_typ fxy tys)
| print_typ fxy (ITyVar v) = str ("'" ^ v);
@@ -94,7 +90,7 @@
| classrels => brackets
[enum " o" "(" ")" (map (str o deresolve) classrels), v_p]
end
- and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
+ and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
(map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
@@ -118,7 +114,7 @@
in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
| print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
+ of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
then print_case is_pseudo_fun some_thm vars fxy cases
else print_app is_pseudo_fun some_thm vars fxy c_ts
| NONE => print_case is_pseudo_fun some_thm vars fxy cases)
@@ -127,7 +123,7 @@
let val k = length function_typs in
if k < 2 orelse length ts = k
then (str o deresolve) c
- :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
+ :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
end
else if is_pseudo_fun c
@@ -135,7 +131,7 @@
else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
- (print_term is_pseudo_fun) syntax_const some_thm vars
+ (print_term is_pseudo_fun) const_syntax some_thm vars
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
let
@@ -194,7 +190,7 @@
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
|> intro_base_names
- (is_none o syntax_const) deresolve consts
+ (is_none o const_syntax) deresolve consts
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
val prolog = if needs_typ then
@@ -343,9 +339,8 @@
end;
in print_stmt end;
-fun print_sml_module name some_decls body = if name = ""
- then Pretty.chunks2 body
- else Pretty.chunks2 (
+fun print_sml_module name some_decls body =
+ Pretty.chunks2 (
Pretty.chunks (
str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
:: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
@@ -369,14 +364,14 @@
(** OCaml serializer **)
-fun print_ocaml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
+fun print_ocaml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =
let
fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
| print_tyco_expr fxy (tyco, [ty]) =
concat [print_typ BR ty, (str o deresolve) tyco]
| print_tyco_expr fxy (tyco, tys) =
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
- and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
+ and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
of NONE => print_tyco_expr fxy (tyco, tys)
| SOME (i, print) => print print_typ fxy tys)
| print_typ fxy (ITyVar v) = str ("'" ^ v);
@@ -395,7 +390,7 @@
else "_" ^ first_upper v ^ string_of_int (i+1))
|> fold_rev (fn classrel => fn p =>
Pretty.block [p, str ".", (str o deresolve) classrel]) classrels
- and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
+ and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
(map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
@@ -416,7 +411,7 @@
in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
| print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
+ of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
then print_case is_pseudo_fun some_thm vars fxy cases
else print_app is_pseudo_fun some_thm vars fxy c_ts
| NONE => print_case is_pseudo_fun some_thm vars fxy cases)
@@ -425,7 +420,7 @@
let val k = length tys in
if length ts = k
then (str o deresolve) c
- :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
+ :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
end
else if is_pseudo_fun c
@@ -433,7 +428,7 @@
else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
- (print_term is_pseudo_fun) syntax_const some_thm vars
+ (print_term is_pseudo_fun) const_syntax some_thm vars
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
let
@@ -499,7 +494,7 @@
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
|> intro_base_names
- (is_none o syntax_const) deresolve consts
+ (is_none o const_syntax) deresolve consts
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in
@@ -525,7 +520,7 @@
val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
val vars = reserved
|> intro_base_names
- (is_none o syntax_const) deresolve consts;
+ (is_none o const_syntax) deresolve consts;
val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
in
Pretty.block (
@@ -669,9 +664,8 @@
end;
in print_stmt end;
-fun print_ocaml_module name some_decls body = if name = ""
- then Pretty.chunks2 body
- else Pretty.chunks2 (
+fun print_ocaml_module name some_decls body =
+ Pretty.chunks2 (
Pretty.chunks (
str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
:: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
@@ -722,7 +716,7 @@
in
-fun ml_node_of_program labelled_name module_name reserved module_alias program =
+fun ml_node_of_program labelled_name reserved module_alias program =
let
val reserved = Name.make_context reserved;
val empty_module = ((reserved, reserved), Graph.empty);
@@ -906,21 +900,21 @@
error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, nodes) end;
-fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
- reserved includes module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program
- (stmt_names, presentation_stmt_names) =
+fun serialize_ml target print_module print_stmt with_signatures { labelled_name,
+ reserved_syms, includes, module_alias, class_syntax, tyco_syntax,
+ const_syntax, program, names, presentation_names } =
let
val is_cons = Code_Thingol.is_cons program;
- val is_presentation = not (null presentation_stmt_names);
- val (deresolver, nodes) = ml_node_of_program labelled_name module_name
- reserved module_alias program;
- val reserved = make_vars reserved;
+ val is_presentation = not (null presentation_names);
+ val (deresolver, nodes) = ml_node_of_program labelled_name
+ reserved_syms module_alias program;
+ val reserved = make_vars reserved_syms;
fun print_node prefix (Dummy _) =
NONE
| print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
- (null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt
+ (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
then NONE
- else SOME (print_stmt labelled_name syntax_tyco syntax_const reserved is_cons (deresolver prefix) stmt)
+ else SOME (print_stmt labelled_name tyco_syntax const_syntax reserved is_cons (deresolver prefix) stmt)
| print_node prefix (Module (module_name, (_, nodes))) =
let
val (decls, body) = print_nodes (prefix @ [module_name]) nodes;
@@ -931,53 +925,45 @@
o rev o flat o Graph.strong_conn) nodes
|> split_list
|> (fn (decls, body) => (flat decls, body))
- val stmt_names' = (map o try)
- (deresolver (if is_some module_name then the_list module_name else [])) stmt_names;
+ val names' = map (try (deresolver [])) names;
val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
+ fun write width NONE = writeln_pretty width
+ | write width (SOME p) = File.write p o string_of_pretty width;
in
- Code_Target.mk_serialization target
- (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
- (rpair stmt_names' o code_of_pretty) p
+ Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p
end;
end; (*local*)
-
-(** for instrumentalization **)
+val serializer_sml : Code_Target.serializer =
+ Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
+ >> (fn with_signatures => serialize_ml target_SML
+ print_sml_module print_sml_stmt with_signatures));
-fun evaluation_code_of thy target struct_name =
- Code_Target.serialize_custom thy (target, fn module_name => fn [] =>
- serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name);
+val serializer_ocaml : Code_Target.serializer =
+ Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
+ >> (fn with_signatures => serialize_ml target_OCaml
+ print_ocaml_module print_ocaml_stmt with_signatures));
(** Isar setup **)
-fun isar_serializer_sml module_name =
- Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
- >> (fn with_signatures => serialize_ml target_SML
- print_sml_module print_sml_stmt module_name with_signatures));
-
-fun isar_serializer_ocaml module_name =
- Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
- >> (fn with_signatures => serialize_ml target_OCaml
- print_ocaml_module print_ocaml_stmt module_name with_signatures));
-
val setup =
Code_Target.add_target
- (target_SML, { serializer = isar_serializer_sml, literals = literals_sml,
+ (target_SML, { serializer = serializer_sml, literals = literals_sml,
check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
#> Code_Target.add_target
- (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
+ (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
- #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
+ #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
str "->",
print_typ (INFX (1, R)) ty2
)))
- #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
+ #> Code_Target.add_tyco_syntax target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
str "->",
--- a/src/Tools/Code/code_printer.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Wed Sep 01 13:45:58 2010 +0200
@@ -68,6 +68,8 @@
val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
+ val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
+
type tyco_syntax
type simple_const_syntax
@@ -124,7 +126,7 @@
fun indent i = Print_Mode.setmp [] (Pretty.indent i);
fun string_of_pretty width p = Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
-fun writeln_pretty width p = writeln (Print_Mode.setmp [] (Pretty.string_of_margin width) p);
+fun writeln_pretty width p = writeln (string_of_pretty width p);
(** names and variable name contexts **)
@@ -244,6 +246,10 @@
(if (fixity BR fxy_ctxt) then enclose "(" ")" else Pretty.block)
(p @@ enum "," opn cls (map f ps));
+fun tuplify _ _ [] = NONE
+ | tuplify print fxy [x] = SOME (print fxy x)
+ | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
+
(* generic syntax *)
@@ -278,8 +284,8 @@
fold_map (Code_Thingol.ensure_declared_const thy) cs naming
|-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
-fun gen_print_app print_app_expr print_term syntax_const some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
- case syntax_const c
+fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
+ case const_syntax c
of NONE => brackify fxy (print_app_expr some_thm vars app)
| SOME (Plain_const_syntax (_, s)) => brackify fxy (str s :: map (print_term some_thm vars BR) ts)
| SOME (Complex_const_syntax (k, print)) =>
--- a/src/Tools/Code/code_scala.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Wed Sep 01 13:45:58 2010 +0200
@@ -24,14 +24,14 @@
(** Scala serializer **)
-fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
+fun print_scala_stmt labelled_name tyco_syntax const_syntax reserved
args_num is_singleton_constr (deresolve, deresolve_full) =
let
fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
(print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys
- and print_typ tyvars fxy (tyco `%% tys) = (case syntax_tyco tyco
+ and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
of NONE => print_tyco_expr tyvars fxy (tyco, tys)
| SOME (i, print) => print (print_typ tyvars) fxy tys)
| print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
@@ -67,7 +67,7 @@
end
| print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
+ of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
then print_case tyvars some_thm vars fxy cases
else print_app tyvars is_pat some_thm vars fxy c_ts
| NONE => print_case tyvars some_thm vars fxy cases)
@@ -76,8 +76,8 @@
let
val k = length ts;
val arg_typs' = if is_pat orelse
- (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
- val (l, print') = case syntax_const c
+ (is_none (const_syntax c) andalso is_singleton_constr c) then [] else arg_typs;
+ val (l, print') = case const_syntax c
of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
@@ -156,7 +156,7 @@
fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
val tyvars = reserved
|> intro_base_names
- (is_none o syntax_tyco) deresolve tycos
+ (is_none o tyco_syntax) deresolve tycos
|> intro_tyvars vs;
val simple = case eqs
of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
@@ -165,14 +165,14 @@
(map (snd o fst) eqs) [];
val vars1 = reserved
|> intro_base_names
- (is_none o syntax_const) deresolve consts
+ (is_none o const_syntax) deresolve consts
val params = if simple
then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
else aux_params vars1 (map (fst o fst) eqs);
val vars2 = intro_vars params vars1;
val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;
- fun print_tuple [p] = p
- | print_tuple ps = enum "," "(" ")" ps;
+ fun tuplify [p] = p
+ | tuplify ps = enum "," "(" ")" ps;
fun print_rhs vars' ((_, t), (some_thm, _)) =
print_term tyvars false some_thm vars' NOBR t;
fun print_clause (eq as ((ts, _), (some_thm, _))) =
@@ -181,7 +181,7 @@
(insert (op =)) ts []) vars1;
in
concat [str "case",
- print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
+ tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
str "=>", print_rhs vars' eq]
end;
val head = print_defhead tyvars vars2 name vs params tys' ty';
@@ -189,7 +189,7 @@
concat [head, print_rhs vars2 (hd eqs)]
else
Pretty.block_enclose
- (concat [head, print_tuple (map (str o lookup_var vars2) params),
+ (concat [head, tuplify (map (str o lookup_var vars2) params),
str "match", str "{"], str "}")
(map print_clause eqs)
end;
@@ -413,13 +413,13 @@
in (deresolver, sca_program) end;
-fun serialize_scala labelled_name raw_reserved includes module_alias
- _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
- program (stmt_names, presentation_stmt_names) destination =
+fun serialize_scala { labelled_name, reserved_syms, includes,
+ module_alias, class_syntax, tyco_syntax, const_syntax, program,
+ names, presentation_names } =
let
(* build program *)
- val reserved = fold (insert (op =) o fst) includes raw_reserved;
+ val reserved = fold (insert (op =) o fst) includes reserved_syms;
val (deresolver, sca_program) = scala_program_of_program labelled_name
(Name.make_context reserved) module_alias program;
@@ -440,7 +440,7 @@
fun is_singleton_constr c = case Graph.get_node program c
of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
| _ => false;
- val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
+ val print_stmt = print_scala_stmt labelled_name tyco_syntax const_syntax
(make_vars reserved) args_num is_singleton_constr;
(* print nodes *)
@@ -455,12 +455,12 @@
in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
fun print_node _ (_, Dummy) = NONE
| print_node prefix_fragments (name, Stmt stmt) =
- if null presentation_stmt_names
- orelse member (op =) presentation_stmt_names name
+ if null presentation_names
+ orelse member (op =) presentation_names name
then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
else NONE
| print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
- if null presentation_stmt_names
+ if null presentation_names
then
let
val prefix_fragments' = prefix_fragments @ [name_fragment];
@@ -477,17 +477,19 @@
in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
(* serialization *)
- val p_includes = if null presentation_stmt_names
- then map (fn (base, p) => print_module base [] p) includes else [];
+ val p_includes = if null presentation_names then map snd includes else [];
val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
+ fun write width NONE = writeln_pretty width
+ | write width (SOME p) = File.write p o string_of_pretty width;
in
- Code_Target.mk_serialization target
- (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
- (rpair [] o code_of_pretty) p destination
+ Code_Target.serialization write (rpair [] oo string_of_pretty) p
end;
end; (*local*)
+val serializer : Code_Target.serializer =
+ Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
+
val literals = let
fun char_scala c = if c = "'" then "\\'"
else if c = "\"" then "\\\""
@@ -503,8 +505,8 @@
literal_char = Library.enclose "'" "'" o char_scala,
literal_string = quote o translate_string char_scala,
literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
- literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
- literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
+ literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
+ literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
infix_cons = (6, "::")
@@ -513,18 +515,14 @@
(** Isar setup **)
-fun isar_serializer _ =
- Code_Target.parse_args (Scan.succeed ())
- #> (fn () => serialize_scala);
-
val setup =
Code_Target.add_target
- (target, { serializer = isar_serializer, literals = literals,
+ (target, { serializer = serializer, literals = literals,
check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
make_command = fn scala_home => fn _ =>
"export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " ROOT.scala" } })
- #> Code_Target.add_syntax_tyco target "fun"
+ #> Code_Target.add_tyco_syntax target "fun"
(SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ BR ty1 (*product type vs. tupled arguments!*),
--- a/src/Tools/Code/code_target.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/Tools/Code/code_target.ML Wed Sep 01 13:45:58 2010 +0200
@@ -1,7 +1,7 @@
(* Title: Tools/Code/code_target.ML
Author: Florian Haftmann, TU Muenchen
-Serializer from intermediate language ("Thin-gol") to target languages.
+Generic infrastructure for target language data.
*)
signature CODE_TARGET =
@@ -9,6 +9,26 @@
val cert_tyco: theory -> string -> string
val read_tyco: theory -> string -> string
+ val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
+ -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
+ val produce_code_for: theory -> string -> int option -> string -> Token.T list
+ -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
+ val present_code_for: theory -> string -> int option -> string -> Token.T list
+ -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
+ val check_code_for: theory -> string -> bool -> Token.T list
+ -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
+
+ val export_code: theory -> string list
+ -> (((string * string) * Path.T option) * Token.T list) list -> unit
+ val produce_code: theory -> string list
+ -> string -> int option -> string -> Token.T list -> string * string option list
+ val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
+ -> string -> int option -> string -> Token.T list -> string
+ val check_code: theory -> string list
+ -> ((string * bool) * Token.T list) list -> unit
+
+ val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
+
type serializer
type literals = Code_Printer.literals
val add_target: string * { serializer: serializer, literals: literals,
@@ -18,34 +38,21 @@
(string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
-> theory -> theory
val assert_target: theory -> string -> string
-
- type destination
+ val the_literals: theory -> string -> literals
type serialization
val parse_args: 'a parser -> Token.T list -> 'a
- val stmt_names_of_destination: destination -> string list
- val mk_serialization: string -> (Path.T option -> 'a -> unit)
- -> ('a -> string * string option list)
+ val serialization: (int -> Path.T option -> 'a -> unit)
+ -> (int -> 'a -> string * string option list)
-> 'a -> serialization
- val serialize: theory -> string -> int option -> string option -> Token.T list
- -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
- val serialize_custom: theory -> string * serializer -> string option
- -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
- val the_literals: theory -> string -> literals
- val export: serialization -> unit
- val file: Path.T -> serialization -> unit
- val string: string list -> serialization -> string
- val code_of: theory -> string -> int option -> string
- -> string list -> (Code_Thingol.naming -> string list) -> string
val set_default_code_width: int -> theory -> theory
- val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
val allow_abort: string -> theory -> theory
type tyco_syntax = Code_Printer.tyco_syntax
type const_syntax = Code_Printer.const_syntax
- val add_syntax_class: string -> class -> string option -> theory -> theory
- val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
- val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
- val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
+ val add_class_syntax: string -> class -> string option -> theory -> theory
+ val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
+ val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
+ val add_const_syntax: string -> string -> const_syntax option -> theory -> theory
val add_reserved: string -> string -> theory -> theory
val add_include: string -> string * (string * string list) option -> theory -> theory
end;
@@ -60,90 +67,91 @@
type const_syntax = Code_Printer.const_syntax;
-(** basics **)
-
-datatype destination = Export | File of Path.T | String of string list;
-type serialization = destination -> (string * string option list) option;
+(** abstract nonsense **)
-fun export f = (f Export; ());
-fun file p f = (f (File p); ());
-fun string stmts f = fst (the (f (String stmts)));
+datatype destination = Export of Path.T option | Produce | Present of string list;
+type serialization = int -> destination -> (string * string option list) option;
-fun stmt_names_of_destination (String stmts) = stmts
+fun stmt_names_of_destination (Present stmt_names) = stmt_names
| stmt_names_of_destination _ = [];
-fun mk_serialization target output _ code Export = (output NONE code ; NONE)
- | mk_serialization target output _ code (File file) = (output (SOME file) code; NONE)
- | mk_serialization target _ string code (String _) = SOME (string code);
+fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
+ | serialization _ string content width Produce = SOME (string width content)
+ | serialization _ string content width (Present _) = SOME (string width content);
+
+fun export some_path f = (f (Export some_path); ());
+fun produce f = the (f Produce);
+fun present stmt_names f = fst (the (f (Present stmt_names)));
(** theory data **)
-datatype name_syntax_table = NameSyntaxTable of {
+datatype symbol_syntax_data = Symbol_Syntax_Data of {
class: string Symtab.table,
instance: unit Symreltab.table,
tyco: Code_Printer.tyco_syntax Symtab.table,
const: Code_Printer.const_syntax Symtab.table
};
-fun mk_name_syntax_table ((class, instance), (tyco, const)) =
- NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const };
-fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) =
- mk_name_syntax_table (f ((class, instance), (tyco, const)));
-fun merge_name_syntax_table (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 },
- NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
- mk_name_syntax_table (
+fun make_symbol_syntax_data ((class, instance), (tyco, const)) =
+ Symbol_Syntax_Data { class = class, instance = instance, tyco = tyco, const = const };
+fun map_symbol_syntax_data f (Symbol_Syntax_Data { class, instance, tyco, const }) =
+ make_symbol_syntax_data (f ((class, instance), (tyco, const)));
+fun merge_symbol_syntax_data
+ (Symbol_Syntax_Data { class = class1, instance = instance1, tyco = tyco1, const = const1 },
+ Symbol_Syntax_Data { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
+ make_symbol_syntax_data (
(Symtab.join (K snd) (class1, class2),
Symreltab.join (K snd) (instance1, instance2)),
(Symtab.join (K snd) (tyco1, tyco2),
Symtab.join (K snd) (const1, const2))
);
-type serializer =
- string option (*module name*)
- -> Token.T list (*arguments*)
- -> (string -> string) (*labelled_name*)
- -> string list (*reserved symbols*)
- -> (string * Pretty.T) list (*includes*)
- -> (string -> string option) (*module aliasses*)
- -> (string -> string option) (*class syntax*)
- -> (string -> Code_Printer.tyco_syntax option)
- -> (string -> Code_Printer.activated_const_syntax option)
- -> ((Pretty.T -> string) * (Pretty.T -> unit))
- -> Code_Thingol.program
- -> (string list * string list) (*selected statements*)
+type serializer = Token.T list (*arguments*) -> {
+ labelled_name: string -> string,
+ reserved_syms: string list,
+ includes: (string * Pretty.T) list,
+ module_alias: string -> string option,
+ class_syntax: string -> string option,
+ tyco_syntax: string -> Code_Printer.tyco_syntax option,
+ const_syntax: string -> Code_Printer.activated_const_syntax option,
+ program: Code_Thingol.program,
+ names: string list,
+ presentation_names: string list }
-> serialization;
-datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
+datatype description = Fundamental of { serializer: serializer,
+ literals: literals,
check: { env_var: string, make_destination: Path.T -> Path.T,
make_command: string -> string -> string } }
- | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
+ | Extension of string *
+ (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
datatype target = Target of {
serial: serial,
description: description,
reserved: string list,
includes: (Pretty.T * string list) Symtab.table,
- name_syntax_table: name_syntax_table,
- module_alias: string Symtab.table
+ module_alias: string Symtab.table,
+ symbol_syntax: symbol_syntax_data
};
-fun make_target ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))) =
+fun make_target ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))) =
Target { serial = serial, description = description, reserved = reserved,
- includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
-fun map_target f ( Target { serial, description, reserved, includes, name_syntax_table, module_alias } ) =
- make_target (f ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))));
+ includes = includes, module_alias = module_alias, symbol_syntax = symbol_syntax };
+fun map_target f ( Target { serial, description, reserved, includes, module_alias, symbol_syntax } ) =
+ make_target (f ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))));
fun merge_target strict target (Target { serial = serial1, description = description,
reserved = reserved1, includes = includes1,
- name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
+ module_alias = module_alias1, symbol_syntax = symbol_syntax1 },
Target { serial = serial2, description = _,
reserved = reserved2, includes = includes2,
- name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
+ module_alias = module_alias2, symbol_syntax = symbol_syntax2 }) =
if serial1 = serial2 orelse not strict then
make_target ((serial1, description),
((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)),
- (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
- Symtab.join (K snd) (module_alias1, module_alias2))
+ (Symtab.join (K snd) (module_alias1, module_alias2),
+ merge_symbol_syntax_data (symbol_syntax1, symbol_syntax2))
))
else
error ("Incompatible targets: " ^ quote target);
@@ -151,8 +159,8 @@
fun the_description (Target { description, ... }) = description;
fun the_reserved (Target { reserved, ... }) = reserved;
fun the_includes (Target { includes, ... }) = includes;
-fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
fun the_module_alias (Target { module_alias , ... }) = module_alias;
+fun the_symbol_syntax (Target { symbol_syntax = Symbol_Syntax_Data x, ... }) = x;
structure Targets = Theory_Data
(
@@ -190,8 +198,8 @@
thy
|> (Targets.map o apfst o apfst o Symtab.update)
(target, make_target ((serial (), seri), (([], Symtab.empty),
- (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
- Symtab.empty))))
+ (Symtab.empty, make_symbol_syntax_data ((Symtab.empty, Symreltab.empty),
+ (Symtab.empty, Symtab.empty))))))
end;
fun add_target (target, seri) = put_target (target, Fundamental seri);
@@ -210,10 +218,10 @@
map_target_data target o apsnd o apfst o apfst;
fun map_includes target =
map_target_data target o apsnd o apfst o apsnd;
-fun map_name_syntax target =
- map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
fun map_module_alias target =
- map_target_data target o apsnd o apsnd o apsnd;
+ map_target_data target o apsnd o apsnd o apfst;
+fun map_symbol_syntax target =
+ map_target_data target o apsnd o apsnd o apsnd o map_symbol_syntax_data;
fun set_default_code_width k = (Targets.map o apsnd) (K k);
@@ -236,6 +244,23 @@
local
+fun activate_target_for thy target naming program =
+ let
+ val ((targets, abortable), default_width) = Targets.get thy;
+ fun collapse_hierarchy target =
+ let
+ val data = case Symtab.lookup targets target
+ of SOME data => data
+ | NONE => error ("Unknown code target language: " ^ quote target);
+ in case the_description data
+ of Fundamental _ => (I, data)
+ | Extension (super, modify) => let
+ val (modify', data') = collapse_hierarchy super
+ in (modify' #> modify naming, merge_target false target (data', data)) end
+ end;
+ val (modify, data) = collapse_hierarchy target;
+ in (default_width, abortable, data, modify program) end;
+
fun activate_syntax lookup_name src_tab = Symtab.empty
|> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
of SOME name => (SOME name,
@@ -253,55 +278,66 @@
| NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
|>> map_filter I;
-fun invoke_serializer thy abortable serializer literals reserved abs_includes
- module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) =
+fun activate_symbol_syntax thy literals naming
+ class_syntax instance_syntax tyco_syntax const_syntax =
let
- val (names_class, class') =
- activate_syntax (Code_Thingol.lookup_class naming) class;
+ val (names_class, class_syntax') =
+ activate_syntax (Code_Thingol.lookup_class naming) class_syntax;
val names_inst = map_filter (Code_Thingol.lookup_instance naming)
- (Symreltab.keys instance);
- val (names_tyco, tyco') =
- activate_syntax (Code_Thingol.lookup_tyco naming) tyco;
- val (names_const, (const', _)) =
- activate_const_syntax thy literals const naming;
- val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
+ (Symreltab.keys instance_syntax);
+ val (names_tyco, tyco_syntax') =
+ activate_syntax (Code_Thingol.lookup_tyco naming) tyco_syntax;
+ val (names_const, (const_syntax', _)) =
+ activate_const_syntax thy literals const_syntax naming;
+ in
+ (names_class @ names_inst @ names_tyco @ names_const,
+ (class_syntax', tyco_syntax', const_syntax'))
+ end;
+
+fun project_program thy abortable names_hidden names1 program2 =
+ let
val names2 = subtract (op =) names_hidden names1;
val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
- val names_all = Graph.all_succs program3 names2;
- val includes = abs_includes names_all;
- val program4 = Graph.subgraph (member (op =) names_all) program3;
+ val names4 = Graph.all_succs program3 names2;
val empty_funs = filter_out (member (op =) abortable)
(Code_Thingol.empty_funs program3);
val _ = if null empty_funs then () else error ("No code equations for "
^ commas (map (Sign.extern_const thy) empty_funs));
+ val program4 = Graph.subgraph (member (op =) names4) program3;
+ in (names4, program4) end;
+
+fun invoke_serializer thy abortable serializer literals reserved abs_includes
+ module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
+ module_name args naming proto_program (names, presentation_names) =
+ let
+ val (names_hidden, (class_syntax, tyco_syntax, const_syntax)) =
+ activate_symbol_syntax thy literals naming
+ proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax;
+ val (names_all, program) = project_program thy abortable names_hidden names proto_program;
+ val includes = abs_includes names_all;
in
- serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes
- (if is_some module_name then K module_name else Symtab.lookup module_alias)
- (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
- (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
- program4 (names1, presentation_names)
+ serializer args {
+ labelled_name = Code_Thingol.labelled_name thy proto_program,
+ reserved_syms = reserved,
+ includes = includes,
+ module_alias = if module_name = "" then Symtab.lookup module_alias else K (SOME module_name),
+ class_syntax = Symtab.lookup class_syntax,
+ tyco_syntax = Symtab.lookup tyco_syntax,
+ const_syntax = Symtab.lookup const_syntax,
+ program = program,
+ names = names,
+ presentation_names = presentation_names }
end;
-fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
+fun mount_serializer thy target some_width raw_module_name args naming proto_program names destination =
let
- val ((targets, abortable), default_width) = Targets.get thy;
- fun collapse_hierarchy target =
- let
- val data = case Symtab.lookup targets target
- of SOME data => data
- | NONE => error ("Unknown code target language: " ^ quote target);
- in case the_description data
- of Fundamental _ => (I, data)
- | Extension (super, modify) => let
- val (modify', data') = collapse_hierarchy super
- in (modify' #> modify naming, merge_target false target (data', data)) end
- end;
- val (modify, data) = collapse_hierarchy target;
- val serializer = the_default (case the_description data
- of Fundamental seri => #serializer seri) alt_serializer;
+ val (default_width, abortable, data, program) =
+ activate_target_for thy target naming proto_program;
+ val serializer = case the_description data
+ of Fundamental seri => #serializer seri;
val presentation_names = stmt_names_of_destination destination;
val module_name = if null presentation_names
- then raw_module_name else SOME "Code";
+ then raw_module_name else "Code";
val reserved = the_reserved data;
fun select_include names_all (name, (content, cs)) =
if null cs then SOME (name, content)
@@ -312,30 +348,40 @@
fun includes names_all = map_filter (select_include names_all)
((Symtab.dest o the_includes) data);
val module_alias = the_module_alias data
- val { class, instance, tyco, const } = the_name_syntax data;
+ val { class, instance, tyco, const } = the_symbol_syntax data;
val literals = the_literals thy target;
val width = the_default default_width some_width;
in
invoke_serializer thy abortable serializer literals reserved
- includes module_alias class instance tyco const module_name width args
- naming (modify program) (names, presentation_names) destination
+ includes module_alias class instance tyco const module_name args
+ naming program (names, presentation_names) width destination
end;
+fun assert_module_name "" = error ("Empty module name not allowed.")
+ | assert_module_name module_name = module_name;
+
in
-fun serialize thy = mount_serializer thy NONE;
+fun export_code_for thy some_path target some_width some_module_name args naming program names =
+ export some_path (mount_serializer thy target some_width some_module_name args naming program names);
+
+fun produce_code_for thy target some_width module_name args naming program names =
+ produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
-fun check thy names_cs naming program target strict args =
+fun present_code_for thy target some_width module_name args naming program (names, selects) =
+ present selects (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
+
+fun check_code_for thy target strict args naming program names_cs =
let
- val module_name = "Code_Test";
+ val module_name = "Code";
val { env_var, make_destination, make_command } =
(#check o the_fundamental thy) target;
val env_param = getenv env_var;
fun ext_check env_param p =
let
val destination = make_destination p;
- val _ = file destination (serialize thy target (SOME 80)
- (SOME module_name) args naming program names_cs);
+ val _ = export (SOME destination) (mount_serializer thy target (SOME 80)
+ module_name args naming program names_cs);
val cmd = make_command env_param module_name;
in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
then error ("Code check failed for " ^ target ^ ": " ^ cmd)
@@ -348,24 +394,9 @@
else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
end;
-fun serialize_custom thy (target_name, seri) module_name naming program names =
- mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String [])
- |> the;
-
end; (* local *)
-(* code presentation *)
-
-fun code_of thy target some_width module_name cs names_stmt =
- let
- val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
- in
- string (names_stmt naming)
- (serialize thy target some_width (SOME module_name) [] naming program names_cs)
- end;
-
-
(* code generation *)
fun transitivly_non_empty_funs thy naming program =
@@ -383,22 +414,35 @@
if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
in union (op =) cs3 cs1 end;
+fun prep_destination "" = NONE
+ | prep_destination "-" = NONE
+ | prep_destination s = SOME (Path.explode s);
+
fun export_code thy cs seris =
let
val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
- fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export
- else file (Path.explode dest);
- val _ = map (fn (((target, module), dest), args) =>
- (mk_seri_dest dest (serialize thy target NONE module args naming program names_cs))) seris;
+ val _ = map (fn (((target, module_name), some_path), args) =>
+ export_code_for thy some_path target NONE module_name args naming program names_cs) seris;
in () end;
-fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
+fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs)
+ ((map o apfst o apsnd) prep_destination seris);
+
+fun produce_code thy cs target some_width some_module_name args =
+ let
+ val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
+ in produce_code_for thy target some_width some_module_name args naming program names_cs end;
+
+fun present_code thy cs names_stmt target some_width some_module_name args =
+ let
+ val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
+ in present_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end;
fun check_code thy cs seris =
let
val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
- val _ = map (fn ((target, strict), args) => check thy names_cs naming program
- target strict args) seris;
+ val _ = map (fn ((target, strict), args) =>
+ check_code_for thy target strict args naming program names_cs) seris;
in () end;
fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
@@ -435,21 +479,21 @@
val change = case some_raw_syn
of SOME raw_syn => upd (x, prep_syn thy x raw_syn)
| NONE => del x;
- in (map_name_syntax target o mapp) change thy end;
+ in (map_symbol_syntax target o mapp) change thy end;
-fun gen_add_syntax_class prep_class =
+fun gen_add_class_syntax prep_class =
gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class ((K o K) I);
-fun gen_add_syntax_inst prep_inst =
+fun gen_add_instance_syntax prep_inst =
gen_add_syntax (apfst o apsnd, Symreltab.update, Symreltab.delete_safe) prep_inst ((K o K) I);
-fun gen_add_syntax_tyco prep_tyco =
+fun gen_add_tyco_syntax prep_tyco =
gen_add_syntax (apsnd o apfst, Symtab.update, Symtab.delete_safe) prep_tyco
(fn thy => fn tyco => fn syn => if fst syn <> Sign.arity_number thy tyco
then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
else syn);
-fun gen_add_syntax_const prep_const =
+fun gen_add_const_syntax prep_const =
gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const
(fn thy => fn c => fn syn =>
if Code_Printer.requires_args syn > Code.args_number thy c
@@ -478,15 +522,17 @@
val add_include = gen_add_include (K I);
val add_include_cmd = gen_add_include Code.read_const;
-fun add_module_alias target (thyname, modlname) =
- let
- val xs = Long_Name.explode modlname;
- val xs' = map (Name.desymbolize true) xs;
- in if xs' = xs
- then map_module_alias target (Symtab.update (thyname, modlname))
- else error ("Invalid module name: " ^ quote modlname ^ "\n"
- ^ "perhaps try " ^ quote (Long_Name.implode xs'))
- end;
+fun add_module_alias target (thyname, "") =
+ map_module_alias target (Symtab.delete thyname)
+ | add_module_alias target (thyname, modlname) =
+ let
+ val xs = Long_Name.explode modlname;
+ val xs' = map (Name.desymbolize true) xs;
+ in if xs' = xs
+ then map_module_alias target (Symtab.update (thyname, modlname))
+ else error ("Invalid module name: " ^ quote modlname ^ "\n"
+ ^ "perhaps try " ^ quote (Long_Name.implode xs'))
+ end;
fun gen_allow_abort prep_const raw_c thy =
let
@@ -513,18 +559,18 @@
in
-val add_syntax_class = gen_add_syntax_class cert_class;
-val add_syntax_inst = gen_add_syntax_inst cert_inst;
-val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
-val add_syntax_const = gen_add_syntax_const (K I);
+val add_class_syntax = gen_add_class_syntax cert_class;
+val add_instance_syntax = gen_add_instance_syntax cert_inst;
+val add_tyco_syntax = gen_add_tyco_syntax cert_tyco;
+val add_const_syntax = gen_add_const_syntax (K I);
val allow_abort = gen_allow_abort (K I);
val add_reserved = add_reserved;
val add_include = add_include;
-val add_syntax_class_cmd = gen_add_syntax_class read_class;
-val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
-val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
-val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
+val add_class_syntax_cmd = gen_add_class_syntax read_class;
+val add_instance_syntax_cmd = gen_add_instance_syntax read_inst;
+val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco;
+val add_const_syntax_cmd = gen_add_const_syntax Code.read_const;
val allow_abort_cmd = gen_allow_abort Code.read_const;
fun parse_args f args =
@@ -545,7 +591,7 @@
-- ((Parse.$$$ "?" |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP))
>> (fn seris => check_code_cmd raw_cs seris)
|| Scan.repeat (Parse.$$$ inK |-- Parse.name
- -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
+ -- Scan.optional (Parse.$$$ module_nameK |-- Parse.name) ""
-- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
-- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
@@ -554,23 +600,23 @@
val _ =
Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
process_multi_syntax Parse.xname (Scan.option Parse.string)
- add_syntax_class_cmd);
+ add_class_syntax_cmd);
val _ =
Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
(Scan.option (Parse.minus >> K ()))
- add_syntax_inst_cmd);
+ add_instance_syntax_cmd);
val _ =
Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
- add_syntax_tyco_cmd);
+ add_tyco_syntax_cmd);
val _ =
Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
- add_syntax_const_cmd);
+ add_const_syntax_cmd);
val _ =
Outer_Syntax.command "code_reserved" "declare words as reserved for target language"
--- a/src/Tools/Code/lib/Tools/codegen Tue Aug 31 23:46:49 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen Wed Sep 01 13:45:58 2010 +0200
@@ -53,13 +53,13 @@
if [ "$QUICK_AND_DIRTY" -eq 1 ]
then
- QND_CMD="set"
+ QND_FLAG="true"
else
- QND_CMD="reset"
+ QND_FLAG="false"
fi
CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (Thy_Info.get_theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
-FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
+FULL_CMD="quick_and_dirty := QND_FLAG; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
"$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1
--- a/src/Tools/nbe.ML Tue Aug 31 23:46:49 2010 +0200
+++ b/src/Tools/nbe.ML Wed Sep 01 13:45:58 2010 +0200
@@ -388,6 +388,7 @@
in
s
|> traced (fn s => "\n--- code to be evaluated:\n" ^ s)
+ |> pair ""
|> ML_Context.evaluate ctxt (!trace) univs_cookie
|> (fn f => f deps_vals)
|> (fn univs => cs ~~ univs)