X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=4a02c8fff2affac5115259a96257184cbf25c847;hb=dfdff98e4417bae54fcf31d49c8a4d718c4487c2;hp=b1892e64a1973fe767afb237c7285d931f5d1e95;hpb=e4d0e879c6288190ae793e1425b1ed74e40346c4;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index b1892e64a..4a02c8fff 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -73,6 +73,7 @@ let resolve_binder = function
   | `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 rec remove_level_info =
   function
@@ -426,14 +427,15 @@ let add_idrefs =
   List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
 
 let instantiate21 idrefs env l1 =
-  let rec subst_singleton env =
+  let rec subst_singleton pos env =
     function
       Ast.AttributedTerm (attr, t) ->
-        Ast.AttributedTerm (attr, subst_singleton env t)
-    | t -> CicNotationUtil.group (subst env t)
-  and subst env = function
+        Ast.AttributedTerm (attr, subst_singleton pos env t)
+    | t -> CicNotationUtil.group (subst pos env t)
+  and subst pos env = function
     | Ast.AttributedTerm (attr, t) as term ->
-        subst env t
+        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
         let ty, value =
@@ -447,16 +449,16 @@ let instantiate21 idrefs env l1 =
         (* following assertion should be a conditional that makes this
          * instantiation fail *)
         assert (CicNotationEnv.well_typed expected_ty value);
-        [ CicNotationEnv.term_of_value value ]
-    | Ast.Magic m -> subst_magic env m
+        [ add_pos_info pos (CicNotationEnv.term_of_value value) ]
+    | Ast.Magic m -> subst_magic pos env m
     | Ast.Literal l as t ->
         let t = add_idrefs idrefs t in
         (match l with
         | `Keyword k -> [ add_keyword_attrs t ]
         | _ -> [ t ])
-    | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ]
-    | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ]
-  and subst_magic env = function
+    | Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ]
+    | t -> [ CicNotationUtil.visit_ast (subst_singleton pos env) t ]
+  and subst_magic pos env = function
     | Ast.List0 (p, sep_opt)
     | Ast.List1 (p, sep_opt) ->
         let rec_decls = CicNotationEnv.declarations_of_term p in
@@ -473,10 +475,11 @@ let instantiate21 idrefs env l1 =
           | [] -> List.rev acc
 	  | value_set :: [] ->
 	      let env = CicNotationEnv.combine rec_decls value_set in
-              instantiate_list (CicNotationUtil.group (subst env p) :: acc) []
+              instantiate_list (CicNotationUtil.group (subst pos env p) :: acc)
+                []
           | value_set :: tl ->
               let env = CicNotationEnv.combine rec_decls value_set in
-              let terms = subst env p in
+              let terms = subst pos env p in
               instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl
         in
         instantiate_list [] values
@@ -496,15 +499,37 @@ let instantiate21 idrefs env l1 =
 	  begin
 	    match env with
 	      | [] -> []
-	      | _ -> subst env p
+	      | _ -> subst pos env p
 	  end
     | _ -> assert false (* impossible *)
-  and subst_layout env = function
+  and subst_layout pos env = function
     | Ast.Box (kind, tl) ->
-        Ast.Box (kind, List.concat (List.map (subst env) tl))
-    | l -> CicNotationUtil.visit_layout (subst_singleton env) l
+        let tl' = subst_children pos env tl in
+        Ast.Box (kind, List.concat tl')
+    | l -> CicNotationUtil.visit_layout (subst_singleton pos env) l
+  and subst_children pos env =
+    function
+    | [] -> []
+    | [ child ] ->
+        let pos' =
+          match pos with
+          | `Inner -> `Right
+          | `Left -> `Left
+          | `None -> assert false
+          | `Right -> `Right
+        in
+        [ subst pos' env child ]
+    | hd :: tl ->
+        let pos' =
+          match pos with
+          | `Inner -> `Inner
+          | `Left -> `Inner
+          | `None -> assert false
+          | `Right -> `Right
+        in
+        (subst pos env hd) :: subst_children pos' env tl
   in
-    subst_singleton env l1
+    subst_singleton `Left env l1
 
 let rec pp_ast1 term = 
   let rec pp_value = function