src/Pure/Isar/class.ML
changeset 26730 bbb5e6904d78
parent 26642 454d11701fa4
child 26761 190da765a628
equal deleted inserted replaced
26729:43a72d892594 26730:bbb5e6904d78
   189       end;
   189       end;
   190   in maps params o ancestry thy end;
   190   in maps params o ancestry thy end;
   191 
   191 
   192 fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
   192 fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
   193 
   193 
   194 fun partial_morphism thy class = #morphism (the_class_data thy class) thy [];
       
   195 fun morphism thy class = #morphism (the_class_data thy class) thy (these_defs thy [class]);
   194 fun morphism thy class = #morphism (the_class_data thy class) thy (these_defs thy [class]);
   196 
   195 
   197 fun these_assm_intros thy =
   196 fun these_assm_intros thy =
   198   Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
   197   Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
   199     ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) [];
   198     ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) [];
   436     val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) operations;
   435     val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) operations;
   437   in
   436   in
   438     ctxt
   437     ctxt
   439     |> fold declare_const primary_constraints
   438     |> fold declare_const primary_constraints
   440     |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints),
   439     |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints),
   441         ((improve, subst), unchecks)), false))
   440         (((improve, subst), true), unchecks)), false))
   442     |> Overloading.set_primary_constraints
   441     |> Overloading.set_primary_constraints
   443   end;
   442   end;
   444 
   443 
   445 fun refresh_syntax class ctxt =
   444 fun refresh_syntax class ctxt =
   446   let
   445   let
   579 
   578 
   580 fun declare class pos ((c, mx), dict) thy =
   579 fun declare class pos ((c, mx), dict) thy =
   581   let
   580   let
   582     val prfx = class_prefix class;
   581     val prfx = class_prefix class;
   583     val thy' = thy |> Sign.add_path prfx;
   582     val thy' = thy |> Sign.add_path prfx;
   584     val phi = partial_morphism thy' class;
   583     val phi = morphism thy' class;
   585 
   584 
   586     val c' = Sign.full_name thy' c;
   585     val c' = Sign.full_name thy' c;
   587     val dict' = Morphism.term phi dict;
   586     val dict' = Morphism.term phi dict;
   588     val dict_def = map_types Logic.unvarifyT dict';
   587     val dict_def = map_types Logic.unvarifyT dict';
   589     val ty' = Term.fastype_of dict_def;
   588     val ty' = Term.fastype_of dict_def;
   606 
   605 
   607 fun abbrev class prmode pos ((c, mx), rhs) thy =
   606 fun abbrev class prmode pos ((c, mx), rhs) thy =
   608   let
   607   let
   609     val prfx = class_prefix class;
   608     val prfx = class_prefix class;
   610     val thy' = thy |> Sign.add_path prfx;
   609     val thy' = thy |> Sign.add_path prfx;
   611     val phi = morphism thy class;
   610 
   612 
   611     val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
       
   612       (these_operations thy [class]);
   613     val c' = Sign.full_name thy' c;
   613     val c' = Sign.full_name thy' c;
   614     val rhs' = Morphism.term phi rhs;
   614     val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
   615     val ty' = Logic.unvarifyT (Term.fastype_of rhs');
   615     val rhs'' = map_types Logic.varifyT rhs';
       
   616     val ty' = Term.fastype_of rhs';
   616   in
   617   in
   617     thy'
   618     thy'
   618     |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') |> snd
   619     |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs'') |> snd
   619     |> Sign.add_const_constraint (c', SOME ty')
   620     |> Sign.add_const_constraint (c', SOME ty')
   620     |> Sign.notation true prmode [(Const (c', ty'), mx)]
   621     |> Sign.notation true prmode [(Const (c', ty'), mx)]
   621     |> register_operation class (c', (rhs', NONE))
   622     |> register_operation class (c', (rhs', NONE))
   622     |> Sign.restore_naming thy
   623     |> Sign.restore_naming thy
   623   end;
   624   end;
   671     val unchecks =
   672     val unchecks =
   672       map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
   673       map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
   673   in
   674   in
   674     ctxt
   675     ctxt
   675     |> Overloading.map_improvable_syntax
   676     |> Overloading.map_improvable_syntax
   676          (fn (((primary_constraints, _), ((improve, _), _)), _) =>
   677          (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
   677             (((primary_constraints, []), ((improve, subst), unchecks)), false))
   678             (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
   678   end;
   679   end;
   679 
   680 
   680 
   681 
   681 (* target *)
   682 (* target *)
   682 
   683 
   742     |> Instantiation.put (mk_instantiation ((tycos, vs, sort), inst_params))
   743     |> Instantiation.put (mk_instantiation ((tycos, vs, sort), inst_params))
   743     |> fold (Variable.declare_term o Logic.mk_type o TFree) vs
   744     |> fold (Variable.declare_term o Logic.mk_type o TFree) vs
   744     |> fold (Variable.declare_names o Free o snd) inst_params
   745     |> fold (Variable.declare_names o Free o snd) inst_params
   745     |> (Overloading.map_improvable_syntax o apfst)
   746     |> (Overloading.map_improvable_syntax o apfst)
   746          (fn ((_, _), ((_, subst), unchecks)) =>
   747          (fn ((_, _), ((_, subst), unchecks)) =>
   747             ((primary_constraints, []), ((improve, K NONE), [])))
   748             ((primary_constraints, []), (((improve, K NONE), false), [])))
   748     |> Overloading.add_improvable_syntax
   749     |> Overloading.add_improvable_syntax
   749     |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
   750     |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
   750     |> synchronize_inst_syntax
   751     |> synchronize_inst_syntax
   751   end;
   752   end;
   752 
   753