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 *


25 
(string list * (sort list * class)) list *


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

0

27 
val merge: sg * sg > sg


28 
val pure: sg


29 
val read_cterm: sg > string * typ > cterm


30 
val read_ctyp: sg > string > ctyp


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

19

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


33 
> (string*string)list


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

0

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


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


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


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

19

39 
const_tab: typ Symtab.table,


40 
syn: Syntax.syntax,


41 
stamps: string ref list}

0

42 
val string_of_cterm: cterm > string


43 
val string_of_ctyp: ctyp > string


44 
val pprint_cterm: cterm > pprint_args > unit


45 
val pprint_ctyp: ctyp > pprint_args > unit


46 
val string_of_term: sg > term > string


47 
val string_of_typ: sg > typ > string


48 
val pprint_term: sg > term > pprint_args > unit


49 
val pprint_typ: sg > typ > pprint_args > unit


50 
val term_of: cterm > term


51 
val typ_of: ctyp > typ


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


53 
end;


54 

143

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


56 
struct

0

57 


58 
structure Type = Type;


59 
structure Symtab = Type.Symtab;


60 
structure Syntax = Syntax;


61 
structure Pretty = Syntax.Pretty


62 

143

63 


64 
(* Signatures of theories. *)


65 

19

66 
datatype sg =

143

67 
Sg of {


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


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


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


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

0

72 


73 


74 
fun rep_sg (Sg args) = args;


75 


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


77 


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


79 


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


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

19

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

0

83 


84 


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


86 
Does not check that term is welltyped!*)

19

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

0

88 
let val showtyp = string_of_typ sign;


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

19

90 
if valid_const tsig const_tab (a,T)


91 
then Type.type_errors (tsig,showtyp) (T,errs)


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

0

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


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

19

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


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

0

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

19

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


99 
Type.type_errors(tsig,showtyp)(T,terrs(t,errs))

0

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


101 
in terrs end;


102 


103 


104 
(** The Extend operation **)


105 


106 
(*Reset TVar indices to zero, renaming to preserve distinctness*)

19

107 
fun zero_tvar_indices tsig T =

0

108 
let val inxSs = typ_tvars T;


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


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


111 
in typ_subst_TVars tye T end


112 

143

113 

0

114 
(*Check that all types mentioned in the list of declarations are valid.


115 
If errors found then raise exception.


116 
Zero type var indices because type inference requires it.


117 
*)


118 
fun read_consts(tsig,syn) =


119 
let val showtyp = Syntax.string_of_typ syn;


120 
fun read [] = []


121 
 read((cs,s)::pairs) =

19

122 
let val t = Syntax.read syn Syntax.typeT s handle ERROR =>


123 
error("The error above occurred in type " ^ quote s);


124 
val S = Type.defaultS tsig;


125 
val T = Type.varifyT(Syntax.typ_of_term (K S) t)


126 
val T0 = zero_tvar_indices tsig T;


127 
in (case Type.type_errors (tsig,showtyp) (T0,[]) of


128 
[] => (cs,T0) :: read pairs


129 
 errs => error (cat_lines


130 
(("Error in type of constants " ^ space_implode " " cs) :: errs)))


131 
end

0

132 
in read end;


133 


134 


135 
(*Extend a signature: may add classes, types and constants.


136 
Replaces syntax with "syn".


137 
The "ref" in stamps ensures that no two signatures are identical 

143

138 
it is impossible to forge a signature. *)


139 


140 
fun extend (Sg {tsig, const_tab, syn, stamps}) signame


141 
(newclasses, newdefault, otypes, newtypes, const_decs, osext) =


142 
let


143 
(* FIXME abbr *)


144 
val tsig' = Type.extend (tsig, newclasses, newdefault, otypes, newtypes);


145 


146 
(* FIXME expand_typ, check typ *)


147 
val read_ty = Syntax.read_typ syn (K (Type.defaultS tsig'));


148 


149 
val roots = filter (Type.logical_type tsig') (distinct (flat (map #1 newtypes)));

0

150 
val xconsts = map #1 newclasses @ flat (map #1 otypes) @ flat (map #1 const_decs);


151 
val syn' =

143

152 
(case osext of


153 
Some sext => Syntax.extend syn read_ty (roots, xconsts, sext)


154 
 None =>


155 
if null roots andalso null xconsts then syn


156 
else Syntax.extend syn read_ty (roots, xconsts, Syntax.empty_sext));


157 
val sconsts =


158 
(case osext of


159 
Some sext => Syntax.constants sext


160 
 None => []);


161 
val const_decs' = read_consts (tsig', syn') (sconsts @ const_decs);


162 
in


163 
Sg {


164 
tsig = tsig',


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


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


167 
syn = syn',


168 
stamps = ref signame :: stamps}


169 
end;

0

170 


171 


172 
(* The empty signature *)

143

173 


174 
val sg0 = Sg {tsig = Type.tsig0,


175 
const_tab = Symtab.null, syn = Syntax.type_syn, stamps= []};

0

176 

143

177 


178 
(* The pure signature *)


179 


180 
val pure = extend sg0 "Pure"

0

181 
([("logic", [])],


182 
["logic"],

143

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


184 
(["prop"], 0),


185 
(Syntax.syntax_types, 0)],

0

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


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


188 
[(["*NORMALIZED*"], "'a::{} => 'a"),

143

189 
([Syntax.constrainC], "'a::logic => 'a")], (* MMW FIXME replace logic by {} (?) *)


190 
Some Syntax.pure_sext);


191 

0

192 


193 


194 
(** The Merge operation **)


195 


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


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


198 
case Symtab.lookup(tab,a) of

19

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


200 
 Some y => if x=y then tab


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

0

202 


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

19

204 
fun merge_tabs (tab1,tab2) =

0

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


206 


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

19

208 
fun smash_tabs (tab1,tab2) =

0

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


210 


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

19

212 
fun merge_stamps (stamps1,stamps2) =

0

213 
let val stamps = stamps1 union stamps2 in


214 
case findrep (map ! stamps) of


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


216 
 [] => stamps


217 
end;


218 


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


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

19

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

0

222 
if stamps2 subset stamps1 then sign1


223 
else if stamps1 subset stamps2 then sign2


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

19

225 
Sg{tsig= Type.merge(tsig1,tsig2),


226 
const_tab= merge_tabs (ctab1, ctab2),


227 
stamps= merge_stamps (stamps1,stamps2),


228 
syn = Syntax.merge(syn1,syn2)};

0

229 


230 


231 
(**** CERTIFIED TYPES ****)


232 


233 


234 
(*Certified typs under a signature*)


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


236 


237 
fun rep_ctyp(Ctyp ctyp) = ctyp;


238 


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


240 


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

19

242 
case Type.type_errors (tsig,string_of_typ sign) (T,[]) of


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


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

0

245 


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


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


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

19

249 
val S0 = Type.defaultS tsig;


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

0

251 
in Syntax.typ_of_term defS0 term end;


252 


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


254 


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


256 


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


258 


259 


260 
(**** CERTIFIED TERMS ****)


261 


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


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


264 


265 
fun rep_cterm (Cterm args) = args;


266 


267 
(*Return the underlying term*)


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


269 


270 
(** pretty printing of terms **)


271 


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


273 


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


275 


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


277 


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


279 


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


281 


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


283 
fun cterm_of sign t =


284 
case term_errors sign (t,[]) of


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


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


287 


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


289 


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


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

19

292 
(a,T) =

0

293 
let val showtyp = string_of_typ sign


294 
and showterm = string_of_term sign


295 
fun termerr [] = ""

19

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


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


298 
cat_lines (map showterm ts)

0

299 
val t = Syntax.read syn T a;


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

19

301 
sorts, showtyp, T, t)


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


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


304 
cat_lines (map showtyp Ts) ^ termerr ts)

0

305 
in (cterm_of sign t', tye)


306 
end


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


308 


309 


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


311 


312 
(** reading of instantiations **)


313 


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

19

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

0

316 


317 
fun absent ixn =


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


319 


320 
fun inst_failure ixn =


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


322 


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


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


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

19

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


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

0

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


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

19

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


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


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


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


334 
else inst_failure ixn


335 
end

0

336 
val tye = map readT tvs;


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

19

338 
let val T = case rtypes ixn of


339 
Some T => typ_subst_TVars tye T


340 
 None => absent ixn;


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


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


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

0

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


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


346 


347 
end;

143

348 
