From 487e3aff8446bed2c5116cefc7d71d98a06e85de Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 29 Feb 2024 06:55:26 +0100 Subject: [PATCH] Port to VPL 0.5 --- .gitignore | 2 ++ Makefile | 13 +++----- _CoqProject | 2 +- src/reification.ml | 33 ++++++++++----------- src/reification.mli | 13 ++++---- src/{vpl_plugin.mllib => vpl_plugin.mlpack} | 0 src/vpltactics.ml4 | 6 ++-- tactic.mk.local | 1 + 8 files changed, 32 insertions(+), 38 deletions(-) rename src/{vpl_plugin.mllib => vpl_plugin.mlpack} (100%) create mode 100644 tactic.mk.local diff --git a/.gitignore b/.gitignore index 91cb42e..897aea7 100644 --- a/.gitignore +++ b/.gitignore @@ -9,6 +9,7 @@ *.glob *.dv *.aux +.coqdeps.d # ocaml files src/vpl_plugin.cmxs @@ -21,6 +22,7 @@ src/vpl_plugin.cmxs *.cmxa *.ml.d *.mllib.d +*.mlpack.d *.ml4.d *.mli.d diff --git a/Makefile b/Makefile index 896870b..d754ee0 100644 --- a/Makefile +++ b/Makefile @@ -1,17 +1,12 @@ -# requires: coq8.7 +# requires: coq8.9 .PHONY: clean tactic cacheclean test archclean install uninstall -MLTACTICOPT:=-rectypes -thread -package vpl -linkpkg - test: tactic - $(MAKE) -j -f tactic.mk "OPT:=-opt" + $(MAKE) -f tactic.mk tactic: tactic.mk - $(MAKE) -j -f tactic.mk src/vpltactics.cmx "OPT:=-opt" "CAMLC:=ocamlfind ocamlc -c $(MLTACTICOPT)" "CAMLOPTC:=ocamlfind ocamlopt -c $(MLTACTICOPT)" "CAMLLINK:=ocamlfind ocamlc $(MLTACTICOPT)" "CAMLOPTLINK:=ocamlfind ocamlopt $(MLTACTICOPT)" - $(MAKE) -j -f tactic.mk src/reification.cmx "OPT:=-opt" "CAMLC:=ocamlfind ocamlc -c $(MLTACTICOPT)" "CAMLOPTC:=ocamlfind ocamlopt -c $(MLTACTICOPT)" "CAMLLINK:=ocamlfind ocamlc $(MLTACTICOPT)" "CAMLOPTLINK:=ocamlfind ocamlopt $(MLTACTICOPT)" - $(MAKE) -j -f tactic.mk src/vpl_plugin.cmxa "OPT:=-opt" - $(MAKE) -j -f tactic.mk "OPT:=-opt" "CAMLC:=ocamlfind ocamlc -c $(MLTACTICOPT)" "CAMLOPTC:=ocamlfind ocamlopt -c $(MLTACTICOPT)" "CAMLLINK:=ocamlfind ocamlc $(MLTACTICOPT)" "CAMLOPTLINK:=ocamlfind ocamlopt $(MLTACTICOPT)" theories/Tactic.vo + $(MAKE) -f tactic.mk theories/Tactic.vo tactic.mk: _CoqProject coq_makefile -f _CoqProject -o tactic.mk @@ -23,7 +18,7 @@ uninstall: tactic.mk $(MAKE) -f tactic.mk uninstall || echo "skip last errors..." coqide: - @echo "coqide -R theories VplTactic -I src" + @echo "coqide" cacheclean: rm -rf */.*.aux .*.cache */*~ *~ diff --git a/_CoqProject b/_CoqProject index 2e61ddb..d6b63e4 100644 --- a/_CoqProject +++ b/_CoqProject @@ -4,7 +4,7 @@ src/reification.mli src/reification.ml src/vpltactics.ml4 -src/vpl_plugin.mllib +src/vpl_plugin.mlpack theories/Input.v theories/Output.v theories/Reduction.v diff --git a/src/reification.ml b/src/reification.ml index aeef029..31cef37 100644 --- a/src/reification.ml +++ b/src/reification.ml @@ -9,8 +9,7 @@ open Vpl module Rat = Scalar.Rat -module Vec = Vector.Rat.Positive -module Var = Var.Positive +module Vec = Vector.Rat exception RatReifyError (* The contrib name is used to locate errors when loading constrs *) @@ -60,29 +59,29 @@ module Positive = struct let reify_as_RatZ sigma = let rec reify_with_shift (s:int) acc p = if EConstr.eq_constr sigma p (Lazy.force xH) then - Rat.Z.orL acc (Rat.Z.shiftL Rat.Z.u s) + Z.logor acc (Z.shift_left Scalar.Int.u s) else match decomp_term sigma p with | Constr.App(head, args) when EConstr.eq_constr sigma head (Lazy.force _xO) -> reify_with_shift (s+1) acc args.(0) | Constr.App(head, args) when EConstr.eq_constr sigma head (Lazy.force _xI) -> - reify_with_shift (s+1) (Rat.Z.orL acc (Rat.Z.shiftL Rat.Z.u s)) args.(0) + reify_with_shift (s+1) (Z.logor acc (Z.shift_left Scalar.Int.u s)) args.(0) | _ -> raise RatReifyError - in fun p -> reify_with_shift 0 Rat.Z.z p + in fun p -> reify_with_shift 0 Scalar.Int.z p let xO p = lapp _xO [| p |] let xI p = lapp _xI [| p |] let from_RatZ = let rec from_RatZ p = - if Rat.Z.cmp p Rat.Z.u <= 0 then + if Scalar.Int.cmp p Scalar.Int.u <= 0 then Lazy.force xH - else if Rat.Z.cmp (Rat.Z.lAnd p Rat.Z.u) Rat.Z.u = 0 then - xI (from_RatZ (Rat.Z.shiftR p 1)) + else if Scalar.Int.cmp (Z.logand p Scalar.Int.u) Scalar.Int.u = 0 then + xI (from_RatZ (Z.shift_right p 1)) else - xO (from_RatZ (Rat.Z.shiftR p 1)) + xO (from_RatZ (Z.shift_right p 1)) in fun p -> - assert (Rat.Z.cmp p Rat.Z.u >= 0); + assert (Scalar.Int.cmp p Scalar.Int.u >= 0); (from_RatZ p) let rec from_Var p = @@ -103,23 +102,23 @@ struct let reify_as_RatZ sigma p = if EConstr.eq_constr sigma p (Lazy.force _Z0) then - Rat.Z.z + Scalar.Int.z else match decomp_term sigma p with | Constr.App(head, args) when EConstr.eq_constr sigma head (Lazy.force _Zpos) -> Positive.reify_as_RatZ sigma args.(0) | Constr.App(head, args) when EConstr.eq_constr sigma head (Lazy.force _Zneg) -> - Rat.Z.neg (Positive.reify_as_RatZ sigma args.(0)) + Scalar.Int.neg (Positive.reify_as_RatZ sigma args.(0)) | _ -> raise RatReifyError let from_RatZ x = - let sign = Rat.Z.cmp Rat.Z.z x in + let sign = Scalar.Int.cmp Scalar.Int.z x in if sign = 0 then Lazy.force _Z0 else if sign < 0 then lapp _Zpos [| Positive.from_RatZ x |] else - lapp _Zneg [| Positive.from_RatZ (Rat.Z.neg x) |] + lapp _Zneg [| Positive.from_RatZ (Scalar.Int.neg x) |] end @@ -217,11 +216,11 @@ module Input = struct let reify_as_cmpT sigma t = if EConstr.eq_constr sigma t (Lazy.force _LeT) then - Cstr.Le + Cstr_type.Le else if EConstr.eq_constr sigma t (Lazy.force _EqT) then - Cstr.Eq + Cstr_type.Eq else if EConstr.eq_constr sigma t (Lazy.force _LtT) then - Cstr.Lt + Cstr_type.Lt else assert false diff --git a/src/reification.mli b/src/reification.mli index 6300f1a..5f19a98 100644 --- a/src/reification.mli +++ b/src/reification.mli @@ -7,8 +7,7 @@ *) open Vpl module Rat = Scalar.Rat -module Vec = Vector.Rat.Positive -module Var = Var.Positive +module Vec = Vector.Rat exception RatReifyError exception DecompositionError of string @@ -74,7 +73,7 @@ sig (* [vplGoal l m g] is a short cut for Coq [vplGoal (sem l m) g] *) val vplGoal: EConstr.constr -> varmap -> EConstr.constr -> EConstr.constr - val reify_as_cmpT: Evd.evar_map -> EConstr.constr -> Cstr.cmpT + val reify_as_cmpT: Evd.evar_map -> EConstr.constr -> Cstr_type.cmpT end (** Reduction of Vpl Library *) @@ -166,16 +165,16 @@ end module Positive: sig (* raise [RatReifyError] in case of non-closed term *) - val reify_as_RatZ: Evd.evar_map -> EConstr.constr -> Rat.Z.t - val from_RatZ: Rat.Z.t -> EConstr.constr + val reify_as_RatZ: Evd.evar_map -> EConstr.constr -> Scalar.Int.t + val from_RatZ: Scalar.Int.t -> EConstr.constr end (* Coq Z *) module Z: sig (* raise [RatReifyError] in case of non-closed term *) - val reify_as_RatZ: Evd.evar_map -> EConstr.constr -> Rat.Z.t - val from_RatZ: Rat.Z.t -> EConstr.constr + val reify_as_RatZ: Evd.evar_map -> EConstr.constr -> Scalar.Int.t + val from_RatZ: Scalar.Int.t -> EConstr.constr end (* Coq Qc *) diff --git a/src/vpl_plugin.mllib b/src/vpl_plugin.mlpack similarity index 100% rename from src/vpl_plugin.mllib rename to src/vpl_plugin.mlpack diff --git a/src/vpltactics.ml4 b/src/vpltactics.ml4 index abcf4b8..24c923d 100644 --- a/src/vpltactics.ml4 +++ b/src/vpltactics.ml4 @@ -9,10 +9,8 @@ open Vpl (*i*) module Rat = Scalar.Rat -module Vec = Vector.Rat.Positive -module Var = Var.Positive -module Cs = Cstr.Rat.Positive -module Cons = IneqSet.Cons +module Vec = Vector.Rat +module Cs = Cstr.Rat type compf = EConstr.constr -> EConstr.constr diff --git a/tactic.mk.local b/tactic.mk.local new file mode 100644 index 0000000..e6a887d --- /dev/null +++ b/tactic.mk.local @@ -0,0 +1 @@ +CAMLPKGS:=-package vpl-core