the in clause of the match costruction was wrongly output

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

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 5f45b2a4ba72d23ea6f942d6124357578f3b2508..cdc0946e6f96bd2d992984bd1043ffc3a7aa9932 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -92,13 +92,12 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Binder (`Pi, (Ast.Ident ("_", None), typ), body) ->
         sprintf "%s \\to %s"
           (match typ with None -> "?" | Some typ -> pp_term typ)
-          (pp_term body)
+          (pp_term ~pp_parens:true body)
     | Ast.Binder (kind, var, body) ->
         sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var)
-          (pp_term body)
+          (pp_term ~pp_parens:true 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 indtype with
           | None -> ""
@@ -107,20 +106,43 @@ let rec pp_term ?(pp_parens = true) t =
               (match debug_printing, href_opt with
               | true, Some uri ->
                   sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
-              | _ -> ""))
+              | _ -> ""))        
+         (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))          
           (pp_patterns patterns)
-    | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2)
+    | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
     | Ast.LetIn (var, t1, t2) ->
-        sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1)
-          (pp_term t2)
+        sprintf "let %s \\def %s in %s" (pp_capture_variable var) (pp_term ~pp_parens:true t1)
+          (pp_term ~pp_parens:true t2)
     | Ast.LetRec (kind, definitions, term) ->
-        sprintf "let %s %s in %s"
+        let strip i t =
+          let rec aux i l = function
+             | Ast.Binder (_, var, body) when i > 0 -> aux (pred i) (var :: l) body
+             | body                                 -> List.rev l, body
+          in 
+          aux i [] t
+       in
+       let rec get_guard i = function
+          | []                   -> assert false
+          | [term, _] when i = 1 -> term
+          | _ :: tl              -> get_guard (pred i) tl
+       in
+       let map (var, body, i) =
+           let id, vars, typ, body = match var with
+             | term, Some typ ->
+                let pvars, pbody = strip i typ in
+                let _, bbody = strip i body in
+                term, pvars, pbody, bbody
+             | _              -> assert false
+          in
+          sprintf "%s %s on %s: %s \\def %s" 
+             (pp_term ~pp_parens:false term)
+             (String.concat " " (List.map pp_capture_variable vars))
+             (pp_term ~pp_parens:false (get_guard i vars))
+             (pp_term typ) (pp_term body)
+       in
+       sprintf "let %s %s in %s"
           (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
-          (String.concat " and "
-            (List.map
-              (fun (var, body, _) ->
-                sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
-              definitions))
+          (String.concat " and " (List.map map definitions))
           (pp_term term)
     | Ast.Ident (name, Some []) | Ast.Ident (name, None)
     | Ast.Uri (name, Some []) | Ast.Uri (name, None) ->
@@ -147,8 +169,13 @@ 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
-  else t_pp
+  match pp_parens, t with
+    | false, _ 
+    | true, Ast.Implicit
+    | true, Ast.Sort _
+    | true, Ast.Ident (_, Some []) 
+    | true, Ast.Ident (_, None)    -> t_pp
+    | _                            -> sprintf "(%s)" t_pp
 
 and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
 and pp_substs substs = String.concat "; " (List.map pp_subst substs)
@@ -172,13 +199,9 @@ and pp_patterns patterns =
   sprintf "[%s]" (String.concat " | " (List.map pp_pattern 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) 
-  in
   function
-  | term, None -> pp_term term
-  | term, Some typ -> "(" ^ clean (pp_term term) ^ ": " ^ pp_term typ ^ ")"
+  | term, None -> pp_term ~pp_parens:false term
+  | term, Some typ -> "(" ^ pp_term ~pp_parens:false term ^ ": " ^ pp_term typ ^ ")"
 
 and pp_box_spec (kind, spacing, indent) =
   let int_of_bool b = if b then 1 else 0 in
@@ -253,7 +276,7 @@ let pp_params = function
           params)
       
 let pp_flavour = function
-  | `Definition -> "Definition"
+  | `Definition -> "definition"
   | `Fact -> "fact"
   | `Goal -> "goal"
   | `Lemma -> "lemma"
@@ -290,16 +313,16 @@ let pp_obj = function
         in
         fst_typ_pp ^ String.concat "" (List.map pp_type tl))
  | Ast.Theorem (flavour, name, typ, body) ->
-    sprintf "%s %s: %s %s"
+    sprintf "%s %s:\n %s\n%s"
       (pp_flavour flavour)
       name
       (pp_term typ)
       (match body with
       | None -> ""
-      | Some body -> "\\def " ^ pp_term body)
+      | Some body -> "\\def\n " ^ pp_term body)
  | Ast.Record (params,name,ty,fields) ->
-    "record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^
-    pp_fields fields ^ "}"
+    "record " ^ name ^ " " ^ pp_params params ^ ": " ^ pp_term ty ^ 
+    " \\def {" ^ pp_fields fields ^ "\n}"
 
 let rec pp_value = function
   | Env.TermValue t -> sprintf "$%s$" (pp_term t)