From ee8cb3c92bdfd478ed5eefe1735e48dc2dccbed2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Jul 2005 12:10:00 +0000 Subject: [PATCH] New function (only partially implemented) to pretty print an Ast at the semantics level. --- helm/ocaml/cic_transformations/tacticAstPp.ml | 13 +++++++++++-- helm/ocaml/cic_transformations/tacticAstPp.mli | 1 + 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 3a8b5213c..7802e582e 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -223,8 +223,8 @@ let pp_command = function | Include (_,path) -> "include " ^ path | Qed _ -> "qed" | Drop _ -> "drop" - | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value - | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!" + | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value + | Coercion (_,term) -> sprintf "coercion %s" (pp_term_ast term) | Alias (_,s) -> pp_alias s | Obj (_,obj) -> pp_obj obj @@ -257,3 +257,12 @@ let pp_comment = function let pp_statement = function | Executable (_, ex) -> pp_executable ex | Comment (_, c) -> pp_comment c + +let pp_cic_command = function + | Include (_,path) -> "include " ^ path + | Qed _ -> "qed" + | Drop _ -> "drop" + | Coercion (_,term) -> sprintf "coercion %s" (CicPp.ppterm term) + | Set (_, _, _) + | Alias (_,_) + | Obj (_,_) -> assert false (* not implemented *) diff --git a/helm/ocaml/cic_transformations/tacticAstPp.mli b/helm/ocaml/cic_transformations/tacticAstPp.mli index d4cae4405..fb9b45084 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.mli +++ b/helm/ocaml/cic_transformations/tacticAstPp.mli @@ -35,3 +35,4 @@ val pp_macro_cic: Cic.term TacticAst.macro -> string val pp_tactical: (CicAst.term, string) TacticAst.tactical -> string val pp_alias: TacticAst.alias_spec -> string +val pp_cic_command: (Cic.term,Cic.obj) TacticAst.command -> string -- 2.39.2