better precedence handling, should remove useless parens

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

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 4a02c8fff2affac5115259a96257184cbf25c847..aa171c55ccedd2aed0a86da4b99de8b0e73b08b8 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -74,6 +74,16 @@ let resolve_binder = function
 
 let add_level_info prec assoc t = Ast.AttributedTerm (`Level (prec, assoc), t)
 let add_pos_info pos t = Ast.AttributedTerm (`ChildPos pos, t)
+let left_pos = add_pos_info `Left
+let right_pos = add_pos_info `Right
+let inner_pos = add_pos_info `Inner
+
+let rec top_pos t = add_level_info ~-1 Gramext.NonA (inner_pos t)
+(*   function
+  | Ast.AttributedTerm (`Level _, t) ->
+      add_level_info ~-1 Gramext.NonA (inner_pos t)
+  | Ast.AttributedTerm (attr, t) -> Ast.AttributedTerm (attr, top_pos t)
+  | t -> add_level_info ~-1 Gramext.NonA (inner_pos t) *)
 
 let rec remove_level_info =
   function
@@ -126,14 +136,23 @@ let pp_ast0 t k =
   let rec aux =
     function
     | Ast.Appl ts ->
+        let rec aux_args pos =
+          function
+          | [] -> []
+          | [ last ] ->
+              let last = k last in
+              if pos = `Left then [ left_pos last ] else [ right_pos last ]
+          | hd :: tl ->
+              (add_pos_info pos (k hd)) :: aux_args `Inner tl
+        in
         add_level_info Ast.apply_prec Ast.apply_assoc
-          (hovbox true true (CicNotationUtil.dress break (List.map k ts)))
+          (hovbox true true (CicNotationUtil.dress break (aux_args `Left ts)))
     | Ast.Binder (binder_kind, (id, ty), body) ->
         add_level_info Ast.binder_prec Ast.binder_assoc
           (hvbox false true
             [ binder_symbol (resolve_binder binder_kind);
               k id; builtin_symbol ":"; aux_ty ty; break;
-              builtin_symbol "."; k body ])
+              builtin_symbol "."; right_pos (k body) ])
     | Ast.Case (what, indty_opt, outty_opt, patterns) ->
         let outty_box =
           match outty_opt with
@@ -150,7 +169,7 @@ let pp_ast0 t k =
         let match_box =
           hvbox false true [
             keyword "match"; break;
-            hvbox false false ([ k what ] @ indty_box); break;
+            hvbox false false ([ top_pos (k what) ] @ indty_box); break;
             keyword "with" ]
         in
         let mk_case_pattern (head, href, vars) =
@@ -163,7 +182,7 @@ let pp_ast0 t k =
                 (hvbox false true [
                   hbox false true [
                     mk_case_pattern lhs; builtin_symbol "\\Rightarrow" ];
-                  break; k rhs ]))
+                  break; top_pos (k rhs) ]))
             patterns
         in
         let patterns'' =
@@ -195,15 +214,15 @@ let pp_ast0 t k =
     | Ast.Cast (bo, ty) ->
         add_level_info Ast.simple_prec Ast.simple_assoc
           (hvbox false true [
-            builtin_symbol "("; k bo; break; builtin_symbol ":"; k ty;
-            builtin_symbol ")"])
+            builtin_symbol "("; top_pos (k bo); break; builtin_symbol ":";
+            top_pos (k ty); builtin_symbol ")"])
     | Ast.LetIn (var, s, t) ->
         add_level_info Ast.let_in_prec Ast.let_in_assoc
           (hvbox false true [
             hvbox false true [
               keyword "let";
               hvbox false true [
-                aux_var var; builtin_symbol "\\def"; break; k s ];
+                aux_var var; builtin_symbol "\\def"; break; top_pos (k s) ];
               break; keyword "in" ];
             break;
             k t ])
@@ -220,7 +239,7 @@ let pp_ast0 t k =
           let (name, body) = fst_fun in
           hvbox false true [
             keyword "let"; keyword rec_op; name; builtin_symbol "\\def"; break;
-            body ]
+            top_pos body ]
         in
         let tl_rows =
           List.map
@@ -434,7 +453,7 @@ let instantiate21 idrefs env l1 =
     | t -> CicNotationUtil.group (subst pos env t)
   and subst pos env = function
     | Ast.AttributedTerm (attr, t) as term ->
-        prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr);
+(*         prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr); *)
         subst pos env t
     | Ast.Variable var ->
         let name, expected_ty = CicNotationEnv.declaration_of_var var in
@@ -515,7 +534,7 @@ let instantiate21 idrefs env l1 =
           match pos with
           | `Inner -> `Right
           | `Left -> `Left
-          | `None -> assert false
+(*           | `None -> assert false *)
           | `Right -> `Right
         in
         [ subst pos' env child ]
@@ -524,7 +543,7 @@ let instantiate21 idrefs env l1 =
           match pos with
           | `Inner -> `Inner
           | `Left -> `Inner
-          | `None -> assert false
+(*           | `None -> assert false *)
           | `Right -> `Right
         in
         (subst pos env hd) :: subst_children pos' env tl
@@ -557,13 +576,12 @@ let rec pp_ast1 term =
           let idrefs =
             List.flatten (List.map CicNotationUtil.get_idrefs ctors)
           in
-          let prec, assoc, l1 =
+          let l1 =
             try
               Hashtbl.find level1_patterns21 pid
             with Not_found -> assert false
           in
-          add_level_info prec assoc
-            (instantiate21 idrefs (ast_env_of_env env) l1))
+          instantiate21 idrefs (ast_env_of_env env) l1)
 
 let instantiate32 term_info idrefs env symbol args =
   let rec instantiate_arg = function
@@ -680,10 +698,24 @@ let lookup_interpretations symbol =
       !(Hashtbl.find interpretations symbol)))
   with Not_found -> raise Interpretation_not_found
 
+let fill_pos_info l1_pattern = l1_pattern
+(*   let rec aux toplevel pos =
+    function
+    | Ast.Layout l ->
+        (match l 
+
+    | Ast.Magic m ->
+        Ast.Box (
+    | Ast.Variable _ as t -> add_pos_info pos t
+    | t -> t
+  in
+  aux true l1_pattern *)
+
 let add_pretty_printer ~precedence ~associativity l2 l1 =
   let id = fresh_id () in
+  let l1' = add_level_info precedence associativity (fill_pos_info l1) in
   let l2' = CicNotationUtil.strip_attributes l2 in
-  Hashtbl.add level1_patterns21 id (precedence, associativity, l1);
+  Hashtbl.add level1_patterns21 id l1';
   pattern21_matrix := (l2', id) :: !pattern21_matrix;
   load_patterns21 !pattern21_matrix;
   id