wenzelm@23152: (*  Title:      HOLCF/Tools/domain/domain_extender.ML
wenzelm@23152:     ID:         $Id$
wenzelm@23152:     Author:     David von Oheimb
wenzelm@23152: 
wenzelm@23152: Theory extender for domain command, including theory syntax.
wenzelm@23152: 
wenzelm@23152: ###TODO: 
wenzelm@23152: 
wenzelm@23152: this definition
wenzelm@23152: domain empty = silly empty
wenzelm@23152: yields
wenzelm@23152: Exception-
wenzelm@23152:    TERM
wenzelm@23152:       ("typ_of_term: bad encoding of type",
wenzelm@23152:          [Abs ("uu", "_", Const ("NONE", "_"))]) raised
wenzelm@23152: but this works fine:
wenzelm@23152: domain Empty = silly Empty
wenzelm@23152: 
wenzelm@23152: strange syntax errors are produced for:
wenzelm@23152: domain xx = xx ("x yy")
wenzelm@23152: domain 'a foo = foo (sel::"'a") 
wenzelm@23152: and bar = bar ("'a dummy")
wenzelm@23152: 
wenzelm@23152: *)
wenzelm@23152: 
wenzelm@23152: signature DOMAIN_EXTENDER =
wenzelm@23152: sig
wenzelm@23152:   val add_domain: string * ((bstring * string list) *
wenzelm@23152:     (string * mixfix * (bool * string option * string) list) list) list
wenzelm@23152:     -> theory -> theory
wenzelm@23152:   val add_domain_i: string * ((bstring * string list) *
wenzelm@23152:     (string * mixfix * (bool * string option * typ) list) list) list
wenzelm@23152:     -> theory -> theory
wenzelm@23152: end;
wenzelm@23152: 
wenzelm@23152: structure Domain_Extender: DOMAIN_EXTENDER =
wenzelm@23152: struct
wenzelm@23152: 
wenzelm@23152: open Domain_Library;
wenzelm@23152: 
wenzelm@23152: (* ----- general testing and preprocessing of constructor list -------------- *)
wenzelm@23152: fun check_and_sort_domain (dtnvs: (string * typ list) list, 
wenzelm@23152:      cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg =
wenzelm@23152:   let
wenzelm@23152:     val defaultS = Sign.defaultS sg;
wenzelm@23152:     val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of 
wenzelm@23152: 	[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
wenzelm@23152:     val test_dupl_cons = (case duplicates (op =) (map first (List.concat cons'')) of 
wenzelm@23152: 	[] => false | dups => error ("Duplicate constructors: " 
wenzelm@23152: 							 ^ commas_quote dups));
wenzelm@23152:     val test_dupl_sels = (case duplicates (op =) (List.mapPartial second
wenzelm@23152: 			       (List.concat (map third (List.concat cons'')))) of
wenzelm@23152:         [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
wenzelm@23152:     val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
wenzelm@23152: 	[] => false | dups => error("Duplicate type arguments: " 
wenzelm@23152: 		   ^commas_quote dups)) (map snd dtnvs);
wenzelm@23152:     (* test for free type variables, illegal sort constraints on rhs,
wenzelm@23152: 	       non-pcpo-types and invalid use of recursive type;
wenzelm@23152:        replace sorts in type variables on rhs *)
wenzelm@23152:     fun analyse_equation ((dname,typevars),cons') = 
wenzelm@23152:       let
wenzelm@23152: 	val tvars = map dest_TFree typevars;
wenzelm@23152: 	val distinct_typevars = map TFree tvars;
wenzelm@23152: 	fun rm_sorts (TFree(s,_)) = TFree(s,[])
wenzelm@23152: 	|   rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
wenzelm@23152: 	|   rm_sorts (TVar(s,_))  = TVar(s,[])
wenzelm@23152: 	and remove_sorts l = map rm_sorts l;
wenzelm@23152: 	val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
wenzelm@23152: 	fun analyse indirect (TFree(v,s))  = (case AList.lookup (op =) tvars v of 
wenzelm@23152: 		    NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
wenzelm@23152: 	          | SOME sort => if eq_set_string (s,defaultS) orelse
wenzelm@23152: 				    eq_set_string (s,sort    )
wenzelm@23152: 				 then TFree(v,sort)
wenzelm@23152: 				 else error ("Inconsistent sort constraint" ^
wenzelm@23152: 				             " for type variable " ^ quote v))
wenzelm@23152:         |   analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of
wenzelm@23152: 		NONE          => if s mem indirect_ok
wenzelm@23152: 				 then Type(s,map (analyse false) typl)
wenzelm@23152: 				 else Type(s,map (analyse true) typl)
wenzelm@23152: 	      | SOME typevars => if indirect 
wenzelm@23152:                            then error ("Indirect recursion of type " ^ 
wenzelm@23152: 				        quote (string_of_typ sg t))
wenzelm@23152:                            else if dname <> s orelse (** BUG OR FEATURE?: 
wenzelm@23152:                                 mutual recursion may use different arguments **)
wenzelm@23152: 				   remove_sorts typevars = remove_sorts typl 
wenzelm@23152: 				then Type(s,map (analyse true) typl)
wenzelm@23152: 				else error ("Direct recursion of type " ^ 
wenzelm@23152: 					     quote (string_of_typ sg t) ^ 
wenzelm@23152: 					    " with different arguments"))
wenzelm@23152:         |   analyse indirect (TVar _) = Imposs "extender:analyse";
wenzelm@23152: 	fun check_pcpo T = if pcpo_type sg T then T
wenzelm@23152:           else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T);
wenzelm@23152: 	val analyse_con = upd_third (map (upd_third (check_pcpo o analyse false)));
wenzelm@23152:       in ((dname,distinct_typevars), map analyse_con cons') end; 
wenzelm@23152:   in ListPair.map analyse_equation (dtnvs,cons'')
wenzelm@23152:   end; (* let *)
wenzelm@23152: 
wenzelm@23152: (* ----- calls for building new thy and thms -------------------------------- *)
wenzelm@23152: 
wenzelm@23152: fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
wenzelm@23152:   let
wenzelm@23152:     val dtnvs = map ((fn (dname,vs) => 
wenzelm@24707: 			 (Sign.full_name thy''' dname, map (Syntax.read_typ_global thy''') vs))
wenzelm@23152:                    o fst) eqs''';
wenzelm@23152:     val cons''' = map snd eqs''';
wenzelm@23152:     fun thy_type  (dname,tvars)  = (Sign.base_name dname, length tvars, NoSyn);
wenzelm@23152:     fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
wenzelm@23152:     val thy'' = thy''' |> Theory.add_types     (map thy_type  dtnvs)
wenzelm@23152: 		       |> fold (AxClass.axiomatize_arity_i o thy_arity) dtnvs;
wenzelm@23152:     val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
wenzelm@23152:     val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
wenzelm@23152:     val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
wenzelm@23152:     val dts  = map (Type o fst) eqs';
wenzelm@23152:     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
wenzelm@23152:     fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
wenzelm@23152:     fun typid (Type  (id,_)) =
wenzelm@23152:           let val c = hd (Symbol.explode (Sign.base_name id))
wenzelm@23152:           in if Symbol.is_letter c then c else "t" end
wenzelm@23152:       | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
wenzelm@23152:       | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
wenzelm@23152:     fun one_con (con,mx,args) =
wenzelm@23152: 	((Syntax.const_name con mx),
wenzelm@23152: 	 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
wenzelm@23152: 					find_index_eq tp dts,
wenzelm@23152: 					DatatypeAux.dtyp_of_typ new_dts tp),
wenzelm@23152: 					sel,vn))
wenzelm@23152: 	     (args,(mk_var_names(map (typid o third) args)))
wenzelm@23152: 	 ) : cons;
wenzelm@23152:     val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
wenzelm@23152:     val thy        = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
wenzelm@23152:     val (theorems_thy, (rewss, take_rews)) = (foldl_map (fn (thy0,eq) =>
wenzelm@23152:       Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs))
wenzelm@23152:       |>>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
wenzelm@23152:   in
wenzelm@23152:     theorems_thy
wenzelm@23152:     |> Theory.add_path (Sign.base_name comp_dnam)
wenzelm@23152:     |> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
wenzelm@23152:     |> Theory.parent_path
wenzelm@23152:   end;
wenzelm@23152: 
wenzelm@23152: val add_domain_i = gen_add_domain Sign.certify_typ;
wenzelm@24707: val add_domain = gen_add_domain Syntax.read_typ_global;
wenzelm@23152: 
wenzelm@23152: 
wenzelm@23152: (** outer syntax **)
wenzelm@23152: 
wenzelm@23152: local structure P = OuterParse and K = OuterKeyword in
wenzelm@23152: 
wenzelm@23152: val dest_decl =
wenzelm@23152:   P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
wenzelm@23152:     (P.name >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
wenzelm@23152:   || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
wenzelm@23152:        >> (fn t => (true,NONE,t))
wenzelm@23152:   || P.typ >> (fn t => (false,NONE,t));
wenzelm@23152: 
wenzelm@23152: val cons_decl =
wenzelm@23152:   P.name -- Scan.repeat dest_decl -- P.opt_mixfix
wenzelm@23152:   >> (fn ((c, ds), mx) => (c, mx, ds));
wenzelm@23152: 
wenzelm@23152: val type_var' = (P.type_ident ^^ 
wenzelm@23152:                  Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
wenzelm@23152: val type_args' = type_var' >> single ||
wenzelm@23152:                  P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
wenzelm@23152:  		 Scan.succeed [];
wenzelm@23152: 
wenzelm@23152: val domain_decl = (type_args' -- P.name >> Library.swap) -- 
wenzelm@23152:                   (P.$$$ "=" |-- P.enum1 "|" cons_decl);
wenzelm@23152: val domains_decl =
wenzelm@23152:   Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl
wenzelm@23152:   >> (fn (opt_name, doms) =>
wenzelm@23152:       (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms));
wenzelm@23152: 
wenzelm@23152: val domainP =
wenzelm@23152:   OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
wenzelm@23152:     (domains_decl >> (Toplevel.theory o add_domain));
wenzelm@23152: 
wenzelm@23152: 
wenzelm@23152: val _ = OuterSyntax.add_keywords ["lazy"];
wenzelm@23152: val _ = OuterSyntax.add_parsers [domainP];
wenzelm@23152: 
wenzelm@23152: end; (* local structure *)
wenzelm@23152: 
wenzelm@23152: end;