Monadified Cryptol-to-SAWCore translation#1552

Merged

eddywestbrook merged 104 commits intomasterfrom feature/monadification

Feb 7, 2022

+3,644-542

Commits on Jul 7, 2021

added more OpenTerm combinators, including: a "failure term"; getting the type of a term; and applying a pi type to an argument
Eddy Westbrook
committed
added Monadify.hs
Eddy Westbrook
committed

Commits on Jul 8, 2021

saving progress on monadification...
Eddy Westbrook
committed

Commits on Jul 13, 2021

figured out how to monadify applications, but still working on lambdas...
Eddy Westbrook
committed
finished a first version of monadification, ready for testing...
Eddy Westbrook
committed

Commits on Jul 14, 2021

refactored monadifyInBinding and monadifyTermAndRun; wrote the top-level entrypoint monadifyTerm
Eddy Westbrook
committed
added the monadify_term function to the interpreter
Eddy Westbrook
committed

Commits on Jul 15, 2021

added bindTCMOpenTerm
Eddy Westbrook
committed
changed monadification to work on plain old Terms rather than TypedSubsTerms
Eddy Westbrook
committed
bug fix: when getting the type of a term in OpenTerm, need to use the current typing context
Eddy Westbrook
committed
added support for datatypes and constructors in monadification
Eddy Westbrook
committed
whoops, monadify_term should not call mkTypedTerm, but just use scTypeOf directly
Eddy Westbrook
committed

Commits on Jul 16, 2021

added openOpenTerm
Eddy Westbrook
committed
trying a different approach to monadification, where we make explicit MonType and MonKind data structures
Eddy Westbrook
committed
added OpenTerm combinators for record terms
Eddy Westbrook
committed

Commits on Jul 17, 2021

started writing monadifyTerm in the new monadification approach
Eddy Westbrook
committed

Commits on Jul 18, 2021

added extCnsOpenTerm; also added a warning to bindTCMOpenTerm
Eddy Westbrook
committed
finished the application cases of the new approach to monadification; updated the top-level entrypoint to be called monadify instead of monadifyTerm
Eddy Westbrook
committed
tweaked monadifyApply to take in an ArgMonTerm instead of a MonTerm
Eddy Westbrook
committed

Commits on Jul 19, 2021

switched to allowing pure terms at any type
Eddy Westbrook
committed
added monadifyType case for Nums
Eddy Westbrook
committed
added monadification macros in order to handle unsafeAssert; also added numAssertEqM as the monadified version of unsafeAssert applied to the Num type
Eddy Westbrook
committed
changed monadification to treat primitives and definitions the same way
Eddy Westbrook
committed

Commits on Jul 20, 2021

changed the top-level monadify call to take in the un-normalized type
Eddy Westbrook
committed
added slightly different versions of tupleOpenTerm and tupleTypeOpenTerm match scTupleValue and scTupleType
Eddy Westbrook
committed
added support for tuple and record projections, in two ways: changed MTyTuple to just MTyPair; and changed monadifyTerm to take an optional type, which allows monadification to do inference when th…
Eddy Westbrook
committed
added a case to monadify Eq types
Eddy Westbrook
committed
whoops, was treating globally defined constants in the wrong way!
Eddy Westbrook
committed

Commits on Jul 22, 2021

fixed the macro for unsafeAssert to return a computational instead of argument term; reorganized the "from" and "to" operations between monadification terms and OpenTerms to avoid these sorts of mi…
Eddy Westbrook
committed
whoops, it is Cryptol.Num, not Prelude.Num
Eddy Westbrook
committed
added bindPPOpenTerm, for error reporting
Eddy Westbrook
committed
changed asTypedGlobalDef to not accidentally unfold constants; added more info to the error message in toPureTerm
Eddy Westbrook
committed

Commits on Jul 26, 2021

added "monadified sequence" types mvec and mseq; added new versions of some of the Cryptol typeclasses to support these
Eddy Westbrook
committed
completely removed the concept of pure terms, because they were not really correct anyway...
Eddy Westbrook
committed
added monadification test case
Eddy Westbrook
committed

Commits on Aug 11, 2021

updated some comments
Eddy Westbrook
committed

Commits on Aug 13, 2021

added a process to monadify an entire cryptol environment
Eddy Westbrook
committed
whoops, want to handle globals that are pure but do not require special-purpose macros
Eddy Westbrook
committed
updating example a bit...
Eddy Westbrook
committed
whoops, fixed an infinite loop when monadifying a non-lambda of functional type
Eddy Westbrook
committed
attempting to monadify all the user-defined cryptol names, but that looks to be all of the cryptol prelude as well...
Eddy Westbrook
committed
switched from an approach based on monadifying a CryptolEnv to a lazy / as-needed approach that just monadifies any constants that occur in a term
Eddy Westbrook
committed
updated example for latest changes to monadification
Eddy Westbrook
committed
slightly more sophistication in monadifying seq types
Eddy Westbrook
committed
whoops, when monadifying constants, forgot to skip the constants we have already handled!
Eddy Westbrook
committed

Commits on Aug 14, 2021

added a macro for if-then-else
Eddy Westbrook
committed

Commits on Aug 18, 2021

moved the monadic versions of Cryptol primitives to a new module, CryptolM, and finished a lot more of them
Eddy Westbrook
committed
whoops, wrong module name in the CryptolM module
Eddy Westbrook
committed

Commits on Aug 19, 2021

condensed the multiple different sorts of mappings for monadifying primitives into a single list
Eddy Westbrook
committed
added a few more examples to the monadification test
Eddy Westbrook
committed
fixed spacing
Eddy Westbrook
committed
got monadification working for non-mutual fixedpoints
Eddy Westbrook
committed

Commits on Aug 25, 2021

added the set_monadification command
Eddy Westbrook
committed
added existsM and forallM monadic combinators to the CompM monad
Eddy Westbrook
committed

Commits on Aug 26, 2021

Commits on Aug 27, 2021

small updates to MR solver to add comments and make globals use arbitrary NameInfos so they can support monadified cryptol terms
Eddy Westbrook
committed

Commits on Oct 6, 2021

added letRecM back as a primitive, and started trying to define the other fixed-point operations in terms of it (though that is still in progres...)
Eddy Westbrook
committed
started rewriting MRSolver
Eddy Westbrook
committed

Commits on Oct 7, 2021

added bitSetElems
Eddy Westbrook
committed
wrote a simple verison of mrProveEq, using mrProveEqSimple
Eddy Westbrook
committed

Commits on Oct 8, 2021

whoops, fixed small bugs in bitSetElems
Eddy Westbrook
committed
added an instance of MonadTerm for any monad transformer
Eddy Westbrook
committed
got an initial versio of mrProveEq to compile
Eddy Westbrook
committed
rewrote the normalizer for MRSolver
Eddy Westbrook
committed

Commits on Oct 11, 2021

added the ExtCns case to asTypedGlobalDef
Eddy Westbrook
committed
wrote up the cases of the new mrRefines function, though it does not yet compile...
Eddy Westbrook
committed

Commits on Oct 12, 2021

almost got mrRefines to compile
Eddy Westbrook
committed
added a VarIndex to GlobalDef, to use as a sorting key
Eddy Westbrook
committed
finished a complete version of the MRSolver module that at least compiles without warnings
Eddy Westbrook
committed
added the top-level call to mr_solver
Eddy Westbrook
committed

Commits on Oct 13, 2021

renamed the monadify examples directory to be called mr_solver
Eddy Westbrook
committed
added a catch block to scCryptolType, so that panics in the simulator when trying to evaluate the type of an expression just turn into a lack of a Cryptol type rather than a top-level panic
Eddy Westbrook
committed
whoops, fixed the type of the mr_solver interpreter command
Eddy Westbrook
committed
MR Solver bug fixes: changed mrProvableRaw to use termToProp instead of boolToProp; changed askMRSolver to check convertibility of the types not of the terms themselves; and added an error case for…
Eddy Westbrook
committed
changed the mr_solver command to return whether the proof succeeded
Eddy Westbrook
committed
fixed mrProveEq to correctly compute the types of its inputs
Eddy Westbrook
committed
removed calls to scEq, which only works on closed terms
Eddy Westbrook
committed
added debug printing to mr_solver, and added the mr_solver_debug command to set the debug level
Eddy Westbrook
committed
added mr_solver unit tests
Eddy Westbrook
committed

Commits on Oct 14, 2021

added some noErrors proofs to our MR solver unit tests
Eddy Westbrook
committed
changed the handling of recursive functions so that the bodies of recursive functions need to line up
Eddy Westbrook
committed
changed GlobalDefs to contain an unfolded body for constants
Eddy Westbrook
committed
added support for unfolding non-recursive functions
Eddy Westbrook
committed
added unit tests for unfolding contstants
Eddy Westbrook
committed

Commits on Oct 15, 2021

defined multiFixM in terms of letRecM
Eddy Westbrook
committed
added a convertibility check to the default case of proveEq
Eddy Westbrook
committed
added unfolding of non-recursive functions to mrRefines, and removed it from normalization
Eddy Westbrook
committed

Commits on Oct 16, 2021

added compFunComp to simplify the composition of returns; added uniquifyName to give each uvar a distinct name; removed the case for FunBinds where we have the same function on both sides, since we…
Eddy Westbrook
committed

Commits on Nov 4, 2021

added a note to my future self
Eddy Westbrook
committed
added some more MR solver tests
Eddy Westbrook
committed

Commits on Jan 21, 2022

Merge remote-tracking branch 'origin/master' into feature/monadification
Eddy Westbrook
committed
whoops, the previous merge added some operations to Prelude.sawcore twice
Eddy Westbrook
committed
fixed a type error in CryptolM.sawcore introduced by the merge
Eddy Westbrook
committed
updated Monadify.hs to work with merge
Eddy Westbrook
committed

Commits on Jan 22, 2022

added the monadifyName function, to map the name of a constant to the name of its monadification
Eddy Westbrook
committed

Commits on Jan 23, 2022

changed efq to specifically mention FalseProp, and added an efq1 to work on types in sort 1
Eddy Westbrook
committed
updated the cryptol monadification translation to have finite computational sequence (i.e., vectors) be strict, in order to make it easier to prove things about them
Eddy Westbrook
committed
removed some debug printing
Eddy Westbrook
committed

Commits on Feb 7, 2022

prefixed unused symbols with underscores
Eddy Westbrook
committed