From de0085539583f59dc7c4bf4e272e18711d565466 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 13 Jul 2006 14:28:31 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta.2 --- contrib/funind/indfun_main.ml4 | 302 +++++++++++++++++++++++++---------------- 1 file changed, 186 insertions(+), 116 deletions(-) (limited to 'contrib/funind/indfun_main.ml4') diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index 61f26d30..00b5f28c 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -14,6 +14,7 @@ open Indfun_common open Indfun open Genarg open Pcoq +open Tacticals let pr_binding prc = function | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) @@ -36,7 +37,8 @@ let pr_with_bindings prc prlc (c,bl) = let pr_fun_ind_using prc prlc _ opt_c = match opt_c with | None -> mt () - | Some c -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc c) + | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b)) + ARGUMENT EXTEND fun_ind_using TYPED AS constr_with_bindings_opt @@ -47,25 +49,9 @@ END TACTIC EXTEND newfuninv - [ "functional" "inversion" ident(hyp) ident(fname) fun_ind_using(princl)] -> + [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] -> [ - fun g -> - let fconst = const_of_id fname in - let princ = - match princl with - | None -> - let f_ind_id = - ( - Indrec.make_elimination_ident - fname - (Tacticals.elimination_sort_of_goal g) - ) - in - let princ = const_of_id f_ind_id in - princ - | Some princ -> destConst (fst princ) - in - Invfun.invfun hyp fconst princ g + Invfun.invfun hyp fname ] END @@ -82,26 +68,11 @@ ARGUMENT EXTEND with_names TYPED AS intro_pattern_opt PRINTED BY pr_intro_as_pat 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 ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> - [ + [ let pat = match pat with | None -> IntroAnonymous @@ -112,77 +83,23 @@ TACTIC EXTEND newfunind | [c] -> c | c::cl -> applist(c,cl) in - let f,args = decompose_app c in - fun g -> - let princ,bindings = - 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 ),Rawterm.NoBindings - | 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,bindings) in - let princ_vars = - List.fold_right - (fun a acc -> - try Idset.add (destVar a) acc - with _ -> acc - ) - args - Idset.empty - in - let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in - let old_idl = Idset.diff old_idl princ_vars in - let subst_and_reduce g = - let idl = - Util.map_succeed - (fun id -> - if Idset.mem id old_idl then failwith ""; - id - ) - (Tacmach.pf_ids_of_hyps g) - in - let flag = - Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; - } - in - Tacticals.tclTHEN - (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl ) - (Hiddentac.h_reduce flag Tacticals.allClauses) - g - in - Tacticals.tclTHEN - (choose_dest_or_ind - princ_infos - args_as_induction_constr - princ' - pat) - subst_and_reduce - g - ] + functional_induction true c princl pat ] +END +(***** debug only ***) +TACTIC EXTEND snewfunind + ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> + [ + let pat = + match pat with + | None -> IntroAnonymous + | Some pat -> pat + in + let c = match cl with + | [] -> assert false + | [c] -> c + | c::cl -> applist(c,cl) + in + functional_induction false c princl pat ] END @@ -213,7 +130,10 @@ VERNAC ARGUMENT EXTEND rec_definition2 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 + 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,"Function", @@ -240,12 +160,15 @@ END VERNAC COMMAND EXTEND Function ["Function" rec_definitions2(recsl)] -> - [ do_generate_principle false recsl] + [ + do_generate_principle false recsl; + + ] END VERNAC ARGUMENT EXTEND fun_scheme_arg -| [ ident(princ_name) ":=" "Induction" "for" ident(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] +| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] END VERNAC ARGUMENT EXTEND fun_scheme_args @@ -257,29 +180,176 @@ VERNAC COMMAND EXTEND NewFunctionalScheme ["Functional" "Scheme" fun_scheme_args(fas) ] -> [ try - Functional_principles_types.make_scheme fas + Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> match fas with | (_,fun_name,_)::_ -> begin - make_graph fun_name; - try Functional_principles_types.make_scheme fas + make_graph (Nametab.global fun_name); + try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> Util.error ("Cannot generate induction principle(s)") end | _ -> assert false (* we can only have non empty list *) ] END - +(***** debug only ***) VERNAC COMMAND EXTEND NewFunctionalCase ["Functional" "Case" fun_scheme_arg(fas) ] -> [ - Functional_principles_types.make_case_scheme fas + Functional_principles_types.build_case_scheme fas ] END - +(***** debug only ***) VERNAC COMMAND EXTEND GenerateGraph -["Generate" "graph" "for" ident(c)] -> [ make_graph c ] +["Generate" "graph" "for" reference(c)] -> [ make_graph (Nametab.global c) ] +END + + + + + +(* FINDUCTION *) + +(* comment this line to see debug msgs *) +(* let msg x = () ;; let pr_lconstr c = str "" *) + (* uncomment this to see debugging *) +let prconstr c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n") +let prlistconstr lc = List.iter prconstr lc +let prstr s = msg(str s) + + + +(** Information about an occurrence of a function call (application) + inside a term. *) +type fapp_info = { + fname: constr; (** The function applied *) + largs: constr list; (** List of arguments *) + free: bool; (** [true] if all arguments are debruijn free *) + max_rel: int; (** max debruijn index in the funcall *) + onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *) +} + + +(** [constr_head_match(a b c) a] returns true, false otherwise. *) +let constr_head_match u t= + if isApp u + then + let uhd,args= destApp u in + uhd=t + else false + +(** [hdMatchSub inu t] returns the list of occurrences of [t] in + [inu]. DeBruijn are not pushed, so some of them may be unbound in + the result. *) +let rec hdMatchSub inu (test: constr -> bool) : fapp_info list = + let subres = + match kind_of_term inu with + | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> + hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test + | Fix (_,(lna,tl,bl)) -> (* not sure Fix is correct *) + Array.fold_left + (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test) + [] bl + | _ -> (* Cofix will be wrong *) + fold_constr + (fun l cstr -> + l @ hdMatchSub cstr test) [] inu in + if not (test inu) then subres + else + let f,args = decompose_app inu in + let freeset = Termops.free_rels inu in + let max_rel = try Util.Intset.max_elt freeset with Not_found -> -1 in + {fname = f; largs = args; free = Util.Intset.is_empty freeset; + max_rel = max_rel; onlyvars = List.for_all isVar args } + ::subres + + +(** [find_fapp test g] returns the list of [app_info] of all calls to + functions that satisfy [test] in the conclusion of goal g. Trivial + repetition (not modulo conversion) are deleted. *) +let find_fapp (test:constr -> bool) g : fapp_info list = + let pre_res = hdMatchSub (Tacmach.pf_concl g) test in + let res = + List.fold_right (fun x acc -> if List.mem x acc then acc else x::acc) pre_res [] in + (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res); + res) + + + +(** [finduction id filter g] tries to apply functional induction on + an occurence of function [id] in the conclusion of goal [g]. If + [id]=[None] then calls to any function are selected. In any case + [heuristic] is used to select the most pertinent occurrence. *) +let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info list) + (nexttac:Proof_type.tactic) g = + let test = match oid with + | Some id -> + let idconstr = mkConst (const_of_id id) in + (fun u -> constr_head_match u idconstr) (* select only id *) + | None -> (fun u -> isApp u) in (* select calls to any function *) + let info_list = find_fapp test g in + let ordered_info_list = heuristic info_list in + prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list); + if List.length ordered_info_list = 0 then Util.error "function not found in goal\n"; + let taclist: Proof_type.tactic list = + List.map + (fun info -> + (tclTHEN + (functional_induction true (applist (info.fname, info.largs)) + None IntroAnonymous) + nexttac)) ordered_info_list in + tclFIRST taclist g + + + + +(** [chose_heuristic oi x] returns the heuristic for reordering + (and/or forgetting some elts of) a list of occurrences of + function calls infos to chose first with functional induction. *) +let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list = + match oi with + | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *) + | None -> + (* Default heuristic: keep only occurrence where all arguments + are *bound* (meaning already introduced) variables *) + (* TODO: put other funcalls at the end instead of deleting them *) + let ordering x y = + if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *) + else if x.free && x.onlyvars then -1 + else if y.free && y.onlyvars then 1 + else 0 (* both not pertinent *) + in + List.sort ordering + + +TACTIC EXTEND finduction + ["finduction" ident(id) natural_opt(oi)] -> + [ + match oi with + | Some(n) when n<=0 -> Util.error "numerical argument must be > 0" + | _ -> + let heuristic = chose_heuristic oi in + finduction (Some id) heuristic tclIDTAC + ] +END + + + +TACTIC EXTEND fauto + [ "fauto" tactic(tac)] -> + [ + let heuristic = chose_heuristic None in + finduction None heuristic (snd tac) + ] + | + [ "fauto" ] -> + [ + let heuristic = chose_heuristic None in + finduction None heuristic tclIDTAC + ] + END + -- cgit v1.2.3