Revert "Re-implement PixMap writer in Elpi"

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
 

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" 
 ]
 

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.

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

dump/_CoqProject

@@ -0,0 +1,7 @@
+-R theories CoRN.dump.theories
+-I src
+
+theories/Loader.v
+
+src/g_dump.mlg
+src/dump_plugin.mlpack

dump/src/dump_plugin.mlpack

@@ -0,0 +1 @@
+G_dump

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))

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
+

dump/theories/Loader.v

@@ -0,0 +1 @@
+Declare ML Module "dump_plugin".

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 *)
 
 

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.