--- a/.hgignore Mon Jan 27 16:38:52 2014 +0000
+++ b/.hgignore Mon Jan 27 17:13:33 2014 +0000
@@ -5,7 +5,6 @@
*.jar
*.orig
*.rej
-*.pyc
.DS_Store
.swp
--- a/Admin/user-aliases Mon Jan 27 16:38:52 2014 +0000
+++ b/Admin/user-aliases Mon Jan 27 17:13:33 2014 +0000
@@ -1,4 +1,5 @@
lcp paulson
+lp15@cam.ac.uk paulson
norbert.schirmer@web.de schirmer
schirmer@in.tum.de schirmer
urbanc@in.tum.de urbanc
--- a/NEWS Mon Jan 27 16:38:52 2014 +0000
+++ b/NEWS Mon Jan 27 17:13:33 2014 +0000
@@ -40,6 +40,19 @@
*** Pure ***
+* Attributes "where" and "of" allow an optional context of local
+variables ('for' declaration): these variables become schematic in the
+instantiated theorem.
+
+* Obsolete attribute "standard" has been discontinued (legacy since
+Isabelle2012). Potential INCOMPATIBILITY, use explicit 'for' context
+where instantiations with schematic variables are intended (for
+declaration commands like 'lemmas' or attributes like "of"). The
+following temporary definition may help to port old applications:
+
+ attribute_setup standard =
+ "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
+
* More thorough check of proof context for goal statements and
attributed fact expressions (concerning background theory, declared
hyps). Potential INCOMPATIBILITY, tools need to observe standard
@@ -53,6 +66,9 @@
*** HOL ***
+* Simproc "finite_Collect" is no longer enabled by default, due to
+spurious crashes and other surprises. Potential INCOMPATIBILITY.
+
* Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
"primrec_new", "primcorec", and "primcorecursive" command are now part of
@@ -266,6 +282,13 @@
*** ML ***
+* Proper context discipline for read_instantiate and instantiate_tac:
+variables that are meant to become schematic need to be given as
+fixed, and are generalized by the explicit context of local variables.
+This corresponds to Isar attributes "where" and "of" with 'for'
+declaration. INCOMPATIBILITY, also due to potential change of indices
+of schematic variables.
+
* Toplevel function "use" refers to raw ML bootstrap environment,
without Isar context nor antiquotations. Potential INCOMPATIBILITY.
Note that 'ML_file' is the canonical command to load ML files into the
--- a/src/Doc/Codegen/Adaptation.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Doc/Codegen/Adaptation.thy Mon Jan 27 17:13:33 2014 +0000
@@ -2,8 +2,8 @@
imports Setup
begin
-setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", K I))
- #> Code_Target.extend_target ("\<SMLdummy>", ("Haskell", K I)) *}
+setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", I))
+ #> Code_Target.extend_target ("\<SMLdummy>", ("Haskell", I)) *}
section {* Adaptation to target languages \label{sec:adaptation} *}
--- a/src/Doc/IsarRef/Generic.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Doc/IsarRef/Generic.thy Mon Jan 27 17:13:33 2014 +0000
@@ -132,7 +132,6 @@
@{attribute_def abs_def} & : & @{text attribute} \\[0.5ex]
@{attribute_def rotated} & : & @{text attribute} \\
@{attribute_def (Pure) elim_format} & : & @{text attribute} \\
- @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
@{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
\end{matharray}
@@ -180,11 +179,6 @@
Note that the Classical Reasoner (\secref{sec:classical}) provides
its own version of this operation.
- \item @{attribute standard} puts a theorem into the standard form of
- object-rules at the outermost theory level. Note that this
- operation violates the local proof context (including active
- locales).
-
\item @{attribute no_vars} replaces schematic variables by free
ones; this is mainly for tuning output of pretty printed theorems.
--- a/src/Doc/IsarRef/Proof.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Doc/IsarRef/Proof.thy Mon Jan 27 17:13:33 2014 +0000
@@ -721,11 +721,13 @@
;
@@{attribute OF} @{syntax thmrefs}
;
- @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})?
+ @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? \<newline>
+ (@'for' (@{syntax vars} + @'and'))?
;
@@{attribute "where"}
((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '='
- (@{syntax type} | @{syntax term}) * @'and')
+ (@{syntax type} | @{syntax term}) * @'and') \<newline>
+ (@'for' (@{syntax vars} + @'and'))?
\<close>}
\begin{description}
@@ -812,6 +814,10 @@
left to right; ``@{text _}'' (underscore) indicates to skip a
position. Arguments following a ``@{text "concl:"}'' specification
refer to positions of the conclusion of a rule.
+
+ An optional context of local variables @{text "\<FOR> x\<^sub>1 \<dots> x\<^sub>m"} may
+ be specified: the instantiated theorem is exported, and these
+ variables become schematic (usually with some shifting of indices).
\item @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n"}
performs named instantiation of schematic type and term variables
@@ -821,6 +827,9 @@
As type instantiations are inferred from term instantiations,
explicit type instantiations are seldom necessary.
+ An optional context of local variables @{text "\<FOR> x\<^sub>1 \<dots> x\<^sub>m"} may
+ be specified as for @{attribute "of"} above.
+
\end{description}
*}
--- a/src/Doc/Tutorial/Protocol/Event.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Doc/Tutorial/Protocol/Event.thy Mon Jan 27 17:13:33 2014 +0000
@@ -93,7 +93,7 @@
(*Simplifying
parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
This version won't loop with the simplifier.*)
-lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
+lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
lemma knows_Spy_Says [simp]:
"knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
@@ -256,7 +256,7 @@
knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
-lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
+lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
ML
{*
@@ -290,7 +290,7 @@
subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
-lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
+lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs
ML
{*
--- a/src/Doc/Tutorial/Protocol/Message.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Doc/Tutorial/Protocol/Message.thy Mon Jan 27 17:13:33 2014 +0000
@@ -190,7 +190,7 @@
lemma parts_increasing: "H \<subseteq> parts(H)"
by blast
-lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
lemma parts_empty [simp]: "parts{} = {}"
apply safe
@@ -388,9 +388,9 @@
apply (erule analz.induct, blast+)
done
-lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
-lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
lemma parts_analz [simp]: "parts (analz H) = parts H"
@@ -404,7 +404,7 @@
apply (erule analz.induct, auto)
done
-lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
subsubsection{*General equational properties *}
@@ -786,21 +786,23 @@
text{*Rewrites to push in Key and Crypt messages, so that other messages can
be pulled out using the @{text analz_insert} rules*}
-lemmas pushKeys [standard] =
+lemmas pushKeys =
insert_commute [of "Key K" "Agent C"]
insert_commute [of "Key K" "Nonce N"]
insert_commute [of "Key K" "Number N"]
insert_commute [of "Key K" "Hash X"]
insert_commute [of "Key K" "MPair X Y"]
insert_commute [of "Key K" "Crypt X K'"]
+ for K C N X Y K'
-lemmas pushCrypts [standard] =
+lemmas pushCrypts =
insert_commute [of "Crypt X K" "Agent C"]
insert_commute [of "Crypt X K" "Agent C"]
insert_commute [of "Crypt X K" "Nonce N"]
insert_commute [of "Crypt X K" "Number N"]
insert_commute [of "Crypt X K" "Hash X'"]
insert_commute [of "Crypt X K" "MPair X' Y"]
+ for X K C N X' Y
text{*Cannot be added with @{text "[simp]"} -- messages should not always be
re-ordered. *}
--- a/src/Doc/isar.sty Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Doc/isar.sty Mon Jan 27 17:13:33 2014 +0000
@@ -11,6 +11,7 @@
\newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}
\newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}}
+\newcommand{\isasymFOR}{\isakeyword{for}}
\newcommand{\isasymAND}{\isakeyword{and}}
\newcommand{\isasymIS}{\isakeyword{is}}
\newcommand{\isasymWHERE}{\isakeyword{where}}
--- a/src/HOL/Bali/AxExample.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Bali/AxExample.thy Mon Jan 27 17:13:33 2014 +0000
@@ -41,9 +41,10 @@
declare lvar_def [simp]
ML {*
-fun inst1_tac ctxt s t st =
- case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
- SOME i => instantiate_tac ctxt [((s, i), t)] st | NONE => Seq.empty;
+fun inst1_tac ctxt s t xs st =
+ (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
+ SOME i => Rule_Insts.instantiate_tac ctxt [((s, i), t)] xs st
+ | NONE => Seq.empty);
val ax_tac =
REPEAT o rtac allI THEN'
@@ -64,7 +65,7 @@
apply (tactic "ax_tac 1" (* Try *))
defer
apply (tactic {* inst1_tac @{context} "Q"
- "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})
+ "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" [] *})
prefer 2
apply simp
apply (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
@@ -83,7 +84,7 @@
apply (tactic "ax_tac 1" (* AVar *))
prefer 2
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (?PP a\<leftarrow>?x)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *})
apply (simp del: avar_def2 peek_and_def2)
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
@@ -124,7 +125,7 @@
apply (tactic "ax_tac 1") (* Ass *)
prefer 2
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. PP a vs l vf\<leftarrow>x \<and>. p" ["PP", "x", "p"] *})
apply (rule allI)
apply (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1 *})
apply (rule ax_derivs.Abrupt)
@@ -132,17 +133,17 @@
apply (tactic "ax_tac 1" (* FVar *))
apply (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
apply (tactic "ax_tac 1")
-apply (tactic {* inst1_tac @{context} "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" *})
+apply (tactic {* inst1_tac @{context} "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" [] *})
apply fastforce
prefer 4
apply (rule ax_derivs.Done [THEN conseq1],force)
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (?PP a\<leftarrow>?x)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *})
apply (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply)
apply (tactic "ax_tac 1")
prefer 2
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>aa v. Normal (QQ aa v\<leftarrow>y)" ["QQ", "y"] *})
apply (simp del: peek_and_def2 heap_free_def2 normal_def2)
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
@@ -161,7 +162,7 @@
apply (tactic "ax_tac 1")
defer
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (?PP vf \<and>. ?p)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (PP vf \<and>. p)" ["PP", "p"] *})
apply (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2)
apply (tactic "ax_tac 1" (* NewC *))
apply (tactic "ax_tac 1" (* ax_Alloc *))
@@ -189,18 +190,18 @@
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
apply (rule_tac [2] ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (P vf l vfa)" ["P"] *})
apply (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
apply (tactic "ax_tac 2" (* NewA *))
apply (tactic "ax_tac 3" (* ax_Alloc_Arr *))
apply (tactic "ax_tac 3")
-apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
+apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (P vf l vfa\<leftarrow>\<diamondsuit>)" ["P"] *})
apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 2 *})
apply (tactic "ax_tac 2")
apply (tactic "ax_tac 1" (* FVar *))
apply (tactic "ax_tac 2" (* StatRef *))
apply (rule ax_derivs.Done [THEN conseq1])
-apply (tactic {* inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" *})
+apply (tactic {* inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" [] *})
apply (clarsimp split del: split_if)
apply (frule atleast_free_weaken [THEN atleast_free_weaken])
apply (drule initedD)
@@ -210,9 +211,9 @@
apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
apply (rule wf_tprg)
apply clarsimp
-apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *})
+apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" [] *})
apply clarsimp
-apply (tactic {* inst1_tac @{context} "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" *})
+apply (tactic {* inst1_tac @{context} "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" [] *})
apply clarsimp
(* end init *)
apply (rule conseq1)
@@ -244,7 +245,7 @@
apply clarsimp
apply (tactic "ax_tac 1" (* If *))
apply (tactic
- {* inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
+ {* inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" [] *})
apply (tactic "ax_tac 1")
apply (rule conseq1)
apply (tactic "ax_tac 1")
@@ -265,7 +266,7 @@
apply (tactic "ax_tac 1")
prefer 2
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" [] *})
apply (rule allI)
apply (rule_tac P' = "Normal ?P" in conseq1)
prefer 2
--- a/src/HOL/Bali/Basis.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Bali/Basis.thy Mon Jan 27 17:13:33 2014 +0000
@@ -179,9 +179,11 @@
where "the_In1r \<equiv> the_Inr \<circ> the_In1"
ML {*
-fun sum3_instantiate ctxt thm = map (fn s =>
- simplify (ctxt delsimps [@{thm not_None_eq}])
- (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
+fun sum3_instantiate ctxt thm =
+ map (fn s =>
+ simplify (ctxt delsimps @{thms not_None_eq})
+ (Rule_Insts.read_instantiate ctxt [(("t", 0), "In" ^ s ^ " x")] ["x"] thm))
+ ["1l","2","3","1r"]
*}
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
--- a/src/HOL/IMP/Hoare_Total.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/IMP/Hoare_Total.thy Mon Jan 27 17:13:33 2014 +0000
@@ -209,4 +209,7 @@
apply(auto simp: hoare_tvalid_def wpt_def)
done
+corollary hoaret_sound_complete: "\<turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> \<Turnstile>\<^sub>t {P}c{Q}"
+by (metis hoaret_sound hoaret_complete)
+
end
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jan 27 17:13:33 2014 +0000
@@ -671,25 +671,17 @@
open Code_Thingol;
-fun imp_program naming =
+val imp_program =
let
- fun is_const c = case lookup_const naming c
- of SOME c' => (fn c'' => c' = c'')
- | NONE => K false;
- val is_bind = is_const @{const_name bind};
- val is_return = is_const @{const_name return};
+ val is_bind = curry (op =) @{const_name bind};
+ val is_return = curry (op =) @{const_name return};
val dummy_name = "";
val dummy_case_term = IVar NONE;
(*assumption: dummy values are not relevant for serialization*)
- val (unitt, unitT) = case lookup_const naming @{const_name Unity}
- of SOME unit' =>
- let
- val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
- in
- (IConst { name = unit', typargs = [], dicts = [], dom = [],
- range = unitT, annotate = false }, unitT)
- end
- | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
+ val unitT = @{type_name unit} `%% [];
+ val unitt =
+ IConst { sym = Code_Symbol.Constant @{const_name Unity}, typargs = [], dicts = [], dom = [],
+ range = unitT, annotate = false };
fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
| dest_abs (t, ty) =
let
@@ -697,7 +689,7 @@
val v = singleton (Name.variant_list vs) "x";
val ty' = (hd o fst o unfold_fun) ty;
in ((SOME v, ty'), t `$ IVar (SOME v)) end;
- fun force (t as IConst { name = c, ... } `$ t') = if is_return c
+ fun force (t as IConst { sym = Code_Symbol.Constant c, ... } `$ t') = if is_return c
then t' else t `$ unitt
| force t = t `$ unitt;
fun tr_bind'' [(t1, _), (t2, ty2)] =
@@ -705,13 +697,13 @@
val ((v, ty), t) = dest_abs (t2, ty2);
in ICase { term = force t1, typ = ty, clauses = [(IVar v, tr_bind' t)], primitive = dummy_case_term } end
and tr_bind' t = case unfold_app t
- of (IConst { name = c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c
+ of (IConst { sym = Code_Symbol.Constant c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c
then tr_bind'' [(x1, ty1), (x2, ty2)]
else force t
| _ => force t;
fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=>
ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term }
- fun imp_monad_bind' (const as { name = c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
+ fun imp_monad_bind' (const as { sym = Code_Symbol.Constant c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
| ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
| (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
@@ -726,7 +718,7 @@
ICase { term = imp_monad_bind t, typ = ty,
clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
- in (Graph.map o K o map_terms_stmt) imp_monad_bind end;
+ in (Code_Symbol.Graph.map o K o map_terms_stmt) imp_monad_bind end;
in
--- a/src/HOL/Library/Binomial.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Library/Binomial.thy Mon Jan 27 17:13:33 2014 +0000
@@ -131,7 +131,7 @@
prefer 4 apply (force simp add: constr_bij)
prefer 3 apply force
prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
- finite_subset [of _ "Pow (insert x F)", standard])
+ finite_subset [of _ "Pow (insert x F)" for F])
apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
done
qed
--- a/src/HOL/Library/Numeral_Type.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Library/Numeral_Type.thy Mon Jan 27 17:13:33 2014 +0000
@@ -284,8 +284,8 @@
lemmas bit0_iszero_numeral [simp] = bit0.iszero_numeral
lemmas bit1_iszero_numeral [simp] = bit1.iszero_numeral
-declare eq_numeral_iff_iszero [where 'a="('a::finite) bit0", standard, simp]
-declare eq_numeral_iff_iszero [where 'a="('a::finite) bit1", standard, simp]
+lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit0"] for dummy :: "'a::finite"
+lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit1"] for dummy :: "'a::finite"
subsection {* Order instances *}
--- a/src/HOL/List.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/List.thy Mon Jan 27 17:13:33 2014 +0000
@@ -6304,7 +6304,7 @@
signature LIST_CODE =
sig
- val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
+ val implode_list: Code_Thingol.iterm -> Code_Thingol.iterm list option
val default_list: int * string
-> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
-> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
@@ -6316,16 +6316,13 @@
open Basic_Code_Thingol;
-fun implode_list nil' cons' t =
+fun implode_list t =
let
- fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
- if c = cons'
- then SOME (t1, t2)
- else NONE
+ fun dest_cons (IConst { sym = Code_Symbol.Constant @{const_name Cons}, ... } `$ t1 `$ t2) = SOME (t1, t2)
| dest_cons _ = NONE;
val (ts, t') = Code_Thingol.unfoldr dest_cons t;
in case t'
- of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
+ of IConst { sym = Code_Symbol.Constant @{const_name Nil}, ... } => SOME ts
| _ => NONE
end;
@@ -6338,15 +6335,15 @@
fun add_literal_list target =
let
- fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
- case Option.map (cons t1) (implode_list nil' cons' t2)
+ fun pretty literals pr _ vars fxy [(t1, _), (t2, _)] =
+ case Option.map (cons t1) (implode_list t2)
of SOME ts =>
Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
| NONE =>
default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
in
Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
- [(target, SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))]))
+ [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
end
end;
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Jan 27 17:13:33 2014 +0000
@@ -1514,8 +1514,7 @@
assume i: "i \<in> Basis"
have "norm (\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le>
norm ((\<Sum>x\<in>P \<inter> - {x. f x \<bullet> i < 0}. f x) \<bullet> i) + norm ((\<Sum>x\<in>P \<inter> {x. f x \<bullet> i < 0}. f x) \<bullet> i)"
- by (simp add: abs_real_def setsum_cases[OF fP] setsum_negf uminus_add_conv_diff
- norm_triangle_ineq4 inner_setsum_left del: real_norm_def)
+ by (simp add: abs_real_def setsum_cases[OF fP] setsum_negf norm_triangle_ineq4 inner_setsum_left del: real_norm_def)
also have "\<dots> \<le> e + e"
unfolding real_norm_def
by (intro add_mono norm_bound_Basis_le i fPs) auto
--- a/src/HOL/Number_Theory/Binomial.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Number_Theory/Binomial.thy Mon Jan 27 17:13:33 2014 +0000
@@ -133,7 +133,7 @@
prefer 4 apply (force simp add: constr_bij)
prefer 3 apply force
prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
- finite_subset [of _ "Pow (insert x F)", standard])
+ finite_subset [of _ "Pow (insert x F)" for F])
apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
done
qed
@@ -669,7 +669,9 @@
have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
using assms by(auto intro!: inj_onI)
moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}"
- using assms by(auto intro!: rev_image_eqI[where x="(card a, a)", standard] simp add: card_gt_0_iff[folded Suc_le_eq] dest: finite_subset intro: card_mono)
+ using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a]
+ simp add: card_gt_0_iff[folded Suc_le_eq]
+ dest: finite_subset intro: card_mono)
ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). -1 ^ (i + 1))"
by(rule setsum_reindex_cong[where f=snd]) fastforce
also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. -1 ^ (i + 1)))"
--- a/src/HOL/Prolog/prolog.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Prolog/prolog.ML Mon Jan 27 17:13:33 2014 +0000
@@ -49,14 +49,16 @@
fun check_HOHH thm = (if isD (concl_of thm) andalso forall isG (prems_of thm)
then thm else raise not_HOHH);
-fun atomizeD ctxt thm = let
+fun atomizeD ctxt thm =
+ let
fun at thm = case concl_of thm of
- _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
- (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
+ _$(Const(@{const_name All} ,_)$Abs(s,_,_))=>
+ let val s' = if s="P" then "PP" else s
+ in at(thm RS (Rule_Insts.read_instantiate ctxt [(("x", 0), s')] [s'] spec)) end
| _$(Const(@{const_name HOL.conj},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
| _$(Const(@{const_name HOL.implies},_)$_$_) => at(thm RS mp)
| _ => [thm]
-in map zero_var_indexes (at thm) end;
+ in map zero_var_indexes (at thm) end;
val atomize_ss =
(empty_simpset @{context} |> Simplifier.set_mksimps (mksimps mksimps_pairs))
--- a/src/HOL/Quickcheck_Narrowing.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Quickcheck_Narrowing.thy Mon Jan 27 17:13:33 2014 +0000
@@ -11,7 +11,7 @@
subsubsection {* Code generation setup *}
-setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *}
+setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, I)) *}
code_printing
type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
--- a/src/HOL/Quickcheck_Random.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Quickcheck_Random.thy Mon Jan 27 17:13:33 2014 +0000
@@ -9,7 +9,7 @@
notation fcomp (infixl "\<circ>>" 60)
notation scomp (infixl "\<circ>\<rightarrow>" 60)
-setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *}
+setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, I)) *}
subsection {* Catching Match exceptions *}
--- a/src/HOL/Rat.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Rat.thy Mon Jan 27 17:13:33 2014 +0000
@@ -622,8 +622,8 @@
(* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
#> Lin_Arith.add_simps [@{thm neg_less_iff_less},
@{thm True_implies_equals},
- read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left},
- read_instantiate @{context} [(("a", 0), "(- numeral ?v)")] @{thm distrib_left},
+ @{thm distrib_left [where a = "numeral v" for v]},
+ @{thm distrib_left [where a = "- numeral v" for v]},
@{thm divide_1}, @{thm divide_zero_left},
@{thm times_divide_eq_right}, @{thm times_divide_eq_left},
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
--- a/src/HOL/Set.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Set.thy Mon Jan 27 17:13:33 2014 +0000
@@ -1577,10 +1577,10 @@
by (auto simp add: Pow_def)
lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
- by (blast intro: image_eqI [where ?x = "u - {a}", standard])
+ by (blast intro: image_eqI [where ?x = "u - {a}" for u])
lemma Pow_Compl: "Pow (- A) = {-B | B. A \<in> Pow B}"
- by (blast intro: exI [where ?x = "- u", standard])
+ by (blast intro: exI [where ?x = "- u" for u])
lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"
by blast
--- a/src/HOL/Set_Interval.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Set_Interval.thy Mon Jan 27 17:13:33 2014 +0000
@@ -728,7 +728,7 @@
qed auto
lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}"
-by(auto intro!: image_eqI[where x="nat x", standard])
+ by (auto intro!: image_eqI [where x = "nat x" for x])
context ordered_ab_group_add
begin
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Jan 27 17:13:33 2014 +0000
@@ -309,9 +309,9 @@
fun dynamic_value_strict opts cookie thy postproc t =
let
val ctxt = Proof_Context.init_global thy
- fun evaluator naming program ((_, vs_ty), t) deps =
+ fun evaluator program ((_, vs_ty), t) deps =
Exn.interruptible_capture (value opts ctxt cookie)
- (Code_Target.evaluator thy target naming program deps (vs_ty, t));
+ (Code_Target.evaluator thy target program deps (vs_ty, t));
in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
(** counterexample generator **)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jan 27 17:13:33 2014 +0000
@@ -416,7 +416,7 @@
|> hackish_string_of_term ctxt
in
((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
- stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
+ stature), th |> Rule_Insts.read_instantiate ctxt [((p_name, 0), p_inst)] [])
end
fun type_match thy (T1, T2) =
--- a/src/HOL/Tools/TFL/post.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Tools/TFL/post.ML Mon Jan 27 17:13:33 2014 +0000
@@ -130,7 +130,7 @@
rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
(*Strip off the outer !P*)
-val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
+val spec'= Rule_Insts.read_instantiate @{context} [(("x", 0), "P::'b=>bool")] [] spec;
fun tracing true _ = ()
| tracing false msg = writeln msg;
--- a/src/HOL/Tools/numeral.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Tools/numeral.ML Mon Jan 27 17:13:33 2014 +0000
@@ -67,23 +67,20 @@
fun add_code number_of negative print target thy =
let
- fun dest_numeral one' bit0' bit1' thm t =
+ fun dest_numeral thm t =
let
- fun dest_bit (IConst { name = c, ... }) = if c = bit0' then 0
- else if c = bit1' then 1
- else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
+ fun dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... }) = 0
+ | dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... }) = 1
| dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
- fun dest_num (IConst { name = c, ... }) = if c = one' then 1
- else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
+ fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = 1
| dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
| dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
in if negative then ~ (dest_num t) else dest_num t end;
- fun pretty literals [one', bit0', bit1'] _ thm _ _ [(t, _)] =
- (Code_Printer.str o print literals o dest_numeral one' bit0' bit1' thm) t;
+ fun pretty literals _ thm _ _ [(t, _)] =
+ (Code_Printer.str o print literals o dest_numeral thm) t;
in
thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
- [(target, SOME (Code_Printer.complex_const_syntax
- (1, ([@{const_name Num.One}, @{const_name Num.Bit0}, @{const_name Num.Bit1}], pretty))))]))
+ [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
end;
end; (*local*)
--- a/src/HOL/Tools/string_code.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/Tools/string_code.ML Mon Jan 27 17:13:33 2014 +0000
@@ -16,28 +16,6 @@
open Basic_Code_Thingol;
-fun decode_char nibbles' tt =
- let
- fun idx c = find_index (curry (op =) c) nibbles';
- fun decode ~1 _ = NONE
- | decode _ ~1 = NONE
- | decode n m = SOME (chr (n * 16 + m));
- in case tt
- of (IConst { name = c1, ... }, IConst { name = c2, ... }) => decode (idx c1) (idx c2)
- | _ => NONE
- end;
-
-fun implode_string literals char' nibbles' ts =
- let
- fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) =
- if c = char' then decode_char nibbles' (t1, t2) else NONE
- | implode_char _ = NONE;
- val ts' = map_filter implode_char ts;
- in if length ts = length ts'
- then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode) ts'
- else NONE
- end;
-
val cs_nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
@{const_name Nibble2}, @{const_name Nibble3},
@{const_name Nibble4}, @{const_name Nibble5},
@@ -46,13 +24,34 @@
@{const_name NibbleA}, @{const_name NibbleB},
@{const_name NibbleC}, @{const_name NibbleD},
@{const_name NibbleE}, @{const_name NibbleF}];
-val cs_summa = [@{const_name Nil}, @{const_name Cons}, @{const_name Char}] @ cs_nibbles;
+
+fun decode_char tt =
+ let
+ fun idx c = find_index (curry (op =) c) cs_nibbles;
+ fun decode ~1 _ = NONE
+ | decode _ ~1 = NONE
+ | decode n m = SOME (chr (n * 16 + m));
+ in case tt
+ of (IConst { sym = Code_Symbol.Constant c1, ... }, IConst { sym = Code_Symbol.Constant c2, ... }) => decode (idx c1) (idx c2)
+ | _ => NONE
+ end;
+
+fun implode_string literals ts =
+ let
+ fun implode_char (IConst { sym = Code_Symbol.Constant @{const_name Char}, ... } `$ t1 `$ t2) =
+ decode_char (t1, t2)
+ | implode_char _ = NONE;
+ val ts' = map_filter implode_char ts;
+ in if length ts = length ts'
+ then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode) ts'
+ else NONE
+ end;
fun add_literal_list_string target =
let
- fun pretty literals (nil' :: cons' :: char' :: nibbles') pr _ vars fxy [(t1, _), (t2, _)] =
- case Option.map (cons t1) (List_Code.implode_list nil' cons' t2)
- of SOME ts => (case implode_string literals char' nibbles' ts
+ fun pretty literals pr _ vars fxy [(t1, _), (t2, _)] =
+ case Option.map (cons t1) (List_Code.implode_list t2)
+ of SOME ts => (case implode_string literals ts
of SOME p => p
| NONE =>
Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
@@ -60,31 +59,31 @@
List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
in
Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
- [(target, SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))]))
+ [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
end;
fun add_literal_char target =
let
- fun pretty literals nibbles' _ thm _ _ [(t1, _), (t2, _)] =
- case decode_char nibbles' (t1, t2)
+ fun pretty literals _ thm _ _ [(t1, _), (t2, _)] =
+ case decode_char (t1, t2)
of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
| NONE => Code_Printer.eqn_error thm "Illegal character expression";
in
Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
- [(target, SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))]))
+ [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
end;
fun add_literal_string target =
let
- fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
- case List_Code.implode_list nil' cons' t
- of SOME ts => (case implode_string literals char' nibbles' ts
+ fun pretty literals _ thm _ _ [(t, _)] =
+ case List_Code.implode_list t
+ of SOME ts => (case implode_string literals ts
of SOME p => p
- | NONE => Code_Printer.eqn_error thm "Illegal message expression")
- | NONE => Code_Printer.eqn_error thm "Illegal message expression";
+ | NONE => Code_Printer.eqn_error thm "Illegal string literal expression")
+ | NONE => Code_Printer.eqn_error thm "Illegal string literal expression";
in
Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
- [(target, SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))]))
+ [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
end;
end;
--- a/src/HOL/ex/Cartouche_Examples.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/HOL/ex/Cartouche_Examples.thy Mon Jan 27 17:13:33 2014 +0000
@@ -52,35 +52,35 @@
end;
*}
-syntax "_STR_cartouche" :: "cartouche_position \<Rightarrow> string" ("STR _")
+syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> string" ("_")
parse_translation {*
- [(@{syntax_const "_STR_cartouche"},
+ [(@{syntax_const "_cartouche_string"},
K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]
*}
-term "STR \<open>\<close>"
-term "STR \<open>abc\<close>"
-term "STR \<open>abc\<close> @ STR \<open>xyz\<close>"
-term "STR \<open>\<newline>\<close>"
-term "STR \<open>\001\010\100\<close>"
+term "\<open>\<close>"
+term "\<open>abc\<close>"
+term "\<open>abc\<close> @ \<open>xyz\<close>"
+term "\<open>\<newline>\<close>"
+term "\<open>\001\010\100\<close>"
subsection {* Alternate outer and inner syntax: string literals *}
subsubsection {* Nested quotes *}
-syntax "_STR_string" :: "string_position \<Rightarrow> string" ("STR _")
+syntax "_string_string" :: "string_position \<Rightarrow> string" ("_")
parse_translation {*
- [(@{syntax_const "_STR_string"}, K (string_tr Lexicon.explode_string))]
+ [(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))]
*}
-term "STR \"\""
-term "STR \"abc\""
-term "STR \"abc\" @ STR \"xyz\""
-term "STR \"\<newline>\""
-term "STR \"\001\010\100\""
+term "\"\""
+term "\"abc\""
+term "\"abc\" @ \"xyz\""
+term "\"\<newline>\""
+term "\"\001\010\100\""
subsubsection {* Term cartouche and regular quotes *}
@@ -95,11 +95,11 @@
in writeln (Syntax.string_of_term ctxt t) end)))
*}
-term_cartouche \<open>STR ""\<close>
-term_cartouche \<open>STR "abc"\<close>
-term_cartouche \<open>STR "abc" @ STR "xyz"\<close>
-term_cartouche \<open>STR "\<newline>"\<close>
-term_cartouche \<open>STR "\001\010\100"\<close>
+term_cartouche \<open>""\<close>
+term_cartouche \<open>"abc"\<close>
+term_cartouche \<open>"abc" @ "xyz"\<close>
+term_cartouche \<open>"\<newline>"\<close>
+term_cartouche \<open>"\001\010\100"\<close>
subsubsection {* Further nesting: antiquotations *}
@@ -125,22 +125,22 @@
*}
ML {*
- @{term_cartouche \<open>STR ""\<close>};
- @{term_cartouche \<open>STR "abc"\<close>};
- @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
- @{term_cartouche \<open>STR "\<newline>"\<close>};
- @{term_cartouche \<open>STR "\001\010\100"\<close>};
+ @{term_cartouche \<open>""\<close>};
+ @{term_cartouche \<open>"abc"\<close>};
+ @{term_cartouche \<open>"abc" @ "xyz"\<close>};
+ @{term_cartouche \<open>"\<newline>"\<close>};
+ @{term_cartouche \<open>"\001\010\100"\<close>};
*}
text {*
@{ML_cartouche
\<open>
(
- @{term_cartouche \<open>STR ""\<close>};
- @{term_cartouche \<open>STR "abc"\<close>};
- @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
- @{term_cartouche \<open>STR "\<newline>"\<close>};
- @{term_cartouche \<open>STR "\001\010\100"\<close>}
+ @{term_cartouche \<open>""\<close>};
+ @{term_cartouche \<open>"abc"\<close>};
+ @{term_cartouche \<open>"abc" @ "xyz"\<close>};
+ @{term_cartouche \<open>"\<newline>"\<close>};
+ @{term_cartouche \<open>"\001\010\100"\<close>}
)
\<close>
}
@@ -160,11 +160,11 @@
@{ML_cartouche
\<open>
(
- @{term_cartouche \<open>STR ""\<close>};
- @{term_cartouche \<open>STR "abc"\<close>};
- @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
- @{term_cartouche \<open>STR "\<newline>"\<close>};
- @{term_cartouche \<open>STR "\001\010\100"\<close>}
+ @{term_cartouche \<open>""\<close>};
+ @{term_cartouche \<open>"abc"\<close>};
+ @{term_cartouche \<open>"abc" @ "xyz"\<close>};
+ @{term_cartouche \<open>"\<newline>"\<close>};
+ @{term_cartouche \<open>"\001\010\100"\<close>}
)
\<close>
}
--- a/src/Pure/General/graph.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Pure/General/graph.ML Mon Jan 27 17:13:33 2014 +0000
@@ -27,7 +27,6 @@
val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T)) (*exception UNDEF*)
val get_node: 'a T -> key -> 'a (*exception UNDEF*)
val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
- val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
val map: (key -> 'a -> 'b) -> 'a T -> 'b T
val imm_preds: 'a T -> key -> Keys.T
val imm_succs: 'a T -> key -> Keys.T
@@ -122,10 +121,6 @@
fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab);
-fun map_entry_yield x f (G as Graph tab) =
- let val (a, node') = f (#2 (get_entry G x))
- in (a, Graph (Table.update (x, node') tab)) end;
-
(* nodes *)
@@ -133,9 +128,6 @@
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
-fun map_node_yield x f = map_entry_yield x (fn (i, ps) =>
- let val (a, i') = f i in (a, (i', ps)) end);
-
fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);
--- a/src/Pure/Isar/args.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Pure/Isar/args.ML Mon Jan 27 17:13:33 2014 +0000
@@ -53,6 +53,7 @@
val typ_abbrev: typ context_parser
val typ: typ context_parser
val term: term context_parser
+ val term_pattern: term context_parser
val term_abbrev: term context_parser
val prop: term context_parser
val type_name: bool -> string context_parser
@@ -198,6 +199,7 @@
val typ_abbrev = Scan.peek (named_typ o Proof_Context.read_typ_abbrev o Context.proof_of);
val typ = Scan.peek (named_typ o Syntax.read_typ o Context.proof_of);
val term = Scan.peek (named_term o Syntax.read_term o Context.proof_of);
+val term_pattern = Scan.peek (named_term o Proof_Context.read_term_pattern o Context.proof_of);
val term_abbrev = Scan.peek (named_term o Proof_Context.read_term_abbrev o Context.proof_of);
val prop = Scan.peek (named_term o Syntax.read_prop o Context.proof_of);
--- a/src/Pure/Isar/attrib.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Pure/Isar/attrib.ML Mon Jan 27 17:13:33 2014 +0000
@@ -37,6 +37,7 @@
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
theory -> theory
+ val internal: (morphism -> attribute) -> src
val add_del: attribute -> attribute -> attribute context_parser
val thm_sel: Facts.interval list parser
val thm: thm context_parser
@@ -45,7 +46,6 @@
val partial_evaluation: Proof.context ->
(binding * (thm list * Args.src list) list) list ->
(binding * (thm list * Args.src list) list) list
- val internal: (morphism -> attribute) -> src
val print_options: Proof.context -> unit
val config_bool: Binding.binding ->
(Context.generic -> bool) -> bool Config.T * (theory -> theory)
@@ -194,6 +194,15 @@
ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
+(* internal attribute *)
+
+fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
+
+val _ = Theory.setup
+ (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
+ "internal attribute");
+
+
(* add/del syntax *)
fun add_del add del = Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add);
@@ -318,119 +327,6 @@
-(** basic attributes **)
-
-(* internal *)
-
-fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
-
-
-(* rule composition *)
-
-val THEN_att =
- Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
- >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)));
-
-val OF_att =
- thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A));
-
-
-(* rename_abs *)
-
-val rename_abs =
- Scan.repeat (Args.maybe Args.name)
- >> (fn args => Thm.rule_attribute (K (Drule.rename_bvars' args)));
-
-
-(* unfold / fold definitions *)
-
-fun unfolded_syntax rule =
- thms >> (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths));
-
-val unfolded = unfolded_syntax Local_Defs.unfold;
-val folded = unfolded_syntax Local_Defs.fold;
-
-
-(* rule format *)
-
-fun rule_format true = Object_Logic.rule_format_no_asm
- | rule_format false = Object_Logic.rule_format;
-
-val elim_format = Thm.rule_attribute (K Tactic.make_elim);
-
-
-(* case names *)
-
-val case_names =
- Scan.repeat1 (Args.name --
- Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") []) >>
- (fn cs =>
- Rule_Cases.cases_hyp_names (map fst cs)
- (map (map (the_default Rule_Cases.case_hypsN) o snd) cs));
-
-
-(* misc rules *)
-
-val no_vars = Thm.rule_attribute (fn context => fn th =>
- let
- val ctxt = Variable.set_body false (Context.proof_of context);
- val ((_, [th']), _) = Variable.import true [th] ctxt;
- in th' end);
-
-val eta_long =
- Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion));
-
-val rotated = Scan.optional Parse.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
-
-
-(* theory setup *)
-
-val _ = Theory.setup
- (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
- "internal attribute" #>
- setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
- setup (Binding.name "untagged") (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
- setup (Binding.name "kind") (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
- setup (Binding.name "THEN") THEN_att "resolution with rule" #>
- setup (Binding.name "OF") OF_att "rule applied to facts" #>
- setup (Binding.name "rename_abs") (Scan.lift rename_abs)
- "rename bound variables in abstractions" #>
- setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
- setup (Binding.name "folded") folded "folded definitions" #>
- setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
- "number of consumed facts" #>
- setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
- "number of equality constraints" #>
- setup (Binding.name "case_names") (Scan.lift case_names) "named rule cases" #>
- setup (Binding.name "case_conclusion")
- (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
- "named conclusion of rule cases" #>
- setup (Binding.name "params")
- (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
- "named rule parameters" #>
- setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
- "result put into standard form (legacy)" #>
- setup (Binding.name "rule_format") (Scan.lift (Args.mode "no_asm") >> rule_format)
- "result put into canonical rule format" #>
- setup (Binding.name "elim_format") (Scan.succeed elim_format)
- "destruct rule turned into elimination rule format" #>
- setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
- setup (Binding.name "eta_long") (Scan.succeed eta_long)
- "put theorem into eta long beta normal form" #>
- setup (Binding.name "atomize") (Scan.succeed Object_Logic.declare_atomize)
- "declaration of atomize rule" #>
- setup (Binding.name "rulify") (Scan.succeed Object_Logic.declare_rulify)
- "declaration of rulify rule" #>
- setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
- setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
- "declaration of definitional transformations" #>
- setup (Binding.name "abs_def")
- (Scan.succeed (Thm.rule_attribute (fn context =>
- Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
- "abstract over free variables of definitional theorem");
-
-
-
(** configuration options **)
(* naming *)
--- a/src/Pure/Isar/calculation.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Pure/Isar/calculation.ML Mon Jan 27 17:13:33 2014 +0000
@@ -95,11 +95,11 @@
(* concrete syntax *)
val _ = Theory.setup
- (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
+ (Attrib.setup @{binding trans} (Attrib.add_del trans_add trans_del)
"declaration of transitivity rule" #>
- Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
+ Attrib.setup @{binding sym} (Attrib.add_del sym_add sym_del)
"declaration of symmetry rule" #>
- Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
+ Attrib.setup @{binding symmetric} (Scan.succeed symmetric)
"resolution with symmetry rule" #>
Global_Theory.add_thms
[((Binding.empty, transitive_thm), [trans_add]),
@@ -197,4 +197,32 @@
val moreover = collect false;
val ultimately = collect true;
+
+(* outer syntax *)
+
+val calc_args =
+ Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"})));
+
+val _ =
+ Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
+ (calc_args >> (Toplevel.proofs' o also_cmd));
+
+val _ =
+ Outer_Syntax.command @{command_spec "finally"}
+ "combine calculation and current facts, exhibit result"
+ (calc_args >> (Toplevel.proofs' o finally_cmd));
+
+val _ =
+ Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
+ (Scan.succeed (Toplevel.proof' moreover));
+
+val _ =
+ Outer_Syntax.command @{command_spec "ultimately"}
+ "augment calculation by current facts, exhibit result"
+ (Scan.succeed (Toplevel.proof' ultimately));
+
+val _ =
+ Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
+ (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
+
end;
--- a/src/Pure/Isar/isar_syn.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Pure/Isar/isar_syn.ML Mon Jan 27 17:13:33 2014 +0000
@@ -688,30 +688,6 @@
Toplevel.skip_proof (fn i => i + 1)));
-(* calculational proof commands *)
-
-val calc_args =
- Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"})));
-
-val _ =
- Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
- (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
-
-val _ =
- Outer_Syntax.command @{command_spec "finally"}
- "combine calculation and current facts, exhibit result"
- (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
-
-val _ =
- Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
- (Scan.succeed (Toplevel.proof' Calculation.moreover));
-
-val _ =
- Outer_Syntax.command @{command_spec "ultimately"}
- "augment calculation by current facts, exhibit result"
- (Scan.succeed (Toplevel.proof' Calculation.ultimately));
-
-
(* proof navigation *)
val _ =
@@ -847,11 +823,6 @@
Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
- (Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
-
-val _ =
Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Method.print_methods o Toplevel.theory_of)));
--- a/src/Pure/Isar/token.scala Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Pure/Isar/token.scala Mon Jan 27 17:13:33 2014 +0000
@@ -108,7 +108,7 @@
else source
def text: (String, String) =
- if (is_command && source == ";") ("terminator", "")
+ if (is_keyword && source == ";") ("terminator", "")
else (kind.toString, source)
}
--- a/src/Pure/Pure.thy Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Pure/Pure.thy Mon Jan 27 17:13:33 2014 +0000
@@ -103,6 +103,7 @@
begin
ML_file "Isar/isar_syn.ML"
+ML_file "Isar/calculation.ML"
ML_file "Tools/rail.ML"
ML_file "Tools/rule_insts.ML";
ML_file "Tools/find_theorems.ML"
@@ -111,6 +112,113 @@
ML_file "Tools/simplifier_trace.ML"
+section {* Basic attributes *}
+
+attribute_setup tagged =
+ "Scan.lift (Args.name -- Args.name) >> Thm.tag"
+ "tagged theorem"
+
+attribute_setup untagged =
+ "Scan.lift Args.name >> Thm.untag"
+ "untagged theorem"
+
+attribute_setup kind =
+ "Scan.lift Args.name >> Thm.kind"
+ "theorem kind"
+
+attribute_setup THEN =
+ "Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
+ >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))"
+ "resolution with rule"
+
+attribute_setup OF =
+ "Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))"
+ "rule resolved with facts"
+
+attribute_setup rename_abs =
+ "Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
+ Thm.rule_attribute (K (Drule.rename_bvars' vs)))"
+ "rename bound variables in abstractions"
+
+attribute_setup unfolded =
+ "Attrib.thms >> (fn ths =>
+ Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))"
+ "unfolded definitions"
+
+attribute_setup folded =
+ "Attrib.thms >> (fn ths =>
+ Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))"
+ "folded definitions"
+
+attribute_setup consumes =
+ "Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes"
+ "number of consumed facts"
+
+attribute_setup constraints =
+ "Scan.lift Parse.nat >> Rule_Cases.constraints"
+ "number of equality constraints"
+
+attribute_setup case_names = {*
+ Scan.lift (Scan.repeat1 (Args.name --
+ Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
+ >> (fn cs =>
+ Rule_Cases.cases_hyp_names
+ (map #1 cs)
+ (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))
+*} "named rule cases"
+
+attribute_setup case_conclusion =
+ "Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion"
+ "named conclusion of rule cases"
+
+attribute_setup params =
+ "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
+ "named rule parameters"
+
+attribute_setup rule_format = {*
+ Scan.lift (Args.mode "no_asm")
+ >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)
+*} "result put into canonical rule format"
+
+attribute_setup elim_format =
+ "Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))"
+ "destruct rule turned into elimination rule format"
+
+attribute_setup no_vars = {*
+ Scan.succeed (Thm.rule_attribute (fn context => fn th =>
+ let
+ val ctxt = Variable.set_body false (Context.proof_of context);
+ val ((_, [th']), _) = Variable.import true [th] ctxt;
+ in th' end))
+*} "imported schematic variables"
+
+attribute_setup eta_long =
+ "Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))"
+ "put theorem into eta long beta normal form"
+
+attribute_setup atomize =
+ "Scan.succeed Object_Logic.declare_atomize"
+ "declaration of atomize rule"
+
+attribute_setup rulify =
+ "Scan.succeed Object_Logic.declare_rulify"
+ "declaration of rulify rule"
+
+attribute_setup rotated =
+ "Scan.lift (Scan.optional Parse.int 1
+ >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))"
+ "rotated theorem premises"
+
+attribute_setup defn =
+ "Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del"
+ "declaration of definitional transformations"
+
+attribute_setup abs_def =
+ "Scan.succeed (Thm.rule_attribute (fn context =>
+ Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))"
+ "abstract over free variables of definitional theorem"
+
+
section {* Further content for the Pure theory *}
subsection {* Meta-level connectives in assumptions *}
--- a/src/Pure/ROOT Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Pure/ROOT Mon Jan 27 17:13:33 2014 +0000
@@ -106,7 +106,6 @@
"Isar/attrib.ML"
"Isar/auto_bind.ML"
"Isar/bundle.ML"
- "Isar/calculation.ML"
"Isar/class.ML"
"Isar/class_declaration.ML"
"Isar/code.ML"
--- a/src/Pure/ROOT.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Pure/ROOT.ML Mon Jan 27 17:13:33 2014 +0000
@@ -236,9 +236,6 @@
use "Isar/method.ML";
use "Isar/proof.ML";
use "Isar/element.ML";
-
-(*derived theory and proof elements*)
-use "Isar/calculation.ML";
use "Isar/obtain.ML";
(*local theories and targets*)
--- a/src/Pure/System/session.scala Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Pure/System/session.scala Mon Jan 27 17:13:33 2014 +0000
@@ -180,12 +180,12 @@
case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
val prev = previous.get_finished
- val (doc_edits, version) =
+ val (syntax_changed, doc_edits, version) =
Timing.timeit("Thy_Load.text_edits", timing) {
thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits)
}
version_result.fulfill(version)
- sender ! Change(doc_blobs, doc_edits, prev, version)
+ sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
case bad => System.err.println("change_parser: ignoring bad message " + bad)
}
@@ -252,6 +252,7 @@
private case class Cancel_Exec(exec_id: Document_ID.Exec)
private case class Change(
doc_blobs: Document.Blobs,
+ syntax_changed: Boolean,
doc_edits: List[Document.Edit_Command],
previous: Document.Version,
version: Document.Version)
@@ -370,9 +371,7 @@
def handle_change(change: Change)
//{{{
{
- val previous = change.previous
- val version = change.version
- val doc_edits = change.doc_edits
+ val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change
def id_command(command: Command)
{
@@ -380,7 +379,7 @@
digest <- command.blobs_digests
if !global_state().defined_blob(digest)
} {
- change.doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
+ doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
case Some(blob) =>
global_state >> (_.define_blob(digest))
prover.get.define_blob(blob)
@@ -401,6 +400,8 @@
val assignment = global_state().the_assignment(previous).check_finished
global_state >> (_.define_version(version, assignment))
prover.get.update(previous.id, version.id, doc_edits)
+
+ if (syntax_changed) thy_load.syntax_changed()
}
//}}}
--- a/src/Pure/Thy/thy_load.scala Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Pure/Thy/thy_load.scala Mon Jan 27 17:13:33 2014 +0000
@@ -103,7 +103,9 @@
reparse_limit: Int,
previous: Document.Version,
doc_blobs: Document.Blobs,
- edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
+ edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
+
+ def syntax_changed() { }
}
--- a/src/Pure/Thy/thy_syntax.scala Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Pure/Thy/thy_syntax.scala Mon Jan 27 17:13:33 2014 +0000
@@ -155,8 +155,8 @@
private def header_edits(
base_syntax: Outer_Syntax,
previous: Document.Version,
- edits: List[Document.Edit_Text])
- : (Outer_Syntax, List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
+ edits: List[Document.Edit_Text]):
+ ((Outer_Syntax, Boolean), List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
{
var updated_imports = false
var updated_keywords = false
@@ -179,11 +179,14 @@
}
val syntax =
- if (previous.is_init || updated_keywords)
- (base_syntax /: nodes.entries) {
- case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
- }
- else previous.syntax
+ if (previous.is_init || updated_keywords) {
+ val syntax =
+ (base_syntax /: nodes.entries) {
+ case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
+ }
+ (syntax, true)
+ }
+ else (previous.syntax, false)
val reparse =
if (updated_imports || updated_keywords)
@@ -428,13 +431,13 @@
previous: Document.Version,
doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text])
- : (List[Document.Edit_Command], Document.Version) =
+ : (Boolean, List[Document.Edit_Command], Document.Version) =
{
- val (syntax, reparse0, nodes0, doc_edits0) =
+ val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) =
header_edits(thy_load.base_syntax, previous, edits)
if (edits.isEmpty)
- (Nil, Document.Version.make(syntax, previous.nodes))
+ (false, Nil, Document.Version.make(syntax, previous.nodes))
else {
val reparse =
(reparse0 /: nodes0.entries)({
@@ -472,7 +475,7 @@
nodes += (name -> node2)
}
- (doc_edits.toList, Document.Version.make(syntax, nodes))
+ (syntax_changed, doc_edits.toList, Document.Version.make(syntax, nodes))
}
}
}
--- a/src/Pure/Tools/rule_insts.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Pure/Tools/rule_insts.ML Mon Jan 27 17:13:33 2014 +0000
@@ -6,8 +6,6 @@
signature BASIC_RULE_INSTS =
sig
- val read_instantiate: Proof.context -> (indexname * string) list -> thm -> thm
- val instantiate_tac: Proof.context -> (indexname * string) list -> tactic
val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
val cut_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
@@ -20,6 +18,12 @@
signature RULE_INSTS =
sig
include BASIC_RULE_INSTS
+ val where_rule: Proof.context -> (indexname * string) list ->
+ (binding * string option * mixfix) list -> thm -> thm
+ val of_rule: Proof.context -> string option list * string option list ->
+ (binding * string option * mixfix) list -> thm -> thm
+ val read_instantiate: Proof.context -> (indexname * string) list -> string list -> thm -> thm
+ val instantiate_tac: Proof.context -> (indexname * string) list -> string list -> tactic
val make_elim_preserve: thm -> thm
val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
(Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
@@ -68,13 +72,13 @@
in
-fun read_termTs ctxt schematic ss Ts =
+fun read_termTs ctxt ss Ts =
let
fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
val ts = map2 parse Ts ss;
val ts' =
map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
- |> Syntax.check_terms ((schematic ? Proof_Context.set_mode Proof_Context.mode_schematic) ctxt)
+ |> Syntax.check_terms ctxt
|> Variable.polymorphic ctxt;
val Ts' = map Term.fastype_of ts';
val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
@@ -108,7 +112,7 @@
val (xs, ss) = split_list term_insts;
val Ts = map (the_type vars1) xs;
- val (ts, inferred) = read_termTs ctxt false ss Ts;
+ val (ts, inferred) = read_termTs ctxt ss Ts;
val instT2 = Term.typ_subst_TVars inferred;
val vars2 = map (apsnd instT2) vars1;
@@ -123,9 +127,10 @@
(map (pairself certT) inst_tvars, map (pairself cert) inst_vars)
end;
-fun read_instantiate_mixed ctxt mixed_insts thm =
+fun where_rule ctxt mixed_insts fixes thm =
let
val ctxt' = ctxt
+ |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2
|> Variable.declare_thm thm
|> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []); (* FIXME !? *)
val tvars = Thm.fold_terms Term.add_tvars thm [];
@@ -133,10 +138,11 @@
val insts = read_insts ctxt' mixed_insts (tvars, vars);
in
Drule.instantiate_normalize insts thm
+ |> singleton (Proof_Context.export ctxt' ctxt)
|> Rule_Cases.save thm
end;
-fun read_instantiate_mixed' ctxt (args, concl_args) thm =
+fun of_rule ctxt (args, concl_args) fixes thm =
let
fun zip_vars _ [] = []
| zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
@@ -145,17 +151,18 @@
val insts =
zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
- in read_instantiate_mixed ctxt insts thm end;
+ in where_rule ctxt insts fixes thm end;
end;
(* instantiation of rule or goal state *)
-fun read_instantiate ctxt =
- read_instantiate_mixed (ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic); (* FIXME !? *)
+fun read_instantiate ctxt insts xs =
+ where_rule ctxt insts (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
-fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
+fun instantiate_tac ctxt insts fixes =
+ PRIMITIVE (read_instantiate ctxt insts fixes);
@@ -165,9 +172,10 @@
val _ = Theory.setup
(Attrib.setup @{binding "where"}
- (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax))) >>
- (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
+ (Scan.lift
+ (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax)) -- Parse.for_fixes) >>
+ (fn (insts, fixes) =>
+ Thm.rule_attribute (fn context => where_rule (Context.proof_of context) insts fixes)))
"named instantiation of theorem");
@@ -186,8 +194,8 @@
val _ = Theory.setup
(Attrib.setup @{binding "of"}
- (Scan.lift insts >> (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
+ (Scan.lift (insts -- Parse.for_fixes) >> (fn (args, fixes) =>
+ Thm.rule_attribute (fn context => of_rule (Context.proof_of context) args fixes)))
"positional instantiation of theorem");
end;
@@ -243,7 +251,8 @@
val (xis, ss) = Library.split_list tinsts;
val Ts = map get_typ xis;
- val (ts, envT) = read_termTs ctxt' true ss Ts;
+ val (ts, envT) =
+ read_termTs (Proof_Context.set_mode Proof_Context.mode_schematic ctxt') ss Ts;
val envT' = map (fn (ixn, T) =>
(TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
val cenv =
--- a/src/Tools/Code/code_haskell.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Tools/Code/code_haskell.ML Mon Jan 27 17:13:33 2014 +0000
@@ -25,6 +25,7 @@
val language_params =
space_implode " " (map (prefix "-X") language_extensions);
+open Basic_Code_Symbol;
open Basic_Code_Thingol;
open Code_Printer;
@@ -37,8 +38,11 @@
fun print_haskell_stmt class_syntax tyco_syntax const_syntax
reserved deresolve deriving_show =
let
+ val deresolve_const = deresolve o Constant;
+ val deresolve_tyco = deresolve o Type_Constructor;
+ val deresolve_class = deresolve o Type_Class;
fun class_name class = case class_syntax class
- of NONE => deresolve class
+ of NONE => deresolve_class class
| SOME class => class;
fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
of [] => []
@@ -53,7 +57,7 @@
fun print_tyco_expr tyvars fxy (tyco, tys) =
brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
- of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
+ of NONE => print_tyco_expr tyvars fxy (deresolve_tyco tyco, tys)
| SOME (_, print) => print (print_typ tyvars) fxy tys)
| print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
fun print_typdecl tyvars (tyco, vs) =
@@ -81,18 +85,19 @@
in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
| print_term tyvars some_thm vars fxy (ICase case_expr) =
(case Code_Thingol.unfold_const_app (#primitive case_expr)
- of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ of SOME (app as ({ sym = Constant const, ... }, _)) =>
+ if is_none (const_syntax const)
then print_case tyvars some_thm vars fxy case_expr
else print_app tyvars some_thm vars fxy app
| NONE => print_case tyvars some_thm vars fxy case_expr)
- and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
+ and print_app_expr tyvars some_thm vars ({ sym, dom, range, annotate, ... }, ts) =
let
- val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
+ val ty = Library.foldr (op `->) (dom, range)
val printed_const =
if annotate then
- brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
+ brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
else
- (str o deresolve) c
+ (str o deresolve) sym
in
printed_const :: map (print_term tyvars some_thm vars BR) ts
end
@@ -122,29 +127,27 @@
(concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
(map print_select clauses)
end;
- fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
+ fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
let
val tyvars = intro_vars (map fst vs) reserved;
fun print_err n =
- semicolon (
- (str o deresolve) name
- :: map str (replicate n "_")
- @ str "="
- :: str "error"
- @@ (str o ML_Syntax.print_string
- o Long_Name.base_name o Long_Name.qualifier) name
+ (semicolon o map str) (
+ deresolve_const const
+ :: replicate n "_"
+ @ "="
+ :: "error"
+ @@ ML_Syntax.print_string const
);
fun print_eqn ((ts, t), (some_thm, _)) =
let
- val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
- |> intro_base_names
- (is_none o const_syntax) deresolve consts
+ |> intro_base_names_for (is_none o const_syntax)
+ deresolve (t :: ts)
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in
semicolon (
- (str o deresolve) name
+ (str o deresolve_const) const
:: map (print_term tyvars some_thm vars BR) ts
@ str "="
@@ print_term tyvars some_thm vars NOBR t
@@ -153,7 +156,7 @@
in
Pretty.chunks (
semicolon [
- (str o suffix " ::" o deresolve) name,
+ (str o suffix " ::" o deresolve_const) const,
print_typscheme tyvars (vs, ty)
]
:: (case filter (snd o snd) raw_eqs
@@ -161,52 +164,52 @@
| eqs => map print_eqn eqs)
)
end
- | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
+ | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
let
val tyvars = intro_vars vs reserved;
in
semicolon [
str "data",
- print_typdecl tyvars (deresolve name, vs)
+ print_typdecl tyvars (deresolve_tyco tyco, vs)
]
end
- | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
+ | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
let
val tyvars = intro_vars vs reserved;
in
semicolon (
str "newtype"
- :: print_typdecl tyvars (deresolve name, vs)
+ :: print_typdecl tyvars (deresolve_tyco tyco, vs)
:: str "="
- :: (str o deresolve) co
+ :: (str o deresolve_const) co
:: print_typ tyvars BR ty
- :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
+ :: (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
)
end
- | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
+ | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
let
val tyvars = intro_vars vs reserved;
fun print_co ((co, _), tys) =
concat (
- (str o deresolve) co
+ (str o deresolve_const) co
:: map (print_typ tyvars BR) tys
)
in
semicolon (
str "data"
- :: print_typdecl tyvars (deresolve name, vs)
+ :: print_typdecl tyvars (deresolve_tyco tyco, vs)
:: str "="
:: print_co co
:: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
- @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
+ @ (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
)
end
- | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
+ | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
let
val tyvars = intro_vars [v] reserved;
fun print_classparam (classparam, ty) =
semicolon [
- (str o deresolve) classparam,
+ (str o deresolve_const) classparam,
str "::",
print_typ tyvars NOBR ty
]
@@ -214,8 +217,8 @@
Pretty.block_enclose (
Pretty.block [
str "class ",
- Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
- str (deresolve name ^ " " ^ lookup_var tyvars v),
+ Pretty.block (print_typcontext tyvars [(v, map snd classrels)]),
+ str (deresolve_class class ^ " " ^ lookup_var tyvars v),
str " where {"
],
str "};"
@@ -226,25 +229,25 @@
val tyvars = intro_vars (map fst vs) reserved;
fun requires_args classparam = case const_syntax classparam
of NONE => NONE
- | SOME (Code_Printer.Plain_const_syntax _) => SOME 0
- | SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k;
+ | SOME (_, Code_Printer.Plain_printer _) => SOME 0
+ | SOME (k, Code_Printer.Complex_printer _) => SOME k;
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
case requires_args classparam
of NONE => semicolon [
- (str o Long_Name.base_name o deresolve) classparam,
+ (str o Long_Name.base_name o deresolve_const) classparam,
str "=",
print_app tyvars (SOME thm) reserved NOBR (const, [])
]
| SOME k =>
let
- val { name = c, dom, range, ... } = const;
+ val { sym = Constant c, dom, range, ... } = const;
val (vs, rhs) = (apfst o map) fst
(Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
val s = if (is_some o const_syntax) c
- then NONE else (SOME o Long_Name.base_name o deresolve) c;
+ then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
val vars = reserved
|> intro_vars (map_filter I (s :: vs));
- val lhs = IConst { name = classparam, typargs = [],
+ val lhs = IConst { sym = Constant classparam, typargs = [],
dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
(*dictionaries are not relevant at this late stage,
and these consts never need type annotations for disambiguation *)
@@ -269,7 +272,7 @@
end;
in print_stmt end;
-fun haskell_program_of_program ctxt symbol_of module_prefix module_name reserved identifiers =
+fun haskell_program_of_program ctxt module_prefix module_name reserved identifiers =
let
fun namify_fun upper base (nsp_fun, nsp_typ) =
let
@@ -280,7 +283,7 @@
let
val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
in (base', (nsp_fun, nsp_typ')) end;
- fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
+ fun namify_stmt (Code_Thingol.Fun (_, SOME _)) = pair
| namify_stmt (Code_Thingol.Fun _) = namify_fun false
| namify_stmt (Code_Thingol.Datatype _) = namify_typ
| namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
@@ -288,7 +291,7 @@
| namify_stmt (Code_Thingol.Classrel _) = pair
| namify_stmt (Code_Thingol.Classparam _) = namify_fun false
| namify_stmt (Code_Thingol.Classinst _) = pair;
- fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false
+ fun select_stmt (Code_Thingol.Fun (_, SOME _)) = false
| select_stmt (Code_Thingol.Fun _) = true
| select_stmt (Code_Thingol.Datatype _) = true
| select_stmt (Code_Thingol.Datatypecons _) = false
@@ -297,7 +300,7 @@
| select_stmt (Code_Thingol.Classparam _) = false
| select_stmt (Code_Thingol.Classinst _) = true;
in
- Code_Namespace.flat_program ctxt symbol_of
+ Code_Namespace.flat_program ctxt
{ module_prefix = module_prefix, module_name = module_name, reserved = reserved,
identifiers = identifiers, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
@@ -324,25 +327,24 @@
("Maybe", ["Nothing", "Just"])
];
-fun serialize_haskell module_prefix string_classes ctxt { symbol_of, module_name,
+fun serialize_haskell module_prefix string_classes ctxt { module_name,
reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program =
let
(* build program *)
val reserved = fold (insert (op =) o fst) includes reserved_syms;
val { deresolver, flat_program = haskell_program } = haskell_program_of_program
- ctxt symbol_of module_prefix module_name (Name.make_context reserved) identifiers program;
+ ctxt module_prefix module_name (Name.make_context reserved) identifiers program;
(* print statements *)
fun deriving_show tyco =
let
fun deriv _ "fun" = false
- | deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco)
- andalso (member (op =) tycos tyco
- orelse case try (Graph.get_node program) tyco
- of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
+ | deriv tycos tyco = member (op =) tycos tyco
+ orelse case try (Code_Symbol.Graph.get_node program) (Type_Constructor tyco)
+ of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
(maps snd cs)
- | NONE => true)
+ | NONE => true
and deriv' tycos (tyco `%% tys) = deriv tycos tyco
andalso forall (deriv' tycos) tys
| deriv' _ (ITyVar _) = true
@@ -370,10 +372,10 @@
val deresolve = deresolver module_name;
fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
val import_ps = import_common_ps @ map (print_qualified_import o fst) imports;
- fun print_stmt' name = case Graph.get_node gr name
+ fun print_stmt' sym = case Code_Symbol.Graph.get_node gr sym
of (_, NONE) => NONE
- | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
- val body_ps = map_filter print_stmt' ((flat o rev o Graph.strong_conn) gr);
+ | (_, SOME stmt) => SOME (markup_stmt sym (print_stmt deresolve (sym, stmt)));
+ val body_ps = map_filter print_stmt' ((flat o rev o Code_Symbol.Graph.strong_conn) gr);
in
print_module_frame module_name
((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
@@ -431,14 +433,14 @@
of SOME ((pat, ty), t') =>
SOME ((SOME ((pat, ty), true), t1), t')
| NONE => NONE;
- fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
- if c = c_bind_name then dest_bind t1 t2
+ fun dest_monad (IConst { sym = Constant c, ... } `$ t1 `$ t2) =
+ if c = c_bind then dest_bind t1 t2
else NONE
- | dest_monad _ t = case Code_Thingol.split_let t
+ | dest_monad t = case Code_Thingol.split_let t
of SOME (((pat, ty), tbind), t') =>
SOME ((SOME ((pat, ty), false), tbind), t')
| NONE => NONE;
- fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
+ val implode_monad = Code_Thingol.unfoldr dest_monad;
fun print_monad print_bind print_term (NONE, t) vars =
(semicolon [print_term vars NOBR t], vars)
| print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars
@@ -447,9 +449,9 @@
| print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars
|> print_bind NOBR bind
|>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]);
- fun pretty _ [c_bind'] print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
+ fun pretty _ print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
of SOME (bind, t') => let
- val (binds, t'') = implode_monad c_bind' t'
+ val (binds, t'') = implode_monad t'
val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
(bind :: binds) vars;
in
@@ -458,7 +460,7 @@
end
| NONE => brackify_infix (1, L) fxy
(print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
- in (2, ([c_bind], pretty)) end;
+ in (2, pretty) end;
fun add_monad target' raw_c_bind thy =
let
@@ -466,7 +468,7 @@
in
if target = target' then
thy
- |> Code_Target.set_printings (Code_Symbol.Constant (c_bind, [(target,
+ |> Code_Target.set_printings (Constant (c_bind, [(target,
SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))]))
else error "Only Haskell target allows for monad syntax"
end;
@@ -486,7 +488,7 @@
make_command = fn module_name =>
"\"$ISABELLE_GHC\" " ^ language_params ^ " -odir build -hidir build -stubdir build -e \"\" " ^
module_name ^ ".hs" } })
- #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+ #> Code_Target.set_printings (Type_Constructor ("fun",
[(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
--- a/src/Tools/Code/code_ml.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Tools/Code/code_ml.ML Mon Jan 27 17:13:33 2014 +0000
@@ -14,6 +14,7 @@
structure Code_ML : CODE_ML =
struct
+open Basic_Code_Symbol;
open Basic_Code_Thingol;
open Code_Printer;
@@ -28,17 +29,17 @@
datatype ml_binding =
ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
- | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
- superinsts: (class * (string * (string * dict list list))) list,
+ | ML_Instance of (string * class) * { class: class, tyco: string, vs: (vname * sort) list,
+ superinsts: (class * dict list list) list,
inst_params: ((string * (const * int)) * (thm * bool)) list,
superinst_params: ((string * (const * int)) * (thm * bool)) list };
datatype ml_stmt =
ML_Exc of string * (typscheme * int)
| ML_Val of ml_binding
- | ML_Funs of ml_binding list * string list
+ | ML_Funs of ml_binding list * Code_Symbol.T list
| ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
- | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
+ | ML_Class of string * (vname * ((class * class) list * (string * itype) list));
fun print_product _ [] = NONE
| print_product print [x] = SOME (print x)
@@ -53,30 +54,35 @@
fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
let
- fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
- | print_tyco_expr (tyco, [ty]) =
- concat [print_typ BR ty, (str o deresolve) tyco]
- | print_tyco_expr (tyco, tys) =
- concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
+ val deresolve_const = deresolve o Constant;
+ val deresolve_tyco = deresolve o Type_Constructor;
+ val deresolve_class = deresolve o Type_Class;
+ val deresolve_classrel = deresolve o Class_Relation;
+ val deresolve_inst = deresolve o Class_Instance;
+ fun print_tyco_expr (sym, []) = (str o deresolve) sym
+ | print_tyco_expr (sym, [ty]) =
+ concat [print_typ BR ty, (str o deresolve) sym]
+ | print_tyco_expr (sym, tys) =
+ concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
- of NONE => print_tyco_expr (tyco, tys)
+ of NONE => print_tyco_expr (Type_Constructor tyco, tys)
| SOME (_, print) => print print_typ fxy tys)
| print_typ fxy (ITyVar v) = str ("'" ^ v);
- fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
+ fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
(map_filter (fn (v, sort) =>
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
fun print_classrels fxy [] ps = brackify fxy ps
- | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps]
+ | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve_classrel) classrel, brackify BR ps]
| print_classrels fxy classrels ps =
- brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps]
+ brackify fxy [enum " o" "(" ")" (map (str o deresolve_classrel) classrels), brackify BR ps]
fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
- ((str o deresolve) inst ::
- (if is_pseudo_fun inst then [str "()"]
+ ((str o deresolve_inst) inst ::
+ (if is_pseudo_fun (Class_Instance inst) then [str "()"]
else map_filter (print_dicts is_pseudo_fun BR) dss))
| print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
[str (if k = 1 then first_upper v ^ "_"
@@ -105,21 +111,22 @@
in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
| print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
(case Code_Thingol.unfold_const_app (#primitive case_expr)
- of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ of SOME (app as ({ sym = Constant const, ... }, _)) =>
+ if is_none (const_syntax const)
then print_case is_pseudo_fun some_thm vars fxy case_expr
else print_app is_pseudo_fun some_thm vars fxy app
| NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
- and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
- if is_constr c then
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
+ if is_constr sym then
let val k = length dom in
if k < 2 orelse length ts = k
- then (str o deresolve) c
+ then (str o deresolve) sym
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
end
- else if is_pseudo_fun c
- then (str o deresolve) c @@ str "()"
- else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
+ else if is_pseudo_fun sym
+ then (str o deresolve) sym @@ str "()"
+ else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
(print_term is_pseudo_fun) const_syntax some_thm vars
@@ -158,39 +165,38 @@
:: map (print_select "|") clauses
)
end;
- fun print_val_decl print_typscheme (name, typscheme) = concat
- [str "val", str (deresolve name), str ":", print_typscheme typscheme];
+ fun print_val_decl print_typscheme (sym, typscheme) = concat
+ [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
let
- fun print_co ((co, _), []) = str (deresolve co)
- | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
+ fun print_co ((co, _), []) = str (deresolve_const co)
+ | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
in
concat (
str definer
- :: print_tyco_expr (tyco, map ITyVar vs)
+ :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
:: str "="
:: separate (str "|") (map print_co cos)
)
end;
fun print_def is_pseudo_fun needs_typ definer
- (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =
+ (ML_Function (const, (vs_ty as (vs, ty), eq :: eqs))) =
let
fun print_eqn definer ((ts, t), (some_thm, _)) =
let
- val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
- |> intro_base_names
- (is_none o const_syntax) deresolve consts
+ |> intro_base_names_for (is_none o const_syntax)
+ deresolve (t :: ts)
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
val prolog = if needs_typ then
- concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
- else (concat o map str) [definer, deresolve name];
+ concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
+ else (concat o map str) [definer, deresolve_const const];
in
concat (
prolog
- :: (if is_pseudo_fun name then [str "()"]
+ :: (if is_pseudo_fun (Constant const) then [str "()"]
else print_dict_args vs
@ map (print_term is_pseudo_fun some_thm vars BR) ts)
@ str "="
@@ -200,53 +206,53 @@
val shift = if null eqs then I else
map (Pretty.block o single o Pretty.block o single);
in pair
- (print_val_decl print_typscheme (name, vs_ty))
+ (print_val_decl print_typscheme (Constant const, vs_ty))
((Pretty.block o Pretty.fbreaks o shift) (
print_eqn definer eq
:: map (print_eqn "|") eqs
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
+ (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
let
- fun print_super_instance (_, (classrel, x)) =
+ fun print_super_instance (super_class, x) =
concat [
- (str o Long_Name.base_name o deresolve) classrel,
+ (str o Long_Name.base_name o deresolve_classrel) (class, super_class),
str "=",
- print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
+ print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
];
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
concat [
- (str o Long_Name.base_name o deresolve) classparam,
+ (str o Long_Name.base_name o deresolve_const) classparam,
str "=",
print_app (K false) (SOME thm) reserved NOBR (const, [])
];
in pair
(print_val_decl print_dicttypscheme
- (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
+ (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
(concat (
str definer
- :: (str o deresolve) inst
- :: (if is_pseudo_fun inst then [str "()"]
+ :: (str o deresolve_inst) inst
+ :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
else print_dict_args vs)
@ str "="
:: enum "," "{" "}"
(map print_super_instance superinsts
@ map print_classparam_instance inst_params)
:: str ":"
- @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
+ @@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
))
end;
- fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
- [print_val_decl print_typscheme (name, vs_ty)]
+ fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
+ [print_val_decl print_typscheme (Constant const, vs_ty)]
((semicolon o map str) (
(if n = 0 then "val" else "fun")
- :: deresolve name
+ :: deresolve_const const
:: replicate n "_"
@ "="
:: "raise"
:: "Fail"
- @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
+ @@ ML_Syntax.print_string const
))
| print_stmt (ML_Val binding) =
let
@@ -258,11 +264,11 @@
| print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
let
val print_def' = print_def (member (op =) pseudo_funs) false;
- fun print_pseudo_fun name = concat [
+ fun print_pseudo_fun sym = concat [
str "val",
- (str o deresolve) name,
+ (str o deresolve) sym,
str "=",
- (str o deresolve) name,
+ (str o deresolve) sym,
str "();"
];
val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
@@ -274,7 +280,7 @@
end
| print_stmt (ML_Datas [(tyco, (vs, []))]) =
let
- val ty_p = print_tyco_expr (tyco, map ITyVar vs);
+ val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
in
pair
[concat [str "type", ty_p]]
@@ -289,42 +295,42 @@
sig_ps
(Pretty.chunks (ps @| semicolon [p]))
end
- | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
+ | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
let
fun print_field s p = concat [str s, str ":", p];
fun print_proj s p = semicolon
(map str ["val", s, "=", "#" ^ s, ":"] @| p);
- fun print_super_class_decl (super_class, classrel) =
+ fun print_super_class_decl (classrel as (_, super_class)) =
print_val_decl print_dicttypscheme
- (classrel, ([(v, [class])], (super_class, ITyVar v)));
- fun print_super_class_field (super_class, classrel) =
- print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
- fun print_super_class_proj (super_class, classrel) =
- print_proj (deresolve classrel)
+ (Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
+ fun print_super_class_field (classrel as (_, super_class)) =
+ print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
+ fun print_super_class_proj (classrel as (_, super_class)) =
+ print_proj (deresolve_classrel classrel)
(print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
fun print_classparam_decl (classparam, ty) =
print_val_decl print_typscheme
- (classparam, ([(v, [class])], ty));
+ (Constant classparam, ([(v, [class])], ty));
fun print_classparam_field (classparam, ty) =
- print_field (deresolve classparam) (print_typ NOBR ty);
+ print_field (deresolve_const classparam) (print_typ NOBR ty);
fun print_classparam_proj (classparam, ty) =
- print_proj (deresolve classparam)
+ print_proj (deresolve_const classparam)
(print_typscheme ([(v, [class])], ty));
in pair
(concat [str "type", print_dicttyp (class, ITyVar v)]
- :: map print_super_class_decl super_classes
+ :: map print_super_class_decl classrels
@ map print_classparam_decl classparams)
(Pretty.chunks (
concat [
str ("type '" ^ v),
- (str o deresolve) class,
+ (str o deresolve_class) class,
str "=",
enum "," "{" "};" (
- map print_super_class_field super_classes
+ map print_super_class_field classrels
@ map print_classparam_field classparams
)
]
- :: map print_super_class_proj super_classes
+ :: map print_super_class_proj classrels
@ map print_classparam_proj classparams
))
end;
@@ -354,29 +360,34 @@
fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
let
- fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
- | print_tyco_expr (tyco, [ty]) =
- concat [print_typ BR ty, (str o deresolve) tyco]
- | print_tyco_expr (tyco, tys) =
- concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
+ val deresolve_const = deresolve o Constant;
+ val deresolve_tyco = deresolve o Type_Constructor;
+ val deresolve_class = deresolve o Type_Class;
+ val deresolve_classrel = deresolve o Class_Relation;
+ val deresolve_inst = deresolve o Class_Instance;
+ fun print_tyco_expr (sym, []) = (str o deresolve) sym
+ | print_tyco_expr (sym, [ty]) =
+ concat [print_typ BR ty, (str o deresolve) sym]
+ | print_tyco_expr (sym, tys) =
+ concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
- of NONE => print_tyco_expr (tyco, tys)
+ of NONE => print_tyco_expr (Type_Constructor tyco, tys)
| SOME (_, print) => print print_typ fxy tys)
| print_typ fxy (ITyVar v) = str ("'" ^ v);
- fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
+ fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
(map_filter (fn (v, sort) =>
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
val print_classrels =
- fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel])
+ fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve_classrel) classrel])
fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
print_plain_dict is_pseudo_fun fxy x
|> print_classrels classrels
and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
- brackify BR ((str o deresolve) inst ::
- (if is_pseudo_fun inst then [str "()"]
+ brackify BR ((str o deresolve_inst) inst ::
+ (if is_pseudo_fun (Class_Instance inst) then [str "()"]
else map_filter (print_dicts is_pseudo_fun BR) dss))
| print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
str (if k = 1 then "_" ^ first_upper v
@@ -402,21 +413,22 @@
in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
| print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
(case Code_Thingol.unfold_const_app (#primitive case_expr)
- of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ of SOME (app as ({ sym = Constant const, ... }, _)) =>
+ if is_none (const_syntax const)
then print_case is_pseudo_fun some_thm vars fxy case_expr
else print_app is_pseudo_fun some_thm vars fxy app
| NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
- and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
- if is_constr c then
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
+ if is_constr sym then
let val k = length dom in
if length ts = k
- then (str o deresolve) c
+ then (str o deresolve) sym
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
end
- else if is_pseudo_fun c
- then (str o deresolve) c @@ str "()"
- else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
+ else if is_pseudo_fun sym
+ then (str o deresolve) sym @@ str "()"
+ else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
(print_term is_pseudo_fun) const_syntax some_thm vars
@@ -450,30 +462,29 @@
:: map (print_select "|") clauses
)
end;
- fun print_val_decl print_typscheme (name, typscheme) = concat
- [str "val", str (deresolve name), str ":", print_typscheme typscheme];
+ fun print_val_decl print_typscheme (sym, typscheme) = concat
+ [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
let
- fun print_co ((co, _), []) = str (deresolve co)
- | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
+ fun print_co ((co, _), []) = str (deresolve_const co)
+ | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
in
concat (
str definer
- :: print_tyco_expr (tyco, map ITyVar vs)
+ :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
:: str "="
:: separate (str "|") (map print_co cos)
)
end;
fun print_def is_pseudo_fun needs_typ definer
- (ML_Function (name, (vs_ty as (vs, ty), eqs))) =
+ (ML_Function (const, (vs_ty as (vs, ty), eqs))) =
let
fun print_eqn ((ts, t), (some_thm, _)) =
let
- val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
- |> intro_base_names
- (is_none o const_syntax) deresolve consts
+ |> intro_base_names_for (is_none o const_syntax)
+ deresolve (t :: ts)
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in concat [
@@ -484,10 +495,9 @@
] end;
fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
let
- val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
- |> intro_base_names
- (is_none o const_syntax) deresolve consts
+ |> intro_base_names_for (is_none o const_syntax)
+ deresolve (t :: ts)
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in
@@ -510,10 +520,9 @@
)
| print_eqns _ (eqs as eq :: eqs') =
let
- val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
val vars = reserved
- |> intro_base_names
- (is_none o const_syntax) deresolve consts;
+ |> intro_base_names_for (is_none o const_syntax)
+ deresolve (map (snd o fst) eqs)
val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
in
Pretty.block (
@@ -533,57 +542,57 @@
)
end;
val prolog = if needs_typ then
- concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
- else (concat o map str) [definer, deresolve name];
+ concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
+ else (concat o map str) [definer, deresolve_const const];
in pair
- (print_val_decl print_typscheme (name, vs_ty))
+ (print_val_decl print_typscheme (Constant const, vs_ty))
(concat (
prolog
:: print_dict_args vs
- @| print_eqns (is_pseudo_fun name) eqs
+ @| print_eqns (is_pseudo_fun (Constant const)) eqs
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
+ (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
let
- fun print_super_instance (_, (classrel, x)) =
+ fun print_super_instance (super_class, x) =
concat [
- (str o deresolve) classrel,
+ (str o deresolve_classrel) (class, super_class),
str "=",
- print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
+ print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
];
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
concat [
- (str o deresolve) classparam,
+ (str o deresolve_const) classparam,
str "=",
print_app (K false) (SOME thm) reserved NOBR (const, [])
];
in pair
(print_val_decl print_dicttypscheme
- (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
+ (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
(concat (
str definer
- :: (str o deresolve) inst
- :: (if is_pseudo_fun inst then [str "()"]
+ :: (str o deresolve_inst) inst
+ :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
else print_dict_args vs)
@ str "="
@@ brackets [
enum_default "()" ";" "{" "}" (map print_super_instance superinsts
@ map print_classparam_instance inst_params),
str ":",
- print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
+ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
]
))
end;
- fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
- [print_val_decl print_typscheme (name, vs_ty)]
+ fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
+ [print_val_decl print_typscheme (Constant const, vs_ty)]
((doublesemicolon o map str) (
"let"
- :: deresolve name
+ :: deresolve_const const
:: replicate n "_"
@ "="
:: "failwith"
- @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
+ @@ ML_Syntax.print_string const
))
| print_stmt (ML_Val binding) =
let
@@ -595,11 +604,11 @@
| print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
let
val print_def' = print_def (member (op =) pseudo_funs) false;
- fun print_pseudo_fun name = concat [
+ fun print_pseudo_fun sym = concat [
str "let",
- (str o deresolve) name,
+ (str o deresolve) sym,
str "=",
- (str o deresolve) name,
+ (str o deresolve) sym,
str "();;"
];
val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
@@ -611,7 +620,7 @@
end
| print_stmt (ML_Datas [(tyco, (vs, []))]) =
let
- val ty_p = print_tyco_expr (tyco, map ITyVar vs);
+ val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
in
pair
[concat [str "type", ty_p]]
@@ -626,26 +635,26 @@
sig_ps
(Pretty.chunks (ps @| doublesemicolon [p]))
end
- | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
+ | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
let
fun print_field s p = concat [str s, str ":", p];
- fun print_super_class_field (super_class, classrel) =
- print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
+ fun print_super_class_field (classrel as (_, super_class)) =
+ print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
fun print_classparam_decl (classparam, ty) =
print_val_decl print_typscheme
- (classparam, ([(v, [class])], ty));
+ (Constant classparam, ([(v, [class])], ty));
fun print_classparam_field (classparam, ty) =
- print_field (deresolve classparam) (print_typ NOBR ty);
+ print_field (deresolve_const classparam) (print_typ NOBR ty);
val w = "_" ^ first_upper v;
fun print_classparam_proj (classparam, _) =
- (concat o map str) ["let", deresolve classparam, w, "=",
- w ^ "." ^ deresolve classparam ^ ";;"];
+ (concat o map str) ["let", deresolve_const classparam, w, "=",
+ w ^ "." ^ deresolve_const classparam ^ ";;"];
val type_decl_p = concat [
str ("type '" ^ v),
- (str o deresolve) class,
+ (str o deresolve_class) class,
str "=",
enum_default "unit" ";" "{" "}" (
- map print_super_class_field super_classes
+ map print_super_class_field classrels
@ map print_classparam_field classparams
)
];
@@ -698,7 +707,7 @@
(** SML/OCaml generic part **)
-fun ml_program_of_program ctxt symbol_of module_name reserved identifiers program =
+fun ml_program_of_program ctxt module_name reserved identifiers program =
let
fun namify_const upper base (nsp_const, nsp_type) =
let
@@ -716,76 +725,76 @@
| namify_stmt (Code_Thingol.Classrel _) = namify_const false
| namify_stmt (Code_Thingol.Classparam _) = namify_const false
| namify_stmt (Code_Thingol.Classinst _) = namify_const false;
- fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
+ fun ml_binding_of_stmt (sym as Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
let
val eqs = filter (snd o snd) raw_eqs;
- val (eqs', some_value_name) = if null (filter_out (null o snd) vs) then case eqs
+ val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
- else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
+ else (eqs, SOME (sym, member (op =) (Code_Thingol.add_constsyms t []) sym))
| _ => (eqs, NONE)
else (eqs, NONE)
- in (ML_Function (name, (tysm, eqs')), some_value_name) end
- | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as { vs, ... })) =
- (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
- | ml_binding_of_stmt (name, _) =
+ in (ML_Function (const, (tysm, eqs')), some_sym) end
+ | ml_binding_of_stmt (sym as Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
+ (ML_Instance (inst, stmt), if forall (null o snd) vs then SOME (sym, false) else NONE)
+ | ml_binding_of_stmt (sym, _) =
error ("Binding block containing illegal statement: " ^
- (Code_Symbol.quote_symbol ctxt o symbol_of) name)
- fun modify_fun (name, stmt) =
+ Code_Symbol.quote ctxt sym)
+ fun modify_fun (sym, stmt) =
let
- val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
+ val (binding, some_value_sym) = ml_binding_of_stmt (sym, stmt);
val ml_stmt = case binding
- of ML_Function (name, ((vs, ty), [])) =>
- ML_Exc (name, ((vs, ty),
+ of ML_Function (const, ((vs, ty), [])) =>
+ ML_Exc (const, ((vs, ty),
(length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
- | _ => case some_value_name
+ | _ => case some_value_sym
of NONE => ML_Funs ([binding], [])
- | SOME (name, true) => ML_Funs ([binding], [name])
- | SOME (name, false) => ML_Val binding
+ | SOME (sym, true) => ML_Funs ([binding], [sym])
+ | SOME (sym, false) => ML_Val binding
in SOME ml_stmt end;
fun modify_funs stmts = single (SOME
(ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
fun modify_datatypes stmts = single (SOME
(ML_Datas (map_filter
- (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))
+ (fn (Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
fun modify_class stmts = single (SOME
(ML_Class (the_single (map_filter
- (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))))
+ (fn (Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
- | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) =
modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)
- | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _) :: _)) =
modify_datatypes stmts
- | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Datatype _) :: _)) =
modify_datatypes stmts
- | modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Class _) :: _)) =
modify_class stmts
- | modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Classrel _) :: _)) =
modify_class stmts
- | modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Classparam _) :: _)) =
modify_class stmts
| modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
[modify_fun stmt]
- | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Classinst _) :: _)) =
modify_funs stmts
| modify_stmts stmts = error ("Illegal mutual dependencies: " ^
- (Library.commas o map (Code_Symbol.quote_symbol ctxt o symbol_of o fst)) stmts);
+ (Library.commas o map (Code_Symbol.quote ctxt o fst)) stmts);
in
- Code_Namespace.hierarchical_program ctxt symbol_of {
+ Code_Namespace.hierarchical_program ctxt {
module_name = module_name, reserved = reserved, identifiers = identifiers,
empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
end;
fun serialize_ml print_ml_module print_ml_stmt with_signatures ctxt
- { symbol_of, module_name, reserved_syms, identifiers, includes,
+ { module_name, reserved_syms, identifiers, includes,
class_syntax, tyco_syntax, const_syntax } program =
let
(* build program *)
val { deresolver, hierarchical_program = ml_program } =
- ml_program_of_program ctxt symbol_of module_name (Name.make_context reserved_syms) identifiers program;
+ ml_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
(* print statements *)
fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
@@ -807,7 +816,7 @@
lift_markup = apsnd } ml_program));
fun write width NONE = writeln o format [] width
| write width (SOME p) = File.write p o format [] width;
- fun prepare names width p = ([("", format names width p)], try (deresolver []));
+ fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
in
Code_Target.serialization write prepare p
end;
@@ -842,7 +851,7 @@
check = { env_var = "ISABELLE_OCAML",
make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
- #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+ #> Code_Target.set_printings (Type_Constructor ("fun",
[(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
#> fold (Code_Target.add_reserved target_SML)
--- a/src/Tools/Code/code_namespace.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Tools/Code/code_namespace.ML Mon Jan 27 17:13:33 2014 +0000
@@ -7,32 +7,32 @@
signature CODE_NAMESPACE =
sig
type flat_program
- val flat_program: Proof.context -> (string -> Code_Symbol.symbol)
+ val flat_program: Proof.context
-> { module_prefix: string, module_name: string,
reserved: Name.context, identifiers: Code_Target.identifier_data, empty_nsp: 'a,
namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
-> Code_Thingol.program
- -> { deresolver: string -> string -> string,
+ -> { deresolver: string -> Code_Symbol.T -> string,
flat_program: flat_program }
datatype ('a, 'b) node =
Dummy
| Stmt of 'a
- | Module of ('b * (string * ('a, 'b) node) Graph.T)
+ | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T)
type ('a, 'b) hierarchical_program
- val hierarchical_program: Proof.context -> (string -> Code_Symbol.symbol)
+ val hierarchical_program: Proof.context
-> { module_name: string,
reserved: Name.context, identifiers: Code_Target.identifier_data,
empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
- cyclic_modules: bool, empty_data: 'b, memorize_data: string -> 'b -> 'b,
- modify_stmts: (string * Code_Thingol.stmt) list -> 'a option list }
+ cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b,
+ modify_stmts: (Code_Symbol.T * Code_Thingol.stmt) list -> 'a option list }
-> Code_Thingol.program
- -> { deresolver: string list -> string -> string,
+ -> { deresolver: string list -> Code_Symbol.T -> string,
hierarchical_program: ('a, 'b) hierarchical_program }
val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
- print_stmt: string list -> string * 'a -> 'c,
+ print_stmt: string list -> Code_Symbol.T * 'a -> 'c,
lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
-> ('a, 'b) hierarchical_program -> 'c list
end;
@@ -42,24 +42,22 @@
(** fundamental module name hierarchy **)
-val split_name = apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
-
-fun lookup_identifier symbol_of identifiers name =
- Code_Symbol.lookup identifiers (symbol_of name)
+fun lookup_identifier identifiers sym =
+ Code_Symbol.lookup identifiers sym
|> Option.map (split_last o Long_Name.explode);
-fun force_identifier symbol_of fragments_tab force_module identifiers name =
- case lookup_identifier symbol_of identifiers name of
- NONE => (apfst (the o Symtab.lookup fragments_tab) o split_name) name
+fun force_identifier ctxt fragments_tab force_module identifiers sym =
+ case lookup_identifier identifiers sym of
+ NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym)
| SOME prefix_name => if null force_module then prefix_name
else (force_module, snd prefix_name);
-fun build_module_namespace { module_prefix, module_identifiers, reserved } program =
+fun build_module_namespace ctxt { module_prefix, module_identifiers, reserved } program =
let
fun alias_fragments name = case module_identifiers name
of SOME name' => Long_Name.explode name'
| NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
- val module_names = Graph.fold (insert (op =) o fst o split_name o fst) program [];
+ val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
in
fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
module_names Symtab.empty
@@ -68,9 +66,9 @@
(** flat program structure **)
-type flat_program = ((string * Code_Thingol.stmt option) Graph.T * (string * string list) list) Graph.T;
+type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
-fun flat_program ctxt symbol_of { module_prefix, module_name, reserved,
+fun flat_program ctxt { module_prefix, module_name, reserved,
identifiers, empty_nsp, namify_stmt, modify_stmt } program =
let
@@ -78,70 +76,70 @@
val module_identifiers = if module_name = ""
then Code_Symbol.lookup_module_data identifiers
else K (SOME module_name);
- val fragments_tab = build_module_namespace { module_prefix = module_prefix,
+ val fragments_tab = build_module_namespace ctxt { module_prefix = module_prefix,
module_identifiers = module_identifiers, reserved = reserved } program;
- val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers
+ val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers
#>> Long_Name.implode;
(* distribute statements over hierarchy *)
- fun add_stmt name stmt =
+ fun add_stmt sym stmt =
let
- val (module_name, base) = prep_name name;
+ val (module_name, base) = prep_sym sym;
in
- Graph.default_node (module_name, (Graph.empty, []))
- #> (Graph.map_node module_name o apfst) (Graph.new_node (name, (base, stmt)))
+ Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
+ #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, stmt)))
end;
- fun add_dependency name name' =
+ fun add_dependency sym sym' =
let
- val (module_name, _) = prep_name name;
- val (module_name', _) = prep_name name';
+ val (module_name, _) = prep_sym sym;
+ val (module_name', _) = prep_sym sym';
in if module_name = module_name'
- then (Graph.map_node module_name o apfst) (Graph.add_edge (name, name'))
- else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) name'))
+ then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym'))
+ else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) sym'))
end;
val proto_program = Graph.empty
- |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
- |> Graph.fold (fn (name, (_, (_, names))) =>
- Graph.Keys.fold (add_dependency name) names) program;
+ |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
+ |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
+ Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program;
(* name declarations and statement modifications *)
- fun declare name (base, stmt) (gr, nsp) =
+ fun declare sym (base, stmt) (gr, nsp) =
let
val (base', nsp') = namify_stmt stmt base nsp;
- val gr' = (Graph.map_node name o apfst) (K base') gr;
+ val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr;
in (gr', nsp') end;
fun declarations gr = (gr, empty_nsp)
- |> fold (fn name => declare name (Graph.get_node gr name)) (Graph.keys gr)
+ |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) (Code_Symbol.Graph.keys gr)
|> fst
- |> (Graph.map o K o apsnd) modify_stmt;
+ |> (Code_Symbol.Graph.map o K o apsnd) modify_stmt;
val flat_program = proto_program
|> (Graph.map o K o apfst) declarations;
(* qualified and unqualified imports, deresolving *)
- fun base_deresolver name = fst (Graph.get_node
- (fst (Graph.get_node flat_program (fst (prep_name name)))) name);
+ fun base_deresolver sym = fst (Code_Symbol.Graph.get_node
+ (fst (Graph.get_node flat_program (fst (prep_sym sym)))) sym);
fun classify_names gr imports =
let
val import_tab = maps
- (fn (module_name, names) => map (rpair module_name) names) imports;
- val imported_names = map fst import_tab;
- val here_names = Graph.keys gr;
+ (fn (module_name, syms) => map (rpair module_name) syms) imports;
+ val imported_syms = map fst import_tab;
+ val here_syms = Code_Symbol.Graph.keys gr;
in
- Symtab.empty
- |> fold (fn name => Symtab.update (name, base_deresolver name)) here_names
- |> fold (fn name => Symtab.update (name,
- Long_Name.append (the (AList.lookup (op =) import_tab name))
- (base_deresolver name))) imported_names
+ Code_Symbol.Table.empty
+ |> fold (fn sym => Code_Symbol.Table.update (sym, base_deresolver sym)) here_syms
+ |> fold (fn sym => Code_Symbol.Table.update (sym,
+ Long_Name.append (the (AList.lookup (op =) import_tab sym))
+ (base_deresolver sym))) imported_syms
end;
val deresolver_tab = Symtab.make (AList.make
(uncurry classify_names o Graph.get_node flat_program)
(Graph.keys flat_program));
- fun deresolver "" name =
- Long_Name.append (fst (prep_name name)) (base_deresolver name)
- | deresolver module_name name =
- the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
+ fun deresolver "" sym =
+ Long_Name.append (fst (prep_sym sym)) (base_deresolver sym)
+ | deresolver module_name sym =
+ the (Code_Symbol.Table.lookup (the (Symtab.lookup deresolver_tab module_name)) sym)
handle Option.Option => error ("Unknown statement name: "
- ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name);
+ ^ Code_Symbol.quote ctxt sym);
in { deresolver = deresolver, flat_program = flat_program } end;
@@ -151,18 +149,18 @@
datatype ('a, 'b) node =
Dummy
| Stmt of 'a
- | Module of ('b * (string * ('a, 'b) node) Graph.T);
+ | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T);
-type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Graph.T;
+type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T;
fun map_module_content f (Module content) = Module (f content);
fun map_module [] = I
| map_module (name_fragment :: name_fragments) =
- apsnd o Graph.map_node name_fragment o apsnd o map_module_content
+ apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content
o map_module name_fragments;
-fun hierarchical_program ctxt symbol_of { module_name, reserved, identifiers, empty_nsp,
+fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp,
namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmts } program =
let
@@ -170,95 +168,95 @@
val module_identifiers = if module_name = ""
then Code_Symbol.lookup_module_data identifiers
else K (SOME module_name);
- val fragments_tab = build_module_namespace { module_prefix = "",
+ val fragments_tab = build_module_namespace ctxt { module_prefix = "",
module_identifiers = module_identifiers, reserved = reserved } program;
- val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers;
+ val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers;
(* building empty module hierarchy *)
- val empty_module = (empty_data, Graph.empty);
+ val empty_module = (empty_data, Code_Symbol.Graph.empty);
fun ensure_module name_fragment (data, nodes) =
- if can (Graph.get_node nodes) name_fragment then (data, nodes)
+ if can (Code_Symbol.Graph.get_node nodes) (Code_Symbol.Module name_fragment) then (data, nodes)
else (data,
- nodes |> Graph.new_node (name_fragment, (name_fragment, Module empty_module)));
+ nodes |> Code_Symbol.Graph.new_node (Code_Symbol.Module name_fragment, (name_fragment, Module empty_module)));
fun allocate_module [] = I
| allocate_module (name_fragment :: name_fragments) =
ensure_module name_fragment
- #> (apsnd o Graph.map_node name_fragment o apsnd o map_module_content o allocate_module) name_fragments;
+ #> (apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o allocate_module) name_fragments;
val empty_program =
empty_module
|> Symtab.fold (fn (_, fragments) => allocate_module fragments) fragments_tab
- |> Graph.fold (allocate_module o these o Option.map fst
- o lookup_identifier symbol_of identifiers o fst) program;
+ |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst
+ o lookup_identifier identifiers o fst) program;
(* distribute statements over hierarchy *)
- fun add_stmt name stmt =
+ fun add_stmt sym stmt =
let
- val (name_fragments, base) = prep_name name;
+ val (name_fragments, base) = prep_sym sym;
in
- (map_module name_fragments o apsnd) (Graph.new_node (name, (base, Stmt stmt)))
+ (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt stmt)))
end;
- fun add_dependency name name' =
+ fun add_dependency sym sym' =
let
- val (name_fragments, _) = prep_name name;
- val (name_fragments', _) = prep_name name';
+ val (name_fragments, _) = prep_sym sym;
+ val (name_fragments', _) = prep_sym sym';
val (name_fragments_common, (diff, diff')) =
chop_prefix (op =) (name_fragments, name_fragments');
val is_module = not (null diff andalso null diff');
- val dep = pairself hd (diff @ [name], diff' @ [name']);
+ val dep = pairself hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']);
val add_edge = if is_module andalso not cyclic_modules
- then (fn node => Graph.add_edge_acyclic dep node
+ then (fn node => Code_Symbol.Graph.add_edge_acyclic dep node
handle Graph.CYCLES _ => error ("Dependency "
- ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name ^ " -> "
- ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name'
+ ^ Code_Symbol.quote ctxt sym ^ " -> "
+ ^ Code_Symbol.quote ctxt sym'
^ " would result in module dependency cycle"))
- else Graph.add_edge dep
+ else Code_Symbol.Graph.add_edge dep
in (map_module name_fragments_common o apsnd) add_edge end;
val proto_program = empty_program
- |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
- |> Graph.fold (fn (name, (_, (_, names))) =>
- Graph.Keys.fold (add_dependency name) names) program;
+ |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
+ |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
+ Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program;
(* name declarations, data and statement modifications *)
fun make_declarations nsps (data, nodes) =
let
- val (module_fragments, stmt_names) = List.partition
- (fn name_fragment => case Graph.get_node nodes name_fragment
- of (_, Module _) => true | _ => false) (Graph.keys nodes);
- fun declare namify name (nsps, nodes) =
+ val (module_fragments, stmt_syms) = List.partition
+ (fn sym => case Code_Symbol.Graph.get_node nodes sym
+ of (_, Module _) => true | _ => false) (Code_Symbol.Graph.keys nodes);
+ fun declare namify sym (nsps, nodes) =
let
- val (base, node) = Graph.get_node nodes name;
+ val (base, node) = Code_Symbol.Graph.get_node nodes sym;
val (base', nsps') = namify node base nsps;
- val nodes' = Graph.map_node name (K (base', node)) nodes;
+ val nodes' = Code_Symbol.Graph.map_node sym (K (base', node)) nodes;
in (nsps', nodes') end;
val (nsps', nodes') = (nsps, nodes)
|> fold (declare (K namify_module)) module_fragments
- |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_names;
+ |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_syms;
fun zip_fillup xs ys = xs ~~ ys @ replicate (length xs - length ys) NONE;
- fun select_names names = case filter (member (op =) stmt_names) names
+ fun select_syms syms = case filter (member (op =) stmt_syms) syms
of [] => NONE
- | xs => SOME xs;
- val modify_stmts' = AList.make (snd o Graph.get_node nodes)
+ | syms => SOME syms;
+ val modify_stmts' = AList.make (snd o Code_Symbol.Graph.get_node nodes)
#> split_list
##> map (fn Stmt stmt => stmt)
- #> (fn (names, stmts) => zip_fillup names (modify_stmts (names ~~ stmts)));
- val stmtss' = (maps modify_stmts' o map_filter select_names o Graph.strong_conn) nodes;
- val nodes'' = Graph.map (fn name => apsnd (fn Module content => Module (make_declarations nsps' content)
- | _ => case AList.lookup (op =) stmtss' name of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes';
- val data' = fold memorize_data stmt_names data;
+ #> (fn (syms, stmts) => zip_fillup syms (modify_stmts (syms ~~ stmts)));
+ val stmtss' = (maps modify_stmts' o map_filter select_syms o Code_Symbol.Graph.strong_conn) nodes;
+ val nodes'' = Code_Symbol.Graph.map (fn sym => apsnd (fn Module content => Module (make_declarations nsps' content)
+ | _ => case AList.lookup (op =) stmtss' sym of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes';
+ val data' = fold memorize_data stmt_syms data;
in (data', nodes'') end;
val (_, hierarchical_program) = make_declarations empty_nsp proto_program;
(* deresolving *)
- fun deresolver prefix_fragments name =
+ fun deresolver prefix_fragments sym =
let
- val (name_fragments, _) = prep_name name;
+ val (name_fragments, _) = prep_sym sym;
val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
- val nodes = fold (fn name_fragment => fn nodes => case Graph.get_node nodes name_fragment
+ val nodes = fold (fn name_fragment => fn nodes => case Code_Symbol.Graph.get_node nodes (Code_Symbol.Module name_fragment)
of (_, Module (_, nodes)) => nodes) name_fragments hierarchical_program;
- val (base', _) = Graph.get_node nodes name;
+ val (base', _) = Code_Symbol.Graph.get_node nodes sym;
in Long_Name.implode (remainder @ [base']) end
- handle Graph.UNDEF _ => error ("Unknown statement name: "
- ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name);
+ handle Code_Symbol.Graph.UNDEF _ => error ("Unknown statement name: "
+ ^ Code_Symbol.quote ctxt sym);
in { deresolver = deresolver, hierarchical_program = hierarchical_program } end;
@@ -266,10 +264,10 @@
let
fun print_node _ (_, Dummy) =
NONE
- | print_node prefix_fragments (name, Stmt stmt) =
- SOME (lift_markup (Code_Printer.markup_stmt name)
- (print_stmt prefix_fragments (name, stmt)))
- | print_node prefix_fragments (name_fragment, Module (data, nodes)) =
+ | print_node prefix_fragments (sym, Stmt stmt) =
+ SOME (lift_markup (Code_Printer.markup_stmt sym)
+ (print_stmt prefix_fragments (sym, stmt)))
+ | print_node prefix_fragments (Code_Symbol.Module name_fragment, Module (data, nodes)) =
let
val prefix_fragments' = prefix_fragments @ [name_fragment]
in
@@ -278,9 +276,9 @@
end
and print_nodes prefix_fragments nodes =
let
- val xs = (map_filter (fn name => print_node prefix_fragments
- (name, snd (Graph.get_node nodes name))) o rev o flat o Graph.strong_conn) nodes
+ val xs = (map_filter (fn sym => print_node prefix_fragments
+ (sym, snd (Code_Symbol.Graph.get_node nodes sym))) o rev o flat o Code_Symbol.Graph.strong_conn) nodes
in if null xs then NONE else SOME xs end;
in these o print_nodes [] end;
-end;
\ No newline at end of file
+end;
--- a/src/Tools/Code/code_printer.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Tools/Code/code_printer.ML Mon Jan 27 17:13:33 2014 +0000
@@ -25,8 +25,8 @@
val semicolon: Pretty.T list -> Pretty.T
val doublesemicolon: Pretty.T list -> Pretty.T
val indent: int -> Pretty.T -> Pretty.T
- val markup_stmt: string -> Pretty.T -> Pretty.T
- val format: string list -> int -> Pretty.T -> string
+ val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
+ val format: Code_Symbol.T list -> int -> Pretty.T -> string
val first_upper: string -> string
val first_lower: string -> string
@@ -36,6 +36,8 @@
val lookup_var: var_ctxt -> string -> string
val intro_base_names: (string -> bool) -> (string -> string)
-> string list -> var_ctxt -> var_ctxt
+ val intro_base_names_for: (string -> bool) -> (Code_Symbol.T -> string)
+ -> iterm list -> var_ctxt -> var_ctxt
val aux_params: var_ctxt -> iterm list list -> string list
type literals
@@ -65,24 +67,25 @@
val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
+ type raw_const_syntax
+ val plain_const_syntax: string -> raw_const_syntax
type simple_const_syntax
+ val simple_const_syntax: simple_const_syntax -> raw_const_syntax
type complex_const_syntax
- type const_syntax
- type activated_complex_const_syntax
- datatype activated_const_syntax = Plain_const_syntax of int * string
- | Complex_const_syntax of activated_complex_const_syntax
+ val complex_const_syntax: complex_const_syntax -> raw_const_syntax
+ val parse_const_syntax: raw_const_syntax parser
+ val requires_args: raw_const_syntax -> int
+ datatype const_printer = Plain_printer of string
+ | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T
+ type const_syntax = int * const_printer
+ val prep_const_syntax: theory -> literals
+ -> string -> raw_const_syntax -> const_syntax
type tyco_syntax
- val requires_args: const_syntax -> int
- val parse_const_syntax: const_syntax parser
val parse_tyco_syntax: tyco_syntax parser
- val plain_const_syntax: string -> const_syntax
- val simple_const_syntax: simple_const_syntax -> const_syntax
- val complex_const_syntax: complex_const_syntax -> const_syntax
- val activate_const_syntax: theory -> literals
- -> string -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
-> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
- -> (string -> activated_const_syntax option)
+ -> (string -> const_syntax option)
-> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm option -> fixity
@@ -92,6 +95,7 @@
structure Code_Printer : CODE_PRINTER =
struct
+open Basic_Code_Symbol;
open Code_Thingol;
(** generic nonsense *)
@@ -123,17 +127,18 @@
fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
fun indent i = Print_Mode.setmp [] (Pretty.indent i);
-fun markup_stmt name = Print_Mode.setmp [code_presentationN]
- (Pretty.mark (code_presentationN, [(stmt_nameN, name)]));
+fun markup_stmt sym = Print_Mode.setmp [code_presentationN]
+ (Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]));
fun filter_presentation [] tree =
Buffer.empty
|> fold XML.add_content tree
- | filter_presentation presentation_names tree =
+ | filter_presentation presentation_syms tree =
let
+ val presentation_idents = map Code_Symbol.marker presentation_syms
fun is_selected (name, attrs) =
name = code_presentationN
- andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN));
+ andalso member (op =) presentation_idents (the (Properties.get attrs stmt_nameN));
fun add_content_with_space tree (is_first, buf) =
buf
|> not is_first ? Buffer.add "\n\n"
@@ -187,12 +192,17 @@
val vars' = intro_vars fished3 vars;
in map (lookup_var vars') fished3 end;
-fun intro_base_names no_syntax deresolve names = names
- |> map_filter (fn name => if no_syntax name then
+fun intro_base_names no_syntax deresolve =
+ map_filter (fn name => if no_syntax name then
let val name' = deresolve name in
if Long_Name.is_qualified name' then NONE else SOME name'
end else NONE)
- |> intro_vars;
+ #> intro_vars;
+
+fun intro_base_names_for no_syntax deresolve ts =
+ []
+ |> fold Code_Thingol.add_constsyms ts
+ |> intro_base_names (fn Constant const => no_syntax const | _ => true) deresolve;
(** pretty literals **)
@@ -277,50 +287,51 @@
type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
-> fixity -> (iterm * itype) list -> Pretty.T);
-type complex_const_syntax = int * (string list * (literals -> string list
+type complex_const_syntax = int * (literals
-> (var_ctxt -> fixity -> iterm -> Pretty.T)
- -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
+ -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
-datatype const_syntax = plain_const_syntax of string
+datatype raw_const_syntax = plain_const_syntax of string
| complex_const_syntax of complex_const_syntax;
+fun simple_const_syntax syn =
+ complex_const_syntax
+ (apsnd (fn f => fn _ => fn print => fn _ => fn vars => f (print vars)) syn);
+
fun requires_args (plain_const_syntax _) = 0
| requires_args (complex_const_syntax (k, _)) = k;
-fun simple_const_syntax syn =
- complex_const_syntax
- (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
-
-type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
- -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)
+datatype const_printer = Plain_printer of string
+ | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T;
-datatype activated_const_syntax = Plain_const_syntax of int * string
- | Complex_const_syntax of activated_complex_const_syntax;
+type const_syntax = int * const_printer;
-fun activate_const_syntax thy literals c (plain_const_syntax s) naming =
- (Plain_const_syntax (Code.args_number thy c, s), naming)
- | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming =
- fold_map (Code_Thingol.ensure_declared_const thy) cs naming
- |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
+fun prep_const_syntax thy literals c (plain_const_syntax s) =
+ (Code.args_number thy c, Plain_printer s)
+ | prep_const_syntax thy literals c (complex_const_syntax (n, f))=
+ (n, Complex_printer (f literals));
fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
- (app as ({ name = c, dom, ... }, ts)) =
- case const_syntax c of
- NONE => brackify fxy (print_app_expr some_thm vars app)
- | SOME (Plain_const_syntax (_, s)) =>
- brackify fxy (str s :: map (print_term some_thm vars BR) ts)
- | SOME (Complex_const_syntax (k, print)) =>
- let
- fun print' fxy ts =
- print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
- in
- if k = length ts
- then print' fxy ts
- else if k < length ts
- then case chop k ts of (ts1, ts2) =>
- brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
- else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
- end;
+ (app as ({ sym, dom, ... }, ts)) =
+ case sym of
+ Constant const => (case const_syntax const of
+ NONE => brackify fxy (print_app_expr some_thm vars app)
+ | SOME (_, Plain_printer s) =>
+ brackify fxy (str s :: map (print_term some_thm vars BR) ts)
+ | SOME (k, Complex_printer print) =>
+ let
+ fun print' fxy ts =
+ print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
+ in
+ if k = length ts
+ then print' fxy ts
+ else if k < length ts
+ then case chop k ts of (ts1, ts2) =>
+ brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
+ else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
+ end)
+ | _ => brackify fxy (print_app_expr some_thm vars app);
fun gen_print_bind print_term thm (fxy : fixity) pat vars =
let
--- a/src/Tools/Code/code_runtime.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Tools/Code/code_runtime.ML Mon Jan 27 17:13:33 2014 +0000
@@ -36,6 +36,7 @@
structure Code_Runtime : CODE_RUNTIME =
struct
+open Basic_Code_Symbol;
open Basic_Code_Thingol;
(** evaluation **)
@@ -52,10 +53,10 @@
datatype truth = Holds;
val _ = Theory.setup
- (Code_Target.extend_target (target, (Code_ML.target_SML, K I))
- #> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop},
+ (Code_Target.extend_target (target, (Code_ML.target_SML, I))
+ #> Code_Target.set_printings (Type_Constructor (@{type_name prop},
[(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
- #> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds},
+ #> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds},
[(target, SOME (Code_Printer.plain_const_syntax s_Holds))]))
#> Code_Target.add_reserved target this
#> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
@@ -87,10 +88,13 @@
val ctxt = Proof_Context.init_global thy;
in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
-fun obtain_evaluator thy some_target naming program consts expr =
- Code_Target.evaluator thy (the_default target some_target) naming program consts expr
+fun obtain_evaluator thy some_target program consts expr =
+ Code_Target.evaluator thy (the_default target some_target) program consts expr
|> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
+fun obtain_evaluator' thy some_target program =
+ obtain_evaluator thy some_target program o map Constant;
+
fun evaluation cookie thy evaluator vs_t args =
let
val ctxt = Proof_Context.init_global thy;
@@ -110,8 +114,8 @@
val _ = if ! trace
then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
else ()
- fun evaluator naming program ((_, vs_ty), t) deps =
- evaluation cookie thy (obtain_evaluator thy some_target naming program deps) (vs_ty, t) args;
+ fun evaluator program ((_, vs_ty), t) deps =
+ evaluation cookie thy (obtain_evaluator thy some_target program deps) (vs_ty, t) args;
in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
fun dynamic_value_strict cookie thy some_target postproc t args =
@@ -120,9 +124,9 @@
fun dynamic_value cookie thy some_target postproc t args =
partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
-fun static_evaluator cookie thy some_target naming program consts' =
+fun static_evaluator cookie thy some_target program consts' =
let
- val evaluator = obtain_evaluator thy some_target naming program consts'
+ val evaluator = obtain_evaluator' thy some_target program consts'
in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end;
fun static_value_exn cookie thy some_target postproc consts =
@@ -175,13 +179,13 @@
in
fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
- (fn naming => fn program => fn vs_t => fn deps =>
- check_holds_oracle thy (obtain_evaluator thy NONE naming program deps) vs_t deps)
+ (fn program => fn vs_t => fn deps =>
+ check_holds_oracle thy (obtain_evaluator thy NONE program deps) vs_t deps)
o reject_vars thy;
fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts
- (fn naming => fn program => fn consts' =>
- check_holds_oracle thy (obtain_evaluator thy NONE naming program consts'))
+ (fn program => fn consts' =>
+ check_holds_oracle thy (obtain_evaluator' thy NONE program consts'))
o reject_vars thy;
end; (*local*)
@@ -192,23 +196,22 @@
fun evaluation_code thy module_name tycos consts =
let
val ctxt = Proof_Context.init_global thy;
- val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
- val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
+ val program = Code_Thingol.consts_program thy false consts;
val (ml_modules, target_names) =
Code_Target.produce_code_for thy
- target NONE module_name [] naming program (consts' @ tycos');
+ target NONE module_name [] program (map Constant consts @ map Type_Constructor tycos);
val ml_code = space_implode "\n\n" (map snd ml_modules);
- val (consts'', tycos'') = chop (length consts') target_names;
+ val (consts', tycos') = chop (length consts) target_names;
val consts_map = map2 (fn const =>
fn NONE =>
error ("Constant " ^ (quote o Code.string_of_const thy) const ^
"\nhas a user-defined serialization")
- | SOME const'' => (const, const'')) consts consts''
+ | SOME const' => (const, const')) consts consts'
val tycos_map = map2 (fn tyco =>
fn NONE =>
error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^
"\nhas a user-defined serialization")
- | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
+ | SOME tyco' => (tyco, tyco')) tycos tycos';
in (ml_code, (tycos_map, consts_map)) end;
@@ -290,7 +293,7 @@
Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
in
thy
- |> Code_Target.set_printings (Code_Symbol.Type_Constructor (tyco, [(target, SOME (k, pr))]))
+ |> Code_Target.set_printings (Type_Constructor (tyco, [(target, SOME (k, pr))]))
end;
fun add_eval_constr (const, const') thy =
@@ -300,11 +303,11 @@
(const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
in
thy
- |> Code_Target.set_printings (Code_Symbol.Constant (const,
+ |> Code_Target.set_printings (Constant (const,
[(target, SOME (Code_Printer.simple_const_syntax (k, pr)))]))
end;
-fun add_eval_const (const, const') = Code_Target.set_printings (Code_Symbol.Constant
+fun add_eval_const (const, const') = Code_Target.set_printings (Constant
(const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')))]));
fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
@@ -435,7 +438,7 @@
|> Code_Target.add_reserved target ml_name
|> Specification.axiomatization [(b, SOME T, NoSyn)] []
|-> (fn ([Const (const, _)], _) =>
- Code_Target.set_printings (Code_Symbol.Constant (const,
+ Code_Target.set_printings (Constant (const,
[(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
#> tap (fn thy => Code_Target.produce_code thy [const] target NONE structure_generated []));
--- a/src/Tools/Code/code_scala.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Tools/Code/code_scala.ML Mon Jan 27 17:13:33 2014 +0000
@@ -15,6 +15,7 @@
val target = "Scala";
+open Basic_Code_Symbol;
open Basic_Code_Thingol;
open Code_Printer;
@@ -27,15 +28,18 @@
fun print_scala_stmt tyco_syntax const_syntax reserved
args_num is_constr (deresolve, deresolve_full) =
let
+ val deresolve_const = deresolve o Constant;
+ val deresolve_tyco = deresolve o Type_Constructor;
+ val deresolve_class = deresolve o Type_Class;
fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
- fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
- (print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys
+ fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]"
+ (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys
and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
- of NONE => print_tyco_expr tyvars fxy (tyco, tys)
+ of NONE => print_tyco_expr tyvars fxy (Type_Constructor tyco, tys)
| SOME (_, print) => print (print_typ tyvars) fxy tys)
| print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
- fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (class, [ty]);
+ fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Type_Class class, [ty]);
fun print_tupled_typ tyvars ([], ty) =
print_typ tyvars NOBR ty
| print_tupled_typ tyvars ([ty1], ty2) =
@@ -67,25 +71,29 @@
end
| print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
(case Code_Thingol.unfold_const_app (#primitive case_expr)
- of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ of SOME (app as ({ sym = Constant const, ... }, _)) =>
+ if is_none (const_syntax const)
then print_case tyvars some_thm vars fxy case_expr
else print_app tyvars is_pat some_thm vars fxy app
| NONE => print_case tyvars some_thm vars fxy case_expr)
and print_app tyvars is_pat some_thm vars fxy
- (app as ({ name = c, typargs, dom, ... }, ts)) =
+ (app as ({ sym, typargs, dom, ... }, ts)) =
let
val k = length ts;
val typargs' = if is_pat then [] else typargs;
- val (l, print') = case const_syntax c
- of NONE => (args_num c, fn fxy => fn ts => gen_applify (is_constr c ) "(" ")"
+ val syntax = case sym of
+ Constant const => const_syntax const
+ | _ => NONE;
+ val (l, print') = case syntax of
+ NONE => (args_num sym, fn fxy => fn ts => gen_applify (is_constr sym) "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
- NOBR ((str o deresolve) c) typargs') ts)
- | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
+ NOBR ((str o deresolve) sym) typargs') ts)
+ | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
NOBR (str s) typargs') ts)
- | SOME (Complex_const_syntax (k, print)) =>
+ | SOME (k, Complex_printer print) =>
(k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
(ts ~~ take k dom))
in if k = l then print' fxy ts
@@ -137,41 +145,39 @@
|> single
|> enclose "(" ")"
end;
- fun print_context tyvars vs name = applify "[" "]"
+ fun print_context tyvars vs sym = applify "[" "]"
(fn (v, sort) => (Pretty.block o map str)
- (lookup_tyvar tyvars v :: maps (fn sort => [" : ", deresolve sort]) sort))
- NOBR ((str o deresolve) name) vs;
- fun print_defhead tyvars vars name vs params tys ty =
+ (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
+ NOBR ((str o deresolve) sym) vs;
+ fun print_defhead tyvars vars const vs params tys ty =
Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
- NOBR (print_context tyvars vs name) (params ~~ tys)) (print_typ tyvars NOBR ty),
+ NOBR (print_context tyvars vs (Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
str " ="];
- fun print_def name (vs, ty) [] =
+ fun print_def const (vs, ty) [] =
let
val (tys, ty') = Code_Thingol.unfold_fun ty;
val params = Name.invent (snd reserved) "a" (length tys);
val tyvars = intro_tyvars vs reserved;
val vars = intro_vars params reserved;
in
- concat [print_defhead tyvars vars name vs params tys ty',
- str ("sys.error(\"" ^ name ^ "\")")]
+ concat [print_defhead tyvars vars const vs params tys ty',
+ str ("sys.error(\"" ^ const ^ "\")")]
end
- | print_def name (vs, ty) eqs =
+ | print_def const (vs, ty) eqs =
let
val tycos = fold (fn ((ts, t), _) =>
fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
val tyvars = reserved
|> intro_base_names
- (is_none o tyco_syntax) deresolve tycos
+ (is_none o tyco_syntax) deresolve_tyco tycos
|> intro_tyvars vs;
val simple = case eqs
of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
| _ => false;
- val consts = fold Code_Thingol.add_constnames
- (map (snd o fst) eqs) [];
val vars1 = reserved
- |> intro_base_names
- (is_none o const_syntax) deresolve consts
+ |> intro_base_names_for (is_none o const_syntax)
+ deresolve (map (snd o fst) eqs);
val params = if simple
then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
else aux_params vars1 (map (fst o fst) eqs);
@@ -190,7 +196,7 @@
tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
str "=>", print_rhs vars' eq]
end;
- val head = print_defhead tyvars vars2 name vs params tys' ty';
+ val head = print_defhead tyvars vars2 const vs params tys' ty';
in if simple then
concat [head, print_rhs vars2 (hd eqs)]
else
@@ -199,34 +205,34 @@
str "match", str "{"], str "}")
(map print_clause eqs)
end;
- val print_method = str o Library.enclose "`" "`" o deresolve_full;
- fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
- print_def name (vs, ty) (filter (snd o snd) raw_eqs)
- | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
+ val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant;
+ fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
+ print_def const (vs, ty) (filter (snd o snd) raw_eqs)
+ | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
let
val tyvars = intro_tyvars (map (rpair []) vs) reserved;
fun print_co ((co, vs_args), tys) =
concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
- ((concat o map str) ["final", "case", "class", deresolve co]) vs_args)
+ ((concat o map str) ["final", "case", "class", deresolve_const co]) vs_args)
@@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
(Name.invent_names (snd reserved) "a" tys))),
str "extends",
applify "[" "]" (str o lookup_tyvar tyvars) NOBR
- ((str o deresolve) name) vs
+ ((str o deresolve_tyco) tyco) vs
];
in
Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
- NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs
+ NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
:: map print_co cos)
end
- | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
+ | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
let
- val tyvars = intro_tyvars [(v, [name])] reserved;
+ val tyvars = intro_tyvars [(v, [class])] reserved;
fun add_typarg s = Pretty.block
[str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
fun print_super_classes [] = NONE
- | print_super_classes classes = SOME (concat (str "extends"
- :: separate (str "with") (map (add_typarg o deresolve o fst) classes)));
+ | print_super_classes classrels = SOME (concat (str "extends"
+ :: separate (str "with") (map (add_typarg o deresolve_class o snd) classrels)));
fun print_classparam_val (classparam, ty) =
concat [str "val", constraint (print_method classparam)
((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)];
@@ -240,22 +246,22 @@
in
concat [str "def", constraint (Pretty.block [applify "(" ")"
(fn (aux, ty) => constraint ((str o lookup_var vars) aux)
- (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
+ (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam))
(auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
- add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
+ add_typarg (deresolve_class class), str ")"]) (print_typ tyvars NOBR ty), str "=",
applify "(" ")" (str o lookup_var vars) NOBR
(Pretty.block [str implicit_name, str ".", print_method classparam]) auxs]
end;
in
Pretty.chunks (
(Pretty.block_enclose
- (concat ([str "trait", (add_typarg o deresolve) name]
- @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
+ (concat ([str "trait", (add_typarg o deresolve_class) class]
+ @ the_list (print_super_classes classrels) @ [str "{"]), str "}")
(map print_classparam_val classparams))
:: map print_classparam_def classparams
)
end
- | print_stmt (name, Code_Thingol.Classinst
+ | print_stmt (sym, Code_Thingol.Classinst
{ class, tyco, vs, inst_params, superinst_params, ... }) =
let
val tyvars = intro_tyvars vs reserved;
@@ -279,13 +285,13 @@
end;
in
Pretty.block_enclose (concat [str "implicit def",
- constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
+ constraint (print_context tyvars vs sym) (print_dicttyp tyvars classtyp),
str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
(map print_classparam_instance (inst_params @ superinst_params))
end;
in print_stmt end;
-fun scala_program_of_program ctxt symbol_of module_name reserved identifiers program =
+fun scala_program_of_program ctxt module_name reserved identifiers program =
let
fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
let
@@ -314,49 +320,49 @@
| namify_stmt (Code_Thingol.Classrel _) = namify_object
| namify_stmt (Code_Thingol.Classparam _) = namify_object
| namify_stmt (Code_Thingol.Classinst _) = namify_common false;
- fun memorize_implicits name =
+ fun memorize_implicits sym =
let
fun is_classinst stmt = case stmt
of Code_Thingol.Classinst _ => true
| _ => false;
- val implicits = filter (is_classinst o Graph.get_node program)
- (Graph.immediate_succs program name);
+ val implicits = filter (is_classinst o Code_Symbol.Graph.get_node program)
+ (Code_Symbol.Graph.immediate_succs program sym);
in union (op =) implicits end;
- fun modify_stmt (_, Code_Thingol.Fun (_, (_, SOME _))) = NONE
+ fun modify_stmt (_, Code_Thingol.Fun (_, SOME _)) = NONE
| modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
| modify_stmt (_, Code_Thingol.Classrel _) = NONE
| modify_stmt (_, Code_Thingol.Classparam _) = NONE
| modify_stmt (_, stmt) = SOME stmt;
in
- Code_Namespace.hierarchical_program ctxt symbol_of
+ Code_Namespace.hierarchical_program ctxt
{ module_name = module_name, reserved = reserved, identifiers = identifiers,
empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module,
namify_stmt = namify_stmt, cyclic_modules = true, empty_data = [],
memorize_data = memorize_implicits, modify_stmts = map modify_stmt } program
end;
-fun serialize_scala ctxt { symbol_of, module_name, reserved_syms, identifiers,
+fun serialize_scala ctxt { module_name, reserved_syms, identifiers,
includes, class_syntax, tyco_syntax, const_syntax } program =
let
(* build program *)
val { deresolver, hierarchical_program = scala_program } =
- scala_program_of_program ctxt symbol_of module_name (Name.make_context reserved_syms) identifiers program;
+ scala_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
(* print statements *)
- fun lookup_constr tyco constr = case Graph.get_node program tyco
- of Code_Thingol.Datatype (_, (_, constrs)) =>
+ fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Type_Constructor tyco)
+ of Code_Thingol.Datatype (_, constrs) =>
the (AList.lookup (op = o apsnd fst) constrs constr);
- fun classparams_of_class class = case Graph.get_node program class
- of Code_Thingol.Class (_, (_, (_, classparams))) => classparams;
- fun args_num c = case Graph.get_node program c
- of Code_Thingol.Fun (_, (((_, ty), []), _)) =>
+ fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Type_Class class)
+ of Code_Thingol.Class (_, (_, classparams)) => classparams;
+ fun args_num (sym as Constant const) = case Code_Symbol.Graph.get_node program sym
+ of Code_Thingol.Fun (((_, ty), []), _) =>
(length o fst o Code_Thingol.unfold_fun) ty
- | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
- | Code_Thingol.Datatypecons (_, tyco) => length (lookup_constr tyco c)
- | Code_Thingol.Classparam (_, class) =>
+ | Code_Thingol.Fun ((_, ((ts, _), _) :: _), _) => length ts
+ | Code_Thingol.Datatypecons tyco => length (lookup_constr tyco const)
+ | Code_Thingol.Classparam class =>
(length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
- (classparams_of_class class)) c;
+ (classparams_of_class class)) const;
fun print_stmt prefix_fragments = print_scala_stmt
tyco_syntax const_syntax (make_vars reserved_syms) args_num
(Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver []);
@@ -380,7 +386,7 @@
lift_markup = I } scala_program);
fun write width NONE = writeln o format [] width
| write width (SOME p) = File.write p o format [] width;
- fun prepare names width p = ([("", format names width p)], try (deresolver []));
+ fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
in
Code_Target.serialization write prepare p
end;
@@ -417,7 +423,7 @@
make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
make_command = fn _ =>
"env JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' \"$SCALA_HOME/bin/scalac\" ROOT.scala" } })
- #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+ #> Code_Target.set_printings (Type_Constructor ("fun",
[(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ BR ty1 (*product type vs. tupled arguments!*),
--- a/src/Tools/Code/code_simp.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Tools/Code/code_simp.ML Mon Jan 27 17:13:33 2014 +0000
@@ -52,7 +52,7 @@
(* build simpset and conversion from program *)
-fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
+fun add_stmt (Code_Thingol.Fun ((_, eqs), some_cong)) ss =
ss
|> fold Simplifier.add_simp ((map_filter (fst o snd)) eqs)
|> fold Simplifier.add_cong (the_list some_cong)
@@ -61,7 +61,7 @@
|> fold Simplifier.add_simp (map (fst o snd) inst_params)
| add_stmt _ ss = ss;
-val add_program = Graph.fold (add_stmt o fst o snd);
+val add_program = Code_Symbol.Graph.fold (add_stmt o fst o snd);
fun simp_ctxt_program thy some_ss program =
simp_ctxt_default thy some_ss
@@ -77,7 +77,7 @@
(* evaluation with dynamic code context *)
fun dynamic_conv thy = Code_Thingol.dynamic_conv thy
- (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
+ (fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE (Proof_Context.init_global thy);
--- a/src/Tools/Code/code_symbol.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Tools/Code/code_symbol.ML Mon Jan 27 17:13:33 2014 +0000
@@ -5,17 +5,25 @@
class relations, class instances, modules.
*)
-signature CODE_SYMBOL =
+signature BASIC_CODE_SYMBOL =
sig
datatype ('a, 'b, 'c, 'd, 'e, 'f) attr =
Constant of 'a | Type_Constructor of 'b | Type_Class of 'c |
Class_Relation of 'd | Class_Instance of 'e | Module of 'f
- type symbol = (string, string, class, class * class, string * class, string) attr
- structure Table: TABLE;
- structure Graph: GRAPH;
- val default_name: Proof.context -> symbol -> string * string
- val quote_symbol: Proof.context -> symbol -> string
- val tyco_fun: string
+end
+
+signature CODE_SYMBOL =
+sig
+ include BASIC_CODE_SYMBOL
+ type T = (string, string, class, class * class, string * class, string) attr
+ structure Table: TABLE
+ structure Graph: GRAPH
+ val default_base: T -> string
+ val default_prefix: Proof.context -> T -> string
+ val quote: Proof.context -> T -> string
+ val marker: T -> string
+ val value: T
+ val is_value: T -> bool
val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l)
-> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr
val maps_attr: ('a -> 'g list) -> ('b -> 'h list)
@@ -37,12 +45,8 @@
val lookup_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class * class -> 'd option
val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option
val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option
- val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> symbol -> 'a option
- val dest_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'a) list
- val dest_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'b) list
- val dest_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (class * 'c) list
- val dest_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> ((class * class) * 'd) list
- val dest_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> ((string * class) * 'e) list
+ val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> T -> 'a option
+ val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> T list
val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'f) list
end;
@@ -54,7 +58,7 @@
datatype ('a, 'b, 'c, 'd, 'e, 'f) attr =
Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Relation of 'd | Class_Instance of 'e | Module of 'f;
-type symbol = (string, string, class, string * class, class * class, string) attr;
+type T = (string, string, class, string * class, class * class, string) attr;
fun symbol_ord (Constant c1, Constant c2) = fast_string_ord (c1, c2)
| symbol_ord (Constant _, _) = GREATER
@@ -75,8 +79,24 @@
| symbol_ord (_, Class_Instance _) = LESS
| symbol_ord (Module name1, Module name2) = fast_string_ord (name1, name2);
-structure Table = Table(type key = symbol val ord = symbol_ord);
-structure Graph = Graph(type key = symbol val ord = symbol_ord);
+structure Table = Table(type key = T val ord = symbol_ord);
+structure Graph = Graph(type key = T val ord = symbol_ord);
+
+local
+ val base = Name.desymbolize false o Long_Name.base_name;
+ fun base_rel (x, y) = base y ^ "_" ^ base x;
+in
+
+fun default_base (Constant "") = "value"
+ | default_base (Constant "==>") = "follows"
+ | default_base (Constant "==") = "meta_eq"
+ | default_base (Constant c) = base c
+ | default_base (Type_Constructor tyco) = base tyco
+ | default_base (Type_Class class) = base class
+ | default_base (Class_Relation classrel) = base_rel classrel
+ | default_base (Class_Instance inst) = base_rel inst;
+
+end;
local
fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
@@ -89,40 +109,35 @@
| NONE => (case Code.get_type_of_constr_or_abstr thy c
of SOME (tyco, _) => thyname_of_type thy tyco
| NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c));
- fun base_rel (x, y) = Long_Name.base_name y ^ "_" ^ Long_Name.base_name x;
- fun plainify ctxt get_prefix get_basename thing =
- (get_prefix (Proof_Context.theory_of ctxt) thing,
- Name.desymbolize false (get_basename thing));
+ fun prefix thy (Constant "") = "Code"
+ | prefix thy (Constant c) = thyname_of_const thy c
+ | prefix thy (Type_Constructor tyco) = thyname_of_type thy tyco
+ | prefix thy (Type_Class class) = thyname_of_class thy class
+ | prefix thy (Class_Relation (class, _)) = thyname_of_class thy class
+ | prefix thy (Class_Instance inst) = thyname_of_instance thy inst;
in
-fun default_name ctxt (Constant "==>") =
- plainify ctxt thyname_of_const (K "follows") "==>"
- | default_name ctxt (Constant "==") =
- plainify ctxt thyname_of_const (K "meta_eq") "=="
- | default_name ctxt (Constant c) =
- plainify ctxt thyname_of_const Long_Name.base_name c
- | default_name ctxt (Type_Constructor "fun") =
- plainify ctxt thyname_of_type (K "fun") "fun"
- | default_name ctxt (Type_Constructor tyco) =
- plainify ctxt thyname_of_type Long_Name.base_name tyco
- | default_name ctxt (Type_Class class) =
- plainify ctxt thyname_of_class Long_Name.base_name class
- | default_name ctxt (Class_Relation classrel) =
- plainify ctxt (fn thy => fn (class, _) => thyname_of_class thy class) base_rel classrel
- | default_name ctxt (Class_Instance inst) =
- plainify ctxt thyname_of_instance base_rel inst;
-
-val tyco_fun = (uncurry Long_Name.append o default_name @{context}) (Type_Constructor "fun");
+fun default_prefix ctxt = prefix (Proof_Context.theory_of ctxt);
end;
-fun quote_symbol ctxt (Constant c) = quote (Code.string_of_const (Proof_Context.theory_of ctxt) c)
- | quote_symbol ctxt (Type_Constructor tyco) = "type " ^ quote (Proof_Context.extern_type ctxt tyco)
- | quote_symbol ctxt (Type_Class class) = "class " ^ quote (Proof_Context.extern_class ctxt class)
- | quote_symbol ctxt (Class_Relation (sub, super)) =
- quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ quote (Proof_Context.extern_class ctxt super)
- | quote_symbol ctxt (Class_Instance (tyco, class)) =
- quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ quote (Proof_Context.extern_class ctxt class);
+val value = Constant "";
+fun is_value (Constant "") = true
+ | is_value _ = false;
+
+fun quote ctxt (Constant c) = Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c)
+ | quote ctxt (Type_Constructor tyco) = "type " ^ Library.quote (Proof_Context.extern_type ctxt tyco)
+ | quote ctxt (Type_Class class) = "class " ^ Library.quote (Proof_Context.extern_class ctxt class)
+ | quote ctxt (Class_Relation (sub, super)) =
+ Library.quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ Library.quote (Proof_Context.extern_class ctxt super)
+ | quote ctxt (Class_Instance (tyco, class)) =
+ Library.quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ Library.quote (Proof_Context.extern_class ctxt class);
+
+fun marker (Constant c) = "CONST " ^ c
+ | marker (Type_Constructor tyco) = "TYPE " ^ tyco
+ | marker (Type_Class class) = "CLASS " ^ class
+ | marker (Class_Relation (sub, super)) = "CLASSREL " ^ sub ^ " < " ^ super
+ | marker (Class_Instance (tyco, class)) = "INSTANCE " ^ tyco ^ " :: " ^ class;
fun map_attr const tyco class classrel inst module (Constant x) = Constant (const x)
| map_attr const tyco class classrel inst module (Type_Constructor x) = Type_Constructor (tyco x)
@@ -199,11 +214,16 @@
| lookup data (Class_Instance x) = lookup_class_instance_data data x
| lookup data (Module x) = lookup_module_data data x;
-fun dest_constant_data x = (Symtab.dest o #constant o dest_data) x;
-fun dest_type_constructor_data x = (Symtab.dest o #type_constructor o dest_data) x;
-fun dest_type_class_data x = (Symtab.dest o #type_class o dest_data) x;
-fun dest_class_relation_data x = (Symreltab.dest o #class_relation o dest_data) x;
-fun dest_class_instance_data x = (Symreltab.dest o #class_instance o dest_data) x;
+fun symbols_of x = (map Constant o Symtab.keys o #constant o dest_data) x
+ @ (map Type_Constructor o Symtab.keys o #type_constructor o dest_data) x
+ @ (map Type_Class o Symtab.keys o #type_class o dest_data) x
+ @ (map Class_Relation o Symreltab.keys o #class_relation o dest_data) x
+ @ (map Class_Instance o Symreltab.keys o #class_instance o dest_data) x
+ @ (map Module o Symtab.keys o #module o dest_data) x;
+
fun dest_module_data x = (Symtab.dest o #module o dest_data) x;
end;
+
+
+structure Basic_Code_Symbol: BASIC_CODE_SYMBOL = Code_Symbol;
--- a/src/Tools/Code/code_target.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Tools/Code/code_target.ML Mon Jan 27 17:13:33 2014 +0000
@@ -11,26 +11,26 @@
val read_const_exprs: theory -> string list -> string list
val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
- -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
+ -> Code_Thingol.program -> Code_Symbol.T list -> unit
val produce_code_for: theory -> string -> int option -> string -> Token.T list
- -> Code_Thingol.naming -> Code_Thingol.program -> string list -> (string * string) list * string option list
+ -> Code_Thingol.program -> Code_Symbol.T list -> (string * string) list * string option list
val present_code_for: theory -> string -> int option -> string -> Token.T list
- -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
+ -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
val check_code_for: theory -> string -> bool -> Token.T list
- -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
+ -> Code_Thingol.program -> Code_Symbol.T list -> unit
val export_code: theory -> string list
-> (((string * string) * Path.T option) * Token.T list) list -> unit
val produce_code: theory -> string list
-> string -> int option -> string -> Token.T list -> (string * string) list * string option list
- val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
+ val present_code: theory -> string list -> Code_Symbol.T list
-> string -> int option -> string -> Token.T list -> string
val check_code: theory -> string list
-> ((string * bool) * Token.T list) list -> unit
val generatedN: string
- val evaluator: theory -> string -> Code_Thingol.naming -> Code_Thingol.program
- -> string list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
+ val evaluator: theory -> string -> Code_Thingol.program
+ -> Code_Symbol.T list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
-> (string * string) list * string
type serializer
@@ -39,14 +39,14 @@
check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }
-> theory -> theory
val extend_target: string *
- (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
+ (string * (Code_Thingol.program -> Code_Thingol.program))
-> theory -> theory
val assert_target: theory -> string -> string
val the_literals: theory -> string -> literals
type serialization
val parse_args: 'a parser -> Token.T list -> 'a
val serialization: (int -> Path.T option -> 'a -> unit)
- -> (string list -> int -> 'a -> (string * string) list * (string -> string option))
+ -> (Code_Symbol.T list -> int -> 'a -> (string * string) list * (Code_Symbol.T -> string option))
-> 'a -> serialization
val set_default_code_width: int -> theory -> theory
@@ -54,11 +54,11 @@
type identifier_data
val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
-> theory -> theory
- type const_syntax = Code_Printer.const_syntax
+ type raw_const_syntax = Code_Printer.raw_const_syntax
type tyco_syntax = Code_Printer.tyco_syntax
- val set_printings: (const_syntax, tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
+ val set_printings: (raw_const_syntax, tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
-> theory -> theory
- val add_const_syntax: string -> string -> const_syntax option -> theory -> theory
+ val add_const_syntax: string -> string -> raw_const_syntax option -> theory -> theory
val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
val add_class_syntax: string -> class -> string option -> theory -> theory
val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
@@ -73,6 +73,7 @@
structure Code_Target : CODE_TARGET =
struct
+open Basic_Code_Symbol;
open Basic_Code_Thingol;
type literals = Code_Printer.literals;
@@ -84,7 +85,7 @@
type identifier_data = (string, string, string, string, string, string) Code_Symbol.data;
type tyco_syntax = Code_Printer.tyco_syntax;
-type const_syntax = Code_Printer.const_syntax;
+type raw_const_syntax = Code_Printer.raw_const_syntax;
(** checking and parsing of symbols **)
@@ -117,7 +118,7 @@
(cert_class thy class, cert_tyco thy tyco);
fun read_inst thy (raw_tyco, raw_class) =
- (read_class thy raw_class, read_tyco thy raw_tyco);
+ (read_tyco thy raw_tyco, read_class thy raw_class);
val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class;
@@ -154,21 +155,21 @@
(* serialization: abstract nonsense to cover different destinies for generated code *)
-datatype destination = Export of Path.T option | Produce | Present of string list;
-type serialization = int -> destination -> ((string * string) list * (string -> string option)) option;
+datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.T list;
+type serialization = int -> destination -> ((string * string) list * (Code_Symbol.T -> string option)) option;
fun serialization output _ content width (Export some_path) =
(output width some_path content; NONE)
| serialization _ string content width Produce =
string [] width content |> SOME
- | serialization _ string content width (Present stmt_names) =
- string stmt_names width content
+ | serialization _ string content width (Present syms) =
+ string syms width content
|> (apfst o map o apsnd) (Pretty.output (SOME width) o Pretty.str)
|> SOME;
fun export some_path f = (f (Export some_path); ());
fun produce f = the (f Produce);
-fun present stmt_names f = space_implode "\n\n" (map snd (fst (the (f (Present stmt_names)))));
+fun present syms f = space_implode "\n\n" (map snd (fst (the (f (Present syms)))));
(* serializers: functions producing serializations *)
@@ -176,14 +177,13 @@
type serializer = Token.T list
-> Proof.context
-> {
- symbol_of: string -> Code_Symbol.symbol,
module_name: string,
reserved_syms: string list,
identifiers: identifier_data,
includes: (string * Pretty.T) list,
class_syntax: string -> string option,
tyco_syntax: string -> Code_Printer.tyco_syntax option,
- const_syntax: string -> Code_Printer.activated_const_syntax option }
+ const_syntax: string -> Code_Printer.const_syntax option }
-> Code_Thingol.program
-> serialization;
@@ -193,7 +193,7 @@
check: { env_var: string, make_destination: Path.T -> Path.T,
make_command: string -> string } }
| Extension of string *
- (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
+ (Code_Thingol.program -> Code_Thingol.program);
(** theory data **)
@@ -311,10 +311,10 @@
of SOME data => data
| NONE => error ("Unknown code target language: " ^ quote target);
in case the_description data
- of Fundamental _ => (K I, data)
+ of Fundamental _ => (I, data)
| Extension (super, modify) => let
val (modify', data') = collapse super
- in (fn naming => modify' naming #> modify naming, merge_target false target (data', data)) end
+ in (modify' #> modify, merge_target false target (data', data)) end
end;
in collapse end;
@@ -326,95 +326,58 @@
val (modify, data) = collapse_hierarchy thy target;
in (default_width, data, modify) end;
-fun activate_const_syntax thy literals cs_data naming =
- (Symtab.empty, naming)
- |> fold_map (fn (c, data) => fn (tab, naming) =>
- case Code_Thingol.lookup_const naming c
- of SOME name => let
- val (syn, naming') =
- Code_Printer.activate_const_syntax thy literals c data naming
- in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
- | NONE => (NONE, (tab, naming))) cs_data
- |>> map_filter I;
-
-fun activate_syntax lookup_name things =
- Symtab.empty
- |> fold_map (fn (thing_identifier, data) => fn tab => case lookup_name thing_identifier
- of SOME name => (SOME name, Symtab.update_new (name, data) tab)
- | NONE => (NONE, tab)) things
- |>> map_filter I;
-
-fun activate_symbol_syntax thy literals naming printings =
- let
- val (names_const, (const_syntax, _)) =
- activate_const_syntax thy literals (Code_Symbol.dest_constant_data printings) naming;
- val (names_tyco, tyco_syntax) =
- activate_syntax (Code_Thingol.lookup_tyco naming) (Code_Symbol.dest_type_constructor_data printings);
- val (names_class, class_syntax) =
- activate_syntax (Code_Thingol.lookup_class naming) (Code_Symbol.dest_type_class_data printings);
- val names_inst = map_filter (Code_Thingol.lookup_instance naming o fst)
- (Code_Symbol.dest_class_instance_data printings);
- in
- (names_const @ names_tyco @ names_class @ names_inst,
- (const_syntax, tyco_syntax, class_syntax))
- end;
-
-fun project_program thy names_hidden names1 program2 =
+fun project_program thy syms_hidden syms1 program2 =
let
val ctxt = Proof_Context.init_global thy;
- val names2 = subtract (op =) names_hidden names1;
- val program3 = Graph.restrict (not o member (op =) names_hidden) program2;
- val names4 = Graph.all_succs program3 names2;
+ val syms2 = subtract (op =) syms_hidden syms1;
+ val program3 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program2;
+ val syms4 = Code_Symbol.Graph.all_succs program3 syms2;
val unimplemented = Code_Thingol.unimplemented program3;
val _ =
if null unimplemented then ()
else error ("No code equations for " ^
commas (map (Proof_Context.extern_const ctxt) unimplemented));
- val program4 = Graph.restrict (member (op =) names4) program3;
- in (names4, program4) end;
+ val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3;
+ in (syms4, program4) end;
-fun prepare_serializer thy (serializer : serializer) literals reserved identifiers
- printings module_name args naming proto_program names =
+fun prepare_serializer thy (serializer : serializer) reserved identifiers
+ printings module_name args proto_program syms =
let
- val (names_hidden, (const_syntax, tyco_syntax, class_syntax)) =
- activate_symbol_syntax thy literals naming printings;
- val (names_all, program) = project_program thy names_hidden names proto_program;
+ val syms_hidden = Code_Symbol.symbols_of printings;
+ val (syms_all, program) = project_program thy syms_hidden syms proto_program;
fun select_include (name, (content, cs)) =
- if null cs orelse exists (fn c => case Code_Thingol.lookup_const naming c
- of SOME name => member (op =) names_all name
- | NONE => false) cs
+ if null cs orelse exists (fn c => member (op =) syms_all (Constant c)) cs
then SOME (name, content) else NONE;
val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
in
(serializer args (Proof_Context.init_global thy) {
- symbol_of = Code_Thingol.symbol_of proto_program,
module_name = module_name,
reserved_syms = reserved,
identifiers = identifiers,
includes = includes,
- const_syntax = Symtab.lookup const_syntax,
- tyco_syntax = Symtab.lookup tyco_syntax,
- class_syntax = Symtab.lookup class_syntax },
+ const_syntax = Code_Symbol.lookup_constant_data printings,
+ tyco_syntax = Code_Symbol.lookup_type_constructor_data printings,
+ class_syntax = Code_Symbol.lookup_type_class_data printings },
program)
end;
-fun mount_serializer thy target some_width module_name args naming program names =
+fun mount_serializer thy target some_width module_name args program syms =
let
val (default_width, data, modify) = activate_target thy target;
val serializer = case the_description data
of Fundamental seri => #serializer seri;
val (prepared_serializer, prepared_program) =
- prepare_serializer thy serializer (the_literals thy target)
+ prepare_serializer thy serializer
(the_reserved data) (the_identifiers data) (the_printings data)
- module_name args naming (modify naming program) names
+ module_name args (modify program) syms
val width = the_default default_width some_width;
in (fn program => prepared_serializer program width, prepared_program) end;
-fun invoke_serializer thy target some_width module_name args naming program names =
+fun invoke_serializer thy target some_width module_name args program syms =
let
val check = if module_name = "" then I else check_name true;
val (mounted_serializer, prepared_program) = mount_serializer thy
- target some_width (check module_name) args naming program names;
+ target some_width (check module_name) args program syms;
in mounted_serializer prepared_program end;
fun assert_module_name "" = error "Empty module name not allowed here"
@@ -429,23 +392,23 @@
fun export_code_for thy some_path target some_width module_name args =
export (using_master_directory thy some_path)
- ooo invoke_serializer thy target some_width module_name args;
+ oo invoke_serializer thy target some_width module_name args;
fun produce_code_for thy target some_width module_name args =
let
val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
- in fn naming => fn program => fn names =>
- produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names)
+ in fn program => fn syms =>
+ produce (serializer program syms) |> apsnd (fn deresolve => map deresolve syms)
end;
fun present_code_for thy target some_width module_name args =
let
val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
- in fn naming => fn program => fn (names, selects) =>
- present selects (serializer naming program names)
+ in fn program => fn (syms, selects) =>
+ present selects (serializer program syms)
end;
-fun check_code_for thy target strict args naming program names_cs =
+fun check_code_for thy target strict args program syms =
let
val { env_var, make_destination, make_command } =
(#check o the_fundamental thy) target;
@@ -453,7 +416,7 @@
let
val destination = make_destination p;
val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
- generatedN args naming program names_cs);
+ generatedN args program syms);
val cmd = make_command generatedN;
in
if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
@@ -468,46 +431,38 @@
else Isabelle_System.with_tmp_dir "Code_Test" ext_check
end;
-fun evaluation mounted_serializer prepared_program consts ((vs, ty), t) =
+fun evaluation mounted_serializer prepared_program syms ((vs, ty), t) =
let
val _ = if Code_Thingol.contains_dict_var t then
error "Term to be evaluated contains free dictionaries" else ();
val v' = singleton (Name.variant_list (map fst vs)) "a";
val vs' = (v', []) :: vs;
- val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
- val value_name = "Value.value.value"
+ val ty' = ITyVar v' `-> ty;
val program = prepared_program
- |> Graph.new_node (value_name,
- Code_Thingol.Fun (@{const_name dummy_pattern}, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
- |> fold (curry (perhaps o try o Graph.add_edge) value_name) consts;
+ |> Code_Symbol.Graph.new_node (Code_Symbol.value,
+ Code_Thingol.Fun (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE))
+ |> fold (curry (perhaps o try o
+ Code_Symbol.Graph.add_edge) Code_Symbol.value) syms;
val (program_code, deresolve) = produce (mounted_serializer program);
- val value_name' = the (deresolve value_name);
- in (program_code, value_name') end;
+ val value_name = the (deresolve Code_Symbol.value);
+ in (program_code, value_name) end;
-fun evaluator thy target naming program consts =
+fun evaluator thy target program syms =
let
- val (mounted_serializer, prepared_program) = mount_serializer thy
- target NONE generatedN [] naming program consts;
- in evaluation mounted_serializer prepared_program consts end;
+ val (mounted_serializer, prepared_program) =
+ mount_serializer thy target NONE generatedN [] program syms;
+ in evaluation mounted_serializer prepared_program syms end;
end; (* local *)
(* code generation *)
-fun implemented_functions thy naming program =
+fun read_const_exprs thy const_exprs =
let
- val cs = Code_Thingol.unimplemented program;
- val names = map_filter (Code_Thingol.lookup_const naming) cs;
- in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
-
-fun read_const_exprs thy cs =
- let
- val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
- val (names2, (naming, program)) = Code_Thingol.consts_program thy true cs2;
- val names3 = implemented_functions thy naming program;
- val cs3 = map_filter (fn (c, name) =>
- if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
+ val (cs1, cs2) = Code_Thingol.read_const_exprs thy const_exprs;
+ val program = Code_Thingol.consts_program thy true cs2;
+ val cs3 = Code_Thingol.implemented_deps program;
in union (op =) cs3 cs1 end;
fun prep_destination "" = NONE
@@ -515,9 +470,9 @@
fun export_code thy cs seris =
let
- val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
+ val program = Code_Thingol.consts_program thy false cs;
val _ = map (fn (((target, module_name), some_path), args) =>
- export_code_for thy some_path target NONE module_name args naming program names_cs) seris;
+ export_code_for thy some_path target NONE module_name args program (map Constant cs)) seris;
in () end;
fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs)
@@ -525,19 +480,19 @@
fun produce_code thy cs target some_width some_module_name args =
let
- val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
- in produce_code_for thy target some_width some_module_name args naming program names_cs end;
+ val program = Code_Thingol.consts_program thy false cs;
+ in produce_code_for thy target some_width some_module_name args program (map Constant cs) end;
-fun present_code thy cs names_stmt target some_width some_module_name args =
+fun present_code thy cs syms target some_width some_module_name args =
let
- val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
- in present_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end;
+ val program = Code_Thingol.consts_program thy false cs;
+ in present_code_for thy target some_width some_module_name args program (map Constant cs, syms) end;
fun check_code thy cs seris =
let
- val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
+ val program = Code_Thingol.consts_program thy false cs;
val _ = map (fn ((target, strict), args) =>
- check_code_for thy target strict args naming program names_cs) seris;
+ check_code_for thy target strict args program (map Constant cs)) seris;
in () end;
fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
@@ -547,22 +502,22 @@
val parse_const_terms = Scan.repeat1 Args.term
>> (fn ts => fn thy => map (Code.check_const thy) ts);
-fun parse_names category parse internalize lookup =
+fun parse_names category parse internalize mark_symbol =
Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
- >> (fn xs => fn thy => fn naming => map_filter (lookup naming o internalize thy) xs);
+ >> (fn xs => fn thy => map (mark_symbol o internalize thy) xs);
val parse_consts = parse_names "consts" Args.term
- Code.check_const Code_Thingol.lookup_const;
+ Code.check_const Constant;
val parse_types = parse_names "types" (Scan.lift Args.name)
- Sign.intern_type Code_Thingol.lookup_tyco;
+ Sign.intern_type Type_Constructor;
val parse_classes = parse_names "classes" (Scan.lift Args.name)
- Sign.intern_class Code_Thingol.lookup_class;
+ Sign.intern_class Type_Class;
val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
- (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_class, Sign.intern_type thy raw_tyco))
- Code_Thingol.lookup_instance;
+ (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class))
+ Class_Instance;
in
@@ -574,7 +529,7 @@
(fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
let val thy = Proof_Context.theory_of ctxt in
present_code thy (mk_cs thy)
- (fn naming => maps (fn f => f thy naming) mk_stmtss)
+ (maps (fn f => f thy) mk_stmtss)
target some_width "Example" []
end);
@@ -599,12 +554,12 @@
(* checking of syntax *)
-fun check_const_syntax thy c syn =
+fun check_const_syntax thy target c syn =
if Code_Printer.requires_args syn > Code.args_number thy c
then error ("Too many arguments in syntax for constant " ^ quote c)
- else syn;
+ else Code_Printer.prep_const_syntax thy (the_literals thy target) c syn;
-fun check_tyco_syntax thy tyco syn =
+fun check_tyco_syntax thy target tyco syn =
if fst syn <> Sign.arity_number thy tyco
then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
else syn;
@@ -648,12 +603,12 @@
fun arrange_printings prep_const thy =
let
fun arrange check (sym, target_syns) =
- map (fn (target, some_syn) => (target, (sym, Option.map (check thy sym) some_syn))) target_syns;
+ map (fn (target, some_syn) => (target, (sym, Option.map (check thy target sym) some_syn))) target_syns;
in
Code_Symbol.maps_attr'
(arrange check_const_syntax) (arrange check_tyco_syntax)
- (arrange ((K o K) I)) (arrange ((K o K) I)) (arrange ((K o K) I))
- (arrange (fn thy => fn _ => fn (raw_content, raw_cs) =>
+ (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I))
+ (arrange (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) =>
(Code_Printer.str raw_content, map (prep_const thy) raw_cs)))
end;
@@ -673,23 +628,23 @@
let
val _ = legacy_feature "prefer \"code_printing\" for custom serialisations"
val x = prep_x thy raw_x;
- in set_printing (target, Symbol (x, Option.map (prep_syn thy x) some_raw_syn)) thy end;
+ in set_printing (target, Symbol (x, Option.map (prep_syn thy target x) some_raw_syn)) thy end;
fun gen_add_const_syntax prep_const =
- gen_add_syntax Code_Symbol.Constant prep_const check_const_syntax;
+ gen_add_syntax Constant prep_const check_const_syntax;
fun gen_add_tyco_syntax prep_tyco =
- gen_add_syntax Code_Symbol.Type_Constructor prep_tyco check_tyco_syntax;
+ gen_add_syntax Type_Constructor prep_tyco check_tyco_syntax;
fun gen_add_class_syntax prep_class =
- gen_add_syntax Code_Symbol.Type_Class prep_class ((K o K) I);
+ gen_add_syntax Type_Class prep_class ((K o K o K) I);
fun gen_add_instance_syntax prep_inst =
- gen_add_syntax Code_Symbol.Class_Instance prep_inst ((K o K) I);
+ gen_add_syntax Class_Instance prep_inst ((K o K o K) I);
fun gen_add_include prep_const target (name, some_content) thy =
- gen_add_syntax Code_Symbol.Module (K I)
- (fn thy => fn _ => fn (raw_content, raw_cs) => (Code_Printer.str raw_content, map (prep_const thy) raw_cs))
+ gen_add_syntax Module (K I)
+ (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) => (Code_Printer.str raw_content, map (prep_const thy) raw_cs))
target name some_content thy;
@@ -739,15 +694,15 @@
fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
parse_single_symbol_pragma @{keyword "constant"} Parse.term parse_const
- >> Code_Symbol.Constant
+ >> Constant
|| parse_single_symbol_pragma @{keyword "type_constructor"} Parse.type_const parse_tyco
- >> Code_Symbol.Type_Constructor
+ >> Type_Constructor
|| parse_single_symbol_pragma @{keyword "type_class"} Parse.class parse_class
- >> Code_Symbol.Type_Class
+ >> Type_Class
|| parse_single_symbol_pragma @{keyword "class_relation"} parse_classrel_ident parse_classrel
- >> Code_Symbol.Class_Relation
+ >> Class_Relation
|| parse_single_symbol_pragma @{keyword "class_instance"} parse_inst_ident parse_inst
- >> Code_Symbol.Class_Instance
+ >> Class_Instance
|| parse_single_symbol_pragma @{keyword "code_module"} Parse.name parse_module
>> Code_Symbol.Module;
--- a/src/Tools/Code/code_thingol.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Tools/Code/code_thingol.ML Mon Jan 27 17:13:33 2014 +0000
@@ -8,6 +8,7 @@
infix 8 `%%;
infix 4 `$;
infix 4 `$$;
+infixr 3 `->;
infixr 3 `|=>;
infixr 3 `|==>;
@@ -15,14 +16,14 @@
sig
type vname = string;
datatype dict =
- Dict of string list * plain_dict
+ Dict of (class * class) list * plain_dict
and plain_dict =
- Dict_Const of string * dict list list
+ Dict_Const of (string * class) * dict list list
| Dict_Var of vname * (int * int);
datatype itype =
`%% of string * itype list
| ITyVar of vname;
- type const = { name: string, typargs: itype list, dicts: dict list list,
+ type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
dom: itype list, range: itype, annotate: bool };
datatype iterm =
IConst of const
@@ -30,6 +31,7 @@
| `$ of iterm * iterm
| `|=> of (vname option * itype) * iterm
| ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
+ val `-> : itype * itype -> itype;
val `$$ : iterm * iterm list -> iterm;
val `|==> : (vname option * itype) list * iterm -> iterm;
type typscheme = (vname * sort) list * itype;
@@ -38,7 +40,6 @@
signature CODE_THINGOL =
sig
include BASIC_CODE_THINGOL
- val fun_tyco: string
val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
val unfold_fun: itype -> itype list * itype
@@ -54,65 +55,58 @@
val is_IAbs: iterm -> bool
val eta_expand: int -> const * iterm list -> iterm
val contains_dict_var: iterm -> bool
- val add_constnames: iterm -> string list -> string list
+ val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list
val add_tyconames: iterm -> string list -> string list
val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
- type naming
- val empty_naming: naming
- val lookup_class: naming -> class -> string option
- val lookup_classrel: naming -> class * class -> string option
- val lookup_tyco: naming -> string -> string option
- val lookup_instance: naming -> class * string -> string option
- val lookup_const: naming -> string -> string option
- val ensure_declared_const: theory -> string -> naming -> string * naming
-
datatype stmt =
- NoStmt of string
- | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
- | Datatype of string * (vname list *
- ((string * vname list (*type argument wrt. canonical order*)) * itype list) list)
- | Datatypecons of string * string
- | Class of class * (vname * ((class * string) list * (string * itype) list))
+ NoStmt
+ | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option
+ | Datatype of vname list *
+ ((string * vname list (*type argument wrt. canonical order*)) * itype list) list
+ | Datatypecons of string
+ | Class of vname * ((class * class) list * (string * itype) list)
| Classrel of class * class
- | Classparam of string * class
+ | Classparam of class
| Classinst of { class: string, tyco: string, vs: (vname * sort) list,
- superinsts: (class * (string * (string * dict list list))) list,
+ superinsts: (class * dict list list) list,
inst_params: ((string * (const * int)) * (thm * bool)) list,
superinst_params: ((string * (const * int)) * (thm * bool)) list };
- type program = stmt Graph.T
+ type program = stmt Code_Symbol.Graph.T
val unimplemented: program -> string list
+ val implemented_deps: program -> string list
val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
- val is_constr: program -> string -> bool
+ val is_constr: program -> Code_Symbol.T -> bool
val is_case: stmt -> bool
- val symbol_of: program -> string -> Code_Symbol.symbol;
val group_stmts: theory -> program
- -> ((string * stmt) list * (string * stmt) list
- * ((string * stmt) list * (string * stmt) list)) list
+ -> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list
+ * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list
val read_const_exprs: theory -> string list -> string list * string list
- val consts_program: theory -> bool -> string list -> string list * (naming * program)
- val dynamic_conv: theory -> (naming -> program
- -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+ val consts_program: theory -> bool -> string list -> program
+ val dynamic_conv: theory -> (program
+ -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
-> conv
- val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
- -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
+ val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (program
+ -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
-> term -> 'a
- val static_conv: theory -> string list -> (naming -> program -> string list
- -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+ val static_conv: theory -> string list -> (program -> string list
+ -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
-> conv
val static_conv_simple: theory -> string list
-> (program -> (string * sort) list -> term -> conv) -> conv
val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
- (naming -> program -> string list
- -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
+ (program -> string list
+ -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
-> term -> 'a
end;
structure Code_Thingol: CODE_THINGOL =
struct
+open Basic_Code_Symbol;
+
(** auxiliary **)
fun unfoldl dest x =
@@ -133,16 +127,29 @@
type vname = string;
datatype dict =
- Dict of string list * plain_dict
+ Dict of (class * class) list * plain_dict
and plain_dict =
- Dict_Const of string * dict list list
+ Dict_Const of (string * class) * dict list list
| Dict_Var of vname * (int * int);
datatype itype =
`%% of string * itype list
| ITyVar of vname;
-type const = { name: string, typargs: itype list, dicts: dict list list,
+fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
+
+val unfold_fun = unfoldr
+ (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
+ | _ => NONE);
+
+fun unfold_fun_n n ty =
+ let
+ val (tys1, ty1) = unfold_fun ty;
+ val (tys3, tys2) = chop n tys1;
+ val ty3 = Library.foldr (op `->) (tys2, ty1);
+ in (tys3, ty3) end;
+
+type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
dom: itype list, range: itype, annotate: bool };
datatype iterm =
@@ -191,7 +198,7 @@
#> fold (fn (p, body) => fold' p #> fold' body) clauses
in fold' end;
-val add_constnames = fold_constexprs (fn { name = c, ... } => insert (op =) c);
+val add_constsyms = fold_constexprs (fn { sym, ... } => insert (op =) sym);
fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
| add_tycos (ITyVar _) = I;
@@ -238,15 +245,15 @@
val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
-fun eta_expand k (const as { name = c, dom = tys, ... }, ts) =
+fun eta_expand k (const as { dom = tys, ... }, ts) =
let
val j = length ts;
val l = k - j;
val _ = if l > length tys
- then error ("Impossible eta-expansion for constant " ^ quote c) else ();
- val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
+ then error "Impossible eta-expansion" else ();
+ val vars = (fold o fold_varnames) Name.declare ts Name.context;
val vs_tys = (map o apfst) SOME
- (Name.invent_names ctxt "a" ((take l o drop j) tys));
+ (Name.invent_names vars "a" ((take l o drop j) tys));
in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
fun contains_dict_var t =
@@ -262,178 +269,31 @@
in cont_term t end;
-(** namings **)
-
-(* policies *)
-
-local
- fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
- fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
- fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy (swap inst)
- of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
- | thyname :: _ => thyname;
- fun thyname_of_const thy c = case Axclass.class_of_param thy c
- of SOME class => thyname_of_class thy class
- | NONE => (case Code.get_type_of_constr_or_abstr thy c
- of SOME (tyco, _) => thyname_of_type thy tyco
- | NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c));
- fun namify thy get_basename get_thyname name =
- let
- val prefix = get_thyname thy name;
- val base = (Name.desymbolize false o get_basename) name;
- in Long_Name.append prefix base end;
-in
-
-fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
-fun namify_classrel thy = namify thy (fn (sub_class, super_class) =>
- Long_Name.base_name super_class ^ "_" ^ Long_Name.base_name sub_class)
- (fn thy => thyname_of_class thy o fst);
- (*order fits nicely with composed projections*)
-fun namify_tyco thy "fun" = "Pure.fun"
- | namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_type tyco;
-fun namify_instance thy = namify thy (fn (class, tyco) =>
- Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance;
-fun namify_const thy "==>" = "Pure.follows"
- | namify_const thy "==" = "Pure.meta_eq"
- | namify_const thy c = namify thy Long_Name.base_name thyname_of_const c;
-
-end; (* local *)
-
-
-(* data *)
-
-datatype naming = Naming of {
- class: class Symtab.table * Name.context,
- classrel: string Symreltab.table * Name.context,
- tyco: string Symtab.table * Name.context,
- instance: string Symreltab.table * Name.context,
- const: string Symtab.table * Name.context
-}
-
-fun dest_Naming (Naming naming) = naming;
-
-val empty_naming = Naming {
- class = (Symtab.empty, Name.context),
- classrel = (Symreltab.empty, Name.context),
- tyco = (Symtab.empty, Name.context),
- instance = (Symreltab.empty, Name.context),
- const = (Symtab.empty, Name.context)
-};
-
-local
- fun mk_naming (class, classrel, tyco, instance, const) =
- Naming { class = class, classrel = classrel,
- tyco = tyco, instance = instance, const = const };
- fun map_naming f (Naming { class, classrel, tyco, instance, const }) =
- mk_naming (f (class, classrel, tyco, instance, const));
-in
- fun map_class f = map_naming
- (fn (class, classrel, tyco, inst, const) =>
- (f class, classrel, tyco, inst, const));
- fun map_classrel f = map_naming
- (fn (class, classrel, tyco, inst, const) =>
- (class, f classrel, tyco, inst, const));
- fun map_tyco f = map_naming
- (fn (class, classrel, tyco, inst, const) =>
- (class, classrel, f tyco, inst, const));
- fun map_instance f = map_naming
- (fn (class, classrel, tyco, inst, const) =>
- (class, classrel, tyco, f inst, const));
- fun map_const f = map_naming
- (fn (class, classrel, tyco, inst, const) =>
- (class, classrel, tyco, inst, f const));
-end; (*local*)
-
-fun add_variant update (thing, name) (tab, used) =
- let
- val (name', used') = Name.variant name used;
- val tab' = update (thing, name') tab;
- in (tab', used') end;
-
-fun declare thy mapp lookup update namify thing =
- mapp (add_variant update (thing, namify thy thing))
- #> `(fn naming => the (lookup naming thing));
-
-
-(* lookup and declare *)
-
-local
-
-val suffix_class = "class";
-val suffix_classrel = "classrel"
-val suffix_tyco = "tyco";
-val suffix_instance = "inst";
-val suffix_const = "const";
-
-fun add_suffix nsp NONE = NONE
- | add_suffix nsp (SOME name) = SOME (Long_Name.append name nsp);
-
-in
-
-val lookup_class = add_suffix suffix_class
- oo Symtab.lookup o fst o #class o dest_Naming;
-val lookup_classrel = add_suffix suffix_classrel
- oo Symreltab.lookup o fst o #classrel o dest_Naming;
-val lookup_tyco = add_suffix suffix_tyco
- oo Symtab.lookup o fst o #tyco o dest_Naming;
-val lookup_instance = add_suffix suffix_instance
- oo Symreltab.lookup o fst o #instance o dest_Naming;
-val lookup_const = add_suffix suffix_const
- oo Symtab.lookup o fst o #const o dest_Naming;
-
-fun declare_class thy = declare thy map_class
- lookup_class Symtab.update_new namify_class;
-fun declare_classrel thy = declare thy map_classrel
- lookup_classrel Symreltab.update_new namify_classrel;
-fun declare_tyco thy = declare thy map_tyco
- lookup_tyco Symtab.update_new namify_tyco;
-fun declare_instance thy = declare thy map_instance
- lookup_instance Symreltab.update_new namify_instance;
-fun declare_const thy = declare thy map_const
- lookup_const Symtab.update_new namify_const;
-
-fun ensure_declared_const thy const naming =
- case lookup_const naming const
- of SOME const' => (const', naming)
- | NONE => declare_const thy const naming;
-
-val fun_tyco = Long_Name.append (namify_tyco Pure.thy "fun") suffix_tyco
- (*depends on add_suffix*);
-
-val unfold_fun = unfoldr
- (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
- | _ => NONE);
-
-fun unfold_fun_n n ty =
- let
- val (tys1, ty1) = unfold_fun ty;
- val (tys3, tys2) = chop n tys1;
- val ty3 = Library.foldr (fn (ty1, ty2) => fun_tyco `%% [ty1, ty2]) (tys2, ty1);
- in (tys3, ty3) end;
-
-end; (* local *)
-
-
(** statements, abstract programs **)
type typscheme = (vname * sort) list * itype;
datatype stmt =
- NoStmt of string
- | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
- | Datatype of string * (vname list * ((string * vname list) * itype list) list)
- | Datatypecons of string * string
- | Class of class * (vname * ((class * string) list * (string * itype) list))
+ NoStmt
+ | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option
+ | Datatype of vname list * ((string * vname list) * itype list) list
+ | Datatypecons of string
+ | Class of vname * ((class * class) list * (string * itype) list)
| Classrel of class * class
- | Classparam of string * class
+ | Classparam of class
| Classinst of { class: string, tyco: string, vs: (vname * sort) list,
- superinsts: (class * (string * (string * dict list list))) list,
+ superinsts: (class * dict list list) list,
inst_params: ((string * (const * int)) * (thm * bool)) list,
superinst_params: ((string * (const * int)) * (thm * bool)) list };
-type program = stmt Graph.T;
+type program = stmt Code_Symbol.Graph.T;
fun unimplemented program =
- Graph.fold (fn (_, (NoStmt c, _)) => cons c | _ => I) program [];
+ Code_Symbol.Graph.fold (fn (Constant c, (NoStmt, _)) => cons c | _ => I) program [];
+
+fun implemented_deps program =
+ Code_Symbol.Graph.keys program
+ |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Constant (unimplemented program)))
+ |> map_filter (fn Constant c => SOME c | _ => NONE);
fun map_terms_bottom_up f (t as IConst _) = f t
| map_terms_bottom_up f (t as IVar _) = f t
@@ -449,9 +309,9 @@
fun map_classparam_instances_as_term f =
(map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const')
-fun map_terms_stmt f (NoStmt c) = (NoStmt c)
- | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
- (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
+fun map_terms_stmt f NoStmt = NoStmt
+ | map_terms_stmt f (Fun ((tysm, eqs), case_cong)) = Fun ((tysm, (map o apfst)
+ (fn (ts, t) => (map f ts, f t)) eqs), case_cong)
| map_terms_stmt f (stmt as Datatype _) = stmt
| map_terms_stmt f (stmt as Datatypecons _) = stmt
| map_terms_stmt f (stmt as Class _) = stmt
@@ -463,41 +323,16 @@
inst_params = map_classparam_instances_as_term f inst_params,
superinst_params = map_classparam_instances_as_term f superinst_params };
-fun is_constr program name = case Graph.get_node program name
+fun is_constr program sym = case Code_Symbol.Graph.get_node program sym
of Datatypecons _ => true
| _ => false;
-fun is_case (Fun (_, (_, SOME _))) = true
+fun is_case (Fun (_, SOME _)) = true
| is_case _ = false;
-fun symbol_of program name =
- case try (Graph.get_node program) name of
- NONE => Code_Symbol.Module "(unknown)"
- (*FIXME: need to be liberal due to ad-hoc introduction of value for evaluation*)
- | SOME stmt => case stmt of
- Fun (c, _) => Code_Symbol.Constant c
- | Datatype (tyco, _) => Code_Symbol.Type_Constructor tyco
- | Datatypecons (c, _) => Code_Symbol.Constant c
- | Class (class, _) => Code_Symbol.Type_Class class
- | Classrel (sub, super) =>
- let
- val Class (sub, _) = Graph.get_node program sub;
- val Class (super, _) = Graph.get_node program super;
- in
- Code_Symbol.Class_Relation (sub, super)
- end
- | Classparam (c, _) => Code_Symbol.Constant c
- | Classinst { class, tyco, ... } =>
- let
- val Class (class, _) = Graph.get_node program class;
- val Datatype (tyco, _) = Graph.get_node program tyco;
- in
- Code_Symbol.Class_Instance (tyco, class)
- end;
-
fun linear_stmts program =
- rev (Graph.strong_conn program)
- |> map (AList.make (Graph.get_node program));
+ rev (Code_Symbol.Graph.strong_conn program)
+ |> map (AList.make (Code_Symbol.Graph.get_node program));
fun group_stmts thy program =
let
@@ -516,8 +351,8 @@
else if forall (is_fun orf is_classinst) stmts
then ([], [], List.partition is_fun stmts)
else error ("Illegal mutual dependencies: " ^ (commas
- o map (Code_Symbol.quote_symbol (Proof_Context.init_global thy)
- o symbol_of program o fst)) stmts);
+ o map (Code_Symbol.quote (Proof_Context.init_global thy)
+ o fst)) stmts);
in
linear_stmts program
|> map group
@@ -528,31 +363,27 @@
(* generic mechanisms *)
-fun ensure_stmt lookup declare generate thing (dep, (naming, program)) =
+fun ensure_stmt symbolize generate x (dep, program) =
let
- fun add_dep name = case dep of NONE => I
- | SOME dep => Graph.add_edge (dep, name);
- val (name, naming') = case lookup naming thing
- of SOME name => (name, naming)
- | NONE => declare thing naming;
+ val sym = symbolize x;
+ val add_dep = case dep of NONE => I
+ | SOME dep => Code_Symbol.Graph.add_edge (dep, sym);
in
- if can (Graph.get_node program) name
+ if can (Code_Symbol.Graph.get_node program) sym
then
program
- |> add_dep name
- |> pair naming'
+ |> add_dep
|> pair dep
- |> pair name
+ |> pair x
else
program
- |> Graph.default_node (name, NoStmt "")
- |> add_dep name
- |> pair naming'
- |> curry generate (SOME name)
+ |> Code_Symbol.Graph.default_node (sym, NoStmt)
+ |> add_dep
+ |> curry generate (SOME sym)
||> snd
- |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
+ |-> (fn stmt => (Code_Symbol.Graph.map_node sym) (K stmt))
|> pair dep
- |> pair name
+ |> pair x
end;
exception PERMISSIVE of unit;
@@ -582,10 +413,6 @@
(err_typ ^ "\n" ^ err_class)
end;
-fun undefineds thy (dep, (naming, program)) =
- (map_filter (lookup_const naming) (Code.undefineds thy),
- (dep, (naming, program)));
-
(* inference of type annotations for disambiguation with type classes *)
@@ -640,18 +467,18 @@
ensure_const thy algbr eqngr permissive c
##>> pair (map (unprefix "'" o fst) vs)
##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
- #>> (fn info => Datatype (tyco, info));
- in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
+ #>> Datatype;
+ in ensure_stmt Type_Constructor stmt_datatype tyco end
and ensure_const thy algbr eqngr permissive c =
let
fun stmt_datatypecons tyco =
ensure_tyco thy algbr eqngr permissive tyco
- #>> (fn tyco => Datatypecons (c, tyco));
+ #>> Datatypecons;
fun stmt_classparam class =
ensure_class thy algbr eqngr permissive class
- #>> (fn class => Classparam (c, class));
+ #>> Classparam;
fun stmt_fun cert = case Code.equations_of_cert thy cert
- of (_, NONE) => pair (NoStmt c)
+ of (_, NONE) => pair NoStmt
| ((vs, ty), SOME eqns) =>
let
val eqns' = annotate_eqns thy algbr eqngr (c, ty) eqns
@@ -661,34 +488,34 @@
##>> translate_typ thy algbr eqngr permissive ty
##>> translate_eqns thy algbr eqngr permissive eqns'
#>>
- (fn (_, NONE) => NoStmt c
- | (tyscm, SOME eqns) => Fun (c, ((tyscm, eqns), some_case_cong)))
+ (fn (_, NONE) => NoStmt
+ | (tyscm, SOME eqns) => Fun ((tyscm, eqns), some_case_cong))
end;
val stmt_const = case Code.get_type_of_constr_or_abstr thy c
of SOME (tyco, _) => stmt_datatypecons tyco
| NONE => (case Axclass.class_of_param thy c
of SOME class => stmt_classparam class
| NONE => stmt_fun (Code_Preproc.cert eqngr c))
- in ensure_stmt lookup_const (declare_const thy) stmt_const c end
+ in ensure_stmt Constant stmt_const c end
and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
let
val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
val cs = #params (Axclass.get_info thy class);
val stmt_class =
- fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
- ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
+ fold_map (fn super_class =>
+ ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
##>> translate_typ thy algbr eqngr permissive ty) cs
- #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
- in ensure_stmt lookup_class (declare_class thy) stmt_class class end
+ #>> (fn info => Class (unprefix "'" Name.aT, info))
+ in ensure_stmt Type_Class stmt_class class end
and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) =
let
val stmt_classrel =
ensure_class thy algbr eqngr permissive sub_class
##>> ensure_class thy algbr eqngr permissive super_class
#>> Classrel;
- in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (sub_class, super_class) end
-and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
+ in ensure_stmt Class_Relation stmt_classrel (sub_class, super_class) end
+and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (tyco, class) =
let
val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
val these_class_params = these o try (#params o Axclass.get_info thy);
@@ -703,10 +530,8 @@
val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
fun translate_super_instance super_class =
ensure_class thy algbr eqngr permissive super_class
- ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)
##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
- #>> (fn ((super_class, classrel), [Dict ([], Dict_Const (inst, dss))]) =>
- (super_class, (classrel, (inst, dss))));
+ #>> (fn (super_class, [Dict ([], Dict_Const (_, dss))]) => (super_class, dss));
fun translate_classparam_instance (c, ty) =
let
val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
@@ -729,7 +554,7 @@
#>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) =>
Classinst { class = class, tyco = tyco, vs = vs,
superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
- in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
+ in ensure_stmt Class_Instance stmt_inst (tyco, class) end
and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
pair (ITyVar (unprefix "'" v))
| translate_typ thy algbr eqngr permissive (Type (tyco, tys)) =
@@ -781,7 +606,7 @@
##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
#>> (fn (((c, typargs), dss), range :: dom) =>
- IConst { name = c, typargs = typargs, dicts = dss,
+ IConst { sym = Constant c, typargs = typargs, dicts = dss,
dom = dom, range = range, annotate = annotate })
end
and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
@@ -790,6 +615,7 @@
#>> (fn (t, ts) => t `$$ ts)
and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
let
+ val undefineds = Code.undefineds thy;
fun arg_types num_args ty = fst (chop num_args (binder_types ty));
val tys = arg_types num_args (snd c_ty);
val ty = nth tys t_pos;
@@ -801,11 +627,11 @@
val constrs =
if null case_pats then []
else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
- fun casify undefineds constrs ty t_app ts =
+ fun casify constrs ty t_app ts =
let
fun collapse_clause vs_map ts body =
case body
- of IConst { name = c, ... } => if member (op =) undefineds c
+ of IConst { sym = Constant c, ... } => if member (op =) undefineds c
then []
else [(ts, body)]
| ICase { term = IVar (SOME v), clauses = clauses, ... } =>
@@ -839,9 +665,8 @@
#>> rpair n) constrs
##>> translate_typ thy algbr eqngr permissive ty
##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
- ##>> undefineds thy
- #>> (fn ((((t, constrs), ty), ts), undefineds) =>
- casify undefineds constrs ty t ts)
+ #>> (fn (((t, constrs), ty), ts) =>
+ casify constrs ty t ts)
end
and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
if length ts < num_args then
@@ -873,12 +698,12 @@
datatype typarg_witness =
Weakening of (class * class) list * plain_typarg_witness
and plain_typarg_witness =
- Global of (class * string) * typarg_witness list list
+ Global of (string * class) * typarg_witness list list
| Local of string * (int * sort);
fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
Weakening ((sub_class, super_class) :: classrels, x);
fun type_constructor (tyco, _) dss class =
- Weakening ([], Global ((class, tyco), (map o map) fst dss));
+ Weakening ([], Global ((tyco, class), (map o map) fst dss));
fun type_variable (TFree (v, sort)) =
let
val sort' = proj_sort sort;
@@ -905,31 +730,33 @@
structure Program = Code_Data
(
- type T = naming * program;
- val empty = (empty_naming, Graph.empty);
+ type T = program;
+ val empty = Code_Symbol.Graph.empty;
);
fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing =
Program.change_yield (if ignore_cache then NONE else SOME thy)
- (fn naming_program => (NONE, naming_program)
+ (fn program => (NONE, program)
|> generate thy algebra eqngr thing
- |-> (fn thing => fn (_, naming_program) => (thing, naming_program)));
+ |-> (fn thing => fn (_, program) => (thing, program)));
(* program generation *)
fun consts_program thy permissive consts =
let
- fun project_consts consts (naming, program) =
- if permissive then (consts, (naming, program))
- else (consts, (naming, Graph.restrict
- (member (op =) (Graph.all_succs program consts)) program));
+ fun project program =
+ if permissive then program
+ else Code_Symbol.Graph.restrict
+ (member (op =) (Code_Symbol.Graph.all_succs program
+ (map Constant consts))) program;
fun generate_consts thy algebra eqngr =
fold_map (ensure_const thy algebra eqngr permissive);
in
invoke_generation permissive thy (Code_Preproc.obtain false thy consts [])
generate_consts consts
- |-> project_consts
+ |> snd
+ |> project
end;
@@ -941,23 +768,24 @@
val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
o dest_TFree))) t [];
val t' = annotate thy algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
+ val dummy_constant = Constant @{const_name dummy_pattern};
val stmt_value =
fold_map (translate_tyvar_sort thy algbr eqngr false) vs
##>> translate_typ thy algbr eqngr false ty
##>> translate_term thy algbr eqngr false NONE (t', NONE)
#>> (fn ((vs, ty), t) => Fun
- (@{const_name dummy_pattern}, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
- fun term_value (dep, (naming, program1)) =
+ (((vs, ty), [(([], t), (NONE, true))]), NONE));
+ fun term_value (dep, program1) =
let
- val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
- Graph.get_node program1 @{const_name dummy_pattern};
- val deps = Graph.immediate_succs program1 @{const_name dummy_pattern};
- val program2 = Graph.del_node @{const_name dummy_pattern} program1;
- val deps_all = Graph.all_succs program2 deps;
- val program3 = Graph.restrict (member (op =) deps_all) program2;
- in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
+ val Fun ((vs_ty, [(([], t), _)]), _) =
+ Code_Symbol.Graph.get_node program1 dummy_constant;
+ val deps = Code_Symbol.Graph.immediate_succs program1 dummy_constant;
+ val program2 = Code_Symbol.Graph.del_node dummy_constant program1;
+ val deps_all = Code_Symbol.Graph.all_succs program2 deps;
+ val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
+ in ((program3, ((vs_ty, t), deps)), (dep, program2)) end;
in
- ensure_stmt ((K o K) NONE) pair stmt_value @{const_name dummy_pattern}
+ ensure_stmt Constant stmt_value @{const_name dummy_pattern}
#> snd
#> term_value
end;
@@ -967,9 +795,9 @@
fun dynamic_evaluator thy evaluator algebra eqngr vs t =
let
- val (((naming, program), (((vs', ty'), t'), deps)), _) =
+ val ((program, (((vs', ty'), t'), deps)), _) =
invoke_generation false thy (algebra, eqngr) ensure_value t;
- in evaluator naming program ((original_sorts vs vs', (vs', ty')), t') deps end;
+ in evaluator program ((original_sorts vs vs', (vs', ty')), t') deps end;
fun dynamic_conv thy evaluator =
Code_Preproc.dynamic_conv thy (dynamic_evaluator thy evaluator);
@@ -977,26 +805,26 @@
fun dynamic_value thy postproc evaluator =
Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator);
-fun lift_evaluation thy evaluation' algebra eqngr naming program vs t =
+fun lift_evaluation thy evaluation' algebra eqngr program vs t =
let
- val (((_, _), (((vs', ty'), t'), deps)), _) =
- ensure_value thy algebra eqngr t (NONE, (naming, program));
+ val ((_, (((vs', ty'), t'), deps)), _) =
+ ensure_value thy algebra eqngr t (NONE, program);
in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
fun lift_evaluator thy evaluator' consts algebra eqngr =
let
fun generate_consts thy algebra eqngr =
fold_map (ensure_const thy algebra eqngr false);
- val (consts', (naming, program)) =
+ val (consts', program) =
invoke_generation true thy (algebra, eqngr) generate_consts consts;
- val evaluation' = evaluator' naming program consts';
- in lift_evaluation thy evaluation' algebra eqngr naming program end;
+ val evaluation' = evaluator' program consts';
+ in lift_evaluation thy evaluation' algebra eqngr program end;
fun lift_evaluator_simple thy evaluator' consts algebra eqngr =
let
fun generate_consts thy algebra eqngr =
fold_map (ensure_const thy algebra eqngr false);
- val (_, (_, program)) =
+ val (_, program) =
invoke_generation true thy (algebra, eqngr) generate_consts consts;
in evaluator' program end;
--- a/src/Tools/jEdit/src/jedit_thy_load.scala Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala Mon Jan 27 17:13:33 2014 +0000
@@ -14,7 +14,7 @@
import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
import org.gjt.sp.jedit.MiscUtilities
-import org.gjt.sp.jedit.{View, Buffer}
+import org.gjt.sp.jedit.{jEdit, View, Buffer}
import org.gjt.sp.jedit.bufferio.BufferIORequest
class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
@@ -111,5 +111,11 @@
}
content()
}
+
+
+ /* theory text edits */
+
+ override def syntax_changed(): Unit =
+ Swing_Thread.later { jEdit.propertiesChanged() }
}
--- a/src/Tools/nbe.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/Tools/nbe.ML Mon Jan 27 17:13:33 2014 +0000
@@ -249,11 +249,9 @@
val univs_cookie = (Univs.get, put_result, name_put);
-val sloppy_name = Long_Name.base_name o Long_Name.qualifier
-
-fun nbe_fun idx_of 0 "" = "nbe_value"
- | nbe_fun idx_of i c = "c_" ^ string_of_int (idx_of c)
- ^ "_" ^ sloppy_name c ^ "_" ^ string_of_int i;
+fun nbe_fun idx_of 0 (Code_Symbol.Constant "") = "nbe_value"
+ | nbe_fun idx_of i sym = "c_" ^ string_of_int (idx_of sym)
+ ^ "_" ^ Code_Symbol.default_base sym ^ "_" ^ string_of_int i;
fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
fun nbe_bound v = "v_" ^ v;
fun nbe_bound_optional NONE = "_"
@@ -266,7 +264,7 @@
fun nbe_apps_local idx_of i c ts = nbe_fun idx_of i c `$` ml_list (rev ts);
fun nbe_apps_constr idx_of c ts =
let
- val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ sloppy_name c ^ "*)"
+ val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)"
else string_of_int (idx_of c);
in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end;
@@ -277,6 +275,7 @@
end;
+open Basic_Code_Symbol;
open Basic_Code_Thingol;
@@ -291,24 +290,24 @@
in (c, (num_args, (dicts, eqns))) end;
val eqnss' = map prep_eqns eqnss;
- fun assemble_constapp c dss ts =
+ fun assemble_constapp sym dss ts =
let
val ts' = (maps o map) assemble_dict dss @ ts;
- in case AList.lookup (op =) eqnss' c
+ in case AList.lookup (op =) eqnss' sym
of SOME (num_args, _) => if num_args <= length ts'
then let val (ts1, ts2) = chop num_args ts'
- in nbe_apps (nbe_apps_local idx_of 0 c ts1) ts2
- end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 c)) ts'
- | NONE => if member (op =) deps c
- then nbe_apps (nbe_fun idx_of 0 c) ts'
- else nbe_apps_constr idx_of c ts'
+ in nbe_apps (nbe_apps_local idx_of 0 sym ts1) ts2
+ end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 sym)) ts'
+ | NONE => if member (op =) deps sym
+ then nbe_apps (nbe_fun idx_of 0 sym) ts'
+ else nbe_apps_constr idx_of sym ts'
end
and assemble_classrels classrels =
- fold_rev (fn classrel => assemble_constapp classrel [] o single) classrels
+ fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] o single) classrels
and assemble_dict (Dict (classrels, x)) =
assemble_classrels classrels (assemble_plain_dict x)
and assemble_plain_dict (Dict_Const (inst, dss)) =
- assemble_constapp inst dss []
+ assemble_constapp (Class_Instance inst) dss []
| assemble_plain_dict (Dict_Var (v, (n, _))) =
nbe_dict v n
@@ -318,7 +317,7 @@
let
val (t', ts) = Code_Thingol.unfold_app t
in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
- and of_iapp match_cont (IConst { name = c, dicts = dss, ... }) ts = constapp c dss ts
+ and of_iapp match_cont (IConst { sym, dicts = dss, ... }) ts = constapp sym dss ts
| of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
| of_iapp match_cont ((v, _) `|=> t) ts =
nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
@@ -353,12 +352,12 @@
val (args', _) = fold_map subst_vars args samepairs;
in (samepairs, args') end;
- fun assemble_eqn c dicts default_args (i, (args, rhs)) =
+ fun assemble_eqn sym dicts default_args (i, (args, rhs)) =
let
- val match_cont = if c = "" then NONE
- else SOME (nbe_apps_local idx_of (i + 1) c (dicts @ default_args));
+ val match_cont = if Code_Symbol.is_value sym then NONE
+ else SOME (nbe_apps_local idx_of (i + 1) sym (dicts @ default_args));
val assemble_arg = assemble_iterm
- (fn c => fn dss => fn ts => nbe_apps_constr idx_of c ((maps o map) (K "_") dss @ ts)) NONE;
+ (fn sym' => fn dss => fn ts => nbe_apps_constr idx_of sym' ((maps o map) (K "_") dss @ ts)) NONE;
val assemble_rhs = assemble_iterm assemble_constapp match_cont;
val (samepairs, args') = subst_nonlin_vars args;
val s_args = map assemble_arg args';
@@ -370,17 +369,17 @@
| SOME default_rhs =>
[([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs),
([ml_list (rev (dicts @ default_args))], default_rhs)]
- in (nbe_fun idx_of i c, eqns) end;
+ in (nbe_fun idx_of i sym, eqns) end;
- fun assemble_eqns (c, (num_args, (dicts, eqns))) =
+ fun assemble_eqns (sym, (num_args, (dicts, eqns))) =
let
val default_args = map nbe_default
(Name.invent Name.context "a" (num_args - length dicts));
- val eqns' = map_index (assemble_eqn c dicts default_args) eqns
- @ (if c = "" then [] else [(nbe_fun idx_of (length eqns) c,
+ val eqns' = map_index (assemble_eqn sym dicts default_args) eqns
+ @ (if Code_Symbol.is_value sym then [] else [(nbe_fun idx_of (length eqns) sym,
[([ml_list (rev (dicts @ default_args))],
- nbe_apps_constr idx_of c (dicts @ default_args))])]);
- in (eqns', nbe_abss num_args (nbe_fun idx_of 0 c)) end;
+ nbe_apps_constr idx_of sym (dicts @ default_args))])]);
+ in (eqns', nbe_abss num_args (nbe_fun idx_of 0 sym)) end;
val (fun_vars, fun_vals) = map_split assemble_eqns eqnss';
val deps_vars = ml_list (map (nbe_fun idx_of 0) deps);
@@ -394,9 +393,9 @@
let
val ctxt = Proof_Context.init_global thy;
val (deps, deps_vals) = split_list (map_filter
- (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node nbe_program dep)))) raw_deps);
+ (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Code_Symbol.Graph.get_node nbe_program dep)))) raw_deps);
val idx_of = raw_deps
- |> map (fn dep => (dep, snd (Graph.get_node nbe_program dep)))
+ |> map (fn dep => (dep, snd (Code_Symbol.Graph.get_node nbe_program dep)))
|> AList.lookup (op =)
|> (fn f => the o f);
val s = assemble_eqnss idx_of deps eqnss;
@@ -413,45 +412,45 @@
(* extract equations from statements *)
-fun dummy_const c dss =
- IConst { name = c, typargs = [], dicts = dss,
+fun dummy_const sym dss =
+ IConst { sym = sym, typargs = [], dicts = dss,
dom = [], range = ITyVar "", annotate = false };
-fun eqns_of_stmt (_, Code_Thingol.NoStmt _) =
+fun eqns_of_stmt (_, Code_Thingol.NoStmt) =
[]
- | eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
+ | eqns_of_stmt (_, Code_Thingol.Fun ((_, []), _)) =
[]
- | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
- [(const, (vs, map fst eqns))]
+ | eqns_of_stmt (sym_const, Code_Thingol.Fun (((vs, _), eqns), _)) =
+ [(sym_const, (vs, map fst eqns))]
| eqns_of_stmt (_, Code_Thingol.Datatypecons _) =
[]
| eqns_of_stmt (_, Code_Thingol.Datatype _) =
[]
- | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
+ | eqns_of_stmt (sym_class, Code_Thingol.Class (v, (classrels, classparams))) =
let
- val names = map snd super_classes @ map fst classparams;
- val params = Name.invent Name.context "d" (length names);
- fun mk (k, name) =
- (name, ([(v, [])],
- [([dummy_const class [] `$$ map (IVar o SOME) params],
+ val syms = map Class_Relation classrels @ map (Constant o fst) classparams;
+ val params = Name.invent Name.context "d" (length syms);
+ fun mk (k, sym) =
+ (sym, ([(v, [])],
+ [([dummy_const sym_class [] `$$ map (IVar o SOME) params],
IVar (SOME (nth params k)))]));
- in map_index mk names end
+ in map_index mk syms end
| eqns_of_stmt (_, Code_Thingol.Classrel _) =
[]
| eqns_of_stmt (_, Code_Thingol.Classparam _) =
[]
- | eqns_of_stmt (inst, Code_Thingol.Classinst { class, vs, superinsts, inst_params, ... }) =
- [(inst, (vs, [([], dummy_const class [] `$$
- map (fn (_, (_, (inst, dss))) => dummy_const inst dss) superinsts
+ | eqns_of_stmt (sym_inst, Code_Thingol.Classinst { class, tyco, vs, superinsts, inst_params, ... }) =
+ [(sym_inst, (vs, [([], dummy_const (Type_Class class) [] `$$
+ map (fn (class, dss) => dummy_const (Class_Instance (tyco, class)) dss) superinsts
@ map (IConst o fst o snd o fst) inst_params)]))];
(* compile whole programs *)
fun ensure_const_idx name (nbe_program, (maxidx, idx_tab)) =
- if can (Graph.get_node nbe_program) name
+ if can (Code_Symbol.Graph.get_node nbe_program) name
then (nbe_program, (maxidx, idx_tab))
- else (Graph.new_node (name, (NONE, maxidx)) nbe_program,
+ else (Code_Symbol.Graph.new_node (name, (NONE, maxidx)) nbe_program,
(maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
fun compile_stmts thy stmts_deps =
@@ -468,20 +467,20 @@
|> rpair nbe_program;
in
fold ensure_const_idx refl_deps
- #> apfst (fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps
+ #> apfst (fold (fn (name, deps) => fold (curry Code_Symbol.Graph.add_edge name) deps) names_deps
#> compile
- #-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
+ #-> fold (fn (name, univ) => (Code_Symbol.Graph.map_node name o apfst) (K (SOME univ))))
end;
fun compile_program thy program =
let
- fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) nbe_program) names
+ fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Code_Symbol.Graph.get_node) nbe_program) names
then (nbe_program, (maxidx, idx_tab))
else (nbe_program, (maxidx, idx_tab))
- |> compile_stmts thy (map (fn name => ((name, Graph.get_node program name),
- Graph.immediate_succs program name)) names);
+ |> compile_stmts thy (map (fn name => ((name, Code_Symbol.Graph.get_node program name),
+ Code_Symbol.Graph.immediate_succs program name)) names);
in
- fold_rev add_stmts (Graph.strong_conn program)
+ fold_rev add_stmts (Code_Symbol.Graph.strong_conn program)
end;
@@ -493,7 +492,7 @@
let
val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
in
- ("", (vs, [([], t)]))
+ (Code_Symbol.value, (vs, [([], t)]))
|> singleton (compile_eqnss thy nbe_program deps)
|> snd
|> (fn t => apps t (rev dict_frees))
@@ -502,43 +501,35 @@
(* reconstruction *)
-fun typ_of_itype program vs (ityco `%% itys) =
- let
- val Code_Thingol.Datatype (tyco, _) = Graph.get_node program ityco;
- in Type (tyco, map (typ_of_itype program vs) itys) end
- | typ_of_itype program vs (ITyVar v) =
- let
- val sort = (the o AList.lookup (op =) vs) v;
- in TFree ("'" ^ v, sort) end;
+fun typ_of_itype vs (tyco `%% itys) =
+ Type (tyco, map (typ_of_itype vs) itys)
+ | typ_of_itype vs (ITyVar v) =
+ TFree ("'" ^ v, (the o AList.lookup (op =) vs) v);
-fun term_of_univ thy program idx_tab t =
+fun term_of_univ thy idx_tab t =
let
fun take_until f [] = []
- | take_until f (x::xs) = if f x then [] else x :: take_until f xs;
- fun is_dict (Const (idx, _)) = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx
- of Code_Thingol.Class _ => true
- | Code_Thingol.Classrel _ => true
- | Code_Thingol.Classinst _ => true
- | _ => false)
+ | take_until f (x :: xs) = if f x then [] else x :: take_until f xs;
+ fun is_dict (Const (idx, _)) =
+ (case Inttab.lookup idx_tab idx of
+ SOME (Constant _) => false
+ | _ => true)
| is_dict (DFree _) = true
| is_dict _ = false;
- fun const_of_idx idx = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx
- of Code_Thingol.NoStmt c => c
- | Code_Thingol.Fun (c, _) => c
- | Code_Thingol.Datatypecons (c, _) => c
- | Code_Thingol.Classparam (c, _) => c);
+ fun const_of_idx idx =
+ case Inttab.lookup idx_tab idx of SOME (Constant const) => const;
fun of_apps bounds (t, ts) =
fold_map (of_univ bounds) ts
#>> (fn ts' => list_comb (t, rev ts'))
and of_univ bounds (Const (idx, ts)) typidx =
let
val ts' = take_until is_dict ts;
- val c = const_of_idx idx;
+ val const = const_of_idx idx;
val T = map_type_tvar (fn ((v, i), _) =>
Type_Infer.param typidx (v ^ string_of_int i, []))
- (Sign.the_const_type thy c);
+ (Sign.the_const_type thy const);
val typidx' = typidx + 1;
- in of_apps bounds (Term.Const (c, T), ts') typidx' end
+ in of_apps bounds (Term.Const (const, T), ts') typidx' end
| of_univ bounds (BVar (n, ts)) typidx =
of_apps bounds (Bound (bounds - n - 1), ts) typidx
| of_univ bounds (t as Abs _) typidx =
@@ -550,11 +541,11 @@
(* evaluation with type reconstruction *)
-fun eval_term thy program (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
+fun eval_term thy (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
let
val ctxt = Syntax.init_pretty_global thy;
val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
- val ty' = typ_of_itype program vs0 ty;
+ val ty' = typ_of_itype vs0 ty;
fun type_infer t =
Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
(Type.constraint ty' t);
@@ -563,7 +554,7 @@
else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
in
compile_term thy nbe_program deps (vs, t)
- |> term_of_univ thy program idx_tab
+ |> term_of_univ thy idx_tab
|> traced (fn t => "Normalized:\n" ^ string_of_term t)
|> type_infer
|> traced (fn t => "Types inferred:\n" ^ string_of_term t)
@@ -576,8 +567,8 @@
structure Nbe_Functions = Code_Data
(
- type T = (Univ option * int) Graph.T * (int * string Inttab.table);
- val empty = (Graph.empty, (0, Inttab.empty));
+ type T = (Univ option * int) Code_Symbol.Graph.T * (int * Code_Symbol.T Inttab.table);
+ val empty = (Code_Symbol.Graph.empty, (0, Inttab.empty));
);
fun compile ignore_cache thy program =
@@ -599,26 +590,23 @@
val (_, raw_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (@{binding normalization_by_evaluation},
- fn (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
- mk_equals thy ct (eval_term thy program nbe_program_idx_tab vsp_ty_t deps))));
+ fn (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
+ mk_equals thy ct (eval_term thy nbe_program_idx_tab vsp_ty_t deps))));
-fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct =
- raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct);
+fun oracle thy nbe_program_idx_tab vsp_ty_t deps ct =
+ raw_oracle (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct);
-fun dynamic_conv thy = lift_triv_classes_conv thy (Code_Thingol.dynamic_conv thy
- (K (fn program => oracle thy program (compile false thy program))));
+fun dynamic_conv thy = lift_triv_classes_conv thy
+ (Code_Thingol.dynamic_conv thy (oracle thy o compile false thy));
fun dynamic_value thy = lift_triv_classes_rew thy
- (Code_Thingol.dynamic_value thy I
- (K (fn program => eval_term thy program (compile false thy program))));
+ (Code_Thingol.dynamic_value thy I (eval_term thy o compile false thy));
-fun static_conv thy consts =
- lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts
- (K (fn program => fn _ => oracle thy program (compile true thy program))));
+fun static_conv thy consts = lift_triv_classes_conv thy
+ (Code_Thingol.static_conv thy consts (K o oracle thy o compile true thy));
fun static_value thy consts = lift_triv_classes_rew thy
- (Code_Thingol.static_value thy I consts
- (K (fn program => fn _ => eval_term thy program (compile true thy program))));
+ (Code_Thingol.static_value thy I consts (K o eval_term thy o compile true thy));
(** setup **)
--- a/src/ZF/ind_syntax.ML Mon Jan 27 16:38:52 2014 +0000
+++ b/src/ZF/ind_syntax.ML Mon Jan 27 17:13:33 2014 +0000
@@ -50,7 +50,7 @@
(*For deriving cases rules. CollectD2 discards the domain, which is redundant;
read_instantiate replaces a propositional variable by a formula variable*)
val equals_CollectD =
- read_instantiate @{context} [(("W", 0), "?Q")]
+ Rule_Insts.read_instantiate @{context} [(("W", 0), "Q")] ["Q"]
(make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));