19 |
19 |
20 open DatatypeAux; |
20 open DatatypeAux; |
21 |
21 |
22 exception RecError of string; |
22 exception RecError of string; |
23 |
23 |
24 (* FIXME: move? *) |
|
25 |
|
26 fun dest_eq (Const ("Trueprop", _) $ (Const ("op =", _) $ lhs $ rhs)) = (lhs, rhs) |
|
27 | dest_eq t = raise TERM ("dest_eq", [t]) |
|
28 |
|
29 fun dest_Type (Type x) = x |
|
30 | dest_Type T = raise TYPE ("dest_Type", [T], []); |
|
31 |
|
32 fun primrec_err s = error ("Primrec definition error:\n" ^ s); |
24 fun primrec_err s = error ("Primrec definition error:\n" ^ s); |
33 fun primrec_eq_err sign s eq = |
25 fun primrec_eq_err sign s eq = |
34 primrec_err (s ^ "\nin equation\n" ^ Sign.string_of_term sign eq); |
26 primrec_err (s ^ "\nin equation\n" ^ Sign.string_of_term sign eq); |
35 |
27 |
36 (* preprocessing of equations *) |
28 (* preprocessing of equations *) |
37 |
29 |
38 fun process_eqn sign (eq, rec_fns) = |
30 fun process_eqn sign (eq, rec_fns) = |
39 let |
31 let |
40 val (lhs, rhs) = if null (term_vars eq) then |
32 val (lhs, rhs) = |
41 dest_eq eq handle _ => raise RecError "not a proper equation" |
33 if null (term_vars eq) then |
42 else raise RecError "illegal schematic variable(s)"; |
34 HOLogic.dest_eq (HOLogic.dest_Trueprop eq) |
|
35 handle _ => raise RecError "not a proper equation" |
|
36 else raise RecError "illegal schematic variable(s)"; |
43 |
37 |
44 val (recfun, args) = strip_comb lhs; |
38 val (recfun, args) = strip_comb lhs; |
45 val (fname, _) = dest_Const recfun handle _ => |
39 val (fname, _) = dest_Const recfun handle _ => |
46 raise RecError "function is not declared as constant in theory"; |
40 raise RecError "function is not declared as constant in theory"; |
47 |
41 |