--- a/src/HOLCF/domain/axioms.ML Thu Nov 03 02:37:09 2005 +0100
+++ b/src/HOLCF/domain/axioms.ML Thu Nov 03 03:06:02 2005 +0100
@@ -84,7 +84,7 @@
val reach_ax = ("reach", mk_trp(cproj (%%:fixN`%%(comp_dname^"_copy")) eqs n
`%x_name === %:x_name));
- val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj'
+ val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj
(%%:iterateN $ Bound 0 ` %%:(comp_dname^"_copy") ` UU) eqs n));
val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name,
mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
--- a/src/HOLCF/domain/extender.ML Thu Nov 03 02:37:09 2005 +0100
+++ b/src/HOLCF/domain/extender.ML Thu Nov 03 03:06:02 2005 +0100
@@ -25,8 +25,11 @@
signature DOMAIN_EXTENDER =
sig
- val add_domain: string *
- ((bstring * string list) * (string * mixfix * (bool * string option * string) list) list) list
+ val add_domain: string * ((bstring * string list) *
+ (string * mixfix * (bool * string option * string) list) list) list
+ -> theory -> theory
+ val add_domain_i: string * ((bstring * string list) *
+ (string * mixfix * (bool * string option * typ) list) list) list
-> theory -> theory
end;
@@ -36,8 +39,8 @@
open Domain_Library;
(* ----- general testing and preprocessing of constructor list -------------- *)
- fun check_and_sort_domain (dtnvs: (string * typ list) list,
- cons'' : ((string * mixfix * (bool*string option*typ) list) list) list) sg =
+fun check_and_sort_domain (dtnvs: (string * typ list) list,
+ cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg =
let
val defaultS = Sign.defaultS sg;
val test_dupl_typs = (case duplicates (map fst dtnvs) of
@@ -57,9 +60,7 @@
fun analyse_equation ((dname,typevars),cons') =
let
val tvars = map dest_TFree typevars;
- fun distinct_name s = "'"^Sign.base_name dname^"_"^s;
- val distinct_typevars = map (fn (n,sort) =>
- TFree (distinct_name n,sort)) tvars;
+ val distinct_typevars = map TFree tvars;
fun rm_sorts (TFree(s,_)) = TFree(s,[])
| rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
| rm_sorts (TVar(s,_)) = TVar(s,[])
@@ -69,7 +70,7 @@
NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
| SOME sort => if eq_set_string (s,defaultS) orelse
eq_set_string (s,sort )
- then TFree(distinct_name v,sort)
+ then TFree(v,sort)
else error ("Inconsistent sort constraint" ^
" for type variable " ^ quote v))
| analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of
@@ -87,8 +88,8 @@
quote (string_of_typ sg t) ^
" with different arguments"))
| analyse indirect (TVar _) = Imposs "extender:analyse";
- fun check_pcpo t = (pcpo_type sg t orelse error(
- "Constructor argument type is not of sort pcpo: "^string_of_typ sg t); t);
+ fun check_pcpo T = if pcpo_type sg T then T
+ else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T);
val analyse_con = upd_third (map (upd_third (check_pcpo o analyse false)));
in ((dname,distinct_typevars), map analyse_con cons') end;
in ListPair.map analyse_equation (dtnvs,cons'')
@@ -96,46 +97,49 @@
(* ----- calls for building new thy and thms -------------------------------- *)
- fun add_domain (comp_dnam,eqs''') thy''' = let
- val sg''' = sign_of thy''';
+fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
+ let
val dtnvs = map ((fn (dname,vs) =>
- (Sign.full_name sg''' dname,map (str2typ sg''') vs))
+ (Sign.full_name thy''' dname, map (str2typ thy''') vs))
o fst) eqs''';
val cons''' = map snd eqs''';
fun thy_type (dname,tvars) = (Sign.base_name dname, length tvars, NoSyn);
fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS);
val thy'' = thy''' |> Theory.add_types (map thy_type dtnvs)
|> Theory.add_arities_i (map thy_arity dtnvs);
- val sg'' = sign_of thy'';
- val cons''=map (map (upd_third (map (upd_third (str2typ sg''))))) cons''';
- val eqs' = check_and_sort_domain (dtnvs,cons'') sg'';
+ val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
+ val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
val dts = map (Type o fst) eqs';
+ val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
fun typid (Type (id,_)) =
let val c = hd (Symbol.explode (Sign.base_name id))
in if Symbol.is_letter c then c else "t" end
| typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
| typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
- fun cons cons' = (map (fn (con,syn,args) =>
- ((Syntax.const_name con syn),
+ fun one_con (con,mx,args) =
+ ((Syntax.const_name con mx),
ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
- find_index_eq tp dts),
+ find_index_eq tp dts,
+ DatatypeAux.dtyp_of_typ new_dts tp),
sel,vn))
(args,(mk_var_names(map (typid o third) args)))
- )) cons') : cons list;
- val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list;
+ ) : cons;
+ val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
val (theorems_thy, (rewss, take_rews)) = (foldl_map (fn (thy0,eq) =>
Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs))
|>>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
-in
- theorems_thy
- |> Theory.add_path (Sign.base_name comp_dnam)
- |> (#1 o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
- |> Theory.parent_path
-end;
+ in
+ theorems_thy
+ |> Theory.add_path (Sign.base_name comp_dnam)
+ |> (#1 o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
+ |> Theory.parent_path
+ end;
+val add_domain_i = gen_add_domain Sign.certify_typ;
+val add_domain = gen_add_domain str2typ;
(** outer syntax **)
@@ -174,6 +178,6 @@
val _ = OuterSyntax.add_keywords ["lazy"];
val _ = OuterSyntax.add_parsers [domainP];
-end;
+end; (* local structure *)
end;
--- a/src/HOLCF/domain/library.ML Thu Nov 03 02:37:09 2005 +0100
+++ b/src/HOLCF/domain/library.ML Thu Nov 03 03:06:02 2005 +0100
@@ -77,17 +77,17 @@
(* ----- constructor list handling ----- *)
-type cons = (string * (* operator name of constr *)
- ((bool*int)* (* (lazy,recursive element or ~1) *)
- string option* (* selector name *)
- string) (* argument name *)
- list); (* argument list *)
+type cons = (string * (* operator name of constr *)
+ ((bool*int*DatatypeAux.dtyp)* (* (lazy,recursive element or ~1) *)
+ string option* (* selector name *)
+ string) (* argument name *)
+ list); (* argument list *)
type eq = (string * (* name of abstracted type *)
typ list) * (* arguments of abstracted type *)
cons list; (* represented type, as a constructor list *)
-fun rec_of arg = snd (first arg);
-fun is_lazy arg = fst (first arg);
+fun rec_of arg = second (first arg);
+fun is_lazy arg = first (first arg);
val sel_of = second;
val vname = third;
val upd_vname = upd_third;
@@ -185,17 +185,8 @@
fun prj _ _ x ( _::[]) _ = x
| prj f1 _ x (_::y::ys) 0 = f1 x y
| prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1);
-fun fix_tp (tn, args) = (tn, map (K oneT) args); (* instantiate type to
- avoid type varaibles *)
fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
fun cproj x = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x;
-fun prj' _ _ x ( _::[]) _ = x
-| prj' f1 _ x (_:: ys) 0 = f1 x (foldr1 HOLogic.mk_prodT ys)
-| prj' f1 f2 x (y:: ys) j = prj' f1 f2 (f2 x y) ys (j-1);
-fun cproj' T eqs = prj'
- (fn S => fn t => Const(cfstN, HOLogic.mk_prodT(dummyT,t)->>dummyT)`S)
- (fn S => fn t => Const(csndN, HOLogic.mk_prodT(t,dummyT)->>dummyT)`S)
- T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs);
fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
fun /\ v T = %%:Abs_CFunN $ mk_lam(v,T);