let pp_auto_params ~term_pp (univ, params) =
String.concat " "
(List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) ^
- if univ <> [] then
- (if params <> [] then " " else "") ^ "by " ^
- String.concat " " (List.map term_pp univ)
- else ""
+ match univ with
+ | None -> ""
+ | Some l -> (if params <> [] then " " else "") ^ "by " ^
+ String.concat " " (List.map term_pp l)
;;
let pp_just ~term_pp =
pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in
function
| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+ | NSmartApply (_,t) -> "fixme"
+ | NAuto (_,(None,flgs)) ->
+ "nautobatch" ^
+ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
+ | NAuto (_,(Some l,flgs)) ->
+ "nautobatch" ^ " by " ^
+ (String.concat "," (List.map CicNotationPp.pp_term l)) ^
+ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
| NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
- | NConstructor (_,None) -> "@"
- | NConstructor (_,Some x) -> "@" ^ string_of_int x
+ | 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
+(*| NDiscriminate (_,t) -> "ndiscriminate " ^ CicNotationPp.pp_term t
+ | NSubst (_,t) -> "nsubst " ^ CicNotationPp.pp_term t *)
+ | NDestruct _ -> "ndestruct"
| NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
+ | NInversion (_,what,where) -> "ninversion " ^ CicNotationPp.pp_term what ^
+ assert false ^ " " ^ 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
- | 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 _ -> "TO BE IMPLEMENTED"
| NDot _ -> "##."
| NSemicolon _ -> "##;"
| NBranch _ -> "##["
| NShift _ -> "##|"
| NPos (_, l) -> "##" ^String.concat "," (List.map string_of_int l)^ ":"
+ | NPosbyname (_, s) -> "##" ^ s ^ ":"
| NWildcard _ -> "##*:"
| NMerge _ -> "##]"
| NFocus (_,l) ->
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 =
(term_pp t) arity saturations
(if do_composites then "" else "nocomposites")
-let pp_ncommand = function
+let pp_ncommand ~obj_pp = function
| UnificationHint (_,t, n) ->
"unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
- | NObj (_,_)
+ | NDiscriminator (_,_)
+ | NInverter (_,_,_,_,_)
| NUnivConstraint (_) -> "not supported"
| NCoercion (_) -> "not supported"
+ | NObj (_,obj) -> obj_pp obj
| NQed (_) -> "nqed"
| NCopy (_,name,uri,map) ->
"copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^
pp_non_punctuation_tactical tac
^ pp_punctuation_tactical punct
| Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
- | NCommand (_, cmd) -> pp_ncommand cmd ^ "."
+ | NCommand (_, cmd) ->
+ let obj_pp = Obj.magic obj_pp in
+ pp_ncommand ~obj_pp cmd ^ "."
let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
function