1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 31 18:38:30 2010 +0200
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Sep 01 07:53:31 2010 +0200
1.3 @@ -447,7 +447,7 @@
1.4 \label{relevance-filter}
1.5
1.6 \begin{enum}
1.7 -\opdefault{relevance\_thresholds}{int\_pair}{45~90}
1.8 +\opdefault{relevance\_thresholds}{int\_pair}{45~85}
1.9 Specifies the thresholds above which facts are considered relevant by the
1.10 relevance filter. The first threshold is used for the first iteration of the
1.11 relevance filter and the second threshold is used for the last iteration (if it
2.1 --- a/doc-src/more_antiquote.ML Tue Aug 31 18:38:30 2010 +0200
2.2 +++ b/doc-src/more_antiquote.ML Wed Sep 01 07:53:31 2010 +0200
2.3 @@ -124,13 +124,13 @@
2.4 in
2.5
2.6 val _ = Thy_Output.antiquotation "code_stmts"
2.7 - (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
2.8 - (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
2.9 + (parse_const_terms -- Scan.repeat parse_names
2.10 + -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
2.11 + (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
2.12 let val thy = ProofContext.theory_of ctxt in
2.13 - Code_Target.code_of thy
2.14 - target NONE "Example" (mk_cs thy)
2.15 + Code_Target.present_code thy (mk_cs thy)
2.16 (fn naming => maps (fn f => f thy naming) mk_stmtss)
2.17 - |> fst
2.18 + target some_width "Example" []
2.19 |> typewriter
2.20 end);
2.21
3.1 --- a/etc/isar-keywords.el Tue Aug 31 18:38:30 2010 +0200
3.2 +++ b/etc/isar-keywords.el Wed Sep 01 07:53:31 2010 +0200
3.3 @@ -245,6 +245,7 @@
3.4 "thus"
3.5 "thy_deps"
3.6 "translations"
3.7 + "try"
3.8 "txt"
3.9 "txt_raw"
3.10 "typ"
3.11 @@ -398,6 +399,7 @@
3.12 "thm"
3.13 "thm_deps"
3.14 "thy_deps"
3.15 + "try"
3.16 "typ"
3.17 "unused_thms"
3.18 "value"
4.1 --- a/src/HOL/HOL.thy Tue Aug 31 18:38:30 2010 +0200
4.2 +++ b/src/HOL/HOL.thy Wed Sep 01 07:53:31 2010 +0200
4.3 @@ -30,6 +30,7 @@
4.4 "~~/src/Tools/induct.ML"
4.5 ("~~/src/Tools/induct_tacs.ML")
4.6 ("Tools/recfun_codegen.ML")
4.7 + "Tools/try.ML"
4.8 begin
4.9
4.10 setup {* Intuitionistic.method_setup @{binding iprover} *}
5.1 --- a/src/HOL/IsaMakefile Tue Aug 31 18:38:30 2010 +0200
5.2 +++ b/src/HOL/IsaMakefile Wed Sep 01 07:53:31 2010 +0200
5.3 @@ -213,6 +213,7 @@
5.4 Tools/sat_funcs.ML \
5.5 Tools/sat_solver.ML \
5.6 Tools/split_rule.ML \
5.7 + Tools/try.ML \
5.8 Tools/typedef.ML \
5.9 Transitive_Closure.thy \
5.10 Typedef.thy \
6.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 31 18:38:30 2010 +0200
6.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Sep 01 07:53:31 2010 +0200
6.3 @@ -6,10 +6,15 @@
6.4 struct
6.5
6.6 val relevance_filter_args =
6.7 - [("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
6.8 + [("worse_irrel_freq", Sledgehammer_Fact_Filter.worse_irrel_freq),
6.9 + ("higher_order_irrel_weight",
6.10 + Sledgehammer_Fact_Filter.higher_order_irrel_weight),
6.11 + ("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
6.12 ("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight),
6.13 ("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight),
6.14 - ("theory_bonus", Sledgehammer_Fact_Filter.theory_bonus),
6.15 + ("intro_bonus", Sledgehammer_Fact_Filter.intro_bonus),
6.16 + ("elim_bonus", Sledgehammer_Fact_Filter.elim_bonus),
6.17 + ("simp_bonus", Sledgehammer_Fact_Filter.simp_bonus),
6.18 ("local_bonus", Sledgehammer_Fact_Filter.local_bonus),
6.19 ("chained_bonus", Sledgehammer_Fact_Filter.chained_bonus),
6.20 ("max_imperfect", Sledgehammer_Fact_Filter.max_imperfect),
7.1 --- a/src/HOL/Tools/Function/function_core.ML Tue Aug 31 18:38:30 2010 +0200
7.2 +++ b/src/HOL/Tools/Function/function_core.ML Wed Sep 01 07:53:31 2010 +0200
7.3 @@ -860,9 +860,9 @@
7.4 rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
7.5 THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
7.6 THEN (simp_default_tac (simpset_of ctxt) 1)
7.7 - THEN (etac not_acc_down 1)
7.8 - THEN ((etac R_cases)
7.9 - THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
7.10 + THEN TRY ((etac not_acc_down 1)
7.11 + THEN ((etac R_cases)
7.12 + THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1))
7.13 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
7.14 end
7.15 in
8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 31 18:38:30 2010 +0200
8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Sep 01 07:53:31 2010 +0200
8.3 @@ -5,7 +5,7 @@
8.4
8.5 signature SLEDGEHAMMER_FACT_FILTER =
8.6 sig
8.7 - datatype locality = General | Theory | Local | Chained
8.8 + datatype locality = General | Intro | Elim | Simp | Local | Chained
8.9
8.10 type relevance_override =
8.11 {add: Facts.ref list,
8.12 @@ -13,10 +13,14 @@
8.13 only: bool}
8.14
8.15 val trace : bool Unsynchronized.ref
8.16 + val worse_irrel_freq : real Unsynchronized.ref
8.17 + val higher_order_irrel_weight : real Unsynchronized.ref
8.18 val abs_rel_weight : real Unsynchronized.ref
8.19 val abs_irrel_weight : real Unsynchronized.ref
8.20 val skolem_irrel_weight : real Unsynchronized.ref
8.21 - val theory_bonus : real Unsynchronized.ref
8.22 + val intro_bonus : real Unsynchronized.ref
8.23 + val elim_bonus : real Unsynchronized.ref
8.24 + val simp_bonus : real Unsynchronized.ref
8.25 val local_bonus : real Unsynchronized.ref
8.26 val chained_bonus : real Unsynchronized.ref
8.27 val max_imperfect : real Unsynchronized.ref
8.28 @@ -44,7 +48,7 @@
8.29
8.30 val respect_no_atp = true
8.31
8.32 -datatype locality = General | Theory | Local | Chained
8.33 +datatype locality = General | Intro | Elim | Simp | Local | Chained
8.34
8.35 type relevance_override =
8.36 {add: Facts.ref list,
8.37 @@ -77,13 +81,22 @@
8.38
8.39 (*** constants with types ***)
8.40
8.41 +fun order_of_type (Type (@{type_name fun}, [T1, @{typ bool}])) =
8.42 + order_of_type T1 (* cheat: pretend sets are first-order *)
8.43 + | order_of_type (Type (@{type_name fun}, [T1, T2])) =
8.44 + Int.max (order_of_type T1 + 1, order_of_type T2)
8.45 + | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
8.46 + | order_of_type _ = 0
8.47 +
8.48 (* An abstraction of Isabelle types and first-order terms *)
8.49 datatype pattern = PVar | PApp of string * pattern list
8.50 +datatype ptype = PType of int * pattern list
8.51
8.52 fun string_for_pattern PVar = "_"
8.53 | string_for_pattern (PApp (s, ps)) =
8.54 if null ps then s else s ^ string_for_patterns ps
8.55 and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
8.56 +fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
8.57
8.58 (*Is the second type an instance of the first one?*)
8.59 fun match_pattern (PVar, _) = true
8.60 @@ -94,17 +107,18 @@
8.61 | match_patterns ([], _) = false
8.62 | match_patterns (p :: ps, q :: qs) =
8.63 match_pattern (p, q) andalso match_patterns (ps, qs)
8.64 +fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
8.65
8.66 (* Is there a unifiable constant? *)
8.67 fun pconst_mem f consts (s, ps) =
8.68 - exists (curry (match_patterns o f) ps)
8.69 + exists (curry (match_ptype o f) ps)
8.70 (map snd (filter (curry (op =) s o fst) consts))
8.71 fun pconst_hyper_mem f const_tab (s, ps) =
8.72 - exists (curry (match_patterns o f) ps) (these (Symtab.lookup const_tab s))
8.73 + exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
8.74
8.75 -fun ptype (Type (s, Ts)) = PApp (s, map ptype Ts)
8.76 - | ptype (TFree (s, _)) = PApp (s, [])
8.77 - | ptype (TVar _) = PVar
8.78 +fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
8.79 + | pattern_for_type (TFree (s, _)) = PApp (s, [])
8.80 + | pattern_for_type (TVar _) = PVar
8.81
8.82 fun pterm thy t =
8.83 case strip_comb t of
8.84 @@ -113,14 +127,17 @@
8.85 | (Var x, []) => PVar
8.86 | _ => PApp ("?", []) (* equivalence class of higher-order constructs *)
8.87 (* Pairs a constant with the list of its type instantiations. *)
8.88 -and pconst_args thy const (s, T) ts =
8.89 - (if const then map ptype (these (try (Sign.const_typargs thy) (s, T)))
8.90 +and ptype thy const x ts =
8.91 + (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
8.92 else []) @
8.93 (if term_patterns then map (pterm thy) ts else [])
8.94 -and pconst thy const (s, T) ts = (s, pconst_args thy const (s, T) ts)
8.95 +and pconst thy const (s, T) ts = (s, ptype thy const (s, T) ts)
8.96 +and rich_ptype thy const (s, T) ts =
8.97 + PType (order_of_type T, ptype thy const (s, T) ts)
8.98 +and rich_pconst thy const (s, T) ts = (s, rich_ptype thy const (s, T) ts)
8.99
8.100 -fun string_for_hyper_pconst (s, pss) =
8.101 - s ^ "{" ^ commas (map string_for_patterns pss) ^ "}"
8.102 +fun string_for_hyper_pconst (s, ps) =
8.103 + s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
8.104
8.105 val abs_name = "Sledgehammer.abs"
8.106 val skolem_prefix = "Sledgehammer.sko"
8.107 @@ -133,12 +150,12 @@
8.108
8.109 (* Add a pconstant to the table, but a [] entry means a standard
8.110 connective, which we ignore.*)
8.111 -fun add_pconst_to_table also_skolem (c, ps) =
8.112 +fun add_pconst_to_table also_skolem (c, p) =
8.113 if member (op =) boring_consts c orelse
8.114 (not also_skolem andalso String.isPrefix skolem_prefix c) then
8.115 I
8.116 else
8.117 - Symtab.map_default (c, [ps]) (insert (op =) ps)
8.118 + Symtab.map_default (c, [p]) (insert (op =) p)
8.119
8.120 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
8.121
8.122 @@ -149,38 +166,40 @@
8.123 each quantifiers that must necessarily be skolemized by the ATP, we
8.124 introduce a fresh constant to simulate the effect of Skolemization. *)
8.125 fun do_const const (s, T) ts =
8.126 - add_pconst_to_table also_skolems (pconst thy const (s, T) ts)
8.127 + add_pconst_to_table also_skolems (rich_pconst thy const (s, T) ts)
8.128 #> fold do_term ts
8.129 and do_term t =
8.130 case strip_comb t of
8.131 (Const x, ts) => do_const true x ts
8.132 | (Free x, ts) => do_const false x ts
8.133 - | (Abs (_, _, t'), ts) =>
8.134 - (null ts ? add_pconst_to_table true (abs_name, []))
8.135 + | (Abs (_, T, t'), ts) =>
8.136 + (null ts
8.137 + ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, [])))
8.138 #> fold do_term (t' :: ts)
8.139 | (_, ts) => fold do_term ts
8.140 - fun do_quantifier will_surely_be_skolemized body_t =
8.141 + fun do_quantifier will_surely_be_skolemized abs_T body_t =
8.142 do_formula pos body_t
8.143 #> (if also_skolems andalso will_surely_be_skolemized then
8.144 - add_pconst_to_table true (gensym skolem_prefix, [])
8.145 + add_pconst_to_table true
8.146 + (gensym skolem_prefix, PType (order_of_type abs_T, []))
8.147 else
8.148 I)
8.149 and do_term_or_formula T =
8.150 if is_formula_type T then do_formula NONE else do_term
8.151 and do_formula pos t =
8.152 case t of
8.153 - Const (@{const_name all}, _) $ Abs (_, _, body_t) =>
8.154 - do_quantifier (pos = SOME false) body_t
8.155 + Const (@{const_name all}, _) $ Abs (_, T, t') =>
8.156 + do_quantifier (pos = SOME false) T t'
8.157 | @{const "==>"} $ t1 $ t2 =>
8.158 do_formula (flip pos) t1 #> do_formula pos t2
8.159 | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
8.160 fold (do_term_or_formula T) [t1, t2]
8.161 | @{const Trueprop} $ t1 => do_formula pos t1
8.162 | @{const Not} $ t1 => do_formula (flip pos) t1
8.163 - | Const (@{const_name All}, _) $ Abs (_, _, body_t) =>
8.164 - do_quantifier (pos = SOME false) body_t
8.165 - | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
8.166 - do_quantifier (pos = SOME true) body_t
8.167 + | Const (@{const_name All}, _) $ Abs (_, T, t') =>
8.168 + do_quantifier (pos = SOME false) T t'
8.169 + | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
8.170 + do_quantifier (pos = SOME true) T t'
8.171 | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
8.172 | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
8.173 | @{const HOL.implies} $ t1 $ t2 =>
8.174 @@ -190,14 +209,14 @@
8.175 | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
8.176 $ t1 $ t2 $ t3 =>
8.177 do_formula NONE t1 #> fold (do_term_or_formula T) [t2, t3]
8.178 - | Const (@{const_name Ex1}, _) $ Abs (_, _, body_t) =>
8.179 - do_quantifier (is_some pos) body_t
8.180 - | Const (@{const_name Ball}, _) $ t1 $ Abs (_, _, body_t) =>
8.181 - do_quantifier (pos = SOME false)
8.182 - (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, body_t))
8.183 - | Const (@{const_name Bex}, _) $ t1 $ Abs (_, _, body_t) =>
8.184 - do_quantifier (pos = SOME true)
8.185 - (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, body_t))
8.186 + | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
8.187 + do_quantifier (is_some pos) T t'
8.188 + | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
8.189 + do_quantifier (pos = SOME false) T
8.190 + (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
8.191 + | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
8.192 + do_quantifier (pos = SOME true) T
8.193 + (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
8.194 | (t0 as Const (_, @{typ bool})) $ t1 =>
8.195 do_term t0 #> do_formula pos t1 (* theory constant *)
8.196 | _ => do_term t
8.197 @@ -227,16 +246,17 @@
8.198 | (PApp _, PVar) => GREATER
8.199 | (PApp q1, PApp q2) =>
8.200 prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
8.201 +fun ptype_ord (PType p, PType q) =
8.202 + prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
8.203
8.204 -structure CTtab =
8.205 - Table(type key = pattern list val ord = dict_ord pattern_ord)
8.206 +structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
8.207
8.208 fun count_axiom_consts theory_relevant thy =
8.209 let
8.210 fun do_const const (s, T) ts =
8.211 (* Two-dimensional table update. Constant maps to types maps to count. *)
8.212 - CTtab.map_default (pconst_args thy const (s, T) ts, 0) (Integer.add 1)
8.213 - |> Symtab.map_default (s, CTtab.empty)
8.214 + PType_Tab.map_default (rich_ptype thy const (s, T) ts, 0) (Integer.add 1)
8.215 + |> Symtab.map_default (s, PType_Tab.empty)
8.216 #> fold do_term ts
8.217 and do_term t =
8.218 case strip_comb t of
8.219 @@ -249,19 +269,38 @@
8.220
8.221 (**** Actual Filtering Code ****)
8.222
8.223 +fun pow_int x 0 = 1.0
8.224 + | pow_int x 1 = x
8.225 + | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
8.226 +
8.227 (*The frequency of a constant is the sum of those of all instances of its type.*)
8.228 fun pconst_freq match const_tab (c, ps) =
8.229 - CTtab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
8.230 - (the (Symtab.lookup const_tab c)) 0
8.231 + PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
8.232 + (the (Symtab.lookup const_tab c)) 0
8.233
8.234
8.235 (* A surprising number of theorems contain only a few significant constants.
8.236 These include all induction rules, and other general theorems. *)
8.237
8.238 (* "log" seems best in practice. A constant function of one ignores the constant
8.239 - frequencies. *)
8.240 -fun rel_log n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0)
8.241 -fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
8.242 + frequencies. Rare constants give more points if they are relevant than less
8.243 + rare ones. *)
8.244 +fun rel_weight_for order freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
8.245 +
8.246 +(* FUDGE *)
8.247 +val worse_irrel_freq = Unsynchronized.ref 100.0
8.248 +val higher_order_irrel_weight = Unsynchronized.ref 1.05
8.249 +
8.250 +(* Irrelevant constants are treated differently. We associate lower penalties to
8.251 + very rare constants and very common ones -- the former because they can't
8.252 + lead to the inclusion of too many new facts, and the latter because they are
8.253 + so common as to be of little interest. *)
8.254 +fun irrel_weight_for order freq =
8.255 + let val (k, x) = !worse_irrel_freq |> `Real.ceil in
8.256 + (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
8.257 + else rel_weight_for order freq / rel_weight_for order k)
8.258 + * pow_int (!higher_order_irrel_weight) (order - 1)
8.259 + end
8.260
8.261 (* FUDGE *)
8.262 val abs_rel_weight = Unsynchronized.ref 0.5
8.263 @@ -269,24 +308,29 @@
8.264 val skolem_irrel_weight = Unsynchronized.ref 0.75
8.265
8.266 (* Computes a constant's weight, as determined by its frequency. *)
8.267 -fun generic_weight abs_weight skolem_weight logx f const_tab (c as (s, _)) =
8.268 +fun generic_pconst_weight abs_weight skolem_weight weight_for f const_tab
8.269 + (c as (s, PType (m, _))) =
8.270 if s = abs_name then abs_weight
8.271 else if String.isPrefix skolem_prefix s then skolem_weight
8.272 - else logx (pconst_freq (match_patterns o f) const_tab c)
8.273 + else weight_for m (pconst_freq (match_ptype o f) const_tab c)
8.274
8.275 -fun rel_weight const_tab =
8.276 - generic_weight (!abs_rel_weight) 0.0 rel_log I const_tab
8.277 -fun irrel_weight const_tab =
8.278 - generic_weight (!abs_irrel_weight) (!skolem_irrel_weight) irrel_log swap
8.279 - const_tab
8.280 +fun rel_pconst_weight const_tab =
8.281 + generic_pconst_weight (!abs_rel_weight) 0.0 rel_weight_for I const_tab
8.282 +fun irrel_pconst_weight const_tab =
8.283 + generic_pconst_weight (!abs_irrel_weight) (!skolem_irrel_weight)
8.284 + irrel_weight_for swap const_tab
8.285
8.286 (* FUDGE *)
8.287 -val theory_bonus = Unsynchronized.ref 0.1
8.288 +val intro_bonus = Unsynchronized.ref 0.15
8.289 +val elim_bonus = Unsynchronized.ref 0.15
8.290 +val simp_bonus = Unsynchronized.ref 0.15
8.291 val local_bonus = Unsynchronized.ref 0.55
8.292 val chained_bonus = Unsynchronized.ref 1.5
8.293
8.294 fun locality_bonus General = 0.0
8.295 - | locality_bonus Theory = !theory_bonus
8.296 + | locality_bonus Intro = !intro_bonus
8.297 + | locality_bonus Elim = !elim_bonus
8.298 + | locality_bonus Simp = !simp_bonus
8.299 | locality_bonus Local = !local_bonus
8.300 | locality_bonus Chained = !chained_bonus
8.301
8.302 @@ -297,10 +341,11 @@
8.303 | (rel, irrel) =>
8.304 let
8.305 val irrel = irrel |> filter_out (pconst_mem swap rel)
8.306 - val rel_weight = 0.0 |> fold (curry (op +) o rel_weight const_tab) rel
8.307 + val rel_weight =
8.308 + 0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
8.309 val irrel_weight =
8.310 ~ (locality_bonus loc)
8.311 - |> fold (curry (op +) o irrel_weight const_tab) irrel
8.312 + |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
8.313 val res = rel_weight / (rel_weight + irrel_weight)
8.314 in if Real.isFinite res then res else 0.0 end
8.315
8.316 @@ -311,14 +356,15 @@
8.317 ([], _) => 0.0
8.318 | (rel, irrel) =>
8.319 let
8.320 -val _ = tracing (PolyML.makestring ("REL: ", rel))
8.321 -val _ = tracing (PolyML.makestring ("IRREL: ", irrel))(*###*)
8.322 val irrel = irrel |> filter_out (pconst_mem swap rel)
8.323 - val rel_weight = 0.0 |> fold (curry (op +) o rel_weight const_tab) rel
8.324 - val irrel_weight =
8.325 + val rels_weight =
8.326 + 0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
8.327 + val irrels_weight =
8.328 ~ (locality_bonus loc)
8.329 - |> fold (curry (op +) o irrel_weight const_tab) irrel
8.330 - val res = rel_weight / (rel_weight + irrel_weight)
8.331 + |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
8.332 +val _ = tracing (PolyML.makestring ("REL: ", map (`(rel_pconst_weight const_tab)) rel))
8.333 +val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight const_tab)) irrel))
8.334 + val res = rels_weight / (rels_weight + irrels_weight)
8.335 in if Real.isFinite res then res else 0.0 end
8.336 *)
8.337
8.338 @@ -332,10 +378,10 @@
8.339 | consts => SOME ((axiom, consts), NONE)
8.340
8.341 type annotated_thm =
8.342 - (((unit -> string) * locality) * thm) * (string * pattern list) list
8.343 + (((unit -> string) * locality) * thm) * (string * ptype) list
8.344
8.345 (* FUDGE *)
8.346 -val max_imperfect = Unsynchronized.ref 10.0
8.347 +val max_imperfect = Unsynchronized.ref 11.5
8.348 val max_imperfect_exp = Unsynchronized.ref 1.0
8.349
8.350 fun take_most_relevant max_relevant remaining_max
8.351 @@ -380,8 +426,7 @@
8.352 fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty
8.353 val goal_const_tab =
8.354 pconsts_in_terms thy false (SOME false) goal_ts
8.355 - |> fold (if_empty_replace_with_locality thy axioms)
8.356 - [Chained, Local, Theory]
8.357 + |> fold (if_empty_replace_with_locality thy axioms) [Chained, Local]
8.358 val add_thms = maps (ProofContext.get_fact ctxt) add
8.359 val del_thms = maps (ProofContext.get_fact ctxt) del
8.360 fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
8.361 @@ -448,7 +493,7 @@
8.362 | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
8.363 (* FIXME: experiment
8.364 val name = fst (fst (fst ax)) ()
8.365 -val _ = if String.isSubstring "abs_of_neg" name then
8.366 +val _ = if String.isSubstring "positive_minus" name orelse String.isSubstring "not_exp_le_zero" name then
8.367 tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight loc const_tab rel_const_tab axiom_consts))
8.368 else
8.369 ()
8.370 @@ -493,9 +538,9 @@
8.371 String.isSuffix "_def" a orelse String.isSuffix "_defs" a
8.372 end;
8.373
8.374 -fun make_fact_table xs =
8.375 - fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
8.376 -fun make_unique xs = Termtab.fold (cons o snd) (make_fact_table xs) []
8.377 +fun mk_fact_table f xs =
8.378 + fold (Termtab.update o `(prop_of o f)) xs Termtab.empty
8.379 +fun uniquify xs = Termtab.fold (cons o snd) (mk_fact_table snd xs) []
8.380
8.381 (* FIXME: put other record thms here, or declare as "no_atp" *)
8.382 val multi_base_blacklist =
8.383 @@ -625,14 +670,26 @@
8.384 is_that_fact thm
8.385 end
8.386
8.387 +fun clasimpset_rules_of ctxt =
8.388 + let
8.389 + val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> rep_cs
8.390 + val intros = safeIs @ hazIs
8.391 + val elims = map Classical.classical_rule (safeEs @ hazEs)
8.392 + val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
8.393 + in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
8.394 +
8.395 fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
8.396 let
8.397 val thy = ProofContext.theory_of ctxt
8.398 - val thy_prefix = Context.theory_name thy ^ Long_Name.separator
8.399 val global_facts = PureThy.facts_of thy
8.400 val local_facts = ProofContext.facts_of ctxt
8.401 val named_locals = local_facts |> Facts.dest_static []
8.402 val is_chained = member Thm.eq_thm chained_ths
8.403 + val (intros, elims, simps) =
8.404 + if exists (curry (op <) 0.0) [!intro_bonus, !elim_bonus, !simp_bonus] then
8.405 + clasimpset_rules_of ctxt
8.406 + else
8.407 + (Termtab.empty, Termtab.empty, Termtab.empty)
8.408 (* Unnamed nonchained formulas with schematic variables are omitted, because
8.409 they are rejected by the backticks (`...`) parser for some reason. *)
8.410 fun is_good_unnamed_local th =
8.411 @@ -655,10 +712,6 @@
8.412 I
8.413 else
8.414 let
8.415 - val base_loc =
8.416 - if not global then Local
8.417 - else if String.isPrefix thy_prefix name0 then Theory
8.418 - else General
8.419 val multi = length ths > 1
8.420 fun backquotify th =
8.421 "`" ^ Print_Mode.setmp [Print_Mode.input]
8.422 @@ -688,7 +741,15 @@
8.423 case find_first check_thms [name1, name2, name0] of
8.424 SOME name => repair_name reserved multi j name
8.425 | NONE => ""
8.426 - end), if is_chained th then Chained else base_loc),
8.427 + end),
8.428 + let val t = prop_of th in
8.429 + if is_chained th then Chained
8.430 + else if not global then Local
8.431 + else if Termtab.defined intros t then Intro
8.432 + else if Termtab.defined elims t then Elim
8.433 + else if Termtab.defined simps t then Simp
8.434 + else General
8.435 + end),
8.436 (multi, th)) :: rest)) ths
8.437 #> snd
8.438 end)
8.439 @@ -722,7 +783,7 @@
8.440 else
8.441 all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
8.442 |> name_thm_pairs ctxt (respect_no_atp andalso not only)
8.443 - |> make_unique
8.444 + |> uniquify
8.445 in
8.446 trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
8.447 " theorems");
9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 31 18:38:30 2010 +0200
9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 01 07:53:31 2010 +0200
9.3 @@ -67,7 +67,7 @@
9.4 ("verbose", "false"),
9.5 ("overlord", "false"),
9.6 ("explicit_apply", "false"),
9.7 - ("relevance_thresholds", "45 90"),
9.8 + ("relevance_thresholds", "45 85"),
9.9 ("max_relevant", "smart"),
9.10 ("theory_relevant", "smart"),
9.11 ("isar_proof", "false"),
10.1 --- a/src/HOL/Tools/list_code.ML Tue Aug 31 18:38:30 2010 +0200
10.2 +++ b/src/HOL/Tools/list_code.ML Wed Sep 01 07:53:31 2010 +0200
10.3 @@ -46,7 +46,7 @@
10.4 Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
10.5 | NONE =>
10.6 default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
10.7 - in Code_Target.add_syntax_const target @{const_name Cons}
10.8 + in Code_Target.add_const_syntax target @{const_name Cons}
10.9 (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
10.10 end
10.11
11.1 --- a/src/HOL/Tools/numeral.ML Tue Aug 31 18:38:30 2010 +0200
11.2 +++ b/src/HOL/Tools/numeral.ML Wed Sep 01 07:53:31 2010 +0200
11.3 @@ -76,7 +76,7 @@
11.4 fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
11.5 (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
11.6 in
11.7 - thy |> Code_Target.add_syntax_const target number_of
11.8 + thy |> Code_Target.add_const_syntax target number_of
11.9 (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
11.10 @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))))
11.11 end;
12.1 --- a/src/HOL/Tools/string_code.ML Tue Aug 31 18:38:30 2010 +0200
12.2 +++ b/src/HOL/Tools/string_code.ML Wed Sep 01 07:53:31 2010 +0200
12.3 @@ -59,7 +59,7 @@
12.4 Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
12.5 | NONE =>
12.6 List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
12.7 - in Code_Target.add_syntax_const target
12.8 + in Code_Target.add_const_syntax target
12.9 @{const_name Cons} (SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))
12.10 end;
12.11
12.12 @@ -69,7 +69,7 @@
12.13 case decode_char nibbles' (t1, t2)
12.14 of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
12.15 | NONE => Code_Printer.eqn_error thm "Illegal character expression";
12.16 - in Code_Target.add_syntax_const target
12.17 + in Code_Target.add_const_syntax target
12.18 @{const_name Char} (SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))
12.19 end;
12.20
12.21 @@ -82,7 +82,7 @@
12.22 of SOME p => p
12.23 | NONE => Code_Printer.eqn_error thm "Illegal message expression")
12.24 | NONE => Code_Printer.eqn_error thm "Illegal message expression";
12.25 - in Code_Target.add_syntax_const target
12.26 + in Code_Target.add_const_syntax target
12.27 @{const_name STR} (SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))
12.28 end;
12.29
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/HOL/Tools/try.ML Wed Sep 01 07:53:31 2010 +0200
13.3 @@ -0,0 +1,81 @@
13.4 +(* Title: HOL/Tools/try.ML
13.5 + Author: Jasmin Blanchette, TU Muenchen
13.6 +
13.7 +Try a combination of proof methods.
13.8 +*)
13.9 +
13.10 +signature TRY =
13.11 +sig
13.12 + val invoke_try : Proof.state -> unit
13.13 +end;
13.14 +
13.15 +structure Try : TRY =
13.16 +struct
13.17 +
13.18 +val timeout = Time.fromSeconds 5
13.19 +
13.20 +fun can_apply pre post tac st =
13.21 + let val {goal, ...} = Proof.goal st in
13.22 + case TimeLimit.timeLimit timeout (Seq.pull o tac) (pre st) of
13.23 + SOME (x, _) => nprems_of (post x) < nprems_of goal
13.24 + | NONE => false
13.25 + end
13.26 +
13.27 +fun do_generic command pre post apply st =
13.28 + let val timer = Timer.startRealTimer () in
13.29 + if can_apply pre post apply st then
13.30 + SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
13.31 + else
13.32 + NONE
13.33 + end
13.34 +
13.35 +fun named_method thy name =
13.36 + Method.method thy (Args.src ((name, []), Position.none))
13.37 +
13.38 +fun apply_named_method name ctxt =
13.39 + let val thy = ProofContext.theory_of ctxt in
13.40 + Method.apply (named_method thy name) ctxt []
13.41 + end
13.42 +
13.43 +fun do_named_method name st =
13.44 + do_generic name (#goal o Proof.goal) snd
13.45 + (apply_named_method name (Proof.context_of st)) st
13.46 +
13.47 +fun apply_named_method_on_first_goal name ctxt =
13.48 + let val thy = ProofContext.theory_of ctxt in
13.49 + Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
13.50 + end
13.51 +
13.52 +fun do_named_method_on_first_goal name st =
13.53 + do_generic (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
13.54 + else "")) I (#goal o Proof.goal)
13.55 + (apply_named_method_on_first_goal name (Proof.context_of st)) st
13.56 +
13.57 +val all_goals_named_methods = ["auto", "safe"]
13.58 +val first_goal_named_methods =
13.59 + ["simp", "fast", "fastsimp", "force", "best", "blast"]
13.60 +val do_methods =
13.61 + map do_named_method_on_first_goal all_goals_named_methods @
13.62 + map do_named_method first_goal_named_methods
13.63 +
13.64 +fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
13.65 +
13.66 +fun invoke_try st =
13.67 + case do_methods |> Par_List.map (fn f => f st)
13.68 + |> map_filter I |> sort (int_ord o pairself snd) of
13.69 + [] => writeln "No proof found."
13.70 + | xs as (s, _) :: _ =>
13.71 + priority ("Try this command: " ^
13.72 + Markup.markup Markup.sendback
13.73 + ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^
13.74 + " " ^ s) ^
13.75 + ".\n(" ^ space_implode "; " (map time_string xs) ^ ")\n")
13.76 +
13.77 +val tryN = "try"
13.78 +
13.79 +val _ =
13.80 + Outer_Syntax.improper_command tryN
13.81 + "try a combination of proof methods" Keyword.diag
13.82 + (Scan.succeed (Toplevel.keep (invoke_try o Toplevel.proof_of)))
13.83 +
13.84 +end;
14.1 --- a/src/HOL/ex/Numeral.thy Tue Aug 31 18:38:30 2010 +0200
14.2 +++ b/src/HOL/ex/Numeral.thy Wed Sep 01 07:53:31 2010 +0200
14.3 @@ -989,7 +989,7 @@
14.4 in dest_num end;
14.5 fun pretty sgn literals [one', dig0', dig1'] _ thm _ _ [(t, _)] =
14.6 (Code_Printer.str o print literals o sgn o dest_num one' dig0' dig1' thm) t
14.7 - fun add_syntax (c, sgn) = Code_Target.add_syntax_const target c
14.8 + fun add_syntax (c, sgn) = Code_Target.add_const_syntax target c
14.9 (SOME (Code_Printer.complex_const_syntax
14.10 (1, ([@{const_name One}, @{const_name Dig0}, @{const_name Dig1}],
14.11 pretty sgn))));
15.1 --- a/src/Pure/ML/ml_context.ML Tue Aug 31 18:38:30 2010 +0200
15.2 +++ b/src/Pure/ML/ml_context.ML Wed Sep 01 07:53:31 2010 +0200
15.3 @@ -35,8 +35,8 @@
15.4 val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
15.5 val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
15.6 Context.generic -> Context.generic
15.7 - val evaluate:
15.8 - Proof.context -> bool -> string * (unit -> 'a) option Unsynchronized.ref -> string -> 'a
15.9 + val evaluate: Proof.context -> bool ->
15.10 + string * (unit -> 'a) option Unsynchronized.ref -> string * string -> 'a
15.11 end
15.12
15.13 structure ML_Context: ML_CONTEXT =
15.14 @@ -203,10 +203,10 @@
15.15
15.16
15.17 (* FIXME not thread-safe -- reference can be accessed directly *)
15.18 -fun evaluate ctxt verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
15.19 +fun evaluate ctxt verbose (ref_name, r) (prelude, txt) = NAMED_CRITICAL "ML" (fn () =>
15.20 let
15.21 - val ants =
15.22 - ML_Lex.read Position.none ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))");
15.23 + val s = prelude ^ "val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))"
15.24 + val ants = ML_Lex.read Position.none s;
15.25 val _ = r := NONE;
15.26 val _ =
15.27 Context.setmp_thread_data (SOME (Context.Proof ctxt))
16.1 --- a/src/Tools/Code/code_eval.ML Tue Aug 31 18:38:30 2010 +0200
16.2 +++ b/src/Tools/Code/code_eval.ML Wed Sep 01 07:53:31 2010 +0200
16.3 @@ -9,8 +9,6 @@
16.4 val target: string
16.5 val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
16.6 -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
16.7 - val evaluation_code: theory -> string -> string list -> string list
16.8 - -> string * ((string * string) list * (string * string) list)
16.9 val setup: theory -> theory
16.10 end;
16.11
16.12 @@ -21,16 +19,12 @@
16.13
16.14 val target = "Eval";
16.15
16.16 -val eval_struct_name = "Code";
16.17 -
16.18 -fun evaluation_code thy struct_name_hint tycos consts =
16.19 +fun evaluation_code thy module_name tycos consts =
16.20 let
16.21 val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
16.22 val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
16.23 - val struct_name = if struct_name_hint = "" then eval_struct_name
16.24 - else struct_name_hint;
16.25 - val (ml_code, target_names) = Code_ML.evaluation_code_of thy target
16.26 - struct_name naming program (consts' @ tycos');
16.27 + val (ml_code, target_names) = Code_Target.produce_code_for thy
16.28 + target NONE module_name [] naming program (consts' @ tycos');
16.29 val (consts'', tycos'') = chop (length consts') target_names;
16.30 val consts_map = map2 (fn const => fn NONE =>
16.31 error ("Constant " ^ (quote o Code.string_of_const thy) const
16.32 @@ -57,11 +51,11 @@
16.33 |> Graph.new_node (value_name,
16.34 Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
16.35 |> fold (curry Graph.add_edge value_name) deps;
16.36 - val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
16.37 - (the_default target some_target) "" naming program' [value_name];
16.38 - val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
16.39 - ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
16.40 - in ML_Context.evaluate ctxt false reff sml_code end;
16.41 + val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
16.42 + (the_default target some_target) NONE "Code" [] naming program' [value_name];
16.43 + val value_code = space_implode " "
16.44 + (value_name' :: map (enclose "(" ")") args);
16.45 + in ML_Context.evaluate ctxt false reff (program_code, value_code) end;
16.46 in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
16.47
16.48
16.49 @@ -69,26 +63,23 @@
16.50
16.51 local
16.52
16.53 -structure CodeAntiqData = Proof_Data
16.54 +structure Code_Antiq_Data = Proof_Data
16.55 (
16.56 - type T = (string list * string list) * (bool * (string
16.57 - * (string * ((string * string) list * (string * string) list)) lazy));
16.58 - fun init _ = (([], []), (true, ("", Lazy.value ("", ([], [])))));
16.59 + type T = (string list * string list) * (bool
16.60 + * (string * ((string * string) list * (string * string) list)) lazy);
16.61 + fun init _ = (([], []), (true, (Lazy.value ("", ([], [])))));
16.62 );
16.63
16.64 -val is_first_occ = fst o snd o CodeAntiqData.get;
16.65 +val is_first_occ = fst o snd o Code_Antiq_Data.get;
16.66
16.67 fun register_code new_tycos new_consts ctxt =
16.68 let
16.69 - val ((tycos, consts), (_, (struct_name, _))) = CodeAntiqData.get ctxt;
16.70 + val ((tycos, consts), _) = Code_Antiq_Data.get ctxt;
16.71 val tycos' = fold (insert (op =)) new_tycos tycos;
16.72 val consts' = fold (insert (op =)) new_consts consts;
16.73 - val (struct_name', ctxt') = if struct_name = ""
16.74 - then ML_Antiquote.variant eval_struct_name ctxt
16.75 - else (struct_name, ctxt);
16.76 - val acc_code = Lazy.lazy
16.77 - (fn () => evaluation_code (ProofContext.theory_of ctxt) eval_struct_name tycos' consts');
16.78 - in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end;
16.79 + val acc_code = Lazy.lazy (fn () =>
16.80 + evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts');
16.81 + in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
16.82
16.83 fun register_const const = register_code [] [const];
16.84
16.85 @@ -99,11 +90,11 @@
16.86
16.87 fun print_code is_first print_it ctxt =
16.88 let
16.89 - val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
16.90 + val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
16.91 val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
16.92 val ml_code = if is_first then ml_code
16.93 else "";
16.94 - val all_struct_name = "Isabelle." ^ struct_code_name;
16.95 + val all_struct_name = "Isabelle";
16.96 in (ml_code, print_it all_struct_name tycos_map consts_map) end;
16.97
16.98 in
16.99 @@ -143,34 +134,30 @@
16.100 Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
16.101 in
16.102 thy
16.103 - |> Code_Target.add_syntax_tyco target tyco (SOME (k, pr))
16.104 + |> Code_Target.add_tyco_syntax target tyco (SOME (k, pr))
16.105 end;
16.106
16.107 fun add_eval_constr (const, const') thy =
16.108 let
16.109 val k = Code.args_number thy const;
16.110 fun pr pr' fxy ts = Code_Printer.brackify fxy
16.111 - (const' :: the_list (Code_ML.print_tuple pr' Code_Printer.BR (map fst ts)));
16.112 + (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
16.113 in
16.114 thy
16.115 - |> Code_Target.add_syntax_const target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
16.116 + |> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
16.117 end;
16.118
16.119 -fun add_eval_const (const, const') = Code_Target.add_syntax_const target
16.120 +fun add_eval_const (const, const') = Code_Target.add_const_syntax target
16.121 const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
16.122
16.123 fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
16.124 - let
16.125 - val pr = Code_Printer.str o Long_Name.append module_name;
16.126 - in
16.127 - thy
16.128 - |> Code_Target.add_reserved target module_name
16.129 - |> Context.theory_map
16.130 - (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
16.131 - |> fold (add_eval_tyco o apsnd pr) tyco_map
16.132 - |> fold (add_eval_constr o apsnd pr) constr_map
16.133 - |> fold (add_eval_const o apsnd pr) const_map
16.134 - end
16.135 + thy
16.136 + |> Code_Target.add_reserved target module_name
16.137 + |> Context.theory_map
16.138 + (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
16.139 + |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
16.140 + |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
16.141 + |> fold (add_eval_const o apsnd Code_Printer.str) const_map
16.142 | process (code_body, _) _ (SOME file_name) thy =
16.143 let
16.144 val preamble =
17.1 --- a/src/Tools/Code/code_haskell.ML Tue Aug 31 18:38:30 2010 +0200
17.2 +++ b/src/Tools/Code/code_haskell.ML Wed Sep 01 07:53:31 2010 +0200
17.3 @@ -24,11 +24,11 @@
17.4
17.5 (** Haskell serializer **)
17.6
17.7 -fun print_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
17.8 +fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
17.9 reserved deresolve contr_classparam_typs deriving_show =
17.10 let
17.11 val deresolve_base = Long_Name.base_name o deresolve;
17.12 - fun class_name class = case syntax_class class
17.13 + fun class_name class = case class_syntax class
17.14 of NONE => deresolve class
17.15 | SOME class => class;
17.16 fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
17.17 @@ -43,7 +43,7 @@
17.18 (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
17.19 fun print_tyco_expr tyvars fxy (tyco, tys) =
17.20 brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
17.21 - and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
17.22 + and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco
17.23 of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
17.24 | SOME (i, print) => print (print_typ tyvars) fxy tys)
17.25 | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
17.26 @@ -72,7 +72,7 @@
17.27 in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
17.28 | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
17.29 (case Code_Thingol.unfold_const_app t0
17.30 - of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
17.31 + of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
17.32 then print_case tyvars some_thm vars fxy cases
17.33 else print_app tyvars some_thm vars fxy c_ts
17.34 | NONE => print_case tyvars some_thm vars fxy cases)
17.35 @@ -90,7 +90,7 @@
17.36 (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs)
17.37 else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
17.38 end
17.39 - and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const
17.40 + and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
17.41 and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
17.42 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
17.43 let
17.44 @@ -133,7 +133,7 @@
17.45 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
17.46 val vars = reserved
17.47 |> intro_base_names
17.48 - (is_none o syntax_const) deresolve consts
17.49 + (is_none o const_syntax) deresolve consts
17.50 |> intro_vars ((fold o Code_Thingol.fold_varnames)
17.51 (insert (op =)) ts []);
17.52 in
17.53 @@ -218,7 +218,7 @@
17.54 | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
17.55 let
17.56 val tyvars = intro_vars (map fst vs) reserved;
17.57 - fun requires_args classparam = case syntax_const classparam
17.58 + fun requires_args classparam = case const_syntax classparam
17.59 of NONE => 0
17.60 | SOME (Code_Printer.Plain_const_syntax _) => 0
17.61 | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k;
17.62 @@ -234,7 +234,7 @@
17.63 val (c, (_, tys)) = const;
17.64 val (vs, rhs) = (apfst o map) fst
17.65 (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
17.66 - val s = if (is_some o syntax_const) c
17.67 + val s = if (is_some o const_syntax) c
17.68 then NONE else (SOME o Long_Name.base_name o deresolve) c;
17.69 val vars = reserved
17.70 |> intro_vars (map_filter I (s :: vs));
17.71 @@ -313,12 +313,12 @@
17.72 handle Option => error ("Unknown statement name: " ^ labelled_name name);
17.73 in (deresolver, hs_program) end;
17.74
17.75 -fun serialize_haskell module_prefix module_name string_classes labelled_name
17.76 - raw_reserved includes module_alias
17.77 - syntax_class syntax_tyco syntax_const program
17.78 - (stmt_names, presentation_stmt_names) =
17.79 +fun serialize_haskell module_prefix string_classes { labelled_name,
17.80 + reserved_syms, includes, module_alias,
17.81 + class_syntax, tyco_syntax, const_syntax, program,
17.82 + names, presentation_names } =
17.83 let
17.84 - val reserved = fold (insert (op =) o fst) includes raw_reserved;
17.85 + val reserved = fold (insert (op =) o fst) includes reserved_syms;
17.86 val (deresolver, hs_program) = haskell_program_of_program labelled_name
17.87 module_prefix reserved module_alias program;
17.88 val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
17.89 @@ -337,7 +337,7 @@
17.90 in deriv [] tyco end;
17.91 val reserved = make_vars reserved;
17.92 fun print_stmt qualified = print_haskell_stmt labelled_name
17.93 - syntax_class syntax_tyco syntax_const reserved
17.94 + class_syntax tyco_syntax const_syntax reserved
17.95 (if qualified then deresolver else Long_Name.base_name o deresolver)
17.96 contr_classparam_typs
17.97 (if string_classes then deriving_show else K false);
17.98 @@ -350,7 +350,7 @@
17.99 fun serialize_module1 (module_name', (deps, (stmts, _))) =
17.100 let
17.101 val stmt_names = map fst stmts;
17.102 - val qualified = is_none module_name;
17.103 + val qualified = null presentation_names;
17.104 val imports = subtract (op =) stmt_names deps
17.105 |> distinct (op =)
17.106 |> map_filter (try deresolver)
17.107 @@ -368,13 +368,13 @@
17.108 );
17.109 in print_module module_name' content end;
17.110 fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks2 (map_filter
17.111 - (fn (name, (_, SOME stmt)) => if null presentation_stmt_names
17.112 - orelse member (op =) presentation_stmt_names name
17.113 + (fn (name, (_, SOME stmt)) => if null presentation_names
17.114 + orelse member (op =) presentation_names name
17.115 then SOME (print_stmt false (name, stmt))
17.116 else NONE
17.117 | (_, (_, NONE)) => NONE) stmts);
17.118 val serialize_module =
17.119 - if null presentation_stmt_names then serialize_module1 else pair "" o serialize_module2;
17.120 + if null presentation_names then serialize_module1 else pair "" o serialize_module2;
17.121 fun write_module width (SOME destination) (modlname, content) =
17.122 let
17.123 val _ = File.check destination;
17.124 @@ -458,18 +458,18 @@
17.125 val c_bind = Code.read_const thy raw_c_bind;
17.126 in if target = target' then
17.127 thy
17.128 - |> Code_Target.add_syntax_const target c_bind
17.129 + |> Code_Target.add_const_syntax target c_bind
17.130 (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
17.131 else error "Only Haskell target allows for monad syntax" end;
17.132
17.133
17.134 (** Isar setup **)
17.135
17.136 -fun isar_serializer module_name =
17.137 +val isar_serializer =
17.138 Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
17.139 -- Scan.optional (Args.$$$ "string_classes" >> K true) false
17.140 >> (fn (module_prefix, string_classes) =>
17.141 - serialize_haskell module_prefix module_name string_classes));
17.142 + serialize_haskell module_prefix string_classes));
17.143
17.144 val _ =
17.145 Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
17.146 @@ -483,7 +483,7 @@
17.147 check = { env_var = "EXEC_GHC", make_destination = I,
17.148 make_command = fn ghc => fn module_name =>
17.149 ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
17.150 - #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
17.151 + #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
17.152 brackify_infix (1, R) fxy (
17.153 print_typ (INFX (1, X)) ty1,
17.154 str "->",
18.1 --- a/src/Tools/Code/code_ml.ML Tue Aug 31 18:38:30 2010 +0200
18.2 +++ b/src/Tools/Code/code_ml.ML Wed Sep 01 07:53:31 2010 +0200
18.3 @@ -8,10 +8,6 @@
18.4 sig
18.5 val target_SML: string
18.6 val target_OCaml: string
18.7 - val evaluation_code_of: theory -> string -> string
18.8 - -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
18.9 - val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
18.10 - -> Code_Printer.fixity -> 'a list -> Pretty.T option
18.11 val setup: theory -> theory
18.12 end;
18.13
18.14 @@ -56,21 +52,21 @@
18.15 | print_product print [x] = SOME (print x)
18.16 | print_product print xs = (SOME o enum " *" "" "") (map print xs);
18.17
18.18 -fun print_tuple _ _ [] = NONE
18.19 - | print_tuple print fxy [x] = SOME (print fxy x)
18.20 - | print_tuple print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
18.21 +fun tuplify _ _ [] = NONE
18.22 + | tuplify print fxy [x] = SOME (print fxy x)
18.23 + | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
18.24
18.25
18.26 (** SML serializer **)
18.27
18.28 -fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
18.29 +fun print_sml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =
18.30 let
18.31 fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
18.32 | print_tyco_expr fxy (tyco, [ty]) =
18.33 concat [print_typ BR ty, (str o deresolve) tyco]
18.34 | print_tyco_expr fxy (tyco, tys) =
18.35 concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
18.36 - and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
18.37 + and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
18.38 of NONE => print_tyco_expr fxy (tyco, tys)
18.39 | SOME (i, print) => print print_typ fxy tys)
18.40 | print_typ fxy (ITyVar v) = str ("'" ^ v);
18.41 @@ -94,7 +90,7 @@
18.42 | classrels => brackets
18.43 [enum " o" "(" ")" (map (str o deresolve) classrels), v_p]
18.44 end
18.45 - and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
18.46 + and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
18.47 val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
18.48 (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
18.49 fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
18.50 @@ -118,7 +114,7 @@
18.51 in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
18.52 | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
18.53 (case Code_Thingol.unfold_const_app t0
18.54 - of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
18.55 + of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
18.56 then print_case is_pseudo_fun some_thm vars fxy cases
18.57 else print_app is_pseudo_fun some_thm vars fxy c_ts
18.58 | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
18.59 @@ -127,7 +123,7 @@
18.60 let val k = length function_typs in
18.61 if k < 2 orelse length ts = k
18.62 then (str o deresolve) c
18.63 - :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
18.64 + :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
18.65 else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
18.66 end
18.67 else if is_pseudo_fun c
18.68 @@ -135,7 +131,7 @@
18.69 else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
18.70 @ map (print_term is_pseudo_fun some_thm vars BR) ts
18.71 and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
18.72 - (print_term is_pseudo_fun) syntax_const some_thm vars
18.73 + (print_term is_pseudo_fun) const_syntax some_thm vars
18.74 and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
18.75 and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
18.76 let
18.77 @@ -194,7 +190,7 @@
18.78 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
18.79 val vars = reserved
18.80 |> intro_base_names
18.81 - (is_none o syntax_const) deresolve consts
18.82 + (is_none o const_syntax) deresolve consts
18.83 |> intro_vars ((fold o Code_Thingol.fold_varnames)
18.84 (insert (op =)) ts []);
18.85 val prolog = if needs_typ then
18.86 @@ -343,9 +339,8 @@
18.87 end;
18.88 in print_stmt end;
18.89
18.90 -fun print_sml_module name some_decls body = if name = ""
18.91 - then Pretty.chunks2 body
18.92 - else Pretty.chunks2 (
18.93 +fun print_sml_module name some_decls body =
18.94 + Pretty.chunks2 (
18.95 Pretty.chunks (
18.96 str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
18.97 :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
18.98 @@ -369,14 +364,14 @@
18.99
18.100 (** OCaml serializer **)
18.101
18.102 -fun print_ocaml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
18.103 +fun print_ocaml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =
18.104 let
18.105 fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
18.106 | print_tyco_expr fxy (tyco, [ty]) =
18.107 concat [print_typ BR ty, (str o deresolve) tyco]
18.108 | print_tyco_expr fxy (tyco, tys) =
18.109 concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
18.110 - and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
18.111 + and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
18.112 of NONE => print_tyco_expr fxy (tyco, tys)
18.113 | SOME (i, print) => print print_typ fxy tys)
18.114 | print_typ fxy (ITyVar v) = str ("'" ^ v);
18.115 @@ -395,7 +390,7 @@
18.116 else "_" ^ first_upper v ^ string_of_int (i+1))
18.117 |> fold_rev (fn classrel => fn p =>
18.118 Pretty.block [p, str ".", (str o deresolve) classrel]) classrels
18.119 - and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
18.120 + and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
18.121 val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
18.122 (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
18.123 fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
18.124 @@ -416,7 +411,7 @@
18.125 in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
18.126 | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
18.127 (case Code_Thingol.unfold_const_app t0
18.128 - of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
18.129 + of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
18.130 then print_case is_pseudo_fun some_thm vars fxy cases
18.131 else print_app is_pseudo_fun some_thm vars fxy c_ts
18.132 | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
18.133 @@ -425,7 +420,7 @@
18.134 let val k = length tys in
18.135 if length ts = k
18.136 then (str o deresolve) c
18.137 - :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
18.138 + :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
18.139 else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
18.140 end
18.141 else if is_pseudo_fun c
18.142 @@ -433,7 +428,7 @@
18.143 else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
18.144 @ map (print_term is_pseudo_fun some_thm vars BR) ts
18.145 and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
18.146 - (print_term is_pseudo_fun) syntax_const some_thm vars
18.147 + (print_term is_pseudo_fun) const_syntax some_thm vars
18.148 and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
18.149 and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
18.150 let
18.151 @@ -499,7 +494,7 @@
18.152 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
18.153 val vars = reserved
18.154 |> intro_base_names
18.155 - (is_none o syntax_const) deresolve consts
18.156 + (is_none o const_syntax) deresolve consts
18.157 |> intro_vars ((fold o Code_Thingol.fold_varnames)
18.158 (insert (op =)) ts []);
18.159 in
18.160 @@ -525,7 +520,7 @@
18.161 val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
18.162 val vars = reserved
18.163 |> intro_base_names
18.164 - (is_none o syntax_const) deresolve consts;
18.165 + (is_none o const_syntax) deresolve consts;
18.166 val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
18.167 in
18.168 Pretty.block (
18.169 @@ -669,9 +664,8 @@
18.170 end;
18.171 in print_stmt end;
18.172
18.173 -fun print_ocaml_module name some_decls body = if name = ""
18.174 - then Pretty.chunks2 body
18.175 - else Pretty.chunks2 (
18.176 +fun print_ocaml_module name some_decls body =
18.177 + Pretty.chunks2 (
18.178 Pretty.chunks (
18.179 str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
18.180 :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
18.181 @@ -722,7 +716,7 @@
18.182
18.183 in
18.184
18.185 -fun ml_node_of_program labelled_name module_name reserved module_alias program =
18.186 +fun ml_node_of_program labelled_name reserved module_alias program =
18.187 let
18.188 val reserved = Name.make_context reserved;
18.189 val empty_module = ((reserved, reserved), Graph.empty);
18.190 @@ -906,21 +900,21 @@
18.191 error ("Unknown statement name: " ^ labelled_name name);
18.192 in (deresolver, nodes) end;
18.193
18.194 -fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
18.195 - reserved includes module_alias _ syntax_tyco syntax_const program
18.196 - (stmt_names, presentation_stmt_names) =
18.197 +fun serialize_ml target print_module print_stmt with_signatures { labelled_name,
18.198 + reserved_syms, includes, module_alias, class_syntax, tyco_syntax,
18.199 + const_syntax, program, names, presentation_names } =
18.200 let
18.201 val is_cons = Code_Thingol.is_cons program;
18.202 - val is_presentation = not (null presentation_stmt_names);
18.203 - val (deresolver, nodes) = ml_node_of_program labelled_name module_name
18.204 - reserved module_alias program;
18.205 - val reserved = make_vars reserved;
18.206 + val is_presentation = not (null presentation_names);
18.207 + val (deresolver, nodes) = ml_node_of_program labelled_name
18.208 + reserved_syms module_alias program;
18.209 + val reserved = make_vars reserved_syms;
18.210 fun print_node prefix (Dummy _) =
18.211 NONE
18.212 | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
18.213 - (null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt
18.214 + (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
18.215 then NONE
18.216 - else SOME (print_stmt labelled_name syntax_tyco syntax_const reserved is_cons (deresolver prefix) stmt)
18.217 + else SOME (print_stmt labelled_name tyco_syntax const_syntax reserved is_cons (deresolver prefix) stmt)
18.218 | print_node prefix (Module (module_name, (_, nodes))) =
18.219 let
18.220 val (decls, body) = print_nodes (prefix @ [module_name]) nodes;
18.221 @@ -931,36 +925,28 @@
18.222 o rev o flat o Graph.strong_conn) nodes
18.223 |> split_list
18.224 |> (fn (decls, body) => (flat decls, body))
18.225 - val stmt_names' = (map o try)
18.226 - (deresolver (if is_some module_name then the_list module_name else [])) stmt_names;
18.227 + val names' = map (try (deresolver [])) names;
18.228 val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
18.229 fun write width NONE = writeln_pretty width
18.230 | write width (SOME p) = File.write p o string_of_pretty width;
18.231 in
18.232 - Code_Target.serialization write (fn width => (rpair stmt_names' o string_of_pretty width)) p
18.233 + Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p
18.234 end;
18.235
18.236 end; (*local*)
18.237
18.238
18.239 -(** for instrumentalization **)
18.240 -
18.241 -fun evaluation_code_of thy target struct_name =
18.242 - Code_Target.serialize_custom thy (target, fn module_name => fn [] =>
18.243 - serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name);
18.244 -
18.245 -
18.246 (** Isar setup **)
18.247
18.248 -fun isar_serializer_sml module_name =
18.249 +val isar_serializer_sml =
18.250 Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
18.251 >> (fn with_signatures => serialize_ml target_SML
18.252 - print_sml_module print_sml_stmt module_name with_signatures));
18.253 + print_sml_module print_sml_stmt with_signatures));
18.254
18.255 -fun isar_serializer_ocaml module_name =
18.256 +val isar_serializer_ocaml =
18.257 Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
18.258 >> (fn with_signatures => serialize_ml target_OCaml
18.259 - print_ocaml_module print_ocaml_stmt module_name with_signatures));
18.260 + print_ocaml_module print_ocaml_stmt with_signatures));
18.261
18.262 val setup =
18.263 Code_Target.add_target
18.264 @@ -971,13 +957,13 @@
18.265 (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
18.266 check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
18.267 make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
18.268 - #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
18.269 + #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
18.270 brackify_infix (1, R) fxy (
18.271 print_typ (INFX (1, X)) ty1,
18.272 str "->",
18.273 print_typ (INFX (1, R)) ty2
18.274 )))
18.275 - #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
18.276 + #> Code_Target.add_tyco_syntax target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
18.277 brackify_infix (1, R) fxy (
18.278 print_typ (INFX (1, X)) ty1,
18.279 str "->",
19.1 --- a/src/Tools/Code/code_printer.ML Tue Aug 31 18:38:30 2010 +0200
19.2 +++ b/src/Tools/Code/code_printer.ML Wed Sep 01 07:53:31 2010 +0200
19.3 @@ -68,6 +68,8 @@
19.4 val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
19.5 val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
19.6 val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
19.7 + val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
19.8 +
19.9
19.10 type tyco_syntax
19.11 type simple_const_syntax
19.12 @@ -244,6 +246,10 @@
19.13 (if (fixity BR fxy_ctxt) then enclose "(" ")" else Pretty.block)
19.14 (p @@ enum "," opn cls (map f ps));
19.15
19.16 +fun tuplify _ _ [] = NONE
19.17 + | tuplify print fxy [x] = SOME (print fxy x)
19.18 + | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
19.19 +
19.20
19.21 (* generic syntax *)
19.22
19.23 @@ -278,8 +284,8 @@
19.24 fold_map (Code_Thingol.ensure_declared_const thy) cs naming
19.25 |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
19.26
19.27 -fun gen_print_app print_app_expr print_term syntax_const some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
19.28 - case syntax_const c
19.29 +fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
19.30 + case const_syntax c
19.31 of NONE => brackify fxy (print_app_expr some_thm vars app)
19.32 | SOME (Plain_const_syntax (_, s)) => brackify fxy (str s :: map (print_term some_thm vars BR) ts)
19.33 | SOME (Complex_const_syntax (k, print)) =>
20.1 --- a/src/Tools/Code/code_scala.ML Tue Aug 31 18:38:30 2010 +0200
20.2 +++ b/src/Tools/Code/code_scala.ML Wed Sep 01 07:53:31 2010 +0200
20.3 @@ -24,14 +24,14 @@
20.4
20.5 (** Scala serializer **)
20.6
20.7 -fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
20.8 +fun print_scala_stmt labelled_name tyco_syntax const_syntax reserved
20.9 args_num is_singleton_constr (deresolve, deresolve_full) =
20.10 let
20.11 fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
20.12 fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
20.13 fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
20.14 (print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys
20.15 - and print_typ tyvars fxy (tyco `%% tys) = (case syntax_tyco tyco
20.16 + and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
20.17 of NONE => print_tyco_expr tyvars fxy (tyco, tys)
20.18 | SOME (i, print) => print (print_typ tyvars) fxy tys)
20.19 | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
20.20 @@ -67,7 +67,7 @@
20.21 end
20.22 | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
20.23 (case Code_Thingol.unfold_const_app t0
20.24 - of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
20.25 + of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
20.26 then print_case tyvars some_thm vars fxy cases
20.27 else print_app tyvars is_pat some_thm vars fxy c_ts
20.28 | NONE => print_case tyvars some_thm vars fxy cases)
20.29 @@ -76,8 +76,8 @@
20.30 let
20.31 val k = length ts;
20.32 val arg_typs' = if is_pat orelse
20.33 - (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
20.34 - val (l, print') = case syntax_const c
20.35 + (is_none (const_syntax c) andalso is_singleton_constr c) then [] else arg_typs;
20.36 + val (l, print') = case const_syntax c
20.37 of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
20.38 (print_term tyvars is_pat some_thm vars NOBR) fxy
20.39 (applify "[" "]" (print_typ tyvars NOBR)
20.40 @@ -156,7 +156,7 @@
20.41 fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
20.42 val tyvars = reserved
20.43 |> intro_base_names
20.44 - (is_none o syntax_tyco) deresolve tycos
20.45 + (is_none o tyco_syntax) deresolve tycos
20.46 |> intro_tyvars vs;
20.47 val simple = case eqs
20.48 of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
20.49 @@ -165,14 +165,14 @@
20.50 (map (snd o fst) eqs) [];
20.51 val vars1 = reserved
20.52 |> intro_base_names
20.53 - (is_none o syntax_const) deresolve consts
20.54 + (is_none o const_syntax) deresolve consts
20.55 val params = if simple
20.56 then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
20.57 else aux_params vars1 (map (fst o fst) eqs);
20.58 val vars2 = intro_vars params vars1;
20.59 val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;
20.60 - fun print_tuple [p] = p
20.61 - | print_tuple ps = enum "," "(" ")" ps;
20.62 + fun tuplify [p] = p
20.63 + | tuplify ps = enum "," "(" ")" ps;
20.64 fun print_rhs vars' ((_, t), (some_thm, _)) =
20.65 print_term tyvars false some_thm vars' NOBR t;
20.66 fun print_clause (eq as ((ts, _), (some_thm, _))) =
20.67 @@ -181,7 +181,7 @@
20.68 (insert (op =)) ts []) vars1;
20.69 in
20.70 concat [str "case",
20.71 - print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
20.72 + tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
20.73 str "=>", print_rhs vars' eq]
20.74 end;
20.75 val head = print_defhead tyvars vars2 name vs params tys' ty';
20.76 @@ -189,7 +189,7 @@
20.77 concat [head, print_rhs vars2 (hd eqs)]
20.78 else
20.79 Pretty.block_enclose
20.80 - (concat [head, print_tuple (map (str o lookup_var vars2) params),
20.81 + (concat [head, tuplify (map (str o lookup_var vars2) params),
20.82 str "match", str "{"], str "}")
20.83 (map print_clause eqs)
20.84 end;
20.85 @@ -413,13 +413,13 @@
20.86
20.87 in (deresolver, sca_program) end;
20.88
20.89 -fun serialize_scala labelled_name raw_reserved includes module_alias
20.90 - _ syntax_tyco syntax_const
20.91 - program (stmt_names, presentation_stmt_names) =
20.92 +fun serialize_scala { labelled_name, reserved_syms, includes,
20.93 + module_alias, class_syntax, tyco_syntax, const_syntax, program,
20.94 + names, presentation_names } =
20.95 let
20.96
20.97 (* build program *)
20.98 - val reserved = fold (insert (op =) o fst) includes raw_reserved;
20.99 + val reserved = fold (insert (op =) o fst) includes reserved_syms;
20.100 val (deresolver, sca_program) = scala_program_of_program labelled_name
20.101 (Name.make_context reserved) module_alias program;
20.102
20.103 @@ -440,7 +440,7 @@
20.104 fun is_singleton_constr c = case Graph.get_node program c
20.105 of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
20.106 | _ => false;
20.107 - val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
20.108 + val print_stmt = print_scala_stmt labelled_name tyco_syntax const_syntax
20.109 (make_vars reserved) args_num is_singleton_constr;
20.110
20.111 (* print nodes *)
20.112 @@ -455,12 +455,12 @@
20.113 in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
20.114 fun print_node _ (_, Dummy) = NONE
20.115 | print_node prefix_fragments (name, Stmt stmt) =
20.116 - if null presentation_stmt_names
20.117 - orelse member (op =) presentation_stmt_names name
20.118 + if null presentation_names
20.119 + orelse member (op =) presentation_names name
20.120 then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
20.121 else NONE
20.122 | print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
20.123 - if null presentation_stmt_names
20.124 + if null presentation_names
20.125 then
20.126 let
20.127 val prefix_fragments' = prefix_fragments @ [name_fragment];
20.128 @@ -477,7 +477,7 @@
20.129 in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
20.130
20.131 (* serialization *)
20.132 - val p_includes = if null presentation_stmt_names
20.133 + val p_includes = if null presentation_names
20.134 then map (fn (base, p) => print_module base [] p) includes else [];
20.135 val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
20.136 fun write width NONE = writeln_pretty width
20.137 @@ -513,9 +513,8 @@
20.138
20.139 (** Isar setup **)
20.140
20.141 -fun isar_serializer _ =
20.142 - Code_Target.parse_args (Scan.succeed ())
20.143 - #> (fn () => serialize_scala);
20.144 +val isar_serializer =
20.145 + Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
20.146
20.147 val setup =
20.148 Code_Target.add_target
20.149 @@ -524,7 +523,7 @@
20.150 make_command = fn scala_home => fn _ =>
20.151 "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
20.152 ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " ROOT.scala" } })
20.153 - #> Code_Target.add_syntax_tyco target "fun"
20.154 + #> Code_Target.add_tyco_syntax target "fun"
20.155 (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
20.156 brackify_infix (1, R) fxy (
20.157 print_typ BR ty1 (*product type vs. tupled arguments!*),
21.1 --- a/src/Tools/Code/code_target.ML Tue Aug 31 18:38:30 2010 +0200
21.2 +++ b/src/Tools/Code/code_target.ML Wed Sep 01 07:53:31 2010 +0200
21.3 @@ -9,17 +9,21 @@
21.4 val cert_tyco: theory -> string -> string
21.5 val read_tyco: theory -> string -> string
21.6
21.7 - val export_code_for: theory -> Path.T option -> string -> int option -> string option -> Token.T list
21.8 + val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
21.9 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
21.10 - val produce_code_for: theory -> string -> int option -> string option -> Token.T list
21.11 - -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string * string option list
21.12 + val produce_code_for: theory -> string -> int option -> string -> Token.T list
21.13 + -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
21.14 + val present_code_for: theory -> string -> int option -> string -> Token.T list
21.15 + -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
21.16 val check_code_for: theory -> string -> bool -> Token.T list
21.17 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
21.18
21.19 val export_code: theory -> string list
21.20 - -> (((string * string option) * Path.T option) * Token.T list) list -> unit
21.21 - val produce_code: theory -> string list -> (Code_Thingol.naming -> string list)
21.22 - -> string -> int option -> string option -> Token.T list -> string * string option list
21.23 + -> (((string * string) * Path.T option) * Token.T list) list -> unit
21.24 + val produce_code: theory -> string list
21.25 + -> string -> int option -> string -> Token.T list -> string * string option list
21.26 + val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
21.27 + -> string -> int option -> string -> Token.T list -> string
21.28 val check_code: theory -> string list
21.29 -> ((string * bool) * Token.T list) list -> unit
21.30
21.31 @@ -39,22 +43,16 @@
21.32 val parse_args: 'a parser -> Token.T list -> 'a
21.33 val serialization: (int -> Path.T option -> 'a -> unit)
21.34 -> (int -> 'a -> string * string option list)
21.35 - -> 'a -> int -> serialization
21.36 + -> 'a -> serialization
21.37 val set_default_code_width: int -> theory -> theory
21.38
21.39 - (*FIXME drop asap*)
21.40 - val code_of: theory -> string -> int option -> string
21.41 - -> string list -> (Code_Thingol.naming -> string list) -> string * string option list
21.42 - val serialize_custom: theory -> string * serializer -> string option
21.43 - -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
21.44 -
21.45 val allow_abort: string -> theory -> theory
21.46 type tyco_syntax = Code_Printer.tyco_syntax
21.47 type const_syntax = Code_Printer.const_syntax
21.48 - val add_syntax_class: string -> class -> string option -> theory -> theory
21.49 - val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
21.50 - val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
21.51 - val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
21.52 + val add_class_syntax: string -> class -> string option -> theory -> theory
21.53 + val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
21.54 + val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
21.55 + val add_const_syntax: string -> string -> const_syntax option -> theory -> theory
21.56 val add_reserved: string -> string -> theory -> theory
21.57 val add_include: string -> string * (string * string list) option -> theory -> theory
21.58 end;
21.59 @@ -69,57 +67,57 @@
21.60 type const_syntax = Code_Printer.const_syntax;
21.61
21.62
21.63 -(** basics **)
21.64 +(** abstract nonsense **)
21.65
21.66 -datatype destination = File of Path.T option | String of string list;
21.67 -type serialization = destination -> (string * string option list) option;
21.68 +datatype destination = Export of Path.T option | Produce | Present of string list;
21.69 +type serialization = int -> destination -> (string * string option list) option;
21.70
21.71 -fun stmt_names_of_destination (String stmt_names) = stmt_names
21.72 +fun stmt_names_of_destination (Present stmt_names) = stmt_names
21.73 | stmt_names_of_destination _ = [];
21.74
21.75 -fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
21.76 - | serialization _ string pretty width (String _) = SOME (string width pretty);
21.77 +fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
21.78 + | serialization _ string content width Produce = SOME (string width content)
21.79 + | serialization _ string content width (Present _) = SOME (string width content);
21.80
21.81 -fun file some_path f = (f (File some_path); ());
21.82 -fun string stmt_names f = the (f (String stmt_names));
21.83 +fun export some_path f = (f (Export some_path); ());
21.84 +fun produce f = the (f Produce);
21.85 +fun present stmt_names f = fst (the (f (Present stmt_names)));
21.86
21.87
21.88 (** theory data **)
21.89
21.90 -datatype name_syntax_table = NameSyntaxTable of {
21.91 +datatype symbol_syntax_data = Symbol_Syntax_Data of {
21.92 class: string Symtab.table,
21.93 instance: unit Symreltab.table,
21.94 tyco: Code_Printer.tyco_syntax Symtab.table,
21.95 const: Code_Printer.const_syntax Symtab.table
21.96 };
21.97
21.98 -fun mk_name_syntax_table ((class, instance), (tyco, const)) =
21.99 - NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const };
21.100 -fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) =
21.101 - mk_name_syntax_table (f ((class, instance), (tyco, const)));
21.102 -fun merge_name_syntax_table
21.103 - (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 },
21.104 - NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
21.105 - mk_name_syntax_table (
21.106 +fun make_symbol_syntax_data ((class, instance), (tyco, const)) =
21.107 + Symbol_Syntax_Data { class = class, instance = instance, tyco = tyco, const = const };
21.108 +fun map_symbol_syntax_data f (Symbol_Syntax_Data { class, instance, tyco, const }) =
21.109 + make_symbol_syntax_data (f ((class, instance), (tyco, const)));
21.110 +fun merge_symbol_syntax_data
21.111 + (Symbol_Syntax_Data { class = class1, instance = instance1, tyco = tyco1, const = const1 },
21.112 + Symbol_Syntax_Data { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
21.113 + make_symbol_syntax_data (
21.114 (Symtab.join (K snd) (class1, class2),
21.115 Symreltab.join (K snd) (instance1, instance2)),
21.116 (Symtab.join (K snd) (tyco1, tyco2),
21.117 Symtab.join (K snd) (const1, const2))
21.118 );
21.119
21.120 -type serializer =
21.121 - string option (*module name*)
21.122 - -> Token.T list (*arguments*)
21.123 - -> (string -> string) (*labelled_name*)
21.124 - -> string list (*reserved symbols*)
21.125 - -> (string * Pretty.T) list (*includes*)
21.126 - -> (string -> string option) (*module aliasses*)
21.127 - -> (string -> string option) (*class syntax*)
21.128 - -> (string -> Code_Printer.tyco_syntax option)
21.129 - -> (string -> Code_Printer.activated_const_syntax option)
21.130 - -> Code_Thingol.program
21.131 - -> (string list * string list) (*selected statements*)
21.132 - -> int
21.133 +type serializer = Token.T list (*arguments*) -> {
21.134 + labelled_name: string -> string,
21.135 + reserved_syms: string list,
21.136 + includes: (string * Pretty.T) list,
21.137 + module_alias: string -> string option,
21.138 + class_syntax: string -> string option,
21.139 + tyco_syntax: string -> Code_Printer.tyco_syntax option,
21.140 + const_syntax: string -> Code_Printer.activated_const_syntax option,
21.141 + program: Code_Thingol.program,
21.142 + names: string list,
21.143 + presentation_names: string list }
21.144 -> serialization;
21.145
21.146 datatype description = Fundamental of { serializer: serializer,
21.147 @@ -134,26 +132,26 @@
21.148 description: description,
21.149 reserved: string list,
21.150 includes: (Pretty.T * string list) Symtab.table,
21.151 - name_syntax_table: name_syntax_table,
21.152 - module_alias: string Symtab.table
21.153 + module_alias: string Symtab.table,
21.154 + symbol_syntax: symbol_syntax_data
21.155 };
21.156
21.157 -fun make_target ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))) =
21.158 +fun make_target ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))) =
21.159 Target { serial = serial, description = description, reserved = reserved,
21.160 - includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
21.161 -fun map_target f ( Target { serial, description, reserved, includes, name_syntax_table, module_alias } ) =
21.162 - make_target (f ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))));
21.163 + includes = includes, module_alias = module_alias, symbol_syntax = symbol_syntax };
21.164 +fun map_target f ( Target { serial, description, reserved, includes, module_alias, symbol_syntax } ) =
21.165 + make_target (f ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))));
21.166 fun merge_target strict target (Target { serial = serial1, description = description,
21.167 reserved = reserved1, includes = includes1,
21.168 - name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
21.169 + module_alias = module_alias1, symbol_syntax = symbol_syntax1 },
21.170 Target { serial = serial2, description = _,
21.171 reserved = reserved2, includes = includes2,
21.172 - name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
21.173 + module_alias = module_alias2, symbol_syntax = symbol_syntax2 }) =
21.174 if serial1 = serial2 orelse not strict then
21.175 make_target ((serial1, description),
21.176 ((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)),
21.177 - (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
21.178 - Symtab.join (K snd) (module_alias1, module_alias2))
21.179 + (Symtab.join (K snd) (module_alias1, module_alias2),
21.180 + merge_symbol_syntax_data (symbol_syntax1, symbol_syntax2))
21.181 ))
21.182 else
21.183 error ("Incompatible targets: " ^ quote target);
21.184 @@ -161,8 +159,8 @@
21.185 fun the_description (Target { description, ... }) = description;
21.186 fun the_reserved (Target { reserved, ... }) = reserved;
21.187 fun the_includes (Target { includes, ... }) = includes;
21.188 -fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
21.189 fun the_module_alias (Target { module_alias , ... }) = module_alias;
21.190 +fun the_symbol_syntax (Target { symbol_syntax = Symbol_Syntax_Data x, ... }) = x;
21.191
21.192 structure Targets = Theory_Data
21.193 (
21.194 @@ -200,8 +198,8 @@
21.195 thy
21.196 |> (Targets.map o apfst o apfst o Symtab.update)
21.197 (target, make_target ((serial (), seri), (([], Symtab.empty),
21.198 - (mk_name_syntax_table ((Symtab.empty, Symreltab.empty),
21.199 - (Symtab.empty, Symtab.empty)), Symtab.empty))))
21.200 + (Symtab.empty, make_symbol_syntax_data ((Symtab.empty, Symreltab.empty),
21.201 + (Symtab.empty, Symtab.empty))))))
21.202 end;
21.203
21.204 fun add_target (target, seri) = put_target (target, Fundamental seri);
21.205 @@ -220,10 +218,10 @@
21.206 map_target_data target o apsnd o apfst o apfst;
21.207 fun map_includes target =
21.208 map_target_data target o apsnd o apfst o apsnd;
21.209 -fun map_name_syntax target =
21.210 - map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
21.211 fun map_module_alias target =
21.212 - map_target_data target o apsnd o apsnd o apsnd;
21.213 + map_target_data target o apsnd o apsnd o apfst;
21.214 +fun map_symbol_syntax target =
21.215 + map_target_data target o apsnd o apsnd o apsnd o map_symbol_syntax_data;
21.216
21.217 fun set_default_code_width k = (Targets.map o apsnd) (K k);
21.218
21.219 @@ -246,6 +244,23 @@
21.220
21.221 local
21.222
21.223 +fun activate_target_for thy target naming program =
21.224 + let
21.225 + val ((targets, abortable), default_width) = Targets.get thy;
21.226 + fun collapse_hierarchy target =
21.227 + let
21.228 + val data = case Symtab.lookup targets target
21.229 + of SOME data => data
21.230 + | NONE => error ("Unknown code target language: " ^ quote target);
21.231 + in case the_description data
21.232 + of Fundamental _ => (I, data)
21.233 + | Extension (super, modify) => let
21.234 + val (modify', data') = collapse_hierarchy super
21.235 + in (modify' #> modify naming, merge_target false target (data', data)) end
21.236 + end;
21.237 + val (modify, data) = collapse_hierarchy target;
21.238 + in (default_width, abortable, data, modify program) end;
21.239 +
21.240 fun activate_syntax lookup_name src_tab = Symtab.empty
21.241 |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
21.242 of SOME name => (SOME name,
21.243 @@ -263,54 +278,66 @@
21.244 | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
21.245 |>> map_filter I;
21.246
21.247 -fun invoke_serializer thy abortable serializer literals reserved abs_includes
21.248 - module_alias class instance tyco const module_name args naming program2 (names1, presentation_names) width =
21.249 +fun activate_symbol_syntax thy literals naming
21.250 + class_syntax instance_syntax tyco_syntax const_syntax =
21.251 let
21.252 - val (names_class, class') =
21.253 - activate_syntax (Code_Thingol.lookup_class naming) class;
21.254 + val (names_class, class_syntax') =
21.255 + activate_syntax (Code_Thingol.lookup_class naming) class_syntax;
21.256 val names_inst = map_filter (Code_Thingol.lookup_instance naming)
21.257 - (Symreltab.keys instance);
21.258 - val (names_tyco, tyco') =
21.259 - activate_syntax (Code_Thingol.lookup_tyco naming) tyco;
21.260 - val (names_const, (const', _)) =
21.261 - activate_const_syntax thy literals const naming;
21.262 - val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
21.263 + (Symreltab.keys instance_syntax);
21.264 + val (names_tyco, tyco_syntax') =
21.265 + activate_syntax (Code_Thingol.lookup_tyco naming) tyco_syntax;
21.266 + val (names_const, (const_syntax', _)) =
21.267 + activate_const_syntax thy literals const_syntax naming;
21.268 + in
21.269 + (names_class @ names_inst @ names_tyco @ names_const,
21.270 + (class_syntax', tyco_syntax', const_syntax'))
21.271 + end;
21.272 +
21.273 +fun project_program thy abortable names_hidden names1 program2 =
21.274 + let
21.275 val names2 = subtract (op =) names_hidden names1;
21.276 val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
21.277 - val names_all = Graph.all_succs program3 names2;
21.278 - val includes = abs_includes names_all;
21.279 - val program4 = Graph.subgraph (member (op =) names_all) program3;
21.280 + val names4 = Graph.all_succs program3 names2;
21.281 val empty_funs = filter_out (member (op =) abortable)
21.282 (Code_Thingol.empty_funs program3);
21.283 val _ = if null empty_funs then () else error ("No code equations for "
21.284 ^ commas (map (Sign.extern_const thy) empty_funs));
21.285 + val program4 = Graph.subgraph (member (op =) names4) program3;
21.286 + in (names4, program4) end;
21.287 +
21.288 +fun invoke_serializer thy abortable serializer literals reserved abs_includes
21.289 + module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
21.290 + module_name args naming proto_program (names, presentation_names) =
21.291 + let
21.292 + val (names_hidden, (class_syntax, tyco_syntax, const_syntax)) =
21.293 + activate_symbol_syntax thy literals naming
21.294 + proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax;
21.295 + val (names_all, program) = project_program thy abortable names_hidden names proto_program;
21.296 + val includes = abs_includes names_all;
21.297 in
21.298 - serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes
21.299 - (if is_some module_name then K module_name else Symtab.lookup module_alias)
21.300 - (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
21.301 - program4 (names1, presentation_names) width
21.302 + serializer args {
21.303 + labelled_name = Code_Thingol.labelled_name thy proto_program,
21.304 + reserved_syms = reserved,
21.305 + includes = includes,
21.306 + module_alias = if module_name = "" then Symtab.lookup module_alias else K (SOME module_name),
21.307 + class_syntax = Symtab.lookup class_syntax,
21.308 + tyco_syntax = Symtab.lookup tyco_syntax,
21.309 + const_syntax = Symtab.lookup const_syntax,
21.310 + program = program,
21.311 + names = names,
21.312 + presentation_names = presentation_names }
21.313 end;
21.314
21.315 -fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
21.316 +fun mount_serializer thy target some_width raw_module_name args naming proto_program names destination =
21.317 let
21.318 - val ((targets, abortable), default_width) = Targets.get thy;
21.319 - fun collapse_hierarchy target =
21.320 - let
21.321 - val data = case Symtab.lookup targets target
21.322 - of SOME data => data
21.323 - | NONE => error ("Unknown code target language: " ^ quote target);
21.324 - in case the_description data
21.325 - of Fundamental _ => (I, data)
21.326 - | Extension (super, modify) => let
21.327 - val (modify', data') = collapse_hierarchy super
21.328 - in (modify' #> modify naming, merge_target false target (data', data)) end
21.329 - end;
21.330 - val (modify, data) = collapse_hierarchy target;
21.331 - val serializer = the_default (case the_description data
21.332 - of Fundamental seri => #serializer seri) alt_serializer;
21.333 + val (default_width, abortable, data, program) =
21.334 + activate_target_for thy target naming proto_program;
21.335 + val serializer = case the_description data
21.336 + of Fundamental seri => #serializer seri;
21.337 val presentation_names = stmt_names_of_destination destination;
21.338 val module_name = if null presentation_names
21.339 - then raw_module_name else SOME "Code";
21.340 + then raw_module_name else "Code";
21.341 val reserved = the_reserved data;
21.342 fun select_include names_all (name, (content, cs)) =
21.343 if null cs then SOME (name, content)
21.344 @@ -321,36 +348,40 @@
21.345 fun includes names_all = map_filter (select_include names_all)
21.346 ((Symtab.dest o the_includes) data);
21.347 val module_alias = the_module_alias data
21.348 - val { class, instance, tyco, const } = the_name_syntax data;
21.349 + val { class, instance, tyco, const } = the_symbol_syntax data;
21.350 val literals = the_literals thy target;
21.351 val width = the_default default_width some_width;
21.352 in
21.353 invoke_serializer thy abortable serializer literals reserved
21.354 includes module_alias class instance tyco const module_name args
21.355 - naming (modify program) (names, presentation_names) width destination
21.356 + naming program (names, presentation_names) width destination
21.357 end;
21.358
21.359 +fun assert_module_name "" = error ("Empty module name not allowed.")
21.360 + | assert_module_name module_name = module_name;
21.361 +
21.362 in
21.363
21.364 -fun serialize thy = mount_serializer thy NONE;
21.365 +fun export_code_for thy some_path target some_width some_module_name args naming program names =
21.366 + export some_path (mount_serializer thy target some_width some_module_name args naming program names);
21.367
21.368 -fun export_code_for thy some_path target some_width some_module_name args naming program names =
21.369 - file some_path (serialize thy target some_width some_module_name args naming program names);
21.370 +fun produce_code_for thy target some_width module_name args naming program names =
21.371 + produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
21.372
21.373 -fun produce_code_for thy target some_width some_module_name args naming program (names, selects) =
21.374 - string selects (serialize thy target some_width some_module_name args naming program names);
21.375 +fun present_code_for thy target some_width module_name args naming program (names, selects) =
21.376 + present selects (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
21.377
21.378 fun check_code_for thy target strict args naming program names_cs =
21.379 let
21.380 - val module_name = "Code_Test";
21.381 + val module_name = "Code";
21.382 val { env_var, make_destination, make_command } =
21.383 (#check o the_fundamental thy) target;
21.384 val env_param = getenv env_var;
21.385 fun ext_check env_param p =
21.386 let
21.387 val destination = make_destination p;
21.388 - val _ = file (SOME destination) (serialize thy target (SOME 80)
21.389 - (SOME module_name) args naming program names_cs);
21.390 + val _ = export (SOME destination) (mount_serializer thy target (SOME 80)
21.391 + module_name args naming program names_cs);
21.392 val cmd = make_command env_param module_name;
21.393 in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
21.394 then error ("Code check failed for " ^ target ^ ": " ^ cmd)
21.395 @@ -363,24 +394,9 @@
21.396 else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
21.397 end;
21.398
21.399 -fun serialize_custom thy (target_name, seri) module_name naming program names =
21.400 - mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String [])
21.401 - |> the;
21.402 -
21.403 end; (* local *)
21.404
21.405
21.406 -(* code presentation *)
21.407 -
21.408 -fun code_of thy target some_width module_name cs names_stmt =
21.409 - let
21.410 - val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
21.411 - in
21.412 - string (names_stmt naming)
21.413 - (serialize thy target some_width (SOME module_name) [] naming program names_cs)
21.414 - end;
21.415 -
21.416 -
21.417 (* code generation *)
21.418
21.419 fun transitivly_non_empty_funs thy naming program =
21.420 @@ -412,10 +428,15 @@
21.421 fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs)
21.422 ((map o apfst o apsnd) prep_destination seris);
21.423
21.424 -fun produce_code thy cs names_stmt target some_width some_module_name args =
21.425 +fun produce_code thy cs target some_width some_module_name args =
21.426 let
21.427 val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
21.428 - in produce_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end;
21.429 + in produce_code_for thy target some_width some_module_name args naming program names_cs end;
21.430 +
21.431 +fun present_code thy cs names_stmt target some_width some_module_name args =
21.432 + let
21.433 + val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
21.434 + in present_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end;
21.435
21.436 fun check_code thy cs seris =
21.437 let
21.438 @@ -458,21 +479,21 @@
21.439 val change = case some_raw_syn
21.440 of SOME raw_syn => upd (x, prep_syn thy x raw_syn)
21.441 | NONE => del x;
21.442 - in (map_name_syntax target o mapp) change thy end;
21.443 + in (map_symbol_syntax target o mapp) change thy end;
21.444
21.445 -fun gen_add_syntax_class prep_class =
21.446 +fun gen_add_class_syntax prep_class =
21.447 gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class ((K o K) I);
21.448
21.449 -fun gen_add_syntax_inst prep_inst =
21.450 +fun gen_add_instance_syntax prep_inst =
21.451 gen_add_syntax (apfst o apsnd, Symreltab.update, Symreltab.delete_safe) prep_inst ((K o K) I);
21.452
21.453 -fun gen_add_syntax_tyco prep_tyco =
21.454 +fun gen_add_tyco_syntax prep_tyco =
21.455 gen_add_syntax (apsnd o apfst, Symtab.update, Symtab.delete_safe) prep_tyco
21.456 (fn thy => fn tyco => fn syn => if fst syn <> Sign.arity_number thy tyco
21.457 then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
21.458 else syn);
21.459
21.460 -fun gen_add_syntax_const prep_const =
21.461 +fun gen_add_const_syntax prep_const =
21.462 gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const
21.463 (fn thy => fn c => fn syn =>
21.464 if Code_Printer.requires_args syn > Code.args_number thy c
21.465 @@ -501,15 +522,17 @@
21.466 val add_include = gen_add_include (K I);
21.467 val add_include_cmd = gen_add_include Code.read_const;
21.468
21.469 -fun add_module_alias target (thyname, modlname) =
21.470 - let
21.471 - val xs = Long_Name.explode modlname;
21.472 - val xs' = map (Name.desymbolize true) xs;
21.473 - in if xs' = xs
21.474 - then map_module_alias target (Symtab.update (thyname, modlname))
21.475 - else error ("Invalid module name: " ^ quote modlname ^ "\n"
21.476 - ^ "perhaps try " ^ quote (Long_Name.implode xs'))
21.477 - end;
21.478 +fun add_module_alias target (thyname, "") =
21.479 + map_module_alias target (Symtab.delete thyname)
21.480 + | add_module_alias target (thyname, modlname) =
21.481 + let
21.482 + val xs = Long_Name.explode modlname;
21.483 + val xs' = map (Name.desymbolize true) xs;
21.484 + in if xs' = xs
21.485 + then map_module_alias target (Symtab.update (thyname, modlname))
21.486 + else error ("Invalid module name: " ^ quote modlname ^ "\n"
21.487 + ^ "perhaps try " ^ quote (Long_Name.implode xs'))
21.488 + end;
21.489
21.490 fun gen_allow_abort prep_const raw_c thy =
21.491 let
21.492 @@ -536,18 +559,18 @@
21.493
21.494 in
21.495
21.496 -val add_syntax_class = gen_add_syntax_class cert_class;
21.497 -val add_syntax_inst = gen_add_syntax_inst cert_inst;
21.498 -val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
21.499 -val add_syntax_const = gen_add_syntax_const (K I);
21.500 +val add_class_syntax = gen_add_class_syntax cert_class;
21.501 +val add_instance_syntax = gen_add_instance_syntax cert_inst;
21.502 +val add_tyco_syntax = gen_add_tyco_syntax cert_tyco;
21.503 +val add_const_syntax = gen_add_const_syntax (K I);
21.504 val allow_abort = gen_allow_abort (K I);
21.505 val add_reserved = add_reserved;
21.506 val add_include = add_include;
21.507
21.508 -val add_syntax_class_cmd = gen_add_syntax_class read_class;
21.509 -val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
21.510 -val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
21.511 -val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
21.512 +val add_class_syntax_cmd = gen_add_class_syntax read_class;
21.513 +val add_instance_syntax_cmd = gen_add_instance_syntax read_inst;
21.514 +val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco;
21.515 +val add_const_syntax_cmd = gen_add_const_syntax Code.read_const;
21.516 val allow_abort_cmd = gen_allow_abort Code.read_const;
21.517
21.518 fun parse_args f args =
21.519 @@ -568,7 +591,7 @@
21.520 -- ((Parse.$$$ "?" |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP))
21.521 >> (fn seris => check_code_cmd raw_cs seris)
21.522 || Scan.repeat (Parse.$$$ inK |-- Parse.name
21.523 - -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
21.524 + -- Scan.optional (Parse.$$$ module_nameK |-- Parse.name) ""
21.525 -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
21.526 -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
21.527
21.528 @@ -577,23 +600,23 @@
21.529 val _ =
21.530 Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
21.531 process_multi_syntax Parse.xname (Scan.option Parse.string)
21.532 - add_syntax_class_cmd);
21.533 + add_class_syntax_cmd);
21.534
21.535 val _ =
21.536 Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
21.537 process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
21.538 (Scan.option (Parse.minus >> K ()))
21.539 - add_syntax_inst_cmd);
21.540 + add_instance_syntax_cmd);
21.541
21.542 val _ =
21.543 Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
21.544 process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
21.545 - add_syntax_tyco_cmd);
21.546 + add_tyco_syntax_cmd);
21.547
21.548 val _ =
21.549 Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
21.550 process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
21.551 - add_syntax_const_cmd);
21.552 + add_const_syntax_cmd);
21.553
21.554 val _ =
21.555 Outer_Syntax.command "code_reserved" "declare words as reserved for target language"
22.1 --- a/src/Tools/nbe.ML Tue Aug 31 18:38:30 2010 +0200
22.2 +++ b/src/Tools/nbe.ML Wed Sep 01 07:53:31 2010 +0200
22.3 @@ -388,6 +388,7 @@
22.4 in
22.5 s
22.6 |> traced (fn s => "\n--- code to be evaluated:\n" ^ s)
22.7 + |> pair ""
22.8 |> ML_Context.evaluate ctxt (!trace) univs_cookie
22.9 |> (fn f => f deps_vals)
22.10 |> (fn univs => cs ~~ univs)