A function has three pointer arguments

[master-q]

Forked from https://github.com/metasepi/idiomaticca/issues/20.

[master-q]

New regress test needs proof arguments for loop function.

$ cat regress/noinc/pointer_sort_noarray/main.c
void sort(int *pa, int *pb, int *pc) {
        int temp = 0, flag = 1;

        while (flag == 1) {
                flag = 0;
                if (*pa > *pb) {
                        temp = *pa;
                        *pa = *pb;
                        *pb = temp;
                        flag = 1;
                }
                if (*pb > *pc) {
                        temp = *pb;
                        *pb = *pc;
                        *pc = temp;
                        flag = 1;
                }
        }
}

int main() {
        int a = 3, b = 1, c = 2;
        int *pa, *pb;

        pa = &a;
        pb = &b;
        sort(pa, pb, &c);

        return a * 100 + b * 10 + c * 1 - 123;
}

[master-q]

Above should be translated as following:

#include "share/atspre_staload.hats"

fun sort {l1:addr}{l2:addr}{l3:addr}( i9a_pf_pa : !int @ l1
                                    , i9a_pf_pb : !int @ l2
                                    , i9a_pf_pc : !int @ l3
                                     | pa : ptr(l1), pb : ptr(l2), pc : ptr(l3)) : void =
  let
    var pa: ptr(l1) = pa
    var pc: ptr(l3) = pc
    var pb: ptr(l2) = pb
  in
    let
      var temp: int = 0
      var flag: int = 1

      fun loop_while {l1:addr}{l2:addr}{l3:addr} ( i9a_pf_pa : !int @ l1 , i9a_pf_pb : !int @ l2 , i9a_pf_pc : !int @ l3 | flag : int, pa : ptr(l1), pb : ptr(l2), pc : ptr(l3), temp : int) :
        (int, ptr(l1), ptr(l2), ptr(l3), int) =
        let
          var flag: int = flag
          var pa: ptr(l1) = pa
          var pb: ptr(l2) = pb
          var pc: ptr(l3) = pc
          var temp: int = temp
        in
          if flag = 1 then
            let
              val () = flag := 0
              val () = if !pa > !pb then
                let
                  val () = temp := !pa
                  val () = !pa := !pb
                  val () = !pb := temp
                  val () = flag := 1
                in end
              val () = if !pb > !pc then
                let
                  val () = temp := !pb
                  val () = !pb := !pc
                  val () = !pc := temp
                  val () = flag := 1
                in end
            in
              loop_while(i9a_pf_pa, i9a_pf_pb, i9a_pf_pc | flag, pa, pb, pc, temp)
            end
          else
            (flag, pa, pb, pc, temp)
        end

      val (i9a_flag, i9a_pa, i9a_pb, i9a_pc, i9a_temp) = loop_while(i9a_pf_pa, i9a_pf_pb, i9a_pf_pc | flag, pa, pb, pc, temp)
      val () = flag := i9a_flag
      val () = pa := i9a_pa
      val () = pb := i9a_pb
      val () = pc := i9a_pc
      val () = temp := i9a_temp
    in end
  end

implement main () =
  let
    var a: int = 3
    var b: int = 1
    var c: int = 2
    var pa: ptr
    var pb: ptr
    val () = pa := addr@a
    val () = pb := addr@b
    val () = sort(view@a, view@b, view@c | pa, pb, addr@c)
  in
    a * 100 + b * 10 + c * 1 - 123
  end

[master-q]

iEnvDeclVars should keep ptr type.

[master-q]

interpretCDerivedDeclrArgs should understand CPtrDeclr.

[master-q]

interpretCDerivedDeclrArgs returns both AArgs include proof and [AUni]. Then makeLoop also takes proof and uni.

[master-q]

makeLoop calls usedTypedVars which find vars from iEnvDeclVars. If so, the iEnvDeclVars should keep at-views with ptr type?

[master-q]

• [x] Add {l1:addr}{l2:addr}{l3:addr} to loop_while defined.
• [x] Add i9a_pf_pa, i9a_pf_pb, i9a_pf_pc | to loop_while calling.

[master-q]

Whats is proof or view?

• iEnvDeclVars :: [(String, (AType, Maybe AType))] keeps view type such as Unconsumed (AtExpr (AlexPn 0 0 0) (Named (Unqualified "int")) (StaticVal (Unqualified "l3")))
• iEnvDynViews :: [(String, AExpr)] keeps view expr such as ViewAt (AlexPn 0 0 0) (NamedVal (Unqualified "b"))

[master-q]

Implement following:

iEnvDeclVarsArgs vars =
  (Just $ go [] [] vars, []) -- xxx Need to add AUni

[master-q]

Supported at 6c5ae8835f6619cea720954deaa575b80dd848b9.