# HG changeset patch # User paulson # Date 1390842813 0 # Node ID 39bcdf19dd14c5a483d15b95e2d2bc0263347653 # Parent 06897ea77f7878bf6f45586a999b9dee2cea11eb# Parent 3ca79ee6eb335dbe1020d5bcb592b8644ee3aaba Merge diff -r 06897ea77f78 -r 39bcdf19dd14 .hgignore --- 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 diff -r 06897ea77f78 -r 39bcdf19dd14 Admin/user-aliases --- 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 diff -r 06897ea77f78 -r 39bcdf19dd14 NEWS --- 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 diff -r 06897ea77f78 -r 39bcdf19dd14 src/Doc/Codegen/Adaptation.thy --- 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", K I)) - #> Code_Target.extend_target ("\", ("Haskell", K I)) *} +setup %invisible {* Code_Target.extend_target ("\", ("SML", I)) + #> Code_Target.extend_target ("\", ("Haskell", I)) *} section {* Adaptation to target languages \label{sec:adaptation} *} diff -r 06897ea77f78 -r 39bcdf19dd14 src/Doc/IsarRef/Generic.thy --- 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. diff -r 06897ea77f78 -r 39bcdf19dd14 src/Doc/IsarRef/Proof.thy --- 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})? \ + (@'for' (@{syntax vars} + @'and'))? ; @@{attribute "where"} ((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '=' - (@{syntax type} | @{syntax term}) * @'and') + (@{syntax type} | @{syntax term}) * @'and') \ + (@'for' (@{syntax vars} + @'and'))? \} \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 "\ x\<^sub>1 \ 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 \ \ 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 "\ x\<^sub>1 \ x\<^sub>m"} may + be specified as for @{attribute "of"} above. + \end{description} *} diff -r 06897ea77f78 -r 39bcdf19dd14 src/Doc/Tutorial/Protocol/Event.thy --- 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} \ 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 \ analz (knows Spy evs)", standard] +lemmas analz_impI = impI [where P = "Y \ 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 \ synth (analz (knows Spy evs))", standard] +lemmas syan_impI = impI [where P = "Y \ synth (analz (knows Spy evs))"] for Y evs ML {* diff -r 06897ea77f78 -r 39bcdf19dd14 src/Doc/Tutorial/Protocol/Message.thy --- 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 \ 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. *} diff -r 06897ea77f78 -r 39bcdf19dd14 src/Doc/isar.sty --- 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}} diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Bali/AxExample.thy --- 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" - "\Y s Z. arr_inv (snd s) \ tprg,s\catch SXcpt NullPointer" *}) + "\Y s Z. arr_inv (snd s) \ tprg,s\catch SXcpt NullPointer" [] *}) prefer 2 apply simp apply (rule_tac P' = "Normal (\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'" "\a. Normal (?PP a\?x)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\a. Normal (PP a\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'" "\a vs l vf. ?PP a vs l vf\?x \. ?p" *}) +apply (tactic {* inst1_tac @{context} "P'" "\a vs l vf. PP a vs l vf\x \. 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" "\a'. Normal ((\Vals:vs (x, s) Z. arr_inv s \ inited Ext (globs s) \ a' \ Null \ vs = [Null]) \. heap_free two)" *}) +apply (tactic {* inst1_tac @{context} "R" "\a'. Normal ((\Vals:vs (x, s) Z. arr_inv s \ inited Ext (globs s) \ a' \ Null \ vs = [Null]) \. 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'" "\a. Normal (?PP a\?x)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\a. Normal (PP a\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'" "\aa v. Normal (?QQ aa v\?y)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\aa v. Normal (QQ aa v\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'" "\vf. Normal (?PP vf \. ?p)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\vf. Normal (PP vf \. 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'" "\vf l vfa. Normal (?P vf l vfa)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\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" "\vf l vfa. Normal (?P vf l vfa\\)" *}) +apply (tactic {* inst1_tac @{context} "P" "\vf l vfa. Normal (P vf l vfa\\)" ["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" "\vf. Normal ((\Y s Z. vf=lvar (VName e) (snd s)) \. heap_free four \. initd Base \. initd Ext)" *}) +apply (tactic {* inst1_tac @{context} "Q" "\vf. Normal ((\Y s Z. vf=lvar (VName e) (snd s)) \. heap_free four \. initd Base \. 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" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. initd Ext)" *}) +apply (tactic {* inst1_tac @{context} "P" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. initd Ext)" [] *}) apply clarsimp -apply (tactic {* inst1_tac @{context} "PP" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. Not \ initd Base)" *}) +apply (tactic {* inst1_tac @{context} "PP" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. Not \ 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 (\s.. (\Y s Z. True)\=Val (the (locals s i)))" *}) + {* inst1_tac @{context} "P'" "Normal (\s.. (\Y s Z. True)\=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'" "\b Y ba Z vf. \Y (x,s) Z. x=None \ snd vf = snd (lvar i s)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\b Y ba Z vf. \Y (x,s) Z. x=None \ snd vf = snd (lvar i s)" [] *}) apply (rule allI) apply (rule_tac P' = "Normal ?P" in conseq1) prefer 2 diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Bali/Basis.thy --- 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 \ the_Inr \ 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] *) diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/IMP/Hoare_Total.thy --- 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: "\\<^sub>t {P}c{Q} \ \\<^sub>t {P}c{Q}" +by (metis hoaret_sound hoaret_complete) + end diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Library/Binomial.thy --- 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 diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Library/Numeral_Type.thy --- 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 *} diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/List.thy --- 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; diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- 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 \ Basis" have "norm (\x\P. \f x \ i\) \ norm ((\x\P \ - {x. f x \ i < 0}. f x) \ i) + norm ((\x\P \ {x. f x \ i < 0}. f x) \ 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 "\ \ e + e" unfolding real_norm_def by (intro add_mono norm_bound_Basis_le i fPs) auto diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Number_Theory/Binomial.thy --- 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 \ A \ I \ {} \ x \ \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 = (\(i, I)\(SIGMA i:{1..card A}. ?I i). -1 ^ (i + 1))" by(rule setsum_reindex_cong[where f=snd]) fastforce also have "\ = (\i=1..card A. (\I|I \ A \ card I = i \ x \ \I. -1 ^ (i + 1)))" diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Prolog/prolog.ML --- 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)) diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Quickcheck_Narrowing.thy --- 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 \ (Haskell_Quickcheck) "Typerep" diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Quickcheck_Random.thy --- 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 "\>" 60) notation scomp (infixl "\\" 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 *} diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Rat.thy --- 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, diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Set.thy --- 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 \ (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 \ 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 diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Set_Interval.thy --- 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.. 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) = diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Tools/TFL/post.ML --- 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; diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Tools/numeral.ML --- 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*) diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/Tools/string_code.ML --- 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; diff -r 06897ea77f78 -r 39bcdf19dd14 src/HOL/ex/Cartouche_Examples.thy --- 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 \ string" ("STR _") +syntax "_cartouche_string" :: "cartouche_position \ string" ("_") parse_translation {* - [(@{syntax_const "_STR_cartouche"}, + [(@{syntax_const "_cartouche_string"}, K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))] *} -term "STR \\" -term "STR \abc\" -term "STR \abc\ @ STR \xyz\" -term "STR \\\" -term "STR \\001\010\100\" +term "\\" +term "\abc\" +term "\abc\ @ \xyz\" +term "\\\" +term "\\001\010\100\" subsection {* Alternate outer and inner syntax: string literals *} subsubsection {* Nested quotes *} -syntax "_STR_string" :: "string_position \ string" ("STR _") +syntax "_string_string" :: "string_position \ 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 \"\\"" -term "STR \"\001\010\100\"" +term "\"\"" +term "\"abc\"" +term "\"abc\" @ \"xyz\"" +term "\"\\"" +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 \STR ""\ -term_cartouche \STR "abc"\ -term_cartouche \STR "abc" @ STR "xyz"\ -term_cartouche \STR "\"\ -term_cartouche \STR "\001\010\100"\ +term_cartouche \""\ +term_cartouche \"abc"\ +term_cartouche \"abc" @ "xyz"\ +term_cartouche \"\"\ +term_cartouche \"\001\010\100"\ subsubsection {* Further nesting: antiquotations *} @@ -125,22 +125,22 @@ *} ML {* - @{term_cartouche \STR ""\}; - @{term_cartouche \STR "abc"\}; - @{term_cartouche \STR "abc" @ STR "xyz"\}; - @{term_cartouche \STR "\"\}; - @{term_cartouche \STR "\001\010\100"\}; + @{term_cartouche \""\}; + @{term_cartouche \"abc"\}; + @{term_cartouche \"abc" @ "xyz"\}; + @{term_cartouche \"\"\}; + @{term_cartouche \"\001\010\100"\}; *} text {* @{ML_cartouche \ ( - @{term_cartouche \STR ""\}; - @{term_cartouche \STR "abc"\}; - @{term_cartouche \STR "abc" @ STR "xyz"\}; - @{term_cartouche \STR "\"\}; - @{term_cartouche \STR "\001\010\100"\} + @{term_cartouche \""\}; + @{term_cartouche \"abc"\}; + @{term_cartouche \"abc" @ "xyz"\}; + @{term_cartouche \"\"\}; + @{term_cartouche \"\001\010\100"\} ) \ } @@ -160,11 +160,11 @@ @{ML_cartouche \ ( - @{term_cartouche \STR ""\}; - @{term_cartouche \STR "abc"\}; - @{term_cartouche \STR "abc" @ STR "xyz"\}; - @{term_cartouche \STR "\"\}; - @{term_cartouche \STR "\001\010\100"\} + @{term_cartouche \""\}; + @{term_cartouche \"abc"\}; + @{term_cartouche \"abc" @ "xyz"\}; + @{term_cartouche \"\"\}; + @{term_cartouche \"\001\010\100"\} ) \ } diff -r 06897ea77f78 -r 39bcdf19dd14 src/Pure/General/graph.ML --- 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); diff -r 06897ea77f78 -r 39bcdf19dd14 src/Pure/Isar/args.ML --- 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); diff -r 06897ea77f78 -r 39bcdf19dd14 src/Pure/Isar/attrib.ML --- 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 *) diff -r 06897ea77f78 -r 39bcdf19dd14 src/Pure/Isar/calculation.ML --- 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; diff -r 06897ea77f78 -r 39bcdf19dd14 src/Pure/Isar/isar_syn.ML --- 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))); diff -r 06897ea77f78 -r 39bcdf19dd14 src/Pure/Isar/token.scala --- 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) } diff -r 06897ea77f78 -r 39bcdf19dd14 src/Pure/Pure.thy --- 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 *} diff -r 06897ea77f78 -r 39bcdf19dd14 src/Pure/ROOT --- 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" diff -r 06897ea77f78 -r 39bcdf19dd14 src/Pure/ROOT.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*) diff -r 06897ea77f78 -r 39bcdf19dd14 src/Pure/System/session.scala --- 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() } //}}} diff -r 06897ea77f78 -r 39bcdf19dd14 src/Pure/Thy/thy_load.scala --- 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() { } } diff -r 06897ea77f78 -r 39bcdf19dd14 src/Pure/Thy/thy_syntax.scala --- 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)) } } } diff -r 06897ea77f78 -r 39bcdf19dd14 src/Pure/Tools/rule_insts.ML --- 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 = diff -r 06897ea77f78 -r 39bcdf19dd14 src/Tools/Code/code_haskell.ML --- 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, diff -r 06897ea77f78 -r 39bcdf19dd14 src/Tools/Code/code_ml.ML --- 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) diff -r 06897ea77f78 -r 39bcdf19dd14 src/Tools/Code/code_namespace.ML --- 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; diff -r 06897ea77f78 -r 39bcdf19dd14 src/Tools/Code/code_printer.ML --- 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 diff -r 06897ea77f78 -r 39bcdf19dd14 src/Tools/Code/code_runtime.ML --- 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 [])); diff -r 06897ea77f78 -r 39bcdf19dd14 src/Tools/Code/code_scala.ML --- 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!*), diff -r 06897ea77f78 -r 39bcdf19dd14 src/Tools/Code/code_simp.ML --- 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); diff -r 06897ea77f78 -r 39bcdf19dd14 src/Tools/Code/code_symbol.ML --- 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; diff -r 06897ea77f78 -r 39bcdf19dd14 src/Tools/Code/code_target.ML --- 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; diff -r 06897ea77f78 -r 39bcdf19dd14 src/Tools/Code/code_thingol.ML --- 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; diff -r 06897ea77f78 -r 39bcdf19dd14 src/Tools/jEdit/src/jedit_thy_load.scala --- 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() } } diff -r 06897ea77f78 -r 39bcdf19dd14 src/Tools/nbe.ML --- 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 **) diff -r 06897ea77f78 -r 39bcdf19dd14 src/ZF/ind_syntax.ML --- 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}));