aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/indfun.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/indfun.ml')
-rw-r--r--plugins/funind/indfun.ml129
1 files changed, 67 insertions, 62 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index dab094f913..13eda3952a 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,7 +1,8 @@
open CErrors
+open Sorts
open Util
open Names
-open Term
+open Constr
open EConstr
open Pp
open Indfun_common
@@ -46,7 +47,7 @@ let functional_induction with_clean c princl pat =
try find_Function_infos c'
with Not_found ->
user_err (str "Cannot find induction information on "++
- Printer.pr_leconstr (mkConst c') )
+ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
in
match Tacticals.elimination_sort_of_goal g with
| InProp -> finfo.prop_lemma
@@ -74,7 +75,7 @@ let functional_induction with_clean c princl pat =
(* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
with Not_found -> (* This one is neither defined ! *)
user_err (str "Cannot find induction principle for "
- ++Printer.pr_leconstr (mkConst c') )
+ ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
in
let princ = EConstr.of_constr princ in
(princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g')
@@ -140,8 +141,7 @@ let rec abstract_glob_constr c = function
| Constrexpr.CLocalPattern _::bl -> assert false
let interp_casted_constr_with_implicits env sigma impls c =
- Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
- c
+ Constrintern.intern_gen Pretyping.WithoutTypeConstraint env sigma ~impls c
(*
Construct a fixpoint as a Glob_term
@@ -154,14 +154,14 @@ let build_newrecursive
let sigma = Evd.from_env env0 in
let (rec_sign,rec_impls) =
List.fold_left
- (fun (env,impls) (((_,recname),_),bl,arityc,_) ->
+ (fun (env,impls) (({CAst.v=recname},_),bl,arityc,_) ->
let arityc = Constrexpr_ops.mkCProdN bl arityc in
let arity,ctx = Constrintern.interp_type env0 sigma arityc in
- let evdref = ref (Evd.from_env env0) in
- let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
- let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in
+ let evd = Evd.from_env env0 in
+ let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in
+ let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in
let open Context.Named.Declaration in
- (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
+ (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
(env0,Constrintern.empty_internalization_env) lnameargsardef in
let recdef =
(* Declare local notations *)
@@ -214,6 +214,7 @@ let is_rec names =
| GCases(_,_,el,brl) ->
List.exists (fun (e,_) -> lookup names e) el ||
List.exists (lookup_br names) brl
+ | GProj(_,c) -> lookup names c
and lookup_br names (_,(idl,_,rt)) =
let new_names = List.fold_right Id.Set.remove idl names in
lookup new_names rt
@@ -281,7 +282,6 @@ let derive_inversion fix_names =
in
Invfun.derive_correctness
Functional_principles_types.make_scheme
- functional_induction
fix_names_as_constant
lind;
with e when CErrors.noncritical e ->
@@ -343,7 +343,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof
(continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
Tacmach.tactic) : unit =
- let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
+ let names = List.map (function (({CAst.v=name},_),_,_,_,_),_ -> name) fix_rec_l in
let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
let funs_args = List.map fst fun_bodies in
let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in
@@ -364,7 +364,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
f_R_mut)
in
let fname_kn (((fname,_),_,_,_,_),_) =
- let f_ref = Ident fname in
+ let f_ref = Ident CAst.(with_loc_val (fun ?loc n -> (loc,n)) fname) in
locate_with_msg
(pr_reference f_ref++str ": Not an inductive type!")
locate_constant
@@ -403,15 +403,16 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
match fixpoint_exprl with
- | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
+ | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
- Command.do_definition
+ ComDefinition.do_definition
+ ~program_mode:false
fname
(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
let evd,rev_pconstants =
List.fold_left
- (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
+ (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
let evd,c =
Evd.fresh_global
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
@@ -425,10 +426,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
in
evd,List.rev rev_pconstants
| _ ->
- Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+ ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
let evd,rev_pconstants =
List.fold_left
- (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
+ (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
let evd,c =
Evd.fresh_global
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
@@ -458,7 +459,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
let rec_arg_num =
let names =
List.map
- snd
+ CAst.(with_val (fun x -> x))
(Constrexpr_ops.names_of_local_assums args)
in
match wf_arg with
@@ -474,8 +475,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
(None,(Ident (Loc.tag fname)),None) ,
(List.map
(function
- | _,Anonymous -> assert false
- | _,Name e -> (Constrexpr_ops.mkIdentC e)
+ | {CAst.v=Anonymous} -> assert false
+ | {CAst.v=Name e} -> (Constrexpr_ops.mkIdentC e)
)
(Constrexpr_ops.names_of_local_assums args)
)
@@ -513,7 +514,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
| None ->
begin
match args with
- | [Constrexpr.CLocalAssum ([(_,Name x)],k,t)] -> t,x
+ | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x
| _ -> error "Recursive argument must be specified"
end
| Some wf_args ->
@@ -523,7 +524,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
(function
| Constrexpr.CLocalAssum(l,k,t) ->
List.exists
- (function (_,Name id) -> Id.equal id wf_args | _ -> false)
+ (function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false)
l
| _ -> false
)
@@ -544,7 +545,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
let fun_from_mes =
let applied_mes =
Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in
- Constrexpr_ops.mkLambdaC ([(Loc.tag @@ Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
+ Constrexpr_ops.mkLambdaC ([CAst.make @@ Name wf_arg],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
in
let wf_rel_from_mes =
Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC ltof,[wf_arg_type;fun_from_mes])
@@ -555,7 +556,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
let a = Names.Id.of_string "___a" in
let b = Names.Id.of_string "___b" in
Constrexpr_ops.mkLambdaC(
- [Loc.tag @@ Name a;Loc.tag @@ Name b],
+ [CAst.make @@ Name a; CAst.make @@ Name b],
Constrexpr.Default Explicit,
wf_arg_type,
Constrexpr_ops.mkAppC(wf_rel_expr,
@@ -589,11 +590,11 @@ and rebuild_nal aux bk bl' nal typ =
match nal,typ with
| _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ
| [], _ -> rebuild_bl aux bl' typ
- | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } ->
- if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na')
+ | na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } ->
+ if Name.equal (na.CAst.v) (na'.CAst.v) || Name.is_anonymous (na'.CAst.v)
then
let assum = CLocalAssum([na],bk,nal't) in
- let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in
+ let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in
rebuild_nal
(assum::aux)
bk
@@ -602,7 +603,7 @@ and rebuild_nal aux bk bl' nal typ =
(CAst.make @@ CProdN(new_rest,typ'))
else
let assum = CLocalAssum([na'],bk,nal't) in
- let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in
+ let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in
rebuild_nal
(assum::aux)
bk
@@ -615,8 +616,8 @@ and rebuild_nal aux bk bl' nal typ =
let rebuild_bl aux bl typ = rebuild_bl aux bl typ
let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
- let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
- let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in
+ let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in
+ let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in
let constr_expr_typel =
with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
let fixpoint_exprl_with_new_bl =
@@ -636,7 +637,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
let _is_struct =
match fixpoint_exprl with
| [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
- let (((((_,name),pl),_,args,types,body)),_) as fixpoint_expr =
+ let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -657,10 +658,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof
true
in
if register_built
- then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook;
+ then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook;
false
|[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] ->
- let (((((_,name),_),_,args,types,body)),_) as fixpoint_expr =
+ let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -681,7 +682,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
true
in
if register_built
- then register_mes name rec_impls wf_mes wf_rel_opt (map_option snd wf_x) using_lemmas args types body pre_hook;
+ then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook;
true
| _ ->
List.iter (function ((_na,(_,ord),_args,_body,_type),_not) ->
@@ -694,7 +695,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
fixpoint_exprl;
let fixpoint_exprl = recompute_binder_list fixpoint_exprl in
let fix_names =
- List.map (function ((((_,name),_),_,_,_,_),_) -> name) fixpoint_exprl
+ List.map (function ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl
in
(* ok all the expressions are structural *)
let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
@@ -729,10 +730,14 @@ let rec add_args id new_args = CAst.map (function
end
| CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.")
| CProdN(nal,b1) ->
- CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
+ CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2)
+ | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t)
+ | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal,
add_args id new_args b1)
| CLambdaN(nal,b1) ->
- CLambdaN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
+ CLambdaN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2)
+ | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t)
+ | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal,
add_args id new_args b1)
| CLetIn(na,b1,t,b2) ->
CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2)
@@ -751,7 +756,7 @@ let rec add_args id new_args = CAst.map (function
List.map (fun (b,na,b_option) ->
add_args id new_args b,
na, b_option) cel,
- List.map (fun (loc,(cpl,e)) -> Loc.tag ?loc @@ (cpl,add_args id new_args e)) cal
+ List.map CAst.(map (fun (cpl,e) -> (cpl,add_args id new_args e))) cal
)
| CLetTuple(nal,(na,b_option),b1,b2) ->
CLetTuple(nal,(na,Option.map (add_args id new_args) b_option),
@@ -778,6 +783,7 @@ let rec add_args id new_args = CAst.map (function
| CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
| CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
| CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
+ | CProj _ -> user_err Pp.(str "Funind does not support primitive projections")
)
exception Stop of Constrexpr.constr_expr
@@ -790,7 +796,7 @@ let rec chop_n_arrow n t =
then t (* If we have already removed all the arrows then return the type *)
else (* If not we check the form of [t] *)
match t.CAst.v with
- | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible :
+ | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, two results are possible :
either we need to discard more than the number of arrows contained
in this product declaration then we just recall [chop_n_arrow] on
the remaining number of arrow to chop and [t'] we discard it and
@@ -802,7 +808,7 @@ let rec chop_n_arrow n t =
let new_n =
let rec aux (n:int) = function
[] -> n
- | (nal,k,t'')::nal_ta' ->
+ | CLocalAssum(nal,k,t'')::nal_ta' ->
let nal_l = List.length nal in
if n >= nal_l
then
@@ -810,9 +816,10 @@ let rec chop_n_arrow n t =
else
let new_t' = CAst.make @@
Constrexpr.CProdN(
- ((snd (List.chop n nal)),k,t'')::nal_ta',t')
+ CLocalAssum((snd (List.chop n nal)),k,t'')::nal_ta',t')
in
raise (Stop new_t')
+ | _ -> anomaly (Pp.str "Not enough products.")
in
aux n nal_ta'
in
@@ -825,28 +832,26 @@ let rec chop_n_arrow n t =
let rec get_args b t : Constrexpr.local_binder_expr list *
Constrexpr.constr_expr * Constrexpr.constr_expr =
match b.CAst.v with
- | Constrexpr.CLambdaN ((nal_ta), b') ->
+ | Constrexpr.CLambdaN (CLocalAssum(nal,k,ta) as d::rest, b') ->
begin
- let n =
- (List.fold_left (fun n (nal,_,_) ->
- n+List.length nal) 0 nal_ta )
- in
- let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in
- (List.map (fun (nal,k,ta) ->
- (Constrexpr.CLocalAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
+ let n = List.length nal in
+ let nal_tas,b'',t'' = get_args (CAst.make ?loc:b.CAst.loc @@ Constrexpr.CLambdaN (rest,b')) (chop_n_arrow n t) in
+ d :: nal_tas, b'',t''
end
+ | Constrexpr.CLambdaN ([], b) -> [],b,t
| _ -> [],b,t
let make_graph (f_ref:global_reference) =
let c,c_body =
match f_ref with
- | ConstRef c ->
- begin try c,Global.lookup_constant c
- with Not_found ->
- raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr (mkConst c)) )
- end
- | _ -> raise (UserError (None, str "Not a function reference") )
+ | ConstRef c ->
+ begin try c,Global.lookup_constant c
+ with Not_found ->
+ let sigma, env = Pfedit.get_current_context () in
+ raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) )
+ end
+ | _ -> raise (UserError (None, str "Not a function reference") )
in
(match Global.body_of_constant_body c_body with
| None -> error "Cannot build a graph over an axiom!"
@@ -869,7 +874,7 @@ let make_graph (f_ref:global_reference) =
let l =
List.map
(fun (id,(n,recexp),bl,t,b) ->
- let loc, rec_id = Option.get n in
+ let { CAst.loc; v=rec_id } = Option.get n in
let new_args =
List.flatten
(List.map
@@ -877,7 +882,7 @@ let make_graph (f_ref:global_reference) =
| Constrexpr.CLocalDef (na,_,_)-> []
| Constrexpr.CLocalAssum (nal,_,_) ->
List.map
- (fun (loc,n) -> CAst.make ?loc @@
+ (fun {CAst.loc;v=n} -> CAst.make ?loc @@
CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None))
nal
| Constrexpr.CLocalPattern _ -> assert false
@@ -885,21 +890,21 @@ let make_graph (f_ref:global_reference) =
nal_tas
)
in
- let b' = add_args (snd id) new_args b in
- ((((id,None), ( Some (Loc.tag rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+ let b' = add_args id.CAst.v new_args b in
+ ((((id,None), ( Some CAst.(make rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
)
fixexprl
in
l
| _ ->
let id = Label.to_id (Constant.label c) in
- [(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
+ [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
in
let mp,dp,_ = Constant.repr3 c in
do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list;
(* We register the infos *)
List.iter
- (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
+ (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
expr_list)
let do_generate_principle = do_generate_principle [] warning_error true
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 21:27:01 +0000