20 fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t |
19 fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t |
21 fun prod (_,_,args) = if args = [] then oneT |
20 fun prod (_,_,args) = if args = [] then oneT |
22 else foldr1 mk_sprodT (map opt_lazy args); |
21 else foldr1 mk_sprodT (map opt_lazy args); |
23 fun freetvar s = let val tvar = mk_TFree s in |
22 fun freetvar s = let val tvar = mk_TFree s in |
24 if tvar mem typevars then freetvar ("t"^s) else tvar end; |
23 if tvar mem typevars then freetvar ("t"^s) else tvar end; |
25 fun when_type (_ ,_,args) = foldr (op ->>) (freetvar "t") (map third args); |
24 fun when_type (_ ,_,args) = List.foldr (op ->>) (freetvar "t") (map third args); |
26 in |
25 in |
27 val dtype = Type(dname,typevars); |
26 val dtype = Type(dname,typevars); |
28 val dtype2 = foldr1 mk_ssumT (map prod cons'); |
27 val dtype2 = foldr1 mk_ssumT (map prod cons'); |
29 val dnam = Sign.base_name dname; |
28 val dnam = Sign.base_name dname; |
30 val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn); |
29 val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn); |
31 val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn); |
30 val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn); |
32 val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); |
31 val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); |
33 val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn); |
32 val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn); |
34 end; |
33 end; |
35 |
34 |
36 (* ----- constants concerning constructors, discriminators, and selectors --- *) |
35 (* ----- constants concerning constructors, discriminators, and selectors --- *) |
37 |
36 |
39 val escape = let |
38 val escape = let |
40 fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs |
39 fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs |
41 else c::esc cs |
40 else c::esc cs |
42 | esc [] = [] |
41 | esc [] = [] |
43 in implode o esc o Symbol.explode end; |
42 in implode o esc o Symbol.explode end; |
44 fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s); |
43 fun con (name,s,args) = (name, List.foldr (op ->>) dtype (map third args),s); |
45 fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT, |
44 fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT, |
46 Mixfix(escape ("is_" ^ con), [], Syntax.max_pri)); |
45 Mixfix(escape ("is_" ^ con), [], Syntax.max_pri)); |
47 (* strictly speaking, these constants have one argument, |
46 (* strictly speaking, these constants have one argument, |
48 but the mixfix (without arguments) is introduced only |
47 but the mixfix (without arguments) is introduced only |
49 to generate parse rules for non-alphanumeric names*) |
48 to generate parse rules for non-alphanumeric names*) |
84 fun app s (l,r) = mk_appl (Constant s) [l,r]; |
83 fun app s (l,r) = mk_appl (Constant s) [l,r]; |
85 val cabs = app "_cabs"; |
84 val cabs = app "_cabs"; |
86 val capp = app "Rep_CFun"; |
85 val capp = app "Rep_CFun"; |
87 fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args); |
86 fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args); |
88 fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n); |
87 fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n); |
89 fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args); |
88 fun arg1 n (con,_,args) = List.foldr cabs (expvar n) (argvars n args); |
90 fun when1 n m = if n = m then arg1 n else K (Constant "UU"); |
89 fun when1 n m = if n = m then arg1 n else K (Constant "UU"); |
91 |
90 |
92 fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"]; |
91 fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"]; |
93 fun app_pat x = mk_appl (Constant "_pat") [x]; |
92 fun app_pat x = mk_appl (Constant "_pat") [x]; |
94 fun args_list [] = Constant "_noargs" |
93 fun args_list [] = Constant "_noargs" |