Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 87 insertions, 79 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3688c347..b50c9bbd 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: command.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
 
 open Pp
 open Util
@@ -136,7 +136,7 @@ let red_constant_entry bl ce = function
 let declare_global_definition ident ce local imps =
   let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
   let gr = ConstRef kn in
-    maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
+    maybe_declare_manual_implicits false gr imps;
     if local = Local && Flags.is_verbose() then
       msg_warning (pr_id ident ++ str" is declared as a global definition");
     definition_message ident;
@@ -166,8 +166,9 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
   hook local r
 
 let syntax_definition ident (vars,c) local onlyparse =
-  let pat = interp_aconstr [] vars c in
-  Syntax_def.declare_syntactic_definition local ident onlyparse pat
+  let ((vars,_),pat) = interp_aconstr [] (vars,[]) c in
+  let onlyparse = onlyparse or Metasyntax.is_not_printable pat in
+  Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
@@ -189,7 +190,7 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) =
         let kn =
           declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
 	let gr = ConstRef kn in
-	  maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
+	  maybe_declare_manual_implicits false gr imps;
         assumption_message ident;
         if local=Local & Flags.is_verbose () then
           msg_warning (pr_id ident ++ str" is declared as a parameter" ++
@@ -339,13 +340,26 @@ let (inDec,outDec) =
 let start_hook = ref ignore
 let set_start_hook = (:=) start_hook
 
-let start_proof id kind c ?init_tac hook =
+let start_proof id kind c ?init_tac ?(compute_guard=false) hook =
   let sign = Global.named_context () in
   let sign = clear_proofs sign in
   !start_hook c;
-  Pfedit.start_proof id kind sign c ?init_tac:init_tac hook
-
-let save id const (locality,kind) hook =
+  Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook
+
+let adjust_guardness_conditions const =
+  (* Try all combinations... not optimal *)
+  match kind_of_term const.const_entry_body with
+  | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
+      let possible_indexes =
+	List.map (fun c ->
+	  interval 0 (List.length (fst (Sign.decompose_lam_assum c))))
+	  (Array.to_list fixdefs) in
+      let indexes = search_guard dummy_loc (Global.env()) possible_indexes fixdecls in 
+      { const with const_entry_body = mkFix ((indexes,0),fixdecls) }
+  | c -> const
+
+let save id const do_guard (locality,kind) hook =
+  let const = if do_guard then adjust_guardness_conditions const else const in
   let {const_entry_body = pft;
        const_entry_type = tpo;
        const_entry_opaque = opacity } = const in
@@ -366,9 +380,9 @@ let save_hook = ref ignore
 let set_save_hook f = save_hook := f
 
 let save_named opacity =
-  let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in
+  let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
   let const = { const with const_entry_opaque = opacity } in
-  save id const persistence hook
+  save id const do_guard persistence hook
 
 let make_eq_decidability ind = 
     (* fetching data *)
@@ -442,7 +456,7 @@ let declare_eliminations sp =
 
 (* 3b| Mutual inductive definitions *)
 
-let compute_interning_datas env l nal typl impll =
+let compute_interning_datas env ty l nal typl impll =
   let mk_interning_data na typ impls =
     let idl, impl =
       let impl = 
@@ -452,7 +466,7 @@ let compute_interning_datas env l nal typl impll =
       let sub_impl' = List.filter is_status_implicit sub_impl in
 	(List.map name_of_implicit sub_impl', impl)
     in
-      (na, (idl, impl, compute_arguments_scope typ)) in
+      (na, (ty, idl, impl, compute_arguments_scope typ)) in
   (l, list_map3 mk_interning_data nal typl impll)
 
 let declare_interning_data (_,impls) (df,c,scope) =
@@ -511,7 +525,9 @@ 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 (env_params, ctx_params), userimpls = interp_context_evars evdref env0 paramsl in
+  let (env_params, ctx_params), userimpls = 
+    interp_context_evars ~fail_anonymous:false 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) *)
@@ -526,7 +542,7 @@ let interp_mutual paramsl indl notations finite =
 
   (* Compute interpretation metadatas *)
   let indimpls = List.map (fun _ -> userimpls) fullarities in
-  let impls = compute_interning_datas env0 params indnames fullarities indimpls in
+  let impls = compute_interning_datas env0 Inductive params indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
 
   let constructors =
@@ -539,6 +555,7 @@ let interp_mutual paramsl indl notations finite =
 
   (* Instantiate evars and check all are resolved *)
   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 = evars_of 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
@@ -604,7 +621,7 @@ let prepare_inductive ntnl indl =
   let indl =
     List.map (fun ((_,indname),_,ar,lc) -> { 
       ind_name = indname;
-      ind_arity = ar;
+      ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Rawterm.RType None)) ar;
       ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
     }) indl in
   List.fold_right Option.List.cons ntnl [], indl
@@ -624,12 +641,10 @@ let declare_mutual_with_eliminations isrecord mie impls =
   let (_,kn) = declare_mind isrecord mie in    
     list_iter_i (fun i (indimpls, constrimpls) -> 
       let ind = (kn,i) in
-	maybe_declare_manual_implicits false (IndRef ind)
-	  (is_implicit_args()) indimpls;
+	maybe_declare_manual_implicits false (IndRef ind) indimpls;
 	list_iter_i
 	  (fun j impls -> 
-	    maybe_declare_manual_implicits false (ConstructRef (ind, succ j))
-	      (is_implicit_args()) impls)
+	    maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls)
 	  constrimpls)
       impls;
     if_verbose ppnl (minductive_message names);
@@ -784,7 +799,7 @@ let declare_fix boxed kind f def t imps =
   } in
   let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
   let gr = ConstRef kn in
-    maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
+    maybe_declare_manual_implicits false gr imps;
     gr
       
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
@@ -831,7 +846,7 @@ let interp_recursive fixkind l boxed =
   let env_rec = push_named_types env fixnames fixtypes in
 
   (* Get interpretation metadatas *)
-  let impls = compute_interning_datas env [] fixnames fixtypes fiximps in
+  let impls = compute_interning_datas env Recursive [] fixnames fixtypes fiximps in
   let notations = List.fold_right Option.List.cons ntnl [] in
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
@@ -1044,13 +1059,12 @@ let build_combined_scheme name schemes =
 (* 4.1| Support for mutually proved theorems *)
 
 let retrieve_first_recthm = function
-          | VarRef id -> 
-              (pi2 (Global.lookup_named id),variable_opacity id)
-          | ConstRef cst -> 
-              let {const_body=body;const_opaque=opaq} =
-                Global.lookup_constant cst in
-              (Option.map Declarations.force body,opaq)
-          | _ -> assert false
+  | VarRef id -> 
+      (pi2 (Global.lookup_named id),variable_opacity id)
+  | ConstRef cst -> 
+      let {const_body=body;const_opaque=opaq} =	Global.lookup_constant cst in
+      (Option.map Declarations.force body,opaq)
+  | _ -> assert false
 
 let default_thm_id = id_of_string "Unnamed_thm"
 
@@ -1108,19 +1122,19 @@ let look_for_mutual_statements thms =
     (* common coinductive conclusion *)
     let n = List.length thms in
     let inds = List.map (fun (id,(t,_) as x) -> 
-      let (hyps,ccl) = splay_prod_assum (Global.env()) Evd.empty t in
+      let (hyps,ccl) = Sign.decompose_prod_assum t in
       let whnf_hyp_hds = map_rel_context_with_binders
         (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c)))
         hyps in
       let ind_hyps =
-        List.filter ((<>) None) (list_map_i (fun i (_,b,t) ->
+        List.flatten (list_map_i (fun i (_,b,t) ->
           match kind_of_term t with
           | Ind (kn,_ as ind) when
                 let mind = Global.lookup_mind kn in
-                mind.mind_ntypes = n & mind.mind_finite & b = None ->
-              Some (ind,x,i)
+                mind.mind_finite & b = None ->
+              [ind,x,i]
           | _ ->
-              None) 1 whnf_hyp_hds) in
+              []) 1 (List.rev whnf_hyp_hds)) in
       let ind_ccl =
         let cclenv = push_rel_context hyps (Global.env()) in
         let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in
@@ -1128,53 +1142,45 @@ let look_for_mutual_statements thms =
         | Ind (kn,_ as ind) when
               let mind = Global.lookup_mind kn in
               mind.mind_ntypes = n & not mind.mind_finite ->
-            Some (ind,x,0)
+            [ind,x,0]
         | _ ->
-            None in
+            [] in
       ind_hyps,ind_ccl) thms in
     let inds_hyps,ind_ccls = List.split inds in
-    let is_same_ind kn = function Some ((kn',_),_,_) -> kn = kn' | _ -> false in
-    let compare_kn ((kn,i),_,_) ((kn,i'),_,_) = i - i' in
+    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> kn = kn' in
     (* Check if all conclusions are coinductive in the same type *)
+    (* (degenerated cartesian product since there is at most one coind ccl) *)
     let same_indccl =
-      match ind_ccls with
-      | (Some ((kn,_),_,_ as x))::rest when List.for_all (is_same_ind kn) rest
-            -> Some (x :: List.map Option.get rest)
-      | _ -> None in
+      list_cartesians_filter (fun hyp oks ->
+	if List.for_all (of_same_mutind hyp) oks 
+	then Some (hyp::oks) else None) [] ind_ccls in
+    let ordered_same_indccl =
+      List.filter (list_for_all_i (fun i ((kn,j),_,_) -> i=j) 0) same_indccl in
     (* Check if some hypotheses are inductive in the same type *)
     let common_same_indhyp =
-      let rec find_same_ind inds = 
-        match inds with
-        | []::_ ->
-            []
-        | (Some ((kn,_),_,_) as x :: hyps_thms1)::other_thms ->
-            let others' = List.map (List.filter (is_same_ind kn)) other_thms in
-            (x,others')::find_same_ind (hyps_thms1::other_thms)
-        | (None::hyps_thm1)::other_thms ->
-            find_same_ind (hyps_thm1::other_thms)
-      | [] ->
-          assert false in
-      find_same_ind inds_hyps in
-    let common_inds,finite =
-      match same_indccl, common_same_indhyp with
-      | None, [(x,rest)] when List.for_all (fun l -> List.length l = 1) rest ->
-        (* One occurrence of common inductive hyps and no common coind ccls *)
-          Option.get x::List.map (fun x -> Option.get (List.hd x)) rest,
-          false
-      | Some indccl, [] ->
-        (* One occurrence of common coind ccls and no common inductive hyps *)
+      list_cartesians_filter (fun hyp oks ->
+	if List.for_all (of_same_mutind hyp) oks
+	then Some (hyp::oks) else None) [] inds_hyps in
+    let ordered_inds,finite =
+      match ordered_same_indccl, common_same_indhyp with
+      | indccl::rest, _ ->
+	  assert (rest=[]);
+          (* One occ. of common coind ccls and no common inductive hyps *)
+	  if common_same_indhyp <> [] then 
+	    if_verbose warning "Assuming mutual coinductive statements.";
+	  flush_all ();
           indccl, true
-      | _ -> 
-          error
-            ("Cannot find a common mutual inductive premise or coinductive" ^
-             " conclusion in the statements") in
-    let ordered_inds = List.sort compare_kn common_inds in
-    list_iter_i (fun i' ((kn,i),_,_) -> 
-      if i <> i' then
-        error
-          ("Cannot find distinct (co)inductive types of the same family" ^ 
-              "of mutual (co)inductive types"))
-              ordered_inds;
+      | [], _::_ ->
+	  if same_indccl <> [] &&
+	     list_distinct (List.map pi1 (List.hd same_indccl)) then
+	    if_verbose warn (strbrk "Coinductive statements do not follow the order of definition, assume the proof to be by induction."); flush_all ();
+	  (* assume the largest indices as possible *)
+	  list_last common_same_indhyp, false
+      | _, [] ->
+	  error
+            ("Cannot find common (mutual) inductive premises or coinductive" ^
+             " conclusions in the statements.")
+    in
     let nl,thms = List.split (List.map (fun (_,x,i) -> (i,x)) ordered_inds) in
     let rec_tac =
       if finite then
@@ -1182,6 +1188,7 @@ let look_for_mutual_statements thms =
         | (id,_)::l -> Hiddentac.h_mutual_cofix true id l
         | _ -> assert false
       else
+	(* nl is dummy: it will be recomputed at Qed-time *)
         match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
         | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l
         | _ -> assert false in
@@ -1208,9 +1215,10 @@ let start_proof_com kind thms hook =
             list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
-	  maybe_declare_manual_implicits false ref (is_implicit_args ()) imps;
+	  maybe_declare_manual_implicits false ref imps;
 	  hook strength ref) thms_data in
-      start_proof id kind t ?init_tac:rec_tac hook
+      start_proof id kind t ?init_tac:rec_tac
+	~compute_guard:(rec_tac<>None) hook
 
 let check_anonymity id save_ident =
   if atompart_of_id id <> "Unnamed_thm" then
@@ -1220,17 +1228,17 @@ let check_anonymity id save_ident =
 *)
 
 let save_anonymous opacity save_ident =
-  let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in
+  let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
   let const = { const with const_entry_opaque = opacity } in
   check_anonymity id save_ident;
-  save save_ident const persistence hook
+  save save_ident const do_guard persistence hook
 
 let save_anonymous_with_strength kind opacity save_ident =
-  let id,(const,_,hook) = Pfedit.cook_proof !save_hook in
+  let id,(const,do_guard,_,hook) = Pfedit.cook_proof !save_hook in
   let const = { const with const_entry_opaque = opacity } in
   check_anonymity id save_ident;
   (* we consider that non opaque behaves as local for discharge *)
-  save save_ident const (Global, Proof kind) hook
+  save save_ident const do_guard (Global, Proof kind) hook
 
 let admit () =
   let (id,k,typ,hook) = Pfedit.current_proof_statement () in