src/Pure/codegen.ML
changeset 22921 475ff421a6a3
parent 22846 fb79144af9a3
child 23178 07ba6b58b3d2
     1.1 --- a/src/Pure/codegen.ML	Thu May 10 10:21:50 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Thu May 10 10:22:17 2007 +0200
     1.3 @@ -35,13 +35,13 @@
     1.4      (string * string) list * codegr
     1.5    val generate_code_i: theory -> string list -> string -> (string * term) list ->
     1.6      (string * string) list * codegr
     1.7 -  val assoc_consts: (xstring * string option * (term mixfix list *
     1.8 -    (string * string) list)) list -> theory -> theory
     1.9 -  val assoc_consts_i: (xstring * typ option * (term mixfix list *
    1.10 -    (string * string) list)) list -> theory -> theory
    1.11 -  val assoc_types: (xstring * (typ mixfix list *
    1.12 -    (string * string) list)) list -> theory -> theory
    1.13 -  val get_assoc_code: theory -> string -> typ ->
    1.14 +  val assoc_const: string * (term mixfix list *
    1.15 +    (string * string) list) -> theory -> theory
    1.16 +  val assoc_const_i: (string * typ) * (term mixfix list *
    1.17 +    (string * string) list) -> theory -> theory
    1.18 +  val assoc_type: xstring * (typ mixfix list *
    1.19 +    (string * string) list) -> theory -> theory
    1.20 +  val get_assoc_code: theory -> string * typ ->
    1.21      (term mixfix list * (string * string) list) option
    1.22    val get_assoc_type: theory -> string ->
    1.23      (typ mixfix list * (string * string) list) option
    1.24 @@ -384,46 +384,34 @@
    1.25  
    1.26  (**** associate constants with target language code ****)
    1.27  
    1.28 -fun gen_assoc_consts prep_type xs thy = Library.foldl (fn (thy, (s, tyopt, syn)) =>
    1.29 +fun gen_assoc_const prep_const (raw_const, syn) thy =
    1.30    let
    1.31      val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
    1.32        CodegenData.get thy;
    1.33 -    val cname = Sign.intern_const thy s;
    1.34 +    val (cname, T) = prep_const thy raw_const;
    1.35    in
    1.36 -    (case Sign.const_type thy cname of
    1.37 -       SOME T =>
    1.38 -         let val T' = (case tyopt of
    1.39 -                NONE => T
    1.40 -              | SOME ty =>
    1.41 -                  let val U = prep_type thy ty
    1.42 -                  in if Type.raw_instance (U, T) then U
    1.43 -                    else error ("Illegal type constraint for constant " ^ cname)
    1.44 -                  end)
    1.45 -         in
    1.46 -           if num_args_of (fst syn) > length (binder_types T') then
    1.47 -             error ("More arguments than in corresponding type of " ^ s)
    1.48 -           else (case AList.lookup (op =) consts (cname, T') of
    1.49 -             NONE => CodegenData.put {codegens = codegens,
    1.50 -               tycodegens = tycodegens,
    1.51 -               consts = ((cname, T'), syn) :: consts,
    1.52 -               types = types, attrs = attrs, preprocs = preprocs,
    1.53 -               modules = modules, test_params = test_params} thy
    1.54 -           | SOME _ => error ("Constant " ^ cname ^ " already associated with code"))
    1.55 -         end
    1.56 -     | _ => error ("Not a constant: " ^ s))
    1.57 -  end) (thy, xs);
    1.58 +    if num_args_of (fst syn) > length (binder_types T) then
    1.59 +      error ("More arguments than in corresponding type of " ^ cname)
    1.60 +    else case AList.lookup (op =) consts (cname, T) of
    1.61 +      NONE => CodegenData.put {codegens = codegens,
    1.62 +        tycodegens = tycodegens,
    1.63 +        consts = ((cname, T), syn) :: consts,
    1.64 +        types = types, attrs = attrs, preprocs = preprocs,
    1.65 +        modules = modules, test_params = test_params} thy
    1.66 +    | SOME _ => error ("Constant " ^ cname ^ " already associated with code")
    1.67 +  end;
    1.68  
    1.69 -val assoc_consts_i = gen_assoc_consts (K I);
    1.70 -val assoc_consts = gen_assoc_consts Sign.read_typ;
    1.71 +val assoc_const_i = gen_assoc_const (K I);
    1.72 +val assoc_const = gen_assoc_const CodegenConsts.read_bare_const;
    1.73  
    1.74  
    1.75  (**** associate types with target language types ****)
    1.76  
    1.77 -fun assoc_types xs thy = Library.foldl (fn (thy, (s, syn)) =>
    1.78 +fun assoc_type (s, syn) thy =
    1.79    let
    1.80      val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
    1.81        CodegenData.get thy;
    1.82 -    val tc = Sign.intern_type thy s
    1.83 +    val tc = Sign.intern_type thy s;
    1.84    in
    1.85      case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
    1.86        SOME (Type.LogicalType i, _) =>
    1.87 @@ -436,7 +424,7 @@
    1.88              preprocs = preprocs, modules = modules, test_params = test_params} thy
    1.89          | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
    1.90      | _ => error ("Not a type constructor: " ^ s)
    1.91 -  end) (thy, xs);
    1.92 +  end;
    1.93  
    1.94  fun get_assoc_type thy = AList.lookup (op =) ((#types o CodegenData.get) thy);
    1.95  
    1.96 @@ -581,7 +569,7 @@
    1.97  fun is_instance thy T1 T2 =
    1.98    Sign.typ_instance thy (T1, Logic.legacy_varifyT T2);
    1.99  
   1.100 -fun get_assoc_code thy s T = Option.map snd (find_first (fn ((s', T'), _) =>
   1.101 +fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
   1.102    s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
   1.103  
   1.104  fun get_aux_code xs = map_filter (fn (m, code) =>
   1.105 @@ -734,7 +722,7 @@
   1.106          in SOME (gr'', mk_app brack (Pretty.str s) ps) end
   1.107  
   1.108      | Const (s, T) =>
   1.109 -      (case get_assoc_code thy s T of
   1.110 +      (case get_assoc_code thy (s, T) of
   1.111           SOME (ms, aux) =>
   1.112             let val i = num_args_of ms
   1.113             in if length ts < i then
   1.114 @@ -1111,7 +1099,7 @@
   1.115     | _ => error ("Malformed annotation: " ^ quote s));
   1.116  
   1.117  val _ = Context.add_setup
   1.118 -  (assoc_types [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
   1.119 +  (fold assoc_type [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
   1.120       [("term_of",
   1.121         "fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
   1.122        ("test",
   1.123 @@ -1139,19 +1127,19 @@
   1.124    OuterSyntax.command "types_code"
   1.125    "associate types with target language types" K.thy_decl
   1.126      (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
   1.127 -     (fn xs => Toplevel.theory (fn thy => assoc_types
   1.128 -       (map (fn ((name, mfx), aux) => (name, (parse_mixfix
   1.129 -         (Sign.read_typ thy) mfx, aux))) xs) thy)));
   1.130 +     (fn xs => Toplevel.theory (fn thy => fold (assoc_type o
   1.131 +       (fn ((name, mfx), aux) => (name, (parse_mixfix
   1.132 +         (Sign.read_typ thy) mfx, aux)))) xs thy)));
   1.133  
   1.134  val assoc_constP =
   1.135    OuterSyntax.command "consts_code"
   1.136    "associate constants with target language code" K.thy_decl
   1.137      (Scan.repeat1
   1.138 -       (P.xname -- (Scan.option (P.$$$ "::" |-- P.typ)) --|
   1.139 +       (P.term --|
   1.140          P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
   1.141 -     (fn xs => Toplevel.theory (fn thy => assoc_consts
   1.142 -       (map (fn (((name, optype), mfx), aux) =>
   1.143 -         (name, optype, (parse_mixfix (Sign.read_term thy) mfx, aux))) xs) thy)));
   1.144 +     (fn xs => Toplevel.theory (fn thy => fold (assoc_const o 
   1.145 +       (fn ((const, mfx), aux) =>
   1.146 +         (const, (parse_mixfix (Sign.read_term thy) mfx, aux)))) xs thy)));
   1.147  
   1.148  fun parse_code lib =
   1.149    Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) --