From c5db01659937acfb928ac51c78ad90426d80b356 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 9 Apr 2024 13:53:05 +0200 Subject: [PATCH] fix(engine/backend): F*: `rec` qual. when interface mode PR #572 introduced basic support for non-mutual recursive definitions, but that was working only in the implementation-only mode. This PR fixes that: `rec` is now insterted in `fst` modules, no matter whether we produce an interface or not. --- engine/backends/fstar/fstar_backend.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 2d88b65e8..4b5896d80 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -802,9 +802,10 @@ struct params in let pat = F.pat @@ F.AST.PatApp (pat, pat_args) in + let qualifier = F.AST.(if is_rec then Rec else NoLetQualifier) in let impl = F.decl ~fsti:false - @@ F.AST.TopLevelLet (NoLetQualifier, [ (pat, pexpr body) ]) + @@ F.AST.TopLevelLet (qualifier, [ (pat, pexpr body) ]) in let interface_mode = ctx.interface_mode && not (List.is_empty params) in let ty = @@ -836,9 +837,7 @@ struct in let pat = F.pat @@ F.AST.PatAscribed (pat, (ty, None)) in let full = - F.decl - @@ F.AST.TopLevelLet - ((if is_rec then Rec else NoLetQualifier), [ (pat, pexpr body) ]) + F.decl @@ F.AST.TopLevelLet (qualifier, [ (pat, pexpr body) ]) in let intf = F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) in