--- a/Datatype.ML Wed Jun 29 12:04:04 1994 +0200
+++ b/Datatype.ML Fri Jul 08 12:01:55 1994 +0200
@@ -32,14 +32,15 @@
val typ_list = "(" $$-- list1 typ --$$ ")" || empty;
- val cons = name -- typ_list;
+ val cons = name -- typ_list -- opt_mixfix;
fun constructs ts =
( cons --$$ "|" -- constructs >> op::
||
cons >> (fn c => [c])) ts;
- val mk_cons = map (fn (s, ts) => pars (s ^ ", " ^ mk_list ts));
+ val mk_cons = map (fn ((s, ts), syn) =>
+ pars (commas [s, mk_list ts, syn]));
(*remove all quotes from a string*)
fun rem_quotes s = implode (filter (fn c => c <> "\"") (explode s));
@@ -48,9 +49,10 @@
fun rules_ineq cs tname =
let (*combine all constructor names with all others w/o duplicates*)
fun negOne _ [] = []
- | negOne (c : string * 'b) ((c2 : string * 'b) :: cs) =
- quote ("ineq_" ^ rem_quotes (#1 c) ^ "_" ^
- rem_quotes (#1 c2)) :: negOne c cs;
+ | negOne (c : (string * 'a) * 'b) ((c2 : (string * 'a) * 'b)
+ :: cs) =
+ quote ("ineq_" ^ rem_quotes (#1 (#1 c)) ^ "_" ^
+ rem_quotes (#1 (#1 c2))) :: negOne c cs;
fun neg1 [] = []
| neg1 (c1 :: cs) = (negOne c1 cs) @ (neg1 cs)
@@ -59,16 +61,16 @@
(0 upto (length cs))
end;
- fun arg1 (id, ts) = not (null ts);
+ fun arg1 ((_, ts), _) = not (null ts);
- (*generate string calling 'add_datatype'*)
+ (*generate string for calling 'add_datatype'*)
fun mk_params ((ts, tname), cons) =
("|> add_datatype\n" ^
pars (commas [mk_list ts, quote tname, mk_list (mk_cons cons)]),
"structure " ^ tname ^ " =\n\
\struct\n\
\ val inject = map (get_axiom thy) " ^
- mk_list (map (fn (s,_) => quote ("inject_" ^ rem_quotes s))
+ mk_list (map (fn ((s,_), _) => quote ("inject_" ^ rem_quotes s))
(filter arg1 cons)) ^ ";\n\
\ val ineq = " ^ (if length cons < dtK then "let val ineq' = " else "")
^ "map (get_axiom thy) " ^ mk_list (rules_ineq cons tname) ^
@@ -77,8 +79,8 @@
else "") ^ ";\n\
\ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
\ val cases = map (get_axiom thy) " ^
- mk_list (map (fn (s,_) => quote (tname ^ "_case_" ^ rem_quotes s))
- cons) ^ ";\n\
+ mk_list (map (fn ((s,_),_) =>
+ quote(tname ^ "_case_" ^ rem_quotes s)) cons) ^ ";\n\
\ val simps = inject @ ineq @ cases;\n\
\ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
\end;\n");
@@ -103,44 +105,43 @@
val mk_list = brackets o commas;
(*check if constructor names are unique*)
- fun check_cons cs =
- (case findrep (map fst cs) of
+ fun check_cons (cs : (string * 'b * 'c) list) =
+ (case findrep (map #1 cs) of
[] => true
| c::_ => error("Constructor \"" ^ c ^ "\" occurs twice"));
(*search for free type variables and convert recursive *)
- fun analyse ((cons, typlist) :: cs) =
- let fun analyseOne ((dtVar v) :: typlist) =
+ fun analyse_types (cons, typlist, syn) =
+ let fun analyse ((dtVar v) :: typlist) =
if ((dtVar v) mem typevars) then
- (dtVar v) :: analyseOne typlist
+ (dtVar v) :: analyse typlist
else error ("Variable " ^ v ^ " is free.")
- | analyseOne ((dtId s) :: typlist) =
- if tname<>s then (dtId s) :: analyseOne typlist
+ | analyse ((dtId s) :: typlist) =
+ if tname<>s then (dtId s) :: analyse typlist
else if null typevars then
- Rek ([], tname) :: analyseOne typlist
+ Rek ([], tname) :: analyse typlist
else error (s ^ " used in different ways")
- | analyseOne (Comp (typl,s) :: typlist) =
- if tname <> s then Comp (analyseOne typl, s)
- :: analyseOne typlist
+ | analyse (Comp (typl,s) :: typlist) =
+ if tname <> s then Comp (analyse typl, s)
+ :: analyse typlist
else if typevars = typl then
- Rek (typl, s) :: analyseOne typlist
+ Rek (typl, s) :: analyse typlist
else
error (s ^ " used in different ways")
- | analyseOne [] = []
- | analyseOne ((Rek _) :: _) = raise Impossible;
- in (cons, analyseOne typlist) :: analyse cs end
- | analyse [] = [];
+ | analyse [] = []
+ | analyse ((Rek _) :: _) = raise Impossible;
+ in (cons, analyse typlist, syn) end;
(*test if there are elements that are not recursive, i.e. if the type is
not empty*)
- fun one_not_rek cs =
+ fun one_not_rek (cs : ('a * dt_type list * 'c) list) =
let val contains_no_rek = forall (fn Rek _ => false | _ => true);
- in exists (contains_no_rek o snd) cs orelse
+ in exists (contains_no_rek o #2) cs orelse
error("Empty type not allowed!") end;
- val _ = check_cons cons_list';
- val cons_list = analyse cons_list';
- val _ = one_not_rek cons_list;
+ val dummy = check_cons cons_list';
+ val cons_list = map analyse_types cons_list';
+ val dummy = one_not_rek cons_list;
(*Pretty printers for type lists;
pp_typlist1: parentheses, pp_typlist2: brackets*)
@@ -160,8 +161,9 @@
Args(var, delim, n+1, m);
(* Generate syntax translation for case rules *)
- fun calc_xrules c_nr y_nr ((c, typlist) :: cs) =
- let val arity = length typlist;
+ fun calc_xrules c_nr y_nr ((id, typlist, syn) :: cs) =
+ let val name = const_name id syn;
+ val arity = length typlist;
val body = "z" ^ string_of_int(c_nr);
val args1 = if arity=0 then ""
else pars (Args ("y", ",", y_nr, y_nr+arity-1));
@@ -169,10 +171,10 @@
else "% " ^ Args ("y", " ", y_nr, y_nr+arity-1)
^ ". ";
val (rest1,rest2) =
- if null cs then ("", "")
+ if null cs then ("","")
else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs
in (" | " ^ h1, ", " ^ h2) end;
- in (c ^ args1 ^ " => " ^ body ^ rest1, args2 ^ body ^ rest2) end
+ in (name ^ args1 ^ " => " ^ body ^ rest1, args2 ^ body ^ rest2) end
| calc_xrules _ _ [] = raise Impossible;
val xrules =
@@ -182,10 +184,10 @@
end;
(*type declarations for constructors*)
- fun const_types ((c, typlist) :: cs) =
- (c,
+ fun const_types ((id, typlist, syn) :: cs) =
+ (id,
(if null typlist then "" else pp_typlist2 typlist ^ " => ") ^
- pp_typlist1 typevars ^ tname, NoSyn)
+ pp_typlist1 typevars ^ tname, syn)
:: const_types cs
| const_types [] = [];
@@ -246,8 +248,9 @@
fun empty_list n = replicate n "";
- fun t_inducting ((name, typl) :: cs) =
- let val tab = insert_types typl [];
+ fun t_inducting ((id, typl, syn) :: cs) =
+ let val name = const_name id syn;
+ val tab = insert_types typl [];
val arity = length typl;
val var_list = convert tab (empty_list arity) typl;
val h = if arity = 0 then " P(" ^ name ^ ")"
@@ -255,24 +258,25 @@
(assumpt (typl, var_list, false)) ^ "P(" ^
name ^ "(" ^ (commas var_list) ^ "))";
val rest = t_inducting cs;
- in if rest="" then h else h ^ "; " ^ rest end
+ in if rest = "" then h else h ^ "; " ^ rest end
| t_inducting [] = "";
fun t_induct cl typ_name=
"[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")";
- fun case_typlist typevar ((c, typlist) :: cs) =
+ fun case_typlist typevar ((_, typlist, _) :: cs) =
let val h = if (length typlist) > 0 then
(pp_typlist2 typlist) ^ "=>"
else ""
in "," ^ h ^ typevar ^ (case_typlist typevar cs) end
| case_typlist _ [] = "";
- fun case_rules t_case arity n ((id, typlist) :: cs) =
- let val args = if null typlist then ""
+ fun case_rules t_case arity n ((id, typlist, syn) :: cs) =
+ let val name = const_name id syn;
+ val args = if null typlist then ""
else "(" ^ Args ("x", ",", 1, length typlist) ^ ")"
in (t_case ^ "_" ^ id,
- t_case ^ "(" ^ id ^ args ^ "," ^ Args ("f", ",", 1, arity)
+ t_case ^ "(" ^ name ^ args ^ "," ^ Args ("f", ",", 1, arity)
^ ") = f" ^ string_of_int(n) ^ args)
:: (case_rules t_case arity (n+1) cs)
end
@@ -280,23 +284,11 @@
val datatype_arity = length typevars;
- val sign = sign_of thy;
- val {tsig, ...} = Sign.rep_sg sign;
-
- val types =
- let val {args, ...} = Type.rep_tsig tsig;
- in case assoc (args, tname) of
- None => [(tname, datatype_arity, NoSyn)]
- | Some _ => []
- end;
+ val types = [(tname, datatype_arity, NoSyn)];
val arities =
- let val {coreg, ...} = Type.rep_tsig tsig;
- val term_list = replicate datatype_arity ["term"];
- in case assoc (coreg, tname) of
- None => [(tname, term_list, ["term"])]
- | Some _ => []
- end;
+ let val term_list = replicate datatype_arity ["term"];
+ in [(tname, term_list, ["term"])] end;
val datatype_name = pp_typlist1 typevars ^ tname;
@@ -311,15 +303,10 @@
in (dekl, rules) end;
val consts =
- let val {const_tab, ...} = Sign.rep_sg sign;
- fun const_undef (c, _, _) = case Symtab.lookup (const_tab, c) of
- Some _ => false
- | None => true;
- in (filter const_undef (const_types cons_list)) @
- (if length cons_list < dtK then []
+ const_types cons_list
+ @ (if length cons_list < dtK then []
else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)])
- @ case_const
- end;
+ @ case_const;
(*generate 'var_n, ..., var_m'*)
fun Args(var, delim, n, m) =
@@ -336,26 +323,28 @@
else "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) ^ " & " ^
Arg_eql(n+1, m);
- fun Ci_ing (c :: cs) =
- let val (name, typlist) = c
- val arity = length typlist
- in if arity>0
- then ("inject_" ^ name,
+ fun Ci_ing ((id, typlist, syn) :: cs) =
+ let val name = const_name id syn;
+ val arity = length typlist;
+ in if arity > 0
+ then ("inject_" ^ id,
"(" ^ C_exp(name,arity,"x") ^ "=" ^ C_exp(name,arity,"y")
- ^ ") = (" ^ Arg_eql(1,arity) ^ ")") :: (Ci_ing cs)
+ ^ ") = (" ^ Arg_eql (1, arity) ^ ")") :: (Ci_ing cs)
else (Ci_ing cs)
end
| Ci_ing [] = [];
fun Ci_negOne _ [] = []
| Ci_negOne c (c1::cs) =
- let val (name1, tl1) = c
- val (name2, tl2) = c1
+ let val (id1, tl1, syn1) = c
+ val (id2, tl2, syn2) = c1
+ val name1 = const_name id1 syn1;
+ val name2 = const_name id2 syn2;
val arit1 = length tl1
val arit2 = length tl2
val h = "(" ^ C_exp(name1, arit1, "x") ^ "~=" ^
C_exp(name2, arit2, "y") ^ ")"
- in ("ineq_" ^ name1 ^ "_" ^ name2, h):: (Ci_negOne c cs)
+ in ("ineq_" ^ id1 ^ "_" ^ id2, h):: (Ci_negOne c cs)
end;
fun Ci_neg1 [] = []
@@ -364,10 +353,11 @@
fun suc_expr n =
if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")";
- fun Ci_neg2equals (ord_t, ((c, typlist) :: cs), n) =
- let val h = ord_t ^ "(" ^ (C_exp(c, length typlist, "x")) ^ ") = " ^
- (suc_expr n)
- in (ord_t ^ (string_of_int(n+1)), h)
+ fun Ci_neg2equals (ord_t, ((id, typlist, syn) :: cs), n) =
+ let val name = const_name id syn;
+ val h = ord_t ^ "(" ^ (C_exp(name, length typlist, "x"))
+ ^ ") = " ^ (suc_expr n)
+ in (ord_t ^ (string_of_int (n+1)), h)
:: (Ci_neg2equals (ord_t, cs , n+1))
end
| Ci_neg2equals (_, [], _) = [];