]> matita.cs.unibo.it Git - helm.git/commit
huge commit regarding coercions to funclass and eat_prods. before there was a
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 8 Sep 2007 23:50:41 +0000 (23:50 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 8 Sep 2007 23:50:41 +0000 (23:50 +0000)
commit5f18d404d23d75d47b018631cc05221ccd2d2b1b
tree9a091380634b77c5ac493dc501fd7d756947ef48
parent143c10b37e360a1d115904c46a954e86904ee203
huge commit regarding coercions to funclass and eat_prods.  before there was a
so broken behaviour that is impossible to describe the changes.

now:
  eat_prods he hety args

  starts checking if hety is metaclosed, if it is does nothing, if not
  unifies it with ?->?-> ... ->? s.t. there is a Pi for every args.
  if this unification fails, does nothing (all coercions are in the
  second phase.

  continues eating prods in hety and args in parallel, if there is an arg
  and no more prods, tries to fix the arity of (he already_processed_args).
  fix_arity gives a range of possible coercions to funclass s.t.
  (c (he ..)) : FunType. The eat prods and args continues, eting the remaining
  args toghether with FunType. If it fails, it continues with another c to
  another FunType. This recursively (yes, it backtracks. no strong opinion
  here, but there is no sane heuristinc to chose one FunType).

  the code is reduced to 1/3, but Localization of errors probably need fixing.
helm/software/components/cic_unification/cicRefine.ml