src/Tools/code/code_package.ML
changeset 24423 ae9cd0e92423
parent 24381 560e8ecdf633
child 24436 b694324cd2be
     1.1 --- a/src/Tools/code/code_package.ML	Fri Aug 24 14:14:18 2007 +0200
     1.2 +++ b/src/Tools/code/code_package.ML	Fri Aug 24 14:14:20 2007 +0200
     1.3 @@ -45,35 +45,25 @@
     1.4    -> CodeFuncgr.T
     1.5    -> (string * typ) * term list -> CodeThingol.transact -> iterm * CodeThingol.transact;
     1.6  
     1.7 -type appgens = (int * (appgen * stamp)) Symtab.table;
     1.8 -val merge_appgens : appgens * appgens -> appgens =
     1.9 -  Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
    1.10 -    bounds1 = bounds2 andalso stamp1 = stamp2);
    1.11 -
    1.12 -structure Consttab = CodeUnit.Consttab;
    1.13 -type abstypes = typ Symtab.table * CodeUnit.const Consttab.table;
    1.14 -fun merge_abstypes ((typs1, consts1) : abstypes, (typs2, consts2) : abstypes) =
    1.15 -  (Symtab.merge (Type.eq_type Vartab.empty) (typs1, typs2),
    1.16 -    Consttab.merge CodeUnit.eq_const (consts1, consts2));
    1.17 -
    1.18 -structure Translation = TheoryDataFun
    1.19 +structure Appgens = TheoryDataFun
    1.20  (
    1.21 -  type T = appgens * abstypes;
    1.22 -  val empty = (Symtab.empty, (Symtab.empty, Consttab.empty));
    1.23 +  type T = (int * (appgen * stamp)) Symtab.table;
    1.24 +  val empty = Symtab.empty;
    1.25    val copy = I;
    1.26    val extend = I;
    1.27 -  fun merge _ ((appgens1, abstypes1), (appgens2, abstypes2)) =
    1.28 -    (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
    1.29 +  fun merge _ = Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
    1.30 +    bounds1 = bounds2 andalso stamp1 = stamp2);
    1.31  );
    1.32  
    1.33  fun code_depgr thy [] = CodeFuncgr.make thy []
    1.34    | code_depgr thy consts =
    1.35        let
    1.36          val gr = CodeFuncgr.make thy consts;
    1.37 -        val select = CodeFuncgr.Constgraph.all_succs gr consts;
    1.38 +        val select = Graph.all_succs gr consts;
    1.39        in
    1.40 -        CodeFuncgr.Constgraph.subgraph
    1.41 -          (member CodeUnit.eq_const select) gr
    1.42 +        gr
    1.43 +        |> Graph.subgraph (member (op =) select) 
    1.44 +        |> Graph.map_nodes ((apsnd o map) (Conv.fconv_rule (Class.overload thy)))
    1.45        end;
    1.46  
    1.47  fun code_thms thy =
    1.48 @@ -89,7 +79,7 @@
    1.49        in { name = name, ID = name, dir = "", unfold = true,
    1.50          path = "", parents = nameparents }
    1.51        end;
    1.52 -    val prgr = CodeFuncgr.Constgraph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
    1.53 +    val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
    1.54    in Present.display_graph prgr end;
    1.55  
    1.56  structure Program = CodeDataFun
    1.57 @@ -105,7 +95,7 @@
    1.58              map_filter (CodeName.const_rev thy) (Graph.keys code);
    1.59            val dels = (Graph.all_preds code
    1.60                o map (CodeName.const thy)
    1.61 -              o filter (member CodeUnit.eq_const cs_exisiting)
    1.62 +              o filter (member (op =) cs_exisiting)
    1.63              ) cs;
    1.64          in Graph.del_nodes dels code end;
    1.65  );
    1.66 @@ -113,10 +103,6 @@
    1.67  
    1.68  (* translation kernel *)
    1.69  
    1.70 -fun get_abstype thy (tyco, tys) = case Symtab.lookup ((fst o snd o Translation.get) thy) tyco
    1.71 - of SOME ty => SOME ((map_atyps (fn TFree (n, _) => nth tys (the (Int.fromString n)))) ty)
    1.72 -  | NONE => NONE;
    1.73 -
    1.74  val value_name = "Isabelle_Eval.EVAL.EVAL";
    1.75  
    1.76  fun ensure_def thy = CodeThingol.ensure_def
    1.77 @@ -128,7 +114,7 @@
    1.78      val (v, cs) = AxClass.params_of_class thy class;
    1.79      val class' = CodeName.class thy class;
    1.80      val classrels' = map (curry (CodeName.classrel thy) class) superclasses;
    1.81 -    val classops' = map (CodeName.const thy o CodeUnit.const_of_cexpr thy) cs;
    1.82 +    val classops' = map (CodeName.const thy o fst) cs;
    1.83      val defgen_class =
    1.84        fold_map (ensure_def_class thy algbr funcgr) superclasses
    1.85        ##>> (fold_map (exprgen_typ thy algbr funcgr) o map snd) cs
    1.86 @@ -152,9 +138,7 @@
    1.87              fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
    1.88              ##>> fold_map (fn (c, tys) =>
    1.89                fold_map (exprgen_typ thy algbr funcgr) tys
    1.90 -              #>> (fn tys' =>
    1.91 -                ((CodeName.const thy o CodeUnit.const_of_cexpr thy)
    1.92 -                  (c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
    1.93 +              #>> (fn tys' => (CodeName.const thy c, tys'))) cos
    1.94              #>> (fn (vs, cos) => CodeThingol.Datatype (vs, cos))
    1.95            end;
    1.96          val tyco' = CodeName.tyco thy tyco;
    1.97 @@ -171,15 +155,10 @@
    1.98        |> exprgen_tyvar_sort thy algbr funcgr vs
    1.99        |>> (fn (v, sort) => ITyVar v)
   1.100    | exprgen_typ thy algbr funcgr (Type (tyco, tys)) trns =
   1.101 -      case get_abstype thy (tyco, tys)
   1.102 -       of SOME ty =>
   1.103 -            trns
   1.104 -            |> exprgen_typ thy algbr funcgr ty
   1.105 -        | NONE =>
   1.106 -            trns
   1.107 -            |> ensure_def_tyco thy algbr funcgr tyco
   1.108 -            ||>> fold_map (exprgen_typ thy algbr funcgr) tys
   1.109 -            |>> (fn (tyco, tys) => tyco `%% tys);
   1.110 +      trns
   1.111 +      |> ensure_def_tyco thy algbr funcgr tyco
   1.112 +      ||>> fold_map (exprgen_typ thy algbr funcgr) tys
   1.113 +      |>> (fn (tyco, tys) => tyco `%% tys);
   1.114  
   1.115  exception CONSTRAIN of (string * typ) * typ;
   1.116  val timing = ref false;
   1.117 @@ -216,10 +195,8 @@
   1.118    end
   1.119  and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
   1.120    let
   1.121 -    val c' = CodeUnit.const_of_cexpr thy (c, ty_ctxt)
   1.122 -    val idf = CodeName.const thy c';
   1.123 -    val ty_decl = Consts.the_declaration consts idf;
   1.124 -    val (tys, tys_decl) = pairself (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
   1.125 +    val ty_decl = Consts.the_declaration consts c;
   1.126 +    val (tys, tys_decl) = pairself (curry (Consts.typargs consts) c) (ty_ctxt, ty_decl);
   1.127      val sorts = map (snd o dest_TVar) tys_decl;
   1.128    in
   1.129      fold_map (exprgen_dicts thy algbr funcgr) (tys ~~ sorts)
   1.130 @@ -237,10 +214,11 @@
   1.131        ||>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
   1.132        |>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
   1.133              (superclass, (classrel, (inst, dss))));
   1.134 -    fun gen_classop_def (classop as (c, ty)) trns =
   1.135 +    fun gen_classop_def (c, ty) trns =
   1.136        trns
   1.137 -      |> ensure_def_const thy algbr funcgr (CodeUnit.const_of_cexpr thy classop)
   1.138 -      ||>> exprgen_term thy algbr funcgr (Const (c, map_type_tfree (K arity_typ) ty));
   1.139 +      |> ensure_def_const thy algbr funcgr c
   1.140 +      ||>> exprgen_term thy algbr funcgr
   1.141 +            (Const (Class.inst_const thy (c, tyco), map_type_tfree (K arity_typ) ty));
   1.142      fun defgen_inst trns =
   1.143        trns
   1.144        |> ensure_def_class thy algbr funcgr class
   1.145 @@ -256,13 +234,13 @@
   1.146      |> ensure_def thy defgen_inst ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
   1.147      |> pair inst
   1.148    end
   1.149 -and ensure_def_const thy (algbr as (_, consts)) funcgr (const as (c, opt_tyco)) =
   1.150 +and ensure_def_const thy (algbr as (_, consts)) funcgr c =
   1.151    let
   1.152 -    val c' = CodeName.const thy const;
   1.153 +    val c' = CodeName.const thy c;
   1.154      fun defgen_datatypecons trns =
   1.155        trns 
   1.156        |> ensure_def_tyco thy algbr funcgr
   1.157 -          ((the o Code.get_datatype_of_constr thy) const)
   1.158 +          ((the o Code.get_datatype_of_constr thy) c)
   1.159        |>> (fn _ => CodeThingol.Bot);
   1.160      fun defgen_classop trns =
   1.161        trns 
   1.162 @@ -271,15 +249,14 @@
   1.163        |>> (fn _ => CodeThingol.Bot);
   1.164      fun defgen_fun trns =
   1.165        let
   1.166 -        val const' = perhaps (Consttab.lookup ((snd o snd o Translation.get) thy)) const;
   1.167 -        val raw_thms = CodeFuncgr.funcs funcgr const';
   1.168 -        val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) const';
   1.169 +        val raw_thms = CodeFuncgr.funcs funcgr c;
   1.170 +        val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
   1.171          val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
   1.172            then raw_thms
   1.173            else map (CodeUnit.expand_eta 1) raw_thms;
   1.174 -        val timeap = if !timing then Output.timeap_msg ("time for " ^ c')
   1.175 +        val timeap = if !timing then Output.timeap_msg ("time for " ^ c)
   1.176            else I;
   1.177 -        val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
   1.178 +        val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
   1.179          val dest_eqthm =
   1.180            apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;
   1.181          fun exprgen_eq (args, rhs) =
   1.182 @@ -292,14 +269,13 @@
   1.183          ||>> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
   1.184          |>> (fn ((vs, ty), eqs) => CodeThingol.Fun ((vs, ty), eqs))
   1.185        end;
   1.186 -    val defgen = if (is_some o Code.get_datatype_of_constr thy) const
   1.187 +    val defgen = if (is_some o Code.get_datatype_of_constr thy) c
   1.188        then defgen_datatypecons
   1.189 -      else if is_some opt_tyco
   1.190 -        orelse (not o is_some o AxClass.class_of_param thy) c
   1.191 -      then defgen_fun
   1.192 -      else defgen_classop
   1.193 +      else if (is_some o AxClass.class_of_param thy) c
   1.194 +      then defgen_classop
   1.195 +      else defgen_fun
   1.196    in
   1.197 -    ensure_def thy defgen ("generating constant " ^ CodeUnit.string_of_const thy const) c'
   1.198 +    ensure_def thy defgen ("generating constant " ^ CodeUnit.string_of_const thy c) c'
   1.199      #> pair c'
   1.200    end
   1.201  and exprgen_term thy algbr funcgr (Const (c, ty)) trns =
   1.202 @@ -330,14 +306,14 @@
   1.203              |>> (fn (t, ts) => t `$$ ts)
   1.204  and appgen_default thy algbr funcgr ((c, ty), ts) trns =
   1.205    trns
   1.206 -  |> ensure_def_const thy algbr funcgr (CodeUnit.const_of_cexpr thy (c, ty))
   1.207 +  |> ensure_def_const thy algbr funcgr c
   1.208    ||>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
   1.209    ||>> exprgen_typ thy algbr funcgr ((snd o Term.strip_type) ty)
   1.210    ||>> exprgen_dict_parms thy algbr funcgr (c, ty)
   1.211    ||>> fold_map (exprgen_term thy algbr funcgr) ts
   1.212    |>> (fn ((((c, tys), ty), iss), ts) => IConst (c, (iss, tys)) `$$ ts)
   1.213  and select_appgen thy algbr funcgr ((c, ty), ts) trns =
   1.214 -  case Symtab.lookup (fst (Translation.get thy)) c
   1.215 +  case Symtab.lookup (Appgens.get thy) c
   1.216     of SOME (i, (appgen, _)) =>
   1.217          if length ts < i then
   1.218            let
   1.219 @@ -396,7 +372,9 @@
   1.220    let
   1.221      val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
   1.222      fun clause_gen (dt, bt) =
   1.223 -      exprgen_term thy algbr funcgr dt
   1.224 +      exprgen_term thy algbr funcgr
   1.225 +        (map_aterms (fn Const (c_ty as (c, ty)) => Const
   1.226 +          (Class.unoverload_const thy c_ty, ty) | t => t) dt)
   1.227        ##>> exprgen_term thy algbr funcgr bt;
   1.228    in
   1.229      exprgen_term thy algbr funcgr st
   1.230 @@ -429,107 +407,25 @@
   1.231      val i = (length o fst o strip_type o Sign.the_const_type thy) c;
   1.232      val _ = Program.change thy (K CodeThingol.empty_code);
   1.233    in
   1.234 -    (Translation.map o apfst)
   1.235 -      (Symtab.update (c, (i, (appgen, stamp ())))) thy
   1.236 +    Appgens.map (Symtab.update (c, (i, (appgen, stamp ())))) thy
   1.237    end;
   1.238  
   1.239  
   1.240 -
   1.241 -(** abstype and constsubst interface **)
   1.242 -
   1.243 -local
   1.244 -
   1.245 -fun add_consts thy f (c1, c2 as (c, opt_tyco)) =
   1.246 -  let
   1.247 -    val _ = if
   1.248 -        is_some (AxClass.class_of_param thy c) andalso is_none opt_tyco
   1.249 -        orelse is_some (Code.get_datatype_of_constr thy c2)
   1.250 -      then error ("Not a function: " ^ CodeUnit.string_of_const thy c2)
   1.251 -      else ();
   1.252 -    val funcgr = CodeFuncgr.make thy [c1, c2];
   1.253 -    val ty1 = (f o CodeFuncgr.typ funcgr) c1;
   1.254 -    val ty2 = CodeFuncgr.typ funcgr c2;
   1.255 -    val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
   1.256 -      error ("Incompatiable type signatures of " ^ CodeUnit.string_of_const thy c1
   1.257 -        ^ " and " ^ CodeUnit.string_of_const thy c2 ^ ":\n"
   1.258 -        ^ CodeUnit.string_of_typ thy ty1 ^ "\n" ^ CodeUnit.string_of_typ thy ty2);
   1.259 -  in Consttab.update (c1, c2) end;
   1.260 -
   1.261 -fun gen_abstyp prep_const prep_typ (raw_abstyp, raw_substtyp) raw_absconsts thy =
   1.262 -  let
   1.263 -    val abstyp = Type.no_tvars (prep_typ thy raw_abstyp);
   1.264 -    val substtyp = Type.no_tvars (prep_typ thy raw_substtyp);
   1.265 -    val absconsts = (map o pairself) (prep_const thy) raw_absconsts;
   1.266 -    val Type (abstyco, tys) = abstyp handle BIND => error ("Bad type: " ^ Sign.string_of_typ thy abstyp);
   1.267 -    val typarms = map (fst o dest_TFree) tys handle MATCH => error ("Bad type: " ^ Sign.string_of_typ thy abstyp);
   1.268 -    fun mk_index v = 
   1.269 -      let
   1.270 -        val k = find_index (fn w => v = w) typarms;
   1.271 -      in if k = ~1
   1.272 -        then error ("Free type variable: " ^ quote v)
   1.273 -        else TFree (string_of_int k, [])
   1.274 -      end;
   1.275 -    val typpat = map_atyps (fn TFree (v, _) => mk_index v) substtyp;
   1.276 -    fun apply_typpat (Type (tyco, tys)) =
   1.277 -          let
   1.278 -            val tys' = map apply_typpat tys;
   1.279 -          in if tyco = abstyco then
   1.280 -            (map_atyps (fn TFree (n, _) => nth tys' (the (Int.fromString n)))) typpat
   1.281 -          else
   1.282 -            Type (tyco, tys')
   1.283 -          end
   1.284 -      | apply_typpat ty = ty;
   1.285 -    val _ = Program.change thy (K CodeThingol.empty_code);
   1.286 -  in
   1.287 -    thy
   1.288 -    |> (Translation.map o apsnd) (fn (abstypes, abscs) =>
   1.289 -          (abstypes
   1.290 -          |> Symtab.update (abstyco, typpat),
   1.291 -          abscs
   1.292 -          |> fold (add_consts thy apply_typpat) absconsts)
   1.293 -       )
   1.294 -  end;
   1.295 -
   1.296 -fun gen_constsubst prep_const raw_constsubsts thy =
   1.297 -  let
   1.298 -    val constsubsts = (map o pairself) (prep_const thy) raw_constsubsts;
   1.299 -    val _ = Program.change thy (K CodeThingol.empty_code);
   1.300 -  in
   1.301 -    thy
   1.302 -    |> (Translation.map o apsnd o apsnd) (fold (add_consts thy I) constsubsts)
   1.303 -  end;
   1.304 -
   1.305 -in
   1.306 -
   1.307 -val abstyp = gen_abstyp (K I) Sign.certify_typ;
   1.308 -val abstyp_e = gen_abstyp CodeUnit.read_const Sign.read_typ;
   1.309 -
   1.310 -val constsubst = gen_constsubst (K I);
   1.311 -val constsubst_e = gen_constsubst CodeUnit.read_const;
   1.312 -
   1.313 -end; (*local*)
   1.314 -
   1.315 -
   1.316  (** code generation interfaces **)
   1.317  
   1.318  (* generic generation combinators *)
   1.319  
   1.320  fun generate thy funcgr gen it =
   1.321    let
   1.322 -    (*FIXME*)
   1.323 -    val _ = CodeFuncgr.intervene thy funcgr;
   1.324 -    val cs = map_filter (Consttab.lookup ((snd o snd o Translation.get) thy))
   1.325 -      (CodeFuncgr.all funcgr);
   1.326 -    val CodeFuncgr' = CodeFuncgr.make thy cs;
   1.327      val naming = NameSpace.qualified_names NameSpace.default_naming;
   1.328      val consttab = Consts.empty
   1.329        |> fold (fn c => Consts.declare naming
   1.330 -           ((CodeName.const thy c, CodeFuncgr.typ CodeFuncgr' c), true))
   1.331 -           (CodeFuncgr.all CodeFuncgr');
   1.332 +           ((c, CodeFuncgr.typ funcgr c), true))
   1.333 +           (CodeFuncgr.all funcgr);
   1.334      val algbr = (Code.operational_algebra thy, consttab);
   1.335    in   
   1.336      Program.change_yield thy
   1.337 -      (CodeThingol.start_transact (gen thy algbr CodeFuncgr' it))
   1.338 +      (CodeThingol.start_transact (gen thy algbr funcgr it))
   1.339      |> fst
   1.340    end;
   1.341  
   1.342 @@ -630,8 +526,7 @@
   1.343  
   1.344  val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK];
   1.345  
   1.346 -val (codeK, code_abstypeK, code_axiomsK, code_thmsK, code_depsK) =
   1.347 -  ("export_code", "code_abstype", "code_axioms", "code_thms", "code_deps");
   1.348 +val (codeK, code_thmsK, code_depsK) = ("export_code", "code_thms", "code_deps");
   1.349  
   1.350  in
   1.351  
   1.352 @@ -644,19 +539,6 @@
   1.353     of SOME f => (writeln "Now generating code..."; f thy)
   1.354      | NONE => error ("Bad directive " ^ quote cmd);
   1.355  
   1.356 -val code_abstypeP =
   1.357 -  OuterSyntax.command code_abstypeK "axiomatic abstypes for code generation" K.thy_decl (
   1.358 -    (P.typ -- P.typ -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
   1.359 -        (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)) [])
   1.360 -    >> (Toplevel.theory o uncurry abstyp_e)
   1.361 -  );
   1.362 -
   1.363 -val code_axiomsP =
   1.364 -  OuterSyntax.command code_axiomsK "axiomatic constant equalities for code generation" K.thy_decl (
   1.365 -    Scan.repeat1 (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)
   1.366 -    >> (Toplevel.theory o constsubst_e)
   1.367 -  );
   1.368 -
   1.369  val code_thmsP =
   1.370    OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag
   1.371      (Scan.repeat P.term
   1.372 @@ -669,7 +551,7 @@
   1.373        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
   1.374          o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
   1.375  
   1.376 -val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_axiomsP, code_thmsP, code_depsP];
   1.377 +val _ = OuterSyntax.add_parsers [codeP, code_thmsP, code_depsP];
   1.378  
   1.379  end; (* local *)
   1.380