From 70660e05baa914569c52555230901d5a8dd92f0b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 5 May 2009 18:57:21 +0000 Subject: [PATCH] - Procedural: new flag "level=n" to control the reconstruction level (defaults to maximum level available). Level 1 reconstruction activated. --- .../components/acic_procedural/.depend | 11 ++- .../components/acic_procedural/.depend.opt | 11 ++- .../components/acic_procedural/Makefile | 1 + .../acic_procedural/acic2Procedural.ml | 81 +++++++++++++++++-- .../components/acic_procedural/procedural1.ml | 51 ++++++++++++ .../acic_procedural/procedural1.mli | 34 ++++++++ .../components/acic_procedural/procedural2.ml | 52 +----------- .../acic_procedural/procedural2.mli | 3 - .../acic_procedural/proceduralHelpers.ml | 7 ++ .../acic_procedural/proceduralHelpers.mli | 3 + .../software/components/grafite/grafiteAst.ml | 5 +- .../components/grafite/grafiteAstPp.ml | 3 +- .../grafite_parser/grafiteParser.ml | 5 +- 13 files changed, 195 insertions(+), 72 deletions(-) create mode 100644 helm/software/components/acic_procedural/procedural1.ml create mode 100644 helm/software/components/acic_procedural/procedural1.mli diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend index 189d36ff1..fde9f7d63 100644 --- a/helm/software/components/acic_procedural/.depend +++ b/helm/software/components/acic_procedural/.depend @@ -1,3 +1,4 @@ +procedural1.cmi: proceduralTypes.cmi procedural2.cmi: proceduralTypes.cmi proceduralTeX.cmi: proceduralTypes.cmi proceduralHelpers.cmo: proceduralHelpers.cmi @@ -14,6 +15,8 @@ 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: procedural1.cmi +procedural1.cmx: procedural1.cmi procedural2.cmo: proceduralTypes.cmi proceduralHelpers.cmi \ proceduralConversion.cmi proceduralClassify.cmi procedural2.cmi procedural2.cmx: proceduralTypes.cmx proceduralHelpers.cmx \ @@ -22,7 +25,7 @@ proceduralTeX.cmo: proceduralTypes.cmi proceduralHelpers.cmi \ proceduralTeX.cmi proceduralTeX.cmx: proceduralTypes.cmx proceduralHelpers.cmx \ proceduralTeX.cmi -acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi procedural2.cmi \ - acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx procedural2.cmx \ - acic2Procedural.cmi +acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi \ + proceduralHelpers.cmi procedural2.cmi procedural1.cmi acic2Procedural.cmi +acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx \ + proceduralHelpers.cmx procedural2.cmx procedural1.cmx acic2Procedural.cmi diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt index 189d36ff1..fde9f7d63 100644 --- a/helm/software/components/acic_procedural/.depend.opt +++ b/helm/software/components/acic_procedural/.depend.opt @@ -1,3 +1,4 @@ +procedural1.cmi: proceduralTypes.cmi procedural2.cmi: proceduralTypes.cmi proceduralTeX.cmi: proceduralTypes.cmi proceduralHelpers.cmo: proceduralHelpers.cmi @@ -14,6 +15,8 @@ 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: procedural1.cmi +procedural1.cmx: procedural1.cmi procedural2.cmo: proceduralTypes.cmi proceduralHelpers.cmi \ proceduralConversion.cmi proceduralClassify.cmi procedural2.cmi procedural2.cmx: proceduralTypes.cmx proceduralHelpers.cmx \ @@ -22,7 +25,7 @@ proceduralTeX.cmo: proceduralTypes.cmi proceduralHelpers.cmi \ proceduralTeX.cmi proceduralTeX.cmx: proceduralTypes.cmx proceduralHelpers.cmx \ proceduralTeX.cmi -acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi procedural2.cmi \ - acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx procedural2.cmx \ - acic2Procedural.cmi +acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi \ + proceduralHelpers.cmi procedural2.cmi procedural1.cmi acic2Procedural.cmi +acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx \ + proceduralHelpers.cmx procedural2.cmx procedural1.cmx acic2Procedural.cmi diff --git a/helm/software/components/acic_procedural/Makefile b/helm/software/components/acic_procedural/Makefile index 5acd1d21d..ce878a21b 100644 --- a/helm/software/components/acic_procedural/Makefile +++ b/helm/software/components/acic_procedural/Makefile @@ -8,6 +8,7 @@ INTERFACE_FILES = \ proceduralTypes.mli \ proceduralMode.mli \ proceduralConversion.mli \ + procedural1.mli \ procedural2.mli \ proceduralTeX.mli \ acic2Procedural.mli \ diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index c8168aa47..4ce01707c 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -23,22 +23,91 @@ * http://cs.unibo.it/helm/. *) -module L = Librarian +module C = Cic +module L = Librarian +module G = GrafiteAst +module H = ProceduralHelpers module T = ProceduralTypes +module P1 = Procedural1 module P2 = Procedural2 module X = ProceduralTeX let tex_formatter = ref None +(* object costruction *******************************************************) + +let th_flavours = [`Theorem; `Lemma; `Remark; `Fact] + +let def_flavours = [`Definition; `Variant] + +let get_flavour sorts params context v attrs = + let rec aux = function + | [] -> + if H.is_acic_proof sorts context v then List.hd th_flavours + else List.hd def_flavours + | `Flavour fl :: _ -> fl + | _ :: tl -> aux tl + in + let flavour_map x y = match x, y with + | None, G.IPAs flavour -> Some flavour + | _ -> x + in + match List.fold_left flavour_map None params with + | Some fl -> fl + | None -> aux attrs + +let proc_obj ?(info="") proc_proof sorts params context = function + | C.AConstant (_, _, s, Some v, t, [], attrs) -> + begin match get_flavour sorts params context v attrs with + | flavour when List.mem flavour th_flavours -> + let ast = proc_proof v in + let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in + let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s" + "COMMENTS" info "Tactics" steps "Final nodes" nodes "END" + in + T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text] + | flavour when List.mem flavour def_flavours -> + [T.Statement (flavour, Some s, t, Some v, "")] + | _ -> + failwith "not a theorem, definition, axiom or inductive type" + end + | C.AConstant (_, _, s, None, t, [], attrs) -> + [T.Statement (`Axiom, Some s, t, None, "")] + | C.AInductiveDefinition (_, types, [], lpsno, attrs) -> + [T.Inductive (types, lpsno, "")] + | _ -> + failwith "not a theorem, definition, axiom or inductive type" + (* interface functions ******************************************************) +let get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params context = + let level_map x y = match x, y with + | None, G.IPLevel level -> Some level + | _ -> x + in + match List.fold_left level_map None params with + | None + | Some 2 -> + P2.proc_proof + (P2.init ~ids_to_inner_sorts ~ids_to_inner_types params context) + | Some 1 -> + P1.proc_proof + (P1.init ~ids_to_inner_sorts ~ids_to_inner_types params context) + | Some n -> + failwith ( + "Procedural reconstruction level not supported: " ^ + string_of_int n + ) + let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?info params anobj = - let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types params [] in + let proc_proof = + get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params [] + in L.time_stamp "P : LEVEL 2 "; HLog.debug "Procedural: level 2 transformation"; - let steps = P2.proc_obj st ?info anobj in + let steps = proc_obj ?info proc_proof ids_to_inner_sorts params [] anobj in let _ = match !tex_formatter with | None -> () | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps @@ -50,9 +119,11 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params context annterm = - let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types params context in + let proc_proof = + get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params context + in HLog.debug "Procedural: level 2 transformation"; - let steps = P2.proc_proof st annterm in + let steps = proc_proof annterm in let _ = match !tex_formatter with | None -> () | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps diff --git a/helm/software/components/acic_procedural/procedural1.ml b/helm/software/components/acic_procedural/procedural1.ml new file mode 100644 index 000000000..550dd07e6 --- /dev/null +++ b/helm/software/components/acic_procedural/procedural1.ml @@ -0,0 +1,51 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module C = Cic +module A = Cic2acic +module G = GrafiteAst + +module T = ProceduralTypes + +type status = { + sorts : (C.id, A.sort_kind) Hashtbl.t; + types : (C.id, A.anntypes) Hashtbl.t; + params : G.inline_param list; + context : C.context +} + +(* interface functions ******************************************************) + +let proc_proof st what = + let dtext = "" in + [T.Exact (what, dtext)] + +let init ~ids_to_inner_sorts ~ids_to_inner_types params context = + { + sorts = ids_to_inner_sorts; + types = ids_to_inner_types; + params = params; + context = context + } diff --git a/helm/software/components/acic_procedural/procedural1.mli b/helm/software/components/acic_procedural/procedural1.mli new file mode 100644 index 000000000..83de9d420 --- /dev/null +++ b/helm/software/components/acic_procedural/procedural1.mli @@ -0,0 +1,34 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type status + +val init: + ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> + ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> + GrafiteAst.inline_param list-> Cic.context -> status + +val proc_proof: + status -> Cic.annterm -> ProceduralTypes.step list diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index 958fc4abb..ed30f767b 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -140,15 +140,6 @@ try with Not_found -> None with Invalid_argument _ -> failwith "A2P.get_inner_types" -let is_proof st v = -try - let id = Ut.id_of_annterm v in - 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 @@ -458,48 +449,7 @@ try with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s) -(* object costruction *******************************************************) - -let th_flavours = [`Theorem; `Lemma; `Remark; `Fact] - -let def_flavours = [`Definition; `Variant] - -let get_flavour st v attrs = - let rec aux = function - | [] -> - if is_proof st v then List.hd th_flavours else List.hd def_flavours - | `Flavour fl :: _ -> fl - | _ :: tl -> aux tl - in - let flavour_map x y = match x, y with - | None, G.IPAs flavour -> Some flavour - | _ -> x - in - match List.fold_left flavour_map None st.params with - | Some fl -> fl - | None -> aux attrs - -let proc_obj ?(info="") st = function - | C.AConstant (_, _, s, Some v, t, [], attrs) -> - begin match get_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 - let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s" - "COMMENTS" info "Tactics" steps "Final nodes" nodes "END" - in - T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text] - | flavour when List.mem flavour def_flavours -> - [T.Statement (flavour, Some s, t, Some v, "")] - | _ -> - failwith "not a theorem, definition, axiom or inductive type" - end - | C.AConstant (_, _, s, None, t, [], attrs) -> - [T.Statement (`Axiom, Some s, t, None, "")] - | C.AInductiveDefinition (_, types, [], lpsno, attrs) -> - [T.Inductive (types, lpsno, "")] - | _ -> - failwith "not a theorem, definition, axiom or inductive type" +(* initialization ***********************************************************) let init ~ids_to_inner_sorts ~ids_to_inner_types params context = let depth_map x y = match x, y with diff --git a/helm/software/components/acic_procedural/procedural2.mli b/helm/software/components/acic_procedural/procedural2.mli index 71cbe4253..7abfb6f1c 100644 --- a/helm/software/components/acic_procedural/procedural2.mli +++ b/helm/software/components/acic_procedural/procedural2.mli @@ -33,7 +33,4 @@ val init: val proc_proof: status -> Cic.annterm -> ProceduralTypes.step list -val proc_obj: - ?info:string -> status -> Cic.annobj -> ProceduralTypes.step list - val debug: bool ref diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index 3628e5944..b2f73f311 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -335,3 +335,10 @@ let acic_bc c t = | t -> t in bc c t + +let is_acic_proof sorts context v = + let id = Ut.id_of_annterm v in + try match Hashtbl.find sorts id with + | `Prop -> true + | _ -> false + with Not_found -> is_proof context (cic v) diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index 358012c87..203224371 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/components/acic_procedural/proceduralHelpers.mli @@ -71,3 +71,6 @@ val cic_bc: Cic.context -> Cic.term -> Cic.term val acic_bc: Cic.context -> Cic.annterm -> Cic.annterm +val is_acic_proof: + (Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.context -> Cic.annterm -> + bool diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 4006320be..039d5bfa4 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -148,10 +148,11 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ] type print_kind = [ `Env | `Coer ] type inline_param = IPPrefix of string - | IPProcedural - | IPDepth of int | IPAs of Cic.object_flavour + | IPProcedural | IPNoDefaults + | IPLevel of int + | IPDepth of int type ('term,'lazy_term) macro = (* Whelp's stuff *) diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index ce7fdcfdf..6806713a4 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -282,8 +282,9 @@ let pp_macro ~term_pp ~lazy_term_pp = | IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\"" | IPAs flavour -> flavour_pp flavour | IPProcedural -> "procedural" - | IPDepth depth -> "depth = " ^ string_of_int depth | IPNoDefaults -> "nodefaults" + | IPDepth depth -> "depth = " ^ string_of_int depth + | IPLevel level -> "level = " ^ string_of_int level in let s = String.concat " " (List.map pp_param l) in if s = "" then s else " " ^ s diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index e2ab011da..ecdee9f7b 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -453,10 +453,11 @@ EXTEND inline_params:[ [ params = LIST0 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix - | IDENT "procedural" -> G.IPProcedural | flavour = inline_flavour -> G.IPAs flavour - | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth + | IDENT "procedural" -> G.IPProcedural | IDENT "nodefaults" -> G.IPNoDefaults + | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth + | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level ] -> params ] ]; -- 2.39.2