more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;

--- a/NEWS	Tue Mar 22 18:03:28 2011 +0100
+++ b/NEWS	Tue Mar 22 20:44:47 2011 +0100
@@ -74,10 +74,12 @@
 * Inner syntax: identifiers in parse trees of generic categories
 "logic", "aprop", "idt" etc. carry position information (disguised as
 type constraints).  Occasional INCOMPATIBILITY with non-compliant
-translations that choke on unexpected type constraints: use
-Syntax.strip_positions or Syntax.strip_positions_ast.  As last resort,
-reset the configuration option Syntax.positions, which is called
-"syntax_positions" in Isar attribute source.
+translations that choke on unexpected type constraints.  Positions can
+be stripped in ML translations via Syntax.strip_positions /
+Syntax.strip_positions_ast, or via the syntax constant
+"_strip_positions" within parse trees.  As last resort, positions can
+be disabled via the configuration option Syntax.positions, which is
+called "syntax_positions" in Isar attribute syntax.
 
 
 

--- a/src/HOL/HOL.thy	Tue Mar 22 18:03:28 2011 +0100
+++ b/src/HOL/HOL.thy	Tue Mar 22 20:44:47 2011 +0100
@@ -106,7 +106,7 @@
   iff  (infixr "\<longleftrightarrow>" 25)
 
 nonterminal letbinds and letbind
-nonterminal case_syn and cases_syn
+nonterminal case_pat and case_syn and cases_syn
 
 syntax
   "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)
@@ -116,10 +116,14 @@
   "_binds"      :: "[letbind, letbinds] => letbinds"     ("_;/ _")
   "_Let"        :: "[letbinds, 'a] => 'a"                ("(let (_)/ in (_))" [0, 10] 10)
 
-  "_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"  ("_/ | _")
+  "_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"                     ("_")
+
+syntax (xsymbols)
+  "_case1" :: "[case_pat, 'b] => case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
 
 translations
   "THE x. P"              == "CONST The (%x. P)"
@@ -130,9 +134,6 @@
       in Syntax.const @{syntax_const "_The"} $ x $ t end)]
 *}  -- {* To avoid eta-contraction of body *}
 
-syntax (xsymbols)
-  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
-
 notation (xsymbols)
   All  (binder "\<forall>" 10) and
   Ex  (binder "\<exists>" 10) and

--- a/src/HOL/HOLCF/Cfun.thy	Tue Mar 22 18:03:28 2011 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Tue Mar 22 20:44:47 2011 +0100
@@ -30,8 +30,6 @@
 
 subsection {* Syntax for continuous lambda abstraction *}
 
-declare [[syntax_positions = false]]  (* FIXME pattern translations choke on position constraints *)
-
 syntax "_cabs" :: "[logic, logic] \<Rightarrow> logic"
 
 parse_translation {*
@@ -59,7 +57,7 @@
   let
     fun Lambda_ast_tr [pats, body] =
           Syntax.fold_ast_p @{syntax_const "_cabs"}
-            (Syntax.unfold_ast @{syntax_const "_cargs"} pats, body)
+            (Syntax.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
       | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
   in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
 *}

--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 22 18:03:28 2011 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 22 20:44:47 2011 +0100
@@ -458,7 +458,7 @@
       fun con1 authentic n (con,args) =
           Library.foldl capp (c_ast authentic con, argvars n args)
       fun case1 authentic (n, c) =
-          app "_case1" (con1 authentic n c, expvar n)
+          app "_case1" (Syntax.strip_positions_ast (con1 authentic n c), expvar n)
       fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
       fun when1 n (m, c) =
           if n = m then arg1 (n, c) else (Constant @{const_syntax bottom})

--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Mar 22 18:03:28 2011 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Mar 22 20:44:47 2011 +0100
@@ -100,16 +100,17 @@
 
 subsection {* Case syntax *}
 
-nonterminal Case_syn and Cases_syn
+nonterminal Case_pat and Case_syn and Cases_syn
 
 syntax
   "_Case_syntax":: "['a, Cases_syn] => 'b"               ("(Case _ of/ _)" 10)
-  "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ =>/ _)" 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"                 ("_")
 
 syntax (xsymbols)
-  "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
+  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          ("(2_ \<Rightarrow>/ _)" 10)
 
 translations
   "_Case_syntax x ms" == "CONST cases\<cdot>(ms\<cdot>x)"

--- a/src/HOL/List.thy	Tue Mar 22 18:03:28 2011 +0100
+++ b/src/HOL/List.thy	Tue Mar 22 20:44:47 2011 +0100
@@ -384,7 +384,7 @@
     let
       val x = Free (Name.variant (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"} $ p $ e;
+      val case1 = Syntax.const @{syntax_const "_case1"} $ Syntax.strip_positions p $ e;
       val case2 =
         Syntax.const @{syntax_const "_case1"} $
           Syntax.const @{const_syntax dummy_pattern} $ NilC;

--- a/src/HOL/Tools/Datatype/datatype_case.ML	Tue Mar 22 18:03:28 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Tue Mar 22 20:44:47 2011 +0100
@@ -339,7 +339,7 @@
           | dest_case1 t = case_error "dest_case1";
         fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
           | dest_case2 t = [t];
-        val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 (Syntax.strip_positions u)));
+        val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
         val (case_tm, _) = make_case_untyped (tab_of thy) ctxt
           (if err then Error else Warning) []
           (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)

--- a/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 18:03:28 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 20:44:47 2011 +0100
@@ -67,6 +67,12 @@
 
 (** parse (ast) translations **)
 
+(* strip_positions *)
+
+fun strip_positions_ast_tr [ast] = Type_Ext.strip_positions_ast ast
+  | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
+
+
 (* constify *)
 
 fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
@@ -490,7 +496,8 @@
 (** Pure translations **)
 
 val pure_trfuns =
-  ([("_constify", constify_ast_tr),
+  ([("_strip_positions", strip_positions_ast_tr),
+    ("_constify", constify_ast_tr),
     ("_appl", appl_ast_tr),
     ("_applC", applC_ast_tr),
     ("_lambda", lambda_ast_tr),

--- a/src/Pure/pure_thy.ML	Tue Mar 22 18:03:28 2011 +0100
+++ b/src/Pure/pure_thy.ML	Tue Mar 22 20:44:47 2011 +0100
@@ -95,6 +95,7 @@
     ("",            typ "longid_position => logic",    Delimfix "_"),
     ("",            typ "var => logic",                Delimfix "_"),
     ("_DDDOT",      typ "logic",                       Delimfix "..."),
+    ("_strip_positions", typ "'a", NoSyn),
     ("_constify",   typ "num => num_const",            Delimfix "_"),
     ("_constify",   typ "float_token => float_const",  Delimfix "_"),
     ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),