diff --git a/configure.sh b/configure.sh index fae7a0895..ef7e86073 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" +DIRECTORIES="algebra complex coq_reals fta ftc liouville logic metrics model raster reals tactics transc order metric2 stdlib_omissions util classes ode write_image" find $DIRECTORIES -name "*.v" >>Make diff --git a/coq-corn.opam b/coq-corn.opam index 0b0ddf60d..bb0b28673 100644 --- a/coq-corn.opam +++ b/coq-corn.opam @@ -48,6 +48,7 @@ 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 deleted file mode 100644 index 9988cb6c9..000000000 --- a/dump/INSTALL +++ /dev/null @@ -1,10 +0,0 @@ -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 deleted file mode 100644 index e0e197650..000000000 --- a/dump/Makefile +++ /dev/null @@ -1,14 +0,0 @@ -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 deleted file mode 100644 index 7bc3f7798..000000000 --- a/dump/_CoqProject +++ /dev/null @@ -1,7 +0,0 @@ --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 deleted file mode 100644 index 37ff652ec..000000000 --- a/dump/src/dump_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -G_dump diff --git a/dump/src/dune b/dump/src/dune deleted file mode 100644 index 52a788a7b..000000000 --- a/dump/src/dune +++ /dev/null @@ -1,6 +0,0 @@ -(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 deleted file mode 100644 index 7224e4dc0..000000000 --- a/dump/src/g_dump.mlg +++ /dev/null @@ -1,120 +0,0 @@ -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 deleted file mode 100644 index 5c0b83292..000000000 --- a/dump/theories/Loader.v +++ /dev/null @@ -1 +0,0 @@ -Declare ML Module "dump_plugin". diff --git a/examples/Circle.v b/examples/Circle.v index e75d60df4..9aca29bc8 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*) -Require Import Plot RasterQ Qmetric. +From CoRN Require Import Plot RasterQ Qmetric. Require Import CoRN.reals.fast.Interval. Require Import CoRN.metric2.MetricMorphisms. Require Import CoRN.reals.faster.ARArith. -Require Import ARplot. +From CoRN 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.dump.theories.Loader. +Require Import CoRN.write_image.WritePPM. Local Open Scope uc_scope. @@ -47,21 +47,19 @@ Definition Cos_faster : sparse_raster _ _ End PlotCirclePath. -(* 6 seconds *) -Time Definition Circle_bigD : sparse_raster _ _ - := Eval vm_compute in - @Circle_faster bigD _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ bigD_appRat. +Definition Circle_bigD : sparse_raster _ _ + := @Circle_faster bigD _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ bigD_appRat. -DumpGrayMap Circle_bigD. -(* Now have a look at plot.pgm *) +(* 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 *) -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 *) +Definition Cos_bigD : sparse_raster _ _ + := @Cos_faster bigD _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ bigD_appRat. +(* 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 @@ -70,20 +68,18 @@ 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)). *) -(* 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 _) +Definition Circle : sparse_raster _ _ + := (let (_,r) := Plot.PlotPath 0 7 (-(1)) 1 (reflexivity _) (-(1)) 1 (reflexivity _) 200 CirclePath in r). -DumpGrayMap Circle. -(* Now have a look at plot.pgm *) +(* 16.3 seconds on Apple M1 *) +Time Elpi WritePPM "Circle2.ppm" ( Circle ). +(* Now have a look at Circle2.ppm *) diff --git a/examples/bigD.v b/examples/bigD.v index bd824ff2b..dad89eba3 100644 --- a/examples/bigD.v +++ b/examples/bigD.v @@ -1,10 +1,6 @@ -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. +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. Add Field Q : (dec_fields.stdlib_field_theory Q). @@ -31,7 +27,6 @@ Check ((1 _):(Z⁺)). Time Eval native_compute in (test (square x)). - -Require Import ARbigD. +From CoRN Require Import ARbigD. Time Eval vm_compute in (test (bigD_div (square x) x (10000%Z))). -Require Import ApproximateRationals. +From CoRN Require Import ApproximateRationals. diff --git a/write_image/README b/write_image/README new file mode 100644 index 000000000..fff959671 --- /dev/null +++ b/write_image/README @@ -0,0 +1,9 @@ +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 new file mode 100644 index 000000000..1f0992adc --- /dev/null +++ b/write_image/WritePPM.v @@ -0,0 +1,168 @@ +(** * 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 new file mode 100644 index 000000000..5b3b63b04 --- /dev/null +++ b/write_image/_CoqProject @@ -0,0 +1,3 @@ +-R . CoRN.write_image + +WritePPM.v