# HG changeset patch # User haftmann # Date 1153485943 -7200 # Node ID 0a8ca32f6e64a6bf38a3db7e3e2a671ddbf295dd # Parent c057b3618963e46c72f235a40fed4bb704303cef class package and codegen refinements diff -r c057b3618963 -r 0a8ca32f6e64 src/Pure/Tools/ROOT.ML --- 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"; diff -r c057b3618963 -r 0a8ca32f6e64 src/Pure/Tools/class_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.$$$ "\\" || 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]; diff -r c057b3618963 -r 0a8ca32f6e64 src/Pure/Tools/codegen_package.ML --- 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 ( diff -r c057b3618963 -r 0a8ca32f6e64 src/Pure/Tools/codegen_serializer.ML --- 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 diff -r c057b3618963 -r 0a8ca32f6e64 src/Pure/Tools/codegen_theorems.ML --- 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) []; diff -r c057b3618963 -r 0a8ca32f6e64 src/Pure/Tools/codegen_thingol.ML --- 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;