src/Tools/Code/code_runtime.ML
changeset 40421 b41aabb629ce
parent 40320 abc52faa7761
child 40422 d425d1ed82af
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Nov 08 02:33:48 2010 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Nov 08 10:43:24 2010 +0100
     1.3 @@ -25,8 +25,8 @@
     1.4      -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result
     1.5    val dynamic_holds_conv: conv
     1.6    val static_holds_conv: theory -> string list -> conv
     1.7 -  val code_reflect: (string * string list) list -> string list -> string -> string option
     1.8 -    -> theory -> theory
     1.9 +  val code_reflect: (string * string list option) list -> string list -> string
    1.10 +    -> string option -> theory -> theory
    1.11    datatype truth = Holds
    1.12    val put_truth: (unit -> truth) -> Proof.context -> Proof.context
    1.13    val trace: bool Unsynchronized.ref
    1.14 @@ -213,8 +213,8 @@
    1.15  structure Code_Antiq_Data = Proof_Data
    1.16  (
    1.17    type T = (string list * string list) * (bool
    1.18 -    * (string * ((string * string) list * (string * string) list)) lazy);
    1.19 -  fun init _ = (([], []), (true, (Lazy.value ("", ([], [])))));
    1.20 +    * (string * (string * string) list) lazy);
    1.21 +  fun init _ = (([], []), (true, (Lazy.value ("", []))));
    1.22  );
    1.23  
    1.24  val is_first_occ = fst o snd o Code_Antiq_Data.get;
    1.25 @@ -225,24 +225,23 @@
    1.26      val tycos' = fold (insert (op =)) new_tycos tycos;
    1.27      val consts' = fold (insert (op =)) new_consts consts;
    1.28      val acc_code = Lazy.lazy (fn () =>
    1.29 -      evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts');
    1.30 +      evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts'
    1.31 +      |> apsnd fst);
    1.32    in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
    1.33  
    1.34  fun register_const const = register_code [] [const];
    1.35  
    1.36 -fun register_datatype tyco constrs = register_code [tyco] constrs;
    1.37 -
    1.38 -fun print_const const all_struct_name tycos_map consts_map =
    1.39 +fun print_const const all_struct_name consts_map =
    1.40    (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
    1.41  
    1.42 -fun print_code is_first print_it ctxt =
    1.43 +fun print_code is_first const ctxt =
    1.44    let
    1.45      val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
    1.46 -    val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
    1.47 +    val (ml_code, consts_map) = Lazy.force acc_code;
    1.48      val ml_code = if is_first then ml_code
    1.49        else "";
    1.50      val all_struct_name = "Isabelle";
    1.51 -  in (ml_code, print_it all_struct_name tycos_map consts_map) end;
    1.52 +  in (ml_code, print_const const all_struct_name consts_map) end;
    1.53  
    1.54  in
    1.55  
    1.56 @@ -251,33 +250,38 @@
    1.57      val const = Code.check_const (ProofContext.theory_of background) raw_const;
    1.58      val is_first = is_first_occ background;
    1.59      val background' = register_const const background;
    1.60 -  in (print_code is_first (print_const const), background') end;
    1.61 +  in (print_code is_first const, background') end;
    1.62  
    1.63  end; (*local*)
    1.64  
    1.65  
    1.66  (* reflection support *)
    1.67  
    1.68 -fun check_datatype thy tyco consts =
    1.69 +fun check_datatype thy tyco some_consts =
    1.70    let
    1.71      val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
    1.72 -    val missing_constrs = subtract (op =) consts constrs;
    1.73 -    val _ = if null missing_constrs then []
    1.74 -      else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
    1.75 -        ^ " for datatype " ^ quote tyco);
    1.76 -    val false_constrs = subtract (op =) constrs consts;
    1.77 -    val _ = if null false_constrs then []
    1.78 -      else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
    1.79 -        ^ " for datatype " ^ quote tyco);
    1.80 -  in () end;
    1.81 +    val _ = case some_consts
    1.82 +     of SOME consts =>
    1.83 +          let
    1.84 +            val missing_constrs = subtract (op =) consts constrs;
    1.85 +            val _ = if null missing_constrs then []
    1.86 +              else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
    1.87 +                ^ " for datatype " ^ quote tyco);
    1.88 +            val false_constrs = subtract (op =) constrs consts;
    1.89 +            val _ = if null false_constrs then []
    1.90 +              else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
    1.91 +                ^ " for datatype " ^ quote tyco)
    1.92 +          in () end
    1.93 +      | NONE => ();
    1.94 +  in (tyco, constrs) end;
    1.95  
    1.96  fun add_eval_tyco (tyco, tyco') thy =
    1.97    let
    1.98      val k = Sign.arity_number thy tyco;
    1.99 -    fun pr pr' fxy [] = tyco'
   1.100 -      | pr pr' fxy [ty] =
   1.101 +    fun pr pr' _ [] = tyco'
   1.102 +      | pr pr' _ [ty] =
   1.103            Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
   1.104 -      | pr pr' fxy tys =
   1.105 +      | pr pr' _ tys =
   1.106            Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
   1.107    in
   1.108      thy
   1.109 @@ -317,10 +321,9 @@
   1.110  fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy  =
   1.111    let
   1.112      val datatypes = map (fn (raw_tyco, raw_cos) =>
   1.113 -      (prep_type thy raw_tyco, map (prep_const thy) raw_cos)) raw_datatypes;
   1.114 -    val _ = map (uncurry (check_datatype thy)) datatypes;
   1.115 -    val tycos = map fst datatypes;
   1.116 -    val constrs = maps snd datatypes;
   1.117 +      (prep_type thy raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes;
   1.118 +    val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes
   1.119 +      |> apsnd flat;
   1.120      val functions = map (prep_const thy) raw_functions;
   1.121      val result = evaluation_code thy module_name tycos (constrs @ functions)
   1.122        |> (apsnd o apsnd) (chop (length constrs));
   1.123 @@ -347,7 +350,8 @@
   1.124  val _ = List.app Keyword.keyword [datatypesK, functionsK];
   1.125  
   1.126  val parse_datatype =
   1.127 -  Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term)));
   1.128 +  Parse.name --| Parse.$$$ "=" -- ((Parse.string >> (fn "*" => NONE | _ => Scan.fail ()))
   1.129 +    || ((Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))) >> SOME));
   1.130  
   1.131  in
   1.132