# HG changeset patch # User wenzelm # Date 1300823087 -3600 # Node ID 3eba96ff3d3e7cb823715868eb23a212f40637bd # Parent 160a630b2c7ece0603dca3c15ae98d6cd812ff12 more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF; diff -r 160a630b2c7e -r 3eba96ff3d3e NEWS --- 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. diff -r 160a630b2c7e -r 3eba96ff3d3e src/HOL/HOL.thy --- 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 "\" 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_ \/ _)" 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_ \/ _)" 10) - notation (xsymbols) All (binder "\" 10) and Ex (binder "\" 10) and diff -r 160a630b2c7e -r 3eba96ff3d3e src/HOL/HOLCF/Cfun.thy --- 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] \ 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; *} diff -r 160a630b2c7e -r 3eba96ff3d3e src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- 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}) diff -r 160a630b2c7e -r 3eba96ff3d3e src/HOL/HOLCF/ex/Pattern_Match.thy --- 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_ \/ _)" 10) + "_Case1" :: "[Case_pat, 'b] => Case_syn" ("(2_ \/ _)" 10) translations "_Case_syntax x ms" == "CONST cases\(ms\x)" diff -r 160a630b2c7e -r 3eba96ff3d3e src/HOL/List.thy --- 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; diff -r 160a630b2c7e -r 3eba96ff3d3e src/HOL/Tools/Datatype/datatype_case.ML --- 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) diff -r 160a630b2c7e -r 3eba96ff3d3e src/Pure/Syntax/syn_trans.ML --- 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), diff -r 160a630b2c7e -r 3eba96ff3d3e src/Pure/pure_thy.ML --- 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>_"),