improved class syntax
authorhaftmann
Thu Oct 18 16:09:38 2007 +0200 (2007-10-18)
changeset 25083765528b4b419
parent 25082 c93a234ccf2b
child 25084 30ce1e078b72
improved class syntax
src/Pure/Isar/class.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/class.ML	Thu Oct 18 16:09:36 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Oct 18 16:09:38 2007 +0200
     1.3 @@ -16,14 +16,14 @@
     1.4      -> string list -> theory -> string * Proof.context
     1.5    val class_cmd: bstring -> xstring list -> Element.context Locale.element list
     1.6      -> xstring list -> theory -> string * Proof.context
     1.7 -  val init: class -> Proof.context -> Proof.context
     1.8 -  val add_const_in_class: string -> (string * mixfix) * term
     1.9 -    -> theory -> string * theory
    1.10 -  val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * term
    1.11 -    -> theory -> string * theory
    1.12 -  val remove_constraint: class -> string -> Proof.context -> Proof.context
    1.13    val is_class: theory -> class -> bool
    1.14    val these_params: theory -> sort -> (string * (string * typ)) list
    1.15 +  val init: class -> Proof.context -> Proof.context
    1.16 +  val add_logical_const: string -> (string * mixfix) * term
    1.17 +    -> theory -> string * theory
    1.18 +  val add_syntactic_const: string -> Syntax.mode -> (string * mixfix) * term
    1.19 +    -> theory -> string * theory
    1.20 +  val refresh_syntax: class -> Proof.context -> Proof.context
    1.21    val intro_classes_tac: thm list -> tactic
    1.22    val default_intro_classes_tac: thm list -> tactic
    1.23    val print_classes: theory -> unit
    1.24 @@ -309,8 +309,8 @@
    1.25    consts: (string * string) list
    1.26      (*locale parameter ~> constant name*),
    1.27    base_sort: sort,
    1.28 -  inst: (typ option list * term option list) * term Symtab.table
    1.29 -    (*canonical interpretation FIXME*),
    1.30 +  inst: term option list
    1.31 +    (*canonical interpretation*),
    1.32    morphism: morphism,
    1.33      (*partial morphism of canonical interpretation*)
    1.34    intro: thm,
    1.35 @@ -433,23 +433,16 @@
    1.36  
    1.37  (* updaters *)
    1.38  
    1.39 -fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
    1.40 +fun add_class_data ((class, superclasses), (cs, base_sort, insttab, phi, intro)) thy =
    1.41    let
    1.42 -    (*FIXME*)
    1.43 -    val is_empty = null (fold (fn ((_, ty), _) => fold_atyps cons ty) cs [])
    1.44 -      andalso null ((fold o fold_types o fold_atyps) cons
    1.45 -        (maps snd (Locale.global_asms_of thy class)) []);
    1.46 -    (*FIXME*)
    1.47 -    val inst_params = map
    1.48 -      (SOME o the o Symtab.lookup inst o fst o fst)
    1.49 +    val inst = map
    1.50 +      (SOME o the o Symtab.lookup insttab o fst o fst)
    1.51          (Locale.parameters_of_expr thy (Locale.Locale class));
    1.52 -    val instT = if is_empty then [] else [SOME (TFree (Name.aT, [class]))];
    1.53 -    val inst' = ((instT, inst_params), inst);
    1.54      val operations = map (fn (v_ty as (_, ty'), (c, ty)) =>
    1.55        (c, ((Free v_ty, ty'), (Logic.varifyT ty, 0)))) cs;
    1.56      val cs = (map o pairself) fst cs;
    1.57      val add_class = Graph.new_node (class,
    1.58 -        mk_class_data ((cs, base_sort, inst', phi, intro), ([], operations)))
    1.59 +        mk_class_data ((cs, base_sort, inst, phi, intro), ([], operations)))
    1.60        #> fold (curry Graph.add_edge class) superclasses;
    1.61    in
    1.62      ClassData.map add_class thy
    1.63 @@ -521,7 +514,7 @@
    1.64  fun class_interpretation class facts defs thy =
    1.65    let
    1.66      val params = these_params thy [class];
    1.67 -    val { inst = ((_, inst), _), ... } = the_class_data thy class;
    1.68 +    val inst = (#inst o the_class_data thy) class;
    1.69      val tac = ALLGOALS (ProofContext.fact_tac facts);
    1.70      val prfx = class_prefix class;
    1.71    in
    1.72 @@ -562,38 +555,78 @@
    1.73  
    1.74  (* class context syntax *)
    1.75  
    1.76 -fun internal_remove_constraint base_sort (c, (_, (ty, _))) ctxt =
    1.77 +structure ClassSyntax = ProofDataFun(
    1.78 +  type T = {
    1.79 +    constraints: (string * typ) list,
    1.80 +    base_sort: sort,
    1.81 +    local_operation: string * typ -> (typ * term) option,
    1.82 +    rews: (term * term) list,
    1.83 +    passed: bool
    1.84 +  } option;
    1.85 +  fun init _ = NONE;
    1.86 +);
    1.87 +
    1.88 +fun synchronize_syntax thy sups base_sort ctxt =
    1.89    let
    1.90 -    val ty' = ty
    1.91 -      |> map_atyps (fn ty as TVar ((v, 0), _) =>
    1.92 -           if v = Name.aT then TVar ((v, 0), base_sort) else ty)
    1.93 -      |> SOME;
    1.94 -  in ProofContext.add_const_constraint (c, ty') ctxt end;
    1.95 +    val operations = these_operations thy sups;
    1.96 +
    1.97 +    (* constraints *)
    1.98 +    fun local_constraint (c, (_, (ty, _))) =
    1.99 +      let
   1.100 +        val ty' = ty
   1.101 +          |> map_atyps (fn ty as TVar ((v, 0), _) =>
   1.102 +               if v = Name.aT then TVar ((v, 0), base_sort) else ty)
   1.103 +          |> SOME;
   1.104 +      in (c, ty') end
   1.105 +    val constraints = (map o apsnd) (fst o snd) operations;
   1.106 +
   1.107 +    (* check phase *)
   1.108 +    val typargs = Consts.typargs (ProofContext.consts_of ctxt);
   1.109 +    fun check_const (c, ty) ((t, _), (_, idx)) =
   1.110 +      ((nth (typargs (c, ty)) idx), t);
   1.111 +    fun local_operation (c_ty as (c, _)) = AList.lookup (op =) operations c
   1.112 +      |> Option.map (check_const c_ty);
   1.113  
   1.114 -fun remove_constraint class c ctxt =
   1.115 +    (* uncheck phase *)
   1.116 +    val proto_rews = map (fn (c, ((t, ty), _)) => (t, Const (c, ty))) operations;
   1.117 +    fun rew_app f (t1 $ t2) = rew_app f t1 $ f t2
   1.118 +      | rew_app f t = t;
   1.119 +    val rews = (map o apfst o rew_app)
   1.120 +      (Pattern.rewrite_term thy proto_rews []) proto_rews;
   1.121 +  in
   1.122 +    ctxt
   1.123 +    |> fold (ProofContext.add_const_constraint o local_constraint) operations
   1.124 +    |> ClassSyntax.map (K (SOME {
   1.125 +        constraints = constraints,
   1.126 +        base_sort = base_sort,
   1.127 +        local_operation = local_operation,
   1.128 +        rews = rews,
   1.129 +        passed = false
   1.130 +      }))
   1.131 +  end;
   1.132 +
   1.133 +fun refresh_syntax class ctxt =
   1.134    let
   1.135      val thy = ProofContext.theory_of ctxt;
   1.136      val base_sort = (#base_sort o the_class_data thy) class;
   1.137 -    val SOME entry = local_operation thy [class] c;
   1.138 -  in
   1.139 -    internal_remove_constraint base_sort (c, entry) ctxt
   1.140 -  end;
   1.141 +  in synchronize_syntax thy [class] base_sort ctxt end;
   1.142  
   1.143 -fun sort_term_check sups base_sort ts ctxt =
   1.144 +val mark_passed = (ClassSyntax.map o Option.map)
   1.145 +  (fn { constraints, base_sort, local_operation, rews, passed } =>
   1.146 +    { constraints = constraints, base_sort = base_sort,
   1.147 +      local_operation = local_operation, rews = rews, passed = true });
   1.148 +
   1.149 +fun sort_term_check ts ctxt =
   1.150    let
   1.151 -    val thy = ProofContext.theory_of ctxt;
   1.152 -    val local_operation = local_operation thy sups o fst;
   1.153 -    val typargs = Consts.typargs (ProofContext.consts_of ctxt);
   1.154 -    val constraints = these_operations thy sups |> (map o apsnd) (fst o snd);
   1.155 -    fun check_typ (c, ty) (TFree (v, _)) t = if v = Name.aT
   1.156 +    val { constraints, base_sort, local_operation, passed, ... } =
   1.157 +      the (ClassSyntax.get ctxt);
   1.158 +    fun check_typ (c, ty) (TFree (v, _), t) = if v = Name.aT
   1.159            then apfst (AList.update (op =) ((c, ty), t)) else I
   1.160 -      | check_typ (c, ty) (TVar (vi, _)) t = if TypeInfer.is_param vi
   1.161 +      | check_typ (c, ty) (TVar (vi, _), t) = if TypeInfer.is_param vi
   1.162            then apfst (AList.update (op =) ((c, ty), t))
   1.163              #> apsnd (insert (op =) vi) else I
   1.164 -      | check_typ _ _ _ = I;
   1.165 -    fun check_const (c, ty) ((t, _), (_, idx)) =
   1.166 -      check_typ (c, ty) (nth (typargs (c, ty)) idx) t;
   1.167 -    fun add_const (Const c_ty) = Option.map (check_const c_ty) (local_operation c_ty)
   1.168 +      | check_typ _ _ = I;
   1.169 +    fun add_const (Const c_ty) = Option.map (check_typ c_ty) (local_operation c_ty)
   1.170            |> the_default I
   1.171        | add_const _ = I;
   1.172      val (cs, typarams) = (fold o fold_aterms) add_const ts ([], []);
   1.173 @@ -603,45 +636,41 @@
   1.174          (fn t as Const (c, ty) => the_default t (AList.lookup (op =) cs (c, ty)) | t => t)
   1.175            #> map_types subst_typ;
   1.176      val ts' = map subst_term ts;
   1.177 -    val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
   1.178 -  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt') end;
   1.179 +  in if eq_list (op aconv) (ts, ts') andalso passed then NONE
   1.180 +  else
   1.181 +    ctxt
   1.182 +    |> fold (ProofContext.add_const_constraint o apsnd SOME) constraints
   1.183 +    |> mark_passed
   1.184 +    |> pair ts'
   1.185 +    |> SOME
   1.186 +  end;
   1.187  
   1.188  val uncheck = ref true;
   1.189  
   1.190 -fun sort_term_uncheck sups ts ctxt =
   1.191 +fun sort_term_uncheck ts ctxt =
   1.192    let
   1.193      (*FIXME abbreviations*)
   1.194      val thy = ProofContext.theory_of ctxt;
   1.195 -    fun rew_app f (t1 $ t2) = rew_app f t1 $ f t2
   1.196 -      | rew_app f t = t;
   1.197 -    val rews = map (fn (c, ((t, ty), _)) => (t, Const (c, ty))) (these_operations thy sups);
   1.198 -    val rews' = (map o apfst o rew_app) (Pattern.rewrite_term thy rews []) rews;
   1.199 -    val _ = map (Thm.cterm_of thy o Logic.mk_equals) rews';
   1.200 +    val rews = (#rews o the o ClassSyntax.get) ctxt;
   1.201      val ts' = if ! uncheck
   1.202 -      then map (Pattern.rewrite_term thy rews' []) ts else ts;
   1.203 +      then map (Pattern.rewrite_term thy rews []) ts else ts;
   1.204    in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
   1.205  
   1.206 -fun init_class_ctxt sups base_sort ctxt =
   1.207 -  let
   1.208 -    val operations = these_operations (ProofContext.theory_of ctxt) sups;
   1.209 -    fun standard_infer_types ts ctxt =
   1.210 -      let
   1.211 -        val ts' = ProofContext.standard_infer_types ctxt ts;
   1.212 -      in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
   1.213 -  in
   1.214 -    ctxt
   1.215 -    |> Variable.declare_term
   1.216 -        (Logic.mk_type (TFree (Name.aT, base_sort)))
   1.217 -    |> fold (internal_remove_constraint base_sort) operations
   1.218 -    |> Context.proof_map (Syntax.add_term_check 1 "class"
   1.219 -            (sort_term_check sups base_sort)
   1.220 -        #> Syntax.add_term_check 1 "standard" standard_infer_types
   1.221 -        #> Syntax.add_term_uncheck (~10) "class" (sort_term_uncheck sups))
   1.222 -  end;
   1.223 +fun init_ctxt thy sups base_sort ctxt =
   1.224 +  ctxt
   1.225 +  |> Variable.declare_term
   1.226 +      (Logic.mk_type (TFree (Name.aT, base_sort)))
   1.227 +  |> synchronize_syntax thy sups base_sort
   1.228 +  |> Context.proof_map (
   1.229 +      Syntax.add_term_check 0 "class" sort_term_check
   1.230 +      #> Syntax.add_term_uncheck (~10) "class" sort_term_uncheck)
   1.231  
   1.232  fun init class ctxt =
   1.233 -  init_class_ctxt [class]
   1.234 -    ((#base_sort o the_class_data (ProofContext.theory_of ctxt)) class) ctxt;
   1.235 +  let
   1.236 +    val thy = ProofContext.theory_of ctxt;
   1.237 +  in
   1.238 +    init_ctxt thy [class] ((#base_sort o the_class_data thy) class) ctxt
   1.239 +  end;
   1.240  
   1.241  
   1.242  (* class definition *)
   1.243 @@ -667,7 +696,7 @@
   1.244      ProofContext.init thy
   1.245      |> Locale.cert_expr supexpr [constrain]
   1.246      |> snd
   1.247 -    |> init_class_ctxt sups base_sort
   1.248 +    |> init_ctxt thy sups base_sort
   1.249      |> process_expr Locale.empty raw_elems
   1.250      |> fst
   1.251      |> (fn elems => ((((sups, supconsts), (supsort, base_sort, mergeexpr)),
   1.252 @@ -681,7 +710,8 @@
   1.253    let
   1.254      val superclasses = map (Sign.certify_class thy) raw_superclasses;
   1.255      val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
   1.256 -    fun add_const ((c, ty), syn) = Sign.declare_const [] (c, ty, syn) #>> Term.dest_Const;
   1.257 +    fun add_const ((c, ty), syn) =
   1.258 +      Sign.declare_const [] (c, Type.strip_sorts ty, syn) #>> Term.dest_Const;
   1.259      fun mk_axioms cs thy =
   1.260        raw_dep_axioms thy cs
   1.261        |> (map o apsnd o map) (Sign.cert_prop thy)
   1.262 @@ -773,36 +803,37 @@
   1.263  
   1.264  (* definition in class target *)
   1.265  
   1.266 -fun add_const_in_class class ((c, mx), rhs) thy =
   1.267 +fun add_logical_const class ((c, mx), dict) thy =
   1.268    let
   1.269      val prfx = class_prefix class;
   1.270      val thy' = thy |> Sign.add_path prfx;
   1.271      val phi = morphism thy' class;
   1.272  
   1.273      val c' = Sign.full_name thy' c;
   1.274 -    val rhs' = (map_types Logic.unvarifyT o Morphism.term phi) rhs;
   1.275 -    val ty' = Term.fastype_of rhs';
   1.276 -    val def = (c, Logic.mk_equals (Const (c', ty'), rhs'));
   1.277 +    val dict' = (map_types Logic.unvarifyT o Morphism.term phi) dict;
   1.278 +    val ty' = Term.fastype_of dict';
   1.279 +    val ty'' = Type.strip_sorts ty';
   1.280 +    val def_eq = Logic.mk_equals (Const (c', ty'), dict');
   1.281      val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
   1.282    in
   1.283      thy'
   1.284      |> Sign.hide_consts_i false [c'']
   1.285 -    |> Sign.declare_const [] (c, ty', mx) |> snd
   1.286 +    |> Sign.declare_const [] (c, ty'', mx) |> snd
   1.287      |> Sign.parent_path
   1.288      |> Sign.sticky_prefix prfx
   1.289 -    |> yield_singleton (PureThy.add_defs_i false) (def, [])
   1.290 +    |> Thm.add_def false (c, def_eq)
   1.291      |>> Thm.symmetric
   1.292 -    |-> (fn def => class_interpretation class [def]
   1.293 -                [(map_types Logic.unvarifyT o Thm.prop_of) def]
   1.294 -          #> register_operation class ((c', rhs), SOME def))
   1.295 +    |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
   1.296 +          #> register_operation class ((c', dict), SOME (Thm.varifyT def)))
   1.297      |> Sign.restore_naming thy
   1.298 +    |> Sign.add_const_constraint (c', SOME ty')
   1.299      |> pair c'
   1.300    end;
   1.301  
   1.302  
   1.303  (* abbreviation in class target *)
   1.304  
   1.305 -fun add_abbrev_in_class class prmode ((c, mx), rhs) thy =
   1.306 +fun add_syntactic_const class prmode ((c, mx), rhs) thy =
   1.307    let
   1.308      val prfx = class_prefix class;
   1.309      val phi = morphism thy class;
     2.1 --- a/src/Pure/Isar/theory_target.ML	Thu Oct 18 16:09:36 2007 +0200
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Oct 18 16:09:38 2007 +0200
     2.3 @@ -195,8 +195,9 @@
     2.4          val t = Term.list_comb (const, map Free xs);
     2.5        in (((c, mx12), t), thy') end;
     2.6      fun class_const ((c, _), _) ((_, (mx1, _)), t) =
     2.7 -      LocalTheory.raw_theory_result (Class.add_const_in_class target ((c, mx1), t))
     2.8 -      #-> LocalTheory.target o Class.remove_constraint target;
     2.9 +      LocalTheory.raw_theory_result (Class.add_logical_const target ((c, mx1), t))
    2.10 +      #> snd
    2.11 +      #> LocalTheory.target (Class.refresh_syntax target);
    2.12  
    2.13      val (abbrs, lthy') = lthy
    2.14        |> LocalTheory.theory_result (fold_map const decls)
    2.15 @@ -218,9 +219,10 @@
    2.16    |> LocalDefs.add_def ((c, NoSyn), t);
    2.17  
    2.18  fun class_abbrev target prmode ((c, mx), rhs) lthy = lthy   (* FIXME pos *)
    2.19 -  |> LocalTheory.raw_theory_result (Class.add_abbrev_in_class target prmode
    2.20 +  |> LocalTheory.raw_theory_result (Class.add_syntactic_const target prmode
    2.21        ((c, mx), rhs))
    2.22 -  |-> LocalTheory.target o Class.remove_constraint target;
    2.23 +  |> snd
    2.24 +  |> LocalTheory.target (Class.refresh_syntax target);
    2.25  
    2.26  in
    2.27