src/Pure/sign.ML
changeset 200 39a931cc6558
parent 197 7c7179e687b2
child 206 0d624d1ba9cc
     1.1 --- a/src/Pure/sign.ML	Tue Dec 21 14:47:29 1993 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Dec 21 16:26:40 1993 +0100
     1.3 @@ -22,6 +22,7 @@
     1.4    val extend: sg -> string ->
     1.5          (class * class list) list * class list *
     1.6          (string list * int) list *
     1.7 +        (string * indexname list * string) list *
     1.8          (string list * (sort list * class)) list *
     1.9          (string list * string)list * Syntax.sext option -> sg
    1.10    val merge: sg * sg -> sg
    1.11 @@ -52,7 +53,7 @@
    1.12    val pretty_term: sg -> term -> Syntax.Pretty.T
    1.13  end;
    1.14  
    1.15 -functor SignFun(structure Type: TYPE and Syntax: SYNTAX): SIGN =
    1.16 +functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
    1.17  struct
    1.18  
    1.19  structure Type = Type;
    1.20 @@ -85,18 +86,18 @@
    1.21  (*Check a term for errors.  Are all constants and types valid in signature?
    1.22    Does not check that term is well-typed!*)
    1.23  fun term_errors (sign as Sg{tsig,const_tab,...}) =
    1.24 -let val showtyp = string_of_typ sign;
    1.25 +let val showtyp = string_of_typ sign
    1.26      fun terrs (Const (a,T), errs) =
    1.27          if valid_const tsig const_tab (a,T)
    1.28 -        then Type.type_errors (tsig,showtyp) (T,errs)
    1.29 +        then Type.type_errors tsig (T,errs)
    1.30          else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
    1.31 -      | terrs (Free (_,T), errs) = Type.type_errors (tsig,showtyp) (T,errs)
    1.32 +      | terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
    1.33        | terrs (Var  ((a,i),T), errs) =
    1.34 -        if  i>=0  then  Type.type_errors (tsig,showtyp) (T,errs)
    1.35 +        if  i>=0  then  Type.type_errors tsig (T,errs)
    1.36          else  ("Negative index for Var: " ^ a) :: errs
    1.37        | terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
    1.38        | terrs (Abs (_,T,t), errs) =
    1.39 -            Type.type_errors(tsig,showtyp)(T,terrs(t,errs))
    1.40 +            Type.type_errors tsig (T,terrs(t,errs))
    1.41        | terrs (f$t, errs) = terrs(f, terrs (t,errs))
    1.42  in  terrs  end;
    1.43  
    1.44 @@ -109,7 +110,7 @@
    1.45     forge a signature. *)
    1.46  
    1.47  fun extend (Sg {tsig, const_tab, syn, stamps}) name
    1.48 -  (classes, default, types, arities, const_decs, opt_sext) =
    1.49 +  (classes, default, types, abbr, arities, const_decs, opt_sext) =
    1.50    let
    1.51      fun err_in_typ s = error ("The error(s) above occurred in type " ^ quote s);
    1.52  
    1.53 @@ -117,7 +118,7 @@
    1.54        Syntax.read_typ sy (K (Type.defaultS tsg)) s handle ERROR => err_in_typ s;
    1.55  
    1.56      fun check_typ tsg sy ty =
    1.57 -      (case Type.type_errors (tsg, Syntax.string_of_typ sy) (ty, []) of
    1.58 +      (case Type.type_errors tsg (ty, []) of
    1.59          [] => ty
    1.60        | errs => (prs (cat_lines errs); err_in_typ (Syntax.string_of_typ sy ty)));
    1.61  
    1.62 @@ -135,32 +136,34 @@
    1.63      fun read_consts tsg sy (cs, s) =
    1.64        let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));
    1.65        in
    1.66 -        (case Type.type_errors (tsg, Syntax.string_of_typ sy) (ty, []) of
    1.67 +        (case Type.type_errors tsg (ty, []) of
    1.68            [] => (cs, ty)
    1.69          | errs => error (cat_lines (("Error in type of constants " ^
    1.70              space_implode " " (map quote cs)) :: errs)))
    1.71        end;
    1.72  
    1.73 -
    1.74 -    (* FIXME abbr *)
    1.75      val tsig' = Type.extend (tsig, classes, default, types, arities);
    1.76  
    1.77 -    (* FIXME *)
    1.78 -    fun expand_typ _ ty = ty;
    1.79 +    fun read_typ_abbr(a,v,s)=
    1.80 +      let val T = Type.varifyT(read_typ tsig' syn s)
    1.81 +      in (a,(v,T)) end handle ERROR => error("This error occured in abbreviation "^ quote a);
    1.82 +
    1.83 +    val abbr' = map read_typ_abbr abbr;
    1.84 +    val tsig'' = Type.add_abbrs(tsig',abbr');
    1.85  
    1.86      val read_ty =
    1.87 -      (expand_typ tsig') o (check_typ tsig' syn) o (read_typ tsig' syn);
    1.88 -    val log_types = Type.logical_types tsig';
    1.89 +      (Type.expand_typ tsig'') o (check_typ tsig'' syn) o (read_typ tsig'' syn);
    1.90 +    val log_types = Type.logical_types tsig'';
    1.91      val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs);
    1.92      val sext = case opt_sext of Some sx => sx | None => Syntax.empty_sext;
    1.93  
    1.94      val syn' = Syntax.extend syn read_ty (log_types, xconsts, sext);
    1.95  
    1.96      val const_decs' =
    1.97 -      map (read_consts tsig' syn') (Syntax.constants sext @ const_decs);
    1.98 +      map (read_consts tsig'' syn') (Syntax.constants sext @ const_decs);
    1.99    in
   1.100      Sg {
   1.101 -      tsig = tsig',
   1.102 +      tsig = tsig'',
   1.103        const_tab = Symtab.st_of_declist (const_decs', const_tab)
   1.104          handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"),
   1.105        syn = syn',
   1.106 @@ -182,6 +185,7 @@
   1.107   [(["fun"], 2),
   1.108    (["prop"], 0),
   1.109    (Syntax.syntax_types, 0)],
   1.110 + [],
   1.111   [(["fun"],  ([["logic"], ["logic"]], "logic")),
   1.112    (["prop"], ([], "logic"))],
   1.113   [([Syntax.constrainC], "'a::logic => 'a")],
   1.114 @@ -241,7 +245,7 @@
   1.115  fun typ_of (Ctyp{sign,T}) = T;
   1.116  
   1.117  fun ctyp_of (sign as Sg{tsig,...}) T =
   1.118 -        case Type.type_errors (tsig,string_of_typ sign) (T,[]) of
   1.119 +        case Type.type_errors tsig (T,[]) of
   1.120            [] => Ctyp{sign= sign,T= T}
   1.121          | errs =>  error (cat_lines ("Error in type:" :: errs));
   1.122  
   1.123 @@ -341,12 +345,10 @@
   1.124                        Some T => typ_subst_TVars tye T
   1.125                      | None => absent ixn;
   1.126              val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
   1.127 -        in ((ixn,T,ct)::cts,tye2 @ tye) end
   1.128 +            val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
   1.129 +        in ((cv,ct)::cts,tye2 @ tye) end
   1.130      val (cterms,tye') = foldl add_cterm (([],tye), vs);
   1.131 -in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye',
   1.132 -    map (fn (ixn,T,ct)=> (cterm_of sign (Var(ixn,typ_subst_TVars tye' T)), ct))
   1.133 -        cterms)
   1.134 -end;
   1.135 +in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
   1.136  
   1.137  end;
   1.138