Fix treatment of {struct x} annotations in presence of generalized

binders.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13086 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 58 insertions, 39 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ecaba603d2..ceb0748fee 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1047,12 +1047,11 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let idl = Array.map
           (fun (id,(n,order),bl,ty,bd) ->
 	     let intern_ro_arg f =
-               let idx = Option.default 0 (index_of_annot bl n) in
-	       let before, after = list_chop idx bl in
+	       let before, after = split_at_annot bl n in
 	       let ((ids',_,_,_) as env',rbefore) =
 		 List.fold_left intern_local_binder (env,[]) before in
 	       let ro = f (intern (ids', unb, tmp_scope, scopes)) in
-	       let n' = Option.map (fun _ -> List.length before) n in
+	       let n' = Option.map (fun _ -> List.length rbefore) n in
 		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
 	     in
 	     let n, ro, ((ids',_,_,_),rbl) =
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 5fade008cf..e9a81f09ca 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -908,17 +908,25 @@ let coerce_to_name = function
 
 (* Interpret the index of a recursion order annotation *)
 
-let index_of_annot bl na =
+let split_at_annot bl na =
   let names = List.map snd (names_of_local_assums bl) in
   match na with
   | None ->
       if names = [] then error "A fixpoint needs at least one parameter." 
-      else None
+      else [], bl
   | Some (loc, id) ->
-      try Some (list_index0 (Name id) names)
-      with Not_found ->
-        user_err_loc(loc,"",
-        str "No parameter named " ++ Nameops.pr_id id ++ str".")
+      let rec aux acc = function
+	| LocalRawAssum (bls, k, t) as x :: rest ->
+	    let l, r = list_split_when (fun (loc, na) -> na = Name id) bls in
+	      if r = [] then aux (x :: acc) rest 
+	      else 
+		(List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc), 
+		 LocalRawAssum (r, k, t) :: rest)
+	| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
+	| [] ->
+            user_err_loc(loc,"",
+			 str "No parameter named " ++ Nameops.pr_id id ++ str".")
+      in aux [] bl
 
 (* Used in correctness and interface *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 8f1fa5c3d4..a30c14966a 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -198,7 +198,7 @@ val coerce_reference_to_id : reference -> identifier
 val coerce_to_id : constr_expr -> identifier located
 val coerce_to_name : constr_expr -> name located
 
-val index_of_annot : local_binder list -> identifier located option -> int option
+val split_at_annot : local_binder list -> identifier located option -> local_binder list * local_binder list
 
 val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
diff --git a/lib/util.ml b/lib/util.ml
index af5f2e33c4..42cdc2bf2c 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -800,6 +800,13 @@ let list_cartesians op init ll =
 
 let list_combinations l = list_cartesians (fun x l -> x::l) [] l
 
+let rec list_combine3 x y z = 
+  match x, y, z with
+  | [], [], [] -> []
+  | (x :: xs), (y :: ys), (z :: zs) ->
+      (x, y, z) :: list_combine3 xs ys zs
+  | _, _, _ -> raise (Invalid_argument "list_combine3")
+  
 (* Keep only those products that do not return None *)
 
 let rec list_cartesian_filter op l1 l2 =
diff --git a/lib/util.mli b/lib/util.mli
index 98d2b6cf9d..43dd439131 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -213,6 +213,7 @@ val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
 
 (** list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
 val list_combinations : 'a list list -> 'a list list
+val list_combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
 
 (** Keep only those products that do not return None *)
 val list_cartesian_filter :
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 9965e7be54..8a7d11d1d8 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -522,8 +522,8 @@ let build_recursive l b =
 		    m ntn false)
 
       | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
-	  let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) ->
-	    ({Command.fix_name = id; Command.fix_binders = bl; 
+	  let fixl = List.map (fun (((_,id),(n,ro),bl,typ,def),ntn) ->
+	    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = n;
 	      Command.fix_body = def; Command.fix_type = typ},ntn)) l
 	  in interp_recursive (IsFixpoint g) fixl b
       | _, _ ->
@@ -532,7 +532,7 @@ let build_recursive l b =
 
 let build_corecursive l b =
   let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
-    ({Command.fix_name = id; Command.fix_binders = bl; 
+    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = None;
       Command.fix_body = def; Command.fix_type = typ},ntn))
     l in
   interp_recursive IsCoFixpoint fixl b
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3e16a956a0..93c92b8f85 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -443,14 +443,18 @@ let check_mutuality env isfix fixl =
 
 type structured_fixpoint_expr = {
   fix_name : identifier;
+  fix_annot : identifier located option;
   fix_binders : local_binder list;
   fix_body : constr_expr option;
   fix_type : constr_expr
 }
 
-let interp_fix_context evdref env fix =
-  interp_context_evars evdref env fix.fix_binders
-
+let interp_fix_context evdref env isfix fix =
+  let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
+  let (env', ctx), imps = interp_context_evars evdref env before in
+  let (env'', ctx'), imps' = interp_context_evars evdref env' after in
+    ((env'', ctx' @ ctx), imps @ imps', Option.map (fun _ -> List.length ctx) fix.fix_annot)
+      
 let interp_fix_ccl evdref (env,_) fix =
   interp_type_evars evdref env fix.fix_type
 
@@ -482,8 +486,8 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
 
 (* Jump over let-bindings. *)
 
-let compute_possible_guardness_evidences na fix (nb,_) =
-  match index_of_annot fix.fix_binders na with
+let compute_possible_guardness_evidences (nb,_,na) =
+  match na with
   | Some i -> [i]
   | None ->
       (* If recursive argument was not given by user, we try all args.
@@ -502,8 +506,8 @@ let interp_recursive isfix fixl notations =
 
   (* Interp arities allowing for unresolved types *)
   let evdref = ref Evd.empty in
-  let fixctxs, fiximps =
-    List.split (List.map (interp_fix_context evdref env) fixl) in
+  let fixctxs, fiximps, fixannots =
+    list_split3 (List.map (interp_fix_context evdref env isfix) fixl) in
   let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let fixtypes = List.map (nf_evar !evdref) fixtypes in
@@ -533,7 +537,7 @@ let interp_recursive isfix fixl notations =
   end;
 
   (* Build the fix declaration block *)
-  (fixnames,fixdefs,fixtypes),List.combine fixctxlength fiximps
+  (fixnames,fixdefs,fixtypes), list_combine3 fixctxlength fiximps fixannots
 
 let interp_fixpoint = interp_recursive true
 let interp_cofixpoint = interp_recursive false
@@ -542,7 +546,7 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
   if List.mem None fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in
+      list_map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
@@ -553,7 +557,7 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let indexes = search_guard dummy_loc (Global.env()) indexes fixdecls in
-    let fiximps = List.map snd fiximps in
+    let fiximps = List.map (fun (n,r,p) -> r) fiximps in
     let fixdecls =
       list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps);
@@ -567,7 +571,7 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
   if List.mem None fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in
+      list_map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
@@ -578,7 +582,7 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-    let fiximps = List.map snd fiximps in
+    let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
@@ -587,28 +591,28 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
   List.iter Metasyntax.add_notation_interpretation ntns
 
 let extract_decreasing_argument = function
-  | (_,(na,CStructRec),_,_,_) -> na
+  | (na,CStructRec) -> na
   | _ -> error 
       "Only structural decreasing is supported for a non-Program Fixpoint"
 
 let extract_fixpoint_components l =
   let fixl, ntnl = List.split l in
-  let wfl = List.map extract_decreasing_argument fixl in
-  let fixl = List.map (fun ((_,id),_,bl,typ,def) ->
-    {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
-  fixl, List.flatten ntnl, wfl
+  let fixl = List.map (fun ((_,id),ann,bl,typ,def) ->
+    let ann = extract_decreasing_argument ann in
+      {fix_name = id; fix_annot = ann; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
+  fixl, List.flatten ntnl
 
 let extract_cofixpoint_components l =
   let fixl, ntnl = List.split l in
   List.map (fun ((_,id),bl,typ,def) ->
-    {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
+    {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
   List.flatten ntnl
 
 let do_fixpoint l b =
-  let fixl,ntns,wfl = extract_fixpoint_components l in
+  let fixl,ntns = extract_fixpoint_components l in
   let fix = interp_fixpoint fixl ntns in
   let possible_indexes =
-    list_map3 compute_possible_guardness_evidences wfl fixl (snd fix) in
+    List.map compute_possible_guardness_evidences (snd fix) in
   declare_fixpoint b fix possible_indexes ntns
 
 let do_cofixpoint l b =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index ab8329fb0b..57c8e0198b 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -94,6 +94,7 @@ val do_mutual_inductive :
 
 type structured_fixpoint_expr = {
   fix_name : identifier;
+  fix_annot : identifier located option;
   fix_binders : local_binder list;
   fix_body : constr_expr option;
   fix_type : constr_expr
@@ -104,8 +105,7 @@ type structured_fixpoint_expr = {
 
 val extract_fixpoint_components :
   (fixpoint_expr * decl_notation list) list ->
-    structured_fixpoint_expr list * decl_notation list *
-    (** possible structural arg: *) lident option list
+    structured_fixpoint_expr list * decl_notation list
 
 val extract_cofixpoint_components :
   (cofixpoint_expr * decl_notation list) list ->
@@ -118,20 +118,20 @@ type recursive_preentry =
 
 val interp_fixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * (int * manual_implicits) list
+    recursive_preentry * (int * manual_implicits * int option) list
 
 val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * (int * manual_implicits) list
+    recursive_preentry * (int * manual_implicits * int option) list
 
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
-  bool -> recursive_preentry * (int * manual_implicits) list -> 
+  bool -> recursive_preentry * (int * manual_implicits * int option) list -> 
   lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint :
-  bool -> recursive_preentry * (int * manual_implicits) list ->
+  bool -> recursive_preentry * (int * manual_implicits * int option) list ->
     decl_notation list -> unit
 
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)