oheimb@2453: (* Title: HOLCF/domain/syntax.ML oheimb@2445: ID: $Id$ wenzelm@12030: Author: David von Oheimb oheimb@2445: wenzelm@12030: Syntax generator for domain section. regensbu@1274: *) regensbu@1274: regensbu@1274: structure Domain_Syntax = struct regensbu@1274: regensbu@1274: local regensbu@1274: regensbu@1274: open Domain_Library; oheimb@4122: infixr 5 -->; infixr 6 ->>; oheimb@4122: fun calc_syntax dtypeprod ((dname, typevars), oheimb@4122: (cons': (string * mixfix * (bool*string*typ) list) list)) = regensbu@1274: let oheimb@4122: (* ----- constants concerning the isomorphism ------------------------------- *) regensbu@1274: regensbu@1274: local oheimb@4122: fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t oheimb@4122: fun prod (_,_,args) = if args = [] then oneT oheimb@4122: else foldr' mk_sprodT (map opt_lazy args); oheimb@4122: fun freetvar s = let val tvar = mk_TFree s in oheimb@4122: if tvar mem typevars then freetvar ("t"^s) else tvar end; skalberg@15574: fun when_type (_ ,_,args) = foldr (op ->>) (freetvar "t") (map third args); regensbu@1274: in regensbu@1274: val dtype = Type(dname,typevars); oheimb@4122: val dtype2 = foldr' mk_ssumT (map prod cons'); oheimb@4008: val dnam = Sign.base_name dname; oheimb@4122: val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn); oheimb@4122: val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn); skalberg@15574: val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); oheimb@4122: val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn); regensbu@1274: end; regensbu@1274: oheimb@4122: (* ----- constants concerning constructors, discriminators, and selectors --- *) regensbu@1274: regensbu@1274: local regensbu@1274: val escape = let oheimb@4122: fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs oheimb@4122: else c::esc cs oheimb@4122: | esc [] = [] wenzelm@4709: in implode o esc o Symbol.explode end; skalberg@15574: fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s); oheimb@4122: fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT, wenzelm@5700: Mixfix(escape ("is_" ^ con), [], Syntax.max_pri)); oheimb@4122: (* stricly speaking, these constants have one argument, oheimb@4122: but the mixfix (without arguments) is introduced only oheimb@4122: to generate parse rules for non-alphanumeric names*) huffman@16224: fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_ssumT(oneT,mk_uT(mk_ctupleT(map third args))), huffman@16224: Mixfix(escape ("match_" ^ con), [], Syntax.max_pri)); oheimb@4122: fun sel (_ ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ->> typ,NoSyn))args; regensbu@1274: in regensbu@1274: val consts_con = map con cons'; regensbu@1274: val consts_dis = map dis cons'; huffman@16224: val consts_mat = map mat cons'; skalberg@15570: val consts_sel = List.concat(map sel cons'); regensbu@1274: end; regensbu@1274: oheimb@4122: (* ----- constants concerning induction ------------------------------------- *) regensbu@1274: oheimb@4122: val const_take = (dnam^"_take" , HOLogic.natT-->dtype->>dtype, NoSyn); oheimb@4122: val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn); regensbu@1274: oheimb@4122: (* ----- case translation --------------------------------------------------- *) regensbu@1274: regensbu@1274: local open Syntax in regensbu@1274: val case_trans = let oheimb@4122: fun c_ast con mx = Constant (const_name con mx); oheimb@4122: fun expvar n = Variable ("e"^(string_of_int n)); oheimb@4122: fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^ oheimb@4122: (string_of_int m)); oheimb@1637: fun app s (l,r) = mk_appl (Constant s) [l,r]; wenzelm@9060: fun case1 n (con,mx,args) = mk_appl (Constant "_case1") skalberg@15570: [Library.foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)), oheimb@1637: expvar n]; oheimb@1637: fun arg1 n (con,_,args) = if args = [] then expvar n oheimb@1637: else mk_appl (Constant "LAM ") oheimb@1637: [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n]; wenzelm@3534: in wenzelm@3534: ParsePrintRule wenzelm@9060: (mk_appl (Constant "_case_syntax") [Variable "x", foldr' wenzelm@9060: (fn (c,cs) => mk_appl (Constant"_case2") [c,cs]) wenzelm@3534: (mapn case1 1 cons')], skalberg@15570: mk_appl (Constant "Rep_CFun") [Library.foldl slotosch@5291: (fn (w,a ) => mk_appl (Constant"Rep_CFun" ) [w,a ]) oheimb@4008: (Constant (dnam^"_when"),mapn arg1 1 cons'), wenzelm@3534: Variable "x"]) regensbu@1274: end; regensbu@1274: end; regensbu@1274: regensbu@1274: in ([const_rep, const_abs, const_when, const_copy] @ huffman@16224: consts_con @ consts_dis @ consts_mat @ consts_sel @ regensbu@1274: [const_take, const_finite], regensbu@1274: [case_trans]) regensbu@1274: end; (* let *) regensbu@1274: oheimb@4122: (* ----- putting all the syntax stuff together ------------------------------ *) regensbu@1274: regensbu@1274: in (* local *) regensbu@1274: oheimb@4008: fun add_syntax (comp_dnam,eqs': ((string * typ list) * oheimb@4122: (string * mixfix * (bool*string*typ) list) list) list) thy'' = regensbu@1274: let oheimb@4122: val dtypes = map (Type o fst) eqs'; oheimb@4122: val boolT = HOLogic.boolT; oheimb@4122: val funprod = foldr' mk_prodT (map (fn tp => tp ->> tp ) dtypes); oheimb@4122: val relprod = foldr' mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes); oheimb@4122: val const_copy = (comp_dnam^"_copy" ,funprod ->> funprod, NoSyn); oheimb@4122: val const_bisim = (comp_dnam^"_bisim" ,relprod --> boolT , NoSyn); regensbu@1274: val ctt = map (calc_syntax funprod) eqs'; skalberg@15570: in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ oheimb@4122: (if length eqs'>1 then [const_copy] else[])@ oheimb@4122: [const_bisim]) skalberg@15570: |> Theory.add_trrules_i (List.concat(map snd ctt)) regensbu@1274: end; (* let *) regensbu@1274: regensbu@1274: end; (* local *) regensbu@1274: end; (* struct *)