src/Pure/sign.ML
changeset 1501 bb7f99a0a6f0
parent 1494 22f67e796445
child 1576 af8f43f742a0
     1.1 --- a/src/Pure/sign.ML	Fri Feb 16 12:19:47 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Feb 16 12:34:18 1996 +0100
     1.3 @@ -6,84 +6,71 @@
     1.4  *)
     1.5  
     1.6  signature SIGN =
     1.7 -sig
     1.8 -  structure Symtab: SYMTAB
     1.9 -  structure Syntax: SYNTAX
    1.10 -  structure Type: TYPE
    1.11 -  sharing Symtab = Type.Symtab
    1.12 -  local open Type Syntax in
    1.13 -    type sg
    1.14 -    val rep_sg: sg ->
    1.15 -      {tsig: type_sig,
    1.16 -       const_tab: typ Symtab.table,
    1.17 -       syn: syntax,
    1.18 -       stamps: string ref list}
    1.19 -    val subsig: sg * sg -> bool
    1.20 -    val eq_sg: sg * sg -> bool
    1.21 -    val same_sg: sg * sg -> bool
    1.22 -    val is_draft: sg -> bool
    1.23 -    val const_type: sg -> string -> typ option
    1.24 -    val classes: sg -> class list
    1.25 -    val subsort: sg -> sort * sort -> bool
    1.26 -    val nodup_Vars: term -> unit
    1.27 -    val norm_sort: sg -> sort -> sort
    1.28 -    val nonempty_sort: sg -> sort list -> sort -> bool
    1.29 -    val print_sg: sg -> unit
    1.30 -    val pretty_sg: sg -> Pretty.T
    1.31 -    val pprint_sg: sg -> pprint_args -> unit
    1.32 -    val pretty_term: sg -> term -> Pretty.T
    1.33 -    val pretty_typ: sg -> typ -> Pretty.T
    1.34 -    val pretty_sort: sort -> Pretty.T
    1.35 -    val string_of_term: sg -> term -> string
    1.36 -    val string_of_typ: sg -> typ -> string
    1.37 -    val pprint_term: sg -> term -> pprint_args -> unit
    1.38 -    val pprint_typ: sg -> typ -> pprint_args -> unit
    1.39 -    val certify_typ: sg -> typ -> typ
    1.40 -    val certify_term: sg -> term -> term * typ * int
    1.41 -    val read_typ: sg * (indexname -> sort option) -> string -> typ
    1.42 -    val exn_type_msg: sg -> string * typ list * term list -> string
    1.43 -    val infer_types: sg -> (indexname -> typ option) ->
    1.44 -      (indexname -> sort option) -> string list -> bool
    1.45 -      -> term list * typ -> int * term * (indexname * typ) list
    1.46 -    val add_classes: (class * class list) list -> sg -> sg
    1.47 -    val add_classrel: (class * class) list -> sg -> sg
    1.48 -    val add_defsort: sort -> sg -> sg
    1.49 -    val add_types: (string * int * mixfix) list -> sg -> sg
    1.50 -    val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
    1.51 -    val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg
    1.52 -    val add_arities: (string * sort list * sort) list -> sg -> sg
    1.53 -    val add_consts: (string * string * mixfix) list -> sg -> sg
    1.54 -    val add_consts_i: (string * typ * mixfix) list -> sg -> sg
    1.55 -    val add_syntax: (string * string * mixfix) list -> sg -> sg
    1.56 -    val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
    1.57 -    val add_trfuns:
    1.58 -      (string * (ast list -> ast)) list *
    1.59 -      (string * (term list -> term)) list *
    1.60 -      (string * (term list -> term)) list *
    1.61 -      (string * (ast list -> ast)) list -> sg -> sg
    1.62 -    val add_trrules: (string * string) trrule list -> sg -> sg
    1.63 -    val add_trrules_i: ast trrule list -> sg -> sg
    1.64 -    val add_name: string -> sg -> sg
    1.65 -    val make_draft: sg -> sg
    1.66 -    val merge: sg * sg -> sg
    1.67 -    val proto_pure: sg
    1.68 -    val pure: sg
    1.69 -    val cpure: sg
    1.70 -    val const_of_class: class -> string
    1.71 -    val class_of_const: string -> class
    1.72 -  end
    1.73 -end;
    1.74 +  sig
    1.75 +  type sg
    1.76 +  val rep_sg: sg -> {tsig: Type.type_sig,
    1.77 +		     const_tab: typ Symtab.table,
    1.78 +		     syn: Syntax.syntax,
    1.79 +		     stamps: string ref list}
    1.80 +  val subsig: sg * sg -> bool
    1.81 +  val eq_sg: sg * sg -> bool
    1.82 +  val same_sg: sg * sg -> bool
    1.83 +  val is_draft: sg -> bool
    1.84 +  val const_type: sg -> string -> typ option
    1.85 +  val classes: sg -> class list
    1.86 +  val subsort: sg -> sort * sort -> bool
    1.87 +  val nodup_Vars: term -> unit
    1.88 +  val norm_sort: sg -> sort -> sort
    1.89 +  val nonempty_sort: sg -> sort list -> sort -> bool
    1.90 +  val print_sg: sg -> unit
    1.91 +  val pretty_sg: sg -> Pretty.T
    1.92 +  val pprint_sg: sg -> pprint_args -> unit
    1.93 +  val pretty_term: sg -> term -> Pretty.T
    1.94 +  val pretty_typ: sg -> typ -> Pretty.T
    1.95 +  val pretty_sort: sort -> Pretty.T
    1.96 +  val string_of_term: sg -> term -> string
    1.97 +  val string_of_typ: sg -> typ -> string
    1.98 +  val pprint_term: sg -> term -> pprint_args -> unit
    1.99 +  val pprint_typ: sg -> typ -> pprint_args -> unit
   1.100 +  val certify_typ: sg -> typ -> typ
   1.101 +  val certify_term: sg -> term -> term * typ * int
   1.102 +  val read_typ: sg * (indexname -> sort option) -> string -> typ
   1.103 +  val exn_type_msg: sg -> string * typ list * term list -> string
   1.104 +  val infer_types: sg -> (indexname -> typ option) ->
   1.105 +    (indexname -> sort option) -> string list -> bool
   1.106 +    -> term list * typ -> int * term * (indexname * typ) list
   1.107 +  val add_classes: (class * class list) list -> sg -> sg
   1.108 +  val add_classrel: (class * class) list -> sg -> sg
   1.109 +  val add_defsort: sort -> sg -> sg
   1.110 +  val add_types: (string * int * mixfix) list -> sg -> sg
   1.111 +  val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
   1.112 +  val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg
   1.113 +  val add_arities: (string * sort list * sort) list -> sg -> sg
   1.114 +  val add_consts: (string * string * mixfix) list -> sg -> sg
   1.115 +  val add_consts_i: (string * typ * mixfix) list -> sg -> sg
   1.116 +  val add_syntax: (string * string * mixfix) list -> sg -> sg
   1.117 +  val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
   1.118 +  val add_trfuns:
   1.119 +    (string * (ast list -> ast)) list *
   1.120 +    (string * (term list -> term)) list *
   1.121 +    (string * (term list -> term)) list *
   1.122 +    (string * (ast list -> ast)) list -> sg -> sg
   1.123 +  val add_trrules: (string * string) trrule list -> sg -> sg
   1.124 +  val add_trrules_i: ast trrule list -> sg -> sg
   1.125 +  val add_name: string -> sg -> sg
   1.126 +  val make_draft: sg -> sg
   1.127 +  val merge: sg * sg -> sg
   1.128 +  val proto_pure: sg
   1.129 +  val pure: sg
   1.130 +  val cpure: sg
   1.131 +  val const_of_class: class -> string
   1.132 +  val class_of_const: string -> class
   1.133 +  end;
   1.134  
   1.135 -functor SignFun(structure Syntax: SYNTAX and Type: TYPE): SIGN =
   1.136 +structure Sign : SIGN =
   1.137  struct
   1.138  
   1.139 -structure Symtab = Type.Symtab;
   1.140 -structure Syntax = Syntax;
   1.141 -structure BasicSyntax: BASIC_SYNTAX = Syntax;
   1.142 -structure Pretty = Syntax.Pretty;
   1.143 -structure Type = Type;
   1.144 -open BasicSyntax Type;
   1.145 -
   1.146 +local open Type Syntax in
   1.147  
   1.148  (** datatype sg **)
   1.149  
   1.150 @@ -92,7 +79,7 @@
   1.151  
   1.152  datatype sg =
   1.153    Sg of {
   1.154 -    tsig: type_sig,                 (*order-sorted signature of types*)
   1.155 +    tsig: Type.type_sig,                 (*order-sorted signature of types*)
   1.156      const_tab: typ Symtab.table,    (*types of constants*)
   1.157      syn: Syntax.syntax,             (*syntax for parsing and printing*)
   1.158      stamps: string ref list};       (*unique theory indentifier*)
   1.159 @@ -605,4 +592,5 @@
   1.160    |> add_syntax Syntax.pure_applC_syntax
   1.161    |> add_name "CPure";
   1.162  
   1.163 +end
   1.164  end;