18 open Domain_Library; |
18 open Domain_Library; |
19 |
19 |
20 (* ----- general testing and preprocessing of constructor list -------------------- *) |
20 (* ----- general testing and preprocessing of constructor list -------------------- *) |
21 |
21 |
22 fun check_domain(eqs':((string * typ list) * |
22 fun check_domain(eqs':((string * typ list) * |
23 (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) = let |
23 (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) = let |
24 val dtnvs = map fst eqs'; |
24 val dtnvs = map fst eqs'; |
25 val cons' = flat (map snd eqs'); |
25 val cons' = flat (map snd eqs'); |
26 val test_dupl_typs = (case duplicates (map fst dtnvs) of |
26 val test_dupl_typs = (case duplicates (map fst dtnvs) of |
27 [] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); |
27 [] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); |
28 val test_dupl_cons = (case duplicates (map first cons') of |
28 val test_dupl_cons = (case duplicates (map first cons') of |
29 [] => false | dups => error ("Duplicate constructors: " ^ commas_quote dups)); |
29 [] => false | dups => error ("Duplicate constructors: " ^ commas_quote dups)); |
30 val test_dupl_sels = (case duplicates(map second (flat(map third cons'))) of |
30 val test_dupl_sels = (case duplicates(map second (flat(map third cons'))) of |
31 [] => false | dups => error ("Duplicate selectors: "^commas_quote dups)); |
31 [] => false | dups => error ("Duplicate selectors: "^commas_quote dups)); |
32 val test_dupl_tvars = let fun vname (TFree(v,_)) = v |
32 val test_dupl_tvars = let fun vname (TFree(v,_)) = v |
33 | vname _ = Imposs "extender:vname"; |
33 | vname _ = Imposs "extender:vname"; |
34 in exists (fn tvars => case duplicates (map vname tvars) of |
34 in exists (fn tvars => case duplicates (map vname tvars) of |
35 [] => false | dups => error ("Duplicate type arguments: " ^commas_quote dups)) |
35 [] => false | dups => error ("Duplicate type arguments: " ^commas_quote dups)) |
36 (map snd dtnvs) end; |
36 (map snd dtnvs) end; |
37 (*test for free type variables and invalid use of recursive type*) |
37 (*test for free type variables and invalid use of recursive type*) |
38 val analyse_types = forall (fn ((_,typevars),cons') => |
38 val analyse_types = forall (fn ((_,typevars),cons') => |
39 forall (fn con' => let |
39 forall (fn con' => let |
40 val types = map third (third con'); |
40 val types = map third (third con'); |
41 fun analyse(t as TFree(v,_)) = t mem typevars orelse |
41 fun analyse(t as TFree(v,_)) = t mem typevars orelse |
42 error ("Free type variable " ^ v ^ " on rhs.") |
42 error ("Free type variable " ^ v ^ " on rhs.") |
43 | analyse(Type(s,typl)) = (case assoc (dtnvs,s) of None => analyses typl |
43 | analyse(Type(s,typl)) = (case assoc (dtnvs,s) of None => analyses typl |
44 | Some tvs => tvs = typl orelse |
44 | Some tvs => tvs = typl orelse |
45 error ("Recursion of type " ^ s ^ " with different arguments")) |
45 error ("Recursion of type " ^ s ^ " with different arguments")) |
46 | analyse(TVar _) = Imposs "extender:analyse" |
46 | analyse(TVar _) = Imposs "extender:analyse" |
47 and analyses ts = forall analyse ts; |
47 and analyses ts = forall analyse ts; |
48 in analyses types end) cons' |
48 in analyses types end) cons' |
49 ) eqs'; |
49 ) eqs'; |
50 in true end; (* let *) |
50 in true end; (* let *) |
51 |
51 |
52 fun check_gen_by thy' (typs': string list,cnstrss': string list list) = let |
52 fun check_gen_by thy' (typs': string list,cnstrss': string list list) = let |
53 val test_dupl_typs = (case duplicates typs' of [] => false |
53 val test_dupl_typs = (case duplicates typs' of [] => false |
54 | dups => error ("Duplicate types: " ^ commas_quote dups)); |
54 | dups => error ("Duplicate types: " ^ commas_quote dups)); |
55 val test_dupl_cnstrs = map (fn cnstrs' => (case duplicates cnstrs' of [] => false |
55 val test_dupl_cnstrs = map (fn cnstrs' => (case duplicates cnstrs' of [] => false |
56 | dups => error ("Duplicate constructors: " ^ commas_quote dups))) cnstrss'; |
56 | dups => error ("Duplicate constructors: " ^ commas_quote dups))) cnstrss'; |
57 val tsig = #tsig(Sign.rep_sg(sign_of thy')); |
57 val tsig = #tsig(Sign.rep_sg(sign_of thy')); |
58 val tycons = map fst (#tycons(Type.rep_tsig tsig)); |
58 val tycons = map fst (#tycons(Type.rep_tsig tsig)); |
59 val test_types = forall(fn t=>t mem tycons orelse error("Unknown type: "^t))typs'; |
59 val test_types = forall(fn t=>t mem tycons orelse error("Unknown type: "^t))typs'; |
60 val cnstrss = let |
60 val cnstrss = let |
61 fun type_of c = case (Sign.const_type(sign_of thy') c) of Some t => t |
61 fun type_of c = case (Sign.const_type(sign_of thy') c) of Some t => t |
62 | None => error ("Unknown constructor: "^c); |
62 | None => error ("Unknown constructor: "^c); |
63 fun args_result_type (t as (Type(tn,[arg,rest]))) = |
63 fun args_result_type (t as (Type(tn,[arg,rest]))) = |
64 if tn = "->" orelse tn = "=>" |
64 if tn = "->" orelse tn = "=>" |
65 then let val (ts,r) = args_result_type rest in (arg::ts,r) end |
65 then let val (ts,r) = args_result_type rest in (arg::ts,r) end |
66 else ([],t) |
66 else ([],t) |
67 | args_result_type t = ([],t); |
67 | args_result_type t = ([],t); |
68 in map (map (fn cn => let val (args,res) = args_result_type (type_of cn) in |
68 in map (map (fn cn => let val (args,res) = args_result_type (type_of cn) in |
69 (cn,mk_var_names args,(args,res)) end)) cnstrss' |
69 (cn,mk_var_names args,(args,res)) end)) cnstrss' |
70 : (string * (* operator name of constr *) |
70 : (string * (* operator name of constr *) |
71 string list * (* argument name list *) |
71 string list * (* argument name list *) |
72 (typ list * (* argument types *) |
72 (typ list * (* argument types *) |
73 typ)) (* result type *) |
73 typ)) (* result type *) |
74 list list end; |
74 list list end; |
75 fun test_equal_type tn (cn,_,(_,rt)) = fst (type_name_vars rt) = tn orelse |
75 fun test_equal_type tn (cn,_,(_,rt)) = fst (type_name_vars rt) = tn orelse |
76 error("Inappropriate result type for constructor "^cn); |
76 error("Inappropriate result type for constructor "^cn); |
77 val typs = map (fn (tn, cnstrs) => |
77 val typs = map (fn (tn, cnstrs) => |
78 (map (test_equal_type tn) cnstrs; snd(third(hd(cnstrs))))) |
78 (map (test_equal_type tn) cnstrs; snd(third(hd(cnstrs))))) |
79 (typs'~~cnstrss); |
79 (typs'~~cnstrss); |
80 val test_typs = map (fn (typ,cnstrs) => |
80 val test_typs = map (fn (typ,cnstrs) => |
81 if not (Type.typ_instance(tsig,typ,TVar(("'a",0),["pcpo"]))) |
81 if not (Type.typ_instance(tsig,typ,TVar(("'a",0),["pcpo"]))) |
82 then error("Not a pcpo type: "^fst(type_name_vars typ)) |
82 then error("Not a pcpo type: "^fst(type_name_vars typ)) |
83 else map (fn (cn,_,(_,rt)) => rt=typ |
83 else map (fn (cn,_,(_,rt)) => rt=typ |
84 orelse error("Non-identical result types for constructors "^ |
84 orelse error("Non-identical result types for constructors "^ |
85 first(hd cnstrs)^" and "^ cn )) cnstrs) (typs~~cnstrss); |
85 first(hd cnstrs)^" and "^ cn )) cnstrs) (typs~~cnstrss); |
86 val proper_args = let |
86 val proper_args = let |
87 fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts |
87 fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts |
88 | occurs _ _ = false; |
88 | occurs _ _ = false; |
89 fun proper_arg cn atyp = forall (fn typ => let |
89 fun proper_arg cn atyp = forall (fn typ => let |
90 val tn = fst(type_name_vars typ) |
90 val tn = fst(type_name_vars typ) |
91 in atyp=typ orelse not (occurs tn atyp) orelse |
91 in atyp=typ orelse not (occurs tn atyp) orelse |
92 error("Illegal use of type "^ tn ^ |
92 error("Illegal use of type "^ tn ^ |
93 " as argument of constructor " ^cn)end )typs; |
93 " as argument of constructor " ^cn)end )typs; |
94 fun proper_curry (cn,_,(args,_)) = forall (proper_arg cn) args; |
94 fun proper_curry (cn,_,(args,_)) = forall (proper_arg cn) args; |
95 in map (map proper_curry) cnstrss end; |
95 in map (map proper_curry) cnstrss end; |
96 in (typs, flat cnstrss) end; |
96 in (typs, flat cnstrss) end; |
97 |
97 |
98 (* ----- calls for building new thy and thms -------------------------------------- *) |
98 (* ----- calls for building new thy and thms -------------------------------------- *) |
99 |
99 |
102 fun add_domain (comp_dname,eqs') thy'' = let |
102 fun add_domain (comp_dname,eqs') thy'' = let |
103 val ok_dummy = check_domain eqs'; |
103 val ok_dummy = check_domain eqs'; |
104 val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dname,eqs'); |
104 val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dname,eqs'); |
105 val dts = map (Type o fst) eqs'; |
105 val dts = map (Type o fst) eqs'; |
106 fun cons cons' = (map (fn (con,syn,args) => |
106 fun cons cons' = (map (fn (con,syn,args) => |
107 (ThyOps.const_name con syn, |
107 (ThyOps.const_name con syn, |
108 map (fn ((lazy,sel,tp),vn) => ((lazy, |
108 map (fn ((lazy,sel,tp),vn) => ((lazy, |
109 find (tp,dts) handle LIST "find" => ~1), |
109 find (tp,dts) handle LIST "find" => ~1), |
110 sel,vn)) |
110 sel,vn)) |
111 (args~~(mk_var_names(map third args))) |
111 (args~~(mk_var_names(map third args))) |
112 )) cons') : cons list; |
112 )) cons') : cons list; |
113 val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list; |
113 val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list; |
114 val thy = thy' |> Domain_Axioms.add_axioms (comp_dname,eqs); |
114 val thy = thy' |> Domain_Axioms.add_axioms (comp_dname,eqs); |
115 in (thy,eqs) end; |
115 in (thy,eqs) end; |
116 |
116 |
117 fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let |
117 fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let |