module Ast = CicNotationPt
-let tactical_terminator = "."
+let tactical_terminator = ""
let tactic_terminator = tactical_terminator
let command_terminator = tactical_terminator
| Some `LeftToRight -> "> "
| Some `RightToLeft -> "< "
+let pp_metadata =
+ function
+ | Dependency buri -> sprintf "dependency %s" buri
+ | Baseuri buri -> sprintf "baseuri %s" buri
+
let pp_command = function
| Include (_,path) -> "include " ^ path
| Qed _ -> "qed"
(pp_associativity assoc)
(pp_precedence prec)
(pp_l2_pattern l2_pattern)
+ | Metadata (_, m) -> sprintf "metadata %s" (pp_metadata m)
| Render _
| Dump _ -> assert false (* ZACK: debugging *)
| Try (_, tac) -> "try " ^ pp_tactical tac
| Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
-and pp_tacticals ~sep tacs =
- String.concat sep (List.map pp_tactical tacs)
+ | Dot _ -> "."
+ | Semicolon _ -> ";"
+ | Branch _ -> "["
+ | Shift _ -> "|"
+ | Pos (_, i) -> sprintf "%d:" i
+ | Merge _ -> "]"
+ | Focus (_, goals) ->
+ sprintf "focus %s" (String.concat " " (List.map string_of_int goals))
+ | Unfocus _ -> "unfocus"
+ | Skip _ -> "skip"
+
+and pp_tacticals ~sep tacs = String.concat sep (List.map pp_tactical tacs)
-let pp_tactical tac = pp_tactical tac ^ tactical_terminator
-let pp_tactic tac = pp_tactic tac ^ tactic_terminator
-let pp_command tac = pp_command tac ^ command_terminator
+let pp_tactical tac = pp_tactical tac
+let pp_tactic tac = pp_tactic tac
+let pp_command tac = pp_command tac
let pp_executable = function
| Macro (_,x) -> pp_macro_ast x
- | Tactical (_,x) -> pp_tactical x
+ | Tactical (_, tac, Some punct) -> pp_tactical tac ^ pp_tactical punct
+ | Tactical (_, tac, None) -> pp_tactical tac
| Command (_,x) -> pp_command x
let pp_comment = function
| Render _
| Dump _
| Interpretation _
+ | Metadata _
| Notation _
| Obj _ -> assert false (* not implemented *)
+let pp_dependency = function
+ | IncludeDep str -> "include \"" ^ str ^ "\""
+ | BaseuriDep str -> "set \"baseuri\" \"" ^ str ^ "\""
+ | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\""
+