extend: cleaned up, adapted for new Syntax.extend;
authorwenzelm
Mon Nov 29 13:54:59 1993 +0100 (1993-11-29)
changeset 1691b2765146aab
parent 168 1bf4e2cab673
child 170 590c9d1e0d73
extend: cleaned up, adapted for new Syntax.extend;
extend, merge: improved roots (logical_types) handling;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Mon Nov 29 13:51:37 1993 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Nov 29 13:54:59 1993 +0100
     1.3 @@ -101,78 +101,84 @@
     1.4  in  terrs  end;
     1.5  
     1.6  
     1.7 +
     1.8  (** The Extend operation **)
     1.9  
    1.10 -(*Reset TVar indices to zero, renaming to preserve distinctness*)
    1.11 -fun zero_tvar_indices tsig T =
    1.12 -  let val inxSs = typ_tvars T;
    1.13 -      val nms' = variantlist(map (#1 o #1) inxSs,[]);
    1.14 -      val tye = map (fn ((v,S),a) => (v, TVar((a,0),S))) (inxSs ~~ nms')
    1.15 -  in typ_subst_TVars tye T end
    1.16 +(* Extend a signature: may add classes, types and constants. The "ref" in
    1.17 +   stamps ensures that no two signatures are identical -- it is impossible to
    1.18 +   forge a signature. *)
    1.19 +
    1.20 +fun extend (Sg {tsig, const_tab, syn, stamps}) name
    1.21 +  (classes, default, types, arities, const_decs, opt_sext) =
    1.22 +  let
    1.23 +    fun err_in_typ s = error ("The error(s) above occurred in type " ^ quote s);
    1.24 +
    1.25 +    fun read_typ tsg sy s =
    1.26 +      Syntax.read_typ sy (K (Type.defaultS tsg)) s handle ERROR => err_in_typ s;
    1.27 +
    1.28 +    fun check_typ tsg sy ty =
    1.29 +      (case Type.type_errors (tsg, Syntax.string_of_typ sy) (ty, []) of
    1.30 +        [] => ty
    1.31 +      | errs => (prs (cat_lines errs); err_in_typ (Syntax.string_of_typ sy ty)));
    1.32 +
    1.33 +    (*reset TVar indices to zero, renaming to preserve distinctness*)
    1.34 +    fun zero_tvar_indices T =
    1.35 +      let
    1.36 +        val inxSs = typ_tvars T;
    1.37 +        val nms' = variantlist (map (#1 o #1) inxSs, []);
    1.38 +        val tye = map (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs ~~ nms');
    1.39 +      in typ_subst_TVars tye T end;
    1.40 +
    1.41 +    (*read and check the type mentioned in a const declaration; zero type var
    1.42 +      indices because type inference requires it*)
    1.43 +
    1.44 +    (* FIXME bug / feature: varifyT'ed TFrees may clash with user specified
    1.45 +      TVars e.g. foo :: "'a => ?'a" *)
    1.46 +    (* FIXME if user supplied TVars were disallowed, zero_tvar_indices would
    1.47 +      become obsolete *)
    1.48 +    (* FIXME disallow "" as const name *)
    1.49 +
    1.50 +    fun read_consts tsg sy (cs, s) =
    1.51 +      let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));
    1.52 +      in
    1.53 +        (case Type.type_errors (tsg, Syntax.string_of_typ sy) (ty, []) of
    1.54 +          [] => (cs, ty)
    1.55 +        | errs => error (cat_lines (("Error in type of constants " ^
    1.56 +            space_implode " " (map quote cs)) :: errs)))
    1.57 +      end;
    1.58  
    1.59  
    1.60 -(*Check that all types mentioned in the list of declarations are valid.
    1.61 -  If errors found then raise exception.
    1.62 -  Zero type var indices because type inference requires it.
    1.63 -*)
    1.64 -fun read_consts(tsig,syn) =
    1.65 -let val showtyp = Syntax.string_of_typ syn;
    1.66 -    fun read [] = []
    1.67 -      | read((cs,s)::pairs) =
    1.68 -        let val t = Syntax.read syn Syntax.typeT s handle ERROR =>
    1.69 -                    error("The error above occurred in type " ^ quote s);
    1.70 -            val S = Type.defaultS tsig;
    1.71 -            val T = Type.varifyT(Syntax.typ_of_term (K S) t)
    1.72 -            val T0 = zero_tvar_indices tsig T;
    1.73 -        in (case Type.type_errors (tsig,showtyp) (T0,[]) of
    1.74 -                [] => (cs,T0) :: read pairs
    1.75 -            | errs => error (cat_lines
    1.76 -           (("Error in type of constants " ^ space_implode " " cs) :: errs)))
    1.77 -        end
    1.78 -in read end;
    1.79 -
    1.80 -
    1.81 -(*Extend a signature: may add classes, types and constants.
    1.82 -  Replaces syntax with "syn".
    1.83 -  The "ref" in stamps ensures that no two signatures are identical --
    1.84 -  it is impossible to forge a signature. *)
    1.85 -
    1.86 -fun extend (Sg {tsig, const_tab, syn, stamps}) signame
    1.87 -  (classes, default, types, arities, const_decs, osext) =
    1.88 -  let
    1.89      (* FIXME abbr *)
    1.90      val tsig' = Type.extend (tsig, classes, default, types, arities);
    1.91  
    1.92 -    (* FIXME expand_typ, check typ *)
    1.93 -    val read_ty = Syntax.read_typ syn (K (Type.defaultS tsig'));
    1.94 +    (* FIXME *)
    1.95 +    fun expand_typ _ ty = ty;
    1.96  
    1.97 -    val roots = filter (Type.logical_type tsig') (distinct (flat (map #1 arities)));
    1.98 +    val read_ty =
    1.99 +      (expand_typ tsig') o (check_typ tsig' syn) o (read_typ tsig' syn);
   1.100 +    val log_types = Type.logical_types tsig';
   1.101      val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs);
   1.102 -    val syn' =
   1.103 -      (case osext of
   1.104 -        Some sext => Syntax.extend syn read_ty (roots, xconsts, sext)
   1.105 -      | None =>
   1.106 -          if null roots andalso null xconsts then syn
   1.107 -          else Syntax.extend syn read_ty (roots, xconsts, Syntax.empty_sext));
   1.108 -    val sconsts =
   1.109 -      (case osext of
   1.110 -        Some sext => Syntax.constants sext
   1.111 -      | None => []);
   1.112 -    val const_decs' = read_consts (tsig', syn') (sconsts @ const_decs);
   1.113 +    val sext = case opt_sext of Some sx => sx | None => Syntax.empty_sext;
   1.114 +
   1.115 +    val syn' = Syntax.extend syn read_ty (log_types, xconsts, sext);
   1.116 +
   1.117 +    val const_decs' =
   1.118 +      map (read_consts tsig' syn') (Syntax.constants sext @ const_decs);
   1.119 +                    (* FIXME ^^^^ should be syn *)
   1.120    in
   1.121      Sg {
   1.122        tsig = tsig',
   1.123        const_tab = Symtab.st_of_declist (const_decs', const_tab)
   1.124          handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"),
   1.125        syn = syn',
   1.126 -      stamps = ref signame :: stamps}
   1.127 +      stamps = ref name :: stamps}
   1.128    end;
   1.129  
   1.130  
   1.131  (* The empty signature *)
   1.132  
   1.133 -val sg0 = Sg {tsig = Type.tsig0,
   1.134 -  const_tab = Symtab.null, syn = Syntax.type_syn, stamps= []};
   1.135 +val sg0 = Sg {tsig = Type.tsig0, const_tab = Symtab.null,
   1.136 +  syn = Syntax.type_syn, stamps = []};
   1.137  
   1.138  
   1.139  (* The pure signature *)
   1.140 @@ -185,7 +191,7 @@
   1.141    (Syntax.syntax_types, 0)],
   1.142   [(["fun"],  ([["logic"], ["logic"]], "logic")),
   1.143    (["prop"], ([], "logic"))],
   1.144 - [([Syntax.constrainC], "'a::logic => 'a")],  (* MMW FIXME replace logic by {} (?) *)
   1.145 + [([Syntax.constrainC], "'a::logic => 'a")],  (* FIXME replace logic by {} (?) *)
   1.146   Some Syntax.pure_sext);
   1.147  
   1.148  
   1.149 @@ -216,15 +222,19 @@
   1.150    end;
   1.151  
   1.152  (*Merge two signatures.  Forms unions of tables.  Prefers sign1. *)
   1.153 -fun merge (sign1 as Sg{tsig=tsig1,const_tab=ctab1,stamps=stamps1,syn=syn1},
   1.154 -           sign2 as Sg{tsig=tsig2,const_tab=ctab2,stamps=stamps2,syn=syn2}) =
   1.155 +fun merge
   1.156 +  (sign1 as Sg {tsig = tsig1, const_tab = ctab1, stamps = stamps1, syn = syn1},
   1.157 +   sign2 as Sg {tsig = tsig2, const_tab = ctab2, stamps = stamps2, syn = syn2}) =
   1.158      if stamps2 subset stamps1 then sign1
   1.159      else if stamps1 subset stamps2 then sign2
   1.160 -    else  (*neither is union already;  must form union*)
   1.161 -           Sg{tsig= Type.merge(tsig1,tsig2),
   1.162 -              const_tab= merge_tabs (ctab1, ctab2),
   1.163 -              stamps= merge_stamps (stamps1,stamps2),
   1.164 -              syn = Syntax.merge(syn1,syn2)};
   1.165 +    else (*neither is union already; must form union*)
   1.166 +      let val tsig = Type.merge (tsig1, tsig2);
   1.167 +      in
   1.168 +        Sg {tsig = tsig, const_tab = merge_tabs (ctab1, ctab2),
   1.169 +          stamps = merge_stamps (stamps1, stamps2),
   1.170 +          syn = Syntax.merge (Type.logical_types tsig) syn1 syn2}
   1.171 +      end;
   1.172 +
   1.173  
   1.174  
   1.175  (**** CERTIFIED TYPES ****)