read/check_specification: proper type inference across multiple sections, result is in closed form;
authorwenzelm
Wed Sep 26 19:17:59 2007 +0200 (2007-09-26)
changeset 247240df74bb87a13
parent 24723 2110df1e157d
child 24725 04b676d1a1fe
read/check_specification: proper type inference across multiple sections, result is in closed form;
added read/check_free_specification for single section, non-closed form;
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Wed Sep 26 19:17:58 2007 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Wed Sep 26 19:17:59 2007 +0200
     1.3 @@ -11,13 +11,21 @@
     1.4    val quiet_mode: bool ref
     1.5    val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
     1.6    val read_specification: (string * string option * mixfix) list ->
     1.7 -    ((string * Attrib.src list) * string list) list -> local_theory ->
     1.8 +    ((string * Attrib.src list) * string list) list list -> Proof.context ->
     1.9 +    (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
    1.10 +    Proof.context
    1.11 +  val check_specification: (string * typ option * mixfix) list ->
    1.12 +    ((string * Attrib.src list) * term list) list list -> Proof.context ->
    1.13      (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
    1.14 -    local_theory
    1.15 -  val cert_specification: (string * typ option * mixfix) list ->
    1.16 -    ((string * Attrib.src list) * term list) list -> local_theory ->
    1.17 +    Proof.context
    1.18 +  val read_free_specification: (string * string option * mixfix) list ->
    1.19 +    ((string * Attrib.src list) * string list) list -> Proof.context ->
    1.20      (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
    1.21 -    local_theory
    1.22 +    Proof.context
    1.23 +  val check_free_specification: (string * typ option * mixfix) list ->
    1.24 +    ((string * Attrib.src list) * term list) list -> Proof.context ->
    1.25 +    (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
    1.26 +    Proof.context
    1.27    val axiomatization: (string * string option * mixfix) list ->
    1.28      ((bstring * Attrib.src list) * string list) list -> local_theory ->
    1.29      (term list * (bstring * thm list) list) * local_theory
    1.30 @@ -69,51 +77,94 @@
    1.31  
    1.32  (* prepare specification *)
    1.33  
    1.34 -fun prep_specification prep_vars prep_propp prep_att raw_vars raw_specs ctxt =
    1.35 +local
    1.36 +
    1.37 +fun close_forms ctxt i xs As =
    1.38 +  let
    1.39 +    fun add_free (Free (x, _)) = if Variable.is_fixed ctxt x then I else insert (op =) x
    1.40 +      | add_free _ = I;
    1.41 +
    1.42 +    val commons = map #1 xs;
    1.43 +    val _ =
    1.44 +      (case duplicates (op =) commons of [] => ()
    1.45 +      | dups => error ("Duplicate local variables " ^ commas_quote dups));
    1.46 +    val frees = rev ((fold o fold_aterms) add_free As (rev commons));
    1.47 +    val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context "'a" (length frees));
    1.48 +    val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
    1.49 +
    1.50 +    fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
    1.51 +      | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
    1.52 +      | abs_body lev y (t as Free (x, T)) =
    1.53 +          if x = y then TypeInfer.constrain (uniform_typing x) (TypeInfer.constrain T (Bound lev))
    1.54 +          else t
    1.55 +      | abs_body _ _ a = a;
    1.56 +    fun close (y, U) B =
    1.57 +      let val B' = abs_body 0 y (Term.incr_boundvars 1 B)
    1.58 +      in if Term.loose_bvar1 (B', 0) then Term.all dummyT $ Abs (y, U, B') else B end;
    1.59 +    fun close_form A =
    1.60 +      let
    1.61 +        val occ_frees = rev (fold_aterms add_free A []);
    1.62 +        val bounds = xs @ map (rpair dummyT) (subtract (op =) commons occ_frees);
    1.63 +      in fold_rev close bounds A end;
    1.64 +  in map close_form As end;
    1.65 +
    1.66 +fun prep_spec prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
    1.67    let
    1.68      val thy = ProofContext.theory_of ctxt;
    1.69  
    1.70      val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
    1.71      val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
    1.72 -    val ((specs, vs), specs_ctxt) =
    1.73 -      prep_propp (params_ctxt, map (map (rpair []) o snd) raw_specs)
    1.74 -      |> swap |>> map (map fst)
    1.75 -      ||>> fold_map ProofContext.inferred_param xs;
    1.76  
    1.77 +    val Asss = (map o map) (map (parse_prop params_ctxt) o snd) raw_specss;
    1.78 +    val idx = (fold o fold o fold) Term.maxidx_term Asss ~1 + 1;
    1.79 +    val specs =
    1.80 +      (if do_close then
    1.81 +        #1 (fold_map (fn Ass => fn i => (burrow (close_forms params_ctxt i []) Ass, i + 1)) Asss idx)
    1.82 +      else Asss)
    1.83 +      |> flat |> burrow (Syntax.check_props params_ctxt);
    1.84 +    val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
    1.85 +
    1.86 +    val vs = specs_ctxt |> fold_map ProofContext.inferred_param xs |> fst;
    1.87      val params = vs ~~ map #3 vars;
    1.88 -    val names = map (fst o fst) raw_specs;
    1.89 -    val atts = map (map (prep_att thy) o snd o fst) raw_specs;
    1.90 -  in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end;
    1.91 +    val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss);
    1.92 +  in ((params, name_atts ~~ specs), specs_ctxt) end;
    1.93 +
    1.94 +fun read_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src x;
    1.95 +fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) x;
    1.96  
    1.97 -fun read_specification x =
    1.98 -  prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.intern_src x;
    1.99 +in
   1.100  
   1.101 -fun cert_specification x =
   1.102 -  prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x;
   1.103 +fun read_specification x = read_spec true x;
   1.104 +fun check_specification x = check_spec true x;
   1.105 +fun read_free_specification vars specs = read_spec false vars [specs];
   1.106 +fun check_free_specification vars specs = check_spec false vars [specs];
   1.107 +
   1.108 +end;
   1.109  
   1.110  
   1.111  (* axiomatization *)
   1.112  
   1.113  fun gen_axioms prep raw_vars raw_specs lthy =
   1.114    let
   1.115 -    val (vars, specs) = fst (prep raw_vars raw_specs lthy);
   1.116 +    val (vars, specs) = fst (prep raw_vars [raw_specs] lthy);
   1.117      val cs = map fst vars;
   1.118 -    val spec_frees = member (op =) (fold (fold Term.add_frees o snd) specs []);
   1.119 +    val spec_frees = member (op =) ((fold (fold Term.add_frees o snd) specs []));
   1.120  
   1.121 -    val ((consts, axioms), lthy') = lthy
   1.122 +    val ((constants, axioms), lthy') = lthy
   1.123        |> LocalTheory.consts spec_frees vars
   1.124 -      ||> fold (fold Variable.auto_fixes o snd) specs   (* FIXME !? *)
   1.125        ||>> LocalTheory.axioms Thm.axiomK specs;
   1.126 +    val consts = map #1 constants;
   1.127 +    val consts' = map (Morphism.term (LocalTheory.target_morphism lthy')) consts;
   1.128  
   1.129      (* FIXME generic target!? *)
   1.130 -    val hs = map (Term.head_of o #2 o Logic.dest_equals o Thm.prop_of o #2) consts;
   1.131 +    val hs = map (Term.head_of o #2 o Logic.dest_equals o Thm.prop_of o #2) constants;
   1.132      val lthy'' = lthy' |> LocalTheory.theory (Theory.add_finals_i false hs);
   1.133  
   1.134 -    val _ = print_consts lthy' spec_frees cs;
   1.135 -  in ((map #1 consts, axioms), lthy'') end;
   1.136 +    val _ = print_consts lthy' (member (op =) (fold Term.add_frees consts' [])) cs;
   1.137 +  in ((consts, axioms), lthy'') end;
   1.138  
   1.139  val axiomatization = gen_axioms read_specification;
   1.140 -val axiomatization_i = gen_axioms cert_specification;
   1.141 +val axiomatization_i = gen_axioms check_specification;
   1.142  
   1.143  
   1.144  (* definition *)
   1.145 @@ -137,8 +188,8 @@
   1.146      val _ = print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
   1.147    in ((lhs, (b, th')), lthy3) end;
   1.148  
   1.149 -val definition = gen_def read_specification;
   1.150 -val definition_i = gen_def cert_specification;
   1.151 +val definition = gen_def read_free_specification;
   1.152 +val definition_i = gen_def check_free_specification;
   1.153  
   1.154  
   1.155  (* abbreviation *)
   1.156 @@ -156,11 +207,12 @@
   1.157        |> ProofContext.set_syntax_mode mode    (* FIXME !? *)
   1.158        |> LocalTheory.abbrev mode ((x, mx), rhs) |> snd
   1.159        |> ProofContext.restore_syntax_mode lthy;
   1.160 +
   1.161      val _ = print_consts lthy' (K false) [(x, T)]
   1.162    in lthy' end;
   1.163  
   1.164 -val abbreviation = gen_abbrev read_specification;
   1.165 -val abbreviation_i = gen_abbrev cert_specification;
   1.166 +val abbreviation = gen_abbrev read_free_specification;
   1.167 +val abbreviation_i = gen_abbrev check_free_specification;
   1.168  
   1.169  
   1.170  (* notation *)