src/Pure/sign.ML
changeset 16494 6961e8ab33e1
parent 16442 1171ecf7fb7e
child 16536 c5744af6b28a
     1.1 --- a/src/Pure/sign.ML	Mon Jun 20 22:14:07 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon Jun 20 22:14:08 2005 +0200
     1.3 @@ -133,6 +133,9 @@
     1.4    val certify_typ_syntax: theory -> typ -> typ
     1.5    val certify_typ_abbrev: theory -> typ -> typ
     1.6    val certify_term: Pretty.pp -> theory -> term -> term * typ * int
     1.7 +  val certify_prop: Pretty.pp -> theory -> term -> term * typ * int
     1.8 +  val cert_term: theory -> term -> term
     1.9 +  val cert_prop: theory -> term -> term
    1.10    val read_sort': Syntax.syntax -> theory -> string -> sort
    1.11    val read_sort: theory -> string -> sort
    1.12    val read_typ': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
    1.13 @@ -156,6 +159,8 @@
    1.14      theory * (indexname -> typ option) * (indexname -> sort option) ->
    1.15      string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
    1.16    val simple_read_term: theory -> typ -> string -> term
    1.17 +  val read_term: theory -> string -> term
    1.18 +  val read_prop: theory -> string -> term
    1.19    val const_of_class: class -> string
    1.20    val class_of_const: string -> class
    1.21    include SIGN_THEORY
    1.22 @@ -464,6 +469,13 @@
    1.23  
    1.24  end;
    1.25  
    1.26 +fun certify_prop pp thy tm =
    1.27 +  let val res as (tm', T, _) = certify_term pp thy tm
    1.28 +  in if T <> propT then raise TYPE ("Term not of type prop", [T], [tm']) else res end;
    1.29 +
    1.30 +fun cert_term thy tm = #1 (certify_term (pp thy) thy tm);
    1.31 +fun cert_prop thy tm = #1 (certify_prop (pp thy) thy tm);
    1.32 +
    1.33  
    1.34  
    1.35  (** read and certify entities **)    (*exception ERROR*)
    1.36 @@ -575,8 +587,7 @@
    1.37    apfst hd (infer_types_simult pp thy def_type def_sort used freeze [tsT]);
    1.38  
    1.39  
    1.40 -
    1.41 -(** read_def_terms -- read terms and infer types **)    (*exception ERROR*)
    1.42 +(* read_def_terms -- read terms and infer types *)    (*exception ERROR*)
    1.43  
    1.44  fun read_def_terms' pp is_logtype syn (thy, types, sorts) used freeze sTs =
    1.45    let
    1.46 @@ -593,6 +604,9 @@
    1.47    in t end
    1.48    handle ERROR => error ("The error(s) above occurred for term " ^ s);
    1.49  
    1.50 +fun read_term thy = simple_read_term thy TypeInfer.logicT;
    1.51 +fun read_prop thy = simple_read_term thy propT;
    1.52 +
    1.53  
    1.54  
    1.55  (** signature extension functions **)  (*exception ERROR/TYPE*)