export consts_of;
authorwenzelm
Tue Feb 07 19:56:49 2006 +0100 (2006-02-07)
changeset 18967ea42ab6c08d1
parent 18966 dc49d8b18886
child 18968 52639ad19a96
export consts_of;
removed const_expansion;
pretty_term', infer_types(_simult): separate Consts.T argument;
added generic certify;
simplified certify_term/prop;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Tue Feb 07 19:56:48 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Feb 07 19:56:49 2006 +0100
     1.3 @@ -25,8 +25,8 @@
     1.4    val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
     1.5    val add_consts: (bstring * string * mixfix) list -> theory -> theory
     1.6    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
     1.7 -  val add_abbrevs: (bstring * string * mixfix) list -> theory -> theory
     1.8 -  val add_abbrevs_i: (bstring * term * mixfix) list -> theory -> theory
     1.9 +  val add_abbrevs: bool -> (bstring * string * mixfix) list -> theory -> theory
    1.10 +  val add_abbrevs_i: bool -> (bstring * term * mixfix) list -> theory -> theory
    1.11    val add_const_constraint: xstring * string -> theory -> theory
    1.12    val add_const_constraint_i: string * typ -> theory -> theory
    1.13    val add_classes: (bstring * xstring list) list -> theory -> theory
    1.14 @@ -109,6 +109,7 @@
    1.15    val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv
    1.16    val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int
    1.17    val is_logtype: theory -> string -> bool
    1.18 +  val consts_of: theory -> Consts.T
    1.19    val const_constraint: theory -> string -> typ option
    1.20    val the_const_constraint: theory -> string -> typ
    1.21    val const_type: theory -> string -> typ option
    1.22 @@ -118,7 +119,6 @@
    1.23    val const_monomorphic: theory -> string -> bool
    1.24    val const_typargs: theory -> string * typ -> typ list
    1.25    val const_instance: theory -> string * typ list -> typ
    1.26 -  val const_expansion: theory -> string * typ -> term option
    1.27    val class_space: theory -> NameSpace.T
    1.28    val type_space: theory -> NameSpace.T
    1.29    val const_space: theory -> NameSpace.T
    1.30 @@ -133,9 +133,8 @@
    1.31    val intern_typ: theory -> typ -> typ
    1.32    val extern_typ: theory -> typ -> typ
    1.33    val intern_term: theory -> term -> term
    1.34 -  val extern_term: theory -> term -> term
    1.35    val intern_tycons: theory -> typ -> typ
    1.36 -  val pretty_term': Syntax.syntax -> Context.generic -> term -> Pretty.T
    1.37 +  val pretty_term': Syntax.syntax -> Consts.T -> Context.generic -> term -> Pretty.T
    1.38    val pretty_term: theory -> term -> Pretty.T
    1.39    val pretty_typ: theory -> typ -> Pretty.T
    1.40    val pretty_sort: theory -> sort -> Pretty.T
    1.41 @@ -154,8 +153,9 @@
    1.42    val certify_typ: theory -> typ -> typ
    1.43    val certify_typ_syntax: theory -> typ -> typ
    1.44    val certify_typ_abbrev: theory -> typ -> typ
    1.45 -  val certify_term: Pretty.pp -> theory -> term -> term * typ * int
    1.46 -  val certify_prop: Pretty.pp -> theory -> term -> term * typ * int
    1.47 +  val certify: bool -> bool -> Pretty.pp -> theory -> term -> term * typ * int
    1.48 +  val certify_term: theory -> term -> term * typ * int
    1.49 +  val certify_prop: theory -> term -> term * typ * int
    1.50    val cert_term: theory -> term -> term
    1.51    val cert_prop: theory -> term -> term
    1.52    val no_vars: Pretty.pp -> term -> term
    1.53 @@ -173,14 +173,14 @@
    1.54    val read_typ_abbrev: theory * (indexname -> sort option) -> string -> typ
    1.55    val read_tyname: theory -> string -> typ
    1.56    val read_const: theory -> string -> term
    1.57 -  val infer_types_simult: Pretty.pp -> theory -> (indexname -> typ option) ->
    1.58 +  val infer_types_simult: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) ->
    1.59      (indexname -> sort option) -> string list -> bool
    1.60      -> (term list * typ) list -> term list * (indexname * typ) list
    1.61 -  val infer_types: Pretty.pp -> theory -> (indexname -> typ option) ->
    1.62 +  val infer_types: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) ->
    1.63      (indexname -> sort option) -> string list -> bool
    1.64      -> term list * typ -> term * (indexname * typ) list
    1.65 -  val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Context.generic ->
    1.66 -    (indexname -> typ option) * (indexname -> sort option) ->
    1.67 +  val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Consts.T ->
    1.68 +    Context.generic -> (indexname -> typ option) * (indexname -> sort option) ->
    1.69      string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
    1.70    val read_def_terms:
    1.71      theory * (indexname -> typ option) * (indexname -> sort option) ->
    1.72 @@ -288,7 +288,6 @@
    1.73  val const_monomorphic = Consts.monomorphic o consts_of;
    1.74  val const_typargs = Consts.typargs o consts_of;
    1.75  val const_instance = Consts.instance o consts_of;
    1.76 -fun const_expansion thy = Consts.expansion (tsig_of thy) (consts_of thy);
    1.77  
    1.78  val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of;
    1.79  val declared_const = is_some oo const_type;
    1.80 @@ -299,7 +298,7 @@
    1.81  
    1.82  val class_space = #1 o #classes o Type.rep_tsig o tsig_of;
    1.83  val type_space = #1 o #types o Type.rep_tsig o tsig_of;
    1.84 -val const_space = Consts.space o consts_of;
    1.85 +val const_space = Consts.space_of o consts_of;
    1.86  
    1.87  val intern_class = NameSpace.intern o class_space;
    1.88  val extern_class = NameSpace.extern o class_space;
    1.89 @@ -347,7 +346,7 @@
    1.90  val intern_typ = typ_mapping intern_class intern_type;
    1.91  val extern_typ = typ_mapping extern_class extern_type;
    1.92  val intern_term = term_mapping intern_class intern_type intern_const;
    1.93 -val extern_term = term_mapping extern_class extern_type extern_const;
    1.94 +val extern_term = term_mapping extern_class extern_type;
    1.95  val intern_tycons = typ_mapping (K I) intern_type;
    1.96  
    1.97  end;
    1.98 @@ -356,13 +355,14 @@
    1.99  
   1.100  (** pretty printing of terms, types etc. **)
   1.101  
   1.102 -fun pretty_term' syn context t =
   1.103 +fun pretty_term' syn consts context t =
   1.104    let
   1.105      val thy = Context.theory_of context;
   1.106      val curried = Context.exists_name Context.CPureN thy;
   1.107 -  in Syntax.pretty_term context syn curried (extern_term thy t) end;
   1.108 +    val extern = NameSpace.extern (Consts.space_of consts);
   1.109 +  in Syntax.pretty_term context syn curried (extern_term (K extern) thy t) end;
   1.110  
   1.111 -fun pretty_term thy t = pretty_term' (syn_of thy) (Context.Theory thy) t;
   1.112 +fun pretty_term thy t = pretty_term' (syn_of thy) (consts_of thy) (Context.Theory thy) t;
   1.113  
   1.114  fun pretty_typ thy T = Syntax.pretty_typ (Context.Theory thy) (syn_of thy) (extern_typ thy T);
   1.115  fun pretty_sort thy S = Syntax.pretty_sort (Context.Theory thy) (syn_of thy) (extern_sort thy S);
   1.116 @@ -405,11 +405,10 @@
   1.117  val certify_typ_abbrev = certify Type.cert_typ_abbrev;
   1.118  
   1.119  
   1.120 -(* certify_term *)
   1.121 +(* certify term/prop *)
   1.122  
   1.123  local
   1.124  
   1.125 -(*determine and check the type of a term*)
   1.126  fun type_check pp tm =
   1.127    let
   1.128      fun err_appl why bs t T u U =
   1.129 @@ -434,37 +433,37 @@
   1.130                  if T1 = U then T2 else err_appl "Incompatible operand type" bs t T u U
   1.131              | _ => err_appl "Operator not of function type" bs t T u U)
   1.132            end;
   1.133 +  in typ_of ([], tm) end;
   1.134  
   1.135 -  in typ_of ([], tm) end;
   1.136 +fun err msg = raise TYPE (msg, [], []);
   1.137 +
   1.138 +fun check_vars (t $ u) = (check_vars t; check_vars u)
   1.139 +  | check_vars (Abs (_, _, t)) = check_vars t
   1.140 +  | check_vars (Var (xi as (_, i), _)) =
   1.141 +      if i < 0 then err ("Malformed variable: " ^ quote (Term.string_of_vname xi)) else ()
   1.142 +  | check_vars _ = ();
   1.143  
   1.144  in
   1.145  
   1.146 -fun certify_term pp thy tm =
   1.147 +fun certify normalize prop pp thy tm =
   1.148    let
   1.149      val _ = Context.check_thy thy;
   1.150 -
   1.151 -    fun check_vars (t $ u) = (check_vars t; check_vars u)
   1.152 -      | check_vars (Abs (_, _, t)) = check_vars t
   1.153 -      | check_vars (t as Var ((x, i), _)) =
   1.154 -          if i < 0 then raise TYPE ("Malformed variable: " ^ quote x, [], [t]) else ()
   1.155 -      | check_vars _ = ();
   1.156 +    val _ = check_vars tm;
   1.157 +    val tm' = Term.map_term_types (certify_typ thy) tm;
   1.158 +    val T = type_check pp tm';
   1.159 +    val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
   1.160 +    val tm'' = Consts.certify pp (tsig_of thy) (consts_of thy) tm';
   1.161 +    val tm'' = if normalize then tm'' else tm';
   1.162 +  in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
   1.163  
   1.164 -    val tm' = tm
   1.165 -      |> map_term_types (certify_typ thy)
   1.166 -      |> Consts.certify pp (tsig_of thy) (consts_of thy)
   1.167 -      |> tap check_vars;
   1.168 -    val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
   1.169 -  in (tm', type_check pp tm', maxidx_of_term tm') end;
   1.170 +fun certify_term thy = certify true false (pp thy) thy;
   1.171 +fun certify_prop thy = certify true true (pp thy) thy;
   1.172 +
   1.173 +val cert_term = #1 oo certify_term;
   1.174 +val cert_prop = #1 oo certify_prop;
   1.175  
   1.176  end;
   1.177  
   1.178 -fun certify_prop pp thy tm =
   1.179 -  let val res as (tm', T, _) = certify_term pp thy tm
   1.180 -  in if T <> propT then raise TYPE ("Term not of type prop", [T], [tm']) else res end;
   1.181 -
   1.182 -fun cert_term thy tm = #1 (certify_term (pp thy) thy tm);
   1.183 -fun cert_prop thy tm = #1 (certify_prop (pp thy) thy tm);
   1.184 -
   1.185  
   1.186  (* specifications *)
   1.187  
   1.188 @@ -538,11 +537,7 @@
   1.189      | _ => error ("Undeclared type constructor: " ^ quote c))
   1.190    end;
   1.191  
   1.192 -fun read_const thy raw_c =
   1.193 -  let
   1.194 -    val c = intern_const thy raw_c;
   1.195 -    val _ = the_const_type thy c handle TYPE (msg, _, _) => error msg;
   1.196 -  in Const (c, dummyT) end;
   1.197 +val read_const = Consts.read_const o consts_of;
   1.198  
   1.199  
   1.200  
   1.201 @@ -558,15 +553,16 @@
   1.202    typs: expected types
   1.203  *)
   1.204  
   1.205 -fun infer_types_simult pp thy def_type def_sort used freeze args =
   1.206 +fun infer_types_simult pp thy consts def_type def_sort used freeze args =
   1.207    let
   1.208      val termss = fold_rev (multiply o fst) args [[]];
   1.209      val typs =
   1.210        map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
   1.211  
   1.212      fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
   1.213 -        (const_constraint thy) def_type def_sort (intern_const thy) (intern_tycons thy)
   1.214 -        (intern_sort thy) used freeze typs ts)
   1.215 +        (try (Consts.constraint consts)) def_type def_sort
   1.216 +        (NameSpace.intern (Consts.space_of consts))
   1.217 +        (intern_tycons thy) (intern_sort thy) used freeze typs ts)
   1.218        handle TYPE (msg, _, _) => Exn (ERROR msg);
   1.219  
   1.220      val err_results = map infer termss;
   1.221 @@ -590,22 +586,23 @@
   1.222        cat_lines (map (Pretty.string_of_term pp) (List.concat (map fst results)))))
   1.223    end;
   1.224  
   1.225 -fun infer_types pp thy def_type def_sort used freeze tsT =
   1.226 -  apfst hd (infer_types_simult pp thy def_type def_sort used freeze [tsT]);
   1.227 +fun infer_types pp thy consts def_type def_sort used freeze tsT =
   1.228 +  apfst hd (infer_types_simult pp thy consts def_type def_sort used freeze [tsT]);
   1.229  
   1.230  
   1.231  (* read_def_terms -- read terms and infer types *)    (*exception ERROR*)
   1.232  
   1.233 -fun read_def_terms' pp is_logtype syn context (types, sorts) used freeze sTs =
   1.234 +fun read_def_terms' pp is_logtype syn consts context (types, sorts) used freeze sTs =
   1.235    let
   1.236      val thy = Context.theory_of context;
   1.237      fun read (s, T) =
   1.238        let val T' = certify_typ thy T handle TYPE (msg, _, _) => error msg
   1.239        in (Syntax.read context is_logtype syn T' s, T') end;
   1.240 -  in infer_types_simult pp thy types sorts used freeze (map read sTs) end;
   1.241 +  in infer_types_simult pp thy consts types sorts used freeze (map read sTs) end;
   1.242  
   1.243  fun read_def_terms (thy, types, sorts) =
   1.244 -  read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (Context.Theory thy) (types, sorts);
   1.245 +  read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (consts_of thy)
   1.246 +    (Context.Theory thy) (types, sorts);
   1.247  
   1.248  fun simple_read_term thy T s =
   1.249    let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
   1.250 @@ -731,7 +728,7 @@
   1.251  
   1.252  local
   1.253  
   1.254 -fun gen_add_abbrevs prep_term raw_args thy =
   1.255 +fun gen_add_abbrevs prep_term revert raw_args thy =
   1.256    let
   1.257      val prep_tm =
   1.258        Compress.term thy o Logic.varify o no_vars (pp thy) o Term.no_dummy_patterns o prep_term thy;
   1.259 @@ -744,7 +741,7 @@
   1.260      val (abbrs, syn) = split_list (map prep raw_args);
   1.261    in
   1.262      thy
   1.263 -    |> map_consts (fold (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy)) abbrs)
   1.264 +    |> map_consts (fold (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) revert) abbrs)
   1.265      |> add_syntax_i syn
   1.266    end;
   1.267