Skip to content

Commit

Permalink
Parameterising identifier names (#826)
Browse files Browse the repository at this point in the history 
* Use FlattenedLiteral module

* Update src/base/ScillaParser.mly

Co-Authored-By: Anton Trunov <anton@zilliqa.com>

* Update src/base/Type.ml

Co-Authored-By: Anton Trunov <anton@zilliqa.com>

* Update src/base/Literal.ml

Co-Authored-By: Anton Trunov <anton@zilliqa.com>

* Update src/base/Literal.ml

Co-Authored-By: Anton Trunov <anton@zilliqa.com>

* Rename equal_id and compare_id

* Rename asId and asIdL

* Make Ident private, and use mk_id and mk_loc_id to construct them instead

* fmt

Co-authored-by: Anton Trunov <anton@zilliqa.com>
  • Loading branch information
@jjcnn
jjcnn and Anton Trunov committed May 1, 2020
1 parent 5f0abd5 commit e15e73d
Show file tree
Hide file tree
Showing 55 changed files with 1,640 additions and 1,355 deletions.
14 changes: 9 additions & 5 deletions src/base/Accept.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,9 @@

open Core_kernel
open! Int.Replace_polymorphic_compare
open Literal
open TypeUtil
open ErrorUtils
open Identifier
open Syntax

module ScillaAcceptChecker
Expand All @@ -39,8 +39,12 @@ module ScillaAcceptChecker
val get_type : rep -> PlainTypes.t inferred_type [@@warning "-32"]
end) =
struct
module EISyntax = ScillaSyntax (SR) (ER)
open EISyntax
(* TODO: Change this to CanonicalLiteral = Literals based on canonical names. *)
module ACLiteral = FlattenedLiteral
module ACType = ACLiteral.LType
module ACIdentifier = ACType.TIdentifier
module ACSyntax = ScillaSyntax (SR) (ER) (ACLiteral)
open ACSyntax

(* Warning level to use when contract has code paths with potentially
* no accept statement. *)
Expand Down Expand Up @@ -104,7 +108,7 @@ struct
( sprintf
"transition %s had a potential code path with duplicate accept \
statements:\n"
(get_id transition.comp_name)
(ACIdentifier.as_error_string transition.comp_name)
^ String.concat ~sep:""
(List.map group ~f:(fun loc ->
sprintf " Accept at %s\n" (get_loc_str loc))) )
Expand All @@ -125,7 +129,7 @@ struct
if List.for_all all_accept_groups ~f:List.is_empty then
warn0
(sprintf "No transition in contract %s contains an accept statement\n"
(get_id contr.cname))
(ACIdentifier.as_error_string contr.cname))
warning_level_missing_accept

(* ************************************** *)
Expand Down
41 changes: 23 additions & 18 deletions src/base/BuiltIns.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,6 @@

open Core_kernel
open! Int.Replace_polymorphic_compare
open Identifier
open Type
open Literal
open Syntax
open ErrorUtils
Expand All @@ -31,6 +29,13 @@ open TypeUtil
open Integer256
open TypeUtilities

(* TODO: Change this to CanonicalLiteral = Literals based on canonical names. *)
module BILiteral = FlattenedLiteral
module BIType = BILiteral.LType
module BIIdentifier = BIType.TIdentifier
open BIType
open BILiteral

module UsefulLiterals = struct
let true_lit = ADTValue ("True", [], [])

Expand Down Expand Up @@ -202,7 +207,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct

let eq_elab t ts =
match ts with
| [ i1; i2 ] when [%equal: Type.t] i1 i2 && is_int_type i1 ->
| [ i1; i2 ] when [%equal: BIType.t] i1 i2 && is_int_type i1 ->
elab_tfun_with_args_no_gas t [ i1 ]
| _ -> fail0 "Failed to elaborate"

Expand All @@ -213,7 +218,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct

let binop_elab t ts =
match ts with
| [ i1; i2 ] when [%equal: Type.t] i1 i2 && is_int_type i1 ->
| [ i1; i2 ] when [%equal: BIType.t] i1 i2 && is_int_type i1 ->
elab_tfun_with_args_no_gas t [ i1 ]
| _ -> fail0 "Failed to elaborate"

Expand Down Expand Up @@ -319,7 +324,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct

let pow_elab t ts =
match ts with
| [ i1; i2 ] when is_int_type i1 && [%equal: Type.t] i2 uint32_typ ->
| [ i1; i2 ] when is_int_type i1 && [%equal: BIType.t] i2 uint32_typ ->
elab_tfun_with_args_no_gas t [ i1 ]
| _ -> fail0 "Failed to elaborate"

Expand Down Expand Up @@ -405,7 +410,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct

let eq_elab sc ts =
match ts with
| [ i1; i2 ] when [%equal: Type.t] i1 i2 && is_uint_type i1 ->
| [ i1; i2 ] when [%equal: BIType.t] i1 i2 && is_uint_type i1 ->
elab_tfun_with_args_no_gas sc [ i1 ]
| _ -> fail0 "Failed to elaborate"

Expand All @@ -416,7 +421,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct

let binop_elab sc ts =
match ts with
| [ i1; i2 ] when [%equal: Type.t] i1 i2 && is_uint_type i1 ->
| [ i1; i2 ] when [%equal: BIType.t] i1 i2 && is_uint_type i1 ->
elab_tfun_with_args_no_gas sc [ i1 ]
| _ -> fail0 "Failed to elaborate"

Expand Down Expand Up @@ -523,7 +528,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct

let pow_elab t ts =
match ts with
| [ i1; i2 ] when is_uint_type i1 && [%equal: Type.t] i2 uint32_typ ->
| [ i1; i2 ] when is_uint_type i1 && [%equal: BIType.t] i2 uint32_typ ->
elab_tfun_with_args_no_gas t [ i1 ]
| _ -> fail0 "Failed to elaborate"

Expand Down Expand Up @@ -632,7 +637,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
let to_nat ls _ =
match ls with
| [ UintLit (Uint32L n) ] ->
let rec nat_builder (i : Uint32.t) (acc : Literal.t) =
let rec nat_builder (i : Uint32.t) (acc : BILiteral.t) =
if [%equal: uint32] i Uint32.zero then acc
else nat_builder (Uint32.pred i) (ADTValue ("Succ", [], [ acc ]))
in
Expand Down Expand Up @@ -795,7 +800,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
match ts with
| [ bstyp1; bstyp2 ]
when (* We want both types to be ByStr with equal width. *)
is_bystrx_type bstyp1 && [%equal: Type.t] bstyp1 bstyp2 ->
is_bystrx_type bstyp1 && [%equal: BIType.t] bstyp1 bstyp2 ->
elab_tfun_with_args_no_gas sc [ bstyp1 ]
| _ -> fail0 "Failed to elaborate"

Expand Down Expand Up @@ -1144,7 +1149,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct

let contains_elab sc ts =
match ts with
| [ MapType (kt, vt); u ] when [%equal: Type.t] kt u ->
| [ MapType (kt, vt); u ] when [%equal: BIType.t] kt u ->
elab_tfun_with_args_no_gas sc [ kt; vt ]
| _ -> fail0 "Failed to elaborate"

Expand All @@ -1166,7 +1171,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
let put_elab sc ts =
match ts with
| [ MapType (kt, vt); kt'; vt' ]
when [%equal: Type.t] kt kt' && [%equal: Type.t] vt vt' ->
when [%equal: BIType.t] kt kt' && [%equal: BIType.t] vt vt' ->
elab_tfun_with_args_no_gas sc [ kt; vt ]
| _ -> fail0 "Failed to elaborate"

Expand All @@ -1189,15 +1194,15 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct

let get_elab sc ts =
match ts with
| [ MapType (kt, vt); kt' ] when [%equal: Type.t] kt kt' ->
| [ MapType (kt, vt); kt' ] when [%equal: BIType.t] kt kt' ->
elab_tfun_with_args_no_gas sc [ kt; vt ]
| _ -> fail0 "Failed to elaborate"

(* Notice that get passes return type *)
let get ls rt =
match (ls, rt) with
| [ Map (_, entries); key ], ADT (tname, [ targ ])
when Core_kernel.String.(get_id tname = "Option") -> (
when Core_kernel.String.(BIIdentifier.get_id tname = "Option") -> (
let res = Caml.Hashtbl.find_opt entries key in
match res with None -> pure @@ none_lit targ | Some v -> some_lit v )
| _ -> builtin_fail "Map.get" ls
Expand All @@ -1211,7 +1216,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct

let remove_elab sc ts =
match ts with
| [ MapType (kt, vt); u ] when [%equal: Type.t] kt u ->
| [ MapType (kt, vt); u ] when [%equal: BIType.t] kt u ->
elab_tfun_with_args_no_gas sc [ kt; vt ]
| _ -> fail0 "Failed to elaborate"

Expand Down Expand Up @@ -1284,11 +1289,11 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
module BuiltInDictionary = struct
(* Elaborates the operation type based on the arguments types *)
type elaborator =
Type.t -> Type.t list -> (Type.t, scilla_error list) result
BIType.t -> BIType.t list -> (BIType.t, scilla_error list) result

(* Takes the expected type as an argument to elaborate the result *)
type built_in_executor =
Literal.t list -> Type.t -> (Literal.t, scilla_error list) result
BILiteral.t list -> BIType.t -> (BILiteral.t, scilla_error list) result

(* A built-in record type:
* arity
Expand All @@ -1297,7 +1302,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
to support polymorphism -- e.g., for ints and maps
* executor - operational semantics of the built-in
*)
type built_in_record = int * Type.t * elaborator * built_in_executor
type built_in_record = int * BIType.t * elaborator * built_in_executor

[@@@ocamlformat "disable"]

Expand Down
29 changes: 19 additions & 10 deletions src/base/BuiltIns.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,26 +19,34 @@
open Syntax
open ErrorUtils
open Core_kernel
open Literal

(* TODO: Change this to CanonicalLiteral = Literals based on canonical names. *)
module BILiteral = FlattenedLiteral
module BIType = BILiteral.LType

module UsefulLiterals : sig
val true_lit : Literal.t
val true_lit : BILiteral.t

val false_lit : Literal.t
val false_lit : BILiteral.t

val to_Bool : bool -> Literal.t
val to_Bool : bool -> BILiteral.t

val some_lit : Literal.t -> (Literal.t, ErrorUtils.scilla_error list) result
val some_lit :
BILiteral.t -> (BILiteral.t, ErrorUtils.scilla_error list) result

val none_lit : Type.t -> Literal.t
val none_lit : BIType.t -> BILiteral.t

val pair_lit :
Literal.t -> Literal.t -> (Literal.t, ErrorUtils.scilla_error list) result
BILiteral.t ->
BILiteral.t ->
(BILiteral.t, ErrorUtils.scilla_error list) result
end

module ScillaBuiltIns (SR : Rep) (ER : Rep) : sig
module BuiltInDictionary : sig
type built_in_executor =
Literal.t list -> Type.t -> (Literal.t, scilla_error list) result
BILiteral.t list -> BIType.t -> (BILiteral.t, scilla_error list) result

(* The return result is a triple:
* The full elaborated type of the operation, e.g., string -> Bool
Expand All @@ -47,10 +55,11 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) : sig
*)
val find_builtin_op :
ER.rep builtin_annot ->
Type.t list ->
(Type.t * Type.t * built_in_executor, scilla_error list) result
BIType.t list ->
(BIType.t * BIType.t * built_in_executor, scilla_error list) result
end

(* Elaborator for the built-in typ *)
val elab_id : Type.t -> Type.t list -> (Type.t, scilla_error list) result
val elab_id :
BIType.t -> BIType.t list -> (BIType.t, scilla_error list) result
end

0 comments on commit e15e73d

Please sign in to comment.