--- a/src/Pure/Tools/ROOT.ML Fri Jul 21 14:45:25 2006 +0200
+++ b/src/Pure/Tools/ROOT.ML Fri Jul 21 14:45:43 2006 +0200
@@ -12,9 +12,9 @@
use "../codegen.ML";
(*code generator, 2nd generation*)
+use "codegen_theorems.ML";
use "codegen_thingol.ML";
use "codegen_serializer.ML";
-use "codegen_theorems.ML";
use "codegen_simtype.ML";
use "codegen_package.ML";
--- a/src/Pure/Tools/class_package.ML Fri Jul 21 14:45:25 2006 +0200
+++ b/src/Pure/Tools/class_package.ML Fri Jul 21 14:45:43 2006 +0200
@@ -11,13 +11,14 @@
-> ProofContext.context * theory
val class_i: bstring -> class list -> Element.context_i list -> theory
-> ProofContext.context * theory
- val instance_arity: (xstring * string list) * string
+ (*FIXME: in _i variants, bstring should be bstring option*)
+ val instance_arity: ((xstring * string list) * string) list
-> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
-> theory -> Proof.state
- val instance_arity_i: (string * sort list) * sort
+ val instance_arity_i: ((string * sort list) * sort) list
-> bstring * attribute list -> ((bstring * attribute list) * term) list
-> theory -> Proof.state
- val prove_instance_arity: tactic -> (string * sort list) * sort
+ val prove_instance_arity: tactic -> ((string * sort list) * sort) list
-> bstring * attribute list -> ((bstring * attribute list) * term) list
-> theory -> theory
val instance_sort: string * string -> theory -> Proof.state
@@ -35,6 +36,9 @@
val the_superclasses: theory -> class -> class list
val the_consts_sign: theory -> class -> string * (string * typ) list
val the_inst_sign: theory -> class * string -> (string * sort) list * (string * typ) list
+ val assume_arities_of_sort: theory -> ((string * sort list) * sort) list -> typ * sort -> bool
+ val assume_arities_thy: theory -> ((string * sort list) * sort) list -> (theory -> 'a) -> 'a
+ (*'a must not keep any reference to theory*)
val print_classes: theory -> unit
val intro_classes_tac: thm list -> tactic
@@ -143,7 +147,7 @@
Sign.super_classes thy class
|> operational_sort_of thy
else
- error ("no class: " ^ class);
+ error ("no operational class: " ^ class);
fun the_ancestry thy classes =
let
@@ -170,12 +174,12 @@
val asorts = Sign.arity_sorts thy tyco [class];
val (clsvar, const_sign) = the_consts_sign thy class;
fun add_var sort used =
- let
- val [v] = Name.invent_list used "'a" 1
- in ((v, sort), v::used) end;
+ let val v = hd (Name.invents used "'a" 1);
+ in ((v, sort), Name.declare v used) end;
val (vsorts, _) =
- [clsvar]
- |> fold (fn (_, ty) => curry (gen_union (op =))
+ Name.context
+ |> Name.declare clsvar
+ |> fold (fn (_, ty) => fold Name.declare
((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) const_sign
|> fold_map add_var asorts;
val ty_inst = Type (tyco, map TFree vsorts);
@@ -228,6 +232,22 @@
certify_sort thy o Sign.read_sort thy;
+(* contexts with arity assumptions *)
+
+fun assume_arities_of_sort thy arities ty_sort =
+ let
+ val pp = Sign.pp thy;
+ val algebra = Sign.classes_of thy
+ |> fold (fn ((tyco, asorts), sort) =>
+ Sorts.add_arities pp (tyco, map (fn class => (class, asorts)) sort)) arities;
+ in Sorts.of_sort algebra ty_sort end;
+
+fun assume_arities_thy thy arities f =
+ let
+ val thy_read = (fold (fn ((tyco, asorts), sort)
+ => Sign.primitive_arity (tyco, asorts, sort)) arities o Theory.copy) thy
+ in f thy_read end;
+
(* tactics and methods *)
fun intro_classes_tac facts st =
@@ -253,16 +273,16 @@
local
-fun gen_instance mk_prop add_thm after_qed inst thy =
+fun gen_instance mk_prop add_thm after_qed insts thy =
thy
|> ProofContext.init
|> Proof.theorem_i PureThy.internalK NONE (after_qed oo (fold o fold) add_thm) NONE ("", [])
- (map (fn t => (("", []), [(t, [])])) (mk_prop thy inst));
+ ((map (fn t => (("", []), [(t, [])])) o maps (mk_prop thy)) insts);
in
val axclass_instance_sort =
- gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I;
+ gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I o single;
val axclass_instance_arity =
gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity;
val axclass_instance_arity_i =
@@ -316,18 +336,17 @@
((map (fst o fst) o Locale.parameters_of_expr thy) expr);
fun extract_tyvar_consts thy name_locale =
let
- fun extract_tyvar_name thy tys =
- fold (curry add_typ_tfrees) tys []
- |> (fn [(v, sort)] =>
- if Sign.subsort thy (supsort, sort)
- then v
- else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort)
- | [] => error ("no class type variable")
- | vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
+ fun extract_classvar ((c, ty), _) w =
+ (case add_typ_tfrees (ty, [])
+ of [(v, _)] => (case w
+ of SOME u => if u = v then w else error ("additonal type variable in type signature of constant " ^ quote c)
+ | NONE => SOME v)
+ | [] => error ("no type variable in type signature of constant " ^ quote c)
+ | _ => error ("more than one type variable in type signature of constant " ^ quote c));
val consts1 =
Locale.parameters_of thy name_locale
|> map (apsnd Syntax.unlocalize_mixfix)
- val v = (extract_tyvar_name thy o map (snd o fst)) consts1;
+ val SOME v = fold extract_classvar consts1 NONE;
val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1;
in (v, chop (length mapp_sup) consts2) end;
fun add_consts v raw_cs_sup raw_cs_this thy =
@@ -386,61 +405,79 @@
local
-fun gen_read_def thy prep_att read_def tyco ((raw_name, raw_atts), raw_t) =
+fun gen_read_def thy prep_att read_def ((raw_name, raw_atts), raw_t) =
let
val (_, t) = read_def thy (raw_name, raw_t);
val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t;
val atts = map (prep_att thy) raw_atts;
+ val insts = (Consts.typargs (Sign.consts_of thy) (c, ty))
+ fun flat_typ (Type (tyco, tys)) = tyco :: maps flat_typ tys
+ | flat_typ _ = [];
val name = case raw_name
- of "" => Thm.def_name (NameSpace.base c ^ "_" ^ NameSpace.base tyco)
+ of "" => let
+ val tycos = maps flat_typ insts;
+ val names = map NameSpace.base (c :: tycos);
+ in Thm.def_name (space_implode "_" names) end
| _ => raw_name;
- in (c, (Logic.varifyT ty, ((name, t), atts))) end;
+ in (c, (insts, ((name, t), atts))) end;
fun read_def thy = gen_read_def thy Attrib.attribute read_axm;
fun read_def_i thy = gen_read_def thy (K I) (K I);
-fun gen_instance_arity prep_arity prep_att read_def do_proof raw_arity (raw_name, raw_atts) raw_defs theory =
+fun gen_instance_arity prep_arity prep_att read_def do_proof raw_arities (raw_name, raw_atts) raw_defs theory =
let
- val pp = Sign.pp theory;
- val arity as (tyco, asorts, sort) = prep_arity theory ((fn ((x, y), z) => (x, y, z)) raw_arity);
- val ty_inst =
- Type (tyco, map2 (curry TVar o rpair 0) (Name.invent_list [] "'a" (length asorts)) asorts)
+ fun prep_arity' ((tyco, asorts), sort) = prep_arity theory (tyco, asorts, sort);
+ val arities = map prep_arity' raw_arities;
+ val arities_pair = map (fn (tyco, asorts, sort) => ((tyco, asorts), sort)) arities;
+ val _ = if null arities then error "at least one arity must be given" else ();
+ val _ = case (duplicates (op =) o map #1) arities
+ of [] => ()
+ | dupl_tycos => error ("type constructors occur more than once in arities: "
+ ^ (commas o map quote) dupl_tycos);
val name = case raw_name
- of "" => Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco)
+ of "" => Thm.def_name ((space_implode "_" o map NameSpace.base)
+ (maps (fn (tyco, _, sort) => sort @ [tyco])
+ (sort (fn ((tyco1, _, _), (tyco2, _, _)) => string_ord (tyco1, tyco2)) arities)))
| _ => raw_name;
val atts = map (prep_att theory) raw_atts;
- fun get_consts class =
+ fun already_defined (c, ty_inst) =
+ is_some (find_first (fn (_, { lhs = [ty_inst'], ...}) =>
+ Sign.typ_instance theory (ty_inst', ty_inst) orelse Sign.typ_instance theory (ty_inst, ty_inst'))
+ (Defs.specifications_of (Theory.defs_of theory) c));
+ fun get_consts_class tyco ty class =
let
val data = (fst o the_class_data theory) class;
- fun defined c =
- is_some (find_first (fn (_, { lhs = [ty], ...}) =>
- Sign.typ_instance theory (ty, ty_inst) orelse Sign.typ_instance theory (ty_inst, ty))
- (Defs.specifications_of (Theory.defs_of theory) c))
val subst_ty = map_type_tfree (fn (v, sort) =>
- if #var data = v then ty_inst else TVar ((v, 0), sort));
+ if #var data = v then ty else TVar ((v, 0), sort));
in
(map_filter (fn (_, (c, ty)) =>
- if defined c then NONE else SOME ((c, (class, subst_ty ty)))) o #consts) data
+ if already_defined (c, ty)
+ then NONE else SOME ((c, ((tyco, class), subst_ty ty)))) o #consts) data
end;
- val cs = (maps get_consts o the_ancestry theory) sort;
- fun read_defs defs cs =
+ fun get_consts_sort (tyco, asorts, sort) =
let
- val thy_read = (Sign.primitive_arity (tyco, asorts, sort) o Theory.copy) theory;
+ val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.give_names Name.context "'a" asorts))
+ in maps (get_consts_class tyco ty) (the_ancestry theory sort) end;
+ val cs = maps get_consts_sort arities;
+ fun read_defs defs cs thy_read =
+ let
fun read raw_def cs =
let
- val (c, (ty, def)) = read_def thy_read tyco raw_def;
- val (class, ty') = case AList.lookup (op =) cs c
+ val (c, (inst, ((_, t), atts))) = read_def thy_read raw_def;
+ val ty = Logic.varifyT (Consts.instance (Sign.consts_of thy_read) (c, inst));
+ val ((tyco, class), ty') = case AList.lookup (op =) cs c
of NONE => error ("superfluous definition for constant " ^ quote c)
| SOME class_ty => class_ty;
- val def' = case instantiations_of thy_read (ty, ty')
+ val name = Thm.def_name (NameSpace.base c ^ "_" ^ NameSpace.base tyco);
+ val t' = case instantiations_of thy_read (ty, ty')
of NONE => error ("superfluous definition for constant " ^
quote c ^ "::" ^ Sign.string_of_typ thy_read ty)
| SOME insttab =>
- (apfst o apsnd o map_term_types)
- (Logic.unvarifyT o Term.instantiateT insttab o Logic.varifyT) def
- in ((class, def'), AList.delete (op =) c cs) end;
+ map_term_types
+ (Logic.unvarifyT o Term.instantiateT insttab o Logic.varifyT) t
+ in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
in fold_map read defs cs end;
- val (defs, _) = read_defs raw_defs cs;
+ val (defs, _) = assume_arities_thy theory arities_pair (read_defs raw_defs cs);
fun get_remove_contraint c thy =
let
val ty = Sign.the_const_constraint thy c;
@@ -453,13 +490,12 @@
thy
|> PureThy.add_defs_i true (map snd defs)
|-> (fn thms => pair (map fst defs ~~ thms));
- fun register_def (class, thm) thy =
- thy
- |> add_inst_def ((class, tyco), thm);
fun note_all thy =
+ (*FIXME: should avoid binding duplicated names*)
let
- val thms = maps (fn class => Symtab.lookup_list
- ((snd o the_class_data thy) class) tyco) (the_ancestry thy sort);
+ val thms = maps (fn (tyco, _, sort) => maps (fn class =>
+ Symtab.lookup_list
+ ((snd o the_class_data thy) class) tyco) (the_ancestry thy sort)) arities;
in
thy
|> PureThy.note_thmss_i PureThy.internalK [((name, atts), [(thms, [])])]
@@ -473,16 +509,18 @@
|> fold_map get_remove_contraint (map fst cs)
||>> add_defs defs
|-> (fn (cs, def_thms) =>
- fold register_def def_thms
+ fold add_inst_def def_thms
#> note_all
- #> do_proof (after_qed cs) arity)
+ #> do_proof (after_qed cs) arities)
end;
fun instance_arity' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute
read_def do_proof;
fun instance_arity_i' do_proof = gen_instance_arity Sign.cert_arity (K I)
read_def_i do_proof;
-fun tactic_proof tac after_qed arity = AxClass.prove_arity arity tac #> after_qed;
+fun tactic_proof tac after_qed arities =
+ fold (fn arity => AxClass.prove_arity arity tac) arities
+ #> after_qed;
in
@@ -653,9 +691,9 @@
val instanceP =
OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) -- P.opt_keyword "open" >> wrap_add_instance_sort
- || P.opt_thm_name ":" -- (parse_inst -- Scan.repeat (P.opt_thm_name ":" -- P.prop))
- >> (fn (("", []), (((tyco, asorts), sort), [])) => axclass_instance_arity I (tyco, asorts, sort)
- | (natts, (inst, defs)) => instance_arity inst natts defs)
+ || P.opt_thm_name ":" -- (P.and_list1 parse_inst -- Scan.repeat (P.opt_thm_name ":" -- P.prop))
+ >> (fn (("", []), ([((tyco, asorts), sort)], [])) => axclass_instance_arity I [(tyco, asorts, sort)]
+ | (natts, (arities, defs)) => instance_arity arities natts defs)
) >> (Toplevel.print oo Toplevel.theory_to_proof));
val _ = OuterSyntax.add_parsers [classP, instanceP];
--- a/src/Pure/Tools/codegen_package.ML Fri Jul 21 14:45:25 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML Fri Jul 21 14:45:43 2006 +0200
@@ -20,9 +20,9 @@
val add_pretty_list: string -> string -> string * (int * string)
-> theory -> theory;
val add_alias: string * string -> theory -> theory;
- val set_get_all_datatype_cons : (theory -> (string * string) list)
+ val set_get_all_datatype_cons: (theory -> (string * string) list)
-> theory -> theory;
- val set_int_tyco: string -> theory -> theory;
+ val purge_code: theory -> theory;
type appgen;
val add_appconst: xstring * appgen -> theory -> theory;
@@ -244,7 +244,7 @@
|> Symtab.update (
#ml CodegenSerializer.serializers
|> apsnd (fn seri => seri
- (nsp_dtcon, nsp_class, K false)
+ (nsp_dtcon, nsp_class)
[[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]]
)
)
@@ -373,6 +373,8 @@
val print_code = CodegenData.print;
+val purge_code = map_codegen_data (fn (_, appgens, target_data, logic_data) =>
+ (empty_module, appgens, target_data, logic_data));
(* advanced name handling *)
@@ -469,9 +471,7 @@
fun gen_add_appconst prep_const (raw_c, appgen) thy =
let
val c = prep_const thy raw_c;
- val _ = writeln c;
val i = (length o fst o strip_type o Sign.the_const_type thy) c
- val _ = (writeln o string_of_int) i;
in map_codegen_data
(fn (modl, appgens, target_data, logic_data) =>
(modl,
@@ -508,18 +508,6 @@
end
| NONE => NONE;
-fun set_int_tyco tyco thy =
- (serializers := (
- ! serializers
- |> Symtab.update (
- #ml CodegenSerializer.serializers
- |> apsnd (fn seri => seri
- (nsp_dtcon, nsp_class, fn tyco' => tyco' = idf_of_name thy nsp_tyco tyco)
- [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst, nsp_instmem]]
- )
- )
- ); thy);
-
(* definition and expression generators *)
@@ -674,16 +662,13 @@
(ClassPackage.sortlookup thy ([supclass], arity_typ));
fun gen_membr (m, ty) trns =
trns
- |> tap (fn _ => writeln ("(1) " ^ m))
|> mk_fun thy tabs (m, ty)
- |> tap (fn _ => writeln "(2)")
|-> (fn NONE => error ("could not derive definition for member "
^ quote m ^ " :: " ^ Sign.string_of_typ thy ty)
| SOME (funn, sorts) => fold_map (fn (sort, sort_ctxt) =>
fold_map (exprgen_classlookup thy tabs)
(ClassPackage.sortlookup thy (sort, TFree sort_ctxt)))
(print sorts ~~ print operational_arity)
- #> tap (fn _ => writeln "(3)")
#-> (fn lss =>
pair (idf_of_name thy nsp_mem m, ((idf_of_name thy nsp_instmem m, funn), lss))));
in
@@ -771,7 +756,7 @@
|-> (fn ty => pair (IVar v))
| exprgen_term thy tabs (Abs (raw_v, ty, raw_t)) trns =
let
- val (v, t) = Term.variant_abs (CodegenThingol.proper_name raw_v, ty, raw_t);
+ val (v, t) = Term.variant_abs (Name.alphanum raw_v, ty, raw_t);
in
trns
|> exprgen_type thy tabs ty
@@ -807,7 +792,7 @@
if length ts < i then
let
val tys = Library.take (i - length ts, ((fst o strip_type) ty));
- val vs = CodegenThingol.give_names [f] tys;
+ val vs = Name.give_names (Name.declare f Name.context) "a" tys;
in
trns
|> fold_map (exprgen_type thy tabs) tys
@@ -856,8 +841,6 @@
fun appgen_case dest_case_expr thy tabs (app as (c_ty, ts)) trns =
let
- val _ = (writeln o fst) c_ty;
- val _ = (writeln o Sign.string_of_typ thy o snd) c_ty;
val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
fun clausegen (dt, bt) trns =
trns
@@ -1038,7 +1021,7 @@
fun codegen_term t thy =
thy
- |> expand_module (SOME (Symtab.keys (#target_data (CodegenData.get thy)))) NONE exprgen_term t;
+ |> expand_module (SOME [] (*(Symtab.keys (#target_data (CodegenData.get thy)))*)) NONE exprgen_term t;
val is_dtcon = has_nsp nsp_dtcon;
@@ -1058,7 +1041,7 @@
val target_data =
((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy;
in
- CodegenSerializer.ml_fun_datatype (nsp_dtcon, nsp_class, K false)
+ CodegenSerializer.ml_fun_datatype (nsp_dtcon, nsp_class)
((Option.map fst oo Symtab.lookup o #syntax_tyco) target_data,
(Option.map fst oo Symtab.lookup o #syntax_const) target_data)
resolv
@@ -1317,10 +1300,8 @@
);
val purgeP =
- OuterSyntax.command purgeK "purge all defintions for constant" K.thy_decl (
- Scan.repeat1 P.term
- >> (Toplevel.theory o purge_consts)
- );
+ OuterSyntax.command purgeK "purge all incrementally generated code" K.thy_decl
+ (Scan.succeed (Toplevel.theory purge_code));
val aliasP =
OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl (
--- a/src/Pure/Tools/codegen_serializer.ML Fri Jul 21 14:45:25 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML Fri Jul 21 14:45:43 2006 +0200
@@ -22,11 +22,11 @@
('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
val pretty_list: string -> string -> int * string -> CodegenThingol.iterm pretty_syntax;
val serializers: {
- ml: string * (string * string * (string -> bool) -> serializer),
+ ml: string * (string * string -> serializer),
haskell: string * (string * string list -> serializer)
};
val mk_flat_ml_resolver: string list -> string -> string;
- val ml_fun_datatype: string * string * (string -> bool)
+ val ml_fun_datatype: string * string
-> ((string -> CodegenThingol.itype pretty_syntax option)
* (string -> CodegenThingol.iterm pretty_syntax option))
-> (string -> string)
@@ -335,9 +335,9 @@
type src = string;
val ord = string_ord;
fun mk reserved_ml (name, 0) =
- (CodegenThingol.proper_name o NameSpace.base) name
+ (Name.alphanum o NameSpace.base) name
| mk reserved_ml (name, i) =
- (CodegenThingol.proper_name o NameSpace.base) name ^ replicate_string i "'";
+ (Name.alphanum o NameSpace.base) name ^ replicate_string i "'";
fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml;
fun maybe_unique _ _ = NONE;
fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
@@ -770,17 +770,16 @@
| defs => error ("illegal mutual dependencies: " ^ (commas o map fst) defs)
end;
-fun ml_annotators (nsp_dtcon, nsp_class, is_int_tyco) =
+fun ml_annotators (nsp_dtcon, nsp_class) =
let
fun needs_type tyco =
- CodegenThingol.has_nsp tyco nsp_class
- orelse is_int_tyco tyco;
+ CodegenThingol.has_nsp tyco nsp_class;
fun is_cons c = CodegenThingol.has_nsp c nsp_dtcon;
in (is_cons, needs_type) end;
in
-fun ml_from_thingol target (nsp_dtcon, nsp_class, is_int_tyco) nspgrp =
+fun ml_from_thingol target (nsp_dtcon, nsp_class) nspgrp =
let
fun ml_from_module resolv _ ((_, name), ps) =
Pretty.chunks ([
@@ -791,7 +790,7 @@
str "",
str ("end; (* struct " ^ name ^ " *)")
]);
- val (is_cons, needs_type) = ml_annotators (nsp_dtcon, nsp_class, is_int_tyco);
+ val (is_cons, needs_type) = ml_annotators (nsp_dtcon, nsp_class);
val serializer = abstract_serializer (target, nspgrp)
"ROOT" (ml_from_defs (is_cons, needs_type), ml_from_module,
abstract_validator reserved_ml, snd);
@@ -828,8 +827,8 @@
|-> (fn _ => I)
in NameMangler.get reserved_ml mangler end;
-fun ml_fun_datatype (nsp_dtcon, nsp_class, is_int_tyco) =
- ml_fun_datatyp (ml_annotators (nsp_dtcon, nsp_class, is_int_tyco));
+fun ml_fun_datatype (nsp_dtcon, nsp_class) =
+ ml_fun_datatyp (ml_annotators (nsp_dtcon, nsp_class));
end; (* local *)
@@ -893,7 +892,7 @@
hs_from_expr BR e2
])
| hs_from_expr fxy (IVar v) =
- (str o String.implode o nth_map 0 Char.toLower o String.explode) v
+ str v
| hs_from_expr fxy (e as _ `|-> _) =
let
val (es, e) = CodegenThingol.unfold_abs e
--- a/src/Pure/Tools/codegen_theorems.ML Fri Jul 21 14:45:25 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML Fri Jul 21 14:45:43 2006 +0200
@@ -223,8 +223,8 @@
(maxidx + 1, v :: set,
(ctyp_of thy ty, ctyp_of thy (TVar ((v', maxidx), sort))) :: acc)
end;
- val lower_name = (prefix "'" o implode o map (Char.toString o Char.toLower o the o Char.fromString)
- o explode o CodegenThingol.proper_name o unprefix "'");
+ val lower_name = implode o map (Char.toString o Char.toLower o the o Char.fromString)
+ o explode o Name.alphanum;
fun tvars_of thm = (fold_types o fold_atyps)
(fn TVar (v_i as (v, i), sort) => cons (v_i, (lower_name v, sort))
| _ => I) (prop_of thm) [];
@@ -242,8 +242,8 @@
(maxidx + 1, v :: set,
(cterm_of thy t, cterm_of thy (Var ((v', maxidx), ty))) :: acc)
end;
- val lower_name = (implode o map (Char.toString o Char.toLower o the o Char.fromString)
- o explode o CodegenThingol.proper_name);
+ val lower_name = implode o map (Char.toString o Char.toLower o the o Char.fromString)
+ o explode o Name.alphanum;
fun vars_of thm = fold_aterms
(fn Var (v_i as (v, i), ty) => cons (v_i, (lower_name v, ty))
| _ => I) (prop_of thm) [];
--- a/src/Pure/Tools/codegen_thingol.ML Fri Jul 21 14:45:25 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML Fri Jul 21 14:45:43 2006 +0200
@@ -32,9 +32,9 @@
| INum of IntInf.int (*non-negative!*) * iterm
| IChar of string (*length one!*) * iterm
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
- (* ((discrimendum expression (de), discrimendum type (dty)),
+ (*((discrimendum expression (de), discrimendum type (dty)),
[(selector expression (se), body expression (be))]),
- native expression (e0)) *)
+ native expression (e0))*)
end;
signature CODEGEN_THINGOL =
@@ -59,9 +59,6 @@
val vars_distinct: iterm list -> bool;
val map_pure: (iterm -> 'a) -> iterm -> 'a;
val eta_expand: (string * (iclasslookup list list * itype)) * iterm list -> int -> iterm;
- val proper_name: string -> string;
- val invent_name: string list -> string;
- val give_names: string list -> 'a list -> (string * 'a) list;
val resolve_tycos: (string -> string) -> itype * iterm list -> itype * iterm list;
val resolve_consts: (string -> string) -> iterm -> iterm;
@@ -132,27 +129,6 @@
| SOME (x1, x2) =>
let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
-fun proper_name s =
- let
- fun replace_invalid c =
- if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
- andalso not (NameSpace.separator = c)
- then c
- else "_";
- fun contract "_" (acc as "_" :: _) = acc
- | contract c acc = c :: acc;
- fun contract_underscores s =
- implode (fold_rev contract (explode s) []);
- fun ensure_char s =
- if forall (Char.isDigit o the o Char.fromString) (explode s)
- then prefix "x" s
- else s
- in
- s
- |> translate_string replace_invalid
- |> contract_underscores
- |> ensure_char
- end;
(** language core - types, pattern, expressions **)
@@ -387,17 +363,12 @@
x |> distinct de |> fold (fn (be, se) => distinct be #> distinct se) bses;
in is_some (fold distinct es (SOME [])) end;
-fun invent_name used = hd (Name.invent_list used "a" 1);
-
-fun give_names used xs =
- Name.invent_list used "a" (length xs) ~~ xs;
-
fun eta_expand (c as (_, (_, ty)), es) k =
let
val j = length es;
val l = k - j;
val tys = (curry Library.take l o curry Library.drop j o fst o unfold_fun) ty;
- val vs_tys = give_names (fold add_varnames es []) tys;
+ val vs_tys = Name.give_names (fold Name.declare (fold add_varnames es []) Name.context) "a" tys;
in vs_tys `|--> IConst c `$$ es @ map (fn (v, _) => IVar v) vs_tys end;