src/Pure/sign.ML
changeset 19 929ad32d63fc
parent 0 a5a9c433f639
child 143 f8152ca36cd5
     1.1 --- a/src/Pure/sign.ML	Mon Oct 04 15:30:49 1993 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Oct 04 15:36:31 1993 +0100
     1.3 @@ -1,13 +1,13 @@
     1.4 -(*  Title: 	sign
     1.5 +(*  Title:      Pure/sign.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1992  University of Cambridge
    1.10  
    1.11    the abstract types "sg" (signatures)
    1.12    and "cterm" (certified terms under a signature)
    1.13  *)
    1.14  
    1.15 -signature SIGN = 
    1.16 +signature SIGN =
    1.17  sig
    1.18    structure Type: TYPE
    1.19    structure Symtab: SYMTAB
    1.20 @@ -20,25 +20,25 @@
    1.21    val cterm_of: sg -> term -> cterm
    1.22    val ctyp_of: sg -> typ -> ctyp
    1.23    val extend: sg -> string ->
    1.24 -	(class * class list) list * class list *
    1.25 -	(string list * int) list *
    1.26 -	(string list * (sort list * class)) list *
    1.27 -	(string list * string)list * Syntax.sext option -> sg
    1.28 +        (class * class list) list * class list *
    1.29 +        (string list * int) list *
    1.30 +        (string list * (sort list * class)) list *
    1.31 +        (string list * string)list * Syntax.sext option -> sg
    1.32    val merge: sg * sg -> sg
    1.33    val pure: sg
    1.34    val read_cterm: sg -> string * typ -> cterm
    1.35    val read_ctyp: sg -> string -> ctyp
    1.36    val read_insts: sg -> (indexname -> typ option) * (indexname -> sort option)
    1.37 -	          -> (indexname -> typ option) * (indexname -> sort option)
    1.38 -		  -> (string*string)list
    1.39 -		  -> (indexname*ctyp)list * (cterm*cterm)list
    1.40 +                  -> (indexname -> typ option) * (indexname -> sort option)
    1.41 +                  -> (string*string)list
    1.42 +                  -> (indexname*ctyp)list * (cterm*cterm)list
    1.43    val read_typ: sg * (indexname -> sort option) -> string -> typ
    1.44    val rep_cterm: cterm -> {T: typ, t: term, sign: sg, maxidx: int}
    1.45    val rep_ctyp: ctyp -> {T: typ, sign: sg}
    1.46    val rep_sg: sg -> {tsig: Type.type_sig,
    1.47 -		     const_tab: typ Symtab.table,
    1.48 -		     syn: Syntax.syntax,
    1.49 -		     stamps: string ref list}
    1.50 +                     const_tab: typ Symtab.table,
    1.51 +                     syn: Syntax.syntax,
    1.52 +                     stamps: string ref list}
    1.53    val string_of_cterm: cterm -> string
    1.54    val string_of_ctyp: ctyp -> string
    1.55    val pprint_cterm: cterm -> pprint_args -> unit
    1.56 @@ -53,7 +53,7 @@
    1.57  end;
    1.58  
    1.59  
    1.60 -functor SignFun (structure Type:TYPE and Syntax:SYNTAX) : SIGN = 
    1.61 +functor SignFun (structure Type:TYPE and Syntax:SYNTAX) : SIGN =
    1.62  struct
    1.63  structure Type = Type;
    1.64  structure Symtab = Type.Symtab;
    1.65 @@ -61,11 +61,11 @@
    1.66  structure Pretty = Syntax.Pretty
    1.67  
    1.68  (*Signatures of theories. *)
    1.69 -datatype sg = 
    1.70 -  Sg of {tsig: Type.type_sig,		(* order-sorted signature of types *)
    1.71 -	 const_tab: typ Symtab.table,	(*types of constants*)
    1.72 -	 syn: Syntax.syntax,		(*Parsing and printing operations*)
    1.73 -	 stamps: string ref list	(*unique theory indentifier*)  };
    1.74 +datatype sg =
    1.75 +  Sg of {tsig: Type.type_sig,           (* order-sorted signature of types *)
    1.76 +         const_tab: typ Symtab.table,   (*types of constants*)
    1.77 +         syn: Syntax.syntax,            (*Parsing and printing operations*)
    1.78 +         stamps: string ref list        (*unique theory indentifier*)  };
    1.79  
    1.80  
    1.81  fun rep_sg (Sg args) = args;
    1.82 @@ -76,24 +76,24 @@
    1.83  
    1.84  (*Is constant present in table with more generic type?*)
    1.85  fun valid_const tsig ctab (a,T) = case Symtab.lookup(ctab, a) of
    1.86 -	Some U => Type.typ_instance(tsig,T,U) | _ => false;
    1.87 +        Some U => Type.typ_instance(tsig,T,U) | _ => false;
    1.88  
    1.89  
    1.90  (*Check a term for errors.  Are all constants and types valid in signature?
    1.91    Does not check that term is well-typed!*)
    1.92 -fun term_errors (sign as Sg{tsig,const_tab,...}) = 
    1.93 +fun term_errors (sign as Sg{tsig,const_tab,...}) =
    1.94  let val showtyp = string_of_typ sign;
    1.95      fun terrs (Const (a,T), errs) =
    1.96 -	if valid_const tsig const_tab (a,T)
    1.97 -	then Type.type_errors (tsig,showtyp) (T,errs)
    1.98 -	else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
    1.99 +        if valid_const tsig const_tab (a,T)
   1.100 +        then Type.type_errors (tsig,showtyp) (T,errs)
   1.101 +        else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
   1.102        | terrs (Free (_,T), errs) = Type.type_errors (tsig,showtyp) (T,errs)
   1.103        | terrs (Var  ((a,i),T), errs) =
   1.104 -	if  i>=0  then  Type.type_errors (tsig,showtyp) (T,errs)
   1.105 -	else  ("Negative index for Var: " ^ a) :: errs
   1.106 +        if  i>=0  then  Type.type_errors (tsig,showtyp) (T,errs)
   1.107 +        else  ("Negative index for Var: " ^ a) :: errs
   1.108        | terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
   1.109 -      | terrs (Abs (_,T,t), errs) = 
   1.110 -	    Type.type_errors(tsig,showtyp)(T,terrs(t,errs))
   1.111 +      | terrs (Abs (_,T,t), errs) =
   1.112 +            Type.type_errors(tsig,showtyp)(T,terrs(t,errs))
   1.113        | terrs (f$t, errs) = terrs(f, terrs (t,errs))
   1.114  in  terrs  end;
   1.115  
   1.116 @@ -102,7 +102,7 @@
   1.117  
   1.118  
   1.119  (*Reset TVar indices to zero, renaming to preserve distinctness*)
   1.120 -fun zero_tvar_indices tsig T = 
   1.121 +fun zero_tvar_indices tsig T =
   1.122    let val inxSs = typ_tvars T;
   1.123        val nms' = variantlist(map (#1 o #1) inxSs,[]);
   1.124        val tye = map (fn ((v,S),a) => (v, TVar((a,0),S))) (inxSs ~~ nms')
   1.125 @@ -116,16 +116,16 @@
   1.126  let val showtyp = Syntax.string_of_typ syn;
   1.127      fun read [] = []
   1.128        | read((cs,s)::pairs) =
   1.129 -	let val t = Syntax.read syn Syntax.typeT s handle ERROR =>
   1.130 -	            error("The error above occurred in type " ^ s);
   1.131 -	    val S = Type.defaultS tsig;
   1.132 -	    val T = Type.varifyT(Syntax.typ_of_term (K S) t)
   1.133 -	    val T0 = zero_tvar_indices tsig T;
   1.134 -	in (case Type.type_errors (tsig,showtyp) (T0,[]) of
   1.135 -		[] => (cs,T0) :: read pairs
   1.136 -	    | errs => error (cat_lines
   1.137 - 	   (("Error in type of constants " ^ space_implode " " cs) :: errs)))
   1.138 -	end
   1.139 +        let val t = Syntax.read syn Syntax.typeT s handle ERROR =>
   1.140 +                    error("The error above occurred in type " ^ quote s);
   1.141 +            val S = Type.defaultS tsig;
   1.142 +            val T = Type.varifyT(Syntax.typ_of_term (K S) t)
   1.143 +            val T0 = zero_tvar_indices tsig T;
   1.144 +        in (case Type.type_errors (tsig,showtyp) (T0,[]) of
   1.145 +                [] => (cs,T0) :: read pairs
   1.146 +            | errs => error (cat_lines
   1.147 +           (("Error in type of constants " ^ space_implode " " cs) :: errs)))
   1.148 +        end
   1.149  in read end;
   1.150  
   1.151  
   1.152 @@ -134,11 +134,11 @@
   1.153    The "ref" in stamps ensures that no two signatures are identical --
   1.154    it is impossible to forge a signature.  *)
   1.155  fun extend (Sg{tsig, const_tab, syn, stamps, ...}) signame
   1.156 -	   (newclasses, newdefault, otypes, newtypes, const_decs, osext) : sg =
   1.157 +           (newclasses, newdefault, otypes, newtypes, const_decs, osext) : sg =
   1.158  let val tsig' = Type.extend(tsig,newclasses,newdefault,otypes,newtypes);
   1.159      val S = Type.defaultS tsig';
   1.160      val roots = filter (Type.logical_type tsig')
   1.161 -		       (distinct(flat(map #1 newtypes)))
   1.162 +                       (distinct(flat(map #1 newtypes)))
   1.163      val xconsts = map #1 newclasses @ flat (map #1 otypes) @ flat (map #1 const_decs);
   1.164      val syn' =
   1.165        case osext of
   1.166 @@ -146,20 +146,20 @@
   1.167        | None => if null roots andalso null xconsts then syn
   1.168                  else Syntax.extend (syn, K S) (roots, xconsts, Syntax.empty_sext);
   1.169      val sconsts = case osext of
   1.170 -		    Some(sext) => Syntax.constants sext
   1.171 -		  | None => [];
   1.172 +                    Some(sext) => Syntax.constants sext
   1.173 +                  | None => [];
   1.174      val const_decs' = read_consts(tsig',syn') (sconsts @ const_decs)
   1.175  in Sg{tsig= tsig',
   1.176        const_tab= Symtab.st_of_declist (const_decs', const_tab)
   1.177 -		 handle Symtab.DUPLICATE(a) =>
   1.178 -		 error("Constant '" ^ a ^ "' declared twice"), 
   1.179 +                 handle Symtab.DUPLICATE(a) =>
   1.180 +                 error("Constant " ^ quote a ^ " declared twice"),
   1.181        syn=syn', stamps= ref signame :: stamps}
   1.182  end;
   1.183  
   1.184  
   1.185  (* The empty signature *)
   1.186  val sg0 = Sg{tsig= Type.tsig0, const_tab= Symtab.null,
   1.187 -	     syn=Syntax.type_syn,  stamps= []};
   1.188 +             syn=Syntax.type_syn,  stamps= []};
   1.189  
   1.190  (*The pure signature*)
   1.191  val pure : sg = extend sg0 "Pure"
   1.192 @@ -181,20 +181,20 @@
   1.193  (*Update table with (a,x) providing any existing asgt to "a" equals x. *)
   1.194  fun update_eq ((a,x),tab) =
   1.195      case Symtab.lookup(tab,a) of
   1.196 -	None => Symtab.update((a,x), tab)
   1.197 -      | Some y => if x=y then tab 
   1.198 -	    else  raise TERM ("Incompatible types for constant: "^a, []);
   1.199 +        None => Symtab.update((a,x), tab)
   1.200 +      | Some y => if x=y then tab
   1.201 +            else  raise TERM ("Incompatible types for constant: "^a, []);
   1.202  
   1.203  (*Combine tables, updating tab2 by tab1 and checking.*)
   1.204 -fun merge_tabs (tab1,tab2) = 
   1.205 +fun merge_tabs (tab1,tab2) =
   1.206      Symtab.balance (foldr update_eq (Symtab.alist_of tab1, tab2));
   1.207  
   1.208  (*Combine tables, overwriting tab2 with tab1.*)
   1.209 -fun smash_tabs (tab1,tab2) = 
   1.210 +fun smash_tabs (tab1,tab2) =
   1.211      Symtab.balance (foldr Symtab.update (Symtab.alist_of tab1, tab2));
   1.212  
   1.213  (*Combine stamps, checking that theory names are disjoint. *)
   1.214 -fun merge_stamps (stamps1,stamps2) = 
   1.215 +fun merge_stamps (stamps1,stamps2) =
   1.216    let val stamps = stamps1 union stamps2 in
   1.217    case findrep (map ! stamps) of
   1.218       a::_ => error ("Attempt to merge different versions of theory: " ^ a)
   1.219 @@ -203,14 +203,14 @@
   1.220  
   1.221  (*Merge two signatures.  Forms unions of tables.  Prefers sign1. *)
   1.222  fun merge (sign1 as Sg{tsig=tsig1,const_tab=ctab1,stamps=stamps1,syn=syn1},
   1.223 -	   sign2 as Sg{tsig=tsig2,const_tab=ctab2,stamps=stamps2,syn=syn2}) =
   1.224 +           sign2 as Sg{tsig=tsig2,const_tab=ctab2,stamps=stamps2,syn=syn2}) =
   1.225      if stamps2 subset stamps1 then sign1
   1.226      else if stamps1 subset stamps2 then sign2
   1.227      else  (*neither is union already;  must form union*)
   1.228 -	   Sg{tsig= Type.merge(tsig1,tsig2),
   1.229 -	      const_tab= merge_tabs (ctab1, ctab2),
   1.230 -	      stamps= merge_stamps (stamps1,stamps2),
   1.231 -	      syn = Syntax.merge(syn1,syn2)};
   1.232 +           Sg{tsig= Type.merge(tsig1,tsig2),
   1.233 +              const_tab= merge_tabs (ctab1, ctab2),
   1.234 +              stamps= merge_stamps (stamps1,stamps2),
   1.235 +              syn = Syntax.merge(syn1,syn2)};
   1.236  
   1.237  
   1.238  (**** CERTIFIED TYPES ****)
   1.239 @@ -224,15 +224,15 @@
   1.240  fun typ_of (Ctyp{sign,T}) = T;
   1.241  
   1.242  fun ctyp_of (sign as Sg{tsig,...}) T =
   1.243 -	case Type.type_errors (tsig,string_of_typ sign) (T,[]) of
   1.244 -	  [] => Ctyp{sign= sign,T= T}
   1.245 -	| errs =>  error (cat_lines ("Error in type:" :: errs));
   1.246 +        case Type.type_errors (tsig,string_of_typ sign) (T,[]) of
   1.247 +          [] => Ctyp{sign= sign,T= T}
   1.248 +        | errs =>  error (cat_lines ("Error in type:" :: errs));
   1.249  
   1.250  (*The only use is a horrible hack in the simplifier!*)
   1.251  fun read_typ(Sg{tsig,syn,...}, defS) s =
   1.252      let val term = Syntax.read syn Syntax.typeT s;
   1.253 -	val S0 = Type.defaultS tsig;
   1.254 -	fun defS0 s = case defS s of Some S => S | None => S0;
   1.255 +        val S0 = Type.defaultS tsig;
   1.256 +        fun defS0 s = case defS s of Some S => S | None => S0;
   1.257      in Syntax.typ_of_term defS0 term end;
   1.258  
   1.259  fun read_ctyp sign = ctyp_of sign o read_typ(sign, K None);
   1.260 @@ -274,19 +274,19 @@
   1.261  
   1.262  (*Lexing, parsing, polymorphic typechecking of a term.*)
   1.263  fun read_def_cterm (sign as Sg{tsig, const_tab, syn,...}, types, sorts)
   1.264 -		   (a,T) =
   1.265 +                   (a,T) =
   1.266    let val showtyp = string_of_typ sign
   1.267        and showterm = string_of_term sign
   1.268        fun termerr [] = ""
   1.269 -	| termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n"
   1.270 -	| termerr ts = "\nInvolving these terms:\n" ^
   1.271 -		       cat_lines (map showterm ts)
   1.272 +        | termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n"
   1.273 +        | termerr ts = "\nInvolving these terms:\n" ^
   1.274 +                       cat_lines (map showterm ts)
   1.275        val t = Syntax.read syn T a;
   1.276        val (t',tye) = Type.infer_types (tsig, const_tab, types,
   1.277 -				       sorts, showtyp, T, t)
   1.278 -		  handle TYPE (msg, Ts, ts) =>
   1.279 -	  error ("Type checking error: " ^ msg ^ "\n" ^
   1.280 -		  cat_lines (map showtyp Ts) ^ termerr ts)
   1.281 +                                       sorts, showtyp, T, t)
   1.282 +                  handle TYPE (msg, Ts, ts) =>
   1.283 +          error ("Type checking error: " ^ msg ^ "\n" ^
   1.284 +                  cat_lines (map showtyp Ts) ^ termerr ts)
   1.285    in (cterm_of sign t', tye)
   1.286    end
   1.287    handle TERM (msg, _) => error ("Error: " ^  msg);
   1.288 @@ -297,7 +297,7 @@
   1.289  (** reading of instantiations **)
   1.290  
   1.291  fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
   1.292 -	| _ => error("Lexical error in variable name: " ^ implode cs);
   1.293 +        | _ => error("Lexical error in variable name " ^ quote (implode cs));
   1.294  
   1.295  fun absent ixn =
   1.296    error("No such variable in term: " ^ Syntax.string_of_vname ixn);
   1.297 @@ -308,24 +308,24 @@
   1.298  fun read_insts (sign as Sg{tsig,...}) (rtypes,rsorts) (types,sorts) insts =
   1.299  let fun split([],tvs,vs) = (tvs,vs)
   1.300        | split((sv,st)::l,tvs,vs) = (case explode sv of
   1.301 -		  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
   1.302 -		| cs => split(l,tvs,(indexname cs,st)::vs));
   1.303 +                  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
   1.304 +                | cs => split(l,tvs,(indexname cs,st)::vs));
   1.305      val (tvs,vs) = split(insts,[],[]);
   1.306      fun readT((a,i),st) =
   1.307 -	let val ixn = ("'" ^ a,i);
   1.308 -	    val S = case rsorts ixn of Some S => S | None => absent ixn;
   1.309 -	    val T = read_typ (sign,sorts) st;
   1.310 -	in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
   1.311 -	   else inst_failure ixn
   1.312 -	end
   1.313 +        let val ixn = ("'" ^ a,i);
   1.314 +            val S = case rsorts ixn of Some S => S | None => absent ixn;
   1.315 +            val T = read_typ (sign,sorts) st;
   1.316 +        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
   1.317 +           else inst_failure ixn
   1.318 +        end
   1.319      val tye = map readT tvs;
   1.320      fun add_cterm ((cts,tye), (ixn,st)) =
   1.321 -	let val T = case rtypes ixn of
   1.322 -		      Some T => typ_subst_TVars tye T
   1.323 -		    | None => absent ixn;
   1.324 -	    val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
   1.325 -	    val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
   1.326 - 	in ((cv,ct)::cts,tye2 @ tye) end
   1.327 +        let val T = case rtypes ixn of
   1.328 +                      Some T => typ_subst_TVars tye T
   1.329 +                    | None => absent ixn;
   1.330 +            val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
   1.331 +            val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
   1.332 +        in ((cv,ct)::cts,tye2 @ tye) end
   1.333      val (cterms,tye') = foldl add_cterm (([],tye), vs);
   1.334  in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
   1.335