# HG changeset patch # User oheimb # Date 878650829 -3600 # Node ID f63c283cefafdf2e5289314b8e761a5a0b6e8ddf # Parent 390e10ddadf2fea3042e4c0256fd180fa5f106f0 * 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...) diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/HOLCFLogic.ML --- /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 *) diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/IOA/meta_theory/Seq.thy --- 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 diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/IsaMakefile --- 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 diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/ROOT.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"; diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/ax_ops/holcflogic.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; diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/ax_ops/thy_axioms.ML --- 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 *) diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/ax_ops/thy_ops.ML --- 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 *) diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/ax_ops/thy_syntax.ML --- 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); diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/contconsts.ML --- /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]; + diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/domain/axioms.ML --- 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 *) diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/domain/extender.ML --- 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 *) diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/domain/interface.ML --- 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 *) diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/domain/library.ML --- 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 *) diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/domain/syntax.ML --- 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 *) diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/ex/Stream.thy --- 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