aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/subtac/subtac.ml6
-rw-r--r--contrib/subtac/subtac_command.ml265
-rw-r--r--contrib/subtac/subtac_command.mli11
-rw-r--r--contrib/subtac/subtac_obligations.ml100
-rw-r--r--contrib/subtac/subtac_obligations.mli11
-rw-r--r--contrib/subtac/test/Mutind.v3
-rw-r--r--contrib/subtac/test/euclid.v11
-rw-r--r--contrib/subtac/test/measure.v10
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1784.v101
-rw-r--r--toplevel/command.mli25
10 files changed, 350 insertions, 193 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 56ebc4f522..f3696f6ec9 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -151,9 +151,9 @@ let subtac (loc, command) =
| VernacInstance (sup, is, props) ->
Subtac_classes.new_instance sup is props
-(* | VernacCoFixpoint (l, b) -> *)
-(* let _ = trace (str "Building cofixpoint") in *)
-(* ignore(Subtac_command.build_recursive l b) *)
+ | VernacCoFixpoint (l, b) ->
+ let _ = trace (str "Building cofixpoint") in
+ ignore(Subtac_command.build_corecursive l b)
(*| VernacEndProof e ->
subtac_end_proof e*)
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 9afa6f0675..b06880bd3e 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -39,6 +39,8 @@ open Tacticals
open Tacinterp
open Vernacexpr
open Notation
+open Evd
+open Evarutil
module SPretyping = Subtac_pretyping.Pretyping
open Subtac_utils
@@ -63,12 +65,15 @@ let interp_gen kind isevars env
let interp_constr isevars env c =
interp_gen (OfType None) isevars env c
-let interp_type isevars env ?(impls=([],[])) c =
+let interp_type_evars isevars env ?(impls=([],[])) c =
interp_gen IsType isevars env ~impls c
let interp_casted_constr isevars env ?(impls=([],[])) c typ =
interp_gen (OfType (Some typ)) isevars env ~impls c
+let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
+ interp_gen (OfType (Some typ)) isevars env ~impls c
+
let interp_open_constr isevars env c =
msgnl (str "Pretyping " ++ my_print_constr_expr c);
let c = Constrintern.intern_constr (Evd.evars_of !isevars) env c in
@@ -92,10 +97,9 @@ let locate_if_isevar loc na = function
let interp_binder sigma env na t =
let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in
- SPretyping.understand_type (Evd.evars_of !sigma) env (locate_if_isevar (loc_of_rawconstr t) na t)
+ SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t)
-
-let interp_context sigma env params =
+let interp_context_evars sigma env params =
List.fold_left
(fun (env,params) d -> match d with
| LocalRawAssum ([_,na],k,(CHole _ as t)) ->
@@ -103,7 +107,7 @@ let interp_context sigma env params =
let d = (na,None,t) in
(push_rel d env, d::params)
| LocalRawAssum (nal,k,t) ->
- let t = interp_type sigma env t in
+ let t = interp_type_evars sigma env t in
let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
let ctx = List.rev ctx in
(push_rel_context ctx env, ctx@params)
@@ -186,7 +190,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
(* Ppconstr.pr_constr_expr body) *)
(* with _ -> () *)
(* in *)
- let env', binders_rel = interp_context isevars env bl in
+ let env', binders_rel = interp_context_evars isevars env bl in
let after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in
let before_length, after_length = List.length before, List.length after in
let argid = match argname with Name n -> n | _ -> assert(false) in
@@ -225,7 +229,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
in
let top_bl = after @ (arg :: before) in
let top_env = push_rel_context top_bl env in
- let top_arity = interp_type isevars top_env arityc in
+ let top_arity = interp_type_evars isevars top_env arityc in
let intern_bl = wfarg 1 :: arg :: before in
let intern_env = push_rel_context intern_bl env in
let proj = (Lazy.force sig_).Coqlib.proj1 in
@@ -264,7 +268,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in
(* (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ()); *)
let fun_env = push_rel_context fun_bl intern_before_env in
- let fun_arity = interp_type isevars fun_env arityc in
+ let fun_arity = interp_type_evars isevars fun_env arityc in
let intern_body = interp_casted_constr isevars fun_env body fun_arity in
let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
let _ =
@@ -305,145 +309,148 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let typ = it_mkProd_or_LetIn top_arity binders_rel in
let fullcoqc = Evarutil.nf_isevar !isevars def in
let fullctyp = Evarutil.nf_isevar !isevars typ in
-(* let _ = try trace (str "After evar normalization: " ++ spc () ++ *)
-(* str "Coq term: " ++ my_print_constr env fullcoqc ++ spc () *)
-(* ++ str "Coq type: " ++ my_print_constr env fullctyp) *)
-(* with _ -> () *)
-(* in *)
let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in
let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in
let evm = non_instanciated_map env isevars evm in
-
- (* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *)
let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
- (* (try trace (str "Generated obligations : "); *)
-(* Array.iter *)
- (* (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *)
- (* evars; *)
- (* with _ -> ()); *)
Subtac_obligations.add_definition recname evars_def evars_typ evars
let nf_evar_context isevars ctx =
List.map (fun (n, b, t) ->
(n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
-let build_mutrec lnameargsardef boxed =
- let sigma = Evd.empty and env = Global.env () in
- let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef
- and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
+let interp_fix_context evdref env fix =
+ interp_context_evars evdref env fix.Command.fix_binders
+
+let interp_fix_ccl evdref (env,_) fix =
+ interp_type_evars evdref env fix.Command.fix_type
+
+let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
+ let env = push_rel_context ctx env_rec in
+ let body = interp_casted_constr_evars evdref env ~impls fix.Command.fix_body ccl in
+ it_mkLambda_or_LetIn body ctx
+
+let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
+
+let prepare_recursive_declaration fixnames fixtypes fixdefs =
+ let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
+ 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,_) fixtype =
+ match n with
+ | Some n -> [n]
+ | 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 ?) *)
+ let m = Term.nb_prod fixtype in
+ let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
+ list_map_i (fun i _ -> i) 0 ctx
+
+let push_named_context = List.fold_right push_named
+
+let interp_recursive fixkind l boxed =
+ let env = Global.env() in
+ let fixl, ntnl = List.split l in
+ let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in
+
+ (* 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.Command.fix_binders)
+ fixl
in
- let isevars = ref (Evd.create_evar_defs sigma) in
- (* Build the recursive context and notations for the recursive types *)
- let (rec_sign,rec_env,rec_impls,arityl) =
- List.fold_left
- (fun (sign,env,impls,arl) ((recname, n, bl,arityc,body),_) ->
- let arityc = Command.generalize_constr_expr arityc bl in
- let arity = interp_type isevars env arityc in
- let impl =
- if Impargs.is_implicit_args()
- then Impargs.compute_implicits env arity
- else [] in
- let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
- ((recname,None,arity) :: sign, Environ.push_named (recname,None,arity) env, impls', (None, arity)::arl))
- ([],env,[],[]) lnameargsardef in
- let arityl = List.rev arityl in
- let notations =
- List.fold_right (fun (_,ntnopt) l -> Option.List.cons ntnopt l)
- lnameargsardef [] in
-
- let recdef =
- (* Declare local notations *)
- let fs = States.freeze() in
- let def =
- try
- List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
- Metasyntax.add_notation_interpretation df rec_impls c None) notations;
- List.map2
- (fun ((_,_,bl,_,def),_) (info, arity) ->
- match info with
- None ->
- let def = abstract_constr_expr def bl in
- info, interp_casted_constr isevars rec_env ~impls:([],rec_impls)
- def arity
- | Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) ->
- let rec_env = push_rel_context fun_bl rec_env in
- let cstr = interp_casted_constr isevars rec_env ~impls:([],rec_impls)
- def intern_arity
- in info, it_mkLambda_or_LetIn cstr fun_bl)
- lnameargsardef arityl
- with e ->
- States.unfreeze fs; raise e in
- States.unfreeze fs; def
+ let fixctxs = 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 rec_sign =
+ List.fold_left2 (fun env id t -> (id,None,t) :: env)
+ [] fixnames fixtypes
in
- let (lnonrec,(namerec,defrec,arrec,nvrec)) =
- collect_non_rec env lrecnames recdef arityl nv in
- if lnonrec <> [] then
- errorlabstrm "Subtac_command.build_mutrec"
- (str "Non-recursive definitions not allowed in mutual fixpoint blocks");
- let recdefs = Array.length defrec in
- trace (str "built recursive definitions");
- (* Normalize all types and defs with respect to *all* evars *)
- Array.iteri
- (fun i (info, def) ->
- let def = evar_nf isevars def in
- let y, typ = arrec.(i) in
- let typ = evar_nf isevars typ in
- arrec.(i) <- (y, typ);
- defrec.(i) <- (info, def))
- defrec;
- trace (str "normalized w.r.t. evars");
- (* Normalize rec_sign which was built earlier *)
- let rec_sign = nf_evar_context !isevars rec_sign in
- trace (str "normalized context");
+ let env_rec = push_named_context rec_sign env in
+
+ (* Get interpretation metadatas *)
+ let impls = Command.compute_interning_datas env [] fixnames fixtypes in
+ let notations = List.fold_right Option.List.cons ntnl [] in
+
+ (* Interp bodies with rollback because temp use of notations/implicit *)
+ let fixdefs =
+ States.with_heavy_rollback (fun () ->
+ List.iter (Command.declare_interning_data impls) notations;
+ list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
+ () in
+
+ (* Instantiate evars and check all are resolved *)
+ let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in
+ let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in
+ let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in
+ let rec_sign = nf_named_context_evar (evars_of evd) rec_sign in
+ let recdefs = List.length rec_sign in
+(* List.iter (check_evars env_rec Evd.empty evd) fixdefs; *)
+(* List.iter (check_evars env Evd.empty evd) fixtypes; *)
+(* check_mutuality env kind (List.combine fixnames fixdefs); *)
+
+ (* Russell-specific code *)
+
(* Get the interesting evars, those that were not instanciated *)
- let isevars = Evd.undefined_evars !isevars in
- trace (str "got undefined evars" ++ Evd.pr_evar_defs isevars);
+ let isevars = Evd.undefined_evars evd in
+ trace (str "got undefined evars" ++ Evd.pr_evar_defs isevars);
let evm = Evd.evars_of isevars in
trace (str "got the evm, recdefs is " ++ int recdefs);
(* Solve remaining evars *)
- let rec collect_evars i acc =
- if i < recdefs then
- let (info, def) = defrec.(i) in
- let y, typ = arrec.(i) in
- trace (str "got the def" ++ int i);
- let _ = try trace (str "In collect evars, isevars is: " ++ Evd.pr_evar_defs isevars) with _ -> () in
- let id = namerec.(i) in
- (* Generalize by the recursive prototypes *)
- let def =
- Termops.it_mkNamedLambda_or_LetIn def rec_sign
- and typ =
- Termops.it_mkNamedProd_or_LetIn typ rec_sign
- in
- let evm' = Subtac_utils.evars_of_term evm Evd.empty def in
- let evm' = Subtac_utils.evars_of_term evm evm' typ in
- let evars, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
- collect_evars (succ i) ((id, def, typ, evars) :: acc)
- else acc
+ let rec collect_evars id def typ imps =
+ let _ = try trace (str "In collect evars, isevars is: " ++ Evd.pr_evar_defs isevars) with _ -> () in
+ (* Generalize by the recursive prototypes *)
+ let def =
+ Termops.it_mkNamedLambda_or_LetIn def rec_sign
+ and typ =
+ Termops.it_mkNamedProd_or_LetIn typ rec_sign
+ in
+ let evm' = Subtac_utils.evars_of_term evm Evd.empty def in
+ let evm' = Subtac_utils.evars_of_term evm evm' typ in
+ let evars, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
+ (id, def, typ, imps, evars)
in
- let defs = collect_evars 0 [] in
- Subtac_obligations.add_mutual_definitions (List.rev defs) nvrec
-
-
+ let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
+ (match fixkind with
+ | Command.IsFixpoint wfl ->
+ let possible_indexes =
+ List.map2 compute_possible_guardness_evidences wfl fixtypes in
+ let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
+ Array.of_list fixtypes, Array.of_list (List.map (subst_vars fixnames) fixdefs)
+ in
+ let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
+ list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l
+ | Command.IsCoFixpoint -> ());
+ Subtac_obligations.add_mutual_definitions defs notations fixkind
+
let out_n = function
Some n -> n
| None -> 0
-let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
- match lnameargsardef with
- | ((id, (n, CWfRec r), bl, typ, body), no) :: [] ->
- ignore(build_wellfounded (id, out_n n, bl, typ, body) r false no boxed)
- | ((id, (n, CMeasureRec r), bl, typ, body), no) :: [] ->
- ignore(build_wellfounded (id, out_n n, bl, typ, body) r true no boxed)
- | l ->
- let lnameargsardef =
- List.map (fun ((id, (n, ro), bl, typ, body), no) ->
- match ro with
- CStructRec -> (id, out_n n, bl, typ, body), no
- | CWfRec _ | CMeasureRec _ ->
- errorlabstrm "Subtac_command.build_recursive"
- (str "Well-founded fixpoints not allowed in mutually recursive blocks"))
- lnameargsardef
- in build_mutrec lnameargsardef boxed
-
-
-
+let build_recursive l b =
+ let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
+ match g, l with
+ [(n, CWfRec r)], [((id,_,bl,typ,def),ntn)] ->
+ ignore(build_wellfounded (id, out_n n, bl, typ, def) r false ntn false)
+
+ | [(n, CMeasureRec r)], [((id,_,bl,typ,def),ntn)] ->
+ ignore(build_wellfounded (id, out_n n, bl, typ, def) r true 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; Command.fix_body = def; Command.fix_type = typ},ntn)) l
+ in interp_recursive (Command.IsFixpoint g) fixl b
+ | _, _ ->
+ errorlabstrm "Subtac_command.build_recursive"
+ (str "Well-founded fixpoints not allowed in mutually recursive blocks")
+
+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_body = def; Command.fix_type = typ},ntn))
+ l in
+ interp_recursive Command.IsCoFixpoint fixl b
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index 6de45d17fe..27520867fe 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -20,12 +20,12 @@ val interp_gen :
val interp_constr :
evar_defs ref ->
env -> constr_expr -> constr
-val interp_type :
+val interp_type_evars :
evar_defs ref ->
env ->
?impls:full_implicits_env ->
constr_expr -> constr
-val interp_casted_constr :
+val interp_casted_constr_evars :
evar_defs ref ->
env ->
?impls:full_implicits_env ->
@@ -38,5 +38,12 @@ val interp_constr_judgment :
constr_expr -> unsafe_judgment
val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
+val interp_binder : Evd.evar_defs ref ->
+ Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr
+
+
val build_recursive :
(fixpoint_expr * decl_notation) list -> bool -> unit
+
+val build_corecursive :
+ (cofixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 05bebf0f56..b7777e6222 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -1,6 +1,7 @@
open Printf
open Pp
open Subtac_utils
+open Command
open Term
open Names
@@ -35,14 +36,17 @@ type obligation =
type obligations = (obligation array * int)
+type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
+
type program_info = {
prg_name: identifier;
prg_body: constr;
prg_type: constr;
prg_obligations: obligations;
prg_deps : identifier list;
- prg_nvrec : int array;
+ prg_fixkind : Command.fixpoint_kind option ;
prg_implicits : (Topconstr.explicitation * (bool * bool)) list;
+ prg_notations : notations ;
prg_kind : definition_object_kind;
prg_hook : definition_hook;
}
@@ -159,39 +163,50 @@ let declare_definition prg =
open Pp
open Ppconstr
+let compute_possible_guardness_evidences (n,_) fixtype =
+ match n with
+ | Some n -> [n]
+ | 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 ?) *)
+ let m = Term.nb_prod fixtype in
+ let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
+ list_map_i (fun i _ -> i) 0 ctx
+
let declare_mutual_definition l =
let len = List.length l in
- let namerec = Array.of_list (List.map (fun x -> x.prg_name) l) in
-(* let arrec = *)
-(* Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l) *)
-(* in *)
- let recvec, arrec =
- let l, l' =
- List.split
- (List.map (fun x ->
- let subs, typ = (subst_body x) in
- snd (decompose_lam_n len subs),
- snd (decompose_prod_n len typ)) l)
- in
- Array.of_list l, Array.of_list l'
- in
- let nvrec = (List.hd l).prg_nvrec in
- let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
- let rec declare i fi =
- (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++
- my_print_constr (Global.env()) (recvec.(i)));
- with _ -> ());
- let ce =
- { const_entry_body = mkFix ((nvrec,i),recdecls);
- const_entry_type = Some arrec.(i);
- const_entry_opaque = false;
- const_entry_boxed = true} in
- Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
+ let fixdefs, fixtypes, fiximps =
+ list_split3
+ (List.map (fun x ->
+ let subs, typ = (subst_body x) in
+ snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
in
- let lrefrec = Array.mapi declare namerec in
- print_message (recursive_message lrefrec);
- lrefrec.(0)
-
+ let fixkind = Option.get (List.hd l).prg_fixkind in
+ let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
+ let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
+ let boxed = true (* TODO *) in
+ let fixnames = (List.hd l).prg_deps in
+ let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
+ let indexes, fixdecls =
+ match fixkind with
+ | IsFixpoint wfl ->
+ let possible_indexes =
+ List.map2 compute_possible_guardness_evidences wfl fixtypes in
+ let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
+ Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
+ | IsCoFixpoint ->
+ None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
+ in
+ (* Declare the recursive definitions *)
+ let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
+ (* Declare notations *)
+ List.iter (Command.declare_interning_data ([],[])) (List.hd l).prg_notations;
+ Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames);
+ (match List.hd kns with ConstRef kn -> kn | _ -> assert false)
+
let declare_obligation obl body =
let ce =
{ const_entry_body = body;
@@ -220,7 +235,7 @@ let try_tactics obls =
let red = Reductionops.nf_betaiota
-let init_prog_info n b t deps nvrec obls impls kind hook =
+let init_prog_info n b t deps fixkind notations obls impls kind hook =
let obls' =
Array.mapi
(fun i (n, t, o, d) ->
@@ -231,7 +246,8 @@ let init_prog_info n b t deps nvrec obls impls kind hook =
obls
in
{ prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
- prg_deps = deps; prg_nvrec = nvrec; prg_implicits = impls; prg_kind = kind; prg_hook = hook; }
+ prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
+ prg_implicits = impls; prg_kind = kind; prg_hook = hook; }
let get_prog name =
let prg_infos = !from_prg in
@@ -422,9 +438,15 @@ let show_obligations ?(msg=true) n =
| Some _ -> ())
obls
+let show_term n =
+ let prg = get_prog_err n in
+ let n = prg.prg_name in
+ msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
+ ++ my_print_constr (Global.env ()) prg.prg_body)
+
let add_definition n b t ?(implicits=[]) ?(kind=Definition) ?(hook=fun x -> ()) obls =
Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
- let prg = init_prog_info n b t [] (Array.make 0 0) obls implicits kind hook in
+ let prg = init_prog_info n b t [] None [] obls implicits kind hook in
let obls,_ = prg.prg_obligations in
if Array.length obls = 0 then (
Flags.if_verbose ppnl (str ".");
@@ -440,12 +462,12 @@ let add_definition n b t ?(implicits=[]) ?(kind=Definition) ?(hook=fun x -> ())
| Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
| _ -> res)
-let add_mutual_definitions l ?(implicits=[]) ?(kind=Definition) nvrec =
- let deps = List.map (fun (n, b, t, obls) -> n) l in
+let add_mutual_definitions l ?(kind=Definition) notations fixkind =
+ let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
let upd = List.fold_left
- (fun acc (n, b, t, obls) ->
- let prg = init_prog_info n b t deps nvrec obls implicits kind (fun x -> ()) in
- ProgMap.add n prg acc)
+ (fun acc (n, b, t, imps, obls) ->
+ let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind (fun x -> ()) in
+ ProgMap.add n prg acc)
!from_prg l
in
from_prg := upd;
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 30fbd02843..b026e59b23 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -19,11 +19,14 @@ val add_definition : Names.identifier -> Term.constr -> Term.types ->
?kind:Decl_kinds.definition_object_kind ->
?hook:definition_hook -> obligation_info -> progress
+type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
+
val add_mutual_definitions :
- (Names.identifier * Term.constr * Term.types * obligation_info) list ->
- ?implicits:(Topconstr.explicitation * (bool * bool)) list ->
+ (Names.identifier * Term.constr * Term.types *
+ (Topconstr.explicitation * (bool * bool)) list * obligation_info) list ->
?kind:Decl_kinds.definition_object_kind ->
- int array -> unit
+ notations ->
+ Command.fixpoint_kind -> unit
val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit
@@ -40,6 +43,8 @@ val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
val show_obligations : ?msg:bool -> Names.identifier option -> unit
+val show_term : Names.identifier option -> unit
+
val admit_obligations : Names.identifier option -> unit
exception NoObligations of Names.identifier option
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index c2ee4595d0..ac49ca96a4 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,10 +1,11 @@
Require Import List.
+
Program Fixpoint f a : { x : nat | x > 0 } :=
match a with
| 0 => 1
| S a' => g a a'
end
-with g a b { struct b } : { x : nat | x > 0 } :=
+with g a b : { x : nat | x > 0 } :=
match b with
| 0 => 1
| S b' => f b'
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index a5a8b85f99..501aa79815 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -1,20 +1,17 @@
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
Require Import Coq.Arith.Compare_dec.
Notation "( x & y )" := (existS _ x y) : core_scope.
+Require Import Omega.
+
Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a} :
{ q : nat & { r : nat | a = b * q + r /\ r < b } } :=
if le_lt_dec b a then let (q', r) := euclid (a - b) b in
(S q' & r)
else (O & a).
-Require Import Omega.
-
-Obligations.
-Solve Obligations using subtac_simpl ; omega.
-
Next Obligation.
- assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega.
+ assert(b * S q' = b * q' + b) by auto with arith ; omega.
Defined.
Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q).
diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v
index 4764037d94..4f938f4f87 100644
--- a/contrib/subtac/test/measure.v
+++ b/contrib/subtac/test/measure.v
@@ -2,7 +2,7 @@ Notation "( x & y )" := (@existS _ _ x y) : core_scope.
Unset Printing All.
Require Import Coq.Arith.Compare_dec.
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
Fixpoint size (a : nat) : nat :=
match a with
@@ -10,15 +10,11 @@ Fixpoint size (a : nat) : nat :=
| S n => S (size n)
end.
-Program Fixpoint test_measure (a : nat) {measure a size} : nat :=
+Program Fixpoint test_measure (a : nat) {measure size a} : nat :=
match a with
| S (S n) => S (test_measure n)
- | x => x
+ | 0 | S 0 => a
end.
-subst.
-unfold n0.
-auto with arith.
-Qed.
Check test_measure.
Print test_measure. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
new file mode 100644
index 0000000000..6778831d85
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -0,0 +1,101 @@
+Require Import List.
+Require Import ZArith.
+Require String. Open Scope string_scope.
+Ltac Case s := let c := fresh "case" in set (c := s).
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Inductive sv : Set :=
+| I : Z -> sv
+| S : list sv -> sv.
+
+Section sv_induction.
+
+Variables
+ (VP: sv -> Prop)
+ (LP: list sv -> Prop)
+
+ (VPint: forall n, VP (I n))
+ (VPset: forall vs, LP vs -> VP (S vs))
+ (lpcons: forall v vs, VP v -> LP vs -> LP (v::vs))
+ (lpnil: LP nil).
+
+Fixpoint setl_value_indp (x:sv) {struct x}: VP x :=
+ match x as x return VP x with
+ | I n => VPint n
+ | S vs =>
+ VPset
+ ((fix values_indp (vs:list sv) {struct vs}: (LP vs) :=
+ match vs as vs return LP vs with
+ | nil => lpnil
+ | v::vs => lpcons (setl_value_indp v) (values_indp vs)
+ end) vs)
+ end.
+End sv_induction.
+
+Inductive slt : sv -> sv -> Prop :=
+| IC : forall z, slt (I z) (I z)
+| IS : forall vs vs', slist_in vs vs' -> slt (S vs) (S vs')
+
+with sin : sv -> list sv -> Prop :=
+| Ihd : forall s s' sv', slt s s' -> sin s (s'::sv')
+| Itl : forall s s' sv', sin s sv' -> sin s (s'::sv')
+
+with slist_in : list sv -> list sv -> Prop :=
+| Inil : forall sv',
+ slist_in nil sv'
+| Icons : forall s sv sv',
+ sin s sv' ->
+ slist_in sv sv' ->
+ slist_in (s::sv) sv'.
+
+Hint Constructors sin slt slist_in.
+
+Require Import Program.
+
+Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
+ match x with
+ | I x =>
+ match y with
+ | I y => if (Z_eq_dec x y) then left else right
+ | S ys => right
+ end
+ | S xs =>
+ match y with
+ | I y => right
+ | S ys =>
+ let fix list_in (xs ys:list sv) {struct xs} :
+ {slist_in xs ys} + {~slist_in xs ys} :=
+ match xs with
+ | nil => left
+ | x::xs =>
+ let fix elem_in (ys:list sv) : {sin x ys}+{~sin x ys} :=
+ match ys with
+ | nil => right
+ | y::ys => if lt_dec x y then left else if elem_in
+ ys then left else right
+ end
+ in
+ if elem_in ys then
+ if list_in xs ys then left else right
+ else right
+ end
+ in if list_in xs ys then left else right
+ end
+ end.
+
+Next Obligation. intro; apply H; inversion H0; subst; trivial. Defined.
+Next Obligation. intro; inversion H. Defined.
+Next Obligation. intro H; inversion H. Defined.
+Next Obligation. intro; inversion H; subst. Defined.
+Next Obligation.
+ contradict H. inversion H; subst. assumption.
+ contradict H0; assumption. Defined.
+Next Obligation.
+ contradict H0. inversion H0; subst. assumption. Defined.
+Next Obligation.
+ contradict H. inversion H; subst. assumption. Defined.
+Next Obligation.
+ contradict H. inversion H; subst; auto. Defined.
+
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 6b15479d77..d587fabf77 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -43,6 +43,10 @@ val declare_assumption : identifier located list ->
coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> bool
->unit
+val declare_interning_data : 'a * Constrintern.implicits_env ->
+ string * Topconstr.constr_expr * Topconstr.scope_name option -> unit
+
+
val compute_interning_datas : Environ.env ->
'a list ->
'b list ->
@@ -58,9 +62,26 @@ val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
val declare_mutual_with_eliminations :
bool -> Entries.mutual_inductive_entry -> mutual_inductive
-val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit
+type fixpoint_kind =
+ | IsFixpoint of (int option * recursion_order_expr) list
+ | IsCoFixpoint
+
+type fixpoint_expr = {
+ fix_name : identifier;
+ fix_binders : local_binder list;
+ fix_body : constr_expr;
+ fix_type : constr_expr
+}
+
+val recursive_message : Decl_kinds.definition_object_kind ->
+ int array option -> Names.identifier list -> Pp.std_ppcmds
+
+val declare_fix : bool -> Decl_kinds.definition_object_kind -> identifier ->
+ constr -> types -> Impargs.manual_explicitation list -> global_reference
+
+val build_recursive : (Topconstr.fixpoint_expr * decl_notation) list -> bool -> unit
-val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit
+val build_corecursive : (Topconstr.cofixpoint_expr * decl_notation) list -> bool -> unit
val build_scheme : (identifier located option * scheme ) list -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 13:22:47 +0000