Merge pull request #4204 from mtzguido/star-is-multiplication

Make * be multiplication by default

Author: mtzguido

.github/workflows/build-linux.yml

@@ -102,7 +102,7 @@ jobs:
       - name: Smoke test
         run: |
           ./fstar/bin/fstar.exe fstar/lib/fstar/ulib/Prims.fst -f
-          echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
+          echo -e "module A\let _ = assert (forall x. 1 + x*x > 0)" > A.fst
           ./fstar/bin/fstar.exe A.fst
           echo -e "module B\n#lang-pulse\nopen Pulse\nfn test (x:int) returns int { (x+1); }" > B.fst
           ./fstar/bin/fstar.exe --admit_smt_queries true B.fst

.github/workflows/build-macos.yml

@@ -83,7 +83,7 @@ jobs:
       - name: Smoke test
         run: |
           ./fstar/bin/fstar.exe --admit_smt_queries true fstar/lib/fstar/ulib/Prims.fst -f
-          echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
+          echo -e "module A\let _ = assert (forall x. 1 + x*x > 0)" > A.fst
           ./fstar/bin/fstar.exe --admit_smt_queries true A.fst
           echo -e "module B\n#lang-pulse\nopen Pulse\nfn test (x:int) returns int { (x+1); }" > B.fst
           ./fstar/bin/fstar.exe --admit_smt_queries true B.fst

.github/workflows/build-opam.yml

@@ -37,7 +37,7 @@ jobs:
 
       - name: Smoke test
         run: |
-          echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
+          echo -e "module A\let _ = assert (forall x. 1 + x*x > 0)" > A.fst
           eval $(opam env) && fstar.exe A.fst
           echo -e "module B\n#lang-pulse\nopen Pulse\nfn test (x:int) returns int { (x+1); }" > B.fst
           eval $(opam env) && fstar.exe B.fst

.github/workflows/build-windows.yml

@@ -181,7 +181,7 @@ jobs:
           cd fstar-*
           .\fstar\bin\fstar.exe fstar\lib\fstar\ulib\Prims.fst -f
           $PSDefaultParameterValues['Out-File:Encoding'] = 'utf8' # Make sure we write UTF-8 files
-          echo "module A`nopen FStar.Mul`nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
+          echo "module A`nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
           .\fstar\bin\fstar.exe --already_cached *,-A A.fst
           echo "module B`n#lang-pulse`nopen Pulse`nfn test (x:int) returns int { (x+1); }" > B.fst
           .\fstar\bin\fstar.exe B.fst

.github/workflows/nightly-ci.yml

@@ -35,7 +35,7 @@ jobs:
       - name: Smoke test
         run: |
           ./fstar/bin/fstar.exe fstar/lib/fstar/ulib/Prims.fst -f
-          echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
+          echo -e "module A\let _ = assert (forall x. 1 + x*x > 0)" > A.fst
           ./fstar/bin/fstar.exe A.fst
           echo -e "module B\n#lang-pulse\nopen Pulse\nfn test (x:int) returns int { (x+1); }" > B.fst
           ./fstar/bin/fstar.exe B.fst
@@ -74,7 +74,7 @@ jobs:
       - name: Smoke test
         run: |
           ./out/bin/fstar.exe out/lib/fstar/ulib/Prims.fst -f
-          echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
+          echo -e "module A\let _ = assert (forall x. 1 + x*x > 0)" > A.fst
           ./out/bin/fstar.exe A.fst
           echo -e "module B\n#lang-pulse\nopen Pulse\nfn test (x:int) returns int { (x+1); }" > B.fst
           ./out/bin/fstar.exe B.fst

.scripts/FStar.IntN.fstip

@@ -1,5 +1,4 @@
 open FStar.Int
-open FStar.Mul
 
 (* NOTE: anything that you fix/update here should be reflected in [FStar.UIntN.fstp], which is mostly
  * a copy-paste of this module. *)

.scripts/FStar.IntN.fstp

@@ -1,5 +1,4 @@
 open FStar.Int
-open FStar.Mul
 
 #set-options "--fuel 0 --ifuel 0"
 

.scripts/FStar.UIntN.fstip

@@ -20,7 +20,6 @@
 /// https://github.com/FStarLang/FStar/issues/1757
 
 open FStar.UInt
-open FStar.Mul
 
 (** Abstract type of machine integers, with an underlying
     representation using a bounded mathematical integer *)

.scripts/FStar.UIntN.fstp

@@ -1,5 +1,4 @@
 open FStar.UInt
-open FStar.Mul
 
 #set-options "--fuel 0 --ifuel 0"
 

.scripts/fstardoc/tests/backticks.fst

@@ -7,4 +7,4 @@ val op_Multiply           : int -> int -> Tot int
 let rec pow2 (x:nat) : Tot pos =
   match x with
   | 0  -> 1
-  | _  -> 2 `op_Multiply` (pow2 (x-1))
+  | _  -> 2 * (pow2 (x-1))