From 8eff703769b4ed115d71817d4c0c9628de5295a7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 13 Jul 2008 15:02:49 +0000 Subject: [PATCH] Procedural: we added the support for theorem flavours and we fixed the handling of unexpected proof constructions --- .../components/acic_procedural/acic2Procedural.ml | 5 +++-- .../components/acic_procedural/proceduralTypes.ml | 9 +++++---- .../components/acic_procedural/proceduralTypes.mli | 3 ++- 3 files changed, 10 insertions(+), 7 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index a6e0667b0..455f714af 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -393,8 +393,9 @@ and proc_appl st what hd tl = mk_preamble st what script and proc_other st what = + let _, dtext = test_depth st in let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in - let script = [T.Note text] in + let script = [T.Apply (what, dtext ^ text)] in mk_preamble st what script and proc_proof st t = @@ -456,7 +457,7 @@ let proc_obj st = function 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 (Some s, t, "") :: ast @ [T.Qed text] + else T.Theorem (`Theorem, Some s, t, "") :: ast @ [T.Qed text] | _ -> failwith "not a theorem" diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index 6534b8725..b0820f225 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -54,6 +54,7 @@ let list_init f i = (****************************************************************************) +type flavour = Cic.object_flavour type name = string option type hyp = string type what = Cic.annterm @@ -66,7 +67,7 @@ type inferred = Cic.annterm type pattern = Cic.annterm type step = Note of note - | Theorem of name * what * note + | Theorem of flavour * name * what * note | Qed of note | Id of note | Intros of count option * name list * note @@ -99,9 +100,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 name t = +let mk_theorem flavour name t = let name = match name with Some name -> name | None -> assert false in - let obj = N.Theorem (`Theorem, name, t, None) in + let obj = N.Theorem (flavour, name, t, None) in G.Executable (floc, G.Command (floc, G.Obj (floc, obj))) let mk_qed = @@ -182,7 +183,7 @@ let mk_vb = G.Shift floc let rec render_step sep a = function | Note s -> mk_notenote s a - | Theorem (n, t, s) -> mk_theorem n t :: mk_thnote 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 diff --git a/helm/software/components/acic_procedural/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli index c493873ff..68c4ce709 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.mli +++ b/helm/software/components/acic_procedural/proceduralTypes.mli @@ -33,6 +33,7 @@ val mk_arel: int -> string -> Cic.annterm (****************************************************************************) +type flavour = Cic.object_flavour type name = string option type hyp = string type what = Cic.annterm @@ -45,7 +46,7 @@ type inferred = Cic.annterm type pattern = Cic.annterm type step = Note of note - | Theorem of name * what * note + | Theorem of flavour * name * what * note | Qed of note | Id of note | Intros of count option * name list * note -- 2.39.2