Code

New module system#1363

Code

Merged

yav merged 172 commits intomasterGaloisInc/cryptol:masterfrom functors-mergeGaloisInc/cryptol:functors-mergeCopy head branch name to clipboardJun 16, 2023

+10,027-29,476

Commits

Commits on Jun 13, 2022

• New module system

  yav

  committed
  6ab1470

  Copy full SHA for 6ab1470

Commits on Jun 14, 2022

• Don't crash on undefined names.

  Show description for 1e3ad37
  yav

  committed
  1e3ad37

  Copy full SHA for 1e3ad37

• Add an example of passing a submodule as an argument to a functor.

  yav

  committed
  3839b3a

  Copy full SHA for 3839b3a

• Remove unused things

  yav

  committed
  ed90c0a

  Copy full SHA for ed90c0a

• Make the remote API compile

  yav

  committed
  67b5bde

  Copy full SHA for 67b5bde

Commits on Jun 15, 2022

• only use top-level imports in implicit interface, get more tests working

  m-yac

  committed
  a643a19

  Copy full SHA for a643a19

Commits on Jun 21, 2022

• fix error for parameterized module instantiations, add tests like T5

  m-yac

  committed
  70d9600

  Copy full SHA for 70d9600

Commits on Jun 24, 2022

• Fix fixities not registering when defined in REPL

  qsctr

  committed
  4b3eac5

  Copy full SHA for 4b3eac5

Commits on Jul 14, 2022

• fix #1372 by excluding defns from functor instances in warnUnused

  m-yac

  committed
  2c179b1

  Copy full SHA for 2c179b1

• fix remaining tests

  m-yac

  committed
  2a8f755

  Copy full SHA for 2a8f755

• Implement functor imports with instantiation.

  Show description for 1419108
  yav

  committed
  1419108

  Copy full SHA for 1419108

• Update docs to document where imports

  yav

  committed
  26121c9

  Copy full SHA for 26121c9

• Fix spacing in a test

  yav

  committed
  488ceec

  Copy full SHA for 488ceec

• Implement insantiating imports with { }

  yav

  committed
  18e1b92

  Copy full SHA for 18e1b92

• Update documentation

  yav

  committed
  b76ec46

  Copy full SHA for b76ec46

• accept whitespace changes in mono-binds tests

  m-yac

  committed
  f9cd75b

  Copy full SHA for f9cd75b

• update AES examples with import instantiation syntax

  m-yac

  committed
  510d185

  Copy full SHA for 510d185

Commits on Jul 15, 2022

• Rename ModuleInstanceArg to ModuleInstanceNamedArg

  yav

  committed
  83f4575

  Copy full SHA for 83f4575

• Correct the order of declaratoins in functors.

  Show description for 5ece8bb
  yav

  committed
  5ece8bb

  Copy full SHA for 5ece8bb

• First stab at passing through functor parameters

  yav

  committed
  a2bc669

  Copy full SHA for a2bc669

Commits on Jul 18, 2022

• Add more tests for passing on parameters

  yav

  committed
  694282e

  Copy full SHA for 694282e

• Document passing through arguments

  yav

  committed
  ff30033

  Copy full SHA for ff30033

Commits on Jul 25, 2022

• Change 'signature' to interface, and also list funcotors

  yav

  committed
  62dddb0

  Copy full SHA for 62dddb0

• Use more descriptive names for internally generated names.

  Show description for 5bf24a2
  yav

  committed
  5bf24a2

  Copy full SHA for 5bf24a2

• Don't show unusable anonymous modules when browsing.

  yav

  committed
  84694d7

  Copy full SHA for 84694d7

• Clean up browsing of signatures

  yav

  committed
  24b1ba6

  Copy full SHA for 24b1ba6

• Don't discrad documentation during type checking

  yav

  committed
  9c9d0db

  Copy full SHA for 9c9d0db

• Use simple language

  yav

  committed
  180c90f

  Copy full SHA for 180c90f

• Detailed help for interfaces.

  Show description for d413e35
  yav

  committed
  d413e35

  Copy full SHA for d413e35

• Fix tests

  yav

  committed
  5c1b0bc

  Copy full SHA for 5c1b0bc

Commits on Jul 26, 2022

• Print documentation for module parameters when inside a functor

  yav

  committed
  d5d9f42

  Copy full SHA for d5d9f42

• Show fixities for value parameters.

  Show description for ccb563c
  yav

  committed
  ccb563c

  Copy full SHA for ccb563c

• Show documentation for modules, functors, and interfaces

  yav

  committed
  6e8ab5a

  Copy full SHA for 6e8ab5a

• Update test with new naming convention

  yav

  committed
  25f92f5

  Copy full SHA for 25f92f5

• Fix more tests

  yav

  committed
  a370845

  Copy full SHA for a370845

• Fix special cases for windows

  yav

  committed
  3eae908

  Copy full SHA for 3eae908

Commits on Aug 4, 2022

• Merge branch 'master' into functors-merge

  yav

  committed
  5b801fc

  Copy full SHA for 5b801fc

• Merge branch 'master' into functors-merge

  Show description for dfdbd12
  yav

  committed
  dfdbd12

  Copy full SHA for dfdbd12

Commits on Aug 12, 2022

• Merge remote-tracking branch 'origin/master' into functors-merge

  Show description for f77e5cc
  yav

  committed
  f77e5cc

  Copy full SHA for f77e5cc

• Fix typo

  yav

  committed
  bd55b96

  Copy full SHA for bd55b96

Commits on Sep 22, 2022

• Remove unused functoion

  yav

  committed
  516ad74

  Copy full SHA for 516ad74

• Resolve Has selectors for each nested module separately.

  Show description for ddcc67b
  yav

  committed
  ddcc67b

  Copy full SHA for ddcc67b

Commits on Sep 24, 2022

• Fix typos in comments

  yav

  committed
  09b68e2

  Copy full SHA for 09b68e2

• Don't try to get information for undefined names.

  Show description for b72a5d9
  yav

  committed
  b72a5d9

  Copy full SHA for b72a5d9

Commits on Sep 27, 2022

• Merge branch 'master' into functors-merge

  Show description for 441e163
  yav

  committed
  441e163

  Copy full SHA for 441e163

• Fix tests

  yav

  committed
  489ded4

  Copy full SHA for 489ded4

• Fix test

  yav

  committed
  6fea305

  Copy full SHA for 6fea305

Commits on Sep 28, 2022

• TraverseNames for EPropGuards

  yav

  committed
  bed32f8

  Copy full SHA for bed32f8

• Disallow foreign with the same name and in functors

  Show description for 4f8bc65
  yav

  committed
  4f8bc65

  Copy full SHA for 4f8bc65

• Update evaluator to account for TError of kind prop.

  Show description for 58a351c
  yav

  committed
  58a351c

  Copy full SHA for 58a351c

• Merge branch 'master' into functors-merge

  yav

  committed
  29e71d1

  Copy full SHA for 29e71d1

• Fix tests for Mac and Windows

  yav

  committed
  12967c4

  Copy full SHA for 12967c4

Commits on Sep 29, 2022

• Handle some more cases where fake names caused problems.

  Show description for 39c6026
  yav

  committed
  39c6026

  Copy full SHA for 39c6026

• Squash yet another fake name issue

  Show description for e1e3fe6
  yav

  committed
  e1e3fe6

  Copy full SHA for e1e3fe6

Commits on Oct 11, 2022

• Remove unused function

  yav

  committed
  3dc316a

  Copy full SHA for 3dc316a

• Add a function to support translation to SAW core

  yav

  committed
  043bd69

  Copy full SHA for 043bd69

• Add a function that can split up a module name in Text, rather than string

  yav

  committed
  91dbed4

  Copy full SHA for 91dbed4

Commits on Oct 13, 2022

• Include one Ubuntu 20.04 configuration (#1447)

  Show description for efc3fe7
  

  RyanGlScott

  authored and

  yav

  committed
  efc3fe7

  Copy full SHA for efc3fe7

• Pretty printing for Core Lint errors

  yav

  committed
  fa3cc20

  Copy full SHA for fa3cc20

• Don't use syntactic equality for numeric types, collect constraints instead

  Show description for 0cefb92
  yav

  committed
  0cefb92

  Copy full SHA for 0cefb92

• Filter out really trivial goals, so we can see the actual interesting goals

  yav

  committed
  f35648c

  Copy full SHA for f35648c

• Merge remote-tracking branch 'origin/T1451' into functors-merge

  Show description for ab0d1c8
  yav

  committed
  ab0d1c8

  Copy full SHA for ab0d1c8

Commits on Oct 14, 2022

• Preserve number of predicates in schema when applying a substitution

  Show description for b0ccbb7
  yav

  committed
  b0ccbb7

  Copy full SHA for b0ccbb7

• Rename "signature" to "interface" to follow standard naming

  yav

  committed
  b66d990

  Copy full SHA for b66d990

• Add pretty printing instances for parameters.

  Show description for 8de5a79
  yav

  committed
  8de5a79

  Copy full SHA for 8de5a79

• Allow loading interfaces.

  Show description for 8922877
  yav

  committed
  8922877

  Copy full SHA for 8922877

Commits on Oct 20, 2022

• Check that when evaluating things we do not use either value or type paramxs.

  Show description for 9701b37
  yav

  committed
  9701b37

  Copy full SHA for 9701b37

Commits on Oct 21, 2022

• Add/improve haddocks

  yav

  committed
  20f8a36

  Copy full SHA for 20f8a36

• Rename Signature to Iface + comments

  yav

  committed
  c5e8662

  Copy full SHA for c5e8662

Commits on Oct 25, 2022

• Have a go at allowing type synonyms in interfaces.

  Show description for dc4b344
  yav

  committed
  dc4b344

  Copy full SHA for dc4b344

• Use the location of the parameters as it is more accurate.

  yav

  committed
  bde2ecc

  Copy full SHA for bde2ecc

• Refactor to separate constraints and declarations. Order declarations properly.

  yav

  committed
  d0562af

  Copy full SHA for d0562af

• Make the help work for type synonyms defined in interfaces.

  yav

  committed
  4f4c202

  Copy full SHA for 4f4c202

• Add some tests

  yav

  committed
  1f6f7cc

  Copy full SHA for 1f6f7cc

• Update the documentation

  yav

  committed
  2d35953

  Copy full SHA for 2d35953

Commits on Oct 26, 2022

• Merge pull request #1461 from GaloisInc/functors-iface-tysyn

  Show description for 13cb103
  yav

  authored
  13cb103

  Copy full SHA for 13cb103

Commits on Nov 14, 2022

• Fix the pretty printing for interfaces.

  yav

  committed
  520eeae

  Copy full SHA for 520eeae

Commits on Nov 16, 2022

• Comment typo

  yav

  committed
  233caca

  Copy full SHA for 233caca

• Add a PP instance for TopEntity and improve PP instance for modules

  Show description for 151efaf
  yav

  committed
  151efaf

  Copy full SHA for 151efaf

• Fixes scoping issues with renaming instantiations

  Show description for 2c3bc87
  yav

  committed
  2c3bc87

  Copy full SHA for 2c3bc87

• Add some tests

  yav

  committed
  ced1c56

  Copy full SHA for ced1c56

• Fix tests

  yav

  committed
  7faf665

  Copy full SHA for 7faf665

• Don't touch fake names

  yav

  committed
  b5d7cfe

  Copy full SHA for b5d7cfe

• Another white space fix

  yav

  committed
  c2cda89

  Copy full SHA for c2cda89

Commits on Nov 21, 2022

• Don't panic if we fail to resolve a top-level instnatiation

  Show description for 18e3563
  yav

  committed
  18e3563

  Copy full SHA for 18e3563

Commits on Nov 22, 2022

• Merge remote-tracking branch 'origin/master' into functors-merge

  yav

  committed
  fa8fa46

  Copy full SHA for fa8fa46

• Checkpoint: store include-ed files

  yav

  committed
  b6f744f

  Copy full SHA for b6f744f

• Remove mImports from typechecked modules.

  Show description for fe00904
  yav

  committed
  fe00904

  Copy full SHA for fe00904

• Keep track of the files used by a module

  yav

  committed
  74ceb6b

  Copy full SHA for 74ceb6b

• Group file related information together.

  Show description for ef8391f
  yav

  committed
  ef8391f

  Copy full SHA for ef8391f

Commits on Nov 23, 2022

• Add a command to show dependencies in JSON

  Show description for 8416a91
  yav

  committed
  8416a91

  Copy full SHA for 8416a91

• Fix capitalization

  yav

  committed
  9071432

  Copy full SHA for 9071432

• Make it build

  yav

  committed
  6c88622

  Copy full SHA for 6c88622

Commits on Nov 24, 2022

• Add "file deps" to the Cryptol API

  yav

  committed
  20130d3

  Copy full SHA for 20130d3

Commits on Nov 28, 2022

• Merge remote-tracking branch 'origin/master' into file-deps

  yav

  committed
  ff6b9ac

  Copy full SHA for ff6b9ac

Commits on Nov 29, 2022

• Update docs

  yav

  committed
  b250383

  Copy full SHA for b250383

• Fix some tests

  yav

  committed
  e0560df

  Copy full SHA for e0560df

• Make the REPL and Python API more similar

  Show description for 3a66cea
  yav

  committed
  3a66cea

  Copy full SHA for 3a66cea

• Merge pull request #1473 from GaloisInc/file-deps

  Show description for 1dd175b
  yav

  authored
  1dd175b

  Copy full SHA for 1dd175b

Commits on Dec 1, 2022

• Add support for getting the dependencies of a module without loading it.

  Show description for e54971e
  yav

  committed
  e54971e

  Copy full SHA for e54971e

Commits on Dec 2, 2022

• File/module dependencies without loading

  yav

  committed
  1f1e56c

  Copy full SHA for 1f1e56c

• Fix test

  yav

  committed
  5987dbd

  Copy full SHA for 5987dbd

• Add a function to compute a dependency tree

  yav

  committed
  4014655

  Copy full SHA for 4014655

• Remove typing stuff

  yav

  committed
  2ef0d0d

  Copy full SHA for 2ef0d0d

• Add type annotations

  yav

  committed
  a85c3a9

  Copy full SHA for a85c3a9

Commits on Dec 5, 2022

• Merge pull request #1477 from GaloisInc/file-deps

  Show description for b35170a
  yav

  authored
  b35170a

  Copy full SHA for b35170a

Commits on Dec 12, 2022

• Add scaffolfing for backtick imports

  yav

  committed
  f834e24

  Copy full SHA for f834e24

Commits on Dec 13, 2022

• Make a module for the instantiation code

  yav

  committed
  02a5e80

  Copy full SHA for 02a5e80

• Rearrange so that each functor parameter can be "backtick" instantiated separately.

  Show description for e0d0135
  yav

  committed
  e0d0135

  Copy full SHA for e0d0135

Commits on Dec 16, 2022

• A not very tested implantation of backitick imports

  Show description for 99906b3
  yav

  committed
  99906b3

  Copy full SHA for 99906b3

Commits on Dec 19, 2022

• Have a go at fixing #1483

  Show description for 3d4f2ab
  yav

  committed
  3d4f2ab

  Copy full SHA for 3d4f2ab

Commits on Dec 20, 2022

• Add some tests

  yav

  committed
  e0d5952

  Copy full SHA for e0d5952

• Fixes #1484

  yav

  committed
  bf99953

  Copy full SHA for bf99953

• Remove a bunch of SAFE annotation.

  Show description for b3a0858
  yav

  committed
  b3a0858

  Copy full SHA for b3a0858

• Debugging code to dump parsed AST

  yav

  committed
  cfa6d8f

  Copy full SHA for cfa6d8f

• Disallow direct functor instantiation in interfaces.

  Show description for f36dbb4
  yav

  committed
  f36dbb4

  Copy full SHA for f36dbb4

• Remove debugging stuff

  yav

  committed
  4b70911

  Copy full SHA for 4b70911

• Syntactic sugar to support backtick imports

  yav

  committed
  7f7fc61

  Copy full SHA for 7f7fc61

Commits on Dec 21, 2022

• During backtick instantiation pass all value parameters in a record

  Show description for 40149dc
  yav

  committed
  40149dc

  Copy full SHA for 40149dc

• Fix windows test

  yav

  committed
  213bb3a

  Copy full SHA for 213bb3a

• Bugfix, apply substitution to schema's constraints.

  yav

  committed
  ca7c47b

  Copy full SHA for ca7c47b

• Check for repeated parameter names in types

  yav

  committed
  b527506

  Copy full SHA for b527506

• Apply the substitution after fixing up the types in module parameters.

  yav

  committed
  b96f77f

  Copy full SHA for b96f77f

Commits on Dec 22, 2022

• Add a function for updating the identifier of a name

  yav

  committed
  e191927

  Copy full SHA for e191927

• Keep track of the qualifiers of module parameters in the typed AST

  yav

  committed
  7c9e75e

  Copy full SHA for 7c9e75e

• Change the names of the parametres in _ imports

  Show description for 94d60a8
  yav

  committed
  94d60a8

  Copy full SHA for 94d60a8

• Update the reference manual to document instantiating with _

  yav

  committed
  7f793d7

  Copy full SHA for 7f793d7

• Merge pull request #1481 from GaloisInc/T1480

  Show description for 98dc7f5
  yav

  authored
  98dc7f5

  Copy full SHA for 98dc7f5

Commits on Jan 13, 2023

• Sync up with poetry.lock on master

  yav

  committed
  5906cbc

  Copy full SHA for 5906cbc

• Merge branch 'master' into functors-merge

  yav

  committed
  f2d8476

  Copy full SHA for f2d8476

• Fix comment to avoid confusing haddock

  yav

  committed
  069957d

  Copy full SHA for 069957d

Commits on Jan 19, 2023

• Eliminate location information when matching application/abstractions.

  

  Iavor Diatchki

  committed
  c0ff727

  Copy full SHA for c0ff727

Commits on Feb 9, 2023

• Change parsing of type declarations.

  Show description for 697d2c1
  yav

  committed
  697d2c1

  Copy full SHA for 697d2c1

• Rename test to match issues, and add expected output

  yav

  committed
  fa5b155

  Copy full SHA for fa5b155

• Keep track of locations in constraints arising from module instantiating

  Show description for ce8b1e2
  yav

  committed
  ce8b1e2

  Copy full SHA for ce8b1e2

Commits on Feb 10, 2023

• Fix tests

  yav

  committed
  14c4a89

  Copy full SHA for 14c4a89

• Fix incorrect conversion to JSON.

  Show description for 46b1719
  yav

  committed
  46b1719

  Copy full SHA for 46b1719

Commits on Feb 14, 2023

• Pretty print intervals with a given name map

  yav

  committed
  ed39cce

  Copy full SHA for ed39cce

• Add a function that allows us to do some reasoning in the context of a bunch of constraints

  yav

  committed
  1dded87

  Copy full SHA for 1dded87

Commits on Feb 15, 2023

• Expose some of the lower level operations for doing proofs

  yav

  committed
  77f7b65

  Copy full SHA for 77f7b65

Commits on Mar 6, 2023

• Merge branch 'master' into functors-merge

  yav

  committed
  9b63a18

  Copy full SHA for 9b63a18

Commits on Mar 23, 2023

• cryptol module docs: tightened some writing, fixed some typos, and introduced the term 'functor' as it was used without definition.

  

  Ian Sweet

  committed
  6ee9220

  Copy full SHA for 6ee9220

• Use standard definition

  yav

  committed
  ca0310f

  Copy full SHA for ca0310f

• Remove id application that does nothing

  yav

  committed
  b669a61

  Copy full SHA for b669a61

• Unused extensions

  yav

  committed
  ba30b60

  Copy full SHA for ba30b60

• Apply substitution to embedded newtype definition as well

  Show description for 7f078c3
  yav

  committed
  7f078c3

  Copy full SHA for 7f078c3

• Some code to print a full newypt declaration

  yav

  committed
  0d271bc

  Copy full SHA for 0d271bc

• Add a test

  yav

  committed
  8a43ba6

  Copy full SHA for 8a43ba6

Commits on Mar 24, 2023

• Merge branch 'master' into functors-merge

  Show description for c9bdd5d
  yav

  committed
  c9bdd5d

  Copy full SHA for c9bdd5d

• bring up to date with functors-merge

  

  Ian Sweet

  committed
  24a708b

  Copy full SHA for 24a708b

• Merge pull request #1509 from GaloisInc/functors-merge-doc-cleanup

  Show description for 3c5f6ff
  yav

  authored
  3c5f6ff

  Copy full SHA for 3c5f6ff

Commits on Mar 28, 2023

• Print nested functors also

  yav

  committed
  f49261f

  Copy full SHA for f49261f

• Apply substitution to nested functors as well

  Show description for 4c269e8
  yav

  committed
  4c269e8

  Copy full SHA for 4c269e8

• Fix test

  yav

  committed
  70a1592

  Copy full SHA for 70a1592

• Fix more tests

  yav

  committed
  cbd87a8

  Copy full SHA for cbd87a8

• Add a test for #1510

  yav

  committed
  0289fbf

  Copy full SHA for 0289fbf

Commits on Mar 29, 2023

• Fix typos in comments

  yav

  committed
  cb551e4

  Copy full SHA for cb551e4

• Things that depend on newtype constructors should depend on the newtypes

  Show description for 05412e9
  yav

  committed
  05412e9

  Copy full SHA for 05412e9

Commits on Apr 20, 2023

• Add a PP instance to PrimIdent

  yav

  committed
  396b02b

  Copy full SHA for 396b02b

Commits on Apr 25, 2023

• Merge branch 'master' into functors-merge

  Show description for abbece3
  yav

  committed
  abbece3

  Copy full SHA for abbece3

Commits on May 5, 2023

• Fix name export, to just put the module name the "module" field

  yav

  committed
  1543bed

  Copy full SHA for 1543bed

• Merge branch 'master' into functors-merge

  Show description for 5dafbe4
  yav

  committed
  5dafbe4

  Copy full SHA for 5dafbe4

Commits on May 15, 2023

• Merge branch 'master' into functors-merge

  yav

  committed
  64d5800

  Copy full SHA for 64d5800

Commits on May 23, 2023

• Restrict PrimMap to only refer to actual primtives.

  Show description for 31da6cb
  yav

  committed
  31da6cb

  Copy full SHA for 31da6cb

• Make the remote-api build

  yav

  committed
  de33458

  Copy full SHA for de33458

Commits on May 24, 2023

• Revert breaking change.

  Show description for 9addbc6
  yav

  committed
  9addbc6

  Copy full SHA for 9addbc6

• Remove some warnings

  yav

  committed
  f7d6a14

  Copy full SHA for f7d6a14

• Remove repeated extension

  yav

  committed
  141fe3a

  Copy full SHA for 141fe3a

• Refactor to avoid using eiter, and preserve a bit more context

  yav

  committed
  614898f

  Copy full SHA for 614898f

• Add a function to compute a mapping from original names to names from an interface.

  Show description for ed0d3fb
  yav

  committed
  ed0d3fb

  Copy full SHA for ed0d3fb

Commits on May 25, 2023

• Merge branch 'master' into functors-merge

  Show description for 77fd64f
  yav

  committed
  77fd64f

  Copy full SHA for 77fd64f

Commits on Jun 16, 2023

• Merge branch 'master' into functors-merge

  yav

  committed
  179c2cf

  Copy full SHA for 179c2cf