69 (* strictly speaking, these constants have one argument, |
69 (* strictly speaking, these constants have one argument, |
70 but the mixfix (without arguments) is introduced only |
70 but the mixfix (without arguments) is introduced only |
71 to generate parse rules for non-alphanumeric names*) |
71 to generate parse rules for non-alphanumeric names*) |
72 fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in |
72 fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in |
73 if tvar mem typevars then freetvar ("t"^s) n else tvar end; |
73 if tvar mem typevars then freetvar ("t"^s) n else tvar end; |
74 fun mk_matT (a,bs,c) = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c; |
74 fun mk_matT (a,bs,c) = a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c; |
75 fun mat (con,args,mx) = (mat_name_ con, |
75 fun mat (con,args,mx) = (mat_name_ con, |
76 mk_matT(dtype, map third args, freetvar "t" 1), |
76 mk_matT(dtype, map third args, freetvar "t" 1), |
77 Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri)); |
77 Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri)); |
78 fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel; |
78 fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel; |
79 fun sel (con,args,mx) = map_filter sel1 args; |
79 fun sel (con,args,mx) = map_filter sel1 args; |