- bugfix: eta abstractions ignores attributed node while counting lambdas

[helm.git] / helm / ocaml / cic_notation / grafiteAstPp.ml

diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml
index b7a62476cf26b05a9c3d52d4a426aadca0604c7b..6a8e79bc10722535c8dff3df30ab016144ace9fe 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteAstPp.ml
+++ b/helm/ocaml/cic_notation/grafiteAstPp.ml
@@ -27,6 +27,8 @@ open Printf
 
 open GrafiteAst
 
+module Ast = CicNotationPt
+
 let tactical_terminator = "."
 let tactic_terminator = tactical_terminator
 let command_terminator = tactical_terminator
@@ -39,10 +41,12 @@ let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
 let pp_terms_ast terms = String.concat ", " (List.map pp_term_ast terms)
 
 let pp_reduction_kind = function
+  | `Normalize -> "normalize"
   | `Reduce -> "reduce"
   | `Simpl -> "simplify"
+  | `Unfold (Some t) -> "unfold " ^ pp_term_ast t
+  | `Unfold None -> "unfold"
   | `Whd -> "whd"
-  | `Normalize -> "normalize"
  
   
 let pp_pattern (t, hyp, goal) = 
@@ -78,8 +82,15 @@ let rec pp_tactic = function
      "cut " ^ pp_term_ast term ^
       (match ident with None -> "" | Some id -> " as " ^ id)
   | DecideEquality _ -> "decide equality"
-  | Decompose (_, term) ->
-      sprintf "decompose %s" (pp_term_ast term)
+  | Decompose (_, [], what, names) ->
+      sprintf "decompose %s%s" what (pp_intros_specs (None, names)) 
+  | Decompose (_, types, what, names) ->
+      let to_ident = function
+         | Ident id -> id
+        | Type _   -> assert false 
+      in
+      let types = List.rev_map to_ident types in
+      sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names)) 
   | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
   | Elim (_, term, using, num, idents) ->
       sprintf "elim " ^ pp_term_ast term ^
@@ -230,7 +241,7 @@ let pp_obj = function
     pp_fields fields ^ "}"
 
 let pp_argument_pattern = function
-  | CicNotationPt.IdentArg (eta_depth, name) ->
+  | Ast.IdentArg (eta_depth, name) ->
       let eta_buf = Buffer.create 5 in
       for i = 1 to eta_depth do
         Buffer.add_string eta_buf "\\eta."
@@ -238,24 +249,26 @@ let pp_argument_pattern = function
       sprintf "%s%s" (Buffer.contents eta_buf) name
 
 let rec pp_cic_appl_pattern = function
-  | CicNotationPt.UriPattern uri -> UriManager.string_of_uri uri
-  | CicNotationPt.VarPattern name -> name
-  | CicNotationPt.ImplicitPattern -> "_"
-  | CicNotationPt.ApplPattern aps ->
+  | Ast.UriPattern uri -> UriManager.string_of_uri uri
+  | Ast.VarPattern name -> name
+  | Ast.ImplicitPattern -> "_"
+  | Ast.ApplPattern aps ->
       sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps))
 
 let pp_l1_pattern = CicNotationPp.pp_term
 let pp_l2_pattern = CicNotationPp.pp_term
 
 let pp_associativity = function
-  | Some Gramext.LeftA -> "left associative "
-  | Some Gramext.RightA -> "right associative "
-  | Some Gramext.NonA -> "non associative "
-  | None -> ""
+  | Gramext.LeftA -> "left associative"
+  | Gramext.RightA -> "right associative"
+  | Gramext.NonA -> "non associative"
+
+let pp_precedence i = sprintf "with precedence %d" i
 
-let pp_precedence = function
-  | Some i -> sprintf "with precedence %d " i
+let pp_dir_opt = function
   | None -> ""
+  | Some `LeftToRight -> "> "
+  | Some `RightToLeft -> "< "
 
 let pp_command = function
   | Include (_,path) -> "include " ^ path
@@ -273,8 +286,9 @@ let pp_command = function
         dsc symbol
         (String.concat " " (List.map pp_argument_pattern arg_patterns))
         (pp_cic_appl_pattern cic_appl_pattern)
-  | Notation (_, l1_pattern, assoc, prec, l2_pattern) ->
-      sprintf "notation \"%s\" %s%sfor %s"
+  | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
+      sprintf "notation %s\"%s\" %s %s for %s"
+        (pp_dir_opt dir_opt)
         (pp_l1_pattern l1_pattern)
         (pp_associativity assoc)
         (pp_precedence prec)
@@ -327,3 +341,8 @@ let pp_cic_command = function
   | Notation _
   | Obj _ -> assert false (* not implemented *)
 
+let pp_dependency = function
+  | IncludeDep str -> "include \"" ^ str ^ "\""
+  | BaseuriDep str -> "set \"baseuri\" \"" ^ str ^ "\""
+  | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\""
+