From 7a39bd5650cc49c5c77788fb42fe2caaf35dfdac Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 6 May 2008 14:05:20 +0000
Subject: Postpone the search for the recursive argument index from the user
 given name after internalisation, to get the correct behavior with typeclass
 binders. This simplifies the pretty printing and translation of the recursive
 argument name in various places too. Use this opportunity to factorize the
 different internalization and interpretation functions of binders as well.
 This definitely fixes part 2 of bug #1846 and makes it possible to use
 fixpoint definitions with typeclass arguments in program too, with an example
 given in EquivDec. At the same time, one fix and one enhancement in Program:
 - fix a de Bruijn bug in subtac_cases - introduce locations of obligations
 and use them in case the obligation tactic raises a failure when tried on a
 particular obligation, as suggested by Sean Wilson.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10889 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml  | 25 +++++++++++--------------
 toplevel/command.mli |  2 +-
 toplevel/record.ml   |  2 +-
 3 files changed, 13 insertions(+), 16 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 860a542f41..7d2a437766 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -510,8 +510,7 @@ let interp_mutual paramsl indl notations finite =
   check_all_names_different indl;
   let env0 = Global.env() in
   let evdref = ref (Evd.create_evar_defs Evd.empty) in
-  let userimpls = Implicit_quantifiers.implicits_of_binders paramsl in
-  let env_params, ctx_params = interp_context_evars evdref env0 paramsl in
+  let (env_params, ctx_params), userimpls = interp_context_evars evdref env0 paramsl in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
   (* Names of parameters as arguments of the inductive type (defs removed) *)
@@ -752,7 +751,7 @@ let check_mutuality env kind fixl =
     | _ -> ()
 
 type fixpoint_kind =
-  | IsFixpoint of (int option * recursion_order_expr) list
+  | IsFixpoint of (identifier located option * recursion_order_expr) list
   | IsCoFixpoint
 
 type fixpoint_expr = {
@@ -792,17 +791,19 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let names = List.map (fun id -> Name id) fixnames in
   (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
 
-let compute_possible_guardness_evidences (n,_) fixl fixtype =
+let rel_index n ctx = 
+  list_index0 (Name n) (List.rev_map (fun (na, _, _) -> na) ctx)
+
+let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
   match n with 
-  | Some n -> [n] 
+  | Some (loc, n) -> [rel_index n fixctx]
   | None -> 
       (* If recursive argument was not given by user, we try all args.
 	 An earlier approach was to look only for inductive arguments,
 	 but doing it properly involves delta-reduction, and it finally 
          doesn't seem to worth the effort (except for huge mutual 
 	 fixpoints ?) *)
-      (* FIXME, local_binders_length does not give the size of the final product if typeclasses are used *)
-      let m = local_binders_length fixl.fix_binders in
+      let m = List.length fixctx in
       let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
       list_map_i (fun i _ -> i) 0 ctx
 
@@ -814,12 +815,8 @@ let interp_recursive fixkind l boxed =
 
   (* Interp arities allowing for unresolved types *)
   let evdref = ref (Evd.create_evar_defs Evd.empty) in
-  let fiximps = 
-    List.map 
-      (fun x -> Implicit_quantifiers.implicits_of_binders x.fix_binders) 
-      fixl 
-  in
-  let fixctxs = List.map (interp_fix_context evdref env) fixl in
+  let fixctxs, fiximps =
+    List.split (List.map (interp_fix_context evdref env) fixl) in
   let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let env_rec = push_named_types env fixnames fixtypes in
@@ -849,7 +846,7 @@ let interp_recursive fixkind l boxed =
     match fixkind with
     | IsFixpoint wfl ->
 	let possible_indexes = 
-	  list_map3 compute_possible_guardness_evidences wfl fixl fixtypes in
+	  list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
 	let indexes = search_guard dummy_loc env possible_indexes fixdecls in 
 	Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
     | IsCoFixpoint ->
diff --git a/toplevel/command.mli b/toplevel/command.mli
index b37c6c359c..8448817f67 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -76,7 +76,7 @@ val declare_mutual_with_eliminations :
   mutual_inductive
 
 type fixpoint_kind =
-  | IsFixpoint of (int option * recursion_order_expr) list
+  | IsFixpoint of (identifier located option * recursion_order_expr) list
   | IsCoFixpoint
 
 type fixpoint_expr = {
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 57a7e63b34..f6815d5379 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -43,7 +43,7 @@ let interp_decl sigma env = function
 
 let typecheck_params_and_fields id t ps fs =
   let env0 = Global.env () in
-  let env1,newps = interp_context Evd.empty env0 ps in
+  let (env1,newps), _ = interp_context Evd.empty env0 ps in
   let fullarity = it_mkProd_or_LetIn t newps in
   let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
   let env2,newfs =
-- 
cgit v1.2.3