# HG changeset patch # User wenzelm # Date 1266783001 -3600 # Node ID b73ae1a8fe7eeefdb53740793fb069840c0f323d # Parent 2cb27605301f122526f2043163ab59aa098fb382 adapted to authentic syntax; diff -r 2cb27605301f -r b73ae1a8fe7e src/Cube/Cube.thy --- a/src/Cube/Cube.thy Sun Feb 21 21:08:25 2010 +0100 +++ b/src/Cube/Cube.thy Sun Feb 21 21:10:01 2010 +0100 @@ -18,43 +18,43 @@ context' typing' consts - Abs :: "[term, term => term] => term" - Prod :: "[term, term => term] => term" - Trueprop :: "[context, typing] => prop" - MT_context :: "context" - Context :: "[typing, context] => context" - star :: "term" ("*") - box :: "term" ("[]") - app :: "[term, term] => term" (infixl "^" 20) - Has_type :: "[term, term] => typing" + Abs :: "[term, term => term] => term" + Prod :: "[term, term => term] => term" + Trueprop :: "[context, typing] => prop" + MT_context :: "context" + Context :: "[typing, context] => context" + star :: "term" ("*") + box :: "term" ("[]") + app :: "[term, term] => term" (infixl "^" 20) + Has_type :: "[term, term] => typing" syntax - Trueprop :: "[context', typing'] => prop" ("(_/ |- _)") - Trueprop1 :: "typing' => prop" ("(_)") - "" :: "id => context'" ("_") - "" :: "var => context'" ("_") - MT_context :: "context'" ("") - Context :: "[typing', context'] => context'" ("_ _") - Has_type :: "[term, term] => typing'" ("(_:/ _)" [0, 0] 5) - Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10) - Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10) - arrow :: "[term, term] => term" (infixr "->" 10) + "\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/ |- _)") + "_Trueprop1" :: "typing' => prop" ("(_)") + "" :: "id => context'" ("_") + "" :: "var => context'" ("_") + "\<^const>Cube.MT_context" :: "context'" ("") + "\<^const>Cube.Context" :: "[typing', context'] => context'" ("_ _") + "\<^const>Cube.Has_type" :: "[term, term] => typing'" ("(_:/ _)" [0, 0] 5) + "_Lam" :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10) + "_Pi" :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10) + "_arrow" :: "[term, term] => term" (infixr "->" 10) translations ("prop") "x:X" == ("prop") "|- x:X" - "Lam x:A. B" == "CONST Abs(A, %x. B)" - "Pi x:A. B" => "CONST Prod(A, %x. B)" - "A -> B" => "CONST Prod(A, %_. B)" + "Lam x:A. B" == "CONST Abs(A, %x. B)" + "Pi x:A. B" => "CONST Prod(A, %x. B)" + "A -> B" => "CONST Prod(A, %_. B)" syntax (xsymbols) - Trueprop :: "[context', typing'] => prop" ("(_/ \ _)") - box :: "term" ("\") - Lam :: "[idt, term, term] => term" ("(3\ _:_./ _)" [0, 0, 0] 10) - Pi :: "[idt, term, term] => term" ("(3\ _:_./ _)" [0, 0] 10) - arrow :: "[term, term] => term" (infixr "\" 10) + "\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/ \ _)") + "\<^const>Cube.box" :: "term" ("\") + "_Lam" :: "[idt, term, term] => term" ("(3\ _:_./ _)" [0, 0, 0] 10) + "_Pi" :: "[idt, term, term] => term" ("(3\ _:_./ _)" [0, 0] 10) + "_arrow" :: "[term, term] => term" (infixr "\" 10) print_translation {* - [(@{const_syntax Prod}, dependent_tr' (@{syntax_const Pi}, @{syntax_const arrow}))] + [(@{const_syntax Prod}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] *} axioms diff -r 2cb27605301f -r b73ae1a8fe7e src/HOL/List.thy --- a/src/HOL/List.thy Sun Feb 21 21:08:25 2010 +0100 +++ b/src/HOL/List.thy Sun Feb 21 21:10:01 2010 +0100 @@ -358,11 +358,11 @@ parse_translation (advanced) {* let - val NilC = Syntax.const @{const_name Nil}; - val ConsC = Syntax.const @{const_name Cons}; - val mapC = Syntax.const @{const_name map}; - val concatC = Syntax.const @{const_name concat}; - val IfC = Syntax.const @{const_name If}; + val NilC = Syntax.const @{const_syntax Nil}; + val ConsC = Syntax.const @{const_syntax Cons}; + val mapC = Syntax.const @{const_syntax map}; + val concatC = Syntax.const @{const_syntax concat}; + val IfC = Syntax.const @{const_syntax If}; fun singl x = ConsC $ x $ NilC; @@ -371,12 +371,14 @@ 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 case2 = Syntax.const @{syntax_const "_case1"} $ Syntax.const Term.dummy_patternN $ NilC; + val case2 = + Syntax.const @{syntax_const "_case1"} $ + Syntax.const @{const_syntax dummy_pattern} $ NilC; val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2; val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs]; in lambda x ft end; - fun abs_tr ctxt (p as Free(s,T)) e opti = + fun abs_tr ctxt (p as Free (s, T)) e opti = let val thy = ProofContext.theory_of ctxt; val s' = Sign.intern_const thy s; diff -r 2cb27605301f -r b73ae1a8fe7e src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Sun Feb 21 21:08:25 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Sun Feb 21 21:10:01 2010 +0100 @@ -310,6 +310,8 @@ fun case_tr err tab_of ctxt [t, u] = let val thy = ProofContext.theory_of ctxt; + val intern_const_syntax = Consts.intern_syntax (Sign.consts_of thy); + (* replace occurrences of dummy_pattern by distinct variables *) (* internalize constant names *) fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used = @@ -319,9 +321,7 @@ let val x = Name.variant used "x" in (Free (x, T), x :: used) end | prep_pat (Const (s, T)) used = - (case try (unprefix Syntax.constN) s of - SOME c => (Const (c, T), used) - | NONE => (Const (Sign.intern_const thy s, T), used)) + (Const (intern_const_syntax s, T), used) | prep_pat (v as Free (s, T)) used = let val s' = Sign.intern_const thy s in @@ -455,14 +455,13 @@ fun case_tr' tab_of cname ctxt ts = let val thy = ProofContext.theory_of ctxt; - val consts = ProofContext.consts_of ctxt; fun mk_clause (pat, rhs) = let val xs = Term.add_frees pat [] in Syntax.const @{syntax_const "_case1"} $ map_aterms (fn Free p => Syntax.mark_boundT p - | Const (s, _) => Const (Consts.extern_early consts s, dummyT) + | Const (s, _) => Syntax.const (Syntax.constN ^ s) | t => t) pat $ map_aterms (fn x as Free (s, T) => diff -r 2cb27605301f -r b73ae1a8fe7e src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Sun Feb 21 21:08:25 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Sun Feb 21 21:10:01 2010 +0100 @@ -223,7 +223,7 @@ fun add_case_tr' case_names thy = Sign.add_advanced_trfuns ([], [], map (fn case_name => - let val case_name' = Sign.const_syntax_name thy case_name + let val case_name' = Syntax.constN ^ case_name in (case_name', Datatype_Case.case_tr' info_of_case case_name') end) case_names, []) thy; diff -r 2cb27605301f -r b73ae1a8fe7e src/HOL/Tools/string_syntax.ML --- a/src/HOL/Tools/string_syntax.ML Sun Feb 21 21:08:25 2010 +0100 +++ b/src/HOL/Tools/string_syntax.ML Sun Feb 21 21:10:01 2010 +0100 @@ -15,15 +15,14 @@ (* nibble *) -val nib_prefix = "String.nibble."; - val mk_nib = - Syntax.Constant o unprefix nib_prefix o + Syntax.Constant o prefix Syntax.constN o fst o Term.dest_Const o HOLogic.mk_nibble; -fun dest_nib (Syntax.Constant c) = - HOLogic.dest_nibble (Const (nib_prefix ^ c, dummyT)) - handle TERM _ => raise Match; +fun dest_nib (Syntax.Constant s) = + (case try (unprefix Syntax.constN) s of + NONE => raise Match + | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match)); (* char *)