preserving order in chainprops

proofs/chainprops/chainprops.ml

@@ -70,7 +70,7 @@ let propositions (ast : S.ast) : decl list =
           "Invalid Dedukti source file: only symbol declarations are supported"
   in
   Stream.iter (fun c -> props := match_decl c.Pos.elt :: !props) ast;
-  !props
+  List.rev !props
 
 (** [merge imp deps props] transform each proposition of [props] into
     implications (the implication is defined by [imp]) from its
@@ -142,7 +142,7 @@ let cmd =
       `Pre "symbol tgt: P;\nsymbol hyp0: H0;\nsymbol hyp1: H1;";
       `P "$(b,psnj-chainprops foo.dep) outputs";
       `Pre
-        "symbol hyp1: H1;\nsymbol hyp0: H0;\nsymbol tgt: @imp H0 (@imp H1 P);";
+        "symbol hyp0: H0;\nsymbol hyp1: H1;\nsymbol tgt: @imp H0 (@imp H1 P);";
     ]
   in
   ( Term.(const chainprops $ deps $ imply $ pp_deps),

proofs/chainprops/chainprops.opam

@@ -6,6 +6,7 @@ depends: [
   "dune" {>= "2.9"}
   "cmdliner"
   "angstrom"
+  "lambdapi"
   "odoc" {with-doc}
 ]
 build: [

proofs/chainprops/test/run.t

   $ ../chainprops.exe example.dep < example.lp
-  symbol hyp1: H1;
-  symbol hyp0: H0;
   symbol tgt: @imp H0 (@imp H1 P);
+  symbol hyp0: H0;
+  symbol hyp1: H1;
 
 
   $ ../chainprops.exe foo.dep < foo.lp
-  symbol nitz: Nitz;
-  symbol frob: Frob;
-  symbol baz: Baz;
-  symbol bar: @imp Frob (@imp Nitz (@imp Baz Bar));
   symbol foo: @imp Bar (@imp Baz Foo);
+  symbol bar: @imp Frob (@imp Nitz (@imp Baz Bar));
+  symbol baz: Baz;
+  symbol frob: Frob;
+  symbol nitz: Nitz;