int -> int64 for lospec literals

Author: strub

libs/lospecs/ast.ml

@@ -50,7 +50,7 @@ type mulk = [`U of hld | `S of hld | `US] [@@deriving yojson]
 (* -------------------------------------------------------------------- *)
 type aexpr_ =
   | EVar of ident
-  | EInt of int
+  | EInt of int64
   | ESlice of aexpr * (aexpr * int * int)
   | EAssign of aexpr * (aexpr * int * int) * aexpr
   | EApp of ident * aexpr list

libs/lospecs/circuit.ml

@@ -131,12 +131,12 @@ let of_int ~(size : int) (v : int) : reg =
   Array.init size (fun i -> constant (bit ~position:i v))
 
 (* -------------------------------------------------------------------- *)
-let of_int32 (v : int32) : reg =
-  Array.init 32 (fun i -> constant (bit32 ~position:i v))
+let of_int32 ?(size = 32) (v : int32) : reg =
+  Array.init size (fun i -> constant (bit32 ~position:i v))
 
 (* -------------------------------------------------------------------- *)
-let of_int64 (v : int64) : reg =
-  Array.init 64 (fun i -> constant (bit64 ~position:i v))
+let of_int64 ?(size = 64) (v : int64) : reg =
+  Array.init size (fun i -> constant (bit64 ~position:i v))
 
 (* -------------------------------------------------------------------- *)
 let of_int32s (vs : int32 array) : reg =

libs/lospecs/circuit.mli

@@ -25,6 +25,10 @@ val bool_list_of_reg : reg -> bool list
 (* ==================================================================== *)
 val of_int : size:int -> int -> reg
 
+val of_int32 : ?size:int -> int32 -> reg
+
+val of_int64 : ?size:int -> int64 -> reg
+
 val of_bigint : size:int -> Z.t -> reg
 
 val of_int32s : int32 array -> reg

libs/lospecs/circuit_spec.ml

@@ -158,7 +158,7 @@ let circuit_of_specification (rs : reg list) (p : adef) : reg =
 
     | ESlice (e, ({ node = EInt offset }, size, scale)) ->
       let e = of_expr env e in
-      let offset = offset * scale in
+      let offset = (Int64.to_int offset) * scale in
       let size = size * scale in
       Array.sub e offset size
 
@@ -177,7 +177,7 @@ let circuit_of_specification (rs : reg list) (p : adef) : reg =
     | EAssign (e, ({ node = EInt offset }, size, scale), v) ->
       let e = of_expr env e in
       let v = of_expr env v in
-      let offset = offset * scale in
+      let offset = (Int64.to_int offset) * scale in
       let size = size * scale in
       let pre, e = split_at_arr offset e in 
       let e, post = split_at_arr size e in
@@ -251,7 +251,7 @@ let circuit_of_specification (rs : reg list) (p : adef) : reg =
 
     | EInt i -> begin
       match e.type_ with
-      | `W n -> Circuit.of_int ~size:n i
+      | `W n -> Circuit.of_int64 ~size:n i
       | _ -> raise (CircuitSpecError (Format.asprintf "Expected int got %a" pp_atype e.type_)) 
     end
 

libs/lospecs/lexer.mll

@@ -48,10 +48,10 @@ rule main = parse
       { Hashtbl.find_default keywords x (IDENT x) }
 
   | decnum as d
-      { NUMBER (int_of_string d) }
+      { NUMBER (Int64.of_string d) }
 
   | hexnum as d
-      { NUMBER (int_of_string d) }
+      { NUMBER (Int64.of_string d) }
 
   | whitespace+
       { main lexbuf }

libs/lospecs/parser.mly

@@ -28,7 +28,7 @@
 %token RPAREN
 
 %token<string> IDENT
-%token<int>    NUMBER
+%token<int64>  NUMBER
 
 %type <Ptree.pprogram> program
 
@@ -50,7 +50,7 @@
 
 %inline wtype_:
 | AT x=NUMBER
-    { `W x }
+    { `W (Int64.to_int x) }
 
 %inline wtype:
 | w=loc(wtype_) { w }
@@ -60,7 +60,7 @@ fname_:
     { (f, None) }
 
 | f=loc(IDENT) p=angled(list0(loc(NUMBER), COMMA))
-    { (f, Some (List.map (Lc.map (fun x -> `W x)) p)) }
+    { (f, Some (List.map (Lc.map (fun x -> `W (Int64.to_int x))) p)) }
 
 %inline fname:
 | f=loc(fname_) { f }

libs/lospecs/ptree.ml

@@ -88,7 +88,7 @@ type pfname = (psymbol * pword list option) loced [@@deriving yojson]
 type pexpr_ =
   | PEParens of pexpr 
   | PEFName of pfname
-  | PEInt of int * pword option
+  | PEInt of int64 * pword option
   | PECond of pexpr * (pexpr * pexpr)
   | PEFun of pargs * pexpr
   | PELet of (psymbol * pargs option * pexpr) * pexpr

libs/lospecs/typing.ml

@@ -109,12 +109,18 @@ let check_plain_arg (_ : env) (arg : pexpr option loced) =
     arg
 
 (* -------------------------------------------------------------------- *)
-let as_int_constant (e : pexpr) : int =
+let as_int_constant (e : pexpr) : int64 =
   match e.data with
   | PEInt (i, None) -> i
   | _ -> tyerror e.range "integer constant expected"
 
 (* -------------------------------------------------------------------- *)
+let as_nativeint_constant (e : pexpr) : int =
+  match e.data with
+  | PEInt (i, None) -> Int64.to_int i
+  | _ -> tyerror e.range "integer constant expected"
+
+  (* -------------------------------------------------------------------- *)
 type sig_ = {
   s_name : string;
   s_ntyparams : int;
@@ -468,17 +474,17 @@ let rec tt_expr_ (env : env) (e : pexpr) : aargs option * aexpr =
   | PESlice (ev, (start, len, scale)) ->
       let ev = tt_expr env ev in
       let start = tt_expr env start in
-      let len = Option.default 1 (Option.map as_int_constant len) in
-      let scale = Option.default 1 (Option.map as_int_constant scale) in
+      let len = Option.default 1 (Option.map as_nativeint_constant len) in
+      let scale = Option.default 1 (Option.map as_nativeint_constant scale) in
       let node = ESlice (ev, (start, len, scale))
       and type_ = `W (len * scale) in
       (None, { node; type_; })
 
   | PEAssign (ev, (start, len, scale), v) ->
     let ev = tt_expr env ev in
     let start = tt_expr env start in
-    let len = Option.default 1 (Option.map as_int_constant len) in
-    let scale = Option.default 1 (Option.map as_int_constant scale) in
+    let len = Option.default 1 (Option.map as_nativeint_constant len) in
+    let scale = Option.default 1 (Option.map as_nativeint_constant scale) in
     let v = tt_expr env ~check:(`W (len * scale)) v in
     let node = EAssign (ev, (start, len, scale), v) in
     (None, { node; type_ = ev.type_; })
@@ -526,7 +532,7 @@ let rec tt_expr_ (env : env) (e : pexpr) : aargs option * aexpr =
       let (`W w) = as_seq1 (tt_type_parameters env fn.range f ~expected:1 w) in
       let args = List.map (check_plain_arg env) args in
       let e, n = as_seq2 (check_arguments_count e.range ~expected:2 args) in
-      let n = as_int_constant n in
+      let n = as_nativeint_constant n in
       let ne = tt_expr env ~check:(`W w) e in
       (None, { node = ERepeat (`W (w * n), (ne, n)); type_ = `W (w * n); })