From 651c5c55cba9ddbe592badc86b18502b83ecf580 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 13 Aug 2009 15:45:49 +0000 Subject: [PATCH] Assert false do not allow to debug... --- .../components/grafite/grafiteAstPp.ml | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index eddac9746..6c7a6638a 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -89,7 +89,12 @@ let pp_just ~term_pp = | `Auto params -> pp_auto_params ~term_pp params ;; -let rec pp_ntactic ~map_unicode_to_tex = function +let rec pp_ntactic ~map_unicode_to_tex = + let term_pp = CicNotationPp.pp_term in + let lazy_term_pp = fun _ -> assert false in + let pp_tactic_pattern = + pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in + function | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^ assert false ^ " " ^ assert false @@ -100,13 +105,15 @@ let rec pp_ntactic ~map_unicode_to_tex = function assert false ^ " " ^ assert false | NId _ -> "nid" | NIntro (_,n) -> "#" ^ n - | NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false + | 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 _ -> assert false + | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> "TO BE IMPLEMENTED" | NDot _ -> "##." | NSemicolon _ -> "##;" | NBranch _ -> "##[" @@ -341,11 +348,6 @@ let pp_associativity = function let pp_precedence i = Printf.sprintf "with precedence %d" i -let pp_dir_opt = function - | None -> "" - | Some `LeftToRight -> "> " - | Some `RightToLeft -> "< " - let pp_default what uris = Printf.sprintf "default \"%s\" %s" what (String.concat " " (List.map UriManager.string_of_uri uris)) -- 2.39.2