Make Var a coercion

It was originally not due to failing the "uniform inheritance criteria", but this criteria is no longer required. This should ensure that variables are actually printed as strings, hiding the Var coercion, which will make code much more readable without the ugly hack of the `Var'` coercions. The massive fallout is due to removing many coercions Var' that were defined for specific type parameters, all of which can now use the single coercion on Var.
mit-pdos · Sep 6, 2024 · abaaea3 · abaaea3
1 parent 56984cd
commit abaaea3
Show file tree

Hide file tree

Showing 80 changed files with 1,612 additions and 114 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -13,6 +13,7 @@
 -arg -w -arg -deprecated-typeclasses-transparency-without-locality
 # Iris-disabled warnings
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-unknown-warning,-argument-scope-delimiter
+-arg -w -arg +ambiguous-paths
 -Q external/stdpp/stdpp stdpp
 -Q external/stdpp/stdpp_unstable stdpp.unstable
 -Q external/stdpp/stdpp_bitvector stdpp.bitvector

diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/comments.v b/external/Goose/github_com/goose_lang/goose/internal/examples/comments.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* 0consts.go *)
 

diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/rfc1813.v b/external/Goose/github_com/goose_lang/goose/internal/examples/rfc1813.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition PROGRAM : expr := #(U32 100003).
 

diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/simpledb.v b/external/Goose/github_com/goose_lang/goose/internal/examples/simpledb.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* Package simpledb implements a one-table version of LevelDB
 

diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import.v b/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import.v
@@ -4,7 +4,6 @@ From Perennial.goose_lang.trusted Require Import github_com.goose_lang.goose.int
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Bar: val :=
   rec: "Bar" <> :=

diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import/trusted_example.v b/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import/trusted_example.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Foo: val :=
   rec: "Foo" <> :=

diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/unittest/generic.v b/external/Goose/github_com/goose_lang/goose/internal/examples/unittest/generic.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition SliceMap (T:ty) (U:ty): val :=
   rec: "SliceMap" "f" "s" :=

diff --git a/external/Goose/github_com/goose_lang/std.v b/external/Goose/github_com/goose_lang/std.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* BytesEqual returns if the two byte slices are equal. *)
 Definition BytesEqual: val :=

diff --git a/external/Goose/github_com/mit_pdos/go_journal/alloc.v b/external/Goose/github_com/mit_pdos/go_journal/alloc.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* Allocator uses a bit map to allocate and free numbers. Bit 0
    corresponds to number 0, bit 1 to 1, and so on. *)

diff --git a/external/Goose/github_com/mit_pdos/go_journal/lockmap.v b/external/Goose/github_com/mit_pdos/go_journal/lockmap.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* lockmap is a sharded lock map.
 

diff --git a/external/Goose/github_com/mit_pdos/go_journal/util.v b/external/Goose/github_com/mit_pdos/go_journal/util.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Debug : expr := #0.
 

diff --git a/external/Goose/github_com/mit_pdos/go_nfsd/nfstypes.v b/external/Goose/github_com/mit_pdos/go_nfsd/nfstypes.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition PROGRAM : expr := #(U32 100003).
 

diff --git a/external/Goose/github_com/mit_pdos/gokv/bank.v b/external/Goose/github_com/mit_pdos/gokv/bank.v
@@ -6,7 +6,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition BAL_TOTAL : expr := #1000.
 

diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/example.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/example.v
@@ -7,7 +7,6 @@ From Goose Require github_com.mit_pdos.gokv.dmvcc.txnmgr.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition main: val :=
   rec: "main" <> :=

diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/index.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/index.v
@@ -4,7 +4,6 @@ From Goose Require github_com.mit_pdos.vmvcc.index.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* 0_server.go *)
 

diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/prophname.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/prophname.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Get: val :=
   rec: "Get" <> :=

diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/txn.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/txn.v
@@ -8,7 +8,6 @@ From Perennial.goose_lang.trusted Require Import github_com.mit_pdos.vmvcc.trust
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Clerk := struct.decl [
   "p" :: ProphIdT;

diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/txncoordinator.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/txncoordinator.v
@@ -4,7 +4,6 @@ From Goose Require github_com.mit_pdos.gokv.dmvcc.index.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* 0_server.go *)
 

diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/txnmgr.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/txnmgr.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* clerk.go *)
 

diff --git a/external/Goose/github_com/mit_pdos/gokv/erpc.v b/external/Goose/github_com/mit_pdos/gokv/erpc.v
@@ -5,7 +5,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* Implements "exactly-once RPCs" with a reply table. *)
 

diff --git a/external/Goose/github_com/mit_pdos/gokv/kv.v b/external/Goose/github_com/mit_pdos/gokv/kv.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Kv := struct.decl [
   "Put" :: (stringT -> stringT -> unitT)%ht;

diff --git a/external/Goose/github_com/mit_pdos/gokv/lockservice.v b/external/Goose/github_com/mit_pdos/gokv/lockservice.v
@@ -4,7 +4,6 @@ From Goose Require github_com.mit_pdos.gokv.kv.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition LockClerk := struct.decl [
   "kv" :: ptrT

diff --git a/external/Goose/github_com/mit_pdos/gokv/map_marshal.v b/external/Goose/github_com/mit_pdos/gokv/map_marshal.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition EncodeMapU64ToU64: val :=
   rec: "EncodeMapU64ToU64" "kvs" :=

diff --git a/external/Goose/github_com/mit_pdos/gokv/map_string_marshal.v b/external/Goose/github_com/mit_pdos/gokv/map_string_marshal.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition EncodeStringMap: val :=
   rec: "EncodeStringMap" "kvs" :=

diff --git a/external/Goose/github_com/mit_pdos/gokv/tutorial/basics.v b/external/Goose/github_com/mit_pdos/gokv/tutorial/basics.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Tracker := struct.decl [
   "mu" :: ptrT;

diff --git a/external/Goose/github_com/mit_pdos/gokv/tutorial/queue.v b/external/Goose/github_com/mit_pdos/gokv/tutorial/queue.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Queue := struct.decl [
   "queue" :: slice.T uint64T;

diff --git a/external/Goose/github_com/mit_pdos/gokv/vrsm/e.v b/external/Goose/github_com/mit_pdos/gokv/vrsm/e.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Notation Error := uint64T (only parsing).
 

diff --git a/external/Goose/github_com/mit_pdos/pav/cryptoffi.v b/external/Goose/github_com/mit_pdos/pav/cryptoffi.v
@@ -2,7 +2,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition HashLen : expr := #32.
 

diff --git a/external/Goose/github_com/mit_pdos/pav/cryptoutil.v b/external/Goose/github_com/mit_pdos/pav/cryptoutil.v
@@ -4,7 +4,6 @@ From Goose Require github_com.mit_pdos.pav.cryptoffi.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Notation Hasher := (slice.T byteT) (only parsing).
 

diff --git a/external/Goose/github_com/mit_pdos/pav/marshalutil.v b/external/Goose/github_com/mit_pdos/pav/marshalutil.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Notation errorTy := boolT (only parsing).
 

diff --git a/external/Goose/github_com/mit_pdos/pav/merkle.v b/external/Goose/github_com/mit_pdos/pav/merkle.v
@@ -6,7 +6,6 @@ From Goose Require github_com.mit_pdos.pav.cryptoutil.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Notation errorTy := boolT (only parsing).
 

diff --git a/external/Goose/github_com/mit_pdos/perennial_examples/alloc.v b/external/Goose/github_com/mit_pdos/perennial_examples/alloc.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition unit := struct.decl [
 ].

diff --git a/external/Goose/github_com/mit_pdos/rsm/distx.v b/external/Goose/github_com/mit_pdos/rsm/distx.v
@@ -4,7 +4,6 @@ From Goose Require github_com.goose_lang.std.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Value := struct.decl [
   "b" :: boolT;

diff --git a/external/Goose/github_com/mit_pdos/rsm/mpaxos.v b/external/Goose/github_com/mit_pdos/rsm/mpaxos.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Paxos := struct.decl [
 ].