From b13e95e1aa9f3518fb59579a3e8353e34953e54a Mon Sep 17 00:00:00 2001 From: msozeau Date: Thu, 1 Jun 2006 20:23:56 +0000 Subject: Fix some nasty bug with the evars-to-dependent sum encoding. Also enclose traces with try with clauses to avoid detypinging anomalies. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8889 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/subtac/eterm.ml | 26 +++++++------- contrib/subtac/subtac.ml | 6 ++-- contrib/subtac/subtac_coercion.ml | 30 +++++++++------- contrib/subtac/subtac_command.ml | 68 +++++++++++++++++++++--------------- contrib/subtac/subtac_pretyping.ml | 18 +++++----- contrib/subtac/subtac_pretyping_F.ml | 2 +- contrib/subtac/subtac_utils.ml | 44 +++++++++++++---------- contrib/subtac/subtac_utils.mli | 2 +- 8 files changed, 114 insertions(+), 82 deletions(-) diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 437acb1f2..382ae2d5b 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -47,9 +47,9 @@ let subst_evars evs n t = | Evar (k, args) -> (try let index, hyps = evar_info k in - trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++ - int (List.length hyps) ++ str " hypotheses"); - + (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++ + int (List.length hyps) ++ str " hypotheses"); with _ -> () ); + let ex = mkRel (index + depth) in (* Evar arguments are created in inverse order, and we must not apply to defined ones (i.e. LetIn's) @@ -140,15 +140,17 @@ let eterm_term evm t tycon = let id = id_of_string ("Evar" ^ string_of_int id) in tclTHEN acc (Tactics.assert_tac false (Name id) c) in - 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(option_map - (fun typ -> - trace (str "Type :" ++ spc () ++ - Termops.print_constr_env (Global.env ()) typ)) - tycon); + (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(option_map + (fun typ -> + trace (str "Type :" ++ spc () ++ + Termops.print_constr_env (Global.env ()) typ)) + tycon); + with _ -> ()); t'', tycon, evar_names let mkMetas n = diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 5b857a688..4cbfe90cf 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -48,8 +48,10 @@ let subtac_one_fixpoint env isevars (f, decl) = let ((id, n, bl, typ, body), decl) = Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl) in - let _ = trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++ - Ppconstr.pr_constr_expr body) + let _ = + try trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++ + Ppconstr.pr_constr_expr body) + with _ -> () in ((id, n, bl, typ, body), decl) diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index cdad00372..f2a1a0185 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -53,7 +53,8 @@ module Coercion = struct | _ -> None and disc_exist env x = - trace (str "Disc_exist: " ++ my_print_constr 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 @@ -66,7 +67,8 @@ module Coercion = struct let disc_proj_exist env x = - trace (str "disc_proj_exist: " ++ my_print_constr 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 @@ -104,23 +106,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 - trace (str "Coerce called for " ++ (my_print_constr env x) ++ - str " and "++ my_print_constr env y ++ - str " with evars: " ++ spc () ++ - my_print_evardefs !isevars); + (try trace (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 = - trace (str "coerce_unify from " ++ (my_print_constr env x) ++ - str " to "++ my_print_constr env y); + (try trace (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; - trace (str "Unified " ++ (my_print_constr env x) ++ - str " and "++ my_print_constr env y); + (try (trace (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 - trace (str "coerce' from " ++ (my_print_constr env x) ++ - str " to "++ my_print_constr env y); + (try trace (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 diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 552acf137..b09228c06 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -56,7 +56,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 - trace (str "Pretyping " ++ my_print_constr_expr c); + (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in evar_nf isevars c' @@ -201,10 +201,12 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl) | CWfRec r -> let n = out_some n in - let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ - Ppconstr.pr_binders bl ++ str " : " ++ - Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++ - Ppconstr.pr_constr_expr body) + let _ = + try trace (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 env0 bl in let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in @@ -234,10 +236,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed let _ = let pr c = my_print_constr env c in let prr = Printer.pr_rel_context env in - trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++ - str "Intern bl" ++ prr intern_bl ++ spc () ++ - str "Extern bl" ++ prr new_bl ++ spc () ++ - str "Intern arity: " ++ pr intern_arity) + try trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++ + str "Intern bl" ++ prr intern_bl ++ spc () ++ + str "Extern bl" ++ prr new_bl ++ spc () ++ + str "Intern arity: " ++ pr intern_arity) + with _ -> () in let impl = if Impargs.is_implicit_args() @@ -286,8 +289,9 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in let rec declare i fi = - trace (str "Declaring: " ++ pr_id fi ++ spc () ++ - my_print_constr env0 (recvec.(i))); + (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++ + my_print_constr env0 (recvec.(i))); + with _ -> ()); let ce = { const_entry_body = mkFix ((nvrec',i),recdecls); const_entry_type = Some arrec.(i); @@ -332,10 +336,10 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed let rec collect_evars i acc = if i < recdefs then let (isevars, info, def) = defrec.(i) in - let _ = trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) 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 _ = trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) 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 @@ -358,10 +362,16 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed trace (str (string_of_id fi) ++ str " is defined");*) let evar_sum = if evars = [] then None - else + else ( + (try trace (str "Building evars sum for : "); + List.iter + (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env0 t)) + evars; + with _ -> ()); let sum = Subtac_utils.build_dependent_sum evars in - trace (str "Evars sum: " ++ my_print_constr env0 (pi1 sum)); - Some sum + (try trace (str "Evars sum: " ++ my_print_constr env0 (snd sum)); + with _ -> ()); + Some sum) in collect_evars (succ i) ((id, evars_def, evar_sum) :: acc) else acc @@ -371,32 +381,34 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed (* Solve evars then create the definitions *) let real_evars = filter_map (fun (id, kn, sum) -> - match sum with Some (sumg, sumtac, _) -> Some (id, kn, sumg, sumtac) | None -> None) + match sum with Some (sumtac, sumg) -> Some (id, kn, sumg, sumtac) | None -> None) defs in Subtac_utils.and_tac real_evars (fun f _ gr -> - let _ = trace (str "Got a proof of: " ++ pr_global gr) in + let _ = trace (str "Got a proof of: " ++ pr_global gr ++ + str "type: " ++ my_print_constr (Global.env ()) (Global.type_of_global gr)) in let constant = match gr with Libnames.ConstRef c -> c | _ -> assert(false) in try (*let value = Environ.constant_value (Global.env ()) constant in*) let pis = f (mkConst constant) in - trace (str "Accessors: " ++ - List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc) - pis (mt())); - trace (str "Applied existentials: " ++ - (List.fold_right - (fun (id, kn, sumg, pi) acc -> - let args = Subtac_utils.destruct_ex pi sumg in - my_print_constr env0 (mkApp (kn, Array.of_list args))) - pis (mt ()))); + (try (trace (str "Accessors: " ++ + List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc) + pis (mt())); + trace (str "Applied existentials: " ++ + (List.fold_right + (fun (id, kn, sumg, pi) acc -> + let args = Subtac_utils.destruct_ex pi sumg in + my_print_constr env0 (mkApp (kn, Array.of_list args))) + pis (mt ())))) + with _ -> ()); let rec aux pis acc = function (id, kn, sum) :: tl -> (match sum with None -> aux pis (kn :: acc) tl - | Some (sumg, _, _) -> + | Some (_, sumg) -> let (id, kn, sumg, pi), pis = List.hd pis, List.tl pis in let args = Subtac_utils.destruct_ex pi sumg in let args = diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 1d37900f1..d0240f5a5 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -116,25 +116,26 @@ 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 _ = trace (str "New env created:" ++ my_print_context env_binders) 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 _ = trace (str "Internalized specification: " ++ my_print_rawconstr 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 _ = trace (str "Interpreted type: " ++ my_print_constr env_binders coqt) 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 _ = trace (str "Internalized term: " ++ my_print_rawconstr 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 _ = trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++ + 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 _ = trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) 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 @@ -142,10 +143,11 @@ 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 _ = trace (str "After evar normalization: " ++ spc () ++ + 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 _ = trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) in + let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in evm, fullcoqc, fullctyp diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 823ff41af..7bfaa0c5c 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -43,7 +43,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct module Cases = Cases.Cases_F(Coercion) (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) - let allow_anonymous_refs = ref false + let allow_anonymous_refs = ref true let evd_comb0 f isevars = let (evd',x) = f !isevars in diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index 966aa80a9..59c858a6a 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -118,8 +118,8 @@ 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 - debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++ - print_args env args); + (try debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++ + print_args env args) with _ -> ()); evar let make_existential_expr loc env c = @@ -160,26 +160,27 @@ open Tactics open Tacticals let build_dependent_sum l = - let rec aux (acc, tac, typ) = function + let rec aux (tac, typ) = function (n, t) :: tl -> let t' = mkLambda (Name n, t, typ) in - trace (str ("treating " ^ string_of_id n) ++ - str "assert: " ++ my_print_constr (Global.env ()) t); + trace (spc () ++ str ("treating evar " ^ string_of_id n)); + (try trace (str " assert: " ++ my_print_constr (Global.env ()) t) + with _ -> ()); let tac' = - tclTHEN (assert_tac true (Name n) t) - (tclTHENLIST - [intros; - (tclTHENSEQ - [tclTRY (constructor_tac (Some 1) 1 - (Rawterm.ImplicitBindings [mkVar n])); - tac]); - ]) + tclTHENS (assert_tac true (Name n) t) + ([intros; + (tclTHENSEQ + [constructor_tac (Some 1) 1 + (Rawterm.ImplicitBindings [mkVar n]); + tac]); + ]) in - aux (mkApp (Lazy.force ex_ind, [| t; t'; |]), tac', t') tl - | [] -> acc, tac, typ + let newt = mkApp (Lazy.force ex_ind, [| t; t'; |]) in + aux (tac', newt) tl + | [] -> tac, typ in match l with - (_, hd) :: tl -> aux (hd, intros, hd) tl + (_, hd) :: tl -> aux (intros, hd) tl | [] -> raise (Invalid_argument "build_dependent_sum") open Proof_type @@ -218,7 +219,8 @@ let and_tac l hook = let and_proof_id, and_goal, and_tac, and_extract = match l with | [] -> raise (Invalid_argument "and_tac: empty list of goals") - | (hdid, x, hdg, hdt) :: tl -> aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl + | (hdid, x, hdg, hdt) :: tl -> + aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl in let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in Command.start_proof and_proofid goal_kind and_goal @@ -238,7 +240,13 @@ let destruct_ex ext ex = try (args.(0), args.(1)) with _ -> assert(false) in - (mk_ex_pi1 dom rng acc) :: aux rng (mk_ex_pi2 dom rng acc) + let pi1 = (mk_ex_pi1 dom rng acc) in + let rng_body = + match kind_of_term rng with + Lambda (_, _, t) -> subst1 pi1 t + | t -> rng + in + pi1 :: aux rng_body (mk_ex_pi2 dom rng acc) | _ -> [acc]) | _ -> [acc] in aux ex ext diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 5ef3af18e..a90f281ff 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -78,7 +78,7 @@ val mkProj1 : constr -> constr -> constr -> constr val mk_ex_pi1 : constr -> constr -> constr -> constr val mk_ex_pi1 : constr -> constr -> constr -> constr -val build_dependent_sum : (identifier * types) list -> constr * Proof_type.tactic * types +val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types val and_tac : (identifier * 'a * constr * Proof_type.tactic) list -> ((constr -> (identifier * 'a * constr * constr) list) -> Tacexpr.declaration_hook) -> unit -- cgit v1.2.3