From cb75149567a9a21206760211eeefcd5f26321bcb Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 11 Mar 2009 13:43:20 +0000
Subject: [PATCH] bug fix + better obj flavour guessing via inner sorts

---
 .../components/acic_procedural/.depend        |  4 ++--
 .../components/acic_procedural/.depend.opt    |  4 ++--
 .../components/acic_procedural/procedural1.ml | 22 ++++++++++---------
 3 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend
index 96306b2e6..122ed1938 100644
--- a/helm/software/components/acic_procedural/.depend
+++ b/helm/software/components/acic_procedural/.depend
@@ -14,9 +14,9 @@ proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi
 proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
 proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi 
 proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi 
-procedural1.cmo: proceduralTypes.cmi proceduralTeX.cmi proceduralHelpers.cmi \
+procedural1.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
     proceduralConversion.cmi proceduralClassify.cmi procedural1.cmi 
-procedural1.cmx: proceduralTypes.cmx proceduralTeX.cmx proceduralHelpers.cmx \
+procedural1.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
     proceduralConversion.cmx proceduralClassify.cmx procedural1.cmi 
 proceduralTeX.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
     proceduralTeX.cmi 
diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt
index 96306b2e6..122ed1938 100644
--- a/helm/software/components/acic_procedural/.depend.opt
+++ b/helm/software/components/acic_procedural/.depend.opt
@@ -14,9 +14,9 @@ proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi
 proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
 proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi 
 proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi 
-procedural1.cmo: proceduralTypes.cmi proceduralTeX.cmi proceduralHelpers.cmi \
+procedural1.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
     proceduralConversion.cmi proceduralClassify.cmi procedural1.cmi 
-procedural1.cmx: proceduralTypes.cmx proceduralTeX.cmx proceduralHelpers.cmx \
+procedural1.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
     proceduralConversion.cmx proceduralClassify.cmx procedural1.cmi 
 proceduralTeX.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
     proceduralTeX.cmi 
diff --git a/helm/software/components/acic_procedural/procedural1.ml b/helm/software/components/acic_procedural/procedural1.ml
index b3e112850..4b9127002 100644
--- a/helm/software/components/acic_procedural/procedural1.ml
+++ b/helm/software/components/acic_procedural/procedural1.ml
@@ -45,7 +45,6 @@ module Cl   = ProceduralClassify
 module T    = ProceduralTypes
 module Cn   = ProceduralConversion
 module H    = ProceduralHelpers
-module X    = ProceduralTeX
 
 type status = {
    sorts : (C.id, A.sort_kind) Hashtbl.t;
@@ -140,14 +139,16 @@ try
       | {A.annsynthesized = st; A.annexpected = None}    -> Some (st, st)
    with Not_found -> None
 with Invalid_argument _ -> failwith "A2P.get_inner_types"
-(*
-let get_inner_sort st v =
+
+let is_proof st v =
 try
    let id = Ut.id_of_annterm v in
-   try Hashtbl.find st.sorts id
-   with Not_found -> `Type (CicUniv.fresh())
-with Invalid_argument _ -> failwith "A2P.get_sort"
-*)
+   try match Hashtbl.find st.sorts id with
+      | `Prop -> true
+      | _     -> false
+   with Not_found -> H.is_proof st.context (H.cic v)
+with Invalid_argument _ -> failwith "P1.is_proof"
+
 let get_entry st id =
    let rec aux = function
       | []                                        -> assert false
@@ -472,9 +473,10 @@ let th_flavours = [`Theorem; `Lemma; `Remark; `Fact]
 
 let def_flavours = [`Definition]
 
-let get_flavour ?flavour attrs =
+let get_flavour ?flavour st v attrs =
    let rec aux = function
-      | []               -> List.hd th_flavours
+      | []               -> 
+         if is_proof st v then List.hd th_flavours else List.hd def_flavours
       | `Flavour fl :: _ -> fl
       | _ :: tl          -> aux tl
    in
@@ -484,7 +486,7 @@ let get_flavour ?flavour attrs =
 
 let proc_obj ?flavour ?(info="") st = function
    | C.AConstant (_, _, s, Some v, t, [], attrs)         ->
-      begin match get_flavour ?flavour attrs with
+      begin match get_flavour ?flavour st v attrs with
          | flavour when List.mem flavour th_flavours  ->
             let ast = proc_proof st v in
             let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
-- 
2.39.2