| `Auto params -> pp_auto_params ~term_pp params
;;
-let rec pp_ntactic ~map_unicode_to_tex = function
+let rec pp_ntactic ~map_unicode_to_tex =
+ let term_pp = CicNotationPp.pp_term in
+ let lazy_term_pp = fun _ -> assert false in
+ let pp_tactic_pattern =
+ pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in
+ function
| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+ | NAuto (_,(l,flgs)) ->
+ "nauto" ^
+ (if l <> [] then (" by " ^
+ (String.concat "," (List.map CicNotationPp.pp_term l))) else "") ^
+ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
| NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
+ | NConstructor (_,None,l) -> "@ " ^
+ String.concat " " (List.map CicNotationPp.pp_term l)
+ | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
+ String.concat " " (List.map CicNotationPp.pp_term l)
| NCase1 (_,n) -> "*" ^ n ^ ":"
| NChange (_,what,wwhat) -> "nchange " ^ assert false ^
" with " ^ CicNotationPp.pp_term wwhat
+ | NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t
| NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
- | NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false
- | NAuto (_,(l,flgs)) ->
- "nauto" ^
- (if l <> [] then (" by " ^
- (String.concat "," (List.map CicNotationPp.pp_term l))) else "") ^
- String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
- | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> assert false
+ | NLApply (_,t) -> "lapply " ^ CicNotationPp.pp_term t
+ | NRewrite (_,dir,n,where) -> "nrewrite " ^
+ (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^
+ " " ^ CicNotationPp.pp_term n ^ " " ^ pp_tactic_pattern where
+ | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> "TO BE IMPLEMENTED"
| NDot _ -> "##."
| NSemicolon _ -> "##;"
| NBranch _ -> "##["
else
"(" ^ s ^ ")"
+let pp_nmacro = function
+ | NCheck (_, term) -> Printf.sprintf "ncheck %s" (CicNotationPp.pp_term term)
+ | Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name
+;;
+
let pp_macro ~term_pp ~lazy_term_pp =
let term_pp = pp_arg ~term_pp in
let flavour_pp = function
let pp_precedence i = Printf.sprintf "with precedence %d" i
-let pp_dir_opt = function
- | None -> ""
- | Some `LeftToRight -> "> "
- | Some `RightToLeft -> "< "
-
let pp_default what uris =
Printf.sprintf "default \"%s\" %s" what
(String.concat " " (List.map UriManager.string_of_uri uris))
let pp_ncommand = function
| UnificationHint (_,t, n) ->
"unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+ | NInverter (_,_,_,_,_)
| NObj (_,_)
| NUnivConstraint (_) -> "not supported"
+ | NCoercion (_) -> "not supported"
| NQed (_) -> "nqed"
+ | NCopy (_,name,uri,map) ->
+ "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^
+ String.concat " and "
+ (List.map
+ (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b)
+ map)
+;;
let pp_command ~term_pp ~obj_pp = function
| Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
function
+ | NMacro (_, macro) -> pp_nmacro macro ^ "."
| Macro (_, macro) -> pp_macro ~term_pp ~lazy_term_pp macro ^ "."
| Tactic (_, Some tac, punct) ->
pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp tac