# HG changeset patch # User haftmann # Date 1138963691 -3600 # Node ID 5590770e1b09014ee902b0b13e83d0f80f618087 # Parent 77e18862990fee531276e6d0886757a5c8d7b9e3 minor improvements diff -r 77e18862990f -r 5590770e1b09 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Fri Feb 03 11:47:57 2006 +0100 +++ b/src/Pure/Tools/class_package.ML Fri Feb 03 11:48:11 2006 +0100 @@ -151,7 +151,7 @@ local -fun gen_add_class add_locale prep_class bname raw_supclasses raw_body thy = +fun gen_add_class add_locale prep_class do_proof bname raw_supclasses raw_body thy = let val supclasses = map (prep_class thy) raw_supclasses; fun get_allcs class = @@ -170,46 +170,39 @@ supclasses; fun mk_c_lookup c_global supcs c_adds = map2 (fn ((c, _), _) => pair c) c_global supcs @ c_adds - fun extract_assumes v c_lookup elems = - elems - |> (map o List.mapPartial) - (fn (Element.Assumes asms) => (SOME o map (map fst o snd)) asms - | _ => NONE) - |> Library.flat o Library.flat o Library.flat + fun extract_tyvar_consts thy name_locale = + let + fun extract_tyvar_name thy tys = + fold (curry add_typ_tfrees) tys [] + |> (fn [(v, sort)] => + if Sorts.sort_le (Sign.classes_of thy) (swap (sort, supsort)) + 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)) + val raw_consts = + Locale.parameters_of thy name_locale + |> map (apsnd Syntax.unlocalize_mixfix) + |> ((curry splitAt o length) supcs); + val v = (extract_tyvar_name thy o map (snd o fst) o op @) raw_consts; + fun subst_ty cs = + map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) cs; + val consts = (subst_ty (fst raw_consts), subst_ty (snd raw_consts)); + val _ = (writeln o commas o map (fst o fst)) (fst consts); + val _ = (writeln o commas o map (fst o fst)) (snd consts); + in (v, consts) end; + fun add_global_const v ((c, ty), syn) thy = + thy + |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)] + |> `(fn thy => (c, (Sign.intern_const thy c |> print, ty))) + fun extract_assumes thy name_locale c_lookup = + Locale.local_asms_of thy name_locale + |> map snd + |> Library.flat |> (map o map_aterms) (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) c_lookup) c, ty) | t => t) |> tap (fn ts => writeln ("(1) axclass axioms: " ^ (commas o map (Sign.string_of_term thy)) ts)); - fun extract_tyvar_name thy tys = - fold (curry add_typ_tfrees) tys [] - |> (fn [(v, sort)] => - if Sorts.sort_le (Sign.classes_of thy) (swap (sort, supsort)) - 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_tyvar_consts thy (import_elems, body_elems) = - let - fun get_elems elems = - elems - |> Library.flat - |> List.mapPartial - (fn (Element.Fixes consts) => SOME consts - | _ => NONE) - |> Library.flat - |> map (fn (c, ty, syn) => ((c, the ty), Syntax.unlocalize_mixfix syn)) - val import_consts = get_elems import_elems; - val body_consts = get_elems body_elems; - val v = extract_tyvar_name thy (map (snd o fst) (import_consts @ body_consts)); - fun subst_ty cs = - map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) cs; - val import_cs = subst_ty import_consts; - val body_cs = subst_ty body_consts; - in (v, (import_cs, body_cs)) end; - fun add_global_const v ((c, ty), syn) thy = - thy - |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)] - |> `(fn thy => (c, (Sign.intern_const thy c, ty))) fun add_global_constraint v class (_, (c, ty)) thy = thy |> Sign.add_const_constraint_i (c, subst_clsvar v (TVar ((v, 0), [class])) ty); @@ -217,36 +210,37 @@ thy |> Locale.interpretation (NameSpace.base name_locale, []) (Locale.Locale name_locale) (map (SOME o fst) cs) - |> Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE); - fun print_ctxt ctxt elem = - map Pretty.writeln (Element.pretty_ctxt ctxt elem) + |> do_proof ax_axioms; in thy |> add_locale bname locexpr raw_body - |-> (fn ((import_elems, body_elems), ctxt) => + |-> (fn ctxt => `(fn thy => Locale.intern thy bname) #-> (fn name_locale => - `(fn thy => extract_tyvar_consts thy (import_elems, body_elems)) + `(fn thy => extract_tyvar_consts thy name_locale) #-> (fn (v, (c_global, c_defs)) => fold_map (add_global_const v) c_defs #-> (fn c_adds => - AxClass.add_axclass_i (bname, supsort) - (map (Thm.no_attributes o pair "") (extract_assumes v (mk_c_lookup c_global supcs c_adds) body_elems)) + `(fn thy => extract_assumes thy name_locale (mk_c_lookup c_global supcs c_adds)) + #-> (fn assumes => + AxClass.add_axclass_i (bname, supsort) (map (Thm.no_attributes o pair "") assumes)) #-> (fn { axioms = ax_axioms : thm list, ...} => `(fn thy => Sign.intern_class thy bname) #-> (fn name_axclass => fold (add_global_constraint v name_axclass) c_adds #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, map snd c_adds)) - #> tap (fn _ => (map o map) (print_ctxt ctxt) import_elems) - #> tap (fn _ => (map o map) (print_ctxt ctxt) body_elems) #> interpret name_locale (supcs @ (map (fn ((c, ty), _) => (Sign.intern_const thy c, ty)) c_defs)) ax_axioms )))))) end; in -val add_class = gen_add_class (Locale.add_locale_context true) intern_class; -val add_class_i = gen_add_class (Locale.add_locale_context_i true) certify_class; +val add_class = gen_add_class (Locale.add_locale true) intern_class + (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE)); +val add_class_i = gen_add_class (Locale.add_locale_i true) certify_class + (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE)); +val add_class_exp = gen_add_class (Locale.add_locale true) intern_class + (K I); end; (* local *) @@ -271,9 +265,10 @@ |> Sign.add_const_constraint_i (c, ty2) |> pair (c, ty1) end; - fun get_c_given thy = map (fst o dest_def o snd o tap_def thy o fst) raw_defs; - fun check_defs c_given c_req thy = + fun check_defs raw_defs c_req thy = let + val thy' = Sign.add_arities_i [(tyco, asorts, sort)] thy; + val c_given = map (fst o dest_def o snd o tap_def thy' o fst) raw_defs; fun eq_c ((c1, ty1), (c2, ty2)) = let val ty1' = Type.varifyT ty1; @@ -297,12 +292,18 @@ #> fold (fn class => add_inst_data (class, (tyco, Context.theory_name thy))) sort; in thy + |> tap (fn thy => check_defs raw_defs c_req thy) |> fold_map get_remove_contraint (map fst c_req) - ||> tap (fn thy => check_defs (get_c_given thy) c_req thy) ||> add_defs (true, raw_defs) |-> (fn cs => AxClass.instance_arity_i (after_qed cs) arity) end; +val _ : string option -> + ((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list -> + theory -> (term * (bstring * thm)) list * (Proof.context * theory) + = Specification.definition_i; + + val add_instance_arity = fn x => gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm x; val add_instance_arity_i = fn x => gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I) x; @@ -521,6 +522,14 @@ >> (Toplevel.theory_context o (fn ((bname, supclasses), elems) => add_class bname supclasses elems))); +val classP_exp = + OuterSyntax.command (classK ^ "_exp") "operational type classes" K.thy_goal ( + P.name --| P.$$$ "=" + -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) [] + -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) [] + >> (Toplevel.theory_to_proof + o (fn ((bname, supclasses), elems) => add_class_exp bname supclasses elems))); + val instanceP = OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal (( P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) >> AxClass.instance_subclass @@ -529,7 +538,7 @@ | (inst, defs) => add_instance_arity inst defs) ) >> (Toplevel.print oo Toplevel.theory_to_proof)); -val _ = OuterSyntax.add_parsers [classP, instanceP]; +val _ = OuterSyntax.add_parsers [classP, classP_exp, instanceP]; end; (* local *) diff -r 77e18862990f -r 5590770e1b09 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Fri Feb 03 11:47:57 2006 +0100 +++ b/src/Pure/Tools/codegen_package.ML Fri Feb 03 11:48:11 2006 +0100 @@ -505,19 +505,19 @@ let fun add_rename (var as ((v, _), sort)) used = let - val v' = variant used v + val v' = "'" ^ variant used (unprefix "'" v) in (((var, TFree (v', sort)), (v', TVar var)), v' :: used) end; fun typ_names (Type (tyco, tys)) (vars, names) = (vars, names |> insert (op =) (NameSpace.base tyco)) |> fold typ_names tys | typ_names (TFree (v, _)) (vars, names) = - (vars, names |> insert (op =) v) - | typ_names (TVar (v, sort)) (vars, names) = - (vars |> AList.update (op =) (v, sort), names); + (vars, names |> insert (op =) (unprefix "'" v)) + | typ_names (TVar (vi, sort)) (vars, names) = + (vars |> AList.update (op =) (vi, sort), names); val (vars, used) = fold typ_names tys ([], []); val (renames, reverse) = fold_map add_rename vars used |> fst |> split_list; in - (reverse, (map o map_atyps) (Term.instantiateT renames) tys) + (reverse, map (Term.instantiateT renames) tys) end; fun burrow_typs_yield f ts = @@ -553,7 +553,7 @@ val (vars, used) = fold term_names ts ([], []); val (renames, reverse) = fold_map add_rename vars used |> fst |> split_list; in - (reverse, (map o map_aterms) (Term.instantiate ([], renames)) ts) + (reverse, map (Term.instantiate ([], renames)) ts) end; fun devarify_term_typs ts = diff -r 77e18862990f -r 5590770e1b09 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Fri Feb 03 11:47:57 2006 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Fri Feb 03 11:48:11 2006 +0100 @@ -404,11 +404,11 @@ (case tyco_syntax tyco of NONE => let - val f' = (str o resolv) tyco + val tyco' = (str o resolv) tyco in case map (ml_from_type BR) tys - of [] => f' - | [p] => Pretty.block [p, Pretty.brk 1, f'] - | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, f'] + of [] => tyco' + | [p] => Pretty.block [p, Pretty.brk 1, tyco'] + | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco'] end | SOME ((i, k), pr) => if not (i <= length tys andalso length tys <= k) @@ -442,8 +442,16 @@ ]) | ml_from_expr fxy (e as IConst x) = ml_from_app fxy (x, []) - | ml_from_expr fxy (IVarE (v, _)) = - str v + | ml_from_expr fxy (IVarE (v, ty)) = + if needs_type ty + then + Pretty.enclose "(" ")" [ + str v, + str ":", + ml_from_type NOBR ty + ] + else + str v | ml_from_expr fxy (IAbs ((v, _), e)) = brackify fxy [ str ("fn " ^ v ^ " =>"), @@ -537,7 +545,7 @@ fun ml_from_datatypes defs = let val defs' = List.mapPartial - (fn (name, Datatype info) => SOME (resolv name, info) + (fn (name, Datatype info) => SOME (name, info) | (name, Datatypecons _) => NONE | (name, def) => error ("datatype block containing illegal def: " ^ (Pretty.output o pretty_def) def) @@ -563,7 +571,7 @@ case defs' of (def::defs_tl) => chunk_defs ( - mk_datatype "datatype " def + mk_datatype "datatype" def :: map (mk_datatype "and ") defs_tl ) |> SOME | _ => NONE @@ -877,7 +885,7 @@ | hs_from_def (name, Fun (eqs, (sctxt, ty))) = Pretty.chunks [ Pretty.block [ - (str o lower_first o resolv) (name ^ " ::"), + (str o suffix " ::" o lower_first o resolv) name, Pretty.brk 1, hs_from_sctxt_type (sctxt, ty) ], diff -r 77e18862990f -r 5590770e1b09 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Fri Feb 03 11:47:57 2006 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Fri Feb 03 11:48:11 2006 +0100 @@ -1044,27 +1044,20 @@ ([], SOME tab) | get_path_name [p] tab = let - val _ = writeln ("(1) " ^ p); val SOME (N (p', tab')) = Symtab.lookup tab p in ([p'], tab') end | get_path_name [p1, p2] tab = - let - val _ = (writeln o prefix "(2) " o NameSpace.pack) [p1, p2]; - in case Symtab.lookup tab p1 + case Symtab.lookup tab p1 of SOME (N (p', SOME tab')) => let - val _ = writeln ("(2) 'twas a module"); val (ps', tab'') = get_path_name [p2] tab' in (p' :: ps', tab'') end | NONE => let - val _ = writeln ("(2) 'twas a definition"); val SOME (N (p', NONE)) = Symtab.lookup tab (NameSpace.pack [p1, p2]) in ([p'], NONE) end - end | get_path_name (p::ps) tab = let - val _ = (writeln o prefix "(3) " o commas) (p::ps); val SOME (N (p', SOME tab')) = Symtab.lookup tab p val (ps', tab'') = get_path_name ps tab' in (p' :: ps', tab'') end; @@ -1072,107 +1065,18 @@ if (is_some o Int.fromString) name then name else let - val _ = writeln ("(0) prefix: " ^ commas prefix); - val _ = writeln ("(0) name: " ^ name) val (common, (_, rem)) = get_prefix (op =) (prefix, NameSpace.unpack name); - val _ = writeln ("(0) common: " ^ commas common); - val _ = writeln ("(0) rem: " ^ commas rem); val (_, SOME tab') = get_path_name common tab; val (name', _) = get_path_name rem tab'; in NameSpace.pack name' end; in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end; -val _ : module -> string list list -> (string * string -> string) -> (string -> string option) -> string list -> string -> string = mk_deresolver; - -fun mk_resolvtab' nsp_conn validate module = - let - fun validate' n = perhaps validate n; - fun ensure_unique prfix prfix' name name' (locals, tab) = - let - fun uniquify name n = - let - val name' = if n = 0 then name else name ^ "_" ^ string_of_int n - in - if member (op =) locals name' - then uniquify name (n+1) - else case validate name - of NONE => name' - | SOME name' => uniquify name' n - end; - val name'' = uniquify name' 0; - in - (locals, tab) - |> apsnd (Symtab.update_new - (NameSpace.pack (prfix @ [name]), NameSpace.pack (prfix' @ [name'']))) - |> apfst (cons name'') - |> pair name'' - end; - fun fill_in prfix prfix' node tab = - let - val keys = Graph.keys node; - val nodes = AList.make (Graph.get_node node) keys; - val (mods, defs) = - nodes - |> List.partition (fn (_, Module _) => true | _ => false) - |> apfst (map (fn (name, Module m) => (name, m))) - |> apsnd (map fst) - fun modl_validate (name, modl) (locals, tab) = - (locals, tab) - |> ensure_unique prfix prfix' name name - |-> (fn name' => apsnd (fill_in (prfix @ [name]) (prfix @ [name']) modl)) - fun ensure_unique_sidf sidf = - let - val [shallow, name] = NameSpace.unpack sidf; - in - nsp_conn - |> get_first - (fn grp => if member (op =) grp shallow - then grp |> remove (op =) shallow |> SOME else NONE) - |> these - |> map (fn s => NameSpace.pack [s, name]) - |> exists (member (op =) defs) - |> (fn b => if b then sidf else name) - end; - fun def_validate sidf (locals, tab) = - (locals, tab) - |> ensure_unique prfix prfix' sidf (ensure_unique_sidf sidf) - |> snd - in - ([], tab) - |> fold modl_validate mods - |> fold def_validate defs - |> snd - end; - in - Symtab.empty - |> fill_in [] [] module - end; - -fun mk_resolv tab = - let - fun resolver modl name = - if NameSpace.is_qualified name then - let - val _ = debug 12 (fn name' => "resolving " ^ quote name ^ " in " - ^ (quote o NameSpace.pack) modl) (); - val modl' = if null modl then [] else - (NameSpace.unpack o the o Symtab.lookup tab o NameSpace.pack) modl; - val name' = (NameSpace.unpack o the o Symtab.lookup tab) name - in - (NameSpace.pack o snd o snd o get_prefix (op =)) (modl', name') - |> debug 12 (fn name' => "resolving " ^ quote name ^ " to " - ^ quote name' ^ " in " ^ (quote o NameSpace.pack) modl) - end - else name - in resolver end; - (* serialization *) fun serialize seri_defs seri_module validate nsp_conn name_root module = let val resolver = mk_deresolver module nsp_conn snd validate; -(* val resolver = mk_resolv (mk_resolvtab' nsp_conn validate module); *) fun mk_name prfx name = let val name_qual = NameSpace.pack (prfx @ [name])