intermediate cleanup
authorhaftmann
Thu Oct 04 19:41:50 2007 +0200 (2007-10-04)
changeset 24836dab06e93ec28
parent 24835 8c26128f8997
child 24837 cacc5744be75
intermediate cleanup
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Thu Oct 04 19:41:49 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Oct 04 19:41:50 2007 +0200
     1.3 @@ -25,7 +25,6 @@
     1.4    val intro_classes_tac: thm list -> tactic
     1.5    val default_intro_classes_tac: thm list -> tactic
     1.6    val class_of_locale: theory -> string -> class option
     1.7 -  val local_syntax: theory -> class -> bool
     1.8    val print_classes: theory -> unit
     1.9  
    1.10    val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
    1.11 @@ -49,10 +48,10 @@
    1.12    (*experimental*)
    1.13    val init_ref: (sort -> Proof.context -> Proof.context) ref
    1.14    val init: sort -> Proof.context -> Proof.context;
    1.15 -  val init_default: sort -> Proof.context -> Proof.context;
    1.16 -  val local_param: theory -> sort -> string -> (term * (class * int)) option
    1.17 -  val remove_constraints': sort -> theory -> (string * typ) list * theory
    1.18 -  val remove_constraints: sort -> Proof.context -> (string * typ) list * Proof.context
    1.19 +  val init_exp: sort -> Proof.context -> Proof.context;
    1.20 +  val local_syntax: theory -> class -> bool
    1.21 +  val add_abbrev_in_class: string -> (string * term) * Syntax.mixfix
    1.22 +    -> theory -> term * theory
    1.23  end;
    1.24  
    1.25  structure Class : CLASS =
    1.26 @@ -100,15 +99,6 @@
    1.27        | NONE => thm;
    1.28    in strip end;
    1.29  
    1.30 -fun get_remove_constraint c thy =
    1.31 -  let
    1.32 -    val ty = Sign.the_const_constraint thy c;
    1.33 -  in
    1.34 -    thy
    1.35 -    |> Sign.add_const_constraint (c, NONE)
    1.36 -    |> pair (c, Logic.unvarifyT ty)
    1.37 -  end;
    1.38 -
    1.39  
    1.40  (** axclass command **)
    1.41  
    1.42 @@ -256,6 +246,14 @@
    1.43       of [] => ()
    1.44        | dupl_tycos => error ("type constructors occur more than once in arities: "
    1.45            ^ (commas o map quote) dupl_tycos);
    1.46 +    fun get_remove_constraint c thy =
    1.47 +      let
    1.48 +        val ty = Sign.the_const_constraint thy c;
    1.49 +      in
    1.50 +        thy
    1.51 +        |> Sign.add_const_constraint (c, NONE)
    1.52 +        |> pair (c, Logic.unvarifyT ty)
    1.53 +      end;
    1.54      fun get_consts_class tyco ty class =
    1.55        let
    1.56          val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class;
    1.57 @@ -329,29 +327,29 @@
    1.58  datatype class_data = ClassData of {
    1.59    locale: string,
    1.60    consts: (string * string) list
    1.61 -    (*locale parameter ~> theory constant name*),
    1.62 +    (*locale parameter ~> constant name*),
    1.63    local_sort: sort,
    1.64    inst: typ Symtab.table * term Symtab.table
    1.65      (*canonical interpretation*),
    1.66    intro: thm,
    1.67    local_syntax: bool,
    1.68    defs: thm list,
    1.69 -  localized: (string * (term * (class * int))) list
    1.70 -    (*theory constant name ~> (locale parameter, (class, instantiaton index of class typ))*)
    1.71 +  operations: (string * (term * int) option) list
    1.72 +    (*constant name ~> (locale term, instantiaton index of class typ)*)
    1.73  };
    1.74  
    1.75  fun rep_class_data (ClassData d) = d;
    1.76 -fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), (defs, localized)) =
    1.77 +fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations)) =
    1.78    ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, intro = intro,
    1.79 -    local_syntax = local_syntax, defs = defs, localized = localized };
    1.80 -fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, local_syntax, defs, localized }) =
    1.81 -  mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), (defs, localized)))
    1.82 +    local_syntax = local_syntax, defs = defs, operations = operations };
    1.83 +fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, local_syntax, defs, operations }) =
    1.84 +  mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations)))
    1.85  fun merge_class_data _ (ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst,
    1.86 -    intro = intro, local_syntax = local_syntax, defs = defs1, localized = localized1 },
    1.87 +    intro = intro, local_syntax = local_syntax, defs = defs1, operations = operations1 },
    1.88    ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _,
    1.89 -    defs = defs2, localized = localized2 }) =
    1.90 +    defs = defs2, operations = operations2 }) =
    1.91    mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
    1.92 -    (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (localized1, localized2)));
    1.93 +    (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (operations1, operations2)));
    1.94  
    1.95  fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
    1.96  
    1.97 @@ -395,12 +393,12 @@
    1.98    Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data))
    1.99      ((fst o ClassData.get) thy) [];
   1.100  
   1.101 -fun these_localized thy =
   1.102 -  maps (#localized o the_class_data thy) o ancestry thy;
   1.103 +fun these_operations thy =
   1.104 +  maps (#operations o the_class_data thy) o ancestry thy;
   1.105  
   1.106 -fun local_param thy = AList.lookup (op =) o these_localized thy;
   1.107 +fun local_operation thy = Option.join oo AList.lookup (op =) o these_operations thy;
   1.108  
   1.109 -fun local_syntax thy = #local_syntax o the_class_data thy
   1.110 +fun local_syntax thy = #local_syntax o the_class_data thy;
   1.111  
   1.112  fun print_classes thy =
   1.113    let
   1.114 @@ -441,15 +439,19 @@
   1.115    ClassData.map (fn (gr, tab) => (
   1.116      gr
   1.117      |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, local_sort, inst,
   1.118 -         intro, local_syntax), ([], map (apsnd (rpair (class, 0) o Free) o swap) consts)))
   1.119 +         intro, local_syntax), ([], map (apsnd (SOME o rpair 0 o Free) o swap) consts)))
   1.120      |> fold (curry Graph.add_edge class) superclasses,
   1.121      tab
   1.122      |> Symtab.update (locale, class)
   1.123    ));
   1.124  
   1.125 -fun add_class_const_def (class, (entry, def)) =
   1.126 +fun register_const (class, (entry, def)) =
   1.127    (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd)
   1.128 -    (fn (defs, localized) => (def :: defs, (apsnd o apsnd) (pair class) entry :: localized));
   1.129 +    (fn (defs, operations) => (def :: defs, apsnd SOME entry :: operations));
   1.130 +
   1.131 +fun register_abbrev class abbrev =
   1.132 +  (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd o apsnd)
   1.133 +    (cons (abbrev, NONE));
   1.134  
   1.135  
   1.136  (** rule calculation, tactics and methods **)
   1.137 @@ -543,84 +545,65 @@
   1.138  
   1.139  (** classes and class target **)
   1.140  
   1.141 -(* class context initialization *)
   1.142 +(* class context initialization - experimental *)
   1.143  
   1.144 -(*experimental*)
   1.145 -fun get_remove_constraint_ctxt c ctxt =
   1.146 +fun get_remove_constraints sort ctxt =
   1.147    let
   1.148 -    val ty = ProofContext.the_const_constraint ctxt c;
   1.149 +    val operations = these_operations (ProofContext.theory_of ctxt) sort;
   1.150 +    fun get_remove (c, _) ctxt =
   1.151 +      let
   1.152 +        val ty = ProofContext.the_const_constraint ctxt c;
   1.153 +        val _ = tracing c;
   1.154 +      in
   1.155 +        ctxt
   1.156 +        |> ProofContext.add_const_constraint (c, NONE)
   1.157 +        |> pair (c, ty)
   1.158 +      end;
   1.159    in
   1.160      ctxt
   1.161 -    |> ProofContext.add_const_constraint (c, NONE)
   1.162 -    |> pair (c, ty)
   1.163 -  end;
   1.164 -
   1.165 -fun remove_constraints' class thy =
   1.166 -  thy |> fold_map (get_remove_constraint o fst) (these_localized thy class);
   1.167 -
   1.168 -fun remove_constraints class ctxt =
   1.169 -  ctxt |> fold_map (get_remove_constraint_ctxt o fst) (these_localized (ProofContext.theory_of ctxt) class);
   1.170 -
   1.171 -fun default_typ ctxt constraints c =
   1.172 -  case AList.lookup (op =) constraints c
   1.173 -   of SOME ty => SOME ty
   1.174 -    | NONE => try (Consts.the_constraint (ProofContext.consts_of ctxt)) c;
   1.175 -
   1.176 -fun infer_constraints ctxt constraints ts =
   1.177 -    TypeInfer.infer_types (ProofContext.pp ctxt) (Sign.tsig_of (ProofContext.theory_of ctxt))
   1.178 -     (Syntax.check_typs ctxt)
   1.179 -      (default_typ ctxt constraints) (K NONE)
   1.180 -      (Variable.names_of ctxt) (Variable.maxidx_of ctxt) (SOME true) (map (rpair dummyT) ts)
   1.181 -    |> #1 |> map #1
   1.182 -  handle TYPE (msg, _, _) => error msg
   1.183 -
   1.184 -fun subst_typ local_sort =
   1.185 -  map_atyps (fn (t as TFree (v, _)) => if v = AxClass.param_tyvarname
   1.186 -        then TFree (v, local_sort)
   1.187 -        else t
   1.188 -    | t => t);
   1.189 -
   1.190 -fun sort_typ_check thy sort =
   1.191 -  let
   1.192 -    val local_sort = (#local_sort o the_class_data thy) (hd sort);
   1.193 -  in
   1.194 -    pair o map (subst_typ local_sort)
   1.195 +    |> fold_map get_remove operations
   1.196    end;
   1.197  
   1.198  fun sort_term_check thy sort constraints =
   1.199    let
   1.200 -    val algebra = Sign.classes_of thy;
   1.201 -    val local_sort = (#local_sort o the_class_data thy) (hd sort);
   1.202 -    val v = AxClass.param_tyvarname;
   1.203 -    val local_param = local_param thy sort;
   1.204 -      (*FIXME efficiency*)
   1.205 -    fun class_arg c idx ty =
   1.206 -      let
   1.207 -        val typargs = Sign.const_typargs thy (c, ty);
   1.208 -        fun classtyp (TFree (w, _)) = w = v
   1.209 -          | classtyp t = false;
   1.210 -      in classtyp (nth typargs idx) end;
   1.211 -    fun subst (t as Const (c, ty)) = (case local_param c
   1.212 -         of NONE => t
   1.213 -          | SOME (t', (_, idx)) => if class_arg c idx ty
   1.214 -             then t' else t)
   1.215 -      | subst t = t;
   1.216 -  in fn ts => fn ctxt =>
   1.217 -    ((map (map_aterms subst) #> infer_constraints ctxt constraints) ts, ctxt)
   1.218 -  end;
   1.219 +    val local_operation = local_operation thy sort;
   1.220 +    fun default_typ consts c = case AList.lookup (op =) constraints c
   1.221 +     of SOME ty => SOME ty
   1.222 +      | NONE => try (Consts.the_constraint consts) c;
   1.223 +    fun infer_constraints ctxt ts =
   1.224 +        TypeInfer.infer_types (ProofContext.pp ctxt)
   1.225 +          (Sign.tsig_of (ProofContext.theory_of ctxt))
   1.226 +          I (default_typ (ProofContext.consts_of ctxt)) (K NONE)
   1.227 +          (Variable.names_of ctxt) (Variable.maxidx_of ctxt) NONE (map (rpair dummyT) ts)
   1.228 +        |> fst |> map fst
   1.229 +      handle TYPE (msg, _, _) => error msg;
   1.230 +    fun check_typ c idx ty = case (nth (Sign.const_typargs thy (c, ty)) idx) (*FIXME localize*)
   1.231 +     of TFree (v, _) => v = AxClass.param_tyvarname
   1.232 +      | TVar (vi, _) => TypeInfer.is_param vi (*FIXME substitute in all typs*)
   1.233 +      | _ => false;
   1.234 +    fun subst_operation (t as Const (c, ty)) = (case local_operation c
   1.235 +         of SOME (t', idx) => if check_typ c idx ty then t' else t
   1.236 +          | NONE => t)
   1.237 +      | subst_operation t = t;
   1.238 +    fun subst_operations ts ctxt =
   1.239 +      ts
   1.240 +      |> (map o map_aterms) subst_operation
   1.241 +      |> infer_constraints ctxt
   1.242 +      |> rpair ctxt; (*FIXME add constraints here*)
   1.243 +  in subst_operations end;
   1.244  
   1.245 -fun init_default sort ctxt =
   1.246 +fun init_exp sort ctxt =
   1.247    let
   1.248      val thy = ProofContext.theory_of ctxt;
   1.249 -    val typ_check = sort_typ_check thy sort;
   1.250 +    val local_sort = (#local_sort o the_class_data thy) (hd sort);
   1.251      val term_check = sort_term_check thy sort;
   1.252    in
   1.253      ctxt
   1.254 -    |> remove_constraints sort
   1.255 -    ||> Variable.declare_term (Logic.mk_type (TFree (AxClass.param_tyvarname, sort)))
   1.256 -    ||> Context.proof_map (Syntax.add_typ_check 0 "class" typ_check)
   1.257 -    |-> (fn constraints =>
   1.258 -        Context.proof_map (Syntax.add_term_check 0 "class" (term_check constraints)))
   1.259 +    |> Variable.declare_term
   1.260 +        (Logic.mk_type (TFree (AxClass.param_tyvarname, local_sort)))
   1.261 +    |> get_remove_constraints sort
   1.262 +    |-> (fn constraints => Context.proof_map (Syntax.add_term_check 50 "class"
   1.263 +          (sort_term_check thy sort constraints)))
   1.264    end;
   1.265  
   1.266  val init_ref = ref (K I : sort -> Proof.context -> Proof.context);
   1.267 @@ -645,6 +628,9 @@
   1.268      val sups = filter (is_some o lookup_class_data thy) supclasses
   1.269        |> Sign.minimize_sort thy;
   1.270      val supsort = Sign.minimize_sort thy supclasses;
   1.271 +    val local_sort = case sups
   1.272 +     of sup :: _ => (#local_sort o the_class_data thy) sup
   1.273 +      | [] => supsort;
   1.274      val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
   1.275      val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
   1.276        | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
   1.277 @@ -662,7 +648,7 @@
   1.278      |> init supsort
   1.279      |> process_expr Locale.empty raw_elems
   1.280      |> fst
   1.281 -    |> (fn elems => ((((sups, supconsts), (supsort, mergeexpr)),
   1.282 +    |> (fn elems => ((((sups, supconsts), (supsort, local_sort, mergeexpr)),
   1.283            (*FIXME*) if null includes then constrain :: elems else elems)))
   1.284    end;
   1.285  
   1.286 @@ -672,7 +658,7 @@
   1.287  fun gen_class prep_spec prep_param local_syntax bname
   1.288      raw_supclasses raw_includes_elems raw_other_consts thy =
   1.289    let
   1.290 -    val (((sups, supconsts), (supsort, mergeexpr)), elems) =
   1.291 +    val (((sups, supconsts), (supsort, local_sort, mergeexpr)), elems) =
   1.292        prep_spec thy raw_supclasses raw_includes_elems;
   1.293      val other_consts = map (prep_param thy) raw_other_consts;
   1.294      fun mk_instT class = Symtab.empty
   1.295 @@ -721,7 +707,7 @@
   1.296      |> Locale.add_locale_i (SOME "") bname mergeexpr elems
   1.297      |-> (fn name_locale => ProofContext.theory_result (
   1.298        `(fn thy => extract_params thy name_locale)
   1.299 -      #-> (fn (local_sort, (globals, params)) =>
   1.300 +      #-> (fn (_, (globals, params)) =>
   1.301          AxClass.define_class_params (bname, supsort) params
   1.302            (extract_assumes name_locale params) other_consts
   1.303        #-> (fn (name_axclass, (consts, axioms)) =>
   1.304 @@ -783,7 +769,7 @@
   1.305        in
   1.306          thy
   1.307          |> class_interpretation class [def'] [def_eq]
   1.308 -        |> add_class_const_def (class, ((c', (rhs, typidx)), def'))
   1.309 +        |> register_const (class, ((c', (rhs, typidx)), def'))
   1.310        end;
   1.311    in
   1.312      thy
   1.313 @@ -797,6 +783,23 @@
   1.314      |> Sign.restore_naming thy
   1.315    end;
   1.316  
   1.317 +fun add_abbrev_in_class class ((c, rhs), syn) thy =
   1.318 +  let
   1.319 +    val local_sort = (#local_sort o the_class_data thy) class;
   1.320 +    val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   1.321 +      if w = AxClass.param_tyvarname then TFree (w, local_sort) else TFree var);
   1.322 +    val ty = fastype_of rhs;
   1.323 +    val rhs' = map_types subst_typ rhs;
   1.324 +  in
   1.325 +    thy
   1.326 +    |> Sign.parent_path (*FIXME*)
   1.327 +    |> Sign.add_abbrev Syntax.internalM [] (c, rhs)
   1.328 +    |-> (fn (lhs as Const (c', _), _) => register_abbrev class c'
   1.329 +      (*#> Sign.add_const_constraint (c', SOME ty)*)
   1.330 +      #> pair lhs)
   1.331 +    ||> Sign.restore_naming thy
   1.332 +  end;
   1.333 +
   1.334  
   1.335  (* interpretation in class target *)
   1.336