Skip to content

Commit

Permalink
refactor
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahxephon89
rahxephon89 committed Feb 11, 2025
1 parent 5716f30 commit dd0fe62
Show file tree
Hide file tree
Showing 7 changed files with 14 additions and 67 deletions.
2 changes: 0 additions & 2 deletions third_party/move/move-compiler/src/expansion/ast.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -284,7 +284,6 @@ pub enum SpecBlockTarget_ {
Module,
Member(Name, Option<Box<FunctionSignature>>),
Schema(Name, Vec<(Name, AbilitySet)>),
Lambda,
}

pub type SpecBlockTarget = Spanned<SpecBlockTarget_>;
Expand Down Expand Up @@ -1179,7 +1178,6 @@ impl AstDebug for SpecBlockTarget_ {
fn ast_debug(&self, w: &mut AstWriter) {
match self {
SpecBlockTarget_::Code => {},
SpecBlockTarget_::Lambda => {},
SpecBlockTarget_::Module => w.write("module "),
SpecBlockTarget_::Member(name, sign_opt) => {
w.write(name.value);
Expand Down
1 change: 0 additions & 1 deletion third_party/move/move-compiler/src/expansion/translate.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2022,7 +2022,6 @@ fn spec_target(context: &mut Context, sp!(loc, pt): P::SpecBlockTarget) -> E::Sp
Box::new(signature)
}),
),
PT::Lambda => ET::Lambda,
};
sp(loc, et)
}
Expand Down
3 changes: 1 addition & 2 deletions third_party/move/move-compiler/src/parser/ast.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -350,7 +350,6 @@ pub enum SpecBlockTarget_ {
Module,
Member(Name, Option<Box<FunctionSignature>>),
Schema(Name, Vec<(Name, Vec<Ability>)>),
Lambda,
}

pub type SpecBlockTarget = Spanned<SpecBlockTarget_>;
Expand Down Expand Up @@ -1411,7 +1410,7 @@ impl AstDebug for SpecBlock_ {
impl AstDebug for SpecBlockTarget_ {
fn ast_debug(&self, w: &mut AstWriter) {
match self {
SpecBlockTarget_::Code | SpecBlockTarget_::Lambda => {},
SpecBlockTarget_::Code => {},
SpecBlockTarget_::Module => w.write("module "),
SpecBlockTarget_::Member(name, sign_opt) => {
w.write(name.value);
Expand Down
20 changes: 6 additions & 14 deletions third_party/move/move-compiler/src/parser/syntax.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1310,7 +1310,7 @@ fn parse_term(context: &mut Context) -> Result<Exp, Box<Diagnostic>> {
},

Tok::Spec => {
let spec_block = parse_spec_block(vec![], context, false)?;
let spec_block = parse_spec_block(vec![], context)?;
Exp_::Spec(spec_block)
},

Expand Down Expand Up @@ -1400,7 +1400,7 @@ fn parse_spec_loop_invariant(context: &mut Context) -> Result<SequenceItem, Box<
// Parse a loop invariant. Also validate that only `invariant`
// properties are contained in the spec block. This is
// transformed into `while ({spec { .. }; cond) body`.
let spec = parse_spec_block(vec![], context, false)?;
let spec = parse_spec_block(vec![], context)?;
for member in &spec.value.members {
match member.value {
// Ok
Expand Down Expand Up @@ -1969,7 +1969,7 @@ fn parse_lambda(
}
let spec_opt = if context.tokens.peek() == Tok::Spec {
let spec_start = context.tokens.start_loc();
let spec = parse_spec_block(vec![], context, true)?;
let spec = parse_spec_block(vec![], context)?;
let spec_end = context.tokens.previous_end_loc();
let loc: Loc = make_loc(context.tokens.file_hash(), spec_start, spec_end);
require_move_version(
Expand Down Expand Up @@ -3569,7 +3569,7 @@ fn parse_module(
},
_ => {
// Regular spec block
ModuleMember::Spec(parse_spec_block(attributes, context, false)?)
ModuleMember::Spec(parse_spec_block(attributes, context)?)
},
}
},
Expand Down Expand Up @@ -3687,7 +3687,7 @@ fn parse_script(
let mut specs = vec![];
while context.tokens.peek() == Tok::NumSign || context.tokens.peek() == Tok::Spec {
let attributes = parse_attributes(context)?;
specs.push(parse_spec_block(attributes, context, false)?);
specs.push(parse_spec_block(attributes, context)?);
}

if context.tokens.peek() != Tok::RBrace {
Expand Down Expand Up @@ -3728,7 +3728,6 @@ fn parse_script(
fn parse_spec_block(
attributes: Vec<Attributes>,
context: &mut Context,
from_lambda: bool,
) -> Result<SpecBlock, Box<Diagnostic>> {
context.tokens.match_doc_comments();
let start_loc = context.tokens.start_loc();
Expand Down Expand Up @@ -3762,13 +3761,7 @@ fn parse_spec_block(
let signature = parse_spec_target_signature_opt(&name.loc, context)?;
SpecBlockTarget_::Member(name, signature)
},
Tok::LBrace => {
if from_lambda {
SpecBlockTarget_::Lambda
} else {
SpecBlockTarget_::Code
}
},
Tok::LBrace => SpecBlockTarget_::Code,
_ => {
return Err(unexpected_token_error(
context.tokens,
Expand All @@ -3781,7 +3774,6 @@ fn parse_spec_block(
target_start_loc,
match target_ {
SpecBlockTarget_::Code => target_start_loc,
SpecBlockTarget_::Lambda => target_start_loc,
_ => context.tokens.previous_end_loc(),
},
target_,
Expand Down
5 changes: 1 addition & 4 deletions third_party/move/move-model/src/ast.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -171,10 +171,7 @@ impl ConditionKind {

pub fn allowed_on_lambda_spec(&self) -> bool {
use ConditionKind::*;
matches!(
self,
Requires | Ensures | FunctionInvariant // TODO(tengzhang): support LetPost and LetPre
)
matches!(self, Requires | Ensures)
}

/// Returns true if this condition is allowed on a struct.
Expand Down
2 changes: 0 additions & 2 deletions third_party/move/move-model/src/builder/exp_builder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2073,7 +2073,6 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo
if let Some((pat, ty)) = &lambda_info {
let nty: Type = subs.specialize_with_defaults(ty);
lambda_info = Some((pat.clone(), nty.clone()));
//println!("nty:{}", nty.display(&self.type_display_context()));
}
self.translate_spec_block(&loc, locals, &block, lambda_info)
} else {
Expand Down Expand Up @@ -2322,7 +2321,6 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo
return Spec::default();
};
// This uses a builder for inlined specification blocks stored in the state.
// let from_lambda = block.value.target.value == EA::SpecBlockTarget_::Lambda;
let context = SpecBlockContext::FunctionCodeV2(fun_name, locals, lambda_info.clone());
self.parent.inline_spec_builder = Spec {
loc: Some(loc.clone()),
Expand Down
48 changes: 6 additions & 42 deletions third_party/move/move-model/src/builder/module_builder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,20 +134,11 @@ impl<'a> SpecBlockContext<'a> {
use SpecBlockContext::*;
match self {
FunctionCode(_, _) => false,
FunctionCodeV2(_, _, _) => false,
//TODO(tengzhang): change for lambda expression,
FunctionCodeV2(_, _, _) => false, // TODO(tengzhang): add support of old(..) to spec of lambda expression
_ => true,
}
}

pub fn check_lambda(&self) -> bool {
use SpecBlockContext::*;
match self {
FunctionCodeV2(_, _, from_lambda) => from_lambda.is_some(),
_ => false,
}
}

pub fn name(&self) -> Option<&QualifiedSymbol> {
use SpecBlockContext::*;
match self {
Expand Down Expand Up @@ -367,7 +358,7 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
target: &'pa EA::SpecBlockTarget,
) -> Option<SpecBlockContext<'pa>> {
match &target.value {
EA::SpecBlockTarget_::Code | EA::SpecBlockTarget_::Lambda => None,
EA::SpecBlockTarget_::Code => None,
EA::SpecBlockTarget_::Member(name, _) => {
let qsym = self.qualified_by_module_from_name(name);
if self.parent.fun_table.contains_key(&qsym) {
Expand Down Expand Up @@ -1280,20 +1271,7 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
spec_block: &EA::SpecBlock,
context: SpecBlockContext,
) {
assert!(self.spec_block_lets.is_empty());
// Sort members so that lets are processed first. This is needed so that lets included
// from schemas are properly renamed on name clash.
let let_sorted_members = spec_block.value.members.iter().sorted_by(|m1, m2| {
let m1_is_let = matches!(m1.value, EA::SpecBlockMember_::Let { .. });
let m2_is_let = matches!(m2.value, EA::SpecBlockMember_::Let { .. });
match (m1_is_let, m2_is_let) {
(true, true) | (false, false) => std::cmp::Ordering::Equal,
(true, false) => std::cmp::Ordering::Less,
(false, true) => std::cmp::Ordering::Greater,
}
});

for member in let_sorted_members {
for member in &spec_block.value.members {
let loc = &self.parent.env.to_loc(&member.loc);
match &member.value {
EA::SpecBlockMember_::Condition {
Expand Down Expand Up @@ -1323,21 +1301,11 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
EA::SpecBlockMember_::Update { lhs, rhs } => {
self.def_ana_global_var_update(loc, &context, lhs, rhs)
},
EA::SpecBlockMember_::Let {
name,
post_state,
def,
} => {
if context.check_lambda() {
self.def_ana_let(&context, loc, *post_state, name, def)
}
},
_ => {
self.parent.error(loc, "item not allowed");
},
}
}
self.spec_block_lets.clear();
}

/// Validates whether a function signature provided with a spec block target matches the
Expand Down Expand Up @@ -2003,7 +1971,7 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {

et
},
FunctionCodeV2(name, locals, _from_lambda) => {
FunctionCodeV2(name, locals, from_lambda) => {
let entry = &self
.parent
.fun_table
Expand All @@ -2020,20 +1988,16 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
et.define_local(loc, *sym, type_.clone(), None, *index)
}

if _from_lambda.is_some()
&& matches!(kind, ConditionKind::Ensures | ConditionKind::LetPost(..))
{
let (_, ty) = _from_lambda.clone().unwrap();
if from_lambda.is_some() && matches!(kind, ConditionKind::Ensures) {
let (_, ty) = from_lambda.clone().unwrap();
et.enter_scope();
if let Type::Tuple(ts) = &ty {
for (i, ty) in ts.iter().enumerate() {
let name: Symbol = et.symbol_pool().make(&format!("result_{}", i + 1));
//let oper: Option<Operation> = Some(Operation::Result(i));
et.define_local(loc, name, ty.clone(), None, None);
}
} else {
let name = et.symbol_pool().make("result");
//let oper = Some(Operation::Result(0));
et.define_local(loc, name, ty.clone(), None, None);
}
}
Expand Down

0 comments on commit dd0fe62

Please sign in to comment.