trying to make output notation parsable

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 5f45b2a4ba72d23ea6f942d6124357578f3b2508..a23d26add935eef6a406e1cc1a7a55bee7621f35 100644 (file)
--- 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