aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore2
-rw-r--r--INSTALL.md14
-rw-r--r--examples/Example.v2
-rw-r--r--src/PropToBool.v4
-rwxr-xr-xsrc/configure.sh2
-rw-r--r--src/lia/lia.ml130
-rw-r--r--src/versions/standard/Makefile.local4
-rw-r--r--src/versions/standard/structures.ml43
-rw-r--r--src/versions/standard/structures.mli6
9 files changed, 113 insertions, 94 deletions
diff --git a/.gitignore b/.gitignore
index 3a518b1..44630d3 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,6 +17,8 @@ setup.log
*.v.d
*.aux
*.vo
+*.vok
+*.vos
*.d
.lia.cache
.nia.cache
diff --git a/INSTALL.md b/INSTALL.md
index eb90daf..9a3577b 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -74,7 +74,7 @@ Then follow the instructions of the previous section.
### Requirements
-You need to have OCaml version >= 4.08 and < 4.10 and Coq version 8.10.*.
+You need to have OCaml version >= 4.09.0 and Coq version 8.11.*.
> **Warning**: The version of Coq that you plan to use must have been compiled
> with the same version of OCaml that you are going to use to compile
@@ -84,7 +84,7 @@ You need to have OCaml version >= 4.08 and < 4.10 and Coq version 8.10.*.
If you want to use SMTCoq with high performance to check large proof
certificates, you need to use the [version of Coq with native
data-structures](https://github.com/smtcoq/native-coq) instead of
-Coq-8.10 (warning: this allows one to use the vernacular commands but not
+Coq-8.11 (warning: this allows one to use the vernacular commands but not
the tactics).
### Install opam
@@ -110,24 +110,24 @@ eval `opam config env`
### Install OCaml
-Now you can install an OCaml compiler (we recommend 4.09.0):
+Now you can install an OCaml compiler (we recommend 4.10.0):
```bash
-opam switch create ocaml-base-compiler.4.09.0
+opam switch create ocaml-base-compiler.4.10.0
```
### Install Coq
-After OCaml is installed, you can install Coq-8.10.2 through opam.
+After OCaml is installed, you can install Coq-8.11.2 through opam.
```bash
-opam install coq.8.10.2
+opam install coq.8.11.2
```
If you also want to install CoqIDE at the same time you can do
```bash
-opam install coq.8.10.2 coqide.8.10.2
+opam install coq.8.11.2 coqide.8.11.2
```
but you might need to install some extra packages and libraries for your system
diff --git a/examples/Example.v b/examples/Example.v
index 952f91c..6c6b43d 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -11,7 +11,7 @@
(* [Require Import SMTCoq.SMTCoq.] loads the SMTCoq library.
- If you are using native-coq instead of Coq 8.10, replace it with:
+ If you are using native-coq instead of Coq 8.11, replace it with:
Require Import SMTCoq.
*)
diff --git a/src/PropToBool.v b/src/PropToBool.v
index 9bd73dc..0475d75 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -243,7 +243,7 @@ Ltac prop2bool_hyps Hs :=
Section Test.
Variable A : Type.
- Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = length l1 + length l2.
+ Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = (length l1 + length l2)%nat.
Hypothesis no_eq : forall (z1 z2:Z), (z1 < z2)%Z.
Hypothesis uninterpreted_type : forall (a:A), a = a.
Hypothesis bool_eq : forall (b:bool), negb (negb b) = b.
@@ -318,7 +318,7 @@ End MultipleCompDec.
polymorphism will be removed before *)
Section Poly.
Hypothesis basic : forall (A:Type) (l1 l2:list A),
- length (l1++l2) = length l1 + length l2.
+ length (l1++l2) = (length l1 + length l2)%nat.
Hypothesis uninterpreted_type : forall (A:Type) (a:A), a = a.
Goal True.
diff --git a/src/configure.sh b/src/configure.sh
index fb265e0..57a4161 100755
--- a/src/configure.sh
+++ b/src/configure.sh
@@ -39,4 +39,6 @@ else
cp ${pre}versions/standard/Structures_standard.v ${pre}versions/standard/Structures.v
cp ${pre}versions/standard/Tactics_standard.v ${pre}Tactics.v
coq_makefile -f _CoqProject -o Makefile
+ # work around https://github.com/coq/coq/issues/12603
+ sed -i 's/^CAMLDONTLINK=unix,str$/CAMLDONTLINK=num,str,unix,dynlink,threads/' Makefile
fi
diff --git a/src/lia/lia.ml b/src/lia/lia.ml
index 8dce3e8..dce79ee 100644
--- a/src/lia/lia.ml
+++ b/src/lia/lia.ml
@@ -181,57 +181,69 @@ end)
let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Structures.Micromega_plugin_Certificate.lia ce b) s)
let xhyps_of_cone base acc prf =
+ let open Structures.Micromega_plugin_Micromega in
+
let rec xtract e acc =
match e with
- | Structures.Micromega_plugin_Micromega.PsatzC _ | Structures.Micromega_plugin_Micromega.PsatzZ | Structures.Micromega_plugin_Micromega.PsatzSquare _ -> acc
- | Structures.Micromega_plugin_Micromega.PsatzIn n -> let n = (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n) in
+ | PsatzC _ | PsatzZ | PsatzSquare _ -> acc
+ | PsatzIn n -> let n = (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n) in
if n >= base
then Structures.Micromega_plugin_Mutils.ISet.add (n-base) acc
else acc
- | Structures.Micromega_plugin_Micromega.PsatzMulC(_,c) -> xtract c acc
- | Structures.Micromega_plugin_Micromega.PsatzAdd(e1,e2) | Structures.Micromega_plugin_Micromega.PsatzMulE(e1,e2) -> xtract e1 (xtract e2 acc) in
+ | PsatzMulC(_,c) -> xtract c acc
+ | PsatzAdd(e1,e2) | PsatzMulE(e1,e2) -> xtract e1 (xtract e2 acc) in
xtract prf acc
let hyps_of_pt pt =
+ let open Structures.Micromega_plugin_Micromega in
let rec xhyps base pt acc =
match pt with
- | Structures.Micromega_plugin_Micromega.DoneProof -> acc
- | Structures.Micromega_plugin_Micromega.RatProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c)
- | Structures.Micromega_plugin_Micromega.CutProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c)
- | Structures.Micromega_plugin_Micromega.EnumProof(c1,c2,l) ->
- let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in
- List.fold_left (fun s x -> xhyps (base + 1) x s) s l in
+ | DoneProof -> acc
+ | RatProof (c, pt) -> xhyps (base + 1) pt (xhyps_of_cone base acc c)
+ | CutProof (c, pt) -> xhyps (base + 1) pt (xhyps_of_cone base acc c)
+ | EnumProof (c1, c2, l) ->
+ let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in
+ List.fold_left (fun s x -> xhyps (base + 1) x s) s l
+ | ExProof (_, pt) -> xhyps (base + 3) pt acc
+ in
- xhyps 0 pt Structures.Micromega_plugin_Mutils.ISet.empty
+ xhyps 0 pt Structures.Micromega_plugin_Mutils.ISet.empty
let compact_cone prf f =
+ let open Structures.Micromega_plugin_Micromega in
+
let np n = Structures.Micromega_plugin_Mutils.CamlToCoq.nat (f (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n)) in
let rec xinterp prf =
match prf with
- | Structures.Micromega_plugin_Micromega.PsatzC _ | Structures.Micromega_plugin_Micromega.PsatzZ | Structures.Micromega_plugin_Micromega.PsatzSquare _ -> prf
- | Structures.Micromega_plugin_Micromega.PsatzIn n -> Structures.Micromega_plugin_Micromega.PsatzIn (np n)
- | Structures.Micromega_plugin_Micromega.PsatzMulC(e,c) -> Structures.Micromega_plugin_Micromega.PsatzMulC(e,xinterp c)
- | Structures.Micromega_plugin_Micromega.PsatzAdd(e1,e2) -> Structures.Micromega_plugin_Micromega.PsatzAdd(xinterp e1,xinterp e2)
- | Structures.Micromega_plugin_Micromega.PsatzMulE(e1,e2) -> Structures.Micromega_plugin_Micromega.PsatzMulE(xinterp e1,xinterp e2) in
+ | PsatzC _ | PsatzZ | PsatzSquare _ -> prf
+ | PsatzIn n -> PsatzIn (np n)
+ | PsatzMulC(e,c) -> PsatzMulC(e,xinterp c)
+ | PsatzAdd(e1,e2) -> PsatzAdd(xinterp e1,xinterp e2)
+ | PsatzMulE(e1,e2) -> PsatzMulE(xinterp e1,xinterp e2) in
xinterp prf
let compact_pt pt f =
- let translate ofset x =
- if x < ofset then x
- else (f (x-ofset) + ofset) in
-
+ let open Structures.Micromega_plugin_Micromega in
+ let translate ofset x = if x < ofset then x else f (x - ofset) + ofset in
let rec compact_pt ofset pt =
match pt with
- | Structures.Micromega_plugin_Micromega.DoneProof -> Structures.Micromega_plugin_Micromega.DoneProof
- | Structures.Micromega_plugin_Micromega.RatProof(c,pt) -> Structures.Micromega_plugin_Micromega.RatProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt )
- | Structures.Micromega_plugin_Micromega.CutProof(c,pt) -> Structures.Micromega_plugin_Micromega.CutProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt )
- | Structures.Micromega_plugin_Micromega.EnumProof(c1,c2,l) -> Structures.Micromega_plugin_Micromega.EnumProof(compact_cone c1 (translate (ofset)), compact_cone c2 (translate (ofset)),
- Structures.Micromega_plugin_Micromega.map (fun x -> compact_pt (ofset+1) x) l) in
- compact_pt 0 pt
+ | DoneProof -> DoneProof
+ | RatProof (c, pt) ->
+ RatProof (compact_cone c (translate ofset), compact_pt (ofset + 1) pt)
+ | CutProof (c, pt) ->
+ CutProof (compact_cone c (translate ofset), compact_pt (ofset + 1) pt)
+ | EnumProof (c1, c2, l) ->
+ EnumProof
+ ( compact_cone c1 (translate ofset)
+ , compact_cone c2 (translate ofset)
+ , map (fun x -> compact_pt (ofset + 1) x) l )
+ | ExProof (x, pt) -> ExProof (x, compact_pt (ofset + 3) pt)
+ in
+ compact_pt 0 pt
let pp_nat o n = Printf.fprintf o "%i" (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n)
@@ -248,40 +260,48 @@ let pp_list op cl elt o l =
Printf.fprintf o "%s%a%s" op _pp l cl
let pp_pol pp_c o e =
+ let open Structures.Micromega_plugin_Micromega in
let rec pp_pol o e =
match e with
- | Structures.Micromega_plugin_Micromega.Pc n -> Printf.fprintf o "Pc %a" pp_c n
- | Structures.Micromega_plugin_Micromega.Pinj(p,pol) -> Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol
- | Structures.Micromega_plugin_Micromega.PX(pol1,p,pol2) -> Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 in
+ | Pc n -> Printf.fprintf o "Pc %a" pp_c n
+ | Pinj(p,pol) -> Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol
+ | PX(pol1,p,pol2) -> Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 in
pp_pol o e
let pp_psatz pp_z o e =
+ let open Structures.Micromega_plugin_Micromega in
let rec pp_cone o e =
match e with
- | Structures.Micromega_plugin_Micromega.PsatzIn n ->
+ | PsatzIn n ->
Printf.fprintf o "(In %a)%%nat" pp_nat n
- | Structures.Micromega_plugin_Micromega.PsatzMulC(e,c) ->
+ | PsatzMulC(e,c) ->
Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c
- | Structures.Micromega_plugin_Micromega.PsatzSquare e ->
+ | PsatzSquare e ->
Printf.fprintf o "(%a^2)" (pp_pol pp_z) e
- | Structures.Micromega_plugin_Micromega.PsatzAdd(e1,e2) ->
+ | PsatzAdd(e1,e2) ->
Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2
- | Structures.Micromega_plugin_Micromega.PsatzMulE(e1,e2) ->
+ | PsatzMulE(e1,e2) ->
Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2
- | Structures.Micromega_plugin_Micromega.PsatzC p ->
+ | PsatzC p ->
Printf.fprintf o "(%a)%%positive" pp_z p
- | Structures.Micromega_plugin_Micromega.PsatzZ ->
+ | PsatzZ ->
Printf.fprintf o "0" in
pp_cone o e
-let rec pp_proof_term o = function
- | Structures.Micromega_plugin_Micromega.DoneProof -> Printf.fprintf o "D"
- | Structures.Micromega_plugin_Micromega.RatProof(cone,rst) -> Printf.fprintf o "R[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst
- | Structures.Micromega_plugin_Micromega.CutProof(cone,rst) -> Printf.fprintf o "C[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst
- | Structures.Micromega_plugin_Micromega.EnumProof(c1,c2,rst) ->
- Printf.fprintf o "EP[%a,%a,%a]"
- (pp_psatz pp_z) c1 (pp_psatz pp_z) c2
- (pp_list "[" "]" pp_proof_term) rst
+let rec pp_proof_term o p =
+ let open Structures.Micromega_plugin_Micromega in
+ match p with
+ | DoneProof -> Printf.fprintf o "D"
+ | RatProof (cone, rst) ->
+ Printf.fprintf o "R[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst
+ | CutProof (cone, rst) ->
+ Printf.fprintf o "C[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst
+ | EnumProof (c1, c2, rst) ->
+ Printf.fprintf o "EP[%a,%a,%a]" (pp_psatz pp_z) c1 (pp_psatz pp_z) c2
+ (pp_list "[" "]" pp_proof_term)
+ rst
+ | ExProof (p, prf) ->
+ Printf.fprintf o "Ex[%a,%a]" pp_positive p pp_proof_term prf
let linear_Z = {
name = "lia";
@@ -294,25 +314,27 @@ let linear_Z = {
}
let find_witness p polys1 =
+ let open Structures.Micromega_plugin_Certificate in
let polys1 = List.map fst polys1 in
match p.prover (p.get_option (), polys1) with
- | Structures.Micromega_plugin_Certificate.Model m -> Structures.Micromega_plugin_Certificate.Model m
- | Structures.Micromega_plugin_Certificate.Unknown -> Structures.Micromega_plugin_Certificate.Unknown
- | Structures.Micromega_plugin_Certificate.Prf prf -> Structures.Micromega_plugin_Certificate.Prf(prf,p)
+ | Model m -> Model m
+ | Unknown -> Unknown
+ | Prf prf -> Prf(prf,p)
let witness_list prover l =
+ let open Structures.Micromega_plugin_Certificate in
let rec xwitness_list l =
match l with
- | [] -> Structures.Micromega_plugin_Certificate.Prf []
+ | [] -> Prf []
| e :: l ->
match xwitness_list l with
- | Structures.Micromega_plugin_Certificate.Model (m,e) -> Structures.Micromega_plugin_Certificate.Model (m,e)
- | Structures.Micromega_plugin_Certificate.Unknown -> Structures.Micromega_plugin_Certificate.Unknown
- | Structures.Micromega_plugin_Certificate.Prf l ->
+ | Model (m,e) -> Model (m,e)
+ | Unknown -> Unknown
+ | Prf l ->
match find_witness prover e with
- | Structures.Micromega_plugin_Certificate.Model m -> Structures.Micromega_plugin_Certificate.Model (m,e)
- | Structures.Micromega_plugin_Certificate.Unknown -> Structures.Micromega_plugin_Certificate.Unknown
- | Structures.Micromega_plugin_Certificate.Prf w -> Structures.Micromega_plugin_Certificate.Prf (w::l) in
+ | Model m -> Model (m,e)
+ | Unknown -> Unknown
+ | Prf w -> Prf (w::l) in
xwitness_list l
let witness_list_tags = witness_list
diff --git a/src/versions/standard/Makefile.local b/src/versions/standard/Makefile.local
index 8abc72c..c57842a 100644
--- a/src/versions/standard/Makefile.local
+++ b/src/versions/standard/Makefile.local
@@ -25,6 +25,10 @@ clean::
CAMLLEX = $(CAMLBIN)ocamllex
CAMLYACC = $(CAMLBIN)ocamlyacc
+CAMLPKGS += -package num
+
+merlin-hook::
+ $(HIDE)echo 'PKG num' >> .merlin
%.ml : %.mll
$(CAMLLEX) $<
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 3b112cf..d069dde 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -10,9 +10,6 @@
(**************************************************************************)
-open Entries
-
-
(* Constr generation and manipulation *)
type id = Names.variable
let mkId = Names.Id.of_string
@@ -50,47 +47,39 @@ let pr_constr_env env = Printer.pr_constr_env env Evd.empty
let pr_constr = pr_constr_env Environ.empty_env
-let mkUConst : Constr.t -> Safe_typing.private_constants Entries.definition_entry = fun c ->
+let mkUConst : Constr.t -> Evd.side_effects Declare.proof_entry = fun c ->
let env = Global.env () in
let evd = Evd.from_env env in
let evd, ty = Typing.type_of env evd (EConstr.of_constr c) in
- { Entries.const_entry_body = Future.from_val ((c, Univ.ContextSet.empty),
- Safe_typing.empty_private_constants);
- const_entry_secctx = None;
- const_entry_feedback = None;
- const_entry_type = Some (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Constr.t *)
- const_entry_universes = Evd.univ_entry ~poly:false evd;
- const_entry_opaque = false;
- const_entry_inline_code = false }
+ Declare.definition_entry
+ ~opaque:false
+ ~inline:false
+ ~types:(EConstr.Unsafe.to_constr ty) (* Cannot contain evars since it comes from a Constr.t *)
+ ~univs:(Evd.univ_entry ~poly:false evd)
+ c
let mkTConst c noc ty =
let env = Global.env () in
let evd = Evd.from_env env in
let evd, _ = Typing.type_of env evd (EConstr.of_constr noc) in
- { const_entry_body = Future.from_val ((c, Univ.ContextSet.empty),
- Safe_typing.empty_private_constants);
- const_entry_secctx = None;
- const_entry_feedback = None;
- const_entry_type = Some ty;
- const_entry_universes = Evd.univ_entry ~poly:false evd;
- const_entry_opaque = false;
- const_entry_inline_code = false }
+ Declare.definition_entry
+ ~opaque:false
+ ~inline:false
+ ~types:ty
+ ~univs:(Evd.univ_entry ~poly:false evd)
+ c
(* TODO : Set -> Type *)
let declare_new_type t =
- let _ = ComAssumption.declare_assumption ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_entry Univ.ContextSet.empty) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make t) in
+ let _ = ComAssumption.declare_variable false ~kind:Decls.Definitional Constr.mkSet [] Glob_term.Explicit (CAst.make t) in
Constr.mkVar t
let declare_new_variable v constr_t =
- let env = Global.env () in
- let evd = Evd.from_env env in
- let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in
- let _ = ComAssumption.declare_assumption ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.univ_entry ~poly:false evd) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in
+ let _ = ComAssumption.declare_variable false ~kind:Decls.Definitional constr_t [] Glob_term.Explicit (CAst.make v) in
Constr.mkVar v
let declare_constant n c =
- Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition)
-
+ Declare.declare_constant ~name:n ~kind:(Decls.IsDefinition Decls.Definition) (Declare.DefinitionEntry c)
type cast_kind = Constr.cast_kind
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli
index 950135c..78c948c 100644
--- a/src/versions/standard/structures.mli
+++ b/src/versions/standard/structures.mli
@@ -43,11 +43,11 @@ val mkArrow : types -> types -> constr
val pr_constr_env : Environ.env -> constr -> Pp.t
val pr_constr : constr -> Pp.t
-val mkUConst : constr -> Safe_typing.private_constants Entries.definition_entry
-val mkTConst : constr -> constr -> types -> Safe_typing.private_constants Entries.definition_entry
+val mkUConst : constr -> Evd.side_effects Declare.proof_entry
+val mkTConst : constr -> constr -> types -> Evd.side_effects Declare.proof_entry
val declare_new_type : id -> types
val declare_new_variable : id -> types -> constr
-val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t
+val declare_constant : id -> Evd.side_effects Declare.proof_entry -> Names.Constant.t
type cast_kind
val vmcast : cast_kind
generated by cgit (git 2.34.1) at 2024-05-20 12:20:38 +0000