isabelle: comparison src/HOLCF/Tools/domain/domain

equal deleted inserted replaced

-:6c593b431f04
+:67dff9c5b2bd
 *)
 signature DOMAIN_EXTENDER =
 sig
 val add_domain_cmd: string ->
 ((string * string option) list * binding * mixfix *
 (binding * (bool * binding option * string) list * mixfix) list) list
 -> theory -> theory
 val add_domain: string ->
 ((string * string option) list * binding * mixfix *
 (binding * (bool * binding option * typ) list * mixfix) list) list
 -> theory -> theory
 end;
 structure Domain_Extender :> DOMAIN_EXTENDER =
 struct
 open Domain_Library;
 (* ----- general testing and preprocessing of constructor list -------------- *)
 fun check_and_sort_domain
 (dtnvs : (string * typ list) list)
 (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
 (sg : theory)
 : ((string * typ list) *
 (binding * (bool * binding option * typ) list * mixfix) list) list =
 let
 val defaultS = Sign.defaultS sg;
 val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of
-	[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
+[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
-val test_dupl_cons = (case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of
+val test_dupl_cons =
-	[] => false | dups => error ("Duplicate constructors: "
+(case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of
-							 ^ commas_quote dups));
+[] => false | dups => error ("Duplicate constructors: "
-val test_dupl_sels = (case duplicates (op =) (map Binding.name_of (List.mapPartial second
+^ commas_quote dups));
-			       (List.concat (map second (List.concat cons''))))) of
+val test_dupl_sels =
-[] => false | dups => error("Duplicate selectors: "^commas_quote dups));
+(case duplicates (op =) (map Binding.name_of (List.mapPartial second
-val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
+(List.concat (map second (List.concat cons''))))) of
-	[] => false | dups => error("Duplicate type arguments: "
+[] => false | dups => error("Duplicate selectors: "^commas_quote dups));
-		   ^commas_quote dups)) (map snd dtnvs);
+val test_dupl_tvars =
-(* test for free type variables, illegal sort constraints on rhs,
+exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
-	       non-pcpo-types and invalid use of recursive type;
+[] => false | dups => error("Duplicate type arguments: "
-replace sorts in type variables on rhs *)
+^commas_quote dups)) (map snd dtnvs);
-fun analyse_equation ((dname,typevars),cons') =
+(* test for free type variables, illegal sort constraints on rhs,
-let
+non-pcpo-types and invalid use of recursive type;
-	val tvars = map dest_TFree typevars;
+replace sorts in type variables on rhs *)
-	val distinct_typevars = map TFree tvars;
+fun analyse_equation ((dname,typevars),cons') =
-	fun rm_sorts (TFree(s,_)) = TFree(s,[])
+let
-	|   rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
+val tvars = map dest_TFree typevars;
-	|   rm_sorts (TVar(s,_))  = TVar(s,[])
+val distinct_typevars = map TFree tvars;
-	and remove_sorts l = map rm_sorts l;
+fun rm_sorts (TFree(s,_)) = TFree(s,[])
-	val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
+| rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
-	fun analyse indirect (TFree(v,s))  = (case AList.lookup (op =) tvars v of
+| rm_sorts (TVar(s,_))  = TVar(s,[])
-		    NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
+and remove_sorts l = map rm_sorts l;
-	          | SOME sort => if eq_set_string (s,defaultS) orelse
+val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
-				    eq_set_string (s,sort    )
+fun analyse indirect (TFree(v,s))  =
-				 then TFree(v,sort)
+(case AList.lookup (op =) tvars v of
-				 else error ("Inconsistent sort constraint" ^
+NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
-				             " for type variable " ^ quote v))
+| SOME sort => if eq_set_string (s,defaultS) orelse
-|   analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of
+eq_set_string (s,sort    )
-		NONE          => if s mem indirect_ok
+then TFree(v,sort)
-				 then Type(s,map (analyse false) typl)
+else error ("Inconsistent sort constraint" ^
-				 else Type(s,map (analyse true) typl)
+" for type variable " ^ quote v))
-	      | SOME typevars => if indirect
+| analyse indirect (t as Type(s,typl)) =
-then error ("Indirect recursion of type " ^
+(case AList.lookup (op =) dtnvs s of
-				        quote (string_of_typ sg t))
+NONE          => if s mem indirect_ok
-else if dname <> s orelse (** BUG OR FEATURE?:
+then Type(s,map (analyse false) typl)
-mutual recursion may use different arguments **)
+else Type(s,map (analyse true) typl)
-				   remove_sorts typevars = remove_sorts typl
+| SOME typevars => if indirect
-				then Type(s,map (analyse true) typl)
+then error ("Indirect recursion of type " ^
-				else error ("Direct recursion of type " ^
+quote (string_of_typ sg t))
-					     quote (string_of_typ sg t) ^
+else if dname <> s orelse
-					    " with different arguments"))
+(** BUG OR FEATURE?:
-|   analyse indirect (TVar _) = Imposs "extender:analyse";
+mutual recursion may use different arguments **)
-fun check_pcpo lazy T =
+remove_sorts typevars = remove_sorts typl
-let val ok = if lazy then cpo_type else pcpo_type
+then Type(s,map (analyse true) typl)
-in if ok sg T then T else error
+else error ("Direct recursion of type " ^
-("Constructor argument type is not of sort pcpo: " ^
+quote (string_of_typ sg t) ^
-string_of_typ sg T)
+" with different arguments"))
-end;
+| analyse indirect (TVar _) = Imposs "extender:analyse";
-fun analyse_arg (lazy, sel, T) =
+fun check_pcpo lazy T =
-(lazy, sel, check_pcpo lazy (analyse false T));
+let val ok = if lazy then cpo_type else pcpo_type
-fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
+in if ok sg T then T else error
-in ((dname,distinct_typevars), map analyse_con cons') end;
+("Constructor argument type is not of sort pcpo: " ^
-in ListPair.map analyse_equation (dtnvs,cons'')
+string_of_typ sg T)
-end; (* let *)
+end;
+fun analyse_arg (lazy, sel, T) =
+(lazy, sel, check_pcpo lazy (analyse false T));
+fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
+in ((dname,distinct_typevars), map analyse_con cons') end;
+in ListPair.map analyse_equation (dtnvs,cons'')
+end; (* let *)
 (* ----- calls for building new thy and thms -------------------------------- *)
 fun gen_add_domain
 (prep_typ : theory -> 'a -> typ)
 (comp_dnam : string)
 (eqs''' : ((string * string option) list * binding * mixfix *
 (binding * (bool * binding option * 'a) list * mixfix) list) list)
 (thy''' : theory) =
 let
 fun readS (SOME s) = Syntax.read_sort_global thy''' s
 | readS NONE = Sign.defaultS thy''';
 fun readTFree (a, s) = TFree (a, readS s);
 val dtnvs = map (fn (vs,dname:binding,mx,_) =>
 (dname, map readTFree vs, mx)) eqs''';
 val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
 fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
 fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
 val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
-		       |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
+|> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
 val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
 val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
-val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list = check_and_sort_domain dtnvs' cons'' thy'';
+val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list =
-val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
+check_and_sort_domain dtnvs' cons'' thy'';
-val dts  = map (Type o fst) eqs';
+val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
-val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+val dts  = map (Type o fst) eqs';
-fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
+val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
-fun typid (Type  (id,_)) =
+fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
+fun typid (Type  (id,_)) =
 let val c = hd (Symbol.explode (Long_Name.base_name id))
 in if Symbol.is_letter c then c else "t" end
 | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
 | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
 fun one_con (con,args,mx) =
-	((Syntax.const_name mx (Binding.name_of con)),
+((Syntax.const_name mx (Binding.name_of con)),
-	 ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy,
+ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy,
-					DatatypeAux.dtyp_of_typ new_dts tp),
+DatatypeAux.dtyp_of_typ new_dts tp),
-					Option.map Binding.name_of sel,vn))
+Option.map Binding.name_of sel,vn))
-	     (args,(mk_var_names(map (typid o third) args)))
+(args,(mk_var_names(map (typid o third) args)))
-	 ) : cons;
+) : cons;
 val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
 val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs;
-val ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn eq =>
+val ((rewss, take_rews), theorems_thy) =
-Domain_Theorems.theorems (eq, eqs)) eqs
+thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
 ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
 in
 theorems_thy
 |> Sign.add_path (Long_Name.base_name comp_dnam)
 |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])]))
 |> Sign.parent_path
 end;
 val add_domain = gen_add_domain Sign.certify_typ;
 val add_domain_cmd = gen_add_domain Syntax.read_typ_global;
 local structure P = OuterParse and K = OuterKeyword in
 val _ = OuterKeyword.keyword "lazy";
 val dest_decl : (bool * binding option * string) parser =
 P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
 (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
 || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
 >> (fn t => (true,NONE,t))
 || P.typ >> (fn t => (false,NONE,t));
 val cons_decl =
 P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
 val type_var' : (string * string option) parser =
 (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));
 val type_args' : (string * string option) list parser =
 type_var' >> single ||
 P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
 Scan.succeed [];
 val domain_decl =
 (type_args' -- P.binding -- P.opt_infix) --
 (P.$$$ "=" |-- P.enum1 "|" cons_decl);
 val domains_decl =
 Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
 P.and_list1 domain_decl;
 fun mk_domain (opt_name : string option,
 doms : ((((string * string option) list * binding) * mixfix) *
 ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
 let
 val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
 val specs : ((string * string option) list * binding * mixfix *
 (binding * (bool * binding option * string) list * mixfix) list) list =
 map (fn (((vs, t), mx), cons) =>
 (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
 val comp_dnam =
 case opt_name of NONE => space_implode "_" names | SOME s => s;
 in add_domain_cmd comp_dnam specs end;
 val _ =
 OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
 (domains_decl >> (Toplevel.theory o mk_domain));
 end;
 end;

changeset 31288	67dff9c5b2bd
parent 31229	8a890890d143
child 31986	a68f88d264f7