added polyml_as_definition -- using external SML files as substitute for proper definitions -- only for polyml!
authorhaftmann
Fri Oct 01 11:46:09 2010 +0200 (2010-10-01)
changeset 39816c7cec137c48a
parent 39811 0659e84bdc5f
child 39817 5228c6b20273
added polyml_as_definition -- using external SML files as substitute for proper definitions -- only for polyml!
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Oct 01 10:25:36 2010 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Oct 01 11:46:09 2010 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4      -> theory -> theory
     1.5    datatype truth = Holds
     1.6    val put_truth: (unit -> truth) -> Proof.context -> Proof.context
     1.7 +  val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
     1.8  end;
     1.9  
    1.10  structure Code_Runtime : CODE_RUNTIME =
    1.11 @@ -341,4 +342,93 @@
    1.12  
    1.13  end; (*local*)
    1.14  
    1.15 +
    1.16 +(** using external SML files as substitute for proper definitions -- only for polyml!  **)
    1.17 +
    1.18 +local
    1.19 +
    1.20 +structure Loaded_Values = Theory_Data(
    1.21 +  type T = string list
    1.22 +  val empty = []
    1.23 +  val merge = merge (op =)
    1.24 +  val extend = I
    1.25 +);
    1.26 +
    1.27 +fun notify_val (string, value) = 
    1.28 +  let
    1.29 +    val _ = #enterVal ML_Env.name_space (string, value);
    1.30 +    val _ = Context.>> ((Context.map_theory o Loaded_Values.map) (insert (op =) string));
    1.31 +  in () end;
    1.32 +
    1.33 +fun abort _ = error "Only value bindings allowed.";
    1.34 +
    1.35 +val notifying_context : use_context =
    1.36 + {tune_source = #tune_source ML_Env.local_context,
    1.37 +  name_space =
    1.38 +   {lookupVal    = #lookupVal ML_Env.name_space,
    1.39 +    lookupType   = #lookupType ML_Env.name_space,
    1.40 +    lookupFix    = #lookupFix ML_Env.name_space,
    1.41 +    lookupStruct = #lookupStruct ML_Env.name_space,
    1.42 +    lookupSig    = #lookupSig ML_Env.name_space,
    1.43 +    lookupFunct  = #lookupFunct ML_Env.name_space,
    1.44 +    enterVal     = notify_val,
    1.45 +    enterType    = abort,
    1.46 +    enterFix     = abort,
    1.47 +    enterStruct  = abort,
    1.48 +    enterSig     = abort,
    1.49 +    enterFunct   = abort,
    1.50 +    allVal       = #allVal ML_Env.name_space,
    1.51 +    allType      = #allType ML_Env.name_space,
    1.52 +    allFix       = #allFix ML_Env.name_space,
    1.53 +    allStruct    = #allStruct ML_Env.name_space,
    1.54 +    allSig       = #allSig ML_Env.name_space,
    1.55 +    allFunct     = #allFunct ML_Env.name_space},
    1.56 +  str_of_pos = #str_of_pos ML_Env.local_context,
    1.57 +  print = #print ML_Env.local_context,
    1.58 +  error = #error ML_Env.local_context};
    1.59 +
    1.60 +in
    1.61 +
    1.62 +fun use_file filepath thy =
    1.63 +  let
    1.64 +    val thy' = Loaded_Values.put [] thy;
    1.65 +    val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
    1.66 +    val _ = Secure.use_text notifying_context
    1.67 +      (0, Path.implode filepath) false (File.read filepath);
    1.68 +    val thy'' = (Context.the_theory o the) (Context.thread_data ())
    1.69 +    val names = Loaded_Values.get thy''
    1.70 +  in (names, thy'') end;
    1.71 +
    1.72 +end;
    1.73 +
    1.74 +fun add_definiendum (ml_name, (b, T)) thy =
    1.75 +  thy
    1.76 +  |> Code_Target.add_reserved target ml_name
    1.77 +  |> Specification.axiomatization [(b, SOME T, NoSyn)] []
    1.78 +  |-> (fn ([Const (const, _)], _) =>
    1.79 +     Code_Target.add_const_syntax target const
    1.80 +       (SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name))));
    1.81 +
    1.82 +fun process_file filepath (definienda, thy) =
    1.83 +  let
    1.84 +    val (ml_names, thy') = use_file filepath thy;
    1.85 +    val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names;
    1.86 +    val _ = if null superfluous then ()
    1.87 +      else error ("Value binding(s) " ^ commas_quote superfluous
    1.88 +        ^ " found in external file " ^ quote (Path.implode filepath)
    1.89 +        ^ " not present among the given contants binding(s).");
    1.90 +    val these_definienda = AList.make (the o AList.lookup (op =) definienda) ml_names;
    1.91 +    val thy'' = fold add_definiendum these_definienda thy';
    1.92 +    val definienda' = fold (AList.delete (op =)) ml_names definienda;
    1.93 +  in (definienda', thy'') end;
    1.94 +
    1.95 +fun polyml_as_definition bTs filepaths thy =
    1.96 +  let
    1.97 +    val definienda = map (fn bT => ((Binding.name_of o fst) bT, bT)) bTs;
    1.98 +    val (remaining, thy') = fold process_file filepaths (definienda, thy);
    1.99 +    val _ = if null remaining then ()
   1.100 +      else error ("Constant binding(s) " ^ commas_quote (map fst remaining)
   1.101 +        ^ " not present in external file(s).");
   1.102 +  in thy' end;
   1.103 +
   1.104  end; (*struct*)