import Std.Data.HashMap

#check Std.HashMap String Nat 

typedef struct {
    int      m_rc; //reference counter - used for garbage collection 
    unsigned m_cs_sz:16; //object size - used for garbage collection
    unsigned m_other:8; //#fields of a constructor object or element size of array
    unsigned m_tag:8; //
} lean_object;


//linear logic applied to lean function arguments
//The "resource" is the reference counter of the ARGUMENT of some function call which can be consumed or not



/* The following typedef's are used to document the calling convention for the primitives. */
//All of these are just pointers to a lean_object

/* Standard object argument: 
Argument's reference counter is viewed as resource that is consumed when called by a function.
A function call like `f(lean_obj_arg x)` means it is safe to mutate aka "destructive update" `x` if the reference counter of x is 1.
[In C++, this is `f(shared_ptr<leanobj>&& x)` ]
 */
typedef lean_object * lean_obj_arg;   

/* Borrowed object argument convention:
We use this to say argument's reference counter doesnt automically get consumed when called by a function meaning it is responsibility of caller to decrement the reference counter.  
[In C++, this is `f(shared_ptr<leanobj> const& x)` ]
 */
typedef lean_object * b_lean_obj_arg; 

/* Unique (aka non shared) object argument. like unique_ptr in C++ */
typedef lean_object * u_lean_obj_arg; 

//Below are the function return conventions. Aka function will return a ptr to a leanObject and the convention tells us if we have to do something after the return. 

/*If a function return type is `lean_obj_res` then whoever called that function is responsible for consuming the reference counter. 
[In C++, this mean returning a smart_ptr by value] */
typedef lean_object * lean_obj_res;   /* Standard object result. */

/*Borrowed result, The caller is not responsible for decreasing the reference counter
[In C++, this means function returns `shared_ptr<leanobj> const&` aka a reference to a smart pointer. ] */
typedef lean_object * b_lean_obj_res; /* Borrowed object result. */

typedef struct {
    lean_external_finalize_proc m_finalize;
    lean_external_foreach_proc  m_foreach;
} lean_external_class;

LEAN_SHARED lean_external_class * lean_register_external_class(lean_external_finalize_proc, lean_external_foreach_proc);

/* Object for wrapping external data. */
typedef struct {
    lean_object           m_header;
    lean_external_class * m_class;
    void *                m_data;
} lean_external_object;