diff options
-rw-r--r-- | contrib/fourier/fourierR.ml | 3 | ||||
-rw-r--r-- | contrib/ring/quote.ml | 7 | ||||
-rw-r--r-- | dev/top_printers.ml | 49 | ||||
-rw-r--r-- | interp/constrextern.ml | 32 | ||||
-rw-r--r-- | interp/constrextern.mli | 3 | ||||
-rw-r--r-- | lib/util.ml | 1 | ||||
-rw-r--r-- | parsing/g_constr.ml4 | 5 | ||||
-rw-r--r-- | parsing/g_ltac.ml4 | 6 | ||||
-rw-r--r-- | parsing/lexer.ml4 | 3 | ||||
-rw-r--r-- | parsing/pptactic.ml | 3 | ||||
-rw-r--r-- | parsing/q_coqast.ml4 | 12 | ||||
-rw-r--r-- | pretyping/clenv.ml | 51 | ||||
-rw-r--r-- | pretyping/evd.ml | 6 | ||||
-rw-r--r-- | pretyping/evd.mli | 1 | ||||
-rw-r--r-- | proofs/tacexpr.ml | 2 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 10 |
16 files changed, 131 insertions, 63 deletions
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index d415cf7d2..ef0ff426d 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -503,8 +503,7 @@ let rec fourier gl= let res=fourier_lineq (!lineq) in let tac=ref tclIDTAC in if res=[] - then (print_string "Tactic Fourier fails.\n"; - flush stdout) + then Util.error "fourier failed" (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 3c1645d47..3b13283e1 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -191,8 +191,11 @@ let decomp_term c = kind_of_term (strip_outer_cast c) ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive type [typ] *) -let coerce_meta_out id = int_of_string (string_of_id id) -let coerce_meta_in n = id_of_string (string_of_int n) +let coerce_meta_out id = + let s = string_of_id id in + int_of_string (String.sub s 1 (String.length s - 1)) +let coerce_meta_in n = + id_of_string ("M" ^ string_of_int n) let compute_lhs typ i nargsi = match kind_of_term typ with diff --git a/dev/top_printers.ml b/dev/top_printers.ml index c06738226..dfd813985 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -50,14 +50,16 @@ let ppsp sp = pp(pr_sp sp) let ppqualid qid = pp(pr_qualid qid) (* term printers *) +let rawdebug = ref false let ppconstr x = pp (Termops.print_constr x) -let ppconstrdb x = pp(Flags.with_option Constrextern.rawdebug Termops.print_constr x) +let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x) let ppterm = ppconstr let ppsconstr x = ppconstr (Declarations.force x) let ppconstr_univ x = Constrextern.with_universes ppconstr x let pprawconstr = (fun x -> pp(pr_lrawconstr x)) let pppattern = (fun x -> pp(pr_constr_pattern x)) let pptype = (fun x -> pp(pr_ltype x)) + let ppfconstr c = ppconstr (Closure.term_of_fconstr c) let ppbigint n = pp (Bigint.pr_bigint n);; @@ -413,3 +415,48 @@ let _ = (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr), ConstrArgType), Some "c")]] + +(* Setting printer of unbound global reference *) +open Names +open Nameops +open Libnames + +let encode_path loc prefix mpdir suffix id = + let dir = match mpdir with + | None -> [] + | Some (mp,dir) -> + (repr_dirpath (dirpath_of_string (string_of_mp mp))@ + repr_dirpath dir) in + Qualid (loc, make_qualid + (make_dirpath (List.rev (id_of_string prefix::dir@suffix))) id) + +let raw_string_of_ref loc = function + | ConstRef cst -> + let (mp,dir,id) = repr_con cst in + encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id) + | IndRef (kn,i) -> + let (mp,dir,id) = repr_kn kn in + encode_path loc "IND" (Some (mp,dir)) [id_of_label id] + (id_of_string ("_"^string_of_int i)) + | ConstructRef ((kn,i),j) -> + let (mp,dir,id) = repr_kn kn in + encode_path loc "CSTR" (Some (mp,dir)) + [id_of_label id;id_of_string ("_"^string_of_int i)] + (id_of_string ("_"^string_of_int j)) + | VarRef id -> + encode_path loc "SECVAR" None [] id + +let short_string_of_ref loc = function + | VarRef id -> Ident (loc,id) + | ConstRef cst -> Ident (loc,id_of_label (pi3 (repr_con cst))) + | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_kn kn))) + | IndRef (kn,i) -> + encode_path loc "IND" None [id_of_label (pi3 (repr_kn kn))] + (id_of_string ("_"^string_of_int i)) + | ConstructRef ((kn,i),j) -> + encode_path loc "CSTR" None + [id_of_label (pi3 (repr_kn kn));id_of_string ("_"^string_of_int i)] + (id_of_string ("_"^string_of_int j)) + +let _ = Constrextern.set_debug_global_reference_printer + (if !rawdebug then raw_string_of_ref else short_string_of_ref) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 1e3587c59..5047d1b98 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -108,35 +108,17 @@ let idopt_of_name = function let extern_evar loc n l = if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None) -let rawdebug = ref false - -let raw_string_of_ref = function - | ConstRef kn -> - "CONST("^(string_of_con kn)^")" - | IndRef (kn,i) -> - "IND("^(string_of_kn kn)^","^(string_of_int i)^")" - | ConstructRef ((kn,i),j) -> - "CONSTRUCT("^ - (string_of_kn kn)^","^(string_of_int i)^","^(string_of_int j)^")" - | VarRef id -> - "SECVAR("^(string_of_id id)^")" - -let short_string_of_ref = function - | VarRef id -> string_of_id id - | ConstRef cst -> string_of_label (pi3 (repr_con cst)) - | IndRef (kn,0) -> string_of_label (pi3 (repr_kn kn)) - | IndRef (kn,i) -> - "IND("^string_of_label (pi3 (repr_kn kn))^(string_of_int i)^")" - | ConstructRef ((kn,i),j) -> - "CONSTRUCT("^ - string_of_label (pi3 (repr_kn kn))^","^(string_of_int i)^","^(string_of_int j)^")" +let debug_global_reference_printer = + ref (fun _ -> failwith "Cannot print a global reference") + +let set_debug_global_reference_printer f = + debug_global_reference_printer := f let extern_reference loc vars r = try Qualid (loc,shortest_qualid_of_global vars r) with Not_found -> (* happens in debugger *) - let f = if !rawdebug then raw_string_of_ref else short_string_of_ref in - Ident (loc,id_of_string (f r)) + !debug_global_reference_printer loc r (************************************************************************) (* Equality up to location (useful for translator v8) *) @@ -922,7 +904,7 @@ let rec raw_of_pat env = function | Name id -> id | Anonymous -> anomaly "rawconstr_of_pattern: index to an anonymous variable" - with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)^"]") in + with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)) in RVar (loc,id) | PMeta None -> RHole (loc,Evd.InternalHole) | PMeta (Some n) -> RPatVar (loc,(false,n)) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 7ae2977f5..a56923fe5 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -56,7 +56,8 @@ val print_no_symbol : bool ref val print_projections : bool ref (* Debug printing options *) -val rawdebug : bool ref +val set_debug_global_reference_printer : + (loc -> global_reference -> reference) -> unit (* This governs printing of implicit arguments. If [with_implicits] is on and not [with_arguments] then implicit args are printed prefixed diff --git a/lib/util.ml b/lib/util.ml index b317c849c..ccd807a90 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -290,6 +290,7 @@ let check_ident s = | _ -> error (s^": an identifier should start with a letter") with | End_of_input -> error "The empty string is not an identifier" + | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence") | Invalid_argument _ -> error (s^": invalid utf8 sequence") (* Lists *) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 0e7c92a6c..f5ea021d4 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -142,10 +142,7 @@ GEXTEND Gram [ [ "_" -> (loc, Anonymous) ] ] ; global: - [ [ r = Prim.reference -> r - - (* This is used in quotations *) - | id = METAIDENT -> Ident (loc,id_of_string id) ] ] + [ [ r = Prim.reference -> r ] ] ; constr_pattern: [ [ c = constr -> c ] ] diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index c0fd07c17..c541b5a7e 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -95,6 +95,8 @@ GEXTEND Gram TacArg (TacExternal (loc,com,req,la)) | st = simple_tactic -> TacAtom (loc,st) | a = may_eval_arg -> TacArg(a) + | IDENT "constr"; ":"; id = METAIDENT -> + TacArg(MetaIdArg (loc,false,id)) | IDENT "constr"; ":"; c = Constr.constr -> TacArg(ConstrMayEval(ConstrTerm c)) | IDENT "ipattern"; ":"; ipat = simple_intropattern -> @@ -125,7 +127,7 @@ GEXTEND Gram | r = reference -> Reference r | c = Constr.constr -> ConstrMayEval (ConstrTerm c) (* Unambigous entries: tolerated w/o "ltac:" modifier *) - | id = METAIDENT -> MetaIdArg (loc,id) + | id = METAIDENT -> MetaIdArg (loc,true,id) | "()" -> TacVoid ] ] ; may_eval_arg: @@ -148,7 +150,7 @@ GEXTEND Gram | c = Constr.constr -> ConstrTerm c ] ] ; tactic_atom: - [ [ id = METAIDENT -> MetaIdArg (loc,id) + [ [ id = METAIDENT -> MetaIdArg (loc,true,id) | n = integer -> Integer n | "()" -> TacVoid ] ] ; diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 5d59a8489..b26f8c77e 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -383,7 +383,8 @@ let parse_after_dot bp c = let rec next_token = parser bp | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> comm_loc bp; push_char c; next_token s - | [< ''$'; len = ident_tail (store 0 '$') >] ep -> + | [< ''$'; ' ('a'..'z' | 'A'..'Z' | '_' as c); + len = ident_tail (store 0 c) >] ep -> comment_stop bp; (("METAIDENT", get_buff len), (bp,ep)) | [< ' ('.' | '?') as c; t = parse_after_dot bp c >] ep -> diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 55c6a4387..2a46388c3 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -957,7 +957,8 @@ let rec pr_tac inherited tac = and pr_tacarg = function | TacDynamic (loc,t) -> pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>")) - | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s)) + | MetaIdArg (loc,true,s) -> pr_with_comments loc (str ("$" ^ s)) + | MetaIdArg (loc,false,s) -> pr_with_comments loc (str ("constr: $" ^ s)) | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat | TacVoid -> str "()" | Reference r -> pr_ref r diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index e698a187c..6313a553e 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -470,19 +470,15 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function <:expr< Tacexpr.TacFun ($mlexpr_of_list mlexpr_of_ident_option idol$, $mlexpr_of_tactic body$) >> -(* - | Tacexpr.TacFunRec of $dloc$ * identifier * tactic_fun_ast -*) -(* - | Tacexpr.TacArg (Tacexpr.AstTacArg (Coqast.Nmeta $dloc$ id)) -> anti loc id -*) - | Tacexpr.TacArg (Tacexpr.MetaIdArg (_,id)) -> anti loc id + | Tacexpr.TacArg (Tacexpr.MetaIdArg (_,true,id)) -> anti loc id | Tacexpr.TacArg t -> <:expr< Tacexpr.TacArg $mlexpr_of_tactic_arg t$ >> | _ -> failwith "Quotation of tactic expressions: TODO" and mlexpr_of_tactic_arg = function - | Tacexpr.MetaIdArg (loc,id) -> anti loc id + | Tacexpr.MetaIdArg (loc,true,id) -> anti loc id + | Tacexpr.MetaIdArg (loc,false,id) -> + <:expr< Tacexpr.ConstrMayEval (Rawterm.ConstrTerm $anti loc id$) >> | Tacexpr.TacCall (loc,t,tl) -> <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>> | Tacexpr.Tacexp t -> diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index e5632515d..072d664fc 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -169,8 +169,10 @@ let mentions clenv mv0 = let rec menrec mv1 = mv0 = mv1 || let mlist = - try (fst (meta_fvalue clenv.evd mv1)).freemetas - with Anomaly _ | Not_found -> Metaset.empty in + try match meta_opt_fvalue clenv.evd mv1 with + | Some (b,_) -> b.freemetas + | None -> Metaset.empty + with Not_found -> Metaset.empty in meta_exists menrec mlist in menrec @@ -230,6 +232,7 @@ let dependent_metas clenv mvs conclmetas = let clenv_dependent hyps_only clenv = let mvs = collect_metas (clenv_value clenv) in + let mvs = undefined_metas clenv.evd in let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in let deps = dependent_metas clenv mvs ctyp_mvs in List.filter @@ -256,21 +259,47 @@ let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl = clenv_unify allow_K CUMUL ~flags:flags (meta_reducible_instance clenv.evd clenv.templtyp) (pf_concl gl) clenv -(* [clenv_pose_dependent_evars clenv] +(* [clenv_pose_metas_as_evars clenv dep_mvs] * For each dependent evar in the clause-env which does not have a value, * pose a value for it by constructing a fresh evar. We do this in * left-to-right order, so that every evar's type is always closed w.r.t. - * metas. *) + * metas. + + * Node added 14/4/08 [HH]: before this date, evars were collected in + clenv_dependent by collect_metas in the fold_constr order which is + (almost) the left-to-right order of dependencies in term. However, + due to K-redexes, collect_metas was sometimes missing some metas. + The call to collect_metas has been replaced by a call to + undefined_metas, but then the order was the one of definition of + the metas (numbers in increasing order) which is _not_ the + dependency order when a clenv_fchain occurs (because clenv_fchain + plugs a term with a list of consecutive metas in place of a - a priori - + arbitrary metavariable belonging to another sequence of consecutive metas: + e.g., clenv_fchain may plug (H ?1 ?2) at the position ?6 of + (nat_ind ?3 ?4 ?5 ?6), leading to a dependency order 3<4<5<1<2). + To ensure the dependency order, we check that the type of each meta + to pose is already meta-free, otherwise we postpone the transformation, + hoping that no cycle may happen. + + Another approach could have been to use decimal numbers for metas so that + in the example above, (H ?1 ?2) would have been renumbered (H ?6.1 ?6.2) + then making the numeric order match the dependency order. +*) let clenv_pose_metas_as_evars clenv dep_mvs = - List.fold_left - (fun clenv mv -> + let rec fold clenv = function + | [] -> clenv + | mv::mvs -> let ty = clenv_meta_type clenv mv in - let (evd,evar) = - new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,GoalEvar) ty in - clenv_assign mv evar {clenv with evd=evd}) - clenv - dep_mvs + (* Postpone the evar-ization if dependent on another meta *) + (* This assumes no cycle in the dependencies - is it correct ? *) + if occur_meta ty then fold clenv (mvs@[mv]) + else + let (evd,evar) = + new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,GoalEvar) ty in + let clenv = clenv_assign mv evar {clenv with evd=evd} in + fold clenv mvs in + fold clenv dep_mvs let evar_clenv_unique_resolver = clenv_unique_resolver diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 91b70e3b0..3adf749f0 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -507,6 +507,12 @@ let pr_sort_constraints (_,sm) = pr_sort_cstrs sm let meta_list evd = metamap_to_list evd.metas +let undefined_metas evd = + List.sort Pervasives.compare (map_succeed (function + | (n,Clval(_,_,typ)) -> failwith "" + | (n,Cltyp (_,typ)) -> n) + (meta_list evd)) + let metas_of evd = List.map (function | (n,Clval(_,_,typ)) -> (n,typ.rebus) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index ebda685bd..352d3021d 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -196,6 +196,7 @@ val meta_reassign : metavariable -> constr * instance_status -> evar_defs -> ev (* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *) val meta_merge : evar_defs -> evar_defs -> evar_defs +val undefined_metas : evar_defs -> metavariable list val metas_of : evar_defs -> metamap type metabinding = metavariable * constr * instance_status diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 7a90040e5..ca25c722c 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -241,7 +241,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast = and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg = | TacDynamic of loc * Dyn.t | TacVoid - | MetaIdArg of loc * string + | MetaIdArg of loc * bool * string | ConstrMayEval of ('constr,'cst) may_eval | IntroPattern of intro_pattern_expr | Reference of 'ref diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index aba96afb3..3367f89f1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -829,10 +829,12 @@ and intern_tacarg strict ist = function IntroPattern (intern_intro_pattern lf ist ipat) | Integer n -> Integer n | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c) - | MetaIdArg (loc,s) -> + | MetaIdArg (loc,istac,s) -> (* $id can occur in Grammar tactic... *) let id = id_of_string s in - if find_ltacvar id ist then Reference (ArgVar (adjust_loc loc,id)) + if find_ltacvar id ist then + if istac then Reference (ArgVar (adjust_loc loc,id)) + else ConstrMayEval (ConstrTerm (RVar (adjust_loc loc,id), None)) else error_syntactic_metavariables_not_allowed loc | TacCall (loc,f,l) -> TacCall (loc, @@ -1635,7 +1637,7 @@ and interp_tacarg ist gl = function | Integer n -> VInteger n | IntroPattern ipat -> VIntroPattern (interp_intro_pattern ist gl ipat) | ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c) - | MetaIdArg (loc,id) -> assert false + | MetaIdArg (loc,_,id) -> assert false | TacCall (loc,r,[]) -> interp_ltac_reference false true ist gl r | TacCall (loc,f,l) -> let fv = interp_ltac_reference true true ist gl f @@ -2464,7 +2466,7 @@ and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body) and subst_tacarg subst = function | Reference r -> Reference (subst_reference subst r) | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c) - | MetaIdArg (_loc,_) -> assert false + | MetaIdArg (_loc,_,_) -> assert false | TacCall (_loc,f,l) -> TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l) | TacExternal (_loc,com,req,la) -> |