Merge pull request #21 from informalsystems/gabriela/syntax-reliability

Avoid useless errors in generated files

src/boilerplate.rs

@@ -87,7 +87,7 @@ pub fn initializers(ctx: &Context) -> String {
         "
   pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT))
 
-  val env_val = {{ block: {{ time: time }} }}
+  val env_val = {{ block: {{ time: time, height: 1 }} }} // TODO: Add a height var if you need it
 
   action init = {{
     // TODO: Change next line according to fund expectations
@@ -100,7 +100,7 @@ pub fn initializers(ctx: &Context) -> String {
     val info = {{ sender: sender, funds: funds }}
 
     pure val message: InstantiateMsg = {}
-    pure val r = instantiate(init_contract_state, {{ block: {{ time: 0 }} }}, info, message)
+    pure val r = instantiate(init_contract_state, {{ block: {{ time: 0, height: 1 }} }}, info, message)
 
     all {{
       contract_state' = r._2,
@@ -126,9 +126,14 @@ pub fn init_value_for_type(ctx: &Context, ty: String) -> String {
         return "[]".to_string();
     }
 
-    if ctx.structs.contains_key(&ty) {
+    if ty.starts_with("Option") {
+        return "None".to_string();
+    }
+
+    let typ = ty.split('[').next().unwrap();
+    if ctx.structs.contains_key(typ) {
         // Type is a struct, initialize fields recursively
-        let fields = ctx.structs.get(&ty).unwrap();
+        let fields = ctx.structs.get(typ).unwrap();
         let struct_value = fields
             .iter()
             .map(|field| {
@@ -139,17 +144,17 @@ pub fn init_value_for_type(ctx: &Context, ty: String) -> String {
                 )
             })
             .collect_vec()
-            .join(",");
+            .join(", ");
         return format!("{{ {} }}", struct_value);
     }
 
-    match ty.as_str() {
+    match typ {
         "str" => "\"\"".to_string(),
         "int" => "0".to_string(),
         "Addr" => "\"s1\"".to_string(),
         _ => {
             eprintln!("No init value for type: {ty}");
-            "<missing-type>".to_string()
+            "\"<missing-value>\"".to_string()
         }
     }
 }
@@ -195,7 +200,7 @@ pub fn post_items(ctx: &Context) -> String {
     {contract_state}
   }}
 
-  pure val init_contract_state = {{
+  pure val init_contract_state: ContractState = {{
     {initializer}
   }}
 

src/lib.rs

@@ -155,10 +155,13 @@ fn translate_items(tcx: TyCtxt, crate_name: &str, items: Vec<&rustc_hir::Item>)
             ("denom".to_string(), "str".to_string()),
             ("amount".to_string(), "int".to_string()),
         ],
+        enums: HashMap::new(),
+        type_aliases: HashMap::new(),
         // scoped
         record_fields: vec![],
         struct_fields: vec![],
         pat_fields: vec![],
+        generics: vec![],
         current_item_name: "".to_string(),
     };
 

src/nondet.rs

@@ -69,7 +69,7 @@ fn missing_nondet_value<T: NondetValue + Debug + Translatable>(
     kind: &str,
 ) -> String {
     eprintln!("No nondet value for {}: {:?}", kind, item.translate(ctx));
-    "<missing-nondet-value>".to_string()
+    "\"<missing-nondet-value>\"".to_string()
 }
 
 fn nondet_value_for_list(ty: &rustc_hir::Ty<'_>, ctx: &mut Context, ident: &str) -> NondetInfo {
@@ -187,6 +187,19 @@ impl NondetValue for rustc_hir::PathSegment<'_> {
             return fields.nondet_info(ctx, ident);
         }
 
+        // If the type refers to an enum, get the first variant and generate a nondet value for it
+        if ctx.enums.contains_key(&translated_type) {
+            let variants = ctx.enums[&translated_type].clone();
+            let variant = variants[0].clone();
+            return self.nondet_info(ctx, variant.as_str());
+        }
+
+        // If the type refers to a type alias, generate a nondet value for the type alias
+        if ctx.type_aliases.contains_key(&translated_type) {
+            let alias = ctx.type_aliases[&translated_type].clone();
+            return self.nondet_info(ctx, alias.as_str());
+        }
+
         // If the type refers to a primitive type, generate a nondet value for the primitive type
         let value = match translated_type.as_str() {
             "str" | "Addr" => "Set(\"s1\", \"s2\", \"s3\")".to_string(),

src/quint-lib-files/cw_types.qnt

@@ -65,7 +65,7 @@ module cw_types {
     gas_limit: None,
   }
 
-  pure def SubMsg_reply_on_sucess(msg: CosmosMsg, id: int): SubMsg = {
+  pure def SubMsg_reply_on_success(msg: CosmosMsg, id: int): SubMsg = {
     __reply_on(msg, id, ReplyOn_Success)
   }
 
@@ -133,7 +133,8 @@ module cw_types {
     querier: TODO,
   }
 
-  type Env = { block: { time: int /*, height: int */ } } // TODO
+  type BlockInfo = { time: int, height: int }
+  type Env = { block: BlockInfo }
 
   type Coin = {
     denom: str,
@@ -149,4 +150,16 @@ module cw_types {
     | FromStr(str)
     | FromInt(int)
     | FromListInt(List[int])
+
+  // These shouldn't be actually used, but they are here for completion
+  type MultiIndex[ik, t, pk] = ()
+  type IndexedMap[k, t i] = ()
+
+  type StdError = str
+  type StdResult[a] = Result[a, StdError]
+
+  // There's no dynamic dispatch in Quint, so the best we can do is to have a
+  // special string argument to identify a behavior and then have the
+  // implementation depend on it
+  type TraitObject = str
 }

src/quint-lib-files/cw_utils.qnt

@@ -4,6 +4,19 @@
 module cw_utils {
   import cw_types.* from "./cw_types"
 
+  type Expiration =
+    // AtHeight will expire when `env.block.height` >= height
+    | Expiration_AtHeight(int)
+    // AtTime will expire when `env.block.time` >= time
+    | Expiration_AtTime(int)
+    // Never will never expire. Used to express the empty variant
+    | Expiration_Never
+
+  type Duration =
+    | Duration_Height(int)
+    // Time in seconds
+    | Duration_Time(int)
+
   def one_coin(info: MessageInfo): Result[Coin, ContractError] = {
     if (info.funds.indices().size() == 0) {
       Err("No funds")

src/state_extraction.rs

@@ -1,7 +1,9 @@
 use itertools::Itertools;
+use regex::Regex;
 use rustc_span::{symbol::Ident, Symbol};
 
 use crate::{translate::Translatable, types::Context};
+extern crate regex;
 
 // State extraction is the only place where we need to deal with
 // rustc_middle::ty::Ty. This is the type given by typeck, which is the only way
@@ -11,19 +13,30 @@ use crate::{translate::Translatable, types::Context};
 impl Translatable for rustc_middle::ty::Ty<'_> {
     fn translate(&self, ctx: &mut Context) -> String {
         // FIXME: This should be quite unstable, but I couldn't figure out how to navigate `ty` here
+
         let var_name = &format!("{:#?}", self);
-        let name = var_name
-            .split("::")
-            .last()
-            .unwrap()
+        let name_core = var_name
+            .clone()
             .split(' ')
             .last()
             .unwrap()
             .split(')')
             .next()
-            .unwrap();
+            .unwrap()
+            .to_string();
+
+        // The name_core can look like namespace::namespace::type<namespace::namespace::type_arg>
+        // The following regex replacement has the goal of transforming it into type<type_arg>
+        let re = Regex::new(r"(\w+::)*(\w+)(<(\w+::)*(\w+)>)?").unwrap();
+        let name = re.replace(name_core.as_str(), |caps: &regex::Captures| {
+            if let Some(m) = caps.get(5) {
+                format!("{}[{}]", &caps[2], m.as_str())
+            } else {
+                caps[2].to_string()
+            }
+        });
 
-        Ident::with_dummy_span(Symbol::intern(name)).translate(ctx)
+        Ident::with_dummy_span(Symbol::intern(name.to_string().as_str())).translate(ctx)
     }
 }
 impl Translatable for rustc_middle::ty::GenericArg<'_> {