Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-01 13:59:06 -0800 (Tue, 01 Feb 2005)
Revision: 6559
Log message:

      Removing extensions/fix.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-02 03:06:01 -0800 (Wed, 02 Feb 2005)
Revision: 6565
Log message:

      Whew, mmc now compiles with full type information.
      
      Here are some tradeoffs.
      
         1. Type information is *very* useful.  I caught many errors
            in mmc with it.
         2. It also requires you be more verbose.  For example, you
            might need separate terms:
      
               Foo{'e : Exp}
               FooList{'el : List{Exp}}
      
            you probably got away with just Foo{'a} before.
         3. It is also unsound.  This is mainly because there is no relation
            between rules, so one rule can't tell any type constraints of
            another rule.
      

Changes by: ( at unknown.email)
Date: 2005-02-03 12:25:54 -0800 (Thu, 03 Feb 2005)
Revision: 6584
Log message:

      This commit was manufactured by cvs2svn to create branch
      'opname_classes4'.

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-03 12:26:59 -0800 (Thu, 03 Feb 2005)
Revision: 6585
Log message:

      Ouch, we had:
      
      dform display_hyp_sep_df : display_hyp_sep{'tag} =
         display_hyp_sep{'tag}
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 18:14:03 -0800 (Thu, 03 Feb 2005)
Revision: 6587
Log message:

      Yet another instance of the opname_classes branch, merged once again with the
      trunk changes and re-branched.
      
      Known issues:
       - The .mli opname declarations are added to the .cmoz in the reverse order.
         This, among other things causes Failure ("unknown typeclass:
         Mmc_base_judgment!Prop") exception on cd'ing into the /mmc_base_judgment
         module.
       - The .mli opname declarations are added to the .cmoz even when .cmoz has its
         own copy. That results in the "ls" output (and other things, such as .cmoz
         and .prla files) being unnecessarily cluttered.
       - If the same shape is declared several times (possibly with incompatible
         types), does anybody notice?
      
      Potential TODOs and RFEs:
       - Proper type checking for display forms.
       - Could we may be come up with a way to propagate certain declarations from
         .ml into .cmiz (instead of the other way around)? Some declarations needs
         to stay in the .ml in order to get properly documented.
       - "declare sequent" shortcuts:
          - when the type is { Term : Term >- Term } : Term, allow omitting it
          - when the type is { Term : Term >- Term } : Foo, allow typing just ": Foo"
       - Perv!nil/Perv!cons should have the Dform type.
          - When the sequent conclusion is omitted, a we should use something other
            than Perv!nil for the conclusion. This new "default conclusion" term
            should be a member of a singleton type (in the Term typeclass), and MMC
            should be using that in the type of Mmc_core_ast!ty_args
          - Base_reflection should use its own cons and nil for bterm lists.
       - The new stuff (both the new syntax and the typechecking algorithm) need to
         be documented.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-05 17:14:46 -0800 (Sat, 05 Feb 2005)
Revision: 6603
Log message:

      Added display-form type checking.  This was a little painful because
      some theories were using xlist as a normal list.  In the end, I changed
      the declarations to the following.
      
         declare xcons{'a : Dform; 'b : Dform} : Dform
         declare xnil : Dform
      
      Base_reflection has its own list, using rcons and rnil.
      You need to use the functions mk_rlist_term, is_rlist_term, etc.,
      instead of mk_xlist_term, is_xlist_term.
      
      The .prla updates are just for the opname renaming.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-05 19:55:00 -0800 (Sat, 05 Feb 2005)
Revision: 6606
Log message:

      Disallow type constraints rules and rewrites.  For type inference,
      type rewrites become equalities.
      
         declare rewrite TyElem{TyExp} <--> Exp
      
      This means, in addition to the rewrite, that TyElem{TyExp} = Exp.
      So, if we are unifying t1 and t2, it is legal to unify t1 with TyElem{TyExp},
      and Exp with t2.
      
      >    Known issues:
      >     - The .mli opname declarations are added to the .cmoz in the reverse order.
      >       This, among other things causes Failure ("unknown typeclass:
      >       Mmc_base_judgment!Prop") exception on cd'ing into the /mmc_base_judgment
      >       module.
      >     - The .mli opname declarations are added to the .cmoz even when .cmoz has its
      >       own copy. That results in the "ls" output (and other things, such as .cmoz
      >       and .prla files) being unnecessarily cluttered.
      
      These are fixed.  Only the declarations that don't exist in the .ml are copied.
      
      >     - If the same shape is declared several times (possibly with incompatible
      >       types), does anybody notice?
      
      This is now checked in Filter_cache_fun.
      
      >    Potential TODOs and RFEs:
      >     - Proper type checking for display forms.
      
      Implemented.
      
      >     - Could we may be come up with a way to propagate certain declarations from
      >       .ml into .cmiz (instead of the other way around)? Some declarations needs
      >       to stay in the .ml in order to get properly documented.
      
      What about copying the documentation from the .mli (preserving the order)?
      
      >     - "declare sequent" shortcuts:
      >        - when the type is { Term : Term >- Term } : Term, allow omitting it
      >        - when the type is { Term : Term >- Term } : Foo, allow typing just ": Foo"
      
      Implemented.
      
      >     - Perv!nil/Perv!cons should have the Dform type.
      >        - When the sequent conclusion is omitted, a we should use something other
      >          than Perv!nil for the conclusion. This new "default conclusion" term
      >          should be a member of a singleton type (in the Term typeclass), and MMC
      >          should be using that in the type of Mmc_core_ast!ty_args
      >        - Base_reflection should use its own cons and nil for bterm lists.
      
      Implemented.
      
      >     - The new stuff (both the new syntax and the typechecking algorithm) need to
      >       be documented.
      
      I need to do this.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-06 15:21:43 -0800 (Sun, 06 Feb 2005)
Revision: 6607
Log message:

      Typechecking is now stricter.
         -- For rules and rewrites, the goal types are existentially quantified.
         -- Rewrites are type-invariant.  For example, the following will fail.
      
            declare typeclass A
            declare typeclass B -> A
            declare foo : A
            declare bar : B
      
            prim_rw bad : foo <--> bar
      
            This is rejected because the (bar --> foo) rewrite is bogus.
      
      At this point, the type system is basically sound, apart from
      rule and rewrite arguments, and assuming the implementation is
      correct.  Let's merge.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-06 19:33:24 -0800 (Sun, 06 Feb 2005)
Revision: 6611
Log message:

      1. Some work on mmc.
      
      2. Fixed the problem with parsed term in comments.
      > 1) The problem with <:doc< ... << ... >> ... >>
      >
      > still exists.
      
         The terms in comments are now parsed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-07 04:25:55 -0800 (Mon, 07 Feb 2005)
Revision: 6624
Log message:

      ***************************************************************************
      ****             !!!!!         WARNING            !!!!!                ****
      ***************************************************************************
      !!!!!           This commit breaks binary compatibility               !!!!!
      !!!!!         Export all your uncommitted proofs before updating      !!!!!
      !!!!!                                                                 !!!!!
      !!!!!  If you export to a .prla that did not exist before, you will   !!!!!
      !!!!!  to edit it manually after you update - find the line that      !!!!!
      !!!!!  starts with "NPerv!cons" replace the last (third) occurrence   !!!!!
      !!!!!  of "cons" with "xcons", then replace last (third) occurrence   !!!!!
      !!!!!  nil" with "xnil" on the "Perv!nil" line.                       !!!!!
      !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
      
      Merging the opname_classes branch!
      
      This commit inroduces types to MetaPRL syntax with an informal (but pretty
      precise) typechecking. Hopefully Jason will write some documentation
      describing how to use this.
      
      This fixes bug 370 and bug 371.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-08 00:04:25 -0800 (Tue, 08 Feb 2005)
Revision: 6629
Log message:

      I overlooked free type variables in the environment during existential
      quantification in rules and rewrites.  This fixes it.  However, note
      that rewrites like the following don't typecheck.
      
         prim_rw add_sub_one :
            ('a in int) -->
            'a <--> (('a +@ 1) -@ 1)
      
      The rewrite is quite sensible in Itt, but problematic because it
      applies to any term in the system (including display forms
      for example).  The quick solution is to add the constraint.
      
         prim_rw add_sub_one ('a :> Term) :
            ('a in int) -->
            'a <--> (('a +@ 1) -@ 1)
      
      This is a bit suboptimal, but rewrites like this are very rare,
      and the extra alpha-equality adds only O(1) overhead.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-13 11:48:21 -0800 (Sun, 13 Feb 2005)
Revision: 6668
Log message:

      Corrected the subtyping rule for hyp contexts.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-21 10:27:25 -0800 (Mon, 21 Feb 2005)
Revision: 6732
Log message:

      Debugging type inference.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-21 11:51:43 -0800 (Mon, 21 Feb 2005)
Revision: 6734
Log message:

      Check token types too.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-21 13:48:53 -0800 (Mon, 21 Feb 2005)
Revision: 6735
Log message:

      More minor updates.  We're now stuck in an infinite loop in CPS.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-21 16:16:40 -0800 (Mon, 21 Feb 2005)
Revision: 6736
Log message:

      1. tycps_tyfun_std had some serious problems.
      2. Removed mmc_core_def, since we get the ability from iforms.
      3. Print stages during debug compiling, so we have some idea where
         things go wrong.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-21 17:46:01 -0800 (Mon, 21 Feb 2005)
Revision: 6739
Log message:

      Working on the backend.  The terms changed a lot, so most of the
      files are not compiled.  I'll add them back as I work through the
      backend.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-21 18:03:12 -0800 (Mon, 21 Feb 2005)
Revision: 6740
Log message:

      Added a <-- form for productions, which really makes more sense than
      the --> form we are using.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-21 19:31:29 -0800 (Mon, 21 Feb 2005)
Revision: 6741
Log message:

      Different quotations should not be required to use the
      same lexer.  This commit adds the ability to define multiple
      lexers (the grammars can still be shared).
      
      Now, instead of
         lex_token "[0-9]+" --> number[lexeme:n]
      you have to specify the lexer
         declare mmc : Lexer
         ...
         lex_token mmc : "[0-9]+" --> number[lexeme:n]
      
      CAUTION: this commit breaks binary compatibility.  I'm sorry about
      this hassle--the change doesn't really affect those of you who
      don't use the input grammars.  In any case, you should export any
      unsaved work before updating from cvs.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-21 20:50:16 -0800 (Mon, 21 Feb 2005)
Revision: 6745
Log message:

      The assembly grammar is partially defined.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-22 14:17:33 -0800 (Tue, 22 Feb 2005)
Revision: 6746
Log message:

      Added two new iform terms:
      
         1. xsovar[x:v]{'cvars; 'args} is iform translated to a so-var.
         2. A hyp of the form
      
               x: xhypcontext{'cvars; 'args}
      
            gets translated to a hyp context.
      
      In both cases, the 'cvars and 'args should be an xlist.
      
      The x86 assembly grammar is nearly complete.  Starting on the
      tast grammar.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-22 15:32:35 -0800 (Tue, 22 Feb 2005)
Revision: 6747
Log message:

      Added most of the grammar for the tast.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-22 15:43:14 -0800 (Tue, 22 Feb 2005)
Revision: 6748
Log message:

      Added tast grammars for integers and Booleans.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-22 18:31:27 -0800 (Tue, 22 Feb 2005)
Revision: 6749
Log message:

      Lm_parser was not computing the nullable productions properly,
      and it was using goto 0 after reduce on an empty production.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-22 19:05:37 -0800 (Tue, 22 Feb 2005)
Revision: 6750
Log message:

      Added contexts, so you can write such things as:
      
         <:tast< fun#std (x: ty, <H>) -> e >>
         <:tast< fun#std <H> -> e >>
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-22 20:25:41 -0800 (Tue, 22 Feb 2005)
Revision: 6751
Log message:

      Added support for nested quotations.  Here is an example.
      
      interactive foo :
         sequent { <H> >- <:tast< let v : << TyInt >> = 1 in v >> in TyTop }