| `Auto params -> pp_auto_params ~term_pp params
;;
-let pp_ntactic ~map_unicode_to_tex = function
+let rec pp_ntactic ~map_unicode_to_tex = function
| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+ | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
+ assert false ^ " " ^ assert false
+ | NCase1 (_,n) -> "*" ^ n ^ ":"
| NChange (_,what,wwhat) -> "nchange " ^ assert false ^
" with " ^ CicNotationPp.pp_term wwhat
| 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
+ | 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"
+ | NTry (_,tac) -> "ntry " ^ pp_ntactic ~map_unicode_to_tex tac
+ | NAssumption _ -> "nassumption"
+ | NBlock (_,l) ->
+ "(" ^ String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) l)^ ")"
+ | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic ~map_unicode_to_tex t
;;
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
let pp_macro ~term_pp ~lazy_term_pp =
let term_pp = pp_arg ~term_pp in
- let style_pp = function
- | Declarative -> ""
- | Procedural None -> "procedural "
- | Procedural (Some i) -> Printf.sprintf "procedural %u " i
- in
- let prefix_pp prefix =
- if prefix = "" then "" else Printf.sprintf " \"%s\"" prefix
- in
let flavour_pp = function
- | None -> ""
- | Some `Definition -> " as definition"
- | Some `MutualDefinition -> " as mutual"
- | Some `Fact -> " as fact"
- | Some `Lemma -> " as lemma"
- | Some `Remark -> " as remark"
- | Some `Theorem -> " as theorem"
- | Some `Variant -> " as variant"
- | Some `Axiom -> " as axiom"
+ | `Definition -> "definition"
+ | `Fact -> "fact"
+ | `Lemma -> "lemma"
+ | `Remark -> "remark"
+ | `Theorem -> "theorem"
+ | `Variant -> "variant"
+ | `Axiom -> "axiom"
+ | `MutualDefinition -> assert false
+ in
+ let pp_inline_params l =
+ let pp_param = function
+ | IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\""
+ | 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
in
let pp_reduction_kind = pp_reduction_kind ~term_pp:lazy_term_pp in
function
| Hint (_, true) -> "hint rewrite"
| Hint (_, false) -> "hint"
| AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params
- | Inline (_, style, suri, prefix, flavour) ->
- Printf.sprintf "inline %s\"%s\"%s%s" (style_pp style) suri (prefix_pp prefix) (flavour_pp flavour)
+ | Inline (_, suri, params) ->
+ Printf.sprintf "inline \"%s\"%s" suri (pp_inline_params params)
let pp_associativity = function
| Gramext.LeftA -> "left associative"
Printf.sprintf "coercion %s %d %d %s"
(term_pp t) arity saturations
(if do_composites then "" else "nocomposites")
+
+let pp_ncommand = function
+ | UnificationHint (_,t, n) ->
+ "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+ | NObj (_,_)
+ | NUnivConstraint (_) -> "not supported"
+ | NCoercion (_) -> "not supported"
+ | NQed (_) -> "nqed"
let pp_command ~term_pp ~obj_pp = function
| Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
+ | Select (_,uri) -> "Selecting " ^ UriManager.string_of_uri uri
| Coercion (_, t, do_composites, i, j) ->
pp_coercion ~term_pp t do_composites i j
| PreferCoercion (_,t) ->
"prefer coercion " ^ term_pp t
- | UnificationHint (_,t, n) ->
- "unification hint " ^ string_of_int n ^ " " ^ term_pp t
+ | Inverter (_,n,ty,params) ->
+ "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params
| Default (_,what,uris) -> pp_default what uris
| Drop _ -> "drop"
- | Include (_,path) -> "include \"" ^ path ^ "\""
+ | Include (_,true,`OldAndNew,path) -> "include \"" ^ path ^ "\""
+ | Include (_,false,`OldAndNew,path) -> "include source \"" ^ path ^ "\""
+ | Include (_,_,`New,path) -> "RECURSIVELY INCLUDING " ^ 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"
+ | Pump (_) -> "not supported"
let pp_punctuation_tactical =
function
^ 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
| Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
+ | NCommand (_, cmd) -> pp_ncommand cmd ^ "."
let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
function
projects / helm.git / blobdiff