trying to make output notation parsable

[helm.git] / components / acic_content / cicNotationPp.ml

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index ee389022c5721097764d10f4fab34acf512d560f..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)
@@ -171,9 +171,14 @@ and pp_pattern ((head, href, vars), term) =
 and pp_patterns patterns =
   sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns))
 
-and pp_capture_variable = function
+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 - 2) 
+  in
+  function
   | term, None -> pp_term term
-  | term, Some typ -> "(" ^ pp_term term ^ ": " ^ pp_term typ ^ ")"
+  | term, Some typ -> "(" ^ clean (pp_term term) ^ ": " ^ pp_term typ ^ ")"
 
 and pp_box_spec (kind, spacing, indent) =
   let int_of_bool b = if b then 1 else 0 in
@@ -234,7 +239,9 @@ and pp_variable = function
   | Ast.Ascription (t, n) -> assert false
   | Ast.FreshVar n -> "fresh " ^ n
 
-let pp_term t = pp_term ~pp_parens:false t
+let _pp_term = ref (pp_term ~pp_parens:false)
+let pp_term t = !_pp_term t
+let set_pp_term f = _pp_term := f
 
 let pp_params = function
   | [] -> ""
@@ -253,6 +260,7 @@ let pp_flavour = function
   | `Remark -> "remark"
   | `Theorem -> "theorem"
   | `Variant -> "variant"
+  | `Axiom -> "axiom"
 
 let pp_fields fields =
   (if fields <> [] then "\n" else "") ^