Merge saw-core repo#1213

Merged

brianhuffman merged 2231 commits intomasterfrom merge-saw-core-repo

Apr 26, 2021

+35,416-12

This pull request is big! We're only showing the most recent 250 commits

Commits on Oct 19, 2020

use eauto for intro + destructing, clean up CompMExtra a bit
m-yac
committed
Specialize some occurrences of the Value type to TValue.
Brian Huffman
committed
Change VVecType to use Natural for its size argument.
Brian Huffman
committed

Commits on Oct 20, 2020

Add VSort constructor, and remove now-unnecessary VType.
Brian Huffman
committed
Merge pull request #91 from GaloisInc/tvalue
brianhuffman
authored
Support uninterpreted polymorphic functions in sbv/what4 backends.
Brian Huffman
committed
Improve error messages for failed uninterpreted functions.
Brian Huffman
committed
add Exists and Forall ArgNames
m-yac
committed

Commits on Oct 21, 2020

Merge pull request #92 from GaloisInc/unint-poly
brianhuffman
authored

Commits on Oct 23, 2020

Modify saw-core external-format parser to use fresh ExtCns indices.
Brian Huffman
committed
Merge pull request #96 from GaloisInc/external-format
brianhuffman
authored

Commits on Oct 27, 2020

Fix type error in saw-core tests
Aaron Tomb
committed

Commits on Oct 28, 2020

Commits on Nov 3, 2020

Add TValue constructor for IntMod type.
Brian Huffman
committed
Avoid using error within what4 backend.
Brian Huffman
committed
Add VIntMod constructor to Value datatype.
Brian Huffman
committed
Add scIntModType to SharedTerm library.
Brian Huffman
committed
Add function asIntModType to Recognizer library.
Brian Huffman
committed
Add constructor FOTIntMod to FirstOrderType datatype.
Brian Huffman
committed
Correctly handle uninterpreted functions on IntMod in sbv/what4 backends.
Brian Huffman
committed
Remove duplicated code.
Brian Huffman
committed
Add function scToIntMod to SharedTerm library.
Brian Huffman
committed
Add FOVIntMod constructor to FirstOrderValue datatype.
Brian Huffman
committed
saw-core-what4: Add IntModLabel to Labeler type.
Brian Huffman
committed
Use safeSymbol instead of userSymbol to avoid an error case.
Brian Huffman
committed
Merge pull request #93 from GaloisInc/intmod
brianhuffman
authored

Commits on Nov 11, 2020

Reimplement getAllExtSet and getConstantSet using Data.IntSet.
Brian Huffman
committed

Commits on Nov 12, 2020

Merge pull request #100 from GaloisInc/intset
brianhuffman
authored

Commits on Nov 13, 2020

Commits on Nov 16, 2020

Commits on Nov 17, 2020

Merge pull request #26 from GaloisInc/structured-names
robdockins
authored

Commits on Nov 19, 2020

Adapt to GaloisInc/cryptol#964 tc-errors.
Brian Huffman
committed

Commits on Nov 20, 2020

Merge pull request #104 from GaloisInc/tc-errors
brianhuffman
authored

Commits on Nov 22, 2020

Convert from ansi-wl-pprint package to prettyprinter.
Brian Huffman
committed

Commits on Nov 23, 2020

Add name to error message about uninterpreted higher-order functions.
Brian Huffman
committed
Merge pull request #102 from GaloisInc/saw-script-issue906
brianhuffman
authored

Commits on Nov 24, 2020

Switch from ansi-wl-pprint to the prettyprinter package.
Brian Huffman
committed
Use custom document style type for semantic prettyprinter annotations.
Brian Huffman
committed
Remove mentions of ansi-wl-pprint from cabal files.
Brian Huffman
committed
Rename Doc type synonym to SawDoc.
Brian Huffman
committed
Use standard prettyprinter combinators instead of locally-defined ones.
Brian Huffman
committed
Merge pull request #106 from GaloisInc/prettyprinter
brianhuffman
authored
Fix implementation of fromIntMod in concrete evaluation backend.
Brian Huffman
committed
Merge pull request #28 from GaloisInc/prettyprinter
brianhuffman
authored

Commits on Nov 25, 2020

Merge pull request #109 from GaloisInc/fix-fromIntMod
brianhuffman
authored

Commits on Nov 30, 2020

Fix reference primitives. (#110 )
andreistefanescu
authored

Commits on Dec 1, 2020

Use OverloadedStrings for prettyprinter Doc type.
Brian Huffman
committed
Use FieldName type synonym more consistently.
Brian Huffman
committed
Define type FieldName = Text instead of String.
Brian Huffman
committed

Commits on Dec 2, 2020

Fix translatePi so that it properly translates bound variables.
Brian Huffman
committed
Fix incorrect local variable environment when translating lambdas.
Brian Huffman
committed
Fix incorrect local variable environment when translating terms.
Brian Huffman
committed
Heapster bound names (#29 )
brianhuffman
authored
re-generated Coq files
Eddy Westbrook
committed

Commits on Dec 5, 2020

Merge branch 'master' into bound-names
brianhuffman
authored
Merge pull request #32 from GaloisInc/bound-names
brianhuffman
authored

Commits on Dec 7, 2020

Merge branch 'master' into wip-heapster-merge
Default Galois
committed
preparation for merge
Karl Smeltzer
committed
Merge branch 'master' into wip-heapster
Karl Smeltzer
committed
Merge branch 'wip-heapster-merge' of https://github.com/GaloisInc/saw-core-coq into wip-heapster-merge
Karl Smeltzer
committed
resolve missed conflict
Karl Smeltzer
committed
Avoid outputting any ANSI codes when color option is disabled.
Brian Huffman
committed
fixed pretty-printing for identifiers that start with "@" by adding parens when needed
Eddy Westbrook
committed

Commits on Dec 9, 2020

Make ruleOfProp return a Maybe instead of calling error.
Brian Huffman
committed
Remove redundant $ in function applications with record syntax.
Brian Huffman
committed
Merge pull request #112 from GaloisInc/ruleOfProp
brianhuffman
authored
whoops, bvToInt was actually intToBV!
Eddy Westbrook
committed
whoops, wrong definition for bvToInt
Eddy Westbrook
committed

Commits on Dec 10, 2020

changed the way record projections are represented in Coq, to handle #34
Eddy Westbrook
committed
Fix incorrect implementation of intModUnOp in sbv backend.
Brian Huffman
committed

Commits on Dec 11, 2020

Merge pull request #115 from GaloisInc/issue114
brianhuffman
authored

Commits on Jan 5, 2021

Adds bvShl and enables CryptolPrimitivesForSAWCore to build
Default Galois
committed

Commits on Jan 16, 2021

Merge pull request #111 from GaloisInc/text-fieldname
brianhuffman
authored
Adapt to GaloisInc/saw-core#111 , which uses Data.Text for FieldName.
Brian Huffman
committed
Merge pull request #36 from GaloisInc/text-fieldname
brianhuffman
authored

Commits on Jan 18, 2021

Type check in context of private symbols
Aaron Tomb
committed

Commits on Jan 19, 2021

Fix broken Read instance for type Ident.
Brian Huffman
committed
Merge pull request #122 from GaloisInc/read-ident
brianhuffman
authored
Move ModuleName, Ident, and NameInfo declarations into new module.
Brian Huffman
committed
Move ExtCns and related definitions to Verifier.SAW.Name.
Brian Huffman
committed
Move SAWNamingEnv type to Verifier.SAW.Name.
Brian Huffman
committed
Move more SAWNamingEnv-related functions into Verifier.SAW.Name.
Brian Huffman
committed
Redefine scFindBestName in terms of bestAlias.
Brian Huffman
committed
Merge pull request #123 from GaloisInc/name-module
brianhuffman
authored
Sort LANGUAGE pragmas and remove duplicates.
Brian Huffman
committed
Switch Lambda and Pi constructors to use Text instead of String.
Brian Huffman
committed
Switch StringLit to use Text instead of String.
Brian Huffman
committed
Merge pull request #119 from GaloisInc/text-lambda
brianhuffman
authored
Adapt to GaloisInc/saw-core#119 .
Brian Huffman
committed
Qualify Data.List import to fix GHC 8.10 compatibility check.
kquick
committed
Merge pull request #125 from GaloisInc/qualified_list
kquick
authored
Switch from GlobalDef to Constant for definitions in .sawcore files.
Brian Huffman
committed
Fix mismatched parser/printers for ModuleIdentifier in ExternalFormat.
Brian Huffman
committed
Fix bug in cryptol-saw-core: Repl is a constructor, not a global.
Brian Huffman
committed
Switch scGlobalEnv from MVar to IORef using atomicModifyIORef'.
Brian Huffman
committed
Merge pull request #37 from GaloisInc/text-lambda
brianhuffman
authored
Merge branch 'master' into wip-heapster-merge
Brian Huffman
committed
Make visibility of Cryptol symbols configurable
Aaron Tomb
committed
Fix cryptol-saw-core tests
Aaron Tomb
committed
Merge pull request #120 from GaloisInc/at-private-imports
Aaron Tomb
authored

Commits on Jan 20, 2021

Add GADTs language pragma to make ghc-8.10 happy.
Brian Huffman
committed
Merge pull request #118 from GaloisInc/globaldef
brianhuffman
authored

Commits on Jan 21, 2021

Commits on Jan 22, 2021

Add new pretty-printing functions that take a SAWNamingEnv.
Brian Huffman
committed
Add naming-aware pretty-printing function scShowTerm.
Brian Huffman
committed
Merge pull request #126 from GaloisInc/pp-term
brianhuffman
authored
Fix implementation of fromIntMod in SBV backend.
Brian Huffman
committed
Fix implementation of fromIntMod in what4 backend.
Brian Huffman
committed
Merge pull request #146 from GaloisInc/issue145
brianhuffman
authored
Add congruence rule for IntModNum and extend proveEq to handle Z type.
Brian Huffman
committed
Merge pull request #149 from GaloisInc/issue147
brianhuffman
authored

Commits on Jan 25, 2021

experimental CI workflow for saw-core-coq
Ptival
committed
saw-core-coq: workflows cannot be in subdirectories
Ptival
committed
Adapt Conversion library to use scGlobalDef when building terms.
Brian Huffman
committed
Merge pull request #152 from GaloisInc/issue151
brianhuffman
authored

Commits on Jan 28, 2021

Adapt to GaloisInc/cryptol#995 "Call stacks".
Brian Huffman
committed
Adapt to GaloisInc/cryptol#993 "Refactor evopts".
Brian Huffman
committed
Adapt to GaloisInc/cryptol#1015 "Newtypes".
Brian Huffman
committed
Merge pull request #153 from GaloisInc/update-cryptol
brianhuffman
authored

Commits on Jan 30, 2021

Merge pull request #116 from GaloisInc/saw-what4-refactor
robdockins
authored

Commits on Feb 1, 2021

Change the sort of saw-core type Eq from sort 1 to Prop.
Brian Huffman
committed
Merge pull request #154 from GaloisInc/eq-prop
brianhuffman
authored
Add dependent sum datatype Sigma to saw-core prelude.
Brian Huffman
committed
Merge pull request #155 from GaloisInc/sigma-type
brianhuffman
authored
Add an inductive List datatype to the saw-core prelude.
Brian Huffman
committed
Merge pull request #156 from GaloisInc/list-type
brianhuffman
authored
Add SAW core emacs mode.

Eddy Westbrook
authored and
Brian Huffman
committed
Merge pull request #157 from GaloisInc/saw-core-mode
brianhuffman
authored

Commits on Feb 12, 2021

Commits on Feb 15, 2021

Edit rme/README.md.
Brian Huffman
committed

Commits on Feb 16, 2021

Commits on Feb 19, 2021

fix coq import bug (SAWVector.. -> SAWCoreVector..)
Ajay Kumar Eeralla
committed

Commits on Feb 22, 2021

Commits on Feb 23, 2021

added tuple combinators to OpenTerm.hs

Eddy Westbrook
authored and
Brian Huffman
committed
added letOpenTerm

Eddy Westbrook
authored and
Brian Huffman
committed
added pair and tuple projection functions, as well as multi-arity lambda and pi abstraction formers, to OpenTerm

Eddy Westbrook
authored and
Brian Huffman
committed
added completeOpenTermType to get the type of an OpenTerm

Eddy Westbrook
authored and
Brian Huffman
committed
Expose implementation of OpenTerm and OpenTermM types.

Eddy Westbrook
authored and
Brian Huffman
committed
added sortOpenTerm

Eddy Westbrook
authored and
Brian Huffman
committed
Merge pull request #166 from GaloisInc/openterm
brianhuffman
authored
Convert more uses of String to Text.
Brian Huffman
committed
Merge pull request #160 from GaloisInc/text-untyped-ast
brianhuffman
authored

Commits on Mar 2, 2021

Add stubs for new cryptol float primitives to cryptol-saw-core.
Brian Huffman
committed
Adapt cryptol-saw-core to GaloisInc/cryptol#1075 "persist-solver".
Brian Huffman
committed
Merge pull request #175 from GaloisInc/update-cryptol
brianhuffman
authored

Commits on Mar 9, 2021

exposed ppTermInCtx as a Term pretty-printing operator

Eddy Westbrook
authored and
Brian Huffman
committed
Merge pull request #167 from GaloisInc/ppTermInCtx
brianhuffman
authored
fixed a bug in ctxReduceRecursor, where recursive arguments with functional type were not getting applied to their arguments in the recursive call

Eddy Westbrook
authored and
Brian Huffman
committed
Merge pull request #168 from GaloisInc/ctxReduceRecursor
brianhuffman
authored
bug fix: when computing the types of the eliminator functions for recursors, we need to normalize them

Eddy Westbrook
authored and
Brian Huffman
committed
Merge pull request #169 from GaloisInc/scRecursorElimTypes
brianhuffman
authored
bug fix: added a check that the types of constructors satisfy the proper universe restrictions

Eddy Westbrook
authored and
Brian Huffman
committed
fix bad multi-line string literals in universe errors

m-yac
authored and
Brian Huffman
committed
Merge pull request #172 from GaloisInc/univInconsistency
brianhuffman
authored

Commits on Mar 10, 2021

Add arrowOpenTerm to OpenTerm module.
Brian Huffman
committed
Add OpenTerm operations for making string literals and the string type.
Brian Huffman
committed
Merge pull request #177 from GaloisInc/OpenTerm
brianhuffman
authored
add scTypeCheckComplete, scCheckSubtype

m-yac
authored and
Brian Huffman
committed
Merge pull request #178 from GaloisInc/scTypeCheckComplete
brianhuffman
authored
Remove the dodgy eq saw-core primitive.
robdockins
committed
Compute first-order types in what I hope is a more
robdockins
committed

Commits on Mar 11, 2021

Commits on Mar 12, 2021

Commits on Mar 14, 2021

Commits on Mar 15, 2021

Commits on Mar 20, 2021

Commits on Mar 30, 2021

Commits on Apr 2, 2021

cryptol-saw-core: Adapt to PLiteralLessThan in cryptol
RyanGlScott
committed
Whitespace-related alignment only
RyanGlScott
committed
Extend proveProp with instance rules for LiteralLessThan.

Brian Huffman
authored and
RyanGlScott
committed
Extend cryptol-saw-core tests to cover LiteralLessThan instance rules.

Brian Huffman
authored and
RyanGlScott
committed
Update normalizeProp to also normalize LiteralLessThan constraints.

Brian Huffman
authored and
RyanGlScott
committed
Fix slightly too-specific instance rule for LiteralLessThan [n].

Brian Huffman
authored and
RyanGlScott
committed
Fix instance rules in comments.

Brian Huffman
authored and
RyanGlScott
committed
Add stub Float instance for Literal/LiteralLessThan.

Brian Huffman
authored and
RyanGlScott
committed
Merge pull request #188 from GaloisInc/PLiteralLessThan
RyanGlScott
authored

Commits on Apr 5, 2021

wip-heapster changes to Prelude to fix saw-core-coq's make (#179 )

m-yac
and
Eddy Westbrook
authored

Commits on Apr 6, 2021

Update saw-core-coq-check-coq-files.yml (#195 )
Ptival
authored

Commits on Apr 14, 2021

Do the right thing when encountering 0 width bitvectors in the What4 backend.
robdockins
committed

Commits on Apr 19, 2021

Commits on Apr 21, 2021

Merge pull request #203 from GaloisInc/sp/crux-mir-comp
spernsteiner
authored

Commits on Apr 26, 2021

Remove conflicting files to prepare for merge into saw-script repo.
Brian Huffman
committed
This merge pulls the previously-separate saw-core repository into the the saw-script repository,
Brian Huffman
committed
Point cabal.project at saw-core packages in this repo.
Brian Huffman
committed
Delete saw-core submodule.
Brian Huffman
committed
Remove reference to deps/saw-core in README.md.
Brian Huffman
committed
Update "issues" URL for panic messages to point at saw-script repo.
Brian Huffman
committed
Update paths to saw-core-coq repo listed in saw-core-coq/README.md.
Brian Huffman
committed
saw-core-coq: update generated files

Ptival
authored and
Brian Huffman
committed
saw-core-coq: fix handwritten files

Ptival
authored and
Brian Huffman
committed