Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

1 files changed, 33 insertions, 29 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1f6e7e83..9b18ef27 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: command.ml 13344 2010-07-28 15:04:36Z msozeau $ *)
 
 open Pp
 open Util
@@ -69,8 +69,7 @@ let red_constant_entry n ce = function
 let interp_definition boxed bl red_option c ctypopt =
   let env = Global.env() in
   let evdref = ref Evd.empty in
-  let (env_bl, ctx), imps1 =
-    interp_context_evars ~fail_anonymous:false evdref env bl in
+  let (env_bl, ctx), imps1 = interp_context_evars evdref env bl in
   let imps,ce =
     match ctypopt with
       None ->
@@ -227,7 +226,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
   let env0 = Global.env() in
   let evdref = ref Evd.empty in
   let (env_params, ctx_params), userimpls =
-    interp_context_evars ~fail_anonymous:false evdref env0 paramsl
+    interp_context_evars evdref env0 paramsl
   in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
@@ -244,7 +243,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
   (* Compute interpretation metadatas *)
   let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in
   let arities = List.map fst arities in
-  let impls = compute_full_internalization_env env0 Inductive params indnames fullarities indimpls in
+  let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
 
   let constructors =
@@ -256,9 +255,9 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
      () in
 
   (* Instantiate evars and check all are resolved *)
-  let evd,_ = consider_remaining_unif_problems env_params !evdref in
+  let evd = consider_remaining_unif_problems env_params !evdref in
   let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in
-  let sigma =  evd in
+  let sigma = evd in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
   let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
   let arities = List.map (nf_evar sigma) arities in
@@ -448,14 +447,19 @@ 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
+  let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
+    ((env'', ctx' @ ctx), imps @ imps', annot)
+      
 let interp_fix_ccl evdref (env,_) fix =
   interp_type_evars evdref env fix.fix_type
 
@@ -487,8 +491,8 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
 
 (* Jump over let-bindings. *)
 
-let compute_possible_guardness_evidences na fix (ids,_) =
-  match index_of_annot fix.fix_binders na with
+let compute_possible_guardness_evidences (ids,_,na) =
+  match na with
   | Some i -> [i]
   | None ->
       (* If recursive argument was not given by user, we try all args.
@@ -507,15 +511,15 @@ 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
   let env_rec = push_named_types env fixnames fixtypes in
 
   (* Get interpretation metadatas *)
-  let impls = compute_full_internalization_env env Recursive [] fixnames fixtypes fiximps in
+  let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let fixdefs =
@@ -525,7 +529,7 @@ let interp_recursive isfix fixl notations =
       () in
 
   (* Instantiate evars and check all are resolved *)
-  let evd,_ = consider_remaining_unif_problems env_rec !evdref in
+  let evd = consider_remaining_unif_problems env_rec !evdref in
   let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in
   let fixtypes = List.map (nf_evar evd) fixtypes in
   let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in
@@ -538,7 +542,7 @@ let interp_recursive isfix fixl notations =
   end;
 
   (* Build the fix declaration block *)
-  (fixnames,fixdefs,fixtypes),List.combine fixctxnames fiximps
+  (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots
 
 let interp_fixpoint = interp_recursive true
 let interp_cofixpoint = interp_recursive false
@@ -547,7 +551,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
@@ -558,7 +562,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);
@@ -572,7 +576,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
@@ -583,7 +587,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
@@ -592,28 +596,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 =