* removed "axioms" and "generated by" section
* replaced "ops" section by extended "consts" section, which is capable of
handling the continuous function space "->" directly
* domain package: now uses normal mixfix annotations (instead of cinfix...)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/HOLCFLogic.ML Tue Nov 04 14:40:29 1997 +0100
@@ -0,0 +1,66 @@
+(* Title: HOLCF/HOLCFLogic.ML
+ ID: $Id$
+ Author: David von Oheimb
+
+Abstract syntax operations for HOLCF.
+*)
+
+infixr 6 ->>;
+
+signature HOLCFLOGIC =
+sig
+ val mk_btyp: string -> typ * typ -> typ
+ val mk_prodT: typ * typ -> typ
+ val mk_not: term -> term
+
+ val HOLCF_sg: Sign.sg
+ val pcpoC: class
+ val pcpoS: sort
+ val mk_TFree: string -> typ
+ val cfun_arrow: string
+ val ->> : typ * typ -> typ
+ val mk_ssumT : typ * typ -> typ
+ val mk_sprodT: typ * typ -> typ
+ val mk_uT: typ -> typ
+ val trT: typ
+ val oneT: typ
+
+end;
+
+
+structure HOLCFLogic: HOLCFLOGIC =
+struct
+
+local
+
+ open HOLogic;
+
+in
+
+fun mk_btyp t (S,T) = Type (t,[S,T]);
+val mk_prodT = mk_btyp "*";
+
+fun mk_not P = Const ("Not", boolT --> boolT) $ P;
+
+(* basics *)
+
+val HOLCF_sg = sign_of HOLCF.thy;
+val pcpoC = Sign.intern_class HOLCF_sg "pcpo";
+val pcpoS = [pcpoC];
+fun mk_TFree s = TFree ("'"^s, pcpoS);
+
+(*cfun, ssum, sprod, u, tr, one *)
+
+local val intern = Sign.intern_tycon HOLCF_sg;
+in
+val cfun_arrow = intern "->";
+val op ->> = mk_btyp cfun_arrow;
+val mk_ssumT = mk_btyp (intern "++");
+val mk_sprodT = mk_btyp (intern "**");
+fun mk_uT T = Type (intern "u" ,[T]);
+val trT = Type (intern "tr" ,[ ]);
+val oneT = Type (intern "one",[ ]);
+end;
+
+end; (* local *)
+end; (* struct *)
--- a/src/HOLCF/IOA/meta_theory/Seq.thy Tue Nov 04 14:37:51 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Tue Nov 04 14:40:29 1997 +0100
@@ -9,7 +9,7 @@
Seq = HOLCF +
-domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq) (cinfixr 65)
+domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq) (infixr 65)
consts
--- a/src/HOLCF/IsaMakefile Tue Nov 04 14:37:51 1997 +0100
+++ b/src/HOLCF/IsaMakefile Tue Nov 04 14:40:29 1997 +0100
@@ -22,8 +22,7 @@
ONLYTHYS =
FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) adm.ML \
- ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \
- ax_ops/thy_ops.ML ax_ops/thy_syntax.ML \
+ HOLCFLogic.ML contconsts.ML \
domain/library.ML domain/syntax.ML domain/axioms.ML \
domain/theorems.ML domain/extender.ML domain/interface.ML
--- a/src/HOLCF/ROOT.ML Tue Nov 04 14:37:51 1997 +0100
+++ b/src/HOLCF/ROOT.ML Tue Nov 04 14:40:29 1997 +0100
@@ -14,14 +14,10 @@
use_thy "HOLCF";
-(* sections axioms, ops *)
-use "ax_ops/holcflogic.ML";
-use "ax_ops/thy_axioms.ML";
-use "ax_ops/thy_ops.ML";
-use "ax_ops/thy_syntax.ML";
+use "HOLCFLogic";
+use "contconsts";
-(* sections domain, generated *)
-
+(* domain package *)
use "domain/library.ML";
use "domain/syntax.ML";
use "domain/axioms.ML";
--- a/src/HOLCF/ax_ops/holcflogic.ML Tue Nov 04 14:37:51 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(*
- ID: $Id$
- Author: Tobias Mayr
-
-Additional term and type constructors, extension of Pure/term.ML, logic.ML
-and HOL/hologic.ML
-
-TODO:
-
-*)
-
-signature HOLCFLOGIC =
-sig
- val True : term;
- val False : term;
- val Imp : term;
- val And : term;
- val Not : term;
- val mkNot : term -> term; (* negates, no Trueprop *)
- val mkNotEqUU : term -> term; (* Trueprop(x ~= UU) *)
- val mkNotEqUU_in : term -> term -> term; (* "v~=UU ==> t" *)
- val ==> : typ * typ -> typ; (* Infix operation typ constructor *)
- val cfun_arrow : string (* internalized "->" *)
- val mkOpApp : term -> term -> term; (* Ops application (f ` x) *)
- val mkCPair : term -> term -> term; (* cpair constructor *)
-end;
-
-structure HOLCFlogic : HOLCFLOGIC =
-struct
-open Logic
-open HOLogic
-
-val True = Const("True",boolT);
-val False = Const("False",boolT);
-val Imp = Const("op -->",boolT --> boolT --> boolT);
-val And = Const("op &",boolT --> boolT --> boolT);
-val Not = Const("Not",boolT --> boolT);
-
-fun mkNot A = Not $ A; (* negates, no Trueprop *)
-
-(* Trueprop(x ~= UU) *)
-fun mkNotEqUU v = mk_Trueprop(mkNot(mk_eq(v,Const("UU",fastype_of v))));
-
-(* mkNotEqUU_in v t = "v~=UU ==> t" *)
-fun mkNotEqUU_in vterm term =
- mk_implies(mkNotEqUU vterm,term)
-
-val HOLCF_sg = sign_of HOLCF.thy;
-fun mk_typ t (S,T) = Sign.intern_typ HOLCF_sg (Type(t,[S,T]));
-fun rep_Type (Type x) = x| rep_Type _ = error "Internal error: rep_Type";
-
-infixr 6 ==>; (* the analogon to --> for operations *)
-val op ==> = mk_typ "->";
-val cfun_arrow = fst (rep_Type (dummyT ==> dummyT));
-
-(* Ops application (f ` x) *)
-fun mkOpApp (f as Const(_,ft as Type(_(*"->"*),[xt,rt]))) x =
- Const("fapp",ft --> xt --> rt) $ f $ x
- | mkOpApp f x = (error("Internal error: mkOpApp: wrong args"));
-
-(* cpair constructor *)
-fun mkCPair x y = let val tx = fastype_of x
- val ty = fastype_of y
- in
- Const("fapp",(ty==>Type("*",[tx,ty]))-->ty-->Type("*",[tx,ty])) $
- (mkOpApp (Const("cpair",tx ==> ty ==> Type("*",[tx,ty]))) x) $ y
- end;
-
-end;
--- a/src/HOLCF/ax_ops/thy_axioms.ML Tue Nov 04 14:37:51 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,209 +0,0 @@
-(*
- ID: $Id$
- Author: Tobias Mayr
-
-Additional theory file section for HOLCF: axioms
-*)
-
-(*** new section of HOLCF : axioms
- since rules are already internally called axioms,
- the new section is internally called ext_axioms res. eaxms *)
-
-signature THY_AXIOMS =
-sig
- (* theory extenders : *)
- val add_ext_axioms : (string * string) list -> (string * string) list
- -> (string * string) list -> theory -> theory;
- val add_ext_axioms_i : (string * (typ option)) list ->
- (string * (typ option)) list ->
- (string * term) list -> theory -> theory;
- val axioms_keywords : string list;
- val axioms_sections : (string * (ThyParse.token list ->
- (string * string) * ThyParse.token list)) list;
-end;
-
-structure ThyAxioms : THY_AXIOMS =
-struct
-
-open HOLCFlogic;
-
-(** library ******************************************************)
-
-fun apsnd_of_three f = fn (a,b,c) => (a,f b,c);
-
-fun is_elem e list = exists (fn y => e=y) list
-
-fun without l1 l2 = (* l1 without the elements of l2 *)
- filter (fn x => (not (is_elem x l2))) l1;
-
-fun conc [e:string] = e
- | conc (head::tail) = head^", "^(conc tail)
- | conc [] = "";
-
-fun appear varlist = (* all (x,_) for which (x,_) is in varlist *)
- filter (fn x => (exists (fn y => (fst x)=(fst y)) varlist))
-
-
-(* all non unique elements of a list *)
-fun doubles (hd::tl) = if (is_elem hd tl)
- then (hd::(doubles tl))
- else (doubles tl)
- | doubles _ = [];
-
-
-(* The main functions are the section parser ext_axiom_decls and the
- theory extender add_ext_axioms. *)
-
-(** theory extender : add_ext_axioms *)
-
-(* forms a function from constrained varnames to their constraints
- these constraints are then used local to each axiom, as an argument
- of read_def_cterm. Called by add_ext_axioms. *)
-fun get_constraints_of_str sign ((vname,vtyp)::tail) =
- if (vtyp <> "")
- then ((fn (x,_)=> if x=vname
- then Some (#T (rep_ctyp (read_ctyp sign vtyp)))
- else raise Match)
- orelf (get_constraints_of_str sign tail))
- else (get_constraints_of_str sign tail)
- | get_constraints_of_str sign [] = K None;
-
-(* does the same job for allready parsed optional constraints.
- Called by add_ext_axioms_i. *)
-fun get_constraints_of_typ sign ((vname,vtyp)::tail) =
- if (is_some vtyp)
- then ((fn (x,_)=> if x=vname
- then vtyp
- else raise Match)
- orelf (get_constraints_of_typ sign tail))
- else (get_constraints_of_typ sign tail)
- | get_constraints_of_typ sign [] = K None;
-
-
-(* applies mkNotEqUU_in on the axiom and every Free that appears in the list
- and in the axiom. Called by check_and_extend. *)
-fun add_prem axiom [] = axiom
- | add_prem axiom (vname::tl) =
- let val vterm = find_first (fn x => ((#1 o dest_Free) x = vname))
- (term_frees axiom)
- in
- add_prem
- (if (is_some vterm)
- then mkNotEqUU_in (the vterm) axiom
- else axiom)
- tl
- end
-
-(* checks for uniqueness and completeness of var/defvar declarations,
- and enriches the axiom term with premises. Called by add_ext_axioms(_i).*)
-fun check_and_extend sign defvarl varl axiom =
- let
- val names_of_frees = map (fst o dest_Free)
- (term_frees axiom);
- val all_decl_varnames = (defvarl @ varl);
- val undeclared = without names_of_frees all_decl_varnames;
- val doubles = doubles all_decl_varnames
- in
- if (doubles <> [])
- then
- (error("Multiple declarations of one identifier in section axioms :\n"
- ^(conc doubles)))
- else ();
- if (undeclared <> [])
- then
- (error("Undeclared identifiers in section axioms : \n"
- ^(conc undeclared)))
- else ();
- add_prem axiom (rev defvarl)
- end;
-
-(* the next five only differ from the original add_axioms' subfunctions
- in the constraints argument for read_def_cterm *)
-local
- fun err_in_axm name =
- error ("The error(s) above occurred in axiom " ^ quote name);
-
- fun no_vars tm =
- if null (term_vars tm) andalso null (term_tvars tm) then tm
- else error "Illegal schematic variable(s) in term";
-
- fun read_ext_cterm sign constraints =
- #1 o read_def_cterm (sign, constraints, K None) [] true;
-
- (* only for add_ext_axioms (working on strings) *)
- fun read_ext_axm sg constraints (name,str) =
- (name, no_vars (term_of (read_ext_cterm sg constraints (str, propT))))
- handle ERROR => err_in_axm name;
-
- (* only for add_ext_axioms_i (working on terms) *)
- fun read_ext_axm_terms sg constraints (name,term) =
- (name, no_vars (#2(Sign.infer_types sg constraints (K None) [] true
- ([term], propT))))
- handle ERROR => err_in_axm name;
-
-in
-
-(******* THE THEORY EXTENDERS THEMSELVES *****)
- fun add_ext_axioms varlist defvarlist axioms theory =
- let val {sign, ...} = rep_theory theory;
- val constraints = get_constraints_of_str sign (defvarlist@varlist)
- in
- PureThy.add_store_axioms_i (map (apsnd
- (check_and_extend sign (map fst defvarlist) (map fst varlist)) o
- (read_ext_axm sign constraints)) axioms) theory
- end
-
- fun add_ext_axioms_i varlist defvarlist axiom_terms theory =
- let val {sign, ...} = rep_theory theory;
- val constraints = get_constraints_of_typ sign (defvarlist@varlist)
- in
- PureThy.add_store_axioms_i (map (apsnd (check_and_extend sign
- (map fst defvarlist) (map fst varlist)) o
- (read_ext_axm_terms sign constraints)) axiom_terms) theory
- end
-end;
-
-
-(******** SECTION PARSER : ext_axiom_decls **********)
-local
- open ThyParse
-
- (* as in the pure section 'rules' :
- making the "val thmname = get_axiom thy thmname" list *)
- val mk_list_of_pairs = mk_big_list o map (mk_pair o apfst quote);
- fun mk_val ax = "val " ^ ax ^ " = get_axiom thy " ^ quote ax ^ ";";
- val mk_vals = cat_lines o map mk_val;
-
- (* making the call for the theory extender *)
- fun mk_eaxms_decls ((vars,defvars),axms) =
- ( "|> ThyAxioms.add_ext_axioms \n " ^
- (mk_list_of_pairs vars) ^ "\n " ^
- (mk_list_of_pairs defvars) ^ "\n " ^
- (mk_list_of_pairs axms),
- mk_vals (map fst axms));
-
- (* parsing the concrete syntax *)
-
- val axiom_decls = (repeat1 (ident -- !! string));
-
- val varlist = "vars" $$--
- repeat1 (ident -- optional ("::" $$-- string) "\"\"");
-
- val defvarlist = "defvars" $$--
- repeat1 (ident -- optional ("::" $$-- string) "\"\"");
-
-in
-
- val ext_axiom_decls = (optional varlist []) -- (optional defvarlist [])
- -- ("in" $$-- axiom_decls) >> mk_eaxms_decls;
-end; (* local *)
-
-
-(**** new keywords and sections ************************************)
-
-val axioms_keywords = ["vars", "defvars","in"];
- (* "::" is already a pure keyword *)
-
-val axioms_sections = [("axioms" , ext_axiom_decls)]
-
-end; (* the structure *)
--- a/src/HOLCF/ax_ops/thy_ops.ML Tue Nov 04 14:37:51 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,449 +0,0 @@
-(* TTITLEF/thy_ops.ML
- ID: $Id$
- Author: Tobias Mayr
-
-Additional theory file section for HOLCF: ops
-
-TODO:
- maybe AST-representation with "op name" instead of _I_...
-*)
-
-signature THY_OPS =
-sig
- (* continuous mixfixes (extension of datatype Mixfix.mixfix) *)
- datatype cmixfix =
- Mixfix of Mixfix.mixfix |
- CInfixl of int |
- CInfixr of int |
- CMixfix of string * int list *int;
-
- exception CINFIX of cmixfix;
- val cmixfix_to_mixfix : cmixfix -> Mixfix.mixfix;
-
- (* theory extenders : *)
- val add_ops : {curried: bool, total: bool, strict: bool} ->
- (string * string * cmixfix) list -> theory -> theory;
- val add_ops_i : {curried: bool, total: bool, strict: bool} ->
- (string * typ * cmixfix) list -> theory -> theory;
- val ops_keywords : string list;
- val ops_sections : (string * (ThyParse.token list ->
- (string * string) * ThyParse.token list)) list;
- val opt_cmixfix: ThyParse.token list -> (string * ThyParse.token list);
- val const_name : string -> cmixfix -> string;
-end;
-
-structure ThyOps : THY_OPS =
-struct
-
-open HOLCFlogic;
-
-(** library ******************************************************)
-
-(* abbreviations *)
-val internal = fst; (* cinfix-ops will have diffrent internal/external names *)
-val external = snd;
-
-fun apsnd_of_three f = fn (a,b,c) => (a,f b,c);
-
-
-(******** ops ********************)
-
-(* the extended copy of mixfix *)
-datatype cmixfix =
- Mixfix of Mixfix.mixfix |
- CInfixl of int |
- CInfixr of int |
- CMixfix of string * int list *int;
-
-exception CINFIX of cmixfix;
-
-fun cmixfix_to_mixfix (Mixfix x) = x
- | cmixfix_to_mixfix x = raise CINFIX x;
-
-
-(** theory extender : add_ops *)
-
-(* generating the declarations of the new constants. *************
- cinfix names x are internally non infix (renamed by mk_internal_name)
- and externally non continous infix function names (changed by op_to_fun).
- Thus the cinfix declaration is splitted in an 'oldstyle' decl,
- which is NoSyn (non infix) and is added by add_consts_i,
- and an syn(tactic) decl, which is an infix function (not operation)
- added by add_syntax_i, so that it can appear in input strings, but
- not in terms.
- The interface between internal and external names is realized by
- transrules A x B <=> _x ' A ' B (generated by xrules_of)
- The boolean argument 'curried' distinguishes between curried and
- tupeled syntax of operation application *)
-
-local
- fun strip ("'" :: c :: cs) = c :: strip cs
- | strip ["'"] = []
- | strip (c :: cs) = c :: strip cs
- | strip [] = [];
-
- val strip_esc = implode o strip o explode;
-
- fun infix_name c = "op " ^ strip_esc c;
-in
- val mk_internal_name = infix_name;
-(*
-(* changing e.g. 'ab' to '_I_97_98'.
- Called by oldstyle, xrules_of, strictness_axms and totality_axms. *)
- fun mk_internal_name name =
- let fun alphanum (s::ss) = "_"^(string_of_int (ord s))^(alphanum ss)
- | alphanum [] = "";
- in
- "_I"^(alphanum o explode) name
- end;
-*)
- (* extension of Pure/Syntax/mixfix.ML: SynExt.const_name *)
- fun const_name c (CInfixl _) = mk_internal_name c
- | const_name c (CInfixr _) = mk_internal_name c
- | const_name c (CMixfix _) = c
- | const_name c (Mixfix x) = Syntax.const_name c x;
-end;
-
-(* Changing a->b->c res. a*b->c to a=>b=>c. Called by syn_decls. *)
-(*####*)
-fun op_to_fun true sign (ty as Type(name ,[larg,t]))= if name = cfun_arrow
- then Type("fun",[larg,op_to_fun true sign t]) else ty
- | op_to_fun false sign (ty as Type(name,[args,res])) = let
- fun otf (Type("*",[larg,rargs])) = Type("fun",[larg,otf rargs])
- | otf t = Type("fun",[t,res]);
- in if name = cfun_arrow then otf args else ty end
- | op_to_fun _ sign t = t;
-(*####*)
-
-(* oldstyle is called by add_ext_axioms(_i) *)
- (* the first part is just copying the homomorphic part of the structures *)
-fun oldstyle ((name,typ,Mixfix(x))::tl) =
- (name,typ,x)::(oldstyle tl)
- | oldstyle ((name,typ,CInfixl(i))::tl) =
- (mk_internal_name name,typ,Mixfix.NoSyn)::
- (oldstyle tl)
- | oldstyle ((name,typ,CInfixr(i))::tl) =
- (mk_internal_name name,typ,Mixfix.NoSyn)::
- (oldstyle tl)
- | oldstyle ((name,typ,CMixfix(x))::tl) =
- (name,typ,Mixfix.NoSyn)::
- (oldstyle tl)
- | oldstyle [] = [];
-
-(* generating the external purely syntactical infix functions.
- Called by add_ext_axioms(_i) *)
-fun syn_decls curried sign ((name,typ,CInfixl(i))::tl) =
- (name,op_to_fun curried sign typ,Mixfix.Infixl(i))::
- (syn_decls curried sign tl)
- | syn_decls curried sign ((name,typ,CInfixr(i))::tl) =
- (name,op_to_fun curried sign typ,Mixfix.Infixr(i))::
- (syn_decls curried sign tl)
- | syn_decls curried sign ((name,typ,CMixfix(x))::tl) =
- (name,op_to_fun curried sign typ,Mixfix.Mixfix(x))::
-
- (syn_decls curried sign tl)
- | syn_decls curried sign (_::tl) = syn_decls curried sign tl
- | syn_decls _ _ [] = [];
-
-fun translate name vars rhs =
- Syntax.ParsePrintRule ((Ast.mk_appl (Constant (mk_internal_name name))
- (map Variable vars)),
- rhs);
-
-(* generating the translation rules. Called by add_ext_axioms(_i) *)
-local open Ast in
-fun xrules_of true ((name,typ,CInfixl(i))::tail) =
- translate name ["A","B"]
- (mk_appl (Constant "@fapp")
- [(mk_appl (Constant "@fapp")
- [Constant (mk_internal_name name),Variable "A"]),Variable "B"])
- ::xrules_of true tail
- | xrules_of true ((name,typ,CInfixr(i))::tail) =
- translate name ["A","B"]
- (mk_appl (Constant "@fapp")
- [(mk_appl (Constant "@fapp")
- [Constant (mk_internal_name name),Variable "A"]),Variable "B"])
- ::xrules_of true tail
-(*####*)
- | xrules_of true ((name,typ,CMixfix(_))::tail) =
- let fun argnames n (Type(name ,[_,t]))= if name = cfun_arrow then
- chr n :: argnames (n+1) t else []
- | argnames _ _ = [];
- val names = argnames (ord"A") typ;
- in if names = [] then [] else
- [Syntax.ParsePrintRule (mk_appl (Constant name) (map Variable names),
- foldl (fn (t,arg) =>
- (mk_appl (Constant "@fapp") [t,Variable arg]))
- (Constant name,names))]
- end
- @xrules_of true tail
-(*####*)
- | xrules_of false ((name,typ,CInfixl(i))::tail) =
- translate name ["A","B"]
- (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
- (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
- ::xrules_of false tail
- | xrules_of false ((name,typ,CInfixr(i))::tail) =
- translate name ["A","B"]
- (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
- (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
- ::xrules_of false tail
-(*####*)
- | xrules_of false ((name,typ,CMixfix(_))::tail) =
- let fun foldr' f l =
- let fun itr [] = raise LIST "foldr'"
- | itr [a] = a
- | itr (a::l) = f(a, itr l)
- in itr l end;
- fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t
- | argnames n _ = [chr n];
- val vars = map Variable (case typ of (Type(name ,[t,_])) =>
- if name = cfun_arrow then argnames (ord"A") t else []
- | _ => []);
- in if vars = [] then [] else
- [Syntax.ParsePrintRule
- (mk_appl (Constant name) vars,
- mk_appl (Constant "@fapp")
- [Constant name,
- case vars of [v] => v
- | args => mk_appl (Constant "@ctuple")
- [hd args,
- foldr' (fn (t,arg) =>
- mk_appl (Constant "_args")
- [t,arg]) (tl args)]])]
- end
- @xrules_of false tail
-(*####*)
- | xrules_of c ((name,typ,Mixfix(_))::tail) = xrules_of c tail
- | xrules_of _ [] = [];
-end;
-(**** producing the new axioms ****************)
-
-datatype arguments = Curried_args of ((typ*typ) list) |
- Tupeled_args of (typ list);
-
-fun num_of_args (Curried_args l) = length l
- | num_of_args (Tupeled_args l) = length l;
-
-fun types_of (Curried_args l) = map fst l
- | types_of (Tupeled_args l) = l;
-
-fun mk_mkNotEqUU_vars (typ::tl) cnt = mkNotEqUU (Free("x"^(string_of_int cnt),typ))::
- (mk_mkNotEqUU_vars tl (cnt+1))
- | mk_mkNotEqUU_vars [] _ = [];
-
-local
- (* T1*...*Tn goes to [T1,...,Tn] *)
- fun args_of_tupel (Type("*",[left,right])) = left::(args_of_tupel right)
- | args_of_tupel T = [T];
-
- (* A1->...->An->R goes to [(A1,B1),...,(An,Bn)] where Bi=Ai->...->An->R
- Bi is the Type of the function that is applied to an Ai type argument *)
- fun args_of_curried (typ as (Type(name,[S,T]))) = if name = cfun_arrow then
- (S,typ) :: args_of_curried T else []
- | args_of_curried _ = [];
-in
- fun args_of_op true typ = Curried_args(rev(args_of_curried typ))
- | args_of_op false (typ as (Type(name,[S,T]))) = if name = cfun_arrow then
- Tupeled_args(args_of_tupel S) else Tupeled_args([])
- | args_of_op false _ = Tupeled_args([]);
-end;
-
-(* generates for the type t the type of the fapp constant
- that will be applied to t *)
-fun mk_fapp_typ (typ as Type(_(*"->"*),argl)) = Type("fun",[typ,Type("fun",argl)])
- | mk_fapp_typ t = (
- error("Internal error:mk_fapp_typ: wrong argument\n"));
-
-fun mk_arg_tupel_UU uu_pos [typ] n =
- if n<>uu_pos then Free("x"^(string_of_int n),typ)
- else Const("UU",typ)
- | mk_arg_tupel_UU uu_pos (typ::tail) n =
- mkCPair
- (if n<>uu_pos then Free("x"^(string_of_int n),typ)
- else Const("UU",typ))
- (mk_arg_tupel_UU uu_pos tail (n+1))
- | mk_arg_tupel_UU _ [] _ = error("Internal error:mk_arg_tupel: empty list");
-
-fun mk_app_UU cnt uu_pos fname (Curried_args((typ,ftyp)::tl)) =
- Const("fapp",mk_fapp_typ ftyp) $
- (mk_app_UU (cnt-1) uu_pos fname (Curried_args tl))$
- (if cnt = uu_pos then Const("UU",typ)
- else Free("x"^(string_of_int cnt),typ))
- | mk_app_UU _ _ (name,typ) (Curried_args []) = Const(name,typ)
- | mk_app_UU cnt uu_pos (name,typ) (Tupeled_args []) = Const(name,typ)
- | mk_app_UU cnt uu_pos (name,typ) (Tupeled_args list) =
- Const("fapp",mk_fapp_typ typ) $ Const(name,typ) $
- mk_arg_tupel_UU uu_pos list 0;
-
-fun mk_app cnt fname args = mk_app_UU cnt (~1) fname args;
-
-(* producing the strictness axioms *)
-local
- fun s_axm_of curried name typ args num cnt =
- if cnt = num then
- error("Internal error: s_axm_of: arg is no operation "^(external name))
- else
- let val app = mk_app_UU (num-1) cnt (internal name,typ) args
- val equation = HOLogic.mk_eq(app,Const("UU",fastype_of app))
- in
- if cnt = num-1 then equation
- else And $ equation $
- s_axm_of curried name typ args num (cnt+1)
- end;
-in
- fun strictness_axms curried ((rawname,typ,cmixfix)::tail) =
- let val name = case cmixfix of
- (CInfixl _) => (mk_internal_name rawname,rawname)
- | (CInfixr _) => (mk_internal_name rawname,rawname)
- | _ => (rawname,rawname)
- val args = args_of_op curried typ;
- val num = num_of_args args;
- in
- ((external name)^"_strict",
- if num <> 0
- then HOLogic.mk_Trueprop(s_axm_of curried name typ args num 0)
- else HOLogic.mk_Trueprop(True)) :: strictness_axms curried tail
- end
- | strictness_axms _ [] = [];
-end; (*local*)
-
-(* producing the totality axioms *)
-
-fun totality_axms curried ((rawname,typ,cmixfix)::tail) =
- let val name = case cmixfix of
- (CInfixl _) => (mk_internal_name rawname,rawname)
- | (CInfixr _) => (mk_internal_name rawname,rawname)
- | _ => (rawname,rawname)
- val args = args_of_op curried typ;
- val prems = mk_mkNotEqUU_vars (if curried then rev (types_of args)
- else (types_of args)) 0;
- val term = mk_app (num_of_args args - 1) (internal name,typ) args;
- in
- ((external name)^"_total",
- if num_of_args args <> 0
- then Logic.list_implies (prems,mkNotEqUU term)
- else HOLogic.mk_Trueprop(True)) :: totality_axms curried tail
- end
- | totality_axms _ [] = [];
-
-
-
-(* the theory extenders ****************************)
-
-fun add_ops {curried,strict,total} raw_decls thy =
- let val {sign,...} = rep_theory thy;
- val decls = map (apsnd_of_three (typ_of o read_ctyp sign)) raw_decls;
- val oldstyledecls = oldstyle decls;
- val syndecls = syn_decls curried sign decls;
- val xrules = xrules_of curried decls;
- val s_axms = (if strict then strictness_axms curried decls else []);
- val t_axms = (if total then totality_axms curried decls else []);
- in
- Theory.add_trrules_i xrules (PureThy.add_store_axioms_i (s_axms @ t_axms)
- (Theory.add_syntax_i syndecls (Theory.add_consts_i oldstyledecls thy)))
- end;
-
-fun add_ops_i {curried,strict,total} decls thy =
- let val {sign,...} = rep_theory thy;
- val oldstyledecls = oldstyle decls;
- val syndecls = syn_decls curried sign decls;
- val xrules = xrules_of curried decls;
- val s_axms = (if strict then strictness_axms curried decls else []);
- val t_axms = (if total then totality_axms curried decls else []);
- in
- Theory.add_trrules_i xrules (PureThy.add_store_axioms_i (s_axms @ t_axms)
- (Theory.add_syntax_i syndecls (Theory.add_consts_i oldstyledecls thy)))
- end;
-
-
-(* parser: ops_decls ********************************)
-
-local open ThyParse
-in
-(* the following is an adapted version of const_decls from thy_parse.ML *)
-
-val names1 = list1 name;
-
-fun split_decls decls = flat (map (fn (xs, y) => map (rpair y) xs) decls);
-
-fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z);
-
-fun mk_strict_vals [] = ""
- | mk_strict_vals [name] =
- "get_axiom thy \""^name^"_strict\"\n"
- | mk_strict_vals (name::tail) =
- "get_axiom thy \""^name^"_strict\",\n"^
- mk_strict_vals tail;
-
-fun mk_total_vals [] = ""
- | mk_total_vals [name] =
- "get_axiom thy \""^name^"_total\"\n"
- | mk_total_vals (name::tail) =
- "get_axiom thy \""^name^"_total\",\n"^
- mk_total_vals tail;
-
-fun mk_ops_decls (((curried,strict),total),list) =
- (* call for the theory extender *)
- ("|> ThyOps.add_ops \n"^
- "{ curried = "^curried^" , strict = "^strict^
- " , total = "^total^" } \n"^
- (mk_big_list o map mk_triple2) list^";\n"^
- "val strict_axms = []; val total_axms = [];\nval thy = thy\n",
- (* additional declarations *)
- (if strict="true" then "val strict_axms = strict_axms @ [\n"^
- mk_strict_vals (map (strip_quotes o fst) list)^
- "];\n"
- else "")^
- (if total="true" then "val total_axms = total_axms @ [\n"^
- mk_total_vals (map (strip_quotes o fst) list)^
- "];\n"
- else ""));
-
-(* mixfix annotations *)
-
-fun cat_parens pre1 pre2 s = cat pre1 (parens (cat pre2 s));
-
-val infxl = "infixl" $$-- !! nat >> cat_parens "ThyOps.Mixfix" "Infixl";
-val infxr = "infixr" $$-- !! nat >> cat_parens "ThyOps.Mixfix" "Infixr";
-
-val cinfxl = "cinfixl" $$-- !! nat >> cat "ThyOps.CInfixl";
-val cinfxr = "cinfixr" $$-- !! nat >> cat "ThyOps.CInfixr";
-
-val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;
-
-val cmixfx = "cmixfix" $$-- string -- !! (opt_pris -- optional nat "max_pri")
- >> (cat "ThyOps.CMixfix" o mk_triple2);
-
-val bindr = "binder" $$--
- !! (string -- ( ("[" $$-- nat --$$ "]") -- nat
- || nat >> (fn n => (n,n))
- ) )
- >> (cat_parens "ThyOps.Mixfix" "Binder" o mk_triple2);
-
-val mixfx = string -- !! (opt_pris -- optional nat "max_pri")
- >> (cat_parens "ThyOps.Mixfix" "Mixfix" o mk_triple2);
-
-fun opt_syn fx = optional ("(" $$-- fx --$$ ")") "ThyOps.Mixfix NoSyn";
-
-val opt_cmixfix = opt_syn (mixfx || infxl || infxr || bindr ||
- cinfxl || cinfxr || cmixfx);
-
-fun ops_decls toks=
- (optional ($$ "curried" >> K "true") "false" --
- optional ($$ "strict" >> K "true") "false" --
- optional ($$ "total" >> K "true") "false" --
- (repeat1 (names1 --$$ "::" -- !! (string -- opt_cmixfix))
- >> split_decls)
- >> mk_ops_decls) toks
-
-end;
-
-(*** new keywords and sections: ******************************************)
-
-val ops_keywords = ["curried","strict","total","cinfixl","cinfixr","cmixfix"];
- (* "::" is already a pure keyword *)
-
-val ops_sections = [("ops" , ops_decls) ];
-
-end; (* the structure ThyOps *)
--- a/src/HOLCF/ax_ops/thy_syntax.ML Tue Nov 04 14:37:51 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-(* Title: HOLCF/thy_syntax.ML
- ID: $Id$
- Author: Tobias Mayr
-
-Additional thy file sections for HOLCF: axioms, ops.
-*)
-
-ThySyn.add_syntax
- (ThyAxioms.axioms_keywords @ ThyOps.ops_keywords)
- (ThyAxioms.axioms_sections @ ThyOps.ops_sections);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/contconsts.ML Tue Nov 04 14:40:29 1997 +0100
@@ -0,0 +1,99 @@
+(* Title: HOLCF/contconsts.ML
+ ID: $Id$
+ Author: Tobias Mayr and David von Oheimb
+
+theory extender for consts section
+*)
+
+structure ContConsts =
+struct
+
+local
+
+open HOLCFLogic;
+
+exception Impossible of string;
+fun Imposs msg = raise Impossible ("ContConst:"^msg);
+fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x;
+fun upd_first f (x,y,z) = (f x, y, z);
+fun upd_second f (x,y,z) = ( x, f y, z);
+fun upd_third f (x,y,z) = ( x, y, f z);
+
+fun filter2 (pred: 'a->bool) : 'a list -> 'a list * 'a list =
+ let fun filt [] = ([],[])
+ | filt (x::xs) = let val (ys,zs) = filt xs in
+ if pred x then (x::ys,zs) else (ys,x::zs) end
+ in filt end;
+
+fun change_arrow 0 T = T
+| change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
+| change_arrow _ _ = Imposs "change_arrow";
+
+fun trans_rules name2 name1 n mx = let
+ fun argnames _ 0 = []
+ | argnames c n = chr c::argnames (c+1) (n-1);
+ val vnames = argnames (ord "A") n;
+ val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
+ in [Syntax.ParsePrintRule (Ast.mk_appl (Constant name2) (map Variable vnames),
+ foldl (fn (t,arg) => (Ast.mk_appl (Constant "fapp")
+ [t,Variable arg]))
+ (Constant name1,vnames))]
+ @(case mx of InfixlName _ => [extra_parse_rule]
+ | InfixrName _ => [extra_parse_rule] | _ => []) end;
+
+
+(* transforming infix/mixfix declarations of constants with type ...->...
+ a declaration of such a constant is transformed to a normal declaration with
+ an internal name, the same type, and nofix. Additionally, a purely syntactic
+ declaration with the original name, type ...=>..., and the original mixfix
+ is generated and connected to the other declaration via some translation.
+*)
+fun fix_mixfix (syn , T, mx as Infixl p ) =
+ (Syntax.const_name syn mx, T, InfixlName (syn, p))
+ | fix_mixfix (syn , T, mx as Infixr p ) =
+ (Syntax.const_name syn mx, T, InfixrName (syn, p))
+ | fix_mixfix decl = decl;
+fun transform decl = let
+ val (c, T, mx) = fix_mixfix decl;
+ val c2 = "@"^c;
+ val n = Syntax.mixfix_args mx
+ in ((c , T,NoSyn),
+ (c2,change_arrow n T,mx ),
+ trans_rules c2 c n mx) end;
+
+fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
+| cfun_arity _ = 0;
+
+fun is_contconst (_,_,NoSyn ) = false
+| is_contconst (_,_,Binder _) = false
+| is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx
+ handle ERROR => error ("in mixfix annotation for " ^
+ quote (Syntax.const_name c mx));
+
+in (* local *)
+
+fun ext_consts prep_typ raw_decls thy =
+let val decls = map (upd_second (typ_of o prep_typ (sign_of thy))) raw_decls;
+ val (contconst_decls, normal_decls) = filter2 is_contconst decls;
+ val transformed_decls = map transform contconst_decls;
+in thy |> Theory.add_consts_i normal_decls
+ |> Theory.add_consts_i (map first transformed_decls)
+ |> Theory.add_syntax_i (map second transformed_decls)
+ |> Theory.add_trrules_i (flat (map third transformed_decls))
+ handle ERROR =>
+ error ("The error(s) above occurred in (cont)consts section")
+end;
+
+fun cert_typ sg typ =
+ ctyp_of sg typ handle TYPE (msg, _, _) => error msg;
+
+val add_consts = ext_consts read_ctyp;
+val add_consts_i = ext_consts cert_typ;
+
+end; (* local *)
+
+end; (* struct *)
+
+val _ = ThySyn.add_syntax []
+ [ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls];
+
--- a/src/HOLCF/domain/axioms.ML Tue Nov 04 14:37:51 1997 +0100
+++ b/src/HOLCF/domain/axioms.ML Tue Nov 04 14:40:29 1997 +0100
@@ -137,25 +137,5 @@
|> Theory.add_path ".."
end;
-
-fun add_induct ((tname,finite),(typs,cnstrs)) thy' = let
- fun P_name typ = "P"^(if typs = [typ] then ""
- else string_of_int(1 + find(typ,typs)));
- fun lift_adm t = lift (fn typ => %%"adm" $ %(P_name typ))
- (if finite then [] else typs,t);
- fun lift_pred_UU t = lift (fn typ => %(P_name typ) $ UU) (typs,t);
- fun one_cnstr (cnstr,vns,(args,res)) = let
- val rec_args = filter (fn (_,typ) => typ mem typs)(vns~~args);
- val app = mk_cfapp(%%cnstr,map (bound_arg vns) vns);
- in foldr mk_All (vns,
- lift (fn (vn,typ) => %(P_name typ) $ bound_arg vns vn)
- (rec_args,defined app ==> %(P_name res)$app)) end;
- fun one_conc typ = let val pn = P_name typ
- in %pn $ %("x"^implode(tl(explode pn))) end;
- val concl = mk_trp(foldr' mk_conj (map one_conc typs));
- val induct = (tname^"_induct",lift_adm(lift_pred_UU(
- foldr (op ===>) (map one_cnstr cnstrs,concl))));
-in thy' |> Theory.add_axioms_i (infer_types thy' [induct]) end;
-
end; (* local *)
end; (* struct *)
--- a/src/HOLCF/domain/extender.ML Tue Nov 04 14:37:51 1997 +0100
+++ b/src/HOLCF/domain/extender.ML Tue Nov 04 14:40:29 1997 +0100
@@ -17,7 +17,7 @@
(* ----- general testing and preprocessing of constructor list -------------- *)
fun check_and_sort_domain (dtnvs: (string * typ list) list, cons'' :
- ((string * ThyOps.cmixfix * (bool*string*typ) list) list) list) sg =
+ ((string * mixfix * (bool*string*typ) list) list) list) sg =
let
val defaultS = Type.defaultS (tsig_of sg);
val test_dupl_typs = (case duplicates (map fst dtnvs) of
@@ -65,52 +65,6 @@
in ListPair.map analyse_equation (dtnvs,cons'')
end; (* let *)
- fun check_gen_by sg' (typs': string list,cnstrss': string list list) = let
- val test_dupl_typs = (case duplicates typs' of [] => false
- | dups => error ("Duplicate types: " ^ commas_quote dups));
- val test_dupl_cnstrs = map (fn cs => (case duplicates cs of [] => false
- | ds => error ("Duplicate constructors: " ^ commas_quote ds))) cnstrss';
- val tycons = map fst (#tycons(Type.rep_tsig (tsig_of sg')));
- val test_types = forall (fn t => t mem tycons orelse
- error("Unknown type: "^t)) typs';
- val cnstrss = let
- fun type_of c = case (Sign.const_type sg' c) of Some t => t
- | None => error ("Unknown constructor: "^c);
- fun args_result_type (t as (Type(tn,[arg,rest]))) =
- if tn = cfun_arrow orelse tn = "=>"
- then let val (ts,r) = args_result_type rest in (arg::ts,r) end
- else ([],t)
- | args_result_type t = ([],t);
- in map (map (fn cn => let val (args,res) = args_result_type (type_of cn) in
- (cn,mk_var_names args,(args,res)) end)) cnstrss'
- : (string * (* operator name of constr *)
- string list * (* argument name list *)
- (typ list * (* argument types *)
- typ)) (* result type *)
- list list end;
- fun test_equal_type tn (cn,_,(_,rt)) = fst (rep_Type rt) = tn orelse
- error("Inappropriate result type for constructor "^cn);
- val typs = ListPair.map (fn (tn, cnstrs) =>(map (test_equal_type tn) cnstrs;
- snd(third(hd(cnstrs))))) (typs',cnstrss);
- val test_typs = ListPair.map (fn (typ,cnstrs) =>
- if not (pcpo_type sg' typ)
- then error("Not a pcpo type: "^string_of_typ sg' typ)
- else map (fn (cn,_,(_,rt)) => rt=typ orelse error(
- "Non-identical result types for constructors "^
- first(hd cnstrs)^" and "^ cn )) cnstrs)
- (typs,cnstrss);
- val proper_args = let
- fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts
- | occurs _ _ = false;
- fun proper_arg cn atyp = forall (fn typ => let
- val tn = fst (rep_Type typ)
- in atyp=typ orelse not (occurs tn atyp) orelse
- error("Illegal use of type "^ tn ^
- " as argument of constructor " ^cn)end )typs;
- fun proper_curry (cn,_,(args,_)) = forall (proper_arg cn) args;
- in map (map proper_curry) cnstrss end;
- in (typs, flat cnstrss) end;
-
(* ----- calls for building new thy and thms -------------------------------- *)
in
@@ -130,22 +84,21 @@
val eqs' = check_and_sort_domain (dtnvs,cons'') sg'';
val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
val dts = map (Type o fst) eqs';
+ fun strip ss = drop (find ("'", ss)+1, ss);
+ fun typid (Type (id,_) ) = hd (explode (Sign.base_name id))
+ | typid (TFree (id,_) ) = hd (strip (tl (explode (Sign.base_name id))))
+ | typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id)));
fun cons cons' = (map (fn (con,syn,args) =>
- ((ThyOps.const_name con syn),
+ ((Syntax.const_name con syn),
ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
find (tp,dts) handle LIST "find" => ~1),
sel,vn))
- (args,(mk_var_names(map third args)))
+ (args,(mk_var_names(map (typid o third) args)))
)) cons') : cons list;
val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list;
- val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
+ val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
in (foldl (fn (thy0,eq) => Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs))
|> Domain_Theorems.comp_theorems (comp_dnam, eqs) end;
- fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let
- val (typs,cnstrs) = check_gen_by (sign_of thy') (typs',cnstrss');
- in
- Domain_Axioms.add_induct ((tname,finite),(typs,cnstrs)) thy' end;
-
end (* local *)
end (* struct *)
--- a/src/HOLCF/domain/interface.ML Tue Nov 04 14:37:51 1997 +0100
+++ b/src/HOLCF/domain/interface.ML Tue Nov 04 14:40:29 1997 +0100
@@ -71,7 +71,7 @@
^ ";\n"
end;
-(* ----- string for calling (comp_)theorems and producing the structures ---- *)
+(* ----- string for producing the structures -------------------------------- *)
val val_gen_string = let
val comp_axioms = [(* copy, *) "reach", "take_def", "finite_def"
@@ -100,18 +100,6 @@
"val thy = thy",
"") end;
-(* ----- strings for calling add_gen_by and producing the value binding ----- *)
-
- fun mk_gen_by (finite,eqs) = let
- val typs = map fst eqs;
- val cnstrss = map snd eqs;
- val tname = implode (separate "_" typs) in
- ("|> Domain_Extender.add_gen_by "
- ^ mk_pair(mk_pair(quote tname, Bool.toString finite),
- mk_pair(mk_list(map quote typs),
- mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))),
- "val "^tname^"_induct = " ^get tname "induct" ^";") end;
-
(* ----- parser for domain declaration equation ----------------------------- *)
val name' = name >> strip_quotes;
@@ -122,7 +110,8 @@
| esc ("]" ::xs) = "}"::esc xs
| esc (x ::xs) = x ::esc xs
in implode (esc (explode s)) end;
- val tvar = (type_var' ^^ optional ($$ "::" ^^ (sort >> esc_quote)) "") >> quote;
+ val tvar = (type_var' ^^
+ optional ($$ "::" ^^ (sort >> esc_quote)) "") >> quote;
fun type_args l = (tvar >> (fn x => [x])
|| "(" $$-- !! (list1 tvar --$$ ")")
|| empty >> K []) l
@@ -131,20 +120,17 @@
to avoid ambiguity with standard mixfix option *)
val domain_arg = "(" $$-- (optional ($$ "lazy" >> K true) false)
-- (optional ((name' >> Some) --$$ "::") None)
- -- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
+ -- typ --$$ ")"
+ >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
|| typ >> (fn x => (false,None,x))
val domain_cons = name' -- !! (repeat domain_arg)
- -- ThyOps.opt_cmixfix
+ -- ThyParse.opt_mixfix
>> (fn ((con,args),syn) => (con,syn,args));
in
val domain_decl = (enum1 "and" (con_typ --$$ "=" -- !!
(enum1 "|" domain_cons))) >> mk_domain;
- val gen_by_decl = (optional ($$ "finite" >> K true) false) --
- (enum1 "," (name' --$$ "by" -- !!
- (enum1 "|" name'))) >> mk_gen_by;
-
val _ = ThySyn.add_syntax
- ["lazy", "and", "by", "finite"]
- [("domain", domain_decl), ("generated", gen_by_decl)]
+ ["lazy", "and"]
+ [("domain", domain_decl)]
end; (* local *)
--- a/src/HOLCF/domain/library.ML Tue Nov 04 14:37:51 1997 +0100
+++ b/src/HOLCF/domain/library.ML Tue Nov 04 14:40:29 1997 +0100
@@ -39,6 +39,8 @@
structure Domain_Library = struct
+open HOLCFLogic;
+
exception Impossible of string;
fun Imposs msg = raise Impossible ("Domain:"^msg);
@@ -59,11 +61,7 @@
(* make distinct names out of the type list,
forbidding "o", "x..","f..","P.." as names *)
(* a number string is added if necessary *)
-fun mk_var_names types : string list = let
- fun strip ss = drop (find ("'", ss)+1, ss);
- fun typid (Type (id,_) ) = hd (explode (Sign.base_name id))
- | typid (TFree (id,_) ) = hd (strip (tl (explode (Sign.base_name id))))
- | typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id)));
+fun mk_var_names ids : string list = let
fun nonreserved s = if s mem ["x","f","P"] then s^"'" else s;
fun index_vnames(vn::vns,occupied) =
(case assoc(occupied,vn) of
@@ -73,13 +71,12 @@
| Some(i) => (vn^(string_of_int (i+1)))
:: index_vnames(vns,(vn,i+1)::occupied))
| index_vnames([],occupied) = [];
-in index_vnames(map (nonreserved o typid) types,[("O",0),("o",0)]) end;
+in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
fun rep_Type (Type x) = x | rep_Type _ = Imposs "library:rep_Type";
fun rep_TFree (TFree x) = x | rep_TFree _ = Imposs "library:rep_TFree";
val tsig_of = #tsig o Sign.rep_sg;
-val HOLCF_sg = sign_of HOLCF.thy;
-val pcpoS = Sign.intern_sort HOLCF_sg ["pcpo"];
+
fun pcpo_type sg t = Type.of_sort (tsig_of sg) (Sign.certify_typ sg t, pcpoS);
fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg;
fun str2typ sg = typ_of o read_ctyp sg;
@@ -107,12 +104,7 @@
(* ----- support for type and mixfix expressions ----- *)
-fun mk_tvar s = TFree("'"^s,pcpoS);
-fun mk_typ t (S,T) = Sign.intern_typ HOLCF_sg (Type(t,[S,T]));
infixr 5 -->;
-infixr 6 ~>; val op ~> = mk_typ "->";
-val cfun_arrow = fst (rep_Type (dummyT ~> dummyT));
-val NoSyn' = ThyOps.Mixfix NoSyn;
(* ----- support for term expressions ----- *)
@@ -140,9 +132,7 @@
fun mk_constrain (typ,T) = %%"_constrain" $ T $ tf typ;
fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs" $ mk_lam(x,P) $ tf typ);
end;
-
fun mk_ex (x,P) = mk_exists (x,dummyT,P);
-fun mk_not P = Const("Not" ,boolT --> boolT) $ P;
end;
fun mk_All (x,P) = %%"all" $ mk_lam(x,P); (* meta universal quantification *)
--- a/src/HOLCF/domain/syntax.ML Tue Nov 04 14:37:51 1997 +0100
+++ b/src/HOLCF/domain/syntax.ML Tue Nov 04 14:40:29 1997 +0100
@@ -11,71 +11,67 @@
local
open Domain_Library;
-infixr 5 -->; infixr 6 ~>;
-fun calc_syntax dtypeprod ((dname, typevars), (cons':
- (string * ThyOps.cmixfix * (bool*string*typ) list) list)) =
+infixr 5 -->; infixr 6 ->>;
+fun calc_syntax dtypeprod ((dname, typevars),
+ (cons': (string * mixfix * (bool*string*typ) list) list)) =
let
-(* ----- constants concerning the isomorphism ------------------------------------- *)
+(* ----- constants concerning the isomorphism ------------------------------- *)
local
- fun opt_lazy (lazy,_,t) = if lazy then Type("u",[t]) else t
- fun prod (_,_,args) = if args = [] then Type("one",[])
- else foldr'(mk_typ "**") (map opt_lazy args);
- fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
- fun when_type (_ ,_,args) = foldr (op ~>) (map third args,freetvar "t");
+ fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
+ fun prod (_,_,args) = if args = [] then oneT
+ else foldr' mk_sprodT (map opt_lazy args);
+ fun freetvar s = let val tvar = mk_TFree s in
+ if tvar mem typevars then freetvar ("t"^s) else tvar end;
+ fun when_type (_ ,_,args) = foldr (op ->>) (map third args,freetvar "t");
in
val dtype = Type(dname,typevars);
- val dtype2 = foldr' (mk_typ "++") (map prod cons');
+ val dtype2 = foldr' mk_ssumT (map prod cons');
val dnam = Sign.base_name dname;
- val const_rep = (dnam^"_rep" , dtype ~> dtype2, NoSyn');
- val const_abs = (dnam^"_abs" , dtype2 ~> dtype , NoSyn');
- val const_when = (dnam^"_when", foldr (op ~>) ((map when_type cons'),
- dtype ~> freetvar "t"), NoSyn');
- val const_copy = (dnam^"_copy", dtypeprod ~> dtype ~> dtype , NoSyn');
+ val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn);
+ val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn);
+ val const_when = (dnam^"_when",foldr (op ->>) ((map when_type cons'),
+ dtype ->> freetvar "t"), NoSyn);
+ val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
end;
-(* ----- constants concerning the constructors, discriminators and selectors ------ *)
-
-fun is_infix (ThyOps.CInfixl _ ) = true
-| is_infix (ThyOps.CInfixr _ ) = true
-| is_infix (ThyOps.Mixfix(Infixl _)) = true
-| is_infix (ThyOps.Mixfix(Infixr _)) = true
-| is_infix _ = false;
+(* ----- constants concerning constructors, discriminators, and selectors --- *)
local
val escape = let
- fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
- else c :: esc cs
- | esc [] = []
+ fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
+ else c::esc cs
+ | esc [] = []
in implode o esc o explode end;
- fun con (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s);
- fun dis (con ,s,_ ) = (dis_name_ con, dtype~>Type("tr",[]),
- ThyOps.Mixfix(Mixfix("is'_"^
- (if is_infix s then Id else escape)con,[],max_pri)));
- fun sel (_ ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args;
+ fun con (name,s,args) = (name,foldr (op ->>) (map third args,dtype),s);
+ fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT,
+ Mixfix(escape ("is_" ^ con), [], max_pri));
+ (* stricly speaking, these constants have one argument,
+ but the mixfix (without arguments) is introduced only
+ to generate parse rules for non-alphanumeric names*)
+ fun sel (_ ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ->> typ,NoSyn))args;
in
val consts_con = map con cons';
val consts_dis = map dis cons';
val consts_sel = flat(map sel cons');
end;
-(* ----- constants concerning induction ------------------------------------------- *)
+(* ----- constants concerning induction ------------------------------------- *)
- val const_take = (dnam^"_take" , Type("nat",[]) --> dtype ~> dtype, NoSyn');
- val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn');
+ val const_take = (dnam^"_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
+ val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn);
-(* ----- case translation --------------------------------------------------------- *)
+(* ----- case translation --------------------------------------------------- *)
local open Syntax in
val case_trans = let
- fun c_ast con syn = Constant (ThyOps.const_name con syn);
- fun expvar n = Variable ("e"^(string_of_int n));
- fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
+ fun c_ast con mx = Constant (const_name con mx);
+ fun expvar n = Variable ("e"^(string_of_int n));
+ fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
+ (string_of_int m));
fun app s (l,r) = mk_appl (Constant s) [l,r];
- fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
- [if is_infix syn
- then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
- else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
+ fun case1 n (con,mx,args) = mk_appl (Constant "@case1")
+ [foldl (app "fapp") (c_ast con mx, (mapn (argvar n) 1 args)),
expvar n];
fun arg1 n (con,_,args) = if args = [] then expvar n
else mk_appl (Constant "LAM ")
@@ -83,10 +79,10 @@
in
ParsePrintRule
(mk_appl (Constant "@case") [Variable "x", foldr'
- (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
+ (fn (c,cs) => mk_appl (Constant"@case2") [c,cs])
(mapn case1 1 cons')],
- mk_appl (Constant "@fapp") [foldl
- (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
+ mk_appl (Constant "fapp") [foldl
+ (fn (w,a ) => mk_appl (Constant"fapp" ) [w,a ])
(Constant (dnam^"_when"),mapn arg1 1 cons'),
Variable "x"])
end;
@@ -98,22 +94,23 @@
[case_trans])
end; (* let *)
-(* ----- putting all the syntax stuff together ------------------------------------ *)
+(* ----- putting all the syntax stuff together ------------------------------ *)
in (* local *)
fun add_syntax (comp_dnam,eqs': ((string * typ list) *
- (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
+ (string * mixfix * (bool*string*typ) list) list) list) thy'' =
let
- val dtypes = map (Type o fst) eqs';
- val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp )dtypes);
- val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes);
- val const_copy = (comp_dnam^"_copy" ,funprod ~> funprod , NoSyn');
- val const_bisim = (comp_dnam^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
+ val dtypes = map (Type o fst) eqs';
+ val boolT = HOLogic.boolT;
+ val funprod = foldr' mk_prodT (map (fn tp => tp ->> tp ) dtypes);
+ val relprod = foldr' mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
+ val const_copy = (comp_dnam^"_copy" ,funprod ->> funprod, NoSyn);
+ val const_bisim = (comp_dnam^"_bisim" ,relprod --> boolT , NoSyn);
val ctt = map (calc_syntax funprod) eqs';
- val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
-in thy'' |> add_cur_ops_i (flat(map fst ctt))
- |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
+in thy'' |> ContConsts.add_consts_i (flat (map fst ctt) @
+ (if length eqs'>1 then [const_copy] else[])@
+ [const_bisim])
|> Theory.add_trrules_i (flat(map snd ctt))
end; (* let *)
--- a/src/HOLCF/ex/Stream.thy Tue Nov 04 14:37:51 1997 +0100
+++ b/src/HOLCF/ex/Stream.thy Tue Nov 04 14:40:29 1997 +0100
@@ -8,7 +8,7 @@
Stream = HOLCF +
-domain 'a stream = "&&" (ft::'a) (lazy rt::'a stream) (cinfixr 65)
+domain 'a stream = "&&" (ft::'a) (lazy rt::'a stream) (infixr 65)
end