--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 31 18:38:30 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Sep 01 07:53:31 2010 +0200
@@ -447,7 +447,7 @@
\label{relevance-filter}
\begin{enum}
-\opdefault{relevance\_thresholds}{int\_pair}{45~90}
+\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 18:38:30 2010 +0200
+++ b/doc-src/more_antiquote.ML Wed Sep 01 07:53:31 2010 +0200
@@ -124,13 +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)
- |> fst
+ target some_width "Example" []
|> typewriter
end);
--- a/etc/isar-keywords.el Tue Aug 31 18:38:30 2010 +0200
+++ b/etc/isar-keywords.el Wed Sep 01 07:53:31 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/HOL.thy Tue Aug 31 18:38:30 2010 +0200
+++ b/src/HOL/HOL.thy Wed Sep 01 07:53:31 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/IsaMakefile Tue Aug 31 18:38:30 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Sep 01 07:53:31 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 \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 31 18:38:30 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Sep 01 07:53:31 2010 +0200
@@ -6,10 +6,15 @@
struct
val relevance_filter_args =
- [("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
+ [("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),
- ("theory_bonus", Sledgehammer_Fact_Filter.theory_bonus),
+ ("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),
--- a/src/HOL/Tools/Function/function_core.ML Tue Aug 31 18:38:30 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Wed Sep 01 07:53:31 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/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 31 18:38:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Sep 01 07:53:31 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,10 +13,14 @@
only: bool}
val trace : 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 theory_bonus : 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
@@ -44,7 +48,7 @@
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,
@@ -77,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
@@ -94,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
@@ -113,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)
+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"
@@ -133,12 +150,12 @@
(* 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)
@@ -149,38 +166,40 @@
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 =>
@@ -190,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
@@ -227,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
@@ -249,19 +269,38 @@
(**** 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 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
@@ -269,24 +308,29 @@
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)
-fun rel_weight const_tab =
- generic_weight (!abs_rel_weight) 0.0 rel_log I const_tab
-fun irrel_weight const_tab =
- generic_weight (!abs_irrel_weight) (!skolem_irrel_weight) irrel_log swap
- const_tab
+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 *)
-val theory_bonus = Unsynchronized.ref 0.1
+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 Theory = !theory_bonus
+ | 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
@@ -297,10 +341,11 @@
| (rel, irrel) =>
let
val irrel = irrel |> filter_out (pconst_mem swap rel)
- val rel_weight = 0.0 |> fold (curry (op +) o rel_weight const_tab) 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_weight const_tab) irrel
+ |> 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
@@ -311,14 +356,15 @@
([], _) => 0.0
| (rel, irrel) =>
let
-val _ = tracing (PolyML.makestring ("REL: ", rel))
-val _ = tracing (PolyML.makestring ("IRREL: ", irrel))(*###*)
val irrel = irrel |> filter_out (pconst_mem swap rel)
- val rel_weight = 0.0 |> fold (curry (op +) o rel_weight const_tab) rel
- val irrel_weight =
+ 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_weight const_tab) irrel
- val res = rel_weight / (rel_weight + irrel_weight)
+ |> 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
*)
@@ -332,10 +378,10 @@
| consts => SOME ((axiom, consts), NONE)
type annotated_thm =
- (((unit -> string) * locality) * thm) * (string * pattern list) list
+ (((unit -> string) * locality) * thm) * (string * ptype) list
(* FUDGE *)
-val max_imperfect = Unsynchronized.ref 10.0
+val max_imperfect = Unsynchronized.ref 11.5
val max_imperfect_exp = Unsynchronized.ref 1.0
fun take_most_relevant max_relevant remaining_max
@@ -380,8 +426,7 @@
fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty
val goal_const_tab =
pconsts_in_terms thy false (SOME false) goal_ts
- |> fold (if_empty_replace_with_locality thy axioms)
- [Chained, Local, Theory]
+ |> 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
fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
@@ -448,7 +493,7 @@
| NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
(* FIXME: experiment
val name = fst (fst (fst ax)) ()
-val _ = if String.isSubstring "abs_of_neg" name then
+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
()
@@ -493,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 =
@@ -625,14 +670,26 @@
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 =
@@ -655,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]
@@ -688,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)
@@ -722,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 18:38:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 01 07:53:31 2010 +0200
@@ -67,7 +67,7 @@
("verbose", "false"),
("overlord", "false"),
("explicit_apply", "false"),
- ("relevance_thresholds", "45 90"),
+ ("relevance_thresholds", "45 85"),
("max_relevant", "smart"),
("theory_relevant", "smart"),
("isar_proof", "false"),
--- a/src/HOL/Tools/list_code.ML Tue Aug 31 18:38:30 2010 +0200
+++ b/src/HOL/Tools/list_code.ML Wed Sep 01 07:53:31 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 18:38:30 2010 +0200
+++ b/src/HOL/Tools/numeral.ML Wed Sep 01 07:53:31 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 18:38:30 2010 +0200
+++ b/src/HOL/Tools/string_code.ML Wed Sep 01 07:53:31 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 07:53:31 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 18:38:30 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Wed Sep 01 07:53:31 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 18:38:30 2010 +0200
+++ b/src/Pure/ML/ml_context.ML Wed Sep 01 07:53:31 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 18:38:30 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Wed Sep 01 07:53:31 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 18:38:30 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Wed Sep 01 07:53:31 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 program
- (stmt_names, presentation_stmt_names) =
+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,13 +368,13 @@
);
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;
+ 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;
@@ -458,18 +458,18 @@
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 =
+val isar_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 module_name string_classes));
+ serialize_haskell module_prefix string_classes));
val _ =
Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
@@ -483,7 +483,7 @@
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 18:38:30 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Wed Sep 01 07:53:31 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 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,36 +925,28 @@
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.serialization write (fn width => (rpair stmt_names' o string_of_pretty width)) p
+ Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p
end;
end; (*local*)
-(** for instrumentalization **)
-
-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);
-
-
(** Isar setup **)
-fun isar_serializer_sml module_name =
+val isar_serializer_sml =
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));
+ print_sml_module print_sml_stmt with_signatures));
-fun isar_serializer_ocaml module_name =
+val isar_serializer_ocaml =
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));
+ print_ocaml_module print_ocaml_stmt with_signatures));
val setup =
Code_Target.add_target
@@ -971,13 +957,13 @@
(target_OCaml, { serializer = isar_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 18:38:30 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Wed Sep 01 07:53:31 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
@@ -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 18:38:30 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Wed Sep 01 07:53:31 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
- program (stmt_names, presentation_stmt_names) =
+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,7 +477,7 @@
in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
(* serialization *)
- val p_includes = if null presentation_stmt_names
+ val p_includes = if null presentation_names
then map (fn (base, p) => print_module base [] p) includes else [];
val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
fun write width NONE = writeln_pretty width
@@ -513,9 +513,8 @@
(** Isar setup **)
-fun isar_serializer _ =
- Code_Target.parse_args (Scan.succeed ())
- #> (fn () => serialize_scala);
+val isar_serializer =
+ Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
val setup =
Code_Target.add_target
@@ -524,7 +523,7 @@
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 18:38:30 2010 +0200
+++ b/src/Tools/Code/code_target.ML Wed Sep 01 07:53:31 2010 +0200
@@ -9,17 +9,21 @@
val cert_tyco: theory -> string -> string
val read_tyco: theory -> string -> string
- val export_code_for: theory -> Path.T option -> string -> int option -> string option -> Token.T list
+ 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 option -> Token.T list
- -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string * string option list
+ 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 option) * Path.T option) * Token.T list) list -> unit
- val produce_code: theory -> string list -> (Code_Thingol.naming -> string list)
- -> string -> int option -> string option -> Token.T list -> string * string option 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
@@ -39,22 +43,16 @@
val parse_args: 'a parser -> Token.T list -> 'a
val serialization: (int -> Path.T option -> 'a -> unit)
-> (int -> 'a -> string * string option list)
- -> 'a -> int -> serialization
+ -> 'a -> serialization
val set_default_code_width: int -> theory -> theory
- (*FIXME drop asap*)
- val code_of: theory -> string -> int option -> string
- -> string list -> (Code_Thingol.naming -> string list) -> string * string option list
- val serialize_custom: theory -> string * serializer -> string option
- -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
-
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;
@@ -69,57 +67,57 @@
type const_syntax = Code_Printer.const_syntax;
-(** basics **)
+(** abstract nonsense **)
-datatype destination = File of Path.T option | String of string list;
-type serialization = destination -> (string * string option list) option;
+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 stmt_names) = stmt_names
+fun stmt_names_of_destination (Present stmt_names) = stmt_names
| stmt_names_of_destination _ = [];
-fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
- | serialization _ string pretty width (String _) = SOME (string width pretty);
+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 file some_path f = (f (File some_path); ());
-fun string stmt_names f = the (f (String stmt_names));
+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)
- -> Code_Thingol.program
- -> (string list * string list) (*selected statements*)
- -> int
+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,
@@ -134,26 +132,26 @@
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);
@@ -161,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
(
@@ -200,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);
@@ -220,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);
@@ -246,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,
@@ -263,54 +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 args naming program2 (names1, presentation_names) width =
+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')
- program4 (names1, presentation_names) width
+ 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)
@@ -321,36 +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 args
- naming (modify program) (names, presentation_names) width destination
+ 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 export_code_for thy some_path target some_width some_module_name args naming program names =
- file some_path (serialize 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 produce_code_for thy target some_width some_module_name args naming program (names, selects) =
- string selects (serialize thy target some_width some_module_name args naming program names);
+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 (SOME 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)
@@ -363,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 =
@@ -412,10 +428,15 @@
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 names_stmt target some_width some_module_name args =
+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, names_stmt naming) end;
+ 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
@@ -458,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
@@ -501,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
@@ -536,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 =
@@ -568,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)));
@@ -577,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/nbe.ML Tue Aug 31 18:38:30 2010 +0200
+++ b/src/Tools/nbe.ML Wed Sep 01 07:53:31 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)