(* 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 inferred = Cic.annterm type pattern = Cic.annterm 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 * pattern * note | Elim of what * using option * pattern * note | Apply of what * note | Change of inferred * what * where * pattern * note | ClearBody of name * 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 pattern = let direction = if direction then `RightToLeft else `LeftToRight in let pattern, rename = match where with | None -> (None, [], Some pattern), [] | Some (premise, name) -> (None, [premise, pattern], None), [name] in let tactic = G.Rewrite (floc, direction, what, pattern, rename) in mk_tactic tactic let mk_elim what using pattern = let pattern = None, [], Some pattern in let tactic = G.Elim (floc, what, using, pattern, Some 0, []) in mk_tactic tactic let mk_apply t = let tactic = G.Apply (floc, t) in mk_tactic tactic let mk_change t where pattern = let pattern = match where with | None -> None, [], Some pattern | Some (premise, _) -> None, [premise, pattern], None in let tactic = G.Change (floc, pattern, t) in mk_tactic tactic let mk_clearbody id = let tactic = G.ClearBody (floc, id) 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, e, s) -> mk_note s :: cont sep (mk_rewrite b t w e :: a) | Elim (t, xu, e, s) -> mk_note s :: cont sep (mk_elim t xu e :: a) | Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a) | Change (t, _, w, e, s) -> mk_note s :: cont sep (mk_change t w e :: a) | ClearBody (n, s) -> mk_note s :: cont sep (mk_clearbody n :: 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