How to use dependent types with the template system

[Brandon Barker]

Here's an example where I want to create a map with integer values only within a certain range. Is this a crazy thing to do? I'm also not sure if this is something best left to ATS2.

Firstly, it appears I'm not sure how to create a "new" dependent type (highlighted in yellow):

absviewtype gIdxMap

typedef  gIdxMap (n:int) = gIdxMap n

extern

fun gIdxMap_find {n:nat} (mp: &gIdxMap n, k: string): intBtw(0,n) i

extern

fun gIdxMap_free(mp: gIdxMap):<> void

extern

fun gIdxMap_insert {i,n:nat | i < n} (mp: &gIdxMap n, gene: string, ival: intBtw(0,n) i

):<> bool

extern

fun gIdxMap_make_nil(): gIdxMap

local

staload LM = "libats/SATS/linmap_avltree.sats"   

staload _ = "libats/DATS/linmap_avltree.dats"   

assume gIdxMap = {n:nat} $LM.map(string, intBtw(0,n))

in // in of [local]

implement 

gIdxMap_make_nil() = $LM.linmap_make_nil {string, int} () 

implement

gIdxMap_find {n:nat} (mp n, k): intBtw(0,n) i = let

  var res: int?

  val b = $LM.linmap_search (mp, k, lam(x,y) 

    => compare_string_string(x,y), res)

  in 

    if b then let

      prval () = opt_unsome {int} (res)

      in res end 

    else let 

      prval () = opt_unnone {int} (res) 

      in ( (* print(k + "not found\n"); $raise MapKeyNotFound;*) ~1.0) end

  end // end of [gIdxMap_find]

implement

gIdxMap_free(mp) = $LM.linmap_free(mp)

implement

gIdxMap_insert (mp n,gene, ival i) = let

  var rdval: int? 

  val b = $LM.linmap_insert<string,int>

    (mp, gene, dval, lam(x,y) => compare_string_string(x,y),rdval)

  //How does this work?:

  prval () = opt_clear (rdval)

  in b end

end // end of [local]

[gmhwxi]

absviewtype gIdxMap_vtype (n:int)
typedef gIdxMap (n: int) = gIdxMap_vtype (n)

...

assume gIdxMap_vtype(n:int) = $LM.map(string, intBtw(0,n))

[gmhwxi]

'intBtw(0, n) i' is wrong; it should just be 'intBtw(0, n)'.

[Brandon Barker]

Thanks; I used viewdef instead of typedef and that part typechecked. Things are getting a bit tricky when it comes to separating a function definition from its implementation (highlighted). I'd like the static variables associated to function arguments available in the implementation, but "the function argument cannot be ascribed refval types." I could probably hack a way around this using prfuns, but I'm betting there's a more elegant way.

absviewtype gIdxMap_vtype (n:int)

viewdef gIdxMap (n: int) = gIdxMap_vtype (n)

extern

fun gIdxMap_find {n:nat} (mp: &gIdxMap n, k: string): intBtw(~1,n)

extern

fun gIdxMap_free {n:nat} (mp: gIdxMap n):<> void

extern

fun gIdxMap_insert {n:nat} (mp: &gIdxMap n, gene: string, ival: intBtw(~1,n)

):<> bool

extern

fun gIdxMap_make_nil {n:nat} (n:int n): gIdxMap n

local

staload LM = "libats/SATS/linmap_avltree.sats"

staload _ = "libats/DATS/linmap_avltree.dats"

assume gIdxMap_vtype(n:int) = $LM.map(string, intBtw(~1,n))

in // in of [local]

implement

gIdxMap_make_nil {n:int} (n:int n) =

$LM.linmap_make_nil {string, intBtw(~1,n)} ()

implement

gIdxMap_find {n:int} (mp: &gIdxMap n , k) = let

  var res: intBtw(~1,n)

  val b = $LM.linmap_search (mp, k, lam(x,y)

    => compare_string_string(x,y), res)

  in

    if b then let

      prval () = opt_unsome {Int} (res)

      in res end

    else let

      prval () = opt_unnone {Int} (res)

      in ( (* print(k + "not found\n"); $raise MapKeyNotFound;*) ~1) end

  end // end of [gIdxMap_find]

implement

gIdxMap_free(mp) = $LM.linmap_free(mp)

implement

gIdxMap_insert (mp, gene, ival) = let

  var rdval: int?

  val b = $LM.linmap_insert<string,Int>(mp, gene, ival, lam(x,y)

[gmhwxi]

viewdef -> viewtypedef

implement

gIdxMap_find {n:int} (mp: &gIdxMap n , k) = let



changes to

implement
gIdxMap_find {n} (mp, k) = let
(*
the static 'n' is available here.
*)



[Brandon Barker]

Great, I attach a type checking (but untested) version for completeness.  The find function returns a negative 1 if a value is not found in the map, which should probably be changed to used the Option mechanism.

absviewtype gIdxMap_vtype (n:int)

viewdef gIdxMap (n: int) = gIdxMap_vtype (n)

extern

fun gIdxMap_find {n:nat} (mp: &gIdxMap n, k: string): intBtw(~1,n)

extern

fun gIdxMap_free {n:nat} (mp: gIdxMap n):<> void

extern

fun gIdxMap_insert {n:nat} (mp: &gIdxMap n, gene: string, ival: intBtw(~1,n)

):<> bool

extern

fun gIdxMap_make_nil {n:nat} (n:int n): gIdxMap n

local

staload LM = "libats/SATS/linmap_avltree.sats"

staload _ = "libats/DATS/linmap_avltree.dats"

assume gIdxMap_vtype(n:int) = $LM.map(string, intBtw(~1,n))

in // in of [local]

implement

gIdxMap_make_nil {n:int} (n:int n) =

$LM.linmap_make_nil {string, intBtw(~1,n)} ()

implement

gIdxMap_find {n} (mp, k) = let

  var res: intBtw(~1,n)?

  val b = $LM.linmap_search (mp, k, lam(x,y)

    => compare_string_string(x,y), res)

  in

    if b then let

      prval () = opt_unsome {intBtw(~1,n)} (res)

      in res end

    else let

      prval () = opt_unnone {intBtw(~1,n)} (res)

      in ( (* print(k + "not found\n"); $raise MapKeyNotFound; *) ~1) end

  end // end of [gIdxMap_find]

implement

gIdxMap_free(mp) = $LM.linmap_free(mp)

implement

gIdxMap_insert {n} (mp, gene, ival) = let  var rdval: intBtw(~1,n)?

  val b = $LM.linmap_insert<string, intBtw(~1,n)>(mp, gene, ival, lam(x,y)

[gmhwxi]

The comparison should be moved out. Otherwise, it gets created whenever gIdxMap_insert is called.

local

val cmp = lam(x:string,y:string):int =<cloref> compare (x, y)

in

...

end


[Brandon Barker]

Is this advice specific to closures? I often see functions (e.g. fun loop(...)) defined inside of other functions.

[gmhwxi]

Writing something like

fun loop (...): <cloref1> void = ...

does NOT mean that a closure is to be created for loop. It simply means that variables from outside can be used in the body of loop.