improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
authorwenzelm
Thu Jan 05 18:18:39 2012 +0100 (2012-01-05)
changeset 4612500cd193a48dc
parent 46124 3ee75fe01986
child 46126 bab00660539d
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
tuned;
NEWS
src/HOL/HOL.thy
src/HOL/HOLCF/One.thy
src/HOL/HOLCF/Ssum.thy
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Up.thy
src/HOL/List.thy
src/HOL/Tools/Datatype/datatype_case.ML
     1.1 --- a/NEWS	Thu Jan 05 15:31:49 2012 +0100
     1.2 +++ b/NEWS	Thu Jan 05 18:18:39 2012 +0100
     1.3 @@ -60,6 +60,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Concrete syntax for case expressions includes constraints for source
     1.8 +positions, and thus produces Prover IDE markup for its bindings.
     1.9 +INCOMPATIBILITY for old-style syntax translations that augment the
    1.10 +pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
    1.11 +one_case.
    1.12 +
    1.13  * Finite_Set.fold now qualified.  INCOMPATIBILITY.
    1.14  
    1.15  * Renamed some facts on canonical fold on lists, in order to avoid problems
     2.1 --- a/src/HOL/HOL.thy	Thu Jan 05 15:31:49 2012 +0100
     2.2 +++ b/src/HOL/HOL.thy	Thu Jan 05 18:18:39 2012 +0100
     2.3 @@ -104,34 +104,31 @@
     2.4  notation (xsymbols)
     2.5    iff  (infixr "\<longleftrightarrow>" 25)
     2.6  
     2.7 -nonterminal letbinds and letbind
     2.8 -nonterminal case_pat and case_syn and cases_syn
     2.9 +syntax
    2.10 +  "_The" :: "[pttrn, bool] => 'a"  ("(3THE _./ _)" [0, 10] 10)
    2.11 +translations
    2.12 +  "THE x. P" == "CONST The (%x. P)"
    2.13 +print_translation {*
    2.14 +  [(@{const_syntax The}, fn [Abs abs] =>
    2.15 +      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
    2.16 +      in Syntax.const @{syntax_const "_The"} $ x $ t end)]
    2.17 +*}  -- {* To avoid eta-contraction of body *}
    2.18  
    2.19 +nonterminal letbinds and letbind
    2.20  syntax
    2.21 -  "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)
    2.22 -
    2.23    "_bind"       :: "[pttrn, 'a] => letbind"              ("(2_ =/ _)" 10)
    2.24    ""            :: "letbind => letbinds"                 ("_")
    2.25    "_binds"      :: "[letbind, letbinds] => letbinds"     ("_;/ _")
    2.26    "_Let"        :: "[letbinds, 'a] => 'a"                ("(let (_)/ in (_))" [0, 10] 10)
    2.27  
    2.28 -  "_case_syntax"      :: "['a, cases_syn] => 'b"              ("(case _ of/ _)" 10)
    2.29 -  "_case1"            :: "[case_pat, 'b] => case_syn"         ("(2_ =>/ _)" 10)
    2.30 -  ""                  :: "case_syn => cases_syn"              ("_")
    2.31 -  "_case2"            :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
    2.32 -  "_strip_positions"  :: "'a => case_pat"                     ("_")
    2.33 -
    2.34 +nonterminal case_syn and cases_syn
    2.35 +syntax
    2.36 +  "_case_syntax" :: "['a, cases_syn] => 'b"  ("(case _ of/ _)" 10)
    2.37 +  "_case1" :: "['a, 'b] => case_syn"  ("(2_ =>/ _)" 10)
    2.38 +  "" :: "case_syn => cases_syn"  ("_")
    2.39 +  "_case2" :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
    2.40  syntax (xsymbols)
    2.41 -  "_case1" :: "[case_pat, 'b] => case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
    2.42 -
    2.43 -translations
    2.44 -  "THE x. P"              == "CONST The (%x. P)"
    2.45 -
    2.46 -print_translation {*
    2.47 -  [(@{const_syntax The}, fn [Abs abs] =>
    2.48 -      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
    2.49 -      in Syntax.const @{syntax_const "_The"} $ x $ t end)]
    2.50 -*}  -- {* To avoid eta-contraction of body *}
    2.51 +  "_case1" :: "['a, 'b] => case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
    2.52  
    2.53  notation (xsymbols)
    2.54    All  (binder "\<forall>" 10) and
     3.1 --- a/src/HOL/HOLCF/One.thy	Thu Jan 05 15:31:49 2012 +0100
     3.2 +++ b/src/HOL/HOLCF/One.thy	Thu Jan 05 18:18:39 2012 +0100
     3.3 @@ -58,6 +58,7 @@
     3.4  
     3.5  translations
     3.6    "case x of XCONST ONE \<Rightarrow> t" == "CONST one_case\<cdot>t\<cdot>x"
     3.7 +  "case x of XCONST ONE :: 'a \<Rightarrow> t" => "CONST one_case\<cdot>t\<cdot>x"
     3.8    "\<Lambda> (XCONST ONE). t" == "CONST one_case\<cdot>t"
     3.9  
    3.10  lemma one_case1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
     4.1 --- a/src/HOL/HOLCF/Ssum.thy	Thu Jan 05 15:31:49 2012 +0100
     4.2 +++ b/src/HOL/HOLCF/Ssum.thy	Thu Jan 05 18:18:39 2012 +0100
     4.3 @@ -168,6 +168,7 @@
     4.4  
     4.5  translations
     4.6    "case s of XCONST sinl\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
     4.7 +  "case s of (XCONST sinl :: 'a)\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" => "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
     4.8  
     4.9  translations
    4.10    "\<Lambda>(XCONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
     5.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jan 05 15:31:49 2012 +0100
     5.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jan 05 18:18:39 2012 +0100
     5.3 @@ -452,27 +452,35 @@
     5.4        val cabs = app "_cabs"
     5.5        val capp = app @{const_syntax Rep_cfun}
     5.6        val capps = Library.foldl capp
     5.7 -      fun con1 authentic n (con,args) =
     5.8 +      fun con1 authentic n (con, args) =
     5.9            Library.foldl capp (c_ast authentic con, argvars n args)
    5.10 -      fun case1 authentic (n, c) =
    5.11 -          app "_case1" (Ast.strip_positions (con1 authentic n c), expvar n)
    5.12 +      fun con1_constraint authentic n (con, args) =
    5.13 +          Library.foldl capp
    5.14 +            (Ast.Appl
    5.15 +              [Ast.Constant @{syntax_const "_constrain"}, c_ast authentic con,
    5.16 +                Ast.Variable ("'a" ^ string_of_int n)],
    5.17 +             argvars n args)
    5.18 +      fun case1 constraint authentic (n, c) =
    5.19 +        app @{syntax_const "_case1"}
    5.20 +          ((if constraint then con1_constraint else con1) authentic n c, expvar n)
    5.21        fun arg1 (n, (_, args)) = List.foldr cabs (expvar n) (argvars n args)
    5.22        fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom}
    5.23        val case_constant = Ast.Constant (syntax (case_const dummyT))
    5.24 -      fun case_trans authentic =
    5.25 -        (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
    5.26 +      fun case_trans constraint authentic =
    5.27            (app "_case_syntax"
    5.28              (Ast.Variable "x",
    5.29 -             foldr1 (app "_case2") (map_index (case1 authentic) spec)),
    5.30 +             foldr1 (app @{syntax_const "_case2"}) (map_index (case1 constraint authentic) spec)),
    5.31             capp (capps (case_constant, map_index arg1 spec), Ast.Variable "x"))
    5.32        fun one_abscon_trans authentic (n, c) =
    5.33 -        (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
    5.34 -          (cabs (con1 authentic n c, expvar n),
    5.35 -           capps (case_constant, map_index (when1 n) spec))
    5.36 +          (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
    5.37 +            (cabs (con1 authentic n c, expvar n),
    5.38 +             capps (case_constant, map_index (when1 n) spec))
    5.39        fun abscon_trans authentic =
    5.40            map_index (one_abscon_trans authentic) spec
    5.41        val trans_rules : Ast.ast Syntax.trrule list =
    5.42 -          case_trans false :: case_trans true ::
    5.43 +          Syntax.Parse_Print_Rule (case_trans false true) ::
    5.44 +          Syntax.Parse_Rule (case_trans false false) ::
    5.45 +          Syntax.Parse_Rule (case_trans true false) ::
    5.46            abscon_trans false @ abscon_trans true
    5.47      in
    5.48        val thy = Sign.add_trrules trans_rules thy
     6.1 --- a/src/HOL/HOLCF/Up.thy	Thu Jan 05 15:31:49 2012 +0100
     6.2 +++ b/src/HOL/HOLCF/Up.thy	Thu Jan 05 18:18:39 2012 +0100
     6.3 @@ -181,6 +181,7 @@
     6.4  
     6.5  translations
     6.6    "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
     6.7 +  "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
     6.8    "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
     6.9  
    6.10  text {* continuous versions of lemmas for @{typ "('a)u"} *}
     7.1 --- a/src/HOL/List.thy	Thu Jan 05 15:31:49 2012 +0100
     7.2 +++ b/src/HOL/List.thy	Thu Jan 05 18:18:39 2012 +0100
     7.3 @@ -386,7 +386,7 @@
     7.4        (* FIXME proper name context!? *)
     7.5        val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
     7.6        val e = if opti then singl e else e;
     7.7 -      val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e;
     7.8 +      val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
     7.9        val case2 =
    7.10          Syntax.const @{syntax_const "_case1"} $
    7.11            Syntax.const @{const_syntax dummy_pattern} $ NilC;
     8.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Thu Jan 05 15:31:49 2012 +0100
     8.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Thu Jan 05 18:18:39 2012 +0100
     8.3 @@ -3,6 +3,9 @@
     8.4      Author:     Stefan Berghofer, TU Muenchen
     8.5  
     8.6  Datatype package: nested case expressions on datatypes.
     8.7 +
     8.8 +TODO: generic tool with separate data slot, without hard-wiring the
     8.9 +datatype package.
    8.10  *)
    8.11  
    8.12  signature DATATYPE_CASE =
    8.13 @@ -57,25 +60,30 @@
    8.14        strip_constraints t ||> cons tT
    8.15    | strip_constraints t = (t, []);
    8.16  
    8.17 -fun mk_fun_constrain tT t =
    8.18 -  Syntax.const @{syntax_const "_constrain"} $ t $
    8.19 -    (Syntax.const @{type_syntax fun} $ tT $ Syntax.const @{type_syntax dummy});
    8.20 +fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
    8.21  
    8.22  
    8.23  (*Produce an instance of a constructor, plus fresh variables for its arguments.*)
    8.24  fun fresh_constr ty_match ty_inst colty used c =
    8.25    let
    8.26 -    val (_, Ty) = dest_Const c;
    8.27 -    val Ts = binder_types Ty;
    8.28 +    val (_, T) = dest_Const c;
    8.29 +    val Ts = binder_types T;
    8.30      val names =
    8.31        Name.variant_list used (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts));
    8.32 -    val ty = body_type Ty;
    8.33 +    val ty = body_type T;
    8.34      val ty_theta = ty_match ty colty
    8.35        handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);
    8.36      val c' = ty_inst ty_theta c;
    8.37      val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts);
    8.38    in (c', gvars) end;
    8.39  
    8.40 +fun strip_comb_positions tm =
    8.41 +  let
    8.42 +    fun result t ts = (Term_Position.strip_positions t, ts);
    8.43 +    fun strip (t as (Const (@{syntax_const "_constrain"}, _) $ _ $ _)) ts = result t ts
    8.44 +      | strip (f $ t) ts = strip f (t :: ts)
    8.45 +      | strip t ts = result t ts;
    8.46 +  in strip tm [] end;
    8.47  
    8.48  (*Go through a list of rows and pick out the ones beginning with a
    8.49    pattern with constructor = name.*)
    8.50 @@ -83,7 +91,7 @@
    8.51    let val k = length (binder_types T) in
    8.52      fold (fn (row as ((prfx, p :: ps), rhs as (_, i))) =>
    8.53        fn ((in_group, not_in_group), (names, cnstrts)) =>
    8.54 -        (case strip_comb p of
    8.55 +        (case strip_comb_positions p of
    8.56            (Const (name', _), args) =>
    8.57              if name = name' then
    8.58                if length args = k then
    8.59 @@ -162,7 +170,8 @@
    8.60        | mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) = mk path [row]
    8.61        | mk (u :: us) (rows as ((_, _ :: _), _) :: _) =
    8.62            let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in
    8.63 -            (case Option.map (apfst head_of) (find_first (not o is_Free o fst) col0) of
    8.64 +            (case Option.map (apfst (fst o strip_comb_positions))
    8.65 +                (find_first (not o is_Free o fst) col0) of
    8.66                NONE =>
    8.67                  let
    8.68                    val rows' = map (fn ((v, _), row) => row ||>
    8.69 @@ -186,7 +195,7 @@
    8.70                          map2 (fn {new_formals, names, constraints, ...} =>
    8.71                            fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
    8.72                              Abs (if s = "" then name else s, T, abstract_over (x, t))
    8.73 -                            |> fold mk_fun_constrain cnstrts) (new_formals ~~ names ~~ constraints))
    8.74 +                            |> fold constrain_Abs cnstrts) (new_formals ~~ names ~~ constraints))
    8.75                          subproblems dtrees;
    8.76                        val types = map type_of (case_functions @ [u]);
    8.77                        val case_const = Const (case_name, types ---> range_ty);
    8.78 @@ -210,7 +219,7 @@
    8.79            case_error (quote s ^ " occurs repeatedly in the pattern " ^
    8.80              quote (Syntax.string_of_term ctxt pat))
    8.81          else x :: xs)
    8.82 -    | _ => I) pat [];
    8.83 +    | _ => I) (Term_Position.strip_positions pat) [];
    8.84  
    8.85  fun gen_make_case ty_match ty_inst type_of ctxt config used x clauses =
    8.86    let
    8.87 @@ -432,7 +441,8 @@
    8.88                  | Const (s, _) => Syntax.const (Lexicon.mark_const s)
    8.89                  | t => t) pat $
    8.90              map_aterms
    8.91 -              (fn x as Free (s, T) => if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
    8.92 +              (fn x as Free (s, T) =>
    8.93 +                  if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
    8.94                  | t => t) rhs
    8.95          end;
    8.96      in