From 876ac1889f8b11c97c8d94a0523504a0bcb70ddd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 14 Jul 2008 11:57:42 +0000 Subject: [PATCH] Procedural: we added the support for rendering definitions and axioms --- .../acic_procedural/acic2Procedural.ml | 15 +++++-- .../acic_procedural/proceduralTypes.ml | 43 ++++++++++--------- .../acic_procedural/proceduralTypes.mli | 3 +- 3 files changed, 35 insertions(+), 26 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 455f714af..298259cb5 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -451,15 +451,22 @@ let is_theorem pars = 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 ******************************************************) diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index b0820f225..d505a8b15 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -65,9 +65,10 @@ type note = string 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 @@ -100,9 +101,9 @@ let mk_notenote str a = 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 = @@ -182,22 +183,22 @@ let mk_vb = G.Shift floc (* 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 @@ -218,7 +219,7 @@ let render_steps a = render_steps mk_dot a let rec count_step a = function | Note _ - | Theorem _ + | Statement _ | Qed _ -> a | Branch (pps, _) -> List.fold_left count_steps a pps | _ -> succ a @@ -227,7 +228,7 @@ and count_steps a = List.fold_left count_step a let rec count_node a = function | Note _ - | Theorem _ + | Statement _ | Qed _ | Id _ | Intros _ diff --git a/helm/software/components/acic_procedural/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli index 68c4ce709..b750688a6 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.mli +++ b/helm/software/components/acic_procedural/proceduralTypes.mli @@ -44,9 +44,10 @@ type note = string 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 -- 2.39.2