src/Pure/sign.ML
changeset 3805 a50d0b5219dd
parent 3791 c5db2c87a646
child 3810 350150bd3744
     1.1 --- a/src/Pure/sign.ML	Tue Oct 07 17:58:50 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Oct 07 18:02:02 1997 +0200
     1.3 @@ -5,6 +5,13 @@
     1.4  The abstract type "sg" of signatures.
     1.5  *)
     1.6  
     1.7 +(*external forms*)
     1.8 +type xstring = string;
     1.9 +type xclass = class;
    1.10 +type xsort = sort;
    1.11 +type xtyp = typ;
    1.12 +type xterm = term;
    1.13 +
    1.14  signature SIGN =
    1.15  sig
    1.16    type sg
    1.17 @@ -26,17 +33,17 @@
    1.18    val norm_sort: sg -> sort -> sort
    1.19    val nonempty_sort: sg -> sort list -> sort -> bool
    1.20    val long_names: bool ref
    1.21 -  val intern_class: sg -> class -> class
    1.22 -  val extern_class: sg -> class -> class
    1.23 -  val intern_sort: sg -> sort -> sort
    1.24 -  val extern_sort: sg -> sort -> sort
    1.25 -  val intern_typ: sg -> typ -> typ
    1.26 -  val extern_typ: sg -> typ -> typ
    1.27 -  val intern_term: sg -> term -> term
    1.28 -  val extern_term: sg -> term -> term
    1.29 -  val intern_tycons: sg -> typ -> typ
    1.30 -  val intern_tycon: sg -> string -> string
    1.31 -  val intern_const: sg -> string -> string
    1.32 +  val intern_class: sg -> xclass -> class
    1.33 +  val extern_class: sg -> class -> xclass
    1.34 +  val intern_sort: sg -> xsort -> sort
    1.35 +  val extern_sort: sg -> sort -> xsort
    1.36 +  val intern_typ: sg -> xtyp -> typ
    1.37 +  val extern_typ: sg -> typ -> xtyp
    1.38 +  val intern_term: sg -> xterm -> term
    1.39 +  val extern_term: sg -> term -> xterm
    1.40 +  val intern_tycons: sg -> xtyp -> typ
    1.41 +  val intern_tycon: sg -> xstring -> string
    1.42 +  val intern_const: sg -> xstring -> string
    1.43    val print_sg: sg -> unit
    1.44    val pretty_sg: sg -> Pretty.T
    1.45    val pprint_sg: sg -> pprint_args -> unit
    1.46 @@ -53,24 +60,24 @@
    1.47    val read_typ: sg * (indexname -> sort option) -> string -> typ
    1.48    val infer_types: sg -> (indexname -> typ option) ->
    1.49      (indexname -> sort option) -> string list -> bool
    1.50 -    -> term list * typ -> int * term * (indexname * typ) list
    1.51 -  val add_classes: (class * class list) list -> sg -> sg
    1.52 -  val add_classes_i: (class * class list) list -> sg -> sg
    1.53 -  val add_classrel: (class * class) list -> sg -> sg
    1.54 +    -> xterm list * typ -> int * term * (indexname * typ) list
    1.55 +  val add_classes: (xclass * xclass list) list -> sg -> sg
    1.56 +  val add_classes_i: (xclass * class list) list -> sg -> sg
    1.57 +  val add_classrel: (xclass * xclass) list -> sg -> sg
    1.58    val add_classrel_i: (class * class) list -> sg -> sg
    1.59 -  val add_defsort: sort -> sg -> sg
    1.60 +  val add_defsort: xsort -> sg -> sg
    1.61    val add_defsort_i: sort -> sg -> sg
    1.62 -  val add_types: (string * int * mixfix) list -> sg -> sg
    1.63 -  val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
    1.64 -  val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg
    1.65 -  val add_arities: (string * sort list * sort) list -> sg -> sg
    1.66 +  val add_types: (xstring * int * mixfix) list -> sg -> sg
    1.67 +  val add_tyabbrs: (xstring * string list * string * mixfix) list -> sg -> sg
    1.68 +  val add_tyabbrs_i: (xstring * string list * typ * mixfix) list -> sg -> sg
    1.69 +  val add_arities: (xstring * xsort list * xsort) list -> sg -> sg
    1.70    val add_arities_i: (string * sort list * sort) list -> sg -> sg
    1.71 -  val add_consts: (string * string * mixfix) list -> sg -> sg
    1.72 -  val add_consts_i: (string * typ * mixfix) list -> sg -> sg
    1.73 -  val add_syntax: (string * string * mixfix) list -> sg -> sg
    1.74 -  val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
    1.75 -  val add_modesyntax: (string * bool) * (string * string * mixfix) list -> sg -> sg
    1.76 -  val add_modesyntax_i: (string * bool) * (string * typ * mixfix) list -> sg -> sg
    1.77 +  val add_consts: (xstring * string * mixfix) list -> sg -> sg
    1.78 +  val add_consts_i: (xstring * typ * mixfix) list -> sg -> sg
    1.79 +  val add_syntax: (xstring * string * mixfix) list -> sg -> sg
    1.80 +  val add_syntax_i: (xstring * typ * mixfix) list -> sg -> sg
    1.81 +  val add_modesyntax: (string * bool) * (xstring * string * mixfix) list -> sg -> sg
    1.82 +  val add_modesyntax_i: (string * bool) * (xstring * typ * mixfix) list -> sg -> sg
    1.83    val add_trfuns:
    1.84      (string * (ast list -> ast)) list *
    1.85      (string * (term list -> term)) list *
    1.86 @@ -83,7 +90,7 @@
    1.87    val add_trrules: (string * string) Syntax.trrule list -> sg -> sg
    1.88    val add_trrules_i: ast Syntax.trrule list -> sg -> sg
    1.89    val add_path: string -> sg -> sg
    1.90 -  val add_space: string * string list -> sg -> sg
    1.91 +  val add_space: string * xstring list -> sg -> sg
    1.92    val add_name: string -> sg -> sg
    1.93    val make_draft: sg -> sg
    1.94    val merge: sg * sg -> sg
    1.95 @@ -102,9 +109,9 @@
    1.96  datatype sg =
    1.97    Sg of {
    1.98      tsig: Type.type_sig,                        (*order-sorted signature of types*)
    1.99 -    const_tab: typ Symtab.table,                (*types of constants*)
   1.100 +    const_tab: typ Symtab.table,                (*type schemes of constants*)
   1.101      syn: Syntax.syntax,                         (*syntax for parsing and printing*)
   1.102 -    path: string list,                     	(*current position in name space*)
   1.103 +    path: string list,                     	(*current name space entry prefix*)
   1.104      spaces: (string * NameSpace.T) list,   	(*name spaces for consts, types etc.*)
   1.105      stamps: string ref list};                   (*unique theory indentifier*)
   1.106  
   1.107 @@ -172,7 +179,7 @@
   1.108  
   1.109  (** name spaces **)
   1.110  
   1.111 -(*prune names by default*)
   1.112 +(*prune names on output by default*)
   1.113  val long_names = ref false;
   1.114  
   1.115  
   1.116 @@ -203,12 +210,8 @@
   1.117  
   1.118  (* intern / extern names *)
   1.119  
   1.120 -(*Note: These functions are not necessarily idempotent!*)	(* FIXME *)
   1.121 -
   1.122  local
   1.123  
   1.124 -  (* FIXME move to term.ML? *)
   1.125 -
   1.126    fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes (Ts, cs)
   1.127      | add_typ_classes (TFree (_, S), cs) = S union cs
   1.128      | add_typ_classes (TVar (_, S), cs) = S union cs;
   1.129 @@ -273,6 +276,9 @@
   1.130    val intrn_term = trn_term o intrn;
   1.131    val extrn_term = trn_term o extrn;
   1.132  
   1.133 +  fun intrn_tycons spaces T =
   1.134 +    map_typ I (mapping (intrn spaces typeK) add_typ_tycons T) T;
   1.135 +
   1.136    val intern_class = intrn_class o spaces_of;
   1.137    val extern_class = extrn_class o spaces_of;
   1.138    val intern_sort = intrn_sort o spaces_of;
   1.139 @@ -282,9 +288,6 @@
   1.140    val intern_term = intrn_term o spaces_of;
   1.141    val extern_term = extrn_term o spaces_of;
   1.142  
   1.143 -  fun intrn_tycons spaces T =
   1.144 -    map_typ I (mapping (intrn spaces typeK) add_typ_tycons T) T;
   1.145 -
   1.146    fun intern_tycon sg = intrn (spaces_of sg) typeK;
   1.147    fun intern_const sg = intrn (spaces_of sg) constK;
   1.148    val intern_tycons = intrn_tycons o spaces_of;
   1.149 @@ -335,7 +338,7 @@
   1.150      fun pretty_const (c, ty) = Pretty.block
   1.151        [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ ty];
   1.152  
   1.153 -    val Sg {tsig, const_tab, syn, path, spaces, stamps} = sg;
   1.154 +    val Sg {tsig, const_tab, syn = _, path, spaces, stamps} = sg;
   1.155      val {classes, classrel, default, tycons, abbrs, arities} =
   1.156        Type.rep_tsig tsig;
   1.157    in
   1.158 @@ -493,7 +496,8 @@
   1.159  fun infer_types sg def_type def_sort used freeze (ts, T) =
   1.160    let
   1.161      val Sg {tsig, ...} = sg;
   1.162 -    val prt = setmp Syntax.show_brackets true (pretty_term sg);
   1.163 +    val prt = setmp Syntax.show_brackets true
   1.164 +      (fn _ => setmp long_names true pretty_term sg) ();
   1.165      val prT = pretty_typ sg;
   1.166      val infer = Type.infer_types prt prT tsig (const_type sg) def_type def_sort
   1.167        (intern_const sg) (intern_tycons sg) (intern_sort sg) used freeze;
   1.168 @@ -503,9 +507,8 @@
   1.169      fun warn () =
   1.170        if length ts > 1 andalso length ts <= ! Syntax.ambiguity_level
   1.171        then (*no warning shown yet*)
   1.172 -        warning "Currently parsed input \
   1.173 -          \produces more than one parse tree.\n\
   1.174 -          \For more information lower Syntax.ambiguity_level."
   1.175 +        warning "Got more than one parse tree.\n\
   1.176 +          \Retry with smaller Syntax.ambiguity_level for more information."
   1.177        else ();
   1.178  
   1.179      datatype result =
   1.180 @@ -528,7 +531,7 @@
   1.181        One res =>
   1.182         (if length ts > ! Syntax.ambiguity_level then
   1.183            warning "Fortunately, only one parse tree is type correct.\n\
   1.184 -            \It helps (speed!) if you disambiguate your grammar or your input."
   1.185 +            \You may still want to disambiguate your grammar or your input."
   1.186          else (); res)
   1.187      | Errs errs => (warn (); error (cat_lines errs))
   1.188      | Ambigs us =>
   1.189 @@ -579,10 +582,10 @@
   1.190      val abbrs' =
   1.191        map (fn (t, vs, rhs, mx) =>
   1.192          (full_name path (Syntax.type_name t mx), vs, rhs)) abbrs;
   1.193 -    val space' = add_names spaces typeK (map #1 abbrs');
   1.194 -    val decls = map (rd_abbr syn' tsig space') abbrs';
   1.195 +    val spaces' = add_names spaces typeK (map #1 abbrs');
   1.196 +    val decls = map (rd_abbr syn' tsig spaces') abbrs';
   1.197    in
   1.198 -    (syn', Type.ext_tsig_abbrs tsig decls, ctab, (path, spaces))
   1.199 +    (syn', Type.ext_tsig_abbrs tsig decls, ctab, (path, spaces'))
   1.200    end;
   1.201  
   1.202  fun ext_tyabbrs abbrs = ext_abbrs read_abbr abbrs;
   1.203 @@ -605,6 +608,9 @@
   1.204  
   1.205  (* add term constants and syntax *)
   1.206  
   1.207 +fun const_name path c mx =
   1.208 +  full_name path (Syntax.const_name c mx);
   1.209 +
   1.210  fun err_in_const c =
   1.211    error ("in declaration of constant " ^ quote c);
   1.212  
   1.213 @@ -612,18 +618,18 @@
   1.214    error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
   1.215  
   1.216  
   1.217 -fun read_const syn tsig spaces (c, ty_src, mx) =
   1.218 +fun read_const syn tsig (path, spaces) (c, ty_src, mx) =
   1.219    (c, read_raw_typ syn tsig spaces (K None) ty_src, mx)
   1.220 -    handle ERROR => err_in_const (Syntax.const_name c mx);
   1.221 +    handle ERROR => err_in_const (const_name path c mx);
   1.222  
   1.223  fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab, (path, spaces)) raw_consts =
   1.224    let
   1.225      fun prep_const (c, ty, mx) =
   1.226        (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
   1.227          handle TYPE (msg, _, _) =>
   1.228 -          (error_msg msg; err_in_const (Syntax.const_name c mx));
   1.229 +          (error_msg msg; err_in_const (const_name path c mx));
   1.230  
   1.231 -    val consts = map (prep_const o rd_const syn tsig spaces) raw_consts;
   1.232 +    val consts = map (prep_const o rd_const syn tsig (path, spaces)) raw_consts;
   1.233      val decls =
   1.234        if syn_only then []
   1.235        else decls_of path Syntax.const_name consts;
   1.236 @@ -758,9 +764,9 @@
   1.237  
   1.238  
   1.239  
   1.240 -(** merge signatures **)    (*exception TERM*) (*exception ERROR (* FIXME *) handle_error? *)
   1.241 +(** merge signatures **)    (*exception TERM*)
   1.242  
   1.243 -fun merge (sg1, sg2) =
   1.244 +fun merge_aux (sg1, sg2) =
   1.245    if fast_subsig (sg2, sg1) then sg1
   1.246    else if fast_subsig (sg1, sg2) then sg2
   1.247    else if subsig (sg2, sg1) then sg1
   1.248 @@ -801,6 +807,11 @@
   1.249          path = path, spaces = spaces, stamps = stamps}
   1.250      end;
   1.251  
   1.252 +fun merge sgs =
   1.253 +  (case handle_error merge_aux sgs of
   1.254 +    OK sg => sg
   1.255 +  | Error msg => raise TERM (msg, []));
   1.256 +
   1.257  
   1.258  
   1.259  (** the Pure signature **)
   1.260 @@ -812,7 +823,7 @@
   1.261      ("prop", 0, NoSyn) ::
   1.262      ("itself", 1, NoSyn) ::
   1.263      Syntax.pure_types)
   1.264 -  |> add_classes_i [(logicC, [])]
   1.265 +  |> add_classes_i [(NameSpace.base logicC, [])]
   1.266    |> add_defsort_i logicS
   1.267    |> add_arities_i
   1.268     [("fun", [logicS, logicS], logicS),