diff options
| -rw-r--r-- | contrib/subtac/eterm.ml | 51 | ||||
| -rw-r--r-- | contrib/subtac/subtac.ml | 3 | ||||
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 5 | ||||
| -rw-r--r-- | contrib/subtac/subtac_command.mli | 127 | ||||
| -rw-r--r-- | contrib/subtac/subtac_interp_fixpoint.ml | 6 | ||||
| -rw-r--r-- | contrib/subtac/subtac_interp_fixpoint.mli | 3 | ||||
| -rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 3 | ||||
| -rw-r--r-- | contrib/subtac/subtac_utils.mli | 104 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 36 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 5 |
10 files changed, 174 insertions, 169 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 66a2b3601..ced1756f1 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -24,27 +24,43 @@ let list_index x l = let list_assoc_index x l = let rec aux i = function - (k, v) :: tl -> if k = x then i else aux (succ i) tl + (k, _, v) :: tl -> if k = x then i else aux (succ i) tl | [] -> raise Not_found in aux 0 l (** Substitute evar references in t using De Bruijn indices, where n binders were passed through. *) let subst_evars evs n t = - let evar_index id = - let idx = list_assoc_index id evs in - idx + 1 + let evar_info id = + let rec aux i = function + (k, h, v) :: tl -> if k = id then (i, h, v) else aux (succ i) tl + | [] -> raise Not_found + in + let (idx, hyps, v) = aux 0 evs in + idx + 1, hyps in let rec substrec depth c = match kind_of_term c with | Evar (k, args) -> (try - msgnl (str "Evar " ++ int k ++ str " found"); - let ex = -(* mkVar (id_of_string ("Evar" ^ string_of_int k));*) - mkRel (evar_index k + depth) + let index, hyps = evar_info k in + msgnl (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++ + int (List.length hyps) ++ str " hypotheses"); + + let ex = mkRel (index + depth) in + (* Evar arguments are created in inverse order, + and we must not apply to defined ones (i.e. LetIn's) + *) + let args = + let rec aux hyps args acc = + match hyps, args with + ((_, None, _) :: tlh), (c :: tla) -> + aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc) + | ((_, Some _, _) :: tlh), (_ :: tla) -> + aux tlh tla acc + | [], [] -> acc + | _, _ -> failwith "subst_evars: invalid argument" + in aux hyps (Array.to_list args) [] in - (* Evar arguments are created in inverse order *) - let args = List.rev_map (map_constr_with_binders succ substrec depth) (Array.to_list args) in mkApp (ex, Array.of_list args) with Not_found -> msgnl (str "Evar " ++ int k ++ str " not found!!!"); @@ -70,7 +86,7 @@ let subst_vars acc n t = to a product : forall H1 : t1, ..., forall Hn : tn, concl. Changes evars and hypothesis references to De Bruijn indices. *) -let etype_of_evar evs ev = +let etype_of_evar evs ev hyps = let rec aux acc n = function (id, copt, t) :: tl -> let t' = subst_evars evs n t in @@ -79,7 +95,7 @@ let etype_of_evar evs ev = | [] -> let t' = subst_evars evs n ev.evar_concl in subst_vars acc 0 t' - in aux [] 0 (rev (Environ.named_context_of_val ev.evar_hyps)) + in aux [] 0 (rev hyps) open Tacticals @@ -91,8 +107,9 @@ let eterm evm t = let evts = (* Remove existential variables in types and build the corresponding products *) fold_left - (fun l (id, y) -> - let y' = (id, etype_of_evar l y) in + (fun l (id, ev) -> + let hyps = Environ.named_context_of_val ev.evar_hyps in + let y' = (id, hyps, etype_of_evar l ev hyps) in y' :: l) [] evl in @@ -102,7 +119,7 @@ let eterm evm t = let t'' = (* Make the lambdas 'generalizing' the existential variables *) fold_left - (fun acc (id, c) -> + (fun acc (id, _, c) -> mkLambda (Name (id_of_string ("Evar" ^ string_of_int id)), c, acc)) t' evts @@ -116,7 +133,9 @@ let eterm evm t = let id = id_of_string ("Evar" ^ string_of_int id) in tclTHEN acc (Tactics.assert_tac false (Name id) c) in - msgnl (str "Term constructed in Eterm" ++ + msgnl (str "Term given to eterm" ++ spc () ++ + Termops.print_constr_env (Global.env ()) t); + msgnl (str "Term constructed in eterm" ++ spc () ++ Termops.print_constr_env (Global.env ()) t''); Tactics.apply_term t'' (List.map (fun _ -> Evarutil.mk_new_meta ()) evts) diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 12755960e..01c959a47 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -114,6 +114,7 @@ let subtac_end_proof = function | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id *) + let subtac (loc, command) = check_required_library ["Coq";"Init";"Datatypes"]; check_required_library ["Coq";"Init";"Specif"]; @@ -139,7 +140,7 @@ let subtac (loc, command) = Pfedit.by tac) | VernacFixpoint (l, b) -> let _ = trace (str "Building fixpoint") in - ignore(Subtac_command.build_recursive l b) + ignore(Subtac_command.build_recursive l b) (*| VernacEndProof e -> subtac_end_proof e*) diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 64aee7611..5659950bc 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -50,8 +50,9 @@ let interp_gen kind isevars env ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in - let c'' = Subtac_interp_fixpoint.rewrite_cases c' in - Evd.evars_of !isevars, SPretyping.pretype_gen isevars env ([],[]) kind c'' + let c' = Subtac_interp_fixpoint.rewrite_cases env c' in + let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in + non_instanciated_map env isevars, c' let interp_constr isevars env c = interp_gen (OfType None) isevars env c diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli index 23a03290c..6c1b0103f 100644 --- a/contrib/subtac/subtac_command.mli +++ b/contrib/subtac/subtac_command.mli @@ -1,103 +1,42 @@ -module SPretyping : - sig - module Cases : - sig - val compile_cases : - Util.loc -> - (Evarutil.type_constraint -> - Environ.env -> Rawterm.rawconstr -> Environ.unsafe_judgment) * - Evd.evar_defs ref -> - Evarutil.type_constraint -> - Environ.env -> - Rawterm.rawconstr option * - (Rawterm.rawconstr * - (Names.name * - (Util.loc * Names.inductive * Names.name list) option)) - list * - (Util.loc * Names.identifier list * Rawterm.cases_pattern list * - Rawterm.rawconstr) - list -> Environ.unsafe_judgment - end - val understand_tcc : - Evd.evar_map -> - Environ.env -> - ?expected_type:Term.types -> Rawterm.rawconstr -> Evd.open_constr - val understand_ltac : - Evd.evar_map -> - Environ.env -> - Pretyping.var_map * Pretyping.unbound_ltac_var_map -> - Pretyping.typing_constraint -> - Rawterm.rawconstr -> Evd.evar_defs * Term.constr - val understand : - Evd.evar_map -> - Environ.env -> - ?expected_type:Term.types -> Rawterm.rawconstr -> Term.constr - val understand_type : - Evd.evar_map -> Environ.env -> Rawterm.rawconstr -> Term.constr - val understand_gen : - Pretyping.typing_constraint -> - Evd.evar_map -> Environ.env -> Rawterm.rawconstr -> Term.constr - val understand_judgment : - Evd.evar_map -> - Environ.env -> Rawterm.rawconstr -> Environ.unsafe_judgment - val understand_judgment_tcc : - Evd.evar_map -> - Environ.env -> - Rawterm.rawconstr -> Evd.evar_map * Environ.unsafe_judgment - val pretype : - Evarutil.type_constraint -> - Environ.env -> - Evd.evar_defs ref -> - Pretyping.var_map * (Names.identifier * Names.identifier option) list -> - Rawterm.rawconstr -> Environ.unsafe_judgment - val pretype_type : - Evarutil.val_constraint -> - Environ.env -> - Evd.evar_defs ref -> - Pretyping.var_map * (Names.identifier * Names.identifier option) list -> - Rawterm.rawconstr -> Environ.unsafe_type_judgment - val pretype_gen : - Evd.evar_defs ref -> - Environ.env -> - Pretyping.var_map * (Names.identifier * Names.identifier option) list -> - Pretyping.typing_constraint -> Rawterm.rawconstr -> Term.constr - end +open Pretyping +open Evd +open Environ +open Term +open Topconstr +open Names +open Libnames +open Pp +open Vernacexpr +open Constrintern + val interp_gen : - Pretyping.typing_constraint -> - Evd.evar_defs ref -> - Environ.env -> - ?impls:Constrintern.full_implicits_env -> + typing_constraint -> + evar_defs ref -> + env -> + ?impls:full_implicits_env -> ?allow_soapp:bool -> - ?ltacvars:Constrintern.ltac_sign -> - Topconstr.constr_expr -> Evd.evar_map * Term.constr + ?ltacvars:ltac_sign -> + constr_expr -> evar_map * constr val interp_constr : - Evd.evar_defs ref -> - Environ.env -> Topconstr.constr_expr -> Evd.evar_map * Term.constr + evar_defs ref -> + env -> constr_expr -> evar_map * constr val interp_type : - Evd.evar_defs ref -> - Environ.env -> - ?impls:Constrintern.full_implicits_env -> - Topconstr.constr_expr -> Evd.evar_map * Term.constr + evar_defs ref -> + env -> + ?impls:full_implicits_env -> + constr_expr -> evar_map * constr val interp_casted_constr : - Evd.evar_defs ref -> - Environ.env -> - ?impls:Constrintern.full_implicits_env -> - Topconstr.constr_expr -> Term.types -> Evd.evar_map * Term.constr + evar_defs ref -> + env -> + ?impls:full_implicits_env -> + constr_expr -> types -> evar_map * constr val interp_open_constr : - Evd.evar_defs ref -> Environ.env -> Topconstr.constr_expr -> Term.constr + evar_defs ref -> env -> constr_expr -> constr val interp_constr_judgment : - Evd.evar_defs ref -> - Environ.env -> - Topconstr.constr_expr -> Evd.evar_defs * Environ.unsafe_judgment + evar_defs ref -> + env -> + constr_expr -> evar_defs * unsafe_judgment val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list -val collect_non_rec : - Environ.env -> - Names.identifier list -> - ('a * Term.types) list -> - 'b list -> - 'c list -> - (Names.identifier * ('a * Term.types) * 'b) list * - (Names.identifier array * ('a * Term.types) array * 'b array * 'c array) -val recursive_message : Libnames.global_reference array -> Pp.std_ppcmds +val recursive_message : global_reference array -> std_ppcmds val build_recursive : - (Topconstr.fixpoint_expr * Vernacexpr.decl_notation) list -> bool -> unit + (fixpoint_expr * decl_notation) list -> bool -> unit diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml index c668c3503..3ed5790e3 100644 --- a/contrib/subtac/subtac_interp_fixpoint.ml +++ b/contrib/subtac/subtac_interp_fixpoint.ml @@ -183,7 +183,7 @@ let rewrite_cases_aux (loc, po, tml, eqns) = let c' = List.fold_left (fun acc (n, t) -> - RLambda (dummy_loc, n, t, acc)) + RLambda (dummy_loc, n, mkHole, acc)) c eqs_types in (loc, idl, cpl, c')) eqns @@ -204,3 +204,7 @@ let rec rewrite_cases c = | _ -> assert(false)) | _ -> map_rawconstr rewrite_cases c +let rewrite_cases env c = + let c' = rewrite_cases c in + let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in + c' diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli index 5a84b2773..ef551aa8d 100644 --- a/contrib/subtac/subtac_interp_fixpoint.mli +++ b/contrib/subtac/subtac_interp_fixpoint.mli @@ -39,4 +39,5 @@ val rewrite_cases_aux : (Util.loc * Names.identifier list * Rawterm.cases_pattern list * Rawterm.rawconstr) list -> Rawterm.rawconstr -val rewrite_cases : Rawterm.rawconstr -> Rawterm.rawconstr + +val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 8dd6f9b8f..5cc735185 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -40,8 +40,11 @@ open Context open Eterm module Pretyping = Pretyping.Pretyping_F(Subtac_coercion.Coercion) + open Pretyping +let _ = Pretyping.allow_anonymous_refs := true + type recursion_info = { arg_name: name; arg_type: types; (* A *) diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 5bbd4639e..84001c374 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -1,53 +1,63 @@ +open Term +open Libnames +open Coqlib +open Environ +open Pp +open Evd +open Decl_kinds +open Topconstr +open Rawterm +open Util + val contrib_name : string val subtac_dir : string list val fix_sub_module : string val fixsub_module : string list -val init_constant : string list -> string -> Term.constr -val init_reference : string list -> string -> Libnames.global_reference -val fixsub : Term.constr lazy_t -val make_ref : string -> Libnames.reference -val well_founded_ref : Libnames.reference -val acc_ref : Libnames.reference -val acc_inv_ref : Libnames.reference -val fix_sub_ref : Libnames.reference -val lt_wf_ref : Libnames.reference -val sig_ref : Libnames.reference -val proj1_sig_ref : Libnames.reference -val proj2_sig_ref : Libnames.reference -val build_sig : unit -> Coqlib.coq_sigma_data -val sig_ : Coqlib.coq_sigma_data lazy_t -val eqind : Term.constr lazy_t -val eqind_ref : Libnames.global_reference lazy_t -val refl_equal_ref : Libnames.global_reference lazy_t -val boolind : Term.constr lazy_t -val sumboolind : Term.constr lazy_t -val natind : Term.constr lazy_t -val intind : Term.constr lazy_t -val existSind : Term.constr lazy_t -val existS : Coqlib.coq_sigma_data lazy_t -val well_founded : Term.constr lazy_t -val fix : Term.constr lazy_t -val extconstr : Term.constr -> Topconstr.constr_expr -val extsort : Term.sorts -> Topconstr.constr_expr -val my_print_constr : Environ.env -> Term.constr -> Pp.std_ppcmds -val my_print_context : Environ.env -> Pp.std_ppcmds -val my_print_env : Environ.env -> Pp.std_ppcmds -val my_print_rawconstr : Environ.env -> Rawterm.rawconstr -> Pp.std_ppcmds +val init_constant : string list -> string -> constr +val init_reference : string list -> string -> global_reference +val fixsub : constr lazy_t +val make_ref : string -> reference +val well_founded_ref : reference +val acc_ref : reference +val acc_inv_ref : reference +val fix_sub_ref : reference +val lt_wf_ref : reference +val sig_ref : reference +val proj1_sig_ref : reference +val proj2_sig_ref : reference +val build_sig : unit -> coq_sigma_data +val sig_ : coq_sigma_data lazy_t +val eqind : constr lazy_t +val eqind_ref : global_reference lazy_t +val refl_equal_ref : global_reference lazy_t +val boolind : constr lazy_t +val sumboolind : constr lazy_t +val natind : constr lazy_t +val intind : constr lazy_t +val existSind : constr lazy_t +val existS : coq_sigma_data lazy_t +val well_founded : constr lazy_t +val fix : constr lazy_t +val extconstr : constr -> constr_expr +val extsort : sorts -> constr_expr +val my_print_constr : env -> constr -> std_ppcmds +val my_print_context : env -> std_ppcmds +val my_print_env : env -> std_ppcmds +val my_print_rawconstr : env -> rawconstr -> std_ppcmds val debug_level : int ref -val debug : int -> Pp.std_ppcmds -> unit -val debug_msg : int -> Pp.std_ppcmds -> Pp.std_ppcmds -val trace : Pp.std_ppcmds -> unit -val wf_relations : (Term.constr, Term.constr lazy_t) Hashtbl.t -val std_relations : unit Lazy.t -type binders = Topconstr.local_binder list +val debug : int -> std_ppcmds -> unit +val debug_msg : int -> std_ppcmds -> std_ppcmds +val trace : std_ppcmds -> unit +val wf_relations : (constr, constr lazy_t) Hashtbl.t + +type binders = local_binder list val app_opt : ('a -> 'a) option -> 'a -> 'a -val print_args : Environ.env -> Term.constr array -> Pp.std_ppcmds -val make_existential : - Util.loc -> Environ.env -> Evd.evar_defs ref -> Term.types -> Term.constr -val make_existential_expr : Util.loc -> 'a -> 'b -> Topconstr.constr_expr -val string_of_hole_kind : Evd.hole_kind -> string -val non_instanciated_map : Environ.env -> Evd.evar_defs ref -> Evd.evar_map -val global_kind : Decl_kinds.logical_kind -val goal_kind : Decl_kinds.locality_flag * Decl_kinds.goal_object_kind -val global_fix_kind : Decl_kinds.logical_kind -val goal_fix_kind : Decl_kinds.locality_flag * Decl_kinds.goal_object_kind +val print_args : env -> constr array -> std_ppcmds +val make_existential : loc -> env -> evar_defs ref -> types -> constr +val make_existential_expr : loc -> 'a -> 'b -> constr_expr +val string_of_hole_kind : hole_kind -> string +val non_instanciated_map : env -> evar_defs ref -> evar_map +val global_kind : logical_kind +val goal_kind : locality_flag * goal_object_kind +val global_fix_kind : logical_kind +val goal_fix_kind : locality_flag * goal_object_kind diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 14326bf44..68342e706 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -63,6 +63,9 @@ sig module Cases : Cases.S + (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) + val allow_anonymous_refs : bool ref + (* Generic call to the interpreter from rawconstr to open_constr, leaving unresolved holes as evars and returning the typing contexts of these evars. Work as [understand_gen] for the rest. *) @@ -134,6 +137,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct module Cases = Cases.Cases_F(Coercion) + (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) + let allow_anonymous_refs = ref false + let evd_comb0 f isevars = let (evd',x) = f !isevars in isevars := evd'; @@ -422,8 +428,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct (List.rev nal) cs.cs_args in let env_f = push_rels fsign env in (* Make dependencies from arity signature impossible *) - let arsgn,_ = get_arity env indf in - let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in + let arsgn = + let arsgn,_ = get_arity env indf in + if not !allow_anonymous_refs then + List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn + else arsgn + in let psign = (na,None,build_dependent_inductive env indf)::arsgn in let nar = List.length arsgn in (match po with @@ -477,9 +487,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct user_err_loc (loc,"", str "If is only for inductive types with two constructors"); - (* Make dependencies from arity signature impossible *) - let arsgn,_ = get_arity env indf in - let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in + let arsgn = + let arsgn,_ = get_arity env indf in + if not !allow_anonymous_refs then + (* Make dependencies from arity signature impossible *) + List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn + else arsgn + in let nar = List.length arsgn in let psign = (na,None,build_dependent_inductive env indf)::arsgn in let pred,p = match po with @@ -500,7 +514,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct let n = rel_context_length cs.cs_args in let pi = liftn n 2 pred in let pi = beta_applist (pi, [build_dependent_constructor cs]) in - let csgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args in + let csgn = + if not !allow_anonymous_refs then + List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args + else + List.map + (fun (n, b, t) -> + match n with + Name _ -> (n, b, t) + | Anonymous -> (Name (id_of_string "H"), b, t)) + cs.cs_args + in let env_c = push_rels csgn env in let bj = pretype (Some pi) env_c isevars lvar b in it_mkLambda_or_LetIn bj.uj_val cs.cs_args in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index f93e46129..ac8e6fec7 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -27,7 +27,10 @@ module type S = sig module Cases : Cases.S - + + (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) + val allow_anonymous_refs : bool ref + (* Generic call to the interpreter from rawconstr to open_constr, leaving unresolved holes as evars and returning the typing contexts of these evars. Work as [understand_gen] for the rest. *) |