src/HOLCF/Tools/domain/domain_extender.ML
author wenzelm
Sun Mar 08 17:26:14 2009 +0100 (2009-03-08)
changeset 30364 577edc39b501
parent 30345 76fd85bbf139
child 30915 f8877f60e1ee
permissions -rw-r--r--
moved basic algebra of long names from structure NameSpace to Long_Name;
     1 (*  Title:      HOLCF/Tools/domain/domain_extender.ML
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4 
     5 Theory extender for domain command, including theory syntax.
     6 
     7 ###TODO: 
     8 
     9 this definition
    10 domain empty = silly empty
    11 yields
    12 Exception-
    13    TERM
    14       ("typ_of_term: bad encoding of type",
    15          [Abs ("uu", "_", Const ("NONE", "_"))]) raised
    16 but this works fine:
    17 domain Empty = silly Empty
    18 
    19 strange syntax errors are produced for:
    20 domain xx = xx ("x yy")
    21 domain 'a foo = foo (sel::"'a") 
    22 and bar = bar ("'a dummy")
    23 
    24 *)
    25 
    26 signature DOMAIN_EXTENDER =
    27 sig
    28   val add_domain: string * ((bstring * string list) *
    29     (string * mixfix * (bool * string option * string) list) list) list
    30     -> theory -> theory
    31   val add_domain_i: string * ((bstring * string list) *
    32     (string * mixfix * (bool * string option * typ) list) list) list
    33     -> theory -> theory
    34 end;
    35 
    36 structure Domain_Extender: DOMAIN_EXTENDER =
    37 struct
    38 
    39 open Domain_Library;
    40 
    41 (* ----- general testing and preprocessing of constructor list -------------- *)
    42 fun check_and_sort_domain (dtnvs: (string * typ list) list, 
    43      cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg =
    44   let
    45     val defaultS = Sign.defaultS sg;
    46     val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of 
    47 	[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
    48     val test_dupl_cons = (case duplicates (op =) (map first (List.concat cons'')) of 
    49 	[] => false | dups => error ("Duplicate constructors: " 
    50 							 ^ commas_quote dups));
    51     val test_dupl_sels = (case duplicates (op =) (List.mapPartial second
    52 			       (List.concat (map third (List.concat cons'')))) of
    53         [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
    54     val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
    55 	[] => false | dups => error("Duplicate type arguments: " 
    56 		   ^commas_quote dups)) (map snd dtnvs);
    57     (* test for free type variables, illegal sort constraints on rhs,
    58 	       non-pcpo-types and invalid use of recursive type;
    59        replace sorts in type variables on rhs *)
    60     fun analyse_equation ((dname,typevars),cons') = 
    61       let
    62 	val tvars = map dest_TFree typevars;
    63 	val distinct_typevars = map TFree tvars;
    64 	fun rm_sorts (TFree(s,_)) = TFree(s,[])
    65 	|   rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
    66 	|   rm_sorts (TVar(s,_))  = TVar(s,[])
    67 	and remove_sorts l = map rm_sorts l;
    68 	val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
    69 	fun analyse indirect (TFree(v,s))  = (case AList.lookup (op =) tvars v of 
    70 		    NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
    71 	          | SOME sort => if eq_set_string (s,defaultS) orelse
    72 				    eq_set_string (s,sort    )
    73 				 then TFree(v,sort)
    74 				 else error ("Inconsistent sort constraint" ^
    75 				             " for type variable " ^ quote v))
    76         |   analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of
    77 		NONE          => if s mem indirect_ok
    78 				 then Type(s,map (analyse false) typl)
    79 				 else Type(s,map (analyse true) typl)
    80 	      | SOME typevars => if indirect 
    81                            then error ("Indirect recursion of type " ^ 
    82 				        quote (string_of_typ sg t))
    83                            else if dname <> s orelse (** BUG OR FEATURE?: 
    84                                 mutual recursion may use different arguments **)
    85 				   remove_sorts typevars = remove_sorts typl 
    86 				then Type(s,map (analyse true) typl)
    87 				else error ("Direct recursion of type " ^ 
    88 					     quote (string_of_typ sg t) ^ 
    89 					    " with different arguments"))
    90         |   analyse indirect (TVar _) = Imposs "extender:analyse";
    91 	fun check_pcpo T = if pcpo_type sg T then T
    92           else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T);
    93 	val analyse_con = upd_third (map (upd_third (check_pcpo o analyse false)));
    94       in ((dname,distinct_typevars), map analyse_con cons') end; 
    95   in ListPair.map analyse_equation (dtnvs,cons'')
    96   end; (* let *)
    97 
    98 (* ----- calls for building new thy and thms -------------------------------- *)
    99 
   100 fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
   101   let
   102     val dtnvs = map ((fn (dname,vs) => 
   103 			 (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
   104                    o fst) eqs''';
   105     val cons''' = map snd eqs''';
   106     fun thy_type  (dname,tvars)  = (Binding.name (Long_Name.base_name dname), length tvars, NoSyn);
   107     fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
   108     val thy'' = thy''' |> Sign.add_types     (map thy_type  dtnvs)
   109 		       |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
   110     val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
   111     val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
   112     val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
   113     val dts  = map (Type o fst) eqs';
   114     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
   115     fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
   116     fun typid (Type  (id,_)) =
   117           let val c = hd (Symbol.explode (Long_Name.base_name id))
   118           in if Symbol.is_letter c then c else "t" end
   119       | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
   120       | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
   121     fun one_con (con,mx,args) =
   122 	((Syntax.const_name mx con),
   123 	 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
   124 					find_index_eq tp dts,
   125 					DatatypeAux.dtyp_of_typ new_dts tp),
   126 					sel,vn))
   127 	     (args,(mk_var_names(map (typid o third) args)))
   128 	 ) : cons;
   129     val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
   130     val thy        = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
   131     val ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn eq =>
   132       Domain_Theorems.theorems (eq, eqs)) eqs
   133       ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
   134   in
   135     theorems_thy
   136     |> Sign.add_path (Long_Name.base_name comp_dnam)
   137     |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])]))
   138     |> Sign.parent_path
   139   end;
   140 
   141 val add_domain_i = gen_add_domain Sign.certify_typ;
   142 val add_domain = gen_add_domain Syntax.read_typ_global;
   143 
   144 
   145 (** outer syntax **)
   146 
   147 local structure P = OuterParse and K = OuterKeyword in
   148 
   149 val _ = OuterKeyword.keyword "lazy";
   150 
   151 val dest_decl =
   152   P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
   153     (P.name >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
   154   || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
   155        >> (fn t => (true,NONE,t))
   156   || P.typ >> (fn t => (false,NONE,t));
   157 
   158 val cons_decl =
   159   P.name -- Scan.repeat dest_decl -- P.opt_mixfix
   160   >> (fn ((c, ds), mx) => (c, mx, ds));
   161 
   162 val type_var' = (P.type_ident ^^ 
   163                  Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
   164 val type_args' = type_var' >> single ||
   165                  P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
   166  		 Scan.succeed [];
   167 
   168 val domain_decl = (type_args' -- P.name >> Library.swap) -- 
   169                   (P.$$$ "=" |-- P.enum1 "|" cons_decl);
   170 val domains_decl =
   171   Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl
   172   >> (fn (opt_name, doms) =>
   173       (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms));
   174 
   175 val _ =
   176   OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
   177     (domains_decl >> (Toplevel.theory o add_domain));
   178 
   179 end;
   180 
   181 end;