Zero et Top

lib/Cst/cst.ml

@@ -20,6 +20,8 @@ type value =
         loc : position
     }
 
+  | CoTop of {loc : position}
+
   | Bindcc of {
       typ : typ option;
       pol : polarity option;
@@ -62,6 +64,8 @@ and stack =
 
   | Ret of { loc : position }
 
+  | CoZero of {loc : position}
+
   | CoBind of {
       name : var;
       typ : typ option;
@@ -177,11 +181,11 @@ type program = program_item list
 
 let loc_of_value = function
   | Var {loc;_} | Bindcc {loc;_} | Box {loc; _} | Cons {loc;_} | Destr {loc;_}
-  | Macro_box {loc; _} | Macro_fun {loc; _} -> loc
+  | Macro_box {loc; _} | Macro_fun {loc; _} | CoTop {loc}-> loc
 
 let loc_of_stack = function
-  | Ret {loc} | CoBind {loc;_} | CoBox {loc;_} | CoCons {loc;_} | CoDestr {loc;_} ->
-    loc
+  | Ret {loc} | CoBind {loc;_} | CoBox {loc;_} | CoCons {loc;_} | CoZero {loc}
+  | CoDestr {loc;_} -> loc
 
 let loc_of_cmd = function
   | Command {loc;_} | Macro_term {loc;_} | Macro_env {loc;_} | Macro_match_val {loc;_}
@@ -196,6 +200,7 @@ let loc_of_item = function
 
 module V = struct
   type t = value
+  let cotop ?loc:(loc = dummy_pos) () = CoTop {loc}
   let var ?loc:(loc = dummy_pos) x = Var {node = x; loc}
   let bindcc ?loc:(loc = dummy_pos) ?pol:pol typ cmd = Bindcc {pol; typ; cmd; loc}
   let box ?loc:(loc = dummy_pos) kind typ cmd = Box {kind; typ; cmd; loc}
@@ -208,6 +213,7 @@ end
 
 module S = struct
   type t = stack
+  let cozero ?loc:(loc = dummy_pos) () = CoZero {loc}
   let ret ?loc:(loc = dummy_pos) ()= Ret {loc}
   let bind ?loc:(loc = dummy_pos) ?pol:pol typ name cmd = CoBind {pol; typ; name; cmd; loc}
   let box ?loc:(loc = dummy_pos) kind stk = CoBox {kind; stk; loc}

lib/Cst/cst.mli

@@ -18,6 +18,7 @@ type value =
       node : var;
       loc : position;
     }
+  | CoTop of {loc : position}
   | Bindcc of {
       typ : typ option;
       pol : polarity option;
@@ -54,6 +55,7 @@ and stack =
   | Ret of {
       loc : position;
     }
+  | CoZero of {loc : position}
   | CoBind of {
       name : var;
       typ : typ option;
@@ -163,6 +165,7 @@ val loc_of_item : program_item -> position
 
 module V : sig
   type t = value
+  val cotop : ?loc:position -> unit -> value
   val var : ?loc:position -> var -> value
   val bindcc : ?loc:position -> ?pol:polarity -> typ option -> command -> value
   val box : ?loc:position -> box_kind -> typ option -> command -> value
@@ -174,6 +177,7 @@ end
 
 module S : sig
   type t = stack
+  val cozero : ?loc:position -> unit -> stack
   val ret : ?loc:position -> unit -> stack
   val bind : ?loc:position -> ?pol:polarity -> typ option -> var -> command -> stack
   val box : ?loc:position -> box_kind -> stack -> stack

lib/Cst/cstPrettyPrinter.ml

@@ -115,6 +115,8 @@ let rec pp_value fmt = function
 
   | Var v -> pp_var fmt v.node
 
+  | CoTop _ -> fprintf fmt "GOT_TOP"
+
   | Bindcc {pol; typ; cmd; _} ->
     fprintf fmt "@[<hov 2>bind/cc%a%a ->@ %a@]"
       pp_pol_annot pol
@@ -152,6 +154,8 @@ and pp_stack_trail fmt s =
 
   | Ret _ -> fprintf fmt "@,.ret()"
 
+  | CoZero _ -> fprintf fmt "@,.GOT_ZERO()"
+
   | CoBind {pol; name; typ; cmd; _} ->
     fprintf fmt "@,@[<hov 2>.bind%a %a ->@ %a@]"
       pp_pol_annot pol

lib/Cst/lexer.mll

@@ -41,6 +41,9 @@ rule token = parse
   | "in" {IN}
   | "do" {DO}
 
+  | "GOT_ZERO" {GOT_ZERO}
+  | "GOT_TOP" {GOT_TOP}
+
   | "box" {BOX}
   | "unbox" {UNBOX}
   | "lin" {LINEAR}

lib/Cst/parser.mly

@@ -12,6 +12,7 @@
 %token COLUMN PLUS EQUAL MINUS DOT ARROW COMMA SLASH META
 %token LPAREN RPAREN
 %token STEP INTO WITH BIND BINDCC MATCH CASE RET END THIS IN DO
+%token GOT_TOP GOT_ZERO
 %token BOX UNBOX LINEAR AFFINE EXP
 %token TUPPLE INJ CALL PROJ LEFT RIGHT YES NO
 %token UNIT ZERO PROD SUM FUN CHOICE TOP BOTTOM SHIFT
@@ -133,6 +134,8 @@ cont_annot:
 value:
   | v = var
     {V.var ~loc:(position $symbolstartpos $endpos) v}
+  | GOT_TOP
+    {V.cotop ~loc:(position $symbolstartpos $endpos) ()}
   | c = value_cons
     {V.cons ~loc:(position $symbolstartpos $endpos) c}
   | BOX LPAREN kind = boxkind RPAREN typ = cont_annot ARROW cmd = cmd
@@ -176,6 +179,8 @@ stack:
   | THIS DOT stk = stk_trail {stk}
 
 stk_trail:
+  | GOT_ZERO LPAREN RPAREN
+    {S.cozero ~loc:(position $symbolstartpos $endpos) ()}
   | RET LPAREN RPAREN
     {S.ret ~loc:(position $symbolstartpos $endpos) ()}
   | CALL LPAREN xs = separated_list(COMMA, value) RPAREN DOT stk = stk_trail

lib/Intern/intern_prettyPrinter.ml

@@ -146,6 +146,8 @@ and pp_pre_value fmt = function
 
   | Var v -> pp_var fmt v
 
+  | CoTop -> fprintf fmt "GOT_TOP"
+
   | Bindcc {pol; bind=(_,typ); cmd; _} ->
     fprintf fmt "@[<v 2>bind/cc%a%a ->@ %a@]"
       pp_pol_annot pol
@@ -181,6 +183,8 @@ and pp_pre_stack_trail fmt s =
 
   | Ret -> fprintf fmt "@,.ret()"
 
+  | CoZero -> fprintf fmt "@,.GOT_ZERO"
+
   | CoBind {pol; bind = (name, typ); cmd; _} ->
     fprintf fmt "@,@[<v 2>.bind%a %a ->@ %a@]"
       pp_pol_annot pol

lib/Intern/intern_prog.ml

@@ -74,6 +74,8 @@ let intern_definition env def =
         | Not_found -> fail_undefined_var node loc
       end
 
+    | Cst.CoTop {loc} -> MetaVal {node = CoTop; loc; val_typ = cons top}
+
     | Cst.Bindcc {typ; pol; cmd; loc} ->
       let pol = intern_pol pol in
       let val_typ = intern_type_annot env typ in
@@ -138,6 +140,9 @@ let intern_definition env def =
     | Cst.Ret {loc} ->
       MetaStack {loc; cont_typ = final_typ; final_typ; node = Ret}
 
+    | Cst.CoZero {loc} ->
+      MetaStack {loc; cont_typ = cons zero; final_typ; node = CoZero}
+
     | Cst.CoBind {loc; name; typ; pol; cmd} ->
       let var = Var.of_string name in
       let cont_typ = intern_type_annot env typ in

lib/Reduction/reduct.ml

@@ -142,6 +142,8 @@ let reduct_head_once prog : runtime_prog =
         else fail_malformed_program prog
     end
 
+  | CoTop, _ | _, CoZero -> raise Internal_No_root_reduction
+
   | _ -> fail_malformed_program prog
 
 let head_normal_form prog =
@@ -152,7 +154,7 @@ let head_normal_form prog =
   try loop () with Internal_No_root_reduction -> !prog
 
 let rec val_nf prog v = match v with
-  | Var _ -> v
+  | Var _ | CoTop -> v
   | Bindcc {bind; pol; cmd} ->
     let prog' = cmd_nf {prog with cont = []; curr = cmd} in
     Bindcc {bind; pol; cmd = prog'.curr}
@@ -163,7 +165,7 @@ let rec val_nf prog v = match v with
   | Destr copatts -> Destr (List.map (copatt_nf prog) copatts)
 
 and stack_nf prog stk = match stk with
-  | Ret -> Ret
+  | Ret | CoZero -> stk
   | CoBind {bind; pol; cmd} ->
     let prog' = cmd_nf
         {prog with curr = cmd;

lib/SortInfer/sortInfer.ml

@@ -106,6 +106,7 @@ let unify_def ?debug env item =
         try VarEnv.find v !env.varpols
         with Not_found -> fail_undefined_var (Var.to_string v) loc in
       unify upol (Loc (loc, Redirect polvar))
+    | CoTop -> unify upol (Loc (loc, Litt negative))
     | Bindcc {bind = (pol1, typ); pol = pol2; cmd} ->
       unify_typ upol typ;
       unify upol (Loc (loc, pol1));
@@ -129,6 +130,7 @@ let unify_def ?debug env item =
   and unify_stk upol final_upol loc stk =
     match stk with
     | Ret -> unify (Loc (loc, upol)) final_upol
+    | CoZero -> unify upol (Loc (loc, Litt positive))
     | CoBind {bind=(var,typ); pol; cmd} ->
       let polvar = PolVar.fresh () in
       env := {!env with varpols = VarEnv.add var polvar !env.varpols};

lib/SortInfer/sort_export.ml

@@ -76,6 +76,7 @@ let export_ast env item =
 
   and export_val loc = function
     | Var v -> FullAst.Var v
+    | CoTop -> FullAst.CoTop
     | Bindcc {bind=(pol2,_) as bind ;pol=pol1; cmd} ->
       let pol1 = export_upol ~loc pol1 in
       let pol2 = export_upol ~loc pol2 in
@@ -93,6 +94,7 @@ let export_ast env item =
 
   and export_stk loc = function
     | Ret -> FullAst.Ret
+    | CoZero -> FullAst.CoZero
     | CoBind {bind; pol; cmd} ->
       let bind = export_bind pol bind in
       let pol = export_upol ~loc pol in

lib/ast.ml

@@ -92,6 +92,7 @@ module Ast (Params : AstParams) = struct
       }
   and pre_value =
     | Var of Var.t
+    | CoTop
     | Bindcc of {
         bind : cont_bind;
         pol : polarity;
@@ -114,6 +115,7 @@ module Ast (Params : AstParams) = struct
       }
   and pre_stack =
     | Ret
+    | CoZero
     | CoBind of {
         bind : val_bind;
         pol : polarity;
@@ -174,6 +176,7 @@ module Ast (Params : AstParams) = struct
 
   module V = struct
     type t = meta_value
+    let cotop = dummy_val_meta CoTop
     let var x = dummy_val_meta (Var x)
     let bindcc pol bind cmd = dummy_val_meta (Bindcc {pol;cmd;bind})
     let box kind bind cmd = dummy_val_meta (Box {kind; bind; cmd})
@@ -183,6 +186,7 @@ module Ast (Params : AstParams) = struct
 
   module S = struct
     type t = meta_stack
+    let cozero = dummy_stack_meta CoZero
     let ret = dummy_stack_meta (Ret)
     let bind pol bind cmd = dummy_stack_meta (CoBind {pol; bind; cmd})
     let box kind stk = dummy_stack_meta (CoBox {kind; stk})

lib/prettyPrinter.ml

@@ -135,6 +135,8 @@ and pp_pre_value fmt = function
 
   | Var v -> pp_var fmt v
 
+  | CoTop -> fprintf fmt "GOT_TOP"
+
   | Bindcc {pol; bind=typ; cmd; _} ->
     fprintf fmt "@[<hov 2>bind/cc%a%a ->@ %a@]"
       pp_pol_annot pol
@@ -170,6 +172,8 @@ and pp_pre_stack_trail fmt s =
 
   | Ret -> fprintf fmt "@,.ret()"
 
+  | CoZero -> fprintf fmt "@,.GOT_ZERO()"
+
   | CoBind {pol; bind = (name, typ); cmd; _} ->
     fprintf fmt "@,@[<hov 2>.bind%a %a ->@ %a@]"
       pp_pol_annot pol

test/intern1.t/run.t

@@ -2,9 +2,9 @@ Test the prelude internalizer
   $ autobill intern test_prelude.bill
   decl type test1<0> : (-) -> +
   type test2<1> : + = unit
-  type test3<2> (a<4> : +) (b<5> : -) : - = b<5>
+  type test3<2> (a<10> : +) (b<11> : -) : - = b<11>
   type test4<3> : - = (test3<2> unit top)
-  type test5<4> (a<6> : -) : - = test4<3>
+  type test5<4> (a<12> : -) : - = test4<3>
   type test6<5> : + = (test1<0> test4<3>)
   data test7<6> =
     case :cons1<0>()
@@ -19,17 +19,17 @@ Test the prelude internalizer
 
 Test the program internalizer on name shadowing:
   $ autobill intern test_prog.bill
-  term<pol2> test9<0> : <t5> = unit()
-  term<pol13> test9<1> : <t20> =
-    bind/cc<pol3> (ret() : <t6>) ->
-      unit().bind<pol11> (x<2> : <t9>) ->
+  term<pol2> test9<0> : <t11> = unit()
+  term<pol13> test9<1> : <t26> =
+    bind/cc<pol3> (ret() : <t12>) ->
+      unit().bind<pol11> (x<2> : <t15>) ->
               step<pol10>
-                bind/cc<pol4> (ret() : <t11>) ->
-                  unit().bind<pol6> (x<3> : <t14>) ->
+                bind/cc<pol4> (ret() : <t17>) ->
+                  unit().bind<pol6> (x<3> : <t20>) ->
                           x<3>.ret()
-              : <t10>
+              : <t16>
               into
-                this.bind<pol9> (y<4> : <t17>) ->
+                this.bind<pol9> (y<4> : <t23>) ->
                       x<2>.ret()
               end
 Finally, test a roundtrip of the whole thing:

test/intern2.t/run.t

@@ -2,9 +2,9 @@ Test the prelude internalizer
   $ autobill polinfer test_prelude.bill
   decl type test1<0> : (-) -> +
   type test2<1> : + = unit
-  type test3<2> (a<4> : +) (b<5> : -) : - = b<5>
+  type test3<2> (a<10> : +) (b<11> : -) : - = b<11>
   type test4<3> : - = (test3<2> unit top)
-  type test5<4> (a<6> : -) : - = test4<3>
+  type test5<4> (a<12> : -) : - = test4<3>
   type test6<5> : + = (test1<0> test4<3>)
   data test7<6> =
     case :cons1<0>()
@@ -18,32 +18,32 @@ Test the prelude internalizer
 
 Test the program internalizer on name shadowing:
   $ autobill polinfer test_prog.bill
-  /* var x<2> : <t9> */
-  /* var x<3> : <t14> */
-  /* var y<4> : <t17> */
-  /* tyvar t6 : + */
-  /* tyvar t9 : + */
-  /* tyvar t11 : + */
-  /* tyvar t14 : + */
+  /* var x<2> : <t15> */
+  /* var x<3> : <t20> */
+  /* var y<4> : <t23> */
+  /* tyvar t12 : + */
+  /* tyvar t15 : + */
   /* tyvar t17 : + */
-  term<+> test9<0> : <t5> = unit()
-  term<+> test9<1> : <t20> =
-    bind/cc+ (ret() : <t6>) -> unit()
-      .bind+ (x<2> : <t9>) ->
+  /* tyvar t20 : + */
+  /* tyvar t23 : + */
+  term<+> test9<0> : <t11> = unit()
+  term<+> test9<1> : <t26> =
+    bind/cc+ (ret() : <t12>) -> unit()
+      .bind+ (x<2> : <t15>) ->
         step+
-          bind/cc+ (ret() : <t11>) -> unit().bind+ (x<3> : <t14>) -> x<3>.ret()
-        : <t10>
+          bind/cc+ (ret() : <t17>) -> unit().bind+ (x<3> : <t20>) -> x<3>.ret()
+        : <t16>
         into
-          this.bind+ (y<4> : <t17>) -> x<2>.ret()
+          this.bind+ (y<4> : <t23>) -> x<2>.ret()
         end
 
 Test both programs:
   $ cat test_prelude.bill test_prog.bill | autobill polinfer
   decl type test1<0> : (-) -> +
   type test2<1> : + = unit
-  type test3<2> (a<4> : +) (b<5> : -) : - = b<5>
+  type test3<2> (a<10> : +) (b<11> : -) : - = b<11>
   type test4<3> : - = (test3<2> unit top)
-  type test5<4> (a<6> : -) : - = test4<3>
+  type test5<4> (a<12> : -) : - = test4<3>
   type test6<5> : + = (test1<0> test4<3>)
   data test7<6> =
     case :cons1<0>()
@@ -53,23 +53,23 @@ Test both programs:
   /* constructor "cons1<0>" is :cons1<0>() : test7<6>*/
   /* constructor "cons2<1>" is :cons2<1>(test2<1>, test6<5>) : test7<6>*/
   /* destructor "destr1<0>" is .destr1<0>().ret((shift- unit)) : test8<7>*/
-  /* var x<2> : <t12> */
-  /* var x<3> : <t17> */
-  /* var y<4> : <t20> */
-  /* tyvar t9 : + */
-  /* tyvar t12 : + */
-  /* tyvar t14 : + */
-  /* tyvar t17 : + */
+  /* var x<2> : <t18> */
+  /* var x<3> : <t23> */
+  /* var y<4> : <t26> */
+  /* tyvar t15 : + */
+  /* tyvar t18 : + */
   /* tyvar t20 : + */
-  term<+> test9<0> : <t8> = unit()
-  term<+> test9<1> : <t23> =
-    bind/cc+ (ret() : <t9>) -> unit()
-      .bind+ (x<2> : <t12>) ->
+  /* tyvar t23 : + */
+  /* tyvar t26 : + */
+  term<+> test9<0> : <t14> = unit()
+  term<+> test9<1> : <t29> =
+    bind/cc+ (ret() : <t15>) -> unit()
+      .bind+ (x<2> : <t18>) ->
         step+
-          bind/cc+ (ret() : <t14>) -> unit().bind+ (x<3> : <t17>) -> x<3>.ret()
-        : <t13>
+          bind/cc+ (ret() : <t20>) -> unit().bind+ (x<3> : <t23>) -> x<3>.ret()
+        : <t19>
         into
-          this.bind+ (y<4> : <t20>) -> x<2>.ret()
+          this.bind+ (y<4> : <t26>) -> x<2>.ret()
         end
 
 

test/parser.t/run.t

@@ -36,6 +36,11 @@ Test the parser on a BILL program testingthe whole grammar
       case this.cons2(x : t, y : u, z : v).ret() : w -> v.ret()
     end
   cmd test : t = unit().ret()
+  cmd test = step
+               GOT_TOP
+             into
+               this.GOT_ZERO()
+             end
   cmd test = unit().call(x).proj(0/2).proj(1/2).proj(1/3).ret()
   cmd test = unit().mycons().ret()
   cmd test = unit().mycons2(x, y, z).ret()
@@ -95,6 +100,11 @@ Now test the parser with a roundtrip
       case this.cons2(x : t, y : u, z : v).ret() : w -> v.ret()
     end
   cmd test : t = unit().ret()
+  cmd test = step
+               GOT_TOP
+             into
+               this.GOT_ZERO()
+             end
   cmd test = unit().call(x).proj(0/2).proj(1/2).proj(1/3).ret()
   cmd test = unit().mycons().ret()
   cmd test = unit().mycons2(x, y, z).ret()

test/parser.t/test.bill

@@ -29,6 +29,7 @@ term test = match
   case this.cons2(x : t, y : u, z : v).ret() : w -> v.ret()
 end
 cmd test : t = step unit() into this.ret() end
+cmd test = step GOT_TOP into this.GOT_ZERO() end
 cmd test = step unit() into this.call(x).yes().no().proj(1/3).ret() end
 cmd test = step unit() into this.mycons().ret() end
 cmd test = step unit() into this.mycons2(x, y, z).ret() end