Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: sequent.ml Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Util
open Pp
open CErrors
open Names
open EConstr
open Formula
open Unify

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 = GlobRef.t * (int*Constr.t) option

module Hitem=
struct
  type t = h_item
  let compare (id1,co1) (id2,co2)=
    let c = GlobRef.Ordered.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 ~abort_on_undefined_evars:false 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 ~abort_on_undefined_evars:false sigma typ in
  try
    let l=CM.find typ cm in
    let l0=List.filter (fun id-> not (GlobRef.equal 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:(GlobRef.t 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)-> GlobRef.equal 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 ~abort_on_undefined_evars:false 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
    | GlobRef.IndRef ind ->
        List.init (Inductiveops.nconstructors ind)
          (fun i -> GlobRef.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 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 env = Global.env () in
    let sigma = Evd.from_env env in
    let xc=Constrextern.extern_constr false env sigma (EConstr.of_constr c) in
      str "| " ++
      prlist Printer.pr_global l ++
      str " : " ++
      Ppconstr.pr_constr_expr env sigma xc ++
      cut () ++
      s in
    (v 0
      (str "-----" ++
       cut () ++
       CM.fold print_entry map (mt ()) ++
       str "-----"))

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.