summaryrefslogtreecommitdiff
path: root/plugins/funind/indfun.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/indfun.ml')
-rw-r--r--plugins/funind/indfun.ml776
1 files changed, 776 insertions, 0 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
new file mode 100644
index 00000000..38f42844
--- /dev/null
+++ b/plugins/funind/indfun.ml
@@ -0,0 +1,776 @@
+open Util
+open Names
+open Term
+open Pp
+open Indfun_common
+open Libnames
+open Rawterm
+open Declarations
+
+let is_rec_info scheme_info =
+ let test_branche min acc (_,_,br) =
+ acc || (
+ let new_branche =
+ it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum br)) in
+ let free_rels_in_br = Termops.free_rels new_branche in
+ let max = min + scheme_info.Tactics.npredicates in
+ Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br
+ )
+ in
+ Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
+
+
+let choose_dest_or_ind scheme_info =
+ if is_rec_info scheme_info
+ then Tactics.new_induct false
+ else Tactics.new_destruct false
+
+
+let functional_induction with_clean c princl pat =
+ Dumpglob.pause ();
+ let res = let f,args = decompose_app c in
+ fun g ->
+ let princ,bindings, princ_type =
+ match princl with
+ | None -> (* No principle is given let's find the good one *)
+ begin
+ match kind_of_term f with
+ | Const c' ->
+ let princ_option =
+ let finfo = (* we first try to find out a graph on f *)
+ try find_Function_infos c'
+ with Not_found ->
+ errorlabstrm "" (str "Cannot find induction information on "++
+ Printer.pr_lconstr (mkConst c') )
+ in
+ match Tacticals.elimination_sort_of_goal g with
+ | InProp -> finfo.prop_lemma
+ | InSet -> finfo.rec_lemma
+ | InType -> finfo.rect_lemma
+ in
+ let princ = (* then we get the principle *)
+ try mkConst (Option.get princ_option )
+ with Option.IsNone ->
+ (*i If there is not default lemma defined then,
+ we cross our finger and try to find a lemma named f_ind
+ (or f_rec, f_rect) i*)
+ let princ_name =
+ Indrec.make_elimination_ident
+ (id_of_label (con_label c'))
+ (Tacticals.elimination_sort_of_goal g)
+ in
+ try
+ mkConst(const_of_id princ_name )
+ with Not_found -> (* This one is neither defined ! *)
+ errorlabstrm "" (str "Cannot find induction principle for "
+ ++Printer.pr_lconstr (mkConst c') )
+ in
+ (princ,Rawterm.NoBindings, Tacmach.pf_type_of g princ)
+ | _ -> raise (UserError("",str "functional induction must be used with a function" ))
+
+ end
+ | Some ((princ,binding)) ->
+ princ,binding,Tacmach.pf_type_of g princ
+ in
+ let princ_infos = Tactics.compute_elim_sig princ_type in
+ let args_as_induction_constr =
+ let c_list =
+ if princ_infos.Tactics.farg_in_concl
+ then [c] else []
+ in
+ List.map (fun c -> Tacexpr.ElimOnConstr (c,NoBindings)) (args@c_list)
+ in
+ let princ' = Some (princ,bindings) in
+ let princ_vars =
+ List.fold_right
+ (fun a acc ->
+ try Idset.add (destVar a) acc
+ with _ -> acc
+ )
+ args
+ Idset.empty
+ in
+ let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in
+ let old_idl = Idset.diff old_idl princ_vars in
+ let subst_and_reduce g =
+ if with_clean
+ then
+ let idl =
+ map_succeed
+ (fun id ->
+ if Idset.mem id old_idl then failwith "subst_and_reduce";
+ id
+ )
+ (Tacmach.pf_ids_of_hyps g)
+ in
+ let flag =
+ Rawterm.Cbv
+ {Rawterm.all_flags
+ with Rawterm.rDelta = false;
+ }
+ in
+ Tacticals.tclTHEN
+ (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id])) idl )
+ (Hiddentac.h_reduce flag Tacticals.allHypsAndConcl)
+ g
+ else Tacticals.tclIDTAC g
+
+ in
+ Tacticals.tclTHEN
+ (choose_dest_or_ind
+ princ_infos
+ args_as_induction_constr
+ princ'
+ (None,pat)
+ None)
+ subst_and_reduce
+ g
+ in
+ Dumpglob.continue ();
+ res
+
+
+
+
+type annot =
+ Struct of identifier
+ | Wf of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
+ | Mes of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
+
+
+type newfixpoint_expr =
+ identifier * annot * Topconstr.local_binder list * Topconstr.constr_expr * Topconstr.constr_expr
+
+let rec abstract_rawconstr c = function
+ | [] -> c
+ | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl)
+ | Topconstr.LocalRawAssum (idl,k,t)::bl ->
+ List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl
+ (abstract_rawconstr c bl)
+
+let interp_casted_constr_with_implicits sigma env impls c =
+(* Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *)
+ Constrintern.intern_gen false sigma env ~impls
+ ~allow_patvar:false ~ltacvars:([],[]) c
+
+
+(*
+ Construct a fixpoint as a Rawterm
+ and not as a constr
+*)
+let build_newrecursive
+(lnameargsardef) =
+ let env0 = Global.env()
+ and sigma = Evd.empty
+ in
+ let (rec_sign,rec_impls) =
+ List.fold_left
+ (fun (env,impls) ((_,recname),_,bl,arityc,_) ->
+ let arityc = Topconstr.prod_constr_expr arityc bl in
+ let arity = Constrintern.interp_type sigma env0 arityc in
+ let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
+ (Environ.push_named (recname,None,arity) env, (recname,impl) :: impls))
+ (env0,[]) lnameargsardef in
+ let rec_impls = Constrintern.set_internalization_env_params rec_impls [] in
+ let recdef =
+ (* Declare local notations *)
+ let fs = States.freeze() in
+ let def =
+ try
+ List.map
+ (fun (_,_,bl,_,def) ->
+ let def = abstract_rawconstr def bl in
+ interp_casted_constr_with_implicits
+ sigma rec_sign rec_impls def
+ )
+ lnameargsardef
+ with e ->
+ States.unfreeze fs; raise e in
+ States.unfreeze fs; def
+ in
+ recdef,rec_impls
+
+
+let compute_annot (name,annot,args,types,body) =
+ let names = List.map snd (Topconstr.names_of_local_assums args) in
+ match annot with
+ | None ->
+ if List.length names > 1 then
+ user_err_loc
+ (dummy_loc,"Function",
+ Pp.str "the recursive argument needs to be specified");
+ let new_annot = (id_of_name (List.hd names)) in
+ (name,Struct new_annot,args,types,body)
+ | Some r -> (name,r,args,types,body)
+
+
+(* Checks whether or not the mutual bloc is recursive *)
+let rec is_rec names =
+ let names = List.fold_right Idset.add names Idset.empty in
+ let check_id id names = Idset.mem id names in
+ let rec lookup names = function
+ | RVar(_,id) -> check_id id names
+ | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false
+ | RCast(_,b,_) -> lookup names b
+ | RRec _ -> error "RRec not handled"
+ | RIf(_,b,_,lhs,rhs) ->
+ (lookup names b) || (lookup names lhs) || (lookup names rhs)
+ | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b) ->
+ lookup names t || lookup (Nameops.name_fold Idset.remove na names) b
+ | RLetTuple(_,nal,_,t,b) -> lookup names t ||
+ lookup
+ (List.fold_left
+ (fun acc na -> Nameops.name_fold Idset.remove na acc)
+ names
+ nal
+ )
+ b
+ | RApp(_,f,args) -> List.exists (lookup names) (f::args)
+ | RCases(_,_,_,el,brl) ->
+ List.exists (fun (e,_) -> lookup names e) el ||
+ List.exists (lookup_br names) brl
+ and lookup_br names (_,idl,_,rt) =
+ let new_names = List.fold_right Idset.remove idl names in
+ lookup new_names rt
+ in
+ lookup names
+
+let rec local_binders_length = function
+ (* Assume that no `{ ... } contexts occur *)
+ | [] -> 0
+ | Topconstr.LocalRawDef _::bl -> 1 + local_binders_length bl
+ | Topconstr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
+
+let prepare_body (name,annot,args,types,body) rt =
+ let n = local_binders_length args in
+(* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_rawconstr rt); *)
+ let fun_args,rt' = chop_rlambda_n n rt in
+ (fun_args,rt')
+
+
+let derive_inversion fix_names =
+ try
+ (* we first transform the fix_names identifier into their corresponding constant *)
+ let fix_names_as_constant =
+ List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names
+ in
+ (*
+ Then we check that the graphs have been defined
+ If one of the graphs haven't been defined
+ we do nothing
+ *)
+ List.iter (fun c -> ignore (find_Function_infos c)) fix_names_as_constant ;
+ try
+ Invfun.derive_correctness
+ Functional_principles_types.make_scheme
+ functional_induction
+ fix_names_as_constant
+ (*i The next call to mk_rel_id is valid since we have just construct the graph
+ Ensures by : register_built
+ i*)
+ (List.map
+ (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id)))
+ fix_names
+ )
+ with e ->
+ msg_warning
+ (str "Cannot built inversion information" ++
+ if do_observe () then Cerrors.explain_exn e else mt ())
+ with _ -> ()
+
+let warning_error names e =
+ let e_explain e =
+ match e with
+ | ToShow e -> spc () ++ Cerrors.explain_exn e
+ | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()
+ in
+ match e with
+ | Building_graph e ->
+ Pp.msg_warning
+ (str "Cannot define graph(s) for " ++
+ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+ e_explain e)
+ | Defining_principle e ->
+ Pp.msg_warning
+ (str "Cannot define principle(s) for "++
+ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+ e_explain e)
+ | _ -> anomaly ""
+
+let error_error names e =
+ let e_explain e =
+ match e with
+ | ToShow e -> spc () ++ Cerrors.explain_exn e
+ | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()
+ in
+ match e with
+ | Building_graph e ->
+ errorlabstrm ""
+ (str "Cannot define graph(s) for " ++
+ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+ e_explain e)
+ | _ -> anomaly ""
+
+let generate_principle on_error
+ is_general do_built fix_rec_l recdefs interactive_proof
+ (continue_proof : int -> Names.constant array -> Term.constr array -> int ->
+ Tacmach.tactic) : unit =
+ let names = List.map (function ((_, 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
+ try
+ (* We then register the Inductive graphs of the functions *)
+ Rawterm_to_relation.build_inductive names funs_args funs_types recdefs;
+ if do_built
+ then
+ begin
+ (*i The next call to mk_rel_id is valid since we have just construct the graph
+ Ensures by : do_built
+ i*)
+ let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in
+ let ind_kn =
+ fst (locate_with_msg
+ (pr_reference f_R_mut++str ": Not an inductive type!")
+ locate_ind
+ f_R_mut)
+ in
+ let fname_kn (fname,_,_,_,_) =
+ let f_ref = Ident fname in
+ locate_with_msg
+ (pr_reference f_ref++str ": Not an inductive type!")
+ locate_constant
+ f_ref
+ in
+ let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in
+ let _ =
+ list_map_i
+ (fun i x ->
+ let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in
+ let princ_type = Typeops.type_of_constant (Global.env()) princ
+ in
+ Functional_principles_types.generate_functional_principle
+ interactive_proof
+ princ_type
+ None
+ None
+ funs_kn
+ i
+ (continue_proof 0 [|funs_kn.(i)|])
+ )
+ 0
+ fix_rec_l
+ in
+ Array.iter (add_Function is_general) funs_kn;
+ ()
+ end
+ with e ->
+ on_error names e
+
+let register_struct is_rec fixpoint_exprl =
+ match fixpoint_exprl with
+ | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
+ let ce,imps =
+ Command.interp_definition
+ (Flags.boxed_definitions ()) bl None body (Some ret_type)
+ in
+ Command.declare_definition
+ fname (Decl_kinds.Global,Decl_kinds.Definition)
+ ce imps (fun _ _ -> ())
+ | _ ->
+ let fixpoint_exprl =
+ List.map (fun ((name,annot,bl,types,body),ntn) ->
+ ((name,annot,bl,types,Some body),ntn)) fixpoint_exprl in
+ Command.do_fixpoint fixpoint_exprl (Flags.boxed_definitions())
+
+let generate_correction_proof_wf f_ref tcc_lemma_ref
+ is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+ (_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic =
+ Functional_principles_proofs.prove_principle_for_gen
+ (f_ref,functional_ref,eq_ref)
+ tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation
+
+
+let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
+ pre_hook
+ =
+ let type_of_f = Topconstr.prod_constr_expr ret_type args in
+ let rec_arg_num =
+ let names =
+ List.map
+ snd
+ (Topconstr.names_of_local_assums args)
+ in
+ match wf_arg with
+ | None ->
+ if List.length names = 1 then 1
+ else error "Recursive argument must be specified"
+ | Some wf_arg ->
+ list_index (Name wf_arg) names
+ in
+ let unbounded_eq =
+ let f_app_args =
+ Topconstr.CAppExpl
+ (dummy_loc,
+ (None,(Ident (dummy_loc,fname))) ,
+ (List.map
+ (function
+ | _,Anonymous -> assert false
+ | _,Name e -> (Topconstr.mkIdentC e)
+ )
+ (Topconstr.names_of_local_assums args)
+ )
+ )
+ in
+ Topconstr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))),
+ [(f_app_args,None);(body,None)])
+ in
+ let eq = Topconstr.prod_constr_expr unbounded_eq args in
+ let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type
+ nb_args relation =
+ try
+ pre_hook
+ (generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
+ functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+ );
+ derive_inversion [fname]
+ with e ->
+ (* No proof done *)
+ ()
+ in
+ Recdef.recursive_definition
+ is_mes fname rec_impls
+ type_of_f
+ wf_rel_expr
+ rec_arg_num
+ eq
+ hook
+ using_lemmas
+
+
+let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type body =
+ let wf_arg_type,wf_arg =
+ match wf_arg with
+ | None ->
+ begin
+ match args with
+ | [Topconstr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x
+ | _ -> error "Recursive argument must be specified"
+ end
+ | Some wf_args ->
+ try
+ match
+ List.find
+ (function
+ | Topconstr.LocalRawAssum(l,k,t) ->
+ List.exists
+ (function (_,Name id) -> id = wf_args | _ -> false)
+ l
+ | _ -> false
+ )
+ args
+ with
+ | Topconstr.LocalRawAssum(_,k,t) -> t,wf_args
+ | _ -> assert false
+ with Not_found -> assert false
+ in
+ let ltof =
+ let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in
+ Libnames.Qualid (dummy_loc,Libnames.qualid_of_path
+ (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof")))
+ in
+ let fun_from_mes =
+ let applied_mes =
+ Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) in
+ Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes)
+ in
+ let wf_rel_from_mes =
+ Topconstr.mkAppC(Topconstr.mkRefC ltof,[wf_arg_type;fun_from_mes])
+ in
+ register_wf ~is_mes:true fname rec_impls wf_rel_from_mes (Some wf_arg)
+ using_lemmas args ret_type body
+
+
+let do_generate_principle on_error register_built interactive_proof fixpoint_exprl =
+ let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
+ let _is_struct =
+ match fixpoint_exprl with
+ | [(((_,name),Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] ->
+ let pre_hook =
+ generate_principle
+ on_error
+ true
+ register_built
+ fixpoint_exprl
+ recdefs
+ true
+ in
+ if register_built
+ then register_wf name rec_impls wf_rel wf_x using_lemmas args types body pre_hook;
+ false
+ | [(((_,name),Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] ->
+ let pre_hook =
+ generate_principle
+ on_error
+ true
+ register_built
+ fixpoint_exprl
+ recdefs
+ true
+ in
+ if register_built
+ then register_mes name rec_impls wf_mes wf_x using_lemmas args types body pre_hook;
+ true
+ | _ ->
+ let fix_names =
+ List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl
+ in
+ let is_one_rec = is_rec fix_names in
+ let old_fixpoint_exprl =
+ List.map
+ (function
+ | (name,Some (Struct id),args,types,body),_ ->
+ let annot =
+ try Some (dummy_loc, id), Topconstr.CStructRec
+ with Not_found ->
+ raise (UserError("",str "Cannot find argument " ++
+ Ppconstr.pr_id id))
+ in
+ (name,annot,args,types,body),([]:Vernacexpr.decl_notation list)
+ | (name,None,args,types,body),recdef ->
+ let names = (Topconstr.names_of_local_assums args) in
+ if is_one_rec recdef && List.length names > 1 then
+ user_err_loc
+ (dummy_loc,"Function",
+ Pp.str "the recursive argument needs to be specified in Function")
+ else
+ let loc, na = List.hd names in
+ (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body),
+ ([]:Vernacexpr.decl_notation list)
+ | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_->
+ error
+ ("Cannot use mutual definition with well-founded recursion or measure")
+ )
+ (List.combine fixpoint_exprl recdefs)
+ in
+ (* ok all the expressions are structural *)
+ let fix_names =
+ List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl
+ in
+ let is_rec = List.exists (is_rec fix_names) recdefs in
+ if register_built then register_struct is_rec old_fixpoint_exprl;
+ generate_principle
+ on_error
+ false
+ register_built
+ fixpoint_exprl
+ recdefs
+ interactive_proof
+ (Functional_principles_proofs.prove_princ_for_struct interactive_proof);
+ if register_built then derive_inversion fix_names;
+ true;
+ in
+ ()
+
+open Topconstr
+let rec add_args id new_args b =
+ match b with
+ | CRef r ->
+ begin match r with
+ | Libnames.Ident(loc,fname) when fname = id ->
+ CAppExpl(dummy_loc,(None,r),new_args)
+ | _ -> b
+ end
+ | CFix _ | CCoFix _ -> anomaly "add_args : todo"
+ | CArrow(loc,b1,b2) ->
+ CArrow(loc,add_args id new_args b1, add_args id new_args b2)
+ | CProdN(loc,nal,b1) ->
+ CProdN(loc,
+ List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
+ add_args id new_args b1)
+ | CLambdaN(loc,nal,b1) ->
+ CLambdaN(loc,
+ List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
+ add_args id new_args b1)
+ | CLetIn(loc,na,b1,b2) ->
+ CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
+ | CAppExpl(loc,(pf,r),exprl) ->
+ begin
+ match r with
+ | Libnames.Ident(loc,fname) when fname = id ->
+ CAppExpl(loc,(pf,r),new_args@(List.map (add_args id new_args) exprl))
+ | _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl)
+ end
+ | CApp(loc,(pf,b),bl) ->
+ CApp(loc,(pf,add_args id new_args b),
+ List.map (fun (e,o) -> add_args id new_args e,o) bl)
+ | CCases(loc,sty,b_option,cel,cal) ->
+ CCases(loc,sty,Option.map (add_args id new_args) b_option,
+ List.map (fun (b,(na,b_option)) ->
+ add_args id new_args b,
+ (na,Option.map (add_args id new_args) b_option)) cel,
+ List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
+ )
+ | CLetTuple(loc,nal,(na,b_option),b1,b2) ->
+ CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option),
+ add_args id new_args b1,
+ add_args id new_args b2
+ )
+
+ | CIf(loc,b1,(na,b_option),b2,b3) ->
+ CIf(loc,add_args id new_args b1,
+ (na,Option.map (add_args id new_args) b_option),
+ add_args id new_args b2,
+ add_args id new_args b3
+ )
+ | CHole _ -> b
+ | CPatVar _ -> b
+ | CEvar _ -> b
+ | CSort _ -> b
+ | CCast(loc,b1,CastConv(ck,b2)) ->
+ CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2))
+ | CCast(loc,b1,CastCoerce) ->
+ CCast(loc,add_args id new_args b1,CastCoerce)
+ | CRecord (loc, w, pars) ->
+ CRecord (loc,
+ (match w with Some w -> Some (add_args id new_args w) | _ -> None),
+ List.map (fun (e,o) -> e, add_args id new_args o) pars)
+ | CNotation _ -> anomaly "add_args : CNotation"
+ | CGeneralization _ -> anomaly "add_args : CGeneralization"
+ | CPrim _ -> b
+ | CDelimiters _ -> anomaly "add_args : CDelimiters"
+ | CDynamic _ -> anomaly "add_args : CDynamic"
+exception Stop of Topconstr.constr_expr
+
+
+(* [chop_n_arrow n t] chops the [n] first arrows in [t]
+ Acts on Topconstr.constr_expr
+*)
+let rec chop_n_arrow n t =
+ if n <= 0
+ 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 with
+ | Topconstr.CArrow(_,_,t) -> (* If we have an arrow, we discard it and recall [chop_n_arrow] *)
+ chop_n_arrow (n-1) t
+ | Topconstr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result 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
+ recall [chop_n_arrow], either this product contains more arrows
+ than the number we need to chop and then we return the new type
+ *)
+ begin
+ try
+ let new_n =
+ let rec aux (n:int) = function
+ [] -> n
+ | (nal,k,t'')::nal_ta' ->
+ let nal_l = List.length nal in
+ if n >= nal_l
+ then
+ aux (n - nal_l) nal_ta'
+ else
+ let new_t' =
+ Topconstr.CProdN(dummy_loc,
+ ((snd (list_chop n nal)),k,t'')::nal_ta',t')
+ in
+ raise (Stop new_t')
+ in
+ aux n nal_ta'
+ in
+ chop_n_arrow new_n t'
+ with Stop t -> t
+ end
+ | _ -> anomaly "Not enough products"
+
+
+let rec get_args b t : Topconstr.local_binder list *
+ Topconstr.constr_expr * Topconstr.constr_expr =
+ match b with
+ | Topconstr.CLambdaN (loc, (nal_ta), 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) ->
+ (Topconstr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
+ end
+ | _ -> [],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 ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) )
+ end
+ | _ -> raise (UserError ("", str "Not a function reference") )
+
+ in
+ Dumpglob.pause ();
+ (match c_body.const_body with
+ | None -> error "Cannot build a graph over an axiom !"
+ | Some b ->
+ let env = Global.env () in
+ let body = (force b) in
+ let extern_body,extern_type =
+ with_full_print
+ (fun () ->
+ (Constrextern.extern_constr false env body,
+ Constrextern.extern_type false env
+ (Typeops.type_of_constant_type env c_body.const_type)
+ )
+ )
+ ()
+ in
+ let (nal_tas,b,t) = get_args extern_body extern_type in
+ let expr_list =
+ match b with
+ | Topconstr.CFix(loc,l_id,fixexprl) ->
+ let l =
+ List.map
+ (fun (id,(n,recexp),bl,t,b) ->
+ let loc, rec_id = Option.get n in
+ let new_args =
+ List.flatten
+ (List.map
+ (function
+ | Topconstr.LocalRawDef (na,_)-> []
+ | Topconstr.LocalRawAssum (nal,_,_) ->
+ List.map
+ (fun (loc,n) ->
+ CRef(Libnames.Ident(loc, Nameops.out_name n)))
+ nal
+ )
+ nal_tas
+ )
+ in
+ let b' = add_args (snd id) new_args b in
+ (id, Some (Struct rec_id),nal_tas@bl,t,b')
+ )
+ fixexprl
+ in
+ l
+ | _ ->
+ let id = id_of_label (con_label c) in
+ [((dummy_loc,id),None,nal_tas,t,b)]
+ in
+ do_generate_principle error_error false false expr_list;
+ (* We register the infos *)
+ let mp,dp,_ = repr_con c in
+ List.iter
+ (fun ((_,id),_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id)))
+ expr_list);
+ Dumpglob.continue ()
+
+
+(* let make_graph _ = assert false *)
+
+let do_generate_principle = do_generate_principle warning_error true
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-02 10:23:39 +0000