Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: obligations.mli 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 Proofview.Notations
open Context.Named.Declaration

module NamedDecl = Context.Named.Declaration

let extract_prefix env info =
  let ctx1 = List.rev (EConstr.named_context env) in
  let ctx2 = List.rev (Evd.evar_context info) in
  let rec share l1 l2 accu = match l1, l2 with
  | d1 :: l1, d2 :: l2 ->
    if d1 == d2 then share l1 l2 (d1 :: accu)
    else (accu, d2 :: l2)
  | _ -> (accu, l2)
  in
  share ctx1 ctx2 []

let typecheck_evar ev env sigma =
  let info = Evd.find sigma ev in
  (* Typecheck the hypotheses. *)
  let type_hyp (sigma, env) decl =
    let t = NamedDecl.get_type decl in
    let sigma, _ = Typing.sort_of env sigma t in
    let sigma = match decl with
    | LocalAssum _ -> sigma
    | LocalDef (_,body,_) -> Typing.check env sigma body t
    in
    (sigma, EConstr.push_named decl env)
  in
  let (common, changed) = extract_prefix env info in
  let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in
  let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
  (* Typecheck the conclusion *)
  let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
  sigma

(* Get the side-effect's constant declarations to update the monad's
  * environmnent *)
let add_if_undefined env eff =
  let open Entries in
  try ignore(Environ.lookup_constant eff.seff_constant env); env
  with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env

(* Add the side effects to the monad's environment, if not already done. *)
let add_side_effects env eff =
  List.fold_left add_if_undefined env eff

let generic_refine ~typecheck f gl =
  let sigma = Proofview.Goal.sigma gl in
  let env = Proofview.Goal.env gl in
  let concl = Proofview.Goal.concl gl in
  let state = Proofview.Goal.state gl in
  (* Save the [future_goals] state to restore them after the
     refinement. *)
  let prev_future_goals = Evd.save_future_goals sigma in
  (* Create the refinement term *)
  Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () ->
  f >>= fun (v, c) ->
  Proofview.tclEVARMAP >>= fun sigma ->
  Proofview.V82.wrap_exceptions begin fun () ->
  let evs = Evd.save_future_goals sigma in
  (* Redo the effects in sigma in the monad's env *)
  let privates_csts = Evd.eval_side_effects sigma in
  let sideff = Safe_typing.side_effects_of_private_constants privates_csts in
  let env = add_side_effects env sideff in
  (* Check that the introduced evars are well-typed *)
  let fold accu ev = typecheck_evar ev env accu in
  let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
  (* Check that the refined term is typesafe *)
  let sigma = if typecheck then Typing.check env sigma c concl else sigma in
  (* Check that the goal itself does not appear in the refined term *)
  let self = Proofview.Goal.goal gl in
  let _ =
    if not (Evarutil.occur_evar_upto sigma self c) then ()
    else Pretype_errors.error_occur_check env sigma self c
  in
  (* Restore the [future goals] state. *)
  let sigma = Evd.restore_future_goals sigma prev_future_goals in
  (* Select the goals *)
  let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in
  let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in
  (* Proceed to the refinement *)
  let sigma = match Proofview.Unsafe.advance sigma self with
  | None ->
    (* Nothing to do, the goal has been solved by side-effect *)
    sigma
  | Some self ->
    match evkmain with
    | None -> Evd.define self c sigma
    | Some evk ->
        let id = Evd.evar_ident self sigma in
        let sigma = Evd.define self c sigma in
        match id with
        | None -> sigma
        | Some id -> Evd.rename evk id sigma
  in
  (* Mark goals *)
  let sigma = Proofview.Unsafe.mark_as_goals sigma comb in
  let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
  let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++
                                   Termops.Internal.print_constr_env env sigma c)) in
  Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
  Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
  Proofview.Unsafe.tclEVARS sigma <*>
  Proofview.Unsafe.tclSETGOALS comb <*>
  Proofview.Unsafe.tclPUTSHELF shelf <*>
  Proofview.Unsafe.tclPUTGIVENUP given_up <*>
  Proofview.tclUNIT v
  end

let lift c =
  Proofview.tclEVARMAP >>= fun sigma ->
  Proofview.V82.wrap_exceptions begin fun () ->
  let (sigma, c) = c sigma in
  Proofview.Unsafe.tclEVARS sigma >>= fun () ->
  Proofview.tclUNIT c
  end

let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl

let refine_one ~typecheck f =
  Proofview.Goal.enter_one (make_refine_enter ~typecheck f)

let refine ~typecheck f =
  let f evd =
    let (evd,c) = f evd in (evd,((), c))
  in
  Proofview.Goal.enter (make_refine_enter ~typecheck f)

(** {7 solve_constraints}

  Ensure no remaining unification problems are left. Run at every "." by default. *)

let solve_constraints =
  let open Proofview in
  tclENV >>= fun env -> tclEVARMAP >>= fun sigma ->
   try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
       Unsafe.tclEVARSADVANCE sigma
   with e -> tclZERO e

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.