# HG changeset patch # User haftmann # Date 1191519710 -7200 # Node ID dab06e93ec2808bfa1a57e0902a7a9ff2bc96f93 # Parent 8c26128f8997bf13a61d0038e4d57b164f61f09a intermediate cleanup diff -r 8c26128f8997 -r dab06e93ec28 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Thu Oct 04 19:41:49 2007 +0200 +++ b/src/Pure/Isar/class.ML Thu Oct 04 19:41:50 2007 +0200 @@ -25,7 +25,6 @@ val intro_classes_tac: thm list -> tactic val default_intro_classes_tac: thm list -> tactic val class_of_locale: theory -> string -> class option - val local_syntax: theory -> class -> bool val print_classes: theory -> unit val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state @@ -49,10 +48,10 @@ (*experimental*) val init_ref: (sort -> Proof.context -> Proof.context) ref val init: sort -> Proof.context -> Proof.context; - val init_default: sort -> Proof.context -> Proof.context; - val local_param: theory -> sort -> string -> (term * (class * int)) option - val remove_constraints': sort -> theory -> (string * typ) list * theory - val remove_constraints: sort -> Proof.context -> (string * typ) list * Proof.context + val init_exp: sort -> Proof.context -> Proof.context; + val local_syntax: theory -> class -> bool + val add_abbrev_in_class: string -> (string * term) * Syntax.mixfix + -> theory -> term * theory end; structure Class : CLASS = @@ -100,15 +99,6 @@ | NONE => thm; in strip end; -fun get_remove_constraint c thy = - let - val ty = Sign.the_const_constraint thy c; - in - thy - |> Sign.add_const_constraint (c, NONE) - |> pair (c, Logic.unvarifyT ty) - end; - (** axclass command **) @@ -256,6 +246,14 @@ of [] => () | dupl_tycos => error ("type constructors occur more than once in arities: " ^ (commas o map quote) dupl_tycos); + fun get_remove_constraint c thy = + let + val ty = Sign.the_const_constraint thy c; + in + thy + |> Sign.add_const_constraint (c, NONE) + |> pair (c, Logic.unvarifyT ty) + end; fun get_consts_class tyco ty class = let val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class; @@ -329,29 +327,29 @@ datatype class_data = ClassData of { locale: string, consts: (string * string) list - (*locale parameter ~> theory constant name*), + (*locale parameter ~> constant name*), local_sort: sort, inst: typ Symtab.table * term Symtab.table (*canonical interpretation*), intro: thm, local_syntax: bool, defs: thm list, - localized: (string * (term * (class * int))) list - (*theory constant name ~> (locale parameter, (class, instantiaton index of class typ))*) + operations: (string * (term * int) option) list + (*constant name ~> (locale term, instantiaton index of class typ)*) }; fun rep_class_data (ClassData d) = d; -fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), (defs, localized)) = +fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations)) = ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, intro = intro, - local_syntax = local_syntax, defs = defs, localized = localized }; -fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, local_syntax, defs, localized }) = - mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), (defs, localized))) + local_syntax = local_syntax, defs = defs, operations = operations }; +fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, local_syntax, defs, operations }) = + mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations))) fun merge_class_data _ (ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, - intro = intro, local_syntax = local_syntax, defs = defs1, localized = localized1 }, + intro = intro, local_syntax = local_syntax, defs = defs1, operations = operations1 }, ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _, - defs = defs2, localized = localized2 }) = + defs = defs2, operations = operations2 }) = mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), - (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (localized1, localized2))); + (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (operations1, operations2))); fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2)); @@ -395,12 +393,12 @@ Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data)) ((fst o ClassData.get) thy) []; -fun these_localized thy = - maps (#localized o the_class_data thy) o ancestry thy; +fun these_operations thy = + maps (#operations o the_class_data thy) o ancestry thy; -fun local_param thy = AList.lookup (op =) o these_localized thy; +fun local_operation thy = Option.join oo AList.lookup (op =) o these_operations thy; -fun local_syntax thy = #local_syntax o the_class_data thy +fun local_syntax thy = #local_syntax o the_class_data thy; fun print_classes thy = let @@ -441,15 +439,19 @@ ClassData.map (fn (gr, tab) => ( gr |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, local_sort, inst, - intro, local_syntax), ([], map (apsnd (rpair (class, 0) o Free) o swap) consts))) + intro, local_syntax), ([], map (apsnd (SOME o rpair 0 o Free) o swap) consts))) |> fold (curry Graph.add_edge class) superclasses, tab |> Symtab.update (locale, class) )); -fun add_class_const_def (class, (entry, def)) = +fun register_const (class, (entry, def)) = (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd) - (fn (defs, localized) => (def :: defs, (apsnd o apsnd) (pair class) entry :: localized)); + (fn (defs, operations) => (def :: defs, apsnd SOME entry :: operations)); + +fun register_abbrev class abbrev = + (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd o apsnd) + (cons (abbrev, NONE)); (** rule calculation, tactics and methods **) @@ -543,84 +545,65 @@ (** classes and class target **) -(* class context initialization *) +(* class context initialization - experimental *) -(*experimental*) -fun get_remove_constraint_ctxt c ctxt = +fun get_remove_constraints sort ctxt = let - val ty = ProofContext.the_const_constraint ctxt c; + val operations = these_operations (ProofContext.theory_of ctxt) sort; + fun get_remove (c, _) ctxt = + let + val ty = ProofContext.the_const_constraint ctxt c; + val _ = tracing c; + in + ctxt + |> ProofContext.add_const_constraint (c, NONE) + |> pair (c, ty) + end; in ctxt - |> ProofContext.add_const_constraint (c, NONE) - |> pair (c, ty) - end; - -fun remove_constraints' class thy = - thy |> fold_map (get_remove_constraint o fst) (these_localized thy class); - -fun remove_constraints class ctxt = - ctxt |> fold_map (get_remove_constraint_ctxt o fst) (these_localized (ProofContext.theory_of ctxt) class); - -fun default_typ ctxt constraints c = - case AList.lookup (op =) constraints c - of SOME ty => SOME ty - | NONE => try (Consts.the_constraint (ProofContext.consts_of ctxt)) c; - -fun infer_constraints ctxt constraints ts = - TypeInfer.infer_types (ProofContext.pp ctxt) (Sign.tsig_of (ProofContext.theory_of ctxt)) - (Syntax.check_typs ctxt) - (default_typ ctxt constraints) (K NONE) - (Variable.names_of ctxt) (Variable.maxidx_of ctxt) (SOME true) (map (rpair dummyT) ts) - |> #1 |> map #1 - handle TYPE (msg, _, _) => error msg - -fun subst_typ local_sort = - map_atyps (fn (t as TFree (v, _)) => if v = AxClass.param_tyvarname - then TFree (v, local_sort) - else t - | t => t); - -fun sort_typ_check thy sort = - let - val local_sort = (#local_sort o the_class_data thy) (hd sort); - in - pair o map (subst_typ local_sort) + |> fold_map get_remove operations end; fun sort_term_check thy sort constraints = let - val algebra = Sign.classes_of thy; - val local_sort = (#local_sort o the_class_data thy) (hd sort); - val v = AxClass.param_tyvarname; - val local_param = local_param thy sort; - (*FIXME efficiency*) - fun class_arg c idx ty = - let - val typargs = Sign.const_typargs thy (c, ty); - fun classtyp (TFree (w, _)) = w = v - | classtyp t = false; - in classtyp (nth typargs idx) end; - fun subst (t as Const (c, ty)) = (case local_param c - of NONE => t - | SOME (t', (_, idx)) => if class_arg c idx ty - then t' else t) - | subst t = t; - in fn ts => fn ctxt => - ((map (map_aterms subst) #> infer_constraints ctxt constraints) ts, ctxt) - end; + val local_operation = local_operation thy sort; + fun default_typ consts c = case AList.lookup (op =) constraints c + of SOME ty => SOME ty + | NONE => try (Consts.the_constraint consts) c; + fun infer_constraints ctxt ts = + TypeInfer.infer_types (ProofContext.pp ctxt) + (Sign.tsig_of (ProofContext.theory_of ctxt)) + I (default_typ (ProofContext.consts_of ctxt)) (K NONE) + (Variable.names_of ctxt) (Variable.maxidx_of ctxt) NONE (map (rpair dummyT) ts) + |> fst |> map fst + handle TYPE (msg, _, _) => error msg; + fun check_typ c idx ty = case (nth (Sign.const_typargs thy (c, ty)) idx) (*FIXME localize*) + of TFree (v, _) => v = AxClass.param_tyvarname + | TVar (vi, _) => TypeInfer.is_param vi (*FIXME substitute in all typs*) + | _ => false; + fun subst_operation (t as Const (c, ty)) = (case local_operation c + of SOME (t', idx) => if check_typ c idx ty then t' else t + | NONE => t) + | subst_operation t = t; + fun subst_operations ts ctxt = + ts + |> (map o map_aterms) subst_operation + |> infer_constraints ctxt + |> rpair ctxt; (*FIXME add constraints here*) + in subst_operations end; -fun init_default sort ctxt = +fun init_exp sort ctxt = let val thy = ProofContext.theory_of ctxt; - val typ_check = sort_typ_check thy sort; + val local_sort = (#local_sort o the_class_data thy) (hd sort); val term_check = sort_term_check thy sort; in ctxt - |> remove_constraints sort - ||> Variable.declare_term (Logic.mk_type (TFree (AxClass.param_tyvarname, sort))) - ||> Context.proof_map (Syntax.add_typ_check 0 "class" typ_check) - |-> (fn constraints => - Context.proof_map (Syntax.add_term_check 0 "class" (term_check constraints))) + |> Variable.declare_term + (Logic.mk_type (TFree (AxClass.param_tyvarname, local_sort))) + |> get_remove_constraints sort + |-> (fn constraints => Context.proof_map (Syntax.add_term_check 50 "class" + (sort_term_check thy sort constraints))) end; val init_ref = ref (K I : sort -> Proof.context -> Proof.context); @@ -645,6 +628,9 @@ val sups = filter (is_some o lookup_class_data thy) supclasses |> Sign.minimize_sort thy; val supsort = Sign.minimize_sort thy supclasses; + val local_sort = case sups + of sup :: _ => (#local_sort o the_class_data thy) sup + | [] => supsort; val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups; val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e) | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []); @@ -662,7 +648,7 @@ |> init supsort |> process_expr Locale.empty raw_elems |> fst - |> (fn elems => ((((sups, supconsts), (supsort, mergeexpr)), + |> (fn elems => ((((sups, supconsts), (supsort, local_sort, mergeexpr)), (*FIXME*) if null includes then constrain :: elems else elems))) end; @@ -672,7 +658,7 @@ fun gen_class prep_spec prep_param local_syntax bname raw_supclasses raw_includes_elems raw_other_consts thy = let - val (((sups, supconsts), (supsort, mergeexpr)), elems) = + val (((sups, supconsts), (supsort, local_sort, mergeexpr)), elems) = prep_spec thy raw_supclasses raw_includes_elems; val other_consts = map (prep_param thy) raw_other_consts; fun mk_instT class = Symtab.empty @@ -721,7 +707,7 @@ |> Locale.add_locale_i (SOME "") bname mergeexpr elems |-> (fn name_locale => ProofContext.theory_result ( `(fn thy => extract_params thy name_locale) - #-> (fn (local_sort, (globals, params)) => + #-> (fn (_, (globals, params)) => AxClass.define_class_params (bname, supsort) params (extract_assumes name_locale params) other_consts #-> (fn (name_axclass, (consts, axioms)) => @@ -783,7 +769,7 @@ in thy |> class_interpretation class [def'] [def_eq] - |> add_class_const_def (class, ((c', (rhs, typidx)), def')) + |> register_const (class, ((c', (rhs, typidx)), def')) end; in thy @@ -797,6 +783,23 @@ |> Sign.restore_naming thy end; +fun add_abbrev_in_class class ((c, rhs), syn) thy = + let + val local_sort = (#local_sort o the_class_data thy) class; + val subst_typ = Term.map_type_tfree (fn var as (w, sort) => + if w = AxClass.param_tyvarname then TFree (w, local_sort) else TFree var); + val ty = fastype_of rhs; + val rhs' = map_types subst_typ rhs; + in + thy + |> Sign.parent_path (*FIXME*) + |> Sign.add_abbrev Syntax.internalM [] (c, rhs) + |-> (fn (lhs as Const (c', _), _) => register_abbrev class c' + (*#> Sign.add_const_constraint (c', SOME ty)*) + #> pair lhs) + ||> Sign.restore_naming thy + end; + (* interpretation in class target *)