# HG changeset patch # User huffman # Date 1118785477 -7200 # Node ID 495dbcd4f4c907a61e37e062ce046a8a799e154d # Parent 4bc08baa3fbb2076efc170fa90b6614b8fe1bed6 in domain declarations, selector names are now optional diff -r 4bc08baa3fbb -r 495dbcd4f4c9 src/HOLCF/domain/axioms.ML --- 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 ------------------------- *) diff -r 4bc08baa3fbb -r 495dbcd4f4c9 src/HOLCF/domain/extender.ML --- 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 diff -r 4bc08baa3fbb -r 495dbcd4f4c9 src/HOLCF/domain/interface.ML --- 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), diff -r 4bc08baa3fbb -r 495dbcd4f4c9 src/HOLCF/domain/library.ML --- 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 *) diff -r 4bc08baa3fbb -r 495dbcd4f4c9 src/HOLCF/domain/syntax.ML --- 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; diff -r 4bc08baa3fbb -r 495dbcd4f4c9 src/HOLCF/domain/theorems.ML --- 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;