22 in |
22 in |
23 ((rhs, thm), lthy') |
23 ((rhs, thm), lthy') |
24 end |
24 end |
25 |
25 |
26 |
26 |
27 (** interface and syntax setup **) |
27 (** Interface and Syntax Setup **) |
28 |
28 |
29 (* the ML-interface takes |
29 (* The ML-interface for a quotient definition takes |
|
30 as argument: |
30 |
31 |
31 - the mixfix annotation |
32 - the mixfix annotation |
32 - name and attributes |
33 - name and attributes |
33 - the new constant as term |
34 - the new constant as term |
34 - the rhs of the definition as term |
35 - the rhs of the definition as term |
35 |
36 |
36 it returns the defined constant and its definition |
37 It returns the defined constant and its definition |
37 theorem; stores the data in the qconsts slot |
38 theorem; stores the data in the qconsts data slot. |
|
39 |
|
40 Restriction: At the moment the right-hand side must |
|
41 be a terms composed of constant. Similarly the |
|
42 left-hand side must be a single constant. |
38 *) |
43 *) |
39 fun quotient_def mx attr lhs rhs lthy = |
44 fun quotient_def mx attr lhs rhs lthy = |
40 let |
45 let |
41 val (lhs_str, lhs_ty) = |
46 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
42 dest_Free lhs |
47 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
43 handle TERM _ => error "The name for the new constant has to be a Free; check that it is not defined yet." |
48 |
44 val qconst_bname = Binding.name lhs_str; |
49 val qconst_bname = Binding.name lhs_str |
45 val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs |
50 val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs |
46 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
51 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
47 val (_, prop') = LocalDefs.cert_def lthy prop |
52 val (_, prop') = LocalDefs.cert_def lthy prop |
48 val (_, newrhs) = Primitive_Defs.abs_def prop' |
53 val (_, newrhs) = Primitive_Defs.abs_def prop' |
49 |
54 |
60 |
65 |
61 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy = |
66 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy = |
62 let |
67 let |
63 val lhs = Syntax.read_term lthy lhs_str |
68 val lhs = Syntax.read_term lthy lhs_str |
64 val rhs = Syntax.read_term lthy rhs_str |
69 val rhs = Syntax.read_term lthy rhs_str |
|
70 (* FIXME: Relating the reads will cause errors. *) |
65 in |
71 in |
66 quotient_def mx attr lhs rhs lthy |> snd |
72 quotient_def mx attr lhs rhs lthy |> snd |
67 end |
73 end |
68 |
74 |
69 val _ = OuterKeyword.keyword "as"; |
75 val _ = OuterKeyword.keyword "as"; |