23 text %mlref {* |
23 text %mlref {* |
24 \begin{mldecls} |
24 \begin{mldecls} |
25 @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\ |
25 @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\ |
26 @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\ |
26 @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\ |
27 @{index_ML Code.add_eqnl: "string * (thm * bool) list lazy -> theory -> theory"} \\ |
27 @{index_ML Code.add_eqnl: "string * (thm * bool) list lazy -> theory -> theory"} \\ |
28 @{index_ML Code.map_pre: "(simpset -> simpset) -> theory -> theory"} \\ |
28 @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\ |
29 @{index_ML Code.map_post: "(simpset -> simpset) -> theory -> theory"} \\ |
29 @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\ |
30 @{index_ML Code.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option) |
30 @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option) |
31 -> theory -> theory"} \\ |
31 -> theory -> theory"} \\ |
32 @{index_ML Code.del_functrans: "string -> theory -> theory"} \\ |
32 @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\ |
33 @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ |
33 @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ |
34 @{index_ML Code.get_datatype: "theory -> string |
34 @{index_ML Code.get_datatype: "theory -> string |
35 -> (string * sort) list * (string * typ list) list"} \\ |
35 -> (string * sort) list * (string * typ list) list"} \\ |
36 @{index_ML Code.get_datatype_of_constr: "theory -> string -> string option"} |
36 @{index_ML Code.get_datatype_of_constr: "theory -> string -> string option"} |
37 \end{mldecls} |
37 \end{mldecls} |
46 |
46 |
47 \item @{ML Code.add_eqnl}~@{text "(const, lthms)"}~@{text "thy"} adds |
47 \item @{ML Code.add_eqnl}~@{text "(const, lthms)"}~@{text "thy"} adds |
48 suspended code equations @{text lthms} for constant |
48 suspended code equations @{text lthms} for constant |
49 @{text const} to executable content. |
49 @{text const} to executable content. |
50 |
50 |
51 \item @{ML Code.map_pre}~@{text "f"}~@{text "thy"} changes |
51 \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes |
52 the preprocessor simpset. |
52 the preprocessor simpset. |
53 |
53 |
54 \item @{ML Code.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds |
54 \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds |
55 function transformer @{text f} (named @{text name}) to executable content; |
55 function transformer @{text f} (named @{text name}) to executable content; |
56 @{text f} is a transformer of the code equations belonging |
56 @{text f} is a transformer of the code equations belonging |
57 to a certain function definition, depending on the |
57 to a certain function definition, depending on the |
58 current theory context. Returning @{text NONE} indicates that no |
58 current theory context. Returning @{text NONE} indicates that no |
59 transformation took place; otherwise, the whole process will be iterated |
59 transformation took place; otherwise, the whole process will be iterated |
60 with the new code equations. |
60 with the new code equations. |
61 |
61 |
62 \item @{ML Code.del_functrans}~@{text "name"}~@{text "thy"} removes |
62 \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes |
63 function transformer named @{text name} from executable content. |
63 function transformer named @{text name} from executable content. |
64 |
64 |
65 \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds |
65 \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds |
66 a datatype to executable content, with generation |
66 a datatype to executable content, with generation |
67 set @{text cs}. |
67 set @{text cs}. |
77 subsection {* Auxiliary *} |
77 subsection {* Auxiliary *} |
78 |
78 |
79 text %mlref {* |
79 text %mlref {* |
80 \begin{mldecls} |
80 \begin{mldecls} |
81 @{index_ML Code_Unit.read_const: "theory -> string -> string"} \\ |
81 @{index_ML Code_Unit.read_const: "theory -> string -> string"} \\ |
82 @{index_ML Code_Unit.head_eqn: "theory -> thm -> string * ((string * sort) list * typ)"} \\ |
|
83 @{index_ML Code_Unit.rewrite_eqn: "simpset -> thm -> thm"} \\ |
82 @{index_ML Code_Unit.rewrite_eqn: "simpset -> thm -> thm"} \\ |
84 \end{mldecls} |
83 \end{mldecls} |
85 |
84 |
86 \begin{description} |
85 \begin{description} |
87 |
86 |
88 \item @{ML Code_Unit.read_const}~@{text thy}~@{text s} |
87 \item @{ML Code_Unit.read_const}~@{text thy}~@{text s} |
89 reads a constant as a concrete term expression @{text s}. |
88 reads a constant as a concrete term expression @{text s}. |
90 |
|
91 \item @{ML Code_Unit.head_eqn}~@{text thy}~@{text thm} |
|
92 extracts the constant and its type from a code equation @{text thm}. |
|
93 |
89 |
94 \item @{ML Code_Unit.rewrite_eqn}~@{text ss}~@{text thm} |
90 \item @{ML Code_Unit.rewrite_eqn}~@{text ss}~@{text thm} |
95 rewrites a code equation @{text thm} with a simpset @{text ss}; |
91 rewrites a code equation @{text thm} with a simpset @{text ss}; |
96 only arguments and right hand side are rewritten, |
92 only arguments and right hand side are rewritten, |
97 not the head of the code equation. |
93 not the head of the code equation. |