Revert "tuple state (coq-community/coq-ext-lib#48 why)"

This reverts commit 31277b9.
vzaliva · Nov 13, 2018 · 956917a · 956917a
1 parent 31277b9
commit 956917a
Show file tree

Hide file tree

Showing 2 changed files with 60 additions and 49 deletions.
diff --git a/coq/LLVMGen/FSigmaHCOLtoIR.v b/coq/LLVMGen/FSigmaHCOLtoIR.v
@@ -89,67 +89,66 @@ Section WithState.
   Import MonadNotation.
   Local Open Scope monad_scope.
 
-  Definition IRState : Type :=
-    (
-      nat * (* block_count *)
-      nat * (* local_count *)
-      nat * (* void_count *)
-      (list (raw_id * typ)) (* vars *)
-    ).
+  Record IRState : Type :=
+    mkIRstate
+      {
+        block_count: nat ;
+        local_count: nat ;
+        void_count : nat ;
+        vars: list (raw_id * typ)
+      }.
 
-  Definition newState: IRState := (0,0,0,[]).
+  Definition newState: IRState :=
+    {|
+      block_count := 0 ;
+      local_count := 0 ;
+      void_count  := 0 ;
+      vars := []
+    |}.
 
   Variable state_m : Type -> Type.
   Context {Monad_m: Monad state_m}.
   Context {State_m: MonadState IRState state_m}.
 
   Definition incBlock (st:IRState): state_m unit :=
-    let '(block_count, local_count, void_count, vars) := st in
-    put (
-        S block_count,
-        local_count,
-        void_count,
-        vars
-      ).
+    put {|
+        block_count := S (block_count st);
+        local_count := local_count st ;
+        void_count := void_count st ;
+        vars := vars st
+      |}.
 
   Definition getNextBlock (st:IRState): block_id :=
-    let '(block_count, _, _ , _ ) := st in
-    Anon (Z.of_nat block_count).
+    Anon (Z.of_nat (block_count st)).
 
   Definition incLocal (st:IRState): state_m unit :=
-    let '(block_count, local_count, void_count, vars) := st in
-    put (
-        block_count,
-        S local_count,
-        void_count,
-        vars
-      ).
+    put {|
+      block_count := block_count st ;
+      local_count := S (local_count st) ;
+      void_count  := void_count st ;
+      vars := vars st
+    |}.
 
   Definition getNextLocal (st:IRState): local_id :=
-    let '(_, local_count, _, _) := st in
-    Anon (Z.of_nat local_count).
+    Anon (Z.of_nat (local_count st)).
 
   Definition incVoid (st:IRState): state_m unit:=
-    let '(block_count, local_count, void_count, vars) := st in
-    put (
-        block_count,
-        local_count,
-        S void_count,
-        vars
-      ).
+    put {|
+        block_count := block_count st ;
+        local_count := local_count st ;
+        void_count  := S (void_count st) ;
+        vars := vars st
+      |}.
 
-  Definition getNextVoid (st:IRState): Z :=
-    let '(_, _, void_count, _) := st in
-    Z.of_nat void_count.
+  Definition getNextVoid (st:IRState): Z := Z.of_nat (void_count st).
 
   Definition addVars (st:IRState) (newvars: list (raw_id * typ)): state_m unit :=
-    let '(block_count, local_count, void_count, vars) := st in
-    put (
-        block_count,
-        local_count,
-        void_count,
-        vars ++ newvars
-      ).
+    put {|
+        block_count := block_count st ;
+        local_count := local_count st ;
+        void_count  := void_count st ;
+        vars := vars st ++ newvars
+      |}.
 
   Definition allocTempArray
              {ft: FloatT}
@@ -263,6 +262,14 @@ Definition LLVMGen
            {ft: FloatT}
            (globals: list (string* (@FSHValType ft)))
            (fshcol: @FSHOperator ft i o) (funname: string)
-  : toplevel_entities (list block)
-  :=
-    evalState (LLVMGen_m (state IRState) globals fshcol funname) newState.
+  : toplevel_entities (list block) :=
+  @evalState IRState (toplevel_entities (list block))
+             (
+               @LLVMGen_m
+                 _
+                 _
+                 (MonadState_state IRState)
+                 i o ft
+                 globals fshcol funname
+             )
+             newState.
diff --git a/ml/test.ml b/ml/test.ml
@@ -35,6 +35,10 @@ let args =
 
 let _ =
   Arg.parse args (fun _ -> ())  "USAGE: ./test [-v] [-o file.ll]\n";
-  let ast = ocaml_LLVMGen (1+4) 1 [("D", FSHvecValType (Nat.of_int 3))] coq_DynWinFSHCOL "dynwin" in
-  output_ll_file !output_file_name ast ;
-  exit 0
+  match ocaml_LLVMGen (1+4) 1 [("D", FSHvecValType (Nat.of_int 3))] coq_DynWinFSHCOL "dynwin" with
+  | None ->
+     Printf.printf "Error: Compilation FSHCOL compilation failed!\n";
+     exit 1
+  | Some ast ->
+     output_ll_file !output_file_name ast ;
+     exit 0