aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile4
-rw-r--r--parsing/g_tactic.ml46
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/tacred.mli1
-rw-r--r--proofs/clenv.ml4
-rw-r--r--proofs/refiner.ml45
-rw-r--r--tactics/auto.ml2
-rw-r--r--toplevel/coqinit.ml9
-rw-r--r--toplevel/errors.ml2
-rw-r--r--toplevel/himsg.ml48
-rw-r--r--toplevel/himsg.mli3
-rw-r--r--toplevel/metasyntax.ml2
12 files changed, 78 insertions, 50 deletions
diff --git a/Makefile b/Makefile
index 72cc981fc..22f2217f0 100644
--- a/Makefile
+++ b/Makefile
@@ -180,7 +180,7 @@ states: states/barestate.coq
SYNTAXPP=syntax/PPCommand.v syntax/PPTactic.v syntax/PPCases.v
states/barestate.coq: $(SYNTAXPP) coqtop.byte
- ./coqtop.byte -q -batch -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq
+ ./coqtop.byte -q -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq
###########################################################################
# theories
@@ -382,7 +382,7 @@ toplevel/mltop.cmx: toplevel/mltop.ml4
$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $<
.v.vo:
- $(COQC) $(COQINCLUDES) $<
+ $(COQC) $(COQINCLUDES) -q $<
.el.elc:
echo "(setq load-path (cons \".\" load-path))" > $*.compile
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 0548788e6..586a1bd67 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -129,7 +129,6 @@ GEXTEND Gram
| IDENT "Unfold"; ul = ne_unfold_occ_list ->
<:ast< (Unfold ($LIST ul)) >>
| IDENT "Fold"; cl = comarg_list -> <:ast< (Fold ($LIST cl)) >>
- | IDENT "Change"; c = comarg -> <:ast< (Change $c) >>
| IDENT "Pattern"; pl = ne_pattern_list ->
<:ast< (Pattern ($LIST $pl)) >> ] ]
;
@@ -306,7 +305,10 @@ GEXTEND Gram
| IDENT "Idtac" -> <:ast< (Idtac) >>
| IDENT "Fail" -> <:ast< (Fail) >>
| "("; tcl = tactic_com_list; ")" -> tcl
- | r = red_tactic; cl = clausearg -> <:ast< (Reduce (REDEXP $r) $cl) >> ]
+ | r = red_tactic; cl = clausearg -> <:ast< (Reduce (REDEXP $r) $cl) >>
+ (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
+ | IDENT "Change"; c = comarg; cl = clausearg ->
+ <:ast< (Change $c $cl) >> ]
| [ id = identarg; l = comarg_list ->
match (isMeta (nvar_of_ast id), l) with
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 16ea6c589..ad33549ca 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -270,7 +270,6 @@ type red_expr =
| Lazy of Closure.flags
| Unfold of (int list * section_path) list
| Fold of constr list
- | Change of constr
| Pattern of (int list * constr * constr) list
let reduction_of_redexp = function
@@ -281,7 +280,6 @@ let reduction_of_redexp = function
| Lazy f -> clos_norm_flags f
| Unfold ubinds -> unfoldn ubinds
| Fold cl -> fold_commands cl
- | Change t -> (fun _ _ _ -> t)
| Pattern lp -> pattern_occs lp
(* Used in several tactics. *)
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index a1aec82cd..a555667e6 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -31,7 +31,6 @@ type red_expr =
| Lazy of Closure.flags
| Unfold of (int list * section_path) list
| Fold of constr list
- | Change of constr
| Pattern of (int list * constr * constr) list
val reduction_of_redexp : red_expr -> 'a reduction_function
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index c53c46233..edda6de8b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -874,6 +874,8 @@ let clenv_add_sign (id,sign) clenv =
hook = w_add_sign (id,sign) clenv.hook}
let clenv_type_of ce c =
+ Typing.type_of (w_env ce.hook) (w_Underlying ce.hook) c
+ (***
let metamap =
List.map
(function
@@ -881,8 +883,6 @@ let clenv_type_of ce c =
| (n,Cltyp typ) -> (n,typ.rebus))
(intmap_to_list ce.env)
in
- failwith "clenv_type_of: TODO"
- (***
(Pretyping.ise_resolve true (w_Underlying ce.hook) metamap
(gLOB(w_hyps ce.hook)) c).uj_type
***)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index aeccbc094..f2f587b13 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -11,6 +11,7 @@ open Evd
open Environ
open Reduction
open Instantiate
+open Type_errors
open Proof_trees
open Logic
@@ -317,6 +318,10 @@ let tclIDTAC gls =
[< 'sTR "tclIDTAC validation is applicable only to"; 'sPC;
'sTR "a one-proof list" >])
+let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" [< 'sTR s>]
+let (tclFAIL : tactic) =
+ fun _ -> errorlabstrm "Refiner.tclFAIL" [< 'sTR"Failtac always fails.">]
+
(* solve_subgoal n tac pf_sigma applies the tactic tac at the nth subgoal of
pf_sigma *)
@@ -483,12 +488,22 @@ let tclNOTSAMEGOAL (tac:tactic) (ptree : goal sigma) =
[< 'sTR"Tactic generated a subgoal identical to the original goal.">];
rslt
-(* ORELSE f1 f2 tries to apply f1 and if it fails, applies f2 *)
+(* ORELSE0 f1 f2 tries to apply f1 and if it fails, applies f2 *)
+let tclORELSE0 f1 f2 g =
+ try
+ f1 g
+ with UserError _ | TypeError _ | RefinerError _
+ | Stdpp.Exc_located(_,(UserError _ | TypeError _ | RefinerError _)) ->
+ f2 g
+
+(* ORELSE f1 f2 tries to apply f1 and if it fails or does not progress,
+ then applies f2 *)
let tclORELSE (f1:tactic) (f2:tactic) (g:goal sigma) =
try
(tclPROGRESS f1) g
- with UserError _ | Stdpp.Exc_located(_,UserError _) ->
+ with UserError _ | TypeError _ | RefinerError _
+ | Stdpp.Exc_located(_,(UserError _ | TypeError _ | RefinerError _)) ->
f2 g
(* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
@@ -510,36 +525,18 @@ let rec tclREPEAT = fun t g ->
(*Try the first tactic that does not fail in a list of tactics*)
-let rec tclFIRST = fun tacl g ->
- match tacl with
- | [] -> errorlabstrm "Refiner.tclFIRST" [< 'sTR"No applicable tactic.">]
- | t::rest -> (try t g with UserError _ -> tclFIRST rest g)
+let rec tclFIRST = function
+ | [] -> tclFAIL_s "No applicable tactic."
+ | t::rest -> tclORELSE0 t (tclFIRST rest)
(*Try the first thats solves the current goal*)
-let tclSOLVE=fun tacl gls ->
- let (sigr,gl)=unpackage gls in
- let rec solve=function
- | [] -> errorlabstrm "Refiner.tclSOLVE" [< 'sTR"Cannot solve the goal.">]
- | e::tail ->
- (try
- let (ngl,p)=apply_sig_tac sigr e gl in
- if ngl = [] then
- (repackage sigr ngl,p)
- else
- solve tail
- with UserError _ ->
- solve tail)
- in
- solve tacl
+let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
let tclTRY t = (tclORELSE t tclIDTAC)
let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
-let (tclFAIL:tactic) =
- fun _ -> errorlabstrm "Refiner.tclFAIL" [< 'sTR"Failtac always fails.">]
-
(* Iteration tactical *)
let tclDO n t =
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 46f2d340a..7e8d7678a 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -237,7 +237,7 @@ let make_resolve_hyp hname htyp =
[make_apply_entry (true, Options.is_verbose()) hname (mkVar hname, htyp)]
with
| Failure _ -> []
- | UserError _ -> anomaly "Papageno programme comme un blaireau"
+ | UserError _ -> anomaly "make_resolve_hyp"
let add_resolves clist dbnames =
List.iter
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 33ee012cf..5253f9fb7 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -30,12 +30,15 @@ let load_rcfile() =
Vernac.load_vernac false (!rcfile^"."^Coq_config.version)
else if file_readable_p !rcfile then
Vernac.load_vernac false !rcfile
- else mSGNL [< 'sTR ("No .coqrc or .coqrc."^Coq_config.version^
- " found. Skipping rcfile loading.") >]
+ else
+ if Options.is_verbose() then
+ mSGNL [< 'sTR ("No .coqrc or .coqrc."^Coq_config.version^
+ " found. Skipping rcfile loading.") >]
with e ->
(mSGNL [< 'sTR"Load of rcfile failed." >];
raise e)
- else mSGNL [< 'sTR"Skipping rcfile loading." >]
+ else
+ if Options.is_verbose() then mSGNL [< 'sTR"Skipping rcfile loading." >]
(* Puts dir in the path of ML and in the LoadPath *)
let add_include s =
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index ba1f36cd7..ad4f6f389 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -52,6 +52,8 @@ let rec explain_exn_default = function
| InductiveError e -> hOV 0 (Himsg.explain_inductive_error e)
+ | Logic.RefinerError e -> hOV 0 (Himsg.explain_refiner_error e)
+
| Stdpp.Exc_located (loc,exc) ->
hOV 0 [< if loc = Ast.dummy_loc then [<>]
else [< 'sTR"At location "; print_loc loc; 'sTR":"; 'fNL >];
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ff96d59a6..a7cc960ab 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -12,6 +12,7 @@ open Sign
open Environ
open Type_errors
open Reduction
+open Logic
open Pretty
open Printer
open Ast
@@ -285,24 +286,47 @@ let explain_type_error k ctx = function
| NeedsInversion (x,t) ->
explain_needs_inversion k ctx x t
-let explain_refiner_bad_type k ctx arg ty conclty =
+let explain_refiner_bad_type arg ty conclty =
[< 'sTR"refiner was given an argument"; 'bRK(1,1);
- gentermpr k ctx arg; 'sPC;
- 'sTR"of type"; 'bRK(1,1); gentermpr k ctx ty; 'sPC;
- 'sTR"instead of"; 'bRK(1,1); gentermpr k ctx conclty >]
+ prterm arg; 'sPC;
+ 'sTR"of type"; 'bRK(1,1); prterm ty; 'sPC;
+ 'sTR"instead of"; 'bRK(1,1); prterm conclty >]
-let explain_refiner_occur_meta k ctx t =
- [< 'sTR"cannot refine with term"; 'bRK(1,1); gentermpr k ctx t;
+let explain_refiner_occur_meta t =
+ [< 'sTR"cannot refine with term"; 'bRK(1,1); prterm t;
'sPC; 'sTR"because there are metavariables, and it is";
'sPC; 'sTR"neither an application nor a Case" >]
-let explain_refiner_cannot_applt k ctx t harg =
+let explain_refiner_cannot_applt t harg =
[< 'sTR"in refiner, a term of type "; 'bRK(1,1);
- gentermpr k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
- gentermpr k ctx harg >]
-
-let explain_refiner_error e =
- [< 'sTR "TODO: EXPLAIN REFINER ERROR" >]
+ prterm t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
+ prterm harg >]
+
+let explain_refiner_cannot_unify m n =
+ let pm = prterm m in
+ let pn = prterm n in
+ [< 'sTR"Impossible to unify"; 'bRK(1,1) ; pm; 'sPC ;
+ 'sTR"with"; 'bRK(1,1) ; pn >]
+
+let explain_refiner_cannot_generalize ty =
+ [< 'sTR "cannot find a generalisation of the goal with type : ";
+ prterm ty >]
+
+let explain_refiner_not_well_typed c =
+ [< 'sTR"The term " ; prterm c ; 'sTR" is not well-typed" >]
+
+let explain_refiner_bad_tactic_args s l =
+ [< 'sTR "Internal tactic "; 'sTR s; 'sTR " cannot be applied to ";
+ Tacmach.pr_tactic (s,l) >]
+
+let explain_refiner_error = function
+ | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
+ | OccurMeta t -> explain_refiner_occur_meta t
+ | CannotApply (t,harg) -> explain_refiner_cannot_applt t harg
+ | CannotUnify (m,n) -> explain_refiner_cannot_unify m n
+ | CannotGeneralize (_,ty) -> explain_refiner_cannot_generalize ty
+ | NotWellTyped c -> explain_refiner_not_well_typed c
+ | BadTacticArgs (s,l) -> explain_refiner_bad_tactic_args s l
let error_non_strictly_positive k lna c v =
let env = assumptions_for_print lna in
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index d12d7963e..7bf0ef9c8 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -7,6 +7,7 @@ open Names
open Inductive
open Sign
open Type_errors
+open Logic
(*i*)
(* This module provides functions to explain the type errors. *)
@@ -14,3 +15,5 @@ open Type_errors
val explain_type_error : path_kind -> context -> type_error -> std_ppcmds
val explain_inductive_error : inductive_error -> std_ppcmds
+
+val explain_refiner_error : refiner_error -> std_ppcmds
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e53dea4de..9781eb2e7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -72,7 +72,7 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
let (inGrammar, outGrammar) =
declare_object
("GRAMMAR",
- { load_function = (fun _ -> ());
+ { load_function = (fun (_, a) -> Egrammar.extend_grammar a);
open_function = (fun _ -> ());
cache_function = (fun (_, a) -> Egrammar.extend_grammar a);
specification_function = (fun x -> x)})
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 07:14:14 +0000