notation on steroids: 'term 40 x' is a valid variable name in notation and

[helm.git] / helm / software / components / content_pres / termContentPres.ml

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 8f15664d0342fb7bdeb1b5131863e90f97d577bd..89dba29879c05208045c4685cc2e6c3f0e92b319 100644 (file)
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -42,18 +42,9 @@ let resolve_binder = function
   | `Forall -> "\\forall"
   | `Exists -> "\\exists"
 
-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 add_level_info prec t = Ast.AttributedTerm (`Level prec, t)
+
+let rec top_pos t = add_level_info ~-1 t
 
 let rec remove_level_info =
   function
@@ -112,18 +103,18 @@ let pp_ast0 t k =
           | [] -> []
           | [ last ] ->
               let last = k last in
-              if pos = `Left then [ left_pos last ] else [ right_pos last ]
+              [ last ]
           | hd :: tl ->
-              (add_pos_info pos (k hd)) :: aux_args `Inner tl
+              (k hd) :: aux_args `Inner tl
         in
-        add_level_info Ast.apply_prec Ast.apply_assoc
+        add_level_info Ast.apply_prec 
           (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
+        add_level_info Ast.binder_prec
           (hvbox false true
             [ binder_symbol (resolve_binder binder_kind);
               k id; builtin_symbol ":"; aux_ty ty; break;
-              builtin_symbol "."; right_pos (k body) ])
+              builtin_symbol "."; k body ])
     | Ast.Case (what, indty_opt, outty_opt, patterns) ->
         let outty_box =
           match outty_opt with
@@ -189,17 +180,17 @@ let pp_ast0 t k =
               hbox false false [ builtin_symbol "["; hd ]
               :: aux_patterns tl
         in
-        add_level_info Ast.simple_prec Ast.simple_assoc
+        add_level_info Ast.simple_prec
           (hvbox false false [
             hvbox false false ([match_box]); break;
             hbox false false [ hvbox false false patterns'' ] ])
     | Ast.Cast (bo, ty) ->
-        add_level_info Ast.simple_prec Ast.simple_assoc
+        add_level_info Ast.simple_prec
           (hvbox false true [
             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
+        add_level_info Ast.let_in_prec 
           (hvbox false true [
             hvbox false true [
               keyword "let"; space;
@@ -251,7 +242,7 @@ let pp_ast0 t k =
                   [ builtin_symbol "\\def"; break; body ])])
             tl_funs
         in
-        add_level_info Ast.let_in_prec Ast.let_in_assoc
+        add_level_info Ast.let_in_prec
           ((hvbox false false
             (fst_row :: List.flatten tl_rows
              @ [ break; keyword "in"; break; k where ])))
@@ -337,7 +328,7 @@ let instantiate21 idrefs env l1 =
               Ast.AttributedTerm (`Level l,value) 
           | _ -> value
         in
-        [ add_pos_info pos value ]
+        [ value ]
     | Ast.Magic m -> subst_magic pos env m
     | Ast.Literal l as t ->
         let t = add_idrefs idrefs t in
@@ -486,9 +477,9 @@ let fresh_id =
     incr counter;
     !counter
 
-let add_pretty_printer ~precedence ~associativity l2 l1 =
+let add_pretty_printer l2 (CicNotationParser.CL1P (l1,precedence)) =
   let id = fresh_id () in
-  let l1' = add_level_info precedence associativity (fill_pos_info l1) in
+  let l1' = add_level_info precedence (fill_pos_info l1) in
   let l2' = CicNotationUtil.strip_attributes l2 in
   Hashtbl.add level1_patterns21 id l1';
   pattern21_matrix := (l2', id) :: !pattern21_matrix;