62 map dest_Free cargs', |
62 map dest_Free cargs', |
63 map dest_Free rs') |
63 map dest_Free rs') |
64 handle TERM _ => raise RecError "illegal argument in pattern"; |
64 handle TERM _ => raise RecError "illegal argument in pattern"; |
65 val lfrees = ls @ rs @ cargs; |
65 val lfrees = ls @ rs @ cargs; |
66 |
66 |
67 val _ = case duplicates lfrees of |
67 fun check_vars _ [] = () |
68 [] => () |
68 | check_vars s vars = raise RecError (s ^ commas_quote (map fst vars)) |
69 | vars => raise RecError("repeated variable names in pattern: " ^ |
|
70 commas_quote (map #1 vars)) |
|
71 |
|
72 val _ = case (map dest_Free (term_frees rhs)) \\ lfrees of |
|
73 [] => () |
|
74 | vars => raise RecError |
|
75 ("extra variables on rhs: " ^ |
|
76 commas_quote (map #1 vars)) |
|
77 in |
69 in |
78 if length middle > 1 then |
70 if length middle > 1 then |
79 raise RecError "more than one non-variable in pattern" |
71 raise RecError "more than one non-variable in pattern" |
80 else (case assoc (rec_fns, fname) of |
72 else |
|
73 (check_vars "repeated variable names in pattern: " (duplicates lfrees); |
|
74 check_vars "extra variables on rhs: " |
|
75 (map dest_Free (term_frees rhs) \\ lfrees); |
|
76 case assoc (rec_fns, fname) of |
81 None => |
77 None => |
82 (fname, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns |
78 (fname, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns |
83 | Some (_, rpos', eqns) => |
79 | Some (_, rpos', eqns) => |
84 if is_some (assoc (eqns, cname)) then |
80 if is_some (assoc (eqns, cname)) then |
85 raise RecError "constructor already occurred as pattern" |
81 raise RecError "constructor already occurred as pattern" |