aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/subtac/FunctionalExtensionality.v3
-rw-r--r--contrib/subtac/Utils.v2
-rw-r--r--contrib/subtac/eterm.ml31
-rw-r--r--contrib/subtac/g_subtac.ml44
-rw-r--r--contrib/subtac/subtac.ml6
-rw-r--r--contrib/subtac/subtac_cases.ml211
-rw-r--r--contrib/subtac/subtac_coercion.ml143
-rw-r--r--contrib/subtac/subtac_command.ml118
-rw-r--r--contrib/subtac/subtac_obligations.ml136
-rw-r--r--contrib/subtac/subtac_obligations.mli2
-rw-r--r--contrib/subtac/subtac_pretyping.ml29
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml8
-rw-r--r--contrib/subtac/subtac_utils.ml6
-rw-r--r--contrib/subtac/subtac_utils.mli1
-rw-r--r--contrib/subtac/test/euclid.v14
15 files changed, 375 insertions, 339 deletions
diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v
index 24c2f0142..1a12ac824 100644
--- a/contrib/subtac/FunctionalExtensionality.v
+++ b/contrib/subtac/FunctionalExtensionality.v
@@ -15,8 +15,7 @@ Lemma fix_sub_eq_ext :
(F_sub : forall x : A, (forall {y : A | R y x}, P (`y)) -> P x),
forall x : A,
Fix_sub A R Rwf P F_sub x =
- let f_sub := F_sub in
- F_sub x (fun {y : A | R y x}=> Fix A R Rwf P f_sub (`y)).
+ F_sub x (fun {y : A | R y x}=> Fix A R Rwf P F_sub (`y)).
Proof.
intros ; apply Fix_eq ; auto.
intros.
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 6b613b0de..412d5ae3b 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -44,7 +44,7 @@ end.
Ltac destruct_exists := repeat (destruct_one_pair) .
-Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in *.
+Ltac subtac_simpl := hnf ; intros ; destruct_exists ; try subst.
(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *)
Ltac destruct_call f :=
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 8ec173630..1844fea55 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -52,8 +52,8 @@ let subst_evar_constr evs n t =
anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
in
seen := Intset.add id !seen;
- (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
- int (List.length hyps) ++ str " hypotheses"); with _ -> () );
+(* (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++ *)
+(* int (List.length hyps) ++ str " hypotheses"); with _ -> () ); *)
(* Evar arguments are created in inverse order,
and we must not apply to defined ones (i.e. LetIn's)
*)
@@ -126,7 +126,6 @@ let eterm_obligations name nclen evm t tycon =
(* 'Serialize' the evars, we assume that the types of the existentials
refer to previous existentials in the list only *)
let evl = List.rev (to_list evm) in
- trace (str "Eterm, transformed to list");
let evn =
let i = ref (-1) in
List.rev_map (fun (id, ev) -> incr i;
@@ -136,13 +135,9 @@ let eterm_obligations name nclen evm t tycon =
(* Remove existential variables in types and build the corresponding products *)
fold_right
(fun (id, (n, nstr), ev) l ->
- trace (str "Eterm: " ++ str "treating evar: " ++ int id);
let hyps = Environ.named_context_of_val ev.evar_hyps in
let hyps = trunc_named_context nclen hyps in
- trace (str "Named context is: " ++ Printer.pr_named_context (Global.env ()) hyps);
let evtyp, deps = etype_of_evar l ev hyps in
- trace (str "Evar " ++ str (string_of_int n) ++ str "'s type is: " ++ Termops.print_constr_env (Global.env ()) evtyp ++
- str " depends on evars : " ++ str (Subtac_utils.string_of_intset deps));
let y' = (id, ((n, nstr), hyps, evtyp, deps)) in
y' :: l)
evn []
@@ -153,17 +148,17 @@ let eterm_obligations name nclen evm t tycon =
let evars =
List.map (fun (_, ((_, name), _, typ, deps)) -> name, typ, deps) evts
in
- (try
- trace (str "Term given to eterm" ++ spc () ++
- Termops.print_constr_env (Global.env ()) t);
- trace (str "Term constructed in eterm" ++ spc () ++
- Termops.print_constr_env (Global.env ()) t');
- ignore(iter
- (fun (name, typ, deps) ->
- trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++
- Termops.print_constr_env (Global.env ()) typ))
- evars);
- with _ -> ());
+(* (try *)
+(* trace (str "Term given to eterm" ++ spc () ++ *)
+(* Termops.print_constr_env (Global.env ()) t); *)
+(* trace (str "Term constructed in eterm" ++ spc () ++ *)
+(* Termops.print_constr_env (Global.env ()) t'); *)
+(* ignore(iter *)
+(* (fun (name, typ, deps) -> *)
+(* trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++ *)
+(* Termops.print_constr_env (Global.env ()) typ)) *)
+(* evars); *)
+(* with _ -> ()); *)
Array.of_list (List.rev evars), t'
let mkMetas n =
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 129ac75df..337cc09fc 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -109,6 +109,10 @@ VERNAC COMMAND EXTEND Subtac_Solve_Obligations
| [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ]
END
+VERNAC COMMAND EXTEND Subtac_Set_Solver
+| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.interp t) ]
+END
+
VERNAC COMMAND EXTEND Subtac_Show_Obligations
| [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ]
| [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ]
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 4433239f3..a7ad70c8a 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -155,14 +155,16 @@ let start_proof_and_print env isevars idopt k t hook =
print_subgoals ()
(*if !pcoq <> None then (out_some !pcoq).start_proof ()*)
+let _ = Subtac_obligations.set_default_tactic
+ (Tacinterp.eval_tactic (utils_call "subtac_simpl" []))
+
+
let subtac (loc, command) =
check_required_library ["Coq";"Init";"Datatypes"];
check_required_library ["Coq";"Init";"Specif"];
(* check_required_library ["Coq";"Logic";"JMeq"]; *)
require_library "Coq.subtac.FixSub";
require_library "Coq.subtac.Utils";
- Subtac_obligations.set_default_tactic
- (Tacinterp.eval_tactic (utils_call "subtac_simpl" []));
let env = Global.env () in
let isevars = ref (create_evar_defs Evd.empty) in
try
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index e6404d7f2..cea3fbf51 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1188,8 +1188,6 @@ let rec generalize_problem pb = function
| [] -> pb
| i::l ->
let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in
- trace (str "In generalize_problem");
- debug 4 (str "Generalize problem: decl " ++ my_print_context (push_rel d pb.env));
let pb' = generalize_problem pb l in
let tomatch = lift_tomatch_stack 1 pb'.tomatch in
let tomatch = regeneralize_index_tomatch (i+1) tomatch in
@@ -1204,13 +1202,7 @@ let build_leaf pb =
| None -> anomaly "Predicate not found"
| Some (PrCcl typ) -> mk_tycon typ
| Some _ -> anomaly "not all parameters of pred have been consumed" in
- (try trace (str "In build leaf:");
- trace (str "typing: " ++ my_print_rawconstr rhs.rhs_env rhs.it);
- trace (str "env is: " ++ my_print_env rhs.rhs_env)
- with _ -> trace (str "error"));
- let x = tag, pb.typing_function tycon rhs.rhs_env rhs.it in
- trace (str "end build leaf");
- x
+ tag, pb.typing_function tycon rhs.rhs_env rhs.it
(* Building the sub-problem when all patterns are variables *)
let shift_problem (current,t) pb =
@@ -1340,8 +1332,6 @@ and match_current pb tomatch =
let ci = make_case_info pb.env mind RegularStyle tags in
let case = mkCase (ci,nf_betaiota pred,current,brvals) in
let inst = List.map mkRel deps in
- debug 4 (str "Building app: " ++ my_print_constr pb.env (applist (case, inst)) ++
- str " for deps " ++ str (string_of_list "," string_of_int deps));
pattern_status tags,
{ uj_val = applist (case, inst);
uj_type = substl inst typ }
@@ -1358,7 +1348,6 @@ and compile_generalization pb d rest =
tomatch = rest;
pred = option_map ungeneralize_predicate pb.pred;
mat = List.map (push_rels_eqn [d]) pb.mat } in
- debug 4 (str "Compile generalization: " ++ my_print_env pb.env);
let patstat,j = compile pb in
patstat,
{ uj_val = mkLambda_or_LetIn d j.uj_val;
@@ -1628,7 +1617,7 @@ let constr_of_pat env isevars ty pat =
(* trace (str "Treating pattern variable " ++ str (string_of_id (id_of_name name))); *)
PatVar (l, name), [name, None, ty], mkRel 1, 1
| PatCstr (l,((_, i) as cstr),args,alias) ->
- let ind = inductive_of_constructor cstr in
+ let _ind = inductive_of_constructor cstr in
let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) ty in
let ind, params = dest_ind_family indf in
let cstrs = get_constructors env indf in
@@ -1656,9 +1645,9 @@ let constr_of_pat env isevars ty pat =
else pat', sign, app, n
in
let pat', sign, y, z = typ env ty pat in
- let prod = it_mkProd_or_LetIn y sign in
- trace (str "Pattern: " ++ Printer.pr_cases_pattern pat ++ str " becomes constr : " ++
- my_print_constr env prod);
+(* let prod = it_mkProd_or_LetIn y sign in *)
+(* trace (str "Pattern: " ++ Printer.pr_cases_pattern pat ++ str " becomes constr : " ++ *)
+(* my_print_constr env prod); *)
pat', (sign, y)
let mk_refl typ a = mkApp (Lazy.force eq_refl, [| typ; a |])
@@ -1707,49 +1696,56 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs =
in
let newpatterns, pats = List.split pats in
let rhs_rels, signlen =
- List.fold_left (fun (env, n) (sign,_) -> (sign @ env, List.length sign + n))
+ List.fold_left (fun (renv, n) (sign,_) ->
+ ((lift_rel_context n sign) @ renv, List.length sign + n))
([], 0) pats in
let eqs, _, _ = List.fold_left2
(fun (eqs, n, slen) (sign, c) (tm, ty) ->
- let len = n + signlen in
- let cstrlen = slen - List.length sign in
- let cstr = liftn (signlen - slen) signlen (lift cstrlen c) in
+ let len = n + signlen in (* Number of already defined equations + signature *)
+ let csignlen = List.length sign in
+ let slen' = slen - csignlen in (* Lift to get pattern variables signature *)
+ let c = liftn (signlen - slen) signlen c in (* Lift to jump over previous ind signatures for pattern variables outside sign
+ in c (e.g. type arguments of constructors instanciated by variables ) *)
+ let cstr = lift (slen' + n) c in
+(* trace (str "lift " ++ my_print_constr (push_rels sign env) c ++ *)
+(* str " by " ++ int ++ str " to get " ++ *)
+(* my_print_constr (push_rels sign env) cstr); *)
let app =
mkApp (Lazy.force eq_ind,
[| lift len (type_of_tomatch ty); cstr; lift len tm |])
- in app :: eqs, succ n, cstrlen + 1)
+ in app :: eqs, succ n, slen')
([], 0, signlen) pats tomatchs
in
let eqs_rels = List.map (fun eq -> Name (id_of_string "H"), None, eq) eqs in
(* let ineqs = build_ineqs eqns newpatterns in *)
let rhs_rels' = eqs_rels @ rhs_rels in
let rhs_env = push_rels rhs_rels' env in
- (try trace (str "branch env: " ++ print_env rhs_env)
- with _ -> trace (str "error in print branch env"));
+(* (try trace (str "branch env: " ++ print_env rhs_env) *)
+(* with _ -> trace (str "error in print branch env")); *)
let tycon = lift_tycon (List.length eqs + signlen) tycon in
let j = typing_fun tycon rhs_env eqn.rhs.it in
- (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++
- str "Typed branch: " ++ Prettyp.print_judgment rhs_env j);
- with _ ->
- trace (str "Error in typed branch pretty printing"));
+(* (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++ *)
+(* str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); *)
+(* with _ -> *)
+(* trace (str "Error in typed branch pretty printing")); *)
let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in
let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
- (try trace (str "Branch decl: " ++ pr_rel_decl env (Name branch_name, Some bbody, btype))
- with _ -> trace (str "Error in branch decl pp"));
+(* (try trace (str "Branch decl: " ++ pr_rel_decl env (Name branch_name, Some bbody, btype)) *)
+(* with _ -> trace (str "Error in branch decl pp")); *)
let branch =
let bref = RVar (dummy_loc, branch_name) in
- match vars_of_ctx rhs_rels' with
+ match vars_of_ctx rhs_rels with
[] -> bref
| l -> RApp (dummy_loc, bref, l)
in
- let branch =
- List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels
- in
- (try trace (str "New branch: " ++ Printer.pr_rawconstr branch)
- with _ -> trace (str "Error in new branch pp"));
+(* let branch = *)
+(* List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels *)
+(* in *)
+(* (try trace (str "New branch: " ++ Printer.pr_rawconstr branch) *)
+(* with _ -> trace (str "Error in new branch pp")); *)
incr i;
let rhs = { eqn.rhs with it = branch } in
(branch_decl :: branches,
@@ -1770,40 +1766,52 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs =
* A type constraint but no annotation case: it is assumed non dependent.
*)
-let prepare_predicate loc typing_fun isevars env tomatchs sign tycon =
+let prepare_predicate_from_tycon loc typing_fun isevars env tomatchs sign tycon =
(* We extract the signature of the arity *)
let arsign = extract_arity_signature env tomatchs sign in
- let env0 = env in
- let env = List.fold_right push_rels arsign env in
+(* let env = List.fold_right push_rels arsign env in *)
let allnames = List.rev (List.map (List.map pi1) arsign) in
let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
let pred = out_some (valcon_of_tycon tycon) in
let predcclj, pred, neqs =
let _, _, eqs =
- List.fold_right2
- (fun ctx (tm,_) (lift0, lift1, eqs) ->
+ List.fold_left2
+ (fun (neqs, slift, eqs) ctx (tm,ty) ->
let len = List.length ctx in
- let name, _, typ = List.hd ctx in
+ let _name, _, _typ' = List.hd ctx in (* FixMe: Ignoring dependent inductives *)
let eq = mkApp (Lazy.force eq_ind,
- [| lift lift0 typ;
- mkRel (lift0 - ((len - 1) + lift1));
- lift lift0 tm|])
+ [| lift (neqs + nar) (type_of_tomatch ty);
+ mkRel (neqs + slift);
+ lift (neqs + nar) tm|])
in
- (succ lift0, lift1 + len, (Anonymous, None, eq) :: eqs))
- arsign tomatchs (nar, 0, [])
+ (succ neqs, slift - len, (Anonymous, None, eq) :: eqs))
+ (0, nar, []) (List.rev arsign) tomatchs
in
let len = List.length eqs in
it_mkProd_wo_LetIn (lift (nar + len) pred) eqs, pred, len
in
let predccl = nf_isevar !isevars predcclj in
- trace (str "Predicate: " ++ my_print_constr env predccl);
build_initial_predicate true allnames predccl, pred
-
+
+let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
+ (* We extract the signature of the arity *)
+ let arsign = extract_arity_signature env tomatchs sign in
+ let env = List.fold_right push_rels arsign env in
+ let allnames = List.rev (List.map (List.map pi1) arsign) in
+ let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
+(* let _ = *)
+(* option_map (fun tycon -> *)
+(* isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val *)
+(* (lift_tycon_type (List.length arsign) tycon)) *)
+(* tycon *)
+(* in *)
+ let predccl = (j_nf_isevar !isevars predcclj).uj_val in
+ Some (build_initial_predicate true allnames predccl)
+
(**************************************************************************)
(* Main entry of the matching compilation *)
let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
- let env0 = env in
let tycon0 = tycon in
(* We build the matrix of patterns and right-hand-side *)
let matx = matx_of_eqns env tomatchl eqns in
@@ -1811,46 +1819,69 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
(* We build the vector of terms to match consistently with the *)
(* constructors found in patterns *)
let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
-
- let lets, matx = constrs_of_pats typing_fun tycon env isevars matx tomatchs in
- let matx = List.rev matx in
- trace (str "Old env: " ++ my_print_env env);
- let env = push_rels lets env in
- let len = List.length lets in
- let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
- trace (str "New env: " ++ my_print_env env);
- let tycon = lift_tycon len tycon in
- let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
- let args = List.map (fun (tm,ty) -> mk_refl (type_of_tomatch ty) tm) tomatchs in
-
- (* We build the elimination predicate if any and check its consistency *)
- (* with the type of arguments to match *)
- let tmsign = List.map snd tomatchl in
- let pred, opred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon in
-
- (* We push the initial terms to match and push their alias to rhs' envs *)
- (* names of aliases will be recovered from patterns (hence Anonymous here) *)
- let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
-
- let pb =
- { env = env;
- isevars = isevars;
- pred = Some pred;
- tomatch = initial_pushed;
- history = start_history (List.length initial_pushed);
- mat = matx;
- caseloc = loc;
- typing_function = typing_fun } in
-
- let _, j = compile pb in
- (* We check for unused patterns *)
- List.iter (check_unused_pattern env) matx;
- let ty = out_some (valcon_of_tycon tycon0) in
- let j =
- { uj_val = it_mkLambda_or_LetIn (applistc j.uj_val args) lets;
- uj_type = ty; }
- in
- trace (str"final judgement:" ++ Prettyp.print_judgment env0 j ++ spc ());
- inh_conv_coerce_to_tycon loc env isevars j tycon0
+ match predopt with
+ None ->
+ let lets, matx = constrs_of_pats typing_fun tycon env isevars matx tomatchs in
+ let matx = List.rev matx in
+ let env = push_rels lets env in
+ let len = List.length lets in
+ let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
+ let tycon = lift_tycon len tycon in
+ let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
+ let args = List.map (fun (tm,ty) -> mk_refl (type_of_tomatch ty) tm) tomatchs in
+
+ (* We build the elimination predicate if any and check its consistency *)
+ (* with the type of arguments to match *)
+ let tmsign = List.map snd tomatchl in
+ let pred, opred = prepare_predicate_from_tycon loc typing_fun isevars env tomatchs tmsign tycon in
+
+ (* We push the initial terms to match and push their alias to rhs' envs *)
+ (* names of aliases will be recovered from patterns (hence Anonymous here) *)
+ let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
+
+ let pb =
+ { env = env;
+ isevars = isevars;
+ pred = Some pred;
+ tomatch = initial_pushed;
+ history = start_history (List.length initial_pushed);
+ mat = matx;
+ caseloc = loc;
+ typing_function = typing_fun } in
+
+ let _, j = compile pb in
+ (* We check for unused patterns *)
+ List.iter (check_unused_pattern env) matx;
+ let ty = out_some (valcon_of_tycon tycon0) in
+ let j =
+ { uj_val = it_mkLambda_or_LetIn (applistc j.uj_val args) lets;
+ uj_type = ty; }
+ in
+ inh_conv_coerce_to_tycon loc env isevars j tycon0
+
+ | Some rtntyp ->
+ (* We build the elimination predicate if any and check its consistency *)
+ (* with the type of arguments to match *)
+ let tmsign = List.map snd tomatchl in
+ let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon rtntyp in
+
+ (* We push the initial terms to match and push their alias to rhs' envs *)
+ (* names of aliases will be recovered from patterns (hence Anonymous here) *)
+ let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
+
+ let pb =
+ { env = env;
+ isevars = isevars;
+ pred = pred;
+ tomatch = initial_pushed;
+ history = start_history (List.length initial_pushed);
+ mat = matx;
+ caseloc = loc;
+ typing_function = typing_fun } in
+
+ let _, j = compile pb in
+ (* We check for unused patterns *)
+ List.iter (check_unused_pattern env) matx;
+ inh_conv_coerce_to_tycon loc env isevars j tycon
end
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index c78145357..16363ac67 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -53,8 +53,6 @@ module Coercion = struct
| _ -> None
and disc_exist env x =
- (try trace (str "Disc_exist: " ++ my_print_constr env x)
- with _ -> ());
match kind_of_term x with
| App (c, l) ->
(match kind_of_term c with
@@ -67,8 +65,6 @@ module Coercion = struct
let disc_proj_exist env x =
- (try trace (str "disc_proj_exist: " ++ my_print_constr env x);
- with _ -> ());
match kind_of_term x with
| App (c, l) ->
(if Term.eq_constr c (Lazy.force sig_).proj1
@@ -108,27 +104,27 @@ module Coercion = struct
: (Term.constr -> Term.constr) option
=
let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
- (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++
- str " and "++ my_print_constr env y ++
- str " with evars: " ++ spc () ++
- my_print_evardefs !isevars);
- with _ -> ());
+(* (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++ *)
+(* str " and "++ my_print_constr env y ++ *)
+(* str " with evars: " ++ spc () ++ *)
+(* my_print_evardefs !isevars); *)
+(* with _ -> ()); *)
let rec coerce_unify env x y =
- (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++
- str " to "++ my_print_constr env y)
- with _ -> ());
+(* (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++ *)
+(* str " to "++ my_print_constr env y) *)
+(* with _ -> ()); *)
try
isevars := the_conv_x_leq env x y !isevars;
- (try debug 1 (str "Unified " ++ (my_print_constr env x) ++
- str " and "++ my_print_constr env y);
- with _ -> ());
+(* (try debug 1 (str "Unified " ++ (my_print_constr env x) ++ *)
+(* str " and "++ my_print_constr env y); *)
+(* with _ -> ()); *)
None
with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y)
and coerce' env x y : (Term.constr -> Term.constr) option =
let subco () = subset_coerce env isevars x y in
- (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++
- str " to "++ my_print_constr env y);
- with _ -> ());
+(* (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++ *)
+(* str " to "++ my_print_constr env y); *)
+(* with _ -> ()); *)
match (kind_of_term x, kind_of_term y) with
| Sort s, Sort s' ->
(match s, s' with
@@ -163,7 +159,6 @@ module Coercion = struct
if i = Term.destInd existS.typ
then
begin
- trace (str "In coerce sigma types");
let (a, pb), (a', pb') =
pair_of_array l, pair_of_array l'
in
@@ -186,7 +181,6 @@ module Coercion = struct
let c2 = coerce_unify env' b b' in
match c1, c2 with
None, None ->
- trace (str "No coercion needed");
None
| _, _ ->
Some
@@ -201,7 +195,6 @@ module Coercion = struct
end
else
begin
- debug 1 (str "In coerce prod types");
let (a, b), (a', b') =
pair_of_array l, pair_of_array l'
in
@@ -236,7 +229,25 @@ module Coercion = struct
(* mkApp (Lazy.force eqrec, *)
(* [| argtype; argx; pred; x; argy; evar |])) *)
(* else *)subco ()
- | _ -> subco ())
+ | x, y when x = y ->
+ let lam_type = Typing.type_of env (evars_of !isevars) c in
+ let rec coerce typ i co =
+ if i < Array.length l then
+ let hdx = l.(i) and hdy = l'.(i) in
+ let (n, eqT, restT) = destProd typ in
+ let pred = mkLambda (n, eqT, mkApp (lift 1 c, [| mkRel 1 |])) in
+ let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in
+ let evar = make_existential dummy_loc env isevars eq in
+ let eq_app x = mkApp (Lazy.force eq_rect,
+ [| eqT; hdx; pred; x; hdy; evar|])
+ in
+ coerce (subst1 hdy restT) (succ i) (fun x -> eq_app (co x))
+ else co
+ in
+ if Array.length l = Array.length l' then
+ Some (coerce lam_type 0 (fun x -> x))
+ else subco ()
+ | _ -> subco ())
| _, _ -> subco ()
and subset_coerce env isevars x y =
@@ -387,13 +398,13 @@ module Coercion = struct
with Reduction.NotConvertible -> raise NoCoercion
let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
- (try
- debug 1 (str "inh_conv_coerce_to_fail called for " ++
- Termops.print_constr_env env t ++ str " and "++ spc () ++
- Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++
- Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
- Termops.print_env env);
- with _ -> ());
+(* (try *)
+(* debug 1 (str "inh_conv_coerce_to_fail called for " ++ *)
+(* Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
+(* Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++ *)
+(* Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
+(* Termops.print_env env); *)
+(* with _ -> ()); *)
try (the_conv_x_leq env t c1 isevars, v, t)
with Reduction.NotConvertible ->
(try
@@ -452,14 +463,14 @@ module Coercion = struct
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
- let inh_conv_coerce_to loc env isevars cj ((n, t) as tycon) =
- (try
- debug 1 (str "Subtac_coercion.inh_conv_coerce_to called for " ++
- Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++
- Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
- Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
- Termops.print_env env);
- with _ -> ());
+ let inh_conv_coerce_to loc env isevars cj ((n, t) as _tycon) =
+(* (try *)
+(* debug 1 (str "Subtac_coercion.inh_conv_coerce_to called for " ++ *)
+(* Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++ *)
+(* Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *)
+(* Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
+(* Termops.print_env env); *)
+(* with _ -> ()); *)
match n with
None ->
let (evd', val', type') =
@@ -477,40 +488,38 @@ module Coercion = struct
| Some (init, cur) ->
(isevars, cj)
- let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
- (try
- debug 1 (str "Subtac_coercion.inh_conv_coerces_to called for " ++
- Termops.print_constr_env env t ++ str " and "++ spc () ++
- Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
- Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
- Termops.print_env env);
- with _ -> ());
+ let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) =
+(* (try *)
+(* trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++ *)
+(* Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
+(* Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *)
+(* Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
+(* Termops.print_env env); *)
+(* with _ -> ()); *)
let nabsinit, nabs =
match abs with
None -> 0, 0
| Some (init, cur) -> init, cur
in
- let (rels, rng) =
(* a little more effort to get products is needed *)
- try decompose_prod_n nabs t
- with _ ->
- trace (str "decompose_prod_n failed");
- raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to")
- in
- (* The final range free variables must have been replaced by evars, we accept only that evars
- in rng are applied to free vars. *)
- if noccur_with_meta 0 (succ nabsinit) rng then (
- trace (str "No occur between 0 and " ++ int (succ nabsinit));
- let env', t, t' =
- let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
- env', rng, lift nabs t'
- in
- try
- pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t'
- with NoCoercion ->
- coerce_itf loc env' isevars None t t')
- with NoSubtacCoercion ->
- let sigma = evars_of isevars in
- error_cannot_coerce env' sigma (t, t'))
- else isevars
+ try let rels, rng = decompose_prod_n nabs t in
+ (* The final range free variables must have been replaced by evars, we accept only that evars
+ in rng are applied to free vars. *)
+ if noccur_with_meta 0 (succ nabsinit) rng then (
+(* trace (str "No occur between 0 and " ++ int (succ nabsinit)); *)
+ let env', t, t' =
+ let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
+ env', rng, lift nabs t'
+ in
+ try
+ pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t'
+ with NoCoercion ->
+ coerce_itf loc env' isevars None t t')
+ with NoSubtacCoercion ->
+ let sigma = evars_of isevars in
+ error_cannot_coerce env' sigma (t, t'))
+ else isevars
+ with _ -> isevars
+ (* trace (str "decompose_prod_n failed"); *)
+ (* raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *)
end
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index ef6d0bed1..68ab8c46e 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -57,7 +57,7 @@ let interp_gen kind isevars env
c =
let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
let c' = Subtac_utils.rewrite_cases env c' in
- (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ());
+(* (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *)
let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
evar_nf isevars c'
@@ -176,19 +176,19 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let sigma = Evd.empty in
let isevars = ref (Evd.create_evar_defs sigma) in
let env = Global.env() in
- let pr c = my_print_constr env c in
- let prr = Printer.pr_rel_context env in
- let prn = Printer.pr_named_context env in
- let pr_rel env = Printer.pr_rel_context env in
let nc = named_context env in
let nc_len = named_context_length nc in
- let _ =
- try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
- Ppconstr.pr_binders bl ++ str " : " ++
- Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
- Ppconstr.pr_constr_expr body)
- with _ -> ()
- in
+(* let pr c = my_print_constr env c in *)
+(* let prr = Printer.pr_rel_context env in *)
+(* let prn = Printer.pr_named_context env in *)
+(* let pr_rel env = Printer.pr_rel_context env in *)
+(* let _ = *)
+(* try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ *)
+(* Ppconstr.pr_binders bl ++ str " : " ++ *)
+(* Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++ *)
+(* Ppconstr.pr_constr_expr body) *)
+(* with _ -> () *)
+ (* in *)
let env', binders_rel = interp_context 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
@@ -228,9 +228,8 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let top_bl = after @ (arg :: before) in
let intern_bl = after @ (wfarg 1 :: arg :: before) in
let top_env = push_rel_context top_bl env in
- let intern_env = push_rel_context intern_bl env in
+ let _intern_env = push_rel_context intern_bl env in
let top_arity = interp_type isevars top_env arityc in
- (try debug 2 (str "Intern bl: " ++ prr intern_bl) with _ -> ());
let proj = (Lazy.force sig_).Coqlib.proj1 in
let projection =
mkApp (proj, [| argtyp ;
@@ -239,32 +238,32 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
mkRel 1
|])
in
- (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ());
+ (* (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ()); *)
let intern_arity = substnl [projection] after_length top_arity in
- (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ());
+(* (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ()); *)
let intern_before_env = push_rel_context before env in
let intern_fun_bl = after @ [wfarg 1] in
- (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ());
+(* (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ()); *)
let intern_fun_arity = intern_arity in
- (try debug 2 (str "Intern fun arity: " ++
- my_print_constr intern_env intern_fun_arity) with _ -> ());
+(* (try debug 2 (str "Intern fun arity: " ++ *)
+(* my_print_constr intern_env intern_fun_arity) with _ -> ()); *)
let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in
let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
let fun_bl = after @ (intern_fun_binder :: [arg]) in
- (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ());
+(* (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 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 _ =
- try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++
- str "Intern bl" ++ prr intern_bl ++ spc () ++
- str "Top bl" ++ prr top_bl ++ spc () ++
- str "Intern arity: " ++ pr intern_arity ++
- str "Top arity: " ++ pr top_arity ++ spc () ++
- str "Intern body " ++ pr intern_body_lam)
- with _ -> ()
- in
+(* let _ = *)
+(* try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++ *)
+(* str "Intern bl" ++ prr intern_bl ++ spc () ++ *)
+(* str "Top bl" ++ prr top_bl ++ spc () ++ *)
+(* str "Intern arity: " ++ pr intern_arity ++ *)
+(* str "Top arity: " ++ pr top_arity ++ spc () ++ *)
+(* str "Intern body " ++ pr intern_body_lam) *)
+(* with _ -> () *)
+(* in *)
let _impl =
if Impargs.is_implicit_args()
then Impargs.compute_implicits top_env top_arity
@@ -288,28 +287,23 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
let def = it_mkLambda_or_LetIn def_appl binders_rel in
let typ = it_mkProd_or_LetIn top_arity binders_rel in
- debug 2 (str "Constructed def");
- debug 2 (my_print_constr intern_before_env def);
- debug 2 (str "Type: " ++ my_print_constr env typ);
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 _ = 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 = non_instanciated_map env isevars in
- let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in
+ (* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *)
let evars, evars_def = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some 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 _ -> ());
- trace (str "Adding to obligations list");
- Subtac_obligations.add_definition recname evars_def fullctyp evars;
- trace (str "Added to obligations list")
-
+ (* (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 fullctyp evars
+
let build_mutrec l boxed =
let sigma = Evd.empty and env = Global.env () in
let nc = named_context env in
@@ -322,9 +316,9 @@ let build_mutrec l boxed =
and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
in
(* Build the recursive context and notations for the recursive types *)
- let (rec_sign,rec_impls,arityl) =
+ let (rec_sign,rec_env,rec_impls,arityl) =
List.fold_left
- (fun (env,impls,arl) ((recname, n, bl,arityc,body),_) ->
+ (fun (sign,env,impls,arl) ((recname, n, bl,arityc,body),_) ->
let isevars = ref (Evd.create_evar_defs sigma) in
let arityc = Command.generalize_constr_expr arityc bl in
let arity = interp_type isevars env arityc in
@@ -333,8 +327,8 @@ let build_mutrec l boxed =
then Impargs.compute_implicits env arity
else [] in
let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
- (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl))
- (env,[],[]) lnameargsardef in
+ ((recname,None,arity) :: sign, Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl))
+ ([],env,[],[]) lnameargsardef in
let arityl = List.rev arityl in
let notations =
List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l)
@@ -353,11 +347,11 @@ let build_mutrec l boxed =
match info with
None ->
let def = abstract_constr_expr def bl in
- isevars, info, interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
+ isevars, info, interp_casted_constr isevars rec_env ~impls:([],rec_impls)
def arity
| Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) ->
- let rec_sign = push_rel_context fun_bl rec_sign in
- let cstr = interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
+ 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 isevars, info, it_mkLambda_or_LetIn cstr fun_bl)
lnameargsardef arityl
@@ -365,34 +359,32 @@ let build_mutrec l boxed =
States.unfreeze fs; raise e in
States.unfreeze fs; def
in
-
let (lnonrec,(namerec,defrec,arrec,nvrec)) =
collect_non_rec env lrecnames recdef arityl nv in
let recdefs = Array.length defrec in
- trace (int recdefs ++ str " recursive definitions");
(* Solve remaining evars *)
let rec collect_evars i acc =
if i < recdefs then
let (isevars, info, def) = defrec.(i) in
- let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in
+ (* let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in *)
let def = evar_nf isevars def in
let isevars = Evd.undefined_evars !isevars in
- let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in
+ (* let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in *)
let evm = Evd.evars_of isevars in
let _, _, typ = arrec.(i) in
let id = namerec.(i) in
- (* Generalize by the recursive prototypes *)
+ (* Generalize by the recursive prototypes *)
let def =
- Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
+ Termops.it_mkNamedLambda_or_LetIn def rec_sign
and typ =
- Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign)
+ Termops.it_mkNamedProd_or_LetIn typ rec_sign
in
let evars, def = Eterm.eterm_obligations id nc_len evm def (Some typ) in
- collect_evars (succ i) ((id, nvrec.(i), def, typ, evars) :: acc)
+ collect_evars (succ i) ((id, def, typ, evars) :: acc)
else acc
in
let defs = collect_evars 0 [] in
- Subtac_obligations.add_mutual_definitions (List.rev defs)
+ Subtac_obligations.add_mutual_definitions (List.rev defs) nvrec
let out_n = function
Some n -> n
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index fd0d289e3..5119145f4 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -28,7 +28,8 @@ type program_info = {
prg_body: constr;
prg_type: constr;
prg_obligations: obligations;
- prg_deps : (identifier * int) list;
+ prg_deps : identifier list;
+ prg_nvrec : int array;
}
let assumption_message id =
@@ -126,7 +127,6 @@ open Ppconstr
let declare_mutual_definition l =
let len = List.length l in
- let l, nvlist = List.split 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)
@@ -137,7 +137,7 @@ let declare_mutual_definition l =
let subs = (subst_body x) in
snd (decompose_lam_n len subs)) l)
in
- let nvrec = Array.of_list nvlist 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 () ++
@@ -183,7 +183,7 @@ let try_tactics obls =
let red = Reductionops.nf_betaiota
-let init_prog_info n b t deps obls =
+let init_prog_info n b t deps nvrec obls =
let obls' =
Array.mapi
(fun i (n, t, d) ->
@@ -194,7 +194,7 @@ let init_prog_info n b t deps obls =
obls
in
{ prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
- prg_deps = deps }
+ prg_deps = deps; prg_nvrec = nvrec; }
let pperror cmd = Util.errorlabstrm "Subtac" cmd
let error s = pperror (str s)
@@ -227,37 +227,11 @@ let update_obls prg obls rem =
declare_definition prg';
from_prg := ProgMap.remove prg.prg_name !from_prg
| l ->
- let progs = List.map (fun (x,y) -> ProgMap.find x !from_prg, y) prg'.prg_deps in
- if List.for_all (fun x -> obligations_solved (fst x)) progs then
+ let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
+ if List.for_all (fun x -> obligations_solved x) progs then
(declare_mutual_definition progs;
from_prg := List.fold_left
- (fun acc x -> ProgMap.remove (fst x).prg_name acc) !from_prg progs))
-
-let add_definition n b t obls =
- Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
- let prg = init_prog_info n b t [] obls in
- let obls,_ = prg.prg_obligations in
- if Array.length obls = 0 then (
- Options.if_verbose ppnl (str ".");
- declare_definition prg;
- from_prg := ProgMap.remove prg.prg_name !from_prg)
- else (
- let len = Array.length obls in
- let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
- from_prg := ProgMap.add n prg !from_prg)
-
-let add_mutual_definitions l =
- let deps = List.map (fun (n, nclen, b, t, obls) -> n, nclen) l in
- let upd = List.fold_left
- (fun acc (n, nclen, b, t, obls) ->
- let prg = init_prog_info n b t deps obls in
- ProgMap.add n prg acc)
- !from_prg l
- in
- from_prg := upd;
- let prg = (ProgMap.find (fst (List.hd deps)) !from_prg) in
- let o, r = prg.prg_obligations in
- update_obls prg o r
+ (fun acc x -> ProgMap.remove x.prg_name acc) !from_prg progs))
let is_defined obls x = obls.(x).obl_body <> None
@@ -272,20 +246,24 @@ let solve_obligation prg num =
let user_num = succ num in
let obls, rem = prg.prg_obligations in
let obl = obls.(num) in
- match deps_remaining obls obl.obl_deps with
- [] ->
- let obl = subst_deps_obl obls obl in
- Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type
- (fun strength gr ->
- debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished");
- let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
- let obls = Array.copy obls in
- let _ = obls.(num) <- obl in
- update_obls prg obls (pred rem));
- Pfedit.by !default_tactic;
- trace (str "Started obligation " ++ int user_num ++ str " proof")
- | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
- ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
+ if obl.obl_body <> None then
+ pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")
+ else
+ match deps_remaining obls obl.obl_deps with
+ [] ->
+ let obl = subst_deps_obl obls obl in
+ Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type
+ (fun strength gr ->
+ debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished");
+ let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
+ let obls = Array.copy obls in
+ let _ = obls.(num) <- obl in
+ update_obls prg obls (pred rem));
+ Pfedit.by !default_tactic;
+ trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
+ Subtac_utils.my_print_constr (Global.env ()) obl.obl_type)
+ | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
+ ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
let subtac_obligation (user_num, name, typ) =
let num = pred user_num in
@@ -311,6 +289,20 @@ let obligations_of_evars evars =
}) evars)
in arr, Array.length arr
+let solve_obligation_by_tac prg obls i tac =
+ let obl = obls.(i) in
+ match obl.obl_body with
+ Some _ -> false
+ | None ->
+ (try
+ if deps_remaining obls obl.obl_deps = [] then
+ let obl = subst_deps_obl obls obl in
+ let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
+ obls.(i) <- { obl with obl_body = Some t };
+ true
+ else false
+ with _ -> false)
+
let solve_obligations n tac =
let prg = get_prog n in
let obls, rem = prg.prg_obligations in
@@ -318,22 +310,37 @@ let solve_obligations n tac =
let obls' = Array.copy obls in
let _ =
Array.iteri (fun i x ->
- match x.obl_body with
- Some _ -> ()
- | None ->
- (try
- if deps_remaining obls' x.obl_deps = [] then
- let t = Subtac_utils.solve_by_tac (evar_of_obligation x) tac in
- decr rem;
- obls'.(i) <- { x with obl_body = Some t }
- else ()
- with UserError (s, cmds) ->
- debug 1 cmds
- | _ -> ()))
+ if solve_obligation_by_tac prg obls' i tac then
+ decr rem)
obls'
in
update_obls prg obls' !rem
+let add_definition n b t obls =
+ Options.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 in
+ let obls,_ = prg.prg_obligations in
+ if Array.length obls = 0 then (
+ Options.if_verbose ppnl (str ".");
+ declare_definition prg;
+ from_prg := ProgMap.remove prg.prg_name !from_prg)
+ else (
+ let len = Array.length obls in
+ let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
+ from_prg := ProgMap.add n prg !from_prg;
+ solve_obligations (Some n) !default_tactic)
+
+let add_mutual_definitions l nvrec =
+ let deps = List.map (fun (n, b, t, 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 in
+ ProgMap.add n prg acc)
+ !from_prg l
+ in
+ from_prg := upd;
+ solve_obligations (Some (List.hd deps)) !default_tactic
+
let admit_obligations n =
let prg = get_prog n in
let obls, rem = prg.prg_obligations in
@@ -356,15 +363,18 @@ let array_find f arr =
raise Not_found
with Found i -> i
-let next_obligation n =
+let rec next_obligation n =
let prg = get_prog n in
let obls, rem = prg.prg_obligations in
let i =
array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = [])
obls
in
- solve_obligation prg i
-
+ if solve_obligation_by_tac prg obls i !default_tactic then (
+ update_obls prg obls (pred rem);
+ next_obligation n
+ ) else solve_obligation prg i
+
open Pp
let show_obligations n =
let prg = get_prog n in
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 7953fb4b0..3981d4c6c 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -8,7 +8,7 @@ val add_definition : Names.identifier -> Term.constr -> Term.types ->
obligation_info -> unit
val add_mutual_definitions :
- (Names.identifier * int * Term.constr * Term.types * obligation_info) list -> unit
+ (Names.identifier * Term.constr * Term.types * obligation_info) list -> int array -> unit
val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index d27ef4c16..7ae8f45d7 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -113,29 +113,23 @@ let env_with_binders env isevars l =
in aux (env, []) l
let subtac_process env isevars id l c tycon =
- let evars () = evars_of !isevars in
- let _ = trace (str "Creating env with binders") in
let env_binders, binders_rel = env_with_binders env isevars l in
- let _ = try (trace (str "New env created:" ++ my_print_context env_binders)) with _ -> () in
let tycon =
match tycon with
None -> empty_tycon
| Some t ->
let t = coqintern !isevars env_binders t in
- let _ = try trace (str "Internalized specification: " ++ my_print_rawconstr env_binders t) with _ -> () in
let coqt, ttyp = interp env_binders isevars t empty_tycon in
- let _ = try trace (str "Interpreted type: " ++ my_print_constr env_binders coqt) with _ -> () in
mk_tycon coqt
in
let c = coqintern !isevars env_binders c in
let c = Subtac_utils.rewrite_cases env c in
- let _ = try trace (str "Internalized term: " ++ my_print_rawconstr env c) with _ -> () in
let coqc, ctyp = interp env_binders isevars c tycon in
- let _ = try trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++
- str "Coq type: " ++ my_print_constr env_binders ctyp)
- with _ -> ()
- in
- let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) with _ -> () in
+(* let _ = try trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++ *)
+(* str "Coq type: " ++ my_print_constr env_binders ctyp) *)
+(* with _ -> () *)
+(* in *)
+(* let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) with _ -> () in *)
let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel
and fullctyp = it_mkProd_or_LetIn ctyp binders_rel
@@ -143,13 +137,13 @@ let subtac_process env isevars id l c tycon =
let fullcoqc = Evarutil.nf_evar (evars_of !isevars) fullcoqc in
let fullctyp = Evarutil.nf_evar (evars_of !isevars) fullctyp 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 _ = 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 = non_instanciated_map env isevars in
- let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in
+(* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *)
evm, fullcoqc, fullctyp
open Subtac_obligations
@@ -159,5 +153,4 @@ let subtac_proof env isevars id l c tycon =
let nc_len = named_context_length nc in
let evm, coqc, coqt = subtac_process env isevars id l c tycon in
let evars, def = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in
- trace (str "Adding to obligations list");
add_definition id def coqt evars
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index d9c193bed..9e44c9096 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -162,10 +162,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(* in environment [env], with existential variables [(evars_of isevars)] and *)
(* the type constraint tycon *)
let rec pretype (tycon : type_constraint) env isevars lvar c =
- let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++
- str " with tycon " ++ Evarutil.pr_tycon env tycon)
- with _ -> ()
- in
+(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *)
+(* str " with tycon " ++ Evarutil.pr_tycon env tycon) *)
+(* with _ -> () *)
+(* in *)
match c with
| RRef (loc,ref) ->
inh_conv_coerce_to_tycon loc env isevars
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index adf8dc620..973d2a150 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -47,6 +47,7 @@ let sig_ = lazy (build_sig ())
let eq_ind = lazy (init_constant ["Init"; "Logic"] "eq")
let eq_rec = lazy (init_constant ["Init"; "Logic"] "eq_rec")
+let eq_rect = lazy (init_constant ["Init"; "Logic"] "eq_rect")
let eq_refl = lazy (init_constant ["Init"; "Logic"] "refl_equal")
let eq_ind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal")
@@ -145,8 +146,9 @@ let print_args env args =
let make_existential loc env isevars c =
let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in
let (key, args) = destEvar evar in
- (try debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++
- print_args env args) with _ -> ());
+ (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++
+ print_args env args ++ str " for type: "++
+ my_print_constr env c) with _ -> ());
evar
let make_existential_expr loc env c =
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 95138c2fc..bb9b926b4 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -34,6 +34,7 @@ val sig_ : coq_sigma_data lazy_t
val eq_ind : constr lazy_t
val eq_rec : constr lazy_t
+val eq_rect : constr lazy_t
val eq_refl : constr lazy_t
val eq_ind_ref : global_reference lazy_t
val refl_equal_ref : global_reference lazy_t
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index 8fedeed51..809503aa2 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -8,33 +8,31 @@ Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} :
(S q' & r)
else (O & a).
-Require Import Coq.subtac.Utils.
-Require Import Coq.subtac.FixSub.
Require Import Omega.
Obligations.
Obligation 1.
intros.
- destruct_exists ; simpl in * ; auto with arith.
+ simpl in * ; auto with arith.
omega.
-Qed.
+Defined.
Obligation 2 of euclid.
intros.
- destruct_exists ; simpl in * ; auto with arith.
assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega.
-Qed.
+Defined.
Obligation 4 of euclid.
exact Wf_nat.lt_wf.
-Qed.
+Defined.
Obligation 3 of euclid.
intros.
- destruct_exists ; simpl in *.
omega.
Qed.
+Eval cbv delta [euclid_obligation_1 euclid_obligation_2] in (euclid 0).
+
Extraction Inline Fix_sub Fix_F_sub.
Extract Inductive sigT => "pair" [ "" ].
Extract Inductive sumbool => "bool" [ "true" "false" ].
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 09:39:53 +0000