aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac')
-rw-r--r--contrib/subtac/eterm.ml5
-rw-r--r--contrib/subtac/eterm.mli6
-rw-r--r--contrib/subtac/g_subtac.ml421
-rw-r--r--contrib/subtac/subtac.ml52
-rw-r--r--contrib/subtac/subtac_cases.ml14
-rw-r--r--contrib/subtac/subtac_classes.ml187
-rw-r--r--contrib/subtac/subtac_classes.mli39
-rw-r--r--contrib/subtac/subtac_command.ml28
-rw-r--r--contrib/subtac/subtac_obligations.ml103
-rw-r--r--contrib/subtac/subtac_obligations.mli13
-rw-r--r--contrib/subtac/subtac_pretyping.ml46
-rw-r--r--contrib/subtac/subtac_pretyping.mli10
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml43
-rw-r--r--contrib/subtac/subtac_utils.ml22
14 files changed, 447 insertions, 142 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index d1b4b50eb..9cb65f76e 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -121,7 +121,7 @@ let rec chop_product n t =
| Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
| _ -> None
-let eterm_obligations env name isevars evm fs t tycon =
+let eterm_obligations env name isevars evm fs t ty =
(* 'Serialize' the evars, we assume that the types of the existentials
refer to previous existentials in the list only *)
trace (str " In eterm: isevars: " ++ my_print_evardefs isevars);
@@ -165,6 +165,7 @@ let eterm_obligations env name isevars evm fs t tycon =
let t', _, transparent = (* Substitute evar refs in the term by variables *)
subst_evar_constr evts 0 t
in
+ let ty, _, _ = subst_evar_constr evts 0 ty in
let evars =
List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None) && not (Idset.mem name transparent), deps) evts
in
@@ -177,7 +178,7 @@ let eterm_obligations env name isevars evm fs t tycon =
Termops.print_constr_env (Global.env ()) typ))
evars);
with _ -> ());
- Array.of_list (List.rev evars), t'
+ Array.of_list (List.rev evars), t', ty
let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index a2582c5ca..e23fd535c 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -19,9 +19,9 @@ val mkMetas : int -> constr list
(* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *)
(* env, id, evars, number of
- function prototypes to try to clear from evars contexts, object and optional type *)
-val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types option ->
- (identifier * types * bool * Intset.t) array * constr
+ function prototypes to try to clear from evars contexts, object and type *)
+val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types ->
+ (identifier * types * bool * Intset.t) array * constr * types
(* Obl. name, type as product, opacity (true = opaque) and dependencies as indexes into the array *)
val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index c2691c781..49e312aeb 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -44,17 +44,20 @@ struct
let subtac_nameopt : identifier option Gram.Entry.e = gec "subtac_nameopt"
end
+open Rawterm
open SubtacGram
open Util
open Pcoq
-
+open Prim
+open Constr
let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
GEXTEND Gram
- GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder subtac_nameopt;
+ GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder_let Constr.binder subtac_nameopt;
subtac_gallina_loc:
- [ [ g = Vernac.gallina -> loc, g ] ]
+ [ [ g = Vernac.gallina -> loc, g
+ | g = Vernac.gallina_ext -> loc, g ] ]
;
subtac_nameopt:
@@ -63,18 +66,18 @@ GEXTEND Gram
;
Constr.binder_let:
- [ [ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
- let typ = mkAppC (sigref, [mkLambdaC ([id], t, c)]) in
- LocalRawAssum ([id], typ)
+ [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
+ let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
+ LocalRawAssum ([id], default_binder_kind, typ)
] ];
Constr.binder:
[ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" ->
- ([id],mkAppC (sigref, [mkLambdaC ([id], c, p)]))
+ ([id],default_binder_kind, mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, c, p)]))
| "("; id=Prim.name; ":"; c=Constr.lconstr; ")" ->
- ([id],c)
+ ([id],default_binder_kind, c)
| "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" ->
- (id::lid,c)
+ (id::lid,default_binder_kind, c)
] ];
END
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 4f5e302c2..56ebc4f52 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -49,6 +49,22 @@ open Decl_kinds
open Tacinterp
open Tacexpr
+let solve_tccs_in_type env id isevars evm c typ =
+ if not (evm = Evd.empty) then
+ let stmt_id = Nameops.add_suffix id "_stmt" in
+ let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 c typ in
+ (** Make all obligations transparent so that real dependencies can be sorted out by the user *)
+ let obls = Array.map (fun (id, t, op, d) -> (id, t, false, d)) obls in
+ match Subtac_obligations.add_definition stmt_id c' typ obls with
+ Subtac_obligations.Defined cst -> constant_value (Global.env()) cst
+ | _ ->
+ 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 id ->
@@ -60,21 +76,11 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
next_global_ident_away false (id_of_string "Unnamed_thm")
(Pfedit.get_all_proof_names ())
in
- let evm, c, typ =
+ let evm, c, typ, _imps =
Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None
in
- if not (evm = Evd.empty) then
- let stmt_id = Nameops.add_suffix id "_stmt" in
- let obls, c' = eterm_obligations env stmt_id !isevars evm 0 c (Some typ) in
- match Subtac_obligations.add_definition stmt_id c' typ obls with
- Subtac_obligations.Defined cst -> Command.start_proof id kind (constant_value (Global.env()) cst) hook
- | _ ->
- 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
- Command.start_proof id kind c hook
+ let c = solve_tccs_in_type env id isevars evm c typ in
+ Command.start_proof id kind c hook
let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
@@ -88,10 +94,12 @@ let assumption_message id =
Flags.if_verbose message ((string_of_id id) ^ " is assumed")
let declare_assumption env isevars idl is_coe k bl c nl =
- if not (Pfedit.refining ()) then
- let evm, c, typ =
- Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None
+ if not (Pfedit.refining ()) then
+ let id = snd (List.hd idl) in
+ let evm, c, typ, imps =
+ Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None
in
+ let c = solve_tccs_in_type env id isevars evm c typ in
List.iter (Command.declare_one_assumption is_coe k c nl) idl
else
errorlabstrm "Command.Assumption"
@@ -114,8 +122,13 @@ let subtac (loc, command) =
match command with
VernacDefinition (defkind, (locid, id), expr, hook) ->
(match expr with
- ProveBody (bl, c) -> ignore(Subtac_pretyping.subtac_proof env isevars id bl c None)
- | DefineBody (bl, _, c, tycon) ->
+ | ProveBody (bl, t) ->
+ if Lib.is_modtype () then
+ errorlabstrm "Subtac_command.StartProof"
+ (str "Proof editing mode not supported in module types");
+ start_proof_and_print env isevars (Some id) (Global, DefinitionBody Definition) (bl,t)
+ (fun _ _ -> ())
+ | DefineBody (bl, _, c, tycon) ->
ignore(Subtac_pretyping.subtac_proof env isevars id bl c tycon))
| VernacFixpoint (l, b) ->
let _ = trace (str "Building fixpoint") in
@@ -135,6 +148,9 @@ let subtac (loc, command) =
| VernacAssumption (stre,nl,l) ->
vernac_assumption env isevars stre l nl
+ | VernacInstance (sup, is, props) ->
+ Subtac_classes.new_instance sup is props
+
(* | VernacCoFixpoint (l, b) -> *)
(* let _ = trace (str "Building cofixpoint") in *)
(* ignore(Subtac_command.build_recursive l b) *)
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 34c398289..e46ca822e 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1395,9 +1395,9 @@ let set_arity_signature dep n arsign tomatchl pred x =
let rec decomp_lam_force n avoid l p =
if n = 0 then (List.rev l,p,avoid) else
match p with
- | RLambda (_,(Name id as na),_,c) ->
+ | RLambda (_,(Name id as na),k,_,c) ->
decomp_lam_force (n-1) (id::avoid) (na::l) c
- | RLambda (_,(Anonymous as na),_,c) -> decomp_lam_force (n-1) avoid (na::l) c
+ | RLambda (_,(Anonymous as na),k,_,c) -> decomp_lam_force (n-1) avoid (na::l) c
| _ ->
let x = next_ident_away (id_of_string "x") avoid in
decomp_lam_force (n-1) (x::avoid) (Name x :: l)
@@ -2091,13 +2091,12 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
(* let env = nf_evars_env !isevars (env : env) in *)
(* trace (str "Evars : " ++ my_print_evardefs !isevars); *)
(* trace (str "Env : " ++ my_print_env env); *)
-
- let tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in
- let tomatchs_len = List.length tomatchs_lets in
- let tycon = lift_tycon tomatchs_len tycon in
- let env = push_rel_context tomatchs_lets env in
let _isdep = List.exists (fun (x, y) -> is_dependent_ind y) tomatchs in
if predopt = None then
+ let tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in
+ let tomatchs_len = List.length tomatchs_lets in
+ let tycon = lift_tycon tomatchs_len tycon in
+ let env = push_rel_context tomatchs_lets env in
let len = List.length eqns in
let sign, allnames, signlen, eqs, neqs, args =
(* The arity signature *)
@@ -2185,7 +2184,6 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
let j = compile pb in
(* We check for unused patterns *)
List.iter (check_unused_pattern env) matx;
- let j = { j with uj_val = it_mkLambda_or_LetIn j.uj_val tomatchs_lets } in
inh_conv_coerce_to_tycon loc env isevars j tycon
end
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
new file mode 100644
index 000000000..da91b0406
--- /dev/null
+++ b/contrib/subtac/subtac_classes.ml
@@ -0,0 +1,187 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
+
+open Pretyping
+open Evd
+open Environ
+open Term
+open Rawterm
+open Topconstr
+open Names
+open Libnames
+open Pp
+open Vernacexpr
+open Constrintern
+open Subtac_command
+open Typeclasses
+open Typeclasses_errors
+open Termops
+open Decl_kinds
+open Entries
+
+module SPretyping = Subtac_pretyping.Pretyping
+
+let interp_binder_evars evdref env na t =
+ let t = Constrintern.intern_gen true (Evd.evars_of !evdref) env t in
+ SPretyping.understand_tcc_evars evdref env IsType t
+
+let interp_binders_evars isevars env avoid l =
+ List.fold_left
+ (fun (env, ids, params) ((loc, i), t) ->
+ let n = Name i in
+ let t' = interp_binder_evars isevars env n t in
+ let d = (i,None,t') in
+ (push_named d env, i :: ids, d::params))
+ (env, avoid, []) l
+
+let interp_typeclass_context_evars isevars env avoid l =
+ List.fold_left
+ (fun (env, ids, params) (iid, bk, cl) ->
+ let t' = interp_binder_evars isevars env (snd iid) cl in
+ let i = match snd iid with
+ | Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids
+ | Name id -> id
+ in
+ let d = (i,None,t') in
+ (push_named d env, i :: ids, d::params))
+ (env, avoid, []) l
+
+let interp_constrs_evars isevars env avoid l =
+ List.fold_left
+ (fun (env, ids, params) t ->
+ let t' = interp_binder_evars isevars env Anonymous t in
+ let id = Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids in
+ let d = (id,None,t') in
+ (push_named d env, id :: ids, d::params))
+ (env, avoid, []) l
+
+let type_ctx_instance isevars env ctx inst subst =
+ List.fold_left2
+ (fun (subst, instctx) (na, _, t) ce ->
+ let t' = replace_vars subst t in
+ let c = interp_casted_constr_evars isevars env ce t' in
+ let d = na, Some c, t' in
+ (na, c) :: subst, d :: instctx)
+ (subst, []) (List.rev ctx) inst
+
+let substitution_of_constrs ctx cstrs =
+ List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
+
+let new_instance sup (instid, bk, cl) props =
+ let id, par = Implicit_quantifiers.destClassApp cl in
+ let env = Global.env() in
+ let isevars = ref (Evd.create_evar_defs Evd.empty) in
+ let avoid = Termops.ids_of_context env in
+ let k =
+ try class_info (snd id)
+ with Not_found -> unbound_class env id
+ in
+ let gen_ctx, sup = Implicit_quantifiers.resolve_class_binders (vars_of_env env) sup in
+ let gen_ctx =
+ let is_free ((_, x), _) =
+ let f l = not (List.exists (fun ((_, y), _) -> y = x) l) in
+ let g l = not (List.exists (fun ((_, y), _, _) -> y = Name x) l) in
+ f gen_ctx && g sup
+ in
+ let parbinders = Implicit_quantifiers.compute_constrs_freevars_binders (vars_of_env env) par in
+ let parbinders' = List.filter is_free parbinders in
+ gen_ctx @ parbinders'
+ in
+ let env', avoid, genctx = interp_binders_evars isevars env avoid gen_ctx in
+ let env', avoid, supctx = interp_typeclass_context_evars isevars env' avoid sup in
+
+ let subst =
+ match bk with
+ | Explicit ->
+ if List.length par <> List.length k.cl_context + List.length k.cl_params then
+ Classes.mismatched_params env par (k.cl_params @ k.cl_context);
+ let len = List.length k.cl_context in
+ let ctx, par = Util.list_chop len par in
+ let subst, _ = type_ctx_instance isevars env' k.cl_context ctx [] in
+ let subst = Typeclasses.substitution_of_named_context isevars env' k.cl_name len subst
+ k.cl_super
+ in
+ let subst, par = type_ctx_instance isevars env' k.cl_params par subst in subst
+
+ | Implicit ->
+ let t' = interp_type_evars isevars env' (Topconstr.mkAppC (CRef (Ident id), par)) in
+ match kind_of_term t' with
+ App (c, args) ->
+ substitution_of_constrs (k.cl_params @ k.cl_super @ k.cl_context)
+ (List.rev (Array.to_list args))
+ | _ -> assert false
+ in
+ isevars := Evarutil.nf_evar_defs !isevars;
+ let sigma = Evd.evars_of !isevars in
+ let substctx = Typeclasses.nf_substitution sigma subst in
+ let subst, _propsctx =
+ let props =
+ List.map (fun (x, l, d) ->
+ x, Topconstr.abstract_constr_expr d (Classes.binders_of_lidents l))
+ props
+ in
+ if List.length props > List.length k.cl_props then
+ Classes.mismatched_props env' (List.map snd props) k.cl_props;
+ let props, rest =
+ List.fold_left
+ (fun (props, rest) (id,_,_) ->
+ try
+ let (_, c) = List.find (fun ((_,id'), c) -> id' = id) rest in
+ let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+ c :: props, rest'
+ with Not_found -> (CHole Util.dummy_loc :: props), rest)
+ ([], props) k.cl_props
+ in
+ if rest <> [] then
+ unbound_method env k.cl_name (fst (List.hd rest))
+ else
+ type_ctx_instance isevars env' k.cl_props props substctx
+ in
+ let app =
+ applistc (mkConstruct (k.cl_impl, 1)) (List.rev_map snd subst)
+ in
+ let term = it_mkNamedLambda_or_LetIn (it_mkNamedLambda_or_LetIn app supctx) genctx in
+ isevars := Evarutil.nf_evar_defs !isevars;
+ let term = Evarutil.nf_isevar !isevars term in
+ let termtype =
+ let app = applistc (mkInd (k.cl_impl)) (List.rev_map snd substctx) in
+ let t = it_mkNamedProd_or_LetIn (it_mkNamedProd_or_LetIn app supctx) genctx in
+ Evarutil.nf_isevar !isevars t
+ in
+ isevars := undefined_evars !isevars;
+ let id =
+ match snd instid with
+ Name id -> id
+ | Anonymous ->
+ let i = Nameops.add_suffix (snd id) "_instance_" in
+ Termops.next_global_ident_away false i (Termops.ids_of_context env)
+ in
+ let imps =
+ Util.list_map_i
+ (fun i (na, b, t) -> ExplByPos (i, Some na), (true, true))
+ 1 (genctx @ List.rev supctx)
+ in
+ let hook cst =
+ let inst =
+ { is_class = k;
+ is_name = id;
+(* is_params = paramsctx; *)
+(* is_super = superctx; *)
+ is_impl = cst;
+(* is_add_hint = (fun () -> Classes.add_instance_hint id); *)
+ }
+ in
+ Classes.add_instance_hint id;
+ Impargs.declare_manual_implicits false (ConstRef cst) false imps;
+ Typeclasses.add_instance inst
+ in
+ let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
+ let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
+ ignore (Subtac_obligations.add_definition id constr typ ~kind:Instance ~hook obls)
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
new file mode 100644
index 000000000..ce4b32cad
--- /dev/null
+++ b/contrib/subtac/subtac_classes.mli
@@ -0,0 +1,39 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
+
+(*i*)
+open Names
+open Decl_kinds
+open Term
+open Sign
+open Evd
+open Environ
+open Nametab
+open Mod_subst
+open Topconstr
+open Util
+open Typeclasses
+open Implicit_quantifiers
+open Classes
+(*i*)
+
+val type_ctx_instance : Evd.evar_defs ref ->
+ Environ.env ->
+ (Names.identifier * 'a * Term.constr) list ->
+ Topconstr.constr_expr list ->
+ (Names.identifier * Term.constr) list ->
+ (Names.identifier * Term.constr) list *
+ (Names.identifier * Term.constr option * Term.constr) list
+
+val new_instance :
+ typeclass_context ->
+ typeclass_constraint ->
+ binder_def_list ->
+ unit
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index a9a30c57a..9afa6f067 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -98,11 +98,11 @@ let interp_binder sigma env na t =
let interp_context sigma env params =
List.fold_left
(fun (env,params) d -> match d with
- | LocalRawAssum ([_,na],(CHole _ as t)) ->
+ | LocalRawAssum ([_,na],k,(CHole _ as t)) ->
let t = interp_binder sigma env na t in
let d = (na,None,t) in
(push_rel d env, d::params)
- | LocalRawAssum (nal,t) ->
+ | LocalRawAssum (nal,k,t) ->
let t = interp_type sigma env t in
let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
let ctx = List.rev ctx in
@@ -152,7 +152,7 @@ let collect_non_rec env =
let list_of_local_binders l =
let rec aux acc = function
Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
- | Topconstr.LocalRawAssum (nl, c) :: tl ->
+ | Topconstr.LocalRawAssum (nl, k, c) :: tl ->
aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl
| [] -> List.rev acc
in aux [] l
@@ -294,12 +294,11 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
lift lift_cst prop ;
lift lift_cst intern_body_lam |])
| Some f ->
- lift (succ after_length)
- (mkApp (constr_of_global (Lazy.force fix_measure_sub_ref),
- [| argtyp ;
- f ;
- lift lift_cst prop ;
- lift lift_cst intern_body_lam |]))
+ mkApp (constr_of_global (Lazy.force fix_measure_sub_ref),
+ [| lift lift_cst argtyp ;
+ lift lift_cst f ;
+ lift lift_cst prop ;
+ lift lift_cst intern_body_lam |])
in
let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
let def = it_mkLambda_or_LetIn def_appl binders_rel in
@@ -316,13 +315,13 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let evm = non_instanciated_map env isevars evm in
(* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *)
- let evars, evars_def = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc (Some fullctyp) in
+ let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
(* (try trace (str "Generated obligations : "); *)
(* Array.iter *)
(* (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *)
(* evars; *)
(* with _ -> ()); *)
- Subtac_obligations.add_definition recname evars_def fullctyp evars
+ Subtac_obligations.add_definition recname evars_def evars_typ evars
let nf_evar_context isevars ctx =
List.map (fun (n, b, t) ->
@@ -412,11 +411,12 @@ let build_mutrec lnameargsardef boxed =
(* Generalize by the recursive prototypes *)
let def =
Termops.it_mkNamedLambda_or_LetIn def rec_sign
- and typ =
+ and typ =
Termops.it_mkNamedProd_or_LetIn typ rec_sign
in
- let evm = Subtac_utils.evars_of_term evm Evd.empty def in
- let evars, def = Eterm.eterm_obligations env id isevars evm recdefs def (Some typ) 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
collect_evars (succ i) ((id, def, typ, evars) :: acc)
else acc
in
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index e3cf7a57a..c184169ac 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -12,6 +12,8 @@ open Decl_kinds
open Util
open Evd
+type definition_hook = constant -> unit
+
let pperror cmd = Util.errorlabstrm "Program" cmd
let error s = pperror (str s)
@@ -40,6 +42,9 @@ type program_info = {
prg_obligations: obligations;
prg_deps : identifier list;
prg_nvrec : int array;
+ prg_implicits : (Topconstr.explicitation * (bool * bool)) list;
+ prg_kind : definition_object_kind;
+ prg_hook : definition_hook;
}
let assumption_message id =
@@ -106,7 +111,7 @@ let progmap_union = ProgMap.fold ProgMap.add
let cache (_, (infos, tac)) =
from_prg := infos;
- default_tactic_expr := tac
+ set_default_tactic tac
let (input,output) =
declare_object
@@ -125,24 +130,30 @@ let rec intset_to = function
let subst_body prg =
let obls, _ = prg.prg_obligations in
- subst_deps obls (intset_to (pred (Array.length obls))) prg.prg_body
-
+ let ints = intset_to (pred (Array.length obls)) in
+ subst_deps obls ints prg.prg_body,
+ subst_deps obls ints (Termops.refresh_universes prg.prg_type)
+
let declare_definition prg =
- let body = subst_body prg in
+ let body, typ = subst_body prg in
(try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
my_print_constr (Global.env()) body ++ str " : " ++
my_print_constr (Global.env()) prg.prg_type);
with _ -> ());
let ce =
{ const_entry_body = body;
- const_entry_type = Some (Termops.refresh_universes prg.prg_type);
+ const_entry_type = Some typ;
const_entry_opaque = false;
const_entry_boxed = false}
in
let c = Declare.declare_constant
- prg.prg_name (DefinitionEntry ce,IsDefinition Definition)
+ prg.prg_name (DefinitionEntry ce,IsDefinition prg.prg_kind)
in
+ let gr = ConstRef c in
+ if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
+ Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits;
print_message (definition_message c);
+ prg.prg_hook c;
c
open Pp
@@ -151,14 +162,18 @@ open Ppconstr
let declare_mutual_definition l =
let len = List.length l in
let namerec = Array.of_list (List.map (fun x -> x.prg_name) l) in
- let arrec =
- Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l)
- in
- let recvec =
- Array.of_list
- (List.map (fun x ->
- let subs = (subst_body x) in
- snd (decompose_lam_n len subs)) l)
+(* let arrec = *)
+(* Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l) *)
+(* in *)
+ let recvec, arrec =
+ let l, l' =
+ List.split
+ (List.map (fun x ->
+ let subs, typ = (subst_body x) in
+ snd (decompose_lam_n len subs),
+ snd (decompose_prod_n len typ)) l)
+ in
+ Array.of_list l, Array.of_list l'
in
let nvrec = (List.hd l).prg_nvrec in
let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
@@ -205,7 +220,7 @@ let try_tactics obls =
let red = Reductionops.nf_betaiota
-let init_prog_info n b t deps nvrec obls =
+let init_prog_info n b t deps nvrec obls impls kind hook =
let obls' =
Array.mapi
(fun i (n, t, o, d) ->
@@ -216,7 +231,7 @@ let init_prog_info n b t deps nvrec obls =
obls
in
{ prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
- prg_deps = deps; prg_nvrec = nvrec; }
+ prg_deps = deps; prg_nvrec = nvrec; prg_implicits = impls; prg_kind = kind; prg_hook = hook; }
let get_prog name =
let prg_infos = !from_prg in
@@ -327,7 +342,8 @@ let rec solve_obligation prg num =
| _ -> ());
trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
- Pfedit.by !default_tactic
+ Pfedit.by !default_tactic;
+ 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))
@@ -393,9 +409,22 @@ and auto_solve_obligations n : progress =
Flags.if_verbose msgnl (str "Solving obligations automatically...");
try solve_obligations n !default_tactic with NoObligations _ -> Dependent
-let add_definition n b t obls =
+open Pp
+let show_obligations ?(msg=true) n =
+ let prg = get_prog_err n in
+ let n = prg.prg_name in
+ let obls, rem = prg.prg_obligations in
+ if msg then msgnl (int rem ++ str " obligation(s) remaining: ");
+ Array.iteri (fun i x ->
+ match x.obl_body with
+ None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
+ my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())
+ | Some _ -> ())
+ obls
+
+let add_definition n b t ?(implicits=[]) ?(kind=Definition) ?(hook=fun x -> ()) obls =
Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
- let prg = init_prog_info n b t [] (Array.make 0 0) obls in
+ let prg = init_prog_info n b t [] (Array.make 0 0) obls implicits kind hook in
let obls,_ = prg.prg_obligations in
if Array.length obls = 0 then (
Flags.if_verbose ppnl (str ".");
@@ -406,19 +435,30 @@ let add_definition n b t obls =
let len = Array.length obls in
let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
from_prg := ProgMap.add n prg !from_prg;
- auto_solve_obligations (Some n))
+ let res = auto_solve_obligations (Some n) in
+ match res with
+ | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
+ | _ -> res)
-let add_mutual_definitions l nvrec =
+let add_mutual_definitions l ?(implicits=[]) ?(kind=Definition) nvrec =
let deps = List.map (fun (n, b, t, obls) -> n) l in
let upd = List.fold_left
(fun acc (n, b, t, obls) ->
- let prg = init_prog_info n b t deps nvrec obls in
+ let prg = init_prog_info n b t deps nvrec obls implicits kind (fun x -> ()) in
ProgMap.add n prg acc)
!from_prg l
in
from_prg := upd;
- List.iter (fun x -> ignore(auto_solve_obligations (Some x))) deps
-
+ let _defined =
+ List.fold_left (fun finished x ->
+ if finished then finished
+ else
+ match auto_solve_obligations (Some x) with
+ Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true
+ | _ -> false)
+ false deps
+ in ()
+
let admit_obligations n =
let prg = get_prog_err n in
let obls, rem = prg.prg_obligations in
@@ -447,18 +487,5 @@ let next_obligation n =
array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = [])
obls
in solve_obligation prg i
-
-open Pp
-let show_obligations n =
- let prg = get_prog_err n in
- let n = prg.prg_name in
- let obls, rem = prg.prg_obligations in
- msgnl (int rem ++ str " obligation(s) remaining: ");
- Array.iteri (fun i x ->
- match x.obl_body with
- None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
- my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())
- | Some _ -> ())
- obls
-
+
let default_tactic () = !default_tactic
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index cd70d5233..30fbd0284 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -12,11 +12,18 @@ type progress = (* Resolution status of a program *)
val set_default_tactic : Tacexpr.glob_tactic_expr -> unit
val default_tactic : unit -> Proof_type.tactic
+type definition_hook = constant -> unit
+
val add_definition : Names.identifier -> Term.constr -> Term.types ->
- obligation_info -> progress
+ ?implicits:(Topconstr.explicitation * (bool * bool)) list ->
+ ?kind:Decl_kinds.definition_object_kind ->
+ ?hook:definition_hook -> obligation_info -> progress
val add_mutual_definitions :
- (Names.identifier * Term.constr * Term.types * obligation_info) list -> int array -> unit
+ (Names.identifier * Term.constr * Term.types * obligation_info) list ->
+ ?implicits:(Topconstr.explicitation * (bool * bool)) list ->
+ ?kind:Decl_kinds.definition_object_kind ->
+ int array -> unit
val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit
@@ -31,7 +38,7 @@ val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic -
val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
-val show_obligations : Names.identifier option -> unit
+val show_obligations : ?msg:bool -> Names.identifier option -> unit
val admit_obligations : Names.identifier option -> unit
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index a0e7e6951..0703bcb83 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -70,7 +70,12 @@ let merge_evms x y =
let interp env isevars c tycon =
let j = pretype tycon env isevars ([],[]) c in
- let evm = evars_of !isevars in
+ let _ = isevars := Evarutil.nf_evar_defs !isevars in
+ let evd,_ = consider_remaining_unif_problems env !isevars in
+ let unevd = undefined_evars evd in
+ let unevd' = Typeclasses.resolve_typeclasses env (Evd.evars_of unevd) evd in
+ let evm = evars_of unevd' in
+ isevars := unevd';
nf_evar evm j.uj_val, nf_evar evm j.uj_type
let find_with_index x l =
@@ -98,7 +103,7 @@ let env_with_binders env isevars l =
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, typ) :: 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 =
@@ -111,45 +116,28 @@ let env_with_binders env isevars l =
| [] -> acc
in aux (env, []) l
-let subtac_process env isevars id l c tycon =
- let c = Command.abstract_constr_expr c l in
-(* let env_binders, binders_rel = env_with_binders env isevars l in *)
+let subtac_process env isevars id bl c tycon =
+(* let bl = Implicit_quantifiers.ctx_of_class_binders (vars_of_env env) cbl @ l in *)
+ let imps = Implicit_quantifiers.implicits_of_binders bl in
+ let c = Command.abstract_constr_expr c bl in
let tycon =
match tycon with
None -> empty_tycon
| Some t ->
- let t = Command.generalize_constr_expr t l in
+ let t = Command.generalize_constr_expr t bl in
let t = coqintern_type !isevars env t in
let coqt, ttyp = interp env isevars t empty_tycon in
mk_tycon coqt
in
let c = coqintern_constr !isevars env c in
let coqc, ctyp = interp env isevars c tycon in
-(* let _ = try trace (str "Interpreted term: " ++ my_print_constr env coqc ++ spc () ++ *)
-(* str "Coq type: " ++ my_print_constr env ctyp) *)
-(* with _ -> () *)
-(* in *)
-(* let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !isevars)) with _ -> () in *)
-
-(* let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel *)
-(* and fullctyp = it_mkProd_or_LetIn ctyp binders_rel *)
-(* in *)
- let fullcoqc = Evarutil.nf_evar (evars_of !isevars) coqc in
- let fullctyp = Evarutil.nf_evar (evars_of !isevars) ctyp in
-(* let evm = evars_of_term (evars_of !isevars) Evd.empty fullctyp in *)
-(* let evm = evars_of_term (evars_of !isevars) evm fullcoqc in *)
-(* let _ = try trace (str "After evar normalization remain: " ++ spc () ++ *)
-(* Evd.pr_evar_map evm) *)
-(* with _ -> () *)
-(* in *)
let evm = non_instanciated_map env isevars (evars_of !isevars) in
-(* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *)
- evm, fullcoqc, fullctyp
+ evm, coqc, ctyp, imps
open Subtac_obligations
-let subtac_proof env isevars id l c tycon =
- let evm, coqc, coqt = subtac_process env isevars id l c tycon in
+let subtac_proof 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 evars, def = Eterm.eterm_obligations env id !isevars evm 0 coqc (Some coqt) in
- add_definition id def coqt evars
+ let evars, def, ty = Eterm.eterm_obligations env id !isevars evm 0 coqc coqt in
+ add_definition id def ty ~implicits:imps evars
diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli
index afe554c87..4af37043f 100644
--- a/contrib/subtac/subtac_pretyping.mli
+++ b/contrib/subtac/subtac_pretyping.mli
@@ -5,11 +5,19 @@ open Sign
open Evd
open Global
open Topconstr
+open Implicit_quantifiers
+open Impargs
module Pretyping : Pretyping.S
+val interp :
+ Environ.env ->
+ Evd.evar_defs ref ->
+ Rawterm.rawconstr ->
+ Evarutil.type_constraint -> Term.constr * Term.constr
+
val subtac_process : env -> evar_defs ref -> identifier -> local_binder list ->
- constr_expr -> constr_expr option -> evar_map * constr * types
+ constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list
val subtac_proof : env -> evar_defs ref -> identifier -> local_binder list ->
constr_expr -> constr_expr option -> Subtac_obligations.progress
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 0ed0632c6..a2d5be66c 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -200,11 +200,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RRec (loc,fixkind,names,bl,lar,vdef) ->
let rec type_bl env ctxt = function
[] -> ctxt
- | (na,None,ty)::bl ->
+ | (na,k,None,ty)::bl ->
let ty' = pretype_type empty_valcon env isevars lvar ty in
let dcl = (na,None,ty'.utj_val) in
type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
- | (na,Some bd,ty)::bl ->
+ | (na,k,Some bd,ty)::bl ->
let ty' = pretype_type empty_valcon env isevars lvar ty in
let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in
let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
@@ -326,7 +326,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| _ -> resj in
inh_conv_coerce_to_tycon loc env isevars resj tycon
- | RLambda(loc,name,c1,c2) ->
+ | RLambda(loc,name,k,c1,c2) ->
let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
let dom_valcon = valcon_of_tycon dom in
let j = pretype_type dom_valcon env isevars lvar c1 in
@@ -334,7 +334,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let j' = pretype rng (push_rel var env) isevars lvar c2 in
judge_of_abstraction env name j j'
- | RProd(loc,name,c1,c2) ->
+ | RProd(loc,name,k,c1,c2) ->
let j = pretype_type empty_valcon env isevars lvar c1 in
let var = (name,j.utj_val) in
let env' = push_rel_assum var env in
@@ -557,7 +557,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(pretype tycon env isevars lvar c).uj_val
| IsType ->
(pretype_type empty_valcon env isevars lvar c).utj_val in
- nf_evar (evars_of !isevars) c'
+ let evd,_ = consider_remaining_unif_problems env !isevars in
+ let evd = nf_evar_defs evd in
+ let c' = nf_evar (evars_of evd) c' in
+(* let evd = undefined_evars evd in *)
+ let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in
+ let c' = nf_evar (evars_of evd) c' in
+ isevars := evd;
+ c'
(* TODO: comment faire remonter l'information si le typage a resolu des
variables du sigma original. il faudrait que la fonction de typage
@@ -585,11 +592,16 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let ise_pretype_gen fail_evar sigma env lvar kind c =
let isevars = ref (Evd.create_evar_defs sigma) in
let c = pretype_gen isevars env lvar kind c in
- let isevars,_ = consider_remaining_unif_problems env !isevars in
- let c = nf_evar (evars_of isevars) c in
- if fail_evar then check_evars env sigma isevars c;
- isevars, c
-
+(* let evd,_ = consider_remaining_unif_problems env !isevars in *)
+(* let evd = nf_evar_defs evd in *)
+(* let c = nf_evar (evars_of evd) c in *)
+(* let evd = undefined_evars evd in *)
+(* let evd = Typeclasses.resolve_typeclasses env sigma evd in *)
+(* let c = nf_evar (evars_of evd) c in *)
+ let evd = !isevars in
+ if fail_evar then check_evars env (Evd.evars_of evd) evd c;
+ evd, c
+
(** Entry points of the high-level type synthesis algorithm *)
let understand_gen kind sigma env c =
@@ -604,8 +616,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let understand_ltac sigma env lvar kind c =
ise_pretype_gen false sigma env lvar kind c
- let understand_tcc_evars isevars env kind c =
- pretype_gen isevars env ([],[]) kind c
+ let understand_tcc_evars evdref env kind c =
+ pretype_gen evdref env ([],[]) kind c
+
+(* evdref := nf_evar_defs !evdref; *)
+(* let c = nf_evar (evars_of !evdref) c in *)
+(* let evd = undefined_evars !evdref in *)
+(* let evd = Typeclasses.resolve_typeclasses env (evars_of evd) !evdref in *)
+(* evdref := evd; *)
+(* nf_evar (evars_of evd) c *)
let understand_tcc sigma env ?expected_type:exptyp c =
let ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index d5df9adc9..46a8bd203 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -357,19 +357,31 @@ let print_message m =
(* Solve an obligation using tactics, return the corresponding proof term *)
let solve_by_tac evi t =
- debug 2 (str "Solving goal using tactics: " ++ Evd.pr_evar_info evi);
let id = id_of_string "H" in
- try
+ try
Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
(fun _ _ -> ());
- debug 2 (str "Started proof");
Pfedit.by (tclCOMPLETE t);
- let _,(const,_,_) = Pfedit.cook_proof () in
+ let _,(const,_,_) = Pfedit.cook_proof () in
Pfedit.delete_current_proof (); const.Entries.const_entry_body
- with e ->
+ with e ->
Pfedit.delete_current_proof();
raise Exit
+(* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 07:09:57 +0000