From: Ferruccio Guidi Date: Wed, 11 Mar 2009 13:43:20 +0000 (+0000) Subject: bug fix + better obj flavour guessing via inner sorts X-Git-Tag: make_still_working~4156 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cb75149567a9a21206760211eeefcd5f26321bcb;p=helm.git bug fix + better obj flavour guessing via inner sorts --- 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