# HG changeset patch # User blanchet # Date 1391118952 -3600 # Node ID a823137bcd87caf2121aa81373b334c08116929f # Parent 067142c53c3bf80a026cd382dc5bc8c1eaeb96be# Parent 81070502914c2fb7c39a95968582078ffd4468ae merged diff -r 067142c53c3b -r a823137bcd87 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Thu Jan 30 22:42:29 2014 +0100 +++ b/src/HOL/Rings.thy Thu Jan 30 22:55:52 2014 +0100 @@ -99,6 +99,14 @@ "of_bool p = of_bool q \ p = q" by (simp add: of_bool_def) +lemma split_of_bool [split]: + "P (of_bool p) \ (p \ P 1) \ (\ p \ P 0)" + by (cases p) simp_all + +lemma split_of_bool_asm: + "P (of_bool p) \ \ (p \ \ P 1 \ \ p \ \ P 0)" + by (cases p) simp_all + end class semiring_1 = zero_neq_one + semiring_0 + monoid_mult diff -r 067142c53c3b -r a823137bcd87 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Thu Jan 30 22:42:29 2014 +0100 +++ b/src/Tools/Code/code_runtime.ML Thu Jan 30 22:55:52 2014 +0100 @@ -196,7 +196,7 @@ fun evaluation_code thy module_name tycos consts = let val ctxt = Proof_Context.init_global thy; - val program = Code_Thingol.consts_program thy false consts; + val program = Code_Thingol.consts_program thy consts; val (ml_modules, target_names) = Code_Target.produce_code_for thy target NONE module_name [] program (map Constant consts @ map Type_Constructor tycos); diff -r 067142c53c3b -r a823137bcd87 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Jan 30 22:42:29 2014 +0100 +++ b/src/Tools/Code/code_target.ML Thu Jan 30 22:55:52 2014 +0100 @@ -8,7 +8,6 @@ sig val cert_tyco: theory -> string -> string val read_tyco: theory -> string -> string - val read_const_exprs: theory -> string list -> string list val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list -> Code_Thingol.program -> Code_Symbol.T list -> unit @@ -458,44 +457,39 @@ (* code generation *) -fun read_const_exprs thy const_exprs = - let - val (cs1, cs2) = Code_Thingol.read_const_exprs thy const_exprs; - val program = Code_Thingol.consts_program thy true cs2; - val cs3 = Code_Thingol.implemented_deps program; - in union (op =) cs3 cs1 end; - fun prep_destination "" = NONE | prep_destination s = SOME (Path.explode s); fun export_code thy cs seris = let - val program = Code_Thingol.consts_program thy false cs; + val program = Code_Thingol.consts_program thy cs; val _ = map (fn (((target, module_name), some_path), args) => export_code_for thy some_path target NONE module_name args program (map Constant cs)) seris; in () end; -fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) +fun export_code_cmd raw_cs seris thy = export_code thy + (Code_Thingol.read_const_exprs thy raw_cs) ((map o apfst o apsnd) prep_destination seris); fun produce_code thy cs target some_width some_module_name args = let - val program = Code_Thingol.consts_program thy false cs; + val program = Code_Thingol.consts_program thy cs; in produce_code_for thy target some_width some_module_name args program (map Constant cs) end; fun present_code thy cs syms target some_width some_module_name args = let - val program = Code_Thingol.consts_program thy false cs; + val program = Code_Thingol.consts_program thy cs; in present_code_for thy target some_width some_module_name args program (map Constant cs, syms) end; fun check_code thy cs seris = let - val program = Code_Thingol.consts_program thy false cs; + val program = Code_Thingol.consts_program thy cs; val _ = map (fn ((target, strict), args) => check_code_for thy target strict args program (map Constant cs)) seris; in () end; -fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris; +fun check_code_cmd raw_cs seris thy = check_code thy + (Code_Thingol.read_const_exprs thy raw_cs) seris; local diff -r 067142c53c3b -r a823137bcd87 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Thu Jan 30 22:42:29 2014 +0100 +++ b/src/Tools/Code/code_thingol.ML Thu Jan 30 22:55:52 2014 +0100 @@ -83,8 +83,8 @@ -> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list - val read_const_exprs: theory -> string list -> string list * string list - val consts_program: theory -> bool -> string list -> program + val read_const_exprs: theory -> string list -> string list + val consts_program: theory -> string list -> program val dynamic_conv: theory -> (program -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv) -> conv @@ -363,54 +363,61 @@ (* generic mechanisms *) -fun ensure_stmt symbolize generate x (dep, program) = +fun ensure_stmt symbolize generate x (deps, program) = let val sym = symbolize x; - val add_dep = case dep of NONE => I - | SOME dep => Code_Symbol.Graph.add_edge (dep, sym); + val add_dep = case deps of [] => I + | dep :: _ => Code_Symbol.Graph.add_edge (dep, sym); in if can (Code_Symbol.Graph.get_node program) sym then program |> add_dep - |> pair dep + |> pair deps |> pair x else program |> Code_Symbol.Graph.default_node (sym, NoStmt) |> add_dep - |> curry generate (SOME sym) + |> curry generate (sym :: deps) ||> snd |-> (fn stmt => (Code_Symbol.Graph.map_node sym) (K stmt)) - |> pair dep + |> pair deps |> pair x end; exception PERMISSIVE of unit; -fun translation_error thy permissive some_thm msg sub_msg = +fun translation_error thy program permissive some_thm deps msg sub_msg = if permissive then raise PERMISSIVE () else let - val err_thm = - (case some_thm of - SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")" - | NONE => ""); - in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end; + val ctxt = Proof_Context.init_global thy; + val thm_msg = + Option.map (fn thm => "in code equation " ^ Display.string_of_thm ctxt thm) some_thm; + val dep_msg = if null (tl deps) then NONE + else SOME ("with dependency " + ^ space_implode " -> " (map (Code_Symbol.quote ctxt) (rev deps))); + val thm_dep_msg = case (thm_msg, dep_msg) + of (SOME thm_msg, SOME dep_msg) => "\n(" ^ thm_msg ^ ",\n" ^ dep_msg ^ ")" + | (SOME thm_msg, NONE) => "\n(" ^ thm_msg ^ ")" + | (NONE, SOME dep_msg) => "\n(" ^ dep_msg ^ ")" + | (NONE, NONE) => "" + in error (msg ^ thm_dep_msg ^ ":\n" ^ sub_msg) end; fun maybe_permissive f prgrm = f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm); -fun not_wellsorted thy permissive some_thm ty sort e = +fun not_wellsorted thy program permissive some_thm deps ty sort e = let val err_class = Sorts.class_error (Context.pretty_global thy) e; val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort " ^ Syntax.string_of_sort_global thy sort; in - translation_error thy permissive some_thm "Wellsortedness error" - (err_typ ^ "\n" ^ err_class) + translation_error thy program permissive some_thm deps + "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end; @@ -455,6 +462,32 @@ (annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns +(* abstract dictionary construction *) + +datatype typarg_witness = + Weakening of (class * class) list * plain_typarg_witness +and plain_typarg_witness = + Global of (string * class) * typarg_witness list list + | Local of string * (int * sort); + +fun construct_dictionaries thy (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) = + let + fun class_relation ((Weakening (classrels, x)), sub_class) super_class = + Weakening ((sub_class, super_class) :: classrels, x); + fun type_constructor (tyco, _) dss class = + Weakening ([], Global ((tyco, class), (map o map) fst dss)); + fun type_variable (TFree (v, sort)) = + let + 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), + type_constructor = type_constructor, + type_variable = type_variable} (ty, proj_sort sort) + handle Sorts.CLASS_ERROR e => not_wellsorted thy program permissive some_thm deps ty sort e; + in (typarg_witnesses, (deps, program)) end; + + (* translation *) fun ensure_tyco thy algbr eqngr permissive tyco = @@ -589,13 +622,16 @@ #>> rpair (some_thm, proper) and translate_eqns thy algbr eqngr permissive eqns = maybe_permissive (fold_map (translate_eqn thy algbr eqngr permissive) eqns) -and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) = +and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) (deps, program) = let val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs)) andalso Code.is_abstr thy c - then translation_error thy permissive some_thm + then translation_error thy program permissive some_thm deps "Abstraction violation" ("constant " ^ Code.string_of_const thy c) else () + in translate_const_proper thy algbr eqngr permissive some_thm (c, ty) (deps, program) end +and translate_const_proper thy algbr eqngr permissive some_thm (c, ty) = + let val (annotate, ty') = dest_tagged_type ty; val typargs = Sign.const_typargs thy (c, ty'); val sorts = Code_Preproc.sortargs eqngr c; @@ -693,26 +729,8 @@ and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr permissive (v, sort) = fold_map (ensure_class thy algbr eqngr permissive) (proj_sort sort) #>> (fn sort => (unprefix "'" v, sort)) -and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) = +and translate_dicts thy algbr eqngr permissive some_thm (ty, sort) = let - datatype typarg_witness = - Weakening of (class * class) list * plain_typarg_witness - and plain_typarg_witness = - Global of (string * class) * typarg_witness list list - | Local of string * (int * sort); - fun class_relation ((Weakening (classrels, x)), sub_class) super_class = - Weakening ((sub_class, super_class) :: classrels, x); - fun type_constructor (tyco, _) dss class = - Weakening ([], Global ((tyco, class), (map o map) fst dss)); - fun type_variable (TFree (v, sort)) = - let - 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), - type_constructor = type_constructor, - type_variable = type_variable} (ty, proj_sort sort) - handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e; fun mk_dict (Weakening (classrels, x)) = fold_map (ensure_classrel thy algbr eqngr permissive) classrels ##>> mk_plain_dict x @@ -723,7 +741,10 @@ #>> (fn (inst, dss) => Dict_Const (inst, dss)) | mk_plain_dict (Local (v, (n, sort))) = pair (Dict_Var (unprefix "'" v, (n, length sort))) - in fold_map mk_dict typarg_witnesses end; + in + construct_dictionaries thy algbr permissive some_thm (ty, sort) + #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses) + end; (* store *) @@ -736,26 +757,32 @@ fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing = Program.change_yield (if ignore_cache then NONE else SOME thy) - (fn program => (NONE, program) + (fn program => ([], program) |> generate thy algebra eqngr thing |-> (fn thing => fn (_, program) => (thing, program))); (* program generation *) -fun consts_program thy permissive consts = +fun consts_program_internal thy permissive consts = let - fun project program = - if permissive then program - else Code_Symbol.Graph.restrict - (member (op =) (Code_Symbol.Graph.all_succs program - (map Constant consts))) program; fun generate_consts thy algebra eqngr = fold_map (ensure_const thy algebra eqngr permissive); in invoke_generation permissive thy (Code_Preproc.obtain false thy consts []) generate_consts consts |> snd + end; + +fun consts_program_permissive thy = consts_program_internal thy true; + +fun consts_program thy consts = + let + fun project program = Code_Symbol.Graph.restrict + (member (op =) (Code_Symbol.Graph.all_succs program + (map Constant consts))) program; + in + consts_program_internal thy false consts |> project end; @@ -775,15 +802,15 @@ ##>> translate_term thy algbr eqngr false NONE (t', NONE) #>> (fn ((vs, ty), t) => Fun (((vs, ty), [(([], t), (NONE, true))]), NONE)); - fun term_value (dep, program1) = + fun term_value (deps, program1) = let val Fun ((vs_ty, [(([], t), _)]), _) = Code_Symbol.Graph.get_node program1 dummy_constant; - val deps = Code_Symbol.Graph.immediate_succs program1 dummy_constant; + val deps' = Code_Symbol.Graph.immediate_succs program1 dummy_constant; val program2 = Code_Symbol.Graph.del_node dummy_constant program1; - val deps_all = Code_Symbol.Graph.all_succs program2 deps; + val deps_all = Code_Symbol.Graph.all_succs program2 deps'; val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2; - in ((program3, ((vs_ty, t), deps)), (dep, program2)) end; + in ((program3, ((vs_ty, t), deps')), (deps, program2)) end; in ensure_stmt Constant stmt_value @{const_name dummy_pattern} #> snd @@ -808,7 +835,7 @@ fun lift_evaluation thy evaluation' algebra eqngr program vs t = let val ((_, (((vs', ty'), t'), deps)), _) = - ensure_value thy algebra eqngr t (NONE, program); + ensure_value thy algebra eqngr t ([], program); in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end; fun lift_evaluator thy evaluator' consts algebra eqngr = @@ -838,9 +865,9 @@ Code_Preproc.static_value thy postproc consts (lift_evaluator thy evaluator consts); -(** diagnostic commands **) +(** constant expressions **) -fun read_const_exprs thy = +fun read_const_exprs_internal thy = let fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I) ((snd o #constants o Consts.dest o Sign.consts_of) thy') []; @@ -859,6 +886,17 @@ | NONE => ([Code.read_const thy str], [])); in pairself flat o split_list o map read_const_expr end; +fun read_const_exprs_all thy = op @ o read_const_exprs_internal thy; + +fun read_const_exprs thy const_exprs = + let + val (consts, consts_permissive) = read_const_exprs_internal thy const_exprs; + val consts' = implemented_deps (consts_program_permissive thy consts_permissive); + in union (op =) consts' consts end; + + +(** diagnostic commands **) + fun code_depgr thy consts = let val (_, eqngr) = Code_Preproc.obtain true thy consts []; @@ -888,8 +926,8 @@ local -fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy; -fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy; +fun code_thms_cmd thy = code_thms thy o read_const_exprs_all thy; +fun code_deps_cmd thy = code_deps thy o read_const_exprs_all thy; in