(* Copyright (C) 2004, 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/ *) open Printf open TacticAst let tactical_terminator = "." let tactical_separator = ";" let pp_term term = CicAstPp.pp_term term let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" let pp_reduction_kind = function | `Reduce -> "reduce" | `Simpl -> "simplify" | `Whd -> "whd" let rec pp_tactic = function | LocatedTactic (loc, tac) -> pp_tactic tac | Absurd term -> "absurd" ^ pp_term term | Apply term -> "apply " ^ pp_term term | Auto -> "auto" | Assumption -> "assumption" | Change (t1, t2, where) -> sprintf "change %s with %s%s" (pp_term t1) (pp_term t2) (match where with None -> "" | Some ident -> "in " ^ ident) | Change_pattern (_, _, _) -> assert false (* TODO *) | Contradiction -> "contradiction" | Cut term -> "cut " ^ pp_term term | Decompose (ident, principles) -> sprintf "decompose %s %s" (pp_idents principles) ident | Discriminate ident -> "discriminate " ^ ident | Elim (term, using) -> sprintf "elim " ^ pp_term term ^ (match using with None -> "" | Some term -> " using " ^ pp_term term) | ElimType term -> "elim type " ^ pp_term term | Exact term -> "exact " ^ pp_term term | Exists -> "exists" | Fold (kind, term) -> sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term term) | Fourier -> "fourier" | Hint -> "hint" | Injection ident -> "injection " ^ ident | Intros (None, []) -> "intro" | Intros (num, idents) -> sprintf "intros%s%s" (match num with None -> "" | Some num -> " " ^ string_of_int num) (match idents with [] -> "" | idents -> " " ^ pp_idents idents) | Left -> "left" | LetIn (term, ident) -> sprintf "let %s in %s" (pp_term term) ident | Reduce (kind, None) | Reduce (kind, Some ([], `Goal)) -> pp_reduction_kind kind | Reduce (kind, Some ([], `Everywhere)) -> sprintf "%s in hyp" (pp_reduction_kind kind) | Reduce (kind, Some (terms, `Goal)) -> sprintf "%s %s" (pp_reduction_kind kind) (String.concat ", " (List.map pp_term terms)) | Reduce (kind, Some (terms, `Everywhere)) -> sprintf "%s in hyp %s" (pp_reduction_kind kind) (String.concat ", " (List.map pp_term terms)) | Reflexivity -> "reflexivity" | Replace (t1, t2) -> sprintf "replace %s with %s" (pp_term t1) (pp_term t2) | Replace_pattern (_, _) -> assert false (* TODO *) | Rewrite (_, _, _) -> assert false (* TODO *) | Right -> "right" | Ring -> "ring" | Split -> "split" | Symmetry -> "symmetry" | Transitivity term -> "transitivity " ^ pp_term term let pp_flavour = function | `Definition -> "Definition" | `Fact -> "Fact" | `Goal -> "Goal" | `Lemma -> "Lemma" | `Remark -> "Remark" | `Theorem -> "Theorem" let pp_search_kind = function | `Locate -> "locate" | `Hint -> "hint" | `Match -> "match" | `Elim -> "elim" let pp_command = function | Abort -> "Abort" | Baseuri (Some uri) -> sprintf "Baseuri \"%s\"" uri | Baseuri None -> "Baseuri" | Check term -> sprintf "Check %s" (pp_term term) | Proof -> "Proof" | Qed name -> (match name with None -> "Qed" | Some name -> sprintf "Save %s" name) | Quit -> "Quit" | Redo None -> "Redo" | Redo (Some n) -> sprintf "Redo %d" n | Search_pat (kind, pat) -> sprintf "search %s \"%s\"" (pp_search_kind kind) pat | Search_term (kind, term) -> sprintf "search %s %s" (pp_search_kind kind) (pp_term term) | Inductive (params, types) -> let pp_params = function | [] -> "" | params -> " " ^ String.concat " " (List.map (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term typ)) params) in let pp_constructors constructors = String.concat "\n" (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ)) constructors) in let pp_type (name, _, typ, constructors) = sprintf "\nwith %s: %s \\def\n%s" name (pp_term typ) (pp_constructors constructors) in (match types with | [] -> assert false | (name, inductive, typ, constructors) :: tl -> let fst_typ_pp = sprintf "%sinductive %s%s: %s \\def\n%s" (if inductive then "" else "co") name (pp_params params) (pp_term typ) (pp_constructors constructors) in fst_typ_pp ^ String.concat "" (List.map pp_type tl)) | Theorem (flavour, name, typ, body) -> sprintf "%s %s: %s %s" (pp_flavour flavour) (match name with None -> "" | Some name -> name) (pp_term typ) (match body with | None -> "" | Some body -> "\\def " ^ pp_term body) | Undo None -> "Undo" | Undo (Some n) -> sprintf "Undo %d" n let rec pp_tactical = function | LocatedTactical (loc, tac) -> pp_tactical tac | Tactic tac -> pp_tactic tac | Command cmd -> pp_command cmd | Fail -> "fail" | Do (count, tac) -> sprintf "do %d %s" count (pp_tactical tac) | IdTac -> "id" | Repeat tac -> "repeat " ^ pp_tactical tac | Seq tacs -> pp_tacticals tacs | Then (tac, tacs) -> sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs) | Tries tacs -> sprintf "tries [%s]" (pp_tacticals tacs) | Try tac -> "try " ^ pp_tactical tac and pp_tacticals tacs = String.concat (tactical_separator ^ " ") (List.map pp_tactical tacs) let pp_tactical tac = pp_tactical tac ^ tactical_terminator