diff options
Diffstat (limited to 'tactics/class_tactics.ml4')
| -rw-r--r-- | tactics/class_tactics.ml4 | 220 |
1 files changed, 110 insertions, 110 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index e9dfce78b..be8b0fb80 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -43,20 +43,20 @@ open Evd let default_eauto_depth = 100 let typeclasses_db = "typeclass_instances" -let _ = Auto.auto_init := (fun () -> +let _ = Auto.auto_init := (fun () -> Auto.create_hint_db false typeclasses_db full_transparent_state true) exception Found of evar_map -let is_dependent ev evm = - Evd.fold (fun ev' evi dep -> +let is_dependent ev evm = + Evd.fold (fun ev' evi dep -> if ev = ev' then dep else dep || occur_evar ev evi.evar_concl) evm false -let valid goals p res_sigma l = - let evm = - List.fold_left2 +let valid goals p res_sigma l = + let evm = + List.fold_left2 (fun sigma (ev, evi) prf -> let cstr, obls = Refiner.extract_open_proof !res_sigma prf in if not (Evd.is_defined sigma ev) then @@ -66,13 +66,13 @@ let valid goals p res_sigma l = in raise (Found evm) let evars_to_goals p evm = - let goals, evm' = + let goals, evm' = Evd.fold (fun ev evi (gls, evm') -> - if evi.evar_body = Evar_empty + if evi.evar_body = Evar_empty && Typeclasses.is_resolvable evi (* && not (is_dependent ev evm) *) - && p ev evi then ((ev,evi) :: gls, Evd.add evm' ev (Typeclasses.mark_unresolvable evi)) else + && p ev evi then ((ev,evi) :: gls, Evd.add evm' ev (Typeclasses.mark_unresolvable evi)) else (gls, Evd.add evm' ev evi)) evm ([], Evd.empty) in @@ -88,9 +88,9 @@ let intersects s t = open Auto -let e_give_exact flags c gl = - let t1 = (pf_type_of gl c) and t2 = pf_concl gl in - if occur_existential t1 or occur_existential t2 then +let e_give_exact flags c gl = + let t1 = (pf_type_of gl c) and t2 = pf_concl gl in + if occur_existential t1 or occur_existential t2 then tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl else exact_check c gl (* let t1 = (pf_type_of gl c) in *) @@ -107,12 +107,12 @@ let auto_unif_flags = { use_evars_pattern_unification = true; } -let unify_e_resolve flags (c,clenv) gls = +let unify_e_resolve flags (c,clenv) gls = let clenv' = connect_clenv gls clenv in let clenv' = clenv_unique_resolver false ~flags clenv' gls in Clenvtac.clenv_refine true ~with_classes:false clenv' gls -let unify_resolve flags (c,clenv) gls = +let unify_resolve flags (c,clenv) gls = let clenv' = connect_clenv gls clenv in let clenv' = clenv_unique_resolver false ~flags clenv' gls in Clenvtac.clenv_refine false ~with_classes:false clenv' gls @@ -120,64 +120,64 @@ let unify_resolve flags (c,clenv) gls = (** Hack to properly solve dependent evars that are typeclasses *) let flags_of_state st = - {auto_unif_flags with + {auto_unif_flags with modulo_conv_on_closed_terms = Some st; modulo_delta = st} let rec e_trivial_fail_db db_list local_db goal = - let tacl = + let tacl = Eauto.registered_e_assumption :: - (tclTHEN Tactics.intro + (tclTHEN Tactics.intro (function g'-> let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in (e_trivial_fail_db db_list (Hint_db.add_list hintl local_db) g'))) :: (List.map pi1 (e_trivial_resolve db_list local_db (pf_concl goal)) ) - in - tclFIRST (List.map tclCOMPLETE tacl) goal + in + tclFIRST (List.map tclCOMPLETE tacl) goal -and e_my_find_search db_list local_db hdc concl = +and e_my_find_search db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in let hintl = list_map_append - (fun db -> - if Hint_db.use_dn db then + (fun db -> + if Hint_db.use_dn db then let flags = flags_of_state (Hint_db.transparent_state db) in List.map (fun x -> (flags, x)) (Hint_db.map_auto (hdc,concl) db) else let flags = flags_of_state (Hint_db.transparent_state db) in List.map (fun x -> (flags, x)) (Hint_db.map_all hdc db)) (local_db::db_list) - in - let tac_of_hint = - fun (flags, {pri=b; pat = p; code=t}) -> + in + let tac_of_hint = + fun (flags, {pri=b; pat = p; code=t}) -> let tac = match t with | Res_pf (term,cl) -> unify_resolve flags (term,cl) | ERes_pf (term,cl) -> unify_e_resolve flags (term,cl) | Give_exact (c) -> e_give_exact flags c | Res_pf_THEN_trivial_fail (term,cl) -> - tclTHEN (unify_e_resolve flags (term,cl)) + tclTHEN (unify_e_resolve flags (term,cl)) (e_trivial_fail_db db_list local_db) | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> conclPattern concl p tacast - in + in (tac,b,pr_autotactic t) - in + in List.map tac_of_hint hintl -and e_trivial_resolve db_list local_db gl = - try - e_my_find_search db_list local_db +and e_trivial_resolve db_list local_db gl = + try + e_my_find_search db_list local_db (fst (head_constr_bound gl)) gl with Bound | Not_found -> [] let e_possible_resolve db_list local_db gl = - try - e_my_find_search db_list local_db + try + e_my_find_search db_list local_db (fst (head_constr_bound gl)) gl with Bound | Not_found -> [] - + let rec catchable = function | Refiner.FailError _ -> true | Stdpp.Exc_located (_, e) -> catchable e @@ -188,17 +188,17 @@ let is_dep gl gls = if evs = Intset.empty then false else List.fold_left - (fun b gl -> - if b then b + (fun b gl -> + if b then b else let evs' = Evarutil.evars_of_term gl.evar_concl in intersects evs evs') false gls -let is_ground gl = +let is_ground gl = Evarutil.is_ground_term (project gl) (pf_concl gl) -let nb_empty_evars s = +let nb_empty_evars s = Evd.fold (fun ev evi acc -> if evi.evar_body = Evar_empty then succ acc else acc) s 0 let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) @@ -214,7 +214,7 @@ type autogoal = goal * autoinfo type 'ans fk = unit -> 'ans type ('a,'ans) sk = 'a -> 'ans fk -> 'ans type 'a tac = { skft : 'ans. ('a,'ans) sk -> 'ans fk -> autogoal sigma -> 'ans } - + type auto_result = autogoal list sigma * validation type atac = auto_result tac @@ -225,9 +225,9 @@ let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : ' match res with | Some (gls,v) -> sk (f gls hints, fun _ -> v) fk | None -> fk () } - -let intro_tac : atac = - lift_tactic Tactics.intro + +let intro_tac : atac = + lift_tactic Tactics.intro (fun {it = gls; sigma = s} info -> let gls' = List.map (fun g' -> @@ -237,8 +237,8 @@ let intro_tac : atac = (g', { info with hints = ldb; auto_last_tac = str"intro" })) gls in {it = gls'; sigma = s}) -let id_tac : atac = - { skft = fun sk fk {it = gl; sigma = s} -> +let id_tac : atac = + { skft = fun sk fk {it = gl; sigma = s} -> sk ({it = [gl]; sigma = s}, fun _ pfs -> List.hd pfs) fk } (* Ordering of states is lexicographic on the number of remaining goals. *) @@ -250,13 +250,13 @@ let compare (pri, _, (res, _)) (pri', _, (res', _)) = if pri <> 0 then pri else nbgoals res - nbgoals res' -let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = +let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls } let solve_tac (x : 'a tac) : 'a tac = { skft = fun sk fk gls -> x.skft (fun ({it = gls},_ as res) fk -> if gls = [] then sk res fk else fk ()) fk gls } - -let hints_tac hints = + +let hints_tac hints = { skft = fun sk fk {it = gl,info; sigma = s} -> (* if !typeclasses_debug then msgnl (str"depth=" ++ int info.auto_depth ++ str": " ++ info.auto_last_tac *) (* ++ spc () ++ str "->" ++ spc () ++ pr_ev s gl); *) @@ -272,7 +272,7 @@ let hints_tac hints = poss in if l = [] && !typeclasses_debug then - msgnl (pr_depth info.auto_depth ++ str": no match for " ++ + msgnl (pr_depth info.auto_depth ++ str": no match for " ++ Printer.pr_constr_env (Evd.evar_env gl) concl ++ int (List.length poss) ++ str" possibilities"); List.map possible_resolve l in @@ -283,24 +283,24 @@ let hints_tac hints = ++ str" on" ++ spc () ++ pr_ev s gl); let fk = (fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *) - aux (succ i) tl) + aux (succ i) tl) in - let glsv = {it = list_map_i (fun j g -> g, - { info with auto_depth = j :: i :: info.auto_depth; + let glsv = {it = list_map_i (fun j g -> g, + { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp }) 1 gls; sigma = s}, fun _ -> v in sk glsv fk | [] -> fk () in aux 1 tacs } - + let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk = let rec aux s (acc : (autogoal list * validation) list) fk = function | (gl,info) :: gls -> - second.skft (fun ({it=gls';sigma=s'},v') fk' -> - let fk'' = if gls' = [] && Evarutil.is_ground_term s gl.evar_concl then + second.skft (fun ({it=gls';sigma=s'},v') fk' -> + let fk'' = if gls' = [] && Evarutil.is_ground_term s gl.evar_concl then (if !typeclasses_debug then msgnl (str"no backtrack on" ++ pr_ev s gl); fk) else fk' in aux s' ((gls',v')::acc) fk'' gls) fk {it = (gl,info); sigma = s} | [] -> Some (List.rev acc, s, fk) - in fun ({it = gls; sigma = s},v) fk -> + in fun ({it = gls; sigma = s},v) fk -> let rec aux' = function | None -> fk () | Some (res, s', fk') -> @@ -316,19 +316,19 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk let then_tac (first : atac) (second : atac) : atac = { skft = fun sk fk -> first.skft (then_list second sk) fk } - -let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option = + +let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option = t.skft (fun x _ -> Some x) (fun _ -> None) gl -let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : auto_result option = - (then_list t (fun x _ -> Some x)) +let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : auto_result option = + (then_list t (fun x _ -> Some x)) (gl, fun s pfs -> valid goals p (ref s) pfs) (fun _ -> None) - -let rec fix (t : 'a tac) : 'a tac = + +let rec fix (t : 'a tac) : 'a tac = then_tac t { skft = fun sk fk -> (fix t).skft sk fk } - + (* A special one for getting everything into a dnet. *) let is_transparent_gr (ids, csts) = function @@ -339,15 +339,15 @@ let is_transparent_gr (ids, csts) = function let make_resolve_hyp env sigma st flags pri (id, _, cty) = let cty = Evarutil.nf_evar sigma cty in let ctx, ar = decompose_prod cty in - let keep = + let keep = match kind_of_term (fst (decompose_app ar)) with | Const c -> is_class (ConstRef c) | Ind i -> is_class (IndRef i) | _ -> false in if keep then let c = mkVar id in - map_succeed - (fun f -> f (c,cty)) + map_succeed + (fun f -> f (c,cty)) [make_exact_entry pri; make_apply_entry env sigma flags pri] else [] @@ -356,9 +356,9 @@ let make_autogoal ?(st=full_transparent_state) g = let hintlist = list_map_append (pf_apply make_resolve_hyp g st (true,false,false) None) sign in let hints = Hint_db.add_list hintlist (Hint_db.empty st true) in (g.it, { hints = hints ; auto_depth = []; auto_last_tac = mt() }) - + let make_autogoals ?(st=full_transparent_state) gs evm' = - { it = list_map_i (fun i g -> + { it = list_map_i (fun i g -> let (gl, auto) = make_autogoal ~st {it = snd g; sigma = evm'} in (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' } @@ -368,9 +368,9 @@ let run_on_evars ?(st=full_transparent_state) p evm tac = | Some (goals, evm') -> match run_list_tac tac p goals (make_autogoals ~st goals evm') with | None -> raise Not_found - | Some (gls, v) -> - try ignore(v (sig_sig gls) []); assert(false) - with Found evm' -> + | Some (gls, v) -> + try ignore(v (sig_sig gls) []); assert(false) + with Found evm' -> Some (Evd.evars_reset_evd evm' evm) let eauto hints g = @@ -378,7 +378,7 @@ let eauto hints g = let gl = { it = make_autogoal g; sigma = project g } in match run_tac tac gl with | None -> raise Not_found - | Some ({it = goals; sigma = s}, valid) -> + | Some ({it = goals; sigma = s}, valid) -> {it = List.map fst goals; sigma = s}, valid s let real_eauto st hints p evd = @@ -404,24 +404,24 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl = let term = Evarutil.nf_evar evd term in evd, term -let _ = +let _ = Typeclasses.solve_instanciation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z) let has_undefined p oevd evd = Evd.fold (fun ev evi has -> has || - (evi.evar_body = Evar_empty && p ev evi && + (evi.evar_body = Evar_empty && p ev evi && (try Typeclasses.is_resolvable (Evd.find oevd ev) with _ -> true))) evd false let rec merge_deps deps = function | [] -> [deps] - | hd :: tl -> - if intersects deps hd then + | hd :: tl -> + if intersects deps hd then merge_deps (Intset.union deps hd) tl else hd :: merge_deps deps tl - + let evars_of_evi evi = - Intset.union (Evarutil.evars_of_term evi.evar_concl) + Intset.union (Evarutil.evars_of_term evi.evar_concl) (match evi.evar_body with | Evar_defined b -> Evarutil.evars_of_term b | Evar_empty -> Intset.empty) @@ -440,9 +440,9 @@ let select_evars evs evm = let resolve_all_evars debug m env p oevd do_split fail = let oevm = oevd in let split = if do_split then split_evars oevd else [Intset.empty] in - let p = if do_split then + let p = if do_split then fun comp ev evi -> (Intset.mem ev comp || not (Evd.mem oevm ev)) && p ev evi - else fun _ -> p + else fun _ -> p in let rec aux n p evd = if has_undefined p oevm evd then @@ -451,23 +451,23 @@ let resolve_all_evars debug m env p oevd do_split fail = aux (pred n) p evd' else None else Some evd - in + in let rec docomp evd = function | [] -> evd | comp :: comps -> let res = try aux 1 (p comp) evd with Not_found -> None in match res with - | None -> + | None -> if fail then let evd = Evarutil.nf_evars evd in - (* Unable to satisfy the constraints. *) + (* Unable to satisfy the constraints. *) let evm = if do_split then select_evars comp evd else evd in - let _, ev = Evd.fold - (fun ev evi (b,acc) -> + let _, ev = Evd.fold + (fun ev evi (b,acc) -> (* focus on one instance if only one was searched for *) if class_of_constr evi.evar_concl <> None then if not b (* || do_split *) then - true, Some ev + true, Some ev else b, None else b, acc) evm (false, None) in @@ -477,28 +477,28 @@ let resolve_all_evars debug m env p oevd do_split fail = in docomp oevd split let resolve_typeclass_evars d p env evd onlyargs split fail = - let pred = - if onlyargs then + let pred = + if onlyargs then (fun ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) && Typeclasses.is_class_evar evd evi) else (fun ev evi -> Typeclasses.is_class_evar evd evi) in resolve_all_evars d p env pred evd split fail - + let solve_inst debug mode depth env evd onlyargs split fail = resolve_typeclass_evars debug (mode, depth) env evd onlyargs split fail -let _ = +let _ = Typeclasses.solve_instanciations_problem := solve_inst false true default_eauto_depth - + VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings | [ "Typeclasses" "Transparent" reference_list(cl) ] -> [ add_hints false [typeclasses_db] (interp_hints (Vernacexpr.HintsTransparency (cl, true))) ] END - + VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings | [ "Typeclasses" "Opaque" reference_list(cl) ] -> [ add_hints false [typeclasses_db] @@ -520,9 +520,9 @@ END let pr_mode _prc _prlc _prt m = match m with Some b -> - if b then Pp.str "depth-first" else Pp.str "breadth-fist" + if b then Pp.str "depth-first" else Pp.str "breadth-fist" | None -> Pp.mt() - + ARGUMENT EXTEND search_mode TYPED AS bool option PRINTED BY pr_mode | [ "dfs" ] -> [ Some true ] | [ "bfs" ] -> [ Some false ] @@ -532,13 +532,13 @@ END let pr_depth _prc _prlc _prt = function Some i -> Util.pr_int i | None -> Pp.mt() - + ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth | [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ] END - + VERNAC COMMAND EXTEND Typeclasses_Settings - | [ "Typeclasses" "eauto" ":=" debug(d) search_mode(s) depth(depth) ] -> [ + | [ "Typeclasses" "eauto" ":=" debug(d) search_mode(s) depth(depth) ] -> [ typeclasses_debug := d; let mode = match s with Some t -> t | None -> true in let depth = match depth with Some i -> i | None -> default_eauto_depth in @@ -560,11 +560,11 @@ let _ = Classes.refine_ref := Refine.refine let rec head_of_constr t = let t = strip_outer_cast(collapse_appl t) in match kind_of_term t with - | Prod (_,_,c2) -> head_of_constr c2 + | Prod (_,_,c2) -> head_of_constr c2 | LetIn (_,_,_,c2) -> head_of_constr c2 | App (f,args) -> head_of_constr f | _ -> t - + TACTIC EXTEND head_of_constr [ "head_of_constr" ident(h) constr(c) ] -> [ let c = head_of_constr c in @@ -584,7 +584,7 @@ let freevars c = let rec frec acc c = match kind_of_term c with | Var id -> Idset.add id acc | _ -> fold_constr frec acc c - in + in frec Idset.empty c let coq_zero = lazy (gen_constant ["Init"; "Datatypes"] "O") @@ -597,15 +597,15 @@ let rec coq_nat_of_int = function let varify_constr_list ty def varh c = let vars = Idset.elements (freevars c) in - let mkaccess i = + let mkaccess i = mkApp (Lazy.force coq_List_nth, [| ty; coq_nat_of_int i; varh; def |]) in - let l = List.fold_right (fun id acc -> + let l = List.fold_right (fun id acc -> mkApp (Lazy.force coq_List_cons, [| ty ; mkVar id; acc |])) vars (mkApp (Lazy.force coq_List_nil, [| ty |])) in - let subst = + let subst = list_map_i (fun i id -> (id, mkaccess i)) 0 vars in l, replace_vars subst c @@ -630,27 +630,27 @@ let rec mkidx i p = else mkApp (Lazy.force coq_index_left, [|mkidx (i - p) (2 * p)|]) else if i = 1 then mkApp (Lazy.force coq_index_right, [|Lazy.force coq_index_end|]) else mkApp (Lazy.force coq_index_right, [|mkidx (i - p) (2 * p)|]) - + let varify_constr_varmap ty def varh c = let vars = Idset.elements (freevars c) in - let mkaccess i = + let mkaccess i = mkApp (Lazy.force coq_varmap_lookup, [| ty; def; i; varh |]) in - let rec vmap_aux l cont = - match l with + let rec vmap_aux l cont = + match l with | [] -> [], mkApp (Lazy.force coq_varmap_empty, [| ty |]) - | hd :: tl -> + | hd :: tl -> let left, right = split_interleaved [] [] tl in let leftvars, leftmap = vmap_aux left (fun x -> cont (mkApp (Lazy.force coq_index_left, [| x |]))) in let rightvars, rightmap = vmap_aux right (fun x -> cont (mkApp (Lazy.force coq_index_right, [| x |]))) in - (hd, cont (Lazy.force coq_index_end)) :: leftvars @ rightvars, + (hd, cont (Lazy.force coq_index_end)) :: leftvars @ rightvars, mkApp (Lazy.force coq_varmap_node, [| ty; hd; leftmap ; rightmap |]) in let subst, vmap = vmap_aux (def :: List.map (fun x -> mkVar x) vars) (fun x -> x) in let subst = List.map (fun (id, x) -> (destVar id, mkaccess x)) (List.tl subst) in vmap, replace_vars subst c - + TACTIC EXTEND varify [ "varify" ident(varh) ident(h') constr(ty) constr(def) constr(c) ] -> [ @@ -661,7 +661,7 @@ TACTIC EXTEND varify END TACTIC EXTEND not_evar - [ "not_evar" constr(ty) ] -> [ + [ "not_evar" constr(ty) ] -> [ match kind_of_term ty with | Evar _ -> tclFAIL 0 (str"Evar") | _ -> tclIDTAC ] |