diff options
-rw-r--r-- | .gitignore | 2 | ||||
-rw-r--r-- | INSTALL.md | 14 | ||||
-rw-r--r-- | examples/Example.v | 2 | ||||
-rw-r--r-- | src/PropToBool.v | 4 | ||||
-rwxr-xr-x | src/configure.sh | 2 | ||||
-rw-r--r-- | src/lia/lia.ml | 130 | ||||
-rw-r--r-- | src/versions/standard/Makefile.local | 4 | ||||
-rw-r--r-- | src/versions/standard/structures.ml | 43 | ||||
-rw-r--r-- | src/versions/standard/structures.mli | 6 |
9 files changed, 113 insertions, 94 deletions
@@ -17,6 +17,8 @@ setup.log *.v.d *.aux *.vo +*.vok +*.vos *.d .lia.cache .nia.cache @@ -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 |