Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: 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 Locus

(** Utilities on occurrences *)

let occurrences_map f = function
  | OnlyOccurrences l ->
    let l' = f l in
    if l' = [] then NoOccurrences else OnlyOccurrences l'
  | AllOccurrencesBut l ->
    let l' = f l in
    if l' = [] then AllOccurrences else AllOccurrencesBut l'
  | (NoOccurrences|AllOccurrences|AtLeastOneOccurrence) as o -> o

let convert_occs = function
  | AtLeastOneOccurrence -> (false,[])
  | AllOccurrences -> (false,[])
  | AllOccurrencesBut l -> (false,l)
  | NoOccurrences -> (true,[])
  | OnlyOccurrences l -> (true,l)

let is_selected occ = function
  | AtLeastOneOccurrence -> true
  | AllOccurrences -> true
  | AllOccurrencesBut l -> not (Int.List.mem occ l)
  | OnlyOccurrences l -> Int.List.mem occ l
  | NoOccurrences -> false

(** Usual clauses *)

let allHypsAndConcl = { onhyps=None; concl_occs=AllOccurrences }
let allHyps = { onhyps=None; concl_occs=NoOccurrences }
let onConcl = { onhyps=Some[]; concl_occs=AllOccurrences }
let nowhere = { onhyps=Some[]; concl_occs=NoOccurrences }
let onHyp h =
  { onhyps=Some[(AllOccurrences,h),InHyp]; concl_occs=NoOccurrences }

let is_nowhere = function
| { onhyps=Some[]; concl_occs=NoOccurrences } -> true
| _ -> false

let is_all_occurrences = function
  | AtLeastOneOccurrence
  | AllOccurrences -> true
  | _ -> false

(** Clause conversion functions, parametrized by a hyp enumeration function *)

(** From [clause] to [simple_clause] *)

let simple_clause_of enum_hyps cl =
  let error_occurrences () =
    CErrors.user_err Pp.(str "This tactic does not support occurrences selection") in
  let error_body_selection () =
    CErrors.user_err Pp.(str "This tactic does not support body selection") in
  let hyps =
    match cl.onhyps with
    | None ->
List.map Option.make (enum_hyps ())
    | Some l ->
List.map (fun ((occs,id),w) ->
          if not (is_all_occurrences occs) then error_occurrences ();
   if w = InHypValueOnly then error_body_selection ();
   Some id) l in
  if cl.concl_occs = NoOccurrences then hyps
  else
    if not (is_all_occurrences cl.concl_occs) then error_occurrences ()
    else None :: hyps

(** From [clause] to [concrete_clause] *)

let concrete_clause_of enum_hyps cl =
  let hyps =
    match cl.onhyps with
    | None ->
let f id = OnHyp (id,AllOccurrences,InHyp) in
List.map f (enum_hyps ())
    | Some l ->
List.map (fun ((occs,id),w) -> OnHyp (id,occs,w)) l in
  if cl.concl_occs = NoOccurrences then hyps
  else
    OnConcl cl.concl_occs :: hyps

(** Miscellaneous functions *)

let out_arg = function
  | ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.")
  | ArgArg x -> x

let occurrences_of_hyp id cls =
  let rec hyp_occ = function
      [] -> NoOccurrences, InHyp
    | ((occs,id'),hl)::_ when Names.Id.equal id id' ->
        occurrences_map (List.map out_arg) occs, hl
    | _::l -> hyp_occ l in
  match cls.onhyps with
      None -> AllOccurrences,InHyp
    | Some l -> hyp_occ l

let occurrences_of_goal cls =
  occurrences_map (List.map out_arg) cls.concl_occs

let in_every_hyp cls = Option.is_empty cls.onhyps

let clause_with_generic_occurrences cls =
  let hyps = match cls.onhyps with
  | None -> true
  | Some hyps ->
     List.for_all
       (function ((AllOccurrences,_),_) -> true | _ -> false) hyps in
  let concl = match cls.concl_occs with
  | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
  | _ -> false in
  hyps && concl

let clause_with_generic_context_selection cls =
  let hyps = match cls.onhyps with
  | None -> true
  | Some hyps ->
     List.for_all
       (function ((AllOccurrences,_),InHyp) -> true | _ -> false) hyps in
  let concl = match cls.concl_occs with
  | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
  | _ -> false in
  hyps && concl

¤ Dauer der Verarbeitung: 0.18 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.