From 0a0445c72e005c328b4764f5fb0f8f38e7a55d60 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jul 2023 14:52:23 +0200
Subject: Start using namespaces in the Lean backend

---
 compiler/Pure.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 4a00dfb2..b251a005 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -18,16 +18,19 @@ module GlobalDeclId = A.GlobalDeclId
     (they monotonically increase across functions) while in {!module:Pure} we want
     the indices to start at 0 for every function.
  *)
-module LoopId = IdGen ()
+module LoopId =
+IdGen ()
 
 type loop_id = LoopId.id [@@deriving show, ord]
 
 (** We give an identifier to every phase of the synthesis (forward, backward
     for group of regions 0, etc.) *)
-module SynthPhaseId = IdGen ()
+module SynthPhaseId =
+IdGen ()
 
 (** Pay attention to the fact that we also define a {!E.VarId} module in Values *)
-module VarId = IdGen ()
+module VarId =
+IdGen ()
 
 type integer_type = T.integer_type [@@deriving show, ord]
 
@@ -723,6 +726,7 @@ type fun_sig_info = {
  *)
 type fun_sig = {
   type_params : type_var list;
+      (** TODO: we should analyse the signature to make the type parameters implicit whenever possible *)
   inputs : ty list;
       (** The input types.
 
-- 
cgit v1.2.3