cicNotationPres.cmi box.cmi content2pres.cmi
content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
cicNotationPres.cmx box.cmx content2pres.cmi
-content2Procedural.cmo: content2Procedural.cmi
-content2Procedural.cmx: content2Procedural.cmi
-objPp.cmo: termContentPres.cmi content2pres.cmi content2Procedural.cmi \
- cicNotationPres.cmi boxPp.cmi objPp.cmi
-objPp.cmx: termContentPres.cmx content2pres.cmx content2Procedural.cmx \
- cicNotationPres.cmx boxPp.cmx objPp.cmi
+cicClassify.cmo: cicClassify.cmi
+cicClassify.cmx: cicClassify.cmi
+proceduralTypes.cmo: proceduralTypes.cmi
+proceduralTypes.cmx: proceduralTypes.cmi
+content2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi \
+ content2Procedural.cmi
+content2Procedural.cmx: proceduralTypes.cmx cicClassify.cmx \
+ content2Procedural.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 \
cicNotationPres.mli \
boxPp.mli \
content2pres.mli \
- content2Procedural.mli \
+ cicClassify.mli \
+ proceduralTypes.mli \
+ acic2Procedural.mli \
objPp.mli \
sequent2pres.mli \
$(NULL)
--- /dev/null
+(* 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 L = CicClassify
+module P = ProceduralTypes
+module D = Deannotate
+module DTI = DoubleTypeInference
+module TC = CicTypeChecker
+module U = CicUniv
+module UM = UriManager
+module Obj = LibraryObjects
+module HObj = HelmLibraryObjects
+module A = Cic2acic
+module T = CicUtil
+
+type status = {
+ sorts : (Cic.id, Cic2acic.sort_kind) Hashtbl.t;
+ types : (C.id, A.anntypes) Hashtbl.t;
+ prefix: string;
+ max_depth: int option;
+ depth: int;
+ entries: C.context;
+ intros: string list
+}
+
+(* helpers ******************************************************************)
+
+let cic = D.deannotate_term
+
+let split2_last l1 l2 =
+ let n = pred (List.length l1) in
+ let before1, after1 = P.list_split n l1 in
+ let before2, after2 = P.list_split n l2 in
+ before1, before2, List.hd after1, List.hd after2
+
+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 next st = {st with depth = succ st.depth; intros = []}
+
+let add st entry intro =
+ {st with entries = entry :: st.entries; intros = intro :: st.intros}
+
+let test_depth st =
+ 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"
+
+let get_itype st v =
+ let id = T.id_of_annterm v in
+ try Some ((Hashtbl.find st.types id).A.annsynthesized)
+ with Not_found -> None
+
+(* proof construction *******************************************************)
+
+let unused_premise = "UNUSED"
+
+let get_intro name t = match name with
+ | C.Anonymous -> unused_premise
+ | C.Name s ->
+ if DTI.does_not_occur 1 (cic t) then unused_premise else s
+
+let mk_intros st script =
+ if st.intros = [] then script else
+ let count = List.length st.intros in
+ P.Intros (Some count, List.rev st.intros, "") :: script
+
+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 mk_premise = function
+ | C.ARel (_, _, _, binder) -> binder
+ | _ -> assert false
+
+let rec mk_fwd_proof st dtext name = function
+ | C.AAppl (_, hd :: tl) as v ->
+ if is_rewrite_right hd then
+ let what, where = List.nth tl 5, List.nth tl 3 in
+ let premise = mk_premise where in
+ [P.Rewrite (true, what, Some (premise, name), dtext)]
+ else if is_rewrite_left hd then
+ let what, where = List.nth tl 5, List.nth tl 3 in
+ let premise = mk_premise where in
+ [P.Rewrite (false, what, Some (premise, name), dtext)]
+ else begin match get_itype st v with
+ | Some ty ->
+ let qs = [[P.Id ""]; mk_proof (next st) v] in
+ [P.Branch (qs, ""); P.Cut (name, ty, dtext)]
+ | None ->
+ let ty, _ = TC.type_of_aux' [] st.entries (cic hd) U.empty_ugraph in
+ let (classes, rc) as h = L.classify ty in
+ let text = Printf.sprintf "%u %s" (List.length classes) (L.to_string h) in
+ [P.LetIn (name, v, dtext ^ text)]
+ end
+ | v ->
+ [P.LetIn (name, v, dtext)]
+
+and mk_proof st = function
+ | C.ALambda (_, name, v, t) ->
+ let entry = Some (name, C.Decl (cic v)) in
+ let intro = get_intro name t in
+ mk_proof (add st entry intro) t
+ | C.ALetIn (_, name, v, t) as what ->
+ let proceed, dtext = test_depth st in
+ let script = if proceed then
+ let intro = get_intro name t in
+ let q = mk_proof (next st) t in
+ List.rev_append (mk_fwd_proof st dtext intro v) q
+ else
+ [P.Apply (what, dtext)]
+ in
+ mk_intros st script
+ | C.ARel _ as what ->
+ let _, dtext = test_depth st in
+ let script = [P.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.entries (cic hd) U.empty_ugraph in
+ let (classes, rc) as h = L.classify ty in
+ let synth = L.S.singleton 0 in
+ let text = Printf.sprintf "%u %s" (List.length classes) (L.to_string h) in
+ match rc with
+ | Some (i, j) when i > 1 ->
+ let classes, tl, _, what = split2_last classes tl in
+ let synth = L.S.add 1 synth in
+ let qs = mk_bkd_proofs (next st) synth classes tl in
+ if is_rewrite_right hd then
+ [P.Rewrite (false, what, None, dtext); P.Branch (qs, "")]
+ else if is_rewrite_left hd then
+ [P.Rewrite (true, what, None, dtext); P.Branch (qs, "")]
+ else
+ let using = Some hd in
+ [P.Elim (what, using, dtext ^ text); P.Branch (qs, "")]
+ | _ ->
+ let qs = mk_bkd_proofs (next st) synth classes tl in
+ [P.Apply (hd, dtext ^ text); P.Branch (qs, "")]
+ else
+ [P.Apply (t, dtext)]
+ in
+ mk_intros st script
+ | t ->
+ let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
+ let script = [P.Note text] in
+ mk_intros st script
+
+and mk_bkd_proofs st synth classes ts =
+ let _, dtext = test_depth st in
+ let aux inv v =
+ if L.overlaps synth inv then None else
+ if L.S.is_empty inv then Some (mk_proof st v) else
+ Some [P.Apply (v, dtext ^ "dependent")]
+ in
+ P.list_map2_filter aux classes ts
+
+(* object costruction *******************************************************)
+
+let mk_obj st = function
+ | C.AConstant (_, _, s, Some v, t, [], _) ->
+ let ast = mk_proof st v in
+ let count = P.count_steps 0 ast in
+ let text = Printf.sprintf "tactics: %u" count in
+ P.Theorem (s, t, text) :: ast @ [P.Qed ""]
+ | _ -> assert false
+
+(* interface functions ******************************************************)
+
+let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types prefix aobj =
+ let st = {
+ sorts = ids_to_inner_sorts;
+ types = ids_to_inner_types;
+ prefix = prefix;
+ max_depth = None;
+ depth = 0;
+ entries = [];
+ intros = []
+ } in
+ prerr_endline "Level 2 transformation";
+ let steps = mk_obj st aobj in
+ prerr_endline "grafite rendering";
+ List.rev (P.render_steps [] steps)
--- /dev/null
+(* 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 ->
+ string -> Cic.annobj ->
+ (Cic.annterm, Cic.annterm,
+ Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
+ GrafiteAst.statement list
+
--- /dev/null
+(* 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 CS = CicSubstitution
+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 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 t =
+ let rec aux a n = function
+ | C.Prod (_, v, t) -> aux (v :: a) (succ n) t
+ | C.Cast (t, v) -> aux a n t
+ | C.LetIn (_, v, t) -> aux a n (CS.subst v t)
+ | v -> v :: a, n
+ in
+ aux [] 0 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 t =
+ let vs, h = split 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 = S.union (fst b.(j)) 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
+ let unused, inverse = b.(j) in
+ b.(j) <- unused, S.add i inverse;
+ 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
+
+let aclassify t = classify (D.deannotate_term t)
+
+let overlaps s1 s2 =
+ let predicate x = S.mem x s1 in
+ S.exists predicate s2
--- /dev/null
+(* 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.term -> S.t list * conclusion
+
+val aclassify: Cic.annterm -> S.t list * conclusion
+
+val to_string: S.t list * conclusion -> string
+
+val overlaps: S.t -> S.t -> bool
+++ /dev/null
-(* 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 U = UriManager
-module C = Content
-module G = GrafiteAst
-module N = CicNotationPt
-
-(* functions to be moved ****************************************************)
-
-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
-
-(****************************************************************************)
-
-type name = string
-type what = Cic.annterm
-type using = Cic.annterm
-type count = int
-type note = string
-
-type step = Note of note
- | Theorem of name * what * note
- | Qed of note
- | Intros of count option * name list * note
- | Elim of what * using option * note
- | LetIn of name * what * note
- | Apply of what * note
- | Exact of what * note
- | Branch of step list list * note
-
-(* annterm constructors *****************************************************)
-
-let mk_arel i b = Cic.ARel ("", "", i, b)
-
-(* level 2 transformation ***************************************************)
-
-let mk_name = function
- | Some name -> name
- | None -> "UNUSED" (**)
-
-let mk_intros_arg = function
- | `Declaration {C.dec_name = name}
- | `Hypothesis {C.dec_name = name}
- | `Definition {C.def_name = name} -> mk_name name
- | `Joint _ -> assert false
- | `Proof _ -> assert false
-
-let mk_intros_args pc = List.map mk_intros_arg pc
-
-let split_inductive n tl =
- let l1, l2 = list_split (int_of_string n) tl in
- List.hd (List.rev l2), l1
-
-let rec mk_apply_term aref ac ds cargs =
- let step0 = mk_arg true (ac, [], ds) (List.hd cargs) in
- let ac, row, ds = List.fold_left (mk_arg false) step0 (List.tl cargs) in
- ac, ds, Cic.AAppl (aref, List.rev row)
-
-and mk_delta ac ds = match ac with
- | p :: ac ->
- let cmethod = p.C.proof_conclude.C.conclude_method in
- let cargs = p.C.proof_conclude.C.conclude_args in
- let capply = p.C.proof_apply_context in
- let ccont = p.C.proof_context in
- let caref = p.C.proof_conclude.C.conclude_aref in
- begin match cmethod with
- | "Exact"
- | "Apply" when ccont = [] && capply = [] ->
- let ac, ds, what = mk_apply_term caref ac ds cargs in
- let name = "PREVIOUS" in
- ac, mk_arel 1 name, LetIn (name, what, "") :: ds
- | _ -> ac, mk_arel 1 "COMPOUND", ds
- end
- | _ -> assert false
-
-and mk_arg first (ac, row, ds) = function
- | C.Lemma {C.lemma_id = aref; C.lemma_uri = uri} ->
- let t = match CicUtil.term_of_uri (U.uri_of_string uri) with
- | Cic.Const (uri, _) -> Cic.AConst (aref, uri, [])
- | Cic.MutConstruct (uri, tno, cno, _) ->
- Cic.AMutConstruct (aref, uri, tno, cno, [])
- | _ -> assert false
- in
- ac, t :: row, ds
- | C.Premise {C.premise_n = Some i; C.premise_binder = Some b} ->
- ac, mk_arel i b :: row, ds
- | C.Premise {C.premise_n = None; C.premise_binder = None} ->
- let ac, arg, ds = mk_delta ac ds in
- ac, arg :: row, ds
- | C.Term t when first -> ac, t :: row, ds
- | C.Term _ -> ac, Cic.AImplicit ("", None) :: row, ds
- | C.Premise _ -> assert false
- | C.ArgMethod _ -> assert false
- | C.ArgProof _ -> assert false
- | C.Aux _ -> assert false
-
-let rec mk_proof p =
- let names = mk_intros_args p.C.proof_context in
- let count = List.length names in
- if count > 0 then Intros (Some count, names, "") :: mk_proof_body p
- else mk_proof_body p
-
-and mk_proof_body p =
- let cmethod = p.C.proof_conclude.C.conclude_method in
- let cargs = p.C.proof_conclude.C.conclude_args in
- let capply = p.C.proof_apply_context in
- let caref = p.C.proof_conclude.C.conclude_aref in
- match cmethod, cargs with
- | "Intros+LetTac", [C.ArgProof p] -> mk_proof p
- | "ByInduction", C.Aux n :: C.Term (Cic.AAppl (_, using :: _)) :: tl ->
- let whatm, ms = split_inductive n tl in (* actual rx params here *)
- let _, row, ds = mk_arg true (List.rev capply, [], []) whatm in
- let what, qs = List.hd row, mk_subproofs ms in
- List.rev ds @ [Elim (what, Some using, ""); Branch (qs, "")]
- | "Apply", _ ->
- let ac, ds, what = mk_apply_term caref (List.rev capply) [] cargs in
- let qs = List.map mk_proof ac in
- List.rev ds @ [Apply (what, ""); Branch (qs, "")]
- | _ ->
- let text =
- Printf.sprintf "UNEXPANDED %s %u" cmethod (List.length cargs)
- in [Note text]
-
-and mk_subproofs cargs =
- let mk_subproof proofs = function
- | C.ArgProof ({C.proof_name = Some n} as p) ->
- (Note n :: mk_proof p) :: proofs
- | C.ArgProof ({C.proof_name = None} as p) ->
- (Note "" :: mk_proof p) :: proofs
- | _ -> proofs
- in
- List.rev (List.fold_left mk_subproof [] cargs)
-
-let mk_obj ids_to_inner_sorts prefix (_, params, xmenv, obj) =
- if List.length params > 0 || xmenv <> None then assert false;
- match obj with
- | `Def (C.Const, t, `Proof ({C.proof_name = Some name} as p)) ->
- Theorem (name, t, "") :: mk_proof p @ [Qed ""]
- | _ -> assert false
-
-(* grafite ast constructors *************************************************)
-
-let floc = H.dummy_floc
-
-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_intros xi ids =
- let tactic = G.Intros (floc, xi, ids) in
- mk_tactic tactic
-
-let mk_elim what using =
- let tactic = G.Elim (floc, what, using, Some 0, []) in
- mk_tactic tactic
-
-let mk_letin name what =
- let tactic = G.LetIn (floc, what, name) in
- mk_tactic tactic
-
-let mk_apply t =
- let tactic = G.Apply (floc, t) in
- mk_tactic tactic
-
-let mk_exact t =
- let tactic = G.Exact (floc, t) 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
- | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a)
- | Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a)
- | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a)
- | Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a)
- | Exact (t, s) -> mk_note s :: cont sep (mk_exact t :: a)
- | Branch ([], s) -> a
- | Branch ([ps], s) -> render_steps a ps
- | Branch (pss, s) ->
- let a = mk_ob :: a in
- let body = mk_cb :: list_rev_map_concat render_steps mk_vb a pss in
- mk_note s :: cont sep body
-
-and render_steps a = function
- | [] -> a
- | [p] -> render_step None a p
- | (Note _ | Theorem _ | Qed _ as p) :: ps ->
- render_steps (render_step None a p) ps
- | p :: ((Branch ([], _) :: _) as ps) ->
- render_steps (render_step None a p) ps
- | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) ->
- render_steps (render_step (Some mk_sc) a p) ps
- | p :: ps ->
- render_steps (render_step (Some mk_dot) a p) ps
-
-(* interface functions ******************************************************)
-
-let content2procedural ~ids_to_inner_sorts prefix cobj =
- prerr_endline "Level 2 transformation";
- let steps = mk_obj ids_to_inner_sorts prefix cobj in
- prerr_endline "grafite rendering";
- List.rev (render_steps [] steps)
-
+++ /dev/null
-(* Copyright (C) 2000, 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 content2procedural:
- ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> string ->
- Cic.annterm Content.cobj ->
- (Cic.annterm, Cic.annterm,
- Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
- GrafiteAst.statement list
-
let obj_to_string n style prefix obj =
let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = Cic2acic.acic_object_of_cic_object obj in
- let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj 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)
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 = Content2Procedural.content2procedural ~ids_to_inner_sorts prefix cobj in
+ let script = Acic2Procedural.acic2procedural
+ ~ids_to_inner_sorts ~ids_to_inner_types prefix aobj in
"\n\n" ^ String.concat "" (List.map aux script)
--- /dev/null
+(* 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
+
+(****************************************************************************)
+
+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
+ | 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 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 hole = C.AImplicit ("", Some `Hole) in
+ 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_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)
+ | Branch ([], s) -> a
+ | Branch ([ps], s) -> render_steps a ps
+ | Branch (pss, s) ->
+ let a = mk_ob :: a in
+ let body = mk_cb :: list_rev_map_concat render_steps mk_vb a pss in
+ mk_note s :: cont sep body
+
+and render_steps a = function
+ | [] -> a
+ | [p] -> render_step None a p
+ | (Note _ | Theorem _ | Qed _ as p) :: ps ->
+ render_steps (render_step None a p) ps
+ | p :: ((Branch ([], _) :: _) as ps) ->
+ render_steps (render_step None a p) ps
+ | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) ->
+ render_steps (render_step (Some mk_sc) a p) ps
+ | p :: ps ->
+ render_steps (render_step (Some mk_dot) a p) ps
+
+(* 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
--- /dev/null
+(* 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
+
+(****************************************************************************)
+
+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
+ | Branch of step list list * note
+
+val render_steps:
+ (what, 'a, '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
| LetIn of loc * 'term * 'ident
| Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern
| Reflexivity of loc
+ | Rename of loc * 'ident list * 'ident list
| Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
| Rewrite of loc * direction * 'term *
- ('term, 'lazy_term, 'ident) pattern
+ ('term, 'lazy_term, 'ident) pattern * 'ident list
| Right of loc
| Ring of loc
| Split of loc
| `Whd -> "whd"
let pp_tactic_pattern ~term_pp ~lazy_term_pp (what, hyp, goal) =
+ if what = None && hyp = [] && goal = None then "" else
let what_text =
match what with
| None -> ""
let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in
function
| Absurd (_, term) -> "absurd" ^ term_pp term
- | Apply (_, term) -> "apply " ^ term_pp term
+ | Apply (_, term) -> "apply (" ^ term_pp term ^ ")" (* FG: rm parentheses *)
| ApplyS (_, term, params) ->
"applyS " ^ term_pp term ^
String.concat " "
| Constructor (_,n) -> "constructor " ^ string_of_int n
| Contradiction _ -> "contradiction"
| Cut (_, ident, term) ->
- "cut " ^ term_pp term ^
+ "cut (" ^ term_pp term ^ ")" ^ (* FG: rm parentheses *)
(match ident with None -> "" | Some id -> " as " ^ id)
| Decompose (_, [], what, names) ->
sprintf "decompose %s%s" (opt_string_pp what) (pp_intros_specs (None, names))
| Demodulate _ -> "demodulate"
| Destruct (_, term) -> "destruct " ^ term_pp term
| Elim (_, term, using, num, idents) ->
- sprintf "elim " ^ term_pp term ^
+ sprintf "elim (" ^ term_pp term ^ ")" ^ (* FG: rm parentheses *)
(match using with None -> "" | Some term -> " using " ^ term_pp term)
^ pp_intros_specs (num, idents)
| ElimType (_, term, using, num, idents) ->
(match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
(match ident_opt with None -> "" | Some ident -> " as " ^ ident)
| Left _ -> "left"
- | LetIn (_, term, ident) -> sprintf "letin %s \\def %s" ident (term_pp term)
+ | LetIn (_, term, ident) ->
+ sprintf "letin %s \\def %s" ident ("(" ^ term_pp term ^ ")") (* FG: rm parentheses *)
| Reduce (_, kind, pat) ->
sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat)
| Reflexivity _ -> "reflexivity"
+ | Rename (_, froms, tos) ->
+ sprintf "rename %s as %s" (pp_idents froms) (pp_idents tos)
| Replace (_, pattern, t) ->
sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t)
- | Rewrite (_, pos, t, pattern) ->
- sprintf "rewrite %s %s %s"
+ | Rewrite (_, pos, t, pattern, names) ->
+ sprintf "rewrite %s %s %s%s"
(if pos = `LeftToRight then ">" else "<")
- (term_pp t)
+ ("(" ^ term_pp t ^ ")") (* FG: rm parentheses *)
(pp_tactic_pattern pattern)
+ (if names = [] then "" else " as " ^ pp_idents names)
| Right _ -> "right"
| Ring _ -> "ring"
| Split _ -> "split"
| `Unfold what -> Tactics.unfold ~pattern what
| `Whd -> Tactics.whd ~pattern)
| GrafiteAst.Reflexivity _ -> Tactics.reflexivity
+ | GrafiteAst.Rename (_, froms, tos) -> Tactics.rename ~froms ~tos
| GrafiteAst.Replace (_, pattern, with_what) ->
Tactics.replace ~pattern ~with_what
- | GrafiteAst.Rewrite (_, direction, t, pattern) ->
- EqualityTactics.rewrite_tac ~direction ~pattern t
+ | GrafiteAst.Rewrite (_, direction, t, pattern, names) ->
+ EqualityTactics.rewrite_tac ~direction ~pattern t names
| GrafiteAst.Right _ -> Tactics.right
| GrafiteAst.Ring _ -> Tactics.ring
| GrafiteAst.Split _ -> Tactics.split
metasenv,GrafiteAst.Reduce(loc, red_kind, pattern)
| GrafiteAst.Reflexivity loc ->
metasenv,GrafiteAst.Reflexivity loc
+ | GrafiteAst.Rename (loc, froms, tos) ->
+ metasenv,GrafiteAst.Rename (loc, froms, tos)
| GrafiteAst.Replace (loc, pattern, with_what) ->
let pattern = disambiguate_pattern pattern in
let with_what = disambiguate_lazy_term with_what in
metasenv,GrafiteAst.Replace (loc, pattern, with_what)
- | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
+ | GrafiteAst.Rewrite (loc, dir, t, pattern, names) ->
let metasenv,term = disambiguate_term context metasenv t in
let pattern = disambiguate_pattern pattern in
- metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern)
+ metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern, names)
| GrafiteAst.Right loc ->
metasenv,GrafiteAst.Right loc
| GrafiteAst.Ring loc ->
GrafiteAst.Reduce (loc, kind, p)
| IDENT "reflexivity" ->
GrafiteAst.Reflexivity loc
+ | IDENT "rename"; froms = ident_list0; "as"; tos = ident_list0 ->
+ GrafiteAst.Rename (loc, froms, tos)
| IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Replace (loc, p, t)
- | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec ->
+ | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
+ xnames = OPT [ "as"; n = ident_list0 -> n ] ->
let (pt,_,_) = p in
if pt <> None then
raise
(CicNotationParser.Parse_error
"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
else
- GrafiteAst.Rewrite (loc, d, t, p)
+ let n = match xnames with None -> [] | Some names -> names in
+ GrafiteAst.Rewrite (loc, d, t, p, n)
| IDENT "right" ->
GrafiteAst.Right loc
| IDENT "ring" ->
ProofEngineTypes.apply_tactic
(EqualityTactics.rewrite_tac ~direction:`RightToLeft
~pattern:(ProofEngineTypes.conclusion_pattern None)
- (Cic.Meta(newmeta,irl)))
+ (Cic.Meta(newmeta,irl)) [])
(proof'',goal)
in
let goal = match goals with [g] -> g | _ -> assert false in
(EqualityTactics.rewrite_simpl_tac
~direction:`RightToLeft
~pattern:(ProofEngineTypes.conclusion_pattern None)
- term)
+ term [])
~continuation:
(IntroductionTactics.constructor_tac ~n:1)))) status
| _ -> fail "not an equality"
(EqualityTactics.rewrite_simpl_tac
~direction:`LeftToRight
~pattern:(ProofEngineTypes.conclusion_pattern None)
- term)
+ term [])
~continuation:EqualityTactics.reflexivity_tac)
])
status
module DTI = DoubleTypeInference
module HEL = HExtlib
-let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality =
- let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
- =
+let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
+ let _rewrite_tac status =
assert (wanted = None); (* this should be checked syntactically *)
let proof,goal = status in
let curi, metasenv, pbo, pty = proof in
match hyps_pat with
he::(_::_ as tl) ->
PET.apply_tactic
- (Tacticals.then_
+ (T.then_
(rewrite_tac ~direction
~pattern:(None,[he],None) equality)
(rewrite_tac ~direction ~pattern:(None,tl,concl_pat)
) status
| [_] as hyps_pat when concl_pat <> None ->
PET.apply_tactic
- (Tacticals.then_
+ (T.then_
(rewrite_tac ~direction
~pattern:(None,hyps_pat,None) equality)
(rewrite_tac ~direction ~pattern:(None,[],concl_pat)
let dummy = "dummy" in
Some arg,false,
(fun ~term typ ->
- Tacticals.seq
+ T.seq
~tactics:
- [ProofEngineStructuralRules.rename name dummy;
+ [PESR.rename [name] [dummy];
P.letin_tac
~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term;
- ProofEngineStructuralRules.clearbody name;
+ PESR.clearbody name;
ReductionTactics.change_tac
~pattern:
(None,[name,Cic.Implicit (Some `Hole)], None)
(ProofEngineTypes.const_lazy_term typ);
- ProofEngineStructuralRules.clear [dummy]
+ PESR.clear [dummy]
]),
Some pat,gty
| _::_ -> assert false
TC.TypeCheckerFailure _ ->
let msg = lazy "rewrite: nothing to rewrite" in
raise (PET.Fail msg)
- in
- ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality)
-
-
-let rewrite_simpl_tac ~direction ~pattern equality =
- let rewrite_simpl_tac ~direction ~pattern equality status =
- ProofEngineTypes.apply_tactic
- (Tacticals.then_
- ~start:(rewrite_tac ~direction ~pattern equality)
+ in
+ PET.mk_tactic _rewrite_tac
+
+let rewrite_tac ~direction ~pattern equality names =
+ let _, hyps_pat, _ = pattern in
+ let froms = List.map fst hyps_pat in
+ let start = rewrite_tac ~direction ~pattern equality in
+ let continuation = PESR.rename ~froms ~tos:names in
+ if names = [] then start else T.then_ ~start ~continuation
+
+let rewrite_simpl_tac ~direction ~pattern equality names =
+ T.then_
+ ~start:(rewrite_tac ~direction ~pattern equality names)
~continuation:
(ReductionTactics.simpl_tac
- ~pattern:(ProofEngineTypes.conclusion_pattern None)))
- status
- in
- ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~direction ~pattern equality)
-;;
+ ~pattern:(ProofEngineTypes.conclusion_pattern None))
+
let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status =
~continuations:[
T.then_
~start:(
- rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1))
+ rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1) [])
~continuation:(
T.then_
~start:(
with (Failure "hd") -> assert false
in
ProofEngineTypes.apply_tactic
- (ProofEngineStructuralRules.clear ~hyps) status))
+ (PESR.clear ~hyps) status))
~continuation:(aux_tac (n + 1) tl));
T.id_tac])
status
let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
let n = List.length new_context - List.length context in
let equality = if n > 0 then S.lift n equality else equality in
- PET.apply_tactic (rewrite_tac ~direction ~pattern equality) status
+ PET.apply_tactic (rewrite_tac ~direction ~pattern equality []) status
in
PET.mk_tactic lift_rewrite_tac
val rewrite_tac:
direction:[`LeftToRight | `RightToLeft] ->
- pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic
+ pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> string list ->
+ ProofEngineTypes.tactic
val rewrite_simpl_tac:
direction:[`LeftToRight | `RightToLeft] ->
- pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic
+ pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> string list ->
+ ProofEngineTypes.tactic
val replace_tac:
pattern:ProofEngineTypes.lazy_pattern ->
(EqualityTactics.rewrite_simpl_tac
~direction:`LeftToRight
~pattern:(ProofEngineTypes.conclusion_pattern None)
- (C.Meta (fresh_meta,irl)))
+ (C.Meta (fresh_meta,irl)) [])
((curi,metasenv',pbo,pty),goal)
in
let new_goals = fresh_meta::goals in
(* $Id$ *)
-open ProofEngineTypes
+module PET = ProofEngineTypes
+module C = Cic
let clearbody ~hyp =
- let clearbody ~hyp (proof, goal) =
- let module C = Cic in
+ let clearbody (proof, goal) =
let curi,metasenv,pbo,pty = proof in
let metano,_,_ = CicUtil.lookup_meta goal metasenv in
let string_of_name =
with
_ ->
raise
- (Fail
+ (PET.Fail
(lazy ("The correctness of hypothesis " ^
string_of_name n ^
" relies on the body of " ^ hyp)
with
_ ->
raise
- (Fail
+ (PET.Fail
(lazy ("The correctness of the goal relies on the body of " ^
hyp)))
in
in
(curi,metasenv',pbo,pty), [goal]
in
- mk_tactic (clearbody ~hyp)
+ PET.mk_tactic clearbody
let clear_one ~hyp =
- let clear_one ~hyp (proof, goal) =
- let module C = Cic in
+ let clear_one (proof, goal) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty =
CicUtil.lookup_meta goal metasenv
CicUniv.empty_ugraph
with _ ->
raise
- (Fail
+ (PET.Fail
(lazy ("Hypothesis " ^ string_of_name n ^
" uses hypothesis " ^ hyp)))
in
) canonical_context (false, [])
in
if not context_changed then
- raise (Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
+ raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv canonical_context' ty
CicUniv.empty_ugraph
with _ ->
- raise (Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
+ raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
in
m,canonical_context',ty
| t -> t
in
(curi,metasenv',pbo,pty), [goal]
in
- mk_tactic (clear_one ~hyp)
+ PET.mk_tactic clear_one
let clear ~hyps =
- let clear hyps status =
+ let clear status =
let aux status hyp =
- match apply_tactic (clear_one ~hyp) status with
+ match PET.apply_tactic (clear_one ~hyp) status with
| proof, [g] -> proof, g
- | _ -> raise (Fail (lazy "clear: internal error"))
+ | _ -> raise (PET.Fail (lazy "clear: internal error"))
in
let proof, g = List.fold_left aux status hyps in
proof, [g]
in
- mk_tactic (clear hyps)
+ PET.mk_tactic clear
(* Warning: this tactic has no effect on the proof term.
It just changes the name of an hypothesis in the current sequent *)
-let rename ~from ~to_ =
- let rename ~from ~to_ (proof, goal) =
- let module C = Cic in
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty =
- CicUtil.lookup_meta goal metasenv
- in
- let metasenv' =
- List.map
- (function
- (m,canonical_context,ty) when m = metano ->
- let canonical_context' =
- List.map
- (function
- Some (Cic.Name hyp,decl_or_def) when hyp = from ->
- Some (Cic.Name to_,decl_or_def)
- | item -> item
- ) canonical_context
- in
- m,canonical_context',ty
- | t -> t
- ) metasenv
- in
- (curi,metasenv',pbo,pty), [goal]
- in
- mk_tactic (rename ~from ~to_)
+let rename ~froms ~tos =
+ let rename (proof, goal) =
+ let error = "rename: lists of different length" in
+ let assocs =
+ try List.combine froms tos
+ with Invalid_argument _ -> raise (PET.Fail (lazy error))
+ in
+ let curi, metasenv, pbo, pty = proof in
+ let metano, _, _ = CicUtil.lookup_meta goal metasenv in
+ let rename_map = function
+ | Some (Cic.Name hyp, decl_or_def) as entry ->
+ begin try Some (Cic.Name (List.assoc hyp assocs), decl_or_def)
+ with Not_found -> entry end
+ | entry -> entry
+ in
+ let map = function
+ | m, canonical_context, ty when m = metano ->
+ let canonical_context = List.map rename_map canonical_context in
+ m, canonical_context, ty
+ | conjecture -> conjecture
+ in
+ let metasenv = List.map map metasenv in
+ (curi, metasenv, pbo, pty), [goal]
+ in
+ PET.mk_tactic rename
let set_goal n =
- ProofEngineTypes.mk_tactic
+ PET.mk_tactic
(fun (proof, goal) ->
let (_, metasenv, _, _) = proof in
if CicUtil.exists_meta n metasenv then
(proof, [n])
else
- raise (ProofEngineTypes.Fail (lazy ("no such meta: " ^ string_of_int n))))
+ raise (PET.Fail (lazy ("no such meta: " ^ string_of_int n))))
(* Warning: this tactic has no effect on the proof term.
It just changes the name of an hypothesis in the current sequent *)
-val rename: from:string -> to_:string -> ProofEngineTypes.tactic
+val rename: froms:string list -> tos:string list -> ProofEngineTypes.tactic
(* change the current goal to those referred by the given meta number *)
val set_goal: int -> ProofEngineTypes.tactic
let normalize = ReductionTactics.normalize_tac
let reduce = ReductionTactics.reduce_tac
let reflexivity = Setoids.setoid_reflexivity_tac
+let rename = ProofEngineStructuralRules.rename
let replace = EqualityTactics.replace_tac
let rewrite = EqualityTactics.rewrite_tac
let rewrite_simpl = EqualityTactics.rewrite_simpl_tac
-(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Dec 21 00:41:09 CET 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Dec 29 00:00:27 CET 2006 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val reduce : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val reflexivity : ProofEngineTypes.tactic
+val rename : froms:string list -> tos:string list -> ProofEngineTypes.tactic
val replace :
pattern:ProofEngineTypes.lazy_pattern ->
with_what:Cic.lazy_term -> ProofEngineTypes.tactic
val rewrite :
direction:[ `LeftToRight | `RightToLeft ] ->
pattern:ProofEngineTypes.lazy_pattern ->
- Cic.term -> ProofEngineTypes.tactic
+ Cic.term -> string list -> ProofEngineTypes.tactic
val rewrite_simpl :
direction:[ `LeftToRight | `RightToLeft ] ->
pattern:ProofEngineTypes.lazy_pattern ->
- Cic.term -> ProofEngineTypes.tactic
+ Cic.term -> string list -> ProofEngineTypes.tactic
val right : ProofEngineTypes.tactic
val ring : ProofEngineTypes.tactic
val set_goal : int -> ProofEngineTypes.tactic
set "baseuri" "cic:/matita/tests".
-alias id "subst0" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1)".
+include "../contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma".
+
+alias id "Abbr" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/1)".
+alias id "Abst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/2)".
+alias id "Appl" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/F.ind#xpointer(1/1/1)".
+alias id "Bind" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/K.ind#xpointer(1/1/1)".
+alias id "Cast" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/F.ind#xpointer(1/1/2)".
+alias id "ex2_sym" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/props/ex2_sym.con".
+alias id "ex3_2_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/ex3_2_ind.con".
+alias id "Flat" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/K.ind#xpointer(1/1/2)".
+alias id "lift" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs/lift.con".
+alias id "or3_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/or3_ind.con".
+alias id "pr0_beta" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/3)".
alias id "pr0" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1)".
-alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)".
-alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
-alias id "ex2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1)".
-alias id "T" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xpointer(1/1)".
+alias id "pr0_comp" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/2)".
+alias id "pr0_delta" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/5)".
+alias id "pr0_epsilon" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/7)".
alias id "pr0_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0_ind.con".
+alias id "pr0_subst0_fwd" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0_fwd.con".
+alias id "pr0_upsilon" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/4)".
+alias id "pr0_zeta" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/6)".
+alias id "s" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/s/defs/s.con".
+alias id "subst0_both" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1/4)".
+alias id "subst0" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1)".
+alias id "subst0_confluence_neq" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/subst0/subst0_confluence_neq.con".
+alias id "subst0_fst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1/2)".
alias id "subst0_gen_head" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd/subst0_gen_head.con".
-alias id "or3_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/or3_ind.con".
-alias id "ex2_ind" = "cic:/Coq/Init/Logic/ex2_ind.con".
-alias id "ex3_2_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/ex3_2_ind.con".
alias id "subst0_gen_lift_ge" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd/subst0_gen_lift_ge.con".
-alias id "or_intror" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/2)".
-alias id "pr0_subst0_fwd" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0_fwd.con".
-alias id "ex2_sym" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/props/ex2_sym.con".
+alias id "subst0_lift_ge_s" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/props/subst0_lift_ge_s.con".
+alias id "subst0_snd" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1/3)".
+alias id "subst0_subst0_back" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/subst0/subst0_subst0_back.con".
+alias id "subst0_trans" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/subst0/subst0_trans.con".
+alias id "T" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xpointer(1/1)".
+alias id "THead" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xpointer(1/1/3)".
inline procedural
"cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con".
<keyword>normalize</keyword>
<keyword>reduce</keyword>
<keyword>reflexivity</keyword>
+ <keyword>rename</keyword>
<keyword>replace</keyword>
<keyword>rewrite</keyword>
<keyword>ring</keyword>
projects / helm.git / commitdiff