]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_transformations/tacticAstPp.ml
snapshot
[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml
1 (* Copyright (C) 2004, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 open Printf
27
28 open TacticAst
29
30 let pp_term term = CicAstPp.pp_term term
31
32 let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
33
34 let pp_reduction_kind = function
35   | `Reduce -> "reduce"
36   | `Simpl -> "simpl"
37   | `Whd -> "whd"
38
39 let rec pp_tactic = function
40   | LocatedTactic (loc, tac) -> pp_tactic tac
41   | Absurd -> "absurd"
42   | Apply term -> "apply " ^ pp_term term
43   | Assumption -> "assumption"
44   | Change (t1, t2, where) ->
45       sprintf "change %s with %s%s" (pp_term t1) (pp_term t2)
46         (match where with None -> "" | Some ident -> "in " ^ ident)
47   | Change_pattern (_, _, _) -> assert false  (* TODO *)
48   | Contradiction -> "contradiction"
49   | Cut term -> "cut " ^ pp_term term
50   | Decompose (ident, principles) ->
51       sprintf "decompose %s %s" (pp_idents principles) ident
52   | Discriminate ident -> "discriminate " ^ ident
53   | Elim (term, using) ->
54       sprintf "elim " ^ pp_term term ^
55       (match using with None -> "" | Some term -> " using " ^ pp_term term)
56   | ElimType term -> "elim type " ^ pp_term term
57   | Exact term -> "exact " ^ pp_term term
58   | Exists -> "exists"
59   | Fold (kind, term) ->
60       sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term term)
61   | Fourier -> "fourier"
62   | Injection ident -> "injection " ^ ident
63   | Intros (num, idents) ->
64       sprintf "intros%s%s"
65         (match num with None -> "" | Some num -> " " ^ string_of_int num)
66         (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
67   | Left -> "left"
68   | LetIn (term, ident) -> sprintf "let %s in %s" (pp_term term) ident
69   | Reduce (_, _, _) -> assert false  (* TODO *)
70   | Reflexivity -> "reflexivity"
71   | Replace (t1, t2) -> sprintf "replace %s with %s" (pp_term t1) (pp_term t2)
72   | Replace_pattern (_, _) -> assert false  (* TODO *)
73   | Rewrite (_, _, _) -> assert false (* TODO *)
74   | Right -> "right"
75   | Ring -> "ring"
76   | Split -> "split"
77   | Symmetry -> "symmetry"
78   | Transitivity term -> "transitivity " ^ pp_term term
79
80 let pp_flavour = function
81   | `Definition -> "Definition"
82   | `Fact -> "Fact"
83   | `Goal -> "Goal"
84   | `Lemma -> "Lemma"
85   | `Remark -> "Remark"
86   | `Theorem -> "Theorem"
87
88 let pp_command = function
89   | Abort -> "Abort"
90   | Check term -> sprintf "Check %s" (CicAstPp.pp_term term)
91   | Proof -> "Proof"
92   | Qed name ->
93       (match name with None -> "Qed" | Some name -> sprintf "Save %s" name)
94   | Quit -> "Quit"
95   | Theorem (flavour, name, typ, body) ->
96       sprintf "%s %s: %s %s"
97         (pp_flavour flavour)
98         (match name with None -> "" | Some name -> name)
99         (CicAstPp.pp_term typ)
100         (match body with
101         | None -> ""
102         | Some body -> "\\def " ^ CicAstPp.pp_term body)
103
104 let rec pp_tactical = function
105   | LocatedTactical (loc, tac) -> pp_tactical tac
106
107   | Tactic tac -> pp_tactic tac
108   | Command cmd -> pp_command cmd
109
110   | Fail -> "fail"
111   | Do (count, tac) -> sprintf "do %d %s" count (pp_tactical tac)
112   | IdTac -> "id"
113   | Repeat tac -> "repeat " ^ pp_tactical tac
114   | Seq tacs -> pp_tacticals tacs
115   | Then (tac, tacs) -> sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs)
116   | Tries tacs -> sprintf "tries [%s]" (pp_tacticals tacs)
117   | Try tac -> "try " ^ pp_tactical tac
118
119 and pp_tacticals tacs = String.concat "; " (List.map pp_tactical tacs)
120
121 let pp_tactical tac = pp_tactical tac ^ "."
122