merged
authorblanchet
Thu Jan 30 22:55:52 2014 +0100 (2014-01-30)
changeset 55196a823137bcd87
parent 55195 067142c53c3b
parent 55190 81070502914c
child 55197 5a54ed681ba2
merged
     1.1 --- a/src/HOL/Rings.thy	Thu Jan 30 22:42:29 2014 +0100
     1.2 +++ b/src/HOL/Rings.thy	Thu Jan 30 22:55:52 2014 +0100
     1.3 @@ -99,6 +99,14 @@
     1.4    "of_bool p = of_bool q \<longleftrightarrow> p = q"
     1.5    by (simp add: of_bool_def)
     1.6  
     1.7 +lemma split_of_bool [split]:
     1.8 +  "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)"
     1.9 +  by (cases p) simp_all
    1.10 +
    1.11 +lemma split_of_bool_asm:
    1.12 +  "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
    1.13 +  by (cases p) simp_all
    1.14 +  
    1.15  end  
    1.16  
    1.17  class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
     2.1 --- a/src/Tools/Code/code_runtime.ML	Thu Jan 30 22:42:29 2014 +0100
     2.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Jan 30 22:55:52 2014 +0100
     2.3 @@ -196,7 +196,7 @@
     2.4  fun evaluation_code thy module_name tycos consts =
     2.5    let
     2.6      val ctxt = Proof_Context.init_global thy;
     2.7 -    val program = Code_Thingol.consts_program thy false consts;
     2.8 +    val program = Code_Thingol.consts_program thy consts;
     2.9      val (ml_modules, target_names) =
    2.10        Code_Target.produce_code_for thy
    2.11          target NONE module_name [] program (map Constant consts @ map Type_Constructor tycos);
     3.1 --- a/src/Tools/Code/code_target.ML	Thu Jan 30 22:42:29 2014 +0100
     3.2 +++ b/src/Tools/Code/code_target.ML	Thu Jan 30 22:55:52 2014 +0100
     3.3 @@ -8,7 +8,6 @@
     3.4  sig
     3.5    val cert_tyco: theory -> string -> string
     3.6    val read_tyco: theory -> string -> string
     3.7 -  val read_const_exprs: theory -> string list -> string list
     3.8  
     3.9    val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
    3.10      -> Code_Thingol.program -> Code_Symbol.T list -> unit
    3.11 @@ -458,44 +457,39 @@
    3.12  
    3.13  (* code generation *)
    3.14  
    3.15 -fun read_const_exprs thy const_exprs =
    3.16 -  let
    3.17 -    val (cs1, cs2) = Code_Thingol.read_const_exprs thy const_exprs;
    3.18 -    val program = Code_Thingol.consts_program thy true cs2;
    3.19 -    val cs3 = Code_Thingol.implemented_deps program;
    3.20 -  in union (op =) cs3 cs1 end;
    3.21 -
    3.22  fun prep_destination "" = NONE
    3.23    | prep_destination s = SOME (Path.explode s);
    3.24  
    3.25  fun export_code thy cs seris =
    3.26    let
    3.27 -    val program = Code_Thingol.consts_program thy false cs;
    3.28 +    val program = Code_Thingol.consts_program thy cs;
    3.29      val _ = map (fn (((target, module_name), some_path), args) =>
    3.30        export_code_for thy some_path target NONE module_name args program (map Constant cs)) seris;
    3.31    in () end;
    3.32  
    3.33 -fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs)
    3.34 +fun export_code_cmd raw_cs seris thy = export_code thy
    3.35 +  (Code_Thingol.read_const_exprs thy raw_cs)
    3.36    ((map o apfst o apsnd) prep_destination seris);
    3.37  
    3.38  fun produce_code thy cs target some_width some_module_name args =
    3.39    let
    3.40 -    val program = Code_Thingol.consts_program thy false cs;
    3.41 +    val program = Code_Thingol.consts_program thy cs;
    3.42    in produce_code_for thy target some_width some_module_name args program (map Constant cs) end;
    3.43  
    3.44  fun present_code thy cs syms target some_width some_module_name args =
    3.45    let
    3.46 -    val program = Code_Thingol.consts_program thy false cs;
    3.47 +    val program = Code_Thingol.consts_program thy cs;
    3.48    in present_code_for thy target some_width some_module_name args program (map Constant cs, syms) end;
    3.49  
    3.50  fun check_code thy cs seris =
    3.51    let
    3.52 -    val program = Code_Thingol.consts_program thy false cs;
    3.53 +    val program = Code_Thingol.consts_program thy cs;
    3.54      val _ = map (fn ((target, strict), args) =>
    3.55        check_code_for thy target strict args program (map Constant cs)) seris;
    3.56    in () end;
    3.57  
    3.58 -fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
    3.59 +fun check_code_cmd raw_cs seris thy = check_code thy
    3.60 +  (Code_Thingol.read_const_exprs thy raw_cs) seris;
    3.61  
    3.62  local
    3.63  
     4.1 --- a/src/Tools/Code/code_thingol.ML	Thu Jan 30 22:42:29 2014 +0100
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Jan 30 22:55:52 2014 +0100
     4.3 @@ -83,8 +83,8 @@
     4.4      -> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list
     4.5        * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list
     4.6  
     4.7 -  val read_const_exprs: theory -> string list -> string list * string list
     4.8 -  val consts_program: theory -> bool -> string list -> program
     4.9 +  val read_const_exprs: theory -> string list -> string list
    4.10 +  val consts_program: theory -> string list -> program
    4.11    val dynamic_conv: theory -> (program
    4.12      -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
    4.13      -> conv
    4.14 @@ -363,54 +363,61 @@
    4.15  
    4.16  (* generic mechanisms *)
    4.17  
    4.18 -fun ensure_stmt symbolize generate x (dep, program) =
    4.19 +fun ensure_stmt symbolize generate x (deps, program) =
    4.20    let
    4.21      val sym = symbolize x;
    4.22 -    val add_dep = case dep of NONE => I
    4.23 -      | SOME dep => Code_Symbol.Graph.add_edge (dep, sym);
    4.24 +    val add_dep = case deps of [] => I
    4.25 +      | dep :: _ => Code_Symbol.Graph.add_edge (dep, sym);
    4.26    in
    4.27      if can (Code_Symbol.Graph.get_node program) sym
    4.28      then
    4.29        program
    4.30        |> add_dep
    4.31 -      |> pair dep
    4.32 +      |> pair deps
    4.33        |> pair x
    4.34      else
    4.35        program
    4.36        |> Code_Symbol.Graph.default_node (sym, NoStmt)
    4.37        |> add_dep
    4.38 -      |> curry generate (SOME sym)
    4.39 +      |> curry generate (sym :: deps)
    4.40        ||> snd
    4.41        |-> (fn stmt => (Code_Symbol.Graph.map_node sym) (K stmt))
    4.42 -      |> pair dep
    4.43 +      |> pair deps
    4.44        |> pair x
    4.45    end;
    4.46  
    4.47  exception PERMISSIVE of unit;
    4.48  
    4.49 -fun translation_error thy permissive some_thm msg sub_msg =
    4.50 +fun translation_error thy program permissive some_thm deps msg sub_msg =
    4.51    if permissive
    4.52    then raise PERMISSIVE ()
    4.53    else
    4.54      let
    4.55 -      val err_thm =
    4.56 -        (case some_thm of
    4.57 -          SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
    4.58 -        | NONE => "");
    4.59 -    in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
    4.60 +      val ctxt = Proof_Context.init_global thy;
    4.61 +      val thm_msg =
    4.62 +        Option.map (fn thm => "in code equation " ^ Display.string_of_thm ctxt thm) some_thm;
    4.63 +      val dep_msg = if null (tl deps) then NONE
    4.64 +        else SOME ("with dependency "
    4.65 +          ^ space_implode " -> " (map (Code_Symbol.quote ctxt) (rev deps)));
    4.66 +      val thm_dep_msg = case (thm_msg, dep_msg)
    4.67 +       of (SOME thm_msg, SOME dep_msg) => "\n(" ^ thm_msg ^ ",\n" ^ dep_msg ^ ")"
    4.68 +        | (SOME thm_msg, NONE) => "\n(" ^ thm_msg ^ ")"
    4.69 +        | (NONE, SOME dep_msg) => "\n(" ^ dep_msg ^ ")"
    4.70 +        | (NONE, NONE) => ""
    4.71 +    in error (msg ^ thm_dep_msg ^ ":\n" ^ sub_msg) end;
    4.72  
    4.73  fun maybe_permissive f prgrm =
    4.74    f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm);
    4.75  
    4.76 -fun not_wellsorted thy permissive some_thm ty sort e =
    4.77 +fun not_wellsorted thy program permissive some_thm deps ty sort e =
    4.78    let
    4.79      val err_class = Sorts.class_error (Context.pretty_global thy) e;
    4.80      val err_typ =
    4.81        "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort " ^
    4.82          Syntax.string_of_sort_global thy sort;
    4.83    in
    4.84 -    translation_error thy permissive some_thm "Wellsortedness error"
    4.85 -      (err_typ ^ "\n" ^ err_class)
    4.86 +    translation_error thy program permissive some_thm deps
    4.87 +      "Wellsortedness error" (err_typ ^ "\n" ^ err_class)
    4.88    end;
    4.89  
    4.90  
    4.91 @@ -455,6 +462,32 @@
    4.92      (annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns
    4.93  
    4.94  
    4.95 +(* abstract dictionary construction *)
    4.96 +
    4.97 +datatype typarg_witness =
    4.98 +    Weakening of (class * class) list * plain_typarg_witness
    4.99 +and plain_typarg_witness =
   4.100 +    Global of (string * class) * typarg_witness list list
   4.101 +  | Local of string * (int * sort);
   4.102 +
   4.103 +fun construct_dictionaries thy (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) =
   4.104 +  let
   4.105 +    fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
   4.106 +      Weakening ((sub_class, super_class) :: classrels, x);
   4.107 +    fun type_constructor (tyco, _) dss class =
   4.108 +      Weakening ([], Global ((tyco, class), (map o map) fst dss));
   4.109 +    fun type_variable (TFree (v, sort)) =
   4.110 +      let
   4.111 +        val sort' = proj_sort sort;
   4.112 +      in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end;
   4.113 +    val typarg_witnesses = Sorts.of_sort_derivation algebra
   4.114 +      {class_relation = K (Sorts.classrel_derivation algebra class_relation),
   4.115 +       type_constructor = type_constructor,
   4.116 +       type_variable = type_variable} (ty, proj_sort sort)
   4.117 +      handle Sorts.CLASS_ERROR e => not_wellsorted thy program permissive some_thm deps ty sort e;
   4.118 +  in (typarg_witnesses, (deps, program)) end;
   4.119 +
   4.120 +
   4.121  (* translation *)
   4.122  
   4.123  fun ensure_tyco thy algbr eqngr permissive tyco =
   4.124 @@ -589,13 +622,16 @@
   4.125    #>> rpair (some_thm, proper)
   4.126  and translate_eqns thy algbr eqngr permissive eqns =
   4.127    maybe_permissive (fold_map (translate_eqn thy algbr eqngr permissive) eqns)
   4.128 -and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) =
   4.129 +and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) (deps, program) =
   4.130    let
   4.131      val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
   4.132          andalso Code.is_abstr thy c
   4.133 -        then translation_error thy permissive some_thm
   4.134 +        then translation_error thy program permissive some_thm deps
   4.135            "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
   4.136        else ()
   4.137 +  in translate_const_proper thy algbr eqngr permissive some_thm (c, ty) (deps, program) end
   4.138 +and translate_const_proper thy algbr eqngr permissive some_thm (c, ty) =
   4.139 +  let
   4.140      val (annotate, ty') = dest_tagged_type ty;
   4.141      val typargs = Sign.const_typargs thy (c, ty');
   4.142      val sorts = Code_Preproc.sortargs eqngr c;
   4.143 @@ -693,26 +729,8 @@
   4.144  and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr permissive (v, sort) =
   4.145    fold_map (ensure_class thy algbr eqngr permissive) (proj_sort sort)
   4.146    #>> (fn sort => (unprefix "'" v, sort))
   4.147 -and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) =
   4.148 +and translate_dicts thy algbr eqngr permissive some_thm (ty, sort) =
   4.149    let
   4.150 -    datatype typarg_witness =
   4.151 -        Weakening of (class * class) list * plain_typarg_witness
   4.152 -    and plain_typarg_witness =
   4.153 -        Global of (string * class) * typarg_witness list list
   4.154 -      | Local of string * (int * sort);
   4.155 -    fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
   4.156 -      Weakening ((sub_class, super_class) :: classrels, x);
   4.157 -    fun type_constructor (tyco, _) dss class =
   4.158 -      Weakening ([], Global ((tyco, class), (map o map) fst dss));
   4.159 -    fun type_variable (TFree (v, sort)) =
   4.160 -      let
   4.161 -        val sort' = proj_sort sort;
   4.162 -      in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end;
   4.163 -    val typarg_witnesses = Sorts.of_sort_derivation algebra
   4.164 -      {class_relation = K (Sorts.classrel_derivation algebra class_relation),
   4.165 -       type_constructor = type_constructor,
   4.166 -       type_variable = type_variable} (ty, proj_sort sort)
   4.167 -      handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e;
   4.168      fun mk_dict (Weakening (classrels, x)) =
   4.169            fold_map (ensure_classrel thy algbr eqngr permissive) classrels
   4.170            ##>> mk_plain_dict x
   4.171 @@ -723,7 +741,10 @@
   4.172            #>> (fn (inst, dss) => Dict_Const (inst, dss))
   4.173        | mk_plain_dict (Local (v, (n, sort))) =
   4.174            pair (Dict_Var (unprefix "'" v, (n, length sort)))
   4.175 -  in fold_map mk_dict typarg_witnesses end;
   4.176 +  in
   4.177 +    construct_dictionaries thy algbr permissive some_thm (ty, sort)
   4.178 +    #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses)
   4.179 +  end;
   4.180  
   4.181  
   4.182  (* store *)
   4.183 @@ -736,26 +757,32 @@
   4.184  
   4.185  fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing =
   4.186    Program.change_yield (if ignore_cache then NONE else SOME thy)
   4.187 -    (fn program => (NONE, program)
   4.188 +    (fn program => ([], program)
   4.189        |> generate thy algebra eqngr thing
   4.190        |-> (fn thing => fn (_, program) => (thing, program)));
   4.191  
   4.192  
   4.193  (* program generation *)
   4.194  
   4.195 -fun consts_program thy permissive consts =
   4.196 +fun consts_program_internal thy permissive consts =
   4.197    let
   4.198 -    fun project program =
   4.199 -      if permissive then program
   4.200 -      else Code_Symbol.Graph.restrict
   4.201 -        (member (op =) (Code_Symbol.Graph.all_succs program
   4.202 -          (map Constant consts))) program;
   4.203      fun generate_consts thy algebra eqngr =
   4.204        fold_map (ensure_const thy algebra eqngr permissive);
   4.205    in
   4.206      invoke_generation permissive thy (Code_Preproc.obtain false thy consts [])
   4.207        generate_consts consts
   4.208      |> snd
   4.209 +  end;
   4.210 +
   4.211 +fun consts_program_permissive thy = consts_program_internal thy true;
   4.212 +
   4.213 +fun consts_program thy consts =
   4.214 +  let
   4.215 +    fun project program = Code_Symbol.Graph.restrict
   4.216 +      (member (op =) (Code_Symbol.Graph.all_succs program
   4.217 +        (map Constant consts))) program;
   4.218 +  in
   4.219 +    consts_program_internal thy false consts
   4.220      |> project
   4.221    end;
   4.222  
   4.223 @@ -775,15 +802,15 @@
   4.224        ##>> translate_term thy algbr eqngr false NONE (t', NONE)
   4.225        #>> (fn ((vs, ty), t) => Fun
   4.226          (((vs, ty), [(([], t), (NONE, true))]), NONE));
   4.227 -    fun term_value (dep, program1) =
   4.228 +    fun term_value (deps, program1) =
   4.229        let
   4.230          val Fun ((vs_ty, [(([], t), _)]), _) =
   4.231            Code_Symbol.Graph.get_node program1 dummy_constant;
   4.232 -        val deps = Code_Symbol.Graph.immediate_succs program1 dummy_constant;
   4.233 +        val deps' = Code_Symbol.Graph.immediate_succs program1 dummy_constant;
   4.234          val program2 = Code_Symbol.Graph.del_node dummy_constant program1;
   4.235 -        val deps_all = Code_Symbol.Graph.all_succs program2 deps;
   4.236 +        val deps_all = Code_Symbol.Graph.all_succs program2 deps';
   4.237          val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
   4.238 -      in ((program3, ((vs_ty, t), deps)), (dep, program2)) end;
   4.239 +      in ((program3, ((vs_ty, t), deps')), (deps, program2)) end;
   4.240    in
   4.241      ensure_stmt Constant stmt_value @{const_name dummy_pattern}
   4.242      #> snd
   4.243 @@ -808,7 +835,7 @@
   4.244  fun lift_evaluation thy evaluation' algebra eqngr program vs t =
   4.245    let
   4.246      val ((_, (((vs', ty'), t'), deps)), _) =
   4.247 -      ensure_value thy algebra eqngr t (NONE, program);
   4.248 +      ensure_value thy algebra eqngr t ([], program);
   4.249    in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
   4.250  
   4.251  fun lift_evaluator thy evaluator' consts algebra eqngr =
   4.252 @@ -838,9 +865,9 @@
   4.253    Code_Preproc.static_value thy postproc consts (lift_evaluator thy evaluator consts);
   4.254  
   4.255  
   4.256 -(** diagnostic commands **)
   4.257 +(** constant expressions **)
   4.258  
   4.259 -fun read_const_exprs thy =
   4.260 +fun read_const_exprs_internal thy =
   4.261    let
   4.262      fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
   4.263        ((snd o #constants o Consts.dest o Sign.consts_of) thy') [];
   4.264 @@ -859,6 +886,17 @@
   4.265        | NONE => ([Code.read_const thy str], []));
   4.266    in pairself flat o split_list o map read_const_expr end;
   4.267  
   4.268 +fun read_const_exprs_all thy = op @ o read_const_exprs_internal thy;
   4.269 +
   4.270 +fun read_const_exprs thy const_exprs =
   4.271 +  let
   4.272 +    val (consts, consts_permissive) = read_const_exprs_internal thy const_exprs;
   4.273 +    val consts' = implemented_deps (consts_program_permissive thy consts_permissive);
   4.274 +  in union (op =) consts' consts end;
   4.275 +
   4.276 +
   4.277 +(** diagnostic commands **)
   4.278 +
   4.279  fun code_depgr thy consts =
   4.280    let
   4.281      val (_, eqngr) = Code_Preproc.obtain true thy consts [];
   4.282 @@ -888,8 +926,8 @@
   4.283  
   4.284  local
   4.285  
   4.286 -fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy;
   4.287 -fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy;
   4.288 +fun code_thms_cmd thy = code_thms thy o read_const_exprs_all thy;
   4.289 +fun code_deps_cmd thy = code_deps thy o read_const_exprs_all thy;
   4.290  
   4.291  in
   4.292