diff options
Diffstat (limited to 'contrib/funind/indfun_main.ml4')
-rw-r--r-- | contrib/funind/indfun_main.ml4 | 134 |
1 files changed, 123 insertions, 11 deletions
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index 00b5f28c..26a1066c 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -103,10 +103,28 @@ TACTIC EXTEND snewfunind END +let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_coma prc + +ARGUMENT EXTEND constr_coma_sequence' + TYPED AS constr_list + PRINTED BY pr_constr_coma_sequence +| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ] +| [ constr(c) ] -> [ [c] ] +END + +let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc + +ARGUMENT EXTEND auto_using' + TYPED AS constr_list + PRINTED BY pr_auto_using +| [ "using" constr_coma_sequence'(l) ] -> [ l ] +| [ ] -> [ [] ] +END + VERNAC ARGUMENT EXTEND rec_annotation2 [ "{" "struct" ident(id) "}"] -> [ Struct id ] -| [ "{" "wf" constr(r) ident_opt(id) "}" ] -> [ Wf(r,id) ] -| [ "{" "measure" constr(r) ident_opt(id) "}" ] -> [ Mes(r,id) ] +| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ] +| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ] END @@ -131,8 +149,8 @@ VERNAC ARGUMENT EXTEND rec_definition2 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" + | 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 @@ -214,11 +232,17 @@ END (* FINDUCTION *) (* comment this line to see debug msgs *) -(* let msg x = () ;; let pr_lconstr c = str "" *) +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) +let prNamedConstr s c = + begin + msg(str ""); + msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n"); + msg(str ""); + end @@ -266,6 +290,55 @@ let rec hdMatchSub inu (test: constr -> bool) : fapp_info list = max_rel = max_rel; onlyvars = List.for_all isVar args } ::subres +let mkEq typ c1 c2 = + mkApp (Coqlib.build_coq_eq(),[| typ; c1; c2|]) + + +let poseq_unsafe idunsafe cstr gl = + let typ = Tacmach.pf_type_of gl cstr in + tclTHEN + (Tactics.letin_tac true (Name idunsafe) cstr allClauses) + (tclTHENFIRST + (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr)) + Tactics.reflexivity) + gl + + +let poseq id cstr gl = + let x = Tactics.fresh_id [] id gl in + poseq_unsafe x cstr gl + +(* dirty? *) + +let list_constr_largs = ref [] + +let rec poseq_list_ids_rec lcstr gl = + match lcstr with + | [] -> tclIDTAC gl + | c::lcstr' -> + match kind_of_term c with + | Var _ -> + (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl) + | _ -> + let _ = prstr "c = " in + let _ = prconstr c in + let _ = prstr "\n" in + let typ = Tacmach.pf_type_of gl c in + let cname = Termops.id_of_name_using_hdchar (Global.env()) typ Anonymous in + let x = Tactics.fresh_id [] cname gl in + let _ = list_constr_largs:=mkVar x :: !list_constr_largs in + let _ = prstr " list_constr_largs = " in + let _ = prlistconstr !list_constr_largs in + let _ = prstr "\n" in + + tclTHEN + (poseq_unsafe x c) + (poseq_list_ids_rec lcstr') + gl + +let poseq_list_ids lcstr gl = + let _ = list_constr_largs := [] in + poseq_list_ids_rec lcstr gl (** [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 @@ -296,11 +369,17 @@ let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info l 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) + (fun info -> + (tclTHEN + (tclTHEN (poseq_list_ids info.largs) + ( + fun gl -> + (functional_induction + true (applist (info.fname, List.rev !list_constr_largs)) + None IntroAnonymous) gl)) nexttac)) ordered_info_list in + (* we try each (f t u v) until one does not fail *) + (* TODO: try also to mix functional schemes *) tclFIRST taclist g @@ -313,9 +392,8 @@ 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 + (* Default heuristic: put first occurrences 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 @@ -325,6 +403,7 @@ let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list = List.sort ordering + TACTIC EXTEND finduction ["finduction" ident(id) natural_opt(oi)] -> [ @@ -353,3 +432,36 @@ TACTIC EXTEND fauto END + +TACTIC EXTEND poseq + [ "poseq" ident(x) constr(c) ] -> + [ poseq x c ] +END + +VERNAC COMMAND EXTEND Showindinfo + [ "showindinfo" ident(x) ] -> [ Merge.showind x ] +END + +VERNAC COMMAND EXTEND MergeFunind + [ "Mergeschemes" lconstr(c) "with" lconstr(c') "using" ident(id) ] -> + [ + let c1 = Constrintern.interp_constr Evd.empty (Global.env()) c in + let c2 = Constrintern.interp_constr Evd.empty (Global.env()) c' in + let id1,args1 = + try + let hd,args = destApp c1 in + if Term.isInd hd then hd , args + else raise (Util.error "Ill-formed (fst) argument") + with Invalid_argument _ + -> Util.error ("Bad argument form for merging schemes") in + let id2,args2 = + try + let hd,args = destApp c2 in + if isInd hd then hd , args + else raise (Util.error "Ill-formed (snd) argument") + with Invalid_argument _ + -> Util.error ("Bad argument form for merging schemes") in + (* TOFO: enlever le ignore et declarer l'inductif *) + ignore(Merge.merge c1 c2 args1 args2 id) + ] +END |