From 3c1f5f810ce2acbbfc6e8f5d50e22bd4068b09a7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 25 Aug 2006 15:07:57 +0000 Subject: [PATCH] trying to make output notation parsable --- components/acic_content/cicNotationPp.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml index 5f45b2a4b..a23d26add 100644 --- a/components/acic_content/cicNotationPp.ml +++ b/components/acic_content/cicNotationPp.ml @@ -97,9 +97,9 @@ let rec pp_term ?(pp_parens = true) t = sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var) (pp_term body) | Ast.Case (term, indtype, typ, patterns) -> - sprintf "%smatch %s%s with %s" - (match typ with None -> "" | Some t -> sprintf "[%s]" (pp_term t)) + sprintf "match %s%s%s with %s" (pp_term term) + (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t)) (match indtype with | None -> "" | Some (ty, href_opt) -> @@ -111,7 +111,7 @@ let rec pp_term ?(pp_parens = true) t = (pp_patterns patterns) | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2) | Ast.LetIn (var, t1, t2) -> - sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1) + sprintf "let %s \\def %s in %s" (pp_capture_variable var) (pp_term t1) (pp_term t2) | Ast.LetRec (kind, definitions, term) -> sprintf "let %s %s in %s" @@ -147,7 +147,7 @@ let rec pp_term ?(pp_parens = true) t = | Ast.Magic m -> pp_magic m | Ast.Variable v -> pp_variable v in - if pp_parens then sprintf "(%s)" t_pp + if pp_parens then sprintf "(%s)\n" t_pp else t_pp and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term) @@ -174,7 +174,7 @@ and pp_patterns patterns = and pp_capture_variable = let clean s = let s = String.sub s 1 (String.length s - 1) in - String.sub s 0 (String.length s - 1) + String.sub s 0 (String.length s - 2) in function | term, None -> pp_term term -- 2.39.2