Changeset 2985

Timestamp:

Mar 27, 2013, 6:31:55 PM (8 years ago)

Author:

sacerdot

Message:

Order of printing of lines in LIN fixed again, truly this time. But I still
do not understand why I needed to reverse the list.

Files:

• extracted/joint_printer.ml (modified) (1 diff)
• src/joint/joint_printer.ma (modified) (2 diffs)

extracted/joint_printer.ml

@@ -1386 +1386 @@
   { cip_print_serialization_params = (lin_print_serialization_params lp pp);
     fold_code = (fun _ f m a ->
-    (List.foldr (fun x res ->
+    (Util.foldl (fun res x ->
       let { Types.fst = pc; Types.snd = res' } = res in
       { Types.fst = (Nat.S pc); Types.snd = (Obj.magic f pc x res') })

src/joint/joint_printer.ma

@@ -104 +104 @@
  ∀string. printing_pass_independent_params string → list string → string ≝
  λstring,pp.
-  foldl ?? (print_concat … pp) (print_empty … pp).  
+  foldr ?? (print_concat … pp) (print_empty … pp).  
 
 definition print_joint_seq :
@@ -261 +261 @@
    (λA.λf:code_point (lin_params_to_params …) → ?.λM:codeT lp globals.
     λa.
-     \snd (foldr ??
-      (λx.λres. let 〈pc,res'〉 ≝ res in 〈S pc,f pc x res'〉)
+     \snd (foldl ??
+      (λres,x. let 〈pc,res'〉 ≝ res in 〈S pc,f pc x res'〉)
       〈0,a〉 M))
      (λlinstr.