18060

1 
(* Title: Pure/consts.ML


2 
ID: $Id$


3 
Author: Makarius


4 

18935

5 
Polymorphic constants: declarations, abbreviations, additional type


6 
constraints.

18060

7 
*)


8 


9 
signature CONSTS =


10 
sig


11 
type T

18935

12 
val dest: T >


13 
{constants: (typ * term option) NameSpace.table,


14 
constraints: typ NameSpace.table}

18965

15 
val space_of: T > NameSpace.T


16 
val abbrevs_of: T > (term * term) list

18935

17 
val declaration: T > string > typ (*exception TYPE*)


18 
val monomorphic: T > string > bool (*exception TYPE*)


19 
val constraint: T > string > typ (*exception TYPE*)


20 
val certify: Pretty.pp > Type.tsig > T > term > term (*exception TYPE*)

18965

21 
val read_const: T > string > term

18146

22 
val typargs: T > string * typ > typ list

18163

23 
val instance: T > string * typ list > typ

18060

24 
val declare: NameSpace.naming > bstring * typ > T > T

18965

25 
val abbreviate: Pretty.pp > Type.tsig > NameSpace.naming > bool > string * term > T > T

18060

26 
val constrain: string * typ > T > T


27 
val hide: bool > string > T > T


28 
val empty: T


29 
val merge: T * T > T


30 
end


31 


32 
structure Consts: CONSTS =


33 
struct


34 


35 
(** datatype T **)


36 

18935

37 
datatype decl =


38 
LogicalConst of typ * int list list 


39 
Abbreviation of typ * term;


40 

18060

41 
datatype T = Consts of

18935

42 
{decls: (decl * serial) NameSpace.table,

18965

43 
abbrevs: (term * term) list,

18060

44 
constraints: typ Symtab.table};


45 

18965

46 
fun make_consts (decls, abbrevs, constraints) =


47 
Consts {decls = decls, abbrevs = abbrevs, constraints = constraints};

18060

48 

18965

49 
fun map_consts f (Consts {decls, abbrevs, constraints}) =


50 
make_consts (f (decls, abbrevs, constraints));


51 


52 
fun dest (Consts {decls = (space, decls), abbrevs = _, constraints}) =

18935

53 
{constants = (space, Symtab.fold


54 
(fn (c, (LogicalConst (T, _), _)) => Symtab.update (c, (T, NONE))


55 
 (c, (Abbreviation (T, t), _)) => Symtab.update (c, (T, SOME t))) decls Symtab.empty),

18060

56 
constraints = (space, constraints)};


57 

18965

58 
fun space_of (Consts {decls = (space, _), ...}) = space;


59 
fun abbrevs_of (Consts {abbrevs, ...}) = abbrevs;

18060

60 


61 


62 
(* lookup consts *)


63 

18935

64 
fun err_undeclared c = raise TYPE ("Undeclared constant: " ^ quote c, [], []);


65 


66 
fun the_const (Consts {decls = (_, tab), ...}) c =


67 
(case Symtab.lookup tab c of SOME (decl, _) => decl  NONE => err_undeclared c);


68 


69 
fun logical_const consts c =


70 
(case the_const consts c of LogicalConst d => d  _ => err_undeclared c);

18060

71 

18935

72 
fun declaration consts c = #1 (logical_const consts c);


73 
fun monomorphic consts c = null (#2 (logical_const consts c));


74 

18060

75 
fun constraint (consts as Consts {constraints, ...}) c =


76 
(case Symtab.lookup constraints c of


77 
SOME T => T

18935

78 
 NONE => (case the_const consts c of LogicalConst (T, _) => T  Abbreviation (T, _) => T));


79 


80 

18965

81 
(* certify: check/expand consts *)

18060

82 

18965

83 
fun certify pp tsig consts =


84 
let


85 
fun err msg (c, T) =


86 
raise TYPE (msg ^ " " ^ quote c ^ " :: " ^ Pretty.string_of_typ pp T, [], []);


87 
fun cert tm =


88 
let


89 
val (head, args) = Term.strip_comb tm;


90 
val args' = map cert args;


91 
in


92 
(case head of


93 
Const (c, T) =>


94 
(case the_const consts c of


95 
LogicalConst (U, _) =>


96 
if Type.typ_instance tsig (T, U) then Term.list_comb (head, args')


97 
else err "Illegal type for constant" (c, T)


98 
 Abbreviation (U, u) =>


99 
Term.betapplys (Envir.expand_atom tsig T (U, u) handle TYPE _ =>


100 
err "Illegal type for abbreviation" (c, T), args'))


101 
 Abs (x, T, t) => Term.list_comb (Abs (x, T, cert t), args')


102 
 _ => Term.list_comb (head, args'))


103 
end;


104 
in cert end;


105 


106 


107 
(* read_const *)


108 


109 
fun read_const consts raw_c =


110 
let


111 
val c = NameSpace.intern (space_of consts) raw_c;


112 
val _ = the_const consts c handle TYPE (msg, _, _) => error msg;


113 
in Const (c, dummyT) end;

18060

114 


115 


116 
(* typargs  view actual const type as instance of declaration *)


117 


118 
fun sub (Type (_, Ts)) (i :: is) = sub (nth Ts i) is


119 
 sub T [] = T


120 
 sub T _ = raise Subscript;


121 

18935

122 
fun typargs consts (c, T) = map (sub T) (#2 (logical_const consts c));

18060

123 

18163

124 
fun instance consts (c, Ts) =


125 
let


126 
val declT = declaration consts c;


127 
val vars = map Term.dest_TVar (typargs consts (c, declT));


128 
in declT > Term.instantiateT (vars ~~ Ts) end;


129 

18060

130 


131 

18935

132 
(** declare consts **)

18060

133 


134 
fun err_dup_consts cs =


135 
error ("Duplicate declaration of constant(s) " ^ commas_quote cs);


136 


137 
fun err_inconsistent_constraints cs =


138 
error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs);


139 

18935

140 
fun extend_decls naming decl tab = NameSpace.extend_table naming (tab, [decl])


141 
handle Symtab.DUPS cs => err_dup_consts cs;

18060

142 

18935

143 


144 
(* name space *)

18060

145 

18965

146 
fun hide fully c = map_consts (fn (decls, abbrevs, constraints) =>


147 
(apfst (NameSpace.hide fully c) decls, abbrevs, constraints));

18935

148 


149 


150 
(* declarations *)


151 

18965

152 
fun declare naming (c, declT) = map_consts (fn (decls, abbrevs, constraints) =>

18060

153 
let

18935

154 
fun args_of (Type (_, Ts)) pos = args_of_list Ts 0 pos


155 
 args_of (TVar v) pos = insert (eq_fst op =) (v, rev pos)


156 
 args_of (TFree _) _ = I


157 
and args_of_list (T :: Ts) i is = args_of T (i :: is) #> args_of_list Ts (i + 1) is


158 
 args_of_list [] _ _ = I;


159 
val decl = (c, (LogicalConst (declT, map #2 (rev (args_of declT [] []))), serial ()));

18965

160 
in (extend_decls naming decl decls, abbrevs, constraints) end);

18060

161 

18935

162 


163 
(* abbreviations *)


164 

18965

165 
fun revert_abbrev const rhs =

18060

166 
let

18965

167 
val (xs, body) = Term.strip_abs (Envir.beta_eta_contract rhs);


168 
val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) [];


169 
in (Term.list_comb (Const const, vars), Term.subst_bounds (rev vars, body)) end;


170 


171 
fun abbreviate pp tsig naming revert (c, raw_rhs) consts =


172 
consts > map_consts (fn (decls, abbrevs, constraints) =>


173 
let


174 
val rhs = certify pp tsig consts raw_rhs;


175 
val T = Term.fastype_of rhs;


176 
val decls' = decls > extend_decls naming (c, (Abbreviation (T, rhs), serial ()));


177 
val abbrevs' =


178 
if revert then revert_abbrev (NameSpace.full naming c, T) rhs :: abbrevs else abbrevs;


179 
in (decls', abbrevs', constraints) end);

18935

180 

18060

181 

18935

182 
(* constraints *)

18060

183 

18965

184 
fun constrain (c, T) = map_consts (fn (decls, abbrevs, constraints) =>


185 
(decls, abbrevs, Symtab.update (c, T) constraints));

18060

186 


187 


188 
(* empty and merge *)


189 

18965

190 
val empty = make_consts (NameSpace.empty_table, [], Symtab.empty);

18060

191 


192 
fun merge

18965

193 
(Consts {decls = decls1, abbrevs = abbrevs1, constraints = constraints1},


194 
Consts {decls = decls2, abbrevs = abbrevs2, constraints = constraints2}) =

18060

195 
let

18935

196 
val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)

18060

197 
handle Symtab.DUPS cs => err_dup_consts cs;

18965

198 
val abbrevs' =


199 
Library.merge (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') (abbrevs1, abbrevs2);

18935

200 
val constraints' = Symtab.merge (op =) (constraints1, constraints2)

18060

201 
handle Symtab.DUPS cs => err_inconsistent_constraints cs;

18965

202 
in make_consts (decls', abbrevs', constraints') end;

18060

203 


204 
end;
