diff options
Diffstat (limited to 'plugins/subtac')
-rw-r--r-- | plugins/subtac/eterm.ml | 30 | ||||
-rw-r--r-- | plugins/subtac/eterm.mli | 2 | ||||
-rw-r--r-- | plugins/subtac/g_subtac.ml4 | 19 | ||||
-rw-r--r-- | plugins/subtac/subtac.ml | 38 | ||||
-rw-r--r-- | plugins/subtac/subtac_cases.ml | 22 | ||||
-rw-r--r-- | plugins/subtac/subtac_cases.mli | 2 | ||||
-rw-r--r-- | plugins/subtac/subtac_classes.ml | 6 | ||||
-rw-r--r-- | plugins/subtac/subtac_classes.mli | 2 | ||||
-rw-r--r-- | plugins/subtac/subtac_coercion.ml | 25 | ||||
-rw-r--r-- | plugins/subtac/subtac_command.ml | 55 | ||||
-rw-r--r-- | plugins/subtac/subtac_command.mli | 6 | ||||
-rw-r--r-- | plugins/subtac/subtac_obligations.ml | 77 | ||||
-rw-r--r-- | plugins/subtac/subtac_obligations.mli | 7 | ||||
-rw-r--r-- | plugins/subtac/subtac_pretyping.ml | 26 | ||||
-rw-r--r-- | plugins/subtac/subtac_pretyping.mli | 2 | ||||
-rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 36 | ||||
-rw-r--r-- | plugins/subtac/subtac_utils.ml | 127 | ||||
-rw-r--r-- | plugins/subtac/subtac_utils.mli | 80 |
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 |