1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243
(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open EConstr open CErrors open Util open Formula open Unify open Globnames open Pp let newcnt ()= let cnt=ref (-1) in fun b->if b then incr cnt;!cnt let priority = (* pure heuristics, <=0 for non reversible *) function Right rf-> begin match rf with Rarrow -> 100 | Rand -> 40 | Ror -> -15 | Rfalse -> -50 | Rforall -> 100 | Rexists (_,_,_) -> -29 end | Left lf -> match lf with Lfalse -> 999 | Land _ -> 90 | Lor _ -> 40 | Lforall (_,_,_) -> -30 | Lexists _ -> 60 | LA(_,lap) -> match lap with LLatom -> 0 | LLfalse (_,_) -> 100 | LLand (_,_) -> 80 | LLor (_,_) -> 70 | LLforall _ -> -20 | LLexists (_,_) -> 50 | LLarrow (_,_,_) -> -10 module OrderedFormula= struct type t=Formula.t let compare e1 e2= (priority e1.pat) - (priority e2.pat) end type h_item = global_reference * (int*Constr.t) option module Hitem= struct type t = h_item let compare (id1,co1) (id2,co2)= let c = Globnames.RefOrdered.compare id1 id2 in if c = 0 then let cmp (i1, c1) (i2, c2) = let c = Int.compare i1 i2 in if c = 0 then Constr.compare c1 c2 else c in Option.compare cmp co1 co2 else c end module CM=Map.Make(Constr) module History=Set.Make(Hitem) let cm_add sigma typ nam cm= let typ = EConstr.to_constr sigma typ in try let l=CM.find typ cm in CM.add typ (nam::l) cm with Not_found->CM.add typ [nam] cm let cm_remove sigma typ nam cm= let typ = EConstr.to_constr sigma typ in try let l=CM.find typ cm in let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in match l0 with []->CM.remove typ cm | _ ->CM.add typ l0 cm with Not_found ->cm module HP=Heap.Functional(OrderedFormula) type t= {redexes:HP.t; context:(global_reference list) CM.t; latoms:constr list; gl:types; glatom:constr option; cnt:counter; history:History.t; depth:int} let deepen seq={seq with depth=seq.depth-1} let record item seq={seq with history=History.add item seq.history} let lookup sigma item seq= History.mem item seq.history || match item with (_,None)->false | (id,Some (m, t))-> let p (id2,o)= match o with None -> false | Some (m2, t2)-> Globnames.eq_gr id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in History.exists p seq.history let add_formula env sigma side nam t seq = match build_formula env sigma side nam t seq.cnt with Left f-> begin match side with Concl -> {seq with redexes=HP.add f seq.redexes; gl=f.constr; glatom=None} | _ -> {seq with redexes=HP.add f seq.redexes; context=cm_add sigma f.constr nam seq.context} end | Right t-> match side with Concl -> {seq with gl=t;glatom=Some t} | _ -> {seq with context=cm_add sigma t nam seq.context; latoms=t::seq.latoms} let re_add_formula_list sigma lf seq= let do_one f cm= if f.id == dummy_id then cm else cm_add sigma f.constr f.id cm in {seq with redexes=List.fold_right HP.add lf seq.redexes; context=List.fold_right do_one lf seq.context} let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr sigma t) seq.context) (*let rev_left seq= try let lpat=(HP.maximum seq.redexes).pat in left_reversible lpat with Heap.EmptyHeap -> false *) let rec take_formula sigma seq= let hd=HP.maximum seq.redexes and hp=HP.remove seq.redexes in if hd.id == dummy_id then let nseq={seq with redexes=hp} in if seq.gl==hd.constr then hd,nseq else take_formula sigma nseq (* discarding deprecated goal *) else hd,{seq with redexes=hp; context=cm_remove sigma hd.constr hd.id seq.context} let empty_seq depth= {redexes=HP.empty; context=CM.empty; latoms=[]; gl=(mkMeta 1); glatom=None; cnt=newcnt (); history=History.empty; depth=depth} let expand_constructor_hints = List.map_append (function | IndRef ind -> List.init (Inductiveops.nconstructors ind) (fun i -> ConstructRef (ind,i+1)) | gr -> [gr]) let extend_with_ref_list env sigma l seq = let l = expand_constructor_hints l in let f gr (seq, sigma) = let sigma, c = Evd.fresh_global env sigma gr in let sigma, typ= Typing.type_of env sigma (EConstr.of_constr c) in (add_formula env sigma Hyp gr typ seq, sigma) in List.fold_right f l (seq, sigma) open Hints let extend_with_auto_hints env sigma l seq = let seqref=ref seq in let f p_a_t = match repr_hint p_a_t.code with Res_pf (c,_) | Give_exact (c,_) | Res_pf_THEN_trivial_fail (c,_) -> let (c, _, _) = c in (try let (gr, _) = Termops.global_of_constr sigma c in let typ=(Typing.unsafe_type_of env sigma c) in seqref:=add_formula env sigma Hint gr typ !seqref with Not_found->()) | _-> () in let g _ _ l = List.iter f l in let h dbname= let hdb= try searchtable_map dbname with Not_found-> user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database")) in Hint_db.iter g hdb in List.iter h l; !seqref, sigma (*FIXME: forgetting about universes*) let print_cmap map= let print_entry c l s= let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty (EConstr.of_constr c) in str "| " ++ prlist Printer.pr_global l ++ str " : " ++ Ppconstr.pr_constr_expr xc ++ cut () ++ s in (v 0 (str "-----" ++ cut () ++ CM.fold print_entry map (mt ()) ++ str "-----"))