# HG changeset patch # User haftmann # Date 1232027555 -3600 # Node ID 49675edf127c9ef932c7d548c44fd001c68cdf8d # Parent 4f864f851f4d1ef4ab830f98ae20b5be1dcb551c# Parent d828e6ca9c11f2557c1793a2d7fe9588e4b20aac merged diff -r 4f864f851f4d -r 49675edf127c src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Thu Jan 15 12:55:38 2009 +0000 +++ b/src/FOL/ex/LocaleTest.thy Thu Jan 15 14:52:35 2009 +0100 @@ -1,7 +1,7 @@ (* Title: FOL/ex/NewLocaleTest.thy Author: Clemens Ballarin, TU Muenchen -Testing environment for locale expressions --- experimental. +Testing environment for locale expressions. *) theory LocaleTest @@ -483,4 +483,6 @@ thm local_free.lone [where ?zero = 0] qed +ML_val {* reset Toplevel.debug *} + end diff -r 4f864f851f4d -r 49675edf127c src/HOL/Library/LaTeXsugar.thy --- a/src/HOL/Library/LaTeXsugar.thy Thu Jan 15 12:55:38 2009 +0000 +++ b/src/HOL/Library/LaTeXsugar.thy Thu Jan 15 14:52:35 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Library/LaTeXsugar.thy - ID: $Id$ Author: Gerwin Klain, Tobias Nipkow, Norbert Schirmer Copyright 2005 NICTA and TUM *) diff -r 4f864f851f4d -r 49675edf127c src/HOL/Library/OptionalSugar.thy --- a/src/HOL/Library/OptionalSugar.thy Thu Jan 15 12:55:38 2009 +0000 +++ b/src/HOL/Library/OptionalSugar.thy Thu Jan 15 14:52:35 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Library/OptionalSugar.thy - ID: $Id$ Author: Gerwin Klain, Tobias Nipkow Copyright 2005 NICTA and TUM *) @@ -37,6 +36,36 @@ "_bind (p#DUMMY) e" <= "_bind p (hd e)" "_bind (DUMMY#p) e" <= "_bind p (tl e)" +(* type constraints with spacing *) +setup {* +let + val typ = SimpleSyntax.read_typ; + val typeT = Syntax.typeT; + val spropT = Syntax.spropT; +in + Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [ + ("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), + ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\_", [4, 0], 3))] + #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ + ("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), + ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \ _", [4, 0], 3))] +end +*} + +(* sorts as intersections *) +setup {* +let + val sortT = Type ("sort", []); (*FIXME*) + val classesT = Type ("classes", []); (*FIXME*) +in + Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ + ("_topsort", sortT, Mixfix ("\", [], Syntax.max_pri)), + ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)), + ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \ _", [], Syntax.max_pri)), + ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \ _", [], Syntax.max_pri)) + ] +end +*} end (*>*) diff -r 4f864f851f4d -r 49675edf127c src/HOL/Tools/function_package/size.ML --- a/src/HOL/Tools/function_package/size.ML Thu Jan 15 12:55:38 2009 +0000 +++ b/src/HOL/Tools/function_package/size.ML Thu Jan 15 14:52:35 2009 +0100 @@ -1,6 +1,5 @@ (* Title: HOL/Tools/function_package/size.ML - ID: $Id$ - Author: Stefan Berghofer, Florian Haftmann, TU Muenchen + Author: Stefan Berghofer, Florian Haftmann & Alexander Krauss, TU Muenchen Size functions for datatypes. *) @@ -81,7 +80,7 @@ val param_size = AList.lookup op = param_size_fs; val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |> - List.mapPartial (Option.map snd o lookup_size thy) |> flat; + map_filter (Option.map snd o lookup_size thy) |> flat; val extra_size = Option.map fst o lookup_size thy; val (((size_names, size_fns), def_names), def_names') = @@ -180,7 +179,7 @@ let val Ts = map (typ_of_dtyp descr sorts) cargs; val tnames = Name.variant_list f_names (DatatypeProp.make_tnames Ts); - val ts = List.mapPartial (fn (sT as (s, T), dt) => + val ts = map_filter (fn (sT as (s, T), dt) => Option.map (fn sz => sz $ Free sT) (if p dt then size_of_type size_of extra_size size_ofp T else NONE)) (tnames ~~ Ts ~~ cargs) diff -r 4f864f851f4d -r 49675edf127c src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Jan 15 12:55:38 2009 +0000 +++ b/src/Pure/Isar/expression.ML Thu Jan 15 14:52:35 2009 +0100 @@ -26,6 +26,8 @@ (* Interpretation *) val cert_goal_expression: expression_i -> Proof.context -> (term list list * (string * morphism) list * morphism) * Proof.context; + val read_goal_expression: expression -> Proof.context -> + (term list list * (string * morphism) list * morphism) * Proof.context; val sublocale: string -> expression_i -> theory -> Proof.state; val sublocale_cmd: string -> expression -> theory -> Proof.state; @@ -812,21 +814,17 @@ local -datatype goal = Reg of string * Morphism.morphism | Eqns of Attrib.binding list; - fun gen_interpretation prep_expr parse_prop prep_attr - expression equations thy = + expression equations theory = let - val ctxt = ProofContext.init thy; - - val ((propss, regs, export), expr_ctxt) = prep_expr expression ctxt; + val ((propss, regs, export), expr_ctxt) = ProofContext.init theory + |> prep_expr expression; val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt; - val eq_attns = map ((apsnd o map) (prep_attr thy) o fst) equations; + val eq_attns = map ((apsnd o map) (prep_attr theory) o fst) equations; val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; val export' = Variable.export_morphism goal_ctxt expr_ctxt; - (*** alternative code -- unclear why it does not work yet ***) fun store_reg ((name, morph), thms) thy = let val thms' = map (Element.morph_witness export') thms; @@ -841,7 +839,7 @@ thy |> fold (fn (name, morph) => Locale.activate_global_facts (name, morph $> export)) regs - | store_eqns_activate regs thms thys = + | store_eqns_activate regs thms thy = let val thms' = thms |> map (Element.conclude_witness #> Morphism.thm (export' $> export) #> @@ -866,40 +864,7 @@ in ProofContext.theory (fold_map store_reg (regs ~~ wits_reg) #-> (fn regs => store_eqns_activate regs wits_eq)) end; - (*** alternative code end ***) - fun store (Reg (name, morph), thms) (regs, thy) = - let - val thms' = map (Element.morph_witness export') thms; - val morph' = morph $> Element.satisfy_morphism thms'; - val add = Locale.add_registration (name, (morph', export)); - in ((name, morph') :: regs, add thy) end - | store (Eqns [], []) (regs, thy) = - let val add = fold_rev (fn (name, morph) => - Locale.activate_global_facts (name, morph $> export)) regs; - in (regs, add thy) end - | store (Eqns attns, thms) (regs, thy) = - let - val thms' = thms |> map (Element.conclude_witness #> - Morphism.thm (export' $> export) #> - LocalDefs.meta_rewrite_rule (ProofContext.init thy) #> - Drule.abs_def); - val eq_morph = - Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms' []) $> - Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms'); - val attns' = map ((apsnd o map) (Attrib.attribute_i thy)) attns; - val add = - fold_rev (fn (name, morph) => - Locale.amend_registration eq_morph (name, morph) #> - Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs #> - PureThy.note_thmss Thm.lemmaK (attns' ~~ map (fn th => [([th], [])]) thms') #> - snd - in (regs, add thy) end; - - fun after_qed results = - ProofContext.theory (fn thy => - fold store (map Reg regs @ [Eqns eq_attns] ~~ - prep_result (propss @ [eqns]) results) ([], thy) |> snd); in goal_ctxt |> Proof.theorem_i NONE after_qed (prep_propp (propss @ [eqns])) |> diff -r 4f864f851f4d -r 49675edf127c src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Thu Jan 15 12:55:38 2009 +0000 +++ b/src/Pure/Thy/present.ML Thu Jan 15 14:52:35 2009 +0100 @@ -467,7 +467,7 @@ val _ = add_file (Path.append html_prefix base_html, HTML.ml_file (Url.File base) (File.read path)); in (Url.File base_html, Url.File raw_path, loadit) end - | NONE => error ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path))); + | NONE => error ("Browser info: expected to find ML file " ^ quote (Path.implode raw_path))); val files_html = map prep_file files;