src/Pure/Tools/codegen_package.ML
changeset 19202 0b9eb4b0ad98
parent 19177 68c6824d8bb6
child 19213 ee83040c3c84
     1.1 --- a/src/Pure/Tools/codegen_package.ML	Tue Mar 07 04:06:02 2006 +0100
     1.2 +++ b/src/Pure/Tools/codegen_package.ML	Tue Mar 07 14:09:48 2006 +0100
     1.3 @@ -138,7 +138,7 @@
     1.4    andalso Sign.typ_instance thy (ty2, ty1);
     1.5  
     1.6  fun is_overloaded thy c = case Defs.specifications_of (Theory.defs_of thy) c
     1.7 - of [] => false
     1.8 + of [] => true
     1.9    | [(ty, _)] => not (eq_typ thy (ty, Sign.the_const_type thy c))
    1.10    | _ => true;
    1.11  
    1.12 @@ -161,10 +161,17 @@
    1.13    fun mk thy ((c, ty), i) =
    1.14      let
    1.15        val c' = idf_of_name thy nsp_overl c;
    1.16 -      val prefix = case (AList.lookup (eq_typ thy)
    1.17 -          (Defs.specifications_of (Theory.defs_of thy) c)) ty
    1.18 -       of SOME thyname => NameSpace.append thyname nsp_overl
    1.19 -        | NONE => NameSpace.drop_base c';
    1.20 +      val prefix = 
    1.21 +        case (AList.lookup (eq_typ thy)
    1.22 +            (Defs.specifications_of (Theory.defs_of thy) c)) ty
    1.23 +         of SOME thyname => NameSpace.append thyname nsp_overl
    1.24 +          | NONE => if c = "op ="
    1.25 +              then
    1.26 +                NameSpace.append
    1.27 +                  (((fn s => Codegen.thyname_of_type s thy) o fst o dest_Type o hd o fst o strip_type) ty)
    1.28 +                  nsp_overl
    1.29 +              else
    1.30 +                NameSpace.drop_base c';
    1.31        val c'' = NameSpace.append prefix (NameSpace.base c');
    1.32        fun mangle (Type (tyco, tys)) =
    1.33              (NameSpace.base o alias_get thy) tyco :: Library.flat (List.mapPartial mangle tys) |> SOME
    1.34 @@ -399,13 +406,13 @@
    1.35        (c, ty) =
    1.36    let
    1.37      fun get_overloaded (c, ty) =
    1.38 -      case Symtab.lookup overltab1 c
    1.39 +      (case Symtab.lookup overltab1 c
    1.40         of SOME tys =>
    1.41              (case find_first (curry (Sign.typ_instance thy) ty) tys
    1.42               of SOME ty' => ConstNameMangler.get thy overltab2
    1.43                    (c, ty') |> SOME
    1.44                | _ => NONE)
    1.45 -        | _ => NONE
    1.46 +        | _ => NONE)
    1.47      fun get_datatypecons (c, ty) =
    1.48        case (snd o strip_type) ty
    1.49         of Type (tyco, _) =>
    1.50 @@ -851,12 +858,12 @@
    1.51  and appgen_default thy tabs ((c, ty), ts) trns =
    1.52    trns
    1.53    |> ensure_def_const thy tabs (c, ty)
    1.54 +  ||>> exprsgen_type thy tabs [ty]
    1.55    ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
    1.56           (ClassPackage.extract_classlookup thy (c, ty))
    1.57 -  ||>> exprsgen_type thy tabs [ty]
    1.58    ||>> fold_map (exprgen_term thy tabs) ts
    1.59 -  |-> (fn (((c, ls), [ty]), es) =>
    1.60 -         pair (IConst ((c, ty), ls) `$$ es))
    1.61 +  |-> (fn (((c, [ty]), ls), es) =>
    1.62 +         pair (IConst (c, (ls, ty)) `$$ es))
    1.63  and appgen thy tabs ((f, ty), ts) trns =
    1.64    case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f
    1.65     of SOME ((imin, imax), (ag, _)) =>
    1.66 @@ -899,43 +906,48 @@
    1.67  
    1.68  (* parametrized generators, for instantiation in HOL *)
    1.69  
    1.70 -fun appgen_let strip_abs thy tabs (app as ((c, ty), [dt, ct])) trns =
    1.71 -  let
    1.72 -    val ([st], bt) = strip_abs 1 ct;
    1.73 -    val dtyp = (hd o fst o strip_type) ty
    1.74 -  in
    1.75 -    trns
    1.76 -    |> exprgen_term thy tabs dt
    1.77 -    ||>> exprgen_type thy tabs dtyp
    1.78 -    ||>> exprgen_term thy tabs st
    1.79 -    ||>> exprgen_term thy tabs bt
    1.80 -    ||>> appgen_default thy tabs app
    1.81 -    |-> (fn ((((de, dty), se), be), e0) => pair (ICase (((de, dty), [(se, be)]), e0)))
    1.82 -  end;
    1.83 -
    1.84 -fun appgen_split strip_abs thy tabs (app as (c as (_, ty), [t])) trns =
    1.85 +fun appgen_split strip_abs thy tabs (app as (c, [t])) trns =
    1.86    case strip_abs 1 (Const c $ t)
    1.87 -   of ([vt], tb) =>
    1.88 +   of ([vt], bt) =>
    1.89          trns
    1.90          |> exprgen_term thy tabs vt
    1.91 -        ||>> exprgen_type thy tabs (((fn [_, ty] => ty) o fst o strip_type) ty)
    1.92 -        ||>> exprgen_term thy tabs tb
    1.93 +        ||>> exprgen_type thy tabs (type_of vt)
    1.94 +        ||>> exprgen_term thy tabs bt
    1.95          ||>> appgen_default thy tabs app
    1.96          |-> (fn (((ve, vty), be), e0) => pair (IAbs (((ve, vty), be), e0)))
    1.97      | _ =>
    1.98          trns
    1.99          |> appgen_default thy tabs app;
   1.100  
   1.101 +fun appgen_let strip_abs thy tabs (app as ((c, ty), [dt, ct])) trns =
   1.102 +  case strip_abs 1 ct
   1.103 +   of ([st], bt) =>
   1.104 +        trns
   1.105 +        |> exprgen_term thy tabs dt
   1.106 +        ||>> exprgen_type thy tabs (type_of dt)
   1.107 +        ||>> exprgen_term thy tabs st
   1.108 +        ||>> exprgen_term thy tabs bt
   1.109 +        ||>> appgen_default thy tabs app
   1.110 +        |-> (fn ((((de, dty), se), be), e0) => pair (ICase (((de, dty), [(se, be)]), e0)))
   1.111 +    | _ =>
   1.112 +        trns
   1.113 +        |> appgen_default thy tabs app;
   1.114 +
   1.115  fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_,
   1.116    Type (_, [_, ty as Type (tyco, [])])), [bin]) trns =
   1.117 -    if tyco = tyco_int then
   1.118 +    if tyco = tyco_nat then
   1.119        trns
   1.120 -      |> exprgen_type thy tabs ty
   1.121 -      |-> (fn ty => pair (CodegenThingol.IConst (((IntInf.toString o bin_to_int thy) bin, ty), [])))
   1.122 -    else if tyco = tyco_nat then
   1.123 -      trns
   1.124 -      |> exprgen_term thy tabs (mk_int_to_nat bin)
   1.125 -    else error ("invalid type constructor for numeral: " ^ quote tyco);
   1.126 +      |> exprgen_term thy tabs (mk_int_to_nat bin) (*should be a preprocessor's work*)
   1.127 +    else
   1.128 +      let
   1.129 +        val i = bin_to_int thy bin;
   1.130 +        val _ = if i < 0 then error ("negative numeral: " ^ IntInf.toString i) else ();
   1.131 +          (*should be a preprocessor's work*)
   1.132 +      in
   1.133 +        trns
   1.134 +        |> exprgen_type thy tabs ty
   1.135 +        |-> (fn ty => pair (CodegenThingol.INum ((i, ty), ())))
   1.136 +      end;
   1.137  
   1.138  fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
   1.139    let
   1.140 @@ -951,25 +963,7 @@
   1.141      ||>> exprsgen_type thy tabs [ty_def]
   1.142      ||>> exprgen_term thy tabs tf
   1.143      ||>> exprgen_term thy tabs tx
   1.144 -    |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst ((idf, ty), ls) `$ tf `$ tx))
   1.145 -  end;
   1.146 -
   1.147 -
   1.148 -fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
   1.149 -  let
   1.150 -    val ty_def = (op ---> o apfst tl o strip_type o Sign.the_const_type thy) c;
   1.151 -    val ty' = (op ---> o apfst tl o strip_type) ty;
   1.152 -    val idf = idf_of_const thy tabs (c, ty);
   1.153 -  in
   1.154 -    trns
   1.155 -    |> ensure_def [("wfrec", (K o succeed) Undef)] ("generating wfrec") idf
   1.156 -    |> exprgen_type thy tabs ty'
   1.157 -    ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
   1.158 -           (ClassPackage.extract_classlookup thy (c, ty))
   1.159 -    ||>> exprsgen_type thy tabs [ty_def]
   1.160 -    ||>> exprgen_term thy tabs tf
   1.161 -    ||>> exprgen_term thy tabs tx
   1.162 -    |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst ((idf, ty), ls) `$ tf `$ tx))
   1.163 +    |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx))
   1.164    end;
   1.165  
   1.166  fun eqextr_eq f fals thy tabs ("op =", ty) =