This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Recursors#27

Merged

brianhuffman merged 162 commits intomasterfrom wip-recursors

Jun 9, 2018

+5,214-4,938

Commits on Sep 9, 2017

updated prelude to use recursors
Eddy Westbrook
committed
added fix back into the Prelude
Eddy Westbrook
committed

Commits on Nov 1, 2017

added back some things that depended on the fix primitive
Eddy Westbrook
committed
Merge branch 'master' into wip-recursors
Eddy Westbrook
committed
added natCase back into the prelude
Eddy Westbrook
committed

Commits on Nov 3, 2017

added some data-types that will eventually replace the SAW primitive data types
Eddy Westbrook
committed

Commits on Nov 27, 2017

Changed all the primitives in the Prelude that we want to map in simulations back into primitives, but added additional "__def" forms and "__eq" axioms asserting the equality of each primitive to i…
Eddy Westbrook
committed

Commits on Dec 19, 2017

changed implies to be defined instead of a primitive
Eddy Westbrook
committed
updated the comments for implies
Eddy Westbrook
committed
Merge branch 'master' into wip-recursors
Eddy Westbrook
committed

Commits on Dec 20, 2017

updated error to work at sort 1; changed the merged true_implies proof to not use patterns
Eddy Westbrook
committed
re-added unsafeCoerce_same to the prelude, as it is now getting used by the Cryptol translation
Eddy Westbrook
committed

Commits on Dec 28, 2017

Removed the concept of primitive data types, replacing them instead with primitives that happen to be types; changed all of the SAW internals that deal with types that used to be primitive data typ…
Eddy Westbrook
committed

Commits on Dec 29, 2017

updated symbolic simulator to treat Nat literals as constructors
Eddy Westbrook
committed

Commits on Mar 11, 2018

Saving progress in large rewrite to add recursors
Eddy Westbrook
committed

Commits on Mar 16, 2018

saving progress...
Eddy Westbrook
committed

Commits on Mar 23, 2018

saving intermediate progress...
Eddy Westbrook
committed
moved all the strongly-typed term stuff, as well as most of the datatype and recursor stuff, to a new module called CtxTerm
Eddy Westbrook
committed

Commits on Apr 12, 2018

wrote a first draft of the function to compute the type of eliminators, though it does not yet typecheck...
Eddy Westbrook
committed

Commits on Apr 13, 2018

almost finished computing the types of eliminators, yay!
Eddy Westbrook
committed
got the generator for eliminator types working, yay!
Eddy Westbrook
committed
finished implementing reduction, though there are still a few FIXMEs I forgot...
Eddy Westbrook
committed

Commits on Apr 18, 2018

finally finished recursors, yay!
Eddy Westbrook
committed
updated ctxReduceRecursor to work on Terms instead of CtxTerms
Eddy Westbrook
committed
added mkCtorElimTypeFun
Eddy Westbrook
committed

Commits on Apr 20, 2018

updated SharedTerm.hs to use the newly-finished CtxTerm functions for recursors
Eddy Westbrook
committed

Commits on Apr 26, 2018

added a Read instance for Ident
Eddy Westbrook
committed
changed ppNat back to taking a PPOpts structure
Eddy Westbrook
committed
added ctorNumArgs
Eddy Westbrook
committed
added back scRecursorElimTypes and scRecursorRetTypeType; fixed compiler warnings
Eddy Westbrook
committed
reimplemented the type-checker in SCTypeCheck to operate on pairs of a term and its type, to make it easier to re-use in the type-checker for untyped (parsed) SAW core terms
Eddy Westbrook
committed
updated ExternalFormat.hs and FiniteValue.hs to new Term constructors
Eddy Westbrook
committed
updated Conversion.hs to match new Term constructs
Eddy Westbrook
committed

Commits on Apr 27, 2018

whoops, ok, this time we actually got FiniteValue.hs to compile with the new term constructs
Eddy Westbrook
committed
added scFind* to the module export list of SharedTerm.hs
Eddy Westbrook
committed
more udpates to try to get everything to compile with the new Term constructs
Eddy Westbrook
committed
added ModuleMap type, and updated the allModuleXXX methods to use ModuleMaps instead of just a top-level Module
Eddy Westbrook
committed
updated simulator to new Term constructs
Eddy Westbrook
committed
updated simulator to new Term constructs
Eddy Westbrook
committed
updated supporting code to use new ModuleMap type
Eddy Westbrook
committed

Commits on Apr 28, 2018

Ok, this time we actually got SCTypeCheck.hs to compile
Eddy Westbrook
committed
removed some commented code
Eddy Westbrook
committed

Commits on May 1, 2018

updated modules to work more clearly as namespaces
Eddy Westbrook
committed
updated the TypeInfer class to also contain the method typeInferComplete for completing objects to a TypedTerm; added string names to the contexts in type inference; added an optional current modul…
Eddy Westbrook
committed
updated SharedContext.hs to adhere to the new findXXX methods in Modules, that take strings instead of Idents
Eddy Westbrook
committed
whoops, forgot to export TermCtx
Eddy Westbrook
committed

Commits on May 4, 2018

updated some comments
Eddy Westbrook
committed

Commits on May 5, 2018

added ctxBindingsOfTerms
Eddy Westbrook
committed
added scUnloadModule and scModifyModule; removed scEnsureModule
Eddy Westbrook
committed
added name resolution and supporting types to the export list of Module.hs
Eddy Westbrook
committed
added new type errors, and exported more of the helper functions, both to support type-checking of untyped terms
Eddy Westbrook
committed
simplified imports in the untyped language; combined RecursorProj into Recursor, and changed the parser to support this; removed DeclQualifier in favor of the existing (and identical) DefQualifier
Eddy Westbrook
committed
rewrote the typechecker for untyped terms to mostly just reuse the existing type-checkiner in SCTypeCheck.hs
Eddy Westbrook
committed

Commits on May 8, 2018

defined mkCtorArgStruct and all of the helper functions it requires
Eddy Westbrook
committed
moved mkCtorArgStruct to the end of the export list of CtxTerm.hs, to match the code
Eddy Westbrook
committed
added the two-part mechanism for defining datatypes, by first "beginning" and then "completing" them
Eddy Westbrook
committed
tweaked an error message
Eddy Westbrook
committed
added scBuildCtor to build a Ctor structure from its CtorArgStruct
Eddy Westbrook
committed
whoops, previous commit did not actually get scBuildCtor to compile...
Eddy Westbrook
committed
added ExistsTp to the export list; changed mkCtorArgStruct to take Ident instead of DataIdent
Eddy Westbrook
committed

Commits on May 9, 2018

finished writing the typechecker for datatype declarations
Eddy Westbrook
committed
added Read instances to untyped terms and a number of their helper types
Eddy Westbrook
committed

Commits on May 10, 2018

updated ParserUtils.hs to load in just untyped modules, not typed modules, as the latter would require a SharedContext at compile time...
Eddy Westbrook
committed
updated Prelude.hs to use new, simpler defineModuleFromFileWithFns function
Eddy Westbrook
committed
added underscore by itself as a special token, that works as an UnusedTermVar
Eddy Westbrook
committed
got the prelude to parse, yay!
Eddy Westbrook
committed
changed defineModuleFromFileWithFns to also emit a function for loading the given module into the current SharedContext
Eddy Westbrook
committed
fixed the Read method for Ident to break on the first non-identifer character
Eddy Westbrook
committed
fixed all the Read methods
Eddy Westbrook
committed
changed completeContext to use contexts instead of nested Pi types
Eddy Westbrook
committed
changed typeInferComplete for terms to add the current position while type-checking; updated completeContext to actually use a real term variable as often as possible
Eddy Westbrook
committed
added the ErrorPos constructor to annotate type errors with positions
Eddy Westbrook
committed
whoops, updated completeDataType to insert the names of the constructors
Eddy Westbrook
committed
whoops, term variables can match if they have different positions...
Eddy Westbrook
committed
whoops, forgot to use a recursor in UnitType__rec
Eddy Westbrook
committed
whoops, updated lexer to drop the "#rec" suffix of a recursor
Eddy Westbrook
committed
fixed bug in type-checker, that was matching applications before recursors
Eddy Westbrook
committed
recursors can now be applied to more arguments than necessary, if they have a functional return type
Eddy Westbrook
committed
fixed up some bugs in the Prelude
Eddy Westbrook
committed
added index out-of-bounds check to substitution function
Eddy Westbrook
committed
added an index out-of-bounds check to tupleConversion
Eddy Westbrook
committed
fixed pretty-printer to be able to handle unbound variables
Eddy Westbrook
committed
added scPrettyTermInCtx
Eddy Westbrook
committed
added context information to TCErrors; combined ArgTypeMismatch and ConstraintFailure errors into one SubtypeFailure error
Eddy Westbrook
committed
removed old typechecker modules
Eddy Westbrook
committed
fixed up the universe inclusion checking for inductive types
Eddy Westbrook
committed
changed checkSubtype to always throw a SubtypeFailure on error, which also contains the term that failed the subtype check; removed some errors that are now unused; updated the type-checking for re…
Eddy Westbrook
committed
added parentheses around the arguments of pi types
Eddy Westbrook
committed

Commits on May 11, 2018

fixed a bug in pretty-printing for pi-abstractions
Eddy Westbrook
committed
whoops, checkSubtype was checking that the value was a subtype of its required type, not the type...
Eddy Westbrook
committed
fixed a bug so that pi-abstractions with variable name "_" do not generate a fresh name for "_"
Eddy Westbrook
committed
fixed up comments for incVars
Eddy Westbrook
committed
updated debugging info for type-checking to also return the type that was inferred
Eddy Westbrook
committed
fixed bug in checkSubtype, where the error was being created in the wrong context
Eddy Westbrook
committed
changed BitSet to an opaque type, so that we do not have gross bit-munging code all over the place; changed the pretty-printer to print underscore variables if they are used
Eddy Westbrook
committed
whoops, scPrettyTermInCtx was binding the variables in the wrong order!
Eddy Westbrook
committed
whoops, fixed bug: we were accidentally processing all decls after a datatype decl in the context of the params of that datatype
Eddy Westbrook
committed
moved ppModule to Verifier.SAW.Module, to keep Pretty from depending on the definition of Modules
Eddy Westbrook
committed
whoops, I implemented ctxLift incorrectly for terms!
Eddy Westbrook
committed
whoops, incorrect precedence for pretty-printing the argument types of pis and lambdas
Eddy Westbrook
committed
whoops, why were we checking that the type of a global was a sort?
Eddy Westbrook
committed
fixed pretty-printing for memoization tables to print the rhs for a memoization variable *before* that variable is bound; also fixed pretty-printing to not memoize sorts
Eddy Westbrook
committed
made it easy to turn on and off tracing of type-checking by introducing a debugging level; also, fixed a bug in type-checking record types
Eddy Westbrook
committed
updated the Prelude so that it uses parameters in its datatypes
Eddy Westbrook
committed
refactored typeInferCompleteInCtx into a new typeclass, TypeInferCtx; renamed inExtendedCtx to withVar, also adding withCtx for multiple variables; removed calls to scTypeOf in the type-checker, as…
Eddy Westbrook
committed
fixed a subtle bug in substitution functions (i.e., instantiateVar and instantiateVarList)
Eddy Westbrook
committed
fixed up the comments for instantiateVarList
Eddy Westbrook
committed

Commits on May 12, 2018

fixed a bug in scRecursorRetTypeType by redefining it in terms of a new function, mkPRetTp, in CtxTer, that was refactored out of ctxCtorElimType
Eddy Westbrook
committed
fixed Eq type to use parameters
Eddy Westbrook
committed
fixed applyPiTyped to reduce its return value
Eddy Westbrook
committed
fixed evaluator (scWhnf) to properly handle recursors as a new sort of eliminator
Eddy Westbrook
committed
fixed up Either and Maybe types in the prelude to properly use parameters
Eddy Westbrook
committed

Commits on May 14, 2018

fixed up description of asCtorParams
Eddy Westbrook
committed
added asCtorOrNat
Eddy Westbrook
committed
added conversion rules to convert between nat literals and constructor applications which represent ground natural numbers
Eddy Westbrook
committed
exported asCtorOrNat
Eddy Westbrook
committed
added iota reduction to the rewriter
Eddy Westbrook
committed
finished getting the prelude to compile
Eddy Westbrook
committed

Commits on May 15, 2018

changed scTypeCheck and friends to work on any type that supports type inference
Eddy Westbrook
committed
re-exported tcInsertModule, as code generated by ParserUtils.hs uses it
Eddy Westbrook
committed
removed the now-unnecessary import of the Typechecker module from Prelude.hs
Eddy Westbrook
committed
added a Show method for TCError
Eddy Westbrook
committed

Commits on May 16, 2018

added signed bitvector comparison operations
Eddy Westbrook
committed
added maxSort operation, to return prop instead of failing on empty lists
Eddy Westbrook
committed
added maxSort operation, to return prop instead of failing on empty lists
Eddy Westbrook
committed
improved the ability of the type-checker to infer the types of variables in definitions by matching on the normalized type for the definition; this now requires variables to not be typed, which was…
Eddy Westbrook
committed
whoops, need to normalize the type of a recursor app before returning it
Eddy Westbrook
committed
resolved conflicts from merge with master
Eddy Westbrook
committed

Commits on May 17, 2018

fixing up Grammar.y, which somehow got out of sync in the merge of master
Eddy Westbrook
committed
moved def of replicateBool before use, to make the prelude type-check with the new rules
Eddy Westbrook
committed
changed NotRecordType errors to also print the term that does not have a record type
Eddy Westbrook
committed
whoops, throwing the wrong errors for record type-checking
Eddy Westbrook
committed
updated the Parser.hs tests to work with the new ModuleMap API
Eddy Westbrook
committed

Commits on May 24, 2018

Commits on May 25, 2018

Commits on May 29, 2018

added record-manipulating helper functions to the export list of SharedTerm.hs
Eddy Westbrook
committed
added asVTuple and asVTupleType to the export list of Concrete.hs
Eddy Westbrook
committed
switched value-manipulating code to use the new tuples (in terms of records) instead of the old ones
Eddy Westbrook
committed
whoops, fixed a bug in the new version of instantiateVarList
Eddy Westbrook
committed
whoops! scRecord was creating record types, not values...
Eddy Westbrook
committed
merged changes from master
Eddy Westbrook
committed
updated evalRecursorApp in the simulator to treat natural number values as constructor applications
Eddy Westbrook
committed

Commits on May 30, 2018

Commits on Jun 6, 2018

Fix typo.
Brian Huffman
committed
Make scDefRewriteRules produce separate rules for constructor patterns.
Brian Huffman
committed
scDefRewriteRules beta-reduces after doing recursor reductions.
Brian Huffman
committed
Fix pretty printing of string literals.
Brian Huffman
committed

Commits on Jun 7, 2018

Use more sensible names for rewrite rules.
Brian Huffman
committed
Merge branch 'master' into wip-recursors
Brian Huffman
committed
Handle recursive calls properly in scDefRewriteRules.
Brian Huffman
committed

Commits on Jun 8, 2018

added findCtorInMap and findDataTypeInMap, and changed the simulator to use these instead of looking through all ctors and datatypes in the entire module map
Eddy Westbrook
committed

Commits on Jun 9, 2018

Make tests compile and pass.
Brian Huffman
committed
scDefRewriteRules handles rhs with recursor applied to extra arguments.
Brian Huffman
committed