summaryrefslogtreecommitdiff
path: root/toplevel/command.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/command.ml')
-rw-r--r--toplevel/command.ml166
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 21:07:11 +0000