src/Pure/Isar/locale.ML
changeset 28259 5b2af04ec9fb
parent 28236 c447b60d67f5
child 28375 c879d88d038a
     1.1 --- a/src/Pure/Isar/locale.ML	Wed Sep 17 11:42:25 2008 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Sep 17 15:21:30 2008 +0200
     1.3 @@ -96,24 +96,32 @@
     1.4    val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
     1.5    val add_declaration: string -> declaration -> Proof.context -> Proof.context
     1.6  
     1.7 +  (* Interpretation *)
     1.8 +  val get_interpret_morph: theory -> string -> string ->
     1.9 +    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
    1.10 +    string -> term list -> Morphism.morphism
    1.11    val interpretation_i: (Proof.context -> Proof.context) ->
    1.12      bool * string -> expr ->
    1.13      term option list * (Attrib.binding * term) list ->
    1.14 -    theory -> Proof.state
    1.15 +    theory ->
    1.16 +    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
    1.17    val interpretation: (Proof.context -> Proof.context) ->
    1.18      bool * string -> expr ->
    1.19      string option list * (Attrib.binding * string) list ->
    1.20 -    theory -> Proof.state
    1.21 +    theory ->
    1.22 +    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
    1.23    val interpretation_in_locale: (Proof.context -> Proof.context) ->
    1.24      xstring * expr -> theory -> Proof.state
    1.25    val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
    1.26      bool * string -> expr ->
    1.27      term option list * (Attrib.binding * term) list ->
    1.28 -    bool -> Proof.state -> Proof.state
    1.29 +    bool -> Proof.state ->
    1.30 +    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
    1.31    val interpret: (Proof.state -> Proof.state Seq.seq) ->
    1.32      bool * string -> expr ->
    1.33      string option list * (Attrib.binding * string) list ->
    1.34 -    bool -> Proof.state -> Proof.state
    1.35 +    bool -> Proof.state ->
    1.36 +    (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
    1.37  end;
    1.38  
    1.39  structure Locale: LOCALE =
    1.40 @@ -240,8 +248,12 @@
    1.41        T * (term list * (((bool * string) * string) * Element.witness list)) list
    1.42      val add_witness: term list -> Element.witness -> T -> T
    1.43      val add_equation: term list -> thm -> T -> T
    1.44 -(*    val update_morph: term list -> Element.witness list * thm list -> T -> T *)
    1.45 -(*    val get_morph: theory -> T -> term list -> string list -> Morphism.morphism *)
    1.46 +(*
    1.47 +    val update_morph: term list -> Morphism.morphism -> T -> T
    1.48 +    val get_morph: theory -> T ->
    1.49 +      term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list)) ->
    1.50 +      Morphism.morphism
    1.51 +*)
    1.52    end =
    1.53  struct
    1.54    (* A registration is indexed by parameter instantiation.
    1.55 @@ -350,15 +362,6 @@
    1.56        (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m))
    1.57        ts regs;
    1.58  
    1.59 -  (* update morphism of registration;
    1.60 -     only if instantiation is exact, otherwise exception Option raised *)
    1.61 -(*
    1.62 -  fun update_morph ts (wits, eqns') regs =
    1.63 -    gen_add (fn (x, e, i, thms, eqns, _) =>
    1.64 -      (x, e, i, thms, eqns, (wits, eqns')))
    1.65 -      ts regs;
    1.66 -*)
    1.67 -
    1.68  end;
    1.69  
    1.70  
    1.71 @@ -1646,19 +1649,24 @@
    1.72    in ((tinst, inst), wits, eqns) end;
    1.73  
    1.74  
    1.75 -(* standardise export morphism *)
    1.76 -
    1.77 -(* clone from Element.generalize_facts *)
    1.78 -fun standardize thy export facts =
    1.79 +(* compute morphism and apply to args *)
    1.80 +
    1.81 +fun inst_morph thy prfx param_prfx insts prems eqns export =
    1.82    let
    1.83 +    (* standardise export morphism *)
    1.84      val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
    1.85      val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
    1.86        (* FIXME sync with exp_fact *)
    1.87      val exp_typ = Logic.type_map exp_term;
    1.88 -    val morphism =
    1.89 +    val export' =
    1.90        Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
    1.91 -  in Element.facts_map (Element.morph_ctxt morphism) facts end;
    1.92 -
    1.93 +  in
    1.94 +    Morphism.name_morphism (Name.qualified prfx o Name.qualified param_prfx) $>
    1.95 +      Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
    1.96 +      Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
    1.97 +      Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $>
    1.98 +      export'
    1.99 +  end;
   1.100  
   1.101  fun morph_ctxt' phi = Element.map_ctxt
   1.102    {name = I,
   1.103 @@ -1668,20 +1676,21 @@
   1.104     fact = Morphism.fact phi,
   1.105     attrib = Args.morph_values phi};
   1.106  
   1.107 -
   1.108 -(* compute morphism and apply to args *)
   1.109 -
   1.110 -fun inst_morph thy prfx param_prfx insts prems eqns =
   1.111 -  Morphism.name_morphism (Name.qualified prfx o Name.qualified param_prfx) $>
   1.112 -    Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
   1.113 -    Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
   1.114 -    Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns);
   1.115 -
   1.116 -fun interpret_args thy inst exp attrib args =
   1.117 -  args |> Element.facts_map (morph_ctxt' inst) |>
   1.118 -(* morph_ctxt' suppresses application of name morphism.  FIXME *)
   1.119 -    standardize thy exp |> Attrib.map_facts attrib;
   1.120 -
   1.121 +fun interpret_args thy inst attrib args =
   1.122 +  args |> Element.facts_map (morph_ctxt' inst) |> Attrib.map_facts attrib;
   1.123 +    (* morph_ctxt' suppresses application of name morphism.  FIXME *)
   1.124 +
   1.125 +(* public interface to interpretation morphism *)
   1.126 +
   1.127 +fun get_interpret_morph thy prfx param_prfx (exp, imp) target ext_ts =
   1.128 +  let
   1.129 +    val parms = the_locale thy target |> #params |> map fst;
   1.130 +    val ids = flatten (ProofContext.init thy, intern_expr thy)
   1.131 +      (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
   1.132 +    val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
   1.133 +  in
   1.134 +    inst_morph thy prfx param_prfx insts prems eqns exp
   1.135 +  end;
   1.136  
   1.137  (* store instantiations of args for all registered interpretations
   1.138     of the theory *)
   1.139 @@ -1700,7 +1709,7 @@
   1.140          val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
   1.141          val attrib = Attrib.attribute_i thy;
   1.142          val args' = args
   1.143 -          |> interpret_args thy (inst_morph thy prfx pprfx insts prems eqns) exp attrib
   1.144 +          |> interpret_args thy (inst_morph thy prfx pprfx insts prems eqns exp) attrib
   1.145            |> add_param_prefixss pprfx;
   1.146        in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
   1.147    in fold activate regs thy end;
   1.148 @@ -2110,7 +2119,7 @@
   1.149          let
   1.150            val ctxt = mk_ctxt thy_ctxt;
   1.151            val facts' = facts |>
   1.152 -              interpret_args (ProofContext.theory_of ctxt) inst exp (attrib thy_ctxt) |>
   1.153 +              interpret_args (ProofContext.theory_of ctxt) inst (attrib thy_ctxt) |>
   1.154                add_param_prefixss pprfx;
   1.155          in snd (note_interp kind loc prfx facts' thy_ctxt) end
   1.156        | activate_elem _ _ _ _ _ thy_ctxt = thy_ctxt;
   1.157 @@ -2125,7 +2134,7 @@
   1.158          val ids = flatten (ProofContext.init thy, intern_expr thy)
   1.159            (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst;
   1.160          val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts;
   1.161 -        val inst = inst_morph thy (snd prfx) pprfx insts prems eqns;
   1.162 +        val inst = inst_morph thy (snd prfx) pprfx insts prems eqns exp;
   1.163        in
   1.164          fold (activate_elem inst loc prfx pprfx) (map fst elems) thy_ctxt
   1.165        end;
   1.166 @@ -2284,7 +2293,9 @@
   1.167  
   1.168      val propss = map extract_asms_elems inst_elemss @ eqn_elems;
   1.169  
   1.170 -  in (propss, activate prfx inst_elemss (map (snd o fst) ids) propss eq_attns morphs) end;
   1.171 +  in
   1.172 +    (propss, activate prfx inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs)
   1.173 +  end;
   1.174  
   1.175  fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
   1.176    test_global_registration
   1.177 @@ -2416,7 +2427,7 @@
   1.178  fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
   1.179    (* prfx = (flag indicating full qualification, name prefix) *)
   1.180    let
   1.181 -    val (propss, activate) = prep_registration thy prfx raw_expr raw_insts;
   1.182 +    val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts;
   1.183      fun after_qed' results =
   1.184        ProofContext.theory (activate (prep_result propss results))
   1.185        #> after_qed;
   1.186 @@ -2426,6 +2437,7 @@
   1.187      |> Proof.theorem_i NONE after_qed' (prep_propp propss)
   1.188      |> Element.refine_witness
   1.189      |> Seq.hd
   1.190 +    |> pair morphs
   1.191    end;
   1.192  
   1.193  fun gen_interpret prep_registration after_qed prfx expr insts int state =
   1.194 @@ -2433,7 +2445,7 @@
   1.195    let
   1.196      val _ = Proof.assert_forward_or_chain state;
   1.197      val ctxt = Proof.context_of state;
   1.198 -    val (propss, activate) = prep_registration ctxt prfx expr insts;
   1.199 +    val (propss, activate, morphs) = prep_registration ctxt prfx expr insts;
   1.200      fun after_qed' results =
   1.201        Proof.map_context (K (ctxt |> activate (prep_result propss results)))
   1.202        #> Proof.put_facts NONE
   1.203 @@ -2443,6 +2455,7 @@
   1.204      |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
   1.205        "interpret" NONE after_qed' (map (pair (Name.no_binding, [])) (prep_propp propss))
   1.206      |> Element.refine_witness |> Seq.hd
   1.207 +    |> pair morphs
   1.208    end;
   1.209  
   1.210  in