summaryrefslogtreecommitdiff
path: root/plugins/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac')
-rw-r--r--plugins/subtac/eterm.ml30
-rw-r--r--plugins/subtac/eterm.mli2
-rw-r--r--plugins/subtac/g_subtac.ml419
-rw-r--r--plugins/subtac/subtac.ml38
-rw-r--r--plugins/subtac/subtac_cases.ml22
-rw-r--r--plugins/subtac/subtac_cases.mli2
-rw-r--r--plugins/subtac/subtac_classes.ml6
-rw-r--r--plugins/subtac/subtac_classes.mli2
-rw-r--r--plugins/subtac/subtac_coercion.ml25
-rw-r--r--plugins/subtac/subtac_command.ml55
-rw-r--r--plugins/subtac/subtac_command.mli6
-rw-r--r--plugins/subtac/subtac_obligations.ml77
-rw-r--r--plugins/subtac/subtac_obligations.mli7
-rw-r--r--plugins/subtac/subtac_pretyping.ml26
-rw-r--r--plugins/subtac/subtac_pretyping.mli2
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml36
-rw-r--r--plugins/subtac/subtac_utils.ml127
-rw-r--r--plugins/subtac/subtac_utils.mli80
18 files changed, 275 insertions, 287 deletions
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index 4b95df19..f1bdd640 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -141,16 +141,28 @@ let evar_dependencies evm ev =
if Intset.equal deps deps' then deps
else aux deps'
in aux (Intset.singleton ev)
-
-let sort_dependencies evl =
- List.stable_sort
- (fun (id, ev, deps) (id', ev', deps') ->
- if id = id' then 0
- else if Intset.mem id deps' then -1
- else if Intset.mem id' deps then 1
- else Pervasives.compare id id')
- evl
+let move_after (id, ev, deps as obl) l =
+ let rec aux restdeps = function
+ | (id', _, _) as obl' :: tl ->
+ let restdeps' = Intset.remove id' restdeps in
+ if Intset.is_empty restdeps' then
+ obl' :: obl :: tl
+ else obl' :: aux restdeps' tl
+ | [] -> [obl]
+ in aux (Intset.remove id deps) l
+
+let sort_dependencies evl =
+ let rec aux l found list =
+ match l with
+ | (id, ev, deps) as obl :: tl ->
+ let found' = Intset.union found (Intset.singleton id) in
+ if Intset.subset deps found' then
+ aux tl found' (obl :: list)
+ else aux (move_after obl tl) found list
+ | [] -> List.rev list
+ in aux evl Intset.empty []
+
let map_evar_body f = function
| Evar_empty -> Evar_empty
| Evar_defined c -> Evar_defined (f c)
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
index d727c19c..262889c8 100644
--- a/plugins/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: eterm.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
open Environ
open Tacmach
open Term
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 87fd0479..cd8708d5 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -14,7 +14,7 @@
Syntax for the subtac terms and types.
Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
-(* $Id$ *)
+(* $Id: g_subtac.ml4 13332 2010-07-26 22:12:43Z msozeau $ *)
open Flags
@@ -53,7 +53,7 @@ open Constr
let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
GEXTEND Gram
- GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder subtac_withtac;
+ GLOBAL: subtac_gallina_loc typeclass_constraint subtac_withtac;
subtac_gallina_loc:
[ [ g = Vernac.gallina -> loc, g
@@ -65,21 +65,12 @@ GEXTEND Gram
| -> None ] ]
;
- Constr.binder_let:
+ Constr.closed_binder:
[[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
[LocalRawAssum ([id], default_binder_kind, typ)]
] ];
- Constr.binder:
- [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" ->
- ([id],default_binder_kind, mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, c, p)]))
- | "("; id=Prim.name; ":"; c=Constr.lconstr; ")" ->
- ([id],default_binder_kind, c)
- | "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" ->
- (id::lid,default_binder_kind, c)
- ] ];
-
END
@@ -161,9 +152,11 @@ VERNAC COMMAND EXTEND Subtac_Set_Solver
(Tacinterp.glob_tactic t) ]
END
+open Pp
+
VERNAC COMMAND EXTEND Subtac_Show_Solver
| [ "Show" "Obligation" "Tactic" ] -> [
- Pp.msgnl (Pptactic.pr_glob_tactic (Global.env ()) (Subtac_obligations.default_tactic_expr ())) ]
+ msgnl (str"Program obligation tactic is " ++ Subtac_obligations.print_default_tactic ()) ]
END
VERNAC COMMAND EXTEND Subtac_Show_Obligations
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index c859c690..885f7fb6 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: subtac.ml 13344 2010-07-28 15:04:36Z msozeau $ *)
open Global
open Pp
@@ -76,7 +76,7 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
(Pfedit.get_all_proof_names ())
in
let evm, c, typ, imps =
- Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr t bl) None
+ Subtac_pretyping.subtac_process ~is_type:true env isevars id [] (Topconstr.prod_constr_expr t bl) None
in
let c = solve_tccs_in_type env id isevars evm c typ in
Lemmas.start_proof id kind c (fun loc gr ->
@@ -138,9 +138,6 @@ let subtac (loc, command) =
Dumpglob.dump_definition lid false "def";
(match expr with
| ProveBody (bl, t) ->
- if Lib.is_modtype () then
- errorlabstrm "Subtac_command.StartProof"
- (str "Proof editing mode not supported in module types");
start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t)
(fun _ _ -> ())
| DefineBody (bl, _, c, tycon) ->
@@ -218,33 +215,10 @@ let subtac (loc, command) =
++ x ++ spc () ++ str "and" ++ spc () ++ y
in msg_warning cmds
- | Cases.PatternMatchingError (env, exn) as e ->
- debug 2 (Himsg.explain_pattern_matching_error env exn);
- raise e
+ | Cases.PatternMatchingError (env, exn) as e -> raise e
- | Type_errors.TypeError (env, exn) as e ->
- debug 2 (Himsg.explain_type_error env exn);
- raise e
+ | Type_errors.TypeError (env, exn) as e -> raise e
- | Pretype_errors.PretypeError (env, exn) as e ->
- debug 2 (Himsg.explain_pretype_error env exn);
- raise e
+ | Pretype_errors.PretypeError (env, exn) as e -> raise e
- | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
- Stdpp.Exc_located (loc, e') as e) ->
- debug 2 (str "Parsing exception: ");
- (match e' with
- | Type_errors.TypeError (env, exn) ->
- debug 2 (Himsg.explain_type_error env exn);
- raise e
-
- | Pretype_errors.PretypeError (env, exn) ->
- debug 2 (Himsg.explain_pretype_error env exn);
- raise e
-
- | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e'');
- raise e)
-
- | e ->
- msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e);
- raise e
+ | e -> raise e
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 28cedc8a..f6f8695b 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: subtac_cases.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
open Cases
open Util
@@ -23,13 +23,11 @@ open Sign
open Reductionops
open Typeops
open Type_errors
-
open Rawterm
open Retyping
open Pretype_errors
open Evarutil
open Evarconv
-
open Subtac_utils
(************************************************************************)
@@ -125,7 +123,7 @@ type tomatch_stack = tomatch_status list
originating from a subterm in which case real args are not dependent;
it accounts for n+1 binders if dep or n binders if not dep
- [PrProd] types abstracted term ([Abstract]); it accounts for one binder
- - [PrCcl] types the right-hand-side
+ - [PrCcl] types the right-hand side
- Aliases [Alias] have no trace in [predicate_signature]
*)
@@ -1152,7 +1150,7 @@ let rec generalize_problem pb = function
tomatch = Abstract d :: tomatch;
pred = Option.map (generalize_predicate i d) pb'.pred }
-(* No more patterns: typing the right-hand-side of equations *)
+(* No more patterns: typing the right-hand side of equations *)
let build_leaf pb =
let rhs = extract_rhs pb in
let tycon = match pb.pred with
@@ -1514,11 +1512,11 @@ let eq_id avoid id =
let hid' = next_ident_away hid avoid in
hid'
-let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
-let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
+let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |])
+let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |])
let mk_JMeq typ x typ' y =
- mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
+ mkApp (delayed_force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (delayed_force Subtac_utils.jmeq_refl, [| typ; x |])
let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
@@ -1610,7 +1608,7 @@ let vars_of_ctx ctx =
| Some t' when kind_of_term t' = Rel 0 ->
prev,
(RApp (dummy_loc,
- (RRef (dummy_loc, Lazy.force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars
+ (RRef (dummy_loc, delayed_force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars
| _ ->
match na with
Anonymous -> raise (Invalid_argument "vars_of_ctx")
@@ -1651,7 +1649,7 @@ let build_ineqs prevpatterns pats liftsign =
lift_rel_context len ppat_sign @ sign,
len',
succ n, (* nth pattern *)
- mkApp (Lazy.force eq_ind,
+ mkApp (delayed_force eq_ind,
[| lift (len' + liftsign) curpat_ty;
liftn (len + liftsign) (succ lens) ppat_c ;
lift len' curpat_c |]) ::
@@ -1929,7 +1927,7 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
let typing_fun tycon env = typing_fun tycon env isevars in
- (* We build the matrix of patterns and right-hand-side *)
+ (* We build the matrix of patterns and right-hand side *)
let matx = matx_of_eqns env eqns in
(* We build the vector of terms to match consistently with the *)
diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli
index 823e9912..a4df1257 100644
--- a/plugins/subtac/subtac_cases.mli
+++ b/plugins/subtac/subtac_cases.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: subtac_cases.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Util
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index f0ff9ba3..b2bf9912 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: subtac_classes.ml 13328 2010-07-26 11:05:30Z herbelin $ i*)
open Pretyping
open Evd
@@ -30,11 +30,11 @@ open Util
module SPretyping = Subtac_pretyping.Pretyping
-let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
+let interp_constr_evars_gen evdref env ?(impls=[]) kind c =
SPretyping.understand_tcc_evars evdref env kind
(intern_gen (kind=IsType) ~impls ( !evdref) env c)
-let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
+let interp_casted_constr_evars evdref env ?(impls=[]) c typ =
interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
let interp_context_evars evdref env params =
diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli
index 1c6c473a..57c7aa5b 100644
--- a/plugins/subtac/subtac_classes.mli
+++ b/plugins/subtac/subtac_classes.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: subtac_classes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Names
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 3f2a5dba..17c7284c 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -6,7 +6,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: subtac_coercion.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
open Util
open Names
@@ -39,7 +39,7 @@ let rec disc_subset x =
(match kind_of_term c with
Ind i ->
let len = Array.length l in
- let sig_ = Lazy.force sig_ in
+ let sig_ = delayed_force sig_ in
if len = 2 && i = Term.destInd sig_.typ
then
let (a, b) = pair_of_array l in
@@ -53,7 +53,7 @@ and disc_exist env x =
| App (c, l) ->
(match kind_of_term c with
Construct c ->
- if c = Term.destConstruct (Lazy.force sig_).intro
+ if c = Term.destConstruct (delayed_force sig_).intro
then Some (l.(0), l.(1), l.(2), l.(3))
else None
| _ -> None)
@@ -66,7 +66,7 @@ module Coercion = struct
let disc_proj_exist env x =
match kind_of_term x with
| App (c, l) ->
- (if Term.eq_constr c (Lazy.force sig_).proj1
+ (if Term.eq_constr c (delayed_force sig_).proj1
&& Array.length l = 3
then disc_exist env l.(2)
else None)
@@ -100,7 +100,7 @@ module Coercion = struct
Some (u, p) ->
let f, ct = aux u in
(Some (fun x ->
- app_opt f (mkApp ((Lazy.force sig_).proj1,
+ app_opt f (mkApp ((delayed_force sig_).proj1,
[| u; p; x |]))),
ct)
| None -> (None, v)
@@ -146,9 +146,9 @@ module Coercion = struct
in
let args = List.rev (restargs @ mkRel 1 :: lift_args 1 tele) in
let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
- let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in
+ let eq = mkApp (delayed_force eq_ind, [| eqT; hdx; hdy |]) in
let evar = make_existential loc env isevars eq in
- let eq_app x = mkApp (Lazy.force eq_rect,
+ let eq_app x = mkApp (delayed_force eq_rect,
[| eqT; hdx; pred; x; hdy; evar|]) in
aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x))
else Some co
@@ -187,8 +187,8 @@ module Coercion = struct
(match kind_of_term c, kind_of_term c' with
Ind i, Ind i' -> (* Inductive types *)
let len = Array.length l in
- let existS = Lazy.force existS in
- let prod = Lazy.force prod in
+ let existS = delayed_force existS in
+ let prod = delayed_force prod in
(* Sigma types *)
if len = Array.length l' && len = 2 && i = i'
&& (i = Term.destInd existS.typ || i = Term.destInd prod.typ)
@@ -279,7 +279,7 @@ module Coercion = struct
Some (u, p) ->
let c = coerce_unify env u y in
let f x =
- app_opt c (mkApp ((Lazy.force sig_).proj1,
+ app_opt c (mkApp ((delayed_force sig_).proj1,
[| u; p; x |]))
in Some f
| None ->
@@ -292,7 +292,7 @@ module Coercion = struct
let evar = make_existential loc env isevars (mkApp (p, [| cx |]))
in
(mkApp
- ((Lazy.force sig_).intro,
+ ((delayed_force sig_).intro,
[| u; p; cx; evar |])))
| None ->
raise NoSubtacCoercion
@@ -496,8 +496,7 @@ module Coercion = struct
with NoCoercion ->
coerce_itf loc env' isevars None t t')
with NoSubtacCoercion ->
- let sigma = isevars in
- error_cannot_coerce env' sigma (t, t'))
+ error_cannot_coerce env' isevars (t, t'))
else isevars
with _ -> isevars
end
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index f2747225..e7dd7ef1 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -53,7 +53,7 @@ let evar_nf isevars c =
Evarutil.nf_evar !isevars c
let interp_gen kind isevars env
- ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
+ ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
let c' = SPretyping.understand_tcc_evars isevars env kind c' in
@@ -62,13 +62,13 @@ let interp_gen kind isevars env
let interp_constr isevars env c =
interp_gen (OfType None) isevars env c
-let interp_type_evars isevars env ?(impls=([],[])) c =
+let interp_type_evars isevars env ?(impls=[]) c =
interp_gen IsType isevars env ~impls c
-let interp_casted_constr isevars env ?(impls=([],[])) c typ =
+let interp_casted_constr isevars env ?(impls=[]) c typ =
interp_gen (OfType (Some typ)) isevars env ~impls c
-let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
+let interp_casted_constr_evars isevars env ?(impls=[]) c typ =
interp_gen (OfType (Some typ)) isevars env ~impls c
let interp_open_constr isevars env c =
@@ -237,14 +237,18 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let rel = interp_constr isevars env r in
let relty = type_of env !isevars rel in
let relargty =
- let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in
- match ctx, kind_of_term ar with
- | [(_, None, t); (_, None, u)], Sort (Prop Null)
- when Reductionops.is_conv env !isevars t u -> t
- | _, _ ->
- user_err_loc (constr_loc r,
- "Subtac_command.build_wellfounded",
- my_print_constr env rel ++ str " is not an homogeneous binary relation.")
+ let error () =
+ user_err_loc (constr_loc r,
+ "Subtac_command.build_wellfounded",
+ my_print_constr env rel ++ str " is not an homogeneous binary relation.")
+ in
+ try
+ let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in
+ match ctx, kind_of_term ar with
+ | [(_, None, t); (_, None, u)], Sort (Prop Null)
+ when Reductionops.is_conv env !isevars t u -> t
+ | _, _ -> error ()
+ with _ -> error ()
in
let measure = interp_casted_constr isevars binders_env measure relargty in
let wf_rel, wf_rel_fun, measure_fn =
@@ -252,14 +256,14 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
it_mkLambda_or_LetIn measure letbinders,
it_mkLambda_or_LetIn measure binders
in
- let comb = constr_of_global (Lazy.force measure_on_R_ref) in
+ let comb = constr_of_global (delayed_force measure_on_R_ref) in
let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
let wf_rel_fun x y =
mkApp (rel, [| subst1 x measure_body;
subst1 y measure_body |])
in wf_rel, wf_rel_fun, measure
in
- let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) in
+ let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in
let argid' = id_of_string (string_of_id argname ^ "'") in
let wfarg len = (Name argid', None,
mkSubset (Name argid') argtyp
@@ -267,7 +271,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
in
let intern_bl = wfarg 1 :: [arg] in
let _intern_env = push_rel_context intern_bl env in
- let proj = (Lazy.force sig_).Coqlib.proj1 in
+ let proj = (delayed_force sig_).Coqlib.proj1 in
let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
let projection = (* in wfarg :: arg :: before *)
mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
@@ -280,7 +284,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in
let curry_fun =
let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
- let arg = mkApp ((Lazy.force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
+ let arg = mkApp ((delayed_force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
let rcurry = mkApp (rel, [| measure; lift len measure |]) in
let lam = (Name (id_of_string "recproof"), None, rcurry) in
@@ -292,21 +296,20 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let lift_lets = Termops.lift_rel_context 1 letbinders in
let intern_body =
let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in
- let (r, l, impls, scopes) =
+ let (r, l, impls, scopes) =
Constrintern.compute_internalization_data env
Constrintern.Recursive full_arity impls
in
let newimpls = [(recname, (r, l, impls @
[Some (id_of_string "recproof", Impargs.Manual, (true, false))],
scopes @ [None]))] in
- let newimpls = Constrintern.set_internalization_env_params newimpls [] in
interp_casted_constr isevars ~impls:newimpls
(push_rel_context ctx env) body (lift 1 top_arity)
in
let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
let prop = mkLambda (Name argname, argtyp, top_arity_let) in
let def =
- mkApp (constr_of_global (Lazy.force fix_sub_ref),
+ mkApp (constr_of_global (delayed_force fix_sub_ref),
[| argtyp ; wf_rel ;
make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
prop ; intern_body_lam |])
@@ -429,7 +432,7 @@ let interp_recursive fixkind l boxed =
List.fold_left2 (fun env' id t ->
let sort = Retyping.get_type_of env !evdref t in
let fixprot =
- try mkApp (Lazy.force Subtac_utils.fix_proto, [|sort; t|])
+ try mkApp (delayed_force Subtac_utils.fix_proto, [|sort; t|])
with e -> t
in
(id,None,fixprot) :: env')
@@ -438,8 +441,8 @@ let interp_recursive fixkind l boxed =
let env_rec = push_named_context rec_sign env in
(* Get interpretation metadatas *)
- let impls = Constrintern.compute_full_internalization_env env
- Constrintern.Recursive [] fixnames fixtypes fiximps
+ let impls = Constrintern.compute_internalization_env env
+ Constrintern.Recursive fixnames fixtypes fiximps
in
let notations = List.flatten ntnl in
@@ -453,7 +456,7 @@ let interp_recursive fixkind l boxed =
let fixdefs = List.map out_def fixdefs in
(* Instantiate evars and check all are resolved *)
- let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in
+ let evd = Evarconv.consider_remaining_unif_problems env_rec !evdref in
let evd = Typeclasses.resolve_typeclasses
~onlyargs:true ~split:true ~fail:false env_rec evd
in
@@ -518,8 +521,8 @@ let build_recursive l b =
m ntn false)
| _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
- let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) ->
- ({Command.fix_name = id; Command.fix_binders = bl;
+ let fixl = List.map (fun (((_,id),(n,ro),bl,typ,def),ntn) ->
+ ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = n;
Command.fix_body = def; Command.fix_type = typ},ntn)) l
in interp_recursive (IsFixpoint g) fixl b
| _, _ ->
@@ -528,7 +531,7 @@ let build_recursive l b =
let build_corecursive l b =
let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
- ({Command.fix_name = id; Command.fix_binders = bl;
+ ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = None;
Command.fix_body = def; Command.fix_type = typ},ntn))
l in
interp_recursive IsCoFixpoint fixl b
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index 304aa139..0f24915e 100644
--- a/plugins/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
@@ -13,7 +13,7 @@ val interp_gen :
typing_constraint ->
evar_map ref ->
env ->
- ?impls:full_internalization_env ->
+ ?impls:internalization_env ->
?allow_patvar:bool ->
?ltacvars:ltac_sign ->
constr_expr -> constr
@@ -23,12 +23,12 @@ val interp_constr :
val interp_type_evars :
evar_map ref ->
env ->
- ?impls:full_internalization_env ->
+ ?impls:internalization_env ->
constr_expr -> constr
val interp_casted_constr_evars :
evar_map ref ->
env ->
- ?impls:full_internalization_env ->
+ ?impls:internalization_env ->
constr_expr -> types -> constr
val interp_open_constr :
evar_map ref -> env -> constr_expr -> constr
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 2836bc73..1424618f 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -21,8 +21,8 @@ let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
let pperror cmd = Util.errorlabstrm "Program" cmd
let error s = pperror (str s)
-let reduce =
- Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty
+let reduce c =
+ Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c
exception NoObligations of identifier option
@@ -61,16 +61,15 @@ type program_info = {
prg_implicits : (Topconstr.explicitation * (bool * bool * bool)) list;
prg_notations : notations ;
prg_kind : definition_kind;
+ prg_reduce : constr -> constr;
prg_hook : Tacexpr.declaration_hook;
}
let assumption_message id =
Flags.if_verbose message ((string_of_id id) ^ " is assumed")
-let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
-let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId [])
-
-let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
+let (set_default_tactic, get_default_tactic, print_default_tactic) =
+ Tactic_option.declare_tactic_option "Program tactic"
(* true = All transparent, false = Opaque if possible *)
let proofs_transparency = ref true
@@ -136,10 +135,9 @@ let map_first m =
let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
-let freeze () = !from_prg, !default_tactic_expr
-let unfreeze (v, t) = from_prg := v; set_default_tactic t
-let init () =
- from_prg := ProgMap.empty; set_default_tactic (Tacexpr.TacId [])
+let freeze () = !from_prg
+let unfreeze v = from_prg := v
+let init () = from_prg := ProgMap.empty
(** Beware: if this code is dynamically loaded via dynlink after the start
of Coq, then this [init] function will not be run by [Lib.init ()].
@@ -155,35 +153,16 @@ let _ =
let progmap_union = ProgMap.fold ProgMap.add
-let cache (_, (local, tac)) =
- set_default_tactic tac
-
-let load (_, (local, tac)) =
- if not local then set_default_tactic tac
-
-let subst (s, (local, tac)) =
- (local, Tacinterp.subst_tactic s tac)
-
let (input,output) =
declare_object
{ (default_object "Program state") with
- cache_function = cache;
- load_function = (fun _ -> load);
- open_function = (fun _ -> load);
- classify_function = (fun (local, tac) ->
+ classify_function = (fun () ->
if not (ProgMap.is_empty !from_prg) then
errorlabstrm "Program" (str "Unsolved obligations when closing module:" ++ spc () ++
prlist_with_sep spc (fun x -> Nameops.pr_id x)
(map_keys !from_prg));
- if local then Dispose else Substitute (local, tac));
- subst_function = subst}
+ Dispose) }
-let update_state local =
- Lib.add_anonymous_leaf (input (local, !default_tactic_expr))
-
-let set_default_tactic local t =
- set_default_tactic t; update_state local
-
open Evd
let progmap_remove prg =
@@ -270,7 +249,7 @@ let declare_mutual_definition l =
let subs, typ = (subst_body true x) in
let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in
let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in
- reduce term, reduce typ, x.prg_implicits) l)
+ x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
in
(* let fixdefs = List.map reduce_fix fixdefs in *)
let fixkind = Option.get first.prg_fixkind in
@@ -300,8 +279,8 @@ let declare_mutual_definition l =
List.iter progmap_remove l; kn
let declare_obligation prg obl body =
- let body = reduce body in
- let ty = reduce obl.obl_type in
+ let body = prg.prg_reduce body in
+ let ty = prg.prg_reduce obl.obl_type in
match obl.obl_status with
| Expand -> { obl with obl_body = Some body }
| Define opaque ->
@@ -321,9 +300,7 @@ let declare_obligation prg obl body =
print_message (Subtac_utils.definition_message obl.obl_name);
{ obl with obl_body = Some (mkConst constant) }
-let red = Reductionops.nf_betaiota Evd.empty
-
-let init_prog_info n b t deps fixkind notations obls impls kind hook =
+let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
let obls', b =
match b with
| None ->
@@ -337,13 +314,13 @@ let init_prog_info n b t deps fixkind notations obls impls kind hook =
Array.mapi
(fun i (n, t, l, o, d, tac) ->
{ obl_name = n ; obl_body = None;
- obl_location = l; obl_type = red t; obl_status = o;
+ obl_location = l; obl_type = reduce t; obl_status = o;
obl_deps = d; obl_tac = tac })
obls, b
in
- { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
+ { prg_name = n ; prg_body = b; prg_type = reduce t; prg_obligations = (obls', Array.length obls');
prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
- prg_implicits = impls; prg_kind = kind; prg_hook = hook; }
+ prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; prg_hook = hook; }
let get_prog name =
let prg_infos = !from_prg in
@@ -469,7 +446,7 @@ let rec solve_obligation prg num tac =
| _ -> ());
trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
- Pfedit.by !default_tactic;
+ Pfedit.by (snd (get_default_tactic ()));
Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac;
Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
| l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
@@ -501,7 +478,7 @@ and solve_obligation_by_tac prg obls i tac =
| None ->
match obl.obl_tac with
| Some t -> t
- | None -> !default_tactic
+ | None -> snd (get_default_tactic ())
in
let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
obls.(i) <- declare_obligation prg obl t;
@@ -579,9 +556,10 @@ let show_term n =
my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
++ my_print_constr (Global.env ()) prg.prg_body)
-let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun _ _ -> ()) obls =
+let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+ ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
- let prg = init_prog_info n term t [] None [] obls implicits kind hook in
+ let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
let obls,_ = prg.prg_obligations in
if Array.length obls = 0 then (
Flags.if_verbose ppnl (str ".");
@@ -596,12 +574,14 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?ta
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
| _ -> res)
-let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun _ _ -> ()) notations fixkind =
+let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
+ ?(hook=fun _ _ -> ()) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
let upd = List.fold_left
(fun acc (n, b, t, imps, obls) ->
- let prg = init_prog_info n (Some b) t deps (Some fixkind) notations obls imps kind hook in
- ProgMap.add n prg acc)
+ let prg = init_prog_info n (Some b) t deps (Some fixkind)
+ notations obls imps kind reduce hook
+ in ProgMap.add n prg acc)
!from_prg l
in
from_prg := upd;
@@ -647,6 +627,3 @@ let next_obligation n tac =
try array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls
with Not_found -> anomaly "Could not find a solvable obligation."
in solve_obligation prg i tac
-
-let default_tactic () = !default_tactic
-let default_tactic_expr () = !default_tactic_expr
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 1608c134..bc5fc3e1 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -3,6 +3,7 @@ open Util
open Libnames
open Evd
open Proof_type
+open Vernacexpr
type obligation_info =
(identifier * Term.types * loc *
@@ -16,8 +17,8 @@ type progress = (* Resolution status of a program *)
| Defined of global_reference (* Defined as id *)
val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit
-val default_tactic : unit -> Proof_type.tactic
-val default_tactic_expr : unit -> Tacexpr.glob_tactic_expr
+val get_default_tactic : unit -> locality_flag * Proof_type.tactic
+val print_default_tactic : unit -> Pp.std_ppcmds
val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
val get_proofs_transparency : unit -> bool
@@ -26,6 +27,7 @@ val add_definition : Names.identifier -> ?term:Term.constr -> Term.types ->
?implicits:(Topconstr.explicitation * (bool * bool * bool)) list ->
?kind:Decl_kinds.definition_kind ->
?tactic:Proof_type.tactic ->
+ ?reduce:(Term.constr -> Term.constr) ->
?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress
type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list
@@ -39,6 +41,7 @@ val add_mutual_definitions :
(Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
?tactic:Proof_type.tactic ->
?kind:Decl_kinds.definition_kind ->
+ ?reduce:(Term.constr -> Term.constr) ->
?hook:Tacexpr.declaration_hook ->
notations ->
fixpoint_kind -> unit
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 030bb3c5..23323ab3 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: subtac_pretyping.ml 13344 2010-07-28 15:04:36Z msozeau $ *)
open Global
open Pp
@@ -70,7 +70,7 @@ let merge_evms x y =
let interp env isevars c tycon =
let j = pretype tycon env isevars ([],[]) c in
let _ = isevars := Evarutil.nf_evar_map !isevars in
- let evd,_ = consider_remaining_unif_problems env !isevars in
+ let evd = consider_remaining_unif_problems env !isevars in
(* let unevd = undefined_evars evd in *)
let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in
let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:false env unevd' in
@@ -86,8 +86,10 @@ let find_with_index x l =
open Vernacexpr
-let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr ( evd) env
-let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type ( evd) env
+let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr =
+ Constrintern.intern_constr evd env
+let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr =
+ Constrintern.intern_type evd env
let env_with_binders env isevars l =
let rec aux ((env, rels) as acc) = function
@@ -109,21 +111,25 @@ let env_with_binders env isevars l =
| [] -> acc
in aux (env, []) l
-let subtac_process env isevars id bl c tycon =
+let subtac_process ?(is_type=false) env isevars id bl c tycon =
let c = Topconstr.abstract_constr_expr c bl in
- let tycon =
+ let tycon, imps =
match tycon with
- None -> empty_tycon
+ None -> empty_tycon, None
| Some t ->
let t = Topconstr.prod_constr_expr t bl in
let t = coqintern_type !isevars env t in
+ let imps = Implicit_quantifiers.implicits_of_rawterm t in
let coqt, ttyp = interp env isevars t empty_tycon in
- mk_tycon coqt
+ mk_tycon coqt, Some imps
in
let c = coqintern_constr !isevars env c in
- let imps = Implicit_quantifiers.implicits_of_rawterm c in
+ let imps = match imps with
+ | Some i -> i
+ | None -> Implicit_quantifiers.implicits_of_rawterm ~with_products:is_type c
+ in
let coqc, ctyp = interp env isevars c tycon in
- let evm = non_instanciated_map env isevars ( !isevars) in
+ let evm = non_instanciated_map env isevars !isevars in
let ty = nf_evar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
evm, coqc, ty, imps
diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli
index 055c6df2..48906b23 100644
--- a/plugins/subtac/subtac_pretyping.mli
+++ b/plugins/subtac/subtac_pretyping.mli
@@ -16,7 +16,7 @@ val interp :
Rawterm.rawconstr ->
Evarutil.type_constraint -> Term.constr * Term.constr
-val subtac_process : env -> evar_map ref -> identifier -> local_binder list ->
+val subtac_process : ?is_type:bool -> env -> evar_map ref -> identifier -> local_binder list ->
constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list
val subtac_proof : Decl_kinds.definition_kind -> Tacexpr.declaration_hook -> env -> evar_map ref -> identifier -> local_binder list ->
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 16f2031b..7fcd4267 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: subtac_pretyping_F.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
open Pp
open Util
@@ -166,6 +166,28 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RProp c -> judge_of_prop_contents c
| RType _ -> judge_of_new_Type ()
+ let split_tycon_lam loc env evd tycon =
+ let rec real_split evd c =
+ let t = whd_betadeltaiota env evd c in
+ match kind_of_term t with
+ | Prod (na,dom,rng) -> evd, (na, dom, rng)
+ | Evar ev when not (Evd.is_defined_evar evd ev) ->
+ let (evd',prod) = define_evar_as_product evd ev in
+ let (_,dom,rng) = destProd prod in
+ evd',(Anonymous, dom, rng)
+ | _ -> error_not_product_loc loc env evd c
+ in
+ match tycon with
+ | None -> evd,(Anonymous,None,None)
+ | Some (abs, c) ->
+ (match abs with
+ | None ->
+ let evd', (n, dom, rng) = real_split evd c in
+ evd', (n, mk_tycon dom, mk_tycon rng)
+ | Some (init, cur) ->
+ evd, (Anonymous, None, Some (Some (init, succ cur), c)))
+
+
(* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
(* in environment [env], with existential variables [( evdref)] and *)
(* the type constraint tycon *)
@@ -233,7 +255,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let newenv =
let marked_ftys =
Array.map (fun ty -> let sort = Retyping.get_type_of env !evdref ty in
- mkApp (Lazy.force Subtac_utils.fix_proto, [| sort; ty |]))
+ mkApp (delayed_force Subtac_utils.fix_proto, [| sort; ty |]))
ftys
in
push_rec_types (names,marked_ftys,[||]) env
@@ -355,7 +377,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
evd, Some ty')
evdref tycon
in
- let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon' in
+ let (name',dom,rng) = evd_comb1 (split_tycon_lam loc env) evdref tycon' in
let dom_valcon = valcon_of_tycon dom in
let j = pretype_type dom_valcon env evdref lvar c1 in
let var = (name,None,j.utj_val) in
@@ -586,11 +608,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(pretype tycon env evdref lvar c).uj_val
| IsType ->
(pretype_type empty_valcon env evdref lvar c).utj_val in
- evdref := fst (consider_remaining_unif_problems env !evdref);
+ evdref := consider_remaining_unif_problems env !evdref;
if resolve_classes then
- evdref :=
- Typeclasses.resolve_typeclasses ~onlyargs:false
+ (evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
~split:true ~fail:fail_evar env !evdref;
+ evdref := consider_remaining_unif_problems env !evdref);
let c = if expand_evar then nf_evar !evdref c' else c' in
if fail_evar then check_evars env Evd.empty !evdref c;
c
@@ -603,7 +625,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let understand_judgment sigma env c =
let evdref = ref (create_evar_defs sigma) in
let j = pretype empty_tycon env evdref ([],[]) c in
- let evd,_ = consider_remaining_unif_problems env !evdref in
+ let evd = consider_remaining_unif_problems env !evdref in
let j = j_nf_evar evd j in
check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
j
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 06a80f68..689b110f 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -1,3 +1,5 @@
+(** -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
+
open Evd
open Libnames
open Coqlib
@@ -18,14 +20,14 @@ let utils_module = "Utils"
let fixsub_module = subtac_dir @ [fix_sub_module]
let utils_module = subtac_dir @ [utils_module]
let tactics_module = subtac_dir @ ["Tactics"]
-let init_constant dir s = gen_constant contrib_name dir s
-let init_reference dir s = gen_reference contrib_name dir s
+let init_constant dir s () = gen_constant contrib_name dir s
+let init_reference dir s () = gen_reference contrib_name dir s
-let fixsub = lazy (init_constant fixsub_module "Fix_sub")
-let ex_pi1 = lazy (init_constant utils_module "ex_pi1")
-let ex_pi2 = lazy (init_constant utils_module "ex_pi2")
+let fixsub = init_constant fixsub_module "Fix_sub"
+let ex_pi1 = init_constant utils_module "ex_pi1"
+let ex_pi2 = init_constant utils_module "ex_pi2"
-let make_ref l s = lazy (init_reference l s)
+let make_ref l s = init_reference l s
let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
let acc_ref = make_ref ["Init";"Wf"] "Acc"
let acc_inv_ref = make_ref ["Init";"Wf"] "Acc_inv"
@@ -41,68 +43,67 @@ let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
let build_sig () =
- { proj1 = init_constant ["Init"; "Specif"] "proj1_sig";
- proj2 = init_constant ["Init"; "Specif"] "proj2_sig";
- elim = init_constant ["Init"; "Specif"] "sig_rec";
- intro = init_constant ["Init"; "Specif"] "exist";
- typ = init_constant ["Init"; "Specif"] "sig" }
+ { proj1 = init_constant ["Init"; "Specif"] "proj1_sig" ();
+ proj2 = init_constant ["Init"; "Specif"] "proj2_sig" ();
+ elim = init_constant ["Init"; "Specif"] "sig_rec" ();
+ intro = init_constant ["Init"; "Specif"] "exist" ();
+ typ = init_constant ["Init"; "Specif"] "sig" () }
-let sig_ = lazy (build_sig ())
+let sig_ = build_sig
-let fix_proto = lazy (init_constant tactics_module "fix_proto")
+let fix_proto = init_constant tactics_module "fix_proto"
let fix_proto_ref () =
match Nametab.global (make_ref "Program.Tactics.fix_proto") with
| ConstRef c -> c
| _ -> assert false
-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")
+let eq_ind = init_constant ["Init"; "Logic"] "eq"
+let eq_rec = init_constant ["Init"; "Logic"] "eq_rec"
+let eq_rect = init_constant ["Init"; "Logic"] "eq_rect"
+let eq_refl = init_constant ["Init"; "Logic"] "refl_equal"
+let eq_ind_ref = init_reference ["Init"; "Logic"] "eq"
+let refl_equal_ref = init_reference ["Init"; "Logic"] "refl_equal"
-let not_ref = lazy (init_constant ["Init"; "Logic"] "not")
+let not_ref = init_constant ["Init"; "Logic"] "not"
-let and_typ = lazy (Coqlib.build_coq_and ())
+let and_typ = Coqlib.build_coq_and
-let eqdep_ind = lazy (init_constant [ "Logic";"Eqdep"] "eq_dep")
-let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
-let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
-let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
+let eqdep_ind = init_constant [ "Logic";"Eqdep"] "eq_dep"
+let eqdep_rec = init_constant ["Logic";"Eqdep"] "eq_dep_rec"
+let eqdep_ind_ref = init_reference [ "Logic";"Eqdep"] "eq_dep"
+let eqdep_intro_ref = init_reference [ "Logic";"Eqdep"] "eq_dep_intro"
let jmeq_ind =
- lazy (check_required_library ["Coq";"Logic";"JMeq"];
- init_constant ["Logic";"JMeq"] "JMeq")
+ init_constant ["Logic";"JMeq"] "JMeq"
+
let jmeq_rec =
- lazy (check_required_library ["Coq";"Logic";"JMeq"];
- init_constant ["Logic";"JMeq"] "JMeq_rec")
+ init_constant ["Logic";"JMeq"] "JMeq_rec"
+
let jmeq_refl =
- lazy (check_required_library ["Coq";"Logic";"JMeq"];
- init_constant ["Logic";"JMeq"] "JMeq_refl")
+ init_constant ["Logic";"JMeq"] "JMeq_refl"
-let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
-let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
+let ex_ind = init_constant ["Init"; "Logic"] "ex"
+let ex_intro = init_reference ["Init"; "Logic"] "ex_intro"
-let proj1 = lazy (init_constant ["Init"; "Logic"] "proj1")
-let proj2 = lazy (init_constant ["Init"; "Logic"] "proj2")
+let proj1 = init_constant ["Init"; "Logic"] "proj1"
+let proj2 = init_constant ["Init"; "Logic"] "proj2"
-let boolind = lazy (init_constant ["Init"; "Datatypes"] "bool")
-let sumboolind = lazy (init_constant ["Init"; "Specif"] "sumbool")
-let natind = lazy (init_constant ["Init"; "Datatypes"] "nat")
-let intind = lazy (init_constant ["ZArith"; "binint"] "Z")
-let existSind = lazy (init_constant ["Init"; "Specif"] "sigS")
+let boolind = init_constant ["Init"; "Datatypes"] "bool"
+let sumboolind = init_constant ["Init"; "Specif"] "sumbool"
+let natind = init_constant ["Init"; "Datatypes"] "nat"
+let intind = init_constant ["ZArith"; "binint"] "Z"
+let existSind = init_constant ["Init"; "Specif"] "sigS"
-let existS = lazy (build_sigma_type ())
+let existS = build_sigma_type
-let prod = lazy (build_prod ())
+let prod = build_prod
(* orders *)
-let well_founded = lazy (init_constant ["Init"; "Wf"] "well_founded")
-let fix = lazy (init_constant ["Init"; "Wf"] "Fix")
-let acc = lazy (init_constant ["Init"; "Wf"] "Acc")
-let acc_inv = lazy (init_constant ["Init"; "Wf"] "Acc_inv")
+let well_founded = init_constant ["Init"; "Wf"] "well_founded"
+let fix = init_constant ["Init"; "Wf"] "Fix"
+let acc = init_constant ["Init"; "Wf"] "Acc"
+let acc_inv = init_constant ["Init"; "Wf"] "Acc_inv"
let extconstr = Constrextern.extern_constr true (Global.env ())
let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)
@@ -151,8 +152,8 @@ let wf_relations = Hashtbl.create 10
let std_relations () =
let add k v = Hashtbl.add wf_relations k v in
- add (init_constant ["Init"; "Peano"] "lt")
- (lazy (init_constant ["Arith"; "Wf_nat"] "lt_wf"))
+ add (init_constant ["Init"; "Peano"] "lt" ())
+ (init_constant ["Arith"; "Wf_nat"] "lt_wf")
let std_relations = Lazy.lazy_from_fun std_relations
@@ -226,7 +227,6 @@ let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixp
open Tactics
open Tacticals
-let id x = x
let filter_map f l =
let rec aux acc = function
hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
@@ -257,51 +257,51 @@ let build_dependent_sum l =
(fun typ ->
let tex = mkLambda (Name n, t, typ) in
conttype
- (mkApp (Lazy.force ex_ind, [| t; tex |])))
+ (mkApp (ex_ind (), [| t; tex |])))
in
aux (mkVar n :: names) conttac conttype tl
| (n, t) :: [] ->
(conttac intros, conttype t)
| [] -> raise (Invalid_argument "build_dependent_sum")
- in aux [] id id (List.rev l)
+ in aux [] identity identity (List.rev l)
open Proof_type
open Tacexpr
let mkProj1 a b c =
- mkApp (Lazy.force proj1, [| a; b; c |])
+ mkApp (delayed_force proj1, [| a; b; c |])
let mkProj2 a b c =
- mkApp (Lazy.force proj2, [| a; b; c |])
+ mkApp (delayed_force proj2, [| a; b; c |])
let mk_ex_pi1 a b c =
- mkApp (Lazy.force ex_pi1, [| a; b; c |])
+ mkApp (delayed_force ex_pi1, [| a; b; c |])
let mk_ex_pi2 a b c =
- mkApp (Lazy.force ex_pi2, [| a; b; c |])
+ mkApp (delayed_force ex_pi2, [| a; b; c |])
let mkSubset name typ prop =
- mkApp ((Lazy.force sig_).typ,
+ mkApp ((delayed_force sig_).typ,
[| typ; mkLambda (name, typ, prop) |])
-let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
-let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (Lazy.force jmeq_refl, [| typ; x |])
+let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |])
+let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |])
+let mk_JMeq typ x typ' y = mkApp (delayed_force jmeq_ind, [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (delayed_force jmeq_refl, [| typ; x |])
let unsafe_fold_right f = function
hd :: tl -> List.fold_right f tl hd
| [] -> raise (Invalid_argument "unsafe_fold_right")
let mk_conj l =
- let conj_typ = Lazy.force and_typ in
+ let conj_typ = delayed_force and_typ in
unsafe_fold_right
(fun c conj ->
mkApp (conj_typ, [| c ; conj |]))
l
let mk_not c =
- let notc = Lazy.force not_ref in
+ let notc = delayed_force not_ref in
mkApp (notc, [| c |])
let and_tac l hook =
@@ -336,7 +336,7 @@ let destruct_ex ext ex =
match kind_of_term c with
App (f, args) ->
(match kind_of_term f with
- Ind i when i = Term.destInd (Lazy.force ex_ind) && Array.length args = 2 ->
+ Ind i when i = Term.destInd (delayed_force ex_ind) && Array.length args = 2 ->
let (dom, rng) =
try (args.(0), args.(1))
with _ -> assert(false)
@@ -477,6 +477,7 @@ let pr_evar_map evd =
let contrib_tactics_path =
make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"])
+
let tactics_tac s =
lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s))
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index d0ad334d..f56c2932 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -17,53 +17,53 @@ val contrib_name : string
val subtac_dir : string list
val fix_sub_module : string
val fixsub_module : string list
-val init_constant : string list -> string -> constr
-val init_reference : string list -> string -> global_reference
-val fixsub : constr lazy_t
-val well_founded_ref : global_reference lazy_t
-val acc_ref : global_reference lazy_t
-val acc_inv_ref : global_reference lazy_t
-val fix_sub_ref : global_reference lazy_t
-val measure_on_R_ref : global_reference lazy_t
-val fix_measure_sub_ref : global_reference lazy_t
-val refl_ref : global_reference lazy_t
+val init_constant : string list -> string -> constr delayed
+val init_reference : string list -> string -> global_reference delayed
+val fixsub : constr delayed
+val well_founded_ref : global_reference delayed
+val acc_ref : global_reference delayed
+val acc_inv_ref : global_reference delayed
+val fix_sub_ref : global_reference delayed
+val measure_on_R_ref : global_reference delayed
+val fix_measure_sub_ref : global_reference delayed
+val refl_ref : global_reference delayed
val lt_ref : reference
val sig_ref : reference
val proj1_sig_ref : reference
val proj2_sig_ref : reference
val build_sig : unit -> coq_sigma_data
-val sig_ : coq_sigma_data lazy_t
+val sig_ : coq_sigma_data delayed
-val fix_proto : constr lazy_t
+val fix_proto : constr delayed
val fix_proto_ref : unit -> constant
-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 not_ref : constr lazy_t
-val and_typ : constr lazy_t
-
-val eqdep_ind : constr lazy_t
-val eqdep_rec : constr lazy_t
-
-val jmeq_ind : constr lazy_t
-val jmeq_rec : constr lazy_t
-val jmeq_refl : constr lazy_t
-
-val boolind : constr lazy_t
-val sumboolind : constr lazy_t
-val natind : constr lazy_t
-val intind : constr lazy_t
-val existSind : constr lazy_t
-val existS : coq_sigma_data lazy_t
-val prod : coq_sigma_data lazy_t
-
-val well_founded : constr lazy_t
-val fix : constr lazy_t
-val acc : constr lazy_t
-val acc_inv : constr lazy_t
+val eq_ind : constr delayed
+val eq_rec : constr delayed
+val eq_rect : constr delayed
+val eq_refl : constr delayed
+
+val not_ref : constr delayed
+val and_typ : constr delayed
+
+val eqdep_ind : constr delayed
+val eqdep_rec : constr delayed
+
+val jmeq_ind : constr delayed
+val jmeq_rec : constr delayed
+val jmeq_refl : constr delayed
+
+val boolind : constr delayed
+val sumboolind : constr delayed
+val natind : constr delayed
+val intind : constr delayed
+val existSind : constr delayed
+val existS : coq_sigma_data delayed
+val prod : coq_sigma_data delayed
+
+val well_founded : constr delayed
+val fix : constr delayed
+val acc : constr delayed
+val acc_inv : constr delayed
val extconstr : constr -> constr_expr
val extsort : sorts -> constr_expr
@@ -81,7 +81,7 @@ val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
val debug : int -> std_ppcmds -> unit
val debug_msg : int -> std_ppcmds -> std_ppcmds
val trace : std_ppcmds -> unit
-val wf_relations : (constr, constr lazy_t) Hashtbl.t
+val wf_relations : (constr, constr delayed) Hashtbl.t
type binders = local_binder list
val app_opt : ('a -> 'a) option -> 'a -> 'a
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 22:15:14 +0000