# HG changeset patch # User haftmann # Date 1191304795 -7200 # Node ID 3bf788a0c49ab480b992a51b9784e5cc35305b37 # Parent 862b71696efe6073507faebde6279e8ef447c1b6 clarified role of class relations diff -r 862b71696efe -r 3bf788a0c49a src/Tools/code/code_name.ML --- 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; diff -r 862b71696efe -r 3bf788a0c49a src/Tools/code/code_package.ML --- 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 "" 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 = diff -r 862b71696efe -r 3bf788a0c49a src/Tools/code/code_target.ML --- 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 {" ], diff -r 862b71696efe -r 3bf788a0c49a src/Tools/code/code_thingol.ML --- 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)