# HG changeset patch # User haftmann # Date 1391094544 -3600 # Node ID 7ca0204ece66b8647e25a418e47fa6f1d02eef7f # Parent 6d0d93316daf9b0e07b9b00c73d64bbcdd07e770 reduced prominence of "permissive code generation" diff -r 6d0d93316daf -r 7ca0204ece66 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Thu Jan 30 16:09:03 2014 +0100 +++ b/src/Tools/Code/code_runtime.ML Thu Jan 30 16:09:04 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 6d0d93316daf -r 7ca0204ece66 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Jan 30 16:09:03 2014 +0100 +++ b/src/Tools/Code/code_target.ML Thu Jan 30 16:09:04 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 6d0d93316daf -r 7ca0204ece66 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Thu Jan 30 16:09:03 2014 +0100 +++ b/src/Tools/Code/code_thingol.ML Thu Jan 30 16:09:04 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 @@ -743,19 +743,25 @@ (* 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; @@ -838,9 +844,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 +865,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 +905,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