--- a/src/Tools/code/code_name.ML Tue Oct 02 07:59:54 2007 +0200
+++ b/src/Tools/code/code_name.ML Tue Oct 02 07:59:55 2007 +0200
@@ -99,19 +99,19 @@
(* identifier categories *)
-val idf_class = "class";
-val idf_classrel = "clsrel"
-val idf_tyco = "tyco";
-val idf_instance = "inst";
-val idf_const = "const";
+val suffix_class = "class";
+val suffix_classrel = "clsrel"
+val suffix_tyco = "tyco";
+val suffix_instance = "inst";
+val suffix_const = "const";
fun string_of_classrel (class, superclass) = class ^ " < " ^ superclass;
fun string_of_instance (class, tyco) = tyco ^ " :: " ^ class;
-fun add_idf nsp name =
+fun add_suffix nsp name =
NameSpace.append name nsp;
-fun dest_idf nsp name =
+fun dest_suffix nsp name =
if NameSpace.base name = nsp
then SOME (NameSpace.qualifier name)
else NONE;
@@ -119,11 +119,11 @@
local
val name_mapping = [
- (idf_class, "class"),
- (idf_classrel, "subclass relation"),
- (idf_tyco, "type constructor"),
- (idf_instance, "instance"),
- (idf_const, "constant")
+ (suffix_class, "class"),
+ (suffix_classrel, "subclass relation"),
+ (suffix_tyco, "type constructor"),
+ (suffix_instance, "instance"),
+ (suffix_const, "constant")
]
in
@@ -150,11 +150,6 @@
thyname_of thy (fn thy => member (op =) (Sign.all_classes thy))
(fn class => "thyname_of_class: no such class: " ^ quote class);
-fun thyname_of_classrel thy =
- thyname_of thy (fn thy => fn (class1, class2) => Sign.subsort thy ([class1], [class2]))
- (fn (class1, class2) => "thyname_of_classrel: no such subclass relation: "
- ^ (quote o string_of_classrel) (class1, class2));
-
fun thyname_of_tyco thy =
thyname_of thy Sign.declared_tyname
(fn tyco => "thyname_of_tyco: no such type constructor: " ^ quote tyco);
@@ -205,7 +200,7 @@
fun class_policy thy = default_policy thy NameSpace.base thyname_of_class;
fun classrel_policy thy = default_policy thy (fn (class1, class2) =>
- NameSpace.base class2 ^ "_" ^ NameSpace.base class1) thyname_of_classrel;
+ NameSpace.base class2 ^ "_" ^ NameSpace.base class1) (fn thy => thyname_of_class thy o fst);
(*order fits nicely with composed projections*)
fun tyco_policy thy = default_policy thy NameSpace.base thyname_of_tyco;
fun instance_policy thy = default_policy thy (fn (class, tyco) =>
@@ -368,54 +363,54 @@
fun class thy =
get thy #class Symtab.lookup map_class Symtab.update class_policy
- #> add_idf idf_class;
+ #> add_suffix suffix_class;
fun classrel thy =
get thy #classrel StringPairTab.lookup map_classrel StringPairTab.update classrel_policy
- #> add_idf idf_classrel;
+ #> add_suffix suffix_classrel;
fun tyco thy =
get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy
- #> add_idf idf_tyco;
+ #> add_suffix suffix_tyco;
fun instance thy =
get thy #instance StringPairTab.lookup map_instance StringPairTab.update instance_policy
- #> add_idf idf_instance;
+ #> add_suffix suffix_instance;
fun const thy =
get_const thy
- #> add_idf idf_const;
+ #> add_suffix suffix_const;
fun class_rev thy =
- dest_idf idf_class
+ dest_suffix suffix_class
#> Option.map (rev thy #class);
fun classrel_rev thy =
- dest_idf idf_classrel
+ dest_suffix suffix_classrel
#> Option.map (rev thy #classrel);
fun tyco_rev thy =
- dest_idf idf_tyco
+ dest_suffix suffix_tyco
#> Option.map (rev thy #tyco);
fun instance_rev thy =
- dest_idf idf_instance
+ dest_suffix suffix_instance
#> Option.map (rev thy #instance);
fun const_rev thy =
- dest_idf idf_const
+ dest_suffix suffix_const
#> Option.map (rev_const thy);
local
val f_mapping = [
- (idf_class, class_rev),
- (idf_classrel, Option.map string_of_classrel oo classrel_rev),
- (idf_tyco, tyco_rev),
- (idf_instance, Option.map string_of_instance oo instance_rev),
- (idf_const, fn thy => Option.map (CodeUnit.string_of_const thy) o const_rev thy)
+ (suffix_class, class_rev),
+ (suffix_classrel, Option.map string_of_classrel oo classrel_rev),
+ (suffix_tyco, tyco_rev),
+ (suffix_instance, Option.map string_of_instance oo instance_rev),
+ (suffix_const, fn thy => Option.map (CodeUnit.string_of_const thy) o const_rev thy)
];
in
-fun labelled_name thy idf =
+fun labelled_name thy suffix_name =
let
- val category = category_of idf;
- val name = NameSpace.qualifier idf;
- val f = (the o AList.lookup (op =) f_mapping o NameSpace.base) idf
- in case f thy idf
+ val category = category_of suffix_name;
+ val name = NameSpace.qualifier suffix_name;
+ val suffix = NameSpace.base suffix_name
+ in case (the o AList.lookup (op =) f_mapping) suffix thy suffix_name
of SOME thing => category ^ " " ^ quote thing
| NONE => error ("Unknown name: " ^ quote name)
end;
--- a/src/Tools/code/code_package.ML Tue Oct 02 07:59:54 2007 +0200
+++ b/src/Tools/code/code_package.ML Tue Oct 02 07:59:55 2007 +0200
@@ -106,25 +106,34 @@
fun ensure_def thy = CodeThingol.ensure_def
(fn s => if s = value_name then "<term>" else CodeName.labelled_name thy s);
+exception CONSTRAIN of (string * typ) * typ;
+
fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr class =
let
val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
val (v, cs) = AxClass.params_of_class thy class;
val class' = CodeName.class thy class;
- val classrels' = map (curry (CodeName.classrel thy) class) superclasses;
- val classops' = map (CodeName.const thy o fst) cs;
val defgen_class =
- fold_map (ensure_def_class thy algbr funcgr) superclasses
- ##>> (fold_map (exprgen_typ thy algbr funcgr) o map snd) cs
- #>> (fn (superclasses, classoptyps) =>
- CodeThingol.Class (superclasses ~~ classrels', (unprefix "'" v, classops' ~~ classoptyps)))
+ fold_map (fn superclass => ensure_def_class thy algbr funcgr superclass
+ ##>> ensure_def_classrel thy algbr funcgr (class, superclass)) superclasses
+ ##>> fold_map (fn (c, ty) => ensure_def_const thy algbr funcgr c
+ ##>> exprgen_typ thy algbr funcgr ty) cs
+ #>> (fn info => CodeThingol.Class (unprefix "'" v, info))
in
- ensure_def thy defgen_class ("generating class " ^ quote class) class'
+ ensure_def thy defgen_class class'
#> pair class'
end
and ensure_def_classrel thy algbr funcgr (subclass, superclass) =
- ensure_def_class thy algbr funcgr subclass
- #>> (fn _ => CodeName.classrel thy (subclass, superclass))
+ let
+ val classrel' = CodeName.classrel thy (subclass, superclass);
+ val defgen_classrel =
+ ensure_def_class thy algbr funcgr subclass
+ ##>> ensure_def_class thy algbr funcgr superclass
+ #>> CodeThingol.Classrel;
+ in
+ ensure_def thy defgen_classrel classrel'
+ #> pair classrel'
+ end
and ensure_def_tyco thy algbr funcgr "fun" =
pair "fun"
| ensure_def_tyco thy algbr funcgr tyco =
@@ -135,13 +144,13 @@
in
fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
##>> fold_map (fn (c, tys) =>
- fold_map (exprgen_typ thy algbr funcgr) tys
- #>> (fn tys' => (CodeName.const thy c, tys'))) cos
- #>> (fn (vs, cos) => CodeThingol.Datatype (vs, cos))
+ ensure_def_const thy algbr funcgr c
+ ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
+ #>> CodeThingol.Datatype
end;
val tyco' = CodeName.tyco thy tyco;
in
- ensure_def thy defgen_datatype ("generating type constructor " ^ quote tyco) tyco'
+ ensure_def thy defgen_datatype tyco'
#> pair tyco'
end
and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr (v, sort) =
@@ -153,11 +162,8 @@
| exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
ensure_def_tyco thy algbr funcgr tyco
##>> fold_map (exprgen_typ thy algbr funcgr) tys
- #>> (fn (tyco, tys) => tyco `%% tys);
-
-exception CONSTRAIN of (string * typ) * typ;
-
-fun exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
+ #>> (fn (tyco, tys) => tyco `%% tys)
+and exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
let
val pp = Sign.pp thy;
datatype typarg =
@@ -241,7 +247,7 @@
CodeThingol.Classinst ((class, (tyco, arity)), (superarities, classops)));
val inst = CodeName.instance thy (class, tyco);
in
- ensure_def thy defgen_inst ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
+ ensure_def thy defgen_inst inst
#> pair inst
end
and ensure_def_const thy (algbr as (_, consts)) funcgr c =
@@ -249,10 +255,10 @@
val c' = CodeName.const thy c;
fun defgen_datatypecons tyco =
ensure_def_tyco thy algbr funcgr tyco
- #>> K CodeThingol.Bot;
+ #>> K (CodeThingol.Datatypecons c');
fun defgen_classop class =
ensure_def_class thy algbr funcgr class
- #>> K CodeThingol.Bot;
+ #>> K (CodeThingol.Classop c');
fun defgen_fun trns =
let
val raw_thms = CodeFuncgr.funcs funcgr c;
@@ -274,7 +280,7 @@
of SOME class => defgen_classop class
| NONE => defgen_fun)
in
- ensure_def thy defgen ("generating constant " ^ CodeUnit.string_of_const thy c) c'
+ ensure_def thy defgen c'
#> pair c'
end
and exprgen_term thy algbr funcgr (Const (c, ty)) =
@@ -448,7 +454,7 @@
val code'' = CodeThingol.project_code false [] (SOME deps) code';
in ((code'', ((vs, ty), t), deps), (dep, code')) end;
in
- ensure_def thy defgen_eval "evaluation" value_name
+ ensure_def thy defgen_eval value_name
#> result
end;
fun h funcgr ct =
--- a/src/Tools/code/code_target.ML Tue Oct 02 07:59:54 2007 +0200
+++ b/src/Tools/code/code_target.ML Tue Oct 02 07:59:55 2007 +0200
@@ -297,7 +297,7 @@
datatype ml_def =
MLFuns of (string * (typscheme * (iterm list * iterm) list)) list
| MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
- | MLClass of string * ((class * string) list * (vname * (string * itype) list))
+ | MLClass of string * (vname * ((class * string) list * (string * itype) list))
| MLClassinst of string * ((class * (string * (vname * sort) list))
* ((class * (string * (string * dict list list))) list
* (string * const) list));
@@ -491,7 +491,7 @@
);
val (ps, p) = split_last (pr_data "datatype" data :: map (pr_data "and") datas');
in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
- | pr_def (MLClass (class, (superclasses, (v, classops)))) =
+ | pr_def (MLClass (class, (v, (superclasses, classops)))) =
let
val w = first_upper v ^ "_";
fun pr_superclass_field (class, classrel) =
@@ -788,7 +788,7 @@
);
val (ps, p) = split_last (pr_data "type" data :: map (pr_data "and") datas');
in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
- | pr_def (MLClass (class, (superclasses, (v, classops)))) =
+ | pr_def (MLClass (class, (v, (superclasses, classops)))) =
let
val w = "_" ^ first_upper v;
fun pr_superclass_field (class, classrel) =
@@ -948,7 +948,10 @@
val (modls, _) = (split_list o map dest_name) names;
val modl' = (the_single o distinct (op =) o map name_modl) modls
handle Empty =>
- error ("Illegal mutual dependencies: " ^ commas (map labelled_name names));
+ error ("Different namespace prefixes for mutual dependencies:\n"
+ ^ commas (map labelled_name names)
+ ^ "\n"
+ ^ commas (map (NameSpace.qualifier o NameSpace.qualifier) names));
val modl_explode = NameSpace.explode modl';
fun add_dep name name'' =
let
@@ -1232,7 +1235,7 @@
@ (if deriving_show name then [str "deriving (Read, Show)"] else [])
)
end
- | pr_def (name, CodeThingol.Class (superclasss, (v, classops))) =
+ | pr_def (name, CodeThingol.Class (v, (superclasses, classops))) =
let
val tyvars = CodeName.intro_vars [v] init_syms;
fun pr_classop (classop, ty) =
@@ -1245,7 +1248,7 @@
Pretty.block_enclose (
Pretty.block [
str "class ",
- pr_typparms tyvars [(v, map fst superclasss)],
+ pr_typparms tyvars [(v, map fst superclasses)],
str (deresolv_here name ^ " " ^ CodeName.lookup_var tyvars v),
str " where {"
],
--- a/src/Tools/code/code_thingol.ML Tue Oct 02 07:59:54 2007 +0200
+++ b/src/Tools/code/code_thingol.ML Tue Oct 02 07:59:55 2007 +0200
@@ -63,7 +63,7 @@
| Fun of typscheme * ((iterm list * iterm) * thm) list
| Datatype of (vname * sort) list * (string * itype list) list
| Datatypecons of string
- | Class of (class * string) list * (vname * (string * itype) list)
+ | Class of vname * ((class * string) list * (string * itype) list)
| Classop of class
| Classrel of class * class
| Classinst of (class * (string * (vname * sort) list))
@@ -81,7 +81,7 @@
val add_eval_def: string (*bind name*) * (iterm * itype) -> code -> code;
val ensure_def: (string -> string) -> (transact -> def * transact) -> string
- -> string -> transact -> transact;
+ -> transact -> transact;
val start_transact: (transact -> 'a * transact) -> code -> 'a * code;
end;
@@ -250,7 +250,7 @@
| Fun of typscheme * ((iterm list * iterm) * thm) list
| Datatype of (vname * sort) list * (string * itype list) list
| Datatypecons of string
- | Class of (class * string) list * (vname * (string * itype) list)
+ | Class of vname * ((class * string) list * (string * itype) list)
| Classop of class
| Classrel of class * class
| Classinst of (class * (string * (vname * sort) list))
@@ -276,8 +276,9 @@
| SOME Bot => Graph.map_node name (K def) code
| SOME _ => error ("Tried to overwrite definition " ^ quote name));
-fun add_dep (dep as (name1, name2)) =
- if name1 = name2 then I else Graph.add_edge dep;
+fun add_dep (NONE, _) = I
+ | add_dep (SOME name1, name2) =
+ if name1 = name2 then I else Graph.add_edge (name1, name2);
val merge_code : code * code -> code = Graph.merge (K true);
@@ -309,100 +310,21 @@
of Datatypecons _ => true
| _ => false;
-fun check_samemodule names =
- fold (fn name =>
- let
- val module_name = (NameSpace.qualifier o NameSpace.qualifier) name
- in
- fn NONE => SOME module_name
- | SOME module_name' => if module_name = module_name' then SOME module_name
- else error ("Inconsistent name prefix for simultanous names: " ^ commas_quote names)
- end
- ) names NONE;
-
-fun check_funeqs eqs =
- (fold (fn ((pats, _), _) =>
- let
- val l = length pats
- in
- fn NONE => SOME l
- | SOME l' => if l = l' then SOME l
- else error "Function definition with different number of arguments"
- end
- ) eqs NONE; eqs);
-
-fun check_prep_def code Bot =
- Bot
- | check_prep_def code (Fun (d, eqs)) =
- Fun (d, check_funeqs eqs)
- | check_prep_def code (d as Datatype _) =
- d
- | check_prep_def code (Datatypecons dtco) =
- error "Attempted to add bare term constructor"
- | check_prep_def code (d as Class _) =
- d
- | check_prep_def code (Classop _) =
- error "Attempted to add bare class operation"
- | check_prep_def code (Classrel _) =
- error "Attempted to add bare class relation"
- | check_prep_def code (d as Classinst ((class, (tyco, arity)), (_, inst_classops))) =
- let
- val Class (_, (_, classops)) = Graph.get_node code class;
- val _ = if length inst_classops > length classops
- then error "Too many class operations given"
- else ();
- fun check_classop (f, _) =
- if AList.defined (op =) (map fst inst_classops) f
- then () else error ("Missing definition for class operation " ^ quote f);
- val _ = map check_classop classops;
- in d end;
-
-fun postprocess_def (name, Datatype (_, constrs)) =
- tap (fn _ => check_samemodule (name :: map fst constrs))
- #> fold (fn (co, _) =>
- add_def_incr (co, Datatypecons name)
- #> add_dep (co, name)
- #> add_dep (name, co)
- ) constrs
- | postprocess_def (name, Class (classrels, (_, classops))) =
- tap (fn _ => check_samemodule (name :: map fst classops @ map snd classrels))
- #> fold (fn (f, _) =>
- add_def_incr (f, Classop name)
- #> add_dep (f, name)
- #> add_dep (name, f)
- ) classops
- #> fold (fn (superclass, classrel) =>
- add_def_incr (classrel, Classrel (name, superclass))
- #> add_dep (classrel, name)
- #> add_dep (name, classrel)
- ) classrels
- | postprocess_def _ =
- I;
-
(* transaction protocol *)
type transact = Graph.key option * code;
-fun ensure_def labelled_name defgen msg name (dep, code) =
+fun ensure_def labelled_name defgen name (dep, code) =
let
- val msg' = (case dep
- of NONE => msg
- | SOME dep => msg ^ ", required for " ^ labelled_name dep);
- fun add_dp NONE = I
- | add_dp (SOME dep) = add_dep (dep, name);
- fun prep_def def code =
- (check_prep_def code def, code);
fun add_def false =
ensure_bot name
- #> add_dp dep
+ #> add_dep (dep, name)
#> curry defgen (SOME name)
##> snd
- #-> (fn def => prep_def def)
- #-> (fn def => add_def_incr (name, def)
- #> postprocess_def (name, def))
+ #-> (fn def => add_def_incr (name, def))
| add_def true =
- add_dp dep;
+ add_dep (dep, name);
in
code
|> add_def (can (Graph.get_node code) name)