diff options
Diffstat (limited to 'plugins/firstorder/sequent.ml')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 312 |
1 files changed, 312 insertions, 0 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml new file mode 100644 index 00000000..685d44a8 --- /dev/null +++ b/plugins/firstorder/sequent.ml @@ -0,0 +1,312 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* $Id$ *) + +open Term +open Util +open Formula +open Unify +open Tacmach +open Names +open Libnames +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 + +let left_reversible lpat=(priority lpat)>0 + +module OrderedFormula= +struct + type t=Formula.t + let compare e1 e2= + (priority e1.pat) - (priority e2.pat) +end + +(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare + the immediate subterms of [c1] of [c2] if needed; Cast's, + application associativity, binders name and Cases annotations are + not taken into account *) + +let rec compare_list f l1 l2= + match l1,l2 with + [],[]-> 0 + | [],_ -> -1 + | _,[] -> 1 + | (h1::q1),(h2::q2) -> (f =? (compare_list f)) h1 h2 q1 q2 + +let compare_array f v1 v2= + let l=Array.length v1 in + let c=l - Array.length v2 in + if c=0 then + let rec comp_aux i= + if i<0 then 0 + else + let ci=f v1.(i) v2.(i) in + if ci=0 then + comp_aux (i-1) + else ci + in comp_aux (l-1) + else c + +let compare_constr_int f t1 t2 = + match kind_of_term t1, kind_of_term t2 with + | Rel n1, Rel n2 -> n1 - n2 + | Meta m1, Meta m2 -> m1 - m2 + | Var id1, Var id2 -> Pervasives.compare id1 id2 + | Sort s1, Sort s2 -> Pervasives.compare s1 s2 + | Cast (c1,_,_), _ -> f c1 t2 + | _, Cast (c2,_,_) -> f t1 c2 + | Prod (_,t1,c1), Prod (_,t2,c2) + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> + (f =? f) t1 t2 c1 c2 + | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> + ((f =? f) ==? f) b1 b2 t1 t2 c1 c2 + | App (_,_), App (_,_) -> + let c1,l1=decompose_app t1 + and c2,l2=decompose_app t2 in + (f =? (compare_list f)) c1 c2 l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> + ((-) =? (compare_array f)) e1 e2 l1 l2 + | Const c1, Const c2 -> Pervasives.compare c1 c2 + | Ind c1, Ind c2 -> Pervasives.compare c1 c2 + | Construct c1, Construct c2 -> Pervasives.compare c1 c2 + | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> + ((f =? f) ==? (compare_array f)) p1 p2 c1 c2 bl1 bl2 + | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> + ((Pervasives.compare =? (compare_array f)) ==? (compare_array f)) + ln1 ln2 tl1 tl2 bl1 bl2 + | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> + ((Pervasives.compare =? (compare_array f)) ==? (compare_array f)) + ln1 ln2 tl1 tl2 bl1 bl2 + | _ -> Pervasives.compare t1 t2 + +let rec compare_constr m n= + compare_constr_int compare_constr m n + +module OrderedConstr= +struct + type t=constr + let compare=compare_constr +end + +type h_item = global_reference * (int*constr) option + +module Hitem= +struct + type t = h_item + let compare (id1,co1) (id2,co2)= + (Pervasives.compare + =? (fun oc1 oc2 -> + match oc1,oc2 with + Some (m1,c1),Some (m2,c2) -> + ((-) =? OrderedConstr.compare) m1 m2 c1 c2 + | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2 +end + +module CM=Map.Make(OrderedConstr) + +module History=Set.Make(Hitem) + +let cm_add typ nam cm= + 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 typ nam cm= + try + let l=CM.find typ cm in + let l0=List.filter (fun id->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 item seq= + History.mem item seq.history || + match item with + (_,None)->false + | (id,Some ((m,t) as c))-> + let p (id2,o)= + match o with + None -> false + | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in + History.exists p seq.history + +let rec add_formula side nam t seq gl= + match build_formula side nam t gl 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 f.constr nam seq.context} + end + | Right t-> + match side with + Concl -> + {seq with gl=t;glatom=Some t} + | _ -> + {seq with + context=cm_add t nam seq.context; + latoms=t::seq.latoms} + +let re_add_formula_list lf seq= + let do_one f cm= + if f.id == dummy_id then cm + else cm_add 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 t seq=List.hd (CM.find t seq.context) + +(*let rev_left seq= + try + let lpat=(HP.maximum seq.redexes).pat in + left_reversible lpat + with Heap.EmptyHeap -> false +*) +let no_formula seq= + seq.redexes=HP.empty + +let rec take_formula 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 nseq (* discarding deprecated goal *) + else + hd,{seq with + redexes=hp; + context=cm_remove 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_tabulate (fun i -> ConstructRef (ind,i+1)) + (Inductiveops.nconstructors ind) + | gr -> + [gr]) + +let extend_with_ref_list l seq gl= + let l = expand_constructor_hints l in + let f gr seq= + let c=constr_of_global gr in + let typ=(pf_type_of gl c) in + add_formula Hyp gr typ seq gl in + List.fold_right f l seq + +open Auto + +let extend_with_auto_hints l seq gl= + let seqref=ref seq in + let f p_a_t = + match p_a_t.code with + Res_pf (c,_) | Give_exact c + | Res_pf_THEN_trivial_fail (c,_) -> + (try + let gr=global_of_constr c in + let typ=(pf_type_of gl c) in + seqref:=add_formula Hint gr typ !seqref gl + with Not_found->()) + | _-> () in + let g _ l=List.iter f l in + let h dbname= + let hdb= + try + searchtable_map dbname + with Not_found-> + error ("Firstorder: "^dbname^" : No such Hint database") in + Hint_db.iter g hdb in + List.iter h l; + !seqref + +let print_cmap map= + let print_entry c l s= + let xc=Constrextern.extern_constr false (Global.env ()) c in + str "| " ++ + Util.prlist Printer.pr_global l ++ + str " : " ++ + Ppconstr.pr_constr_expr xc ++ + cut () ++ + s in + msgnl (v 0 + (str "-----" ++ + cut () ++ + CM.fold print_entry map (mt ()) ++ + str "-----")) + + |