19

1 
(* Title: Pure/sign.ML

0

2 
ID: $Id$

19

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1992 University of Cambridge


5 

143

6 
The abstract types "sg" (signatures) and "cterm" / "ctyp" (certified terms /


7 
typs under a signature).

0

8 
*)


9 

19

10 
signature SIGN =

0

11 
sig


12 
structure Type: TYPE


13 
structure Symtab: SYMTAB


14 
structure Syntax: SYNTAX

143

15 
sharing Symtab = Type.Symtab

0

16 
type sg


17 
type cterm


18 
type ctyp


19 
val cfun: (term > term) > (cterm > cterm)


20 
val cterm_of: sg > term > cterm


21 
val ctyp_of: sg > typ > ctyp


22 
val extend: sg > string >

19

23 
(class * class list) list * class list *


24 
(string list * int) list *

200

25 
(string * indexname list * string) list *

19

26 
(string list * (sort list * class)) list *


27 
(string list * string)list * Syntax.sext option > sg

0

28 
val merge: sg * sg > sg


29 
val pure: sg


30 
val read_cterm: sg > string * typ > cterm


31 
val read_ctyp: sg > string > ctyp


32 
val read_insts: sg > (indexname > typ option) * (indexname > sort option)

19

33 
> (indexname > typ option) * (indexname > sort option)


34 
> (string*string)list


35 
> (indexname*ctyp)list * (cterm*cterm)list

0

36 
val read_typ: sg * (indexname > sort option) > string > typ


37 
val rep_cterm: cterm > {T: typ, t: term, sign: sg, maxidx: int}


38 
val rep_ctyp: ctyp > {T: typ, sign: sg}


39 
val rep_sg: sg > {tsig: Type.type_sig,

19

40 
const_tab: typ Symtab.table,


41 
syn: Syntax.syntax,


42 
stamps: string ref list}

0

43 
val string_of_cterm: cterm > string


44 
val string_of_ctyp: ctyp > string


45 
val pprint_cterm: cterm > pprint_args > unit


46 
val pprint_ctyp: ctyp > pprint_args > unit


47 
val string_of_term: sg > term > string


48 
val string_of_typ: sg > typ > string


49 
val pprint_term: sg > term > pprint_args > unit


50 
val pprint_typ: sg > typ > pprint_args > unit


51 
val term_of: cterm > term


52 
val typ_of: ctyp > typ


53 
val pretty_term: sg > term > Syntax.Pretty.T


54 
end;


55 

200

56 
functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =

143

57 
struct

0

58 


59 
structure Type = Type;


60 
structure Symtab = Type.Symtab;


61 
structure Syntax = Syntax;


62 
structure Pretty = Syntax.Pretty


63 

143

64 


65 
(* Signatures of theories. *)


66 

19

67 
datatype sg =

143

68 
Sg of {


69 
tsig: Type.type_sig, (*ordersorted signature of types*)


70 
const_tab: typ Symtab.table, (*types of constants*)


71 
syn: Syntax.syntax, (*syntax for parsing and printing*)


72 
stamps: string ref list}; (*unique theory indentifier*)

0

73 


74 


75 
fun rep_sg (Sg args) = args;


76 


77 
fun string_of_typ(Sg{tsig,syn,...}) = Syntax.string_of_typ syn;


78 


79 
fun pprint_typ(Sg{syn,...}) = Pretty.pprint o Pretty.quote o (Syntax.pretty_typ syn);


80 


81 
(*Is constant present in table with more generic type?*)


82 
fun valid_const tsig ctab (a,T) = case Symtab.lookup(ctab, a) of

19

83 
Some U => Type.typ_instance(tsig,T,U)  _ => false;

0

84 


85 


86 
(*Check a term for errors. Are all constants and types valid in signature?


87 
Does not check that term is welltyped!*)

19

88 
fun term_errors (sign as Sg{tsig,const_tab,...}) =

200

89 
let val showtyp = string_of_typ sign

0

90 
fun terrs (Const (a,T), errs) =

19

91 
if valid_const tsig const_tab (a,T)

200

92 
then Type.type_errors tsig (T,errs)

19

93 
else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs

200

94 
 terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)

0

95 
 terrs (Var ((a,i),T), errs) =

200

96 
if i>=0 then Type.type_errors tsig (T,errs)

19

97 
else ("Negative index for Var: " ^ a) :: errs

0

98 
 terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)

19

99 
 terrs (Abs (_,T,t), errs) =

200

100 
Type.type_errors tsig (T,terrs(t,errs))

0

101 
 terrs (f$t, errs) = terrs(f, terrs (t,errs))


102 
in terrs end;


103 


104 

169

105 

0

106 
(** The Extend operation **)


107 

169

108 
(* Extend a signature: may add classes, types and constants. The "ref" in


109 
stamps ensures that no two signatures are identical  it is impossible to


110 
forge a signature. *)


111 


112 
fun extend (Sg {tsig, const_tab, syn, stamps}) name

200

113 
(classes, default, types, abbr, arities, const_decs, opt_sext) =

169

114 
let


115 
fun err_in_typ s = error ("The error(s) above occurred in type " ^ quote s);


116 


117 
fun read_typ tsg sy s =


118 
Syntax.read_typ sy (K (Type.defaultS tsg)) s handle ERROR => err_in_typ s;


119 


120 
fun check_typ tsg sy ty =

200

121 
(case Type.type_errors tsg (ty, []) of

169

122 
[] => ty


123 
 errs => (prs (cat_lines errs); err_in_typ (Syntax.string_of_typ sy ty)));


124 


125 
(*reset TVar indices to zero, renaming to preserve distinctness*)


126 
fun zero_tvar_indices T =


127 
let


128 
val inxSs = typ_tvars T;


129 
val nms' = variantlist (map (#1 o #1) inxSs, []);


130 
val tye = map (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs ~~ nms');


131 
in typ_subst_TVars tye T end;


132 


133 
(*read and check the type mentioned in a const declaration; zero type var


134 
indices because type inference requires it*)


135 


136 
fun read_consts tsg sy (cs, s) =


137 
let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));


138 
in

200

139 
(case Type.type_errors tsg (ty, []) of

169

140 
[] => (cs, ty)


141 
 errs => error (cat_lines (("Error in type of constants " ^


142 
space_implode " " (map quote cs)) :: errs)))


143 
end;

0

144 

155

145 
val tsig' = Type.extend (tsig, classes, default, types, arities);

143

146 

200

147 
fun read_typ_abbr(a,v,s)=


148 
let val T = Type.varifyT(read_typ tsig' syn s)


149 
in (a,(v,T)) end handle ERROR => error("This error occured in abbreviation "^ quote a);


150 


151 
val abbr' = map read_typ_abbr abbr;


152 
val tsig'' = Type.add_abbrs(tsig',abbr');

143

153 

169

154 
val read_ty =

200

155 
(Type.expand_typ tsig'') o (check_typ tsig'' syn) o (read_typ tsig'' syn);


156 
val log_types = Type.logical_types tsig'';

155

157 
val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs);

169

158 
val sext = case opt_sext of Some sx => sx  None => Syntax.empty_sext;


159 


160 
val syn' = Syntax.extend syn read_ty (log_types, xconsts, sext);


161 


162 
val const_decs' =

200

163 
map (read_consts tsig'' syn') (Syntax.constants sext @ const_decs);

143

164 
in


165 
Sg {

200

166 
tsig = tsig'',

143

167 
const_tab = Symtab.st_of_declist (const_decs', const_tab)


168 
handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"),


169 
syn = syn',

169

170 
stamps = ref name :: stamps}

143

171 
end;

0

172 


173 


174 
(* The empty signature *)

143

175 

169

176 
val sg0 = Sg {tsig = Type.tsig0, const_tab = Symtab.null,


177 
syn = Syntax.type_syn, stamps = []};

0

178 

143

179 


180 
(* The pure signature *)


181 


182 
val pure = extend sg0 "Pure"

0

183 
([("logic", [])],


184 
["logic"],

143

185 
[(["fun"], 2),


186 
(["prop"], 0),


187 
(Syntax.syntax_types, 0)],

200

188 
[],

0

189 
[(["fun"], ([["logic"], ["logic"]], "logic")),


190 
(["prop"], ([], "logic"))],

171

191 
[([Syntax.constrainC], "'a::logic => 'a")],

143

192 
Some Syntax.pure_sext);


193 

0

194 


195 


196 
(** The Merge operation **)


197 


198 
(*Update table with (a,x) providing any existing asgt to "a" equals x. *)


199 
fun update_eq ((a,x),tab) =


200 
case Symtab.lookup(tab,a) of

19

201 
None => Symtab.update((a,x), tab)


202 
 Some y => if x=y then tab


203 
else raise TERM ("Incompatible types for constant: "^a, []);

0

204 


205 
(*Combine tables, updating tab2 by tab1 and checking.*)

19

206 
fun merge_tabs (tab1,tab2) =

0

207 
Symtab.balance (foldr update_eq (Symtab.alist_of tab1, tab2));


208 


209 
(*Combine tables, overwriting tab2 with tab1.*)

19

210 
fun smash_tabs (tab1,tab2) =

0

211 
Symtab.balance (foldr Symtab.update (Symtab.alist_of tab1, tab2));


212 


213 
(*Combine stamps, checking that theory names are disjoint. *)

19

214 
fun merge_stamps (stamps1,stamps2) =

0

215 
let val stamps = stamps1 union stamps2 in


216 
case findrep (map ! stamps) of


217 
a::_ => error ("Attempt to merge different versions of theory: " ^ a)


218 
 [] => stamps


219 
end;


220 


221 
(*Merge two signatures. Forms unions of tables. Prefers sign1. *)

169

222 
fun merge


223 
(sign1 as Sg {tsig = tsig1, const_tab = ctab1, stamps = stamps1, syn = syn1},


224 
sign2 as Sg {tsig = tsig2, const_tab = ctab2, stamps = stamps2, syn = syn2}) =

0

225 
if stamps2 subset stamps1 then sign1


226 
else if stamps1 subset stamps2 then sign2

169

227 
else (*neither is union already; must form union*)


228 
let val tsig = Type.merge (tsig1, tsig2);


229 
in


230 
Sg {tsig = tsig, const_tab = merge_tabs (ctab1, ctab2),


231 
stamps = merge_stamps (stamps1, stamps2),


232 
syn = Syntax.merge (Type.logical_types tsig) syn1 syn2}


233 
end;


234 

0

235 


236 


237 
(**** CERTIFIED TYPES ****)


238 


239 


240 
(*Certified typs under a signature*)


241 
datatype ctyp = Ctyp of {sign: sg, T: typ};


242 


243 
fun rep_ctyp(Ctyp ctyp) = ctyp;


244 


245 
fun typ_of (Ctyp{sign,T}) = T;


246 


247 
fun ctyp_of (sign as Sg{tsig,...}) T =

200

248 
case Type.type_errors tsig (T,[]) of

19

249 
[] => Ctyp{sign= sign,T= T}


250 
 errs => error (cat_lines ("Error in type:" :: errs));

0

251 


252 
(*The only use is a horrible hack in the simplifier!*)


253 
fun read_typ(Sg{tsig,syn,...}, defS) s =


254 
let val term = Syntax.read syn Syntax.typeT s;

19

255 
val S0 = Type.defaultS tsig;


256 
fun defS0 s = case defS s of Some S => S  None => S0;

0

257 
in Syntax.typ_of_term defS0 term end;


258 


259 
fun read_ctyp sign = ctyp_of sign o read_typ(sign, K None);


260 


261 
fun string_of_ctyp (Ctyp{sign,T}) = string_of_typ sign T;


262 


263 
fun pprint_ctyp (Ctyp{sign,T}) = pprint_typ sign T;


264 


265 


266 
(**** CERTIFIED TERMS ****)


267 


268 
(*Certified terms under a signature, with checked typ and maxidx of Vars*)


269 
datatype cterm = Cterm of {sign: sg, t: term, T: typ, maxidx: int};


270 


271 
fun rep_cterm (Cterm args) = args;


272 


273 
(*Return the underlying term*)


274 
fun term_of (Cterm{sign,t,T,maxidx}) = t;


275 


276 
(** pretty printing of terms **)


277 


278 
fun pretty_term (Sg{tsig,syn,...}) = Syntax.pretty_term syn;


279 


280 
fun string_of_term sign t = Pretty.string_of (pretty_term sign t);


281 


282 
fun pprint_term sign = Pretty.pprint o Pretty.quote o (pretty_term sign);


283 


284 
fun string_of_cterm (Cterm{sign,t,...}) = string_of_term sign t;


285 


286 
fun pprint_cterm (Cterm{sign,t,...}) = pprint_term sign t;


287 


288 
(*Create a cterm by checking a "raw" term with respect to a signature*)


289 
fun cterm_of sign t =


290 
case term_errors sign (t,[]) of


291 
[] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}


292 
 errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);


293 


294 
fun cfun f = fn Cterm{sign,t,...} => cterm_of sign (f t);


295 


296 
(*Lexing, parsing, polymorphic typechecking of a term.*)


297 
fun read_def_cterm (sign as Sg{tsig, const_tab, syn,...}, types, sorts)

19

298 
(a,T) =

0

299 
let val showtyp = string_of_typ sign


300 
and showterm = string_of_term sign


301 
fun termerr [] = ""

19

302 
 termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n"


303 
 termerr ts = "\nInvolving these terms:\n" ^


304 
cat_lines (map showterm ts)

0

305 
val t = Syntax.read syn T a;


306 
val (t',tye) = Type.infer_types (tsig, const_tab, types,

19

307 
sorts, showtyp, T, t)


308 
handle TYPE (msg, Ts, ts) =>


309 
error ("Type checking error: " ^ msg ^ "\n" ^


310 
cat_lines (map showtyp Ts) ^ termerr ts)

0

311 
in (cterm_of sign t', tye)


312 
end


313 
handle TERM (msg, _) => error ("Error: " ^ msg);


314 


315 


316 
fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None));


317 


318 
(** reading of instantiations **)


319 


320 
fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v

19

321 
 _ => error("Lexical error in variable name " ^ quote (implode cs));

0

322 


323 
fun absent ixn =


324 
error("No such variable in term: " ^ Syntax.string_of_vname ixn);


325 


326 
fun inst_failure ixn =


327 
error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");


328 


329 
fun read_insts (sign as Sg{tsig,...}) (rtypes,rsorts) (types,sorts) insts =


330 
let fun split([],tvs,vs) = (tvs,vs)


331 
 split((sv,st)::l,tvs,vs) = (case explode sv of

19

332 
"'"::cs => split(l,(indexname cs,st)::tvs,vs)


333 
 cs => split(l,tvs,(indexname cs,st)::vs));

0

334 
val (tvs,vs) = split(insts,[],[]);


335 
fun readT((a,i),st) =

19

336 
let val ixn = ("'" ^ a,i);


337 
val S = case rsorts ixn of Some S => S  None => absent ixn;


338 
val T = read_typ (sign,sorts) st;


339 
in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)


340 
else inst_failure ixn


341 
end

0

342 
val tye = map readT tvs;


343 
fun add_cterm ((cts,tye), (ixn,st)) =

19

344 
let val T = case rtypes ixn of


345 
Some T => typ_subst_TVars tye T


346 
 None => absent ixn;


347 
val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);

200

348 
val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))


349 
in ((cv,ct)::cts,tye2 @ tye) end

0

350 
val (cterms,tye') = foldl add_cterm (([],tye), vs);

200

351 
in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;

0

352 


353 
end;

143

354 
