Tasks 2/6

[michaelto20]

1. Change :dv syntax to ":dv : "
2. Add rule we discussed in meeting to evaluator
3. Look into why this example typechecks:

   add (one s z) (one s z) s z
   ((s z) s) (((((\(s:? -> ?).\(z:?).s z) s)

   • this may be fixed with adding an application case in the type-checking algorithm

[michaelto20]

Improvements to core type checker:

• Go through syntax and add cases in typecheck_aux that aren't there (ex: fst, snd, case), not for TypeApp
  • Look at pseudocode in picture for how to do it for fst, this is also where the reqProd is needed
• Is there a reqProd function? If not, write it like reqArrow
• If type is above the line on a rule, you'll need to infer it
• Type annotations are needed for LCase, add Typebetween CTermand CTermin constructor in CoreSyntax file
• In function evalCTerm' copy how CBoxevaluates the term, but case split on Varinstead