18060

1 
(* Title: Pure/consts.ML


2 
ID: $Id$


3 
Author: Makarius


4 


5 
Polymorphic constants.


6 
*)


7 


8 
signature CONSTS =


9 
sig


10 
type T


11 
val dest: T > {declarations: typ NameSpace.table, constraints: typ NameSpace.table}


12 
val space: T > NameSpace.T


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


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


15 
val monomorphic: T > string > bool


16 
val typargs: T > string > typ > typ list


17 
val modify_typargs: T > string > (typ list > typ list) > typ > typ


18 
val map_typargs: T > string > (typ > typ) > typ > typ


19 
val fold_typargs: T > string > (typ > 'a > 'a) > typ > 'a > 'a


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


21 
val constrain: string * typ > T > T


22 
val hide: bool > string > T > T


23 
val empty: T


24 
val merge: T * T > T


25 
end


26 


27 
structure Consts: CONSTS =


28 
struct


29 


30 


31 
(** datatype T **)


32 


33 
type arg = (indexname * sort) * int list; (*type variable with first occurrence*)


34 


35 
datatype T = Consts of


36 
{declarations: ((typ * arg list) * serial) NameSpace.table,


37 
constraints: typ Symtab.table};


38 


39 
fun make_consts (declarations, constraints) =


40 
Consts {declarations = declarations, constraints = constraints};


41 


42 
fun map_consts f (Consts {declarations, constraints}) =


43 
make_consts (f (declarations, constraints));


44 


45 
fun dest (Consts {declarations = (space, decls), constraints}) =


46 
{declarations = (space, Symtab.map (#1 o #1) decls),


47 
constraints = (space, constraints)};


48 


49 
fun space (Consts {declarations = (space, _), ...}) = space;


50 


51 


52 
(* lookup consts *)


53 


54 
fun the_const (Consts {declarations = (_, decls), ...}) c =


55 
(case Symtab.lookup decls c of SOME (decl, _) => decl


56 
 NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));


57 


58 
fun declaration consts c = #1 (the_const consts c);


59 


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


61 
(case Symtab.lookup constraints c of


62 
SOME T => T


63 
 NONE => declaration consts c);


64 


65 
fun monomorphic consts c = null (#2 (the_const consts c));


66 


67 


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


69 


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


71 
 sub T [] = T


72 
 sub T _ = raise Subscript;


73 


74 
fun typargs consts c =


75 
let val (_, args) = the_const consts c


76 
in fn T => map (sub T o #2) args end;


77 


78 
fun modify_typargs consts c =


79 
let val (declT, args) = the_const consts c in


80 
fn f => fn T =>


81 
let


82 
val Us = f (map (sub T o #2) args);


83 
val _ =


84 
if length args = length Us then ()


85 
else raise TYPE ("modify_typargs: bad number of args", [T], []);


86 
val inst = ListPair.map (fn ((v, _), U) => (v, U)) (args, Us);


87 
in declT > Term.instantiateT inst end


88 
end;


89 


90 
fun map_typargs consts c =


91 
let val (declT, args) = the_const consts c in


92 
fn f => fn T => declT > Term.instantiateT (args > map (fn (v, pos) => (v, f (sub T pos))))


93 
end;


94 


95 
fun fold_typargs consts c =


96 
let val (_, args) = the_const consts c


97 
in fn f => fn T => fold (f o sub T o #2) args end;


98 


99 


100 


101 
(** build consts **)


102 


103 
fun err_dup_consts cs =


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


105 


106 
fun err_inconsistent_constraints cs =


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


108 


109 


110 
(* declarations etc. *)


111 


112 
fun args_of declT =


113 
let


114 
fun args (Type (_, Ts)) pos = args_list Ts 0 pos


115 
 args (TVar v) pos = insert (eq_fst op =) (v, rev pos)


116 
 args (TFree _) _ = I


117 
and args_list (T :: Ts) i is = args T (i :: is) #> args_list Ts (i + 1) is


118 
 args_list [] _ _ = I;


119 
in rev (args declT [] []) end;


120 


121 
fun declare naming (c, T) = map_consts (apfst (fn declarations =>


122 
let


123 
val decl = (c, ((T, args_of T), serial ()));


124 
val declarations' = NameSpace.extend_table naming (declarations, [decl])


125 
handle Symtab.DUPS cs => err_dup_consts cs;


126 
in declarations' end));


127 


128 
val constrain = map_consts o apsnd o Symtab.update;


129 


130 
fun hide fully c = map_consts (apfst (apfst (NameSpace.hide fully c)));


131 


132 


133 
(* empty and merge *)


134 


135 
val empty = make_consts (NameSpace.empty_table, Symtab.empty);


136 


137 
fun merge


138 
(Consts {declarations = declarations1, constraints = constraints1},


139 
Consts {declarations = declarations2, constraints = constraints2}) =


140 
let


141 
val declarations = NameSpace.merge_tables (eq_snd (op =)) (declarations1, declarations2)


142 
handle Symtab.DUPS cs => err_dup_consts cs;


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


144 
handle Symtab.DUPS cs => err_inconsistent_constraints cs;


145 
in make_consts (declarations, constraints) end;


146 


147 
end;
