From e053aaf3085a079c3125ed4666ba648a48fbb2af Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 4 Sep 2008 09:42:26 +0000 Subject: [PATCH] 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. --- .../content_pres/cicNotationParser.ml | 13 ++++++++ .../content_pres/cicNotationParser.mli | 2 ++ .../content_pres/termContentPres.ml | 5 +++ .../components/lexicon/cicNotation.ml | 7 ++++ .../components/lexicon/cicNotation.mli | 2 ++ .../components/lexicon/lexiconSync.ml | 2 +- .../contribs/PREDICATIVE-TOPOLOGY/Makefile | 16 +++++++++ .../PREDICATIVE-TOPOLOGY/class_defs.ma | 4 +-- .../contribs/PREDICATIVE-TOPOLOGY/depends | 12 +++++++ .../contribs/PREDICATIVE-TOPOLOGY/makefile | 33 ------------------- .../matita/contribs/PREDICATIVE-TOPOLOGY/root | 1 + 11 files changed, 61 insertions(+), 36 deletions(-) create mode 100644 helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile create mode 100644 helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/depends delete mode 100644 helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/makefile create mode 100644 helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/root diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index f58bd21b5..5236193d0 100644 --- 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 0df3f83d0..a348d9088 100644 --- 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 29845af1d..0c83dd0bb 100644 --- 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 e10a89d5b..248e08bcb 100644 --- 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 81b01aa45..6c8647ad8 100644 --- 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 9010dfcff..b9c9b1cc2 100644 --- 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 index 000000000..a3e891435 --- /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 62fc8bdfa..f337d8ce5 100644 --- 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 index 000000000..13fa00c5a --- /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 index 711fba21c..000000000 --- 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 index 000000000..cde289d74 --- /dev/null +++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/root @@ -0,0 +1 @@ +baseuri=cic:/matita/PREDICATIVE-TOPOLOGY -- 2.39.2