73 (string_of_int m)); |
73 (string_of_int m)); |
74 fun app s (l,r) = mk_appl (Constant s) [l,r]; |
74 fun app s (l,r) = mk_appl (Constant s) [l,r]; |
75 fun case1 n (con,mx,args) = mk_appl (Constant "_case1") |
75 fun case1 n (con,mx,args) = mk_appl (Constant "_case1") |
76 [Library.foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)), |
76 [Library.foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)), |
77 expvar n]; |
77 expvar n]; |
78 fun arg1 n (con,_,args) = if args = [] then expvar n |
78 fun cabs (x,t) = mk_appl (Constant "_cabs") [x,t]; |
79 else mk_appl (Constant "LAM ") |
79 fun arg1 n (con,_,args) = foldr cabs (expvar n) (mapn (argvar n) 1 args); |
80 [foldr1 (app "_idts") (mapn (argvar n) 1 args) , expvar n]; |
|
81 in |
80 in |
82 ParsePrintRule |
81 ParsePrintRule |
83 (mk_appl (Constant "_case_syntax") [Variable "x", foldr1 |
82 (mk_appl (Constant "_case_syntax") [Variable "x", foldr1 |
84 (fn (c,cs) => mk_appl (Constant"_case2") [c,cs]) |
83 (fn (c,cs) => mk_appl (Constant"_case2") [c,cs]) |
85 (mapn case1 1 cons')], |
84 (mapn case1 1 cons')], |