48 fun %%: s = Const(s,dummyT); |
48 fun %%: s = Const(s,dummyT); |
49 infix 0 ==; fun S == T = %%:"==" $ S $ T; |
49 infix 0 ==; fun S == T = %%:"==" $ S $ T; |
50 infix 1 ===; fun S === T = %%:"op =" $ S $ T; |
50 infix 1 ===; fun S === T = %%:"op =" $ S $ T; |
51 infix 9 ` ; fun f ` x = %%:"Cfun.Rep_CFun" $ f $ x; |
51 infix 9 ` ; fun f ` x = %%:"Cfun.Rep_CFun" $ f $ x; |
52 |
52 |
53 (* infers the type of a term *) |
53 (* infers the type of a term *) (* FIXME better avoid this low-level stuff *) |
54 (* similar to Theory.inferT_axm, but allows any type, not just propT *) |
54 (* similar to Theory.inferT_axm, but allows any type, not just propT *) |
55 fun infer sg t = |
55 fun infer sg t = |
56 fst (Sign.infer_types (Sign.pp sg) sg (K NONE) (K NONE) [] true ([t],dummyT)); |
56 fst (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) [] true |
57 |
57 ([t],dummyT)); |
58 (* Similar to Term.lambda, but also allows abstraction over constants *) |
|
59 fun lambda' (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t)) |
|
60 | lambda' (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t)) |
|
61 | lambda' (v as Const (x, T)) t = Abs (Sign.base_name x, T, abstract_over (v, t)) |
|
62 | lambda' v t = raise TERM ("lambda'", [v, t]); |
|
63 |
58 |
64 (* builds the expression (LAM v. rhs) *) |
59 (* builds the expression (LAM v. rhs) *) |
65 fun big_lambda v rhs = %%:"Cfun.Abs_CFun"$(lambda' v rhs); |
60 fun big_lambda v rhs = %%:"Cfun.Abs_CFun"$(Term.lambda v rhs); |
66 |
61 |
67 (* builds the expression (LAM v1 v2 .. vn. rhs) *) |
62 (* builds the expression (LAM v1 v2 .. vn. rhs) *) |
68 fun big_lambdas [] rhs = rhs |
63 fun big_lambdas [] rhs = rhs |
69 | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs); |
64 | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs); |
70 |
65 |