# HG changeset patch # User paulson # Date 1457544163 0 # Node ID b351da9b4c7d35dde9a8e0eb180097ad4d1641ee # Parent f2fc5485e3b08e176d5471d3b6d085c5902fb879# Parent 00f8bca4aba0d9ca0c1565e08e31ae42ea0586c3 Merge diff -r f2fc5485e3b0 -r b351da9b4c7d NEWS --- a/NEWS Wed Mar 09 17:16:08 2016 +0000 +++ b/NEWS Wed Mar 09 17:22:43 2016 +0000 @@ -54,7 +54,6 @@ resemble the f.split naming convention, INCOMPATIBILITY. * Multiset membership is now expressed using set_mset rather than count. -ASCII infix syntax ":#" has been discontinued. - Expressions "count M a > 0" and similar simplify to membership by default. diff -r f2fc5485e3b0 -r b351da9b4c7d src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Wed Mar 09 17:16:08 2016 +0000 +++ b/src/HOL/Library/Multiset.thy Wed Mar 09 17:22:43 2016 +0000 @@ -113,11 +113,27 @@ definition set_mset :: "'a multiset \ 'a set" where "set_mset M = {x. count M x > 0}" -abbreviation Melem :: "'a \ 'a multiset \ bool" (infix "\#" 50) - where "a \# M \ a \ set_mset M" - -abbreviation not_Melem :: "'a \ 'a multiset \ bool" (infix "\#" 50) - where "a \# M \ a \ set_mset M" +abbreviation Melem :: "'a \ 'a multiset \ bool" + where "Melem a M \ a \ set_mset M" + +notation + Melem ("op \#") and + Melem ("(_/ \# _)" [51, 51] 50) + +notation (ASCII) + Melem ("op :#") and + Melem ("(_/ :# _)" [51, 51] 50) + +abbreviation not_Melem :: "'a \ 'a multiset \ bool" + where "not_Melem a M \ a \ set_mset M" + +notation + not_Melem ("op \#") and + not_Melem ("(_/ \# _)" [51, 51] 50) + +notation (ASCII) + not_Melem ("op ~:#") and + not_Melem ("(_/ ~:# _)" [51, 51] 50) context begin @@ -134,6 +150,10 @@ "_MBall" :: "pttrn \ 'a set \ bool \ bool" ("(3\_\#_./ _)" [0, 0, 10] 10) "_MBex" :: "pttrn \ 'a set \ bool \ bool" ("(3\_\#_./ _)" [0, 0, 10] 10) +syntax (ASCII) + "_MBall" :: "pttrn \ 'a set \ bool \ bool" ("(3\_:#_./ _)" [0, 0, 10] 10) + "_MBex" :: "pttrn \ 'a set \ bool \ bool" ("(3\_:#_./ _)" [0, 0, 10] 10) + translations "\x\#A. P" \ "CONST Multiset.Ball A (\x. P)" "\x\#A. P" \ "CONST Multiset.Bex A (\x. P)" diff -r f2fc5485e3b0 -r b351da9b4c7d src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Wed Mar 09 17:16:08 2016 +0000 +++ b/src/Pure/proofterm.ML Wed Mar 09 17:22:43 2016 +0000 @@ -1057,7 +1057,7 @@ fun of_sort_proof thy hyps = Sorts.of_sort_derivation (Sign.classes_of thy) - {class_relation = fn typ => fn (prf, c1) => fn c2 => + {class_relation = fn typ => fn _ => fn (prf, c1) => fn c2 => if c1 = c2 then prf else canonical_instance [typ] (classrel_proof thy (c1, c2)) %% prf, type_constructor = fn (a, typs) => fn dom => fn c => diff -r f2fc5485e3b0 -r b351da9b4c7d src/Pure/sorts.ML --- a/src/Pure/sorts.ML Wed Mar 09 17:16:08 2016 +0000 +++ b/src/Pure/sorts.ML Wed Mar 09 17:22:43 2016 +0000 @@ -55,7 +55,7 @@ val meet_sort_typ: algebra -> typ * sort -> typ -> typ (*exception CLASS_ERROR*) val of_sort: algebra -> typ * sort -> bool val of_sort_derivation: algebra -> - {class_relation: typ -> 'a * class -> class -> 'a, + {class_relation: typ -> bool -> 'a * class -> class -> 'a, type_constructor: string * typ list -> ('a * class) list list -> class -> 'a, type_variable: typ -> ('a * class) list} -> typ * sort -> 'a list (*exception CLASS_ERROR*) @@ -403,9 +403,10 @@ if S1 = S2 then map fst D1 else S2 |> map (fn c2 => - (case D1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of - SOME d1 => class_relation T d1 c2 - | NONE => raise CLASS_ERROR (No_Subsort (S1, S2)))) + (case D1 |> filter (fn (_, c1) => class_le algebra (c1, c2)) of + [d1] => class_relation T true d1 c2 + | (d1 :: _ :: _) => class_relation T false d1 c2 + | [] => raise CLASS_ERROR (No_Subsort (S1, S2)))) end; fun derive (_, []) = [] diff -r f2fc5485e3b0 -r b351da9b4c7d src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Wed Mar 09 17:16:08 2016 +0000 +++ b/src/Tools/Code/code_ml.ML Wed Mar 09 17:22:43 2016 +0000 @@ -87,12 +87,13 @@ ((str o deresolve_inst) inst :: (if is_pseudo_fun (Class_Instance inst) then [str "()"] else map_filter (print_dicts is_pseudo_fun BR) dss)) - | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) = - [str (if k = 1 then Name.enforce_case true v ^ "_" - else Name.enforce_case true v ^ string_of_int (i+1) ^ "_")] + | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length }) = + [str (if length = 1 then Name.enforce_case true var ^ "_" + else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")] and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR - (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort)); + (map_index (fn (i, _) => + Dict ([], Dict_Var { var = v, index = i, length = length sort })) sort)); fun print_term is_pseudo_fun some_thm vars fxy (IConst const) = print_app is_pseudo_fun some_thm vars fxy (const, []) | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = @@ -398,12 +399,13 @@ brackify BR ((str o deresolve_inst) inst :: (if is_pseudo_fun (Class_Instance inst) then [str "()"] else map_filter (print_dicts is_pseudo_fun BR) dss)) - | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) = - str (if k = 1 then "_" ^ Name.enforce_case true v - else "_" ^ Name.enforce_case true v ^ string_of_int (i+1)) + | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length }) = + str (if length = 1 then "_" ^ Name.enforce_case true var + else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1)) and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR - (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort)); + (map_index (fn (i, _) => + Dict ([], Dict_Var { var = v, index = i, length = length sort })) sort)); fun print_term is_pseudo_fun some_thm vars fxy (IConst const) = print_app is_pseudo_fun some_thm vars fxy (const, []) | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = diff -r f2fc5485e3b0 -r b351da9b4c7d src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Wed Mar 09 17:16:08 2016 +0000 +++ b/src/Tools/Code/code_preproc.ML Wed Mar 09 17:22:43 2016 +0000 @@ -476,7 +476,7 @@ fun dicts_of ctxt (proj_sort, algebra) (T, sort) = let val thy = Proof_Context.theory_of ctxt; - fun class_relation (x, _) _ = x; + fun class_relation _ (x, _) _ = x; fun type_constructor (tyco, _) xs class = inst_params thy tyco (Sorts.complete_sort algebra [class]) @ (maps o maps) fst xs; diff -r f2fc5485e3b0 -r b351da9b4c7d src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Wed Mar 09 17:16:08 2016 +0000 +++ b/src/Tools/Code/code_thingol.ML Wed Mar 09 17:22:43 2016 +0000 @@ -19,7 +19,7 @@ Dict of (class * class) list * plain_dict and plain_dict = Dict_Const of (string * class) * dict list list - | Dict_Var of vname * (int * int); + | Dict_Var of { var: vname, index: int, length: int }; datatype itype = `%% of string * itype list | ITyVar of vname; @@ -132,7 +132,7 @@ Dict of (class * class) list * plain_dict and plain_dict = Dict_Const of (string * class) * dict list list - | Dict_Var of vname * (int * int); + | Dict_Var of { var: vname, index: int, length: int }; datatype itype = `%% of string * itype list @@ -482,7 +482,7 @@ val sort' = proj_sort sort; in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end; val typarg_witnesses = Sorts.of_sort_derivation algebra - {class_relation = K (Sorts.classrel_derivation algebra class_relation), + {class_relation = fn _ => fn _ => Sorts.classrel_derivation algebra class_relation, type_constructor = type_constructor, type_variable = type_variable} (ty, proj_sort sort) handle Sorts.CLASS_ERROR e => not_wellsorted ctxt permissive some_thm deps ty sort e; @@ -760,8 +760,8 @@ ensure_inst ctxt algbr eqngr permissive inst ##>> (fold_map o fold_map) mk_dict dss #>> (fn (inst, dss) => Dict_Const (inst, dss)) - | mk_plain_dict (Local (v, (n, sort))) = - pair (Dict_Var (unprefix "'" v, (n, length sort))) + | mk_plain_dict (Local (v, (index, sort))) = + pair (Dict_Var { var = unprefix "'" v, index = index, length = length sort }) in construct_dictionaries ctxt algbr permissive some_thm (ty, sort) #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses) diff -r f2fc5485e3b0 -r b351da9b4c7d src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed Mar 09 17:16:08 2016 +0000 +++ b/src/Tools/nbe.ML Wed Mar 09 17:22:43 2016 +0000 @@ -311,8 +311,8 @@ assemble_classrels classrels (assemble_plain_dict x) and assemble_plain_dict (Dict_Const (inst, dss)) = assemble_constapp (Class_Instance inst) dss [] - | assemble_plain_dict (Dict_Var (v, (n, _))) = - nbe_dict v n + | assemble_plain_dict (Dict_Var { var, index, ... }) = + nbe_dict var index fun assemble_iterm constapp = let