coq/frontend: Speed up typechecking by avoiding a conversion

The previous strategy didn't do the final check (whether a rule had type unit_t,
or whether a function had the right output type) in the typechecker, leaving it
instead to the unification engine, so in RVCore the definition of rv_rules took
a while.

coq/ErrorReporting.v

@@ -15,7 +15,6 @@ Section TypeErrors.
   | SugaredConstructorInAst
   | UnboundVariable (var: var_t)
   | UnboundEnumMember (f: string) (sig: enum_sig)
-  | IncorrectRuleType (tau: type)
   | BasicError (msg: basic_error_message)
   | TooManyArguments (fn_name: fn_name_t) (nexpected: nat) (nextra: nat)
   | TooFewArguments (fn_name: fn_name_t) (nexpected: nat) (nmissing: nat).

coq/Extraction.v

@@ -20,7 +20,7 @@ Extraction "extracted.ml"
            Vect.vect_to_list Vect.vect_of_list Vect.Bits.to_nat Vect.index_to_nat Vect.vect_zip
            Syntax.scheduler
            Desugaring.desugar_action
-           TypeInference.type_action TypeInference.type_rule
+           TypeInference.tc_rule
            TypedSyntaxFunctions.unannot
            TypedSyntaxFunctions.scheduler_rules
            TypedSyntaxFunctions.action_mentions_var

coq/Frontend.v

@@ -95,9 +95,13 @@ Notation ">>> x <<<" :=
              esource := ErrSrc (ErrorHere x) |}) : error_messages.
 Global Open Scope error_messages.
 
-Notation desugar_and_tc_action R Sigma uaction args :=
+Notation desugar_and_tc_action R Sigma tau sig uaction :=
   (let desugared := desugar_action dummy_pos uaction in
-   type_action R Sigma dummy_pos args desugared).
+   tc_action R Sigma dummy_pos tau sig desugared).
+
+Notation desugar_and_tc_rule R Sigma uaction :=
+  (let desugared := desugar_action dummy_pos uaction in
+   tc_rule R Sigma dummy_pos desugared).
 
 Definition is_success {S F} (r: result S F) :=
   match r with
@@ -111,13 +115,29 @@ Definition extract_success {S F} (r: result S F) (pr: is_success r = true) :=
   | Failure f => fun pr => match Bool.diff_false_true pr with end
   end pr.
 
-Notation _must_succeed r :=
+Notation _must_succeed_conv r :=
+  (extract_success r (@eq_refl bool true : is_success r = true)).
+Notation _must_succeed_vm r :=
   (extract_success r (@eq_refl bool true <: is_success r = true)).
-
-Ltac _tc_action_fast R Sigma uaction args :=
-  let result := constr:(desugar_and_tc_action R Sigma uaction args) in
-  let typed := constr:(projT2 (_must_succeed result)) in
-  exact typed.
+Notation _must_succeed_native r :=
+  (extract_success r (@eq_refl bool true <<: is_success r = true)).
+
+Inductive TC_Strategy := TC_conv | TC_vm | TC_native.
+Ltac _tc_strategy := exact TC_vm.
+
+Ltac _extract_success r :=
+  let strategy := constr:(ltac:(_tc_strategy)) in
+  let eq_pr :=
+      match strategy with
+      | TC_conv => constr:(@eq_refl bool true : is_success r = true)
+      | TC_vm => constr:(@eq_refl bool true <: is_success r = true)
+      | TC_native => constr:(@eq_refl bool true <<: is_success r = true)
+      end in
+  exact (extract_success r eq_pr).
+
+Ltac _tc_action_fast R Sigma sig tau uaction :=
+  let result := constr:(desugar_and_tc_action R Sigma sig tau uaction) in
+  _extract_success result.
 
 Arguments place_error_beacon {var_t fn_name_t reg_t ext_fn_t} / rev_target current_path a : assert.
 
@@ -166,33 +186,31 @@ Ltac _report_typechecking_errors uaction tc_result :=
     fail "Unexpected typechecker output:" tc_result
   end.
 
-Ltac _tc_illtyped_action R Sigma uaction args :=
+Ltac _tc_illtyped_action R Sigma sig tau uaction :=
   let annotated := constr:(reposition PThis uaction) in
-  let result := constr:(desugar_and_tc_action R Sigma annotated args) in
+  let result := constr:(desugar_and_tc_action R Sigma sig tau annotated) in
   _report_typechecking_errors uaction result.
 
-Ltac _tc_action R Sigma uaction args :=
-  (_tc_action_fast R Sigma uaction args ||
-   _tc_illtyped_action R Sigma uaction args).
-
-Definition annotate_uaction_type {reg_t ext_fn_t}
-           (R: reg_t -> type) (Sigma: ext_fn_t -> Sig 1)
-           (ua: uaction reg_t ext_fn_t) :=
-  ua : uaction reg_t ext_fn_t.
-
-Ltac _arg_type R :=
-  match type of R with
-  | ?t -> _ => t
-  end.
+Ltac _tc_action R Sigma sig tau uaction :=
+  (_tc_action_fast R Sigma sig tau uaction ||
+   _tc_illtyped_action R Sigma sig tau uaction).
 
 (* FIXME: Find a way to propagate reg_t and ext_fn_t from R and Sigma to ua.
    With this users could write [tc_action R Sigma {{ skip }}] directly, without
    having to annotate the [{{ skip }}]. *)
-Notation tc_action R Sigma ua :=
-  (ltac:(_tc_action R Sigma ua (@List.nil (var_t * type)))) (only parsing).
+Notation tc_action R Sigma sig tau ua :=
+  (ltac:(_tc_action R Sigma sig tau ua)) (only parsing).
+
+Notation tc_rule R Sigma ua :=
+  (tc_action R Sigma (@List.nil (var_t * type)) unit_t ua) (only parsing).
 
 Notation tc_function R Sigma uf :=
-  (ltac:(_tc_action R Sigma (int_body uf) (int_argspec uf))) (only parsing).
+  (tc_action R Sigma (int_argspec uf) (int_retSig uf) (int_body uf)) (only parsing).
+
+Ltac _arg_type R :=
+  match type of R with
+  | ?t -> _ => t
+  end.
 
 Ltac _tc_rules R Sigma uactions :=
   let rule_name_t := _arg_type uactions in
@@ -203,7 +221,7 @@ Ltac _tc_rules R Sigma uactions :=
                               (* FIXME: why does the ‘<:’ above need this hnf? *)
                               let ua := constr:(uactions rr) in
                               let ua := (eval hnf in ua) in
-                              _tc_action R Sigma ua (@List.nil (var_t * type))
+                              _tc_action R Sigma (@List.nil (var_t * type)) constr:(unit_t) ua
                             end)) in
   exact res.
 

coq/TypeInference.v

@@ -74,9 +74,6 @@ Section TypeInference.
     Definition cast_action pos {sig tau1} tau2 (e: action sig tau1) :=
       cast_action' pos tau2 e (BasicError (TypeMismatch tau1 tau2)).
 
-    Definition cast_rule (pos: pos_t) {tau} (e: action [] tau) :=
-      cast_action' pos (bits_t 0) e (IncorrectRuleType tau).
-
     Notation EX Px := (existT _ _ Px).
 
     Fixpoint actpos {reg_t ext_fn_t} pos (e: uaction reg_t ext_fn_t) :=
@@ -180,8 +177,13 @@ Section TypeInference.
         Success (EX (APos pos ``e))
       end.
 
-    Definition type_rule (pos: pos_t) (e: uaction reg_t ext_fn_t) : result rule :=
-      let/res rl := type_action pos [] e in
-      cast_rule pos (``rl).
+    Definition tc_action (pos: pos_t)
+               (sig: tsig var_t) (expected_tau: type)
+               (e: uaction reg_t ext_fn_t) : result (action sig expected_tau) :=
+      let/res a := type_action pos sig e in
+      cast_action pos expected_tau (``a).
+
+    Definition tc_rule (pos: pos_t) (e: uaction reg_t ext_fn_t) : result rule :=
+      tc_action pos [] unit_t e.
   End Action.
 End TypeInference.

examples/rv/RVCore.v

@@ -818,9 +818,6 @@ Module RV32Core (RVP: RVParams).
         write0(cycle_count, read0(cycle_count) + |32`d1|)
     }}.
 
-  Definition tc_tick :=
-    tc_action R Sigma tick.
-
   Definition rv_register_name {n} (v: Vect.index n) :=
     match index_to_nat v with
     | 0  => "x00_zero" (* hardwired zero *)
@@ -915,22 +912,26 @@ Module RV32IParams <: RVParams.
   Definition NREGS := 32.
 End RV32IParams.
 
+(* TC_native adds overhead but makes typechecking large rules faster *)
+Ltac _tc_strategy ::= exact TC_native.
+
 Module RV32I <: Core.
   Include (RV32Core RV32IParams).
 
   Definition _reg_t := reg_t.
   Definition _ext_fn_t := ext_fn_t.
 
-  Definition tc_fetch := tc_action R Sigma fetch.
-  Definition tc_wait_imem := tc_action R Sigma wait_imem.
-  Definition tc_decode := tc_action R Sigma decode.
-  Definition tc_execute := tc_action R Sigma execute.
-  Definition tc_writeback := tc_action R Sigma writeback.
-  Definition tc_step_multiplier := tc_action R Sigma step_multiplier.
-  Definition tc_imem := tc_action R Sigma (mem imem).
-  Definition tc_dmem := tc_action R Sigma (mem dmem).
-
-  Definition rv_rules (rl:rv_rules_t) : rule R Sigma :=
+  Definition tc_fetch := tc_rule R Sigma fetch.
+  Definition tc_wait_imem := tc_rule R Sigma wait_imem.
+  Definition tc_decode := tc_rule R Sigma decode.
+  Definition tc_execute := tc_rule R Sigma execute.
+  Definition tc_writeback := tc_rule R Sigma writeback.
+  Definition tc_step_multiplier := tc_rule R Sigma step_multiplier.
+  Definition tc_imem := tc_rule R Sigma (mem imem).
+  Definition tc_dmem := tc_rule R Sigma (mem dmem).
+  Definition tc_tick := tc_rule R Sigma tick.
+
+  Definition rv_rules (rl: rv_rules_t) : rule R Sigma :=
     match rl with
     | Fetch          => tc_fetch
     | Decode         => tc_decode
@@ -958,16 +959,17 @@ Module RV32E <: Core.
   Definition _reg_t := reg_t.
   Definition _ext_fn_t := ext_fn_t.
 
-  Definition tc_fetch := tc_action R Sigma fetch.
-  Definition tc_wait_imem := tc_action R Sigma wait_imem.
-  Definition tc_decode := tc_action R Sigma decode.
-  Definition tc_execute := tc_action R Sigma execute.
-  Definition tc_writeback := tc_action R Sigma writeback.
-  Definition tc_step_multiplier := tc_action R Sigma step_multiplier.
-  Definition tc_imem := tc_action R Sigma (mem imem).
-  Definition tc_dmem := tc_action R Sigma (mem dmem).
-
-  Definition rv_rules (rl:rv_rules_t) : rule R Sigma :=
+  Definition tc_fetch := tc_rule R Sigma fetch <: rule R Sigma.
+  Definition tc_wait_imem := tc_rule R Sigma wait_imem <: rule R Sigma.
+  Definition tc_decode := tc_rule R Sigma decode <: rule R Sigma.
+  Definition tc_execute := tc_rule R Sigma execute <: rule R Sigma.
+  Definition tc_writeback := tc_rule R Sigma writeback <: rule R Sigma.
+  Definition tc_step_multiplier := tc_rule R Sigma step_multiplier <: rule R Sigma.
+  Definition tc_imem := tc_rule R Sigma (mem imem) <: rule R Sigma.
+  Definition tc_dmem := tc_rule R Sigma (mem dmem) <: rule R Sigma.
+  Definition tc_tick := tc_rule R Sigma tick.
+
+  Definition rv_rules (rl: rv_rules_t) : rule R Sigma :=
     match rl with
     | Fetch          => tc_fetch
     | Decode         => tc_decode

ocaml/cuttlebone/cuttlebone.ml

@@ -142,7 +142,6 @@ module Util = struct
     | OutOfBounds of { pos: int; sg: array_sig }
     | UnboundField of { field: string; sg: struct_sig }
     | UnboundEnumMember of { name: string; sg: enum_sig }
-    | IncorrectRuleType of { actual: typ }
     | TooManyArguments of { name: string; actual: int; expected: int }
     | TooFewArguments of { name: string; actual: int; expected: int }
     | TypeMismatch of { expected: typ; actual: typ }
@@ -158,8 +157,6 @@ module Util = struct
     | Extr.UnboundEnumMember (name, sg) ->
        UnboundEnumMember { name = string_of_coq_string name;
                            sg = enum_sig_of_extr_enum_sig sg }
-    | Extr.IncorrectRuleType tau ->
-       IncorrectRuleType { actual = typ_of_extr_type tau }
     | Extr.TooManyArguments (name, expected, nextras) ->
        TooManyArguments { name; expected; actual = expected + nextras }
     | Extr.TooFewArguments (name, expected, nmissing) ->
@@ -358,7 +355,7 @@ module Compilation = struct
 
   let typecheck_rule pos (ast: 'f extr_uaction) : ('f extr_action, ('f * _)) result =
     let desugared = Extr.desugar_action pos ast in
-    let typed = Extr.type_rule Util.string_eq_dec _R _Sigma pos desugared in
+    let typed = Extr.tc_rule Util.string_eq_dec _R _Sigma pos desugared in
     result_of_type_result typed
 
   let rec extr_circuit_equivb sz max_depth (c1: _ extr_circuit) (c2: _ extr_circuit) =

ocaml/frontends/lv.ml

@@ -438,7 +438,6 @@ module Errors = struct
       | OutOfBounds _ -> `TypeError
       | UnboundField _ -> `NameError
       | UnboundEnumMember _ -> `NameError
-      | IncorrectRuleType _ -> `TypeError
       | TooManyArguments _ -> `SyntaxError
       | TooFewArguments _ -> `SyntaxError
       | TypeMismatch _ -> `TypeError
@@ -458,9 +457,6 @@ module Errors = struct
          sprintf "Unbound field %a in %s" fquote field (struct_sig_to_string sg)
       | UnboundEnumMember { name; sg } ->
          sprintf "Enumerator %a is not a member of %s" fquote name (enum_sig_to_string sg)
-      | IncorrectRuleType { actual } ->
-         sprintf "This expression has type %a, but rules are expected to have type unit (bits 0)"
-           fquote (typ_to_string actual)
       | TooManyArguments { name; actual; expected } ->
          sprintf "Too many arguments in call to %a: expected %d, got %d"
            fquote name expected actual