diff --git a/configure.sh b/configure.sh index ef7e86073..fae7a0895 100755 --- a/configure.sh +++ b/configure.sh @@ -4,7 +4,7 @@ cp -f Make.in Make -DIRECTORIES="algebra complex coq_reals fta ftc liouville logic metrics model raster reals tactics transc order metric2 stdlib_omissions util classes ode write_image" +DIRECTORIES="algebra complex coq_reals fta ftc liouville logic metrics model raster reals tactics transc order metric2 stdlib_omissions util classes ode" find $DIRECTORIES -name "*.v" >>Make diff --git a/coq-corn.opam b/coq-corn.opam index bb0b28673..0b0ddf60d 100644 --- a/coq-corn.opam +++ b/coq-corn.opam @@ -48,7 +48,6 @@ install: [make "install"] depends: [ "coq" {(>= "8.18" & < "8.20~") | (= "dev")} "coq-math-classes" {(>= "8.8.1") | (= "dev")} - "coq-elpi" {(>= "1.18.0") | (= "dev")} "coq-bignums" ] diff --git a/dump/INSTALL b/dump/INSTALL new file mode 100644 index 000000000..9988cb6c9 --- /dev/null +++ b/dump/INSTALL @@ -0,0 +1,10 @@ +Dump is a Coq plugin that exports rasters to graymap PGM files. +Rasters are defined in module CoRN.raster.Raster, as matrices of booleans. + +Type make to build this plugin, then +Require Import CoRN.dump.theories.Loader +from a Coq file where you have rasters to export. +The vernac command defined by the plugin is DumpGrayMap, which takes +as argument the name of a global definition of a raster. It exports +the raster in file plot.pgm, which it will place in the current directory. +See module CoRN.examples.Circle. diff --git a/dump/Makefile b/dump/Makefile new file mode 100644 index 000000000..e0e197650 --- /dev/null +++ b/dump/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/dump/_CoqProject b/dump/_CoqProject new file mode 100644 index 000000000..7bc3f7798 --- /dev/null +++ b/dump/_CoqProject @@ -0,0 +1,7 @@ +-R theories CoRN.dump.theories +-I src + +theories/Loader.v + +src/g_dump.mlg +src/dump_plugin.mlpack diff --git a/dump/src/dump_plugin.mlpack b/dump/src/dump_plugin.mlpack new file mode 100644 index 000000000..37ff652ec --- /dev/null +++ b/dump/src/dump_plugin.mlpack @@ -0,0 +1 @@ +G_dump diff --git a/dump/src/dune b/dump/src/dune new file mode 100644 index 000000000..52a788a7b --- /dev/null +++ b/dump/src/dune @@ -0,0 +1,6 @@ +(library + (name dump_plugin) + (public_name coq.plugins.tutorial.p0) + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_dump)) diff --git a/dump/src/g_dump.mlg b/dump/src/g_dump.mlg new file mode 100644 index 000000000..7224e4dc0 --- /dev/null +++ b/dump/src/g_dump.mlg @@ -0,0 +1,120 @@ +DECLARE PLUGIN "dump_plugin" + +{ + +open Pp +open Names +open Printer +open Globnames +open Stdarg +open Typeops +open Constr + +exception Bad_list +exception Bad_int + +let rec int_of_pos (p : Constr.t) : int = + if isApp p then + (let (constructorTag, args) = destApp p in + let (r,_) = destRef constructorTag in + match r with + | GlobRef.ConstructRef (_,r) -> (* r is the number of the constructor, + starting from 1. *) + (if r = 1 then 2*int_of_pos args.(0)+1 else 2*int_of_pos args.(0)) + | _ -> raise Bad_int) + else 1 + +let int_of_z (z : Constr.t) : int = + if isApp z then + (let (constructorTag, args) = destApp z in + let (r,_) = destRef constructorTag in + match r with + | GlobRef.ConstructRef (_,r) -> (* r is the number of the constructor, + starting from 1. *) + (if r = 2 then int_of_pos args.(0) else -int_of_pos args.(0)) + | _ -> raise Bad_int) + else 0 + +let pair_int_of_pair_z (zz : Constr.t) : int*int = + if isApp zz then + (let (constructorTag, args) = destApp zz in + (int_of_z args.(2), int_of_z args.(3))) + else raise Bad_int + +let rec process_constr_list (l : Constr.t) (f : Constr.t -> unit) : unit = + if isApp l then + (let (constructorTag, args) = destApp l in + if Array.length args = 3 then + (* args stores type, current element and tail *) + (f args.(1) ; process_constr_list args.(2) f) + else ()) (* empty list *) + else raise Bad_list + +let dump_bool_list (l : Constr.t) (oc : out_channel) : unit = + process_constr_list l + (fun b -> + (* b is either true of false, which are constructors of the type bool *) + let (r,_) = destRef b in + match r with + | GlobRef.ConstructRef (_,r) -> (* r is the number of the constructor, + starting from 1. *) + output_string oc (if r = 1 then "1 " else "0 ") + | _ -> raise Bad_list) ; + output_string oc "\n" + +let dump_pgm (raster : Constr.t) (rastertype : Pp.t) = + let bufType = Buffer.create 1000 in + let fmtType = Format.formatter_of_buffer bufType in + pp_with fmtType rastertype; + Format.pp_print_flush fmtType (); + let (strType : string) = Buffer.contents bufType in + if Str.string_match (Str.regexp "(sparse_raster \\([0-9]+\\) \\([0-9]+\\))") + strType 0 then + (let line_count = int_of_string (Str.matched_group 2 strType) in + let column_count = int_of_string (Str.matched_group 1 strType) in + let oc = open_out "plot.pgm" in + let pixels = Array.make_matrix line_count column_count false in + let (constructorTag, args) = destApp raster in + process_constr_list args.(2) + (fun zz -> let (i,j) = pair_int_of_pair_z zz in + pixels.(i).(j) <- true); + (* P2 is the magic number for PGM ascii files. + Then come the dimensions of the image and + the number of levels of gray, ie 1. *) + output_string oc "P2\n"; + output_string oc (string_of_int column_count); + output_string oc " "; + output_string oc (string_of_int line_count); + output_string oc "\n1\n"; + (for i=0 to line_count-1 do + for j=0 to column_count-1 do + output_string oc (if pixels.(i).(j) then "1 " else "0 ") + done; + output_string oc "\n" + done); + close_out oc) + else failwith "Bad raster" + +(* Write the global term t to an ascii PGM file (portable gray map), + which is a format for grayscale matrices. + t should be already reduced, for example by + Definition t := Eval vm_compute in [some raster expression] *) +let eval_and_dump_pgm (t : Libnames.qualid) = + let env = Global.env () in + prerr_endline "dumping to plot.pgm"; + let (tg : GlobRef.t) = Constrintern.intern_reference t in + let (tt : Constr.types) = fst (type_of_global_in_context env tg) in + let (c : Constr.constr) = printable_constr_of_global tg in + (* Delta-reduce c to unfold the name of the matrix of booleans + and get its contents. *) + let evalc = Reductionops.whd_delta env (Evd.from_env env) (EConstr.of_constr c) in + let evalt = Reductionops.nf_all env (Evd.from_env env) (EConstr.of_constr tt) in + dump_pgm (EConstr.to_constr (Evd.from_env env) evalc) + (pr_econstr_env env (Evd.from_env env) evalt) + +} + +VERNAC COMMAND EXTEND DumpGrayMap CLASSIFIED AS QUERY +| [ "DumpGrayMap" global(a) ] -> { eval_and_dump_pgm a } +END + diff --git a/dump/theories/Loader.v b/dump/theories/Loader.v new file mode 100644 index 000000000..5c0b83292 --- /dev/null +++ b/dump/theories/Loader.v @@ -0,0 +1 @@ +Declare ML Module "dump_plugin". diff --git a/examples/Circle.v b/examples/Circle.v index 9aca29bc8..e75d60df4 100644 --- a/examples/Circle.v +++ b/examples/Circle.v @@ -3,18 +3,18 @@ (* I define the image of a path, a [Compact] subset of the plane.*) (* Finally, plot a hi-res Circle*) -From CoRN Require Import Plot RasterQ Qmetric. +Require Import Plot RasterQ Qmetric. Require Import CoRN.reals.fast.Interval. Require Import CoRN.metric2.MetricMorphisms. Require Import CoRN.reals.faster.ARArith. -From CoRN Require Import ARplot. +Require Import ARplot. Require Import CoRN.reals.faster.ARcos CoRN.reals.faster.ARsin CoRN.reals.faster.ARexp CoRN.reals.faster.ARbigD CoRN.reals.faster.ARinterval. Require Import CoRN.reals.fast.CRtrans. -Require Import CoRN.write_image.WritePPM. +Require Import CoRN.dump.theories.Loader. Local Open Scope uc_scope. @@ -47,19 +47,21 @@ Definition Cos_faster : sparse_raster _ _ End PlotCirclePath. -Definition Circle_bigD : sparse_raster _ _ - := @Circle_faster bigD _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ bigD_appRat. +(* 6 seconds *) +Time Definition Circle_bigD : sparse_raster _ _ + := Eval vm_compute in + @Circle_faster bigD _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ bigD_appRat. -(* 3.7s on Apple M1 - this is mostly the creation of the sparse raster *) -Time Elpi WritePPM "Circle.ppm" ( Circle_bigD ). -(* Now have a look at Circle.ppm *) +DumpGrayMap Circle_bigD. +(* Now have a look at plot.pgm *) -Definition Cos_bigD : sparse_raster _ _ - := @Cos_faster bigD _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ bigD_appRat. +Time Definition Cos_bigD : sparse_raster _ _ + := Eval vm_compute in + @Cos_faster bigD _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ bigD_appRat. + +DumpGrayMap Cos_bigD. +(* Now have a look at plot.pgm *) -(* 3.1s on Apple M1 *) -Time Elpi WritePPM "Cos.ppm" ( Cos_bigD ). -(* Now have a look at Cos.ppm *) Definition CircleFunction_aux : ProductMS Q_as_MetricSpace Q_as_MetricSpace --> ProductMS CR CR @@ -68,18 +70,20 @@ Definition CircleFunction_aux Definition CirclePath : Q_as_MetricSpace --> Complete Q2:= (uc_compose (uc_compose Couple CircleFunction_aux) (diag Q_as_MetricSpace)). (* The following hangs: - TODO this does not even compile Definition CirclePath': UCFunction Q R2:= - ucFunction (fun q:Q => Couple (cos_uc q, sin_uc q)). *) + ucFunction (fun q:Q => Couple (cos_uc q, sin_uc q)).*) -Definition Circle : sparse_raster _ _ - := (let (_,r) := Plot.PlotPath 0 7 (-(1)) 1 (reflexivity _) +(* 20 seconds *) +(* The raster must be evaluated before being plotted by DumpGrayMap, + here with vm_compute. *) +Time Definition Circle : sparse_raster _ _ + := Eval vm_compute in + (let (_,r) := Plot.PlotPath 0 7 (-(1)) 1 (reflexivity _) (-(1)) 1 (reflexivity _) 200 CirclePath in r). -(* 16.3 seconds on Apple M1 *) -Time Elpi WritePPM "Circle2.ppm" ( Circle ). -(* Now have a look at Circle2.ppm *) +DumpGrayMap Circle. +(* Now have a look at plot.pgm *) diff --git a/examples/bigD.v b/examples/bigD.v index dad89eba3..bd824ff2b 100644 --- a/examples/bigD.v +++ b/examples/bigD.v @@ -1,6 +1,10 @@ -Require Import Program QArith ZArith Bignums.BigZ.BigZ. -From CoRN Require Import Qpossec MetricMorphisms Qmetric Qdlog ARArith. -From MathClasses.implementations Require Import stdlib_rationals stdlib_binary_integers fast_integers dyadics. +Require Import + Program QArith ZArith Bignums.BigZ.BigZ Qpossec + MetricMorphisms Qmetric Qdlog ARArith + MathClasses.implementations.stdlib_rationals + MathClasses.implementations.stdlib_binary_integers + MathClasses.implementations.fast_integers + MathClasses.implementations.dyadics. Add Field Q : (dec_fields.stdlib_field_theory Q). @@ -27,6 +31,7 @@ Check ((1 _):(Z⁺)). Time Eval native_compute in (test (square x)). -From CoRN Require Import ARbigD. + +Require Import ARbigD. Time Eval vm_compute in (test (bigD_div (square x) x (10000%Z))). -From CoRN Require Import ApproximateRationals. +Require Import ApproximateRationals. diff --git a/write_image/README b/write_image/README deleted file mode 100644 index fff959671..000000000 --- a/write_image/README +++ /dev/null @@ -1,9 +0,0 @@ -write_image writes a CoRN "sparse_raster" to a file in PPM (portable pixmap) format. - -Usage: - -Require Import CoRN.write_image.WritePPM. - - - -Elpi WritePPM ".ppm" ( ). diff --git a/write_image/WritePPM.v b/write_image/WritePPM.v deleted file mode 100644 index 1f0992adc..000000000 --- a/write_image/WritePPM.v +++ /dev/null @@ -1,168 +0,0 @@ -(** * Write a CoRN sparse-raster as PPM file (portable pix map) *) - -(* The conversion from a sparse-raster to a 2D list of bools is done as Coq program. *) -(* The output of the Pixmap to a file in PPM is done as Elpi program - (Elpi is correctly the only tactic language which allows to write files) *) - -From CoRN Require Import Plot RasterQ Qmetric. - -Require Import ZArith. -Require Import Orders. -Require Import Mergesort. -Require Import List. -Import ListNotations. -Require Import Lia. - -Require Import elpi.elpi. - -(** A module for sorting the points of the sparse raster first by y and then by x coordinate *) - -Module SparseRasterOrder <: TotalLeBool. - Definition t := (Z*Z)%type. - Definition leb (x y : t) := - let (x1,x2):=x in - let (y1,y2):=y in - Z.ltb x1 y1 || (Z.eqb x1 y1) && (Z.leb x2 y2). - Theorem leb_total : forall x y : t, (eq (leb x y) true) \/ (eq (leb y x) true). - Proof. - intros x y. - unfold leb. - destruct x as [x1 x2], y as [y1 y2]. - lia. (* I love lia so much! *) - Qed. -End SparseRasterOrder. - -Module Import SparseRasterSort := Sort SparseRasterOrder. - -(* The function sorts a list of (x,y) pairs first be y and then by x coordinate *) - -Local Example SparseRasterSort'Ex1: eq - (SparseRasterSort.sort [(2, 1); (2, 2); (0, 2); (0, 1); (1, 1); (1, 0)]%Z) - [(0, 1); (0, 2); (1, 0); (1, 1); (2, 1); (2, 2)]%Z. -Proof. reflexivity. Qed. - -Fixpoint sparseRasterSorted_getLine (data : list (Z*Z)) (row : Z) : (list Z) * (list (Z*Z)) := - match data with - | [] => ([], []) - | (y,x)::t => - if Z.eqb y row - then let (current,rest) := sparseRasterSorted_getLine t row in (x::current, rest) - else ([],data) - end. - -(* If row matches the y coordinate of the first element, the function returns the - list of the x coordinates of the leading elements with this y coordinate and the remaining (x,y) pairs *) - -Local Example sparseRasterSorted_getLine'Ex1: eq - (sparseRasterSorted_getLine [(0, 1); (0, 2); (1, 0); (1, 1); (2, 1); (2, 2)]%Z 0) - ([1; 2]%Z, [(1, 0); (1, 1); (2, 1); (2, 2)]%Z). -Proof. reflexivity. Qed. - -(* Otherwise the x coordinate list is empty and the (x,y) pair list is returned unaltered *) - -Local Example sparseRasterSorted_getLine'Ex2: eq - (sparseRasterSorted_getLine [(0, 1); (0, 2); (1, 0); (1, 1); (2, 1); (2, 2)]%Z 1) - ([], [(0, 1); (0, 2); (1, 0); (1, 1); (2, 1); (2, 2)]%Z). -Proof. reflexivity. Qed. - -Definition listSorted_removeDuplicates {T : Type} (eqb : T->T->bool) (data : list T) := - let fix aux (data : list T) := - match data with - | [] => data - | [a] => data - | a::(b::t) as t'=> if eqb a b then aux t' else a::(aux t') - end - in aux data. - -Local Example listSorted_removeDuplicates'Ex1: eq (listSorted_removeDuplicates Z.eqb [1;2;2;3;3;3]%Z) [1;2;3]%Z. -Proof. reflexivity. Qed. - -Definition sparseRasterLine_rasterize (width : positive) (row : list Z) : list bool := - let fix aux (width : nat) (x : Z) (row : list Z) : list bool := - match width, row with - | O, _ => [] - | S w', [] => false :: (aux w' 0%Z row) - | S w', h::t => if Z.eqb h x then true :: (aux w' (x+1)%Z t) else false :: (aux w' (x+1)%Z row) - end - in aux (Pos.to_nat width) 0%Z (listSorted_removeDuplicates Z.eqb row). - -Local Example sparseRasterLine_rasterize'Ex1: eq - (sparseRasterLine_rasterize 10%positive [2;4;4;5]%Z) - [false; false; true; false; true; true; false; false; false; false]. -Proof. reflexivity. Qed. - -Definition sparseRaster_rasterize {width height : positive} (sr : sparse_raster width height) -: positive * positive * list (list bool) -:= - let '(sparse_raster_data _ _ data) := sr in - let data_sorted := SparseRasterSort.sort data in - let fix aux (nrows : nat) (irow : Z) (rest : list (Z*Z)) := - match nrows with - | O => [] - | S nrows' => - let (row, rest') := sparseRasterSorted_getLine rest irow in - let rownd := listSorted_removeDuplicates Z.eqb row in - sparseRasterLine_rasterize width row :: aux nrows' (irow+1)%Z rest' - end in - (width, height, aux (Pos.to_nat height) 0%Z data_sorted). - -Local Example sparseRaster_rasterize'Ex1 : eq - (sparseRaster_rasterize (sparse_raster_data 3 4 [(3, 1); (3, 2); (0, 2); (0, 1); (1, 1); (1, 0)]%Z)) - (3%positive, 4%positive, [ - [false; true; true ]; - [true; true; false]; - [false; false; false]; - [false; true; true ] - ] ). -Proof. reflexivity. Qed. - -Elpi Command WritePPM. -Elpi Accumulate lp:{{ - - % Convert a Coq positive to an ELpi int - pred coq-pos->elpi-int i:term, o:int. - coq-pos->elpi-int {{ xH }} 1 :- !. - coq-pos->elpi-int {{ xO lp:X }} Y :- calc (2 * { coq-pos->elpi-int X} ) Y, !. - coq-pos->elpi-int {{ xI lp:X }} Y :- calc (2 * { coq-pos->elpi-int X} + 1) Y, !. - coq-pos->elpi-int T I :- coq.say "coq-pos->elpi-int: Unexpected term" T I, !. - - % Convert a CoRN "sparse_raster" to a 2D Coq list of booleans - pred sparse-raster-rasterize i:term, o:int, o:int, o:term. - sparse-raster-rasterize DC NRE NCE DCR :- - coq.reduction.vm.norm {{ sparseRaster_rasterize lp:DC }} _ {{ (lp:NRC, lp:NCC, lp:DCR) }}, - coq-pos->elpi-int NRC NRE, - coq-pos->elpi-int NCC NCE, !. - sparse-raster-rasterize T _ _ _ :- coq.say "sparse-raster-rasterize: Unexpected term" T, !. - - % Convert a Coq list of booleans to an Elpi 01 string with "\n" termination - pred raster-row-to-string i:term, o:string. - raster-row-to-string {{ [] }} "\n". - raster-row-to-string {{ false :: lp:T }} S :- raster-row-to-string T TS, calc ("0" ^ TS) S. - raster-row-to-string {{ true :: lp:T }} S :- raster-row-to-string T TS, calc ("1" ^ TS) S. - raster-row-to-string T _ :- coq.say "raster-row-to-string: Unexpected term" T. - - % Write a Coq 2D list of booleans as lines of 01 data to an output stream - pred raster-write-rows i:out_stream, i:term. - raster-write-rows _ {{ [] }}. - raster-write-rows OS {{ lp:ROW :: lp:T }} :- - raster-row-to-string ROW ROWS, - output OS ROWS, - raster-write-rows OS T. - - % Main function of command - main [str FILEPATH, trm PM] :- - sparse-raster-rasterize PM PMNR PMNC PMData, - % Write PPM header - open_out FILEPATH OSTREAM, - output OSTREAM "P1\n", - output OSTREAM { calc (int_to_string PMNR) }, - output OSTREAM " ", - output OSTREAM { calc (int_to_string PMNC) }, - output OSTREAM "\n", - % Write PPM data - raster-write-rows OSTREAM PMData, - close_out OSTREAM - . -}}. -Elpi Typecheck. - diff --git a/write_image/_CoqProject b/write_image/_CoqProject deleted file mode 100644 index 5b3b63b04..000000000 --- a/write_image/_CoqProject +++ /dev/null @@ -1,3 +0,0 @@ --R . CoRN.write_image - -WritePPM.v