| 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
+ | NDot _ -> "##."
+ | NSemicolon _ -> "##;"
+ | NBranch _ -> "##["
+ | NShift _ -> "##|"
+ | NPos (_, l) -> "##" ^String.concat "," (List.map string_of_int l)^ ":"
+ | NWildcard _ -> "##*:"
+ | NMerge _ -> "##]"
+ | NFocus (_,l) ->
+ Printf.sprintf "##focus %s"
+ (String.concat " " (List.map string_of_int l))
+ | NUnfocus _ -> "##unfocus"
+ | NSkip _ -> "##skip"
;;
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
let pp_inline_params l =
let pp_param = function
| IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\""
- | IPAs flavour -> flavour_pp flavour
- | IPProcedural -> "procedural"
- | IPNoDefaults -> "nodefaults"
+ | IPAs flavour -> flavour_pp flavour
+ | IPCoercions -> "coercions"
+ | IPDebug debug -> "debug = " ^ string_of_int debug
+ | IPProcedural -> "procedural"
+ | IPNoDefaults -> "nodefaults"
| IPDepth depth -> "depth = " ^ string_of_int depth
| IPLevel level -> "level = " ^ string_of_int level
+ | IPComments -> "comments"
+ | IPCR -> "cr"
in
let s = String.concat " " (List.map pp_param l) in
if s = "" then s else " " ^ s
"unification hint " ^ string_of_int n ^ " " ^ term_pp t
| Default (_,what,uris) -> pp_default what uris
| Drop _ -> "drop"
- | Include (_,false,path) -> "include \"" ^ path ^ "\""
- | Include (_,true,path) -> "include source \"" ^ path ^ "\""
+ | Include (_,true,path) -> "include \"" ^ path ^ "\""
+ | Include (_,false,path) -> "include source \"" ^ path ^ "\""
| Obj (_,obj) -> obj_pp obj
| Qed _ -> "qed"
| Relation (_,id,a,aeq,refl,sym,trans) ->
| None -> "")
| Print (_,s) -> "print " ^ s
| Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value
- | NObj (_,o) -> "not supported"
+ | NObj (_,_)
| NUnivConstraint (_) -> "not supported"
- | NQed (_) -> "not supported"
+ | NQed (_) -> "nqed"
| Pump (_) -> "not supported"
let pp_punctuation_tactical =
^ pp_punctuation_tactical punct
| Tactic (_, None, punct) ->
pp_punctuation_tactical punct
- | NTactic (_,tac, punct) ->
- pp_ntactic ~map_unicode_to_tex tac
- ^ pp_punctuation_tactical punct
+ | NTactic (_,tacl) ->
+ String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) tacl)
| NonPunctuationTactical (_, tac, punct) ->
pp_non_punctuation_tactical tac
^ pp_punctuation_tactical punct
- | NNonPunctuationTactical (_, tac, punct) ->
- pp_non_punctuation_tactical tac
- ^ pp_punctuation_tactical punct
| Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =