# HG changeset patch # User wenzelm # Date 1325783919 -3600 # Node ID 00cd193a48dc142af3b166bddbd6278ca8ac14fe # Parent 3ee75fe01986ed14666abe24bdab2bb7dc8274e5 improved case syntax: more careful treatment of position constraints, which enables PIDE markup; tuned; diff -r 3ee75fe01986 -r 00cd193a48dc NEWS --- a/NEWS Thu Jan 05 15:31:49 2012 +0100 +++ b/NEWS Thu Jan 05 18:18:39 2012 +0100 @@ -60,6 +60,12 @@ *** HOL *** +* Concrete syntax for case expressions includes constraints for source +positions, and thus produces Prover IDE markup for its bindings. +INCOMPATIBILITY for old-style syntax translations that augment the +pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of +one_case. + * Finite_Set.fold now qualified. INCOMPATIBILITY. * Renamed some facts on canonical fold on lists, in order to avoid problems diff -r 3ee75fe01986 -r 00cd193a48dc src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Jan 05 15:31:49 2012 +0100 +++ b/src/HOL/HOL.thy Thu Jan 05 18:18:39 2012 +0100 @@ -104,34 +104,31 @@ notation (xsymbols) iff (infixr "\" 25) -nonterminal letbinds and letbind -nonterminal case_pat and case_syn and cases_syn +syntax + "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) +translations + "THE x. P" == "CONST The (%x. P)" +print_translation {* + [(@{const_syntax The}, fn [Abs abs] => + let val (x, t) = Syntax_Trans.atomic_abs_tr' abs + in Syntax.const @{syntax_const "_The"} $ x $ t end)] +*} -- {* To avoid eta-contraction of body *} +nonterminal letbinds and letbind syntax - "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) - "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) "" :: "letbind => letbinds" ("_") "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" [0, 10] 10) - "_case_syntax" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) - "_case1" :: "[case_pat, 'b] => case_syn" ("(2_ =>/ _)" 10) - "" :: "case_syn => cases_syn" ("_") - "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") - "_strip_positions" :: "'a => case_pat" ("_") - +nonterminal case_syn and cases_syn +syntax + "_case_syntax" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) + "_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) + "" :: "case_syn => cases_syn" ("_") + "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") syntax (xsymbols) - "_case1" :: "[case_pat, 'b] => case_syn" ("(2_ \/ _)" 10) - -translations - "THE x. P" == "CONST The (%x. P)" - -print_translation {* - [(@{const_syntax The}, fn [Abs abs] => - let val (x, t) = Syntax_Trans.atomic_abs_tr' abs - in Syntax.const @{syntax_const "_The"} $ x $ t end)] -*} -- {* To avoid eta-contraction of body *} + "_case1" :: "['a, 'b] => case_syn" ("(2_ \/ _)" 10) notation (xsymbols) All (binder "\" 10) and diff -r 3ee75fe01986 -r 00cd193a48dc src/HOL/HOLCF/One.thy --- a/src/HOL/HOLCF/One.thy Thu Jan 05 15:31:49 2012 +0100 +++ b/src/HOL/HOLCF/One.thy Thu Jan 05 18:18:39 2012 +0100 @@ -58,6 +58,7 @@ translations "case x of XCONST ONE \ t" == "CONST one_case\t\x" + "case x of XCONST ONE :: 'a \ t" => "CONST one_case\t\x" "\ (XCONST ONE). t" == "CONST one_case\t" lemma one_case1 [simp]: "(case \ of ONE \ t) = \" diff -r 3ee75fe01986 -r 00cd193a48dc src/HOL/HOLCF/Ssum.thy --- a/src/HOL/HOLCF/Ssum.thy Thu Jan 05 15:31:49 2012 +0100 +++ b/src/HOL/HOLCF/Ssum.thy Thu Jan 05 18:18:39 2012 +0100 @@ -168,6 +168,7 @@ translations "case s of XCONST sinl\x \ t1 | XCONST sinr\y \ t2" == "CONST sscase\(\ x. t1)\(\ y. t2)\s" + "case s of (XCONST sinl :: 'a)\x \ t1 | XCONST sinr\y \ t2" => "CONST sscase\(\ x. t1)\(\ y. t2)\s" translations "\(XCONST sinl\x). t" == "CONST sscase\(\ x. t)\\" diff -r 3ee75fe01986 -r 00cd193a48dc src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Thu Jan 05 15:31:49 2012 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Thu Jan 05 18:18:39 2012 +0100 @@ -452,27 +452,35 @@ val cabs = app "_cabs" val capp = app @{const_syntax Rep_cfun} val capps = Library.foldl capp - fun con1 authentic n (con,args) = + fun con1 authentic n (con, args) = Library.foldl capp (c_ast authentic con, argvars n args) - fun case1 authentic (n, c) = - app "_case1" (Ast.strip_positions (con1 authentic n c), expvar n) + fun con1_constraint authentic n (con, args) = + Library.foldl capp + (Ast.Appl + [Ast.Constant @{syntax_const "_constrain"}, c_ast authentic con, + Ast.Variable ("'a" ^ string_of_int n)], + argvars n args) + fun case1 constraint authentic (n, c) = + app @{syntax_const "_case1"} + ((if constraint then con1_constraint else con1) authentic n c, expvar n) fun arg1 (n, (_, args)) = List.foldr cabs (expvar n) (argvars n args) fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom} val case_constant = Ast.Constant (syntax (case_const dummyT)) - fun case_trans authentic = - (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule) + fun case_trans constraint authentic = (app "_case_syntax" (Ast.Variable "x", - foldr1 (app "_case2") (map_index (case1 authentic) spec)), + foldr1 (app @{syntax_const "_case2"}) (map_index (case1 constraint authentic) spec)), capp (capps (case_constant, map_index arg1 spec), Ast.Variable "x")) fun one_abscon_trans authentic (n, c) = - (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule) - (cabs (con1 authentic n c, expvar n), - capps (case_constant, map_index (when1 n) spec)) + (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule) + (cabs (con1 authentic n c, expvar n), + capps (case_constant, map_index (when1 n) spec)) fun abscon_trans authentic = map_index (one_abscon_trans authentic) spec val trans_rules : Ast.ast Syntax.trrule list = - case_trans false :: case_trans true :: + Syntax.Parse_Print_Rule (case_trans false true) :: + Syntax.Parse_Rule (case_trans false false) :: + Syntax.Parse_Rule (case_trans true false) :: abscon_trans false @ abscon_trans true in val thy = Sign.add_trrules trans_rules thy diff -r 3ee75fe01986 -r 00cd193a48dc src/HOL/HOLCF/Up.thy --- a/src/HOL/HOLCF/Up.thy Thu Jan 05 15:31:49 2012 +0100 +++ b/src/HOL/HOLCF/Up.thy Thu Jan 05 18:18:39 2012 +0100 @@ -181,6 +181,7 @@ translations "case l of XCONST up\x \ t" == "CONST fup\(\ x. t)\l" + "case l of (XCONST up :: 'a)\x \ t" => "CONST fup\(\ x. t)\l" "\(XCONST up\x). t" == "CONST fup\(\ x. t)" text {* continuous versions of lemmas for @{typ "('a)u"} *} diff -r 3ee75fe01986 -r 00cd193a48dc src/HOL/List.thy --- a/src/HOL/List.thy Thu Jan 05 15:31:49 2012 +0100 +++ b/src/HOL/List.thy Thu Jan 05 18:18:39 2012 +0100 @@ -386,7 +386,7 @@ (* FIXME proper name context!? *) val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT); val e = if opti then singl e else e; - val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e; + val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e; val case2 = Syntax.const @{syntax_const "_case1"} $ Syntax.const @{const_syntax dummy_pattern} $ NilC; diff -r 3ee75fe01986 -r 00cd193a48dc src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Thu Jan 05 15:31:49 2012 +0100 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Thu Jan 05 18:18:39 2012 +0100 @@ -3,6 +3,9 @@ Author: Stefan Berghofer, TU Muenchen Datatype package: nested case expressions on datatypes. + +TODO: generic tool with separate data slot, without hard-wiring the +datatype package. *) signature DATATYPE_CASE = @@ -57,25 +60,30 @@ strip_constraints t ||> cons tT | strip_constraints t = (t, []); -fun mk_fun_constrain tT t = - Syntax.const @{syntax_const "_constrain"} $ t $ - (Syntax.const @{type_syntax fun} $ tT $ Syntax.const @{type_syntax dummy}); +fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT; (*Produce an instance of a constructor, plus fresh variables for its arguments.*) fun fresh_constr ty_match ty_inst colty used c = let - val (_, Ty) = dest_Const c; - val Ts = binder_types Ty; + val (_, T) = dest_Const c; + val Ts = binder_types T; val names = Name.variant_list used (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)); - val ty = body_type Ty; + val ty = body_type T; val ty_theta = ty_match ty colty handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1); val c' = ty_inst ty_theta c; val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts); in (c', gvars) end; +fun strip_comb_positions tm = + let + fun result t ts = (Term_Position.strip_positions t, ts); + fun strip (t as (Const (@{syntax_const "_constrain"}, _) $ _ $ _)) ts = result t ts + | strip (f $ t) ts = strip f (t :: ts) + | strip t ts = result t ts; + in strip tm [] end; (*Go through a list of rows and pick out the ones beginning with a pattern with constructor = name.*) @@ -83,7 +91,7 @@ let val k = length (binder_types T) in fold (fn (row as ((prfx, p :: ps), rhs as (_, i))) => fn ((in_group, not_in_group), (names, cnstrts)) => - (case strip_comb p of + (case strip_comb_positions p of (Const (name', _), args) => if name = name' then if length args = k then @@ -162,7 +170,8 @@ | mk path (rows as ((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 (fst o strip_comb_positions)) + (find_first (not o is_Free o fst) col0) of NONE => let val rows' = map (fn ((v, _), row) => row ||> @@ -186,7 +195,7 @@ map2 (fn {new_formals, names, constraints, ...} => fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t => Abs (if s = "" then name else s, T, abstract_over (x, t)) - |> fold mk_fun_constrain cnstrts) (new_formals ~~ names ~~ constraints)) + |> fold constrain_Abs cnstrts) (new_formals ~~ names ~~ constraints)) subproblems dtrees; val types = map type_of (case_functions @ [u]); val case_const = Const (case_name, types ---> range_ty); @@ -210,7 +219,7 @@ case_error (quote s ^ " occurs repeatedly in the pattern " ^ quote (Syntax.string_of_term ctxt pat)) else x :: xs) - | _ => I) pat []; + | _ => I) (Term_Position.strip_positions pat) []; fun gen_make_case ty_match ty_inst type_of ctxt config used x clauses = let @@ -432,7 +441,8 @@ | Const (s, _) => Syntax.const (Lexicon.mark_const s) | t => t) pat $ map_aterms - (fn x as Free (s, T) => if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x + (fn x as Free (s, T) => + if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x | t => t) rhs end; in