take ports into account in IRR generation

src/irr/eval_irr.v

@@ -365,11 +365,16 @@ Section eval_irr.
   (* TODO how to handle uninitialized? *)
 
   (* TODO return bitvector instead? *)
+  Variable ports_env: string_map value.
   Fixpoint eval_irr (expr: irr_expression) (fuel: nat) : value + error :=
     match fuel with
     | 0 => inr {| cause := error_not_enough_fuel; info := "eval_irr" |}
     | S fuel =>
     match expr with
+    | irr_ref r =>
+      let/err e := N2expr r in
+      eval_irr e fuel
+    | irr_port p => map.get ports_env p
     | irr_uconst        c => inl (mk_unsigned  c)
     | irr_sconst        c => inl (mk_signed    c)
     | irr_vconst t n    c => inl (mk_vector_bv t n c)
@@ -378,9 +383,6 @@ Section eval_irr.
     | irr_as_enum_tag variants tag e =>
       let/err e := eval_irr e fuel in
       mk_enum variants tag e
-    | irr_ref r =>
-      let/err e := N2expr r in
-      eval_irr e fuel
     | irr_mux sel port_a port_b | irr_when sel port_a port_b =>
       let/err sel_v := eval_irr sel fuel in
       match bitvector_to_bool (data sel_v) with

src/irr/irr.v

@@ -7,6 +7,7 @@ Section irr.
   Inductive irr_expression :=
   (* Reference *)
   | irr_ref (n: N)
+  | irr_port (name: string)
   (* Nullary *)
   | irr_uconst (constant: bitvector) | irr_sconst (constant: bitvector)
   | irr_vconst (t: type) (n: N) (constant: bitvector)

src/irr/pre_irr.v

@@ -6,6 +6,9 @@ From COQQTL.irr   Require Import irr.
 From COQQTL.value Require Import type type_util.
 Import ListNotations.
 
+(* Pre-IRR expressions are like IRR expressions except that they still contain
+   id-based references. *)
+
 Section pre_irr.
   Inductive pre_irr_expression :=
   (* References *)

src/statement/TEMP_test.v

@@ -53,7 +53,7 @@ Definition stmt_to_irr (s: statement.statement) (ports: list port) :=
   let id2type  := id2type_local  name2mod resolve_type lg in
   let rid2type := rid2type_local name2mod resolve_type lg in
   let/err lg   := preprocess_log name2mod resolve_type rid2type lg in
-  generate_irr id2type rid2type lg.
+  generate_irr id2type rid2type lg ports.
 
 Definition clock := {|
   p_name := "cl"; p_direction := input; p_type := ur_clock_t

src/statement/log_to_irr.v

@@ -2,7 +2,7 @@ From Coq              Require Import List NArith String.
 From stdpp            Require Import gmap.
 From mbty_std         Require Import option list.
 From bitvector        Require Import bitvector.
-From COQQTL.module    Require Import module.
+From COQQTL.module    Require Import module port.
 From COQQTL.util      Require Import error map misc set id syntax_tree_position.
 From COQQTL.value     Require Import component type type_util value.
 From COQQTL.irr       Require Import irr pre_irr pre_irr_to_irr.
@@ -870,7 +870,7 @@ Section log_to_irr.
       from.
 
   Definition generate_traversal_order (lg: @log_with_deps pre_irr_expression)
-  : _ + error :=
+  : list id + error :=
     let/err inputs              := gather_input rid2type lg in
     let/err statefuls           := gather_stateful lg in
     let/err relevant_ids        := gather_relevant_ids rid2type lg in
@@ -889,7 +889,25 @@ Section log_to_irr.
     let/err tr := traversal relevant_deps in
     inl (List.rev tr).
 
-  Definition generate_irr (lg: @log_with_deps pre_irr_expression) : _ + error :=
+  Definition generate_irr
+    (lg: @log_with_deps pre_irr_expression) (ports: list port)
+  : _ + error :=
+    (* First, we generate a node for each available port *)
+    let/err res :=
+      fold_left_err
+        (fun '(irr_vars, next_free_id, id_N_map) port =>
+          let port_id := ([], p_name port, []) in
+          let irr_vars :=
+            map.set irr_vars next_free_id (irr_port (p_name port))
+          in
+          let id_N_map := map.set id_N_map port_id next_free_id in
+          inl (irr_vars, (next_free_id + 1)%N, id_N_map)
+        )
+        ports
+        (map.empty, 0%N, map.empty)
+    in
+    let '(irr_vars, next_free_id, id_N_map) := res in
+    (* Only then do we handle the log *)
     let/err tr := generate_traversal_order lg in
     let connections :=
       annotate_connection_tree_with_cond_ids (connections_wd lg)
@@ -907,5 +925,5 @@ Section log_to_irr.
         inl (irr_vars, next_free_id, cond_irr_exprs, id_N_map)
       )
       tr
-      (map.empty, 0%N, map.empty, map.empty).
+      (irr_vars, next_free_id, map.empty, id_N_map).
 End log_to_irr.