Consider following functions(only for asking question) foo_1 and foo_2 :
(* for convenience assume n > 0 *)
extern
fun
foo_1{n:nat | n > 0}
(A : &(@[int][n])) : void
(* for convenience assume n > 0 *)
extern
fun
foo_2{n:nat | n > 0}{l:addr}
(pf : !array_v(int,l,n) | p : ptr (l) ) : void
implement
foo_1{n}(A) =
let
val () = println! (A[0])
val p = addr@A
prval avw = view@A
val () = foo_2(avw | p)
prval () = view@A := avw
in end
implement
foo_2{n}{l} (pf | p) =
let
(* val () = foo_1 (???) *)
prval (pf_at,pf_rest) = array_v_uncons(pf)
val x = ptr_get(pf_at | p)
val () = println! (x)
prval () = pf := array_v_cons(pf_at,pf_rest)
in end
They are called from main0 :
implement main0 () = {
var tarr = @[int]10
val () = foo_1(tarr)
val (pf | p) = (view@tarr | addr@tarr)
val () = foo_2(pf | p)
prval () = view@tarr := pf
}
The parameters to both functions are reference to an array type one is
implicit other is explicit (Am I right ??? ).
In foo_1 I can simply use A[i] to access values of array A.
But I can’t do so in foo_2 , so from given arguments of foo_2 , how do I
create a binding
say B so that I can use B[i] in foo_2 function using cast or anything else
?
Say I want to call foo_1 from foo_2 , so how would I do that ?
val () = foo_1 (!p)On Monday, February 24, 2014 9:25:03 AM UTC-5, gmhwxi wrote:
In foo_1, you can use A.[i] (instead of A[i]). In foo_2, please use p->[i]
On Monday, February 24, 2014 9:12:45 AM UTC-5, chotu s wrote:
For now please ignore the non terminating mutual recursion that may
happen if foo_1 is called from foo_2 in above code (assume that they
terminate or something like that )
On Mon, Feb 24, 2014 at 7:38 PM, chotu s cho...@gmail.com wrote:
Consider following functions(only for asking question) foo_1 and foo_2 :
(* for convenience assume n > 0 *)
extern
fun
foo_1{n:nat | n > 0}
(A : &(@[int][n])) : void
(* for convenience assume n > 0 *)
extern
fun
foo_2{n:nat | n > 0}{l:addr}
(pf : !array_v(int,l,n) | p : ptr (l) ) : void
implement
foo_1{n}(A) =
let
val () = println! (A[0])
val p = addr@A
prval avw = view@A
val () = foo_2(avw | p)
prval () = view@A := avw
in end
implement
foo_2{n}{l} (pf | p) =
let
(* val () = foo_1 (???) *)
prval (pf_at,pf_rest) = array_v_uncons(pf)
val x = ptr_get(pf_at | p)
val () = println! (x)
prval () = pf := array_v_cons(pf_at,pf_rest)
in end
They are called from main0 :
implement main0 () = {
var tarr = @[int]10
val () = foo_1(tarr)
val (pf | p) = (view@tarr | addr@tarr)
val () = foo_2(pf | p)
prval () = view@tarr := pf
}
The parameters to both functions are reference to an array type one is
implicit other is explicit (Am I right ??? ).
In foo_1 I can simply use A[i] to access values of array A.
But I can’t do so in foo_2 , so from given arguments of foo_2 , how do I
create a binding
say B so that I can use B[i] in foo_2 function using cast or anything
else ?
Say I want to call foo_1 from foo_2 , so how would I do that ?
In foo_1, you can use A.[i] (instead of A[i]). In foo_2, please use p->[i]On Monday, February 24, 2014 9:12:45 AM UTC-5, chotu s wrote:
For now please ignore the non terminating mutual recursion that may
happen if foo_1 is called from foo_2 in above code (assume that they
terminate or something like that )
On Mon, Feb 24, 2014 at 7:38 PM, chotu s <cho...@gmail.com <javascript:>>wrote:
Consider following functions(only for asking question) foo_1 and foo_2 :
(* for convenience assume n > 0 *)
extern
fun
foo_1{n:nat | n > 0}
(A : &(@[int][n])) : void
(* for convenience assume n > 0 *)
extern
fun
foo_2{n:nat | n > 0}{l:addr}
(pf : !array_v(int,l,n) | p : ptr (l) ) : void
implement
foo_1{n}(A) =
let
val () = println! (A[0])
val p = addr@A
prval avw = view@A
val () = foo_2(avw | p)
prval () = view@A := avw
in end
implement
foo_2{n}{l} (pf | p) =
let
(* val () = foo_1 (???) *)
prval (pf_at,pf_rest) = array_v_uncons(pf)
val x = ptr_get(pf_at | p)
val () = println! (x)
prval () = pf := array_v_cons(pf_at,pf_rest)
in end
They are called from main0 :
implement main0 () = {
var tarr = @[int]10
val () = foo_1(tarr)
val (pf | p) = (view@tarr | addr@tarr)
val () = foo_2(pf | p)
prval () = view@tarr := pf
}
The parameters to both functions are reference to an array type one is
implicit other is explicit (Am I right ??? ).
In foo_1 I can simply use A[i] to access values of array A.
But I can’t do so in foo_2 , so from given arguments of foo_2 , how do I
create a binding
say B so that I can use B[i] in foo_2 function using cast or anything
else ?
Say I want to call foo_1 from foo_2 , so how would I do that ?
Thanks , I think I did not knew about p->[i] . I’ll try to use A.[i] from
now on accessing elements of an array.
One last question is it possible to call foo_1(???) from foo_2 ?On Mon, Feb 24, 2014 at 7:55 PM, gmhwxi gmh...@gmail.com wrote:
In foo_1, you can use A.[i] (instead of A[i]). In foo_2, please use p->[i]
On Monday, February 24, 2014 9:12:45 AM UTC-5, chotu s wrote:
For now please ignore the non terminating mutual recursion that may
happen if foo_1 is called from foo_2 in above code (assume that they
terminate or something like that )
On Mon, Feb 24, 2014 at 7:38 PM, chotu s cho...@gmail.com wrote:
Consider following functions(only for asking question) foo_1 and foo_2 :
(* for convenience assume n > 0 *)
extern
fun
foo_1{n:nat | n > 0}
(A : &(@[int][n])) : void
(* for convenience assume n > 0 *)
extern
fun
foo_2{n:nat | n > 0}{l:addr}
(pf : !array_v(int,l,n) | p : ptr (l) ) : void
implement
foo_1{n}(A) =
let
val () = println! (A[0])
val p = addr@A
prval avw = view@A
val () = foo_2(avw | p)
prval () = view@A := avw
in end
implement
foo_2{n}{l} (pf | p) =
let
(* val () = foo_1 (???) *)
prval (pf_at,pf_rest) = array_v_uncons(pf)
val x = ptr_get(pf_at | p)
val () = println! (x)
prval () = pf := array_v_cons(pf_at,pf_rest)
in end
They are called from main0 :
implement main0 () = {
var tarr = @[int]10
val () = foo_1(tarr)
val (pf | p) = (view@tarr | addr@tarr)
val () = foo_2(pf | p)
prval () = view@tarr := pf
}
The parameters to both functions are reference to an array type one is
implicit other is explicit (Am I right ??? ).
In foo_1 I can simply use A[i] to access values of array A.
But I can’t do so in foo_2 , so from given arguments of foo_2 , how do I
create a binding
say B so that I can use B[i] in foo_2 function using cast or anything
else ?
Say I want to call foo_1 from foo_2 , so how would I do that ?
Thanks
–
You received this message because you are subscribed to the Google
Groups “ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send
an email to ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
Great, foo_1(!p) works . I don’t think I could have come up with this(using
!p in the arg) real soon . ThanksOn Mon, Feb 24, 2014 at 8:22 PM, gmhwxi gmh...@gmail.com wrote:
Too call foo_1 in foo_2:
val () = foo_1 (!p)
On Monday, February 24, 2014 9:25:03 AM UTC-5, gmhwxi wrote:
In foo_1, you can use A.[i] (instead of A[i]). In foo_2, please use p->[i]
On Monday, February 24, 2014 9:12:45 AM UTC-5, chotu s wrote:
For now please ignore the non terminating mutual recursion that may
happen if foo_1 is called from foo_2 in above code (assume that they
terminate or something like that )
On Mon, Feb 24, 2014 at 7:38 PM, chotu s cho...@gmail.com wrote:
Consider following functions(only for asking question) foo_1 and foo_2 :
(* for convenience assume n > 0 *)
extern
fun
foo_1{n:nat | n > 0}
(A : &(@[int][n])) : void
(* for convenience assume n > 0 *)
extern
fun
foo_2{n:nat | n > 0}{l:addr}
(pf : !array_v(int,l,n) | p : ptr (l) ) : void
implement
foo_1{n}(A) =
let
val () = println! (A[0])
val p = addr@A
prval avw = view@A
val () = foo_2(avw | p)
prval () = view@A := avw
in end
implement
foo_2{n}{l} (pf | p) =
let
(* val () = foo_1 (???) *)
prval (pf_at,pf_rest) = array_v_uncons(pf)
val x = ptr_get(pf_at | p)
val () = println! (x)
prval () = pf := array_v_cons(pf_at,pf_rest)
in end
They are called from main0 :
implement main0 () = {
var tarr = @[int]10
val () = foo_1(tarr)
val (pf | p) = (view@tarr | addr@tarr)
val () = foo_2(pf | p)
prval () = view@tarr := pf
}
The parameters to both functions are reference to an array type one is
implicit other is explicit (Am I right ??? ).
In foo_1 I can simply use A[i] to access values of array A.
But I can’t do so in foo_2 , so from given arguments of foo_2 , how do
I create a binding
say B so that I can use B[i] in foo_2 function using cast or anything
else ?
Say I want to call foo_1 from foo_2 , so how would I do that ?
Thanks
–
You received this message because you are subscribed to the Google
Groups “ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send
an email to ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/
msgid/ats-lang-users/89e6dc1c-1da3-4a8d-81af-42b7d517f487% 40googlegroups.com.
For now please ignore the non terminating mutual recursion that may happen
if foo_1 is called from foo_2 in above code (assume that they terminate or
something like that )On Mon, Feb 24, 2014 at 7:38 PM, chotu s chot...@gmail.com wrote:
Consider following functions(only for asking question) foo_1 and foo_2 :
(* for convenience assume n > 0 *)
extern
fun
foo_1{n:nat | n > 0}
(A : &(@[int][n])) : void
(* for convenience assume n > 0 *)
extern
fun
foo_2{n:nat | n > 0}{l:addr}
(pf : !array_v(int,l,n) | p : ptr (l) ) : void
implement
foo_1{n}(A) =
let
val () = println! (A[0])
val p = addr@A
prval avw = view@A
val () = foo_2(avw | p)
prval () = view@A := avw
in end
implement
foo_2{n}{l} (pf | p) =
let
(* val () = foo_1 (???) *)
prval (pf_at,pf_rest) = array_v_uncons(pf)
val x = ptr_get(pf_at | p)
val () = println! (x)
prval () = pf := array_v_cons(pf_at,pf_rest)
in end
They are called from main0 :
implement main0 () = {
var tarr = @[int]10
val () = foo_1(tarr)
val (pf | p) = (view@tarr | addr@tarr)
val () = foo_2(pf | p)
prval () = view@tarr := pf
}
The parameters to both functions are reference to an array type one is
implicit other is explicit (Am I right ??? ).
In foo_1 I can simply use A[i] to access values of array A.
But I can’t do so in foo_2 , so from given arguments of foo_2 , how do I
create a binding
say B so that I can use B[i] in foo_2 function using cast or anything else
?
Say I want to call foo_1 from foo_2 , so how would I do that ?
. ThanksOn Mon, Feb 24, 2014 at 8:22 PM, gmhwxi