notation_id were compared using Pervasives.equal this was rarely triggering the

exception eq_on_functional_values. New implementation of compare using
a camlp5, that only provides an equality function, that is hacked to
return an integer.

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index f58bd21b59b460295d196e3a095f626ac8298e48..5236193d054257091e2962ea626d20f90122777d 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -214,6 +214,19 @@ let extract_term_production pattern =
 
 type rule_id = Grammar.token Gramext.g_symbol list
 
+let compare_rule_id x y =
+  let rec aux = function
+    | [],[] -> 0
+    | [],_ -> ~-1
+    | _,[] -> 1
+    | s1::tl1, s2::tl2 ->
+        if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
+        else 
+          let d = List.length tl1 - List.length tl2 in
+          if d <> 0 then d else 1 (* bad and broken *)
+  in
+    aux (x,y)
+
   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
 let owned_keywords = Hashtbl.create 23
 

diff --git a/helm/software/components/content_pres/cicNotationParser.mli b/helm/software/components/content_pres/cicNotationParser.mli
index 0df3f83d06ad9f9ddc64a21b4a695f99f928652e..a348d9088bc1861816f03e0bd3ca17084efb2feb 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.mli
+++ b/helm/software/components/content_pres/cicNotationParser.mli
@@ -42,6 +42,8 @@ val parse_level2_meta: Ulexing.lexbuf -> CicNotationPt.term
 
 type rule_id
 
+val compare_rule_id : rule_id -> rule_id -> int
+
 val check_l1_pattern: (* level1_pattern *)
  CicNotationPt.term -> int -> Gramext.g_assoc -> checked_l1_pattern
 

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 29845af1ded26666ec2467cd0e1bf22d17862364..0c83dd0bbb602334227444f8b0788811adb76e9f 100644 (file)
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -342,16 +342,21 @@ let instantiate21 idrefs env l1 =
   and subst_magic pos env = function
     | Ast.List0 (p, sep_opt)
     | Ast.List1 (p, sep_opt) ->
+        prerr_endline "1";
         let rec_decls = CicNotationEnv.declarations_of_term p in
+        prerr_endline "2";
         let rec_values =
           List.map (fun (n, _) -> CicNotationEnv.lookup_list env n) rec_decls
         in
+        prerr_endline "3";
         let values = CicNotationUtil.ncombine rec_values in
+        prerr_endline "4";
         let sep =
           match sep_opt with
             | None -> []
             | Some l -> [ Ast.Literal l; break; space ]
        in
+        prerr_endline "5";
         let rec instantiate_list acc = function
           | [] -> List.rev acc
          | value_set :: [] ->

diff --git a/helm/software/components/lexicon/cicNotation.ml b/helm/software/components/lexicon/cicNotation.ml
index e10a89d5bf06152328349222ad516a82acfb3146..248e08bcb242c7ada134c5e5325eae86814e2062 100644 (file)
--- a/helm/software/components/lexicon/cicNotation.ml
+++ b/helm/software/components/lexicon/cicNotation.ml
@@ -32,6 +32,13 @@ type notation_id =
   | InterpretationId of TermAcicContent.interpretation_id
   | PrettyPrinterId of TermContentPres.pretty_printer_id
 
+let compare_notation_id x y = 
+  match x,y with
+  | RuleId i1, RuleId i2 -> CicNotationParser.compare_rule_id i1 i2
+  | RuleId _, _ -> ~-1
+  | _, RuleId _ -> 1
+  | x,y -> Pervasives.compare x y
+
 let parser_ref_counter = RefCounter.create ()
 let rule_ids_to_items = Hashtbl.create 113
 

diff --git a/helm/software/components/lexicon/cicNotation.mli b/helm/software/components/lexicon/cicNotation.mli
index 81b01aa45625364cb33310838c832d9ca7572f4e..6c8647ad8552516c313662952eeebbc2be502612 100644 (file)
--- a/helm/software/components/lexicon/cicNotation.mli
+++ b/helm/software/components/lexicon/cicNotation.mli
@@ -25,6 +25,8 @@
 
 type notation_id
 
+val compare_notation_id : notation_id -> notation_id -> int
+
 val process_notation: LexiconAst.command -> notation_id list
 
 val remove_notation: notation_id -> unit

diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml
index 9010dfcff01cbdefb4e74f1080a230cbcae0f89e..b9c9b1cc2c43a77198fd1240e7d114f6a1407b24 100644 (file)
--- a/helm/software/components/lexicon/lexiconSync.ml
+++ b/helm/software/components/lexicon/lexiconSync.ml
@@ -89,7 +89,7 @@ let add_aliases_for_objs =
 module OrderedId = 
 struct
   type t = CicNotation.notation_id
-  let compare = Pervasives.compare
+  let compare =  CicNotation.compare_notation_id
 end
 
 module IdSet  = Set.Make (OrderedId)

diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile
new file mode 100644 (file)
index 0000000..a3e8914
--- /dev/null
+++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile
@@ -0,0 +1,16 @@
+include ../Makefile.defs
+
+DIR=$(shell basename $$PWD)
+
+$(DIR) all:
+       $(BIN)matitac
+$(DIR).opt opt all.opt:
+       $(BIN)matitac.opt
+clean:
+       $(BIN)matitaclean
+clean.opt:
+       $(BIN)matitaclean.opt
+depend:
+       $(BIN)matitadep
+depend.opt:
+       $(BIN)matitadep.opt

diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
index 62fc8bdfa3047eb47b32990fd09771fed91f6b34..f337d8ce5dd22a8e2515073b98b92a34d6203f33 100644 (file)
--- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
+++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
@@ -63,7 +63,7 @@ interpretation "external for all" 'xforall \eta.x =
   (cic:/matita/PREDICATIVE-TOPOLOGY/class_defs/call.ind#xpointer(1/1) _ x).
 
 notation > "hvbox(\xforall ident i opt (: ty) break . p)"
-  right associative with precedence 20
+   with precedence 20
 for @{ 'xforall ${default
   @{\lambda ${ident i} : $ty. $p}
   @{\lambda ${ident i} . $p}}}.
@@ -73,7 +73,7 @@ interpretation "external for all 2" 'xforall2 \eta.x \eta.y =
   (cic:/matita/PREDICATIVE-TOPOLOGY/class_defs/call2.ind#xpointer(1/1) _ _ x y).
 
 notation > "hvbox(\xforall ident i1 opt (: ty1) ident i2 opt (: ty2) break . p)"
-  right associative with precedence 20
+  with precedence 20
 for @{ 'xforall2 ${default
   @{\lambda ${ident i1} : $ty1. \lambda ${ident i2} : $ty2. $p}
   @{\lambda ${ident i1}, ${ident i2}. $p}}}.

diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/depends b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/depends
new file mode 100644 (file)
index 0000000..13fa00c
--- /dev/null
+++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/depends
@@ -0,0 +1,12 @@
+class_eq.ma class_defs.ma
+domain_defs.ma class_defs.ma
+coa_props.ma coa_defs.ma
+class_defs.ma logic/connectives.ma
+domain_data.ma datatypes/bool.ma datatypes/constructors.ma domain_defs.ma
+subset_defs.ma domain_defs.ma
+coa_defs.ma domain_data.ma iff.ma
+iff.ma ../../library/logic/connectives.ma
+../../library/logic/connectives.ma 
+datatypes/bool.ma 
+datatypes/constructors.ma 
+logic/connectives.ma 

diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/makefile b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/makefile
deleted file mode 100644 (file)
index 711fba2..0000000
--- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/makefile
+++ /dev/null
@@ -1,33 +0,0 @@
-H=@
-
-RT_BASEDIR=../../
-OPTIONS=-bench
-MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
-CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
-MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
-CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) 
-
-devel:=$(shell basename `pwd`)
-
-all: preall
-       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
-clean: preall
-       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
-cleanall: preall
-       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
-
-all.opt opt: preall
-       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
-clean.opt: preall
-       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
-cleanall.opt: preall
-       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
-
-%.mo: preall
-       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
-%.mo.opt: preall
-       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
-       
-preall:
-       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
-

diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/root b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/root
new file mode 100644 (file)
index 0000000..cde289d
--- /dev/null
+++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/root
@@ -0,0 +1 @@
+baseuri=cic:/matita/PREDICATIVE-TOPOLOGY