--- a/src/HOLCF/domain/axioms.ML Tue Jun 14 22:19:32 2005 +0200
+++ b/src/HOLCF/domain/axioms.ML Tue Jun 14 23:44:37 2005 +0200
@@ -69,11 +69,11 @@
in map mdef cons end;
val sel_defs = let
- fun sdef con n arg = (sel_of arg^"_def",%%:(sel_of arg) ==
+ fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel ==
mk_cRep_CFun(%%:(dname^"_when"),map
(fn (con',args) => if con'<>con then %%:"UU" else
- foldr /\# (Bound (length args - n)) args) cons));
- in List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end;
+ foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
+ in List.mapPartial Id (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
(* ----- axiom and definitions concerning induction ------------------------- *)
--- a/src/HOLCF/domain/extender.ML Tue Jun 14 22:19:32 2005 +0200
+++ b/src/HOLCF/domain/extender.ML Tue Jun 14 23:44:37 2005 +0200
@@ -26,7 +26,7 @@
signature DOMAIN_EXTENDER =
sig
val add_domain: string *
- ((bstring * string list) * (string * mixfix * (bool * string * string) list) list) list
+ ((bstring * string list) * (string * mixfix * (bool * string option * string) list) list) list
-> theory -> theory
end;
@@ -36,9 +36,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*typ) list) list) list) sg =
+ 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
@@ -46,8 +45,8 @@
val test_dupl_cons = (case duplicates (map first (List.concat cons'')) of
[] => false | dups => error ("Duplicate constructors: "
^ commas_quote dups));
- val test_dupl_sels = (case duplicates
- (map second (List.concat (map third (List.concat cons'')))) of
+ val test_dupl_sels = (case duplicates (List.mapPartial second
+ (List.concat (map third (List.concat cons'')))) of
[] => false | dups => error("Duplicate selectors: "^commas_quote dups));
val test_dupl_tvars = exists(fn s=>case duplicates(map(fst o rep_TFree)s)of
[] => false | dups => error("Duplicate type arguments: "
@@ -145,7 +144,10 @@
val dest_decl =
P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
- P.name -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1;
+ (P.name >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
+ || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
+ >> (fn t => (true,NONE,t))
+ || P.typ >> (fn t => (false,NONE,t));
val cons_decl =
P.name -- Scan.repeat dest_decl -- P.opt_mixfix
--- a/src/HOLCF/domain/interface.ML Tue Jun 14 22:19:32 2005 +0200
+++ b/src/HOLCF/domain/interface.ML Tue Jun 14 23:44:37 2005 +0200
@@ -63,7 +63,7 @@
fun mk_conslist cons' =
mk_list (map (fn (c,syn,ts)=> "\n"^
mk_triple(Library.quote c, syn, mk_list (map (fn (b,s ,tp) =>
- mk_triple(Bool.toString b, Library.quote s, tp)) ts))) cons');
+ mk_triple(Bool.toString b, "SOME "^Library.quote s, tp)) ts))) cons');
in "val thy = thy |> Domain_Extender.add_domain "
^ mk_pair(Library.quote comp_dname, mk_list(map (fn ((n,vs),cs) => "\n"^
mk_pair (mk_pair (Library.quote n, mk_list vs),
--- a/src/HOLCF/domain/library.ML Tue Jun 14 22:19:32 2005 +0200
+++ b/src/HOLCF/domain/library.ML Tue Jun 14 23:44:37 2005 +0200
@@ -85,7 +85,7 @@
type cons = (string * (* operator name of constr *)
((bool*int)* (* (lazy,recursive element or ~1) *)
- string* (* selector name *)
+ string option* (* selector name *)
string) (* argument name *)
list); (* argument list *)
type eq = (string * (* name of abstracted type *)
--- a/src/HOLCF/domain/syntax.ML Tue Jun 14 22:19:32 2005 +0200
+++ b/src/HOLCF/domain/syntax.ML Tue Jun 14 23:44:37 2005 +0200
@@ -12,7 +12,7 @@
open Domain_Library;
infixr 5 -->; infixr 6 ->>;
fun calc_syntax dtypeprod ((dname, typevars),
- (cons': (string * mixfix * (bool*string*typ) list) list)) =
+ (cons': (string * mixfix * (bool*string option*typ) list) list)) =
let
(* ----- constants concerning the isomorphism ------------------------------- *)
@@ -49,7 +49,8 @@
to generate parse rules for non-alphanumeric names*)
fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_ssumT(oneT,mk_uT(mk_ctupleT(map third args))),
Mixfix(escape ("match_" ^ con), [], Syntax.max_pri));
- fun sel (_ ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ->> typ,NoSyn))args;
+ fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
+ fun sel (_ ,_,args) = List.mapPartial sel1 args;
in
val consts_con = map con cons';
val consts_dis = map dis cons';
@@ -100,7 +101,7 @@
in (* local *)
fun add_syntax (comp_dnam,eqs': ((string * typ list) *
- (string * mixfix * (bool*string*typ) list) list) list) thy'' =
+ (string * mixfix * (bool*string option*typ) list) list) list) thy'' =
let
val dtypes = map (Type o fst) eqs';
val boolT = HOLogic.boolT;
--- a/src/HOLCF/domain/theorems.ML Tue Jun 14 22:19:32 2005 +0200
+++ b/src/HOLCF/domain/theorems.ML Tue Jun 14 23:44:37 2005 +0200
@@ -70,8 +70,8 @@
val axs_con_def = map (fn (con,_) => ga (extern_name con^"_def") dname) cons;
val axs_dis_def = map (fn (con,_) => ga ( dis_name con^"_def") dname) cons;
val axs_mat_def = map (fn (con,_) => ga ( mat_name con^"_def") dname) cons;
-val axs_sel_def = List.concat(map (fn (_,args) =>
- map (fn arg => ga (sel_of arg ^"_def") dname) args)
+val axs_sel_def = List.concat(map (fn (_,args) => List.mapPartial (fn arg =>
+ Option.map (fn sel => ga (sel^"_def") dname) (sel_of arg)) args)
cons);
val ax_copy_def = ga "copy_def" dname;
end; (* local *)
@@ -246,7 +246,7 @@
val sel_stricts = let fun one_sel sel = pg axs_sel_def (mk_trp(strict(%%:sel))) [
simp_tac (HOLCF_ss addsimps when_rews) 1];
-in List.concat(map (fn (_,args) =>map (fn arg => one_sel (sel_of arg)) args) cons) end;
+in List.concat(map (fn (_,args) => List.mapPartial (fn arg => Option.map one_sel (sel_of arg)) args) cons) end;
val sel_apps = let fun one_sel c n sel = map (fn (con,args) =>
let val nlas = nonlazy args;
val vns = map vname args;
@@ -261,13 +261,13 @@
(List.nth(vns,n))] else [])
@ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
in List.concat(map (fn (c,args) =>
- List.concat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end;
-val sel_defins = if length cons=1 then map (fn arg => pg [](defined(%:x_name)==>
- defined(%%:(sel_of arg)`%x_name)) [
+ List.concat(List.mapPartial Id (mapn (fn n => fn arg => Option.map (one_sel c n) (sel_of arg)) 0 args))) cons) end;
+val sel_defins = if length cons=1 then List.mapPartial (fn arg => Option.map (fn sel => pg [](defined(%:x_name)==>
+ defined(%%:sel`%x_name)) [
rtac casedist 1,
contr_tac 1,
DETERM_UNTIL_SOLVED (CHANGED(asm_simp_tac
- (HOLCF_ss addsimps sel_apps) 1))])
+ (HOLCF_ss addsimps sel_apps) 1))])(sel_of arg))
(filter_out is_lazy (snd(hd cons))) else [];
val sel_rews = sel_stricts @ sel_defins @ sel_apps;