New content level representations for LetRec, Inductive and CoInductive.

[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 785c8bd8687794049dbd0000cf57685580378880..47bfe2748693c07975996bd6f7662fb91ddc44d4 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -114,33 +114,21 @@ let rec pp_term ?(pp_parens = true) t =
         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) ->
-        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*) 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
-             | term, None ->
-                 let pbody = Ast.Implicit in
-                let pvars, bbody = strip i body in
-                term, pvars, pbody, bbody
-          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 params))
+             (pp_term ~pp_parens:false (get_guard i params))
              (pp_term typ) (pp_term body)
        in
        sprintf "let %s %s in %s"
@@ -271,12 +259,7 @@ let set_pp_term f = _pp_term := f
 
 let pp_params = 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 params)
       
 let pp_flavour = function
   | `Definition -> "definition"