diff options
49 files changed, 683 insertions, 2902 deletions
diff --git a/Makefile.build b/Makefile.build index 04c01973e..d63558c2b 100644 --- a/Makefile.build +++ b/Makefile.build @@ -451,7 +451,7 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \ ########################################################################### .PHONY: plugins omega micromega ring setoid_ring nsatz dp xml extraction -.PHONY: field fourier funind cc subtac rtauto btauto pluginsopt +.PHONY: field fourier funind cc rtauto btauto pluginsopt plugins: $(PLUGINSVO) omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA) @@ -466,7 +466,6 @@ field: $(FIELDVO) $(FIELDCMA) fourier: $(FOURIERVO) $(FOURIERCMA) funind: $(FUNINDCMA) $(FUNINDVO) cc: $(CCVO) $(CCCMA) -subtac: $(SUBTACCMA) rtauto: $(RTAUTOVO) $(RTAUTOCMA) btauto: $(BTAUTOVO) $(BTAUTOCMA) diff --git a/Makefile.common b/Makefile.common index 88f035ac4..5f32ee13f 100644 --- a/Makefile.common +++ b/Makefile.common @@ -81,7 +81,7 @@ SRCDIRS:=\ $(addprefix plugins/, \ omega romega micromega quote ring dp \ setoid_ring xml extraction fourier \ - cc funind firstorder field subtac \ + cc funind firstorder field \ rtauto nsatz syntax decl_mode btauto) # Order is relevent here because kernel and checker contain files @@ -184,7 +184,6 @@ EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma FUNINDCMA:=plugins/funind/recdef_plugin.cma FOCMA:=plugins/firstorder/ground_plugin.cma CCCMA:=plugins/cc/cc_plugin.cma -SUBTACCMA:=plugins/subtac/subtac_plugin.cma BTAUTOCMA:=plugins/btauto/btauto_plugin.cma RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cma @@ -199,13 +198,13 @@ DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \ $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \ - $(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) $(BTAUTOCMA) \ + $(CCCMA) $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \ $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) ifneq ($(HASNATDYNLINK),false) STATICPLUGINS:= INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \ - $(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) $(NATSYNTAXCMA) + $(XMLCMA) $(FUNINDCMA) $(NATSYNTAXCMA) INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) PLUGINS:=$(PLUGINSCMA) PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs) diff --git a/kernel/environ.ml b/kernel/environ.ml index c38d4186f..15babb2ab 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -100,6 +100,7 @@ let map_named_val f (ctxt,ctxtv) = let empty_named_context = empty_named_context let push_named = push_named +let push_named_context = List.fold_right push_named let push_named_context_val = push_named_context_val let val_of_named_context ctxt = diff --git a/kernel/environ.mli b/kernel/environ.mli index 42100e4eb..70369ae4c 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -81,6 +81,7 @@ val map_named_val : (constr -> constr) -> named_context_val -> named_context_val val push_named : named_declaration -> env -> env +val push_named_context : named_context -> env -> env val push_named_context_val : named_declaration -> named_context_val -> named_context_val diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a52903df0..9b66cacb1 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -80,7 +80,9 @@ GEXTEND Gram vernac_aux: (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) (* "." is still in the stream and discard_to_dot works correctly *) - [ [ g = gallina; "." -> g + [ [ IDENT "Program"; g = gallina; "." -> program_flag := true; g + | IDENT "Program"; g = gallina_ext; "." -> program_flag := true; g + | g = gallina; "." -> g | g = gallina_ext; "." -> g | c = command; "." -> c | c = syntax; "." -> c diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 449dcd20e..31814b141 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -361,12 +361,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp match fixpoint_exprl with | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in - let ce,imps = - Command.interp_definition bl None body (Some ret_type) - in - Command.declare_definition - fname (Decl_kinds.Global,Decl_kinds.Definition) - ce imps (fun _ _ -> ()) + Command.do_definition fname (Decl_kinds.Global,Decl_kinds.Definition) + bl None body (Some ret_type) (fun _ _ -> ()) | _ -> Command.do_fixpoint fixpoint_exprl diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index f6500f74d..bb59a5c9c 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -55,7 +55,7 @@ val jmeq_refl : unit -> Term.constr val new_save_named : bool -> unit val save : bool -> identifier -> Entries.definition_entry -> Decl_kinds.goal_kind -> - Tacexpr.declaration_hook -> unit + unit Tacexpr.declaration_hook -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and abort the proof @@ -63,7 +63,7 @@ val save : bool -> identifier -> Entries.definition_entry -> Decl_kinds.goal_k val get_proof_clean : bool -> Names.identifier * (Entries.definition_entry * Decl_kinds.goal_kind * - Tacexpr.declaration_hook) + unit Tacexpr.declaration_hook) diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml deleted file mode 100644 index 0bde8dca9..000000000 --- a/plugins/subtac/eterm.ml +++ /dev/null @@ -1,260 +0,0 @@ -(** - - Get types of existentials ; - - Flatten dependency tree (prefix order) ; - - Replace existentials by De Bruijn indices in term, applied to the right arguments ; - - Apply term prefixed by quantification on "existentials". -*) - -open Term -open Sign -open Names -open Evd -open List -open Pp -open Errors -open Util -open Subtac_utils -open Proof_type - -let trace s = - if !Flags.debug then (msgnl s; msgerr s) - else () - -let succfix (depth, fixrels) = - (succ depth, List.map succ fixrels) - -type oblinfo = - { ev_name: int * identifier; - ev_hyps: named_context; - ev_status: obligation_definition_status; - ev_chop: int option; - ev_src: hole_kind located; - ev_typ: types; - ev_tac: tactic option; - ev_deps: Intset.t } - -(* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *) -open Store.Field -let evar_tactic = Store.field () - -(** Substitute evar references in t using De Bruijn indices, - where n binders were passed through. *) - -let subst_evar_constr evs n idf t = - let seen = ref Intset.empty in - let transparent = ref Idset.empty in - let evar_info id = List.assoc id evs in - let rec substrec (depth, fixrels) c = match kind_of_term c with - | Evar (k, args) -> - let { ev_name = (id, idstr) ; - ev_hyps = hyps ; ev_chop = chop } = - try evar_info k - with Not_found -> - anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") - in - seen := Intset.add id !seen; - (* Evar arguments are created in inverse order, - and we must not apply to defined ones (i.e. LetIn's) - *) - let args = - let n = match chop with None -> 0 | Some c -> c in - let (l, r) = list_chop n (List.rev (Array.to_list args)) in - List.rev r - in - let args = - let rec aux hyps args acc = - match hyps, args with - ((_, None, _) :: tlh), (c :: tla) -> - aux tlh tla ((substrec (depth, fixrels) c) :: acc) - | ((_, Some _, _) :: tlh), (_ :: tla) -> - aux tlh tla acc - | [], [] -> acc - | _, _ -> acc (*failwith "subst_evars: invalid argument"*) - in aux hyps args [] - in - if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then - transparent := Idset.add idstr !transparent; - mkApp (idf idstr, Array.of_list args) - | Fix _ -> - map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c - | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c - in - let t' = substrec (0, []) t in - t', !seen, !transparent - - -(** Substitute variable references in t using De Bruijn indices, - where n binders were passed through. *) -let subst_vars acc n t = - let var_index id = Util.list_index id acc in - let rec substrec depth c = match kind_of_term c with - | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c) - | _ -> map_constr_with_binders succ substrec depth c - in - substrec 0 t - -(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ]) - to a product : forall H1 : t1, ..., forall Hn : tn, concl. - Changes evars and hypothesis references to variable references. -*) -let etype_of_evar evs hyps concl = - let rec aux acc n = function - (id, copt, t) :: tl -> - let t', s, trans = subst_evar_constr evs n mkVar t in - let t'' = subst_vars acc 0 t' in - let rest, s', trans' = aux (id :: acc) (succ n) tl in - let s' = Intset.union s s' in - let trans' = Idset.union trans trans' in - (match copt with - Some c -> - let c', s'', trans'' = subst_evar_constr evs n mkVar c in - let c' = subst_vars acc 0 c' in - mkNamedProd_or_LetIn (id, Some c', t'') rest, - Intset.union s'' s', - Idset.union trans'' trans' - | None -> - mkNamedProd_or_LetIn (id, None, t'') rest, s', trans') - | [] -> - let t', s, trans = subst_evar_constr evs n mkVar concl in - subst_vars acc 0 t', s, trans - in aux [] 0 (rev hyps) - - -open Tacticals - -let trunc_named_context n ctx = - let len = List.length ctx in - list_firstn (len - n) ctx - -let rec chop_product n t = - if n = 0 then Some t - else - match kind_of_term t with - | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None - | _ -> None - -let evars_of_evar_info evi = - Intset.union (Evarutil.evars_of_term evi.evar_concl) - (Intset.union - (match evi.evar_body with - | Evar_empty -> Intset.empty - | Evar_defined b -> Evarutil.evars_of_term b) - (Evarutil.evars_of_named_context (evar_filtered_context evi))) - -let evar_dependencies evm oev = - let one_step deps = - Intset.fold (fun ev s -> - let evi = Evd.find evm ev in - let deps' = evars_of_evar_info evi in - if Intset.mem oev deps' then - raise (Invalid_argument ("Ill-formed evar map: cycle detected for evar " ^ string_of_int oev)) - else Intset.union deps' s) - deps deps - in - let rec aux deps = - let deps' = one_step deps in - if Intset.equal deps deps' then deps - else aux deps' - in aux (Intset.singleton oev) - -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) - -open Environ - -let map_evar_info f evi = - { evi with evar_hyps = val_of_named_context (map_named_context f (named_context_of_val evi.evar_hyps)); - evar_concl = f evi.evar_concl; - evar_body = map_evar_body f evi.evar_body } - -let eterm_obligations env name isevars evm fs ?status t ty = - (* 'Serialize' the evars *) - let nc = Environ.named_context env in - let nc_len = Sign.named_context_length nc in - let evl = List.rev (to_list evm) in - let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in - let sevl = sort_dependencies evl in - let evl = List.map (fun (id, ev, _) -> id, ev) sevl in - let evn = - let i = ref (-1) in - List.rev_map (fun (id, ev) -> incr i; - (id, (!i, id_of_string - (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), - ev)) evl - in - let evts = - (* Remove existential variables in types and build the corresponding products *) - fold_right - (fun (id, (n, nstr), ev) l -> - let hyps = Evd.evar_filtered_context ev in - let hyps = trunc_named_context nc_len hyps in - let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in - let evtyp, hyps, chop = - match chop_product fs evtyp with - | Some t -> t, trunc_named_context fs hyps, fs - | None -> evtyp, hyps, 0 - in - let loc, k = evar_source id isevars in - let status = match k with QuestionMark o -> Some o | _ -> status in - let status, chop = match status with - | Some (Define true as stat) -> - if chop <> fs then Define false, None - else stat, Some chop - | Some s -> s, None - | None -> Define true, None - in - let tac = match evar_tactic.get ev.evar_extra with - | Some t -> - if Dyn.tag t = "tactic" then - Some (Tacinterp.interp - (Tacinterp.globTacticIn (Tacinterp.tactic_out t))) - else None - | None -> None - in - let info = { ev_name = (n, nstr); - ev_hyps = hyps; ev_status = status; ev_chop = chop; - ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac } - in (id, info) :: l) - evn [] - in - let t', _, transparent = (* Substitute evar refs in the term by variables *) - subst_evar_constr evts 0 mkVar t - in - let ty, _, _ = subst_evar_constr evts 0 mkVar ty in - let evars = - List.map (fun (ev, info) -> - let { ev_name = (_, name); ev_status = status; - ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info - in - let status = match status with - | Define true when Idset.mem name transparent -> Define false - | _ -> status - in name, typ, src, status, deps, tac) evts - in - let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in - let evmap f c = pi1 (subst_evar_constr evts 0 f c) in - Array.of_list (List.rev evars), (evnames, evmap), t', ty - -let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli deleted file mode 100644 index 4812fe0a6..000000000 --- a/plugins/subtac/eterm.mli +++ /dev/null @@ -1,34 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Environ -open Tacmach -open Term -open Evd -open Names -open Pp -open Util -open Tacinterp - -val mkMetas : int -> constr list - -val evar_dependencies : evar_map -> int -> Intset.t -val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * Intset.t) list - -(* env, id, evars, number of function prototypes to try to clear from - evars contexts, object and type *) -val eterm_obligations : env -> identifier -> evar_map -> evar_map -> int -> - ?status:obligation_definition_status -> constr -> types -> - (identifier * types * hole_kind located * obligation_definition_status * Intset.t * - tactic option) array - (* Existential key, obl. name, type as product, location of the original evar, associated tactic, - status and dependencies as indexes into the array *) - * ((existential_key * identifier) list * ((identifier -> constr) -> constr -> constr)) * constr * types - (* Translations from existential identifiers to obligation identifiers - and for terms with existentials to closed terms, given a - translation from obligation identifiers to constrs, new term, new type *) diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 deleted file mode 100644 index 27de89f67..000000000 --- a/plugins/subtac/g_subtac.ml4 +++ /dev/null @@ -1,210 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i camlp4deps: "parsing/grammar.cma" i*) - -(* - Syntax for the subtac terms and types. - Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) - - -open Flags -open Errors -open Pp -open Names -open Nameops -open Vernacentries -open Reduction -open Term -open Libnames -open Topconstr - -(* We define new entries for programs, with the use of this module - * Subtac. These entries are named Subtac.<foo> - *) - -module Gram = Pcoq.Gram -module Vernac = Pcoq.Vernac_ -module Tactic = Pcoq.Tactic - -module SubtacGram = -struct - let gec s = Gram.entry_create ("Subtac."^s) - (* types *) - let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.entry = gec "subtac_gallina_loc" - - let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "subtac_withtac" -end - -open Glob_term -open SubtacGram -open Util -open Tok -open Pcoq -open Prim -open Constr -let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) - -let enforce_locality arg = - let flag = !Vernacexpr.locality_flag in - match flag with - | None -> (* no locality flag set for now *) - Vernacexpr.locality_flag := arg - | Some _ -> (* a locality flag has been set, we cannot redefine it *) - begin match arg with - | None -> () - | Some _ -> error "A locality flag has already been set." - end - -GEXTEND Gram - GLOBAL: subtac_gallina_loc typeclass_constraint subtac_withtac; - - (* FIXME : Program should be handled at a higher level in rule hierarchy. *) - subtac_locality: - [ [ IDENT "Local" -> enforce_locality (Some (loc, true)) - | IDENT "Global" -> enforce_locality (Some (loc, false)) - | -> enforce_locality None ] ] - ; - - subtac_gallina_loc: - [ [ subtac_locality; g = Vernac.gallina -> loc, g - | subtac_locality; g = Vernac.gallina_ext -> loc, g ] ] - ; - - subtac_withtac: - [ [ "with"; t = Tactic.tactic -> Some t - | -> None ] ] - ; - - 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)] - ] ]; - - END - -type 'a gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) Genarg.abstract_argument_type - -let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype), - (globwit_subtac_gallina_loc : Genarg.glevel gallina_loc_argtype), - (rawwit_subtac_gallina_loc : Genarg.rlevel gallina_loc_argtype) = - Genarg.create_arg "subtac_gallina_loc" - -type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type - -let (wit_subtac_withtac : Genarg.tlevel withtac_argtype), - (globwit_subtac_withtac : Genarg.glevel withtac_argtype), - (rawwit_subtac_withtac : Genarg.rlevel withtac_argtype) = - Genarg.create_arg "subtac_withtac" - -VERNAC COMMAND EXTEND Subtac -[ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ] - END - -let try_catch_exn f e = - try f e - with exn -> errorlabstrm "Program" (Errors.print exn) - -let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e -let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e -let try_solve_obligation e = try_catch_exn Subtac_obligations.try_solve_obligation e -let try_solve_obligations e = try_catch_exn Subtac_obligations.try_solve_obligations e -let solve_all_obligations e = try_catch_exn Subtac_obligations.solve_all_obligations e -let admit_obligations e = try_catch_exn Subtac_obligations.admit_obligations e - -VERNAC COMMAND EXTEND Subtac_Obligations -| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) subtac_withtac(tac) ] -> - [ subtac_obligation (num, Some name, Some t) tac ] -| [ "Obligation" integer(num) "of" ident(name) subtac_withtac(tac) ] -> - [ subtac_obligation (num, Some name, None) tac ] -| [ "Obligation" integer(num) ":" lconstr(t) subtac_withtac(tac) ] -> - [ subtac_obligation (num, None, Some t) tac ] -| [ "Obligation" integer(num) subtac_withtac(tac) ] -> - [ subtac_obligation (num, None, None) tac ] -| [ "Next" "Obligation" "of" ident(name) subtac_withtac(tac) ] -> - [ next_obligation (Some name) tac ] -| [ "Next" "Obligation" subtac_withtac(tac) ] -> [ next_obligation None tac ] -END - -VERNAC COMMAND EXTEND Subtac_Solve_Obligation -| [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> - [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> - [ try_solve_obligation num None (Some (Tacinterp.interp t)) ] - END - -VERNAC COMMAND EXTEND Subtac_Solve_Obligations -| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> - [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" "using" tactic(t) ] -> - [ try_solve_obligations None (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" ] -> - [ try_solve_obligations None None ] - END - -VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations -| [ "Solve" "All" "Obligations" "using" tactic(t) ] -> - [ solve_all_obligations (Some (Tacinterp.interp t)) ] -| [ "Solve" "All" "Obligations" ] -> - [ solve_all_obligations None ] - END - -VERNAC COMMAND EXTEND Subtac_Admit_Obligations -| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] -| [ "Admit" "Obligations" ] -> [ admit_obligations None ] - END - -VERNAC COMMAND EXTEND Subtac_Set_Solver -| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - Subtac_obligations.set_default_tactic - (Vernacexpr.use_section_locality ()) - (Tacinterp.glob_tactic t) ] -END - -open Pp - -VERNAC COMMAND EXTEND Subtac_Show_Solver -| [ "Show" "Obligation" "Tactic" ] -> [ - msgnl (str"Program obligation tactic is " ++ Subtac_obligations.print_default_tactic ()) ] -END - -VERNAC COMMAND EXTEND Subtac_Show_Obligations -| [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ] -| [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ] -END - -VERNAC COMMAND EXTEND Subtac_Show_Preterm -| [ "Preterm" "of" ident(name) ] -> [ Subtac_obligations.show_term (Some name) ] -| [ "Preterm" ] -> [ Subtac_obligations.show_term None ] -END - -open Pp - -(* Declare a printer for the content of [Program] *) -let () = - let printer _ _ _ expr = Ppvernac.pr_vernac_body (snd expr) in - (* should not happen *) - let dummy _ _ _ expr = assert false in - Pptactic.declare_extra_genarg_pprule - (rawwit_subtac_gallina_loc, printer) - (globwit_subtac_gallina_loc, dummy) - (wit_subtac_gallina_loc, dummy) - -(* Declare a printer for the content of Program tactics *) -let () = - let printer _ _ _ = function - | None -> mt () - | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic (Global.env ()) tac - in - (* should not happen *) - let dummy _ _ _ expr = assert false in - Pptactic.declare_extra_genarg_pprule - (rawwit_subtac_withtac, printer) - (globwit_subtac_withtac, dummy) - (wit_subtac_withtac, dummy) diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml deleted file mode 100644 index ffcd40f94..000000000 --- a/plugins/subtac/subtac.ml +++ /dev/null @@ -1,229 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Compat -open Global -open Pp -open Errors -open Util -open Names -open Sign -open Evd -open Term -open Termops -open Namegen -open Reductionops -open Environ -open Type_errors -open Typeops -open Libnames -open Classops -open List -open Recordops -open Evarutil -open Pretype_errors -open Glob_term -open Evarconv -open Pattern -open Vernacexpr - -open Subtac_coercion -open Subtac_utils -open Coqlib -open Printer -open Subtac_errors -open Eterm - -let require_library dirpath = - let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in - Library.require_library [qualid] None - -open Pp -open Ppconstr -open Decl_kinds -open Tacinterp -open Tacexpr - -let solve_tccs_in_type env id isevars evm c typ = - if not (Evd.is_empty evm) then - let stmt_id = Nameops.add_suffix id "_stmt" in - let obls, _, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in - match Subtac_obligations.add_definition stmt_id ~term:c' typ obls with - | Subtac_obligations.Defined cst -> constant_value (Global.env()) - (match cst with ConstRef kn -> kn | _ -> assert false) - | _ -> - errorlabstrm "start_proof" - (str "The statement obligations could not be resolved automatically, " ++ spc () ++ - str "write a statement definition first.") - else - let _ = Typeops.infer_type env c in c - - -let start_proof_com env isevars sopt kind (bl,t) hook = - let id = match sopt with - | Some (loc,id) -> - (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then - user_err_loc (loc,"start_proof",pr_id id ++ str " already exists"); - id - | None -> - next_global_ident_away (id_of_string "Unnamed_thm") - (Pfedit.get_all_proof_names ()) - in - let evm, c, typ, imps = - 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 -> - Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps]; - hook loc gr) - -let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () - -let start_proof_and_print env isevars idopt k t hook = - start_proof_com env isevars idopt k t hook; - print_subgoals () - -let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n))) - -let assumption_message id = - Flags.if_verbose message ((string_of_id id) ^ " is assumed") - -let declare_assumptions env isevars idl is_coe k bl c nl = - if not (Pfedit.refining ()) then - let id = snd (List.hd idl) in - let evm, c, typ, imps = - Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr c bl) None - in - let c = solve_tccs_in_type env id isevars evm c typ in - List.iter (Command.declare_assumption is_coe k c imps false nl) idl - else - errorlabstrm "Command.Assumption" - (str "Cannot declare an assumption while in proof editing mode.") - -let dump_constraint ty ((loc, n), _, _) = - match n with - | Name id -> Dumpglob.dump_definition (loc, id) false ty - | Anonymous -> () - -let dump_variable lid = () - -let vernac_assumption env isevars kind l nl = - let global = fst kind = Global in - List.iter (fun (is_coe,(idl,c)) -> - if Dumpglob.dump () then - List.iter (fun lid -> - if global then Dumpglob.dump_definition lid (not global) "ax" - else dump_variable lid) idl; - declare_assumptions env isevars idl is_coe kind [] c nl) l - -let check_fresh (loc,id) = - if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then - user_err_loc (loc,"",pr_id id ++ str " already exists") - -let subtac (loc, command) = - check_required_library ["Coq";"Init";"Datatypes"]; - check_required_library ["Coq";"Init";"Specif"]; - let env = Global.env () in - let isevars = ref (create_evar_defs Evd.empty) in - try - match command with - | VernacDefinition (defkind, (_, id as lid), expr, hook) -> - check_fresh lid; - Dumpglob.dump_definition lid false "def"; - (match expr with - | ProveBody (bl, t) -> - start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) - (fun _ _ -> ()) - | DefineBody (bl, _, c, tycon) -> - ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon)) - - | VernacFixpoint l -> - List.iter (fun ((lid, _, _, _, _), _) -> - check_fresh lid; - Dumpglob.dump_definition lid false "fix") l; - let _ = trace (str "Building fixpoint") in - ignore(Subtac_command.build_recursive l) - - | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) -> - if guard <> None then - error "Do not support building theorems as a fixpoint."; - Dumpglob.dump_definition id false "prf"; - if not(Pfedit.refining ()) then - if lettop then - errorlabstrm "Subtac_command.StartProof" - (str "Let declarations can only be used in proof editing mode"); - if Lib.is_modtype () then - errorlabstrm "Subtac_command.StartProof" - (str "Proof editing mode not supported in module types"); - check_fresh id; - start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook - - | VernacAssumption (stre,nl,l) -> - vernac_assumption env isevars stre l nl - - | VernacInstance (abst, glob, sup, is, props, pri) -> - dump_constraint "inst" is; - if abst then - error "Declare Instance not supported here."; - ignore(Subtac_classes.new_instance ~global:glob sup is props pri) - - | VernacCoFixpoint l -> - if Dumpglob.dump () then - List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l; - ignore(Subtac_command.build_corecursive l) - - | _ -> user_err_loc (loc,"", str ("Invalid Program command")) - with - | Typing_error e -> - msg_warning (str "Type error in Program tactic:"); - let cmds = - (match e with - | NonFunctionalApp (loc, x, mux, e) -> - str "non functional application of term " ++ - e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux - | NonSigma (loc, t) -> - str "Term is not of Sigma type: " ++ t - | NonConvertible (loc, x, y) -> - str "Unconvertible terms:" ++ spc () ++ - x ++ spc () ++ str "and" ++ spc () ++ y - | IllSorted (loc, t) -> - str "Term is ill-sorted:" ++ spc () ++ t - ) - in msg_warning cmds - - | Subtyping_error e -> - msg_warning (str "(Program tactic) Subtyping error:"); - let cmds = - match e with - | UncoercibleInferType (loc, x, y) -> - str "Uncoercible terms:" ++ spc () - ++ x ++ spc () ++ str "and" ++ spc () ++ y - | UncoercibleInferTerm (loc, x, y, tx, ty) -> - str "Uncoercible terms:" ++ spc () - ++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x - ++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y - | UncoercibleRewrite (x, y) -> - str "Uncoercible terms:" ++ spc () - ++ x ++ spc () ++ str "and" ++ spc () ++ y - in msg_warning cmds - - | Cases.PatternMatchingError (env, exn) as e -> raise e - - | Type_errors.TypeError (env, exn) as e -> raise e - - | Pretype_errors.PretypeError (env, _, exn) as e -> raise e - - | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) | - Loc.Exc_located (loc, e') as e) -> raise e - - | e -> - (* msg_warning (str "Uncaught exception: " ++ Errors.print e); *) - raise e - -let subtac c = Program.with_program subtac c diff --git a/plugins/subtac/subtac.mli b/plugins/subtac/subtac.mli deleted file mode 100644 index 32d484091..000000000 --- a/plugins/subtac/subtac.mli +++ /dev/null @@ -1,2 +0,0 @@ -val require_library : string -> unit -val subtac : Pp.loc * Vernacexpr.vernac_expr -> unit diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml deleted file mode 100644 index 75d0f3429..000000000 --- a/plugins/subtac/subtac_classes.ml +++ /dev/null @@ -1,190 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pretyping -open Evd -open Environ -open Term -open Glob_term -open Topconstr -open Names -open Libnames -open Pp -open Vernacexpr -open Constrintern -open Subtac_command -open Typeclasses -open Typeclasses_errors -open Decl_kinds -open Entries -open Errors -open Util - -let interp_constr_evars_gen evdref env ?(impls=Constrintern.empty_internalization_env) kind c = - understand_tcc_evars evdref env kind - (intern_gen (kind=IsType) ~impls !evdref env c) - -let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internalization_env) c typ = - interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c - -let interp_context_evars evdref env params = - let impls_env, bl = Constrintern.interp_context_gen - (fun env t -> understand_tcc_evars evdref env IsType t) - (understand_judgment_tcc evdref) !evdref env params in bl - -let interp_type_evars_impls ~evdref ?(impls=empty_internalization_env) env c = - let c = intern_gen true ~impls !evdref env c in - let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in - understand_tcc_evars ~fail_evar:false evdref env IsType c, imps - -let type_ctx_instance evars env ctx inst subst = - let rec aux (subst, instctx) l = function - (na, b, t) :: ctx -> - let t' = substl subst t in - let c', l = - match b with - | None -> interp_casted_constr_evars evars env (List.hd l) t', List.tl l - | Some b -> substl subst b, l - in - evars := resolve_typeclasses ~onlyargs:true ~fail:true env !evars; - let d = na, Some c', t' in - aux (c' :: subst, d :: instctx) l ctx - | [] -> subst - in aux (subst, []) inst (List.rev ctx) - -let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri = - let env = Global.env() in - let evars = ref Evd.empty in - let tclass, _ = - match bk with - | Implicit -> - Implicit_quantifiers.implicit_application Idset.empty (* need no avoid *) - ~allow_partial:false (fun avoid (clname, (id, _, t)) -> - match clname with - | Some (cl, b) -> - let t = - if b then - let _k = class_info cl in - CHole (Pp.dummy_loc, Some Evd.InternalHole) - else CHole (Pp.dummy_loc, None) - in t, avoid - | None -> failwith ("new instance: under-applied typeclass")) - cl - | Explicit -> cl, Idset.empty - in - let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in - let k, cty, ctx', ctx, len, imps, subst = - let (env', ctx), imps = interp_context_evars evars env ctx in - let c', imps' = interp_type_evars_impls ~evdref:evars env' tclass in - let len = List.length ctx in - let imps = imps @ Impargs.lift_implicits len imps' in - let ctx', c = decompose_prod_assum c' in - let ctx'' = ctx' @ ctx in - let cl, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in - let _, args = - List.fold_right (fun (na, b, t) (args, args') -> - match b with - | None -> (List.tl args, List.hd args :: args') - | Some b -> (args, substl args' b :: args')) - (snd cl.cl_context) (args, []) - in - cl, c', ctx', ctx, len, imps, args - in - let id = - match snd instid with - | Name id -> - let sp = Lib.make_path id in - if Nametab.exists_cci sp then - errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists"); - id - | Anonymous -> - let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in - Namegen.next_global_ident_away i (Termops.ids_of_context env) - in - evars := Typeclasses.mark_resolvables (Evarutil.nf_evar_map !evars); - evars := resolve_typeclasses ~onlyargs:false ~fail:true env !evars; - let ctx = Evarutil.nf_rel_context_evar !evars ctx - and ctx' = Evarutil.nf_rel_context_evar !evars ctx' in - let env' = push_rel_context ctx env in - let sigma = !evars in - let subst = List.map (Evarutil.nf_evar sigma) subst in - let props = - match props with - | Some (CRecord (loc, _, fs)) -> - if List.length fs > List.length k.cl_props then - Classes.mismatched_props env' (List.map snd fs) k.cl_props; - Inl fs - | Some p -> Inr p - | None -> Inl [] - in - let subst = - match props with - | Inr term -> - let c = interp_casted_constr_evars evars env' term cty in - Inr c - | Inl props -> - let get_id = - function - | Ident id' -> id' - | _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled") - in - let props, rest = - List.fold_left - (fun (props, rest) (id,b,_) -> - if b = None then - try - let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in - let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in - let (loc, mid) = get_id loc_mid in - List.iter - (fun (n, _, x) -> - if n = Name mid then - Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x) - k.cl_projs; - c :: props, rest' - with Not_found -> - (CHole (Pp.dummy_loc, None) :: props), rest - else props, rest) - ([], props) k.cl_props - in - if rest <> [] then - unbound_method env' k.cl_impl (get_id (fst (List.hd rest))) - else - Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst) - in - evars := Evarutil.nf_evar_map !evars; - evars := Typeclasses.mark_resolvables !evars; - evars := resolve_typeclasses ~onlyargs:true ~fail:true env !evars; - let term, termtype = - match subst with - | Inl subst -> - let subst = List.fold_left2 - (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst') - [] subst (k.cl_props @ snd k.cl_context) - in - let app, ty_constr = instance_constructor k subst in - let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in - term, termtype - | Inr def -> - let termtype = it_mkProd_or_LetIn cty ctx in - let term = Termops.it_mkLambda_or_LetIn def ctx in - term, termtype - in - let termtype = Evarutil.nf_evar !evars termtype in - let term = Evarutil.nf_evar !evars term in - evars := undefined_evars !evars; - Evarutil.check_evars env Evd.empty !evars termtype; - let hook vis gr = - let cst = match gr with ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false gr ~enriching:false [imps]; - Typeclasses.declare_instance pri (not global) (ConstRef cst) - in - let evm = Subtac_utils.evars_of_term !evars Evd.empty term in - let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in - id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,Instance) ~hook obls diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli deleted file mode 100644 index 5b8636a12..000000000 --- a/plugins/subtac/subtac_classes.mli +++ /dev/null @@ -1,40 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i*) -open Names -open Decl_kinds -open Term -open Sign -open Evd -open Environ -open Nametab -open Mod_subst -open Topconstr -open Errors -open Util -open Typeclasses -open Implicit_quantifiers -open Classes -(*i*) - -val type_ctx_instance : Evd.evar_map ref -> - Environ.env -> - ('a * Term.constr option * Term.constr) list -> - Topconstr.constr_expr list -> - Term.constr list -> - Term.constr list - -val new_instance : - ?global:bool -> - local_binder list -> - typeclass_constraint -> - constr_expr option -> - ?generalize:bool -> - int option -> - identifier * Subtac_obligations.progress diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml deleted file mode 100644 index 33560995d..000000000 --- a/plugins/subtac/subtac_command.ml +++ /dev/null @@ -1,474 +0,0 @@ -open Closure -open RedFlags -open Declarations -open Entries -open Libobject -open Pattern -open Matching -open Pp -open Glob_term -open Sign -open Tacred -open Errors -open Util -open Names -open Nameops -open Libnames -open Nametab -open Pfedit -open Proof_type -open Refiner -open Tacmach -open Tactic_debug -open Topconstr -open Term -open Tacexpr -open Safe_typing -open Typing -open Hiddentac -open Genarg -open Decl_kinds -open Mod_subst -open Printer -open Inductiveops -open Syntax_def -open Environ -open Tactics -open Tacticals -open Tacinterp -open Vernacexpr -open Notation -open Evd -open Evarutil - -open Subtac_utils -open Pretyping -open Subtac_obligations - -(*********************************************************************) -(* Functions to parse and interpret constructions *) - -let evar_nf isevars c = - Evarutil.nf_evar !isevars c - -let interp_gen kind isevars env - ?(impls=Constrintern.empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) - c = - let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in - let c' = understand_tcc_evars isevars env kind c' in - evar_nf isevars c' - -let interp_constr isevars env c = - interp_gen (OfType None) isevars env c - -let interp_type_evars isevars env ?(impls=Constrintern.empty_internalization_env) c = - interp_gen IsType isevars env ~impls c - -let interp_casted_constr isevars env ?(impls=Constrintern.empty_internalization_env) c typ = - interp_gen (OfType (Some typ)) isevars env ~impls c - -let interp_casted_constr_evars isevars env ?(impls=Constrintern.empty_internalization_env) c typ = - interp_gen (OfType (Some typ)) isevars env ~impls c - -let interp_open_constr isevars env c = - msgnl (str "Pretyping " ++ my_print_constr_expr c); - let c = Constrintern.intern_constr ( !isevars) env c in - let c' = understand_tcc_evars isevars env (OfType None) c in - evar_nf isevars c' - -let interp_constr_judgment isevars env c = - let j = - understand_judgment_tcc isevars env - (Constrintern.intern_constr ( !isevars) env c) - in - { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type } - -let locate_if_isevar loc na = function - | GHole _ -> - (try match na with - | Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id) - | Anonymous -> raise Not_found - with Not_found -> GHole (loc, Evd.BinderType na)) - | x -> x - -let interp_binder sigma env na t = - let t = Constrintern.intern_gen true ( !sigma) env t in - understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_glob_constr t) na t) - -let interp_context_evars evdref env params = - let int_env, bl = Constrintern.intern_context false !evdref env Constrintern.empty_internalization_env params in - let (env, par, _, impls) = - List.fold_left - (fun (env,params,n,impls) (na, k, b, t) -> - match b with - None -> - let t' = locate_if_isevar (loc_of_glob_constr t) na t in - let t = understand_tcc_evars evdref env IsType t' in - let d = (na,None,t) in - let impls = - if k = Implicit then - let na = match na with Name n -> Some n | Anonymous -> None in - (ExplByPos (n, na), (true, true, true)) :: impls - else impls - in - (push_rel d env, d::params, succ n, impls) - | Some b -> - let c = understand_judgment_tcc evdref env b in - let d = (na, Some c.uj_val, c.uj_type) in - (push_rel d env,d::params, succ n, impls)) - (env,[],1,[]) (List.rev bl) - in (env, par), impls - - -open Coqlib - -let sigT = Lazy.lazy_from_fun build_sigma_type - -let rec telescope = function - | [] -> assert false - | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1 - | (n, None, t) :: tl -> - let ty, tys, (k, constr) = - List.fold_left - (fun (ty, tys, (k, constr)) (n, b, t) -> - let pred = mkLambda (n, t, ty) in - let sigty = mkApp ((Lazy.force sigT).typ, [|t; pred|]) in - let intro = mkApp ((Lazy.force sigT).intro, [|lift k t; lift k pred; mkRel k; constr|]) in - (sigty, pred :: tys, (succ k, intro))) - (t, [], (2, mkRel 1)) tl - in - let (last, subst) = List.fold_right2 - (fun pred (n, b, t) (prev, subst) -> - let proj1 = applistc (Lazy.force sigT).proj1 [t; pred; prev] in - let proj2 = applistc (Lazy.force sigT).proj2 [t; pred; prev] in - (lift 1 proj2, (n, Some proj1, t) :: subst)) - (List.rev tys) tl (mkRel 1, []) - in ty, ((n, Some last, t) :: subst), constr - - | (n, Some b, t) :: tl -> let ty, subst, term = telescope tl in - ty, ((n, Some b, t) :: subst), lift 1 term - -let nf_evar_context isevars ctx = - List.map (fun (n, b, t) -> - (n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx - -let build_wellfounded (recname,n,bl,arityc,body) r measure notation = - Coqlib.check_required_library ["Coq";"Program";"Wf"]; - let sigma = Evd.empty in - let isevars = ref (Evd.create_evar_defs sigma) in - let env = Global.env() in - let _pr c = my_print_constr env c in - let _prr = Printer.pr_rel_context env in - let _prn = Printer.pr_named_context env in - let _pr_rel env = Printer.pr_rel_context env in - let (env', binders_rel), impls = interp_context_evars isevars env bl in - let len = List.length binders_rel in - let top_env = push_rel_context binders_rel env in - let top_arity = interp_type_evars isevars top_env arityc in - let full_arity = it_mkProd_or_LetIn top_arity binders_rel in - let argtyp, letbinders, make = telescope binders_rel in - let argname = id_of_string "recarg" in - let arg = (Name argname, None, argtyp) in - let binders = letbinders @ [arg] in - let binders_env = push_rel_context binders_rel env in - let rel = interp_constr isevars env r in - let relty = type_of env !isevars rel in - let relargty = - 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 = - let measure_body, measure = - it_mkLambda_or_LetIn measure letbinders, - it_mkLambda_or_LetIn measure binders - 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 (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 - (wf_rel_fun (mkRel 1) (mkRel (len + 1)))) - in - let intern_bl = wfarg 1 :: [arg] in - let _intern_env = push_rel_context intern_bl env 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 |]) - in - let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in - let intern_arity = substl [projection] top_arity_let in - (* substitute the projection of wfarg for something, - now intern_arity is in wfarg :: arg *) - let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in - 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 ((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 - let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in - let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in - (Name recname, Some body, ty) - in - let fun_bl = intern_fun_binder :: [arg] in - 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) = - Constrintern.compute_internalization_data env - Constrintern.Recursive full_arity impls - in - let newimpls = Idmap.singleton recname - (r, l, impls @ [(Some (id_of_string "recproof", Impargs.Manual, (true, false)))], - scopes @ [None]) 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 (delayed_force fix_sub_ref), - [| argtyp ; wf_rel ; - make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ; - prop ; intern_body_lam |]) - in - let _ = isevars := Evarutil.nf_evar_map !isevars in - let binders_rel = nf_evar_context !isevars binders_rel in - let binders = nf_evar_context !isevars binders in - let top_arity = Evarutil.nf_evar !isevars top_arity in - let hook, recname, typ = - if List.length binders_rel > 1 then - let name = add_suffix recname "_func" in - let hook l gr = - let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in - let ty = it_mkProd_or_LetIn top_arity binders_rel in - let ce = - { const_entry_body = Evarutil.nf_evar !isevars body; - const_entry_secctx = None; - const_entry_type = Some ty; - const_entry_opaque = false } - in - let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in - let gr = ConstRef c in - if Impargs.is_implicit_args () || impls <> [] then - Impargs.declare_manual_implicits false gr [impls] - in - let typ = it_mkProd_or_LetIn top_arity binders in - hook, name, typ - else - let typ = it_mkProd_or_LetIn top_arity binders_rel in - let hook l gr = - if Impargs.is_implicit_args () || impls <> [] then - Impargs.declare_manual_implicits false gr [impls] - in hook, recname, typ - in - let fullcoqc = Evarutil.nf_evar !isevars def in - let fullctyp = Evarutil.nf_evar !isevars typ in - let evm = evars_of_term !isevars Evd.empty fullctyp in - let evm = evars_of_term !isevars evm fullcoqc in - let evm = non_instanciated_map env isevars evm in - let evars, _, evars_def, evars_typ = - Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp - in - Subtac_obligations.add_definition recname ~term:evars_def evars_typ evars ~hook - -let interp_fix_context evdref env fix = - interp_context_evars evdref env fix.Command.fix_binders - -let interp_fix_ccl evdref (env,_) fix = - interp_type_evars evdref env fix.Command.fix_type - -let interp_fix_body evdref env_rec impls (_,ctx) fix ccl = - let env = push_rel_context ctx env_rec in - let body = Option.map (fun c -> interp_casted_constr_evars evdref env ~impls c ccl) fix.Command.fix_body in - Option.map (fun c -> it_mkLambda_or_LetIn c ctx) body - -let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx - -let prepare_recursive_declaration fixnames fixtypes fixdefs = - let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in - let names = List.map (fun id -> Name id) fixnames in - (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) - -let rel_index n ctx = - list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx)) - -let rec unfold f b = - match f b with - | Some (x, b') -> x :: unfold f b' - | None -> [] - -let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype = - match n with - | Some (loc, n) -> [rel_index n fixctx] - | None -> - (* If recursive argument was not given by user, we try all args. - An earlier approach was to look only for inductive arguments, - but doing it properly involves delta-reduction, and it finally - doesn't seem to worth the effort (except for huge mutual - fixpoints ?) *) - let len = List.length fixctx in - unfold (function x when x = len -> None - | n -> Some (n, succ n)) 0 - -let push_named_context = List.fold_right push_named - -let check_evars env initial_sigma evd c = - let sigma = evd in - let c = nf_evar sigma c in - let rec proc_rec c = - match kind_of_term c with - | Evar (evk,args) -> - assert (Evd.mem sigma evk); - if not (Evd.mem initial_sigma evk) then - let (loc,k) = evar_source evk evd in - (match k with - | QuestionMark _ - | ImplicitArg (_, _, false) -> () - | _ -> - let evi = nf_evar_info sigma (Evd.find sigma evk) in - Pretype_errors.error_unsolvable_implicit loc env sigma evi k None) - | _ -> iter_constr proc_rec c - in proc_rec c - -let out_def = function - | Some def -> def - | None -> error "Program Fixpoint needs defined bodies." - -let interp_recursive fixkind l = - let env = Global.env() in - let fixl, ntnl = List.split l in - let kind = fixkind <> IsCoFixpoint in - let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in - - (* Interp arities allowing for unresolved types *) - let evdref = ref Evd.empty in - let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in - let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in - let fixtypes = List.map2 build_fix_type fixctxs fixccls in - let rec_sign = - List.fold_left2 (fun env' id t -> - let sort = Retyping.get_type_of env !evdref t in - let fixprot = - try mkApp (delayed_force Subtac_utils.fix_proto, [|sort; t|]) - with e -> t - in - (id,None,fixprot) :: env') - [] fixnames fixtypes - in - let env_rec = push_named_context rec_sign env in - - (* Get interpretation metadatas *) - let impls = Constrintern.compute_internalization_env env - Constrintern.Recursive fixnames fixtypes fiximps - in - let notations = List.flatten ntnl in - - (* Interp bodies with rollback because temp use of notations/implicit *) - let fixdefs = - States.with_state_protection (fun () -> - List.iter (Metasyntax.set_notation_for_interpretation impls) notations; - list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) - () in - - 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 = Typeclasses.resolve_typeclasses - ~onlyargs:true ~split:true ~fail:false env_rec evd - in - let evd = Evarutil.nf_evar_map evd in - let fixdefs = List.map (nf_evar evd) fixdefs in - let fixtypes = List.map (nf_evar evd) fixtypes in - let rec_sign = nf_named_context_evar evd rec_sign in - - let recdefs = List.length rec_sign in - List.iter (check_evars env_rec Evd.empty evd) fixdefs; - List.iter (check_evars env Evd.empty evd) fixtypes; - Command.check_mutuality env kind (List.combine fixnames fixdefs); - - (* Russell-specific code *) - - (* Get the interesting evars, those that were not instanciated *) - let isevars = Evd.undefined_evars evd in - let evm = isevars in - (* Solve remaining evars *) - let rec collect_evars id def typ imps = - (* Generalize by the recursive prototypes *) - let def = - Termops.it_mkNamedLambda_or_LetIn def rec_sign - and typ = - Termops.it_mkNamedProd_or_LetIn typ rec_sign - in - let evm' = Subtac_utils.evars_of_term evm Evd.empty def in - let evm' = Subtac_utils.evars_of_term evm evm' typ in - let evars, _, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in - (id, def, typ, imps, evars) - in - let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in - (match fixkind with - | IsFixpoint wfl -> - let possible_indexes = - list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in - let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), - Array.of_list fixtypes, - Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) - in - let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in - list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l - | IsCoFixpoint -> ()); - Subtac_obligations.add_mutual_definitions defs notations fixkind - -let out_n = function - Some n -> n - | None -> raise Not_found - -let build_recursive l = - let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in - match g, l with - [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] -> - ignore(build_wellfounded (id, n, bl, typ, out_def def) r - (match n with Some n -> mkIdentC (snd n) | None -> - errorlabstrm "Subtac_command.build_recursive" - (str "Recursive argument required for well-founded fixpoints")) - ntn) - - | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] -> - ignore(build_wellfounded (id, n, bl, typ, out_def def) (Option.default (CRef lt_ref) r) - m ntn) - - | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g -> - 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 - | _, _ -> - errorlabstrm "Subtac_command.build_recursive" - (str "Well-founded fixpoints not allowed in mutually recursive blocks") - -let build_corecursive l = - let fixl = List.map (fun (((_,id),bl,typ,def),ntn) -> - ({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 diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli deleted file mode 100644 index 72549a011..000000000 --- a/plugins/subtac/subtac_command.mli +++ /dev/null @@ -1,60 +0,0 @@ -open Pretyping -open Evd -open Environ -open Term -open Topconstr -open Names -open Libnames -open Pp -open Vernacexpr -open Constrintern - -val interp_gen : - typing_constraint -> - evar_map ref -> - env -> - ?impls:internalization_env -> - ?allow_patvar:bool -> - ?ltacvars:ltac_sign -> - constr_expr -> constr -val interp_constr : - evar_map ref -> - env -> constr_expr -> constr -val interp_type_evars : - evar_map ref -> - env -> - ?impls:internalization_env -> - constr_expr -> constr -val interp_casted_constr_evars : - evar_map ref -> - env -> - ?impls:internalization_env -> - constr_expr -> types -> constr -val interp_open_constr : - evar_map ref -> env -> constr_expr -> constr -val interp_constr_judgment : - evar_map ref -> - env -> - constr_expr -> unsafe_judgment -val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list - -val interp_binder : Evd.evar_map ref -> - Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr - - -val telescope : - (Names.name * Term.types option * Term.types) list -> - Term.types * (Names.name * Term.types option * Term.types) list * - Term.constr - -val build_wellfounded : - Names.identifier * 'a * Topconstr.local_binder list * - Topconstr.constr_expr * Topconstr.constr_expr -> - Topconstr.constr_expr -> - Topconstr.constr_expr -> 'b -> Subtac_obligations.progress - -val build_recursive : - (fixpoint_expr * decl_notation list) list -> unit - -val build_corecursive : - (cofixpoint_expr * decl_notation list) list -> unit diff --git a/plugins/subtac/subtac_errors.ml b/plugins/subtac/subtac_errors.ml deleted file mode 100644 index f07bbeb43..000000000 --- a/plugins/subtac/subtac_errors.ml +++ /dev/null @@ -1,25 +0,0 @@ -open Errors -open Util -open Pp -open Printer - -type term_pp = Pp.std_ppcmds - -type subtyping_error = - | UncoercibleInferType of loc * term_pp * term_pp - | UncoercibleInferTerm of loc * term_pp * term_pp * term_pp * term_pp - | UncoercibleRewrite of term_pp * term_pp - -type typing_error = - | NonFunctionalApp of loc * term_pp * term_pp * term_pp - | NonConvertible of loc * term_pp * term_pp - | NonSigma of loc * term_pp - | IllSorted of loc * term_pp - -exception Subtyping_error of subtyping_error -exception Typing_error of typing_error - -exception Debug_msg of string - -let typing_error e = raise (Typing_error e) -let subtyping_error e = raise (Subtyping_error e) diff --git a/plugins/subtac/subtac_errors.mli b/plugins/subtac/subtac_errors.mli deleted file mode 100644 index c65203075..000000000 --- a/plugins/subtac/subtac_errors.mli +++ /dev/null @@ -1,15 +0,0 @@ -type term_pp = Pp.std_ppcmds -type subtyping_error = - UncoercibleInferType of Pp.loc * term_pp * term_pp - | UncoercibleInferTerm of Pp.loc * term_pp * term_pp * term_pp * term_pp - | UncoercibleRewrite of term_pp * term_pp -type typing_error = - NonFunctionalApp of Pp.loc * term_pp * term_pp * term_pp - | NonConvertible of Pp.loc * term_pp * term_pp - | NonSigma of Pp.loc * term_pp - | IllSorted of Pp.loc * term_pp -exception Subtyping_error of subtyping_error -exception Typing_error of typing_error -exception Debug_msg of string -val typing_error : typing_error -> 'a -val subtyping_error : subtyping_error -> 'a diff --git a/plugins/subtac/subtac_plugin.mllib b/plugins/subtac/subtac_plugin.mllib deleted file mode 100644 index c932a7171..000000000 --- a/plugins/subtac/subtac_plugin.mllib +++ /dev/null @@ -1,10 +0,0 @@ -Subtac_utils -Eterm -Subtac_errors -Subtac_obligations -Subtac_pretyping -Subtac_command -Subtac_classes -Subtac -G_subtac -Subtac_plugin_mod diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml deleted file mode 100644 index f64c1ae2f..000000000 --- a/plugins/subtac/subtac_pretyping.ml +++ /dev/null @@ -1,137 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Global -open Pp -open Errors -open Util -open Names -open Sign -open Evd -open Term -open Termops -open Reductionops -open Environ -open Type_errors -open Typeops -open Libnames -open Classops -open List -open Recordops -open Evarutil -open Pretype_errors -open Glob_term -open Evarconv -open Pattern - -open Subtac_coercion -open Subtac_utils -open Coqlib -open Printer -open Subtac_errors -open Eterm - -open Pretyping - -let _ = Pretyping.allow_anonymous_refs := true - -type recursion_info = { - arg_name: name; - arg_type: types; (* A *) - args_after : rel_context; - wf_relation: constr; (* R : A -> A -> Prop *) - wf_proof: constr; (* : well_founded R *) - f_type: types; (* f: A -> Set *) - f_fulltype: types; (* Type with argument and wf proof product first *) -} - -let my_print_rec_info env t = - str "Name: " ++ Nameops.pr_name t.arg_name ++ spc () ++ - str "Arg type: " ++ my_print_constr env t.arg_type ++ spc () ++ - str "Wf relation: " ++ my_print_constr env t.wf_relation ++ spc () ++ - str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++ - str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++ - str "Full type: " ++ my_print_constr env t.f_fulltype -(* trace (str "pretype for " ++ (my_print_glob_constr env c) ++ *) -(* str " and tycon "++ my_print_tycon env tycon ++ *) -(* str " in environment: " ++ my_print_env env); *) - -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 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 - let evm = unevd' in - isevars := unevd'; - nf_evar evm j.uj_val, nf_evar evm j.uj_type - -let find_with_index x l = - let rec aux i = function - (y, _, _) as t :: tl -> if x = y then i, t else aux (succ i) tl - | [] -> raise Not_found - in aux 0 l - -open Vernacexpr - -let coqintern_constr evd env : Topconstr.constr_expr -> Glob_term.glob_constr = - Constrintern.intern_constr evd env -let coqintern_type evd env : Topconstr.constr_expr -> Glob_term.glob_constr = - Constrintern.intern_type evd env - -let env_with_binders env isevars l = - let rec aux ((env, rels) as acc) = function - Topconstr.LocalRawDef ((loc, name), def) :: tl -> - let rawdef = coqintern_constr !isevars env def in - let coqdef, deftyp = interp env isevars rawdef empty_tycon in - let reldecl = (name, Some coqdef, deftyp) in - aux (push_rel reldecl env, reldecl :: rels) tl - | Topconstr.LocalRawAssum (bl, k, typ) :: tl -> - let rawtyp = coqintern_type !isevars env typ in - let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in - let acc = - List.fold_left (fun (env, rels) (loc, name) -> - let reldecl = (name, None, coqtyp) in - (push_rel reldecl env, - reldecl :: rels)) - (env, rels) bl - in aux acc tl - | [] -> acc - in aux (env, []) l - -let subtac_process ?(is_type=false) env isevars id bl c tycon = - let c = Topconstr.abstract_constr_expr c bl in - let tycon, imps = - match tycon with - 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_glob_constr t in - let coqt, ttyp = interp env isevars t empty_tycon in - mk_tycon coqt, Some imps - in - let c = coqintern_constr !isevars env c in - let imps = match imps with - | Some i -> i - | None -> Implicit_quantifiers.implicits_of_glob_constr ~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 ty = nf_evar !isevars (match tycon with Some c -> c | _ -> ctyp) in - evm, coqc, ty, imps - -open Subtac_obligations - -let subtac_proof kind hook env isevars id bl c tycon = - let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in - let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in - let evm' = Subtac_utils.evars_of_term evm evm' coqt in - let evars, _, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in - add_definition id ~term:def ty ~implicits:imps ~kind ~hook evars diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli deleted file mode 100644 index e999f1710..000000000 --- a/plugins/subtac/subtac_pretyping.mli +++ /dev/null @@ -1,21 +0,0 @@ -open Term -open Environ -open Names -open Sign -open Evd -open Global -open Topconstr -open Implicit_quantifiers -open Impargs - -val interp : - Environ.env -> - Evd.evar_map ref -> - Glob_term.glob_constr -> - Evarutil.type_constraint -> Term.constr * Term.constr - -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 -> - constr_expr -> constr_expr option -> Subtac_obligations.progress diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml deleted file mode 100644 index 8f56bf52c..000000000 --- a/plugins/subtac/subtac_utils.ml +++ /dev/null @@ -1,479 +0,0 @@ -(** -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *) - -open Evd -open Libnames -open Coqlib -open Term -open Names -open Errors -open Pp -open Util - -let ($) f x = f x - -(****************************************************************************) -(* Library linking *) - -let contrib_name = "Program" -let subtac_dir = [contrib_name] -let fixsub_module = subtac_dir @ ["Wf"] -let utils_module = subtac_dir @ ["Utils"] -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 safe_init_constant md name () = - check_required_library ("Coq"::md); - init_constant md name () -let fix_proto = safe_init_constant tactics_module "fix_proto" -let hide_obligation = safe_init_constant tactics_module "obligation" - -let ex_pi1 = init_constant utils_module "ex_pi1" -let ex_pi2 = init_constant utils_module "ex_pi2" - -let make_ref l s = init_reference l s -let fix_sub_ref = make_ref fixsub_module "Fix_sub" -let measure_on_R_ref = make_ref fixsub_module "MR" -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" -let fix_measure_sub_ref = make_ref fixsub_module "Fix_measure_sub" -let refl_ref = make_ref ["Init";"Logic"] "refl_equal" - -let make_ref s = Qualid (dummy_loc, qualid_of_string s) -let lt_ref = make_ref "Init.Peano.lt" -let sig_ref = make_ref "Init.Specif.sig" -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" () } - -let sig_ = build_sig - -let fix_proto = safe_init_constant tactics_module "fix_proto" -let hide_obligation = safe_init_constant tactics_module "obligation" - -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 = init_constant ["Init"; "Logic"] "not" - -let and_typ = Coqlib.build_coq_and - -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 = - safe_init_constant ["Logic";"JMeq"] "JMeq" - -let jmeq_rec = - init_constant ["Logic";"JMeq"] "JMeq_rec" - -let jmeq_refl = - init_constant ["Logic";"JMeq"] "JMeq_refl" - -let ex_ind = init_constant ["Init"; "Logic"] "ex" -let ex_intro = init_reference ["Init"; "Logic"] "ex_intro" - -let proj1 = init_constant ["Init"; "Logic"] "proj1" -let proj2 = init_constant ["Init"; "Logic"] "proj2" - -let existS = build_sigma_type - -let prod = build_prod - - -(* orders *) -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) - -open Pp - -let my_print_constr = Termops.print_constr_env -let my_print_constr_expr = Ppconstr.pr_constr_expr -let my_print_rel_context env ctx = Printer.pr_rel_context env ctx -let my_print_context = Termops.print_rel_context -let my_print_named_context = Termops.print_named_context -let my_print_env = Termops.print_env -let my_print_glob_constr = Printer.pr_glob_constr_env -let my_print_evardefs = Evd.pr_evar_map None - -let my_print_tycon = Evarutil.pr_tycon - -let debug_level = 2 - -let debug_on = true - -let debug n s = - if debug_on then - if !Flags.debug && n >= debug_level then - msgnl s - else () - else () - -let debug_msg n s = - if debug_on then - if !Flags.debug && n >= debug_level then s - else mt () - else mt () - -let trace s = - if debug_on then - if !Flags.debug && debug_level > 0 then msgnl s - else () - else () - -let rec pp_list f = function - [] -> mt() - | x :: y -> f x ++ spc () ++ pp_list f y - -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" ()) - (init_constant ["Arith"; "Wf_nat"] "lt_wf") - -let std_relations = Lazy.lazy_from_fun std_relations - -type binders = Topconstr.local_binder list - -let app_opt c e = - match c with - Some constr -> constr e - | None -> e - -let print_args env args = - Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "") - -let make_existential loc ?(opaque = Define true) env isevars c = - let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in - let (key, args) = destEvar evar in - (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++ - print_args env args ++ str " for type: "++ - my_print_constr env c) with _ -> ()); - evar - -let make_existential_expr loc env c = - let key = Evarutil.new_untyped_evar () in - let evar = Topconstr.CEvar (loc, key, None) in - debug 2 (str "Constructed evar " ++ int key); - evar - -let string_of_hole_kind = function - | ImplicitArg _ -> "ImplicitArg" - | BinderType _ -> "BinderType" - | QuestionMark _ -> "QuestionMark" - | CasesType -> "CasesType" - | InternalHole -> "InternalHole" - | TomatchTypeParameter _ -> "TomatchTypeParameter" - | GoalEvar -> "GoalEvar" - | ImpossibleCase -> "ImpossibleCase" - | MatchingVar _ -> "MatchingVar" - -let evars_of_term evc init c = - let rec evrec acc c = - match kind_of_term c with - | Evar (n, _) when Evd.mem evc n -> Evd.add acc n (Evd.find evc n) - | Evar (n, _) -> assert(false) - | _ -> fold_constr evrec acc c - in - evrec init c - -let non_instanciated_map env evd evm = - List.fold_left - (fun evm (key, evi) -> - let (loc,k) = evar_source key !evd in - debug 2 (str "evar " ++ int key ++ str " has kind " ++ - str (string_of_hole_kind k)); - match k with - | QuestionMark _ -> Evd.add evm key evi - | ImplicitArg (_,_,false) -> Evd.add evm key evi - | _ -> - debug 2 (str " and is an implicit"); - Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k None) - Evd.empty (Evarutil.non_instantiated evm) - -let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition -let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition - -let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma -let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma - -let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint -let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint - -open Tactics -open Tacticals - -let filter_map f l = - let rec aux acc = function - hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl - | None -> aux acc tl) - | [] -> List.rev acc - in aux [] l - -let build_dependent_sum l = - let rec aux names conttac conttype = function - (n, t) :: ((_ :: _) as tl) -> - let hyptype = substl names t in - trace (spc () ++ str ("treating evar " ^ string_of_id n)); - (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype) - with _ -> ()); - let tac = assert_tac (Name n) hyptype in - let conttac = - (fun cont -> - conttac - (tclTHENS tac - ([intros; - (tclTHENSEQ - [constructor_tac false (Some 1) 1 - (Glob_term.ImplicitBindings [mkVar n]); - cont]); - ]))) - in - let conttype = - (fun typ -> - let tex = mkLambda (Name n, t, typ) in - conttype - (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 [] identity identity (List.rev l) - -open Proof_type -open Tacexpr - -let mkProj1 a b c = - mkApp (delayed_force proj1, [| a; b; c |]) - -let mkProj2 a b c = - mkApp (delayed_force proj2, [| a; b; c |]) - -let mk_ex_pi1 a b c = - mkApp (delayed_force ex_pi1, [| a; b; c |]) - -let mk_ex_pi2 a b c = - mkApp (delayed_force ex_pi2, [| a; b; c |]) - -let mkSubset name typ prop = - mkApp ((delayed_force sig_).typ, - [| typ; mkLambda (name, typ, prop) |]) - -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 = delayed_force and_typ in - unsafe_fold_right - (fun c conj -> - mkApp (conj_typ, [| c ; conj |])) - l - -let mk_not c = - let notc = delayed_force not_ref in - mkApp (notc, [| c |]) - -let and_tac l hook = - let andc = Coqlib.build_coq_and () in - let rec aux ((accid, goal, tac, extract) as acc) = function - | [] -> (* Singleton *) acc - - | (id, x, elgoal, eltac) :: tl -> - let tac' = tclTHEN simplest_split (tclTHENLIST [tac; eltac]) in - let proj = fun c -> mkProj2 goal elgoal c in - let extract = List.map (fun (id, x, y, f) -> (id, x, y, (fun c -> f (mkProj1 goal elgoal c)))) extract in - aux ((string_of_id id) ^ "_" ^ accid, mkApp (andc, [| goal; elgoal |]), tac', - (id, x, elgoal, proj) :: extract) tl - - in - let and_proof_id, and_goal, and_tac, and_extract = - match l with - | [] -> raise (Invalid_argument "and_tac: empty list of goals") - | (hdid, x, hdg, hdt) :: tl -> - aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl - in - let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in - Lemmas.start_proof and_proofid goal_kind and_goal - (hook (fun c -> List.map (fun (id, x, t, f) -> (id, x, t, f c)) and_extract)); - trace (str "Started and proof"); - Pfedit.by and_tac; - trace (str "Applied and tac") - - -let destruct_ex ext ex = - let rec aux c acc = - match kind_of_term c with - App (f, args) -> - (match kind_of_term f with - 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) - in - let pi1 = (mk_ex_pi1 dom rng acc) in - let rng_body = - match kind_of_term rng with - Lambda (_, _, t) -> subst1 pi1 t - | t -> rng - in - pi1 :: aux rng_body (mk_ex_pi2 dom rng acc) - | _ -> [acc]) - | _ -> [acc] - in aux ex ext - -open Glob_term - -let id_of_name = function - Name n -> n - | Anonymous -> raise (Invalid_argument "id_of_name") - -let definition_message id = - Nameops.pr_id id ++ str " is defined" - -let recursive_message v = - match Array.length v with - | 0 -> error "no recursive definition" - | 1 -> (Printer.pr_constant (Global.env ()) v.(0) ++ str " is recursively defined") - | _ -> hov 0 (prvect_with_sep pr_comma (Printer.pr_constant (Global.env ())) v ++ - spc () ++ str "are recursively defined") - -let print_message m = - Flags.if_verbose ppnl m - -(* Solve an obligation using tactics, return the corresponding proof term *) -let solve_by_tac evi t = - let id = id_of_string "H" in - try - Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl - (fun _ _ -> ()); - Pfedit.by (tclCOMPLETE t); - let _,(const,_,_,_) = Pfedit.cook_proof ignore in - Pfedit.delete_current_proof (); - Inductiveops.control_only_guard (Global.env ()) - const.Entries.const_entry_body; - const.Entries.const_entry_body - with e -> - Pfedit.delete_current_proof(); - raise e - -(* let apply_tac t goal = t goal *) - -(* let solve_by_tac evi t = *) -(* let ev = 1 in *) -(* let evm = Evd.add Evd.empty ev evi in *) -(* let goal = {it = evi; sigma = evm } in *) -(* let (res, valid) = apply_tac t goal in *) -(* if res.it = [] then *) -(* let prooftree = valid [] in *) -(* let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *) -(* if obls = [] then proofterm *) -(* else raise Exit *) -(* else raise Exit *) - -let rec string_of_list sep f = function - [] -> "" - | x :: [] -> f x - | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl - -let string_of_intset d = - string_of_list "," string_of_int (Intset.elements d) - -(**********************************************************) -(* Pretty-printing *) -open Printer -open Ppconstr -open Nameops -open Evd - -let pr_meta_map evd = - let ml = meta_list evd in - let pr_name = function - Name id -> str"[" ++ pr_id id ++ str"]" - | _ -> mt() in - let pr_meta_binding = function - | (mv,Cltyp (na,b)) -> - hov 0 - (pr_meta mv ++ pr_name na ++ str " : " ++ - Termops.print_constr b.rebus ++ fnl ()) - | (mv,Clval(na,b,_)) -> - hov 0 - (pr_meta mv ++ pr_name na ++ str " := " ++ - Termops.print_constr (fst b).rebus ++ fnl ()) - in - prlist pr_meta_binding ml - -let pr_idl idl = pr_sequence pr_id idl - -let pr_evar_info evi = - let phyps = - (*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *) - Printer.pr_named_context (Global.env()) (evar_context evi) - in - let pty = Termops.print_constr evi.evar_concl in - let pb = - match evi.evar_body with - | Evar_empty -> mt () - | Evar_defined c -> spc() ++ str"=> " ++ Termops.print_constr c - in - hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]") - -let pr_evar_map sigma = - h 0 - (prlist_with_sep fnl - (fun (ev,evi) -> - h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi)) - (to_list sigma)) - -let pr_constraints pbs = - h 0 - (prlist_with_sep fnl (fun (pbty,t1,t2) -> - Termops.print_constr t1 ++ spc() ++ - str (match pbty with - | Reduction.CONV -> "==" - | Reduction.CUMUL -> "<=") ++ - spc() ++ Termops.print_constr t2) pbs) - -let pr_evar_map evd = - let pp_evm = - let evars = evd in - if evars = empty then mt() else - str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in - let pp_met = - if meta_list evd = [] then mt() else - str"METAS:"++brk(0,1)++pr_meta_map evd in - v 0 (pp_evm ++ pp_met) - -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)) - -let tactics_call tac args = - TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args)) diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli deleted file mode 100644 index 5cbb307db..000000000 --- a/plugins/subtac/subtac_utils.mli +++ /dev/null @@ -1,130 +0,0 @@ -open Term -open Libnames -open Coqlib -open Environ -open Pp -open Evd -open Decl_kinds -open Topconstr -open Glob_term -open Errors -open Util -open Evarutil -open Names -open Sign - -val ($) : ('a -> 'b) -> 'a -> 'b -val contrib_name : string -val subtac_dir : string list -val fixsub_module : string list -val init_constant : string list -> string -> constr delayed -val init_reference : string list -> string -> global_reference 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 delayed - -val fix_proto : constr delayed - -val hide_obligation : constr delayed - -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 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 - -val my_print_constr : env -> constr -> std_ppcmds -val my_print_constr_expr : constr_expr -> std_ppcmds -val my_print_evardefs : evar_map -> std_ppcmds -val my_print_context : env -> std_ppcmds -val my_print_rel_context : env -> rel_context -> std_ppcmds -val my_print_named_context : env -> std_ppcmds -val my_print_env : env -> std_ppcmds -val my_print_glob_constr : env -> glob_constr -> std_ppcmds -val my_print_tycon : env -> type_constraint -> 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 delayed) Hashtbl.t - -type binders = local_binder list -val print_args : env -> constr array -> std_ppcmds -val make_existential : loc -> ?opaque:obligation_definition_status -> - env -> evar_map ref -> types -> constr -val make_existential_expr : loc -> 'a -> 'b -> constr_expr -val string_of_hole_kind : hole_kind -> string -val evars_of_term : evar_map -> evar_map -> constr -> evar_map -val non_instanciated_map : env -> evar_map ref -> evar_map -> evar_map -val global_kind : logical_kind -val goal_kind : locality * goal_object_kind -val global_proof_kind : logical_kind -val goal_proof_kind : locality * goal_object_kind -val global_fix_kind : logical_kind -val goal_fix_kind : locality * goal_object_kind - -val mkSubset : name -> constr -> constr -> constr -val mkProj1 : constr -> constr -> constr -> constr -val mkProj1 : constr -> constr -> constr -> constr -val mk_ex_pi1 : constr -> constr -> constr -> constr -val mk_ex_pi1 : constr -> constr -> constr -> constr -val mk_eq : types -> constr -> constr -> types -val mk_eq_refl : types -> constr -> constr -val mk_JMeq : types -> constr-> types -> constr -> types -val mk_JMeq_refl : types -> constr -> constr -val mk_conj : types list -> types -val mk_not : types -> types - -val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types -val and_tac : (identifier * 'a * constr * Proof_type.tactic) list -> - ((constr -> (identifier * 'a * constr * constr) list) -> Tacexpr.declaration_hook) -> unit - -val destruct_ex : constr -> constr -> constr list - -val id_of_name : name -> identifier - -val definition_message : identifier -> std_ppcmds -val recursive_message : constant array -> std_ppcmds - -val print_message : std_ppcmds -> unit - -val solve_by_tac : evar_info -> Tacmach.tactic -> constr - -val string_of_list : string -> ('a -> string) -> 'a list -> string -val string_of_intset : Intset.t -> string - -val pr_evar_map : evar_map -> Pp.std_ppcmds - -val tactics_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr - -val pp_list : ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds diff --git a/plugins/subtac/test/ListDep.v b/plugins/subtac/test/ListDep.v deleted file mode 100644 index e3dbd127f..000000000 --- a/plugins/subtac/test/ListDep.v +++ /dev/null @@ -1,49 +0,0 @@ -(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) -Require Import List. -Require Import Coq.Program.Program. - -Set Implicit Arguments. - -Definition sub_list (A : Set) (l' l : list A) := (forall v, In v l' -> In v l) /\ length l' <= length l. - -Lemma sub_list_tl : forall A : Set, forall x (l l' : list A), sub_list (x :: l) l' -> sub_list l l'. -Proof. - intros. - inversion H. - split. - intros. - apply H0. - auto with datatypes. - auto with arith. -Qed. - -Section Map_DependentRecursor. - Variable U V : Set. - Variable l : list U. - Variable f : { x : U | In x l } -> V. - - Obligations Tactic := unfold sub_list in * ; - program_simpl ; intuition. - - Program Fixpoint map_rec ( l' : list U | sub_list l' l ) - { measure length l' } : { r : list V | length r = length l' } := - match l' with - | nil => nil - | cons x tl => let tl' := map_rec tl in - f x :: tl' - end. - - Next Obligation. - destruct_call map_rec. - simpl in *. - subst l'. - simpl ; auto with arith. - Qed. - - Program Definition map : list V := map_rec l. - -End Map_DependentRecursor. - -Extraction map. -Extraction map_rec. - diff --git a/plugins/subtac/test/ListsTest.v b/plugins/subtac/test/ListsTest.v deleted file mode 100644 index 2cea0841d..000000000 --- a/plugins/subtac/test/ListsTest.v +++ /dev/null @@ -1,99 +0,0 @@ -(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) -Require Import Coq.Program.Program. -Require Import List. - -Set Implicit Arguments. - -Section Accessors. - Variable A : Set. - - Program Definition myhd : forall (l : list A | length l <> 0), A := - fun l => - match l with - | nil => ! - | hd :: tl => hd - end. - - Program Definition mytail (l : list A | length l <> 0) : list A := - match l with - | nil => ! - | hd :: tl => tl - end. -End Accessors. - -Program Definition test_hd : nat := myhd (cons 1 nil). - -(*Eval compute in test_hd*) -(*Program Definition test_tail : list A := mytail nil.*) - -Section app. - Variable A : Set. - - Program Fixpoint app (l : list A) (l' : list A) { struct l } : - { r : list A | length r = length l + length l' } := - match l with - | nil => l' - | hd :: tl => hd :: (tl ++ l') - end - where "x ++ y" := (app x y). - - Next Obligation. - intros. - destruct_call app ; program_simpl. - Defined. - - Program Lemma app_id_l : forall l : list A, l = nil ++ l. - Proof. - simpl ; auto. - Qed. - - Program Lemma app_id_r : forall l : list A, l = l ++ nil. - Proof. - induction l ; simpl in * ; auto. - rewrite <- IHl ; auto. - Qed. - -End app. - -Extraction app. - -Section Nth. - - Variable A : Set. - - Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A := - match n, l with - | 0, hd :: _ => hd - | S n', _ :: tl => nth tl n' - | _, nil => ! - end. - - Next Obligation. - Proof. - simpl in *. auto with arith. - Defined. - - Next Obligation. - Proof. - inversion H. - Qed. - - Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := - match l, n with - | hd :: _, 0 => hd - | _ :: tl, S n' => nth' tl n' - | nil, _ => ! - end. - Next Obligation. - Proof. - simpl in *. auto with arith. - Defined. - - Next Obligation. - Proof. - intros. - inversion H. - Defined. - -End Nth. - diff --git a/plugins/subtac/test/Mutind.v b/plugins/subtac/test/Mutind.v deleted file mode 100644 index 01e2d75f3..000000000 --- a/plugins/subtac/test/Mutind.v +++ /dev/null @@ -1,20 +0,0 @@ -Require Import List. - -Program Fixpoint f a : { x : nat | x > 0 } := - match a with - | 0 => 1 - | S a' => g a a' - end -with g a b : { x : nat | x > 0 } := - match b with - | 0 => 1 - | S b' => f b' - end. - -Check f. -Check g. - - - - - diff --git a/plugins/subtac/test/Test1.v b/plugins/subtac/test/Test1.v deleted file mode 100644 index 7e0755d57..000000000 --- a/plugins/subtac/test/Test1.v +++ /dev/null @@ -1,16 +0,0 @@ -Program Definition test (a b : nat) : { x : nat | x = a + b } := - ((a + b) : { x : nat | x = a + b }). -Proof. -intros. -reflexivity. -Qed. - -Print test. - -Require Import List. - -Program hd_opt (l : list nat) : { x : nat | x <> 0 } := - match l with - nil => 1 - | a :: l => a - end. diff --git a/plugins/subtac/test/euclid.v b/plugins/subtac/test/euclid.v deleted file mode 100644 index 97c3d9414..000000000 --- a/plugins/subtac/test/euclid.v +++ /dev/null @@ -1,24 +0,0 @@ -Require Import Coq.Program.Program. -Require Import Coq.Arith.Compare_dec. -Notation "( x & y )" := (existS _ x y) : core_scope. - -Require Import Omega. - -Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a} : - { q : nat & { r : nat | a = b * q + r /\ r < b } } := - if le_lt_dec b a then let (q', r) := euclid (a - b) b in - (S q' & r) - else (O & a). - -Next Obligation. - assert(b * S q' = b * q' + b) by auto with arith ; omega. -Defined. - -Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q). - -Eval lazy beta zeta delta iota in test_euclid. - -Program Definition testsig (a : nat) : { x : nat & { y : nat | x < y } } := - (a & S a). - -Check testsig. diff --git a/plugins/subtac/test/id.v b/plugins/subtac/test/id.v deleted file mode 100644 index 9ae110881..000000000 --- a/plugins/subtac/test/id.v +++ /dev/null @@ -1,46 +0,0 @@ -Require Coq.Arith.Arith. - -Require Import Coq.subtac.Utils. -Program Fixpoint id (n : nat) : { x : nat | x = n } := - match n with - | O => O - | S p => S (id p) - end. -intros ; auto. - -pose (subset_simpl (id p)). -simpl in e. -unfold p0. -rewrite e. -auto. -Defined. - -Check id. -Print id. -Extraction id. - -Axiom le_gt_dec : forall n m, { n <= m } + { n > m }. -Require Import Omega. - -Program Fixpoint id_if (n : nat) { wf n lt }: { x : nat | x = n } := - if le_gt_dec n 0 then 0 - else S (id_if (pred n)). -intros. -auto with arith. -intros. -pose (subset_simpl (id_if (pred n))). -simpl in e. -rewrite e. -induction n ; auto with arith. -Defined. - -Print id_if_instance. -Extraction id_if_instance. - -Notation "( x & y )" := (@existS _ _ x y) : core_scope. - -Program Definition testsig ( a : nat ) : { x : nat & { y : nat | x = y }} := - (a & a). -intros. -auto. -Qed. diff --git a/plugins/subtac/test/measure.v b/plugins/subtac/test/measure.v deleted file mode 100644 index 4f938f4f8..000000000 --- a/plugins/subtac/test/measure.v +++ /dev/null @@ -1,20 +0,0 @@ -Notation "( x & y )" := (@existS _ _ x y) : core_scope. -Unset Printing All. -Require Import Coq.Arith.Compare_dec. - -Require Import Coq.Program.Program. - -Fixpoint size (a : nat) : nat := - match a with - 0 => 1 - | S n => S (size n) - end. - -Program Fixpoint test_measure (a : nat) {measure size a} : nat := - match a with - | S (S n) => S (test_measure n) - | 0 | S 0 => a - end. - -Check test_measure. -Print test_measure.
\ No newline at end of file diff --git a/plugins/subtac/test/rec.v b/plugins/subtac/test/rec.v deleted file mode 100644 index aaefd8cc5..000000000 --- a/plugins/subtac/test/rec.v +++ /dev/null @@ -1,65 +0,0 @@ -Require Import Coq.Arith.Arith. -Require Import Lt. -Require Import Omega. - -Axiom lt_ge_dec : forall x y : nat, { x < y } + { x >= y }. -(*Proof. - intros. - elim (le_lt_dec y x) ; intros ; auto with arith. -Defined. -*) -Require Import Coq.subtac.FixSub. -Require Import Wf_nat. - -Lemma preda_lt_a : forall a, 0 < a -> pred a < a. -auto with arith. -Qed. - -Program Fixpoint id_struct (a : nat) : nat := - match a with - 0 => 0 - | S n => S (id_struct n) - end. - -Check struct_rec. - - if (lt_ge_dec O a) - then S (wfrec (pred a)) - else O. - -Program Fixpoint wfrec (a : nat) { wf a lt } : nat := - if (lt_ge_dec O a) - then S (wfrec (pred a)) - else O. -intros. -apply preda_lt_a ; auto. - -Defined. - -Extraction wfrec. -Extraction Inline proj1_sig. -Extract Inductive bool => "bool" [ "true" "false" ]. -Extract Inductive sumbool => "bool" [ "true" "false" ]. -Extract Inlined Constant lt_ge_dec => "<". - -Extraction wfrec. -Extraction Inline lt_ge_dec le_lt_dec. -Extraction wfrec. - - -Program Fixpoint structrec (a : nat) { wf a lt } : nat := - match a with - S n => S (structrec n) - | 0 => 0 - end. -intros. -unfold n0. -omega. -Defined. - -Print structrec. -Extraction structrec. -Extraction structrec. - -Definition structrec_fun (a : nat) : nat := structrec a (lt_wf a). -Print structrec_fun. diff --git a/plugins/subtac/test/take.v b/plugins/subtac/test/take.v deleted file mode 100644 index 90ae8bae8..000000000 --- a/plugins/subtac/test/take.v +++ /dev/null @@ -1,34 +0,0 @@ -(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) -Require Import JMeq. -Require Import List. -Require Import Program. - -Set Implicit Arguments. -Obligations Tactic := idtac. - -Print cons. - -Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } := - match n with - | 0 => nil - | S p => - match l with - | cons hd tl => let rest := take tl p in cons hd rest - | nil => ! - end - end. - -Require Import Omega. -Solve All Obligations. -Next Obligation. - destruct_call take ; program_simpl. -Defined. - -Next Obligation. - intros. - inversion H. -Defined. - - - - diff --git a/plugins/subtac/test/wf.v b/plugins/subtac/test/wf.v deleted file mode 100644 index 5ccc154af..000000000 --- a/plugins/subtac/test/wf.v +++ /dev/null @@ -1,48 +0,0 @@ -Notation "( x & y )" := (@existS _ _ x y) : core_scope. -Unset Printing All. -Require Import Coq.Arith.Compare_dec. - -Require Import Coq.subtac.Utils. - -Ltac one_simpl_hyp := - match goal with - | [H : (`exist _ _ _) = _ |- _] => simpl in H - | [H : _ = (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) < _ |- _] => simpl in H - | [H : _ < (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) <= _ |- _] => simpl in H - | [H : _ <= (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) > _ |- _] => simpl in H - | [H : _ > (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) >= _ |- _] => simpl in H - | [H : _ >= (`exist _ _ _) |- _] => simpl in H - end. - -Ltac one_simpl_subtac := - destruct_exists ; - repeat one_simpl_hyp ; simpl. - -Ltac simpl_subtac := do 3 one_simpl_subtac ; simpl. - -Require Import Omega. -Require Import Wf_nat. - -Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} : - { q : nat & { r : nat | a = b * q + r /\ r < b } } := - if le_lt_dec b a then let (q', r) := euclid (a - b) b in - (S q' & r) - else (O & a). -destruct b ; simpl_subtac. -omega. -simpl_subtac. -assert(x0 * S q' = x0 + x0 * q'). -rewrite <- mult_n_Sm. -omega. -rewrite H2 ; omega. -simpl_subtac. -split ; auto with arith. -omega. -apply lt_wf. -Defined. - -Check euclid_evars_proof.
\ No newline at end of file diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 9c600b01e..9f44d4fef 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -141,5 +141,5 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq := Next Obligation. destruct y ; intuition eauto. Defined. - Solve Obligations using unfold equiv, complement in * ; + Solve Obligations with unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index d9e9fe257..afdfb4cec 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -105,13 +105,15 @@ Section Respecting. (** Here we build an equivalence instance for functions which relates respectful ones only, we do not export it. *) - Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type := + Definition respecting `(eqa : Equivalence A (R : relation A), + eqb : Equivalence B (R' : relation B)) : Type := { morph : A -> B | respectful R R' morph morph }. Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') : - Equivalence (fun (f g : respecting eqa eqb) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)). + Equivalence (fun (f g : respecting eqa eqb) => + forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)). - Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl. + Solve Obligations with unfold respecting in * ; simpl_relation ; program_simpl. Next Obligation. Proof. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 8e491b1b8..e0d7a3d7a 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -224,7 +224,7 @@ Hint Extern 4 (subrelation (inverse _) _) => class_apply @subrelation_symmetric : typeclass_instances. (** The complement of a relation conserves its proper elements. *) - +Set Printing All. Program Definition complement_proper `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : Proper (RA ==> RA ==> iff) (complement R) := _. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 6708220ea..a090d2007 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -108,7 +108,7 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) else in_right else in_right. - Solve Obligations using unfold complement ; program_simpl. + Solve Obligations with unfold complement ; program_simpl. (** Objects of function spaces with countable domains like bool have decidable equality. *) @@ -121,7 +121,7 @@ Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) else in_right else in_right. - Solve Obligations using try red ; unfold equiv, complement ; program_simpl. + Solve Obligations with try red ; unfold equiv, complement ; program_simpl. Next Obligation. Proof. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 2e2eb166d..6d0315b82 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -494,9 +494,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p'). - Global Program Instance eqk_equiv : Equivalence eq_key. - Global Program Instance eqke_equiv : Equivalence eq_key_elt. - Global Program Instance ltk_strorder : StrictOrder lt_key. + Global Instance eqk_equiv : Equivalence eq_key := _. + Global Instance eqke_equiv : Equivalence eq_key_elt := _. + Global Instance ltk_strorder : StrictOrder lt_key := _. Lemma mem_find : forall m x, mem x m = match find x m with None => false | _ => true end. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index e929c561c..4b3c1b4fb 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -21,7 +21,6 @@ Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". Declare ML Module "dp_plugin". Declare ML Module "recdef_plugin". -Declare ML Module "subtac_plugin". Declare ML Module "xml_plugin". (* Default substrings not considered by queries like SearchAbout *) Add Search Blacklist "_admitted" "_subproof" "Private_". diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index ca4002d7f..dda0ed68d 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -79,14 +79,14 @@ Qed. (* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f] in tactics. *) -Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B := +Definition match_eq (A B : Type) (x : A) (fn : {y : A | y = x} -> B) : B := fn (exist _ x eq_refl). (* This is what we want to be able to do: replace the originaly matched object by a new, propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *) -Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : forall (y : A | y = x), B) - (y : A | y = x), +Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B) + (y : {y:A | y = x}), match_eq A B x fn = fn y. Proof. intros. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index a823aedd3..ee0a7451b 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -35,11 +35,11 @@ Section Well_founded. Hypothesis F_ext : forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)), - (forall (y : A | R y x), f y = g y) -> F_sub x f = F_sub x g. + (forall y:{y : A | R y x}, f y = g y) -> F_sub x f = F_sub x g. Lemma Fix_F_eq : forall (x:A) (r:Acc R x), - F_sub x (fun (y:A|R y x) => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r. + F_sub x (fun y:{y:A | R y x} => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r. Proof. destruct r using Acc_inv_dep; auto. Qed. @@ -50,7 +50,7 @@ Section Well_founded. rewrite (proof_irrelevance (Acc R x) r s) ; auto. Qed. - Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun (y:A|R y x) => Fix_sub (proj1_sig y)). + Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun y:{ y:A | R y x} => Fix_sub (proj1_sig y)). Proof. intro x; unfold Fix_sub in |- *. rewrite <- (Fix_F_eq ). @@ -62,7 +62,7 @@ Section Well_founded. forall x : A, Fix_sub x = let f_sub := F_sub in - f_sub x (fun (y : A | R y x) => Fix_sub (`y)). + f_sub x (fun y: {y : A | R y x} => Fix_sub (`y)). exact Fix_eq. Qed. @@ -231,10 +231,10 @@ Module WfExtensionality. Program Lemma fix_sub_eq_ext : forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R) (P : A -> Type) - (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x), + (F_sub : forall x : A, (forall y:{y : A | R y x}, P y) -> P x), forall x : A, Fix_sub A R Rwf P F_sub x = - F_sub x (fun (y : A | R y x) => Fix_sub A R Rwf P F_sub y). + F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub y). Proof. intros ; apply Fix_eq ; auto. intros. diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 2f1b7138b..ceaab3d0f 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -172,7 +172,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props let env' = push_rel_context ctx env in evars := Evarutil.nf_evar_map !evars; evars := mark_resolvables !evars; - evars := resolve_typeclasses env !evars; + evars := resolve_typeclasses ~onlyargs:false ~fail:true env !evars; let sigma = !evars in let subst = List.map (Evarutil.nf_evar sigma) subst in if abstract then @@ -190,52 +190,58 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props (None,termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical) in instance_hook k None global imps ?hook (ConstRef cst); id end - else - begin - let props = - match props with - | Some (CRecord (loc, _, fs)) -> - if List.length fs > List.length k.cl_props then - mismatched_props env' (List.map snd fs) k.cl_props; - Some (Inl fs) - | Some t -> Some (Inr t) - | None -> None - in - let subst = - match props with - | None -> if k.cl_props = [] then Some (Inl subst) else None - | Some (Inr term) -> - let c = interp_casted_constr_evars evars env' term cty in - Some (Inr (c, subst)) - | Some (Inl props) -> - let get_id = - function - | Ident id' -> id' - | _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled") - in - let props, rest = - List.fold_left - (fun (props, rest) (id,b,_) -> - if b = None then - try - let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in - let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in - let (loc, mid) = get_id loc_mid in - List.iter (fun (n, _, x) -> - if n = Name mid then - Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x) - k.cl_projs; - c :: props, rest' - with Not_found -> - (CHole (Pp.dummy_loc, None) :: props), rest - else props, rest) - ([], props) k.cl_props - in - if rest <> [] then - unbound_method env' k.cl_impl (get_id (fst (List.hd rest))) - else - Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst)) - in + else ( + let props = + match props with + | Some (CRecord (loc, _, fs)) -> + if List.length fs > List.length k.cl_props then + mismatched_props env' (List.map snd fs) k.cl_props; + Some (Inl fs) + | Some t -> Some (Inr t) + | None -> + if Flags.is_program_mode () then Some (Inl []) + else None + in + let subst = + match props with + | None -> if k.cl_props = [] then Some (Inl subst) else None + | Some (Inr term) -> + let c = interp_casted_constr_evars evars env' term cty in + Some (Inr (c, subst)) + | Some (Inl props) -> + let get_id = + function + | Ident id' -> id' + | _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled") + in + let props, rest = + List.fold_left + (fun (props, rest) (id,b,_) -> + if b = None then + try + let (loc_mid, c) = + List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest + in + let rest' = + List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest + in + let (loc, mid) = get_id loc_mid in + List.iter (fun (n, _, x) -> + if n = Name mid then + Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x) + k.cl_projs; + c :: props, rest' + with Not_found -> + (CHole (Pp.dummy_loc, None) :: props), rest + else props, rest) + ([], props) k.cl_props + in + if rest <> [] then + unbound_method env' k.cl_impl (get_id (fst (List.hd rest))) + else + Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') + k.cl_props props subst)) + in evars := Evarutil.nf_evar_map !evars; let term, termtype = match subst with @@ -258,23 +264,42 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props let termtype = Evarutil.nf_evar !evars termtype in let term = Option.map (Evarutil.nf_evar !evars) term in let evm = undefined_evars !evars in - Evarutil.check_evars env Evd.empty !evars termtype; + Evarutil.check_evars env Evd.empty !evars termtype; if Evd.is_empty evm && term <> None then declare_instance_constant k pri global imps ?hook id (Option.get term) termtype else begin evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars; let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in - Flags.silently (fun () -> - Lemmas.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook); - if term <> None then - Pfedit.by (!refine_ref (evm, Option.get term)) - else if Flags.is_auto_intros () then - Pfedit.by (Refiner.tclDO len Tactics.intro); - (match tac with Some tac -> Pfedit.by tac | None -> ())) (); - Flags.if_verbose (msg $$ Printer.pr_open_subgoals) (); - id - end - end + if Flags.is_program_mode () then + let hook vis gr = + let cst = match gr with ConstRef kn -> kn | _ -> assert false in + Impargs.declare_manual_implicits false gr ~enriching:false [imps]; + Typeclasses.declare_instance pri (not global) (ConstRef cst) + in + let obls, constr, typ = + match term with + | Some t -> + let obls, _, constr, typ = + Obligations.eterm_obligations env id !evars evm 0 t termtype + in obls, Some constr, typ + | None -> [||], None, termtype + in + ignore (Obligations.add_definition id ?term:constr + typ ~kind:(Global,Instance) ~hook obls); + id + else + (Flags.silently + (fun () -> + Lemmas.start_proof id kind termtype + (fun _ -> instance_hook k pri global imps ?hook); + if term <> None then + Pfedit.by (!refine_ref (evm, Option.get term)) + else if Flags.is_auto_intros () then + Pfedit.by (Refiner.tclDO len Tactics.intro); + (match tac with Some tac -> Pfedit.by tac | None -> ())) (); + Flags.if_verbose (msg $$ Printer.pr_open_subgoals) (); + id) + end) let named_of_rel_context l = let acc, ctx = diff --git a/toplevel/command.ml b/toplevel/command.ml index 82ec85b7a..0b4e9daa1 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -75,7 +75,6 @@ let interp_definition bl red_option c ctypopt = None -> let c, imps2 = interp_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c in let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in - check_evars env Evd.empty !evdref body; imps1@(Impargs.lift_implicits nb_args imps2), { const_entry_body = body; const_entry_secctx = None; @@ -86,15 +85,19 @@ let interp_definition bl red_option c ctypopt = let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c ty in let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in - check_evars env Evd.empty !evdref body; - check_evars env Evd.empty !evdref typ; imps1@(Impargs.lift_implicits nb_args imps2), { const_entry_body = body; const_entry_secctx = None; const_entry_type = Some typ; const_entry_opaque = false } in - red_constant_entry (rel_context_length ctx) ce red_option, imps + red_constant_entry (rel_context_length ctx) ce red_option, !evdref, imps + +let check_definition (ce, evd, imps) = + let env = Global.env () in + check_evars env Evd.empty evd ce.const_entry_body; + Option.iter (check_evars env Evd.empty evd) ce.const_entry_type; + ce let declare_global_definition ident ce local k imps = let kn = declare_constant ident (DefinitionEntry ce,IsDefinition k) in @@ -127,6 +130,25 @@ let declare_definition ident (local,k) ce imps hook = declare_global_definition ident ce local k imps in hook local r +let _ = Obligations.declare_definition_ref := declare_definition + +let do_definition ident k bl red_option c ctypopt hook = + let (ce, evd, imps as def) = interp_definition bl red_option c ctypopt in + if Flags.is_program_mode () then + let env = Global.env () in + let c = ce.const_entry_body in + let typ = match ce.const_entry_type with + | Some t -> t + | None -> Retyping.get_type_of env evd c + in + let evm = Obligations.non_instanciated_map env (ref evd) evd in + let obls, _, c, cty = + Obligations.eterm_obligations env ident evd evm 0 c typ + in + ignore(Obligations.add_definition ident ~term:c cty ~implicits:imps ~kind:k ~hook obls) + else let ce = check_definition def in + declare_definition ident k ce imps hook + (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = @@ -488,6 +510,8 @@ let declare_fix kind f def t imps = maybe_declare_manual_implicits false gr imps; gr +let _ = Obligations.declare_fix_ref := declare_fix + let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in let names = List.map (fun id -> Name id) fixnames in @@ -522,15 +546,18 @@ let tactics_module = subtac_dir @ ["Tactics"] let init_reference dir s () = Coqlib.gen_reference "Command" dir s let init_constant dir s () = Coqlib.gen_constant "Command" dir s let make_ref l s = init_reference l s +let fix_proto = init_constant tactics_module "fix_proto" let fix_sub_ref = make_ref fixsub_module "Fix_sub" let measure_on_R_ref = make_ref fixsub_module "MR" let well_founded = init_constant ["Init"; "Wf"] "well_founded" let mkSubset name typ prop = mkApp ((delayed_force build_sigma).typ, [| typ; mkLambda (name, typ, prop) |]) - let sigT = Lazy.lazy_from_fun build_sigma_type +let make_qref s = Qualid (dummy_loc, qualid_of_string s) +let lt_ref = make_qref "Init.Peano.lt" + let rec telescope = function | [] -> assert false | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1 @@ -691,7 +718,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let evars, _, evars_def, evars_typ = Obligations.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in - Obligations.add_definition recname ~term:evars_def evars_typ evars ~hook + ignore(Obligations.add_definition recname ~term:evars_def evars_typ evars ~hook) let interp_recursive isfix fixl notations = @@ -705,7 +732,20 @@ let interp_recursive isfix fixl notations = let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in let fixtypes = List.map2 build_fix_type fixctxs fixccls in let fixtypes = List.map (nf_evar !evdref) fixtypes in - let env_rec = push_named_types env fixnames fixtypes in + let rec_sign = + List.fold_left2 + (fun env' id t -> + if Flags.is_program_mode () then + let sort = Retyping.get_type_of env !evdref t in + let fixprot = + try mkApp (delayed_force fix_proto, [|sort; t|]) + with e -> t + in + (id,None,fixprot) :: env' + else (id,None,t) :: env') + [] fixnames fixtypes + in + let env_rec = push_named_context rec_sign env in (* Get interpretation metadatas *) let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in @@ -722,20 +762,23 @@ let interp_recursive isfix fixl notations = let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in let fixtypes = List.map (nf_evar evd) fixtypes in let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in + + (* Build the fix declaration block *) + (env,rec_sign,evd), (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots + +let check_recursive isfix ((env,rec_sign,evd),(fixnames,fixdefs,fixtypes),info) = let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in - List.iter (Option.iter (check_evars env_rec Evd.empty evd)) fixdefs; + List.iter (Option.iter (check_evars (push_named_context rec_sign env) Evd.empty evd)) fixdefs; List.iter (check_evars env Evd.empty evd) fixtypes; if not (List.mem None fixdefs) then begin let fixdefs = List.map Option.get fixdefs in check_mutuality env isfix (List.combine fixnames fixdefs) end; + ((fixnames,fixdefs,fixtypes),info) - (* Build the fix declaration block *) - (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots - -let interp_fixpoint = interp_recursive true -let interp_cofixpoint = interp_recursive false - +let interp_fixpoint l ntns = check_recursive true (interp_recursive true l ntns) +let interp_cofixpoint l ntns = check_recursive false (interp_recursive false l ntns) + let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = if List.mem None fixdefs then (* Some bodies to define by proof *) @@ -803,7 +846,93 @@ let extract_cofixpoint_components l = {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl, List.flatten ntnl +let check_program_evars env initial_sigma evd c = + let sigma = evd in + let c = nf_evar sigma c in + let rec proc_rec c = + match kind_of_term c with + | Evar (evk,args) -> + assert (Evd.mem sigma evk); + if not (Evd.mem initial_sigma evk) then + let (loc,k) = Evd.evar_source evk evd in + (match k with + | Evd.QuestionMark _ + | Evd.ImplicitArg (_, _, false) -> () + | _ -> + let evi = nf_evar_info sigma (Evd.find sigma evk) in + Pretype_errors.error_unsolvable_implicit loc env sigma evi k None) + | _ -> iter_constr proc_rec c + in proc_rec c + +let out_def = function + | Some def -> def + | None -> error "Program Fixpoint needs defined bodies." + +let do_program_recursive fixkind fixl ntns = + let isfix = fixkind <> Obligations.IsCoFixpoint in + let (env, rec_sign, evd), fix, info = + interp_recursive isfix fixl ntns + in + (* Program-specific code *) + (* Get the interesting evars, those that were not instanciated *) + let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env evd in + (* Solve remaining evars *) + let rec collect_evars id def typ imps = + (* Generalize by the recursive prototypes *) + let def = + Termops.it_mkNamedLambda_or_LetIn def rec_sign + and typ = + Termops.it_mkNamedProd_or_LetIn typ rec_sign + in + let evars, _, def, typ = + Obligations.eterm_obligations env id evd (Evd.undefined_evars evd) + (List.length rec_sign) + (nf_evar evd def) (nf_evar evd typ) + in (id, def, typ, imps, evars) + in + let (fixnames,fixdefs,fixtypes) = fix in + let fiximps = List.map pi2 info in + let fixdefs = List.map Option.get fixdefs in + let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in + if isfix then begin + let possible_indexes = List.map compute_possible_guardness_evidences info in + let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), + Array.of_list fixtypes, + Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) + in + let indexes = + Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in + list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl + end; + Obligations.add_mutual_definitions defs ntns fixkind + +let do_program_fixpoint l = + let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in + match g, l with + | [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] -> + let recarg = + match n with + | Some n -> mkIdentC (snd n) + | None -> + errorlabstrm "do_program_fixpoint" + (str "Recursive argument required for well-founded fixpoints") + in build_wellfounded (id, n, bl, typ, out_def def) r recarg ntn + + | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] -> + build_wellfounded (id, n, bl, typ, out_def def) + (Option.default (CRef lt_ref) r) m ntn + + | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g -> + let fixl,ntns = extract_fixpoint_components true l in + let fixkind = Obligations.IsFixpoint g in + do_program_recursive fixkind fixl ntns + + | _, _ -> + errorlabstrm "do_program_fixpoint" + (str "Well-founded fixpoints not allowed in mutually recursive blocks") + let do_fixpoint l = + if Flags.is_program_mode () then do_program_fixpoint l else let fixl,ntns = extract_fixpoint_components true l in let fix = interp_fixpoint fixl ntns in let possible_indexes = @@ -812,4 +941,8 @@ let do_fixpoint l = let do_cofixpoint l = let fixl,ntns = extract_cofixpoint_components l in - declare_cofixpoint (interp_cofixpoint fixl ntns) ntns + if Flags.is_program_mode () then + do_program_recursive Obligations.IsCoFixpoint fixl ntns + else + let cofix = interp_cofixpoint fixl ntns in + declare_cofixpoint cofix ntns diff --git a/toplevel/command.mli b/toplevel/command.mli index 0adc66d56..3cced65f1 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -32,11 +32,15 @@ val set_declare_assumptions_hook : (types -> unit) -> unit val interp_definition : local_binder list -> red_expr option -> constr_expr -> - constr_expr option -> definition_entry * Impargs.manual_implicits + constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits -val declare_definition : identifier -> locality * definition_object_kind -> +val declare_definition : identifier -> definition_kind -> definition_entry -> Impargs.manual_implicits -> 'a declaration_hook -> 'a +val do_definition : identifier -> definition_kind -> + local_binder list -> red_expr option -> constr_expr -> + constr_expr option -> unit declaration_hook -> unit + (** {6 Parameters/Assumptions} *) val interp_assumption : diff --git a/plugins/subtac/subtac_obligations.ml b/toplevel/obligations.ml index 527c5e084..ae25b4fde 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/toplevel/obligations.ml @@ -1,9 +1,6 @@ open Printf open Pp -open Subtac_utils -open Command open Environ - open Term open Names open Libnames @@ -18,6 +15,289 @@ open Declare open Proof_type open Compat +(** + - Get types of existentials ; + - Flatten dependency tree (prefix order) ; + - Replace existentials by De Bruijn indices in term, applied to the right arguments ; + - Apply term prefixed by quantification on "existentials". +*) + +open Term +open Sign +open Names +open Evd +open List +open Pp +open Errors +open Util +open Proof_type + +let declare_fix_ref = ref (fun _ _ _ _ _ -> assert false) +let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false) + +let trace s = + if !Flags.debug then (msgnl s; msgerr s) + else () + +let succfix (depth, fixrels) = + (succ depth, List.map succ fixrels) + +let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n + +let non_instanciated_map env evd evm = + List.fold_left + (fun evm (key, evi) -> + let (loc,k) = evar_source key !evd in + match k with + | QuestionMark _ -> Evd.add evm key evi + | ImplicitArg (_,_,false) -> Evd.add evm key evi + | _ -> + Pretype_errors.error_unsolvable_implicit loc env + evm (Evarutil.nf_evar_info evm evi) k None) + Evd.empty (Evarutil.non_instantiated evm) + +type oblinfo = + { ev_name: int * identifier; + ev_hyps: named_context; + ev_status: obligation_definition_status; + ev_chop: int option; + ev_src: hole_kind located; + ev_typ: types; + ev_tac: tactic option; + ev_deps: Intset.t } + +(* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *) +open Store.Field +let evar_tactic = Store.field () + +(** Substitute evar references in t using De Bruijn indices, + where n binders were passed through. *) + +let subst_evar_constr evs n idf t = + let seen = ref Intset.empty in + let transparent = ref Idset.empty in + let evar_info id = List.assoc id evs in + let rec substrec (depth, fixrels) c = match kind_of_term c with + | Evar (k, args) -> + let { ev_name = (id, idstr) ; + ev_hyps = hyps ; ev_chop = chop } = + try evar_info k + with Not_found -> + anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") + in + seen := Intset.add id !seen; + (* Evar arguments are created in inverse order, + and we must not apply to defined ones (i.e. LetIn's) + *) + let args = + let n = match chop with None -> 0 | Some c -> c in + let (l, r) = list_chop n (List.rev (Array.to_list args)) in + List.rev r + in + let args = + let rec aux hyps args acc = + match hyps, args with + ((_, None, _) :: tlh), (c :: tla) -> + aux tlh tla ((substrec (depth, fixrels) c) :: acc) + | ((_, Some _, _) :: tlh), (_ :: tla) -> + aux tlh tla acc + | [], [] -> acc + | _, _ -> acc (*failwith "subst_evars: invalid argument"*) + in aux hyps args [] + in + if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then + transparent := Idset.add idstr !transparent; + mkApp (idf idstr, Array.of_list args) + | Fix _ -> + map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c + | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c + in + let t' = substrec (0, []) t in + t', !seen, !transparent + + +(** Substitute variable references in t using De Bruijn indices, + where n binders were passed through. *) +let subst_vars acc n t = + let var_index id = Util.list_index id acc in + let rec substrec depth c = match kind_of_term c with + | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c) + | _ -> map_constr_with_binders succ substrec depth c + in + substrec 0 t + +(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ]) + to a product : forall H1 : t1, ..., forall Hn : tn, concl. + Changes evars and hypothesis references to variable references. +*) +let etype_of_evar evs hyps concl = + let rec aux acc n = function + (id, copt, t) :: tl -> + let t', s, trans = subst_evar_constr evs n mkVar t in + let t'' = subst_vars acc 0 t' in + let rest, s', trans' = aux (id :: acc) (succ n) tl in + let s' = Intset.union s s' in + let trans' = Idset.union trans trans' in + (match copt with + Some c -> + let c', s'', trans'' = subst_evar_constr evs n mkVar c in + let c' = subst_vars acc 0 c' in + mkNamedProd_or_LetIn (id, Some c', t'') rest, + Intset.union s'' s', + Idset.union trans'' trans' + | None -> + mkNamedProd_or_LetIn (id, None, t'') rest, s', trans') + | [] -> + let t', s, trans = subst_evar_constr evs n mkVar concl in + subst_vars acc 0 t', s, trans + in aux [] 0 (rev hyps) + + +open Tacticals + +let trunc_named_context n ctx = + let len = List.length ctx in + list_firstn (len - n) ctx + +let rec chop_product n t = + if n = 0 then Some t + else + match kind_of_term t with + | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None + | _ -> None + +let evars_of_evar_info evi = + Intset.union (Evarutil.evars_of_term evi.evar_concl) + (Intset.union + (match evi.evar_body with + | Evar_empty -> Intset.empty + | Evar_defined b -> Evarutil.evars_of_term b) + (Evarutil.evars_of_named_context (evar_filtered_context evi))) + +let evar_dependencies evm oev = + let one_step deps = + Intset.fold (fun ev s -> + let evi = Evd.find evm ev in + let deps' = evars_of_evar_info evi in + if Intset.mem oev deps' then + raise (Invalid_argument ("Ill-formed evar map: cycle detected for evar " ^ string_of_int oev)) + else Intset.union deps' s) + deps deps + in + let rec aux deps = + let deps' = one_step deps in + if Intset.equal deps deps' then deps + else aux deps' + in aux (Intset.singleton oev) + +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) + +open Environ + +let map_evar_info f evi = + { evi with evar_hyps = + val_of_named_context (map_named_context f (named_context_of_val evi.evar_hyps)); + evar_concl = f evi.evar_concl; + evar_body = map_evar_body f evi.evar_body } + +let eterm_obligations env name isevars evm fs ?status t ty = + (* 'Serialize' the evars *) + let nc = Environ.named_context env in + let nc_len = Sign.named_context_length nc in + let evl = List.rev (to_list evm) in + let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in + let sevl = sort_dependencies evl in + let evl = List.map (fun (id, ev, _) -> id, ev) sevl in + let evn = + let i = ref (-1) in + List.rev_map (fun (id, ev) -> incr i; + (id, (!i, id_of_string + (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), + ev)) evl + in + let evts = + (* Remove existential variables in types and build the corresponding products *) + fold_right + (fun (id, (n, nstr), ev) l -> + let hyps = Evd.evar_filtered_context ev in + let hyps = trunc_named_context nc_len hyps in + let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in + let evtyp, hyps, chop = + match chop_product fs evtyp with + | Some t -> t, trunc_named_context fs hyps, fs + | None -> evtyp, hyps, 0 + in + let loc, k = evar_source id isevars in + let status = match k with QuestionMark o -> Some o | _ -> status in + let status, chop = match status with + | Some (Define true as stat) -> + if chop <> fs then Define false, None + else stat, Some chop + | Some s -> s, None + | None -> Define true, None + in + let tac = match evar_tactic.get ev.evar_extra with + | Some t -> + if Dyn.tag t = "tactic" then + Some (Tacinterp.interp + (Tacinterp.globTacticIn (Tacinterp.tactic_out t))) + else None + | None -> None + in + let info = { ev_name = (n, nstr); + ev_hyps = hyps; ev_status = status; ev_chop = chop; + ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac } + in (id, info) :: l) + evn [] + in + let t', _, transparent = (* Substitute evar refs in the term by variables *) + subst_evar_constr evts 0 mkVar t + in + let ty, _, _ = subst_evar_constr evts 0 mkVar ty in + let evars = + List.map (fun (ev, info) -> + let { ev_name = (_, name); ev_status = status; + ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info + in + let status = match status with + | Define true when Idset.mem name transparent -> Define false + | _ -> status + in name, typ, src, status, deps, tac) evts + in + let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in + let evmap f c = pi1 (subst_evar_constr evts 0 f c) in + Array.of_list (List.rev evars), (evnames, evmap), t', ty + +let tactics_module = ["Program";"Tactics"] +let safe_init_constant md name () = + Coqlib.check_required_library ("Coq"::md); + Coqlib.gen_constant "Obligations" md name +let fix_proto = safe_init_constant tactics_module "fix_proto" +let hide_obligation = safe_init_constant tactics_module "obligation" + let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) let pperror cmd = Errors.errorlabstrm "Program" cmd let error s = pperror (str s) @@ -63,7 +343,7 @@ type program_info = { prg_notations : notations ; prg_kind : definition_kind; prg_reduce : constr -> constr; - prg_hook : Tacexpr.declaration_hook; + prg_hook : unit Tacexpr.declaration_hook; } let assumption_message id = @@ -211,10 +491,11 @@ let progmap_union = ProgMap.fold ProgMap.add let close sec = if not (ProgMap.is_empty !from_prg) then let keys = map_keys !from_prg in - errorlabstrm "Program" (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++ - prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++ - (str (if List.length keys = 1 then " has " else "have ") ++ - str "unsolved obligations")) + errorlabstrm "Program" + (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++ + prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++ + (str (if List.length keys = 1 then " has " else "have ") ++ + str "unsolved obligations")) let input : program_info ProgMap.t -> obj = declare_object @@ -246,38 +527,15 @@ let subst_body expand prg = let declare_definition prg = let body, typ = subst_body true prg in - let (local, kind) = prg.prg_kind in let ce = { const_entry_body = body; const_entry_secctx = None; const_entry_type = Some typ; const_entry_opaque = false } in - (Command.get_declare_definition_hook ()) ce; - match local with - | Local when Lib.sections_are_opened () -> - let c = - SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in - let _ = declare_variable prg.prg_name (Lib.cwd(),c,IsDefinition kind) in - print_message (Subtac_utils.definition_message prg.prg_name); - if Pfedit.refining () then - Flags.if_verbose msg_warning - (str"Local definition " ++ Nameops.pr_id prg.prg_name ++ - str" is not visible from current goals"); - progmap_remove prg; - VarRef prg.prg_name - | (Global|Local) -> - let c = - Declare.declare_constant - prg.prg_name (DefinitionEntry ce,IsDefinition (snd prg.prg_kind)) - in - let gr = ConstRef c in - if Impargs.is_implicit_args () || prg.prg_implicits <> [] then - Impargs.declare_manual_implicits false gr [prg.prg_implicits]; - print_message (Subtac_utils.definition_message prg.prg_name); - progmap_remove prg; - prg.prg_hook local gr; - gr + progmap_remove prg; + !declare_definition_ref prg.prg_name prg.prg_kind ce prg.prg_implicits + (fun local gr -> prg.prg_hook local gr; gr) open Pp open Ppconstr @@ -331,7 +589,7 @@ let declare_mutual_definition l = None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l in (* Declare the recursive definitions *) - let kns = list_map4 (declare_fix kind) fixnames fixdecls fixtypes fiximps in + let kns = list_map4 (!declare_fix_ref kind) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter Metasyntax.add_notation_interpretation first.prg_notations; Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames; @@ -359,7 +617,7 @@ let declare_obligation prg obl body = if not opaque then Auto.add_hints false [string_of_id prg.prg_name] (Auto.HintsUnfoldEntry [EvalConstRef constant]); - print_message (Subtac_utils.definition_message obl.obl_name); + definition_message obl.obl_name; { obl with obl_body = Some (mkConst constant) } let init_prog_info n b t deps fixkind notations obls impls kind reduce hook = @@ -380,7 +638,8 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook = obl_deps = d; obl_tac = tac }) obls, b in - { prg_name = n ; prg_body = b; prg_type = reduce 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_reduce = reduce; prg_hook = hook; } @@ -455,10 +714,19 @@ let dependencies obls n = obls; !res +let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition +let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition + +let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma +let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma + +let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint +let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint + let kind_of_opacity o = match o with - | Define false | Expand -> Subtac_utils.goal_kind - | _ -> Subtac_utils.goal_proof_kind + | Define false | Expand -> goal_kind + | _ -> goal_proof_kind let not_transp_msg = str "Obligation should be transparent but was declared opaque." ++ spc () ++ @@ -467,6 +735,27 @@ let not_transp_msg = let warn_not_transp () = ppwarn not_transp_msg let error_not_transp () = pperror not_transp_msg +let rec string_of_list sep f = function + [] -> "" + | x :: [] -> f x + | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl + +(* Solve an obligation using tactics, return the corresponding proof term *) +let solve_by_tac evi t = + let id = id_of_string "H" in + try + Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl + (fun _ _ -> ()); + Pfedit.by (tclCOMPLETE t); + let _,(const,_,_,_) = Pfedit.cook_proof ignore in + Pfedit.delete_current_proof (); + Inductiveops.control_only_guard (Global.env ()) + const.Entries.const_entry_body; + const.Entries.const_entry_body + with e -> + Pfedit.delete_current_proof(); + raise e + let rec solve_obligation prg num tac = let user_num = succ num in let obls, rem = prg.prg_obligations in @@ -508,12 +797,12 @@ let rec solve_obligation prg num tac = ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps) | _ -> ()); trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ - Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); + Printer.pr_constr_env (Global.env ()) obl.obl_type); 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) " - ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) + ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) and subtac_obligation (user_num, name, typ) tac = let num = pred user_num in @@ -543,7 +832,7 @@ and solve_obligation_by_tac prg obls i tac = | Some t -> t | None -> snd (get_default_tactic ()) in - let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in + let t = solve_by_tac (evar_of_obligation obl) tac in obls.(i) <- declare_obligation prg obl t; true else false @@ -605,7 +894,8 @@ let show_obligations_of_prg ?(msg=true) prg = decr showed; msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ - hov 1 (my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ()))) + hov 1 (Printer.pr_constr_env (Global.env ()) x.obl_type ++ + str "." ++ fnl ()))) | Some _ -> ()) obls @@ -621,8 +911,8 @@ let show_term n = let prg = get_prog_err n in let n = prg.prg_name in msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ - my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl () - ++ my_print_constr (Global.env ()) prg.prg_body) + Printer.pr_constr_env (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl () + ++ Printer.pr_constr_env (Global.env ()) prg.prg_body) let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls = @@ -656,7 +946,9 @@ let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce) else let res = auto_solve_obligations (Some x) tactic in match res with - | Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true + | Defined _ -> + (* If one definition is turned into a constant, + the whole block is defined. *) true | _ -> false) false deps in () diff --git a/plugins/subtac/subtac_obligations.mli b/toplevel/obligations.mli index 284e975db..de020f8e3 100644 --- a/plugins/subtac/subtac_obligations.mli +++ b/toplevel/obligations.mli @@ -1,10 +1,55 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Environ +open Tacmach +open Term +open Evd open Names open Pp open Util +open Tacinterp open Libnames -open Evd open Proof_type open Vernacexpr +open Decl_kinds +open Tacexpr + +(** Forward declaration. *) +val declare_fix_ref : (definition_object_kind -> identifier -> + constr -> types -> Impargs.manual_implicits -> global_reference) ref + +val declare_definition_ref : + (identifier -> locality * definition_object_kind -> + Entries.definition_entry -> Impargs.manual_implicits + -> global_reference declaration_hook -> global_reference) ref + +val non_instanciated_map : env -> evar_map ref -> evar_map -> evar_map + +val mkMetas : int -> constr list + +val evar_dependencies : evar_map -> int -> Intset.t +val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * Intset.t) list + +(* env, id, evars, number of function prototypes to try to clear from + evars contexts, object and type *) +val eterm_obligations : env -> identifier -> evar_map -> evar_map -> int -> + ?status:obligation_definition_status -> constr -> types -> + (identifier * types * hole_kind located * obligation_definition_status * Intset.t * + tactic option) array + (* Existential key, obl. name, type as product, + location of the original evar, associated tactic, + status and dependencies as indexes into the array *) + * ((existential_key * identifier) list * ((identifier -> constr) -> constr -> constr)) * + constr * types + (* Translations from existential identifiers to obligation identifiers + and for terms with existentials to closed terms, given a + translation from obligation identifiers to constrs, new term, new type *) type obligation_info = (identifier * Term.types * hole_kind located * @@ -29,7 +74,7 @@ val add_definition : Names.identifier -> ?term:Term.constr -> Term.types -> ?kind:Decl_kinds.definition_kind -> ?tactic:Proof_type.tactic -> ?reduce:(Term.constr -> Term.constr) -> - ?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress + ?hook:(unit Tacexpr.declaration_hook) -> obligation_info -> progress type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list @@ -43,7 +88,7 @@ val add_mutual_definitions : ?tactic:Proof_type.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(Term.constr -> Term.constr) -> - ?hook:Tacexpr.declaration_hook -> + ?hook:unit Tacexpr.declaration_hook -> notations -> fixpoint_kind -> unit @@ -70,4 +115,3 @@ val admit_obligations : Names.identifier option -> unit exception NoObligations of Names.identifier option val explain_no_obligations : Names.identifier option -> Pp.std_ppcmds - diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 7d891997b..2ca2f0739 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -17,6 +17,7 @@ Ppvernac Vernacinterp Mltop Vernacentries +G_obligations Whelp Vernac Ide_intf diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7a7246733..20c9531fe 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -343,8 +343,7 @@ let vernac_definition (local,k) (loc,id as lid) def hook = | Some r -> let (evc,env)= get_current_context () in Some (interp_redexp env evc r) in - let ce,imps = interp_definition bl red_option c typ_opt in - declare_definition id (local,k) ce imps hook) + do_definition id (local,k) bl red_option c typ_opt hook) let vernac_start_proof kind l lettop hook = if Dumpglob.dump () then @@ -1578,5 +1577,12 @@ let interp c = match c with (* Extensions *) | VernacExtend (opn,args) -> Vernacinterp.call (opn,args) -let interp c = interp c ; check_locality () +let interp c = + let mode = Flags.is_program_mode () in + let flag = mode || !program_flag in + Flags.program_mode := flag; + interp c; check_locality (); + program_flag := false; + Flags.program_mode := mode + (* with_program_flag (fun () -> interp c ; check_locality ()) *) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 31d04fcfa..e49cd3b66 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -128,7 +128,8 @@ type verbose_flag = bool (* true = Verbose; false = Silent *) type opacity_flag = bool (* true = Opaque; false = Transparent *) type locality_flag = bool (* true = Local; false = Global *) type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) -type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) +type instance_flag = bool option + (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) type inductive_flag = Decl_kinds.recursivity_kind type onlyparsing_flag = bool (* true = Parse only; false = Print also *) @@ -481,3 +482,16 @@ let enforce_module_locality local = (**********************************************************************) +(**********************************************************************) +(* Managing the Program extension. *) + +let program_flag = ref false +let with_program_flag m = + if Flags.is_program_mode () then + (program_flag := false; m ()) + else if !program_flag then + (Flags.program_mode := true; + m (); + Flags.program_mode := false; + program_flag := false) + |