merged
authorwenzelm
Thu, 15 Jan 2009 15:51:50 +0100
changeset 29500 8fd3c1c7f0cb
parent 29498 49675edf127c (diff)
parent 29499 2819ba5f0c32 (current diff)
child 29503 d1df1504ff5e
child 29506 71f00a2c6dbd
child 29536 2de73447d47c
merged
--- a/src/FOL/ex/LocaleTest.thy	Thu Jan 15 15:51:19 2009 +0100
+++ b/src/FOL/ex/LocaleTest.thy	Thu Jan 15 15:51:50 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
--- a/src/HOL/Library/LaTeXsugar.thy	Thu Jan 15 15:51:19 2009 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Thu Jan 15 15:51:50 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
 *)
--- a/src/HOL/Library/OptionalSugar.thy	Thu Jan 15 15:51:19 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Thu Jan 15 15:51:50 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 ("_\<Colon>_", [4, 0], 3)),
+    ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
+  #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
+      ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
+      ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [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 ("\<top>", [], Syntax.max_pri)),
+    ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)),
+    ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri)),
+    ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri))
+  ]
+end
+*}
 
 end
 (*>*)
--- a/src/HOL/Tools/function_package/size.ML	Thu Jan 15 15:51:19 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Thu Jan 15 15:51:50 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)
--- a/src/Pure/Isar/expression.ML	Thu Jan 15 15:51:19 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Thu Jan 15 15:51:50 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])) |>
--- a/src/Pure/Thy/present.ML	Thu Jan 15 15:51:19 2009 +0100
+++ b/src/Pure/Thy/present.ML	Thu Jan 15 15:51:50 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;
 
--- a/src/Pure/Thy/thy_output.ML	Thu Jan 15 15:51:19 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Jan 15 15:51:50 2009 +0100
@@ -11,6 +11,7 @@
   val quotes: bool ref
   val indent: int ref
   val source: bool ref
+  val break: bool ref
   val add_commands: (string * (Args.src -> Toplevel.node option -> string)) list -> unit
   val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
   val defined_command: string -> bool