summaryrefslogtreecommitdiff
path: root/contrib/funind
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind')
-rw-r--r--contrib/funind/indfun.ml468
-rw-r--r--contrib/funind/indfun_common.ml319
-rw-r--r--contrib/funind/indfun_common.mli41
-rw-r--r--contrib/funind/indfun_main.ml4201
-rw-r--r--contrib/funind/invfun.ml148
-rw-r--r--contrib/funind/new_arg_principle.ml1770
-rw-r--r--contrib/funind/new_arg_principle.mli34
-rw-r--r--contrib/funind/rawterm_to_relation.ml1012
-rw-r--r--contrib/funind/rawterm_to_relation.mli16
-rw-r--r--contrib/funind/rawtermops.ml525
-rw-r--r--contrib/funind/rawtermops.mli111
-rw-r--r--contrib/funind/tacinv.ml4656
-rw-r--r--contrib/funind/tacinvutils.ml18
-rw-r--r--contrib/funind/tacinvutils.mli7
14 files changed, 4995 insertions, 331 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
new file mode 100644
index 00000000..2fcdd3a7
--- /dev/null
+++ b/contrib/funind/indfun.ml
@@ -0,0 +1,468 @@
+open Util
+open Names
+open Term
+
+open Pp
+open Indfun_common
+open Libnames
+open Rawterm
+open Declarations
+
+type annot =
+ Struct of identifier
+ | Wf of Topconstr.constr_expr * identifier option
+ | Mes of Topconstr.constr_expr * identifier option
+
+
+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,t)::bl ->
+ List.fold_right (fun x b -> Topconstr.mkLambdaC([x],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:([],impls)
+ ~allow_soapp:false ~ltacvars:([],[]) c
+
+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 = Command.generalize_constr_expr arityc bl in
+ let arity = Constrintern.interp_type sigma env0 arityc in
+ let impl =
+ if Impargs.is_implicit_args()
+ then Impargs.compute_implicits env0 arity
+ else [] in
+ let impls' =(recname,([],impl,Notation.compute_arguments_scope arity))::impls in
+ (Environ.push_named (recname,None,arity) env, impls'))
+ (env0,[]) lnameargsardef 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
+
+
+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,"GenFixpoint",
+ 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)
+
+
+
+let rec is_rec names =
+ let names = List.fold_right Idset.add names Idset.empty in
+ let check_id id = Idset.mem id names in
+ let rec lookup = function
+ | RVar(_,id) -> check_id id
+ | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false
+ | RCast(_,b,_,_) -> lookup b
+ | RRec _ -> assert false
+ | RIf _ -> failwith "Rif not implemented"
+ | RLetIn(_,_,t,b) | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetTuple(_,_,_,t,b) ->
+ lookup t || lookup b
+ | RApp(_,f,args) -> List.exists lookup (f::args)
+ | RCases(_,_,el,brl) ->
+ List.exists (fun (e,_) -> lookup e) el ||
+ List.exists (fun (_,_,_,ret)-> lookup ret) brl
+ in
+ lookup
+
+let prepare_body (name,annot,args,types,body) rt =
+ let n = (Topconstr.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 generate_principle
+ do_built fix_rec_l recdefs interactive_proof parametrize
+ (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) =
+ 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 parametrize names funs_args funs_types recdefs;
+ if do_built
+ then
+ begin
+ 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 (dummy_loc,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 _ =
+ Util.list_map_i
+ (fun i x ->
+ let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in
+ let princ_type =
+ (Global.lookup_constant princ).Declarations.const_type
+ in
+ New_arg_principle.generate_functional_principle
+ interactive_proof
+ princ_type
+ None
+ None
+ funs_kn
+ i
+ (continue_proof 0 [|funs_kn.(i)|])
+ )
+ 0
+ fix_rec_l
+ in
+ ()
+ end
+ with e ->
+ Pp.msg_warning (Cerrors.explain_exn e)
+
+
+let register_struct is_rec fixpoint_exprl =
+ match fixpoint_exprl with
+ | [(fname,_,bl,ret_type,body),_] when not is_rec ->
+ Command.declare_definition
+ fname
+ (Decl_kinds.Global,Options.boxed_definitions (),Decl_kinds.Definition)
+ bl
+ None
+ body
+ (Some ret_type)
+ (fun _ _ -> ())
+ | _ ->
+ Command.build_recursive fixpoint_exprl (Options.boxed_definitions())
+
+
+let generate_correction_proof_wf tcc_lemma_ref
+ is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+ (_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic =
+ Recdef.prove_principle tcc_lemma_ref
+ is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+
+
+let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
+ pre_hook
+ =
+ let type_of_f = Command.generalize_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 ->
+ Util.list_index (Name wf_arg) names
+ in
+ let unbounded_eq =
+ let f_app_args =
+ Topconstr.CApp
+ (dummy_loc,
+ (None,Topconstr.mkIdentC fname) ,
+ (List.map
+ (function
+ | _,Anonymous -> assert false
+ | _,Name e -> (Topconstr.mkIdentC e,None)
+ )
+ (Topconstr.names_of_local_assums args)
+ )
+ )
+ in
+ Topconstr.CApp (dummy_loc,(None,Topconstr.mkIdentC (id_of_string "eq")),
+ [(f_app_args,None);(body,None)])
+ in
+ let eq = Command.generalize_constr_expr unbounded_eq args in
+ let hook tcc_lemma_ref f_ref eq_ref rec_arg_num rec_arg_type nb_args relation =
+ try
+ pre_hook
+ (generate_correction_proof_wf tcc_lemma_ref is_mes
+ f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+ );
+ Command.save_named true
+ with e ->
+ (* No proof done *)
+ ()
+ in
+ Recdef.recursive_definition
+ is_mes fname
+ type_of_f
+ wf_rel_expr
+ rec_arg_num
+ eq
+ hook
+
+
+let register_mes fname wf_mes_expr wf_arg args ret_type body =
+ let wf_arg_type,wf_arg =
+ match wf_arg with
+ | None ->
+ begin
+ match args with
+ | [Topconstr.LocalRawAssum ([(_,Name x)],t)] -> t,x
+ | _ -> error "Recursive argument must be specified"
+ end
+ | Some wf_args ->
+ try
+ match
+ List.find
+ (function
+ | Topconstr.LocalRawAssum(l,t) ->
+ List.exists
+ (function (_,Name id) -> id = wf_args | _ -> false)
+ l
+ | _ -> false
+ )
+ args
+ with
+ | Topconstr.LocalRawAssum(_,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_sp
+ (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)],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 wf_rel_from_mes (Some wf_arg) args ret_type body
+
+
+let do_generate_principle register_built interactive_proof fixpoint_exprl =
+ let recdefs = build_newrecursive fixpoint_exprl in
+ let _is_struct =
+ match fixpoint_exprl with
+ | [((name,Some (Wf (wf_rel,wf_x)),args,types,body))] ->
+ let pre_hook =
+ generate_principle
+ register_built
+ fixpoint_exprl
+ recdefs
+ true
+ false
+ in
+ if register_built then register_wf name wf_rel wf_x args types body pre_hook;
+ false
+ | [((name,Some (Mes (wf_mes,wf_x)),args,types,body))] ->
+ let pre_hook =
+ generate_principle
+ register_built
+ fixpoint_exprl
+ recdefs
+ true
+ false
+ in
+ if register_built then register_mes name wf_mes wf_x args types body pre_hook;
+ false
+ | _ ->
+ 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 names =
+ List.map
+ snd
+ (Topconstr.names_of_local_assums args)
+ in
+ let annot =
+ try Util.list_index (Name id) names - 1, Topconstr.CStructRec
+ with Not_found -> raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id))
+ in
+ (name,annot,args,types,body),(None:Vernacexpr.decl_notation)
+ | (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
+ Util.user_err_loc
+ (Util.dummy_loc,"GenFixpoint",
+ Pp.str "the recursive argument needs to be specified")
+ else
+ (name,(0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
+ | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_->
+ error
+ ("Cannot use mutual definition with well-founded recursion")
+ )
+ (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
+ register_built
+ fixpoint_exprl
+ recdefs
+ interactive_proof
+ true
+ (New_arg_principle.prove_princ_for_struct interactive_proof);
+ true
+
+ in
+ ()
+
+let make_graph (id:identifier) =
+ let c_body =
+ try
+ let c = const_of_id id in
+ Global.lookup_constant c
+ with Not_found ->
+ raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id) )
+ in
+
+ 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 =
+ let old_implicit_args = Impargs.is_implicit_args ()
+ and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
+ and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
+ let old_rawprint = !Options.raw_print in
+ Options.raw_print := true;
+ Impargs.make_implicit_args false;
+ Impargs.make_strict_implicit_args false;
+ Impargs.make_contextual_implicit_args false;
+ try
+ let res = Constrextern.extern_constr false env body in
+ let res' = Constrextern.extern_type false env c_body.const_type in
+ Impargs.make_implicit_args old_implicit_args;
+ Impargs.make_strict_implicit_args old_strict_implicit_args;
+ Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+ Options.raw_print := old_rawprint;
+ res,res'
+ with
+ | UserError(s,msg) as e ->
+ Impargs.make_implicit_args old_implicit_args;
+ Impargs.make_strict_implicit_args old_strict_implicit_args;
+ Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+ Options.raw_print := old_rawprint;
+ raise e
+ | e ->
+ Impargs.make_implicit_args old_implicit_args;
+ Impargs.make_strict_implicit_args old_strict_implicit_args;
+ Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+ Options.raw_print := old_rawprint;
+ raise e
+ in
+ let expr_list =
+ match extern_body with
+ | Topconstr.CFix(loc,l_id,fixexprl) ->
+ let l =
+ List.map
+ (fun (id,(n,recexp),bl,t,b) ->
+ let nal =
+ List.flatten
+ (List.map
+ (function
+ | Topconstr.LocalRawDef (na,_)-> []
+ | Topconstr.LocalRawAssum (nal,_) -> nal
+ )
+ bl
+ )
+ in
+ let rec_id =
+ match List.nth nal n with |(_,Name id) -> id | _ -> anomaly ""
+ in
+ (id, Some (Struct rec_id),bl,t,b)
+ )
+ fixexprl
+ in
+ l
+ | _ ->
+ let rec get_args b t : Topconstr.local_binder list *
+ Topconstr.constr_expr * Topconstr.constr_expr =
+(* Pp.msgnl (str "body: " ++Ppconstr.pr_lconstr_expr b); *)
+(* Pp.msgnl (str "type: " ++ Ppconstr.pr_lconstr_expr t); *)
+(* Pp.msgnl (fnl ()); *)
+ 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 rec chop_n_arrow n t =
+ if n > 0
+ then
+ match t with
+ | Topconstr.CArrow(_,_,t) -> chop_n_arrow (n-1) t
+ | Topconstr.CProdN(_,nal_ta',t') ->
+ let n' =
+ List.fold_left
+ (fun n (nal,t'') ->
+ n+List.length nal) n nal_ta'
+ in
+ assert (n'<= n);
+ chop_n_arrow (n - n') t'
+ | _ -> anomaly "Not enough products"
+ else t
+ in
+ let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in
+ (List.map (fun (nal,ta) -> (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t''
+ end
+ | _ -> [],b,t
+ in
+ let nal_tas,b,t = get_args extern_body extern_type in
+ [(id,None,nal_tas,t,b)]
+
+ in
+ do_generate_principle false false expr_list
+(* let make_graph _ = assert false *)
+
+let do_generate_principle = do_generate_principle true
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
new file mode 100644
index 00000000..b32dfacb
--- /dev/null
+++ b/contrib/funind/indfun_common.ml
@@ -0,0 +1,319 @@
+open Names
+open Pp
+
+open Libnames
+
+let mk_prefix pre id = id_of_string (pre^(string_of_id id))
+let mk_rel_id = mk_prefix "R_"
+
+let msgnl m =
+ ()
+
+let invalid_argument s = raise (Invalid_argument s)
+
+(* let idtbl = Hashtbl.create 29 *)
+(* let reset_name () = Hashtbl.clear idtbl *)
+
+(* let fresh_id s = *)
+(* try *)
+(* let id = Hashtbl.find idtbl s in *)
+(* incr id; *)
+(* id_of_string (s^(string_of_int !id)) *)
+(* with Not_found -> *)
+(* Hashtbl.add idtbl s (ref (-1)); *)
+(* id_of_string s *)
+
+(* let fresh_name s = Name (fresh_id s) *)
+(* let get_name ?(default="H") = function *)
+(* | Anonymous -> fresh_name default *)
+(* | Name n -> Name n *)
+
+
+
+let fresh_id avoid s = Termops.next_global_ident_away true (id_of_string s) avoid
+
+let fresh_name avoid s = Name (fresh_id avoid s)
+
+let get_name avoid ?(default="H") = function
+ | Anonymous -> fresh_name avoid default
+ | Name n -> Name n
+
+let array_get_start a =
+ try
+ Array.init
+ (Array.length a - 1)
+ (fun i -> a.(i))
+ with Invalid_argument "index out of bounds" ->
+ invalid_argument "array_get_start"
+
+let id_of_name = function
+ Name id -> id
+ | _ -> raise Not_found
+
+let locate ref =
+ let (loc,qid) = qualid_of_reference ref in
+ Nametab.locate qid
+
+let locate_ind ref =
+ match locate ref with
+ | IndRef x -> x
+ | _ -> raise Not_found
+
+let locate_constant ref =
+ match locate ref with
+ | ConstRef x -> x
+ | _ -> raise Not_found
+
+
+let locate_with_msg msg f x =
+ try
+ f x
+ with
+ | Not_found -> raise (Util.UserError("", msg))
+ | e -> raise e
+
+
+let filter_map filter f =
+ let rec it = function
+ | [] -> []
+ | e::l ->
+ if filter e
+ then
+ (f e) :: it l
+ else it l
+ in
+ it
+
+
+let chop_rlambda_n =
+ let rec chop_lambda_n acc n rt =
+ if n == 0
+ then List.rev acc,rt
+ else
+ match rt with
+ | Rawterm.RLambda(_,name,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
+ | Rawterm.RLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
+ | _ ->
+ raise (Util.UserError("chop_rlambda_n",
+ str "chop_rlambda_n: Not enough Lambdas"))
+ in
+ chop_lambda_n []
+
+let chop_rprod_n =
+ let rec chop_prod_n acc n rt =
+ if n == 0
+ then List.rev acc,rt
+ else
+ match rt with
+ | Rawterm.RProd(_,name,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
+ | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
+ in
+ chop_prod_n []
+
+
+
+let list_union_eq eq_fun l1 l2 =
+ let rec urec = function
+ | [] -> l2
+ | a::l -> if List.exists (eq_fun a) l2 then urec l else a::urec l
+ in
+ urec l1
+
+let list_add_set_eq eq_fun x l =
+ if List.exists (eq_fun x) l then l else x::l
+
+
+
+
+let const_of_id id =
+ let _,princ_ref =
+ qualid_of_reference (Libnames.Ident (Util.dummy_loc,id))
+ in
+ try Nametab.locate_constant princ_ref
+ with Not_found -> Util.error ("cannot find "^ string_of_id id)
+
+let def_of_const t =
+ match (Term.kind_of_term t) with
+ Term.Const sp ->
+ (try (match (Global.lookup_constant sp) with
+ {Declarations.const_body=Some c} -> Declarations.force c
+ |_ -> assert false)
+ with _ -> assert false)
+ |_ -> assert false
+
+let coq_constant s =
+ Coqlib.gen_constant_in_modules "RecursiveDefinition"
+ (Coqlib.init_modules @ Coqlib.arith_modules) s;;
+
+let constant sl s =
+ constr_of_reference
+ (Nametab.locate (make_qualid(Names.make_dirpath
+ (List.map id_of_string (List.rev sl)))
+ (id_of_string s)));;
+
+let find_reference sl s =
+ (Nametab.locate (make_qualid(Names.make_dirpath
+ (List.map id_of_string (List.rev sl)))
+ (id_of_string s)));;
+
+let eq = lazy(coq_constant "eq")
+let refl_equal = lazy(coq_constant "refl_equal")
+
+
+(* (\************************************************\) *)
+(* (\* Should be removed latter *\) *)
+(* (\* Comes from new induction (cf Pierre) *\) *)
+(* (\************************************************\) *)
+
+(* open Sign *)
+(* open Term *)
+
+(* type elim_scheme = *)
+
+(* (\* { (\\* lists are in reverse order! *\\) *\) *)
+(* (\* params: rel_context; (\\* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *\\) *\) *)
+(* (\* predicates: rel_context; (\\* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *\\) *\) *)
+(* (\* branches: rel_context; (\\* branchr,...,branch1 *\\) *\) *)
+(* (\* args: rel_context; (\\* (xni, Ti_ni) ... (x1, Ti_1) *\\) *\) *)
+(* (\* indarg: rel_declaration option; (\\* Some (H,I prm1..prmp x1...xni) if present, None otherwise *\\) *\) *)
+(* (\* concl: types; (\\* Qi x1...xni HI, some prmis may not be present *\\) *\) *)
+(* (\* indarg_in_concl:bool; (\\* true if HI appears at the end of conclusion (dependent scheme) *\\) *\) *)
+(* (\* } *\) *)
+
+
+
+(* let occur_rel n c = *)
+(* let res = not (noccurn n c) in *)
+(* res *)
+
+(* let list_filter_firsts f l = *)
+(* let rec list_filter_firsts_aux f acc l = *)
+(* match l with *)
+(* | e::l' when f e -> list_filter_firsts_aux f (acc@[e]) l' *)
+(* | _ -> acc,l *)
+(* in *)
+(* list_filter_firsts_aux f [] l *)
+
+(* let count_rels_from n c = *)
+(* let rels = Termops.free_rels c in *)
+(* let cpt,rg = ref 0, ref n in *)
+(* while Util.Intset.mem !rg rels do *)
+(* cpt:= !cpt+1; rg:= !rg+1; *)
+(* done; *)
+(* !cpt *)
+
+(* let count_nonfree_rels_from n c = *)
+(* let rels = Termops.free_rels c in *)
+(* if Util.Intset.exists (fun x -> x >= n) rels then *)
+(* let cpt,rg = ref 0, ref n in *)
+(* while not (Util.Intset.mem !rg rels) do *)
+(* cpt:= !cpt+1; rg:= !rg+1; *)
+(* done; *)
+(* !cpt *)
+(* else raise Not_found *)
+
+(* (\* cuts a list in two parts, first of size n. Size must be greater than n *\) *)
+(* let cut_list n l = *)
+(* let rec cut_list_aux acc n l = *)
+(* if n<=0 then acc,l *)
+(* else match l with *)
+(* | [] -> assert false *)
+(* | e::l' -> cut_list_aux (acc@[e]) (n-1) l' in *)
+(* let res = cut_list_aux [] n l in *)
+(* res *)
+
+(* let exchange_hd_prod subst_hd t = *)
+(* let hd,args= decompose_app t in mkApp (subst_hd,Array.of_list args) *)
+
+(* let compute_elim_sig elimt = *)
+(* (\* conclusion is the final (Qi ...) *\) *)
+(* let hyps,conclusion = decompose_prod_assum elimt in *)
+(* (\* ccl is conclusion where Qi (that is rel <something>) is replaced *)
+(* by a constant (Prop) to avoid it being counted as an arg or *)
+(* parameter in the following. *\) *)
+(* let ccl = exchange_hd_prod mkProp conclusion in *)
+(* (\* indarg is the inductive argument if it exists. If it exists it is *)
+(* the last hyp before the conclusion, so it is the first element of *)
+(* hyps. To know the first elmt is an inductive arg, we check if the *)
+(* it appears in the conclusion (as rel 1). If yes, then it is not *)
+(* an inductive arg, otherwise it is. There is a pathological case *)
+(* with False_inf where Qi is rel 1, so we first get rid of Qi in *)
+(* ccl. *\) *)
+(* (\* if last arg of ccl is an application then this a functional ind *)
+(* principle *\) let last_arg_ccl = *)
+(* try List.hd (List.rev (snd (decompose_app ccl))) *)
+(* with Failure "hd" -> mkProp in (\* dummy constr that is not an app *)
+(* *\) let hyps',indarg,dep = *)
+(* if isApp last_arg_ccl *)
+(* then *)
+(* hyps,None , false (\* no HI at all *\) *)
+(* else *)
+(* try *)
+(* if noccurn 1 ccl (\* rel 1 does not occur in ccl *\) *)
+(* then *)
+(* List.tl hyps , Some (List.hd hyps), false (\* it does not *)
+(* occur in concl *\) else *)
+(* List.tl hyps , Some (List.hd hyps) , true (\* it does occur in concl *\) *)
+(* with Failure s -> Util.error "cannot recognise an induction schema" *)
+(* in *)
+
+(* (\* Arguments [xni...x1] must appear in the conclusion, so we count *)
+(* successive rels appearing in conclusion **Qi is not considered a *)
+(* rel** *\) let nargs = count_rels_from *)
+(* (match indarg with *)
+(* | None -> 1 *)
+(* | Some _ -> 2) ccl in *)
+(* let args,hyps'' = cut_list nargs hyps' in *)
+(* let rel_is_pred (_,_,c) = isSort (snd(decompose_prod_assum c)) in *)
+(* let branches,hyps''' = *)
+(* list_filter_firsts (function x -> not (rel_is_pred x)) hyps'' *)
+(* in *)
+(* (\* Now we want to know which hyps remaining are predicates and which *)
+(* are parameters *\) *)
+(* (\* We rebuild *)
+
+(* forall (x1:Ti_1) (xni:Ti_ni) (HI:I prm1..prmp x1...xni), DUMMY *)
+(* x1...xni HI ^^^^^^^^^^^^^^^^^^^^^^^^^ ^^ *)
+(* optional *)
+(* opt *)
+
+(* Free rels appearing in this term are parameters. We catch all of *)
+(* them if HI is present. In this case the number of parameters is *)
+(* the number of free rels. Otherwise (principle generated by *)
+(* functional induction or by hand) WE GUESS that all parameters *)
+(* appear in Ti_js, IS THAT TRUE??. *)
+
+(* TODO: if we want to generalize to the case where arges are merged *)
+(* with branches (?) and/or where several predicates are cited in *)
+(* the conclusion, we should do something more precise than just *)
+(* counting free rels. *)
+(* *\) *)
+(* let concl_with_indarg = *)
+(* match indarg with *)
+(* | None -> ccl *)
+(* | Some c -> it_mkProd_or_LetIn ccl [c] in *)
+(* let concl_with_args = it_mkProd_or_LetIn concl_with_indarg args in *)
+(* (\* let nparams2 = Util.Intset.cardinal (Termops.free_rels concl_with_args) in *\) *)
+(* let nparams = *)
+(* try List.length (hyps'''@branches) - count_nonfree_rels_from 1 *)
+(* concl_with_args with Not_found -> 0 in *)
+(* let preds,params = cut_list (List.length hyps''' - nparams) hyps''' in *)
+(* let elimscheme = { *)
+(* params = params; *)
+(* predicates = preds; *)
+(* branches = branches; *)
+(* args = args; *)
+(* indarg = indarg; *)
+(* concl = conclusion; *)
+(* indarg_in_concl = dep; *)
+(* } *)
+(* in *)
+(* elimscheme *)
+
+(* let get_params elimt = *)
+(* (compute_elim_sig elimt).params *)
+(* (\************************************************\) *)
+(* (\* end of Should be removed latter *\) *)
+(* (\* Comes from new induction (cf Pierre) *\) *)
+(* (\************************************************\) *)
+
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
new file mode 100644
index 00000000..ab5195b0
--- /dev/null
+++ b/contrib/funind/indfun_common.mli
@@ -0,0 +1,41 @@
+open Names
+open Pp
+
+val mk_rel_id : identifier -> identifier
+
+val msgnl : std_ppcmds -> unit
+
+val invalid_argument : string -> 'a
+
+val fresh_id : identifier list -> string -> identifier
+val fresh_name : identifier list -> string -> name
+val get_name : identifier list -> ?default:string -> name -> name
+
+val array_get_start : 'a array -> 'a array
+
+val id_of_name : name -> identifier
+
+val locate_ind : Libnames.reference -> inductive
+val locate_constant : Libnames.reference -> constant
+val locate_with_msg :
+ Pp.std_ppcmds -> (Libnames.reference -> 'a) ->
+ Libnames.reference -> 'a
+
+val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list
+val list_union_eq :
+ ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
+val list_add_set_eq :
+ ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
+
+val chop_rlambda_n : int -> Rawterm.rawconstr ->
+ (name*Rawterm.rawconstr*bool) list * Rawterm.rawconstr
+
+val chop_rprod_n : int -> Rawterm.rawconstr ->
+ (name*Rawterm.rawconstr) list * Rawterm.rawconstr
+
+val def_of_const : Term.constr -> Term.constr
+val eq : Term.constr Lazy.t
+val refl_equal : Term.constr Lazy.t
+val const_of_id: identifier -> constant
+
+
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
new file mode 100644
index 00000000..7b3d8cbd
--- /dev/null
+++ b/contrib/funind/indfun_main.ml4
@@ -0,0 +1,201 @@
+(************************************************************************)
+(* 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 camlp4deps: "parsing/grammar.cma" i*)
+open Term
+open Names
+open Pp
+open Topconstr
+open Indfun_common
+open Indfun
+open Genarg
+
+TACTIC EXTEND newfuninv
+ [ "functional" "inversion" ident(hyp) ident(fname) ] ->
+ [
+ Invfun.invfun hyp fname
+ ]
+END
+
+
+let pr_fun_ind_using prc _ _ opt_c =
+ match opt_c with
+ | None -> mt ()
+ | Some c -> spc () ++ hov 2 (str "using" ++ spc () ++ prc c)
+
+ARGUMENT EXTEND fun_ind_using
+ TYPED AS constr_opt
+ PRINTED BY pr_fun_ind_using
+| [ "using" constr(c) ] -> [ Some c ]
+| [ ] -> [ None ]
+END
+
+let pr_intro_as_pat prc _ _ pat =
+ str "as" ++ spc () ++ pr_intro_pattern pat
+
+
+
+
+
+ARGUMENT EXTEND with_names TYPED AS intro_pattern PRINTED BY pr_intro_as_pat
+| [ "as" simple_intropattern(ipat) ] -> [ ipat ]
+| [] ->[ IntroAnonymous ]
+END
+
+
+let is_rec scheme_info =
+ let test_branche min acc (_,_,br) =
+ acc ||
+ (let new_branche = Sign.it_mkProd_or_LetIn mkProp (fst (Sign.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 scheme_info
+ then Tactics.new_induct
+ else
+ Tactics.new_destruct
+
+
+TACTIC EXTEND newfunind
+ ["new" "functional" "induction" constr(c) fun_ind_using(princl) with_names(pat)] ->
+ [
+ let f,args = decompose_app c in
+ fun g ->
+ let princ =
+ match princl with
+ | None -> (* No principle is given let's find the good one *)
+ let fname =
+ match kind_of_term f with
+ | Const c' ->
+ id_of_label (con_label c')
+ | _ -> Util.error "Must be used with a function"
+ in
+ let princ_name =
+ (
+ Indrec.make_elimination_ident
+ fname
+ (Tacticals.elimination_sort_of_goal g)
+ )
+ in
+ mkConst(const_of_id princ_name )
+ | Some princ -> princ
+ in
+ let princ_type = 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) (args@c_list)
+ in
+ let princ' = Some (princ,Rawterm.NoBindings) in
+ choose_dest_or_ind
+ princ_infos
+ args_as_induction_constr
+ princ'
+ pat g
+ ]
+END
+
+
+VERNAC ARGUMENT EXTEND rec_annotation2
+ [ "{" "struct" ident(id) "}"] -> [ Struct id ]
+| [ "{" "wf" constr(r) ident_opt(id) "}" ] -> [ Wf(r,id) ]
+| [ "{" "mes" constr(r) ident_opt(id) "}" ] -> [ Mes(r,id) ]
+END
+
+
+VERNAC ARGUMENT EXTEND binder2
+ [ "(" ne_ident_list(idl) ":" lconstr(c) ")"] ->
+ [
+ LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,c) ]
+END
+
+
+VERNAC ARGUMENT EXTEND rec_definition2
+ [ ident(id) binder2_list( bl)
+ rec_annotation2_opt(annot) ":" lconstr( type_)
+ ":=" lconstr(def)] ->
+ [let names = List.map snd (Topconstr.names_of_local_assums bl) in
+ let check_one_name () =
+ if List.length names > 1 then
+ Util.user_err_loc
+ (Util.dummy_loc,"GenFixpoint",
+ Pp.str "the recursive argument needs to be specified");
+ in
+ let check_exists_args an =
+ try
+ let id = match an with Struct id -> id | Wf(_,Some id) -> id | Mes(_,Some id) -> id | Wf(_,None) | Mes(_,None) -> failwith "check_exists_args" in
+ (try ignore(Util.list_index (Name id) names - 1); annot
+ with Not_found -> Util.user_err_loc
+ (Util.dummy_loc,"GenFixpoint",
+ Pp.str "No argument named " ++ Nameops.pr_id id)
+ )
+ with Failure "check_exists_args" -> check_one_name ();annot
+ in
+ let ni =
+ match annot with
+ | None ->
+ annot
+ | Some an ->
+ check_exists_args an
+ in
+ (id, ni, bl, type_, def) ]
+ END
+
+
+VERNAC ARGUMENT EXTEND rec_definitions2
+| [ rec_definition2(rd) ] -> [ [rd] ]
+| [ rec_definition2(hd) "with" rec_definitions2(tl) ] -> [ hd::tl ]
+END
+
+
+VERNAC COMMAND EXTEND GenFixpoint
+ ["GenFixpoint" rec_definitions2(recsl)] ->
+ [ do_generate_principle false recsl]
+END
+
+VERNAC COMMAND EXTEND IGenFixpoint
+ ["IGenFixpoint" rec_definitions2(recsl)] ->
+ [ do_generate_principle true recsl]
+END
+
+
+VERNAC ARGUMENT EXTEND fun_scheme_arg
+| [ ident(princ_name) ":=" "Induction" "for" ident(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ]
+END
+
+VERNAC ARGUMENT EXTEND fun_scheme_args
+| [ fun_scheme_arg(fa) ] -> [ [fa] ]
+| [ fun_scheme_arg(fa) "with" fun_scheme_args(fas) ] -> [fa::fas]
+END
+
+VERNAC COMMAND EXTEND NewFunctionalScheme
+ ["New" "Functional" "Scheme" fun_scheme_args(fas) ] ->
+ [
+ New_arg_principle.make_scheme fas
+ ]
+END
+
+
+VERNAC COMMAND EXTEND NewFunctionalCase
+ ["New" "Functional" "Case" fun_scheme_arg(fas) ] ->
+ [
+ New_arg_principle.make_case_scheme fas
+ ]
+END
+
+
+VERNAC COMMAND EXTEND GenerateGraph
+["Generate" "graph" "for" ident(c)] -> [ make_graph c ]
+END
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
new file mode 100644
index 00000000..1f711297
--- /dev/null
+++ b/contrib/funind/invfun.ml
@@ -0,0 +1,148 @@
+open Util
+open Names
+open Term
+open Tacinvutils
+open Pp
+open Libnames
+open Tacticals
+open Tactics
+open Indfun_common
+open Tacmach
+open Sign
+
+
+let tac_pattern l =
+ (Hiddentac.h_reduce
+ (Rawterm.Pattern l)
+ Tacticals.onConcl
+ )
+
+
+let rec nb_prod x =
+ let rec count n c =
+ match kind_of_term c with
+ Prod(_,_,t) -> count (n+1) t
+ | LetIn(_,a,_,t) -> count n (subst1 a t)
+ | Cast(c,_,_) -> count n c
+ | _ -> n
+ in count 0 x
+
+let intro_discr_until n tac : tactic =
+ let rec intro_discr_until acc : tactic =
+ fun g ->
+ if nb_prod (pf_concl g) <= n then tac (List.rev acc) g
+ else
+ tclTHEN
+ intro
+ (fun g' ->
+ let id,_,t = pf_last_hyp g' in
+ tclORELSE
+ (tclABSTRACT None (Extratactics.h_discrHyp (Rawterm.NamedHyp id)))
+ (intro_discr_until ((id,t)::acc))
+ g'
+ )
+ g
+ in
+ intro_discr_until []
+
+
+let rec discr_rew_in_H hypname idl : tactic =
+ match idl with
+ | [] -> (Extratactics.h_discrHyp (Rawterm.NamedHyp hypname))
+ | ((id,t)::idl') ->
+ match kind_of_term t with
+ | App(eq',[| _ ; arg1 ; _ |]) when eq_constr eq' (Lazy.force eq) ->
+ begin
+ let constr,_ = decompose_app arg1 in
+ if isConstruct constr
+ then
+ (discr_rew_in_H hypname idl')
+ else
+ tclTHEN
+ (tclTRY (Equality.general_rewrite_in true hypname (mkVar id)))
+ (discr_rew_in_H hypname idl')
+ end
+ | _ -> discr_rew_in_H hypname idl'
+
+let finalize fname hypname idl : tactic =
+ tclTRY (
+ (tclTHEN
+ (Hiddentac.h_reduce
+ (Rawterm.Unfold [[],EvalConstRef fname])
+ (Tacticals.onHyp hypname)
+ )
+ (discr_rew_in_H hypname idl)
+ ))
+
+let gen_fargs fargs : tactic =
+ fun g ->
+ generalize
+ (List.map
+ (fun arg ->
+ let targ = pf_type_of g arg in
+ let refl_arg = mkApp (Lazy.force refl_equal , [|targ ; arg|]) in
+ refl_arg
+ )
+ (Array.to_list fargs)
+ )
+ g
+
+
+let invfun (hypname:identifier) (fid:identifier) : tactic=
+ fun g ->
+ let nprod_goal = nb_prod (pf_concl g) in
+ let f_ind_id =
+ (
+ Indrec.make_elimination_ident
+ fid
+ (Tacticals.elimination_sort_of_goal g)
+ )
+ in
+ let fname = const_of_id fid in
+ let princ = const_of_id f_ind_id in
+ let princ_info =
+ let princ_type =
+ (try (match (Global.lookup_constant princ) with
+ {Declarations.const_type=t} -> t
+ )
+ with _ -> assert false)
+ in
+ Tactics.compute_elim_sig princ_type
+ in
+ let _,_,typhyp = List.find (fun (id,_,_) -> hypname=id) (pf_hyps g) in
+ let do_invert fargs appf : tactic =
+ let frealargs = (snd (array_chop (List.length princ_info.params) fargs))
+ in
+ let pat_args =
+ (List.map (fun e -> ([-1],e)) (Array.to_list frealargs)) @ [[],appf]
+ in
+ tclTHENSEQ
+ [
+ gen_fargs frealargs;
+ tac_pattern pat_args;
+ Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings);
+ intro_discr_until nprod_goal (finalize fname hypname)
+
+ ]
+ in
+ match kind_of_term typhyp with
+ | App(eq',[| _ ; arg1 ; arg2 |]) when eq_constr eq' (Lazy.force eq) ->
+(* let valf = def_of_const (mkConst fname) in *)
+ let eq_arg1 , eq_arg2 , good_eq_form , fargs =
+ match kind_of_term arg1 , kind_of_term arg2 with
+ | App(f, args),_ when eq_constr f (mkConst fname) ->
+ arg1 , arg2 , tclIDTAC , args
+ | _,App(f, args) when eq_constr f (mkConst fname) ->
+ arg2 , arg1 , symmetry_in hypname , args
+ | _ , _ -> error "inversion impossible"
+ in
+ tclTHEN
+ good_eq_form
+ (do_invert fargs eq_arg1)
+ g
+ | App(f',fargs) when eq_constr f' (mkConst fname) ->
+ do_invert fargs typhyp g
+
+
+ | _ -> error "inversion impossible"
+
diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml
new file mode 100644
index 00000000..8ef23c48
--- /dev/null
+++ b/contrib/funind/new_arg_principle.ml
@@ -0,0 +1,1770 @@
+open Printer
+open Util
+open Term
+open Termops
+open Names
+open Declarations
+open Pp
+open Entries
+open Hiddentac
+open Evd
+open Tacmach
+open Proof_type
+open Tacticals
+open Tactics
+open Indfun_common
+
+
+let msgnl = Pp.msgnl
+
+let do_observe () =
+ Tacinterp.get_debug () <> Tactic_debug.DebugOff
+
+
+let observe strm =
+ if do_observe ()
+ then Pp.msgnl strm
+ else ()
+
+let observennl strm =
+ if do_observe ()
+ then begin Pp.msg strm;Pp.pp_flush () end
+ else ()
+
+
+
+
+let do_observe_tac s tac g =
+ try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
+ with e ->
+ let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
+ msgnl (str "observation "++str s++str " raised exception " ++
+ Cerrors.explain_exn e ++ str "on goal " ++ goal );
+ raise e;;
+
+
+let observe_tac s tac g =
+ if do_observe ()
+ then do_observe_tac s tac g
+ else tac g
+
+
+let tclTRYD tac =
+ if !Options.debug || do_observe ()
+ then (fun g -> try do_observe_tac "" tac g with _ -> tclIDTAC g)
+ else tac
+
+
+let list_chop ?(msg="") n l =
+ try
+ list_chop n l
+ with Failure (msg') ->
+ failwith (msg ^ msg')
+
+
+let make_refl_eq type_of_t t =
+ let refl_equal_term = Lazy.force refl_equal in
+ mkApp(refl_equal_term,[|type_of_t;t|])
+
+
+type static_fix_info =
+ {
+ idx : int;
+ name : identifier;
+ types : types
+ }
+
+type static_infos =
+ {
+ fixes_ids : identifier list;
+ ptes_to_fixes : static_fix_info Idmap.t
+ }
+
+type 'a dynamic_info =
+ {
+ nb_rec_hyps : int;
+ rec_hyps : identifier list ;
+ eq_hyps : identifier list;
+ info : 'a
+ }
+
+let finish_proof dynamic_infos g =
+ observe_tac "finish"
+ h_assumption
+ g
+
+
+let refine c =
+ Tacmach.refine_no_check c
+
+let thin l =
+ Tacmach.thin_no_check l
+
+
+let cut_replacing id t tac :tactic=
+ tclTHENS (cut t)
+ [ tclTHEN (thin_no_check [id]) (introduction_no_check id);
+ tac
+ ]
+
+let intro_erasing id = tclTHEN (thin [id]) (introduction id)
+
+
+
+let rec_hyp_id = id_of_string "rec_hyp"
+
+let is_trivial_eq t =
+ match kind_of_term t with
+ | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
+ eq_constr t1 t2
+ | _ -> false
+
+
+let rec incompatible_constructor_terms t1 t2 =
+ let c1,arg1 = decompose_app t1
+ and c2,arg2 = decompose_app t2
+ in
+ (not (eq_constr t1 t2)) &&
+ isConstruct c1 && isConstruct c2 &&
+ (
+ not (eq_constr c1 c2) ||
+ List.exists2 incompatible_constructor_terms arg1 arg2
+ )
+
+let is_incompatible_eq t =
+ match kind_of_term t with
+ | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
+ incompatible_constructor_terms t1 t2
+ | _ -> false
+
+let change_hyp_with_using hyp_id t tac =
+ fun g ->
+ let prov_id = pf_get_new_id hyp_id g in
+ tclTHENLIST
+ [
+ forward (Some tac) (Genarg.IntroIdentifier prov_id) t;
+ thin [hyp_id];
+ h_rename prov_id hyp_id
+ ] g
+
+exception TOREMOVE
+
+
+let prove_trivial_eq h_id context (type_of_term,term) =
+ let nb_intros = List.length context in
+ tclTHENLIST
+ [
+ tclDO nb_intros intro; (* introducing context *)
+ (fun g ->
+ let context_hyps =
+ fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g))
+ in
+ let context_hyps' =
+ (mkApp(Lazy.force refl_equal,[|type_of_term;term|]))::
+ (List.map mkVar context_hyps)
+ in
+ let to_refine = applist(mkVar h_id,List.rev context_hyps') in
+ refine to_refine g
+ )
+ ]
+
+
+let isAppConstruct t =
+ if isApp t
+ then isConstruct (fst (destApp t))
+ else false
+
+
+let nf_betaoiotazeta = Reductionops.local_strong Reductionops.whd_betaiotazeta
+
+let remove_useless_rel env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2 =
+ let rel_num = destRel t2 in
+
+ let nb_kept = List.length context - rel_num
+ and nb_popped = rel_num - 1
+ in
+
+ (* We remove the equation *)
+ let new_end_of_type = pop end_of_type in
+
+ let lt_relnum,ge_relnum =
+ list_chop
+ ~msg:("removing useless variable "^(string_of_int rel_num)^" :")
+ nb_popped
+ context
+ in
+ (* we rebuilt the type of hypothesis after the rel to remove *)
+ let hyp_type_lt_relnum =
+ it_mkProd_or_LetIn ~init:new_end_of_type lt_relnum
+ in
+ (* we replace Rel 1 by t1 *)
+ let new_hyp_type_lt_relnum = subst1 t1 hyp_type_lt_relnum in
+ (* we resplit the type of hyp_type *)
+ let new_lt_relnum,new_end_of_type =
+ Sign.decompose_prod_n_assum nb_popped new_hyp_type_lt_relnum
+ in
+ (* and rebuilt new context of hyp *)
+ let new_context = new_lt_relnum@(List.tl ge_relnum) in
+ let new_typ_of_hyp =
+ nf_betaoiotazeta (it_mkProd_or_LetIn ~init:new_end_of_type new_context)
+ in
+ let prove_simpl_eq =
+ tclTHENLIST
+ [
+ tclDO (nb_popped + nb_kept) intro;
+ (fun g' ->
+ let new_hyps_ids = pf_ids_of_hyps g' in
+ let popped_ids,others =
+ list_chop ~msg:"removing useless variable pop :"
+ nb_popped new_hyps_ids in
+ let kept_ids,_ =
+ list_chop ~msg: " removing useless variable kept : "
+ nb_kept others
+ in
+ let rev_to_apply =
+ (mkApp(Lazy.force refl_equal,[|Typing.type_of env sigma t1;t1|]))::
+ ((List.map mkVar popped_ids)@
+ (t1::
+ (List.map mkVar kept_ids)))
+ in
+ let to_refine = applist(mkVar hyp_id,List.rev rev_to_apply) in
+ refine to_refine g'
+ )
+ ]
+ in
+ let simpl_eq_tac = change_hyp_with_using hyp_id new_typ_of_hyp
+ (observe_tac "prove_simpl_eq" prove_simpl_eq)
+ in
+ let new_end_of_type = nf_betaoiotazeta new_end_of_type in
+ (new_context,new_end_of_type,simpl_eq_tac),new_typ_of_hyp,
+ (str " removing useless variable " ++ str (string_of_int rel_num) )
+
+
+let decompose_eq env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2 =
+ let c1,args1 = destApp t1
+ and c2,args2 = destApp t2
+ in
+ (* This tactic must be used after is_incompatible_eq *)
+ assert (eq_constr c1 c2);
+ (* we remove this equation *)
+ let new_end_of_type = pop end_of_type in
+ let new_eqs =
+ array_map2_i
+ (fun i arg1 arg2 ->
+ let new_eq =
+ let type_of_arg = Typing.type_of env sigma arg1 in
+ mkApp(Lazy.force eq,[|type_of_arg;arg1;arg2|])
+ in
+ Anonymous,None,lift i new_eq
+ )
+ args1
+ args2
+ in
+ let nb_new_eqs = Array.length new_eqs in
+ (* we add the new equation *)
+ let new_end_of_type = lift nb_new_eqs new_end_of_type in
+ let local_context =
+ List.rev (Array.to_list new_eqs) in
+ let new_end_of_type = it_mkProd_or_LetIn ~init:new_end_of_type local_context in
+ let new_typ_of_hyp =
+ nf_betaoiotazeta (it_mkProd_or_LetIn ~init:new_end_of_type context)
+ in
+ let prove_pattern_simplification =
+ let context_length = List.length context in
+ tclTHENLIST
+ [
+ tclDO (context_length + nb_new_eqs) intro ;
+ (fun g ->
+ let new_eqs,others =
+ list_chop ~msg:"simplifying pattern : new_eqs" nb_new_eqs (pf_hyps g)
+ in
+ let context_hyps,_ = list_chop ~msg:"simplifying pattern : context_hyps"
+ context_length others in
+ let eq_args =
+ List.rev_map
+ (fun (_,_, eq) -> let _,args = destApp eq in args.(1),args.(2))
+ new_eqs
+ in
+ let lhs_args,rhs_args = List.split eq_args in
+ let lhs_eq = applist(c1,lhs_args)
+ and rhs_eq = applist(c1,rhs_args)
+ in
+ let type_of_eq = pf_type_of g lhs_eq in
+ let eq_to_assert =
+ mkApp(Lazy.force eq,[|type_of_eq;lhs_eq;rhs_eq|])
+ in
+ let prove_new_eq =
+ tclTHENLIST [
+ tclMAP
+ (fun (id,_,_) ->
+ (* The tclTRY here is used when trying to rewrite
+ on Set
+ eg (@cons A x l)=(@cons A x' l') generates 3 eqs
+ A=A -> x=x' -> l = l' ...
+
+ *)
+ tclTRY (Equality.rewriteLR (mkVar id))
+ )
+ new_eqs;
+ reflexivity
+ ]
+ in
+ let new_eq_id = pf_get_new_id (id_of_string "H") g in
+ let create_new_eq =
+ forward
+ (Some (observe_tac "prove_new_eq" (prove_new_eq)))
+ (Genarg.IntroIdentifier new_eq_id)
+ eq_to_assert
+ in
+ let to_refine =
+ applist (
+ mkVar hyp_id,
+ List.rev ((mkVar new_eq_id)::
+ (List.map (fun (id,_,_) -> mkVar id) context_hyps)))
+ in
+ tclTHEN
+ (observe_tac "create_new_eq" create_new_eq )
+ (observe_tac "refine in decompose_eq " (refine to_refine))
+ g
+ )
+ ]
+ in
+ let simpl_eq_tac =
+ change_hyp_with_using hyp_id new_typ_of_hyp (observe_tac "prove_pattern_simplification " prove_pattern_simplification)
+ in
+ (context,nf_betaoiotazeta new_end_of_type,simpl_eq_tac),new_typ_of_hyp,
+ str "simplifying an equation "
+
+let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type =
+ if not (noccurn 1 end_of_type)
+ then (* if end_of_type depends on this term we don't touch it *)
+ begin
+ observe (str "Not treating " ++ pr_lconstr t );
+ failwith "NoChange";
+ end;
+ let res,new_typ_of_hyp,msg =
+ if not (isApp t) then failwith "NoChange";
+ let f,args = destApp t in
+ if not (eq_constr f (Lazy.force eq)) then failwith "NoChange";
+ let t1 = args.(1)
+ and t2 = args.(2)
+ in
+ if isRel t2 && closed0 t1 then (* closed_term = x with x bound in context *)
+ begin
+ remove_useless_rel env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2
+ end
+ else if isAppConstruct t1 && isAppConstruct t2 (* C .... = C .... *)
+ then decompose_eq env sigma hyp_id context t end_of_type t1 t2
+ else failwith "NoChange"
+ in
+ observe (str "In " ++ Ppconstr.pr_id hyp_id ++
+ msg ++ fnl ()++
+ str "old_typ_of_hyp :=" ++
+ Printer.pr_lconstr_env
+ env
+ (it_mkProd_or_LetIn ~init:end_of_type ((x,None,t)::context))
+ ++ fnl () ++
+ str "new_typ_of_hyp := "++
+ Printer.pr_lconstr_env env new_typ_of_hyp ++ fnl ());
+ (res:'a*'b*'c)
+
+
+
+
+let is_property static_info t_x =
+ if isApp t_x
+ then
+ let pte,args = destApp t_x in
+ if isVar pte && array_for_all closed0 args
+ then Idmap.mem (destVar pte) static_info.ptes_to_fixes
+ else false
+ else false
+
+let isLetIn t =
+ match kind_of_term t with
+ | LetIn _ -> true
+ | _ -> false
+
+
+let h_reduce_with_zeta =
+ h_reduce
+ (Rawterm.Cbv
+ {Rawterm.all_flags
+ with Rawterm.rDelta = false;
+ })
+
+(*
+let rewrite_until_var arg_num : tactic =
+ let constr_eq = Lazy.force eq in
+ let replace_if_unify arg (pat,cl,id,lhs) : tactic =
+ fun g ->
+ try
+ let (evd,matched) =
+ Unification.w_unify_to_subterm
+ (pf_env g) ~mod_delta:false (pat,arg) cl.Clenv.env
+ in
+ let cl' = {cl with Clenv.env = evd } in
+ let c2 = Clenv.clenv_nf_meta cl' lhs in
+ (Equality.replace matched c2) g
+ with _ -> tclFAIL 0 (str "") g
+ in
+ let rewrite_on_step equalities : tactic =
+ fun g ->
+ match kind_of_term (pf_concl g) with
+ | App(_,args) when (not (test_var args arg_num)) ->
+(* tclFIRST (List.map (fun a -> observe_tac (str "replace_if_unify") (replace_if_unify args.(arg_num) a)) equalities) g *)
+ tclFIRST (List.map (replace_if_unify args.(arg_num)) equalities) g
+ | _ ->
+ raise (Util.UserError("", (str "No more rewrite" ++
+ pr_lconstr_env (pf_env g) (pf_concl g))))
+ in
+ fun g ->
+ let equalities =
+ List.filter
+ (
+ fun (_,_,id_t) ->
+ match kind_of_term id_t with
+ | App(f,_) -> eq_constr f constr_eq
+ | _ -> false
+ )
+ (pf_hyps g)
+ in
+ let f (id,_,ctype) =
+ let c = mkVar id in
+ let eqclause = Clenv.make_clenv_binding g (c,ctype) Rawterm.NoBindings in
+ let clause_type = Clenv.clenv_type eqclause in
+ let f,args = decompose_app (clause_type) in
+ let rec split_last_two = function
+ | [c1;c2] -> (c1, c2)
+ | x::y::z ->
+ split_last_two (y::z)
+ | _ ->
+ error ("The term provided is not an equivalence")
+ in
+ let (c1,c2) = split_last_two args in
+ (c2,eqclause,id,c1)
+ in
+ let matching_hyps = List.map f equalities in
+ tclTRY (tclREPEAT (tclPROGRESS (rewrite_on_step matching_hyps))) g
+
+*)
+
+
+let rewrite_until_var arg_num eq_ids : tactic =
+ let test_var g =
+ let _,args = destApp (pf_concl g) in
+ isVar args.(arg_num)
+ in
+ let rec do_rewrite eq_ids g =
+ if test_var g
+ then tclIDTAC g
+ else
+ match eq_ids with
+ | [] -> anomaly "Cannot find a way to prove recursive property";
+ | eq_id::eq_ids ->
+ tclTHEN
+ (tclTRY (Equality.rewriteRL (mkVar eq_id)))
+ (do_rewrite eq_ids)
+ g
+ in
+ do_rewrite eq_ids
+
+let prove_rec_hyp eq_hyps fix_info =
+ tclTHEN
+ (rewrite_until_var (fix_info.idx - 1) eq_hyps)
+ (fun g ->
+ let _,pte_args = destApp (pf_concl g) in
+ let rec_hyp_proof =
+ mkApp(mkVar fix_info.name,array_get_start pte_args)
+ in
+ refine rec_hyp_proof g
+ )
+
+
+
+
+
+let rec_pte_id = id_of_string "Hrec"
+let clean_hyp_with_heq static_infos eq_hyps hyp_id env sigma =
+ let coq_False = Coqlib.build_coq_False () in
+ let coq_True = Coqlib.build_coq_True () in
+ let coq_I = Coqlib.build_coq_I () in
+ let rec scan_type context type_of_hyp : tactic =
+ if isLetIn type_of_hyp then
+ let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in
+ let reduced_type_of_hyp = nf_betaoiotazeta real_type_of_hyp in
+ (* length of context didn't change ? *)
+ let new_context,new_typ_of_hyp =
+ Sign.decompose_prod_n_assum (List.length context) reduced_type_of_hyp
+ in
+ tclTHENLIST
+ [
+ h_reduce_with_zeta
+ (Tacticals.onHyp hyp_id)
+ ;
+ scan_type new_context new_typ_of_hyp
+
+ ]
+ else if isProd type_of_hyp
+ then
+ begin
+ let (x,t_x,t') = destProd type_of_hyp in
+ if is_property static_infos t_x then
+ begin
+ let pte,pte_args = (destApp t_x) in
+ let fix_info = Idmap.find (destVar pte) static_infos.ptes_to_fixes in
+ let popped_t' = pop t' in
+ let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in
+ let prove_new_type_of_hyp =
+ let context_length = List.length context in
+ tclTHENLIST
+ [
+ tclDO context_length intro;
+ (fun g ->
+ let context_hyps_ids =
+ fst (list_chop ~msg:"rec hyp : context_hyps"
+ context_length (pf_ids_of_hyps g))
+ in
+ let rec_pte_id = pf_get_new_id rec_pte_id g in
+ let to_refine =
+ applist(mkVar hyp_id,
+ List.rev_map mkVar (rec_pte_id::context_hyps_ids)
+ )
+ in
+ tclTHENLIST
+ [
+ forward
+ (Some (prove_rec_hyp eq_hyps fix_info))
+ (Genarg.IntroIdentifier rec_pte_id)
+ t_x;
+ refine to_refine
+ ]
+ g
+ )
+ ]
+ in
+ tclTHENLIST
+ [
+ observe_tac "hyp rec"
+ (change_hyp_with_using hyp_id real_type_of_hyp prove_new_type_of_hyp);
+ scan_type context popped_t'
+ ]
+ end
+ else if eq_constr t_x coq_False then
+ begin
+ observe (str "Removing : "++ Ppconstr.pr_id hyp_id++
+ str " since it has False in its preconds "
+ );
+ raise TOREMOVE; (* False -> .. useless *)
+ end
+ else if is_incompatible_eq t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *)
+ else if eq_constr t_x coq_True (* Trivial => we remove this precons *)
+ then
+ let _ =
+ observe (str "In "++Ppconstr.pr_id hyp_id++
+ str " removing useless precond True"
+ )
+ in
+ let popped_t' = pop t' in
+ let real_type_of_hyp =
+ it_mkProd_or_LetIn ~init:popped_t' context
+ in
+ let prove_trivial =
+ let nb_intro = List.length context in
+ tclTHENLIST [
+ tclDO nb_intro intro;
+ (fun g ->
+ let context_hyps =
+ fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g))
+ in
+ let to_refine =
+ applist (mkVar hyp_id,
+ List.rev (coq_I::List.map mkVar context_hyps)
+ )
+ in
+ refine to_refine g
+ )
+ ]
+ in
+ tclTHENLIST[
+ change_hyp_with_using hyp_id real_type_of_hyp (observe_tac "prove_trivial" prove_trivial);
+ scan_type context popped_t'
+ ]
+ else if is_trivial_eq t_x
+ then (* t_x := t = t => we remove this precond *)
+ let popped_t' = pop t' in
+ let real_type_of_hyp =
+ it_mkProd_or_LetIn ~init:popped_t' context
+ in
+ let _,args = destApp t_x in
+ tclTHENLIST
+ [
+ change_hyp_with_using
+ hyp_id
+ real_type_of_hyp
+ (observe_tac "prove_trivial_eq" (prove_trivial_eq hyp_id context (args.(0),args.(1))));
+ scan_type context popped_t'
+ ]
+ else
+ begin
+ try
+ let new_context,new_t',tac = change_eq env sigma hyp_id context x t_x t' in
+ tclTHEN
+ tac
+ (scan_type new_context new_t')
+ with Failure "NoChange" ->
+ (* Last thing todo : push the rel in the context and continue *)
+ scan_type ((x,None,t_x)::context) t'
+ end
+ end
+ else
+ tclIDTAC
+ in
+ try
+ scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id]
+ with TOREMOVE ->
+ thin [hyp_id],[]
+
+
+let clean_goal_with_heq static_infos continue_tac dyn_infos =
+ fun g ->
+ let env = pf_env g
+ and sigma = project g
+ in
+ let tac,new_hyps =
+ List.fold_left (
+ fun (hyps_tac,new_hyps) hyp_id ->
+ let hyp_tac,new_hyp =
+ clean_hyp_with_heq static_infos dyn_infos.eq_hyps hyp_id env sigma
+ in
+ (tclTHEN hyp_tac hyps_tac),new_hyp@new_hyps
+ )
+ (tclIDTAC,[])
+ dyn_infos.rec_hyps
+ in
+ let new_infos =
+ { dyn_infos with
+ rec_hyps = new_hyps;
+ nb_rec_hyps = List.length new_hyps
+ }
+ in
+ tclTHENLIST
+ [
+ tac ;
+ (continue_tac new_infos)
+ ]
+ g
+
+let heq_id = id_of_string "Heq"
+
+let treat_new_case static_infos nb_prod continue_tac term dyn_infos =
+ fun g ->
+ let heq_id = pf_get_new_id heq_id g in
+ let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
+ tclTHENLIST
+ [
+ (* We first introduce the variables *)
+ tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps);
+ (* Then the equation itself *)
+ introduction_no_check heq_id;
+ (* Then the new hypothesis *)
+ tclMAP introduction_no_check dyn_infos.rec_hyps;
+ observe_tac "after_introduction" (fun g' ->
+ (* We get infos on the equations introduced*)
+ let new_term_value_eq = pf_type_of g' (mkVar heq_id) in
+ (* compute the new value of the body *)
+ let new_term_value =
+ match kind_of_term new_term_value_eq with
+ | App(f,[| _;_;args2 |]) -> args2
+ | _ ->
+ observe (pr_gls g' ++ fnl () ++ str "last hyp is" ++
+ pr_lconstr_env (pf_env g') new_term_value_eq
+ );
+ assert false
+ in
+ let fun_body =
+ mkLambda(Anonymous,
+ pf_type_of g' term,
+ replace_term term (mkRel 1) dyn_infos.info
+ )
+ in
+ let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
+ let new_infos =
+ {dyn_infos with
+ info = new_body;
+ eq_hyps = heq_id::dyn_infos.eq_hyps
+ }
+ in
+ clean_goal_with_heq static_infos continue_tac new_infos g'
+ )
+ ]
+ g
+
+let do_prove_princ_for_struct
+ (interactive_proof:bool)
+ (fnames:constant list)
+ static_infos
+(* (ptes:identifier list) *)
+(* (fixes:(int*constr*identifier*constr) Idmap.t) *)
+(* (hyps: identifier list) *)
+(* (term:constr) *)
+ dyn_infos
+ : tactic =
+(* let fixes_ids = Idmap.fold (fun _ (_,_,id,_) acc -> id::acc) fixes [] in *)
+ let rec do_prove_princ_for_struct_aux do_finalize dyn_infos : tactic =
+ fun g ->
+(* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
+ match kind_of_term dyn_infos.info with
+ | Case(_,_,t,_) ->
+ let g_nb_prod = nb_prod (pf_concl g) in
+ let type_of_term = pf_type_of g t in
+ let term_eq =
+ make_refl_eq type_of_term t
+ in
+ tclTHENSEQ
+ [
+ h_generalize (term_eq::List.map mkVar dyn_infos.rec_hyps);
+ thin dyn_infos.rec_hyps;
+ pattern_option [[-1],t] None;
+ h_simplest_case t;
+ (fun g' ->
+ let g'_nb_prod = nb_prod (pf_concl g') in
+ let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
+ observe_tac "treat_new_case"
+ (treat_new_case
+ static_infos
+ nb_instanciate_partial
+ (do_prove_princ_for_struct do_finalize)
+ t
+ dyn_infos)
+ g'
+ )
+
+ ] g
+ | Lambda(n,t,b) ->
+ begin
+ match kind_of_term( pf_concl g) with
+ | Prod _ ->
+ tclTHEN
+ intro
+ (fun g' ->
+ let (id,_,_) = pf_last_hyp g' in
+ let new_term =
+ pf_nf_betaiota g'
+ (mkApp(dyn_infos.info,[|mkVar id|]))
+ in
+ let new_infos = {dyn_infos with info = new_term} in
+ do_prove_princ_for_struct do_finalize new_infos g'
+ ) g
+ | _ ->
+ do_finalize dyn_infos g
+ end
+ | Cast(t,_,_) ->
+ do_prove_princ_for_struct do_finalize {dyn_infos with info = t} g
+ | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
+ do_finalize dyn_infos g
+ | App(_,_) ->
+ let f,args = decompose_app dyn_infos.info in
+ begin
+ match kind_of_term f with
+ | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ ->
+ let new_infos =
+ { dyn_infos with
+ info = (f,args)
+ }
+ in
+ do_prove_princ_for_struct_args do_finalize new_infos g
+ | Const c when not (List.mem c fnames) ->
+ let new_infos =
+ { dyn_infos with
+ info = (f,args)
+ }
+ in
+ do_prove_princ_for_struct_args do_finalize new_infos g
+ | Const _ ->
+ do_finalize dyn_infos g
+ | _ ->
+(* observe *)
+(* (str "Applied binders not yet implemented: in "++ fnl () ++ *)
+(* pr_lconstr_env (pf_env g) term ++ fnl () ++ *)
+(* pr_lconstr_env (pf_env g) f ++ spc () ++ str "is applied") ; *)
+ tclFAIL 0 (str "TODO : Applied binders not yet implemented") g
+ end
+ | Fix _ | CoFix _ ->
+ error ( "Anonymous local (co)fixpoints are not handled yet")
+
+ | Prod _ -> assert false
+ | LetIn _ ->
+ let new_infos =
+ { dyn_infos with
+ info = nf_betaoiotazeta dyn_infos.info
+ }
+ in
+
+ tclTHENLIST
+ [tclMAP
+ (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id))
+ dyn_infos.rec_hyps;
+ h_reduce_with_zeta Tacticals.onConcl;
+ do_prove_princ_for_struct do_finalize new_infos
+ ] g
+ | _ ->
+ errorlabstrm "" (str "in do_prove_princ_for_struct found : "(* ++ *)
+(* pr_lconstr_env (pf_env g) term *)
+ )
+ and do_prove_princ_for_struct do_finalize dyn_infos g =
+(* observe (str "proving with "++Printer.pr_lconstr term++ str " on goal " ++ pr_gls g); *)
+ do_prove_princ_for_struct_aux do_finalize dyn_infos g
+ and do_prove_princ_for_struct_args do_finalize dyn_infos (* f_args' args *) :tactic =
+ fun g ->
+(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *)
+(* then msgnl (str "do_prove_princ_for_struct_args with " ++ *)
+(* pr_lconstr_env (pf_env g) f_args' *)
+(* ); *)
+ let (f_args',args) = dyn_infos.info in
+ let tac =
+ match args with
+ | [] ->
+ do_finalize {dyn_infos with info = f_args'}
+ | arg::args ->
+ let do_finalize dyn_infos =
+ let new_arg = dyn_infos.info in
+ tclTRYD
+ (do_prove_princ_for_struct_args
+ do_finalize
+ {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args}
+ )
+ in
+ do_prove_princ_for_struct do_finalize
+ {dyn_infos with info = arg }
+ in
+ tclTRYD(tac ) g
+ in
+ let do_finish_proof dyn_infos =
+ clean_goal_with_heq
+ static_infos
+ finish_proof dyn_infos
+ in
+ observe_tac "do_prove_princ_for_struct"
+ (do_prove_princ_for_struct do_finish_proof dyn_infos)
+
+let is_pte_type t =
+ isSort (snd (decompose_prod t))
+
+let is_pte (_,_,t) = is_pte_type t
+
+exception Not_Rec
+
+
+
+let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id =
+ let args = Array.of_list (List.map mkVar args_id) in
+ let instanciate_one_hyp hid =
+ tclORELSE
+ ( (* we instanciate the hyp if possible *)
+(* tclTHENLIST *)
+(* [h_generalize [mkApp(mkVar hid,args)]; *)
+(* intro_erasing hid] *)
+ fun g ->
+ let prov_hid = pf_get_new_id hid g in
+ tclTHENLIST[
+ forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
+ thin [hid];
+ h_rename prov_hid hid
+ ] g
+ )
+ ( (*
+ if not then we are in a mutual function block
+ and this hyp is a recursive hyp on an other function.
+
+ We are not supposed to use it while proving this
+ principle so that we can trash it
+
+ *)
+ (fun g ->
+ observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid);
+ thin [hid] g
+ )
+ )
+ in
+ (* if no args then no instanciation ! *)
+ if args_id = []
+ then
+ tclTHENLIST [
+ tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
+ do_prove hyps
+ ]
+ else
+ tclTHENLIST
+ [
+ tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
+ tclMAP instanciate_one_hyp hyps;
+ (fun g ->
+ let all_g_hyps_id =
+ List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty
+ in
+ let remaining_hyps =
+ List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps
+ in
+ do_prove remaining_hyps g
+ )
+ ]
+
+
+let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : tactic =
+ fun goal ->
+(* observe (str "Proving principle for "++ str (string_of_int fun_num) ++ str "th function : " ++ *)
+(* pr_lconstr (mkConst fnames.(fun_num))); *)
+ let princ_type = pf_concl goal in
+ let princ_info = compute_elim_sig princ_type in
+ let get_body const =
+ match (Global.lookup_constant const ).const_body with
+ | Some b ->
+ let body = force b in
+ Tacred.cbv_norm_flags
+ (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ (Global.env ())
+ (Evd.empty)
+ body
+ | None -> error ( "Cannot define a principle over an axiom ")
+ in
+ let fbody = get_body fnames.(fun_num) in
+ let params : identifier list ref = ref [] in
+ let predicates : identifier list ref = ref [] in
+ let args : identifier list ref = ref [] in
+ let branches : identifier list ref = ref [] in
+ let pte_to_fix = ref Idmap.empty in
+ let fbody_with_params = ref None in
+ let intro_with_remembrance ref number : tactic =
+ tclTHEN
+ ( tclDO number intro )
+ (fun g ->
+ let last_n = list_chop number (pf_hyps g) in
+ ref := List.map (fun (id,_,_) -> id) (fst last_n)@ !ref;
+ tclIDTAC g
+ )
+ in
+ let rec partial_combine body params =
+ match kind_of_term body,params with
+ | Lambda (x,t,b),param::params ->
+ partial_combine (subst1 param b) params
+ | Fix(infos),_ ->
+ body,params, Some (infos)
+ | _ -> body,params,None
+ in
+ let build_pte_to_fix (offset:int) params predicates
+ ((idxs,fix_num),(na,typearray,ca)) (avoid,_) =
+(* let true_params,_ = list_chop offset params in *)
+ let true_params = List.rev params in
+ let avoid = ref avoid in
+ let res = list_fold_left_i
+ (fun i acc pte_id ->
+ let this_fix_id = fresh_id !avoid "fix___" in
+ avoid := this_fix_id::!avoid;
+(* let this_body = substl (List.rev fnames_as_constr) ca.(i) in *)
+ let new_type = prod_applist typearray.(i) true_params in
+ let new_type_args,_ = decompose_prod new_type in
+ let nargs = List.length new_type_args in
+ let pte_args =
+ (* let rev_args = List.rev_map (fun (id,_,_) -> mkVar id) new_type_args in *)
+ let f = applist((* all_funs *)mkConst fnames.(i),true_params) in
+ let app_f = mkApp(f,Array.init nargs (fun i -> mkRel(nargs - i))) in
+ (Array.to_list (Array.init nargs (fun i -> mkRel(nargs - i))))@[app_f]
+ in
+ let app_pte = applist(mkVar pte_id,pte_args) in
+ let new_type = compose_prod new_type_args app_pte in
+ let fix_info =
+ {
+ idx = idxs.(i) - offset + 1;
+ name = this_fix_id;
+ types = new_type
+ }
+ in
+ pte_to_fix := Idmap.add pte_id fix_info !pte_to_fix;
+ fix_info::acc
+ )
+ 0
+ []
+ predicates
+ in
+ !avoid,List.rev res
+ in
+ let mk_fixes : tactic =
+ fun g ->
+ let body_p,params',fix_infos =
+ partial_combine fbody (List.rev_map mkVar !params)
+ in
+ fbody_with_params := Some body_p;
+ let offset = List.length params' in
+ let not_real_param,true_params =
+ list_chop
+ ((List.length !params ) - offset)
+ !params
+ in
+ params := true_params; args := not_real_param;
+(* observe (str "mk_fixes : params are "++ *)
+(* prlist_with_sep spc *)
+(* (fun id -> pr_lconstr (mkVar id)) *)
+(* !params *)
+(* ); *)
+ let new_avoid,infos =
+ option_fold_right
+ (build_pte_to_fix
+ offset
+ (List.map mkVar !params)
+ (List.rev !predicates)
+ )
+ fix_infos
+ ((pf_ids_of_hyps g),[])
+ in
+ let pre_info,infos = list_chop fun_num infos in
+ match pre_info,infos with
+ | [],[] -> tclIDTAC g
+ | _,this_fix_info::infos' ->
+ let other_fix_info =
+ List.map
+ (fun fix_info -> fix_info.name,fix_info.idx,fix_info.types)
+ (pre_info@infos')
+ in
+ tclORELSE
+ (h_mutual_fix this_fix_info.name this_fix_info.idx other_fix_info)
+ (tclFAIL 1000 (str "bad index" ++
+ str (string_of_int this_fix_info.idx) ++
+ str "offset := " ++
+ (str (string_of_int offset))))
+ g
+ | _,[] -> anomaly "Not a valid information"
+ in
+ let do_prove ptes_to_fixes args branches : tactic =
+ fun g ->
+ let static_infos =
+ {
+ ptes_to_fixes = ptes_to_fixes;
+ fixes_ids =
+ Idmap.fold
+ (fun _ fix_info acc -> fix_info.name::acc)
+ ptes_to_fixes []
+ }
+ in
+ match kind_of_term (pf_concl g) with
+ | App(pte,pte_args) when isVar pte ->
+ begin
+ let pte = destVar pte in
+ try
+ if not (Idmap.mem pte ptes_to_fixes) then raise Not_Rec;
+ let nparams = List.length !params in
+ let args_as_constr = List.map mkVar args in
+ let rec_num,new_body =
+ let idx' = list_index pte (List.rev !predicates) - 1 in
+ let f = fnames.(idx') in
+ let body_with_params = match !fbody_with_params with Some f -> f | _ -> anomaly ""
+ in
+ let name_of_f = Name ( id_of_label (con_label f)) in
+ let ((rec_nums,_),(na,_,bodies)) = destFix body_with_params in
+ let idx'' = list_index name_of_f (Array.to_list na) - 1 in
+ let body = substl (List.rev (Array.to_list all_funs)) bodies.(idx'') in
+ let body = Reductionops.nf_beta (applist(body,(List.rev_map mkVar !params))) in
+ rec_nums.(idx'') - nparams ,body
+ in
+ let applied_body =
+ Reductionops.nf_beta
+ (applist(new_body,List.rev args_as_constr))
+ in
+ let do_prove branches applied_body =
+ do_prove_princ_for_struct
+ interactive_proof
+ (Array.to_list fnames)
+ static_infos
+ branches
+ applied_body
+ in
+ let replace_and_prove =
+ tclTHENS
+ (fun g ->
+(* observe (str "replacing " ++ *)
+(* pr_lconstr_env (pf_env g) (array_last pte_args) ++ *)
+(* str " with " ++ *)
+(* pr_lconstr_env (pf_env g) applied_body ++ *)
+(* str " rec_arg_num is " ++ str (string_of_int rec_num) *)
+(* ); *)
+ (Equality.replace (array_last pte_args) applied_body) g
+ )
+ [
+ clean_goal_with_heq
+ static_infos do_prove
+ {
+ nb_rec_hyps = List.length branches;
+ rec_hyps = branches;
+ info = applied_body;
+ eq_hyps = [];
+ } ;
+ try
+ let id = List.nth (List.rev args_as_constr) (rec_num) in
+ (* observe (str "choosen var := "++ pr_lconstr id); *)
+ (tclTHENSEQ
+ [(h_simplest_case id);
+ Tactics.intros_reflexivity
+ ])
+ with _ -> tclIDTAC
+
+ ]
+ in
+ (observe_tac "doing replacement" ( replace_and_prove)) g
+ with Not_Rec ->
+ let fname = destConst (fst (decompose_app (array_last pte_args))) in
+ tclTHEN
+ (unfold_in_concl [([],Names.EvalConstRef fname)])
+ (observe_tac ""
+ (fun g' ->
+ let body = array_last (snd (destApp (pf_concl g'))) in
+ let dyn_infos =
+ { nb_rec_hyps = List.length branches;
+ rec_hyps = branches;
+ info = body;
+ eq_hyps = []
+ }
+ in
+ let do_prove =
+ do_prove_princ_for_struct
+ interactive_proof
+ (Array.to_list fnames)
+ static_infos
+ in
+ clean_goal_with_heq static_infos
+ do_prove dyn_infos g'
+ )
+ )
+ g
+ end
+ | _ -> assert false
+ in
+ tclTHENSEQ
+ [
+ (fun g -> observe_tac "introducing params" (intro_with_remembrance params princ_info.nparams) g);
+ (fun g -> observe_tac "introducing predicate" (intro_with_remembrance predicates princ_info.npredicates) g);
+ (fun g -> observe_tac "introducing branches" (intro_with_remembrance branches princ_info.nbranches) g);
+ (fun g -> observe_tac "declaring fix(es)" mk_fixes g);
+ (fun g ->
+ let nb_prod_g = nb_prod (pf_concl g) in
+ tclTHENLIST [
+ tclDO nb_prod_g intro;
+ (fun g' ->
+ let args =
+ fst (list_chop ~msg:"args" nb_prod_g (pf_ids_of_hyps g'))
+ in
+ let do_prove_on_branches branches : tactic =
+ observe_tac "proving" (do_prove !pte_to_fix args branches)
+ in
+ observe_tac "instanciating rec hyps"
+ (instanciate_hyps_with_args do_prove_on_branches !branches (List.rev args))
+ g'
+ )
+ ]
+ g
+ )
+ ]
+ goal
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+exception Toberemoved_with_rel of int*constr
+exception Toberemoved
+
+let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
+ let princ_type_info = compute_elim_sig princ_type in
+ let env = Global.env () in
+(* let type_sort = (Termops.new_sort_in_family InType) in *)
+ let change_predicate_sort i (x,_,t) =
+ let new_sort = sorts.(i) in
+ let args,_ = decompose_prod t in
+ let real_args =
+ if princ_type_info.indarg_in_concl
+ then List.tl args
+ else args
+ in
+ x,None,compose_prod real_args (mkSort new_sort)
+ in
+ let new_predicates =
+ list_map_i
+ change_predicate_sort
+ 0
+ princ_type_info.predicates
+ in
+ let env_with_params_and_predicates =
+ Environ.push_rel_context
+ new_predicates
+ (Environ.push_rel_context
+ princ_type_info.params
+ env
+ )
+ in
+ let rel_as_kn =
+ fst (match princ_type_info.indref with
+ | Some (Libnames.IndRef ind) -> ind
+ | _ -> failwith "Not a valid predicate"
+ )
+ in
+ let pre_princ =
+ it_mkProd_or_LetIn
+ ~init:
+ (it_mkProd_or_LetIn
+ ~init:(option_fold_right
+ mkProd_or_LetIn
+ princ_type_info.indarg
+ princ_type_info.concl
+ )
+ princ_type_info.args
+ )
+ princ_type_info.branches
+ in
+ let is_dom c =
+ match kind_of_term c with
+ | Ind((u,_)) -> u = rel_as_kn
+ | Construct((u,_),_) -> u = rel_as_kn
+ | _ -> false
+ in
+ let get_fun_num c =
+ match kind_of_term c with
+ | Ind(_,num) -> num
+ | Construct((_,num),_) -> num
+ | _ -> assert false
+ in
+ let dummy_var = mkVar (id_of_string "________") in
+ let mk_replacement c i args =
+ let res = mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) in
+(* observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); *)
+ res
+ in
+ let rec has_dummy_var t =
+ fold_constr
+ (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t))
+ false
+ t
+ in
+ let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
+ let (new_princ_type,_) as res =
+ match kind_of_term pre_princ with
+ | Rel n ->
+ begin
+ try match Environ.lookup_rel n env with
+ | _,_,t when is_dom t -> raise Toberemoved
+ | _ -> pre_princ,[] with Not_found -> assert false
+ end
+ | Prod(x,t,b) ->
+ compute_new_princ_type_for_binder remove mkProd env x t b
+ | Lambda(x,t,b) ->
+ compute_new_princ_type_for_binder remove mkLambda env x t b
+ | Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved
+ | App(f,args) when is_dom f ->
+ let var_to_be_removed = destRel (array_last args) in
+ let num = get_fun_num f in
+ raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement pre_princ num args))
+ | App(f,args) ->
+ let is_pte =
+ match kind_of_term f with
+ | Rel n ->
+ is_pte (Environ.lookup_rel n env)
+ | _ -> false
+ in
+ let args =
+ if is_pte && remove
+ then array_get_start args
+ else args
+ in
+ let new_args,binders_to_remove =
+ Array.fold_right (compute_new_princ_type_with_acc remove env)
+ args
+ ([],[])
+ in
+ let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in
+ applist(new_f, new_args),
+ list_union_eq eq_constr binders_to_remove_from_f binders_to_remove
+ | LetIn(x,v,t,b) ->
+ compute_new_princ_type_for_letin remove env x v t b
+ | _ -> pre_princ,[]
+ in
+(* observennl ( *)
+(* match kind_of_term pre_princ with *)
+(* | Prod _ -> *)
+(* str "compute_new_princ_type for "++ *)
+(* pr_lconstr_env env pre_princ ++ *)
+(* str" is "++ *)
+(* pr_lconstr_env env new_princ_type ++ fnl () *)
+(* | _ -> str "" *)
+(* ); *)
+ res
+
+ and compute_new_princ_type_for_binder remove bind_fun env x t b =
+ begin
+ try
+ let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
+ let new_x : name = get_name (ids_of_context env) x in
+ let new_env = Environ.push_rel (x,None,t) env in
+ let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
+ if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
+ then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+ else
+ (
+ bind_fun(new_x,new_t,new_b),
+ list_union_eq
+ eq_constr
+ binders_to_remove_from_t
+ (List.map pop binders_to_remove_from_b)
+ )
+
+ with
+ | Toberemoved ->
+(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+ let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in
+ new_b, List.map pop binders_to_remove_from_b
+ | Toberemoved_with_rel (n,c) ->
+(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+ let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in
+ new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+ end
+ and compute_new_princ_type_for_letin remove env x v t b =
+ begin
+ try
+ let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
+ let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in
+ let new_x : name = get_name (ids_of_context env) x in
+ let new_env = Environ.push_rel (x,Some v,t) env in
+ let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
+ if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
+ then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+ else
+ (
+ mkLetIn(new_x,new_v,new_t,new_b),
+ list_union_eq
+ eq_constr
+ (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
+ (List.map pop binders_to_remove_from_b)
+ )
+
+ with
+ | Toberemoved ->
+(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+ let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in
+ new_b, List.map pop binders_to_remove_from_b
+ | Toberemoved_with_rel (n,c) ->
+(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+ let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in
+ new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+ end
+ and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) =
+ let new_e,to_remove_from_e = compute_new_princ_type remove env e
+ in
+ new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
+ in
+(* observe (str "Computing new principe from " ++ pr_lconstr_env env_with_params_and_predicates pre_princ); *)
+ let pre_res,_ =
+ compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ in
+ it_mkProd_or_LetIn
+ ~init:(it_mkProd_or_LetIn ~init:pre_res new_predicates)
+ princ_type_info.params
+
+
+
+let change_property_sort toSort princ princName =
+ let princ_info = compute_elim_sig princ in
+ let change_sort_in_predicate (x,v,t) =
+ (x,None,
+ let args,_ = decompose_prod t in
+ compose_prod args (mkSort toSort)
+ )
+ in
+ let princName_as_constr = Tacinterp.constr_of_id (Global.env ()) princName in
+ let init =
+ let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in
+ mkApp(princName_as_constr,
+ Array.init nargs
+ (fun i -> mkRel (nargs - i )))
+ in
+ it_mkLambda_or_LetIn
+ ~init:
+ (it_mkLambda_or_LetIn ~init
+ (List.map change_sort_in_predicate princ_info.predicates)
+ )
+ princ_info.params
+
+
+let pp_dur time time' =
+ str (string_of_float (System.time_difference time time'))
+
+(* Things to be removed latter : just here to compare
+ saving proof with and without normalizing the proof
+*)
+let new_save id const (locality,kind) hook =
+ let {const_entry_body = pft;
+ const_entry_type = tpo;
+ const_entry_opaque = opacity } = const in
+ let l,r = match locality with
+ | Decl_kinds.Local when Lib.sections_are_opened () ->
+ let k = Decl_kinds.logical_kind_of_goal_kind kind in
+ let c = Declare.SectionLocalDef (pft, tpo, opacity) in
+ let _ = Declare.declare_variable id (Lib.cwd(), c, k) in
+ (Decl_kinds.Local, Libnames.VarRef id)
+ | Decl_kinds.Local ->
+ let k = Decl_kinds.logical_kind_of_goal_kind kind in
+ let kn = Declare.declare_constant id (DefinitionEntry const, k) in
+ (Decl_kinds.Global, Libnames.ConstRef kn)
+ | Decl_kinds.Global ->
+ let k = Decl_kinds.logical_kind_of_goal_kind kind in
+ let kn = Declare.declare_constant id (DefinitionEntry const, k) in
+ (Decl_kinds.Global, Libnames.ConstRef kn) in
+ let time1 = System.get_time () in
+ Pfedit.delete_current_proof ();
+ let time2 = System.get_time () in
+ hook l r;
+ time1,time2
+(* definition_message id *)
+
+
+
+
+
+let new_save_named opacity =
+(* if do_observe () *)
+(* then *)
+ let time1 = System.get_time () in
+ let id,(const,persistence,hook) = Pfedit.cook_proof () in
+ let time2 = System.get_time () in
+ let const =
+ { const with
+ const_entry_body = (* nf_betaoiotazeta *)const.const_entry_body ;
+ const_entry_opaque = opacity
+ }
+ in
+ let time3 = System.get_time () in
+ let time4,time5 = new_save id const persistence hook in
+ let time6 = System.get_time () in
+ Pp.msgnl
+ (str "cooking proof time : " ++ pp_dur time1 time2 ++ fnl () ++
+ str "reducing proof time : " ++ pp_dur time2 time3 ++ fnl () ++
+ str "saving proof time : " ++ pp_dur time3 time4 ++fnl () ++
+ str "deleting proof time : " ++ pp_dur time4 time5 ++fnl () ++
+ str "hook time :" ++ pp_dur time5 time6
+ )
+
+;;
+
+(* End of things to be removed latter : just here to compare
+ saving proof with and without normalizing the proof
+*)
+
+
+let generate_functional_principle
+ interactive_proof
+ old_princ_type sorts new_princ_name funs i proof_tac
+ =
+ let f = funs.(i) in
+ let type_sort = Termops.new_sort_in_family InType in
+ let new_sorts =
+ match sorts with
+ | None -> Array.make (Array.length funs) (type_sort)
+ | Some a -> a
+ in
+ (* First we get the type of the old graph principle *)
+ let mutr_nparams = (compute_elim_sig old_princ_type).nparams in
+ (* First we get the type of the old graph principle *)
+ let new_principle_type =
+ compute_new_princ_type_from_rel
+ (Array.map mkConst funs)
+ new_sorts
+ old_princ_type
+ in
+(* observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *)
+ let base_new_princ_name,new_princ_name =
+ match new_princ_name with
+ | Some (id) -> id,id
+ | None ->
+ let id_of_f = id_of_label (con_label f) in
+ id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
+ in
+ let names = ref [new_princ_name] in
+ let hook _ _ =
+ if sorts = None
+ then
+(* let id_of_f = id_of_label (con_label f) in *)
+ let register_with_sort fam_sort =
+ let s = Termops.new_sort_in_family fam_sort in
+ let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
+ let value =
+ change_property_sort s new_principle_type new_princ_name
+ in
+(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
+ let ce =
+ { const_entry_body = value;
+ const_entry_type = None;
+ const_entry_opaque = false;
+ const_entry_boxed = Options.boxed_definitions()
+ }
+ in
+ ignore(
+ Declare.declare_constant
+ name
+ (Entries.DefinitionEntry ce,
+ Decl_kinds.IsDefinition (Decl_kinds.Scheme)
+ )
+ );
+ names := name :: !names
+ in
+ register_with_sort InProp;
+ register_with_sort InSet
+ in
+ begin
+ Command.start_proof
+ new_princ_name
+ (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
+ new_principle_type
+ hook
+ ;
+ try
+ let _tim1 = System.get_time () in
+ Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams);
+ let _tim2 = System.get_time () in
+(* begin *)
+(* let dur1 = System.time_difference tim1 tim2 in *)
+(* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
+(* end; *)
+ let do_save = not (do_observe ()) && not interactive_proof in
+ let _ =
+ try
+ Options.silently Command.save_named true;
+ let _dur2 = System.time_difference _tim2 (System.get_time ()) in
+(* Pp.msgnl (str ("Time to check proof: ") ++ str (string_of_float dur2)); *)
+ Options.if_verbose
+ (fun () ->
+ Pp.msgnl (
+ prlist_with_sep
+ (fun () -> str" is defined " ++ fnl ())
+ Ppconstr.pr_id
+ (List.rev !names) ++ str" is defined "
+ )
+ )
+ ()
+ with e when do_save ->
+ msg_warning
+ (
+ Cerrors.explain_exn e
+ );
+ if not (do_observe ())
+ then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end
+ in
+ ()
+
+(* let tim3 = Sys.time () in *)
+(* Pp.msgnl (str ("Time to save proof: ") ++ str (string_of_float (tim3 -. tim2))); *)
+
+ with
+ | e ->
+ msg_warning
+ (
+ Cerrors.explain_exn e
+ );
+ if not ( do_observe ())
+ then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end
+ end
+
+
+
+
+
+
+let get_funs_constant mp dp =
+ let rec get_funs_constant const e : (Names.constant*int) array =
+ match kind_of_term (snd (decompose_lam e)) with
+ | Fix((_,(na,_,_))) ->
+ Array.mapi
+ (fun i na ->
+ match na with
+ | Name id ->
+ let const = make_con mp dp (label_of_id id) in
+ const,i
+ | Anonymous ->
+ anomaly "Anonymous fix"
+ )
+ na
+ | _ -> [|const,0|]
+ in
+ function const ->
+ let find_constant_body const =
+ match (Global.lookup_constant const ).const_body with
+ | Some b ->
+ let body = force b in
+ let body = Tacred.cbv_norm_flags
+ (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ (Global.env ())
+ (Evd.empty)
+ body
+ in
+ body
+ | None -> error ( "Cannot define a principle over an axiom ")
+ in
+ let f = find_constant_body const in
+ let l_const = get_funs_constant const f in
+ (*
+ We need to check that all the functions found are in the same block
+ to prevent Reset stange thing
+ *)
+ let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in
+ let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in
+ (* all the paremeter must be equal*)
+ let _check_params =
+ let first_params = List.hd l_params in
+ List.iter
+ (fun params ->
+ if not ((=) first_params params)
+ then error "Not a mutal recursive block"
+ )
+ l_params
+ in
+ (* The bodies has to be very similar *)
+ let _check_bodies =
+ try
+ let extract_info is_first body =
+ match kind_of_term body with
+ | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
+ | _ ->
+ if is_first && (List.length l_bodies = 1)
+ then raise Not_Rec
+ else error "Not a mutal recursive block"
+ in
+ let first_infos = extract_info true (List.hd l_bodies) in
+ let check body = (* Hope this is correct *)
+ if not (first_infos = (extract_info false body))
+ then error "Not a mutal recursive block"
+ in
+ List.iter check l_bodies
+ with Not_Rec -> ()
+ in
+ l_const
+
+let make_scheme fas =
+ let env = Global.env ()
+ and sigma = Evd.empty in
+ let id_to_constr id =
+ Tacinterp.constr_of_id env id
+ in
+ let funs = List.map (fun (_,f,_) -> id_to_constr f) fas in
+ let first_fun = destConst (List.hd funs) in
+ let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in
+ let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in
+ let first_fun_kn =
+ (* Fixme: take into accour funs_mp and funs_dp *)
+ fst (destInd (id_to_constr first_fun_rel_id))
+ in
+ let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
+ let this_block_funs = Array.map fst this_block_funs_indexes in
+ let prop_sort = InProp in
+ let funs_indexes =
+ let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
+ List.map
+ (function const -> List.assoc (destConst const) this_block_funs_indexes)
+ funs
+ in
+ let ind_list =
+ List.map
+ (fun (idx) ->
+ let ind = first_fun_kn,idx in
+ let (mib,mip) = Global.lookup_inductive ind in
+ ind,mib,mip,true,prop_sort
+ )
+ funs_indexes
+ in
+ let l_schemes = List.map (Typing.type_of env sigma ) (Indrec.build_mutual_indrec env sigma ind_list) in
+ let i = ref (-1) in
+ let sorts =
+ List.rev_map (fun (_,_,x) ->
+ Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+ )
+ fas
+ in
+ let princ_names = List.map (fun (x,_,_) -> x) fas in
+ let _ = List.map2
+ (fun princ_name scheme_type ->
+ incr i;
+(* observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *)
+(* pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *)
+(* ); *)
+ generate_functional_principle
+ false
+ scheme_type
+ (Some (Array.of_list sorts))
+ (Some princ_name)
+ this_block_funs
+ !i
+ (prove_princ_for_struct false !i (Array.of_list (List.map destConst funs)))
+ )
+ princ_names
+ l_schemes
+ in
+ ()
+
+let make_case_scheme fa =
+ let env = Global.env ()
+ and sigma = Evd.empty in
+ let id_to_constr id =
+ Tacinterp.constr_of_id env id
+ in
+ let funs = (fun (_,f,_) -> id_to_constr f) fa in
+ let first_fun = destConst funs in
+ let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in
+ let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in
+ let first_fun_kn =
+ (* Fixme: take into accour funs_mp and funs_dp *)
+ fst (destInd (id_to_constr first_fun_rel_id))
+ in
+ let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
+ let this_block_funs = Array.map fst this_block_funs_indexes in
+ let prop_sort = InProp in
+ let funs_indexes =
+ let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
+ List.assoc (destConst funs) this_block_funs_indexes
+ in
+ let ind_fun =
+ let ind = first_fun_kn,funs_indexes in
+ ind,prop_sort
+ in
+ let scheme_type = (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf) ind_fun) in
+ let sorts =
+ (fun (_,_,x) ->
+ Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+ )
+ fa
+ in
+ let princ_name = (fun (x,_,_) -> x) fa in
+ let _ =
+(* observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *)
+(* pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *)
+(* ); *)
+ generate_functional_principle
+ false
+ scheme_type
+ (Some ([|sorts|]))
+ (Some princ_name)
+ this_block_funs
+ 0
+ (prove_princ_for_struct false 0 [|destConst funs|])
+ in
+ ()
diff --git a/contrib/funind/new_arg_principle.mli b/contrib/funind/new_arg_principle.mli
new file mode 100644
index 00000000..cad68da6
--- /dev/null
+++ b/contrib/funind/new_arg_principle.mli
@@ -0,0 +1,34 @@
+
+val generate_functional_principle :
+ (* do we accept interactive proving *)
+ bool ->
+ (* induction principle on rel *)
+ Term.types ->
+ (* *)
+ Term.sorts array option ->
+ (* Name of the new principle *)
+ (Names.identifier) option ->
+ (* the compute functions to use *)
+ Names.constant array ->
+ (* We prove the nth- principle *)
+ int ->
+ (* The tactic to use to make the proof w.r
+ the number of params
+ *)
+ (Term.constr array -> int -> Tacmach.tactic) ->
+ unit
+
+
+
+(* val my_reflexivity : Tacmach.tactic *)
+
+val prove_princ_for_struct :
+ bool ->
+ int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic
+
+
+val compute_new_princ_type_from_rel : Term.constr array -> Term.sorts array ->
+ Term.types -> Term.types
+
+val make_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort) list -> unit
+val make_case_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort) -> unit
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
new file mode 100644
index 00000000..327198b9
--- /dev/null
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -0,0 +1,1012 @@
+open Printer
+open Pp
+open Names
+open Term
+open Rawterm
+open Libnames
+open Indfun_common
+open Util
+open Rawtermops
+
+let observe strm =
+ if Tacinterp.get_debug () <> Tactic_debug.DebugOff && false
+ then Pp.msgnl strm
+ else ()
+let observennl strm =
+ if Tacinterp.get_debug () <> Tactic_debug.DebugOff &&false
+ then Pp.msg strm
+ else ()
+
+(* type binder_type = *)
+(* | Lambda *)
+(* | Prod *)
+(* | LetIn *)
+
+(* type raw_context = (binder_type*name*rawconstr) list *)
+
+type binder_type =
+ | Lambda of name
+ | Prod of name
+ | LetIn of name
+(* | LetTuple of name list * name *)
+
+type raw_context = (binder_type*rawconstr) list
+
+
+(*
+ compose_raw_context [(bt_1,n_1,t_1);......] rt returns
+ b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the
+ binders corresponding to the bt_i's
+*)
+let compose_raw_context =
+ let compose_binder (bt,t) acc =
+ match bt with
+ | Lambda n -> mkRLambda(n,t,acc)
+ | Prod n -> mkRProd(n,t,acc)
+ | LetIn n -> mkRLetIn(n,t,acc)
+(* | LetTuple (nal,na) -> *)
+(* RLetTuple(dummy_loc,nal,(na,None),t,acc) *)
+ in
+ List.fold_right compose_binder
+
+
+(*
+ The main part deals with building a list of raw constructor expressions
+ from the rhs of a fixpoint equation.
+
+
+*)
+
+
+
+type 'a build_entry_pre_return =
+ {
+ context : raw_context; (* the binding context of the result *)
+ value : 'a; (* The value *)
+ }
+
+type 'a build_entry_return =
+ {
+ result : 'a build_entry_pre_return list;
+ to_avoid : identifier list
+ }
+
+
+(*
+ [combine_results combine_fun res1 res2] combine two results [res1] and [res2]
+ w.r.t. [combine_fun].
+
+ Informally, both [res1] and [res2] are lists of "constructors" [res1_1;...]
+ and [res2_1,....] and we need to produce
+ [combine_fun res1_1 res2_1;combine_fun res1_1 res2_2;........]
+*)
+
+let combine_results
+ (combine_fun : 'a build_entry_pre_return -> 'b build_entry_pre_return ->
+ 'c build_entry_pre_return
+ )
+ (res1: 'a build_entry_return)
+ (res2 : 'b build_entry_return)
+ : 'c build_entry_return
+ =
+ let pre_result = List.map
+ ( fun res1 -> (* for each result in arg_res *)
+ List.map (* we add it in each args_res *)
+ (fun res2 ->
+ combine_fun res1 res2
+ )
+ res2.result
+ )
+ res1.result
+ in (* and then we flatten the map *)
+ {
+ result = List.concat pre_result;
+ to_avoid = list_union res1.to_avoid res2.to_avoid
+ }
+
+
+(*
+ The combination function for an argument with a list of argument
+*)
+
+let combine_args arg args =
+ {
+ context = arg.context@args.context;
+ (* Note that the binding context of [arg] MUST be placed before the one of
+ [args] in order to preserve possible type dependencies
+ *)
+ value = arg.value::args.value;
+ }
+
+
+let ids_of_binder = function
+ | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> []
+ | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> [id]
+(* | LetTuple(nal,_) -> *)
+(* map_succeed (function Name id -> id | _ -> failwith "ids_of_binder") nal *)
+
+let rec change_vars_in_binder mapping = function
+ [] -> []
+ | (bt,t)::l ->
+ let new_mapping = List.fold_right Idmap.remove (ids_of_binder bt) mapping in
+ (bt,change_vars mapping t)::
+ (if idmap_is_empty new_mapping
+ then l
+ else change_vars_in_binder new_mapping l
+ )
+
+let rec replace_var_by_term_in_binder x_id term = function
+ | [] -> []
+ | (bt,t)::l ->
+ (bt,replace_var_by_term x_id term t)::
+ if List.mem x_id (ids_of_binder bt)
+ then l
+ else replace_var_by_term_in_binder x_id term l
+
+let add_bt_names bt = List.append (ids_of_binder bt)
+
+(* let rec replace_var_by_term_in_binder x_id term = function *)
+(* | [] -> [] *)
+(* | (bt,Name id,t)::l when id_ord id x_id = 0 -> *)
+(* (bt,Name id,replace_var_by_term x_id term t)::l *)
+(* | (bt,na,t)::l -> *)
+(* (bt,na,replace_var_by_term x_id term t)::(replace_var_by_term_in_binder x_id term l) *)
+
+(* let rec change_vars_in_binder mapping = function *)
+(* | [] -> [] *)
+(* | (bt,(Name id as na),t)::l when Idmap.mem id mapping -> *)
+(* (bt,na,change_vars mapping t):: l *)
+(* | (bt,na,t)::l -> *)
+(* (bt,na,change_vars mapping t):: *)
+(* (change_vars_in_binder mapping l) *)
+
+
+(* let alpha_ctxt avoid b = *)
+(* let rec alpha_ctxt = function *)
+(* | [] -> [],b *)
+(* | (bt,n,t)::ctxt -> *)
+(* let new_ctxt,new_b = alpha_ctxt ctxt in *)
+(* match n with *)
+(* | Name id when List.mem id avoid -> *)
+(* let new_id = Nameops.next_ident_away id avoid in *)
+(* let mapping = Idmap.add id new_id Idmap.empty in *)
+(* (bt,Name new_id,t):: *)
+(* (change_vars_in_binder mapping new_ctxt), *)
+(* change_vars mapping new_b *)
+(* | _ -> (bt,n,t)::new_ctxt,new_b *)
+(* in *)
+(* alpha_ctxt *)
+let apply_args ctxt body args =
+ let need_convert_id avoid id =
+ List.exists (is_free_in id) args || List.mem id avoid
+ in
+ let need_convert avoid bt =
+ List.exists (need_convert_id avoid) (ids_of_binder bt)
+ in
+(* let add_name na avoid = *)
+(* match na with *)
+(* | Anonymous -> avoid *)
+(* | Name id -> id::avoid *)
+(* in *)
+ let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) =
+ match na with
+ | Name id when List.mem id avoid ->
+ let new_id = Nameops.next_ident_away id avoid in
+ Name new_id,Idmap.add id new_id mapping,new_id::avoid
+ | _ -> na,mapping,avoid
+ in
+ let next_bt_away bt (avoid:identifier list) =
+ match bt with
+ | LetIn na ->
+ let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in
+ LetIn new_na,mapping,new_avoid
+ | Prod na ->
+ let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in
+ Prod new_na,mapping,new_avoid
+ | Lambda na ->
+ let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in
+ Lambda new_na,mapping,new_avoid
+(* | LetTuple (nal,na) -> *)
+(* let rev_new_nal,mapping,new_avoid = *)
+(* List.fold_left *)
+(* (fun (nal,mapping,(avoid:identifier list)) na -> *)
+(* let new_na,new_mapping,new_avoid = next_name_away na mapping avoid in *)
+(* (new_na::nal,new_mapping,new_avoid) *)
+(* ) *)
+(* ([],Idmap.empty,avoid) *)
+(* nal *)
+(* in *)
+(* (LetTuple(List.rev rev_new_nal,na),mapping,new_avoid) *)
+ in
+ let rec do_apply avoid ctxt body args =
+ match ctxt,args with
+ | _,[] -> (* No more args *)
+ (ctxt,body)
+ | [],_ -> (* no more fun *)
+ let f,args' = raw_decompose_app body in
+ (ctxt,mkRApp(f,args'@args))
+ | (Lambda Anonymous,t)::ctxt',arg::args' ->
+ do_apply avoid ctxt' body args'
+ | (Lambda (Name id),t)::ctxt',arg::args' ->
+ let new_avoid,new_ctxt',new_body,new_id =
+ if need_convert_id avoid id
+ then
+ let new_avoid = id::avoid in
+ let new_id = Nameops.next_ident_away id new_avoid in
+ let new_avoid' = new_id :: new_avoid in
+ let mapping = Idmap.add id new_id Idmap.empty in
+ let new_ctxt' = change_vars_in_binder mapping ctxt' in
+ let new_body = change_vars mapping body in
+ new_avoid',new_ctxt',new_body,new_id
+ else
+ id::avoid,ctxt',body,id
+ in
+ let new_body = replace_var_by_term new_id arg new_body in
+ let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
+ do_apply avoid new_ctxt' new_body args'
+ | (bt,t)::ctxt',_ ->
+ let new_avoid,new_ctxt',new_body,new_bt =
+ let new_avoid = add_bt_names bt avoid in
+ if need_convert avoid bt
+ then
+ let new_bt,mapping,new_avoid = next_bt_away bt new_avoid in
+ (
+ new_avoid,
+ change_vars_in_binder mapping ctxt',
+ change_vars mapping body,
+ new_bt
+ )
+ else new_avoid,ctxt',body,bt
+ in
+ let new_ctxt',new_body =
+ do_apply new_avoid new_ctxt' new_body args
+ in
+ (new_bt,t)::new_ctxt',new_body
+ in
+ do_apply [] ctxt body args
+
+
+let combine_app f args =
+ let new_ctxt,new_value = apply_args f.context f.value args.value in
+ {
+ (* Note that the binding context of [args] MUST be placed before the one of
+ the applied value in order to preserve possible type dependencies
+ *)
+
+ context = args.context@new_ctxt;
+ value = new_value;
+ }
+
+let combine_lam n t b =
+ {
+ context = [];
+ value = mkRLambda(n, compose_raw_context t.context t.value,
+ compose_raw_context b.context b.value )
+ }
+
+
+
+let combine_prod n t b =
+ { context = t.context@((Prod n,t.value)::b.context); value = b.value}
+
+let combine_letin n t b =
+ { context = t.context@((LetIn n,t.value)::b.context); value = b.value}
+
+(* let combine_tuple nal na b in_e = *)
+(* { *)
+(* context = b.context@(LetTuple(nal,na),b.value)::in_e.context; *)
+(* value = in_e.value *)
+(* } *)
+
+let mk_result ctxt value avoid =
+ {
+ result =
+ [{context = ctxt;
+ value = value}]
+ ;
+ to_avoid = avoid
+ }
+
+
+let make_discr_match_el =
+ List.map (fun e -> (e,(Anonymous,None)))
+
+let coq_True_ref =
+ lazy (Coqlib.gen_reference "" ["Init";"Logic"] "True")
+
+let coq_False_ref =
+ lazy (Coqlib.gen_reference "" ["Init";"Logic"] "False")
+
+let make_discr_match_brl i =
+ list_map_i
+ (fun j (_,idl,patl,_) ->
+ if j=i
+ then (dummy_loc,idl,patl, mkRRef (Lazy.force coq_True_ref))
+ else (dummy_loc,idl,patl, mkRRef (Lazy.force coq_False_ref))
+ )
+ 0
+
+let make_discr_match brl =
+ fun el i ->
+ mkRCases(None,
+ make_discr_match_el el,
+ make_discr_match_brl i brl)
+
+
+
+let rec make_pattern_eq_precond id e pat : identifier * (binder_type * Rawterm.rawconstr) list =
+ match pat with
+ | PatVar(_,Anonymous) -> assert false
+ | PatVar(_,Name x) ->
+ id,[Prod (Name x),mkRHole ();Prod Anonymous,raw_make_eq (mkRVar x) e]
+ | PatCstr(_,constr,patternl,_) ->
+ let new_id,new_patternl,patternl_eq_precond =
+ List.fold_right
+ (fun pat' (id,new_patternl,preconds) ->
+ match pat' with
+ | PatVar (_,Name id) -> (id,id::new_patternl,preconds)
+ | _ ->
+ let new_id = Nameops.lift_ident id in
+ let new_id',pat'_precond =
+ make_pattern_eq_precond new_id (mkRVar id) pat'
+ in
+ (new_id',id::new_patternl,preconds@pat'_precond)
+ )
+ patternl
+ (id,[],[])
+ in
+ let cst_narg =
+ Inductiveops.mis_constructor_nargs_env
+ (Global.env ())
+ constr
+ in
+ let implicit_args =
+ Array.to_list
+ (Array.init
+ (cst_narg - List.length patternl)
+ (fun _ -> mkRHole ())
+ )
+ in
+ let cst_as_term =
+ mkRApp(mkRRef(Libnames.ConstructRef constr),
+ implicit_args@(List.map mkRVar new_patternl)
+ )
+ in
+ let precond' =
+ (Prod Anonymous, raw_make_eq cst_as_term e)::patternl_eq_precond
+ in
+ let precond'' =
+ List.fold_right
+ (fun id acc ->
+ (Prod (Name id),(mkRHole ()))::acc
+ )
+ new_patternl
+ precond'
+ in
+ new_id,precond''
+
+let pr_name = function
+ | Name id -> Ppconstr.pr_id id
+ | Anonymous -> str "_"
+
+let make_pattern_eq_precond id e pat =
+ let res = make_pattern_eq_precond id e pat in
+ observe
+ (prlist_with_sep spc
+ (function (Prod na,t) ->
+ str "forall " ++ pr_name na ++ str ":" ++ pr_rawconstr t
+ | _ -> assert false
+ )
+ (snd res)
+ );
+ res
+
+
+let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
+(* Pp.msgnl (str " Entering : " ++ Printer.pr_rawconstr rt); *)
+ match rt with
+ | RRef _ | RVar _ | REvar _ | RPatVar _ | RSort _ | RHole _ ->
+ mk_result [] rt avoid
+ | RApp(_,_,_) ->
+ let f,args = raw_decompose_app rt in
+ let args_res : (rawconstr list) build_entry_return =
+ List.fold_right
+ (fun arg ctxt_argsl ->
+ let arg_res = build_entry_lc funnames ctxt_argsl.to_avoid arg in
+ combine_results combine_args arg_res ctxt_argsl
+ )
+ args
+ (mk_result [] [] avoid)
+ in
+ begin
+ match f with
+ | RVar(_,id) when Idset.mem id funnames ->
+ let res = fresh_id args_res.to_avoid "res" in
+ let new_avoid = res::args_res.to_avoid in
+ let res_rt = mkRVar res in
+ let new_result =
+ List.map
+ (fun arg_res ->
+ let new_hyps =
+ [Prod (Name res),mkRHole ();
+ Prod Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)]
+ in
+ {context = arg_res.context@new_hyps; value = res_rt }
+ )
+ args_res.result
+ in
+ { result = new_result; to_avoid = new_avoid }
+ | RVar _ | REvar _ | RPatVar _ | RHole _ | RSort _ | RRef _ ->
+ {
+ args_res with
+ result =
+ List.map
+ (fun args_res ->
+ {args_res with value = mkRApp(f,args_res.value)})
+ args_res.result
+ }
+ | RApp _ -> assert false (* we have collected all the app *)
+ | RLetIn(_,n,t,b) ->
+ let new_n,new_b,new_avoid =
+ match n with
+ | Name id when List.exists (is_free_in id) args ->
+ (* need to alpha-convert the name *)
+ let new_id = Nameops.next_ident_away id avoid in
+ let new_avoid = id:: avoid in
+ let new_b =
+ replace_var_by_term
+ id
+ (RVar(dummy_loc,id))
+ b
+ in
+ (Name new_id,new_b,new_avoid)
+ | _ -> n,b,avoid
+ in
+ build_entry_lc
+ funnames
+ avoid
+ (mkRLetIn(new_n,t,mkRApp(new_b,args)))
+ | RCases _ | RLambda _ ->
+ let f_res = build_entry_lc funnames args_res.to_avoid f in
+ combine_results combine_app f_res args_res
+ | RDynamic _ ->error "Not handled RDynamic"
+ | RCast _ -> error "Not handled RCast"
+ | RRec _ -> error "Not handled RRec"
+ | RIf _ -> error "Not handled RIf"
+ | RLetTuple _ -> error "Not handled RLetTuple"
+ | RProd _ -> error "Cannot apply a type"
+ end
+ | RLambda(_,n,t,b) ->
+ let b_res = build_entry_lc funnames avoid b in
+ let t_res = build_entry_lc funnames avoid t in
+ let new_n =
+ match n with
+ | Name _ -> n
+ | Anonymous -> Name (Indfun_common.fresh_id [] "_x")
+ in
+ combine_results (combine_lam new_n) t_res b_res
+ | RProd(_,n,t,b) ->
+ let b_res = build_entry_lc funnames avoid b in
+ let t_res = build_entry_lc funnames avoid t in
+ combine_results (combine_prod n) t_res b_res
+ | RLetIn(_,n,t,b) ->
+ let b_res = build_entry_lc funnames avoid b in
+ let t_res = build_entry_lc funnames avoid t in
+ combine_results (combine_letin n) t_res b_res
+ | RCases(_,_,el,brl) ->
+ let make_discr = make_discr_match brl in
+ build_entry_lc_from_case funnames make_discr el brl avoid
+ | RIf _ -> error "Not handled RIf"
+ | RLetTuple _ -> error "Not handled RLetTuple"
+ | RRec _ -> error "Not handled RRec"
+ | RCast _ -> error "Not handled RCast"
+ | RDynamic _ -> error "Not handled RDynamic"
+and build_entry_lc_from_case funname make_discr
+ (el:(Rawterm.rawconstr *
+ (Names.name * (loc * Names.inductive * Names.name list) option) )
+ list)
+ (brl:(loc * identifier list * cases_pattern list * rawconstr) list) avoid :
+ rawconstr build_entry_return =
+ match el with
+ | [] -> assert false (* matched on Nothing !*)
+ | el ->
+ let case_resl =
+ List.fold_right
+ (fun (case_arg,_) ctxt_argsl ->
+ let arg_res = build_entry_lc funname avoid case_arg in
+ combine_results combine_args arg_res ctxt_argsl
+ )
+ el
+ (mk_result [] [] avoid)
+ in
+ let results =
+ List.map
+ (build_entry_lc_from_case_term funname make_discr [] brl case_resl.to_avoid)
+ case_resl.result
+ in
+ {
+ result = List.concat (List.map (fun r -> r.result) results);
+ to_avoid =
+ List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results
+ }
+
+and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avoid
+ matched_expr =
+ match brl with
+ | [] -> (* computed_branches *) {result = [];to_avoid = avoid}
+ | br::brl' ->
+ let _,idl,patl,return = alpha_br avoid br in
+ let new_avoid = idl@avoid in
+(* let e_ctxt,el = (matched_expr.context,matched_expr.value) in *)
+(* if (List.length patl) <> (List.length el) *)
+(* then error ("Pattern matching on product: not yet implemented"); *)
+ let not_those_patterns : (identifier list -> rawconstr -> rawconstr) list =
+ List.map
+ (fun pat ->
+ fun avoid pat'_as_term ->
+ let renamed_pat,_,_ = alpha_pat avoid pat in
+ let pat_ids = get_pattern_id renamed_pat in
+ List.fold_right
+ (fun id acc -> mkRProd (Name id,mkRHole (),acc))
+ pat_ids
+ (raw_make_neq pat'_as_term (pattern_to_term renamed_pat))
+ )
+ patl
+ in
+ let unify_with_those_patterns : (cases_pattern -> bool*bool) list =
+ List.map
+ (fun pat pat' -> are_unifiable pat pat',eq_cases_pattern pat pat')
+ patl
+ in
+ let brl'_res =
+ build_entry_lc_from_case_term
+ funname
+ make_discr
+ ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent)
+ brl'
+ avoid
+ matched_expr
+ in
+(* let ids = List.map (fun id -> Prod (Name id),mkRHole ()) idl in *)
+ let those_pattern_preconds =
+( List.flatten
+ (
+ List.map2
+ (fun pat e ->
+ let this_pat_ids = ids_of_pat pat in
+ let pat_as_term = pattern_to_term pat in
+ List.fold_right
+ (fun id acc ->
+ if Idset.mem id this_pat_ids
+ then (Prod (Name id),mkRHole ())::acc
+ else acc
+
+ )
+ idl
+ [(Prod Anonymous,raw_make_eq pat_as_term e)]
+ )
+ patl
+ matched_expr.value
+ )
+)
+ @
+ (if List.exists (function (unifl,neql) ->
+ let (unif,eqs) =
+ List.split (List.map2 (fun x y -> x y) unifl patl)
+ in
+ List.for_all (fun x -> x) unif) patterns_to_prevent
+ then
+ let i = List.length patterns_to_prevent in
+ [(Prod Anonymous,make_discr (List.map pattern_to_term patl) i )]
+ else
+ []
+ )
+ in
+ let return_res = build_entry_lc funname new_avoid return in
+ let this_branch_res =
+ List.map
+ (fun res ->
+ { context =
+ matched_expr.context@
+(* ids@ *)
+ those_pattern_preconds@res.context ;
+ value = res.value}
+ )
+ return_res.result
+ in
+ { brl'_res with result = this_branch_res@brl'_res.result }
+
+
+let is_res id =
+ try
+ String.sub (string_of_id id) 0 3 = "res"
+ with Invalid_argument _ -> false
+
+(* rebuild the raw constructors expression.
+ eliminates some meaningless equalities, applies some rewrites......
+*)
+let rec rebuild_cons nb_args relname args crossed_types depth rt =
+ match rt with
+ | RProd(_,n,t,b) ->
+ let not_free_in_t id = not (is_free_in id t) in
+ let new_crossed_types = t::crossed_types in
+ begin
+ match t with
+ | RApp(_,(RVar(_,res_id) as res_rt),args') when is_res res_id ->
+ begin
+ match args' with
+ | (RVar(_,this_relname))::args' ->
+ let new_b,id_to_exclude =
+ rebuild_cons
+ nb_args relname
+ args new_crossed_types
+ (depth + 1) b
+ in
+ let new_t =
+ mkRApp(mkRVar(mk_rel_id this_relname),args'@[res_rt])
+ in mkRProd(n,new_t,new_b),
+ Idset.filter not_free_in_t id_to_exclude
+ | _ -> (* the first args is the name of the function! *)
+ assert false
+ end
+ | RApp(_,RRef(_,eq_as_ref),[_;RVar(_,id);rt])
+ when eq_as_ref = Lazy.force Coqlib.coq_eq_ref
+ ->
+ let is_in_b = is_free_in id b in
+ let _keep_eq =
+ not (List.exists (is_free_in id) args) || is_in_b ||
+ List.exists (is_free_in id) crossed_types
+ in
+ let new_args = List.map (replace_var_by_term id rt) args in
+ let subst_b =
+ if is_in_b then b else replace_var_by_term id rt b
+ in
+ let new_b,id_to_exclude =
+ rebuild_cons
+ nb_args relname
+ new_args new_crossed_types
+ (depth + 1) subst_b
+ in
+ mkRProd(n,t,new_b),id_to_exclude
+(* if keep_eq then *)
+(* mkRProd(n,t,new_b),id_to_exclude *)
+(* else new_b, Idset.add id id_to_exclude *)
+ | _ ->
+ let new_b,id_to_exclude =
+ rebuild_cons
+ nb_args relname
+ args new_crossed_types
+ (depth + 1) b
+ in
+ match n with
+ | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
+ new_b,Idset.remove id
+ (Idset.filter not_free_in_t id_to_exclude)
+ | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+ end
+ | RLambda(_,n,t,b) ->
+ begin
+(* let not_free_in_t id = not (is_free_in id t) in *)
+(* let new_crossed_types = t :: crossed_types in *)
+(* let new_b,id_to_exclude = rebuild_cons relname args new_crossed_types b in *)
+(* match n with *)
+(* | Name id when Idset.mem id id_to_exclude -> *)
+(* new_b, *)
+(* Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *)
+(* | _ -> *)
+(* RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude *)
+ let not_free_in_t id = not (is_free_in id t) in
+ let new_crossed_types = t :: crossed_types in
+(* let new_b,id_to_exclude = rebuild_cons relname (args new_crossed_types b in *)
+ match n with
+ | Name id ->
+ let new_b,id_to_exclude =
+ rebuild_cons
+ nb_args relname
+ (args@[mkRVar id])new_crossed_types
+ (depth + 1 ) b
+ in
+ if Idset.mem id id_to_exclude && depth >= nb_args
+ then
+ new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
+ else
+ RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+ | _ -> anomaly "Should not have an anonymous function here"
+ (* We have renamed all the anonymous functions during alpha_renaming phase *)
+
+ end
+ | RLetIn(_,n,t,b) ->
+ begin
+ let not_free_in_t id = not (is_free_in id t) in
+ let new_b,id_to_exclude =
+ rebuild_cons
+ nb_args relname
+ args (t::crossed_types)
+ (depth + 1 ) b in
+ match n with
+ | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
+ new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
+ | _ -> RLetIn(dummy_loc,n,t,new_b),
+ Idset.filter not_free_in_t id_to_exclude
+ end
+ | RLetTuple(_,nal,(na,rto),t,b) ->
+ assert (rto=None);
+ begin
+ let not_free_in_t id = not (is_free_in id t) in
+ let new_t,id_to_exclude' =
+ rebuild_cons
+ nb_args
+ relname
+ args (crossed_types)
+ depth t
+ in
+ let new_b,id_to_exclude =
+ rebuild_cons
+ nb_args relname
+ args (t::crossed_types)
+ (depth + 1) b
+ in
+(* match n with *)
+(* | Name id when Idset.mem id id_to_exclude -> *)
+(* new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *)
+(* | _ -> *)
+ RLetTuple(dummy_loc,nal,(na,None),t,new_b),
+ Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude')
+
+ end
+
+ | _ -> mkRApp(mkRVar relname,args@[rt]),Idset.empty
+
+
+let rebuild_cons nb_args relname args crossed_types rt =
+ observennl (str "rebuild_cons : rt := "++ pr_rawconstr rt ++
+ str "nb_args := " ++ str (string_of_int nb_args));
+ let res =
+ rebuild_cons nb_args relname args crossed_types 0 rt
+ in
+ observe (str " leads to "++ pr_rawconstr (fst res));
+ res
+
+let rec compute_cst_params relnames params = function
+ | RRef _ | RVar _ | REvar _ | RPatVar _ -> params
+ | RApp(_,RVar(_,relname'),rtl) when Idset.mem relname' relnames ->
+ compute_cst_params_from_app [] (params,rtl)
+ | RApp(_,f,args) ->
+ List.fold_left (compute_cst_params relnames) params (f::args)
+ | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) ->
+ let t_params = compute_cst_params relnames params t in
+ compute_cst_params relnames t_params b
+ | RCases _ -> params (* If there is still cases at this point they can only be
+ discriminitation ones *)
+ | RSort _ -> params
+ | RHole _ -> params
+ | RIf _ | RRec _ | RCast _ | RDynamic _ ->
+ raise (UserError("compute_cst_params", str "Not handled case"))
+and compute_cst_params_from_app acc (params,rtl) =
+ match params,rtl with
+ | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
+ | ((Name id,_,is_defined) as param)::params',(RVar(_,id'))::rtl'
+ when id_ord id id' == 0 && not is_defined ->
+ compute_cst_params_from_app (param::acc) (params',rtl')
+ | _ -> List.rev acc
+
+let compute_params_name relnames (args : (Names.name * Rawterm.rawconstr * bool) list array) csts =
+ let rels_params =
+ Array.mapi
+ (fun i args ->
+ List.fold_left
+ (fun params (_,cst) -> compute_cst_params relnames params cst)
+ args
+ csts.(i)
+ )
+ args
+ in
+ let l = ref [] in
+ let _ =
+ try
+ list_iter_i
+ (fun i ((n,nt,is_defined) as param) ->
+ if array_for_all
+ (fun l ->
+ let (n',nt',is_defined') = List.nth l i in
+ n = n' && Topconstr.eq_rawconstr nt nt' && is_defined = is_defined')
+ rels_params
+ then
+ l := param::!l
+ )
+ rels_params.(0)
+ with _ ->
+ ()
+ in
+ List.rev !l
+
+(* (Topconstr.CProdN
+ (dummy_loc,
+ [[(dummy_loc,Anonymous)],returned_types.(i)],
+ Topconstr.CSort(dummy_loc, RProp Null )
+ )
+ )
+*)
+let rec rebuild_return_type rt =
+ match rt with
+ | Topconstr.CProdN(loc,n,t') ->
+ Topconstr.CProdN(loc,n,rebuild_return_type t')
+ | Topconstr.CArrow(loc,t,t') ->
+ Topconstr.CArrow(loc,t,rebuild_return_type t')
+ | Topconstr.CLetIn(loc,na,t,t') ->
+ Topconstr.CLetIn(loc,na,t,rebuild_return_type t')
+ | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc, RProp Null))
+
+
+let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list) returned_types (rtl:rawconstr list) =
+(* Pp.msgnl (prlist_with_sep fnl Printer.pr_rawconstr rtl); *)
+ let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in
+ let funnames = Array.of_list funnames in
+ let funsargs = Array.of_list funsargs in
+ let returned_types = Array.of_list returned_types in
+ let rtl_alpha = List.map (function rt -> (alpha_rt [] rt) ) rtl in
+ let rta = Array.of_list rtl_alpha in
+ let relnames = Array.map mk_rel_id funnames in
+ let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in
+ let resa = Array.map (build_entry_lc funnames_as_set []) rta in
+ let constr i res =
+ List.map
+ (function result (* (args',concl') *) ->
+ let rt = compose_raw_context result.context result.value in
+ let nb_args = List.length funsargs.(i) in
+(* Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
+ fst (
+ rebuild_cons nb_args relnames.(i)
+(* (List.map *)
+(* (function *)
+(* (Anonymous,_,_) -> mkRVar(fresh_id res.to_avoid "x__") *)
+(* | Name id, _,_ -> mkRVar id *)
+(* ) *)
+(* funsargs.(i) *)
+(* ) *)
+ []
+ []
+ rt
+ )
+ )
+ res.result
+ in
+ let next_constructor_id = ref (-1) in
+ let mk_constructor_id i =
+ incr next_constructor_id;
+ id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
+ in
+ let rel_constructors i rt : (identifier*rawconstr) list =
+ List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt)
+ in
+ let rel_constructors = Array.mapi rel_constructors resa in
+ let rels_params =
+ if parametrize
+ then
+ compute_params_name relnames_as_set funsargs rel_constructors
+ else []
+ in
+ let nrel_params = List.length rels_params in
+ let rel_constructors =
+ Array.map (List.map
+ (fun (id,rt) -> (id,snd (chop_rprod_n nrel_params rt))))
+ rel_constructors
+ in
+ let rel_arity i funargs =
+ let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list =
+ (snd (list_chop nrel_params funargs))
+ in
+ List.fold_right
+ (fun (n,t,is_defined) acc ->
+ if is_defined
+ then
+ Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_rawconstr Idset.empty t,
+ acc)
+ else
+ Topconstr.CProdN
+ (dummy_loc,
+ [[(dummy_loc,n)],Constrextern.extern_rawconstr Idset.empty t],
+ acc
+ )
+ )
+ rel_first_args
+ (rebuild_return_type returned_types.(i))
+(* (Topconstr.CProdN *)
+(* (dummy_loc, *)
+(* [[(dummy_loc,Anonymous)],returned_types.(i)], *)
+(* Topconstr.CSort(dummy_loc, RProp Null ) *)
+(* ) *)
+(* ) *)
+ in
+ let rel_arities = Array.mapi rel_arity funsargs in
+ let old_rawprint = !Options.raw_print in
+ Options.raw_print := true;
+ let rel_params =
+ List.map
+ (fun (n,t,is_defined) ->
+ if is_defined
+ then
+ Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_rawconstr Idset.empty t)
+ else
+ Topconstr.LocalRawAssum
+ ([(dummy_loc,n)], Constrextern.extern_rawconstr Idset.empty t)
+ )
+ rels_params
+ in
+ let ext_rels_constructors =
+ Array.map (List.map
+ (fun (id,t) ->
+ false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty t)
+ ))
+ rel_constructors
+ in
+ let rel_ind i ext_rel_constructors =
+ (dummy_loc,relnames.(i)),
+ None,
+ rel_params,
+ rel_arities.(i),
+ ext_rel_constructors
+ in
+ let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in
+ let rel_inds = Array.to_list ext_rel_constructors in
+ let _ =
+ observe (
+ str "Inductive" ++ spc () ++
+ prlist_with_sep
+ (fun () -> fnl ()++spc () ++ str "with" ++ spc ())
+ (function ((_,id),_,params,ar,constr) ->
+ Ppconstr.pr_id id ++ spc () ++
+ Ppconstr.pr_binders params ++ spc () ++
+ str ":" ++ spc () ++
+ Ppconstr.pr_lconstr_expr ar ++ spc () ++
+ prlist_with_sep
+ (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ())
+ (function (_,((_,id),t)) ->
+ Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++
+ Ppconstr.pr_lconstr_expr t)
+ constr
+ )
+ rel_inds
+ )
+ in
+ let old_implicit_args = Impargs.is_implicit_args ()
+ and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
+ and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
+ Impargs.make_implicit_args false;
+ Impargs.make_strict_implicit_args false;
+ Impargs.make_contextual_implicit_args false;
+ try
+ Options.silently (Command.build_mutual rel_inds) true;
+ Impargs.make_implicit_args old_implicit_args;
+ Impargs.make_strict_implicit_args old_strict_implicit_args;
+ Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+ Options.raw_print := old_rawprint;
+ with
+ | UserError(s,msg) ->
+ Impargs.make_implicit_args old_implicit_args;
+ Impargs.make_strict_implicit_args old_strict_implicit_args;
+ Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+ Options.raw_print := old_rawprint;
+ let msg =
+ str "while trying to define"++ spc () ++
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
+ msg
+ in
+ observe (msg);
+ raise
+ (UserError(s, msg))
+ | e ->
+ Impargs.make_implicit_args old_implicit_args;
+ Impargs.make_strict_implicit_args old_strict_implicit_args;
+ Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+ Options.raw_print := old_rawprint;
+ let msg =
+ str "while trying to define"++ spc () ++
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
+ Cerrors.explain_exn e
+ in
+ observe msg;
+ raise
+ (UserError("",msg))
+
+
diff --git a/contrib/funind/rawterm_to_relation.mli b/contrib/funind/rawterm_to_relation.mli
new file mode 100644
index 00000000..0cda56df
--- /dev/null
+++ b/contrib/funind/rawterm_to_relation.mli
@@ -0,0 +1,16 @@
+
+(* val new_build_entry_lc : *)
+(* Names.identifier list -> *)
+(* (Names.name*Rawterm.rawconstr) list list -> *)
+(* Topconstr.constr_expr list -> *)
+(* Rawterm.rawconstr list -> *)
+(* unit *)
+
+val build_inductive :
+ bool ->
+ Names.identifier list ->
+ (Names.name*Rawterm.rawconstr*bool) list list ->
+ Topconstr.constr_expr list ->
+ Rawterm.rawconstr list ->
+ unit
+
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
new file mode 100644
index 00000000..99bf2bf1
--- /dev/null
+++ b/contrib/funind/rawtermops.ml
@@ -0,0 +1,525 @@
+open Pp
+open Rawterm
+open Util
+open Names
+(* Ocaml 3.06 Map.S does not handle is_empty *)
+let idmap_is_empty m = m = Idmap.empty
+
+(*
+ Some basic functions to rebuild rawconstr
+ In each of them the location is Util.dummy_loc
+*)
+let mkRRef ref = RRef(dummy_loc,ref)
+let mkRVar id = RVar(dummy_loc,id)
+let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl)
+let mkRLambda(n,t,b) = RLambda(dummy_loc,n,t,b)
+let mkRProd(n,t,b) = RProd(dummy_loc,n,t,b)
+let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
+let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
+let mkRSort s = RSort(dummy_loc,s)
+let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
+
+
+(*
+ Some basic functions to decompose rawconstrs
+ These are analogous to the ones constrs
+*)
+let raw_decompose_prod =
+ let rec raw_decompose_prod args = function
+ | RProd(_,n,t,b) ->
+ raw_decompose_prod ((n,t)::args) b
+ | rt -> args,rt
+ in
+ raw_decompose_prod []
+
+let raw_compose_prod =
+ List.fold_left (fun b (n,t) -> mkRProd(n,t,b))
+
+let raw_decompose_app =
+ let rec decompose_rapp acc rt =
+(* msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *)
+ match rt with
+ | RApp(_,rt,rtl) ->
+ decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt
+ | rt -> rt,List.rev acc
+ in
+ decompose_rapp []
+
+
+
+
+(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *)
+let raw_make_eq t1 t2 =
+ mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[mkRHole ();t2;t1])
+
+(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *)
+let raw_make_neq t1 t2 =
+ mkRApp(mkRRef (Lazy.force Coqlib.coq_not_ref),[raw_make_eq t1 t2])
+
+(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *)
+let raw_make_or t1 t2 = mkRApp (mkRRef(Lazy.force Coqlib.coq_or_ref),[t1;t2])
+
+(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding
+ to [P1 \/ ( .... \/ Pn)]
+*)
+let rec raw_make_or_list = function
+ | [] -> raise (Invalid_argument "mk_or")
+ | [e] -> e
+ | e::l -> raw_make_or e (raw_make_or_list l)
+
+
+
+
+let change_vars =
+ let rec change_vars mapping rt =
+ match rt with
+ | RRef _ -> rt
+ | RVar(loc,id) ->
+ let new_id =
+ try
+ Idmap.find id mapping
+ with Not_found -> id
+ in
+ RVar(loc,new_id)
+ | REvar _ -> rt
+ | RPatVar _ -> rt
+ | RApp(loc,rt',rtl) ->
+ RApp(loc,
+ change_vars mapping rt',
+ List.map (change_vars mapping) rtl
+ )
+ | RLambda(_,Name id,_,_) when Idmap.mem id mapping -> rt
+ | RLambda(loc,name,t,b) ->
+ RLambda(loc,
+ name,
+ change_vars mapping t,
+ change_vars mapping b
+ )
+ | RProd(_,Name id,_,_) when Idmap.mem id mapping -> rt
+ | RProd(loc,name,t,b) ->
+ RProd(loc,
+ name,
+ change_vars mapping t,
+ change_vars mapping b
+ )
+ | RLetIn(_,Name id,_,_) when Idmap.mem id mapping -> rt
+ | RLetIn(loc,name,def,b) ->
+ RLetIn(loc,
+ name,
+ change_vars mapping def,
+ change_vars mapping b
+ )
+ | RLetTuple(_,nal,(na,_),_,_) when List.exists (function Name id -> Idmap.mem id mapping | _ -> false) (na::nal) -> rt
+ | RLetTuple(loc,nal,(na,rto),b,e) ->
+ RLetTuple(loc,
+ nal,
+ (na, option_app (change_vars mapping) rto),
+ change_vars mapping b,
+ change_vars mapping e
+ )
+ | RCases(loc,infos,el,brl) ->
+ RCases(loc,
+ infos,
+ List.map (fun (e,x) -> (change_vars mapping e,x)) el,
+ List.map (change_vars_br mapping) brl
+ )
+ | RIf _ -> error "Not handled RIf"
+ | RRec _ -> error "Not handled RRec"
+ | RSort _ -> rt
+ | RHole _ -> rt
+ | RCast(loc,b,k,t) ->
+ RCast(loc,change_vars mapping b,k,change_vars mapping t)
+ | RDynamic _ -> error "Not handled RDynamic"
+ and change_vars_br mapping ((loc,idl,patl,res) as br) =
+ let new_mapping = List.fold_right Idmap.remove idl mapping in
+ if idmap_is_empty new_mapping
+ then br
+ else (loc,idl,patl,change_vars new_mapping res)
+ in
+ change_vars
+
+
+
+let rec alpha_pat excluded pat =
+ match pat with
+ | PatVar(loc,Anonymous) ->
+ let new_id = Indfun_common.fresh_id excluded "_x" in
+ PatVar(loc,Name new_id),(new_id::excluded),Idmap.empty
+ | PatVar(loc,Name id) ->
+ if List.mem id excluded
+ then
+ let new_id = Nameops.next_ident_away id excluded in
+ PatVar(loc,Name new_id),(new_id::excluded),
+ (Idmap.add id new_id Idmap.empty)
+ else pat,excluded,Idmap.empty
+ | PatCstr(loc,constr,patl,na) ->
+ let new_na,new_excluded,map =
+ match na with
+ | Name id when List.mem id excluded ->
+ let new_id = Nameops.next_ident_away id excluded in
+ Name new_id,new_id::excluded, Idmap.add id new_id Idmap.empty
+ | _ -> na,excluded,Idmap.empty
+ in
+ let new_patl,new_excluded,new_map =
+ List.fold_left
+ (fun (patl,excluded,map) pat ->
+ let new_pat,new_excluded,new_map = alpha_pat excluded pat in
+ (new_pat::patl,new_excluded,Idmap.fold Idmap.add new_map map)
+ )
+ ([],new_excluded,map)
+ patl
+ in
+ PatCstr(loc,constr,List.rev new_patl,new_na),new_excluded,new_map
+
+let alpha_patl excluded patl =
+ let patl,new_excluded,map =
+ List.fold_left
+ (fun (patl,excluded,map) pat ->
+ let new_pat,new_excluded,new_map = alpha_pat excluded pat in
+ new_pat::patl,new_excluded,(Idmap.fold Idmap.add new_map map)
+ )
+ ([],excluded,Idmap.empty)
+ patl
+ in
+ (List.rev patl,new_excluded,map)
+
+
+
+
+let raw_get_pattern_id pat acc =
+ let rec get_pattern_id pat =
+ match pat with
+ | PatVar(loc,Anonymous) -> assert false
+ | PatVar(loc,Name id) ->
+ [id]
+ | PatCstr(loc,constr,patternl,_) ->
+ List.fold_right
+ (fun pat idl ->
+ let idl' = get_pattern_id pat in
+ idl'@idl
+ )
+ patternl
+ []
+ in
+ (get_pattern_id pat)@acc
+
+let get_pattern_id pat = raw_get_pattern_id pat []
+
+let rec alpha_rt excluded rt =
+ let new_rt =
+ match rt with
+ | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt
+ | RLambda(loc,Anonymous,t,b) ->
+ let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in
+ let new_excluded = new_id :: excluded in
+ let new_t = alpha_rt new_excluded t in
+ let new_b = alpha_rt new_excluded b in
+ RLambda(loc,Name new_id,new_t,new_b)
+ | RProd(loc,Anonymous,t,b) ->
+ let new_t = alpha_rt excluded t in
+ let new_b = alpha_rt excluded b in
+ RProd(loc,Anonymous,new_t,new_b)
+ | RLetIn(loc,Anonymous,t,b) ->
+ let new_t = alpha_rt excluded t in
+ let new_b = alpha_rt excluded b in
+ RLetIn(loc,Anonymous,new_t,new_b)
+ | RLambda(loc,Name id,t,b) ->
+ let new_id = Nameops.next_ident_away id excluded in
+ let t,b =
+ if new_id = id
+ then t,b
+ else
+ let replace = change_vars (Idmap.add id new_id Idmap.empty) in
+ (replace t,replace b)
+ in
+ let new_excluded = new_id::excluded in
+ let new_t = alpha_rt new_excluded t in
+ let new_b = alpha_rt new_excluded b in
+ RLambda(loc,Name new_id,new_t,new_b)
+ | RProd(loc,Name id,t,b) ->
+ let new_id = Nameops.next_ident_away id excluded in
+ let new_excluded = new_id::excluded in
+ let t,b =
+ if new_id = id
+ then t,b
+ else
+ let replace = change_vars (Idmap.add id new_id Idmap.empty) in
+ (replace t,replace b)
+ in
+ let new_t = alpha_rt new_excluded t in
+ let new_b = alpha_rt new_excluded b in
+ RProd(loc,Name new_id,new_t,new_b)
+ | RLetIn(loc,Name id,t,b) ->
+ let new_id = Nameops.next_ident_away id excluded in
+ let t,b =
+ if new_id = id
+ then t,b
+ else
+ let replace = change_vars (Idmap.add id new_id Idmap.empty) in
+ (replace t,replace b)
+ in
+ let new_excluded = new_id::excluded in
+ let new_t = alpha_rt new_excluded t in
+ let new_b = alpha_rt new_excluded b in
+ RLetIn(loc,Name new_id,new_t,new_b)
+
+
+ | RLetTuple(loc,nal,(na,rto),t,b) ->
+ let rev_new_nal,new_excluded,mapping =
+ List.fold_left
+ (fun (nal,excluded,mapping) na ->
+ match na with
+ | Anonymous -> (na::nal,excluded,mapping)
+ | Name id ->
+ let new_id = Nameops.next_ident_away id excluded in
+ if new_id = id
+ then
+ na::nal,id::excluded,mapping
+ else
+ (Name new_id)::nal,id::excluded,(Idmap.add id new_id mapping)
+ )
+ ([],excluded,Idmap.empty)
+ nal
+ in
+ let new_nal = List.rev rev_new_nal in
+ let new_rto,new_t,new_b =
+ if idmap_is_empty mapping
+ then rto,t,b
+ else let replace = change_vars mapping in
+ (option_app replace rto,replace t,replace b)
+ in
+ let new_t = alpha_rt new_excluded new_t in
+ let new_b = alpha_rt new_excluded new_b in
+ let new_rto = option_app (alpha_rt new_excluded) new_rto in
+ RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
+ | RCases(loc,infos,el,brl) ->
+ let new_el =
+ List.map (function (rt,i) -> alpha_rt excluded rt, i) el
+ in
+ RCases(loc,infos,new_el,List.map (alpha_br excluded) brl)
+ | RIf _ -> error "Not handled RIf"
+ | RRec _ -> error "Not handled RRec"
+ | RSort _ -> rt
+ | RHole _ -> rt
+ | RCast (loc,b,k,t) ->
+ RCast(loc,alpha_rt excluded b,k,alpha_rt excluded t)
+ | RDynamic _ -> error "Not handled RDynamic"
+ | RApp(loc,f,args) ->
+ RApp(loc,
+ alpha_rt excluded f,
+ List.map (alpha_rt excluded) args
+ )
+ in
+ if Tacinterp.get_debug () <> Tactic_debug.DebugOff && false
+ then
+ Pp.msgnl (str "debug: alpha_rt(" ++ str "[" ++
+ prlist_with_sep (fun _ -> str";") Ppconstr.pr_id excluded ++
+ str "]" ++ spc () ++ str "," ++ spc () ++
+ Printer.pr_rawconstr rt ++ spc () ++ str ")" ++ spc () ++ str "=" ++
+ spc () ++ Printer.pr_rawconstr new_rt
+ );
+ new_rt
+
+and alpha_br excluded (loc,ids,patl,res) =
+ let new_patl,new_excluded,mapping = alpha_patl excluded patl in
+ let new_ids = List.fold_right raw_get_pattern_id new_patl [] in
+ let new_excluded = new_ids@excluded in
+ let renamed_res = change_vars mapping res in
+ let new_res = alpha_rt new_excluded renamed_res in
+ (loc,new_ids,new_patl,new_res)
+
+
+
+
+
+
+
+(*
+ [is_free_in id rt] checks if [id] is a free variable in [rt]
+*)
+let is_free_in id =
+ let rec is_free_in = function
+ | RRef _ -> false
+ | RVar(_,id') -> id_ord id' id == 0
+ | REvar _ -> false
+ | RPatVar _ -> false
+ | RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
+ | RLambda(_,n,t,b) | RProd(_,n,t,b) | RLetIn(_,n,t,b) ->
+ let check_in_b =
+ match n with
+ | Name id' -> id_ord id' id <> 0
+ | _ -> true
+ in
+ is_free_in t || (check_in_b && is_free_in b)
+ | RCases(_,_,el,brl) ->
+ (List.exists (fun (e,_) -> is_free_in e) el) ||
+ List.exists is_free_in_br brl
+
+ | RLetTuple(_,nal,_,b,t) ->
+ let check_in_nal =
+ not (List.exists (function Name id' -> id'= id | _ -> false) nal)
+ in
+ is_free_in t || (check_in_nal && is_free_in b)
+
+ | RIf(_,cond,_,br1,br2) ->
+ is_free_in cond || is_free_in br1 || is_free_in br2
+ | RRec _ -> raise (UserError("",str "Not handled RRec"))
+ | RSort _ -> false
+ | RHole _ -> false
+ | RCast (_,b,_,t) -> is_free_in b || is_free_in t
+ | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
+ and is_free_in_br (_,ids,_,rt) =
+ (not (List.mem id ids)) && is_free_in rt
+ in
+ is_free_in
+
+
+
+let rec pattern_to_term = function
+ | PatVar(loc,Anonymous) -> assert false
+ | PatVar(loc,Name id) ->
+ mkRVar id
+ | PatCstr(loc,constr,patternl,_) ->
+ let cst_narg =
+ Inductiveops.mis_constructor_nargs_env
+ (Global.env ())
+ constr
+ in
+ let implicit_args =
+ Array.to_list
+ (Array.init
+ (cst_narg - List.length patternl)
+ (fun _ -> mkRHole ())
+ )
+ in
+ let patl_as_term =
+ List.map pattern_to_term patternl
+ in
+ mkRApp(mkRRef(Libnames.ConstructRef constr),
+ implicit_args@patl_as_term
+ )
+
+let replace_var_by_term x_id term =
+ let rec replace_var_by_pattern rt =
+ match rt with
+ | RRef _ -> rt
+ | RVar(_,id) when id_ord id x_id == 0 -> term
+ | RVar _ -> rt
+ | REvar _ -> rt
+ | RPatVar _ -> rt
+ | RApp(loc,rt',rtl) ->
+ RApp(loc,
+ replace_var_by_pattern rt',
+ List.map replace_var_by_pattern rtl
+ )
+ | RLambda(_,Name id,_,_) when id_ord id x_id == 0 -> rt
+ | RLambda(loc,name,t,b) ->
+ RLambda(loc,
+ name,
+ replace_var_by_pattern t,
+ replace_var_by_pattern b
+ )
+ | RProd(_,Name id,_,_) when id_ord id x_id == 0 -> rt
+ | RProd(loc,name,t,b) ->
+ RProd(loc,
+ name,
+ replace_var_by_pattern t,
+ replace_var_by_pattern b
+ )
+ | RLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt
+ | RLetIn(loc,name,def,b) ->
+ RLetIn(loc,
+ name,
+ replace_var_by_pattern def,
+ replace_var_by_pattern b
+ )
+ | RLetTuple(_,nal,_,_,_)
+ when List.exists (function Name id -> id = x_id | _ -> false) nal ->
+ rt
+ | RLetTuple(loc,nal,(na,rto),def,b) ->
+ RLetTuple(loc,
+ nal,
+ (na,option_app replace_var_by_pattern rto),
+ replace_var_by_pattern def,
+ replace_var_by_pattern b
+ )
+ | RCases(loc,infos,el,brl) ->
+ RCases(loc,
+ infos,
+ List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el,
+ List.map replace_var_by_pattern_br brl
+ )
+ | RIf _ -> raise (UserError("",str "Not handled RIf"))
+ | RRec _ -> raise (UserError("",str "Not handled RRec"))
+ | RSort _ -> rt
+ | RHole _ -> rt
+ | RCast(loc,b,k,t) ->
+ RCast(loc,replace_var_by_pattern b,k,replace_var_by_pattern t)
+ | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
+ and replace_var_by_pattern_br ((loc,idl,patl,res) as br) =
+ if List.exists (fun id -> id_ord id x_id == 0) idl
+ then br
+ else (loc,idl,patl,replace_var_by_pattern res)
+ in
+ replace_var_by_pattern
+
+
+
+
+(* checking unifiability of patterns *)
+exception NotUnifiable
+
+let rec are_unifiable_aux = function
+ | [] -> ()
+ | eq::eqs ->
+ match eq with
+ | PatVar _,_ | _,PatVar _ -> are_unifiable_aux eqs
+ | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) ->
+ if constructor2 <> constructor1
+ then raise NotUnifiable
+ else
+ let eqs' =
+ try ((List.combine cpl1 cpl2)@eqs)
+ with _ -> anomaly "are_unifiable_aux"
+ in
+ are_unifiable_aux eqs'
+
+let are_unifiable pat1 pat2 =
+ try
+ are_unifiable_aux [pat1,pat2];
+ true
+ with NotUnifiable -> false
+
+
+let rec eq_cases_pattern_aux = function
+ | [] -> ()
+ | eq::eqs ->
+ match eq with
+ | PatVar _,PatVar _ -> eq_cases_pattern_aux eqs
+ | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) ->
+ if constructor2 <> constructor1
+ then raise NotUnifiable
+ else
+ let eqs' =
+ try ((List.combine cpl1 cpl2)@eqs)
+ with _ -> anomaly "eq_cases_pattern_aux"
+ in
+ eq_cases_pattern_aux eqs'
+ | _ -> raise NotUnifiable
+
+let eq_cases_pattern pat1 pat2 =
+ try
+ eq_cases_pattern_aux [pat1,pat2];
+ true
+ with NotUnifiable -> false
+
+
+
+let ids_of_pat =
+ let rec ids_of_pat ids = function
+ | PatVar(_,Anonymous) -> ids
+ | PatVar(_,Name id) -> Idset.add id ids
+ | PatCstr(_,_,patl,_) -> List.fold_left ids_of_pat ids patl
+ in
+ ids_of_pat Idset.empty
+
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
new file mode 100644
index 00000000..92df0ec6
--- /dev/null
+++ b/contrib/funind/rawtermops.mli
@@ -0,0 +1,111 @@
+open Rawterm
+
+(* Ocaml 3.06 Map.S does not handle is_empty *)
+val idmap_is_empty : 'a Names.Idmap.t -> bool
+
+
+(* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *)
+val get_pattern_id : cases_pattern -> Names.identifier list
+
+(* [pattern_to_term pat] returns a rawconstr corresponding to [pat].
+ [pat] must not contain occurences of anonymous pattern
+*)
+val pattern_to_term : cases_pattern -> rawconstr
+
+(*
+ Some basic functions to rebuild rawconstr
+ In each of them the location is Util.dummy_loc
+*)
+val mkRRef : Libnames.global_reference -> rawconstr
+val mkRVar : Names.identifier -> rawconstr
+val mkRApp : rawconstr*(rawconstr list) -> rawconstr
+val mkRLambda : Names.name*rawconstr*rawconstr -> rawconstr
+val mkRProd : Names.name*rawconstr*rawconstr -> rawconstr
+val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr
+val mkRCases : rawconstr option *
+ (rawconstr * (Names.name * (Util.loc * Names.inductive * Names.name list) option)) list *
+ (Util.loc * Names.identifier list * cases_pattern list * rawconstr) list ->
+ rawconstr
+val mkRSort : rawsort -> rawconstr
+val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
+
+(*
+ Some basic functions to decompose rawconstrs
+ These are analogous to the ones constrs
+*)
+val raw_decompose_prod : rawconstr -> (Names.name*rawconstr) list * rawconstr
+val raw_compose_prod : rawconstr -> (Names.name*rawconstr) list -> rawconstr
+val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list)
+
+
+(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *)
+val raw_make_eq : rawconstr -> rawconstr -> rawconstr
+(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *)
+val raw_make_neq : rawconstr -> rawconstr -> rawconstr
+(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *)
+val raw_make_or : rawconstr -> rawconstr -> rawconstr
+
+(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding
+ to [P1 \/ ( .... \/ Pn)]
+*)
+val raw_make_or_list : rawconstr list -> rawconstr
+
+
+(* alpha_conversion functions *)
+
+
+
+(* Replace the var mapped in the rawconstr/context *)
+val change_vars : Names.identifier Names.Idmap.t -> rawconstr -> rawconstr
+
+
+
+(* [alpha_pat avoid pat] rename all the variables present in [pat] s.t.
+ the result does not share variables with [avoid]. This function create
+ a fresh variable for each occurence of the anonymous pattern.
+
+ Also returns a mapping from old variables to new ones and the concatenation of
+ [avoid] with the variables appearing in the result.
+*)
+ val alpha_pat :
+ Names.Idmap.key list ->
+ Rawterm.cases_pattern ->
+ Rawterm.cases_pattern * Names.Idmap.key list *
+ Names.identifier Names.Idmap.t
+
+(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt
+ conventions and does not share bound variables with avoid
+*)
+val alpha_rt : Names.identifier list -> rawconstr -> rawconstr
+
+(* same as alpha_rt but for case branches *)
+val alpha_br : Names.identifier list ->
+ Util.loc * Names.identifier list * Rawterm.cases_pattern list *
+ Rawterm.rawconstr ->
+ Util.loc * Names.identifier list * Rawterm.cases_pattern list *
+ Rawterm.rawconstr
+
+
+(* Reduction function *)
+val replace_var_by_term :
+ Names.identifier ->
+ Rawterm.rawconstr -> Rawterm.rawconstr -> Rawterm.rawconstr
+
+
+
+(*
+ [is_free_in id rt] checks if [id] is a free variable in [rt]
+*)
+val is_free_in : Names.identifier -> rawconstr -> bool
+
+
+val are_unifiable : cases_pattern -> cases_pattern -> bool
+val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
+
+
+
+(*
+ ids_of_pat : cases_pattern -> Idset.t
+ returns the set of variables appearing in a pattern
+*)
+val ids_of_pat : cases_pattern -> Names.Idset.t
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index 1500e1ae..c2410d55 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -46,6 +46,8 @@ let smap_to_list m = Smap.fold (fun c cb l -> (c,cb)::l) m []
let merge_smap m1 m2 = Smap.fold (fun c cb m -> Smap.add c cb m) m1 m2
let rec listsuf i l = if i<=0 then l else listsuf (i-1) (List.tl l)
let rec listpref i l = if i<=0 then [] else List.hd l :: listpref (i-1) (List.tl l)
+let rec split3 l =
+ List.fold_right (fun (e1,e2,e3) (a,b,c) -> (e1::a),(e2::b),(e3::c)) l ([],[],[])
let mkthesort = mkProp (* would like to put Type here, but with which index? *)
@@ -56,9 +58,7 @@ let equality_hyp_string = "_eg_"
(* bug de refine: on doit ssavoir sur quelle hypothese on se trouve. valeur
initiale au debut de l'appel a la fonction proofPrinc: 1. *)
let nthhyp = ref 1
- (*debugging*)
- (* let rewrules = ref [] *)
- (*debugging*)
+
let debug i = prstr ("DEBUG "^ string_of_int i ^"\n")
let pr2constr = (fun c1 c2 -> prconstr c1; prstr " <---> "; prconstr c2)
(* Operations on names *)
@@ -71,21 +71,6 @@ let string_of_name nme = string_of_id (id_of_name nme)
(* Interpretation of constr's *)
let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
-let rec collect_cases l =
- match l with
- | [||] -> [||],[],[],[||],[||],[]
- | arr ->
- let (a,c,d,f,e,g)= arr.(0) in
- let aa,lc,ld,_,_,_ =
- collect_cases (Array.sub arr 1 ((Array.length arr)-1)) in
- Array.append [|a|] aa , (c@lc) , (d@ld) , f , e, g
-
-let rec collect_pred l =
- match l with
- | [] -> [],[],[]
- | (e1,e2,e3)::l' -> let a,b,c = collect_pred l' in (e1::a),(e2::b),(e3::c)
-
-
(*s specific manipulations on constr *)
let lift1_leqs leq=
List.map
@@ -194,29 +179,25 @@ let applFull c typofc =
let res = mkAppRel c ltyp (List.length ltyp) in
res
-
+(* Take two terms with same structure and return a map of deBruijn from the
+ first to the second. Only DeBruijn should be different between the two
+ terms. *)
let rec build_rel_map typ type_of_b =
match (kind_of_term typ), (kind_of_term type_of_b) with
Evar _ , Evar _ -> Smap.empty
- | Rel i, Rel j -> if i=j then Smap.empty
- else Smap.add typ type_of_b Smap.empty
+ | Const c1, Const c2 when c1=c2 -> Smap.empty
+ | Ind c1, Ind c2 when c1=c2 -> Smap.empty
+ | Rel i, Rel j when i=j -> Smap.empty
+ | Rel i, Rel j -> Smap.add typ type_of_b Smap.empty
| Prod (name,c1,c2), Prod (nameb,c1b,c2b) ->
let map1 = build_rel_map c1 c1b in
let map2 = build_rel_map (pop c2) (pop c2b) in
merge_smap map1 map2
- | App (f,args), App (fb,argsb) ->
- (try build_rel_map_list (Array.to_list args) (Array.to_list argsb)
- with Invalid_argument _ ->
- failwith ("Could not generate case annotation. "^
- "Two application with different length"))
- | Const c1, Const c2 -> if c1=c2 then Smap.empty
- else failwith ("Could not generate case annotation. "^
- "Two different constants in a case annotation.")
- | Ind c1, Ind c2 -> if c1=c2 then Smap.empty
- else failwith ("Could not generate case annotation. "^
- "Two different constants in a case annotation.")
+ | App (f,args), App (fb,argsb) when Array.length args = Array.length argsb ->
+ build_rel_map_list (Array.to_list args) (Array.to_list argsb)
| _,_ -> failwith ("Could not generate case annotation. "^
"Incompatibility between annotation and actual type")
+
and build_rel_map_list ltyp ltype_of_b =
List.fold_left2 (fun a b c -> merge_smap a (build_rel_map b c))
Smap.empty ltyp ltype_of_b
@@ -224,299 +205,235 @@ and build_rel_map_list ltyp ltype_of_b =
(*s Use (and proof) of the principle *)
-(*
- \begin {itemize}
- \item [concl] ([constr]): conclusions, cad (xi:ti)gl, ou gl est le but a
- prouver, et xi:ti correspondent aux arguments donnés à la tactique. On
- enlève un produit à chaque fois qu'on rencontre un binder, sans lift ou pop.
- Initialement: une seule conclusion, puis specifique a chaque branche.
- \item[absconcl] ([constr array]): les conclusions (un predicat pour chaque
- fixp. mutuel) patternisées pour pouvoir être appliquées.
- \item [mimick] ([constr]): le terme qu'on imite. On plonge dedans au fur et
- à mesure, sans lift ni pop.
- \item [nmefonc] ([constr array]): la constante correspondant à la fonction
- appelée, permet de remplacer les appels recursifs par des appels à la
- constante correspondante (non pertinent (et inutile) si on permet l'appel de
- la tactique sur une terme donné directement (au lieu d'une constante comme
- pour l'instant)).
- \item [fonc] ([int*int]) : bornes des indices des variable correspondant aux
- appels récursifs (plusieurs car fixp. mutuels), utile pour reconnaître les
- appels récursifs (ATTENTION: initialement vide, reste vide tant qu'on n'est
- pas dans un fix).
- \end{itemize}
-*)
+(* This is the type of the argument of [proofPrinc] *)
type mimickinfo =
{
- concl: constr;
- absconcl: constr array;
- mimick: constr;
- env: env;
- sigma: Evd.evar_map;
- nmefonc: constr array;
- fonc: int * int;
+ concl: constr; (* conclusion voulue, cad (xi:ti)gl, ou gl est le but a
+ prouver, et xi:ti correspondent aux arguments donnés à
+ la tactique. On enlèvera un produit à chaque fois
+ qu'on rencontrera un binder, sans lift ou pop.
+ Initialement: une seule conclusion, puis specifique à
+ chaque branche. *)
+ absconcl: constr array; (* conclusions patternisées pour pouvoir être
+ appliquées = un predicat pour chaque fixpt
+ mutuel. *)
+ mimick: constr; (* le terme qu'on imite. On plongera dedans au fur et
+ à mesure, sans lift ni pop. *)
+ env: env; (* The global typing environment, we will add thing in it when
+ going inside the term (push_rel, push_rec_types) *)
+ sigma: Evd.evar_map;
+ nmefonc: constr array; (* la constante correspondant à la fonction
+ appelée, permet de remplacer les appels
+ recursifs par des appels à la constante
+ correspondante (non pertinent (et inutile) si
+ on permet l'appel de la tactique sur une terme
+ donné directement (au lieu d'une constante
+ comme pour l'instant)). *)
+ fonc: int * int; (* bornes des indices des variable correspondant aux
+ appels récursifs (plusieurs car fixp. mutuels),
+ utile pour reconnaître les appels récursifs
+ (ATTENTION: initialement vide, reste vide tant qu'on
+ n'est pas dans un fix). *)
doeqs: bool; (* this reference is to toggle building of equalities during
the building of the principle (default is true) *)
- fix: bool (* did I already went through a fix or case constr? lambdas
+ fix: bool; (* did I already went through a fix or case constr? lambdas
found before a case or a fix are treated as parameters of
the induction principle *)
+ lst_vars: (constr*(name*constr)) list ; (* Variables rencontrées jusque là *)
+ lst_eqs: (Term.constr * (Term.constr * Term.constr * Term.constr)) list ;
+ (* liste d'équations engendrées au cours du
+ parcours, cette liste grandit à chaque
+ case, et il faut lifter le tout à chaque
+ binder *)
+ lst_recs: constr list ; (* appels récursifs rencontrés jusque là *)
}
-(*
- \begin{itemize}
- \item [lst_vars] ([(constr*(name*constr)) list]): liste des variables
- rencontrées jusqu'à maintenant.
- \item [lst_eqs] ([constr list]): liste d'équations engendrées au cours du
- parcours, cette liste grandit à chaque case, et il faut lifter le tout à
- chaque binder.
- \item [lst_recs] ([constr list]): listes des appels récursifs rencontrés
- jusque là.
- \end{itemize}
-
- Cette fonction rends un nuplet de la forme:
-
- [t,
- [(ev1,tev1);(ev2,tev2)..],
- [(i1,j1,k1);(i2,j2,k2)..],
- [|c1;c2..|],
- [|typ1;typ2..|],
- [(param,tparam)..]]
-
- *)
-
-(* This could be the return type of [proofPrinc], but not yet *)
-type funind =
+(* This is the return type of [proofPrinc] *)
+type 'a funind = (* 'A = CONTR OU CONSTR ARRAY *)
{
- princ:constr;
- evarlist: (constr*Term.types) list;
- hypnum: (int*int*int) list;
- mutfixmetas: constr array ;
- conclarray: types array;
- params:(constr*name*constr) list
+
+ princ:'a; (* le (ou les) principe(s) demandé(s), il contient des meta
+ variables représentant soit des trous à prouver plus tard,
+ soit les conclusions à compléter avant de rendre le terme
+ (suivant qu'on utilise le principe pour faire refine ou
+ functional scheme). Il y plusieurs conclusions si plusieurs
+ fonction mutuellement récursives) voir la suite. *)
+ evarlist: (constr*Term.types) list; (* [(ev1,tev1);(ev2,tev2)...]]
+ l'ensemble des meta variables
+ correspondant à des trous. [evi]
+ est la meta variable, [tevi] est
+ son type. *)
+ hypnum: (int*int*int) list; (* [[(in,jn,kn)...]] sont les nombres
+ respectivement de variables, d'équations,
+ et d'hypothèses de récurrence pour le but
+ n. Permet de faire le bon nombre d'intros
+ et des rewrite au bons endroits dans la
+ suite. *)
+ mutfixmetas: constr array ; (* un tableau de meta variables correspondant
+ à chacun des prédicats mutuellement
+ récursifs construits. *)
+ conclarray: types array; (* un tableau contenant les conclusions
+ respectives de chacun des prédicats
+ mutuellement récursifs. Permet de finir la
+ construction du principe. *)
+ params:(constr*name*constr) list; (* [[(metavar,param,tparam)..]] la
+ liste des paramètres (les lambdas
+ au-dessus du fix) du fixpoint si
+ fixpoint il y a, le paramètre est
+ une meta var, dont on stocke le nom
+ et le type. TODO: utiliser la
+ structure adequat? *)
}
-(*
- où:
- \begin{itemize}
- \item[t] est le principe demandé, il contient des meta variables
- représentant soit des trous à prouver plus tard, soit les conclusions à
- compléter avant de rendre le terme (suivant qu'on utilise le principe pour
- faire refine ou functional scheme). Il y plusieurs conclusions si plusieurs
- fonction mutuellement récursives) voir la suite.
+let empty_funind_constr =
+ {
+ princ = mkProp;
+ evarlist = [];
+ hypnum = [];
+ mutfixmetas = [||];
+ conclarray = [||];
+ params = []
+ }
- \item[[(ev1,tev1);(ev2,tev2)...]] est l'ensemble des méta variables
- correspondant à des trous. [evi] est la meta variable, [tevi] est son type.
+let empty_funind_array =
+ { empty_funind_constr with
+ princ = [||];
+ }
- \item[(in,jn,kn)] sont les nombres respectivement de variables, d'équations,
- et d'hypothèses de récurrence pour le but n. Permet de faire le bon nombre
- d'intros et des rewrite au bons endroits dans la suite.
+(* Replace the calls to the function (recursive calls) by calls to the
+ corresponding constant *)
+let replace_reccalls mi b =
+ let d,f = mi.fonc in
+ let res = ref b in
+ let _ = for i = d to f do
+ res := substitterm 0 (mkRel i) mi.nmefonc.(f-i) !res done in
+ !res
+
- \item[[|c1;c2...|]] est un tableau de meta variables correspondant à chacun
- des prédicats mutuellement récursifs construits.
- \item[[|typ1;typ2...|]] est un tableau contenant les conclusions respectives
- de chacun des prédicats mutuellement récursifs. Permet de finir la
- construction du principe.
+(* collects all information of match branches stored in [l] *)
+let rec collect_cases l =
+ match l with
+ | [||] -> empty_funind_array
+ | arr ->
+ let x = arr.(0) in
+ let resrec = collect_cases (Array.sub arr 1 (Array.length arr - 1)) in
+ { x with
+ princ= Array.append [|x.princ|] resrec.princ;
+ evarlist = x.evarlist@resrec.evarlist;
+ hypnum = x.hypnum@resrec.hypnum;
+ }
+
+let collect_pred l =
+ let l1,l2,l3 = split3 l in
+ Array.of_list l1 , Array.of_list l2 , Array.of_list l3
+
+
+(* [build_pred n tarr] builds the right predicates for each element of [tarr]
+ (of type: [type array] of size [n]). Return the list of triples:
+ (?i ,
+ fun (x1:t1) ... (xn:tn) => (?i x1...xn) ,
+ forall (x1:t1) ... (xn:tn), (?i x1...xn)),
+ where ti's are deduced from elements of tarr, which are of the form:
+ t1 -> t2 -> ... -> tn -> <nevermind>. *)
+let rec build_pred n tarr =
+ if n >= Array.length tarr (* iarr *) then []
+ else
+ let ftyp = Array.get tarr n in
+ let gl = mknewmeta() in
+ let gl_app = applFull gl ftyp in
+ let pis = prod_change_concl ftyp gl_app in
+ let gl_abstr = lam_change_concl ftyp gl_app in
+ (gl,gl_abstr,pis):: build_pred (n+1) tarr
- \item[[(param,tparam)..]] est la liste des paramètres (les lambda au-dessus
- du fix) du fixpoint si fixpoint il y a.
- \end{itemize}
-*)
let heq_prefix = "H_eq_"
type kind_of_hyp = Var | Eq (*| Rec*)
-let rec proofPrinc mi lst_vars lst_eqs lst_recs:
- constr * (constr*Term.types) list * (int*int*int) list
- * constr array * types array * (constr*name*constr) list =
+(* the main function, build the principle by exploring the term and reproduce
+ the same structure. *)
+let rec proofPrinc mi: constr funind =
match kind_of_term mi.mimick with
(* Fixpoint: we reproduce the Fix, fonc becomes (1,nbofmutf) to point on
the name of recursive calls *)
| Fix((iarr,i),(narr,tarr,carr)) ->
-
- (* We construct the right predicates for each mutual fixpt *)
- let rec build_pred n =
- if n >= Array.length iarr then []
- else
- let ftyp = Array.get tarr n in
- let gl = mknewmeta() in
- let gl_app = applFull gl ftyp in
- let pis = prod_change_concl ftyp gl_app in
- let gl_abstr = lam_change_concl ftyp gl_app in
- (gl,gl_abstr,pis):: build_pred (n+1) in
-
- let evarl,predl,pisl = collect_pred (build_pred 0) in
- let newabsconcl = Array.of_list predl in
- let evararr = Array.of_list evarl in
- let pisarr = Array.of_list pisl in
+ (* We construct the right predicates for each mutual fixpt *)
+ let evararr,newabsconcl,pisarr = collect_pred (build_pred 0 tarr) in
let newenv = push_rec_types (narr,tarr,carr) mi.env in
-
- let rec collect_fix n =
- if n >= Array.length iarr then [],[],[],[]
- else
- let nme = Array.get narr n in
- let c = Array.get carr n in
- (* rappelle sur le sous-terme, on ajoute un niveau de
- profondeur (lift) parce que Fix est un binder. *)
- let newmi = {mi with concl=(pisarr.(n)); absconcl=newabsconcl;
- mimick=c; fonc=(1,((Array.length iarr)));env=newenv;fix=true} in
- let appel_rec,levar,lposeq,_,evarrarr,parms =
- proofPrinc newmi (lift1_lvars lst_vars)
- (lift1_leqs lst_eqs) (lift1L lst_recs) in
- let lnme,lappel_rec,llevar,llposeq = collect_fix (n+1) in
- (nme::lnme),(appel_rec::lappel_rec),(levar@llevar), (lposeq@llposeq) in
-
- let lnme,lappel_rec,llevar,llposeq =collect_fix 0 in
- let lnme' = List.map (fun nme -> newname_append nme "_ind") lnme in
- let anme = Array.of_list lnme' in
- let aappel_rec = Array.of_list lappel_rec in
- (* llevar are put outside the fix, so one level of rel must be removed *)
- mkFix((iarr,i),(anme, pisarr,aappel_rec))
- , (pop1_levar llevar) , llposeq,evararr,pisarr,[]
-
+ let anme',aappel_rec,llevar,llposeq =
+ collect_fix mi 0 iarr narr carr pisarr newabsconcl newenv in
+ let anme = Array.map (fun nme -> newname_append nme "_ind") anme' in
+ {
+ princ = mkFix((iarr,i),(anme, pisarr,aappel_rec));
+ evarlist= pop1_levar llevar; (* llevar are put outside the fix, so we pop 1 *)
+ hypnum = llposeq;
+ mutfixmetas = evararr;
+ conclarray = pisarr;
+ params = []
+ }
(* <pcase> Cases b of arrPt end.*)
- | Case(cinfo, pcase, b, arrPt) ->
-
+ | Case (cinfo, pcase, b, arrPt) ->
let prod_pcase,_ = decompose_lam pcase in
- let nmeb,lastprod_pcase = List.hd prod_pcase in
- let b'= apply_leqtrpl_t b lst_eqs in
+ let nmeb,_ = List.hd prod_pcase in
+ let newb'= apply_leqtrpl_t b mi.lst_eqs in
let type_of_b = Typing.type_of mi.env mi.sigma b in
- let new_lst_recs = lst_recs @ hdMatchSub_cpl b mi.fonc in
- (* Replace the calls to the function (recursive calls) by calls to the
- corresponding constant: *)
- let d,f = mi.fonc in
- let res = ref b' in
- let _ = for i = d to f do
- res := substitterm 0 (mkRel i) mi.nmefonc.(f-i) !res done in
- let newb = !res in
-
- (* [fold_proof t l n] rend le resultat de l'appel recursif sur les
- elements de la liste l (correpsondant a arrPt), appele avec les bons
- arguments: [concl] devient [(DUMMY1:t1;...;DUMMY:tn)concl'], ou [n]
- est le nombre d'arguments du constructeur considéré (FIX: Hormis les
- parametres!!), et [concl'] est concl ou l'on a réécrit [b] en ($c_n$
- [rel1]...).*)
-
- let rec fold_proof nth_construct eltPt' =
- (* mise a jour de concl pour l'interieur du case, concl'= concl[b <- C x3
- x2 x1... ], sans quoi les annotations ne sont plus coherentes *)
- let cstr_appl,nargs = nth_dep_constructor type_of_b nth_construct in
- let concl'' =
- substitterm 0 (lift nargs b) cstr_appl (lift nargs mi.concl) in
- let neweq = mkEq type_of_b newb (popn nargs cstr_appl) in
- let concl_dummy = add_n_dummy_prod concl'' nargs in
- let lsteqs_rew = apply_eq_leqtrpl lst_eqs neweq in
- let new_lsteqs =
- (mkRel (0-nargs),(type_of_b,newb, popn nargs cstr_appl))::lsteqs_rew in
- let a',a'' = decompose_lam_n nargs eltPt' in
- let newa'' =
- if mi.doeqs
- then mkLambda (name_of_string heq_prefix,lift nargs neweq,lift 1 a'')
- else a'' in
- let newmimick = lamn nargs a' newa'' in
- let b',b'' = decompose_prod_n nargs concl_dummy in
- let newb'' =
- if mi.doeqs
- then mkProd (name_of_string heq_prefix,lift nargs neweq,lift 1 b'')
- else b'' in
- let newconcl = prodn nargs b' newb'' in
- let newmi = {mi with mimick=newmimick; concl=newconcl; fix=true} in
- let a,b,c,d,e,p = proofPrinc newmi lst_vars new_lsteqs new_lst_recs in
- a,b,c,d,e,p
- in
-
- let arrPt_proof,levar,lposeq,evararr,absc,_ =
- collect_cases (Array.mapi fold_proof arrPt) in
- let prod_pcase,concl_pcase = decompose_lam pcase in
- let nme,typ = List.hd prod_pcase in
- let suppllam_pcase = List.tl prod_pcase in
- (* je remplace b par rel1 (apres avoir lifte un coup) dans la
- future annotation du futur case: ensuite je mettrai un lambda devant *)
- let typesofeqs' = eqs_of_beqs_named equality_hyp_string lst_eqs in
- (* let typesofeqs = prod_it_lift typesofeqs' mi.concl in *)
- let typesofeqs = mi.concl in
- let typeof_case'' =
- substitterm 0 (lift 1 b) (mkRel 1) (lift 1 typesofeqs) in
-
- (* C'est un peu compliqué ici: en cas de type inductif vraiment dépendant
- le piquant du case [pcase] contient des lambdas supplémentaires en tête
- je les ai dans la variable [suppllam_pcase]. Le problème est que la
- conclusion du piquant doit faire référence à ces variables plutôt qu'à
- celle de l'exterieur. Ce qui suit permet de changer les reference de
- newpacse' pour pointer vers les lambda du piquant. On procède comme
- suit: on repère les rels qui pointent à l'interieur du piquant dans la
- fonction imitée, pour ça on parcourt le dernier lambda du piquant (qui
- contient le type de l'argument du case), et on remplace les rels
- correspondant dans la preuve construite. *)
-
- (* typ vient du piquant, type_of_b vient du typage de b.*)
-
- let rel_smap =
- if List.length suppllam_pcase=0 then Smap.empty else
- build_rel_map (lift (List.length suppllam_pcase) type_of_b) typ in
- let rel_map = smap_to_list rel_smap in
- let rec substL l c =
- match l with
- [] -> c
- | ((e,e') ::l') -> substL l' (substitterm 0 e (lift 1 e') c) in
- let newpcase' = substL rel_map typeof_case'' in
- let neweq = mkEq (lift (List.length suppllam_pcase + 1) type_of_b)
- (lift (List.length suppllam_pcase + 1) newb) (mkRel 1) in
- let newpcase =
- if mi.doeqs then
- mkProd (name_of_string "eg", neweq, lift 1 newpcase') else newpcase'
- in
- (* construction du dernier lambda du piquant. *)
- let typeof_case' = mkLambda (newname_append nme "_ind" ,typ, newpcase) in
- (* ajout des lambdas supplémentaires (type dépendant) du piquant. *)
- let typeof_case =
- lamn (List.length suppllam_pcase) suppllam_pcase typeof_case' in
- let trm' = mkCase (cinfo,typeof_case,newb, arrPt_proof) in
- let trm =
- if mi.doeqs then mkApp (trm',[|(mkRefl type_of_b newb)|])
- else trm' in
- trm,levar,lposeq,evararr,absc,[] (* fix parms here (fix inside case)*)
-
+ (* Replace the recursive calls to the function by calls to the constant *)
+ let newb = replace_reccalls mi newb' in
+ let cases = collect_cases (Array.mapi (fold_proof mi b type_of_b newb) arrPt) in
+ (* the match (case) annotation must be transformed, see [build_pcase] below *)
+ let newpcase = build_pcase mi pcase b type_of_b newb in
+ let trm' = mkCase (cinfo,newpcase,newb, cases.princ) in
+ { cases with
+ princ = if mi.doeqs then mkApp (trm',[|(mkRefl type_of_b newb)|]) else trm';
+ params = [] (* FIX: fix parms here (fixpt inside a match)*)
+ }
+
+
| Lambda(nme, typ, cstr) ->
let _, _, cconcl = destProd mi.concl in
let d,f=mi.fonc in
let newenv = push_rel (nme,None,typ) mi.env in
- let newmi = {mi with concl=cconcl; mimick=cstr; env=newenv;
- fonc=((if d > 0 then d+1 else 0),(if f > 0 then f+1 else 0))} in
let newlst_var = (* if this lambda is a param, then don't add it here *)
- if mi.fix then (mkRel 1,(nme,typ)) :: lift1_lvars lst_vars
- else (*(mkRel 1,(nme,typ)) :: *) lift1_lvars lst_vars in
- let rec_call,levar,lposeq,evararr,absc,parms =
- proofPrinc newmi newlst_var (lift1_leqs lst_eqs) (lift1L lst_recs) in
+ if mi.fix then (mkRel 1,(nme,typ)) :: lift1_lvars mi.lst_vars
+ else (*(mkRel 1,(nme,typ)) :: *) lift1_lvars mi.lst_vars in
+ let newmi = {mi with concl=cconcl; mimick=cstr; env=newenv;
+ fonc = (if d > 0 then d+1 else 0) , (if f > 0 then f+1 else 0);
+ lst_vars = newlst_var ; lst_eqs = lift1_leqs mi.lst_eqs;
+ lst_recs = lift1L mi.lst_recs} in
+ let resrec = proofPrinc newmi in
(* are we inside a fixpoint or a case? then this is a normal lambda *)
- if mi.fix then mkLambda (nme,typ,rec_call) , levar, lposeq,evararr,absc,[]
+ if mi.fix
+ then { resrec with princ = mkLambda (nme,typ,resrec.princ) ; params = [] }
else (* otherwise this is a parameter *)
let metav = mknewmeta() in
let substmeta t = popn 1 (substitterm 0 (mkRel 1) metav t) in
- let newrec_call = substmeta rec_call in
- let newlevar = List.map (fun (ev,tev) -> ev, substmeta tev) levar in
- let newabsc = Array.map substmeta absc in
- newrec_call,newlevar,lposeq,evararr,newabsc,((metav,nme, typ)::parms)
+ { resrec with
+ princ = substmeta resrec.princ;
+ evarlist = List.map (fun (ev,tev) -> ev, substmeta tev) resrec.evarlist;
+ conclarray = Array.map substmeta resrec.conclarray;
+ params = (metav,nme,typ) :: resrec.params
+ }
+
| LetIn(nme,cstr1, typ, cstr) ->
failwith ("I don't deal with let ins yet. "^
"Please expand them before applying this function.")
| u ->
- let varrels = List.rev (List.map fst lst_vars) in
- let varnames = List.map snd lst_vars in
+ let varrels = List.rev (List.map fst mi.lst_vars) in
+ let varnames = List.map snd mi.lst_vars in
let nb_vars = List.length varnames in
- let nb_eqs = List.length lst_eqs in
- let eqrels = List.map fst lst_eqs in
+ let nb_eqs = List.length mi.lst_eqs in
+ let eqrels = List.map fst mi.lst_eqs in
(* [terms_recs]: appel rec du fixpoint, On concatène les appels recs
trouvés dans les let in et les Cases avec ceux trouves dans u (ie
mi.mimick). *)
(* TODO: il faudra gérer plusieurs pt fixes imbriqués ? *)
- let terms_recs = lst_recs @ hdMatchSub_cpl mi.mimick mi.fonc in
-
+ let terms_recs = mi.lst_recs @ hdMatchSub_cpl mi.mimick mi.fonc in
(*c construction du terme: application successive des variables, des
egalites et des appels rec, a la variable existentielle correspondant a
l'hypothese de recurrence en cours. *)
@@ -527,18 +444,110 @@ let rec proofPrinc mi lst_vars lst_eqs lst_recs:
let appsrecpred = exchange_reli_arrayi_L mi.absconcl mi.fonc terms_recs in
let typeofhole'' = prod_it_anonym_lift mi.concl appsrecpred in
let typeofhole = prodn nb_vars varnames typeofhole'' in
-
(* Un bug de refine m'oblige à mettre ici un H (meta variable à ce point,
mais remplacé par H avant le refine) au lieu d'un '?', je mettrai les
'?' à la fin comme ça [(([H1,H2,H3...] ...) ? ? ?)] *)
-
let newmeta = mknewmeta() in
let concl_with_var = applistc newmeta varrels in
let conclrecs = applistc concl_with_var terms_recs in
- conclrecs,[newmeta,typeofhole], [nb_vars,(List.length terms_recs)
- ,nb_eqs],[||],mi.absconcl,[]
-
+ { empty_funind_constr with
+ princ = conclrecs;
+ evarlist = [ newmeta , typeofhole ];
+ hypnum = [ nb_vars , List.length terms_recs , nb_eqs ];
+ conclarray = mi.absconcl;
+ }
+
+(* C'est un peu compliqué ici: en cas de type inductif vraiment dépendant
+ l'annotation de type du case [pcase] contient des lambdas supplémentaires
+ en tête. Je les récupère dans la variable [suppllam_pcase]. Le problème est
+ que la conclusion de l'annotation du nouveauacse doit faire référence à ces
+ variables plutôt qu'à celle de l'exterieur. Ce qui suit permet de changer
+ les reference de newpcase' pour pointer vers les lambda du piquant. On
+ procède comme suit: on repère les rels qui pointent à l'interieur de
+ l'annotation dans la fonction initiale et on les relie à celle du type
+ voulu pour le case, pour ça ([build_rel_map]) on parcourt en même temps le
+ dernier lambda du piquant ([typ]) (qui contient le type de l'argument du
+ case) et le type attendu pour le case ([type_of_b]) et on construit un
+ map. Ensuite on remplace les rels correspondant dans la preuve construite
+ en suivant le map. *)
+
+and build_pcase mi pcase b type_of_b newb =
+ let prod_pcase,_ = decompose_lam pcase in
+ let nme,typ = List.hd prod_pcase in
+ (* je remplace b par rel1 (apres avoir lifte un coup) dans la future
+ annotation du futur case: ensuite je mettrai un lambda devant *)
+ let typeof_case'' = substitterm 0 (lift 1 b) (mkRel 1) (lift 1 mi.concl) in
+ let suppllam_pcase = List.tl prod_pcase in
+ let suppllam_pcasel = List.length suppllam_pcase in
+ let rel_smap =
+ if suppllam_pcasel=0 then Smap.empty else (* FIX: is this test necessary ? *)
+ build_rel_map (lift suppllam_pcasel type_of_b) typ in
+ let newpcase''' =
+ Smap.fold (fun e e' acc -> substitterm 0 e (lift 1 e') acc)
+ rel_smap typeof_case'' in
+ let neweq = mkEq (lift (suppllam_pcasel + 1) type_of_b)
+ (lift (suppllam_pcasel + 1) newb) (mkRel 1) in
+ let newpcase'' =
+ if mi.doeqs
+ then mkProd (name_of_string "eg", neweq, lift 1 newpcase''')
+ else newpcase''' in
+ (* construction du dernier lambda du piquant. *)
+ let newpcase' = mkLambda (newname_append nme "_ind" ,typ, newpcase'') in
+ (* ajout des lambdas supplémentaires (type dépendant) du piquant. *)
+ lamn suppllam_pcasel suppllam_pcase newpcase'
+
+
+(* [fold_proof mi b typeofb newb l n] rend le resultat de l'appel recursif sur
+ cstr (correpsondant au ième elt de [arrPt] ci-dessus et donc au ième
+ constructeur de [typeofb]), appele avec les bons arguments: [mi.concl]
+ devient [(DUMMY1:t1;...;DUMMY:tn)concl'], ou [n] est le nombre d'arguments
+ du constructeur considéré, et [concl'] est [mi.concl] ou l'on a réécrit [b]
+ en ($c_n$ [rel1]...). *)
+and fold_proof mi b type_of_b newb i cstr =
+ let new_lst_recs = mi.lst_recs @ hdMatchSub_cpl b mi.fonc in
+ (* mise a jour de concl pour l'interieur du case, concl'= concl[b <- C x3
+ x2 x1... ], sans quoi les annotations ne sont plus coherentes *)
+ let cstr_appl,nargs = nth_dep_constructor type_of_b i in
+ let concl'' =
+ substitterm 0 (lift nargs b) cstr_appl (lift nargs mi.concl) in
+ let neweq = mkEq type_of_b newb (popn nargs cstr_appl) in
+ let concl_dummy = add_n_dummy_prod concl'' nargs in
+ let lsteqs_rew = apply_eq_leqtrpl mi.lst_eqs neweq in
+ let new_lsteqs = (mkRel (-nargs),(type_of_b,newb, popn nargs cstr_appl))::lsteqs_rew in
+ let a',a'' = decompose_lam_n nargs cstr in
+ let newa'' =
+ if mi.doeqs
+ then mkLambda (name_of_string heq_prefix,lift nargs neweq,lift 1 a'')
+ else a'' in
+ let newmimick = lamn nargs a' newa'' in
+ let b',b'' = decompose_prod_n nargs concl_dummy in
+ let newb'' =
+ if mi.doeqs
+ then mkProd (name_of_string heq_prefix,lift nargs neweq,lift 1 b'')
+ else b'' in
+ let newconcl = prodn nargs b' newb'' in
+ let newmi = {mi with mimick=newmimick; concl=newconcl; fix=true;
+ lst_eqs= new_lsteqs; lst_recs = new_lst_recs} in
+ proofPrinc newmi
+
+
+and collect_fix mi n iarr narr carr pisarr newabsconcl newenv =
+ if n >= Array.length iarr then [||],[||],[],[]
+ else
+ let nme = Array.get narr n in
+ let c = Array.get carr n in
+ (* rappelle sur le sous-terme, on ajoute un niveau de
+ profondeur (lift) parce que Fix est un binder. *)
+ let newmi = {mi with concl=(pisarr.(n)); absconcl=newabsconcl;
+ mimick=c; fonc=(1,((Array.length iarr)));env=newenv;fix=true;
+ lst_vars=lift1_lvars mi.lst_vars; lst_eqs=lift1_leqs mi.lst_eqs;
+ lst_recs= lift1L mi.lst_recs;} in
+ let resrec = proofPrinc newmi in
+ let lnme,lappel_rec,llevar,llposeq =
+ collect_fix mi (n+1) iarr narr carr pisarr newabsconcl newenv in
+ Array.append [|nme|] lnme , Array.append [|resrec.princ|] lappel_rec
+ , (resrec.evarlist@llevar) , (resrec.hypnum@llposeq)
let mkevarmap_aux ex = let x,y = ex in (mkevarmap_from_listex x),y
@@ -568,9 +577,10 @@ let interp_fonc_tacarg fonctac gl =
let invfun_proof fonc def_fonc gl_abstr pis env sigma =
let mi = {concl=pis; absconcl=gl_abstr; mimick=def_fonc; env=env;
- sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false} in
- let princ_proof,levar,lposeq,evararr,absc,parms = proofPrinc mi [] [] [] in
- princ_proof,levar,lposeq,evararr,absc,parms
+ sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false ;
+ lst_vars = []; lst_eqs = []; lst_recs = []} in
+ proofPrinc mi
+
(* Do intros [i] times, then do rewrite on all introduced hyps which are called
like [heq_prefix], FIX: have another filter than the name. *)
let rec iterintro i =
@@ -587,7 +597,7 @@ let rec iterintro i =
let sub =
try String.sub hypname 0 (String.length heq_prefix)
with _ -> "" (* different than [heq_prefix] *) in
- if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 "Cannot rewrite")
+ if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 (str "Cannot rewrite"))
)) gl)
@@ -647,7 +657,7 @@ let rec applistc_iota cstr lcstr env sigma =
| [] -> cstr,[]
| arg::lcstr' ->
let arghd =
- if isApp arg then let x,_ = destApplication arg in x else arg in
+ if isApp arg then let x,_ = destApp arg in x else arg in
if isConstruct arghd (* of the form [(C ...)]*)
then
applistc_iota (Tacred.nf env sigma (nf_beta (applistc cstr [arg])))
@@ -686,39 +696,38 @@ let invfun c l dorew gl =
let pis = add_pis (pf_concl gl) gl listargs' in
(* princ_proof builds the principle *)
let _ = resetmeta() in
- let princ_proof,levar, lposeq,evararr,_,parms =
- invfun_proof [|fonc|] def_fonc [||] pis (pf_env gl) (project gl) in
+ let pr = invfun_proof [|fonc|] def_fonc [||] pis (pf_env gl) (project gl) in
(* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *)
let gl_abstr' = add_lambdas (pf_concl gl) gl listargs' in
(* apply parameters immediately *)
let gl_abstr =
- applistc gl_abstr' (List.map (fun (x,y,z) -> x) (List.rev parms)) in
+ applistc gl_abstr' (List.map (fun (x,y,z) -> x) (List.rev pr.params)) in
(* we apply args of the fix now, the parameters will be applied later *)
let princ_proof_applied_args =
- applistc princ_proof (listsuf (List.length parms) listargs') in
+ applistc pr.princ (listsuf (List.length pr.params) listargs') in
(* parameters are still there so patternify must not take them -> lift *)
let princ_proof_applied_lift =
- lift (List.length levar) princ_proof_applied_args in
- let princ_applied_hyps'' = patternify (List.rev levar)
+ lift (List.length pr.evarlist) princ_proof_applied_args in
+ let princ_applied_hyps'' = patternify (List.rev pr.evarlist)
princ_proof_applied_lift (Name (id_of_string "Hyp")) in
(* if there was a fix, we will not add "Q" as in funscheme, so we make a pop,
TODO: find were we made the lift in proofPrinc instead and supress it here,
and add lift in funscheme. *)
let princ_applied_hyps' =
- if Array.length evararr > 0 then popn 1 princ_applied_hyps''
+ if Array.length pr.mutfixmetas > 0 then popn 1 princ_applied_hyps''
else princ_applied_hyps'' in
(* if there is was fix, we have to replace the meta representing the
predicate of the goal by the abstracted goal itself. *)
let princ_applied_hyps =
- if Array.length evararr > 0 then (* mutual Fixpoint not treated in the tactic *)
- (substit_red 0 (evararr.(0)) gl_abstr princ_applied_hyps')
+ if Array.length pr.mutfixmetas > 0 then(* mutual Fixpoint not treated in the tactic*)
+ (substit_red 0 (pr.mutfixmetas.(0)) gl_abstr princ_applied_hyps')
else princ_applied_hyps' (* No Fixpoint *) in
let _ = prNamedConstr "princ_applied_hyps" princ_applied_hyps in
(* Same thing inside levar *)
let newlevar' =
- if Array.length evararr > 0 then (* mutual Fixpoint not treated in the tactic *)
- List.map (fun (x,y) -> x,substit_red 0 (evararr.(0)) gl_abstr y) levar
- else levar
+ if Array.length pr.mutfixmetas > 0 then(* mutual Fixpoint not treated in the tactic*)
+ List.map (fun (x,y) -> x,substit_red 0 (pr.mutfixmetas.(0)) gl_abstr y) pr.evarlist
+ else pr.evarlist
in
(* replace params metavar by real args *)
let rec replace_parms lparms largs t =
@@ -726,19 +735,19 @@ let invfun c l dorew gl =
[], _ -> t
| ((p,_,_)::lp), (a::la) -> let t'= substitterm 0 p a t in replace_parms lp la t'
| _, _ -> error "problem with number of args." in
- let princ_proof_applied = replace_parms parms listargs' princ_applied_hyps in
+ let princ_proof_applied = replace_parms pr.params listargs' princ_applied_hyps in
let _ = prNamedLConstr "levar:" (List.map fst newlevar') in
let _ = prNamedLConstr "levar types:" (List.map snd newlevar') in
let _ = prNamedConstr "princ_proof_applied" princ_proof_applied in
(* replace also in levar *)
let newlevar =
- List.rev (List.map (fun (x,y) -> x, replace_parms parms listargs' y) newlevar') in
+ List.rev (List.map (fun (x,y) -> x, replace_parms pr.params listargs' y) newlevar') in
(*
(* replace params metavar by abstracted variables *)
- let princ_proof_params = npatternify (List.rev parms) princ_applied_hyps in
+ let princ_proof_params = npatternify (List.rev pr.params) princ_applied_hyps in
(* we apply now the real parameters *)
let princ_proof_applied =
- applistc princ_proof_params (listpref (List.length parms) listargs') in
+ applistc princ_proof_params (listpref (List.length pr.params) listargs') in
*)
let princ_applied_evars = apply_levars princ_proof_applied newlevar in
let open_princ_proof_applied = princ_applied_evars in
@@ -746,11 +755,11 @@ let invfun c l dorew gl =
let _ = prNamedLConstr "evars" (List.map snd (fst princ_applied_evars)) in
let listargs_ids = List.map destVar (List.filter isVar listargs') in
(* debug: impression du but*)
-(* let lgl = Evd.to_list (sig_sig gl) in *)
-(* let _ = prNamedLConstr "\ngl= " (List.map (fun x -> (snd x).evar_concl) lgl) in *)
-(* let _ = prstr "fin gl \n\n" in *)
+ let lgl = Evd.to_list (sig_sig gl) in
+ let _ = prNamedLConstr "\ngl= " (List.map (fun x -> (snd x).evar_concl) lgl) in
+ let _ = prstr "fin gl \n\n" in
invfun_basic (mkevarmap_aux open_princ_proof_applied) listargs_ids
- gl dorew lposeq
+ gl dorew pr.hypnum
(* function must be a constant, all arguments must be given. *)
let invfun_verif c l dorew gl =
@@ -763,8 +772,8 @@ let invfun_verif c l dorew gl =
else error "wrong number of arguments for the function"
-TACTIC EXTEND FunctionalInduction
- [ "Functional" "Induction" constr(c) ne_constr_list(l) ]
+TACTIC EXTEND functional_induction
+ [ "functional" "induction" constr(c) ne_constr_list(l) ]
-> [ invfun_verif c l true ]
END
@@ -780,13 +789,14 @@ let buildFunscheme fonc mutflist =
let pis = prod_change_concl ftyp gl_app in
(* Here we call the function invfun_proof, that effectively
builds the scheme *)
- let princ_proof,levar,_,evararr,absc,parms =
- invfun_proof mutflist def_fonc [||] pis (Global.env()) Evd.empty in
+(* let princ_proof,levar,_,evararr,absc,parms = *)
+ let _ = prstr "Recherche du principe... lancement de invfun_proof\n" in
+ let pr = invfun_proof mutflist def_fonc [||] pis (Global.env()) Evd.empty in
(* parameters are still there (unboud rel), and patternify must not take them
-> lift*)
- let princ_proof_lift = lift (List.length levar) princ_proof in
+ let princ_proof_lift = lift (List.length pr.evarlist) pr.princ in
let princ_proof_hyps =
- patternify (List.rev levar) princ_proof_lift (Name (id_of_string "Hyp")) in
+ patternify (List.rev pr.evarlist) princ_proof_lift (Name (id_of_string "Hyp")) in
let rec princ_replace_metas ev abs i t =
if i>= Array.length ev then t
else (* fix? *)
@@ -802,38 +812,46 @@ let buildFunscheme fonc mutflist =
mkLambda (Name (id_of_name nam) , typ,
substitterm 0 ev (mkRel 1) (lift 0 acc)))
t (List.rev params) in
- if Array.length evararr = 0 (* Is there a Fixpoint? *)
+ if Array.length pr.mutfixmetas = 0 (* Is there a Fixpoint? *)
then (* No Fixpoint *)
- princ_replace_params parms (mkLambda ((Name (id_of_string "Q")),
+ princ_replace_params pr.params (mkLambda ((Name (id_of_string "Q")),
prod_change_concl ftyp mkthesort,
(substitterm 0 gl (mkRel 1) princ_proof_hyps)))
else (* there is a fix -> add parameters + replace metas *)
- let princ_rpl = princ_replace_metas evararr absc 0 princ_proof_hyps in
- princ_replace_params parms princ_rpl
+ let princ_rpl =
+ princ_replace_metas pr.mutfixmetas pr.conclarray 0 princ_proof_hyps in
+ princ_replace_params pr.params princ_rpl
(* Declaration of the functional scheme. *)
let declareFunScheme f fname mutflist =
+ let _ = prstr "Recherche du perincipe...\n" in
+ let id_to_cstr id =
+ try constr_of_id (Global.env()) id
+ with
+ Not_found -> error (string_of_id id ^ " not found in the environment") in
let flist = if mutflist=[] then [f] else mutflist in
- let fcstrlist = Array.of_list (List.map constr_of flist) in
- let scheme = buildFunscheme (constr_of f) fcstrlist in
+ let fcstrlist = Array.of_list (List.map id_to_cstr flist) in
+ let idf = id_to_cstr f in
+ let scheme = buildFunscheme idf fcstrlist in
let _ = prstr "Principe:" in
let _ = prconstr scheme in
let ce = {
const_entry_body = scheme;
const_entry_type = None;
- const_entry_opaque = false } in
- let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition)) in
+ const_entry_opaque = false;
+ const_entry_boxed = true } in
+ let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition Scheme)) in
()
VERNAC COMMAND EXTEND FunctionalScheme
[ "Functional" "Scheme" ident(na) ":=" "Induction" "for"
- constr(c) "with" ne_constr_list(l) ]
+ ident(c) "with" ne_ident_list(l) ]
-> [ declareFunScheme c na l ]
-| [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" constr(c) ]
+| [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ]
-> [ declareFunScheme c na [] ]
END
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index a125b9a7..2877c19d 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -21,9 +21,9 @@ open Reductionops
(*s printing of constr -- debugging *)
(* comment this line to see debug msgs *)
-let msg x = () ;; let prterm c = str ""
+let msg x = () ;; let pr_lconstr c = str ""
(* uncomment this to see debugging *)
-let prconstr c = msg (str" " ++ prterm c ++ str"\n")
+let prconstr c = msg (str" " ++ pr_lconstr c ++ str"\n")
let prlistconstr lc = List.iter prconstr lc
let prstr s = msg(str s)
@@ -31,7 +31,7 @@ let prchr () = msg (str" (ret) \n")
let prNamedConstr s c =
begin
msg(str "");
- msg(str(s^"==>\n ") ++ prterm c ++ str "\n<==\n");
+ msg(str(s^"==>\n ") ++ pr_lconstr c ++ str "\n<==\n");
msg(str "");
end
@@ -74,7 +74,7 @@ let rec mkevarmap_from_listex lex =
let _ = prconstr typ in*)
let info ={
evar_concl = typ;
- evar_hyps = empty_named_context;
+ evar_hyps = empty_named_context_val;
evar_body = Evar_empty} in
Evd.add (mkevarmap_from_listex lex') ex info
@@ -126,7 +126,7 @@ let apply_leqtrpl_t t leq =
let apply_refl_term eq t =
- let _,arr = destApplication eq in
+ let _,arr = destApp eq in
let reli= (Array.get arr 1) in
let by_t= (Array.get arr 2) in
substitterm 0 reli by_t t
@@ -144,7 +144,7 @@ let apply_eq_leqtrpl leq eq =
let constr_head_match u t=
if isApp u
then
- let uhd,args= destApplication u in
+ let uhd,args= destApp u in
uhd=t
else false
@@ -187,7 +187,7 @@ let rec buildrefl_from_eqs eqs =
match eqs with
| [] -> []
| cstr::eqs' ->
- let eq,args = destApplication cstr in
+ let eq,args = destApp cstr in
(mkRefl (Array.get args 0) (Array.get args 2))
:: (buildrefl_from_eqs eqs')
@@ -237,7 +237,7 @@ let rec substit_red prof t by_t in_u =
(* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each
reli by tarr.(f-i). *)
let exchange_reli_arrayi tarr (d,f) t =
- let hd,args= destApplication t in
+ let hd,args= destApp t in
let i = destRel hd in
let res = whd_beta (mkApp (tarr.(f-i) ,args)) in
res
@@ -269,7 +269,7 @@ let def_of_const t =
(* nom d'une constante. Must be a constante. x*)
let name_of_const t =
match (kind_of_term t) with
- Const cst -> Names.string_of_label (Names.label cst)
+ Const cst -> Names.string_of_label (Names.con_label cst)
|_ -> assert false
;;
diff --git a/contrib/funind/tacinvutils.mli b/contrib/funind/tacinvutils.mli
index 2fc37b2c..64b21213 100644
--- a/contrib/funind/tacinvutils.mli
+++ b/contrib/funind/tacinvutils.mli
@@ -71,9 +71,10 @@ val expand_letins: constr -> constr
val def_of_const: constr -> constr
val name_of_const: constr -> string
+
(*i
- Local Variables:
- compile-command: "make -k tacinvutils.cmi"
- End:
+ *** Local Variables: ***
+ *** compile-command: "make -C ../.. contrib/funind/tacinvutils.cmi" ***
+ *** End: ***
i*)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 10:58:33 +0000