further reduce memory footprint

CakeML · Oct 23, 2022 · b869e7a · b869e7a
1 parent 6bca48c
commit b869e7a
Show file tree

Hide file tree

Showing 3 changed files with 106 additions and 96 deletions.
diff --git a/examples/lpr_checker/array/lpr_arrayFullProgScript.sml b/examples/lpr_checker/array/lpr_arrayFullProgScript.sml
@@ -829,20 +829,18 @@ val check_unsat_1 = (append_prog o process_topdecs) `
     Inl err => TextIO.output TextIO.stdErr err
   | Inr (mv,(ncl,fml)) => TextIO.print_list (print_dimacs fml)`
 
-val _ = translate miscTheory.enumerate_def;
-
 val check_unsat_2 = (append_prog o process_topdecs) `
   fun check_unsat_2 f1 f2 =
   case parse_dimacs_full f1 of
     Inl err => TextIO.output TextIO.stdErr err
   | Inr (mv,(ncl,fml)) =>
-  let val ls = enumerate 1 fml
+  let val one = 1
       val arr = Array.array (2*ncl) None
-      val arr = fill_arr arr ls
+      val arr = fill_arr arr one fml
       val bnd = 2*mv + 3
       val earr = Array.array bnd None
-      val earr = fill_earliest earr ls
-      val rls = List.rev (List.map fst ls)
+      val earr = fill_earliest earr one fml
+      val rls = rev_enum_full 1 fml
   in
     case check_unsat' 0 arr rls earr f2 bnd [[]] of
       Inl err => TextIO.output TextIO.stdErr err
@@ -864,13 +862,13 @@ val check_unsat_3 = (append_prog o process_topdecs) `
   case parse_dimacs_full f3 of
     Inl err => TextIO.output TextIO.stdErr err
   | Inr (mv2,(ncl2,fml2)) =>
-  let val ls = enumerate 1 fml
+  let val one = 1
       val arr = Array.array (2*ncl) None
-      val arr = fill_arr arr ls
+      val arr = fill_arr arr one fml
       val bnd = 2*mv + 3
       val earr = Array.array bnd None
-      val earr = fill_earliest earr ls
-      val rls = List.rev (List.map fst ls)
+      val earr = fill_earliest earr one fml
+      val rls = rev_enum_full 1 fml
   in
     case check_unsat' 0 arr rls earr f2 bnd fml2 of
       Inl err => TextIO.output TextIO.stdErr err
@@ -912,13 +910,13 @@ val check_unsat_4 = (append_prog o process_topdecs) `
   | Some (Inr (i,j)) =>
     if check_cond i j pf
     then
-    let val ls = enumerate 1 fml
+    let val one = 1
         val arr = Array.array (2*ncl) None
-        val arr = fill_arr arr ls
+        val arr = fill_arr arr one fml
         val bnd = 2*mv + 3
         val earr = Array.array bnd None
-        val earr = fill_earliest earr ls
-        val rls = List.rev (List.map fst ls)
+        val earr = fill_earliest earr one fml
+        val rls = rev_enum_full 1 fml
     in
       case check_lpr_range_arr f3 arr rls earr bnd (ncl+1) pf i j of
         Inl err => TextIO.output TextIO.stdErr err
@@ -1050,6 +1048,10 @@ Proof
   >- (xmatch>> err_tac)>>
   PairCases_on`x`>>fs[SUM_TYPE_def,PAIR_TYPE_def]>>
   xmatch>>
+  xlet`POSTv v. &NUM 1 v * STDIO fs` >- (xlit>>xsimpl)>>
+  drule fill_arr_spec>>
+  drule fill_earliest_spec>>
+  rw[]>>
   rpt(xlet_autop)>>
   (* help instantiate fill_arr_spec *)
   `LIST_REL (OPTION_TYPE (LIST_TYPE INT)) (REPLICATE (2 * x1) NONE)
@@ -1060,18 +1062,7 @@ Proof
   `LIST_REL (OPTION_TYPE NUM) (REPLICATE (2 * x0 + 3) NONE)
           (REPLICATE (2 * x0 + 3) (Conv (SOME (TypeStamp "None" 2)) []))` by
     simp[LIST_REL_REPLICATE_same,OPTION_TYPE_def]>>
-  xlet_autop>>
-  xlet`
-    POSTv lv.
-    ARRAY resv' earliestv' * ARRAY resv arrlsv' * STDIO fs *
-    &(LIST_TYPE NUM (MAP FST (enumerate 1 x2)) lv)`
-  >- (
-    xapp_spec (ListProgTheory.map_1_v_thm |> INST_TYPE [alpha |-> ``:num``, beta |-> ``:num # int list``])>>
-    xsimpl>>
-    asm_exists_tac >>simp[]>>
-    qexists_tac`FST`>>
-    qexists_tac`NUM`>>simp[fst_v_thm])>>
-  rpt xlet_autop >>
+  rpt xlet_autop>>
   simp[check_lpr_unsat_list_def]>>
   qmatch_goalsub_abbrev_tac`check_lpr_list _ _ a b c d`>>
   xlet`POSTv v.
@@ -1120,6 +1111,7 @@ Proof
       disch_then drule>>
       simp[index_def]>>rw[]>>
       intLib.ARITH_TAC)>>
+    fs[LENGTH_enumerate,rev_enum_full_rev_enumerate]>>
     metis_tac[])>>
   reverse TOP_CASE_TAC>>simp[]
   >- (fs[SUM_TYPE_def]>>xmatch>>err_tac)>>
@@ -1206,6 +1198,10 @@ Proof
   >- (xmatch>> err_tac)>>
   PairCases_on`x`>>fs[SUM_TYPE_def,PAIR_TYPE_def]>>
   xmatch>>
+  xlet`POSTv v. &NUM 1 v * STDIO fs` >- (xlit>>xsimpl)>>
+  drule fill_arr_spec>>
+  drule fill_earliest_spec>>
+  rw[]>>
   rpt(xlet_autop)>>
   (* help instantiate fill_arr_spec *)
   `LIST_REL (OPTION_TYPE (LIST_TYPE INT)) (REPLICATE (2 * x1) NONE)
@@ -1216,18 +1212,7 @@ Proof
   `LIST_REL (OPTION_TYPE NUM) (REPLICATE (2 * x0 + 3) NONE)
           (REPLICATE (2 * x0 + 3) (Conv (SOME (TypeStamp "None" 2)) []))` by
     simp[LIST_REL_REPLICATE_same,OPTION_TYPE_def]>>
-  xlet_autop>>
-  xlet`
-    POSTv lv.
-    ARRAY resv' earliestv' * ARRAY resv arrlsv' * STDIO fs *
-    &(LIST_TYPE NUM (MAP FST (enumerate 1 x2)) lv)`
-  >- (
-    xapp_spec (ListProgTheory.map_1_v_thm |> INST_TYPE [alpha |-> ``:num``, beta |-> ``:num # int list``])>>
-    xsimpl>>
-    asm_exists_tac >>simp[]>>
-    qexists_tac`FST`>>
-    qexists_tac`NUM`>>simp[fst_v_thm])>>
-  rpt xlet_autop >>
+  rpt xlet_autop>>
   simp[check_lpr_sat_equiv_list_def]>>
   qmatch_goalsub_abbrev_tac`check_lpr_list _ _ a b c d`>>
   xlet`POSTv v.
@@ -1276,6 +1261,7 @@ Proof
       disch_then drule>>
       simp[index_def]>>rw[]>>
       intLib.ARITH_TAC)>>
+    fs[LENGTH_enumerate,rev_enum_full_rev_enumerate]>>
     metis_tac[])>>
   reverse TOP_CASE_TAC>>simp[]
   >- (fs[SUM_TYPE_def]>>xmatch>>err_tac)>>
@@ -1515,6 +1501,10 @@ Proof
     qexists_tac`fs`>>xsimpl>>
     rw[]>>
     qexists_tac`strlit"c Invalid range specification: range a-b must satisfy a <= b <= num lines in proof file\n"`>>xsimpl)>>
+  xlet`POSTv v. &NUM 1 v * STDIO fs` >- (xlit>>xsimpl)>>
+  drule fill_arr_spec>>
+  drule fill_earliest_spec>>
+  strip_tac >> strip_tac>>
   rpt(xlet_autop)>>
   (* help instantiate fill_arr_spec *)
   `LIST_REL (OPTION_TYPE (LIST_TYPE INT)) (REPLICATE (2 * x1) NONE)
@@ -1525,17 +1515,6 @@ Proof
   `LIST_REL (OPTION_TYPE NUM) (REPLICATE (2 * x0 + 3) NONE)
           (REPLICATE (2 * x0 + 3) (Conv (SOME (TypeStamp "None" 2)) []))` by
     simp[LIST_REL_REPLICATE_same,OPTION_TYPE_def]>>
-  xlet_autop>>
-  xlet`
-    POSTv lv.
-    ARRAY resv' earliestv' * ARRAY resv arrlsv' * STDIO fs *
-    &(LIST_TYPE NUM (MAP FST (enumerate 1 x2)) lv)`
-  >- (
-    xapp_spec (ListProgTheory.map_1_v_thm |> INST_TYPE [alpha |-> ``:num``, beta |-> ``:num # int list``])>>
-    xsimpl>>
-    asm_exists_tac >>simp[]>>
-    qexists_tac`FST`>>
-    qexists_tac`NUM`>>simp[fst_v_thm])>>
   rpt xlet_autop >>
   xlet_auto
   >- (
@@ -1579,9 +1558,12 @@ Proof
     rw[]>>
     simp[check_lpr_range_list_def]>>fs[]>>
     simp[check_lpr_sat_equiv_list_def]>>
-    qexists_tac`err`>>xsimpl)>>
+    qexists_tac`err`>>xsimpl>>
+    fs[LENGTH_enumerate,rev_enum_full_rev_enumerate]>>
+    xsimpl)>>
   TOP_CASE_TAC>>simp[check_lpr_range_list_def,check_lpr_sat_equiv_list_def]>>
   simp[SUM_TYPE_def]>>strip_tac>>
+  fs[LENGTH_enumerate,rev_enum_full_rev_enumerate]>>
   TOP_CASE_TAC>>fs[OPTION_TYPE_def,SUM_TYPE_def]>> xmatch
   >- (
     xlet_autop>>

diff --git a/examples/lpr_checker/array/lpr_arrayProgScript.sml b/examples/lpr_checker/array/lpr_arrayProgScript.sml
@@ -2895,71 +2895,68 @@ val print_dimacs_side = Q.prove(
   |> update_precondition;
 
 val fill_earliest = process_topdecs`
-  fun fill_earliest earr ls =
+  fun fill_earliest earr n ls =
     case ls of [] => earr
-    | (x::xs) =>
-    case x of (n,c) =>
-      fill_earliest (update_earliest_arr earr n c) xs` |> append_prog
+    | (c::cs) =>
+      fill_earliest (update_earliest_arr earr n c) (n+1) cs` |> append_prog
 
 Theorem fill_earliest_spec:
-  ∀ls lsv earliest earliestv Earrv.
-  LIST_TYPE (PAIR_TYPE NUM (LIST_TYPE INT)) ls lsv ∧
+  ∀ls lsv earliest earliestv Earrv c cv.
+  NUM c cv ∧
+  LIST_TYPE (LIST_TYPE INT) ls lsv ∧
   LIST_REL (OPTION_TYPE NUM) earliest earliestv
   ⇒
   app (p:'ffi ffi_proj) ^(fetch_v"fill_earliest"(get_ml_prog_state()))
-  [Earrv; lsv]
+  [Earrv; cv; lsv]
   (ARRAY Earrv earliestv)
   (POSTv resv.
   SEP_EXISTS earliestv'. ARRAY resv earliestv' *
-    &(LIST_REL (OPTION_TYPE NUM) (FOLDL (λacc (i,v). update_earliest acc i v) earliest ls) earliestv'))
+    &(LIST_REL (OPTION_TYPE NUM) (FOLDL (λacc (i,v). update_earliest acc i v) earliest (enumerate c ls)) earliestv'))
 Proof
   Induct>>rw[]>>
   xcf "fill_earliest" (get_ml_prog_state ())>>
-  fs[LIST_TYPE_def]>>
+  fs[LIST_TYPE_def,miscTheory.enumerate_def]>>
   xmatch
   >- (xvar>>xsimpl)>>
-  Cases_on`h`>>fs[PAIR_TYPE_def]>>
-  xmatch>>
+  xlet_autop >>
   xlet_autop >>
   xapp>>
-  simp[]
+  xsimpl
 QED
 
 val fill_arr = process_topdecs`
-  fun fill_arr arr ls =
+  fun fill_arr arr i ls =
     case ls of [] => arr
-    | (x::xs) =>
-    case x of (i,v) =>
-      fill_arr (resize_update_arr (Some v) i arr) xs` |> append_prog
+    | (v::vs) =>
+      fill_arr (resize_update_arr (Some v) i arr) (i+1) vs` |> append_prog
 
 Theorem fill_arr_spec:
-  ∀ls lsv arrv arrls arrlsv.
-  LIST_TYPE (PAIR_TYPE NUM (LIST_TYPE INT)) ls lsv ∧
+  ∀ls lsv arrv arrls arrlsv i iv.
+  NUM i iv ∧
+  LIST_TYPE (LIST_TYPE INT) ls lsv ∧
   LIST_REL (OPTION_TYPE (LIST_TYPE INT)) arrls arrlsv
   ⇒
   app (p:'ffi ffi_proj) ^(fetch_v"fill_arr"(get_ml_prog_state()))
-  [arrv; lsv]
+  [arrv; iv; lsv]
   (ARRAY arrv arrlsv)
   (POSTv resv.
   SEP_EXISTS arrlsv'. ARRAY resv arrlsv' *
-    & LIST_REL (OPTION_TYPE (LIST_TYPE INT)) (FOLDL (λacc (i,v).  resize_update_list acc NONE (SOME v) i) arrls ls) arrlsv')
+    & LIST_REL (OPTION_TYPE (LIST_TYPE INT))
+    (FOLDL (λacc (i,v).  resize_update_list acc NONE (SOME v) i) arrls (enumerate i ls)) arrlsv')
 Proof
   Induct>>rw[]>>
   xcf "fill_arr" (get_ml_prog_state ())>>
-  fs[LIST_TYPE_def]>>
+  fs[LIST_TYPE_def,miscTheory.enumerate_def]>>
   xmatch
   >- (xvar>>xsimpl)>>
-  Cases_on`h`>>fs[PAIR_TYPE_def]>>
-  xmatch>>
-  xlet_autop >>
+  rpt xlet_autop >>
   xlet`(POSTv resv.
       SEP_EXISTS fmllsv'.
       ARRAY resv fmllsv' *
-      &(LIST_REL (OPTION_TYPE (LIST_TYPE INT)) (resize_update_list arrls NONE (SOME r) q) fmllsv') )`
+      &(LIST_REL (OPTION_TYPE (LIST_TYPE INT)) (resize_update_list arrls NONE (SOME h) i) fmllsv') )`
   >- (
     xapp >> xsimpl>>
-    simp[OPTION_TYPE_def] )
-  >>
+    simp[OPTION_TYPE_def] ) >>
   xapp>>
   xsimpl
 QED
@@ -3191,5 +3188,41 @@ Proof
   metis_tac[fml_rel_contains_clauses_list]
 QED
 
+Definition rev_enum_def:
+  rev_enum (s:num) (e:num) acc =
+  if s < e then
+    rev_enum (s+1) e (s::acc)
+  else
+    acc
+Termination
+  WF_REL_TAC`measure (λ(s,e,acc). e-s)`
+End
+
+Theorem rev_enum_rev_enumerate:
+  ∀fml k acc.
+  rev_enum k (LENGTH fml + k) acc =
+  REVERSE (MAP FST (enumerate k fml)) ++ acc
+Proof
+  Induct>>rw[Once rev_enum_def]>>
+  simp[miscTheory.enumerate_def]>>
+  first_x_assum(qspec_then`k+1` mp_tac)>>
+  simp[ADD1]
+QED
+
+val _ = translate rev_enum_def;
+
+Definition rev_enum_full_def:
+  rev_enum_full k fml =
+  rev_enum k (LENGTH fml + k) []
+End
+
+Theorem rev_enum_full_rev_enumerate:
+  rev_enum_full k fml =
+  REVERSE (MAP FST (enumerate k fml))
+Proof
+  rw[rev_enum_full_def,rev_enum_rev_enumerate]
+QED
+
+val _ = translate rev_enum_full_def;
 
 val _ = export_theory();
diff --git a/examples/lpr_checker/array/lpr_arrayRamseyProgScript.sml b/examples/lpr_checker/array/lpr_arrayRamseyProgScript.sml
@@ -61,14 +61,14 @@ val max_lit_fml_side = Q.prove(
 val check_unsat_1 = (append_prog o process_topdecs) `
   fun check_unsat_1 enc f =
   let val fml = enc ()
-      val ls = enumerate 1 fml
-      val arr = Array.array (2*(List.length ls)) None
-      val arr = fill_arr arr ls
+      val one = 1
+      val arr = Array.array (2*(List.length fml)) None
+      val arr = fill_arr arr one fml
       val mv = max_lit_fml fml
       val bnd = 2*mv + 3
       val earr = Array.array bnd None
-      val earr = fill_earliest earr ls
-      val rls = List.rev (List.map fst ls)
+      val earr = fill_earliest earr one fml
+      val rls = rev_enum_full 1 fml
   in
     case check_unsat' 0 arr rls earr f bnd [[]] of
       Inl err => TextIO.output TextIO.stdErr err
@@ -115,35 +115,29 @@ Proof
   rw[]>>
   xcf "check_unsat_1" (get_ml_prog_state ())>>
   rpt xlet_autop>>
+  xlet`POSTv v. &NUM 1 v * STDIO fs` >- (xlit>>xsimpl)>>
+  drule fill_arr_spec>>
+  drule fill_earliest_spec>>
+  rw[]>>
+  rpt xlet_autop>>
   (* help instantiate fill_arr_spec *)
   qmatch_asmsub_abbrev_tac`NUM (LENGTH fmlls) nv`>>
   `LIST_REL (OPTION_TYPE (LIST_TYPE INT)) (REPLICATE (2*(LENGTH fmlls)) NONE)
         (REPLICATE (2 * (LENGTH fmlls)) (Conv (SOME (TypeStamp "None" 2)) []))` by
     simp[LIST_REL_REPLICATE_same,OPTION_TYPE_def]>>
-  drule fill_arr_spec>>
-  disch_then drule>>
+  first_x_assum drule>>
+  rpt (disch_then drule)>>
   strip_tac>>
   rpt xlet_autop>>
   (* help instantiate fill_earliest_spec *)
   qmatch_asmsub_abbrev_tac`NUM (2 * mv) _`>>
   `LIST_REL (OPTION_TYPE NUM) (REPLICATE (2 * mv + 3) NONE)
           (REPLICATE (2 * mv + 3) (Conv (SOME (TypeStamp "None" 2)) []))` by
     simp[LIST_REL_REPLICATE_same,OPTION_TYPE_def]>>
-  drule  fill_earliest_spec>>
+  first_x_assum drule>>
   disch_then drule>>
   strip_tac>>
   simp[Abbr`mv`]>>
-  xlet_autop >>
-  xlet`
-    POSTv lv.
-    ARRAY resv' earliestv' * ARRAY resv arrlsv' * STDIO fs *
-    &(LIST_TYPE NUM (MAP FST (enumerate 1 (enc()))) lv)`
-  >- (
-    xapp_spec (ListProgTheory.map_1_v_thm |> INST_TYPE [alpha |-> ``:num``, beta |-> ``:num # int list``])>>
-    xsimpl>>
-    asm_exists_tac >>simp[]>>
-    qexists_tac`FST`>>
-    qexists_tac`NUM`>>simp[fst_v_thm])>>
   rpt xlet_autop >>
   simp[check_unsat_1_sem_def,check_lpr_unsat_list_def]>>
   qmatch_goalsub_abbrev_tac`check_lpr_list _ _ a b c d`>>
@@ -194,6 +188,7 @@ Proof
       disch_then drule>>
       simp[index_def]>>rw[]>>
       intLib.ARITH_TAC)>>
+    fs[LENGTH_enumerate,rev_enum_full_rev_enumerate]>>
     metis_tac[])>>
   reverse TOP_CASE_TAC>>simp[]
   >- (fs[SUM_TYPE_def]>>xmatch>>err_tac)>>