--- a/src/HOL/Tools/case_translation.ML Sun May 26 19:45:54 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML Sun May 26 22:57:48 2013 +0200
@@ -90,25 +90,30 @@
val lookup_by_case = Symtab.lookup o cases_of;
+
(** installation **)
fun case_error s = error ("Error in case expression:\n" ^ s);
val name_of = try (dest_Const #> fst);
+
(* parse translation *)
fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
fun case_tr err ctxt [t, u] =
let
- val thy = Proof_Context.theory_of ctxt;
+ val consts = Proof_Context.consts_of ctxt;
+ fun is_const s = can (Consts.the_constraint consts) (Consts.intern consts s);
- fun is_const s =
- Sign.declared_const thy (Proof_Context.intern_const ctxt s);
+ fun variant_free x used =
+ let val (x', used') = Name.variant x used
+ in if is_const x' then variant_free x' used' else (x', used') end;
- fun abs p tTs t = Syntax.const @{const_syntax case_abs} $
- fold constrain_Abs tTs (absfree p t);
+ fun abs p tTs t =
+ Syntax.const @{const_syntax case_abs} $
+ fold constrain_Abs tTs (absfree p t);
fun abs_pat (Const (@{syntax_const "_constrain"}, _) $ t $ tT) tTs =
abs_pat t (tT :: tTs)
@@ -119,7 +124,7 @@
(* replace occurrences of dummy_pattern by distinct variables *)
fun replace_dummies (Const (@{const_syntax dummy_pattern}, T)) used =
- let val (x, used') = Name.variant "x" used
+ let val (x, used') = variant_free "x" used
in (Free (x, T), used') end
| replace_dummies (t $ u) used =
let
@@ -129,9 +134,9 @@
| replace_dummies t used = (t, used);
fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) =
- let val (l', _) = replace_dummies l (Term.declare_term_frees t Name.context)
- in abs_pat l' []
- (Syntax.const @{const_syntax case_elem} $ Term_Position.strip_positions l' $ r)
+ let val (l', _) = replace_dummies l (Term.declare_term_frees t Name.context) in
+ abs_pat l' []
+ (Syntax.const @{const_syntax case_elem} $ Term_Position.strip_positions l' $ r)
end
| dest_case1 _ = case_error "dest_case1";
@@ -140,11 +145,11 @@
val errt = if err then @{term True} else @{term False};
in
- Syntax.const @{const_syntax case_guard} $ errt $ t $ (fold_rev
- (fn t => fn u =>
- Syntax.const @{const_syntax case_cons} $ dest_case1 t $ u)
- (dest_case2 u)
- (Syntax.const @{const_syntax case_nil}))
+ Syntax.const @{const_syntax case_guard} $ errt $ t $
+ (fold_rev
+ (fn t => fn u => Syntax.const @{const_syntax case_cons} $ dest_case1 t $ u)
+ (dest_case2 u)
+ (Syntax.const @{const_syntax case_nil}))
end
| case_tr _ _ _ = case_error "case_tr";
@@ -161,17 +166,19 @@
| mk_clause (Const (@{const_syntax case_elem}, _) $ pat $ rhs) xs _ =
Syntax.const @{syntax_const "_case1"} $
subst_bounds (map Syntax_Trans.mark_bound_abs xs, pat) $
- subst_bounds (map Syntax_Trans.mark_bound_body xs, rhs);
+ subst_bounds (map Syntax_Trans.mark_bound_body xs, rhs)
+ | mk_clause _ _ _ = raise Match;
fun mk_clauses (Const (@{const_syntax case_nil}, _)) = []
| mk_clauses (Const (@{const_syntax case_cons}, _) $ t $ u) =
- mk_clause t [] (Term.declare_term_frees t Name.context) ::
- mk_clauses u
+ mk_clause t [] (Term.declare_term_frees t Name.context) :: mk_clauses u
+ | mk_clauses _ = raise Match;
in
list_comb (Syntax.const @{syntax_const "_case_syntax"} $ x $
foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
(mk_clauses t), ts)
- end;
+ end
+ | case_tr' _ = raise Match;
val trfun_setup' = Sign.print_translation [(@{const_syntax "case_guard"}, K case_tr')];
@@ -204,13 +211,13 @@
(*Each pattern carries with it a tag i, which denotes the clause it
-came from. i = ~1 indicates that the clause was added by pattern
-completion.*)
+ came from. i = ~1 indicates that the clause was added by pattern
+ completion.*)
-fun add_row_used ((prfx, pats), (tm, tag)) =
+fun add_row_used ((prfx, pats), (tm, _)) =
fold Term.declare_term_frees (tm :: pats @ map Free prfx);
-(* try to preserve names given by user *)
+(*try to preserve names given by user*)
fun default_name "" (Free (name', _)) = name'
| default_name name _ = name;
@@ -220,8 +227,9 @@
let
val (_, T) = dest_Const c;
val Ts = binder_types T;
- val (names, _) = fold_map Name.variant
- (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)) used;
+ val (names, _) =
+ fold_map Name.variant
+ (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)) used;
val ty = body_type T;
val ty_theta = Type.raw_match (ty, colty) Vartab.empty
handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);
@@ -251,8 +259,7 @@
(* Partitioning *)
fun partition _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
- | partition used constructors colty res_ty
- (rows as (((prfx, _ :: ps), _) :: _)) =
+ | partition used constructors colty res_ty (rows as (((prfx, _ :: ps), _) :: _)) =
let
fun part [] [] = []
| part [] ((_, (_, i)) :: _) = raise CASE_ERROR ("Not a constructor pattern", i)
@@ -293,7 +300,7 @@
let
val get_info = lookup_by_constr_permissive ctxt;
- fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand", ~1)
+ fun expand _ _ _ ((_, []), _) = raise CASE_ERROR ("mk_case: expand", ~1)
| expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
if is_Free p then
let
@@ -308,11 +315,10 @@
fun mk _ [] = raise CASE_ERROR ("no rows", ~1)
| mk [] (((_, []), (tm, tag)) :: _) = ([tag], tm) (* Done *)
- | mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) = mk path [row]
+ | mk path ((row as ((_, [Free _]), _)) :: _ :: _) = mk path [row]
| mk (u :: us) (rows as ((_, _ :: _), _) :: _) =
let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in
- (case Option.map (apfst head_of)
- (find_first (not o is_Free o fst) col0) of
+ (case Option.map (apfst head_of) (find_first (not o is_Free o fst) col0) of
NONE =>
let
val rows' = map (fn ((v, _), row) => row ||>
@@ -326,8 +332,7 @@
val pty = body_type cT;
val used' = fold Term.declare_term_frees us used;
val nrows = maps (expand constructors used' pty) rows;
- val subproblems =
- partition used' constructors pty range_ty nrows;
+ val subproblems = partition used' constructors pty range_ty nrows;
val (pat_rect, dtrees) =
split_list (map (fn {new_formals, group, ...} =>
mk (new_formals @ us) group) subproblems);
@@ -509,13 +514,13 @@
encode_clause recur S T p $ encode_cases recur S T ps;
fun encode_case recur (t, ps as (pat, rhs) :: _) =
- let
- val tT = fastype_of t;
- val T = fastype_of rhs;
- in
- Const (@{const_name case_guard}, @{typ bool} --> tT --> (tT --> T) --> T) $
- @{term True} $ t $ (encode_cases recur (fastype_of pat) (fastype_of rhs) ps)
- end
+ let
+ val tT = fastype_of t;
+ val T = fastype_of rhs;
+ in
+ Const (@{const_name case_guard}, @{typ bool} --> tT --> (tT --> T) --> T) $
+ @{term True} $ t $ (encode_cases recur (fastype_of pat) (fastype_of rhs) ps)
+ end
| encode_case _ _ = case_error "encode_case";
fun strip_case' ctxt d (pat, rhs) =
@@ -542,8 +547,8 @@
(strip_case_full ctxt d x, maps (strip_case' ctxt d) clauses)
| NONE =>
(case t of
- (t $ u) => strip_case_full ctxt d t $ strip_case_full ctxt d u
- | (Abs (x, T, u)) =>
+ t $ u => strip_case_full ctxt d t $ strip_case_full ctxt d u
+ | Abs (x, T, u) =>
let val (x', u') = Term.dest_abs (x, T, u);
in Term.absfree (x', T) (strip_case_full ctxt d u') end
| _ => t));
@@ -577,17 +582,25 @@
fun print_case_translations ctxt =
let
- val cases = Symtab.dest (cases_of ctxt);
- fun show_case (_, data as (comb, ctrs)) =
- (Pretty.block o Pretty.fbreaks)
- [Pretty.block [Pretty.str (Tname_of_data data), Pretty.str ":"],
- Pretty.block [Pretty.brk 3, Pretty.block
- [Pretty.str "combinator:", Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt comb)]],
- Pretty.block [Pretty.brk 3, Pretty.block
- [Pretty.str "constructors:", Pretty.brk 1,
- Pretty.block (Pretty.commas (map (Pretty.quote o Syntax.pretty_term ctxt) ctrs))]]];
+ val cases = map snd (Symtab.dest (cases_of ctxt));
+ val type_space = Proof_Context.type_space ctxt;
+
+ val pretty_term = Syntax.pretty_term ctxt;
+
+ fun pretty_data (data as (comb, ctrs)) =
+ let
+ val name = Tname_of_data data;
+ val xname = Name_Space.extern ctxt type_space name;
+ val markup = Name_Space.markup type_space name;
+ val prt =
+ (Pretty.block o Pretty.fbreaks)
+ [Pretty.block [Pretty.mark_str (markup, xname), Pretty.str ":"],
+ Pretty.block [Pretty.str "combinator:", Pretty.brk 1, pretty_term comb],
+ Pretty.block (Pretty.str "constructors:" :: Pretty.brk 1 ::
+ Pretty.commas (map pretty_term ctrs))];
+ in (xname, prt) end;
in
- Pretty.big_list "case translations:" (map show_case cases)
+ Pretty.big_list "case translations:" (map #2 (sort_wrt #1 (map pretty_data cases)))
|> Pretty.writeln
end;
--- a/src/Pure/Isar/proof_context.ML Sun May 26 19:45:54 2013 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun May 26 22:57:48 2013 +0200
@@ -28,7 +28,6 @@
val set_defsort: sort -> Proof.context -> Proof.context
val default_sort: Proof.context -> indexname -> sort
val consts_of: Proof.context -> Consts.T
- val the_const_constraint: Proof.context -> string -> typ
val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
val facts_of: Proof.context -> Facts.T
@@ -264,8 +263,6 @@
fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
val consts_of = #1 o #consts o rep_data;
-val the_const_constraint = Consts.the_constraint o consts_of;
-
val facts_of = #facts o rep_data;
val cases_of = #cases o rep_data;
--- a/src/Pure/Syntax/syntax.ML Sun May 26 19:45:54 2013 +0200
+++ b/src/Pure/Syntax/syntax.ML Sun May 26 22:57:48 2013 +0200
@@ -91,8 +91,6 @@
val mode_input: mode
val empty_syntax: syntax
val merge_syntax: syntax * syntax -> syntax
- val token_markers: string list
- val basic_nonterms: string list
val print_gram: syntax -> unit
val print_trans: syntax -> unit
val print_syntax: syntax -> unit
@@ -528,20 +526,6 @@
end;
-(* basic syntax *)
-
-val token_markers =
- ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
-
-val basic_nonterms =
- Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
- "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
- "any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
- "float_position", "xnum_position", "index", "struct", "tid_position",
- "tvar_position", "id_position", "longid_position", "var_position", "str_position",
- "type_name", "class_name"];
-
-
(** print syntax **)
--- a/src/Pure/Syntax/syntax_phases.ML Sun May 26 19:45:54 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Sun May 26 22:57:48 2013 +0200
@@ -151,11 +151,16 @@
then [Ast.Variable (Lexicon.str_of_token tok)]
else [];
+ fun ast_of_position tok =
+ Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok));
+
+ fun ast_of_dummy a tok =
+ if raw then Ast.Constant a
+ else Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok];
+
fun asts_of_position c tok =
if raw then asts_of_token tok
- else
- [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok),
- Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
+ else [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
let
@@ -174,6 +179,12 @@
in [Ast.Constant (Lexicon.mark_type c)] end
| asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
| asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
+ | asts_of (Parser.Node (a as "\\<^const>dummy_pattern", [Parser.Tip tok])) =
+ [ast_of_dummy a tok]
+ | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) =
+ [ast_of_dummy a tok]
+ | asts_of (Parser.Node ("_idtypdummy", pts as [Parser.Tip tok, _, _])) =
+ [Ast.Appl (Ast.Constant "_constrain" :: ast_of_dummy "_idtdummy" tok :: maps asts_of pts)]
| asts_of (Parser.Node (a, pts)) =
let
val _ = pts |> List.app
@@ -517,7 +528,7 @@
val {structs, fixes} = idents;
fun mark_atoms ((t as Const (c, _)) $ u) =
- if member (op =) Syntax.token_markers c
+ if member (op =) Pure_Thy.token_markers c
then t $ u else mark_atoms t $ mark_atoms u
| mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
| mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
--- a/src/Pure/Syntax/syntax_trans.ML Sun May 26 19:45:54 2013 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Sun May 26 22:57:48 2013 +0200
@@ -121,9 +121,6 @@
fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]
| idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
-fun idtypdummy_ast_tr [ty] = Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty]
- | idtypdummy_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
-
fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
| lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
@@ -513,7 +510,6 @@
("_applC", fn _ => applC_ast_tr),
("_lambda", fn _ => lambda_ast_tr),
("_idtyp", fn _ => idtyp_ast_tr),
- ("_idtypdummy", fn _ => idtypdummy_ast_tr),
("_bigimpl", fn _ => bigimpl_ast_tr),
("_indexdefault", fn _ => indexdefault_ast_tr),
("_indexvar", fn _ => indexvar_ast_tr),
--- a/src/Pure/pure_thy.ML Sun May 26 19:45:54 2013 +0200
+++ b/src/Pure/pure_thy.ML Sun May 26 22:57:48 2013 +0200
@@ -8,6 +8,7 @@
sig
val old_appl_syntax: theory -> bool
val old_appl_syntax_setup: theory -> theory
+ val token_markers: string list
end;
structure Pure_Thy: PURE_THY =
@@ -52,6 +53,9 @@
(* main content *)
+val token_markers =
+ ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
+
val _ = Context.>> (Context.map_theory
(Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
Old_Appl_Syntax.put false #>
@@ -60,8 +64,15 @@
(Binding.name "prop", 0, NoSyn),
(Binding.name "itself", 1, NoSyn),
(Binding.name "dummy", 0, NoSyn)]
- #> Sign.add_nonterminals_global (map Binding.name Syntax.basic_nonterms)
- #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) Syntax.token_markers)
+ #> Sign.add_nonterminals_global
+ (map Binding.name
+ (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
+ "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
+ "any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
+ "float_position", "xnum_position", "index", "struct", "tid_position",
+ "tvar_position", "id_position", "longid_position", "var_position", "str_position",
+ "type_name", "class_name"]))
+ #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) token_markers)
#> Sign.add_syntax_i
[("", typ "prop' => prop", Delimfix "_"),
("", typ "logic => any", Delimfix "_"),
@@ -153,7 +164,7 @@
("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
(const "==>", typ "prop => prop => prop", Delimfix "op ==>"),
- (const Term.dummy_patternN, typ "aprop", Delimfix "'_"),
+ (const "dummy_pattern", typ "aprop", Delimfix "'_"),
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
(const "Pure.term", typ "logic => prop", Delimfix "TERM _"),
(const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
@@ -183,12 +194,12 @@
(Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
(Binding.name "prop", typ "prop => prop", NoSyn),
(Binding.name "TYPE", typ "'a itself", NoSyn),
- (Binding.name Term.dummy_patternN, typ "'a", Delimfix "'_")]
+ (Binding.name "dummy_pattern", typ "'a", Delimfix "'_")]
#> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
#> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
#> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
#> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
- #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
+ #> Theory.add_deps_global "dummy_pattern" ("dummy_pattern", typ "'a") []
#> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
#> Sign.parse_translation Syntax_Trans.pure_parse_translation
#> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
--- a/src/Pure/term.ML Sun May 26 19:45:54 2013 +0200
+++ b/src/Pure/term.ML Sun May 26 22:57:48 2013 +0200
@@ -159,7 +159,6 @@
val maxidx_term: term -> int -> int
val has_abs: term -> bool
val dest_abs: string * typ * term -> string * term
- val dummy_patternN: string
val dummy_pattern: typ -> term
val dummy: term
val dummy_prop: term
@@ -925,9 +924,7 @@
(* dummy patterns *)
-val dummy_patternN = "dummy_pattern";
-
-fun dummy_pattern T = Const (dummy_patternN, T);
+fun dummy_pattern T = Const ("dummy_pattern", T);
val dummy = dummy_pattern dummyT;
val dummy_prop = dummy_pattern propT;
--- a/src/Tools/Code/code_target.ML Sun May 26 19:45:54 2013 +0200
+++ b/src/Tools/Code/code_target.ML Sun May 26 22:57:48 2013 +0200
@@ -419,7 +419,7 @@
val value_name = "Value.value.value"
val program = prepared_program
|> Graph.new_node (value_name,
- Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
+ 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;
val (program_code, deresolve) = produce (mounted_serializer program);
val value_name' = the (deresolve value_name);
--- a/src/Tools/Code/code_thingol.ML Sun May 26 19:45:54 2013 +0200
+++ b/src/Tools/Code/code_thingol.ML Sun May 26 22:57:48 2013 +0200
@@ -938,24 +938,24 @@
val ty = fastype_of t;
val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
o dest_TFree))) t [];
- val t' = annotate thy algbr eqngr (Term.dummy_patternN, ty) [] t;
+ val t' = annotate thy algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
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
- (Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
+ (@{const_name dummy_pattern}, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
fun term_value (dep, (naming, program1)) =
let
val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
- Graph.get_node program1 Term.dummy_patternN;
- val deps = Graph.immediate_succs program1 Term.dummy_patternN;
- val program2 = Graph.del_node Term.dummy_patternN program1;
+ 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;
in
- ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
+ ensure_stmt ((K o K) NONE) pair stmt_value @{const_name dummy_pattern}
#> snd
#> term_value
end;