# HG changeset patch # User wenzelm # Date 1369601868 -7200 # Node ID 3c18725d576af76358c40446034ea7f976d1fd8e # Parent f5773a46cf058afd700bb9cf761820b1979bd477# Parent 72e83c82c1d487786951e4ae3655290fddaa37f3 merged diff -r f5773a46cf05 -r 3c18725d576a src/HOL/Tools/case_translation.ML --- 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; diff -r f5773a46cf05 -r 3c18725d576a src/Pure/Isar/proof_context.ML --- 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; diff -r f5773a46cf05 -r 3c18725d576a src/Pure/Syntax/syntax.ML --- 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 **) diff -r f5773a46cf05 -r 3c18725d576a src/Pure/Syntax/syntax_phases.ML --- 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) diff -r f5773a46cf05 -r 3c18725d576a src/Pure/Syntax/syntax_trans.ML --- 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), diff -r f5773a46cf05 -r 3c18725d576a src/Pure/pure_thy.ML --- 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 diff -r f5773a46cf05 -r 3c18725d576a src/Pure/term.ML --- 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; diff -r f5773a46cf05 -r 3c18725d576a src/Tools/Code/code_target.ML --- 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); diff -r f5773a46cf05 -r 3c18725d576a src/Tools/Code/code_thingol.ML --- 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;