1 (* Copyright (C) 2004, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 let tactical_terminator = ""
31 let tactic_terminator = tactical_terminator
32 let command_terminator = tactical_terminator
34 let pp_tactic_pattern ~map_unicode_to_tex (what, hyp, goal) =
35 if what = None && hyp = [] && goal = None then "" else
39 | Some t -> Printf.sprintf "in match (%s) " (NotationPp.pp_term t) in
42 (List.map (fun (name, p) -> Printf.sprintf "%s:(%s)" name
43 (NotationPp.pp_term p)) hyp) in
48 let vdash = if map_unicode_to_tex then "\\vdash" else "⊢" in
49 Printf.sprintf "%s (%s)" vdash (NotationPp.pp_term t)
51 Printf.sprintf "%sin %s%s" what_text hyp_text goal_text
53 let rec pp_ntactic ~map_unicode_to_tex =
54 let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in
56 | NApply (_,t) -> "napply " ^ NotationPp.pp_term t
57 | NSmartApply (_,t) -> "fixme"
58 | NAuto (_,(None,flgs)) ->
60 String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
61 | NAuto (_,(Some l,flgs)) ->
62 "nautobatch" ^ " by " ^
63 (String.concat "," (List.map NotationPp.pp_term l)) ^
64 String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
65 | NCases (_,what,where) -> "ncases " ^ NotationPp.pp_term what ^
66 "...to be implemented..." ^ " " ^ "...to be implemented..."
67 | NConstructor (_,None,l) -> "@ " ^
68 String.concat " " (List.map NotationPp.pp_term l)
69 | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
70 String.concat " " (List.map NotationPp.pp_term l)
71 | NCase1 (_,n) -> "*" ^ n ^ ":"
72 | NChange (_,what,wwhat) -> "nchange " ^ "...to be implemented..." ^
73 " with " ^ NotationPp.pp_term wwhat
74 | NCut (_,t) -> "ncut " ^ NotationPp.pp_term t
75 (*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term t
76 | NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term t *)
77 | NDestruct (_,dom,skip) -> "ndestruct ..."
78 | NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term what ^
79 "...to be implemented..." ^ " " ^ "...to be implemented..."
81 | NIntro (_,n) -> "#" ^ n
82 | NIntros (_,l) -> "#" ^ String.concat " " l
83 | NInversion (_,what,where) -> "ninversion " ^ NotationPp.pp_term what ^
84 assert false ^ " " ^ assert false
85 | NLApply (_,t) -> "lapply " ^ NotationPp.pp_term t
86 | NRewrite (_,dir,n,where) -> "nrewrite " ^
87 (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^
88 " " ^ NotationPp.pp_term n ^ " " ^ pp_tactic_pattern where
89 | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> "TO BE IMPLEMENTED"
94 | NPos (_, l) -> String.concat "," (List.map string_of_int l)^ ":"
95 | NPosbyname (_, s) -> s ^ ":"
99 Printf.sprintf "focus %s"
100 (String.concat " " (List.map string_of_int l))
101 | NUnfocus _ -> "unfocus"
103 | NTry (_,tac) -> "ntry " ^ pp_ntactic ~map_unicode_to_tex tac
104 | NAssumption _ -> "nassumption"
106 "(" ^ String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) l)^ ")"
107 | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic ~map_unicode_to_tex t
110 let pp_nmacro = function
111 | NCheck (_, term) -> Printf.sprintf "ncheck %s" (NotationPp.pp_term term)
112 | Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name
115 let pp_ncommand = function
116 | UnificationHint (_,t, n) ->
117 "unification hint " ^ string_of_int n ^ " " ^ NotationPp.pp_term t
118 | NDiscriminator (_,_)
119 | NInverter (_,_,_,_,_)
120 | NUnivConstraint (_) -> "not supported"
121 | NCoercion (_) -> "not supported"
122 | NObj (_,obj) -> NotationPp.pp_obj NotationPp.pp_term obj
124 | NCopy (_,name,uri,map) ->
125 "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^
126 String.concat " and "
128 (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b)
132 let pp_command = function
133 | Include (_,path,_,_) -> "include \"" ^ path ^ "\""
134 | Print (_,s) -> "print " ^ s
135 | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value
137 let pp_executable ~map_unicode_to_tex =
139 | NMacro (_, macro) -> pp_nmacro macro ^ "."
140 | NTactic (_,tacl) ->
141 String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) tacl)
142 | Command (_, cmd) -> pp_command cmd ^ "."
143 | NCommand (_, cmd) -> pp_ncommand cmd ^ "."
145 let pp_comment ~map_unicode_to_tex =
147 | Note (_,"") -> Printf.sprintf "\n"
148 | Note (_,str) -> Printf.sprintf "\n(* %s *)" str
150 Printf.sprintf "\n(** %s. **)" (pp_executable ~map_unicode_to_tex code)
154 | Executable (_, ex) -> pp_executable ex
155 | Comment (_, c) -> pp_comment c