From c30b437b1e9407fb8050ea40c097d72c3751c2ac Mon Sep 17 00:00:00 2001 From: Benjamin Lipp Date: Tue, 16 Jun 2026 17:30:21 +0200 Subject: [PATCH] fix: indentation in nested levels Co-authored-by: Anja Rabich --- marzipan/src/letfuncdecl.py | 68 +++++++++++++++++++++++++------------ marzipan/src/sample.pv | 8 +++++ 2 files changed, 55 insertions(+), 21 deletions(-) diff --git a/marzipan/src/letfuncdecl.py b/marzipan/src/letfuncdecl.py index d80a855e..771d37fe 100644 --- a/marzipan/src/letfuncdecl.py +++ b/marzipan/src/letfuncdecl.py @@ -25,6 +25,7 @@ this_module = sys.modules[__name__] pp = pprint.PrettyPrinter(indent=4, width=50) +DEBUG = False CONFIG = { "space": " ", @@ -53,6 +54,7 @@ CONFIG = { "line_break": "\n", "indentation_style": " " * 4, # 4 spaces "empty_lines_after_decl": "\n" * 1, + "break_after_n_list_elements": 4, } @@ -112,6 +114,9 @@ def pretty( return_str = "" + if DEBUG: + return_str += f"[c:{column}, f:{format_spec}, t:{type(value)}]" + # new line that is indented one column more if format_spec == "indentline": return_str += ctx.indentation_style * (column + 1) @@ -134,7 +139,8 @@ def pretty( ) = get_list_config(format_spec, ctx) if len(value) > 1: - if len(value) < 5: + break_after_n = 5 + if len(value) < break_after_n: return_str += ( left_bracket + list_separator.join( @@ -153,14 +159,16 @@ def pretty( left_bracket + list_separator.join( pretty(item, column=column, format_spec=format_spec, ctx=ctx) - for item in value[:5] + for item in value[:break_after_n] ) + list_separator + "\n" - + ctx.indentation_style * column - + list_separator.join( - pretty(item, column=column, format_spec=format_spec, ctx=ctx) - for item in value[5:] + + ctx.indentation_style * (column + 1) + + pretty( + value[break_after_n:], + column=column, + format_spec=format_spec, + ctx=ctx, ) + right_bracket ) @@ -383,12 +391,12 @@ class EventGterm(MarzipanAST): at: Optional[Ident] = None def pretty_print(self, column: int = 0) -> str: - str = "event (" - str += self.event_gterms.pretty_print() - str += ")" - if self.at is not None: - str += "@" + self.at.value - return str + return pretty_format( + self, + "event ({event_gterms:list.gterm})" + + ("@{at}" if self.at is not None else ""), + column=column, + ) @dataclass @@ -396,7 +404,11 @@ class ParenGterm(MarzipanAST): paren_gterms: GtermList def pretty_print(self, column: int = 0) -> str: - return "(" + self.paren_gterms.pretty_print() + ")" + return pretty_format( + self, + "({paren_gterms:list.gterm})", + column=column, + ) @dataclass @@ -462,9 +474,12 @@ class Gterm(MarzipanAST): LetGterm, ), ): - return self.gterm.pretty_print() + return pretty_format( + self, + "{gterm}", + column=column, + ) return "not implemented" - # return f"{' ' * indent}{self}" @dataclass @@ -500,7 +515,8 @@ class LetfunDecl(MarzipanAST): self, "letfun {ident}" + ("({typedecl})" if self.typedecl is not None else "") - + " =\n{pterm:indentline}.", + + " =\n{pterm:indentline}." + + "{ctx.empty_lines_after_decl}", column=column, ) @@ -511,10 +527,11 @@ class LemmaGterm(MarzipanAST): lemma: Optional[Lemma] = None def pretty_print(self, column: int = 0) -> str: - str = self.gterm.pretty_print() - if self.lemma is not None: - str += ";" + self.lemma.pretty_print() - return str + return pretty_format( + self, + "{gterm}" + ("; {lemma}" if self.lemma is not None else ""), + column=column, + ) @dataclass @@ -566,7 +583,11 @@ class Lemma(MarzipanAST): lemma: LemmaGterm | LemmaPublicVars | LemmaPublicVarsSecret def pretty_print(self, column: int = 0) -> str: - return self.lemma.pretty_print() + return pretty_format( + self, + "{lemma}", + column=column, + ) # def __post_init__(self): # print(f"[constructor] Lemma: lemma={self.lemma}") @@ -993,6 +1014,7 @@ def pretty_print(asttree: list): def parse(input: str): + global DEBUG parsetree = parser.parse(input) # print("=" * 100) # print("print parsetree") @@ -1023,6 +1045,10 @@ def parse(input: str): print_tree(clean_ast) print("=" * 100) + if DEBUG: + DEBUG = False + pretty_print(clean_ast) + DEBUG = True return pretty_print(clean_ast) # print("=" * 100) diff --git a/marzipan/src/sample.pv b/marzipan/src/sample.pv index 531f30a1..669d8fbf 100644 --- a/marzipan/src/sample.pv +++ b/marzipan/src/sample.pv @@ -2,6 +2,11 @@ type c. letfun foo (bar: bitstring, baz: int) = (5, foo, bar, barz, lol, rofl). + +lemma skp:kem_sk_prec; + let bumm = bla in + (one, two, three, four, five, six, seven, eight, nine, ten, eleven, twelve). + letfun foo (bar: bitstring, baz: int) = (). letfun foo (bar: bitstring, baz: int) = @@ -32,6 +37,9 @@ lemma k:kem_sk, kp:kem_sk_prec; @lemma "asymmetric secrecy: Secure SSKI is sufficient for ck secrecy after trusted InitHello transmission from responder perspective" lemma ck_ini:key, ck:key, any_psk:key, any_sskr:kem_sk, PSsski:kem_sk_prec, any_epki:kem_pk, any_epti:key, PSspti:seed_prec; let secure_spki = kem_pub(trusted_kem_sk(PSsski)) in + let secure_spti = rng_key(trusted_seed(PSspti, two, three, four, five, + six, seven, eight, nine, ten, + eleven, twelve)) in let secure_spti = rng_key(trusted_seed(PSspti)) in attacker(ck) && event(OskOinit_hello(ck_ini, ck, any_psk, any_sskr, secure_spki, any_epki, any_epti, secure_spti)).