some clarifications
authorhaftmann
Wed Dec 27 19:10:07 2006 +0100 (2006-12-27 ago)
changeset 2191668c848f636bb
parent 21915 4e63c55f4cb4
child 21917 12b8fde1f9c0
some clarifications
src/Pure/Tools/codegen_package.ML
     1.1 --- a/src/Pure/Tools/codegen_package.ML	Wed Dec 27 19:10:06 2006 +0100
     1.2 +++ b/src/Pure/Tools/codegen_package.ML	Wed Dec 27 19:10:07 2006 +0100
     1.3 @@ -200,8 +200,8 @@
     1.4        | mk_dict (Contxt ((v, sort), (classes, k))) trns =
     1.5            trns
     1.6            |> fold_map (ensure_def_class thy algbr funcgr strct) classes
     1.7 -          |-> (fn classes => pair (Context (classes, (unprefix "'" v,
     1.8 -                if length sort = 1 then ~1 else k))))
     1.9 +          |-> (fn classes => pair (Context ((classes, k), (unprefix "'" v,
    1.10 +                length sort))))
    1.11    in
    1.12      trns
    1.13      |> fold_map mk_dict insts
    1.14 @@ -483,6 +483,28 @@
    1.15  
    1.16  (** abstype and constsubst interface **)
    1.17  
    1.18 +local
    1.19 +
    1.20 +fun add_consts thy f (c1, c2 as (c, tys)) =
    1.21 +  let
    1.22 +    val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
    1.23 +    val _ = case tys
    1.24 +     of [TVar _] => if is_some (AxClass.class_of_param thy c)
    1.25 +          then error ("not a function: " ^ CodegenConsts.string_of_const thy c2)
    1.26 +          else ()
    1.27 +      | _ => ();
    1.28 +    val _ = if is_some (CodegenData.get_datatype_of_constr thy c2)
    1.29 +      then error ("not a function: " ^ CodegenConsts.string_of_const thy c2)
    1.30 +      else ();
    1.31 +    val funcgr = CodegenFuncgr.make thy [c1, c2];
    1.32 +    val ty1 = (f o CodegenFuncgr.typ funcgr) c1;
    1.33 +    val ty2 = CodegenFuncgr.typ funcgr c2;
    1.34 +    val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
    1.35 +      error ("Incompatiable type signatures of " ^ CodegenConsts.string_of_const thy c1
    1.36 +        ^ " and " ^ CodegenConsts.string_of_const thy c2 ^ ":\n"
    1.37 +        ^ string_of_typ ty1 ^ "\n" ^ string_of_typ ty2);
    1.38 +  in Consttab.update (c1, c2) end;
    1.39 +
    1.40  fun gen_abstyp prep_const prep_typ (raw_abstyp, raw_substtyp) raw_absconsts thy =
    1.41    let
    1.42      val abstyp = Type.no_tvars (prep_typ thy raw_abstyp);
    1.43 @@ -507,20 +529,6 @@
    1.44              Type (tyco, tys')
    1.45            end
    1.46        | apply_typpat ty = ty;
    1.47 -    val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
    1.48 -    fun add_consts (c1, c2) =
    1.49 -      let
    1.50 -        val _ = if CodegenNames.has_nsp CodegenNames.nsp_fun (CodegenNames.const thy c2)
    1.51 -          then ()
    1.52 -          else error ("not a function: " ^ CodegenConsts.string_of_const thy c2);
    1.53 -        val funcgr = CodegenFuncgr.make thy [c1, c2];
    1.54 -        val ty1 = (apply_typpat o CodegenFuncgr.typ funcgr) c1;
    1.55 -        val ty2 = CodegenFuncgr.typ funcgr c2;
    1.56 -        val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
    1.57 -          error ("Incompatiable type signatures of " ^ CodegenConsts.string_of_const thy c1
    1.58 -            ^ " and " ^ CodegenConsts.string_of_const thy c2 ^ ":\n"
    1.59 -            ^ string_of_typ ty1 ^ "\n" ^ string_of_typ ty2);
    1.60 -      in Consttab.update (c1, c2) end;
    1.61      val _ = Code.change thy (K CodegenThingol.empty_code);
    1.62    in
    1.63      thy
    1.64 @@ -528,39 +536,28 @@
    1.65            (abstypes
    1.66            |> Symtab.update (abstyco, typpat),
    1.67            abscs
    1.68 -          |> fold add_consts absconsts)
    1.69 +          |> fold (add_consts thy apply_typpat) absconsts)
    1.70         )
    1.71    end;
    1.72  
    1.73  fun gen_constsubst prep_const raw_constsubsts thy =
    1.74    let
    1.75      val constsubsts = (map o pairself) (prep_const thy) raw_constsubsts;
    1.76 -    val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
    1.77 -    fun add_consts (c1, c2) =
    1.78 -      let
    1.79 -        val _ = if CodegenNames.has_nsp CodegenNames.nsp_fun (CodegenNames.const thy c2)
    1.80 -          then ()
    1.81 -          else error ("not a function: " ^ CodegenConsts.string_of_const thy c2);
    1.82 -        val funcgr = CodegenFuncgr.make thy [c1, c2];
    1.83 -        val ty1 = CodegenFuncgr.typ funcgr c1;
    1.84 -        val ty2 = CodegenFuncgr.typ funcgr c2;
    1.85 -        val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
    1.86 -          error ("Incompatiable type signatures of " ^ CodegenConsts.string_of_const thy c1
    1.87 -            ^ " and " ^ CodegenConsts.string_of_const thy c2 ^ ":\n"
    1.88 -            ^ string_of_typ ty1 ^ "\n" ^ string_of_typ ty2);
    1.89 -      in Consttab.update (c1, c2) end;
    1.90      val _ = Code.change thy (K CodegenThingol.empty_code);
    1.91    in
    1.92      thy
    1.93 -    |> (CodegenPackageData.map o apsnd o apsnd) (fold add_consts constsubsts)
    1.94 +    |> (CodegenPackageData.map o apsnd o apsnd) (fold (add_consts thy I) constsubsts)
    1.95    end;
    1.96  
    1.97 +in
    1.98 +
    1.99  val abstyp = gen_abstyp CodegenConsts.norm Sign.certify_typ;
   1.100  val abstyp_e = gen_abstyp CodegenConsts.read_const (fn thy => Sign.read_typ (thy, K NONE));
   1.101  
   1.102  val constsubst = gen_constsubst CodegenConsts.norm;
   1.103  val constsubst_e = gen_constsubst CodegenConsts.read_const;
   1.104  
   1.105 +end; (*local*)
   1.106  
   1.107  
   1.108  (** code generation interfaces **)
   1.109 @@ -599,7 +596,7 @@
   1.110        error ("Term" ^ Sign.string_of_term thy t ^ "is polymorhpic"))
   1.111        t;
   1.112      val t' = codegen_term thy t;
   1.113 -  in CodegenSerializer.eval_term thy (ref_spec, t') (Code.get thy) end;
   1.114 +  in CodegenSerializer.eval_term thy (Code.get thy) (ref_spec, t') end;
   1.115  
   1.116  
   1.117  (* constant specifications with wildcards *)
   1.118 @@ -669,7 +666,7 @@
   1.119  in
   1.120  
   1.121  val code_bareP = (
   1.122 -    P.!!! (Scan.repeat P.term
   1.123 +    (Scan.repeat P.term
   1.124      -- Scan.repeat (P.$$$ "(" |--
   1.125          P.name -- P.arguments
   1.126          --| P.$$$ ")"))
   1.127 @@ -678,11 +675,11 @@
   1.128  
   1.129  val codeP =
   1.130    OuterSyntax.improper_command codeK "generate and serialize executable code for constants"
   1.131 -    K.diag (code_bareP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
   1.132 +    K.diag (P.!!! code_bareP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
   1.133  
   1.134  fun codegen_command thy cmd =
   1.135 -  case Scan.read OuterLex.stopper code_bareP ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
   1.136 -   of SOME f => f thy
   1.137 +  case Scan.read OuterLex.stopper (P.!!! code_bareP) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
   1.138 +   of SOME f => (writeln "Now generating code..."; f thy)
   1.139      | NONE => error ("bad directive " ^ quote cmd);
   1.140  
   1.141  val code_abstypeP =