List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars ||
List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars
+let is_definition pars =
+ List.mem (`Flavour `Definition) pars
+
let proc_obj st = function
- | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
+ | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
let ast = proc_proof st v in
let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
let text = Printf.sprintf "tactics: %u\nnodes: %u" steps nodes in
if st.skip_thm_and_qed then ast
- else T.Theorem (`Theorem, Some s, t, "") :: ast @ [T.Qed text]
- | _ ->
- failwith "not a theorem"
+ else T.Statement (`Theorem, Some s, t, None, "") :: ast @ [T.Qed text]
+ | C.AConstant (_, _, s, Some v, t, [], pars) when is_definition pars ->
+ [T.Statement (`Definition, Some s, t, Some v, "")]
+ | C.AConstant (_, _, s, None, t, [], pars) ->
+ [T.Statement (`Axiom, Some s, t, None, "")]
+ | _ ->
+ failwith "not a theorem, definition, axiom"
(* interface functions ******************************************************)
type where = (hyp * name) option
type inferred = Cic.annterm
type pattern = Cic.annterm
+type body = Cic.annterm option
type step = Note of note
- | Theorem of flavour * name * what * note
+ | Statement of flavour * name * what * body * note
| Qed of note
| Id of note
| Intros of count option * name list * note
let mk_thnote str a =
if str = "" then a else mk_note "" :: mk_note str :: a
-let mk_theorem flavour name t =
+let mk_statement flavour name t v =
let name = match name with Some name -> name | None -> assert false in
- let obj = N.Theorem (flavour, name, t, None) in
+ let obj = N.Theorem (flavour, name, t, v) in
G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
let mk_qed =
(* rendering ****************************************************************)
let rec render_step sep a = function
- | Note s -> mk_notenote s a
- | Theorem (f, n, t, s) -> mk_theorem f n t :: mk_thnote s a
- | Qed s -> mk_qed :: mk_tacnote s a
- | Id s -> mk_id sep :: mk_tacnote s a
- | Intros (c, ns, s) -> mk_intros c ns sep :: mk_tacnote s a
- | Cut (n, t, s) -> mk_cut n t sep :: mk_tacnote s a
- | LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a
- | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a
- | Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a
- | Apply (t, s) -> mk_apply t sep :: mk_tacnote s a
- | Change (t, _, w, e, s) -> mk_change t w e sep :: mk_tacnote s a
- | Clear (ns, s) -> mk_clear ns sep :: mk_tacnote s a
- | ClearBody (n, s) -> mk_clearbody n sep :: mk_tacnote s a
- | Branch ([], s) -> a
- | Branch ([ps], s) -> render_steps sep a ps
- | Branch (ps :: pss, s) ->
+ | Note s -> mk_notenote s a
+ | Statement (f, n, t, v, s) -> mk_statement f n t v :: mk_thnote s a
+ | Qed s -> mk_qed :: mk_tacnote s a
+ | Id s -> mk_id sep :: mk_tacnote s a
+ | Intros (c, ns, s) -> mk_intros c ns sep :: mk_tacnote s a
+ | Cut (n, t, s) -> mk_cut n t sep :: mk_tacnote s a
+ | LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a
+ | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a
+ | Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a
+ | Apply (t, s) -> mk_apply t sep :: mk_tacnote s a
+ | Change (t, _, w, e, s) -> mk_change t w e sep :: mk_tacnote s a
+ | Clear (ns, s) -> mk_clear ns sep :: mk_tacnote s a
+ | ClearBody (n, s) -> mk_clearbody n sep :: mk_tacnote s a
+ | Branch ([], s) -> a
+ | Branch ([ps], s) -> render_steps sep a ps
+ | Branch (ps :: pss, s) ->
let a = mk_ob :: mk_tacnote s a in
let a = List.fold_left (render_steps mk_vb) a (List.rev pss) in
mk_punctation sep :: render_steps mk_cb a ps
let rec count_step a = function
| Note _
- | Theorem _
+ | Statement _
| Qed _ -> a
| Branch (pps, _) -> List.fold_left count_steps a pps
| _ -> succ a
let rec count_node a = function
| Note _
- | Theorem _
+ | Statement _
| Qed _
| Id _
| Intros _
projects / helm.git / commitdiff