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 assert false ^ " " ^ assert false
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 " ^ assert false ^
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 assert false ^ " " ^ assert false
81 | NIntro (_,n) -> "#" ^ n
82 | NInversion (_,what,where) -> "ninversion " ^ NotationPp.pp_term what ^
83 assert false ^ " " ^ assert false
84 | NLApply (_,t) -> "lapply " ^ NotationPp.pp_term t
85 | NRewrite (_,dir,n,where) -> "nrewrite " ^
86 (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^
87 " " ^ NotationPp.pp_term n ^ " " ^ pp_tactic_pattern where
88 | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> "TO BE IMPLEMENTED"
90 | NSemicolon _ -> "##;"
93 | NPos (_, l) -> "##" ^String.concat "," (List.map string_of_int l)^ ":"
94 | NPosbyname (_, s) -> "##" ^ s ^ ":"
95 | NWildcard _ -> "##*:"
98 Printf.sprintf "##focus %s"
99 (String.concat " " (List.map string_of_int l))
100 | NUnfocus _ -> "##unfocus"
101 | NSkip _ -> "##skip"
102 | NTry (_,tac) -> "ntry " ^ pp_ntactic ~map_unicode_to_tex tac
103 | NAssumption _ -> "nassumption"
105 "(" ^ String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) l)^ ")"
106 | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic ~map_unicode_to_tex t
109 let pp_nmacro = function
110 | NCheck (_, term) -> Printf.sprintf "ncheck %s" (NotationPp.pp_term term)
111 | Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name
114 let pp_ncommand = function
115 | UnificationHint (_,t, n) ->
116 "unification hint " ^ string_of_int n ^ " " ^ NotationPp.pp_term t
117 | NDiscriminator (_,_)
118 | NInverter (_,_,_,_,_)
119 | NUnivConstraint (_) -> "not supported"
120 | NCoercion (_) -> "not supported"
121 | NObj (_,obj) -> NotationPp.pp_obj NotationPp.pp_term obj
123 | NCopy (_,name,uri,map) ->
124 "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^
125 String.concat " and "
127 (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b)
131 let pp_command = function
132 | Include (_,path) -> "include \"" ^ path ^ "\""
133 | Print (_,s) -> "print " ^ s
134 | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value
136 let pp_executable ~map_unicode_to_tex =
138 | NMacro (_, macro) -> pp_nmacro macro ^ "."
139 | NTactic (_,tacl) ->
140 String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) tacl)
141 | Command (_, cmd) -> pp_command cmd ^ "."
142 | NCommand (_, cmd) -> pp_ncommand cmd ^ "."
144 let pp_comment ~map_unicode_to_tex =
146 | Note (_,"") -> Printf.sprintf "\n"
147 | Note (_,str) -> Printf.sprintf "\n(* %s *)" str
149 Printf.sprintf "\n(** %s. **)" (pp_executable ~map_unicode_to_tex code)
153 | Executable (_, ex) -> pp_executable ex
154 | Comment (_, c) -> pp_comment c