From 0148419c577eab74538b8e2564a64e399d8bdd65 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 15 Dec 2003 23:00:39 +0000 Subject: [PATCH] new experimental cic textual parser: checkin --- helm/ocaml/cic_disambiguation/.cvsignore | 7 + helm/ocaml/cic_disambiguation/.depend | 9 + helm/ocaml/cic_disambiguation/Makefile | 47 + .../ocaml/cic_disambiguation/arit_notation.ml | 27 + helm/ocaml/cic_disambiguation/ast.mli | 107 + helm/ocaml/cic_disambiguation/lexer.ml | 71 + helm/ocaml/cic_disambiguation/lexer.mli | 5 + .../cic_disambiguation/logic_notation.ml | 23 + helm/ocaml/cic_disambiguation/macro.ml | 28 + helm/ocaml/cic_disambiguation/macro.mli | 10 + .../ocaml/cic_disambiguation/macro_table.dump | Bin 0 -> 49047 bytes .../macros/dictionary-tex.xml | 378 +++ .../macros/entities-table.xml | 2081 +++++++++++++++++ .../macros/extra-entities.xml | 5 + helm/ocaml/cic_disambiguation/make_table.ml | 88 + .../cic_disambiguation/pa_unicode_macro.ml | 36 + helm/ocaml/cic_disambiguation/parser.ml | 102 + helm/ocaml/cic_disambiguation/pp.ml | 56 + helm/ocaml/cic_disambiguation/pp.mli | 1 + helm/ocaml/cic_disambiguation/test_lexer.ml | 11 + helm/ocaml/cic_disambiguation/test_parser.ml | 13 + 21 files changed, 3105 insertions(+) create mode 100644 helm/ocaml/cic_disambiguation/.cvsignore create mode 100644 helm/ocaml/cic_disambiguation/.depend create mode 100644 helm/ocaml/cic_disambiguation/Makefile create mode 100644 helm/ocaml/cic_disambiguation/arit_notation.ml create mode 100644 helm/ocaml/cic_disambiguation/ast.mli create mode 100644 helm/ocaml/cic_disambiguation/lexer.ml create mode 100644 helm/ocaml/cic_disambiguation/lexer.mli create mode 100644 helm/ocaml/cic_disambiguation/logic_notation.ml create mode 100644 helm/ocaml/cic_disambiguation/macro.ml create mode 100644 helm/ocaml/cic_disambiguation/macro.mli create mode 100644 helm/ocaml/cic_disambiguation/macro_table.dump create mode 100644 helm/ocaml/cic_disambiguation/macros/dictionary-tex.xml create mode 100644 helm/ocaml/cic_disambiguation/macros/entities-table.xml create mode 100644 helm/ocaml/cic_disambiguation/macros/extra-entities.xml create mode 100644 helm/ocaml/cic_disambiguation/make_table.ml create mode 100644 helm/ocaml/cic_disambiguation/pa_unicode_macro.ml create mode 100644 helm/ocaml/cic_disambiguation/parser.ml create mode 100644 helm/ocaml/cic_disambiguation/pp.ml create mode 100644 helm/ocaml/cic_disambiguation/pp.mli create mode 100644 helm/ocaml/cic_disambiguation/test_lexer.ml create mode 100644 helm/ocaml/cic_disambiguation/test_parser.ml diff --git a/helm/ocaml/cic_disambiguation/.cvsignore b/helm/ocaml/cic_disambiguation/.cvsignore new file mode 100644 index 000000000..b94ae04d1 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/.cvsignore @@ -0,0 +1,7 @@ +*.cma +*.cmo +*.cmi +*.cmx +*.cmxa +test_lexer +test_parser diff --git a/helm/ocaml/cic_disambiguation/.depend b/helm/ocaml/cic_disambiguation/.depend new file mode 100644 index 000000000..16d57692a --- /dev/null +++ b/helm/ocaml/cic_disambiguation/.depend @@ -0,0 +1,9 @@ +pp.cmi: ast.cmi +pp.cmo: ast.cmi pp.cmi +pp.cmx: ast.cmi pp.cmi +macro.cmo: macro.cmi +macro.cmx: macro.cmi +lexer.cmo: macro.cmi lexer.cmi +lexer.cmx: macro.cmx lexer.cmi +parser.cmo: ast.cmi lexer.cmi +parser.cmx: ast.cmi lexer.cmx diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile new file mode 100644 index 000000000..4827da666 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/Makefile @@ -0,0 +1,47 @@ + +PACKAGE = cic_textual_parser2 +REQUIRES = ulex camlp4 pxp +INTERFACE_FILES = ast.mli pp.mli macro.mli lexer.mli +NOTATIONS = logic arit +IMPLEMENTATION_FILES = \ + pp.ml macro.ml lexer.ml parser.ml \ + $(patsubst %,%_notation.ml,$(NOTATIONS)) + +ULEXDIR := $(shell ocamlfind query ulex) + +LEXER_P4_OPTS = -I $(ULEXDIR) pa_ulex.cma +PARSER_P4_OPTS = pa_extend.cmo ./macro.cmo ./pa_unicode_macro.cmo +PA_P4_OPTS = q_MLast.cmo pa_extend.cmo + +include ../Makefile.common + +lexer.cmo: lexer.ml + $(OCAMLC) -pp "camlp4o $(LEXER_P4_OPTS)" -c $< +parser.cmo: parser.ml macro.cmo pa_unicode_macro.cmo + $(OCAMLC) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< + +%_notation.cmo: %_notation.ml parser.cmo + $(OCAMLC) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< + +pa_unicode_macro.cmo: pa_unicode_macro.ml macro.cmo + $(OCAMLC) -pp "camlp4o $(PA_P4_OPTS)" -c $< + +LOCAL_LINKOPTS = -linkpkg gramlib.cma $(PACKAGE).cma +test: test_lexer test_parser +test_lexer: test_lexer.ml $(PACKAGE).cma + $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< +test_parser: test_parser.ml $(PACKAGE).cma + $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< +make_table: make_table.ml + $(OCAMLC) -linkpkg -o $@ $< + +.PHONY: macro_table.dump +macro_table.dump: make_table + ./make_table $@ + +clean: extra_clean +distclean: extra_clean + rm -f macro_table.dump +extra_clean: + rm -f test_lexer test_parser make_table + diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml new file mode 100644 index 000000000..522021f5f --- /dev/null +++ b/helm/ocaml/cic_disambiguation/arit_notation.ml @@ -0,0 +1,27 @@ +open Ast +open Parser + +EXTEND + term: LEVEL "add" + [ + [ t1 = term; SYMBOL "+"; t2 = term -> + return_term loc (Appl [Ident ("plus", []); t1; t2]) + | t1 = term; SYMBOL "-"; t2 = term -> + return_term loc (Appl [Ident ("minus", []); t1; t2]) + ] + ]; + term: LEVEL "mult" + [ + [ t1 = term; SYMBOL "*"; t2 = term -> + return_term loc (Appl [Ident ("times", []); t1; t2]) + | t1 = term; SYMBOL "/"; t2 = term -> + return_term loc (Appl [Ident ("div", []); t1; t2]) + ] + ]; + term: LEVEL "inv" + [ + [ SYMBOL "-"; t = term -> + return_term loc (Appl [Ident ("uminus", []); t]) + ] + ]; +END diff --git a/helm/ocaml/cic_disambiguation/ast.mli b/helm/ocaml/cic_disambiguation/ast.mli new file mode 100644 index 000000000..d579ccdd3 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/ast.mli @@ -0,0 +1,107 @@ + + (* when an 'ident option is None, the default is to apply the tactic + to the current goal *) + +type reduction_kind = [ `Reduce | `Simpl | `Whd ] + +type 'term pattern = + | Pattern of 'term + +type location = int * int + +type ('term, 'ident) tactic = + | LocatedTactic of location * ('term, 'ident) tactic + + | Absurd + | Apply of 'term + | Assumption + | Change of 'term * 'term * 'ident option (* what, with what, where *) + | Change_pattern of 'term pattern * 'term * 'ident option + (* what, with what, where *) + | Contradiction + | Cut of 'term + | Decompose of 'ident * 'ident list (* which hypothesis, which principles *) + | Discriminate of 'ident + | Elim of 'term * 'term option (* what to elim, which principle to use *) + | ElimType of 'term + | Exact of 'term + | Exists + | Fold of reduction_kind * 'term + | Fourier + | Injection of 'ident + | Intros of int option + | Left + | LetIn of 'term * 'ident + | Named_intros of 'ident list + | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *) + | Reflexivity + | Replace of 'term * 'term (* what, with what *) + | Replace_pattern of 'term pattern * 'term + | RewriteLeft of 'term * 'ident option + | RewriteRight of 'term * 'ident option + | Right + | Ring + | Split + | Symmetry + | Transitivity of 'term + +type 'tactic tactical = + | LocatedTactical of location * 'tactic tactical + + | Fail + | For of int * 'tactic tactical + | IdTac + | Repeat of 'tactic tactical + | Seq of 'tactic tactical list (* sequential composition *) + | Tactic of 'tactic + | Then of 'tactic tactical * 'tactic tactical list + | Tries of 'tactic tactical list + (* try a sequence of tacticals until one succeeds, fail otherwise *) + | Try of 'tactic tactical (* try a tactical and mask failures *) + +type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] + +type case_pattern = string list + +type term = + | LocatedTerm of location * term + + | Appl of term list + | Binder of binder_kind * string * term option * term + (* kind, name, type, body *) + | Case of term * term option * (case_pattern * term) list + (* what to match, case type, list *) + | LetIn of string * term * term (* name, body, where *) + | LetRec of (string * term * term option * int) list * term + (* (name, body, type, decreasing argument) list, where *) + | Ident of string * subst list + | Meta of string * meta_subst list + | Int of int + +and meta_subst = term option +and subst = string * term + +(* +type cexpr = + | Symbol of string option * string * (subst option) * string option + (* h:xref, name, subst, definitionURL *) + | LocalVar of string option * string (* h:xref, name *) + | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *) + | Num of string option * string (* h:xref, value *) + | Appl of string option * cexpr list (* h:xref, args *) + | Binder of string option *string * decl * cexpr + (* h:xref, name, decl, body *) + | Letin of string option * def * cexpr (* h:xref, def, body *) + | Letrec of string option * def list * cexpr (* h:xref, def list, body *) + | Case of string option * cexpr * ((string * cexpr) list) + (* h:xref, case_expr, named-pattern list *) +and + decl = string * cexpr (* name, type *) +and + def = string * cexpr (* name, body *) +and + subst = (UriManager.uri * cexpr) list +and + meta_subst = cexpr option list +*) + diff --git a/helm/ocaml/cic_disambiguation/lexer.ml b/helm/ocaml/cic_disambiguation/lexer.ml new file mode 100644 index 000000000..79003792b --- /dev/null +++ b/helm/ocaml/cic_disambiguation/lexer.ml @@ -0,0 +1,71 @@ + +exception Error of int * int * string + +let regexp alpha = [ 'a' - 'z' 'A' - 'Z' ] +let regexp digit = [ '0' - '9' ] +let regexp blank = [ ' ' '\t' '\n' ] + +let regexp blanks = blank+ +let regexp num = digit+ +let regexp ident = alpha (alpha | num)* +let regexp symbol = [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' ] +let regexp tex_token = '\\' alpha+ +let regexp lparen = [ '(' '[' '{' ] +let regexp rparen = [ ')' ']' '}' ] +let regexp meta = '?' (alpha | num)+ + +let keywords = Hashtbl.create 17 +let _ = + List.iter (fun keyword -> Hashtbl.add keywords keyword ("", keyword)) + [ "Prop"; "Type"; "Set"; "let"; "rec"; "using"; "match"; "with" ] + +let error lexbuf msg = + raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg)) +let error_at_end lexbuf msg = + raise (Error (Ulexing.lexeme_end lexbuf, Ulexing.lexeme_end lexbuf, msg)) + +let return lexbuf token = (token, Ulexing.loc lexbuf) + +let rec token = lexer +| blanks -> token lexbuf +| ident -> + let lexeme = Ulexing.utf8_lexeme lexbuf in + (try + return lexbuf (Hashtbl.find keywords lexeme) + with Not_found -> + return lexbuf ("IDENT", lexeme)) +| num -> return lexbuf ("INT", Ulexing.utf8_lexeme lexbuf) +| lparen -> return lexbuf ("LPAREN", Ulexing.utf8_lexeme lexbuf) +| rparen -> return lexbuf ("RPAREN", Ulexing.utf8_lexeme lexbuf) +| meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf) +| symbol -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) +| tex_token -> + let macro = + Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1) + in + (try + return lexbuf ("SYMBOL", Macro.expand macro) + with Macro.Macro_not_found _ -> + return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)) +| eof -> return lexbuf ("EOI", "") +| _ -> error lexbuf "Invalid character" + +let tok_func stream = + let lexbuf = Ulexing.from_utf8_stream stream in + Token.make_stream_and_location + (fun () -> + try + token lexbuf + with + | Ulexing.Error -> error_at_end lexbuf "Unexpected character" + | Ulexing.InvalidCodepoint i -> error_at_end lexbuf "Invalid code point") + +let lex = + { + Token.tok_func = tok_func; + Token.tok_using = (fun _ -> ()); + Token.tok_removing = (fun _ -> ()); + Token.tok_match = Token.default_match; + Token.tok_text = Token.lexer_text; + Token.tok_comm = None; + } diff --git a/helm/ocaml/cic_disambiguation/lexer.mli b/helm/ocaml/cic_disambiguation/lexer.mli new file mode 100644 index 000000000..f8fe7c955 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/lexer.mli @@ -0,0 +1,5 @@ + +exception Error of int * int * string + +val lex : (string * string) Token.glexer + diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml new file mode 100644 index 000000000..35ce4b90c --- /dev/null +++ b/helm/ocaml/cic_disambiguation/logic_notation.ml @@ -0,0 +1,23 @@ +open Ast +open Parser + +EXTEND + term: LEVEL "add" + [ + [ t1 = term; SYMBOL "∨"; t2 = term -> + return_term loc (Appl [Ident ("or", []); t1; t2]) + ] + ]; + term: LEVEL "mult" + [ + [ t1 = term; SYMBOL "∧"; t2 = term -> + return_term loc (Appl [Ident ("and", []); t1; t2]) + ] + ]; + term: LEVEL "inv" + [ + [ SYMBOL "¬"; t = term -> + return_term loc (Appl [Ident ("not", []); t]) + ] + ]; +END diff --git a/helm/ocaml/cic_disambiguation/macro.ml b/helm/ocaml/cic_disambiguation/macro.ml new file mode 100644 index 000000000..fd93aa9ae --- /dev/null +++ b/helm/ocaml/cic_disambiguation/macro.ml @@ -0,0 +1,28 @@ + +exception Macro_not_found of string +exception Utf8_not_found of string + +let dump_file = "macro_table.dump" + +let init () = + let ic = open_in dump_file in + let (macro2utf8, utf82macro): + ((string, string) Hashtbl.t * (string, string) Hashtbl.t) + = + Marshal.from_channel ic + in + close_in ic; + (macro2utf8, utf82macro) + +let (macro2utf8, utf82macro) = init () + +let expand macro = + try + Hashtbl.find macro2utf8 macro + with Not_found -> raise (Macro_not_found macro) + +let contract utf8 = + try + Hashtbl.find utf82macro utf8 + with Not_found -> raise (Utf8_not_found utf8) + diff --git a/helm/ocaml/cic_disambiguation/macro.mli b/helm/ocaml/cic_disambiguation/macro.mli new file mode 100644 index 000000000..5f8cf5994 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/macro.mli @@ -0,0 +1,10 @@ + +exception Macro_not_found of string +exception Utf8_not_found of string + + (* @param macro name + @return utf8 string *) +val expand: string -> string + +val contract: string -> string + diff --git a/helm/ocaml/cic_disambiguation/macro_table.dump b/helm/ocaml/cic_disambiguation/macro_table.dump new file mode 100644 index 0000000000000000000000000000000000000000..627b86b2abee7ba51793356bf4522def7c6f188b GIT binary patch literal 49047 zcmagH2Y8&-mH3S<9hH$D^)6weX>vC;$?hhLjcu^OG#3b@p)!_)M>Fz_B$qT93sqyl z-Bbf^k|{5k7K%w+lI+4lNOse!vdLyQh4i|~{(tA*JEO6a=lggp-hRvJ?cN#KefY$A z=e@S|yz_#y&O2{-`+4Vma{R!7Y5Dni=UuSyJTDkawkCqVcyQ-dFSz3B)=mB|j(GmI zw!q|_g9{gWq3gSvTNC~>+q|Y&cOudnSs$95ck_}~dHg1v5xqg(`5t<~}F+T+cR(M~eb6Is8Wwni2* z#tqGhM0`VFa&XUC7Yn_MdN#y6BF$}y&i0O;)Jq4hiTfCFYqC}Uyvyidr4C?qqO&>H9*r!ew`gE;>R zEi`Q5dFnBRXJ@S4|N4DiQ)@id-WCTU;|dXfJK!5RqCjqqv~@=PXZF$`O-<}y=*?di zPjqgM$9kHhD>`G0e3wEr+!$B9mrE$CzoXx2rM0&A?`D@C7fh zY%SdkY||HmZ9R$3z~mnK1Rqy+Mx&9oRb9=|sD*i8a_HdA`01Y@j~h*G;~8E-qzcyq<6PB3xqA**qQ86(jCxGLFve`)N!FVv$Z!7-PEV# zF}8i7cVUbv8q69xi$IrSPcYcU@n}3o6EAR{Xi2Q&^~2k|`8u#A@eMIcIG|&zb^#Vg zlz(PM6Rq(?ECK+xJ-pDH-PPQk?1{JWKJ)HWd%zqkM4kj!bKCMGBuOGb23&a&)C+NMW@t>7q6`I2n-X%Ib9i}1M z)Hn~_lYWE7=k#{#plHf)-tND>5n67f$mt2jnusgJAK2@K78wkly2D^_Ruo$6iNVU@ z$&sVT0A6in!qEF&^l_;X6Kns5aUM6=Uw$>b<3Ih3*93ERM|=5d^dW5)bVj<9odDne z7NpB{V6&ATFDR^fz{A87p1-p-Fxjs}6-{&~_YQF$Y)^J}fr;aM(-~WLeU*OU9!Jfy1xR_=P&7Xv9Fm5CDjJ8R#ccggZ)Ku)v+eFsY?YD-M)?Mvu}{o1)=a zM#4neRs<$@BU?gky=GL0o?=uArN)objFQuE`Z}C+viAPeBZd=RluUNE^Ww-Zt`PKQ zLR)O(D`|X(0>rZWF|RT1fAckHqPb1MF?=5l!30|#oq8kGy1~BuG;LoQPb`W;s>A&N znU*csj~?WzGuaul#HZq7fq}$X{JU+TH!D+g4|&0sn98PRF_^9R60(h8jiy>QZrT^KXmyS6jg!RQa2 z@Gi99Wis`ldv#8;qBNLdk$b$R^}UfKii>GHe9kjwa*Iy$m^W*2ygMz76f$O#JxsF4 z;t=rfLZAf~#k<$4N_>$wLdgW(geM1g7$%B3X)~r@8>)i7cY%QLbxzCN3#rGNq3elJ zFR)lo#*{9?Npxw)I&}GAK-SLmj%)!nk*@BZO=!mO-o6JS~zQK_EtXb>v{`$U}d$oqu}Z!SlQv z?|@SWpogoIk%Yny{+feo?TI8}o$(mrVBjtlWkwmGM-@qnjJSGd_ouZxzf$rD;wjeL z62*QQ9`XX$X+sZY-U>x~z&{e{)2R>4r!jvt29I~edy_zE`_o?VdW(Aw_$;cm7r3hB2AG>d)K!o zn)@RDQ@o_u?N|a^AL3k@UEwz1g(K}r!;KUB=(ee)vmG76Ku7m`p{^xM^mO>8v+gtI zo7@cULi@(!-G*=tAA?sTbAy|Db!^*pCOyau`WkptN!Q}-0WY}D4E_OL@OME}!#mT* z1}g(KUpLWC&sE@z5d6&vU36t_Wcn zb^_0BBblccDeX^*C)55RY{pQpHS~{pp=Hgjk#+vp=?U!yJGA=G+>4Ox>V$0kXZj&a zM;yC##!7VPzg>t^X40j9&^DHNi=xR3UV-TjZSc5BRfN$&M-QX_+6+4~;SG^CwaB(X z1O6CTd^L4wimY$7hSP|4)fDYbI8Dg+f$J=#Azi(&bxjaqPi3B)5%u{`z2G(JtP$o6 z=`kIq-sH2`O-l?)MzNgMxk*8=(EoBfYJ{tq3&c2jC%4-%P#}YGZ%#{d>$um0dt3xt2aMlH{B|#n%`!S;uVo_rNj!p332J2Yu zIEHBNYffP2Bck8B_pA$8kNb(p+PHcT!%WcM-RXa;KXq7;HhPt>6+mN(?U=QLV4uBb zT^M=W-Q_>|G`E|3dK2ma?SGQi{^lMK3m7r86&W9e?~nAOqKrp@atUs7lV>8~>zy{+ z?ae!DI1Glz{%+tt@)F?ZsS-vAUN&yRUtc!jl}PJh~)W%UGt(Q@T#3;i?DoQ3{| z(B$BQK%drnRTfMRp+aLTditjPSM`0>zk{kLGSB%Y6pxxt51&A9_jX17rv|t?Gv)R$ z%$L3Qo~^2;_#L_PvbM2$)iTviD0MH~-rUvI+~$Al0WYKk+2{Y4`?=kOJ=GcOYYt5g zk0_V@5M6^Dc$r(V|V5Y1Xnk*6&?p2C}AmN_=4R z+zpOaH@7tA14F0YFnMPwe{PGg?Rx=a#PZuy zN*wgr($%ZzK8CH@*%|LaBM%T<2t}Pl8_qaYh+5Hgmlsn0vTR@2fbN{t)%hl znbIQ)F&qn(rKj)WJmq`tdBnTeOiw45Y4%}uUT@H}hp{mggiu@3+T){KqK+K15AQKp z>{#8=%+L}1XFm%@?G$%$`*#m6{daWRQ1{oBMw_>sF0dWXv^$Gi-+EAJMs9~r%X}M%4fL3Bqxrur+Zy*ZC?j;<7hnP(A`Z&hy6_M8F-lPhL z=V(;zKSSb&7{^RBc}v2$ljB5aE_5W6DeZQ7LG|>IPvgiZ#b*avfiXP?w42i-RKeP7 zx%AXa-W<5HSwkt^9mt}=H1gEMyMn;eIwtvpemFsg9o+2Zb2oa<1}~1=2WuEB66#?y z&sM-cijf;yi5TYgLB#(hSRH1}tDR%dqtN6L8x`t_^X(3#FwE3AizAf59c>#Tw`ftJ z9c^3RtN81Gh{jv2Wj3bN7hTlTtUCIjvTSIXCE0^SfZRL{d8pcb9TgogL7GR^k+aH` zPu4YecVo7^G+uIc};MF4KduAd9IJQG$k+|9EcE8C>WC-sEKwZs4dKac zTU8~8ljut0YaOyp5{5&l_cZFDR;^E{JRy$g-vHDG_N9(ApCnj@?}nF%yck17`Zqvk zBmL>)JjmC$6)E3>xFr!BU0Zu1miO@Cy z1rxx5Jn0INjp`3>Bvgf}dR0k4BWZh{@Md2b@8v_jRv(W5f`4PD|4jl;_AoOwPDW1z zwA~u%ryn)|4k)co4y#+!X2lv&EjYFVAcBVNgmUaih)8;K4Yw}F^d)kt)~~)9;WOe& z2UNZ|2={cX<0FL5E9Rybh%V*zvHN%o+Kr8YAdGY+fq6gSg;3P7%swKiE;xOZxTd!t zC5ckz;F}1+nJ7DAaf;KUdwEIeT8-QRl${Ct8FE6(Xvl16mp41P9;QZ_D4mRAe?`-1 zof!GMUo^F*C8JI|)Ew>ZKoUGXb*2+hf>z&RCd}#(J*tta;5Ej8P>@=~>2+iGVuskj zH-p&9Yf2w+$74kC+apN~S7gPmv!Bok=5Ox`d?^(ai57wm2p1xOvCMf6@^B_#C$ON? zCb01CC7q-fI(s@>o1@m|S!7ZMuOmLfu@-gk&|7z_0fT$k5>@5a?_CJ7qz3AkS)>2K zSdWRFVpv>hEyG=}x{t3FFQNI1j(f1p17xI60)8hL}l0LUcIJNakEi z)V{ZCRX4sC${76v0Q;6POf_b&v*P~@WEYHGWem$>HZkG_uXRQ*j(uAy?t~LzzE=dO z%4hW5J@#c~6T7->`7jrKDb1jgEC=o9{UlJ~=?0~0kp`lM}0;ibB&7iNcF z_dJWKyG&m{ggavV2L&8~0Pj6Cew~K0+MI}WhtTAXM~#gfQsAK6CmvTxXX0av)HF^h z>B(*5aEJBspYrA|-Pj$Ek#Oj2))?QNIHAGSZpJ`*u4_Fd*$Lu1dyR=5v{Z=7*#(5d z8&u?@jz?g5FmL?(w}>dD&ft!v*Ing5gB6E&ZIdW>dVz>)OLQ{?k`6X#dMBB@vNsw{ zb$pn<2>fEV9U+^d#1C+G;n~kx-O(9yXzhnk)PQa?`uZ4x!>CX|M?jW~-b8|!{KPnvrOBs>1B^1( z=N#xKjG^SPlL;u#3;-4BWZfXP<5?GK3)q+r>O~tjn$qCOoifl{l_U4M$VbW&1Las+ zUT_7j7Scv@gP}FnQn+7z3lkIFjo!Q@9dE*J?rcwuMDu9DtE^?X10fKOu61ViXy!Ss zMx8)YtRWF?x(78ib*@kjV)?A~pM-%!2|B_yRP$;kGbhKTxw+v(Ua+G%$~(xVnRebr z-VdE~6^gZ6KL+j%cDsoX3Pte6u7Ir9q1p_M`3WmBreu6=kCN>+GX~t~m%QM0Zers) zunigm#U%+CYk9Xj4npmg0(ADVh*}|tWx^9(&E%*!-}5B8)y6zjiMXls1TW`5rbzN^@*K{;Ud5i+Ht2Mz6p0C<$k0loCXjA5~Aff2ReuXlF3GSjWbW;lu`LVS_r zF`@z+q$PovN5zjZDJx`7VQ9~Ta$sB&BhWeRIsSKU(OaM!fBr3U*^ss79uPNbZ6O{~ z_B1MDraCck^YjoBC$L1p38@B2IcuhThlVP`o2@`ObAp*_f(B@eeVTKue-qOtI5NK@ z9$$Bs!k+kh_jCY(&p=DLcu#O;R9ltxg;O%ZKs8wd&m27LqsXq)+ z1=o^?BLIXDTHd=(hd!8bFW7>90f$edKSSgmhNe@k;JF-z<6w8qEs)dP=(5ZhpQ(GP zcOizu8t8HZV9bZHR_9O6*g9i_kELHh_Z@zMDP9kZTK%Umd)&8}iie@A!1b1Yc6d!B zve9$2`M`nnTL|;R8q!dt7y&>90sbR~7>bv0=ghW5%Q|Na;cEuhTOjR(F_*4h=0C-~ z5GF$c3OW2~^nG(Qq8e=gX&-Ds8zEuf9~GLaEGMucAZ8ObsVWZ9W0wK2^Yv$Maox`Fe9ck@B8)p(Ywh6o*MNN`Wa zS<~WlDFIv-+GsM<@9ZX28r zDEvOMfSOl5qNY!WLHTJMG8K)=Zge={&1&t4w60V62&PS(HlcBGV5qzh=u-kF5~CcZ zB7|huTA-?h9d|$kmRf)qz)k=kxJG#pyml*IpYsCkOPSah`b&*pq|Ek=r+l`?I!0$6 zw_V_+4ijX-#_BY|#>X;FA+KmOT|j_%#XeYuU8mwW7%@ygqA@LRHrR{Bd$3!e>S45S z5Rru+{1j(h(N;!r3@hZKv=VhrFw-MXPUkTu!j~gM+OU!gB(!JhOrfHYcf#JmBq>m) z2Yvs|Exu)dH!(nUk$B5%7l8RBVUhDj?*LY3In$c*nX}l$Nmkp^lu>o|$Ze}D zXY}UiC>q8FSjeMBRFRB50BVfqZj}7Q^IpKnJtXj~SW?3SHd=qsIHm>(ZHy7N#Ck9+ zjc5(E)1gjN^B4rbO<~MYEgK2<(S2-bcye@9jX9E*hCatY2>^!7cJ(XPL!jIg5s)5A zpXz*8_C_N}tL9BArH(vHgDFo5zcgsVGbbU9&~hsiw{vQu6^(OIt&5vCMI)P3TOu|u zGLltMltD7v;74ZB!`Kf(e%?i^T*Z}wEalDJ>n)fOfKdnoy2Vbalo?*9kK! z%nzA(f2Vo}U&Mq7!ZX|*+zou4NCXf8HJbPXB>4M19sbj}Kt z$YdHS*51u9l&_Ew^Okh3T^mVQS7?bT$MdjUG6JpPUUfEA^xci2kWdXk9xLtwcHYb- z)GpcjvJqo~8M=r#x?l)F4YP(P2kurf$-GeV2&cWDJ2KCCLTVDzZIRB1+CFkKW*&NvJfY82T;W(I%b>-_4GD5i|thf8Bz(5 z*-(Ib=3}JMn7H#twq~Bw&rJ3BI)F>?LzAP%44ZG+HD%#D{|PpT#y3Mkw78c(v7j}V zgnlr?4KA?;?Jf=U&&%KrH3SFo{Q{;669qMU$}-`}j&rXeoOG(oyvYPe-!8U_3$+lA zxXEHK5ku8l%#-l*%&B0&$V(;*hJf&&)QTwU<3Gxm%*mvOfJlJwrvI(s^f6?fG1)^# zKzZ}mbYr6^5u}Jh`5JFXCF?k1=Nf0hLrH{Njpi9w3DSmGKn!Tr8!8ra8KxY;ps^K0 zXEB84``en^+tn%QKj2+xTw=%s_DGc`K5yihNxCCrGG5L&S8_4k(##Oz{6be1n(hlY zqx{2bakekI*!XGl;PkXSr#Q_@Rr|&zu%(**Yb?F*^XA)7$W($yYf7Sy(=q-`yO;V; zs)ujRFQbLs0Ba>6LTFN0WNyEk+xvB_QCqAx`kH(2ULH`xU_FVG#<17HX&m<0kT)-d z*;KUm1pRcnIJyRA+f7XdL!PbZN)?hobo8ZJz*uLWR=;dZUuj~BMuH|j^ZNa%m*CYg zeAwVE4zu@=uhtatrF{IXj=Q(b$j6~O@%&O2t~yLQyNeZUT9Ib26a=t(FlNR^{M8F- zPyt%Ni3GTsk$#g(QhVfSi?cTvWq6I79JMU100NFXhWQX`jRF*$3aD2DFfN;Thd1k5 zP0Zh5VqFxZ1g^G-y9I4s55hO`(sk1~vBQY?!c^!j;b8ZsWM?r>HJGp!iyty$^jdXFU3?;)%duKNhtED!pLy=OD+6WZF zVQqw%lL<-gKj6)Dl>i`ZV7C`sVaLq-GYu+xwG?qbvBzFlkn;3Yp>T@U9gAG5U_|9- zeg{swsBZzmqZ%mdvq7`bXS}(}21aTb7iWm5MR>E7lxHxp*yzrh~VboD&v6 zaFz9wc4&w;WMUQwU9GxPT!n73!I#l-j7gU~V18scBWn#QjA#`f(S0mK|0&9C(`Vu9 zO=8}EN~wt0yVmZX9=8N_nMxi)W?>4sBMCxS1ITZ6ZPl;UQ6u}QiXXm%RI;JK%aj65 zWF&a28?H-#L=e`BPG#Z+IB_^|S}T2HZ(M`r8X9Z5F0w%j)Ej+XU@gYL+XIFQL#B!! zNvvvQCVmO|?x{=-L+d7=OcP@aD2)3?bPci7kNRruZK2{b;~w8@G{WkfqmOyPW;aI2 z&&2$Z|72*6&``9wtECM|L)?Cig~=JM(@EWBD51E6I7NY-CRFh@a?6xnrFq6g#w
xBjK#t5epURu2GRW9lLfgFVf$4)Z^Y z{P!sGi7za&06Rs>i0L#ZTJe6}f$NnnxDF-786qU1Dq_l>bFR}CG=C68gV_yXsEDvFH7cSMB*vvY^$-OAY@Tz5t zO_B}P0;M(40@UDp$Q&@uC_5WwU;o;2n)b!s_$u;AK&Dt(C zI&b_q9Wg@0<}n-yF7US$JLs5Dukn`Oe#p}dv(ais4ikP=(J&J+mnw@_XQa;OSJzb^XK-z}eQc{%LsWJ`Z8CR*=44rPLWlA`XdMjf| ze;zRx?%34b5y9!`*XUiZiJDN;+=CAv^Pi%?%VlS_db3?Bk*F^-)b=m4p)V-=oS>Fk z#_+wV$vEm=n2{m9N(&+yZ{uUlfTnCc1AMzG3*2UCUUeCQ7#YChh>CO;FSMwQu+8{i zv=X?%lC}oa;h=QJd4wo(c$E`c_bCp#jVXVpzGZBm=7j&`Q_!iVy!~&fE?1*v9X8v5 z!A&4)LgdJnV2iQaSeg;Xp|JVSz3IE!Z_oxfM-O@PO>Kmt2a-3{5d+3GO}{|1jDLa{ z?ySXF{*eTV4#$N?!d-F7%b}jpBi_tjLThf_3bpgp7=^QC3t-9WIvCnF=iOd#;H1*kS2kc=iokX7KyI(k{nZ-m7cGP1gOSk z;xiU(L5H46`-Y)(BSlz1!;2(Wz$s$vZtvY{47->Qn4OCHj1hN_X;2F2hbcu=+=rJf zT50kbnpL}9V=BSh_5NAs%@Jdzsr3}Xv@xq6?lE7tr6MHw9*S>(JUXZZ9npf&F;y*U z;Ts`LP;Gu@SX@H}qr`7{s<9|Mds(ml9gO%!a#}_OYNE#}!AETQ7V*dECiD5L=R61EP!_2&AWl^WxQA}FM05;Si}ggwWMsY7 zCrtc8!W1cLF{}^80w(o}RUsZT&Vbsl$Y^TdS(2s;Drt+H@p2f>f7;VrAZOgeTS&jk zD6V%-7pCkA%ou%{H5wGOFtTxQ8ob%zV!Mh!)p=Cyj6JR*kRmN()*O2V@K2S~oY2{9 zH2Gm`1J6xK1dReS!n<|3Y7bRGoWDd5Q4<{44=gQy$7ui&6D0(MGf4!cX|u*TjEJFP zm%`_6Oc5%diQ2_Cy72hu0eVd|lOgk;d^r`kH-;X)>>;&dbc)UoodQdxE1$SPmKoTL ztCbbFNjY1+Q!S*S&`}YcuY`12*Z=f z(@FO~YNFnmkYN2W#ZQ^9@PRRPjch%n(fQR*8xgfz<^s&toQgQCs2depZ7TcU#G*=_ zF~G&nV?Yk#U+O~d(>oz86G^o}l2KSMaFZdFE%b$Hj|<=q3W#Ql4i%)DKr%5DwH`1u zdg277Mm2vHMDLrh1=?7}a}=H)JjR1CtJAPg)Mrbb@%GhjR2uBRMggrcp?M}T0xg+Z z3Kx9D0Ba^OPIIRE!#1+6@q_AU#Fcb30}V2g z4Bb0*Y626hU4;M>c}A&81ImX9Q3P19sDIwPb2xs_r~lq9H7`sFsd^6KM5@ST%v+FA zh2S*ItN*_*80f{@CoaI=Go;`TyU(L(>mU%^%j83Pu@p{5iWL6v>R>KHud z$}E_3Q?`g2d=;O>W~+x`zTjr1(=)FirzlEOnYaxJz1%n?YLF`@Sv0}V!L<$rX!j*1 z*I=Ta_*q5`LEWodn%2PvQ^HiQBgn#Q9B}k}Lxh4}n2(ZV{0viVir%#)lHan~gzq=GoLLV4EqWJgMEd4aQ;&cG*$x#7(}&j8fyh>$?*sLa;?y za`u$p2@s)yV4n%&9W#NOM4}rJa8Qk-l-eI*!E~%o*=XeH%)81`YW|OqvC>$r<7H)Q zZcR!E3n}ejlnFJ?e%swb+}V96;h{%8*m%nq_BUZOW__*-!hugvO3(zgX z!%T4utWnZF?JhzNlSXXdKyxQSSJJ3iD$>I74Uxo3t>I6NWFJY83{Vb1(afCS<_NX6 zpxiJIu4W(+Y4@LGl`avoRB0*{L}@C0tT$mP>cHVV-FJdQ*U??tAq1slc2vt2lF3X{ zms(;kycA=l4;jN$aEvMM)VT~$X3K0L#3Lq>HcMl~I5Zmh(l{{?M;l_*EtpDLI|(?b z1`EXurnrRyrmz;SUvvqIkw{QTMIdpe(MMp;xLbHiIk$P|Qr=OytlPV!q6kg8M@7xoO#N*zzE@g^f?7WFRR`gOaK1 zpsiyYz0a6JnQj1h*{*o8iKRi>3c4amqPKV{-52>!!s~%(yj}myt&9C9q3o_s(&YY= z&ta`}bvK3q6lP3oJn0VR%}e|zforO~*f?XroLd^YW7iulkT^;VR*b?z)_~B+j{{dP z3K0`|i6i{&^rx#ahmR|4h9%cmhM+tkBhh`Po*3C|bbvDAI?w8NkpMZ?5KjaJ5@|OpcuVls2ve zO2R47tfi47>JkA_&PW<1dv!Sbabn#q=0GN`mB=nu-3Uu$jJg~@fpz1mV^Bl7>VdkZ zwABt)XnAzVtleImDx7>mk+j+7#!c*7BaGuDJdAOug&~7zi_oH_#;eCfLb)is2G!uk z&9Q5qbQx1nvvdBpG%m&R3@d8)AtlpG)}8Nn3|(l7Ot;vDiB5_1YX~o?8XD#sQ(H_S z1{#O@X|~$@)}xkSE~Y(EY9~>ByNqg0ZkV7nj*|G z{7j^_&Aw4W5^d>{?`HP#@}FTDnVJxa$HSP+9cU>X7|~xZc$M`6c0u03RVD+1 zSv51|st~$jU1#PM{oZKVX4hFEu|=th724_16-ATVpY@uSv(rqcn(9MDw<$bBb_}Z< z&C)O}Gz4!oQ)1r+lTaRHC5Xwu0IOHvR8xqHpkin$K}YVKI%6bDoo>LRWyEWY$#v#Q z@8Yv+a-B-wgZUL^A&jPHPnqSpUCkTmbfbQXv@`TV%qUHdhHrvbsV8vy059p{En}1* zFIZ!{#yMx(&VE2A#>r72>}T~HMYnBf7$5Qo&l7j!8L9?}XtENJaDXba#@WyowecqW zF`z0;@6oX?;8w?(u+vsuI%Bq8NF~Y--AC?_V1tUe{TODJNtsQ$0FPQR7{^kC#!N%0 zT^guZxZQ5>@-|X_?hQ~e#gb?=BcX`ang6^wsqze61FSRyR;X&3z_iuU&ZW^vmtmS= z0u>nGCO?6#o<0k&vk{fk*iW#7Tnu?RJ3=+@P(ON`)rk&|*fW7Hm0A=9!ARC2IgN58 zPUZGnQ6|6LO#(MI%nD;u364Lb0MfmGG^+sx7;}Qn$a;G%xw4*o>TXl3sS;8r4N_Ol z?v`fVarQ-U8FN>6QX}TL^^25NTy%lqtINIAsMk|$ueD?ern%a)KzWn@B&2$=<>|96 zpi!2r7?7{&P7x-?lB%I!awX|j(I*>|I5AP3cKAT@$TXSR>hZS`1>bp{<1)UDY3 zr*V9{6J!RM+9+XFvl9kDA@Aj$1KQwv2f;^`WG?=D-Lm&x@Op=L1bJYiVZK)Pt~DXH0jap$L`UuapTvDOId~8t~#fD*EVDhu0swZx8W98%Utqv&MpTE*Ah)FZvnB!FTluYgO z1v6xn{H6?Wo$BnU*;%QX!h5(Gt1qM_`vg{xVGzx>+b+3>Dkald`pk5{hCrc+WQX}5 z1a2WY;muL+EbZFrW>VqJ>@%29VUO>Yk$hbOBy|=3yc^idg2_cR1A*<6-ND!|55lcW1UTEZq`5&{0Z%~b_0yP6|NO-q39AN7Wy5dnjwA$l9!H>DR5CHkdsT(u82r=)p~HrrY_jw*^szQhe20 zV6yy%w4fAC^P8>e6pf1BOsn=$&wrKke8MXn4Qpr&2TTni0yxcZVXNa;OSeQp62@XV z^qldL&JDkec&bHon~d7)Lb%Kj-Y|q6Th^=|M%%y$m9$nS87*|5da!xU{8Zz4`lwtO!?t^^}cq_7AWf4Oql{`D9 z_DqT*?=roGOi2Wa5MiY*o&O~3T~=5~V@R0CN>MKwZ2gU@pp-kcT9c(o+IK8!R>NR| z1zic{Veit#1U%X9_S`iS8W|ugl8RO_iZQBI;v1K&V4V@65C3wa83XsGjt2aySBb87 zyYdBvkybAu-}ajT*lhB6FczL3w}{-B_EyrKsxXWgOf4c2EcgW!bZ9I>woztDwf{}R zwX56?3n{rXDh#Z%I7()cJ zn}|wM3>Az`EA(*RLu$T3S`&E2_EX%uVeH;THu2YQVH?r?SFKo8P^+V*!3Z8UIoZn% znt)EBZq`7vO|xAz_W*=y(KZddvp%yAx*R2Q)yF?SxhC(_lopoh=xOvbbQ|h1yVK5EY(fo7RH%*8c}TY)fpjLc z%Ka7>#-~u!!~*~s>(nb#3*6L-T*rV)4!pkk!)XZr_(yLSS299y^W;Sumj z0H|@!SvP@4*c1aZ;A0vpi8!$^qLzp`Z@k=_XDb{jH?vU?jqk8@7vWDHOP89F7mCH# z`aieBl8UkcsUt?}_T4b1A9z%6kbQo1i<<7W*bC(9Nc$`JBDy)amj8H{Ov%;^B*2vA$94&a?V`0f4`z+}uO6OjYDqc9?x=oS%7qbN)Xmez4KwWZf7=&XaAja&Hq z)QNwE%45uMja@i-eiY*>7zeOuZaB$QK0pr7df_EgD9bokX!14UZm%*V>oM_Gb}PyZ zQk0hu5Tei(rfzkqEoDRQ>g>%+fa0hc!98|gC*1C&W&~OslTc^*M#!_qTv-yM~J(&*lUg*@7kyolr0jN5C%bmxIB7z%1ljc@Z zqJPKV++)K`J|ZGvVr{xWV(MHwRA8(D7#KhyHVV@9cTX_~NV&65eY$a|N{4IIt0HKH z^G>!BbZblWx-Hr85luiOH4x(Qs>n^n)x#1Ebz(a>cmafY{6!}l9fC=A}sz#Xbf~(xT zFrmEJz1?oF44^(VoZdYxQye~kmxB4FY?k(9ak|JtF2W9{!q01Bjw&`F94$8wm?BWh zEmJ4lTB#Ps0i91|iIGO*m?dr*t4$}6l19(3wE>BvrW|;dUB6*VdJpirSpTNsRStX;h?7}i=)dG=t{BGpJY+@a)>x_3a zi(m)gY+Ll)LwA}`WD$tph~Uaa#Q1r(-JWFVc+4@iMbWyiXD74VvwY< z0Sp5ezzVu?P^@LaWXUwZL>Y#|4+f+E2C|q3+<|A|HLg$!?wdolknla*sOX|ZU44U3 z>>z?o*=t?sy|`^5Qy$`flZXTw)_A^#*C0Ih_=#Cx;tW-bsrM91#{WA7x#;%e#C337 z16L^$Q5gOk68zHx`sHPXzEav57B+OnEFBD!g=M{fo5}uj_5@ICUJDGFgi_ViR$3S& zO{P55IBe9`umF`pTci_Pyk$HOu_N*r;#JCc708o(0)sVYM`Vgztoxf7^J;11v zk&Ou22cGw4TMc`Iq1@5kjF@@}SPX*{uO--~ph=7 zimhw|^FT!F1XgOU=m)yxdsxdgRXiMgj6EE5byyn&cN94vWZz>G|9~&Jy4H>!)()&R zJAL3A;xpUQPxdg%JP#}~zYC#b3%8`4GNMKc44a-MDN$ekmFQaBQg`H|`RV$}8{KLd zR2bC_Za{FuObdGR+W-tCV2D-gwu7s!)3xI%PfI2vX*-pntZ<82?zckGlwo1pr*8w{ zs1s)-!^0$jwK(e&Q)fB|SI5ha7j`ovjT@ViDionLhPvY7T%L+wZ!@4`-a2Omaq21PJKwJg6x`BroICzY14mLUow_=LI&Ym5R-OgDo5B zKMtE%2@L5iKrk8v8jPq_h?7DH6Du2ggCzt2(9CH}C4$}uQHRy>V1J*M#t(C{)PxCC z>rhsgNN44LN@1N0dR==kx0)E_05FGZp8BxPmPXe+b~&>SG{& z83sxhlmyI-hsV<=iZLghpaRW?rE7>Z8cA{yuTr^Xqg_Q|5+!jLDj^maV@|B*I-oXN zQ*YYvqL3oyw$#(G2s?NIR5sFxrPiG3iZnj%UWzYb489<+QO`lw=(B%>n*%k=P-;637XAjc=+b`@TP+-SRvat)ml!@DB;*j-q+4VGb1kM)sfV^^$#%vC z@5EH{y-FXtrLWCGcni#`Zi|KY7h=P2c!WBFl8+ ze_O&qj?+p%kl61vP31q#mad_VX{ZJ_xH(W0+!K$GGhr_%0(#WCVJ_m|2VzA?f~t@+6sCB`)-Yp+Q%v!&wXVQAf$X6b`Oa?j@7z{9X2(MZ5QO_- z0u#FWubEZ0nzN*884J>-NROo3v|t$p-Jw?JOk$DFW8XY7CF+M8KT=m&GP!G&R1Ojt znv)_88&@?EG~*gU`4m@LH%ZT#oZS(5n4L5`yG$+93p5qfU<2%~zEaPIPF02@Y%F+P zoFz-m>jLk*%x`q4+EEdO%Q*WAe&Zlc1+gxjVwZJ=qzk>{l?L#A^$+M&>4V@^<|r-idu=q^kSfj}#_!(_wv)ki#%$hv{G?9oUM3SVk?!6^d6RM1YEY{qrt0 z>r|0XXRTFzXAg^a+T6kcUJoZybxVjV7C2GR1z+It2Vz>=K=^#twQQzD_*=uv1C((` zQ%FCGv0x^TEJQq;!QHfs!95Pe*a8kh#%4sl{Vi~kVm}PH>B$UfXxe;k4R{&yXayF2Vu?UTwKb9iIlI^0I7-P zA0={UnpSWg;M^64?Yq;POZGfd=I`|8;Id3DnbHNwq0Za2UhVX8*ke-Eg5Lf_sqv%QSX-2tmn53dyZzSZmOYyV<`}D|O@12#vjw)h~vi;5(zl-peFA_tE}kbqs4d*AWQ4K?bZY-QSLl1wR@FR=~!!(!z|da z0Rt7$wxqzt(9`w`6-_qn{fO5@nl$yx6THvY8=xDIpb%h;Nd8nrnG!B6(%rfk$P`L3 zsfhs#c2x21W9lR6q>M$Lni=8d;MLCeF&3;6fP#b6IYw#3IdBKL3TXv6ym3rRoq`Dq z%7eB8ot#EQ+1yIE6k*3VwXcm}U~??zot(XYJd0mbZ<~pAc7YQ8p(qZJuVR_K#n=!R zjF1XiOk@7jR9-@2mnezt^a58{#9|sKTw16Z_$ac}rslNX-0mpm@GyeunXv6Ef$I0s4 z_E=KH1V>V+6R0*TZWAn?-eTC+Og)E@=Hk1oe&}*T!Z6d0lxLCd;ZBoU@Snus3EHhz zhY9edMUtyU$FmE>U<=%a;5Ba08u8wkE=@B7fa5W0Q(3dUTc_5(TD0v2ZEC^k4zWiu zfzzklcKd;hKrsGh47!7Nb5pSnP6t(ZwCS%=z76l=*4UU1))U*Sf%08^!f^|xB08K; zjO)TC#TgfjcDeIS(GkIw%mQJG#X&b_#WzCwINR>988d}cDzabXhcBCZ{BHpNnHuS{ zVdf*0gi~hE^L|V=2j2sxnN*O7Ws(*ZtN?z4+V!dX#`5dJ7gqn-O6T#X89d#M;G%|E z>TF|i4|z?RCpN^U78(;Zzn7{&SGQSp3ap%Q&I6WOni{4D8D3etdD|NJyqX58PFMFekgNPhO*=jxOJzSM@BjEssL{WE7hob`CKms5$> zi5I+SIdxpjD`0+k0PL_QvHtue7^PNa>Rh20wC));pw?w!o9GM)QSiv@tDmkAX1#&h zW*OJ;zVjU)cQ&eBk`9iH^mO|grvq9;YBcc6k+!fOBOZD(8;BmG-YV*fW)D#(qh+#< zO*({d+{jY@DN?pmr`iUjybV3YD-{0V#2E+9R63igZ~~>Ilig{MJ#Siw#WgL~oyw!6 z(O>lDE#kL%HeJcG7#n3)BIdU>T6G-9=LPm&wTEJ=+4X#Lj))v}yZs}j{8HsJgaPU6&#V@^1+ot}wWr6Uy2c>FAop{>)e zE=>RGFr8|@*)L|3kyz+S^)jhm?#Z+TGVMZ7YPL%aEG#9pQc~wh)u2=jd6KtI@}k_W z`xmMESB|B%Qd-Bca#$)yJSl3DqM3Rbm&$HWe7_Ul?@cevjeM$e%{f|i9M>*zvR&q}2^^;PE^cG)__7b3n;luz7O6s-NZ#d=r?1yem)b0j@==l70N{T~^^ZCHP^y2# z&09on^|HNe9mce8%QWWdJ0`xzIgE>s?(5p5F2b{~$+WNYPJTf0gB%(q-w&7`lj4Jn z=(yxy(Mx5GRMv8+lFDiZex+1h#og&2m+7D2uvw;mj7wj;_&Ruci&Wjp;by7&05^Xu zzW?UXA-+z1=ab_56c2wRRloJ5A}JL*;pr!3`Y8@C$@G`G%zj6*e*t#SNa^P|oRZSh z-2ACz|BQ!O?UF?=SuK*)s!+&^N>-PcrR4(q)dB?oBu4umus_sm2BEEw8GWbCHoswH~&MXeT8=l5>k+4m=jWa zjH%X3c>`C6rS=HVl2V|E_I*u!UuTMQq-rj(s+H+5ckVYO_gnPEKPA?jQ<4L|4gc}# z=cVckJo%&)LpOQTB~MAdZb<5eA&onvbSsB`DcwSIf0XHe;$i+bC7m#%LT-_5+UTxza%H+fj|hSdBUaGxoa zv$%Sl8#M5Wl%S!-FgJ%!NmW1dTqt>qxcZV*eVK=KQK^H*3%5w&9mtE7Qnre_zGuXT ztSSGglq+LY2c$a4r~4(3_>APgB>68x%6CfEAeRMer2vAceO_uoc6C^)n|SvM$yTgTMm-x7Hx>RN{)_{}*xy)H3IX7|leyJpAB(ZR{Usd8f>|DFar3nceKE=z(^5~9Vcq<9%q`HJLyl|kGr(~vqP zC#2*x#{Ud|pbvpq+I|T@3X8N~ZssRxg&~ zOZ4vTQn!vze1GLxqwBg8QpZ5@ zPe?w8`h8NrAL471qKJO64$N}sq#NLWugDH&&?wXVT;0PB=Kgc0PmhICqGR@5Aij42 zf;`F1=W=>Lri1bnyoydskwUfPeNys%I^8Gvc=A#)O)93-u;bIhh!n2ncHN}Z{eWY6 zla$ZoSbdFDuh9D+l)4Ww)(55jAugxiDAQMRthqvJpcN?}lJa4W#S5fZ(cr5SUp>d7 zuS(I^7L7rT$8eRjZ|HjnQRH=D(!$$9nHIsZw?;?2^Km9?gh2$s3nEMSS5i zQh1zW-E66w1EGCKD!)q)bERmWKK+msewfR0DXQRd`u#Hf0SN5Br3|Fh&ye~HTz_>% zQioJ22}wzq&*n+te4`O67fPjKtaeyxF&k>Kq(%j8;U+0mL0tZ0DMw|M|47RJisb%St*C8E5@XPO%?P#-)-V+)>FMG zIUpsEaIA_*mD1F-KgzT}arli)`z?1rAyuE`Zc4o7FOd8TdAeDqeGI(4OQtvSw7x*< zVeOJXNXZ|8!UdA^F2vREq`=y4U|^fn5~TRs|B!BrC2I*Cd|zbJ45*<%8Vb!>c9vvk z)7c4`2Iu89OI{0|mHDKsfaA0~WZG7azH7yI9jx+<U+5aioKjc{Qk5cka4E1^`xPi;ssMI2)eV-CvKbLuXB@X~kyGy2R z2b;xGU6Q_OL^bb}{#r_ZLwEI(-@sv9@|F54>ZO9qnvGJkiK}Xn>beJPvdGJj0+w{dyDl&SJDEis}TOd#%lRm#4`-I}+g z=8IfDC}k?c%047zAJ$`yl-0rl0Vz^FX5I#I|1P!v0a|}2*}rE}-<4_K<6+ejsanb~ zzAB}Nwc6!Udo>{Yvy}g@e))AN`-UF1VY>TIsZok3eOpSu#AJUZIp~nGo2Bdn+|7AT za-QemS}AP@Als!{J!i@Pz2yIar*})vJ@j56*@fD~N2T;O<}*`#vv^o2IV$%n_=oDN zI4Tw6Tsm8`J|y)Bwu0-RL8!G+>X9l9`O@HnIJ=}oWoy+cL@*6mm0h)x8+5iqvUk$l zKS{;=c&8>JHEWq%hm?2nyJkB$Z)a&Hj{R_tV#Esb9k=t%+5* zP72XuzOCYe^s=`|_8nX~i?rfSsZhH7gH*%bg|A5AtMqJdR&13DzNolSDj=Nf8zlQi z`e?|J25?z%9-0eesZvYdEc<6EyPTWdQna2izFW%i!KC4f((pEyAChvg(eM^GfaLF_ z6nr);l7=fF>p7A&msi$E`AvLL`-s#&3eA5H*}>hvNIA;7e3g^~tGrc`$D#HysXfR% zo)@3`d%5RHt`29X6zu}Hf0Qx=UCv)5hYw3WA|)T?)j{zM@v5&ze2|&1N_^GKe7RIZ zI$24{>Y?#dl6M-SeoX3UydW$EO?;8{E6IXld{2n)Nyc$Gss;cQOGSw`_gC@#9|Jfh zxsTIaT&lZ4$nT``_dLwrFWG1Z-=*TajLVV=DS>$k3Z$SA5_?_p-{9)YQt_6zAn#<|ELk4_GLw=6-&cPh3BXlQazZ?;UM1ClwsfhK zUddoLO9_e~t5&k=Xzm+QsD^s(ZzUJov+^;iRPf&kSZVz=$^Hz_el5Abfv6Y5o($)R zG#urN>A#ifd@=pkGM$Ic0V&Cm5~!%~pQP}8Jo}VP@8{LLcS&9&t#*qK`l)D;iu1XO zbAv&?DLHR}+V4o&clj_|3WeEyRq|D$7&C`<9+BzLP1zzTgQ!Y>FQu@syIJrvDfl_O z@iVFCP_~e__^y^u0hzTLaxanGOKHu4rD3-;?BVJgQVj~SswJxi>HKafeh;JhyySd= zVW=ZXGmFGWhlN#ASk3o^N2Cz+6iwor@~U5Q0(`Hb3`V?6@|Sbv4F95eQZyfsy-TW? zcwrmX7Lf0gk_~)6Uy4xjCQw2%9g@>Y<5i_nRR*YLN#1OL{IAmRI&^VNYM{Q#+ocjE zk^Lvh{xfe@NL3|YR9-5Tm(k9c__lGdI-|H-ih*(dBa;6p@09+ll+sRavE)KD^#Q3@ z5nSIX^|y0qlX`~b`@Q&pXVtf*>N~*fVv$RD_K?&+Odns9N{v%AER_amr|3VV=qrr* za>?Ol_CHAWKQiZQCF?p~y;Ukd$oB=JK10J|X@FRAE|DAseZ{w>g2pSpDHY#>H9ju| zU*K->kEQs(dFfiop@G5yDZG=rRWC@@i!kfYqz;VMj$jPZ$zLQ3p7(t~e7Dem4`yQk zR(aI@Lh63Wht7Z~e^|;7z;{2ym}JN+rAT#PZKKrsRRiSRC3)K!;9sQy{?6OR4epi< zOUVcWJRudY(aodcdki4_6uRQspp>YD$$nI_xm(*UwSYML5pK}Uc~U-&FDAtYQ8*o4 zIVqKD<(rW)+^ zJ|Yz#<-6IEJ%`o`Zj=J_N&TqQkELZs_AbfZ&4*9pUC@866vLKzt&-Qq7loZt2pRgG z#&F`pCAcq8>|*SBUj2v^(|Ez7QUJ&cqqr>~_)^JNd7HOX@}S20xYVmq&XvkMfOAUZ zG!JXODK*eo!>BYc4&VEU+3?POsZ{^G=-W~R9acu9l4%uvU5dbqQ4;#42CEpsi&FY& zW^k9}Zs)H2OawagMF{UOlCMbNSJO8OFOkAa8PBIB?m)x) z&p|0x9Z~QHDZoNn$Y-G+$q#O)aEt4t*j08nOG&?C3a8A|<$%52<*Ng84 z$akZZZQ}co)P(7BnG`H%tO+Sj@?q9TBn#Ro9+6@sL-CLl4>Q-7r1oW=Es(4WY5U(q zm`CoDlKT{+`KD9@)`lNQ!+(PHcS(`DK$QhjiKH?fEmz-?%5QV{Dl(5lp;Y>4#s+!o zi=@67AYUQ%i|J_yAC~V^UfOr1;(K(}DY+1H#doCQyA1r0)IbUn7HMKq9~a*znD}(5 z%Hqwa`M1gW&9r)()N`oGCN4wck4xyJX$XNWUxP46)%?((r3OEPhamAENQsr0_Ek zOR1EULBnrK-dj9-h-eYi^%E)mDTl36I>5kxFIDt({%_>`-|~I+KB?ZHhJVg6$$6Z{ zeLsG_2ebtzLG`>P+T+5Y>3s-+Ys&8R5MfiZg z_7$mll@D%}vJZ0ji`Aei+^}wfN#87am>2+G zd_{7RMUE^hMx+9EkS9f+V#I0{^SN>bjh3D#rPCPB87co9{8%D6rLfieq~QGk`Il0` z%SCHF6T?_0;N+ICL^GjZUWRU)gw#{Wq5Pq_IxDgHc%_md)^ zi=$G+cMj8euSwo#X!HG2%d`BaiLTI7{v64l3yHiY^*qe}sAS*9_b*E^5SI6efc}O* zNW&j_bH3z*w)&G&e+pvwz0|?+^8G_yoHV}siZpzcQM@d|VCr9# z`cDJrg^~*{s(PdfQgA7|;%`eaJ!JRe<-yuGDRT@q}b#tX`9)}z$%cbq&_ek-3`QkI!S{yziMQA9O zcgx)*xtn>%_XUFDG@d0@*}QWjwkbD%N}L-o91%GRxqeH^VX#yH{FL}qBou!`ioeN+ z2c?Pu7=w!umq>0YbHo%b;+^yVEa(3(4OpkTXiSQ>@$h*mcmeV|A~iJbT-xGKNpU|A z>y!!Fgp$00e}l7?;_r*lUyjY=60!B$Cb5BYd2Ldq&>e4fmh&xgyU_-cl@Qc6|e6v2LRDp!Ys7*h|Dl9(o89x#fZaF+Qj5mNev8F_!%h# zkA-`s5TY)M6Z>GOXC(V`I=LSqj~VMVQm}$ntyOUTEpk4VTuIO5tC zA@yHL->i>FJ^WPCAtlOsD`kdyUlmVF#WPIc!;=3Ia5f@!s;X`jfdic5Y5Zwk&Ha|- z!UDd4_<~&7G^L5OcyfWr1vzwek(6BwtR9wv1Kj+mTyPsm{+{H0pJ&ws9BIb)4e`M< z1%H+T*uwb{GA=TKAUZ6SNBH78$%E$|TNq=P4~uV-;+uKrJgJ<8N>kRI4A{5O3 zYN=D|?vb)yF6&Q8JvN*3BJw9B|5*B_KJJ$4dl>2cQv87S{EjsI zf>u8&b+>W#b8c{$kOrD5yN{qPU(A+jb<%1}rM8TAZ0x1Bgc~5>ZmFWV@shA#WHl>LV0zJvWr zbJnnP;KIR?RusLW84Ja4Y#&Er`1E-7nddY4NjSF%myE{-m$RXIfI3m|=6s^8$Q z!2+LLCuI;*NgTz*-Sgiq=QF{a???`V&wWX9Uj|OrkEy>z>Mx};wYYgTZ-(Suz{6cq zu$xi;KpF;6LAG;)CE^dNXgWW*Z6+x%(;{=JipxUes`U<_S$Xjw)R?U--D>^1=SaW z-LL4kP{U^wK8p}c6EUW*DEcZZ`8K8JQ0`_Z2XtYQ9Fw1WkKB8a>TH#71uMxdL#_W_ zbq<5X;1+#N(Jqwt6UiJP(Lst1Mo{Oe?|eXFFLGa$YdcNsssl7pMSNbh;b7AsQ16~9a`IHSRCTD8`x#Y-Sw-2Clsy?(AEx^DJ&zgl z;z+#lmg;RTPl+Fm_4Fe(ERa;i<5fH%A+H5YptcH~wcO=9RsJPnzD^kyq5B!R!^oQX zDOW0_;h{Ri%1n4yx%U8PDt8uW-)9jd9kei*IKA)*H-Mzjb%2Jyr|kPNhck#Uk9A4* zwLyQ9B&Ngl3jdql9ijXL;|XSSX9dP~_kjW!)@6#AoBmAswnYVhz~O_$mZ=JLK-Eqz zd;YQVanV|Z%T#|A*qEip4Z!qEO0#_WmaA_CXyV>)tWx9eRuv++KrQ}NVf=ZSTD?Hz z-jMdF^=(z(uJ;+drr>q^z|*i`b-MsSn6~5Y)Ukp!Hc?XMw4ml-e1|O;b4C(Bz_5e?;~9%q?@3 z7T;l4m)iinK&cBs zTc1;ly=K6e<(@0|hY0i&JS(JTEHcP4O_e*1GXJjdEkrX%wYgCHzNx-L00-g7Vj54B zH;L+d(E;uOa_wNR&s5z8I5kqKFBrU6DT{38({IaX6D{nZ!e=eT;(LJgQ*e=6dUJ-F ztm(wa?wp67Z5i!{+D6D53G91Xeb2!3@5+3QER(T%LQTz73T-b|#EiQ!P7U*;#9oM` zgkX$KCidS?4}2mtvhA_GP+0R79s*c zYgc0jhB`-Ob~HC7*O{yKwrbmKW#;!Bx#@$HM)t9FttXhoiID^vIWNdroOHOpzv`$O z?$71kNC}yju&@B#NpdI0Wma0M*pzP%S9`}eQ%p`=-0n7Vw`GZLuc`$Ul_#i-NXp|? zJ`B`*Mcxu%5=53bHmW~XHGYGRn3P=v+fsSUV2cCf;?iTodi)g}sDR@o*hhiwu;CF3 zCjbsrI3D4BUlj`t$kvr*`etj&qWONx4-&L+rer9Mkr8=O(M!o^R#65aoW{8rmqNwE z6l_mT%T-wslX`zBXuN8NZ9s`lxa(0q?GqVort;?NvoPqxRpQ)sjwO0_{ge&A>E~CJ zbVxlU}aM72xT~O5572T&xN! zsJ2?QHO3c5DF95fu;i(#u$2Ti5g^5UScQ3s#D~?in^SX@nxOI36Er(m*&&SJU2^XR z&5cmb)_mo3Rn7piAe?!?@N){yh?ZH1I!>?aYBxYrH!H=0ioU7n5YXl(Y7QdxA+>)` z^9Ex)h8k_Bh~*zXrx5+SF-DEC#@o}?iJI!`15GS2)qPammn~wj>XtPQ1E7&>lzp4V z*&Pt7H$>hRw9$f}L2JWRGjR^sHuFa-Z&s1)LS;=m99WISepk0ncDrEqF;0_x5yZ^un|ufqEPrz<>z zmW@zrB(3k0xp!mR2R!LMr9q=Hir8u6EemRPYh|}#Rs5L9TPDI91!go(EDHXI^0|*C zl@%{l(fV+((%*!~tH`U;+@6A+8o{XoweJ-5oyxF$tolDdGgEPS0?P%Ji_C)alsez? z4wuJ@^A^c_5;XM#rOstG6xHUw(hW^F2jzm2CaBH16jc;e;cW(LGSQo})V#s6u2A?lba`^kZip$uW*#Y(Z(GgvIycB78-c#*J}NS%Jx!bZUyzSx5{z}%%>#$FOFh|8vU1|9|2Rh zD#c~G^Idhm2WG)QQ2kZ%X?W+S>Rb(&rjF_L{ z4W7nbYTQjhBUBlQ08G;W<98l)4pq1n#NO)@?<{#!$k7~5W(Iw!TFa2aw{eR=P3^AK z9>{%jbp#qbuHXq~)!WLv0~*y7agIe*MLxVaE>Q6FDd424J*?UzJvE99FQOwek&|~O z!88TaVR==xRsIyQG+pc@QToZHd zapj%>mZ}&eK~GmMK03*R1GkMno zW9Rt#is8n;8I>=o@a2spQdAs$xGsr~q&T}Md!;g~*3s>Yv?YYmtWRX1mMGkS1Y2;4 z0?d*@O98W}cA{#WPla7nSYM}|tL|WRhtRuOYTeK)zw4@-UBCQ|eItkE1e*VI5^~){ zxj_R7NPn!{aRaEezcflE+l))!z&^JwVc-jiAE)Z^WIT_NTSs*cku!?fH(Jdx36)tI zYkVPYNX*o~rI?KtC-%Lyb4fy9LzUSuO{tbFG}~KuA7 z#KD{%s`OT%19$EE3~XQE{)_TC^#*MI**%mcbKxBo-X*m$Q;nZ8`u5fmw6LWLLxIsY z*gApUNDdH&*Fp|KoratyQdpt#-$4D}%71`{yh`)~X!-`Fe-8B;G$YX1pMWsleWEl+#q<5YDeueihW@sbTsArB4J6A_Z;gds}5Y>ATmfizzyDfif2Y zu2IJ731=z1fz7)YUf@rW{~f5c4^;b*+84=v5;TcjY|l~~-o|*Mu%PA-QGOIK4*CGL zk5}7OM~w0+s9Z`Yu(`h#JY0m)f(cJ%_~hmj4a144htx^Dz_R#(^BG`gHI#HNOqo zI!Y~ewVsI|8U04VT~u4(?n`QAPgTASa8yZyCQ(JshjKmwbvtsq2XqVQg^ftqq+za9z3E8}j@=vPsjvTH9&TDdB z2W>s0*0WS(?>9k{@UHB9WleIK1C&9xuPjjIG3ray#lp|Is!<=m^I&qXlzSERnbj4v z^N~6qQ{Pj)$CAzhIppo^p$^lzb_H%sm}$>tG1R|NGA zmxot2+f}yTQq4cX1Ugj>+jx=zY(B51=?K}DvM6Njm1^5+Y7SC!Q>3x8s%%I3jPg0C zrOQ;hoFcALgZ{c($=w=iI9uVZ^tWevh-NDStF2UR73E!^HVdwPuj==~8jV!MrclhN z=u*I@ayNsTJa4HTLAU``C(*ceOWG-(qyrxw^n)^ zN>ASSdB@8;fnnj7TSFX{PR{1-YTkjQf2;BX^yp+<>l9!uR=e|+DN_F}< z@OCcop?027XA#Z#3(i5Z6pJdNFhuVvdJkTEISIB}5#}K04LNU8+~XLz;moO+CkG|h zXi)hSl}}}q?0E;&^06vUB!t! zs>SZnx>BvH$dbRFe-1$7kKb*2rb|%`B-EOx*6mQkD~UXz_+IpCuFGpLS}WE2NX)E3yP>>C)m#A2LkdtkE2DWa zK$-{|Z8ef!(RQ}O?DezC+>8;>ipq{^r{9Qq-gNVFl1ou;Uf6z9+tkljO>f8w$ z9I4u$T<%+<{ZmO6;wD?^WzXxpo3dhO%8g%?kj~`W=g&nIY zy=3aRTK(6Mr#@PB8|>KB3k+{pcn3_>p2DyROrNOqNyvDS@=qFig6Vo|e;AnqR6dYO q4p;j>EMH<`j32Hcvc2Vf1L6|Q^J_CDAISCV>g+|O_u$SLNc}&}ZZmfP literal 0 HcmV?d00001 diff --git a/helm/ocaml/cic_disambiguation/macros/dictionary-tex.xml b/helm/ocaml/cic_disambiguation/macros/dictionary-tex.xml new file mode 100644 index 000000000..47995454f --- /dev/null +++ b/helm/ocaml/cic_disambiguation/macros/dictionary-tex.xml @@ -0,0 +1,378 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/ocaml/cic_disambiguation/macros/entities-table.xml b/helm/ocaml/cic_disambiguation/macros/entities-table.xml new file mode 100644 index 000000000..ca0bdabcf --- /dev/null +++ b/helm/ocaml/cic_disambiguation/macros/entities-table.xml @@ -0,0 +1,2081 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/ocaml/cic_disambiguation/macros/extra-entities.xml b/helm/ocaml/cic_disambiguation/macros/extra-entities.xml new file mode 100644 index 000000000..991c2d84b --- /dev/null +++ b/helm/ocaml/cic_disambiguation/macros/extra-entities.xml @@ -0,0 +1,5 @@ + + + + + diff --git a/helm/ocaml/cic_disambiguation/make_table.ml b/helm/ocaml/cic_disambiguation/make_table.ml new file mode 100644 index 000000000..770fe2b05 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/make_table.ml @@ -0,0 +1,88 @@ + +open Printf +open Pxp_types +open Pxp_ev_parser + +(* Usage: make_table *) + +let debug = false +let debug_print s = if debug then prerr_endline s + +let tables = [ +(* + `Entities, "/usr/share/gtkmathview/entities-table.xml"; + `Dictionary, "/usr/share/editex/dictionary-tex.xml" +*) + `Entities, "macros/entities-table.xml"; + `Dictionary, "macros/dictionary-tex.xml"; + `Entities, "macros/extra-entities.xml"; +] + +let macro2utf8 = Hashtbl.create 2000 +let utf82macro = Hashtbl.create 2000 + +let add_macro macro utf8 = + debug_print (sprintf "Adding macro %s = '%s'" macro utf8); + Hashtbl.add macro2utf8 macro utf8; + Hashtbl.add utf82macro utf8 macro + +let rec find_first_tag pull_parser = + match pull_parser () with + | Some (E_start_tag _ as e) -> e + | None -> assert false + | _ -> find_first_tag pull_parser + +let iter_entities_file f pull_parser = + ignore (find_first_tag pull_parser); (* *) + let rec aux () = + match pull_parser () with + | Some (E_start_tag ("entity", attrs, _)) -> + (try + let name = List.assoc "name" attrs in + let value = List.assoc "value" attrs in + f name value + with Not_found -> ()); + aux () + | None -> () + | _ -> aux () + in + aux () + +let iter_dictionary_file f pull_parser = + ignore (find_first_tag pull_parser); (* *) + let rec aux () = + match pull_parser () with + | Some (E_start_tag ("entry", attrs, _)) -> + (try + let name = List.assoc "name" attrs in + let value = List.assoc "val" attrs in + f name value + with Not_found -> ()); + aux () + | None -> () + | _ -> aux () + in + aux () + +let fill_table () = + List.iter + (fun (typ, fname) -> + let entry = `Entry_document [ `Extend_dtd_fully; `Parse_xml_decl ] in + let config = { default_config with encoding = `Enc_utf8 } in + let entity_manager = + create_entity_manager ~is_document:true config (from_file fname) + in + let pull_parser = create_pull_parser config entry entity_manager in + match typ with + | `Entities -> iter_entities_file add_macro pull_parser + | `Dictionary -> iter_dictionary_file add_macro pull_parser) + tables + +let main () = + let oc = open_out Sys.argv.(1) in + fill_table (); + Marshal.to_channel oc (macro2utf8, utf82macro) []; + close_out oc + +let _ = main () + diff --git a/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml b/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml new file mode 100644 index 000000000..044f8ae02 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml @@ -0,0 +1,36 @@ + +let debug = false +let debug_print = if debug then prerr_endline else ignore + +let loc = (0, 0) + +let expand_unicode_macro macro = + debug_print (Printf.sprintf "Expanding macro '%s' ..." macro); + let expansion = Macro.expand macro in + <:expr< $str:expansion$ >> + +let _ = + Quotation.add "unicode" + (Quotation.ExAst (expand_unicode_macro, (fun _ -> assert false))) + +open Pa_extend + +EXTEND + symbol: FIRST + [ + [ x = UIDENT; q = QUOTATION -> + let (quotation, arg) = + let pos = String.index q ':' in + (String.sub q 0 pos, + String.sub q (pos + 1) (String.length q - pos - 1)) + in + debug_print (Printf.sprintf "QUOTATION = %s; ARG = %s" quotation arg); + if quotation = "unicode" then + let text = TXtok (loc, x, expand_unicode_macro arg) in + {used = []; text = text; styp = STlid (loc, "string")} + else + assert false + ] + ]; +END + diff --git a/helm/ocaml/cic_disambiguation/parser.ml b/helm/ocaml/cic_disambiguation/parser.ml new file mode 100644 index 000000000..0ee41ab2a --- /dev/null +++ b/helm/ocaml/cic_disambiguation/parser.ml @@ -0,0 +1,102 @@ + +open Ast + +let grammar = Grammar.gcreate Lexer.lex + +let term = Grammar.Entry.create grammar "term" +(* let tactic = Grammar.Entry.create grammar "tactic" *) +(* let tactical = Grammar.Entry.create grammar "tactical" *) + +let return_term loc term = LocatedTerm (loc, term) + +EXTEND + GLOBAL: term; + meta_subst: [ + [ s = SYMBOL "_" -> None + | t = term -> Some t ] + ]; + binder: [ + [ SYMBOL <:unicode> (* λ *) -> `Lambda + | SYMBOL <:unicode> (* π *) -> `Pi + | SYMBOL <:unicode> (* ∃ *) -> `Exists + | SYMBOL <:unicode> (* ∀ *) -> `Forall + ] + ]; + substituted_name: [ (* a subs.name is an explicit substitution subject *) + [ s = [ IDENT | SYMBOL ]; + subst = OPT [ + SYMBOL "\subst"; (* to avoid catching frequent "a [1]" cases *) + LPAREN "["; + substs = LIST1 [ + i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) + ] SEP SYMBOL ";"; + RPAREN "]" -> + substs + ] -> + (match subst with + | Some l -> Ident (s, l) + | None -> Ident (s, [])) + ] + ]; + name: [ (* as substituted_name with no explicit substitution *) + [ s = [ IDENT | SYMBOL ] -> s ] + ]; + pattern: [ + [ n = name -> [n] + | LPAREN "("; names = LIST1 name; RPAREN ")" -> names ] + ]; + term: + [ "add" LEFTA [ (* nothing here by default *) ] + | "mult" LEFTA [ (* nothing here by default *) ] + | "inv" NONA [ (* nothing here by default *) ] + | "simple" NONA + [ + b = binder; vars = LIST1 IDENT SEP SYMBOL ","; + typ = OPT [ SYMBOL ":"; t = term -> t ]; + SYMBOL "."; body = term -> + let binder = + List.fold_right (fun var body -> Binder (b, var, typ, body)) + vars body + in + return_term loc binder + | n = substituted_name -> return_term loc n + | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" -> + return_term loc (Appl (head :: args)) + | i = INT -> return_term loc (Int (int_of_string i)) + | m = META; + substs = [ + LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" -> + substs + ] -> + return_term loc (Meta (m, substs)) + (* actually "in" and "and" are _not_ keywords. Parsing works anyway + * since applications are required to be bound by parens *) + | "let"; name = IDENT; SYMBOL <:unicode> (* ≝ *); t1 = term; + IDENT "in"; t2 = term -> + return_term loc (LetIn (name, t1, t2)) + | "let"; "rec"; defs = LIST1 [ + name = IDENT; + index = OPT [ LPAREN "("; index = INT; RPAREN ")" -> + int_of_string index + ]; + typ = OPT [ SYMBOL ":"; typ = term -> typ ]; + SYMBOL <:unicode> (* ≝ *); t1 = term -> + (name, t1, typ, (match index with None -> 1 | Some i -> i)) + ] SEP (IDENT "and"); + IDENT "in"; body = term -> + return_term loc (LetRec (defs, body)) + | typ = OPT [ LPAREN "["; typ = term; RPAREN "]" -> typ ]; + "match"; t = term; "with"; + LPAREN "["; + patterns = LIST0 [ + p = pattern; SYMBOL <:unicode> (* ⇒*); t = term -> (p, t) + ] SEP SYMBOL "|"; + RPAREN "]" -> + return_term loc (Case (t, typ, patterns)) + | LPAREN "("; t = term; RPAREN ")" -> return_term loc t + ] + ]; +END + +let parse_term = Grammar.Entry.parse term + diff --git a/helm/ocaml/cic_disambiguation/pp.ml b/helm/ocaml/cic_disambiguation/pp.ml new file mode 100644 index 000000000..6ee9cf39a --- /dev/null +++ b/helm/ocaml/cic_disambiguation/pp.ml @@ -0,0 +1,56 @@ + +open Ast +open Printf + +let pp_binder = function + | `Lambda -> "lambda" + | `Pi -> "pi" + | `Exists -> "exists" + | `Forall -> "forall" + +let rec pp_term = function + | LocatedTerm ((p_begin, p_end), term) -> + sprintf "[%d,%d]%s" p_begin p_end (pp_term term) + + | Appl terms -> sprintf "(%s)" (String.concat " " (List.map pp_term terms)) + | Binder (kind, var, typ, body) -> + sprintf "\\%s %s%s.%s" (pp_binder kind) var + (match typ with None -> "" | Some typ -> ": " ^ pp_term typ) + (pp_term body) + | Case (term, typ, patterns) -> + sprintf "%smatch %s with %s" + (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t)) + (pp_term term) (pp_patterns patterns) + | LetIn (name, t1, t2) -> + sprintf "let %s = %s in %s" name (pp_term t1) (pp_term t2) + | LetRec (definitions, term) -> + sprintf "let rec %s in %s" + (String.concat " and " + (List.map + (fun (name, body, typ, index) -> + sprintf "%s%s = %s" name + (match typ with None -> "" | Some typ -> ": " ^ pp_term typ) + (pp_term body)) + definitions)) + (pp_term term) + | Ident (name, []) -> name + | Ident (name, substs) -> sprintf "%s[%s]" name (pp_substs substs) + | Meta (name, substs) -> + sprintf "%s[%s]" name + (String.concat "; " + (List.map (function None -> "_" | Some term -> pp_term term) substs)) + | Int num -> string_of_int num + +and pp_subst (name, term) = sprintf "%s := %s" name (pp_term term) +and pp_substs substs = String.concat "; " (List.map pp_subst substs) + +and pp_pattern (names, term) = + sprintf "%s -> %s" + (match names with + | [n] -> n + | names -> "(" ^ String.concat " " names ^ ")") + (pp_term term) + +and pp_patterns patterns = + sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns)) + diff --git a/helm/ocaml/cic_disambiguation/pp.mli b/helm/ocaml/cic_disambiguation/pp.mli new file mode 100644 index 000000000..078517c56 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/pp.mli @@ -0,0 +1 @@ +val pp_term: Ast.term -> string diff --git a/helm/ocaml/cic_disambiguation/test_lexer.ml b/helm/ocaml/cic_disambiguation/test_lexer.ml new file mode 100644 index 000000000..8667953c3 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/test_lexer.ml @@ -0,0 +1,11 @@ +let ic = open_in Sys.argv.(1) in +let token_stream = fst (Lexer.lex.Token.tok_func (Stream.of_channel ic)) in +let rec dump () = + let (a,b) = Stream.next token_stream in + if a = "EOI" then raise Stream.Failure; + print_endline (Printf.sprintf "%s '%s'" a b); + dump () +in +try + dump () +with Stream.Failure -> () diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml new file mode 100644 index 000000000..41634cbb3 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/test_parser.ml @@ -0,0 +1,13 @@ +try + let ic = open_in Sys.argv.(1) in + let term = Parser.parse_term (Stream.of_channel ic) in + close_in ic; + print_endline (Pp.pp_term term) +with Stdpp.Exc_located ((p_start, p_end), exn) -> + prerr_endline (Printf.sprintf "Exception at character %d-%d: %s" + p_start p_end (Printexc.to_string exn)) + +(* print_endline (Macro.expand "def") *) + +(* Printf.printf "'%s'\n" (Macro.expand Sys.argv.(1)) *) + -- 2.39.2