--- a/src/HOLCF/domain/extender.ML Fri Jul 11 13:54:26 2003 +0200
+++ b/src/HOLCF/domain/extender.ML Fri Jul 11 13:54:32 2003 +0200
@@ -1,6 +1,6 @@
(* Title: HOLCF/domain/extender.ML
ID: $Id$
- Author: David von Oheimb and Markus Wenzel
+ Author: David von Oheimb
License: GPL (GNU GENERAL PUBLIC LICENSE)
Theory extender for domain section, including new-style theory syntax.
@@ -49,23 +49,23 @@
| rm_sorts (TVar(s,_)) = TVar(s,[])
and remove_sorts l = map rm_sorts l;
fun analyse(TFree(v,s)) = (case assoc_string(tvars,v) of
- None => error ("Free type variable " ^ v ^ " on rhs.")
+ None => error ("Free type variable " ^ quote v ^ " on rhs.")
| Some sort => if eq_set_string (s,defaultS) orelse
eq_set_string (s,sort )
then TFree(distinct_name v,sort)
- else error ("Additional constraint on rhs "^
- "for type variable "^quote v))
+ else error ("Inconsistent sort constraint" ^
+ " for type variable " ^ quote v))
(** BUG OR FEATURE?: mutual recursion may use different arguments **)
| analyse(Type(s,typl)) = (case assoc_string((*dtnvs*)
[(dname,typevars)],s) of
None => Type(s,map analyse typl)
| Some typevars => if remove_sorts typevars = remove_sorts typl
then Type(s,map analyse typl)
- else error ("Recursion of type " ^ s ^
+ else error ("Recursion of type " ^ quote s ^
" with different arguments"))
| analyse(TVar _) = Imposs "extender:analyse";
fun check_pcpo t = (pcpo_type sg t orelse error(
- "Type not of sort pcpo: "^string_of_typ sg t); t);
+ "Constructor argument type is not of sort pcpo: "^string_of_typ sg t); t);
val analyse_con = upd_third (map (upd_third (check_pcpo o analyse)));
in ((dname,distinct_typevars), map analyse_con cons') end;
in ListPair.map analyse_equation (dtnvs,cons'')
@@ -127,7 +127,14 @@
P.name -- Scan.repeat dest_decl -- P.opt_mixfix
>> (fn ((c, ds), mx) => (c, mx, ds));
-val domain_decl = (P.type_args -- P.name >> Library.swap) -- (P.$$$ "=" |-- P.enum1 "|" cons_decl);
+val type_var' = (P.type_ident ^^
+ Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
+val type_args' = type_var' >> single ||
+ P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
+ Scan.succeed [];
+
+val domain_decl = (type_args' -- P.name >> Library.swap) --
+ (P.$$$ "=" |-- P.enum1 "|" cons_decl);
val domains_decl =
Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl
>> (fn (opt_name, doms) =>
--- a/src/HOLCF/domain/interface.ML Fri Jul 11 13:54:26 2003 +0200
+++ b/src/HOLCF/domain/interface.ML Fri Jul 11 13:54:32 2003 +0200
@@ -5,6 +5,7 @@
Parser for domain section.
*)
+(** BEWARE: this is still needed for old-style theories **)
local
open ThyParse;
@@ -101,21 +102,21 @@
"") end;
(* ----- parser for domain declaration equation ----------------------------- *)
+(** BEWARE: should be consistent with domains_decl in extender.ML **)
val name' = name >> unenclose;
- val type_var' = type_var >> unenclose;
fun esc_quote s = let fun esc [] = []
| esc ("\""::xs) = esc xs
| esc ("[" ::xs) = "{"::esc xs
| esc ("]" ::xs) = "}"::esc xs
| esc (x ::xs) = x ::esc xs
in implode (esc (Symbol.explode s)) end;
- val tvar = (type_var' ^^
- optional ($$ "::" ^^ (sort >> esc_quote)) "") >> quote;
- fun type_args l = (tvar >> (fn x => [x])
- || "(" $$-- !! (list1 tvar --$$ ")")
- || empty >> K []) l
- fun con_typ l = (type_args -- name' >> (fn (x,y) => (y,x))) l
+ val type_var' = ((type_var >> unenclose) ^^
+ optional ($$ "::" ^^ !! (sort >> esc_quote)) "") >> quote;
+ val type_args = (type_var' >> single
+ || "(" $$-- !! (list1 type_var' --$$ ")")
+ || empty >> K [])
+ val con_typ = (type_args -- name' >> Library.swap)
(* here ident may be used instead of name'
to avoid ambiguity with standard mixfix option *)
val domain_arg = "(" $$-- (optional ($$ "lazy" >> K true) false)