diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-18 21:39:03 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-18 21:39:03 +0200 |
commit | 23041481ff368b0b4cfc9a2493c9f465df90ea90 (patch) | |
tree | fa981847c7fe17b18d4453403d19df9e32b26a38 | |
parent | dbdff037af1a80d223be6e4d093417bae301c583 (diff) |
Fix debug printing with primitive projections.
Add a flag to indicate if we're in the toplevel or debuggger to not try
to retype terms in the wrong environment (and making find_rectype,
get_type_of untraceable). This fixes bug #3638 along with the previous
commit.
-rw-r--r-- | dev/base_include | 3 | ||||
-rw-r--r-- | dev/top_printers.ml | 2 | ||||
-rw-r--r-- | interp/constrextern.ml | 14 | ||||
-rw-r--r-- | interp/constrextern.mli | 2 | ||||
-rw-r--r-- | lib/flags.ml | 2 | ||||
-rw-r--r-- | lib/flags.mli | 2 | ||||
-rw-r--r-- | pretyping/detyping.ml | 17 | ||||
-rw-r--r-- | pretyping/retyping.ml | 5 | ||||
-rw-r--r-- | pretyping/unification.ml | 1 | ||||
-rw-r--r-- | printing/pptactic.ml | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/3638.v | 25 |
11 files changed, 51 insertions, 24 deletions
diff --git a/dev/base_include b/dev/base_include index 2699551a5..1d43e64df 100644 --- a/dev/base_include +++ b/dev/base_include @@ -210,7 +210,8 @@ let pf_e gl s = Constrintern.interp_constr (pf_env gl) (project gl) (parse_constr s);; (* Set usual printing since the global env is available from the tracer *) -let _ = Constrextern.in_debugger := false +let _ = Flags.in_debugger := false +let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 4fedbec8e..6bf294967 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -552,6 +552,6 @@ let short_string_of_ref loc _ = function (* Anticipate that printers can be used from ocamldebug and that pretty-printer should not make calls to the global env since ocamldebug runs in a different process and does not have the proper env at hand *) -let _ = Constrextern.in_debugger := true +let _ = Flags.in_debugger := true let _ = Constrextern.set_extern_reference (if !rawdebug then raw_string_of_ref else short_string_of_ref) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index b774da356..885b0e6b4 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -158,13 +158,11 @@ let get_extern_reference () = !my_extern_reference let extern_reference loc vars l = !my_extern_reference loc vars l -let in_debugger = ref false - (**********************************************************************) (* mapping patterns to cases_pattern_expr *) let add_patt_for_params ind l = - if !in_debugger then l else + if !Flags.in_debugger then l else Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l let drop_implicits_in_patt cst nb_expl args = @@ -275,7 +273,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = not explicit application. *) match pat with | PatCstr(loc,cstrsp,args,na) - when !in_debugger||Inductiveops.constructor_has_local_defs cstrsp -> + when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp -> let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, []) @@ -402,7 +400,7 @@ let rec extern_symbol_ind_pattern allscopes vars ind args = function let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = (* pboutill: There are letins in pat which is incompatible with notations and not explicit application. *) - if !in_debugger||Inductiveops.inductive_has_local_defs ind then + if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then let c = extern_reference Loc.ghost vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in CPatCstr (Loc.ghost, c, add_patt_for_params ind args, []) @@ -438,7 +436,7 @@ let occur_name na aty = | Anonymous -> false let is_projection nargs = function - | Some r when not !in_debugger && not !Flags.raw_print && !print_projections -> + | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections -> (try let n = Recordops.find_projection_nparams r + 1 in if n <= nargs then None @@ -731,7 +729,7 @@ let rec extern inctx scopes vars r = (na',Option.map (fun (loc,ind,nal) -> let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in let fullargs = - if !in_debugger then args else + if !Flags.in_debugger then args else Notation_ops.add_patterns_for_params ind args in extern_ind_pattern_in_scope scopes vars ind fullargs ) x))) tml in @@ -944,7 +942,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t = (* those goal/section/rel variables that occurs in the subterm under *) (* consideration; see namegen.ml for further details *) let avoid = if goal_concl_style then ids_of_context env else [] in - let r = Detyping.detype ~lax goal_concl_style avoid env sigma t in + let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in let vars = vars_of_env env in extern false (scopt,[]) vars r diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 023c5be22..804795480 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -59,8 +59,6 @@ val set_extern_reference : val get_extern_reference : unit -> (Loc.t -> Id.Set.t -> global_reference -> reference) -val in_debugger : bool ref - (** This governs printing of implicit arguments. If [with_implicits] is on and not [with_arguments] then implicit args are printed prefixed by "!"; if [with_implicits] and [with_arguments] are both on the diff --git a/lib/flags.ml b/lib/flags.ml index 0356863ab..a744ce9b0 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -73,6 +73,8 @@ let async_proofs_is_master () = !async_proofs_mode = APon && !async_proofs_worker_id = "master" let debug = ref false +let in_debugger = ref false +let in_toplevel = ref false let profile = false diff --git a/lib/flags.mli b/lib/flags.mli index f94d80ffc..e53de166d 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -34,6 +34,8 @@ val string_of_priority : priority -> string val priority_of_string : string -> priority val debug : bool ref +val in_debugger : bool ref +val in_toplevel : bool ref val profile : bool diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 823f5ef64..d691acb45 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -438,15 +438,14 @@ let rec detype flags avoid env sigma t = (Array.map_to_list (detype flags avoid env sigma) args) | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance u) | Proj (p,c) -> - (try - let ty = Retyping.get_type_of (snd env) sigma c in - let (ind, args) = Inductive.find_rectype (snd env) ty in - GApp (dl, GRef (dl, ConstRef p, None), - List.map (detype flags avoid env sigma) (args @ [c])) - with e when fst flags (* lax mode, used by debug printers only *) -> - GApp (dl, GRef (dl, ConstRef p, None), - [detype flags avoid env sigma c]) - | e -> raise e) + if fst flags || !Flags.in_debugger || !Flags.in_toplevel then + (* lax mode, used by debug printers only *) + GApp (dl, GRef (dl, ConstRef p, None), + [detype flags avoid env sigma c]) + else let ty = Retyping.get_type_of (snd env) sigma c in + let (ind, args) = Inductive.find_rectype (snd env) ty in + GApp (dl, GRef (dl, ConstRef p, None), + List.map (detype flags avoid env sigma) (args @ [c])) | Evar (evk,cl) -> let id,l = try Evd.evar_ident evk sigma, diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index c7bdabe93..8f1a16dce 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -126,8 +126,9 @@ let retype ?(polyprop=true) sigma = (subst_type env sigma (type_of env f) (Array.to_list args)) | Proj (p,c) -> let Inductiveops.IndType(pars,realargs) = - try Inductiveops.find_rectype env sigma (type_of env c) - with Not_found -> anomaly ~label:"type_of" (str "Bad recursive type") + let ty = type_of env c in + try Inductiveops.find_rectype env sigma ty + with Not_found -> retype_error BadRecursiveType in let (_,u), pars = dest_ind_family pars in substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u)) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 7b302229b..d03fd8521 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1325,6 +1325,7 @@ let make_pattern_test inf_flags env sigma0 (sigma,c) = with | PretypeError (_,_,CannotUnify (c1,c2,Some e)) -> raise (NotUnifiable (Some (c1,c2,e))) + (** MS: This is pretty bad, it catches Not_found for example *) | e when Errors.noncritical e -> raise (NotUnifiable None) in let merge_fun c1 c2 = match c1, c2 with diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 841eb6039..bd4e9d93e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -342,7 +342,7 @@ let pr_ltac_or_var pr = function | ArgVar (loc,id) -> pr_with_comments loc (pr_id id) let pr_ltac_constant kn = - if !Constrextern.in_debugger then pr_kn kn + if !Flags.in_debugger then pr_kn kn else try pr_qualid (Nametab.shortest_qualid_of_tactic kn) with Not_found -> (* local tactic not accessible anymore *) diff --git a/test-suite/bugs/closed/3638.v b/test-suite/bugs/closed/3638.v new file mode 100644 index 000000000..70144174d --- /dev/null +++ b/test-suite/bugs/closed/3638.v @@ -0,0 +1,25 @@ +(* File reduced by coq-bug-finder from original input, then from 7593 lines to 243 lines, then from 256 lines to 102 lines, then from 104 lines to 28 lines *) +(* coqc version trunk (September 2014) compiled on Sep 17 2014 0:22:30 with OCaml 4.01.0 + coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d34e1eed232c84590ddb80d70db9f7f7cf13584a) *) +Set Primitive Projections. +Set Implicit Arguments. +Record prod (A B : Type) := pair { fst : A ; snd : B }. +Notation "x * y" := (prod x y) : type_scope. +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. +Class UnitSubuniverse := { O : Type -> Type ; O_unit : forall T, T -> O T }. +Class ReflectiveSubuniverse := { rsubu_usubu : UnitSubuniverse ; O_rectnd : forall {P Q : Type} (f : P -> Q), O P -> Q }. +Global Existing Instance rsubu_usubu. +Context {subU : ReflectiveSubuniverse}. +Goal forall (A B : Type) (x : O A * O B) (x0 : B), + { g : _ & O_rectnd (fun z : A * B => (O_unit (fst z), O_unit (snd z))) + (O_rectnd (fun a : A => O_unit (a, x0)) (fst x)) = + g x0 }. + eexists. + Show Existentials. Set Printing Existential Instances. + match goal with + | [ |- context[?e] ] => is_evar e; let e' := fresh "e'" in set (e' := e) + end. + + +(* Toplevel input, characters 15-114: +Anomaly: Bad recursive type. Please report. *)
\ No newline at end of file |