Merge pull request FStarLang#2785 from FStarLang/aseem_tot_gtot_univs

Removing universes from Tot and GTot comps

.common.mk

@@ -33,5 +33,8 @@ endif
 # Passing RESOURCEMONITOR=1 will create .runlim files through the source tree with
 # information about the time and space taken by each F* invocation.
 ifneq ($(RESOURCEMONITOR),)
-	RUNLIM=runlim -p -o $@.runlim
+	ifneq ($(MONID),)
+		MONPREFIX=$(MONID).
+	endif
+	RUNLIM=runlim -p -o $@.$(MONPREFIX)runlim
 endif

.scripts/runlim_diff.py

@@ -0,0 +1,180 @@
+# This script compares two runlim runs and produces a scatter plot with linear regression
+#
+# It takes as input two identifiers, the identifiers for the new run and the old run resp.
+#
+# Suppose the requirement is to compare the runlim runs across two branches b1 and b2
+# First you would git checkout b1, and run F* with RESOURCEMONITOR=1 and MONID=1 (or any other identifier)
+# Then you would git checkout b2, and run F* with RESOURCEMONITOR=1 and MONID=2 (or something else)
+# And then you can invoke this script as `python3 runlim_diff.py 2 1`,
+#   and it would compare the run 2 with the baseline run 1
+#
+# It can be used across local changes also, not just to compare two branches
+#
+
+# a function that takes as input a filename, 2 hashtables, and a line
+# it removes the "[runlim] " prefix from the line
+# it splits the rest of the line into a list of strings
+# if the first element of the list is "time:", it adds the filename and the second string to the first hashtable
+# if the first element of the list is "space:", it adds the filename and the second string to the second hashtable
+# it returns the two hashtables
+def parse_line(filename, time, space, line):
+    line = line.replace("[runlim] ", "")
+    line = line.split()
+    if line[0] == "time:":
+        time[filename] = line[1]
+    elif line[0] == "space:":
+        space[filename] = line[1]
+    return time, space
+
+
+# a function that takes as input a filename, an identifier, and 2 hashtables
+# it opens the file and reads each line
+# it strips .identifier".runlim" from the filename
+# it calls parse_line on the on the resulting string, the 2 hashtables, and each line
+# it returns the 2 hashtables
+def parse_file(filename, identifier, time, space):
+    with open(filename) as f:
+        for line in f:
+            filename = filename.replace(".{}.runlim".format(identifier), "")
+            time, space = parse_line(
+                filename, time, space, line)
+    return time, space
+
+
+# a function that takes as input a directory
+# it lists all the files in the directory recursively
+# it returns the list of files
+
+
+def list_files(directory):
+    import os
+    files = []
+    for filename in os.listdir(directory):
+        if os.path.isfile(os.path.join(directory, filename)):
+            files.append(os.path.join(directory, filename))
+        else:
+            files = files + list_files(os.path.join(directory, filename))
+    return files
+
+
+# a function that takes as input an identifier
+# it creates 2 empty hashtables
+# it calls list_files on "." (the current directory)
+# it calls parse_file on all the files in the list with suffix .identifier".runlim"
+# it returns the 2 hashtables
+def parse_all(identifier):
+    time = {}
+    space = {}
+    files = list_files(".")
+    for filename in files:
+        if filename.endswith(".{}.runlim".format(identifier)):
+            time, space = parse_file(filename, identifier, time, space)
+    return time, space
+
+# a function that takes as input 2 hashtables
+# it creates one array
+# it iterates over the keys of the first hashtable
+# it adds the tuple (key, value in the first hashtable, value in the second hashtable, percentage difference of values of the first and second hashtables) to the array
+# it returns the array
+
+
+def diff_hashtables(hashtable1, hashtable2):
+    diff = []
+    for key in hashtable2:
+        if key in hashtable1:
+            diff.append((key, hashtable1[key], hashtable2[key], (float(
+                hashtable1[key]) - float(hashtable2[key])) / float(hashtable2[key]) * 100))
+        else:
+            print(key + " is in the base run but not the new run, dropping")
+    return diff
+
+# a function that takes as input an array of tuples
+# it sorts the array by the third element of the tuples
+# it returns the sorted array
+
+
+def sort_array(array):
+    return sorted(array, key=lambda x: x[2])
+
+# generate_scatter_plot is lift and shift from runlim_stats.py
+
+def generate_scatter_plot(sorted_lines, xlabel, ylabel, title):
+    import matplotlib.pyplot as plt
+    import numpy as np
+    # create an array of the query timing differences
+    x_axis = []
+    y_axis = []
+    for line in sorted_lines:
+        x_axis.append(float(line[2]))
+        y_axis.append(float(line[1]))
+    # plot the query timing differences
+    plt.scatter(x_axis, y_axis)
+    # label x-axis as xlabel
+    plt.xlabel(xlabel)
+    # label y-axis as ylabel
+    plt.ylabel(ylabel)
+    # add a linear regression line
+    # Fit linear regression via least squares with numpy.polyfit
+    # It returns an slope (b) and intercept (a)
+    # deg=1 means linear fit (i.e. polynomial of degree 1)
+    b, a = np.polyfit(x_axis, y_axis, deg=1)
+    print(title + " slope: " + str(b))
+    #print (title + "intercept: " + str(a))
+    # Create sequence of 100 numbers from 0 to 100
+    # find the maximum of the x_axis
+    max_x = max(x_axis)
+    xseq = np.linspace(0, max_x, num=1000)
+
+    # Plot regression line
+    plt.plot(xseq, a + b * xseq, color="k", lw=2.5)
+
+    # add a title
+    plt.title(title + "; Linear regression slope = " + str(b))
+
+    plt.show()
+
+# a function that takes as input a hashtable
+# it prints the hashtable
+# it exits the program
+
+
+def print_hashtable(hashtable):
+    import sys
+    for key in hashtable:
+        print(key + " " + hashtable[key])
+    sys.exit(0)
+
+# a function that takes as input two identifiers
+# it calls parse_all on the first identifier
+# it calls parse_all on the second identifier
+# it calls diff_hashtables on the two hashtables
+# it calls sort_array on the two arrays
+# it calls generate_scatter_plot on the two arrays with xlabel as the second identifier and ylabel as the first identifier and title as "F* runlim"
+
+
+def diff(identifier1, identifier2):
+    time1, space1 = parse_all(identifier1)
+    time2, space2 = parse_all(identifier2)
+    time_diff = diff_hashtables(time1, time2)
+    space_diff = diff_hashtables(space1, space2)
+    time_diff = sort_array(time_diff)
+    space_diff = sort_array(space_diff)
+    generate_scatter_plot(
+        time_diff, "ID " + identifier2, "ID " + identifier1, "F* runlim time")
+    generate_scatter_plot(
+        space_diff, "ID " + identifier2, "ID " + identifier1, "F* runlim space")
+
+# main function that parses two identifiers from the command line
+# it calls diff on the two identifiers
+
+
+def main():
+    import sys
+    if len(sys.argv) != 3:
+        print(
+            "Usage: python diff_runlim.py identifier1(the new run) identifier2(the old run)")
+        return
+    diff(sys.argv[1], sys.argv[2])
+
+
+main()

.scripts/runlim_stats.py → .scripts/runlim_diff_old.py

@@ -1,3 +1,9 @@
+#
+# NOTE: This file may soon be removed from the repository,
+#       superseded by runlim_diff.py that provides an easier
+#       API to compare two runlim runs
+#
+
 from array import array
 import re
 
@@ -162,4 +168,8 @@ def main():
     generate_scatter_plot(sorted_time_lines, file1, file2, "time")
 
 
+#
+# SEE THE NOTE AT THE BEGINNING OF THE FILE
+#
+
 main()

CHANGES.md

@@ -14,6 +14,13 @@ Guidelines for the changelog:
 # Version 0.9.7.0
 
 ## Tactics & Reflection
+  * PR https://github.com/FStarLang/FStar/pull/2785 changes the reflection syntax
+    for computation types, by removing universe field from the Total and GTotal
+    comps. It also moves the decreases clause to the general C_Eff case.
+
+    This is a breaking change for the reflection clients, but the regressions should
+    only be syntactic.
+
   * As a better fix for Bug2635, F* now has a memoizing core typechecker for total
     (including ghost terms that are total) terms. The unification solutions, including
     those computed in the tactics engine, are typechecked using this core typechecker.

examples/param/Param.fst

@@ -53,7 +53,7 @@ let rec param' (bvmap : bvmap) (t:term) : Tac term =
   | Tv_Arrow b c ->
     let bv, (q, _attrs) = inspect_binder b in
     begin match inspect_comp c with
-    | C_Total t2 _ _ ->
+    | C_Total t2 ->
       let t1 = (inspect_bv bv).bv_sort in
       // bv:t1 -> t2
 

examples/tactics/Printers.fst

@@ -48,7 +48,7 @@ let mk_print_bv (self : name) (f : term) (bv : bv) : Tac term =
 let mk_printer_type (t : term) : Tac term =
     let b = fresh_binder_named "arg" t in
     let str = pack (Tv_FVar (pack_fv string_lid)) in
-    let c = pack_comp (C_Total str u_unk []) in
+    let c = pack_comp (C_Total str) in
     pack (Tv_Arrow b c)
 
 

src/fstar/FStar.CheckedFiles.fst

@@ -40,7 +40,7 @@ module Dep     = FStar.Parser.Dep
  * detect when loading the cache that the version number is same
  * It needs to be kept in sync with prims.fst
  *)
-let cache_version_number = 46
+let cache_version_number = 47
 
 (*
  * Abbreviation for what we store in the checked files (stages as described below)