cic module removed (RIP)

tentative parser patch with symbolic tactics names

elim implemented as a notation for apply

Bug fixed: it always made an undo to the empty status (stupid bug
introduced in last commit)

camlp5 probably changed some internal data structures and now they cannot be compared with pervasives.comapre, thus we avoid it. Was breaking the natural deduction stuff

fixed many scripts that broke for various reasons

backport of patches to unification

fixed List.for_all2 called without knowing if the two lists have the same length

new case for higher order unification:

  (? ?) =?= (f x)

is not handled by delift, since flexible arguments in the local context
are skipped by delift, resulting in the instantiation of the head meta to
a constant function, even if the rhs is structurally the same.

removed wrong optimization in delift and export is_flexible

the Makefile was still calling transcript.

transcript removed (currently useless)

Polymorphic recursion no longer required!!!

- bug fixed (introduced by last commit from Andrea in MatitaEngine):
  recursive inclusion was de-activated
- some dead code removal

- grafiteSync no longer used
- grafiteTypes.status simplified

Propagation of changes to grafiteAst.

Cic.term and Cic.obj unused!

- cic almost not used

hgdome no longer used (RIP)

- most of cicUtil no longer used

- most of cic/ removed

Library committed again (because of a bug in SVN)

SVN bug: library lost, copying it again from previous version (???)

- hmysql removed (RIP)
- library simplified to handle only new files, moo and lexicon
- BROKEN FEATURES: recursive decompilation of library files is currently
  broken since, without the db, there is currently no way to compute the
  reverse dependencies

cicNotation* ==> notation*

- acic_content ==> content
- termAcicContent ==> interpretations

xmldiff removed

- cic_exportation, cic_acic, acic_content (only parts related to acic)
  metadata, cic_proof_checking and old binaries removed

cic_unification removed

acic_procedural and tactics removed

Removed tptp_grafite

removed tptp_grafite

nAuto --> nnAuto

Removed nauto debug checkbox

removed zipTree and andOrTree.

Removed nAuto.ml-mli

whelp and cic disambiguation removed

-hbugs: RIP

£- use ----------- in place of ## for sequents

-textual widget no longer editable

Font resizing and syntax highlighting re-activated for the browser and
sequent windows.

- parser: "whelp ...Â"removed
- interface: whelp bar removed
- interface: whelp and dependency graphs removed

- matitaWiki removed
- dump_moo removed
- matitaAutoGui removed

16.2

MathML widget no longer used. Requesciat in pacem

sync with stable:

patches for hints & unification:

1)
===========
It is an old and know issue. The check_stack calls fo_unif_w_hints only
on a prefix of applications, leaving some arguments on the stack. This
prevents hints to be found. Example

 Hint: And A B === fun_of_morph And_morphism A B

If the problem

  And A B =?= fun_of_morph ? A B

is found immediately (before entering the KAM) the it is solved, but if
it shows up inside the KAM, A and B are left on the stack and a
fo_unif_w_hints has to solve

  And =?= fun_of_morph ?

While one could declare hints multiple times, varying the number of
actual arguments, I believe that the right solution is to make the
KAM code pass more information to fo_unif_w_hints, like the remaining
arguments. Nevertheless, the new fo_unif_w_hints is hard to factor with
the old one (that is used elsewere) so I wrote a new one called
fo_unif_heads_and_cont_or_unwind_and_hints. It first tries fo_unif on
the heads, and if successfull call a continuation (that will unify
all stack arguments pairwise) or unwinds the machine and looks for hints
on the complete terms, not just a prefix.

2)
===========
The fo_unif function does some clever higher order unification in the
case

    (? x1 ... xn)    =?=  (t y1 ... ym)

but in the very similar case

  K (? x1 ... xn) _  =?=  (t y1 ... ym)

it does not.

K has to be reduced away, and afterwards the KAM configuration
has ? and t as heads, xs and ys on the stack. Assume m-n=l, the
unification problems generated by the check_stack function are

  ?   =?=  t y1 .. yl
  xi  =?=  yl+i            for i in 1 .. n

That is clearly suboptimal, since xn and ym could differ, but a clever
instantiation of the flexible head could drop or move around xm.

Moreover one expects the two unification problems to be solved in the
same way by the system, but it does not, and in my case the second one
actually fails. The KAM code should just be a speedup over a naive
unfolding of constants, beta-iota-zeta reduction and fo_unif, but in
this (unfortunate) case it is weaker.

3)
============
The delift function does a lot of work even if the metavariable is being
instantiated with a closed term. This is very often the case when the
term is suggested by hints. Hints may suggest constants in partially
unfolded form (see paper submitted to Type09), that can thus be very
big. This simple patch speeds up delift in this case.

patches for hints & unification:

1)
===========
It is an old and know issue. The check_stack calls fo_unif_w_hints only
on a prefix of applications, leaving some arguments on the stack. This
prevents hints to be found. Example

 Hint: And A B === fun_of_morph And_morphism A B

If the problem

  And A B =?= fun_of_morph ? A B

is found immediately (before entering the KAM) the it is solved, but if
it shows up inside the KAM, A and B are left on the stack and a
fo_unif_w_hints has to solve

  And =?= fun_of_morph ?

While one could declare hints multiple times, varying the number of
actual arguments, I believe that the right solution is to make the
KAM code pass more information to fo_unif_w_hints, like the remaining
arguments. Nevertheless, the new fo_unif_w_hints is hard to factor with
the old one (that is used elsewere) so I wrote a new one called
fo_unif_heads_and_cont_or_unwind_and_hints. It first tries fo_unif on
the heads, and if successfull call a continuation (that will unify
all stack arguments pairwise) or unwinds the machine and looks for hints
on the complete terms, not just a prefix.

2)
===========
The fo_unif function does some clever higher order unification in the
case

    (? x1 ... xn)    =?=  (t y1 ... ym)

but in the very similar case

  K (? x1 ... xn) _  =?=  (t y1 ... ym)

it does not.

K has to be reduced away, and afterwards the KAM configuration
has ? and t as heads, xs and ys on the stack. Assume m-n=l, the
unification problems generated by the check_stack function are

  ?   =?=  t y1 .. yl
  xi  =?=  yl+i            for i in 1 .. n

That is clearly suboptimal, since xn and ym could differ, but a clever
instantiation of the flexible head could drop or move around xm.

Moreover one expects the two unification problems to be solved in the
same way by the system, but it does not, and in my case the second one
actually fails. The KAM code should just be a speedup over a naive
unfolding of constants, beta-iota-zeta reduction and fo_unif, but in
this (unfortunate) case it is weaker.

3)
============
The delift function does a lot of work even if the metavariable is being
instantiated with a closed term. This is very often the case when the
term is suggested by hints. Hints may suggest constants in partially
unfolded form (see paper submitted to Type09), that can thus be very
big. This simple patch speeds up delift in this case.

...

test to see if svn cp worked as expected

Stuff moved from old Matita.

Towards Matita 1.0 (new kernel etc. only).

hints for \epsilon

hints polished and fixed to allow recursive inference of ext_carr

nicer hints, 16.1->3 done

many fixes to setoids for re, 16.1 almost done

fixed notation for \cup and \cap

some reorganization + some more re-setoids.ma proofs

morphism support moved to sets/ and logic/cprop

interpretation for <->

fix typo

patch by Brian committed, cut&paste should not crash matita any longer

Setoid-Rewriting under Ex works for an arbitrary depth of Ex. Patches needed:

Index: ../components/ng_refiner/nCicUnification.ml
===================================================================
--- ../components/ng_refiner/nCicUnification.ml (revision 10941)
+++ ../components/ng_refiner/nCicUnification.ml (working copy)
@@ -97,7 +97,7 @@
    let time2 = Unix.gettimeofday () in
    let time1 =
     match !times with time1::tl -> times := tl; time1 | [] -> assert false in
-   prerr_endline ("}}} " ^ string_of_float (time2 -. time1));
+   prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1));
    (match exc_opt with
    | Some e ->  prerr_endline ("exception raised: " ^ Printexc.to_string e)
    | None -> ());
@@ -730,6 +730,32 @@
               | Uncertain _ as exn -> raise exn
               | _ -> assert false
     in
+    let fo_unif_heads_and_cont_or_unwind_and_hints
+      test_eq_only metasenv subst m1 m2 cont hm1 hm2
+     =
+      let ms, continuation =
+        (* calling the continuation inside the outermost try is an option
+           and makes unification stronger, but looks not frequent to me
+           that heads unify but not the arguments and that an hints can fix
+           that *)
+        try fo_unif test_eq_only metasenv subst m1 m2, cont
+        with
+        | UnificationFailure _
+        | KeepReducing _ | Uncertain _ as exn ->
+           let (t1,norm1),(t2,norm2) = hm1, hm2 in
+           match
+             try_hints metasenv subst
+              (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
+           with
+            | Some x -> x, fun x -> x
+            | None ->
+                match exn with
+                | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
+                | UnificationFailure _ | Uncertain _ as exn -> raise exn
+                | _ -> assert false
+      in
+        continuation ms
+    in
     let height_of = function
      | NCic.Const (Ref.Ref (_,Ref.Def h))
      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
@@ -767,7 +793,7 @@
             match t1 with
             | C.Const r -> NCicEnvironment.get_relevance r
             | _ -> [] *) in
-          let unif_from_stack t1 t2 b metasenv subst =
+          let unif_from_stack (metasenv, subst) (t1, t2, b) =
               try
                 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
                 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
@@ -784,14 +810,19 @@
                 NCicReduction.unwind (k2,e2,t2,List.rev l2),
                 todo
           in
-        let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
+          let check_stack l1 l2 r =
+            match t1, t2 with
+            | NCic.Meta _, _ | _, NCic.Meta _ ->
+                (NCicReduction.unwind (k1,e1,t1,s1)),
+                (NCicReduction.unwind (k2,e2,t2,s2)),[]
+            | _ -> check_stack l1 l2 r []
+          in
+        let hh1,hh2,todo = check_stack (List.rev s1) (List.rev s2) relevance in
         try
-         let metasenv,subst =
-          fo_unif_w_hints test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) in
-         List.fold_left
-          (fun (metasenv,subst) (x1,x2,r) ->
-            unif_from_stack x1 x2 r metasenv subst
-          ) (metasenv,subst) todo
+          fo_unif_heads_and_cont_or_unwind_and_hints
+            test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
+            (fun ms -> List.fold_left unif_from_stack ms todo)
+            m1 m2
         with
          | KeepReducing _ -> assert false
          | KeepReducingThis _ ->

fixed notation

some more work

Change (or better define) the order of hints premises.

They are now processed top to bottom, and not viceversa as before. This seems
to be right thing, since rules like:

  X := carr T
  ....
  R := mk_foo ... (P X) ... T ...
 --------------------------------- |-
  carr R = (P X)

can't be written putting X := carr T last, but you really want to be sure that
the needed assumptions to obtain a foo (in that case, that X is the carrier of
a setoid T) are available _before_ you even try to typecheck the bigger
unification problem (that may not be well typed if X and carr T are not
_convertible_, since in the fix function called in instantiate we call the
typechecker and not the refiner).

non uniform coercions landed in hints_declaration.ma, setoids and sets library
updated accordingly

Some refactoring in set*.ma, some new notations and new hints for \cup.
non uniform coercions still to be pushed from re-setoids.ma to a place
before sets.ma, maybe in hints_declaration.ma since they are complementary.

th 16.2 proved in the setoids setting

...

better not allowed sort elimination error messsage

...

...

...

some fixes to cope with the new mowgli server architecture

we can now generate static html pages about crg terms

some inprovements on the generated html pages

ld.dtd: updated to comply with crg
Makefiles: updated to comply with new HELM server configuration
top: some traces of old command line option "-m" removed

we removed old HAL exportation (replaced by XML exportation)

we renamed the module abbreviations according to src/modules.ml
ld.dtd: now is more strict
Makefiles: some refactoring
crg: bug fix in name/indexes translation
xmlLibrary: bug fix in the rendering of the "name" attribute: ^ is
forbidden in a NMTOKEN
brgOutput: new xml exportation via xmlCrg

the refactoring continues ...

new module "xml" devoted to xml I/O

the refactoring continues ....

now we take the NUri module from the helm-ng_kernel packeage

the refactoring continues

refactoring: helena sources are now in a dedicated directory

txtLexer: bug fix in parsing the string tokens
library: we now export the "meta" attribute
crgXml: crg exportation factorized and alpha conversion now works
crgBrg: we now mark the abstraction and the reverse translation works
ld.dtd: updated to export crg contents

- we simplified the parser return values
- now the display of parser and lexer debug information is controlled
from the command line (with the options -P and -L)
complete_rg: now the empty binders are not treated especially
top: we isolated a fragment of slow code (process_streaming) to be
investigated. It can be enabled with the -1 command line option)
Makefile: we now create the etc directory when it is missing

Bug fixed: nodes were copied.

interpret non ambiguous symbols ASAP

...

allows auto before eq is defined

...

Fixes unexpected behaviour of ncut when multiple goals are selected.

Experimental enhancements to the ndestruct tactic. By using the syntax

ndestruct (e1 ... em) skip (H1 ... Hn)

the user can tell the tactic that
- only equations e1 ... em should be considered
- rewriting should happen only in hypotheses H1 ... Hn and in the goal

both "(e1 ... em)" and "skip (H1 ... Hn)" are optional parameters.

Some experiments on a co-inductive Heityng algebra.

...

some work on \exists

eq -> eq0 renaming

useless box removed

fixed precedence so that no () are needed around variable assignement