package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file tacmach.ml

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
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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 Namegen
open Termops
open Reductionops
open Typing
open Tacred
open Logic
open Context.Named.Declaration

module NamedDecl = Context.Named.Declaration

(* Variants of [Tacmach] functions built with the new proof engine *)

let project gl =
  Proofview.Goal.sigma gl

let pf_apply f gl =
  f (Proofview.Goal.env gl) (project gl)

let pf_env = Proofview.Goal.env
let pf_concl = Proofview.Goal.concl

let pf_type_of gl t =
  pf_apply type_of gl t

let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2

let pf_ids_of_hyps gl =
  (* We only get the identifiers in [hyps] *)
  let hyps = Proofview.Goal.hyps gl in
  ids_of_named_context hyps

let pf_ids_set_of_hyps gl =
  (* We only get the identifiers in [hyps] *)
  let env = Proofview.Goal.env gl in
  Environ.ids_of_named_context_val (Environ.named_context_val env)

let pf_get_new_id id gl =
  let ids = pf_ids_set_of_hyps gl in
  next_ident_away id ids

let pf_get_hyp id gl =
  let hyps = Proofview.Goal.env gl in
  let sigma = project gl in
  let sign =
    try EConstr.lookup_named id hyps
    with Not_found -> raise (RefinerError (hyps, sigma, NoSuchHyp id))
  in
  sign

let pf_get_hyp_typ id gl =
  pf_get_hyp id gl |> NamedDecl.get_type

let pf_hyps_types gl =
  let env = Proofview.Goal.env gl in
  let sign = Environ.named_context env in
  List.map (function LocalAssum (id,x)
                    | LocalDef (id,_,x) -> id.Context.binder_name, EConstr.of_constr x)
            sign

let pf_last_hyp gl =
  let hyps = Proofview.Goal.hyps gl in
  List.hd hyps

let pf_nf_concl (gl : Proofview.Goal.t) =
  (* We normalize the conclusion just after *)
  let concl = Proofview.Goal.concl gl in
  let sigma = project gl in
  nf_evar sigma concl

let pf_whd_all gl t = pf_apply whd_all gl t

let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t

let pf_hnf_constr gl t = pf_apply hnf_constr gl t
let pf_hnf_type_of gl t =
  pf_whd_all gl (pf_get_type_of gl t)

let pf_compute gl t = pf_apply compute gl t
let pf_whd_compute gl t = pf_apply whd_compute gl t

let pf_nf_evar gl t = nf_evar (project gl) t

open Pp

let pr_gls gl =
  let sigma = project gl in
  let env = pf_env gl in
  let concl = Proofview.Goal.concl gl in
  let penv = Termops.Internal.print_named_context env in
  let pc = Termops.Internal.print_constr_env env sigma concl in
  let g = str"  " ++ hv 0 (penv ++ fnl () ++
                  str "============================" ++ fnl ()  ++
                  str" "  ++ pc) ++ fnl ()
  in
  hov 0 (pr_evar_map (Some 2) env sigma ++ fnl () ++ g)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct