Several bugs fixed:

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

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 49cefaec7db3f7f76652d9e24e9543bd4de9f495..2873912c0129d51b9b17e9a6f2f3aae80c144797 100644 (file)
--- a/components/acic_content/cicNotationPp.ml
+++ b/components/acic_content/cicNotationPp.ml
@@ -79,6 +79,11 @@ let pp_attribute =
   | `Loc _ -> "@"
   | `ChildPos p -> sprintf "P(%s)" (pp_pos p)
 
+let pp_capture_variable pp_term = 
+  function
+  | term, None -> pp_term (* ~pp_parens:false *) term
+  | term, Some typ -> "(" ^ pp_term (* ~pp_parens:false *) term ^ ": " ^ pp_term typ ^ ")"
+
 let rec pp_term ?(pp_parens = true) t =
   let t_pp =
     match t with
@@ -94,7 +99,7 @@ let rec pp_term ?(pp_parens = true) t =
           (match typ with None -> "?" | Some typ -> pp_term typ)
           (pp_term ~pp_parens:true body)
     | Ast.Binder (kind, var, body) ->
-        sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var)
+        sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable pp_term var)
           (pp_term ~pp_parens:true body)
     | Ast.Case (term, indtype, typ, patterns) ->
         sprintf "match %s%s%s with %s"
@@ -111,33 +116,24 @@ let rec pp_term ?(pp_parens = true) t =
           (pp_patterns patterns)
     | 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 \\def %s in %s" (pp_capture_variable var) (pp_term ~pp_parens:true t1)
+        sprintf "let %s \\def %s in %s" (pp_capture_variable pp_term var) (pp_term ~pp_parens:true t1)
           (pp_term ~pp_parens:true t2)
     | Ast.LetRec (kind, definitions, term) ->
-        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
+          | []                   -> (*assert false*) Ast.Implicit
           | [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
+       let map (params, (id,typ), body, i) =
+         let typ =
+          match typ with
+             None -> Ast.Implicit
+           | Some typ -> typ
+         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))
+             (String.concat " " (List.map (pp_capture_variable pp_term) params))
+             (pp_term ~pp_parens:false (get_guard i params))
              (pp_term typ) (pp_term body)
        in
        sprintf "let %s %s in %s"
@@ -192,17 +188,12 @@ and pp_pattern ((head, href, vars), term) =
     | [] -> head_pp
     | _ ->
         sprintf "(%s %s)" head_pp
-          (String.concat " " (List.map pp_capture_variable vars)))
+          (String.concat " " (List.map (pp_capture_variable pp_term) vars)))
     (pp_term term)
 
 and pp_patterns patterns =
   sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns))
 
-and pp_capture_variable = 
-  function
-  | 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
   let kind_string =
@@ -266,17 +257,13 @@ 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
+let pp_params pp_term = function
   | [] -> ""
-  | params ->
-      " " ^
-      String.concat " "
-        (List.map
-          (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term typ))
-          params)
+  | params -> " " ^ String.concat " " (List.map (pp_capture_variable pp_term) params)
       
 let pp_flavour = function
   | `Definition -> "definition"
+  | `MutualDefinition -> assert false
   | `Fact -> "fact"
   | `Goal -> "goal"
   | `Lemma -> "lemma"
@@ -285,7 +272,7 @@ let pp_flavour = function
   | `Variant -> "variant"
   | `Axiom -> "axiom"
 
-let pp_fields fields =
+let pp_fields pp_term fields =
   (if fields <> [] then "\n" else "") ^ 
   String.concat ";\n" 
     (List.map 
@@ -295,7 +282,7 @@ let pp_fields fields =
           if arity > 0 then string_of_int arity else "" ^ ">") else ": " ^
         pp_term ty) fields)
         
-let pp_obj = function
+let pp_obj pp_term = function
  | Ast.Inductive (params, types) ->
     let pp_constructors constructors =
       String.concat "\n"
@@ -311,10 +298,12 @@ let pp_obj = function
     | (name, inductive, typ, constructors) :: tl ->
         let fst_typ_pp =
           sprintf "%sinductive %s%s: %s \\def\n%s"
-            (if inductive then "" else "co") name (pp_params params)
+            (if inductive then "" else "co") name (pp_params pp_term params)
             (pp_term typ) (pp_constructors constructors)
         in
         fst_typ_pp ^ String.concat "" (List.map pp_type tl))
+ | Ast.Theorem (`MutualDefinition, name, typ, body) ->
+    sprintf "<<pretty printing of mutual definitions not implemented yet>>"
  | Ast.Theorem (flavour, name, typ, body) ->
     sprintf "%s %s:\n %s\n%s"
       (pp_flavour flavour)
@@ -324,8 +313,8 @@ let pp_obj = function
       | None -> ""
       | Some body -> "\\def\n " ^ pp_term body)
  | Ast.Record (params,name,ty,fields) ->
-    "record " ^ name ^ " " ^ pp_params params ^ ": " ^ pp_term ty ^ 
-    " \\def {" ^ pp_fields fields ^ "\n}"
+    "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^ 
+    " \\def {" ^ pp_fields pp_term fields ^ "\n}"
 
 let rec pp_value = function
   | Env.TermValue t -> sprintf "$%s$" (pp_term t)