1274
|
1 |
(* extender.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author : David von Oheimb
|
|
4 |
Created: 17-May-95
|
|
5 |
Updated: 31-May-95 extracted syntax.ML, theorems.ML
|
|
6 |
Updated: 07-Jul-95 streamlined format of cons list
|
|
7 |
Updated: 21-Jul-95 gen_by-section
|
|
8 |
Updated: 28-Aug-95 simultaneous domain equations
|
|
9 |
Copyright 1995 TU Muenchen
|
|
10 |
*)
|
|
11 |
|
|
12 |
|
|
13 |
structure Extender =
|
|
14 |
struct
|
|
15 |
|
|
16 |
local
|
|
17 |
|
|
18 |
open Domain_Library;
|
|
19 |
|
|
20 |
(* ----- general testing and preprocessing of constructor list -------------------- *)
|
|
21 |
|
|
22 |
fun check_domain(eqs':((string * typ list) *
|
|
23 |
(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) = let
|
|
24 |
val dtnvs = map fst eqs';
|
|
25 |
val cons' = flat (map snd eqs');
|
|
26 |
val test_dupl_typs = (case duplicates (map fst dtnvs) of
|
|
27 |
[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
|
|
28 |
val test_dupl_cons = (case duplicates (map first cons') of
|
|
29 |
[] => false | dups => error ("Duplicate constructors: " ^ commas_quote dups));
|
|
30 |
val test_dupl_sels = (case duplicates(map second (flat(map third cons'))) of
|
|
31 |
[] => false | dups => error ("Duplicate selectors: "^commas_quote dups));
|
|
32 |
val test_dupl_tvars = let fun vname (TFree(v,_)) = v
|
|
33 |
| vname _ = Imposs "extender:vname";
|
|
34 |
in exists (fn tvars => case duplicates (map vname tvars) of
|
|
35 |
[] => false | dups => error ("Duplicate type arguments: " ^commas_quote dups))
|
|
36 |
(map snd dtnvs) end;
|
|
37 |
(*test for free type variables and invalid use of recursive type*)
|
|
38 |
val analyse_types = forall (fn ((_,typevars),cons') =>
|
|
39 |
forall (fn con' => let
|
|
40 |
val types = map third (third con');
|
|
41 |
fun analyse(t as TFree(v,_)) = t mem typevars orelse
|
|
42 |
error ("Free type variable " ^ v ^ " on rhs.")
|
|
43 |
| analyse(Type(s,typl)) = (case assoc (dtnvs,s) of None => analyses typl
|
|
44 |
| Some tvs => tvs = typl orelse
|
|
45 |
error ("Recursion of type " ^ s ^ " with different arguments"))
|
|
46 |
| analyse(TVar _) = Imposs "extender:analyse"
|
|
47 |
and analyses ts = forall analyse ts;
|
|
48 |
in analyses types end) cons'
|
|
49 |
) eqs';
|
|
50 |
in true end; (* let *)
|
|
51 |
|
|
52 |
fun check_gen_by thy' (typs': string list,cnstrss': string list list) = let
|
|
53 |
val test_dupl_typs = (case duplicates typs' of [] => false
|
|
54 |
| dups => error ("Duplicate types: " ^ commas_quote dups));
|
|
55 |
val test_dupl_cnstrs = map (fn cnstrs' => (case duplicates cnstrs' of [] => false
|
|
56 |
| dups => error ("Duplicate constructors: " ^ commas_quote dups))) cnstrss';
|
|
57 |
val tsig = #tsig(Sign.rep_sg(sign_of thy'));
|
|
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';
|
|
60 |
val cnstrss = let
|
|
61 |
fun type_of c = case (Sign.const_type(sign_of thy') c) of Some t => t
|
|
62 |
| None => error ("Unknown constructor: "^c);
|
|
63 |
fun args_result_type (t as (Type(tn,[arg,rest]))) =
|
|
64 |
if tn = "->" orelse tn = "=>"
|
|
65 |
then let val (ts,r) = args_result_type rest in (arg::ts,r) end
|
|
66 |
else ([],t)
|
|
67 |
| args_result_type t = ([],t);
|
|
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'
|
|
70 |
: (string * (* operator name of constr *)
|
|
71 |
string list * (* argument name list *)
|
|
72 |
(typ list * (* argument types *)
|
|
73 |
typ)) (* result type *)
|
|
74 |
list list end;
|
|
75 |
fun test_equal_type tn (cn,_,(_,rt)) = fst (type_name_vars rt) = tn orelse
|
|
76 |
error("Inappropriate result type for constructor "^cn);
|
|
77 |
val typs = map (fn (tn, cnstrs) =>
|
|
78 |
(map (test_equal_type tn) cnstrs; snd(third(hd(cnstrs)))))
|
|
79 |
(typs'~~cnstrss);
|
|
80 |
val test_typs = map (fn (typ,cnstrs) =>
|
|
81 |
if not (Type.typ_instance(tsig,typ,TVar(("'a",0),["pcpo"])))
|
|
82 |
then error("Not a pcpo type: "^fst(type_name_vars typ))
|
|
83 |
else map (fn (cn,_,(_,rt)) => rt=typ
|
|
84 |
orelse error("Non-identical result types for constructors "^
|
|
85 |
first(hd cnstrs)^" and "^ cn )) cnstrs) (typs~~cnstrss);
|
|
86 |
val proper_args = let
|
|
87 |
fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts
|
|
88 |
| occurs _ _ = false;
|
|
89 |
fun proper_arg cn atyp = forall (fn typ => let
|
|
90 |
val tn = fst(type_name_vars typ)
|
|
91 |
in atyp=typ orelse not (occurs tn atyp) orelse
|
|
92 |
error("Illegal use of type "^ tn ^
|
|
93 |
" as argument of constructor " ^cn)end )typs;
|
|
94 |
fun proper_curry (cn,_,(args,_)) = forall (proper_arg cn) args;
|
|
95 |
in map (map proper_curry) cnstrss end;
|
|
96 |
in (typs, flat cnstrss) end;
|
|
97 |
|
|
98 |
(* ----- calls for building new thy and thms -------------------------------------- *)
|
|
99 |
|
|
100 |
in
|
|
101 |
|
|
102 |
fun add_domain (comp_dname,eqs') thy'' = let
|
|
103 |
val ok_dummy = check_domain eqs';
|
|
104 |
val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dname,eqs');
|
|
105 |
val dts = map (Type o fst) eqs';
|
|
106 |
fun cons cons' = (map (fn (con,syn,args) =>
|
|
107 |
(ThyOps.const_name con syn,
|
|
108 |
map (fn ((lazy,sel,tp),vn) => ((lazy,
|
|
109 |
find (tp,dts) handle LIST "find" => ~1),
|
|
110 |
sel,vn))
|
|
111 |
(args~~(mk_var_names(map third args)))
|
|
112 |
)) cons') : cons 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);
|
|
115 |
in (thy,eqs) end;
|
|
116 |
|
|
117 |
fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let
|
|
118 |
val (typs,cnstrs) = check_gen_by thy' (typs',cnstrss');
|
|
119 |
in
|
|
120 |
Domain_Axioms.add_gen_by ((tname,finite),(typs,cnstrs)) thy' end;
|
|
121 |
|
|
122 |
end (* local *)
|
|
123 |
end (* struct *)
|