From: Ferruccio Guidi Date: Tue, 6 Feb 2007 19:36:05 +0000 (+0000) Subject: - Procedural: moved in a directory on its own X-Git-Tag: 0.4.95@7852~624 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68d46ac40a575f3fce5958fb2776b38739703951;p=helm.git - Procedural: moved in a directory on its own - ApplyTransofrmation: now handles inline macro expansion - GrafiteParser MatitaEngine MatitacLib: added a callback in each - tests/letrecand.ma: changed baseuri --- diff --git a/components/METAS/meta.helm-acic_procedural.src b/components/METAS/meta.helm-acic_procedural.src new file mode 100644 index 000000000..e91f1f7d8 --- /dev/null +++ b/components/METAS/meta.helm-acic_procedural.src @@ -0,0 +1,4 @@ +requires="helm-cic_proof_checking helm-acic_content helm-grafite" +version="0.0.1" +archive(byte)="acic_procedural.cma" +archive(native)="acic_procedural.cmxa" diff --git a/components/Makefile b/components/Makefile index a700970af..9f42d0dad 100644 --- a/components/Makefile +++ b/components/Makefile @@ -24,6 +24,7 @@ MODULES = \ library \ acic_content \ grafite \ + acic_procedural \ content_pres \ cic_unification \ whelp \ diff --git a/components/acic_procedural/.depend b/components/acic_procedural/.depend new file mode 100644 index 000000000..5f1cd6590 --- /dev/null +++ b/components/acic_procedural/.depend @@ -0,0 +1,10 @@ +cicClassify.cmo: cicClassify.cmi +cicClassify.cmx: cicClassify.cmi +proceduralConversion.cmo: proceduralConversion.cmi +proceduralConversion.cmx: proceduralConversion.cmi +proceduralTypes.cmo: proceduralTypes.cmi +proceduralTypes.cmx: proceduralTypes.cmi +acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \ + cicClassify.cmi acic2Procedural.cmi +acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \ + cicClassify.cmx acic2Procedural.cmi diff --git a/components/acic_procedural/.depend.opt b/components/acic_procedural/.depend.opt new file mode 100644 index 000000000..5f1cd6590 --- /dev/null +++ b/components/acic_procedural/.depend.opt @@ -0,0 +1,10 @@ +cicClassify.cmo: cicClassify.cmi +cicClassify.cmx: cicClassify.cmi +proceduralConversion.cmo: proceduralConversion.cmi +proceduralConversion.cmx: proceduralConversion.cmi +proceduralTypes.cmo: proceduralTypes.cmi +proceduralTypes.cmx: proceduralTypes.cmi +acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \ + cicClassify.cmi acic2Procedural.cmi +acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \ + cicClassify.cmx acic2Procedural.cmi diff --git a/components/acic_procedural/Makefile b/components/acic_procedural/Makefile new file mode 100644 index 000000000..3435f01d0 --- /dev/null +++ b/components/acic_procedural/Makefile @@ -0,0 +1,14 @@ +PACKAGE = acic_procedural +PREDICATES = + +INTERFACE_FILES = \ + cicClassify.mli \ + proceduralConversion.mli \ + proceduralTypes.mli \ + acic2Procedural.mli \ + $(NULL) +IMPLEMENTATION_FILES = \ + $(INTERFACE_FILES:%.mli=%.ml) + +include ../../Makefile.defs +include ../Makefile.common diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml new file mode 100644 index 000000000..adfe4b05c --- /dev/null +++ b/components/acic_procedural/acic2Procedural.ml @@ -0,0 +1,348 @@ +(* 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 D = Deannotate +module DTI = DoubleTypeInference +module TC = CicTypeChecker +module Un = CicUniv +module UM = UriManager +module Obj = LibraryObjects +module HObj = HelmLibraryObjects +module A = Cic2acic +module Ut = CicUtil +module E = CicEnvironment + +module Cl = CicClassify +module T = ProceduralTypes +module Cn = ProceduralConversion + +type status = { + sorts : (C.id, A.sort_kind) Hashtbl.t; + types : (C.id, A.anntypes) Hashtbl.t; + prefix: string; + max_depth: int option; + depth: int; + context: C.context; + intros: string list; + ety: C.annterm option +} + +(* helpers ******************************************************************) + +let id x = x + +let comp f g x = f (g x) + +let cic = D.deannotate_term + +let split2_last l1 l2 = +try + let n = pred (List.length l1) in + let before1, after1 = T.list_split n l1 in + let before2, after2 = T.list_split n l2 in + before1, before2, List.hd after1, List.hd after2 +with Invalid_argument _ -> failwith "A2P.split2_last" + +let string_of_head = function + | C.ASort _ -> "sort" + | C.AConst _ -> "const" + | C.AMutInd _ -> "mutind" + | C.AMutConstruct _ -> "mutconstruct" + | C.AVar _ -> "var" + | C.ARel _ -> "rel" + | C.AProd _ -> "prod" + | C.ALambda _ -> "lambda" + | C.ALetIn _ -> "letin" + | C.AFix _ -> "fix" + | C.ACoFix _ -> "cofix" + | C.AAppl _ -> "appl" + | C.ACast _ -> "cast" + | C.AMutCase _ -> "mutcase" + | C.AMeta _ -> "meta" + | C.AImplicit _ -> "implict" + +let clear st = {st with intros = []; ety = None} + +let next st = {(clear st) with depth = succ st.depth} + +let set_ety st ety = + if st.ety = None then {st with ety = ety} else st + +let add st entry intro ety = + let st = set_ety st ety in + {st with context = entry :: st.context; intros = intro :: st.intros} + +let test_depth st = +try + let msg = Printf.sprintf "Depth %u: " st.depth in + match st.max_depth with + | None -> true, "" + | Some d -> if st.depth < d then true, msg else false, "DEPTH EXCEDED: " +with Invalid_argument _ -> failwith "A2P.test_depth" + +let is_rewrite_right = function + | C.AConst (_, uri, []) -> + UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri + | _ -> false + +let is_rewrite_left = function + | C.AConst (_, uri, []) -> + UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri + | _ -> false +(* +let get_ind_name uri tno xcno = +try + let ts = match E.get_obj Un.empty_ugraph uri with + | C.InductiveDefinition (ts, _, _,_), _ -> ts + | _ -> assert false + in + let tname, cs = match List.nth ts tno with + | (name, _, _, cs) -> name, cs + in + match xcno with + | None -> tname + | Some cno -> fst (List.nth cs (pred cno)) +with Invalid_argument _ -> failwith "A2P.get_ind_name" +*) +let get_inner_types st v = +try + let id = Ut.id_of_annterm v in + try match Hashtbl.find st.types id with + | {A.annsynthesized = st; A.annexpected = Some et} -> Some (st, et) + | {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 = +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" + +(* proof construction *******************************************************) + +let unused_premise = "UNUSED" + +let defined_premise = "DEFINED" + +let assumed_premise = "ASSUMED" + +let expanded_premise = "EXPANDED" + +let eta_expand n t = + let ty = C.AImplicit ("", None) in + let name i = Printf.sprintf "%s%u" expanded_premise i in + let lambda i t = C.ALambda ("", C.Name (name i), ty, t) in + let arg i n = T.mk_arel (n - i) (name i) in + let rec aux i f a = + if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a) + in + let absts, args = aux 0 id [] in + match Cn.lift 1 n t with + | C.AAppl (id, ts) -> absts (C.AAppl (id, ts @ args)) + | t -> absts (C.AAppl ("", t :: args)) + +let appl_expand n = function + | C.AAppl (id, ts) -> + let before, after = T.list_split (List.length ts + n) ts in + C.AAppl ("", C.AAppl (id, before) :: after) + | _ -> assert false + +let get_intro name t = +try +match name with + | C.Anonymous -> unused_premise + | C.Name s -> + if DTI.does_not_occur 1 (cic t) then unused_premise else s +with Invalid_argument _ -> failwith "A2P.get_intro" + +let mk_intros st script = +try + if st.intros = [] then script else + let count = List.length st.intros in + let p0 = T.Whd (count, "") in + let p1 = T.Intros (Some count, List.rev st.intros, "") in + match st.ety with + | Some ety when Cn.need_whd count ety -> p0 :: p1 :: script + | _ -> p1 :: script +with Invalid_argument _ -> failwith "A2P.mk_intros" + +let rec mk_atomic st dtext what = + if T.is_atomic what then [], what else + let name = defined_premise in + mk_fwd_proof st dtext name what, T.mk_arel 0 name + +and mk_fwd_rewrite st dtext name tl direction = + let what, where = List.nth tl 5, List.nth tl 3 in + let rewrite premise = + let script, what = mk_atomic st dtext what in + T.Rewrite (direction, what, Some (premise, name), dtext) :: script + in + match where with + | C.ARel (_, _, _, binder) -> rewrite binder + | _ -> + assert (get_inner_sort st where = `Prop); + let pred, old = List.nth tl 2, List.nth tl 1 in + let pred_name = defined_premise in + let pred_text = "extracted" in + let p1 = T.LetIn (pred_name, pred, pred_text) in + let cut_name = assumed_premise in + let cut_type = C.AAppl ("", [T.mk_arel 0 pred_name; old]) in + let cut_text = "" in + let p2 = T.Cut (cut_name, cut_type, cut_text) in + let qs = [rewrite cut_name; mk_proof (next st) where] in + [T.Branch (qs, ""); p2; p1] + +and mk_fwd_proof st dtext name = function + | C.AAppl (_, hd :: tl) as v -> + if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else + if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else + begin match get_inner_types st v with + | Some (ity, _) -> + let qs = [[T.Id ""]; mk_proof (next st) v] in + [T.Branch (qs, ""); T.Cut (name, ity, dtext)] + | None -> + let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in + let (classes, rc) as h = Cl.classify st.context ty in + let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in + [T.LetIn (name, v, dtext ^ text)] + end + | v -> + [T.LetIn (name, v, dtext)] + +and mk_proof st = function + | C.ALambda (_, name, v, t) as what -> + let entry = Some (name, C.Decl (cic v)) in + let intro = get_intro name t in + let ety = match get_inner_types st what with + | Some (_, ety) -> Some ety + | None -> None + in + mk_proof (add st entry intro ety) t + | C.ALetIn (_, name, v, t) as what -> + let proceed, dtext = test_depth st in + let script = if proceed then + let entry = Some (name, C.Def (cic v, None)) in + let intro = get_intro name t in + let q = mk_proof (next (add st entry intro None)) t in + List.rev_append (mk_fwd_proof st dtext intro v) q + else + [T.Apply (what, dtext)] + in + mk_intros st script + | C.ARel _ as what -> + let _, dtext = test_depth st in + let text = "assumption" in + let script = [T.Apply (what, dtext ^ text)] in + mk_intros st script + | C.AMutConstruct _ as what -> + let _, dtext = test_depth st in + let script = [T.Apply (what, dtext)] in + mk_intros st script + | C.AAppl (_, hd :: tl) as t -> + let proceed, dtext = test_depth st in + let script = if proceed then + let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in + let (classes, rc) as h = Cl.classify st.context ty in + let decurry = List.length classes - List.length tl in + if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else + if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else + let synth = Cl.S.singleton 0 in + let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in + match rc with + | Some (i, j) when i > 1 && i <= List.length classes -> + let classes, tl, _, what = split2_last classes tl in + let script, what = mk_atomic st dtext what in + let synth = Cl.S.add 1 synth in + let qs = mk_bkd_proofs (next st) synth classes tl in + if is_rewrite_right hd then + List.rev script @ + [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")] + else if is_rewrite_left hd then + List.rev script @ + [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")] + else + let using = Some hd in + List.rev script @ + [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")] + | _ -> + let qs = mk_bkd_proofs (next st) synth classes tl in + let script, hd = mk_atomic st dtext hd in + List.rev script @ + [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] + else + [T.Apply (t, dtext)] + in + mk_intros st script + | t -> + let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in + let script = [T.Note text] in + mk_intros st script + +and mk_bkd_proofs st synth classes ts = +try + let _, dtext = test_depth st in + let aux inv v = + if Cl.overlaps synth inv then None else + if Cl.S.is_empty inv then Some (mk_proof st v) else + Some [T.Apply (v, dtext ^ "dependent")] + in + T.list_map2_filter aux classes ts +with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs" + +(* object costruction *******************************************************) + +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 mk_obj st = function + | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars -> + let ast = mk_proof (set_ety st (Some t)) v in + let count = T.count_steps 0 ast in + let text = Printf.sprintf "tactics: %u" count in + T.Theorem (s, t, text) :: ast @ [T.Qed ""] + | _ -> + failwith "not a theorem" + +(* interface functions ******************************************************) + +let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj = + let st = { + sorts = ids_to_inner_sorts; + types = ids_to_inner_types; + prefix = prefix; + max_depth = depth; + depth = 0; + context = []; + intros = []; + ety = None + } in + prerr_endline "Level 2 transformation"; + let steps = mk_obj st aobj in + prerr_endline "grafite rendering"; + List.rev (T.render_steps [] steps) diff --git a/components/acic_procedural/acic2Procedural.mli b/components/acic_procedural/acic2Procedural.mli new file mode 100644 index 000000000..d1ff6a0c2 --- /dev/null +++ b/components/acic_procedural/acic2Procedural.mli @@ -0,0 +1,33 @@ +(* 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/. + *) + +val acic2procedural: + ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> + ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> + ?depth:int -> string -> Cic.annobj -> + (Cic.annterm, Cic.annterm, + Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) + GrafiteAst.statement list + diff --git a/components/acic_procedural/cicClassify.ml b/components/acic_procedural/cicClassify.ml new file mode 100644 index 000000000..4cfd47e5a --- /dev/null +++ b/components/acic_procedural/cicClassify.ml @@ -0,0 +1,149 @@ +(* 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 R = CicReduction +module D = Deannotate +module Int = struct + type t = int + let compare = compare +end +module S = Set.Make (Int) + +type conclusion = (int * int) option + +(* debugging ****************************************************************) + +let string_of_entry inverse = + if S.mem 0 inverse then "C" else + if S.is_empty inverse then "I" else "P" + +let to_string (classes, rc) = + let linearize = String.concat " " (List.map string_of_entry classes) in + match rc with + | None -> linearize + | Some (i, j) -> Printf.sprintf "%s %u %u" linearize i j + +let out_table b = + let map i (_, inverse) = + let map i tl = Printf.sprintf "%2u" i :: tl in + let iset = String.concat " " (S.fold map inverse []) in + Printf.eprintf "%2u|%s\n" i iset + in + Array.iteri map b; + prerr_newline () + +(****************************************************************************) + +let id x = x + +let rec list_fold_left g map = function + | [] -> g + | hd :: tl -> map (list_fold_left g map tl) hd + +let get_rels h t = + let rec aux d g = function + | C.Sort _ + | C.Implicit _ -> g + | C.Rel i -> + if i < d then g else fun a -> g (S.add (i - d + h + 1) a) + | C.Appl ss -> list_fold_left g (aux d) ss + | C.Const (_, ss) + | C.MutInd (_, _, ss) + | C.MutConstruct (_, _, _, ss) + | C.Var (_, ss) -> + let map g (_, t) = aux d g t in + list_fold_left g map ss + | C.Meta (_, ss) -> + let map g = function + | None -> g + | Some t -> aux d g t + in + list_fold_left g map ss + | C.Cast (t1, t2) -> aux d (aux d g t2) t1 + | C.LetIn (_, t1, t2) + | C.Lambda (_, t1, t2) + | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1 + | C.MutCase (_, _, t1, t2, ss) -> + aux d (aux d (list_fold_left g (aux d) ss) t2) t1 + | C.Fix (_, ss) -> + let k = List.length ss in + let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in + list_fold_left g map ss + | C.CoFix (_, ss) -> + let k = List.length ss in + let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in + list_fold_left g map ss + in + let g a = a in + aux 1 g t S.empty + +let split c t = + let add s v c = Some (s, C.Decl v) :: c in + let rec aux whd a n c = function + | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t + | v when whd -> v :: a, n + | v -> aux true a n c (R.whd ~delta:true c v) + in + aux false [] 0 c t + +let classify_conclusion = function + | C.Rel i -> Some (i, 0) + | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl) + | _ -> None + +let classify c t = +try + let vs, h = split c t in + let rc = classify_conclusion (List.hd vs) in + let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in + let l, h = List.fold_left map ([], 0) vs in + let b = Array.of_list (List.rev l) in + let mk_closure b h = + let map j = if j < h then S.union (fst b.(j)) else id in + for i = pred h downto 0 do + let direct, unused = b.(i) in + b.(i) <- S.fold map direct direct, unused + done; b + in + let b = mk_closure b h in + let rec mk_inverse i direct = + if S.is_empty direct then () else + let j = S.choose direct in + if j < h then + let unused, inverse = b.(j) in + b.(j) <- unused, S.add i inverse + else (); + mk_inverse i (S.remove j direct) + in + let map i (direct, _) = mk_inverse i direct in + Array.iteri map b; +(* out_table b; *) + List.rev_map snd (List.tl (Array.to_list b)), rc +with Invalid_argument _ -> failwith "Classify.classify" + +let overlaps s1 s2 = + let predicate x = S.mem x s1 in + S.exists predicate s2 diff --git a/components/acic_procedural/cicClassify.mli b/components/acic_procedural/cicClassify.mli new file mode 100644 index 000000000..3d92134df --- /dev/null +++ b/components/acic_procedural/cicClassify.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/. + *) + +module S : Set.S with type elt = int + +type conclusion = (int * int) option + +val classify: Cic.context -> Cic.term -> S.t list * conclusion + +val to_string: S.t list * conclusion -> string + +val overlaps: S.t -> S.t -> bool diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml new file mode 100644 index 000000000..abd6fd62a --- /dev/null +++ b/components/acic_procedural/proceduralConversion.ml @@ -0,0 +1,61 @@ +(* 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 + +let rec need_whd i = function + | C.ACast (_, t, _) -> need_whd i t + | C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t + | _ when i > 0 -> true + | _ -> false + +let lift k n = + let rec lift_xns k (uri, t) = uri, lift_term k t + and lift_ms k = function + | None -> None + | Some t -> Some (lift_term k t) + and lift_fix len k (id, name, i, ty, bo) = + id, name, i, lift_term k ty, lift_term (k + len) bo + and lift_cofix len k (id, name, ty, bo) = + id, name, lift_term k ty, lift_term (k + len) bo + and lift_term k = function + | C.ASort _ as t -> t + | C.AImplicit _ as t -> t + | C.ARel (id, rid, m, b) as t -> if m < k then t else C.ARel (id, rid, m + n, b) + | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (lift_xns k) xnss) + | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (lift_xns k) xnss) + | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (lift_xns k) xnss) + | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (lift_xns k) xnss) + | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (lift_ms k) mss) + | C.AAppl (id, ts) -> C.AAppl (id, List.map (lift_term k) ts) + | C.ACast (id, te, ty) -> C.ACast (id, lift_term k te, lift_term k ty) + | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl) + | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t) + | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t) + | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term (succ k) t) + | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl) + | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl) + in + lift_term k diff --git a/components/acic_procedural/proceduralConversion.mli b/components/acic_procedural/proceduralConversion.mli new file mode 100644 index 000000000..d5ad4fd1c --- /dev/null +++ b/components/acic_procedural/proceduralConversion.mli @@ -0,0 +1,28 @@ +(* 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/. + *) + +val need_whd: int -> Cic.annterm -> bool + +val lift: int -> int -> Cic.annterm -> Cic.annterm diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml new file mode 100644 index 000000000..95fdc6e56 --- /dev/null +++ b/components/acic_procedural/proceduralTypes.ml @@ -0,0 +1,204 @@ +(* 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 H = HExtlib +module C = Cic +module G = GrafiteAst +module N = CicNotationPt + +(* functions to be moved ****************************************************) + +let list_map2_filter map l1 l2 = + let rec filter l = function + | [] -> l + | None :: tl -> filter l tl + | Some a :: tl -> filter (a :: l) tl + in + filter [] (List.rev_map2 map l1 l2) + +let rec list_split n l = + if n = 0 then [], l else + let l1, l2 = list_split (pred n) (List.tl l) in + List.hd l :: l1, l2 + +let cont sep a = match sep with + | None -> a + | Some sep -> sep :: a + +let list_rev_map_concat map sep a l = + let rec aux a = function + | [] -> a + | [x] -> map a x + | x :: y :: l -> aux (sep :: map a x) (y :: l) + in + aux a l + +let is_atomic = function + | C.ASort _ + | C.AConst _ + | C.AMutInd _ + | C.AMutConstruct _ + | C.AVar _ + | C.ARel _ + | C.AMeta _ + | C.AImplicit _ -> true + | _ -> false + +(****************************************************************************) + +type name = string +type what = Cic.annterm +type how = bool +type using = Cic.annterm +type count = int +type note = string +type where = (name * name) option + +type step = Note of note + | Theorem of name * what * note + | Qed of note + | Id of note + | Intros of count option * name list * note + | Cut of name * what * note + | LetIn of name * what * note + | Rewrite of how * what * where * note + | Elim of what * using option * note + | Apply of what * note + | Whd of count * note + | Branch of step list list * note + +(* annterm constructors *****************************************************) + +let mk_arel i b = Cic.ARel ("", "", i, b) + +(* grafite ast constructors *************************************************) + +let floc = H.dummy_floc + +let hole = C.AImplicit ("", Some `Hole) + +let mk_note str = G.Comment (floc, G.Note (floc, str)) + +let mk_theorem name t = + let obj = N.Theorem (`Theorem, name, t, None) in + G.Executable (floc, G.Command (floc, G.Obj (floc, obj))) + +let mk_qed = + G.Executable (floc, G.Command (floc, G.Qed floc)) + +let mk_tactic tactic = + G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), None)) + +let mk_id = + let tactic = G.IdTac floc in + mk_tactic tactic + +let mk_intros xi ids = + let tactic = G.Intros (floc, xi, ids) in + mk_tactic tactic + +let mk_cut name what = + let tactic = G.Cut (floc, Some name, what) in + mk_tactic tactic + +let mk_letin name what = + let tactic = G.LetIn (floc, what, name) in + mk_tactic tactic + +let mk_rewrite direction what where = + let direction = if direction then `RightToLeft else `LeftToRight in + let pattern, rename = match where with + | None -> (None, [], Some hole), [] + | Some (premise, name) -> (None, [premise, hole], None), [name] + in + let tactic = G.Rewrite (floc, direction, what, pattern, rename) in + mk_tactic tactic + +let mk_elim what using = + let tactic = G.Elim (floc, what, using, Some 0, []) in + mk_tactic tactic + +let mk_apply t = + let tactic = G.Apply (floc, t) in + mk_tactic tactic + +let mk_whd i = + let pattern = None, [], Some hole in + let tactic = G.Reduce (floc, `Whd, pattern) in + mk_tactic tactic + +let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None)) + +let mk_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None)) + +let mk_ob = G.Executable (floc, G.Tactical (floc, G.Branch floc, None)) + +let mk_cb = G.Executable (floc, G.Tactical (floc, G.Merge floc, None)) + +let mk_vb = G.Executable (floc, G.Tactical (floc, G.Shift floc, None)) + +(* rendering ****************************************************************) + +let rec render_step sep a = function + | Note s -> mk_note s :: a + | Theorem (n, t, s) -> mk_note s :: mk_theorem n t :: a + | Qed s -> mk_note s :: mk_qed :: a + | Id s -> mk_note s :: cont sep (mk_id :: a) + | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a) + | Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a) + | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a) + | Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a) + | Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a) + | Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a) + | Whd (c, s) -> mk_note s :: cont sep (mk_whd c :: a) + | Branch ([], s) -> a + | Branch ([ps], s) -> render_steps sep a ps + | Branch (pss, s) -> + let a = mk_ob :: a in + let body = mk_cb :: list_rev_map_concat (render_steps None) mk_vb a pss in + mk_note s :: cont sep body + +and render_steps sep a = function + | [] -> a + | [p] -> render_step sep a p + | p :: Branch ([], _) :: ps -> + render_steps sep a (p :: ps) + | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) -> + render_steps sep (render_step (Some mk_sc) a p) ps + | p :: ps -> + render_steps sep (render_step (Some mk_dot) a p) ps + +let render_steps a = render_steps None a + +(* counting *****************************************************************) + +let rec count_step a = function + | Note _ + | Theorem _ + | Qed _ -> a + | Branch (pps, _) -> List.fold_left count_steps a pps + | _ -> succ a + +and count_steps a = List.fold_left count_step a diff --git a/components/acic_procedural/proceduralTypes.mli b/components/acic_procedural/proceduralTypes.mli new file mode 100644 index 000000000..dfd82df12 --- /dev/null +++ b/components/acic_procedural/proceduralTypes.mli @@ -0,0 +1,65 @@ +(* 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/. + *) + +(* functions to be moved ****************************************************) + +val list_map2_filter: ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list + +val list_split: int -> 'a list -> 'a list * 'a list + +val mk_arel: int -> string -> Cic.annterm + +val is_atomic:Cic.annterm -> bool + +(****************************************************************************) + +type name = string +type what = Cic.annterm +type how = bool +type using = Cic.annterm +type count = int +type note = string +type where = (name * name) option + +type step = Note of note + | Theorem of name * what * note + | Qed of note + | Id of note + | Intros of count option * name list * note + | Cut of name * what * note + | LetIn of name * what * note + | Rewrite of how * what * where * note + | Elim of what * using option * note + | Apply of what * note + | Whd of count * note + | Branch of step list list * note + +val render_steps: + (what, 'a, [> `Whd] as 'b, what CicNotationPt.obj, name) GrafiteAst.statement list -> + step list -> + (what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list + +val count_steps: + int -> step list -> int diff --git a/components/content_pres/.depend b/components/content_pres/.depend index 78cde4140..2c5d65140 100644 --- a/components/content_pres/.depend +++ b/components/content_pres/.depend @@ -30,18 +30,6 @@ content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ cicNotationPres.cmi box.cmi content2pres.cmi content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ cicNotationPres.cmx box.cmx content2pres.cmi -cicClassify.cmo: cicClassify.cmi -cicClassify.cmx: cicClassify.cmi -proceduralConversion.cmo: proceduralConversion.cmi -proceduralConversion.cmx: proceduralConversion.cmi -proceduralTypes.cmo: proceduralTypes.cmi -proceduralTypes.cmx: proceduralTypes.cmi -acic2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx cicClassify.cmx acic2Procedural.cmi -objPp.cmo: termContentPres.cmi content2pres.cmi cicNotationPres.cmi boxPp.cmi \ - acic2Procedural.cmi objPp.cmi -objPp.cmx: termContentPres.cmx content2pres.cmx cicNotationPres.cmx boxPp.cmx \ - acic2Procedural.cmx objPp.cmi sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \ box.cmi sequent2pres.cmi sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \ diff --git a/components/content_pres/.depend.opt b/components/content_pres/.depend.opt index 78cde4140..2c5d65140 100644 --- a/components/content_pres/.depend.opt +++ b/components/content_pres/.depend.opt @@ -30,18 +30,6 @@ content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ cicNotationPres.cmi box.cmi content2pres.cmi content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ cicNotationPres.cmx box.cmx content2pres.cmi -cicClassify.cmo: cicClassify.cmi -cicClassify.cmx: cicClassify.cmi -proceduralConversion.cmo: proceduralConversion.cmi -proceduralConversion.cmx: proceduralConversion.cmi -proceduralTypes.cmo: proceduralTypes.cmi -proceduralTypes.cmx: proceduralTypes.cmi -acic2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx cicClassify.cmx acic2Procedural.cmi -objPp.cmo: termContentPres.cmi content2pres.cmi cicNotationPres.cmi boxPp.cmi \ - acic2Procedural.cmi objPp.cmi -objPp.cmx: termContentPres.cmx content2pres.cmx cicNotationPres.cmx boxPp.cmx \ - acic2Procedural.cmx objPp.cmi sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \ box.cmi sequent2pres.cmi sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \ diff --git a/components/content_pres/Makefile b/components/content_pres/Makefile index 9c627cb23..fb6d0fe46 100644 --- a/components/content_pres/Makefile +++ b/components/content_pres/Makefile @@ -12,11 +12,6 @@ INTERFACE_FILES = \ cicNotationPres.mli \ boxPp.mli \ content2pres.mli \ - cicClassify.mli \ - proceduralConversion.mli \ - proceduralTypes.mli \ - acic2Procedural.mli \ - objPp.mli \ sequent2pres.mli \ $(NULL) IMPLEMENTATION_FILES = \ diff --git a/components/content_pres/acic2Procedural.ml b/components/content_pres/acic2Procedural.ml deleted file mode 100644 index adfe4b05c..000000000 --- a/components/content_pres/acic2Procedural.ml +++ /dev/null @@ -1,348 +0,0 @@ -(* 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 D = Deannotate -module DTI = DoubleTypeInference -module TC = CicTypeChecker -module Un = CicUniv -module UM = UriManager -module Obj = LibraryObjects -module HObj = HelmLibraryObjects -module A = Cic2acic -module Ut = CicUtil -module E = CicEnvironment - -module Cl = CicClassify -module T = ProceduralTypes -module Cn = ProceduralConversion - -type status = { - sorts : (C.id, A.sort_kind) Hashtbl.t; - types : (C.id, A.anntypes) Hashtbl.t; - prefix: string; - max_depth: int option; - depth: int; - context: C.context; - intros: string list; - ety: C.annterm option -} - -(* helpers ******************************************************************) - -let id x = x - -let comp f g x = f (g x) - -let cic = D.deannotate_term - -let split2_last l1 l2 = -try - let n = pred (List.length l1) in - let before1, after1 = T.list_split n l1 in - let before2, after2 = T.list_split n l2 in - before1, before2, List.hd after1, List.hd after2 -with Invalid_argument _ -> failwith "A2P.split2_last" - -let string_of_head = function - | C.ASort _ -> "sort" - | C.AConst _ -> "const" - | C.AMutInd _ -> "mutind" - | C.AMutConstruct _ -> "mutconstruct" - | C.AVar _ -> "var" - | C.ARel _ -> "rel" - | C.AProd _ -> "prod" - | C.ALambda _ -> "lambda" - | C.ALetIn _ -> "letin" - | C.AFix _ -> "fix" - | C.ACoFix _ -> "cofix" - | C.AAppl _ -> "appl" - | C.ACast _ -> "cast" - | C.AMutCase _ -> "mutcase" - | C.AMeta _ -> "meta" - | C.AImplicit _ -> "implict" - -let clear st = {st with intros = []; ety = None} - -let next st = {(clear st) with depth = succ st.depth} - -let set_ety st ety = - if st.ety = None then {st with ety = ety} else st - -let add st entry intro ety = - let st = set_ety st ety in - {st with context = entry :: st.context; intros = intro :: st.intros} - -let test_depth st = -try - let msg = Printf.sprintf "Depth %u: " st.depth in - match st.max_depth with - | None -> true, "" - | Some d -> if st.depth < d then true, msg else false, "DEPTH EXCEDED: " -with Invalid_argument _ -> failwith "A2P.test_depth" - -let is_rewrite_right = function - | C.AConst (_, uri, []) -> - UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri - | _ -> false - -let is_rewrite_left = function - | C.AConst (_, uri, []) -> - UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri - | _ -> false -(* -let get_ind_name uri tno xcno = -try - let ts = match E.get_obj Un.empty_ugraph uri with - | C.InductiveDefinition (ts, _, _,_), _ -> ts - | _ -> assert false - in - let tname, cs = match List.nth ts tno with - | (name, _, _, cs) -> name, cs - in - match xcno with - | None -> tname - | Some cno -> fst (List.nth cs (pred cno)) -with Invalid_argument _ -> failwith "A2P.get_ind_name" -*) -let get_inner_types st v = -try - let id = Ut.id_of_annterm v in - try match Hashtbl.find st.types id with - | {A.annsynthesized = st; A.annexpected = Some et} -> Some (st, et) - | {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 = -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" - -(* proof construction *******************************************************) - -let unused_premise = "UNUSED" - -let defined_premise = "DEFINED" - -let assumed_premise = "ASSUMED" - -let expanded_premise = "EXPANDED" - -let eta_expand n t = - let ty = C.AImplicit ("", None) in - let name i = Printf.sprintf "%s%u" expanded_premise i in - let lambda i t = C.ALambda ("", C.Name (name i), ty, t) in - let arg i n = T.mk_arel (n - i) (name i) in - let rec aux i f a = - if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a) - in - let absts, args = aux 0 id [] in - match Cn.lift 1 n t with - | C.AAppl (id, ts) -> absts (C.AAppl (id, ts @ args)) - | t -> absts (C.AAppl ("", t :: args)) - -let appl_expand n = function - | C.AAppl (id, ts) -> - let before, after = T.list_split (List.length ts + n) ts in - C.AAppl ("", C.AAppl (id, before) :: after) - | _ -> assert false - -let get_intro name t = -try -match name with - | C.Anonymous -> unused_premise - | C.Name s -> - if DTI.does_not_occur 1 (cic t) then unused_premise else s -with Invalid_argument _ -> failwith "A2P.get_intro" - -let mk_intros st script = -try - if st.intros = [] then script else - let count = List.length st.intros in - let p0 = T.Whd (count, "") in - let p1 = T.Intros (Some count, List.rev st.intros, "") in - match st.ety with - | Some ety when Cn.need_whd count ety -> p0 :: p1 :: script - | _ -> p1 :: script -with Invalid_argument _ -> failwith "A2P.mk_intros" - -let rec mk_atomic st dtext what = - if T.is_atomic what then [], what else - let name = defined_premise in - mk_fwd_proof st dtext name what, T.mk_arel 0 name - -and mk_fwd_rewrite st dtext name tl direction = - let what, where = List.nth tl 5, List.nth tl 3 in - let rewrite premise = - let script, what = mk_atomic st dtext what in - T.Rewrite (direction, what, Some (premise, name), dtext) :: script - in - match where with - | C.ARel (_, _, _, binder) -> rewrite binder - | _ -> - assert (get_inner_sort st where = `Prop); - let pred, old = List.nth tl 2, List.nth tl 1 in - let pred_name = defined_premise in - let pred_text = "extracted" in - let p1 = T.LetIn (pred_name, pred, pred_text) in - let cut_name = assumed_premise in - let cut_type = C.AAppl ("", [T.mk_arel 0 pred_name; old]) in - let cut_text = "" in - let p2 = T.Cut (cut_name, cut_type, cut_text) in - let qs = [rewrite cut_name; mk_proof (next st) where] in - [T.Branch (qs, ""); p2; p1] - -and mk_fwd_proof st dtext name = function - | C.AAppl (_, hd :: tl) as v -> - if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else - if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else - begin match get_inner_types st v with - | Some (ity, _) -> - let qs = [[T.Id ""]; mk_proof (next st) v] in - [T.Branch (qs, ""); T.Cut (name, ity, dtext)] - | None -> - let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in - let (classes, rc) as h = Cl.classify st.context ty in - let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in - [T.LetIn (name, v, dtext ^ text)] - end - | v -> - [T.LetIn (name, v, dtext)] - -and mk_proof st = function - | C.ALambda (_, name, v, t) as what -> - let entry = Some (name, C.Decl (cic v)) in - let intro = get_intro name t in - let ety = match get_inner_types st what with - | Some (_, ety) -> Some ety - | None -> None - in - mk_proof (add st entry intro ety) t - | C.ALetIn (_, name, v, t) as what -> - let proceed, dtext = test_depth st in - let script = if proceed then - let entry = Some (name, C.Def (cic v, None)) in - let intro = get_intro name t in - let q = mk_proof (next (add st entry intro None)) t in - List.rev_append (mk_fwd_proof st dtext intro v) q - else - [T.Apply (what, dtext)] - in - mk_intros st script - | C.ARel _ as what -> - let _, dtext = test_depth st in - let text = "assumption" in - let script = [T.Apply (what, dtext ^ text)] in - mk_intros st script - | C.AMutConstruct _ as what -> - let _, dtext = test_depth st in - let script = [T.Apply (what, dtext)] in - mk_intros st script - | C.AAppl (_, hd :: tl) as t -> - let proceed, dtext = test_depth st in - let script = if proceed then - let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in - let (classes, rc) as h = Cl.classify st.context ty in - let decurry = List.length classes - List.length tl in - if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else - if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else - let synth = Cl.S.singleton 0 in - let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in - match rc with - | Some (i, j) when i > 1 && i <= List.length classes -> - let classes, tl, _, what = split2_last classes tl in - let script, what = mk_atomic st dtext what in - let synth = Cl.S.add 1 synth in - let qs = mk_bkd_proofs (next st) synth classes tl in - if is_rewrite_right hd then - List.rev script @ - [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")] - else if is_rewrite_left hd then - List.rev script @ - [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")] - else - let using = Some hd in - List.rev script @ - [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")] - | _ -> - let qs = mk_bkd_proofs (next st) synth classes tl in - let script, hd = mk_atomic st dtext hd in - List.rev script @ - [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] - else - [T.Apply (t, dtext)] - in - mk_intros st script - | t -> - let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in - let script = [T.Note text] in - mk_intros st script - -and mk_bkd_proofs st synth classes ts = -try - let _, dtext = test_depth st in - let aux inv v = - if Cl.overlaps synth inv then None else - if Cl.S.is_empty inv then Some (mk_proof st v) else - Some [T.Apply (v, dtext ^ "dependent")] - in - T.list_map2_filter aux classes ts -with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs" - -(* object costruction *******************************************************) - -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 mk_obj st = function - | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars -> - let ast = mk_proof (set_ety st (Some t)) v in - let count = T.count_steps 0 ast in - let text = Printf.sprintf "tactics: %u" count in - T.Theorem (s, t, text) :: ast @ [T.Qed ""] - | _ -> - failwith "not a theorem" - -(* interface functions ******************************************************) - -let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj = - let st = { - sorts = ids_to_inner_sorts; - types = ids_to_inner_types; - prefix = prefix; - max_depth = depth; - depth = 0; - context = []; - intros = []; - ety = None - } in - prerr_endline "Level 2 transformation"; - let steps = mk_obj st aobj in - prerr_endline "grafite rendering"; - List.rev (T.render_steps [] steps) diff --git a/components/content_pres/acic2Procedural.mli b/components/content_pres/acic2Procedural.mli deleted file mode 100644 index d1ff6a0c2..000000000 --- a/components/content_pres/acic2Procedural.mli +++ /dev/null @@ -1,33 +0,0 @@ -(* 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/. - *) - -val acic2procedural: - ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> - ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> - ?depth:int -> string -> Cic.annobj -> - (Cic.annterm, Cic.annterm, - Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) - GrafiteAst.statement list - diff --git a/components/content_pres/cicClassify.ml b/components/content_pres/cicClassify.ml deleted file mode 100644 index 4cfd47e5a..000000000 --- a/components/content_pres/cicClassify.ml +++ /dev/null @@ -1,149 +0,0 @@ -(* 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 R = CicReduction -module D = Deannotate -module Int = struct - type t = int - let compare = compare -end -module S = Set.Make (Int) - -type conclusion = (int * int) option - -(* debugging ****************************************************************) - -let string_of_entry inverse = - if S.mem 0 inverse then "C" else - if S.is_empty inverse then "I" else "P" - -let to_string (classes, rc) = - let linearize = String.concat " " (List.map string_of_entry classes) in - match rc with - | None -> linearize - | Some (i, j) -> Printf.sprintf "%s %u %u" linearize i j - -let out_table b = - let map i (_, inverse) = - let map i tl = Printf.sprintf "%2u" i :: tl in - let iset = String.concat " " (S.fold map inverse []) in - Printf.eprintf "%2u|%s\n" i iset - in - Array.iteri map b; - prerr_newline () - -(****************************************************************************) - -let id x = x - -let rec list_fold_left g map = function - | [] -> g - | hd :: tl -> map (list_fold_left g map tl) hd - -let get_rels h t = - let rec aux d g = function - | C.Sort _ - | C.Implicit _ -> g - | C.Rel i -> - if i < d then g else fun a -> g (S.add (i - d + h + 1) a) - | C.Appl ss -> list_fold_left g (aux d) ss - | C.Const (_, ss) - | C.MutInd (_, _, ss) - | C.MutConstruct (_, _, _, ss) - | C.Var (_, ss) -> - let map g (_, t) = aux d g t in - list_fold_left g map ss - | C.Meta (_, ss) -> - let map g = function - | None -> g - | Some t -> aux d g t - in - list_fold_left g map ss - | C.Cast (t1, t2) -> aux d (aux d g t2) t1 - | C.LetIn (_, t1, t2) - | C.Lambda (_, t1, t2) - | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1 - | C.MutCase (_, _, t1, t2, ss) -> - aux d (aux d (list_fold_left g (aux d) ss) t2) t1 - | C.Fix (_, ss) -> - let k = List.length ss in - let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in - list_fold_left g map ss - | C.CoFix (_, ss) -> - let k = List.length ss in - let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in - list_fold_left g map ss - in - let g a = a in - aux 1 g t S.empty - -let split c t = - let add s v c = Some (s, C.Decl v) :: c in - let rec aux whd a n c = function - | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t - | v when whd -> v :: a, n - | v -> aux true a n c (R.whd ~delta:true c v) - in - aux false [] 0 c t - -let classify_conclusion = function - | C.Rel i -> Some (i, 0) - | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl) - | _ -> None - -let classify c t = -try - let vs, h = split c t in - let rc = classify_conclusion (List.hd vs) in - let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in - let l, h = List.fold_left map ([], 0) vs in - let b = Array.of_list (List.rev l) in - let mk_closure b h = - let map j = if j < h then S.union (fst b.(j)) else id in - for i = pred h downto 0 do - let direct, unused = b.(i) in - b.(i) <- S.fold map direct direct, unused - done; b - in - let b = mk_closure b h in - let rec mk_inverse i direct = - if S.is_empty direct then () else - let j = S.choose direct in - if j < h then - let unused, inverse = b.(j) in - b.(j) <- unused, S.add i inverse - else (); - mk_inverse i (S.remove j direct) - in - let map i (direct, _) = mk_inverse i direct in - Array.iteri map b; -(* out_table b; *) - List.rev_map snd (List.tl (Array.to_list b)), rc -with Invalid_argument _ -> failwith "Classify.classify" - -let overlaps s1 s2 = - let predicate x = S.mem x s1 in - S.exists predicate s2 diff --git a/components/content_pres/cicClassify.mli b/components/content_pres/cicClassify.mli deleted file mode 100644 index 3d92134df..000000000 --- a/components/content_pres/cicClassify.mli +++ /dev/null @@ -1,34 +0,0 @@ -(* 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 S : Set.S with type elt = int - -type conclusion = (int * int) option - -val classify: Cic.context -> Cic.term -> S.t list * conclusion - -val to_string: S.t list * conclusion -> string - -val overlaps: S.t -> S.t -> bool diff --git a/components/content_pres/objPp.ml b/components/content_pres/objPp.ml deleted file mode 100644 index f83b18635..000000000 --- a/components/content_pres/objPp.ml +++ /dev/null @@ -1,65 +0,0 @@ -(* Copyright (C) 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://helm.cs.unibo.it/ - *) - -let remove_closed_substs s = - Pcre.replace ~pat:"{...}" ~templ:"" s - -let term2pres n ids_to_inner_sorts annterm = - let ast, ids_to_uris = - TermAcicContent.ast_of_acic ids_to_inner_sorts annterm - in - let bobj = - CicNotationPres.box_of_mpres ( - CicNotationPres.render ~prec:90 ids_to_uris - (TermContentPres.pp_ast ast) - ) - in - let render = function _::x::_ -> x | _ -> assert false in - let mpres = CicNotationPres.mpres_of_box bobj in - let s = BoxPp.render_to_string render n mpres in - remove_closed_substs s - -let obj_to_string n style prefix obj = - let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = - try Cic2acic.acic_object_of_cic_object obj - with e -> - let msg = "Cic2ACic: " ^ Printexc.to_string e in - failwith msg - in - match style with - | GrafiteAst.Declarative -> - let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in - let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in - remove_closed_substs ("\n\n" ^ - BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) - ) - | GrafiteAst.Procedural depth -> - let term_pp = term2pres (n - 8) ids_to_inner_sorts in - let lazy_term_pp = term_pp in - let obj_pp = CicNotationPp.pp_obj term_pp in - let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in - let script = Acic2Procedural.acic2procedural - ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in - "\n\n" ^ String.concat "" (List.map aux script) diff --git a/components/content_pres/objPp.mli b/components/content_pres/objPp.mli deleted file mode 100644 index de320bf14..000000000 --- a/components/content_pres/objPp.mli +++ /dev/null @@ -1,28 +0,0 @@ -(* Copyright (C) 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://helm.cs.unibo.it/ - *) - -(* columns, rendering style, name prefix, object *) -val obj_to_string: - int -> GrafiteAst.presentation_style -> string -> Cic.obj -> string diff --git a/components/content_pres/proceduralConversion.ml b/components/content_pres/proceduralConversion.ml deleted file mode 100644 index abd6fd62a..000000000 --- a/components/content_pres/proceduralConversion.ml +++ /dev/null @@ -1,61 +0,0 @@ -(* 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 - -let rec need_whd i = function - | C.ACast (_, t, _) -> need_whd i t - | C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t - | _ when i > 0 -> true - | _ -> false - -let lift k n = - let rec lift_xns k (uri, t) = uri, lift_term k t - and lift_ms k = function - | None -> None - | Some t -> Some (lift_term k t) - and lift_fix len k (id, name, i, ty, bo) = - id, name, i, lift_term k ty, lift_term (k + len) bo - and lift_cofix len k (id, name, ty, bo) = - id, name, lift_term k ty, lift_term (k + len) bo - and lift_term k = function - | C.ASort _ as t -> t - | C.AImplicit _ as t -> t - | C.ARel (id, rid, m, b) as t -> if m < k then t else C.ARel (id, rid, m + n, b) - | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (lift_xns k) xnss) - | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (lift_xns k) xnss) - | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (lift_xns k) xnss) - | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (lift_xns k) xnss) - | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (lift_ms k) mss) - | C.AAppl (id, ts) -> C.AAppl (id, List.map (lift_term k) ts) - | C.ACast (id, te, ty) -> C.ACast (id, lift_term k te, lift_term k ty) - | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl) - | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t) - | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t) - | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term (succ k) t) - | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl) - | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl) - in - lift_term k diff --git a/components/content_pres/proceduralConversion.mli b/components/content_pres/proceduralConversion.mli deleted file mode 100644 index d5ad4fd1c..000000000 --- a/components/content_pres/proceduralConversion.mli +++ /dev/null @@ -1,28 +0,0 @@ -(* 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/. - *) - -val need_whd: int -> Cic.annterm -> bool - -val lift: int -> int -> Cic.annterm -> Cic.annterm diff --git a/components/content_pres/proceduralTypes.ml b/components/content_pres/proceduralTypes.ml deleted file mode 100644 index 95fdc6e56..000000000 --- a/components/content_pres/proceduralTypes.ml +++ /dev/null @@ -1,204 +0,0 @@ -(* 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 H = HExtlib -module C = Cic -module G = GrafiteAst -module N = CicNotationPt - -(* functions to be moved ****************************************************) - -let list_map2_filter map l1 l2 = - let rec filter l = function - | [] -> l - | None :: tl -> filter l tl - | Some a :: tl -> filter (a :: l) tl - in - filter [] (List.rev_map2 map l1 l2) - -let rec list_split n l = - if n = 0 then [], l else - let l1, l2 = list_split (pred n) (List.tl l) in - List.hd l :: l1, l2 - -let cont sep a = match sep with - | None -> a - | Some sep -> sep :: a - -let list_rev_map_concat map sep a l = - let rec aux a = function - | [] -> a - | [x] -> map a x - | x :: y :: l -> aux (sep :: map a x) (y :: l) - in - aux a l - -let is_atomic = function - | C.ASort _ - | C.AConst _ - | C.AMutInd _ - | C.AMutConstruct _ - | C.AVar _ - | C.ARel _ - | C.AMeta _ - | C.AImplicit _ -> true - | _ -> false - -(****************************************************************************) - -type name = string -type what = Cic.annterm -type how = bool -type using = Cic.annterm -type count = int -type note = string -type where = (name * name) option - -type step = Note of note - | Theorem of name * what * note - | Qed of note - | Id of note - | Intros of count option * name list * note - | Cut of name * what * note - | LetIn of name * what * note - | Rewrite of how * what * where * note - | Elim of what * using option * note - | Apply of what * note - | Whd of count * note - | Branch of step list list * note - -(* annterm constructors *****************************************************) - -let mk_arel i b = Cic.ARel ("", "", i, b) - -(* grafite ast constructors *************************************************) - -let floc = H.dummy_floc - -let hole = C.AImplicit ("", Some `Hole) - -let mk_note str = G.Comment (floc, G.Note (floc, str)) - -let mk_theorem name t = - let obj = N.Theorem (`Theorem, name, t, None) in - G.Executable (floc, G.Command (floc, G.Obj (floc, obj))) - -let mk_qed = - G.Executable (floc, G.Command (floc, G.Qed floc)) - -let mk_tactic tactic = - G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), None)) - -let mk_id = - let tactic = G.IdTac floc in - mk_tactic tactic - -let mk_intros xi ids = - let tactic = G.Intros (floc, xi, ids) in - mk_tactic tactic - -let mk_cut name what = - let tactic = G.Cut (floc, Some name, what) in - mk_tactic tactic - -let mk_letin name what = - let tactic = G.LetIn (floc, what, name) in - mk_tactic tactic - -let mk_rewrite direction what where = - let direction = if direction then `RightToLeft else `LeftToRight in - let pattern, rename = match where with - | None -> (None, [], Some hole), [] - | Some (premise, name) -> (None, [premise, hole], None), [name] - in - let tactic = G.Rewrite (floc, direction, what, pattern, rename) in - mk_tactic tactic - -let mk_elim what using = - let tactic = G.Elim (floc, what, using, Some 0, []) in - mk_tactic tactic - -let mk_apply t = - let tactic = G.Apply (floc, t) in - mk_tactic tactic - -let mk_whd i = - let pattern = None, [], Some hole in - let tactic = G.Reduce (floc, `Whd, pattern) in - mk_tactic tactic - -let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None)) - -let mk_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None)) - -let mk_ob = G.Executable (floc, G.Tactical (floc, G.Branch floc, None)) - -let mk_cb = G.Executable (floc, G.Tactical (floc, G.Merge floc, None)) - -let mk_vb = G.Executable (floc, G.Tactical (floc, G.Shift floc, None)) - -(* rendering ****************************************************************) - -let rec render_step sep a = function - | Note s -> mk_note s :: a - | Theorem (n, t, s) -> mk_note s :: mk_theorem n t :: a - | Qed s -> mk_note s :: mk_qed :: a - | Id s -> mk_note s :: cont sep (mk_id :: a) - | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a) - | Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a) - | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a) - | Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a) - | Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a) - | Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a) - | Whd (c, s) -> mk_note s :: cont sep (mk_whd c :: a) - | Branch ([], s) -> a - | Branch ([ps], s) -> render_steps sep a ps - | Branch (pss, s) -> - let a = mk_ob :: a in - let body = mk_cb :: list_rev_map_concat (render_steps None) mk_vb a pss in - mk_note s :: cont sep body - -and render_steps sep a = function - | [] -> a - | [p] -> render_step sep a p - | p :: Branch ([], _) :: ps -> - render_steps sep a (p :: ps) - | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) -> - render_steps sep (render_step (Some mk_sc) a p) ps - | p :: ps -> - render_steps sep (render_step (Some mk_dot) a p) ps - -let render_steps a = render_steps None a - -(* counting *****************************************************************) - -let rec count_step a = function - | Note _ - | Theorem _ - | Qed _ -> a - | Branch (pps, _) -> List.fold_left count_steps a pps - | _ -> succ a - -and count_steps a = List.fold_left count_step a diff --git a/components/content_pres/proceduralTypes.mli b/components/content_pres/proceduralTypes.mli deleted file mode 100644 index dfd82df12..000000000 --- a/components/content_pres/proceduralTypes.mli +++ /dev/null @@ -1,65 +0,0 @@ -(* 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/. - *) - -(* functions to be moved ****************************************************) - -val list_map2_filter: ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list - -val list_split: int -> 'a list -> 'a list * 'a list - -val mk_arel: int -> string -> Cic.annterm - -val is_atomic:Cic.annterm -> bool - -(****************************************************************************) - -type name = string -type what = Cic.annterm -type how = bool -type using = Cic.annterm -type count = int -type note = string -type where = (name * name) option - -type step = Note of note - | Theorem of name * what * note - | Qed of note - | Id of note - | Intros of count option * name list * note - | Cut of name * what * note - | LetIn of name * what * note - | Rewrite of how * what * where * note - | Elim of what * using option * note - | Apply of what * note - | Whd of count * note - | Branch of step list list * note - -val render_steps: - (what, 'a, [> `Whd] as 'b, what CicNotationPt.obj, name) GrafiteAst.statement list -> - step list -> - (what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list - -val count_steps: - int -> step list -> int diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 9a0cc9f43..f3dd386a9 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -60,6 +60,10 @@ type by_continuation = | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term +let out = ref ignore + +let set_callback f = out := f + EXTEND GLOBAL: term statement; constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; @@ -674,7 +678,8 @@ EXTEND (loc,GrafiteAst.Include (iloc,buri)))) | scom = lexicon_command ; SYMBOL "." -> fun ~include_paths status -> - let status = LexiconEngine.eval_command status scom in + !out scom; + let status = LexiconEngine.eval_command status scom in status,LNone loc | EOI -> raise End_of_file ] diff --git a/components/grafite_parser/grafiteParser.mli b/components/grafite_parser/grafiteParser.mli index 6d941d5db..f38f0e5dc 100644 --- a/components/grafite_parser/grafiteParser.mli +++ b/components/grafite_parser/grafiteParser.mli @@ -38,6 +38,9 @@ type statement = LexiconEngine.status -> LexiconEngine.status * ast_statement localized_option +(* this callback is called on every lexicon command *) +val set_callback: (LexiconAst.command -> unit) -> unit + val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *) val statement: statement Grammar.Entry.e diff --git a/components/metadata/metadataDeps.ml b/components/metadata/metadataDeps.ml index f2b1d0496..330984350 100644 --- a/components/metadata/metadataDeps.ml +++ b/components/metadata/metadataDeps.ml @@ -101,6 +101,34 @@ let topological_sort ~dbd uris = Topo.topological_sort uris (fun uri -> fst (List.split (direct_deps ~dbd uri))) +let sorted_uris_of_baseuri ~dbd baseuri = + let sql_pat = + Pcre.replace ~rex:(Pcre.regexp "_") ~templ:"\\_" baseuri ^ "%" + in + let query = + Printf.sprintf + ("SELECT source FROM %s WHERE source LIKE \"%s\" UNION "^^ + "SELECT source FROM %s WHERE source LIKE \"%s\"") + (MetadataTypes.name_tbl ()) sql_pat + MetadataTypes.library_name_tbl sql_pat + in + let result = HMysql.exec dbd query in + let map cols = match cols.(0) with + | Some s -> UriManager.uri_of_string s + | _ -> assert false + in + let uris = HMysql.map result map in + let sorted_uris = topological_sort ~dbd uris in + let filter_map uri = + let s = + Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:"" + (UriManager.string_of_uri uri) + in + try ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s); None + with Not_found -> Some (UriManager.uri_of_string s) + in + HExtlib.filter_map filter_map sorted_uris + module DepGraph = struct module UriTbl = UriManager.UriHashtbl diff --git a/components/metadata/metadataDeps.mli b/components/metadata/metadataDeps.mli index f5a6ac22e..4def88d9e 100644 --- a/components/metadata/metadataDeps.mli +++ b/components/metadata/metadataDeps.mli @@ -38,6 +38,9 @@ val inverse_deps: val topological_sort: dbd:HMysql.dbd -> UriManager.uri list -> UriManager.uri list +val sorted_uris_of_baseuri: + dbd:HMysql.dbd -> string -> UriManager.uri list + (** Representation of a (lazy) dependency graph. * Imperative data structure. *) module DepGraph: diff --git a/matita/.depend b/matita/.depend index 8dd26ce54..8b943bb3d 100644 --- a/matita/.depend +++ b/matita/.depend @@ -11,13 +11,15 @@ lablGraphviz.cmx: lablGraphviz.cmi matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \ - matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi matitacLib.cmi + matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi \ + applyTransformation.cmi matitacLib.cmi matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \ - matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi + matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitacLib.cmi matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \ - matitacLib.cmi gragrep.cmi + matitacLib.cmi matitaWiki.cmo gragrep.cmi matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \ - matitacLib.cmx gragrep.cmx + matitacLib.cmx matitaWiki.cmx gragrep.cmx matitadep.cmo: matitaInit.cmi matitadep.cmi matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi @@ -51,9 +53,11 @@ matitaMathView.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \ matitaMisc.cmo: buildTimeConf.cmi matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ - matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi + matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi \ + applyTransformation.cmi matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \ - matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx + matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ buildTimeConf.cmi matitaprover.cmi matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ @@ -66,6 +70,10 @@ matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaMisc.cmx \ applyTransformation.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi +matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ + buildTimeConf.cmi applyTransformation.cmi +matitaWiki.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ + buildTimeConf.cmx applyTransformation.cmx matitaGtkMisc.cmi: matitaGeneratedGui.cmo matitaGui.cmi: matitaGuiTypes.cmi matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo diff --git a/matita/.depend.opt b/matita/.depend.opt index 7860c2d16..b0119369b 100644 --- a/matita/.depend.opt +++ b/matita/.depend.opt @@ -11,13 +11,15 @@ lablGraphviz.cmx: lablGraphviz.cmi matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \ - matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi matitacLib.cmi + matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi \ + applyTransformation.cmi matitacLib.cmi matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \ - matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi + matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitacLib.cmi matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \ - matitacLib.cmi gragrep.cmi + matitacLib.cmi matitaWiki.cmx gragrep.cmi matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \ - matitacLib.cmx gragrep.cmx + matitacLib.cmx matitaWiki.cmx gragrep.cmx matitadep.cmo: matitaInit.cmi matitadep.cmi matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi @@ -51,9 +53,11 @@ matitaMathView.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \ matitaMisc.cmo: buildTimeConf.cmi matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ - matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi + matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi \ + applyTransformation.cmi matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \ - matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx + matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ buildTimeConf.cmi matitaprover.cmi matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ @@ -66,6 +70,10 @@ matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaMisc.cmx \ applyTransformation.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi +matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ + buildTimeConf.cmi applyTransformation.cmi +matitaWiki.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ + buildTimeConf.cmx applyTransformation.cmx matitaGtkMisc.cmi: matitaGeneratedGui.cmx matitaGui.cmi: matitaGuiTypes.cmi matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmx diff --git a/matita/Makefile b/matita/Makefile index ed5ebb320..1b73fe2da 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -34,9 +34,9 @@ CMOS = \ matitaInit.cmo \ matitaExcPp.cmo \ matitaEngine.cmo \ + applyTransformation.cmo \ matitacLib.cmo \ matitaprover.cmo \ - applyTransformation.cmo \ matitaGtkMisc.cmo \ matitaScript.cmo \ matitaGeneratedGui.cmo \ @@ -52,8 +52,8 @@ CCMOS = \ matitaInit.cmo \ matitaExcPp.cmo \ matitaEngine.cmo \ - matitacLib.cmo \ applyTransformation.cmo \ + matitacLib.cmo \ matitaWiki.cmo \ matitaprover.cmo \ $(NULL) diff --git a/matita/applyTransformation.ml b/matita/applyTransformation.ml index f27da2caa..0678887ce 100644 --- a/matita/applyTransformation.ml +++ b/matita/applyTransformation.ml @@ -97,3 +97,60 @@ let txt_of_cic_sequent_conclusion size metasenv sequent = let txt_of_cic_term size metasenv context t = let fake_sequent = (-1,context,t) in txt_of_cic_sequent_conclusion size metasenv fake_sequent + +(****************************************************************************) +(* txt_of_cic_object: IMPROVE ME *) + +let remove_closed_substs s = + Pcre.replace ~pat:"{...}" ~templ:"" s + +let term2pres n ids_to_inner_sorts annterm = + let ast, ids_to_uris = + TermAcicContent.ast_of_acic ids_to_inner_sorts annterm + in + let bobj = + CicNotationPres.box_of_mpres ( + CicNotationPres.render ~prec:90 ids_to_uris + (TermContentPres.pp_ast ast) + ) + in + let render = function _::x::_ -> x | _ -> assert false in + let mpres = CicNotationPres.mpres_of_box bobj in + let s = BoxPp.render_to_string render n mpres in + remove_closed_substs s + +let txt_of_cic_object n style prefix obj = + let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = + try Cic2acic.acic_object_of_cic_object obj + with e -> + let msg = "Cic2ACic: " ^ Printexc.to_string e in + failwith msg + in + match style with + | GrafiteAst.Declarative -> + let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in + let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in + remove_closed_substs ("\n\n" ^ + BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) + ) + | GrafiteAst.Procedural depth -> + let term_pp = term2pres (n - 8) ids_to_inner_sorts in + let lazy_term_pp = term_pp in + let obj_pp = CicNotationPp.pp_obj term_pp in + let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in + let script = Acic2Procedural.acic2procedural + ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in + "\n\n" ^ String.concat "" (List.map aux script) + +let txt_of_inline_macro style suri prefix = + let dbd = LibraryDb.instance () in + let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in + let map uri = + try txt_of_cic_object 78 style prefix (* FG: mi pare meglio 78 *) + (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri)) + with + | e -> + Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" + (UriManager.string_of_uri uri) (Printexc.to_string e) + in + String.concat "\n\n" (List.map map sorted_uris) diff --git a/matita/applyTransformation.mli b/matita/applyTransformation.mli index 218a92ca9..8e0b19361 100644 --- a/matita/applyTransformation.mli +++ b/matita/applyTransformation.mli @@ -62,3 +62,10 @@ val txt_of_cic_sequent: val txt_of_cic_sequent_conclusion: int -> Cic.metasenv -> Cic.conjecture -> string +(* columns, rendering style, name prefix, object *) +val txt_of_cic_object: + int -> GrafiteAst.presentation_style -> string -> Cic.obj -> string + +(* presentation_style, uri or baseuri, name prefix *) +val txt_of_inline_macro: + GrafiteAst.presentation_style -> string -> string -> string diff --git a/matita/matita.ml b/matita/matita.ml index 46926ea9b..5717b710a 100644 --- a/matita/matita.ml +++ b/matita/matita.ml @@ -173,7 +173,7 @@ let _ = addDebugItem "Print current proof (natural language) to stderr" (fun _ -> prerr_endline - (ObjPp.obj_to_string 120 GrafiteAst.Declarative "" + (ApplyTransformation.txt_of_cic_object 120 GrafiteAst.Declarative "" (match (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status with diff --git a/matita/matitaEngine.ml b/matita/matitaEngine.ml index 9778f0900..191c60bb1 100644 --- a/matita/matitaEngine.ml +++ b/matita/matitaEngine.ml @@ -100,6 +100,10 @@ let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status exception TryingToAdd of string +let out = ref ignore + +let set_callback f = out := f + let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false) ?do_heavy_checks ?clean_baseuri ?(enforce_no_new_aliases=true) ?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb @@ -122,6 +126,7 @@ let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false) loop lexicon_status grafite_status (((grafite_status,lexicon_status),None)::statuses) | GrafiteParser.LSome ast -> + !out ast; cb grafite_status ast; let new_statuses = eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status diff --git a/matita/matitaEngine.mli b/matita/matitaEngine.mli index 71bfff0b8..83b549ec4 100644 --- a/matita/matitaEngine.mli +++ b/matita/matitaEngine.mli @@ -61,3 +61,5 @@ val eval_from_stream : (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option ) list +(* this callback is called on every grafite command *) +val set_callback: (GrafiteParser.ast_statement -> unit) -> unit diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index f124bd5c9..8ab94d979 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -289,54 +289,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); [], "", parsed_text_length | TA.Inline (_,style,suri,prefix) -> - let dbd = LibraryDb.instance () in - let uris = - let sql_pat = - (Pcre.replace ~rex:(Pcre.regexp "_") ~templ:"\\_" suri) ^ "%" in - let query = - sprintf ("SELECT source FROM %s WHERE source LIKE \"%s\" UNION "^^ - "SELECT source FROM %s WHERE source LIKE \"%s\"") - (MetadataTypes.name_tbl ()) sql_pat - MetadataTypes.library_name_tbl sql_pat in - let result = HMysql.exec dbd query in - HMysql.map result - (function cols -> - match cols.(0) with - Some s -> UriManager.uri_of_string s - | _ -> assert false) - in -prerr_endline "Inizio sorting"; - let sorted_uris = MetadataDeps.topological_sort ~dbd uris in -prerr_endline "Fine sorting"; - let sorted_uris_without_xpointer = - HExtlib.filter_map - (function uri -> - let s = - Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:"" - (UriManager.string_of_uri uri) in - try - ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s); - None - with - Not_found -> - Some (UriManager.uri_of_string s) - ) sorted_uris - in - let declarative = - String.concat "\n\n" - (List.map - (fun uri -> -prerr_endline ("Stampo " ^ UriManager.string_of_uri uri); - try - ObjPp.obj_to_string 78 style prefix (* FG: mi pare meglio 78 *) - (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri)) - with - | e (* BRRRRRRRRR *) -> - Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" - (UriManager.string_of_uri uri) (Printexc.to_string e) - ) sorted_uris_without_xpointer) - in - [],declarative,String.length parsed_text + let str = ApplyTransformation.txt_of_inline_macro style suri prefix in + [], str, String.length parsed_text and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index ba9af1302..52ad776e7 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -31,6 +31,10 @@ open GrafiteTypes exception AttemptToInsertAnAlias +let out = ref ignore + +let set_callback f = out := f + let pp_ast_statement = GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) @@ -126,8 +130,14 @@ let rec interactive_loop () = "matita.includes")) with | GrafiteEngine.Drop -> pp_ocaml_mode () - | GrafiteEngine.Macro (floc,_) -> - let x, y = HExtlib.loc_of_floc floc in + | GrafiteEngine.Macro (floc, f) -> + begin match snd (f []) with + | GrafiteAst.Inline (_, style, suri, prefix) -> + let str = ApplyTransformation.txt_of_inline_macro style suri prefix in + !out str + | _ -> () + end; + let x, y = HExtlib.loc_of_floc floc in HLog.error (sprintf "A macro has been found in a script at %d-%d" x y); interactive_loop () diff --git a/matita/matitacLib.mli b/matita/matitacLib.mli index 636c51d57..5e8a2635b 100644 --- a/matita/matitacLib.mli +++ b/matita/matitacLib.mli @@ -35,3 +35,6 @@ val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit otherwise it performs the clean-up without exiting *) val clean_exit : int option -> unit + +(* this callback is called on the expansion of every inline macro *) +val set_callback: (string -> unit) -> unit diff --git a/matita/tests/letrecand.ma b/matita/tests/letrecand.ma index 017c2ae89..d9dfec329 100644 --- a/matita/tests/letrecand.ma +++ b/matita/tests/letrecand.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/letrecand". +set "baseuri" "cic:/matita/tests/letrecand". include "nat/nat.ma". @@ -71,4 +71,4 @@ qed. lemma test_dispari2: dispari2 (S O). simplify. constructor 1. -qed. \ No newline at end of file +qed.