Merge 0f105e1 into e50166c

README.md

@@ -65,12 +65,11 @@ Why use `scc`?
  - Large language support
  - Can ignore duplicate files
  - Has complexity estimations
+ - You need to tell the difference between Coq and Verilog in the same directory
 
 Why not use `scc`?
 
- - Unable to tell the difference between Coq and Verilog (currently, if enough people raise a bug it will be resolved)
  - You don't like Go for some reason
- - You are working on a Linux system with less than 4 CPU cores and really need the fastest counter possible (use loc or polyglot)
 
 ### Usage
 
@@ -307,7 +306,7 @@ Creole (creole)
 Crystal (cr)
 CSS (css)
 CSV (csv)
-Cython (pyx)
+Cython (pyx,pxi,pxd)
 D (d)
 Dart (dart)
 Device Tree (dts,dtsi)
@@ -451,7 +450,7 @@ SVG (svg)
 Swift (swift)
 Swig (i)
 Systemd (automount,device,link,mount,path,scope,service,slice,socket,swap,target,timer)
-SystemVerilog (sv,svh)
+SystemVerilog (sv,svh,v)
 TaskPaper (taskpaper)
 TCL (tcl)
 TeX (tex,sty)
@@ -463,6 +462,7 @@ TypeScript Typings (d.ts)
 Unreal Script (uc,uci,upkg)
 Ur/Web (ur,urs)
 Ur/Web Project (urp)
+V (v)
 Vala (vala)
 Varnish Configuration (vcl)
 Verilog (vg,vh)

examples/shared_extension/coq/Qabs.v

@@ -0,0 +1,168 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Export QArith.
+Require Export Qreduction.
+
+Hint Resolve Qlt_le_weak : qarith.
+
+Definition Qabs (x:Q) := let (n,d):=x in (Z.abs n#d).
+
+Lemma Qabs_case : forall (x:Q) (P : Q -> Type), (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P (Qabs x).
+Proof.
+intros x P H1 H2.
+destruct x as [[|xn|xn] xd];
+[apply H1|apply H1|apply H2];
+abstract (compute; discriminate).
+Defined.
+
+Add Morphism Qabs with signature Qeq ==> Qeq as Qabs_wd.
+intros [xn xd] [yn yd] H.
+simpl.
+unfold Qeq in *.
+simpl in *.
+change (Zpos yd)%Z with (Z.abs (Zpos yd)).
+change (Zpos xd)%Z with (Z.abs (Zpos xd)).
+repeat rewrite <- Z.abs_mul.
+congruence.
+Qed.
+
+Lemma Qabs_pos : forall x, 0 <= x -> Qabs x == x.
+Proof.
+intros x H.
+apply Qabs_case.
+reflexivity.
+intros H0.
+setoid_replace x with 0.
+reflexivity.
+apply Qle_antisym; assumption.
+Qed.
+
+Lemma Qabs_neg : forall x, x <= 0 -> Qabs x == - x.
+Proof.
+intros x H.
+apply Qabs_case.
+intros H0.
+setoid_replace x with 0.
+reflexivity.
+apply Qle_antisym; assumption.
+reflexivity.
+Qed.
+
+Lemma Qabs_nonneg : forall x, 0 <= (Qabs x).
+intros x.
+apply Qabs_case.
+auto.
+apply (Qopp_le_compat x 0).
+Qed.
+
+Lemma Zabs_Qabs : forall n d, (Z.abs n#d)==Qabs (n#d).
+Proof.
+intros [|n|n]; reflexivity.
+Qed.
+
+Lemma Qabs_opp : forall x, Qabs (-x) == Qabs x.
+Proof.
+intros x.
+do 2 apply Qabs_case; try (intros; ring);
+(intros H0 H1;
+setoid_replace x with 0;[reflexivity|];
+apply Qle_antisym);try assumption;
+rewrite Qle_minus_iff in *;
+ring_simplify;
+ring_simplify in H1;
+assumption.
+Qed.
+
+Lemma Qabs_triangle : forall x y, Qabs (x+y) <= Qabs x + Qabs y.
+Proof.
+intros [xn xd] [yn yd].
+unfold Qplus.
+unfold Qle.
+simpl.
+apply Z.mul_le_mono_nonneg_r;auto with *.
+change (Zpos yd)%Z with (Z.abs (Zpos yd)).
+change (Zpos xd)%Z with (Z.abs (Zpos xd)).
+repeat rewrite <- Z.abs_mul.
+apply Z.abs_triangle.
+Qed.
+
+Lemma Qabs_Qmult : forall a b, Qabs (a*b) == (Qabs a)*(Qabs b).
+Proof.
+intros [an ad] [bn bd].
+simpl.
+rewrite Z.abs_mul.
+reflexivity.
+Qed.
+
+Lemma Qabs_Qinv : forall q, Qabs (/ q) == / (Qabs q).
+Proof.
+  intros [n d]; simpl.
+  unfold Qinv.
+  case_eq n; intros; simpl in *; apply Qeq_refl.
+Qed.
+
+Lemma Qabs_Qminus x y: Qabs (x - y) = Qabs (y - x).
+Proof.
+ unfold Qminus, Qopp. simpl.
+ rewrite Pos.mul_comm, <- Z.abs_opp.
+ do 2 f_equal. ring.
+Qed.
+
+Lemma Qle_Qabs : forall a, a <= Qabs a.
+Proof.
+intros a.
+apply Qabs_case; auto with *.
+intros H.
+apply Qle_trans with 0; try assumption.
+change 0 with (-0).
+apply Qopp_le_compat.
+assumption.
+Qed.
+
+Lemma Qabs_triangle_reverse : forall x y, Qabs x - Qabs y <= Qabs (x - y).
+Proof.
+intros x y.
+rewrite Qle_minus_iff.
+setoid_replace (Qabs (x - y) + - (Qabs x - Qabs y)) with ((Qabs (x - y) + Qabs y) + - Qabs x) by ring.
+rewrite <- Qle_minus_iff.
+setoid_replace (Qabs x) with (Qabs (x-y+y)).
+apply Qabs_triangle.
+apply Qabs_wd.
+ring.
+Qed.
+
+Lemma Qabs_Qle_condition x y: Qabs x <= y <-> -y <= x <= y.
+Proof.
+ split.
+  split.
+   rewrite <- (Qopp_opp x).
+   apply Qopp_le_compat.
+   apply Qle_trans with (Qabs (-x)).
+   apply Qle_Qabs.
+   now rewrite Qabs_opp.
+  apply Qle_trans with (Qabs x); auto using Qle_Qabs.
+ intros (H,H').
+ apply Qabs_case; trivial.
+ intros. rewrite <- (Qopp_opp y). now apply Qopp_le_compat.
+Qed.
+
+Lemma Qabs_diff_Qle_condition x y r: Qabs (x - y) <= r <-> x - r <= y <= x + r.
+Proof.
+ intros. unfold Qminus.
+ rewrite Qabs_Qle_condition.
+ rewrite <- (Qplus_le_l (-r) (x+-y) (y+r)).
+ rewrite <- (Qplus_le_l (x+-y) r (y-r)).
+ setoid_replace (-r + (y + r)) with y by ring.
+ setoid_replace (r + (y - r)) with y by ring.
+ setoid_replace (x + - y + (y + r)) with (x + r) by ring.
+ setoid_replace (x + - y + (y - r)) with (x - r) by ring.
+ intuition.
+Qed.

examples/shared_extension/verilog/button_debounce.v

@@ -0,0 +1,79 @@
+// Copyright 2018 Schuyler Eldridge
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+`timescale 1ns / 1ps
+module button_debounce
+  #(
+    parameter
+    CLK_FREQUENCY  = 10_000_000,
+    DEBOUNCE_HZ    = 2
+    // These parameters are specified such that you can choose any power
+    // of 2 frequency for a debouncer between 1 Hz and
+    // CLK_FREQUENCY. Note, that this will throw errors if you choose a
+    // non power of 2 frequency (i.e. count_value evaluates to some
+    // number / 3 which isn't interpreted as a logical right shift). I'm
+    // assuming this will not work for DEBOUNCE_HZ values less than 1,
+    // however, I'm uncertain of the value of a debouncer for fractional
+    // hertz button presses.
+    )
+  (
+   input      clk,     // clock
+   input      reset_n, // asynchronous reset
+   input      button,  // bouncy button
+   output reg debounce // debounced 1-cycle signal
+   );
+
+  localparam
+    COUNT_VALUE  = CLK_FREQUENCY / DEBOUNCE_HZ,
+    WAIT         = 0,
+    FIRE         = 1,
+    COUNT        = 2;
+
+  reg [1:0]   state, next_state;
+  reg [25:0]  count;
+
+  always @ (posedge clk or negedge reset_n)
+    state <= (!reset_n) ? WAIT : next_state;
+
+  always @ (posedge clk or negedge reset_n) begin
+    if (!reset_n) begin
+      debounce <= 0;
+      count    <= 0;
+    end
+    else begin
+      debounce <= 0;
+      count    <= 0;
+      case (state)
+        WAIT: begin
+        end
+        FIRE: begin
+          debounce <= 1;
+        end
+        COUNT: begin
+          count <= count + 1;
+        end
+      endcase
+    end
+  end
+
+  always @ * begin
+    case (state)
+      WAIT:    next_state = (button)                  ? FIRE : state;
+      FIRE:    next_state = COUNT;
+      COUNT:   next_state = (count > COUNT_VALUE - 1) ? WAIT : state;
+      default: next_state = WAIT;
+    endcase
+  end
+
+endmodule

examples/shared_extension/vlang/users.v

@@ -0,0 +1,73 @@
+// Please share your thoughts, suggestions, questions, etc here:
+// https://github.com/vlang-io/V/issues/3
+
+// I'm very interested in your feedback.
+
+module main
+
+import json // V will automatically insert missing imports (like the goimports tool)
+import http
+
+// Right now V requires all consts to be uppercase.
+// I'm still not certain about this.
+const API_URL = 'https://vlang.io/users.json'
+
+// V will generate json.encode and json.decode functions for this type since
+// `json.decode([]User, ...)` is called later. This results in better
+// performance, since reflection is not used.
+struct User {
+	name          string // V will automatically format and align your code.
+	age           int    // No need to use an additional tool.
+	is_registered bool
+}
+
+fn main() {
+	// `http.get()` returns an optional string.
+	// V optionals combine the features of Rust's Option<T> and Result<T>.
+	// We must unwrap all optionals with `or`, otherwise V will complain.
+	s := http.get(API_URL) or {
+		// `err` is a reserved variable (not a global) that
+		// contains an error message if there is one
+		eprintln('Failed to fetch "users.json": $err')
+		// `or` blocks must end with `return`, `break`, or `continue`
+		return
+	}
+	// Types can be passed as arguments
+	users := json.decode([]User, s) or {
+		eprintln('Failed to parse users.json')
+		return
+	}
+	// Encoding JSON doesn't require a type, since V knows what type
+	// the variable `users` has
+	println(json.encode(users))
+	// Please note the difference between V and Go:
+	// when there's only one variable, it's a value, not an index.
+	for user in users {
+		println('$user.name: $user.age')
+	}
+	// `for` loop has an alternative form when an index is required:
+	for i, user in users {
+		println('$i) $user')
+		if !user.can_register() {
+			// V allows both ' and " to denote strings.
+			// However, for consistency V will replace " with '
+			// unless the string contains an apostrophe.
+			println("Can't register")
+		}
+	}
+}
+
+// The method declaration is the same as in Go.
+// There is one big difference. Here `u` can be either passed by value (User)
+// or by reference (&User). The compiler will make the right decision
+// depending on the size of the User struct. You no longer have to remember
+// which one to use. It works here because `u` can't be modified (it's not
+// marked as `mut`).
+fn (u User) can_register() bool {
+	return u.age >= 16
+}
+
+// Here `u` can be modified and it will always be a reference.
+fn (u mut User) register() {
+	u.is_registered = true
+}