Fix list bounds with subrules

regression/config.otr

@@ -11,6 +11,7 @@
 . . . . . + ../tests/test_jan_2006-09-08.ott
 + + . + + + ../tests/test_lists_coq_list_functions_4.ott
 + + . + + + ../tests/test_lists_coq_list_functions_3.ott
++ + . + + + ../tests/test_lists_coq_defn_subrule_4.ott
 + + . + + + ../tests/test_lists_coq_defn_subrule_3.ott
 + + . + + + ../tests/test_lists_coq_defn_subrule_2.ott
 + + . + + + ../tests/test_lists_coq_defn_subrule_1.ott 

regression/regression.otl

@@ -86,6 +86,7 @@ sys-purercdsub : ../examples/tapl/common.ott ../examples/tapl/common_typing.ott
 ../tests/test_lists_coq_defn_subrule_1.ott
 ../tests/test_lists_coq_defn_subrule_2.ott
 ../tests/test_lists_coq_defn_subrule_3.ott
+../tests/test_lists_coq_defn_subrule_4.ott
 ../tests/test_lists_coq_defn_tuple_1.ott
 ../tests/test_lists_coq_defn_tuple_2.ott
 ../tests/test_lists_coq_list_functions_1.ott

src/bounds.ml

@@ -321,11 +321,44 @@ let dotenv23 ntmvsn_without_bounds ntmvsn_with_bounds  =
   let de3 = Auxl.option_map (function ((ntmv,subntr_data),zo)->match zo with None->Some(ntmv,subntr_data)|Some z -> None) y in
   de2,de3
 
+let coalesce_bounds xd loc x : ((Types.nt_or_mv * Types.subntr_data) * Types.bound option) list =
+  let merge_data (nm : Types.nt_or_mv) d1 d2 : Types.subntr_data = match (d1, d2) with
+    | (None, d) -> d
+      | (d, None) -> d
+      | (Some d1, Some d2) ->
+        if d1 == d2 then (Some d1) else
+          raise (Bounds (
+              loc,
+              "incompatible subntr_data "
+              ^ (Grammar_pp.pp_plain_subntr_data (Some d1))
+              ^ " and " ^ (Grammar_pp.pp_plain_subntr_data (Some d2))
+              ^ "on nonterminal "
+              ^ (Grammar_pp.pp_nt_or_mv (Types.pp_ascii_opts_default) xd nm)  ))
+  in let merge_bounds (nm : Types.nt_or_mv) b1 b2 : Types.bound option = match (b1, b2) with
+      | (None, b) -> b
+      | (b, None) -> b
+      | (Some b1, Some b2) ->
+        if b1 == b2 then (Some b1) else
+          raise (Bounds (
+              loc,
+              "incompatible bounds "
+              ^ (Grammar_pp.pp_plain_bound b1)
+              ^ " and " ^ (Grammar_pp.pp_plain_bound b2)
+              ^ "on nonterminal "
+              ^ (Grammar_pp.pp_nt_or_mv (Types.pp_ascii_opts_default) xd nm)  ))
+  in let names = Auxl.remove_duplicates (List.map (fun ((a,b),c) -> a) x)
+  in let namesMatching nm =  List.filter (fun  ((ntmv, _),_) -> ntmv == nm) x
+  in let merge_pairs ((nm,d1),b1) ((_,d2),b2) =
+       ((nm, merge_data nm d1 d2), merge_bounds nm b1 b2)
+  in List.map (fun nm ->
+       let matching = (namesMatching nm )
+       in List.fold_right merge_pairs matching (List.hd matching)) names
 
 
 let bound_extraction m xd loc sts : dotenv * dotenv3 * string = 
   try  
-    let x = nt_or_mv_of_symterms sts in
+    let x_unc =  nt_or_mv_of_symterms sts in
+    let x = coalesce_bounds xd loc x_unc in
     let bounds = check_length_consistency loc x in
     let pp_bounds = String.concat "  " 
         (List.map Grammar_pp.pp_plain_bound bounds) in

tests/test_lists_coq_defn_subrule_4.ott

@@ -0,0 +1,44 @@
+% Mixing list bounds with subrules
+% Should pass on all targets, but previous versions failed
+% in Coq with "The variable tau_ is bound several times in pattern"
+% due to an error in how bound were calculated for sub-non-terminals
+
+metavar var, X ::= {{coq nat}} 
+
+indexvar n ::=  {{coq nat}}
+
+grammar
+
+Kind, K :: kind_ ::= 
+  | KindStar :: :: KindStar 
+
+typexpr, T :: T_ ::=                  
+    | X                   ::   :: var                     
+    | ForAll << X1 , .. , Xn >> .  T            ::   :: polyarrow
+    |  [ X1 |-> tau1 .. Xn |-> taun ] T        :: M :: tsub  {{icho  [[T]]  }}
+
+tau :: tau_ ::=    
+    | X                   ::   :: var   
+
+    formula :: 'formula_' ::=
+      | judgement           ::   :: judgement
+      | formula1 .. formulan :: :: dots
+
+    subrules
+      tau <:: T
+
+    defns
+      Jtype :: '' ::=
+
+    defn
+        |- T : K :: :: kind :: Kind by
+
+        ------------------------------------ :: Var
+        |- T : KindStar
+
+    defn
+        |- T <: T' :: :: sub :: Sub by
+
+        </ |-  taun : KindStar // n />
+        ------------------------------------------ :: InstL
+        |-  ForAll << </ Xn // n /> >> .  T  <: [ </ Xn |-> taun // n /> ] T