* generate list elements in correct order

* handle list inside boxes
* handle box layout
* generate separator between elements (not after elements)

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 79316319a7a7c42385d2f7dc4951f9ddde7d1e14..529353daa3e492e0d7ff12c3bc55795c368731d9 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -223,8 +223,14 @@ let set_compiled32 f = compiled32 := Some f
 
 let instantiate21 env precedence associativity l1 =
   prerr_endline "instantiate21";
-  let rec subst last_box env = function
-    | Ast.AttributedTerm (_, t) -> subst last_box env t
+  let boxify = function
+    | [t] -> t
+    | tl -> Ast.Layout (Ast.Box (Ast.H, tl))
+  in
+  let rec subst_singleton env t =
+    boxify (subst env t)
+  and subst env = function
+    | Ast.AttributedTerm (_, t) -> subst env t
     | Ast.Variable var ->
         let name, expected_ty = CicNotationEnv.declaration_of_var var in
         let ty, value =
@@ -236,12 +242,12 @@ let instantiate21 env precedence associativity 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 last_box env m
-    | Ast.Literal _ as t -> t
-    | Ast.Layout l -> Ast.Layout (subst_layout last_box env l)
-    | t -> CicNotationUtil.visit_ast (subst last_box env) t
-  and subst_magic last_box env = function
+        [ CicNotationEnv.term_of_value value ]
+    | Ast.Magic m -> subst_magic env m
+    | Ast.Literal _ as 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.List0 (p, sep_opt)
     | Ast.List1 (p, sep_opt) ->
         let rec_decls = CicNotationEnv.declarations_of_term p in
@@ -256,12 +262,14 @@ let instantiate21 env precedence associativity l1 =
         in
         let rec instantiate_list acc = function
           | [] -> List.rev acc
+         | value_set :: [] ->
+             let env = CicNotationEnv.combine rec_decls value_set in
+               instantiate_list ((boxify (subst env p)) :: acc) []
           | value_set :: tl ->
               let env = CicNotationEnv.combine rec_decls value_set in
-              instantiate_list ([subst last_box env p] @ sep @ acc) tl
+              instantiate_list ((boxify (subst env p @ sep)) :: acc) tl
         in
-        let children = instantiate_list [] values in
-        CicNotationPt.Layout (CicNotationPt.Box (last_box, children))
+        instantiate_list [] (List.rev values)
     | Ast.Opt p ->
         let opt_decls = CicNotationEnv.declarations_of_term p in
         let env =
@@ -275,18 +283,17 @@ let instantiate21 env precedence associativity l1 =
           in
           try build_env opt_decls with Exit -> []
         in
-        let children =
-          if env = [] then []
-          else [subst last_box env p]
-        in
-        CicNotationPt.Layout (CicNotationPt.Box (last_box, children))
+         begin
+           match env with
+             | [] -> []
+             | _ -> subst env p
+         end
     | _ -> assert false (* impossible *)
-  and subst_layout last_box env l =
-    CicNotationUtil.visit_layout (subst last_box env) l
-    (* TODO ZACK here we need to remember the last box traversed, but
-     * visit_layout is opaque :-((( *)
+  and subst_layout env = function
+    | Ast.Box (kind, tl) -> Ast.Box (kind, List.concat (List.map (subst env) tl))
+    | l -> CicNotationUtil.visit_layout (subst_singleton env) l
   in
-  subst CicNotationPt.H env l1
+    subst_singleton env l1
 
 let rec pp_ast1 term = 
   let rec pp_value = function