Skip to content

Instantly share code, notes, and snippets.

@bbarker

bbarker/linset_ats1libtest.dats Secret

Last active January 3, 2016 07:19
Download ZIP

Revisions

  1. bbarker revised this gist Jan 16, 2014. 1 changed file with 8 additions and 1 deletion.
    9 changes: 8 additions & 1 deletion linset_ats1libtest.dats
    View file
    Original file line number Diff line number Diff line change
    @@ -86,7 +86,14 @@ fun loop
    In this example, x1 is always less than x2. When xs1 is initially
    folded (last call to loop before xs1 => list_vt_nil), it includes
    x1 = 3 (last member of xs1) and !p_xs1 = {4, 5, 6} (the entire
    second list, since res := xs2 according to the list_nil case.) *)
    second list, since res := xs2 according to the list_nil case --
    Remember, !p_xs1 is the res argument in loop in this case).
    Nothing ever needs to be freed in this case; the two input lists
    are disjoint, so the view is altered to include all the data in both
    lists.
    In ATS2, since we do not need (and can't be default) fold this dataviewtype,
    we instead assign res with a list_vt_cons. *)
    case+ xs2 of
    | list_vt_cons (x2, !p_xs2) => let
    val sgn = compare_elt_elt<a> (x1, x2, cmp)
  2. bbarker revised this gist Jan 16, 2014. 1 changed file with 5 additions and 3 deletions.
    8 changes: 5 additions & 3 deletions linset_ats1libtest.dats
    View file
    Original file line number Diff line number Diff line change
    @@ -82,9 +82,11 @@ fun loop
    xs1: list_vt (a, n1), xs2: list_vt (a, n2), res: &res? >> res
    ) :<cloref> (* normally <cloref> *) void = // how to combine <!ref> and <cloref>?
    case+ xs1 of
    | list_vt_cons (x1, !p_xs1) => (
    // p_xs1 is a reference, and can be changed; when xs1 is folded,
    // and subsequently res is updated to contain xs1, res may grow in size.
    | list_vt_cons (x1, !p_xs1) => ( (*
    In this example, x1 is always less than x2. When xs1 is initially
    folded (last call to loop before xs1 => list_vt_nil), it includes
    x1 = 3 (last member of xs1) and !p_xs1 = {4, 5, 6} (the entire
    second list, since res := xs2 according to the list_nil case.) *)
    case+ xs2 of
    | list_vt_cons (x2, !p_xs2) => let
    val sgn = compare_elt_elt<a> (x1, x2, cmp)
  3. bbarker revised this gist Jan 16, 2014. 1 changed file with 23 additions and 15 deletions.
    38 changes: 23 additions & 15 deletions linset_ats1libtest.dats
    View file
    Original file line number Diff line number Diff line change
    @@ -41,6 +41,12 @@ fun{a:t0p} print_val(x: a):<!ref> void
    implement
    print_val<int> (x) = print(x)

    fn{a:t0p} print_lvt0(xsl: !List_vt (a)):<!ref> void =
    begin (
    list_vt_foreach_fun<a> (xsl, lam x =<!ref> (print_val<a> (x); print ' '));
    print_newline();
    ) end

    fn{a:t0p} print_lvt{n:nat}(xsl: !list_vt (a, n)):<!ref> void =
    begin (
    list_vt_foreach_fun<a> (xsl, lam x =<!ref> (print_val<a> (x); print ' '));
    @@ -49,7 +55,6 @@ print_newline();

    fun{a:t0p} print_linset(xs: !set (a)): void =
    let
    //
    // Not ideal to make a copy just to print
    // (just for testing purposes)
    val xsl = linset_listize(xs)
    @@ -78,36 +83,45 @@ fun loop
    ) :<cloref> (* normally <cloref> *) void = // how to combine <!ref> and <cloref>?
    case+ xs1 of
    | list_vt_cons (x1, !p_xs1) => (
    // p_xs1 is a reference, and can be changed; when xs1 is folded,
    // and subsequently res is updated to contain xs1, res may grow in size.
    case+ xs2 of
    | list_vt_cons (x2, !p_xs2) => let
    val sgn = compare_elt_elt<a> (x1, x2, cmp)
    in
    if sgn < 0 then let
    val xs11 = !p_xs1
    val () = $effmask_all(print_lvt<a> (xs11))
    val () = $effmask_all(print "xs11: ") //Test
    val () = $effmask_all(print_lvt<a> (xs11)) //Test
    prval () = fold@ {a} (xs2)
    val () = loop (xs11, xs2, !p_xs1)
    prval () = fold@ {a} (xs1)
    in
    res := xs1
    end else if sgn > 0 then let
    in (
    res := xs1;
    $effmask_all(print "res: "); //Test
    $effmask_all(print_lvt0<a> (res)) //Test
    ) end else if sgn > 0 then let
    prval () = fold@ {a} (xs1)
    val xs21 = !p_xs2
    val () = $effmask_all(print "xs21: ") //Test
    val () = $effmask_all(print_lvt<a> (xs21)) //Test
    val () = loop (xs1, xs21, !p_xs2)
    prval () = fold@ (xs2)
    in
    res := xs2
    end else let // x1 = x2
    val xs11 = !p_xs1
    val xs21 = !p_xs2
    val () = $effmask_all(print "xs11 ==: ") //Test
    val () = $effmask_all(print_lvt<a> (xs11)) //Test
    val () = $effmask_all(print "xs21 ==: ") //Test
    val () = $effmask_all(print_lvt<a> (xs21)) //Test
    val () = free@ {a}{0} (xs2)
    val () = loop (xs11, xs21, !p_xs1)
    prval () = fold@ (xs1)
    in (
    // print_lvt(xs1);
    // print_lvt(xs2);
    in
    res := xs1
    ) end // end of [if]
    end // end of [if]
    end // end of [list_vt_cons]
    | ~list_vt_nil () => (fold@ (xs1); res := xs1)
    ) // end of [list_vt_cons]
    @@ -122,12 +136,6 @@ end // end of [linset_union]
    implement
    $LS.compare_elt_elt<int> (x1, x2, _(*cmp*)) =
    if x1 < x2 then ~1 else if x1 > x2 then 1 else 0

    (*
    fun{a:vt0p}
    list_vt_foreach_fun {n:int} {f:eff}
    (xs: !list_vt (a, n), f: (&a) -<fun,f> void):<f> void
    *)

    implement main () =
    let
  4. bbarker revised this gist Jan 15, 2014. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions linset_ats1libtest.dats
    View file
    Original file line number Diff line number Diff line change
    @@ -41,8 +41,8 @@ fun{a:t0p} print_val(x: a):<!ref> void
    implement
    print_val<int> (x) = print(x)

    fn{a:t0p} print_lvt(xsl: !List_vt (a)):<!ref> void =
    begin ( // how do we inherit function effects in lam?:
    fn{a:t0p} print_lvt{n:nat}(xsl: !list_vt (a, n)):<!ref> void =
    begin (
    list_vt_foreach_fun<a> (xsl, lam x =<!ref> (print_val<a> (x); print ' '));
    print_newline();
    ) end
  5. bbarker revised this gist Jan 15, 2014. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion linset_ats1libtest.dats
    View file
    Original file line number Diff line number Diff line change
    @@ -42,7 +42,7 @@ implement
    print_val<int> (x) = print(x)

    fn{a:t0p} print_lvt(xsl: !List_vt (a)):<!ref> void =
    begin (
    begin ( // how do we inherit function effects in lam?:
    list_vt_foreach_fun<a> (xsl, lam x =<!ref> (print_val<a> (x); print ' '));
    print_newline();
    ) end
  6. bbarker revised this gist Jan 15, 2014. 1 changed file with 3 additions and 3 deletions.
    6 changes: 3 additions & 3 deletions linset_ats1libtest.dats
    View file
    Original file line number Diff line number Diff line change
    @@ -65,7 +65,7 @@ fn cmp (x1: int, x2: int):<cloref> Sgn = compare (x1, x2)

    extern
    fun{a:t@ype} my_linset_union
    (xs1: set a, xs2: set a, cmp: cmp a):<!ref> (* normally <> *) set (a)
    (xs1: set a, xs2: set a, cmp: cmp a):<> (* normally <> *) set (a)

    implement{a}
    my_linset_union
    @@ -75,7 +75,7 @@ viewtypedef res = List_vt (a)
    fun loop
    {n1,n2:nat} .<n1+n2>. (
    xs1: list_vt (a, n1), xs2: list_vt (a, n2), res: &res? >> res
    ) :<!ref,clo> (* normally <cloref> *) void = // how to combine <!ref> and <cloref>?
    ) :<cloref> (* normally <cloref> *) void = // how to combine <!ref> and <cloref>?
    case+ xs1 of
    | list_vt_cons (x1, !p_xs1) => (
    case+ xs2 of
    @@ -84,7 +84,7 @@ fun loop
    in
    if sgn < 0 then let
    val xs11 = !p_xs1
    //val () = print_lvt<a> (xs11)
    val () = $effmask_all(print_lvt<a> (xs11))
    prval () = fold@ {a} (xs2)
    val () = loop (xs11, xs2, !p_xs1)
    prval () = fold@ {a} (xs1)
  7. bbarker revised this gist Jan 15, 2014. 1 changed file with 1 addition and 3 deletions.
    4 changes: 1 addition & 3 deletions linset_ats1libtest.dats
    View file
    Original file line number Diff line number Diff line change
    @@ -25,7 +25,6 @@ staload _(*anon*) = "prelude/DATS/reference.dats"
    staload LS = "libats/SATS/linset_listord.sats"
    staload LVT = "prelude/SATS/list_vt.sats"


    // defined in linset_listord.sats:
    //absviewtype
    //set_t0ype_viewtype (elt: t@ype+)
    @@ -48,7 +47,6 @@ list_vt_foreach_fun<a> (xsl, lam x =<!ref> (print_val<a> (x); print ' '));
    print_newline();
    ) end


    fun{a:t0p} print_linset(xs: !set (a)): void =
    let
    //
    @@ -77,7 +75,7 @@ viewtypedef res = List_vt (a)
    fun loop
    {n1,n2:nat} .<n1+n2>. (
    xs1: list_vt (a, n1), xs2: list_vt (a, n2), res: &res? >> res
    ) :<!ref> (* normally <cloref> *) void = // how to combine <!ref> and <cloref>?
    ) :<!ref,clo> (* normally <cloref> *) void = // how to combine <!ref> and <cloref>?
    case+ xs1 of
    | list_vt_cons (x1, !p_xs1) => (
    case+ xs2 of
  8. bbarker revised this gist Jan 15, 2014. 1 changed file with 3 additions and 5 deletions.
    8 changes: 3 additions & 5 deletions linset_ats1libtest.dats
    View file
    Original file line number Diff line number Diff line change
    @@ -36,7 +36,6 @@ staload LVT = "prelude/SATS/list_vt.sats"

    (**** Print Functions *****)


    extern
    fun{a:t0p} print_val(x: a):<!ref> void

    @@ -64,6 +63,8 @@ list_vt_free (xsl);

    (**** End Print Functions *****)

    fn cmp (x1: int, x2: int):<cloref> Sgn = compare (x1, x2)

    extern
    fun{a:t@ype} my_linset_union
    (xs1: set a, xs2: set a, cmp: cmp a):<!ref> (* normally <> *) set (a)
    @@ -85,7 +86,7 @@ fun loop
    in
    if sgn < 0 then let
    val xs11 = !p_xs1
    val () = print_lvt<a> (xs11)
    //val () = print_lvt<a> (xs11)
    prval () = fold@ {a} (xs2)
    val () = loop (xs11, xs2, !p_xs1)
    prval () = fold@ {a} (xs1)
    @@ -124,14 +125,11 @@ implement
    $LS.compare_elt_elt<int> (x1, x2, _(*cmp*)) =
    if x1 < x2 then ~1 else if x1 > x2 then 1 else 0


    (*
    fun{a:vt0p}
    list_vt_foreach_fun {n:int} {f:eff}
    (xs: !list_vt (a, n), f: (&a) -<fun,f> void):<f> void
    *)

    fn cmp (x1: int, x2: int):<cloref> Sgn = compare (x1, x2)

    implement main () =
    let
  9. bbarker revised this gist Jan 15, 2014. 1 changed file with 0 additions and 4 deletions.
    4 changes: 0 additions & 4 deletions linset_ats1libtest.dats
    View file
    Original file line number Diff line number Diff line change
    @@ -19,10 +19,6 @@ staload _(*anon*) = "prelude/DATS/pointer.dats"
    staload _(*anon*) = "prelude/DATS/reference.dats"
    //


    staload
    _(*anon*) = "prelude/DATS/list_vt.dats"

    (* ****** ****** *)

    #include "libats/DATS/linset_listord.dats"
  10. bbarker created this gist Jan 15, 2014.
    160 changes: 160 additions & 0 deletions linset_ats1libtest.dats
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,160 @@
    //
    staload _(*anon*) = "libc/SATS/stdio.sats"
    //
    staload _(*anon*) = "prelude/DATS/array.dats"
    staload _(*anon*) = "prelude/DATS/array0.dats"
    //
    staload _(*anon*) = "prelude/DATS/list.dats"
    staload _(*anon*) = "prelude/DATS/list0.dats"
    staload _(*anon*) = "prelude/DATS/list_vt.dats"
    //
    staload _(*anon*) = "prelude/DATS/matrix.dats"
    staload _(*anon*) = "prelude/DATS/matrix0.dats"
    //
    staload _(*anon*) = "prelude/DATS/option.dats"
    staload _(*anon*) = "prelude/DATS/option0.dats"
    //
    staload _(*anon*) = "prelude/DATS/pointer.dats"
    //
    staload _(*anon*) = "prelude/DATS/reference.dats"
    //


    staload
    _(*anon*) = "prelude/DATS/list_vt.dats"

    (* ****** ****** *)

    #include "libats/DATS/linset_listord.dats"
    staload LS = "libats/SATS/linset_listord.sats"
    staload LVT = "prelude/SATS/list_vt.sats"


    // defined in linset_listord.sats:
    //absviewtype
    //set_t0ype_viewtype (elt: t@ype+)
    //stadef set = set_t0ype_viewtype

    //assume
    //set_t0ype_viewtype (elt: t@ype) = List_vt (elt)

    (**** Print Functions *****)


    extern
    fun{a:t0p} print_val(x: a):<!ref> void

    implement
    print_val<int> (x) = print(x)

    fn{a:t0p} print_lvt(xsl: !List_vt (a)):<!ref> void =
    begin (
    list_vt_foreach_fun<a> (xsl, lam x =<!ref> (print_val<a> (x); print ' '));
    print_newline();
    ) end


    fun{a:t0p} print_linset(xs: !set (a)): void =
    let
    //
    // Not ideal to make a copy just to print
    // (just for testing purposes)
    val xsl = linset_listize(xs)
    //
    in (
    print_lvt(xsl);
    list_vt_free (xsl);
    ) end

    (**** End Print Functions *****)

    extern
    fun{a:t@ype} my_linset_union
    (xs1: set a, xs2: set a, cmp: cmp a):<!ref> (* normally <> *) set (a)

    implement{a}
    my_linset_union
    (xs1, xs2, cmp) = let
    //
    viewtypedef res = List_vt (a)
    fun loop
    {n1,n2:nat} .<n1+n2>. (
    xs1: list_vt (a, n1), xs2: list_vt (a, n2), res: &res? >> res
    ) :<!ref> (* normally <cloref> *) void = // how to combine <!ref> and <cloref>?
    case+ xs1 of
    | list_vt_cons (x1, !p_xs1) => (
    case+ xs2 of
    | list_vt_cons (x2, !p_xs2) => let
    val sgn = compare_elt_elt<a> (x1, x2, cmp)
    in
    if sgn < 0 then let
    val xs11 = !p_xs1
    val () = print_lvt<a> (xs11)
    prval () = fold@ {a} (xs2)
    val () = loop (xs11, xs2, !p_xs1)
    prval () = fold@ {a} (xs1)
    in
    res := xs1
    end else if sgn > 0 then let
    prval () = fold@ {a} (xs1)
    val xs21 = !p_xs2
    val () = loop (xs1, xs21, !p_xs2)
    prval () = fold@ (xs2)
    in
    res := xs2
    end else let // x1 = x2
    val xs11 = !p_xs1
    val xs21 = !p_xs2
    val () = free@ {a}{0} (xs2)
    val () = loop (xs11, xs21, !p_xs1)
    prval () = fold@ (xs1)
    in (
    // print_lvt(xs1);
    // print_lvt(xs2);
    res := xs1
    ) end // end of [if]
    end // end of [list_vt_cons]
    | ~list_vt_nil () => (fold@ (xs1); res := xs1)
    ) // end of [list_vt_cons]
    | ~list_vt_nil () => (res := xs2)
    // end of [loop]
    var res: res // uninitialized
    val () = loop (xs1, xs2, res)
    in
    res
    end // end of [linset_union]

    implement
    $LS.compare_elt_elt<int> (x1, x2, _(*cmp*)) =
    if x1 < x2 then ~1 else if x1 > x2 then 1 else 0


    (*
    fun{a:vt0p}
    list_vt_foreach_fun {n:int} {f:eff}
    (xs: !list_vt (a, n), f: (&a) -<fun,f> void):<f> void
    *)

    fn cmp (x1: int, x2: int):<cloref> Sgn = compare (x1, x2)

    implement main () =
    let
    val xmin = 1
    val xmax = 3
    val ymin = 4
    val ymax = 6
    var ints1: $LS.set (int) = $LS.linset_make_nil ()
    var ints2: $LS.set (int) = $LS.linset_make_nil ()
    var i: int
    val () = for (i := xmin; i <= xmax; i := i+1) {
    val _ = $LS.linset_insert<int> (ints1, i, cmp)
    } (* end of [for] *)
    val () = for (i := ymin; i <= ymax; i := i+1) {
    val _ = $LS.linset_insert<int> (ints2, i, cmp)
    } (* end of [for] *)
    val ints_union = my_linset_union (ints1, ints2, cmp)
    val () = print_linset<int>(ints_union)
    val () = $LS.linset_free (ints_union)
    in
    print ("On to figuring out the algorithm!"); print_newline ()
    end // end of [main]