more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
authorwenzelm
Tue Mar 22 20:44:47 2011 +0100 (2011-03-22)
changeset 420573eba96ff3d3e
parent 42056 160a630b2c7e
child 42068 b579e787b582
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
NEWS
src/HOL/HOL.thy
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/ex/Pattern_Match.thy
src/HOL/List.thy
src/HOL/Tools/Datatype/datatype_case.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/pure_thy.ML
     1.1 --- a/NEWS	Tue Mar 22 18:03:28 2011 +0100
     1.2 +++ b/NEWS	Tue Mar 22 20:44:47 2011 +0100
     1.3 @@ -74,10 +74,12 @@
     1.4  * Inner syntax: identifiers in parse trees of generic categories
     1.5  "logic", "aprop", "idt" etc. carry position information (disguised as
     1.6  type constraints).  Occasional INCOMPATIBILITY with non-compliant
     1.7 -translations that choke on unexpected type constraints: use
     1.8 -Syntax.strip_positions or Syntax.strip_positions_ast.  As last resort,
     1.9 -reset the configuration option Syntax.positions, which is called
    1.10 -"syntax_positions" in Isar attribute source.
    1.11 +translations that choke on unexpected type constraints.  Positions can
    1.12 +be stripped in ML translations via Syntax.strip_positions /
    1.13 +Syntax.strip_positions_ast, or via the syntax constant
    1.14 +"_strip_positions" within parse trees.  As last resort, positions can
    1.15 +be disabled via the configuration option Syntax.positions, which is
    1.16 +called "syntax_positions" in Isar attribute syntax.
    1.17  
    1.18  
    1.19  
     2.1 --- a/src/HOL/HOL.thy	Tue Mar 22 18:03:28 2011 +0100
     2.2 +++ b/src/HOL/HOL.thy	Tue Mar 22 20:44:47 2011 +0100
     2.3 @@ -106,7 +106,7 @@
     2.4    iff  (infixr "\<longleftrightarrow>" 25)
     2.5  
     2.6  nonterminal letbinds and letbind
     2.7 -nonterminal case_syn and cases_syn
     2.8 +nonterminal case_pat and case_syn and cases_syn
     2.9  
    2.10  syntax
    2.11    "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)
    2.12 @@ -116,10 +116,14 @@
    2.13    "_binds"      :: "[letbind, letbinds] => letbinds"     ("_;/ _")
    2.14    "_Let"        :: "[letbinds, 'a] => 'a"                ("(let (_)/ in (_))" [0, 10] 10)
    2.15  
    2.16 -  "_case_syntax":: "['a, cases_syn] => 'b"               ("(case _ of/ _)" 10)
    2.17 -  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ =>/ _)" 10)
    2.18 -  ""            :: "case_syn => cases_syn"               ("_")
    2.19 -  "_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
    2.20 +  "_case_syntax"      :: "['a, cases_syn] => 'b"              ("(case _ of/ _)" 10)
    2.21 +  "_case1"            :: "[case_pat, 'b] => case_syn"         ("(2_ =>/ _)" 10)
    2.22 +  ""                  :: "case_syn => cases_syn"              ("_")
    2.23 +  "_case2"            :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
    2.24 +  "_strip_positions"  :: "'a => case_pat"                     ("_")
    2.25 +
    2.26 +syntax (xsymbols)
    2.27 +  "_case1" :: "[case_pat, 'b] => case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
    2.28  
    2.29  translations
    2.30    "THE x. P"              == "CONST The (%x. P)"
    2.31 @@ -130,9 +134,6 @@
    2.32        in Syntax.const @{syntax_const "_The"} $ x $ t end)]
    2.33  *}  -- {* To avoid eta-contraction of body *}
    2.34  
    2.35 -syntax (xsymbols)
    2.36 -  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
    2.37 -
    2.38  notation (xsymbols)
    2.39    All  (binder "\<forall>" 10) and
    2.40    Ex  (binder "\<exists>" 10) and
     3.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Mar 22 18:03:28 2011 +0100
     3.2 +++ b/src/HOL/HOLCF/Cfun.thy	Tue Mar 22 20:44:47 2011 +0100
     3.3 @@ -30,8 +30,6 @@
     3.4  
     3.5  subsection {* Syntax for continuous lambda abstraction *}
     3.6  
     3.7 -declare [[syntax_positions = false]]  (* FIXME pattern translations choke on position constraints *)
     3.8 -
     3.9  syntax "_cabs" :: "[logic, logic] \<Rightarrow> logic"
    3.10  
    3.11  parse_translation {*
    3.12 @@ -59,7 +57,7 @@
    3.13    let
    3.14      fun Lambda_ast_tr [pats, body] =
    3.15            Syntax.fold_ast_p @{syntax_const "_cabs"}
    3.16 -            (Syntax.unfold_ast @{syntax_const "_cargs"} pats, body)
    3.17 +            (Syntax.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
    3.18        | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
    3.19    in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
    3.20  *}
     4.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 22 18:03:28 2011 +0100
     4.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 22 20:44:47 2011 +0100
     4.3 @@ -458,7 +458,7 @@
     4.4        fun con1 authentic n (con,args) =
     4.5            Library.foldl capp (c_ast authentic con, argvars n args)
     4.6        fun case1 authentic (n, c) =
     4.7 -          app "_case1" (con1 authentic n c, expvar n)
     4.8 +          app "_case1" (Syntax.strip_positions_ast (con1 authentic n c), expvar n)
     4.9        fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
    4.10        fun when1 n (m, c) =
    4.11            if n = m then arg1 (n, c) else (Constant @{const_syntax bottom})
     5.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Mar 22 18:03:28 2011 +0100
     5.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Mar 22 20:44:47 2011 +0100
     5.3 @@ -100,16 +100,17 @@
     5.4  
     5.5  subsection {* Case syntax *}
     5.6  
     5.7 -nonterminal Case_syn and Cases_syn
     5.8 +nonterminal Case_pat and Case_syn and Cases_syn
     5.9  
    5.10  syntax
    5.11    "_Case_syntax":: "['a, Cases_syn] => 'b"               ("(Case _ of/ _)" 10)
    5.12 -  "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ =>/ _)" 10)
    5.13 +  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          ("(2_ =>/ _)" 10)
    5.14    ""            :: "Case_syn => Cases_syn"               ("_")
    5.15    "_Case2"      :: "[Case_syn, Cases_syn] => Cases_syn"  ("_/ | _")
    5.16 +  "_strip_positions" :: "'a => Case_pat"                 ("_")
    5.17  
    5.18  syntax (xsymbols)
    5.19 -  "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
    5.20 +  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          ("(2_ \<Rightarrow>/ _)" 10)
    5.21  
    5.22  translations
    5.23    "_Case_syntax x ms" == "CONST cases\<cdot>(ms\<cdot>x)"
     6.1 --- a/src/HOL/List.thy	Tue Mar 22 18:03:28 2011 +0100
     6.2 +++ b/src/HOL/List.thy	Tue Mar 22 20:44:47 2011 +0100
     6.3 @@ -384,7 +384,7 @@
     6.4      let
     6.5        val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
     6.6        val e = if opti then singl e else e;
     6.7 -      val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
     6.8 +      val case1 = Syntax.const @{syntax_const "_case1"} $ Syntax.strip_positions p $ e;
     6.9        val case2 =
    6.10          Syntax.const @{syntax_const "_case1"} $
    6.11            Syntax.const @{const_syntax dummy_pattern} $ NilC;
     7.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Tue Mar 22 18:03:28 2011 +0100
     7.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Tue Mar 22 20:44:47 2011 +0100
     7.3 @@ -339,7 +339,7 @@
     7.4            | dest_case1 t = case_error "dest_case1";
     7.5          fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
     7.6            | dest_case2 t = [t];
     7.7 -        val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 (Syntax.strip_positions u)));
     7.8 +        val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
     7.9          val (case_tm, _) = make_case_untyped (tab_of thy) ctxt
    7.10            (if err then Error else Warning) []
    7.11            (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
     8.1 --- a/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 18:03:28 2011 +0100
     8.2 +++ b/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 20:44:47 2011 +0100
     8.3 @@ -67,6 +67,12 @@
     8.4  
     8.5  (** parse (ast) translations **)
     8.6  
     8.7 +(* strip_positions *)
     8.8 +
     8.9 +fun strip_positions_ast_tr [ast] = Type_Ext.strip_positions_ast ast
    8.10 +  | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
    8.11 +
    8.12 +
    8.13  (* constify *)
    8.14  
    8.15  fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
    8.16 @@ -490,7 +496,8 @@
    8.17  (** Pure translations **)
    8.18  
    8.19  val pure_trfuns =
    8.20 -  ([("_constify", constify_ast_tr),
    8.21 +  ([("_strip_positions", strip_positions_ast_tr),
    8.22 +    ("_constify", constify_ast_tr),
    8.23      ("_appl", appl_ast_tr),
    8.24      ("_applC", applC_ast_tr),
    8.25      ("_lambda", lambda_ast_tr),
     9.1 --- a/src/Pure/pure_thy.ML	Tue Mar 22 18:03:28 2011 +0100
     9.2 +++ b/src/Pure/pure_thy.ML	Tue Mar 22 20:44:47 2011 +0100
     9.3 @@ -95,6 +95,7 @@
     9.4      ("",            typ "longid_position => logic",    Delimfix "_"),
     9.5      ("",            typ "var => logic",                Delimfix "_"),
     9.6      ("_DDDOT",      typ "logic",                       Delimfix "..."),
     9.7 +    ("_strip_positions", typ "'a", NoSyn),
     9.8      ("_constify",   typ "num => num_const",            Delimfix "_"),
     9.9      ("_constify",   typ "float_token => float_const",  Delimfix "_"),
    9.10      ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),