diff options
Diffstat (limited to 'contrib/funind')
-rw-r--r-- | contrib/funind/indfun.ml | 468 | ||||
-rw-r--r-- | contrib/funind/indfun_common.ml | 319 | ||||
-rw-r--r-- | contrib/funind/indfun_common.mli | 41 | ||||
-rw-r--r-- | contrib/funind/indfun_main.ml4 | 201 | ||||
-rw-r--r-- | contrib/funind/invfun.ml | 148 | ||||
-rw-r--r-- | contrib/funind/new_arg_principle.ml | 1770 | ||||
-rw-r--r-- | contrib/funind/new_arg_principle.mli | 34 | ||||
-rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 1012 | ||||
-rw-r--r-- | contrib/funind/rawterm_to_relation.mli | 16 | ||||
-rw-r--r-- | contrib/funind/rawtermops.ml | 525 | ||||
-rw-r--r-- | contrib/funind/rawtermops.mli | 111 | ||||
-rw-r--r-- | contrib/funind/tacinv.ml4 | 656 | ||||
-rw-r--r-- | contrib/funind/tacinvutils.ml | 18 | ||||
-rw-r--r-- | contrib/funind/tacinvutils.mli | 7 |
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*) |