From 6459acbd4bb69475cfaa0b37a9771ced94193667 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Sat, 24 Jan 2004 16:59:45 +0000 Subject: [PATCH] - factorized DisambiguateChoices module - implemented alias language for gTopLevel --- helm/ocaml/cic_disambiguation/.depend | 23 +++--- helm/ocaml/cic_disambiguation/Makefile | 19 ++--- .../ocaml/cic_disambiguation/arit_notation.ml | 12 +-- .../cic_disambiguation/cicTextualLexer2.ml | 12 ++- .../cic_disambiguation/cicTextualLexer2.mli | 2 +- .../cic_disambiguation/cicTextualParser2.ml | 76 ++++++++++++++++++- .../cic_disambiguation/cicTextualParser2.mli | 20 +++-- helm/ocaml/cic_disambiguation/disambiguate.ml | 22 +----- .../ocaml/cic_disambiguation/disambiguate.mli | 12 --- .../cic_disambiguation/disambiguateChoices.ml | 65 ++++++++++++++++ .../disambiguateChoices.mli | 58 ++++++++++++++ .../cic_disambiguation/disambiguateTypes.ml | 44 ----------- .../cic_disambiguation/disambiguateTypes.mli | 10 --- .../cic_disambiguation/logic_notation.ml | 4 +- helm/ocaml/cic_disambiguation/test_lexer.ml | 2 +- helm/ocaml/cic_disambiguation/test_parser.ml | 41 +++++++--- 16 files changed, 287 insertions(+), 135 deletions(-) create mode 100644 helm/ocaml/cic_disambiguation/disambiguateChoices.ml create mode 100644 helm/ocaml/cic_disambiguation/disambiguateChoices.mli diff --git a/helm/ocaml/cic_disambiguation/.depend b/helm/ocaml/cic_disambiguation/.depend index 0342a9b11..1f34686b2 100644 --- a/helm/ocaml/cic_disambiguation/.depend +++ b/helm/ocaml/cic_disambiguation/.depend @@ -1,8 +1,11 @@ +disambiguateChoices.cmi: disambiguateTypes.cmi cicTextualParser2Pp.cmi: cicTextualParser2Ast.cmi +cicTextualParser2.cmi: cicTextualParser2Ast.cmi disambiguateTypes.cmi disambiguate.cmi: cicTextualParser2Ast.cmi disambiguateTypes.cmi -cicTextualParser2.cmi: cicTextualParser2Ast.cmi disambiguateTypes.cmo: disambiguateTypes.cmi disambiguateTypes.cmx: disambiguateTypes.cmi +disambiguateChoices.cmo: disambiguateTypes.cmi disambiguateChoices.cmi +disambiguateChoices.cmx: disambiguateTypes.cmx disambiguateChoices.cmi cicTextualParser2Pp.cmo: cicTextualParser2Ast.cmi cicTextualParser2Pp.cmi cicTextualParser2Pp.cmx: cicTextualParser2Ast.cmi cicTextualParser2Pp.cmi macro.cmo: macro.cmi @@ -10,18 +13,20 @@ macro.cmx: macro.cmi cicTextualLexer2.cmo: macro.cmi cicTextualLexer2.cmi cicTextualLexer2.cmx: macro.cmx cicTextualLexer2.cmi cicTextualParser2.cmo: cicTextualLexer2.cmi cicTextualParser2Ast.cmi \ - cicTextualParser2.cmi + disambiguateChoices.cmi disambiguateTypes.cmi cicTextualParser2.cmi cicTextualParser2.cmx: cicTextualLexer2.cmx cicTextualParser2Ast.cmi \ - cicTextualParser2.cmi + disambiguateChoices.cmx disambiguateTypes.cmx cicTextualParser2.cmi disambiguate.cmo: cicTextualParser2.cmi cicTextualParser2Ast.cmi \ - disambiguateTypes.cmi disambiguate.cmi + disambiguateChoices.cmi disambiguateTypes.cmi disambiguate.cmi disambiguate.cmx: cicTextualParser2.cmx cicTextualParser2Ast.cmi \ - disambiguateTypes.cmx disambiguate.cmi + disambiguateChoices.cmx disambiguateTypes.cmx disambiguate.cmi logic_notation.cmo: cicTextualParser2.cmi cicTextualParser2Ast.cmi \ - disambiguate.cmi + disambiguateChoices.cmi logic_notation.cmx: cicTextualParser2.cmx cicTextualParser2Ast.cmi \ - disambiguate.cmx + disambiguateChoices.cmx arit_notation.cmo: cicTextualParser2.cmi cicTextualParser2Ast.cmi \ - disambiguate.cmi + disambiguateChoices.cmi arit_notation.cmx: cicTextualParser2.cmx cicTextualParser2Ast.cmi \ - disambiguate.cmx + disambiguateChoices.cmx +tex_notation.cmo: cicTextualParser2.cmi +tex_notation.cmx: cicTextualParser2.cmx diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile index 9652369b4..cadca9413 100644 --- a/helm/ocaml/cic_disambiguation/Makefile +++ b/helm/ocaml/cic_disambiguation/Makefile @@ -1,25 +1,18 @@ PACKAGE = cic_textual_parser2 -REQUIRES = \ - ulex pxp helm-tactics helm-cic helm-logger helm-cic_unification \ - camlp4.gramlib +REQUIRES = ulex pxp helm-tactics helm-logger helm-cic_unification camlp4.gramlib NOTATIONS = logic arit tex INTERFACE_FILES = \ - cicTextualParser2Ast.mli \ + disambiguateTypes.mli \ + disambiguateChoices.mli \ cicTextualParser2Pp.mli \ macro.mli \ cicTextualLexer2.mli \ - disambiguate.mli \ cicTextualParser2.mli \ - disambiguateTypes.mli + disambiguate.mli IMPLEMENTATION_FILES = \ - disambiguateTypes.ml \ - cicTextualParser2Pp.ml \ - macro.ml \ - cicTextualLexer2.ml \ - cicTextualParser2.ml \ - disambiguate.ml \ - $(patsubst %,%_notation.ml,$(NOTATIONS)) \ + $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ + $(patsubst %,%_notation.ml,$(NOTATIONS)) ULEXDIR := $(shell ocamlfind query ulex) diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml index f0f8d52bc..e4c700d0a 100644 --- a/helm/ocaml/cic_disambiguation/arit_notation.ml +++ b/helm/ocaml/cic_disambiguation/arit_notation.ml @@ -57,28 +57,28 @@ EXTEND END let _ = - Disambiguate.add_num_choice + DisambiguateChoices.add_num_choice ("natural number", (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num))); - Disambiguate.add_num_choice + DisambiguateChoices.add_num_choice ("real number", (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num))); - Disambiguate.add_symbol_choice "plus" + DisambiguateChoices.add_symbol_choice "plus" ("natural plus", (fun env _ args -> let t1, t2 = match args with | [t1; t2] -> t1, t2 - | _ -> raise Disambiguate.Invalid_choice + | _ -> raise DisambiguateChoices.Invalid_choice in Cic.Appl [ HelmLibraryObjects.Peano.plus; t1; t2 ])); - Disambiguate.add_symbol_choice "plus" + DisambiguateChoices.add_symbol_choice "plus" ("real plus", (fun env _ args -> let t1, t2 = match args with | [t1; t2] -> t1, t2 - | _ -> raise Disambiguate.Invalid_choice + | _ -> raise DisambiguateChoices.Invalid_choice in Cic.Appl [ HelmLibraryObjects.Reals.rplus; t1; t2 ])); diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index 21f020520..b339b8dc4 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -41,6 +41,10 @@ let regexp ident = (alpha ident_cont*) | ('_' ident_cont+) let regexp ident' = ((alpha | tex_token) ident_cont'*) | ('_' ident_cont'+) let regexp paren = [ '(' '[' '{' ')' ']' '}' ] let regexp meta = '?' num +let regexp qstring = '"' [^ '"']* '"' +let regexp uri = + (* schema *) (* path *) (* ext *) (* xpointer *) + ("cic:/" | "theory:/") ident ('/' ident)* ('.' ident)+ ('#' num ('/' num)*)? (* let regexp catchall = .* *) let keywords = Hashtbl.create 17 @@ -86,6 +90,7 @@ and token = lexer *) let rec token = lexer | blanks -> token lexbuf + | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf) | ident -> let lexeme = Ulexing.utf8_lexeme lexbuf in (try @@ -94,6 +99,10 @@ let rec token = lexer | num -> return lexbuf ("NUM", Ulexing.utf8_lexeme lexbuf) | paren -> return lexbuf ("PAREN", Ulexing.utf8_lexeme lexbuf) | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf) + | qstring -> + let lexeme = Ulexing.utf8_lexeme lexbuf in + let s = String.sub lexeme 1 (String.length lexeme - 2) in + return lexbuf ("QSTRING", s) | symbol -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) | tex_token -> let macro = @@ -116,7 +125,7 @@ let tok_func stream = | Ulexing.Error -> error_at_end lexbuf "Unexpected character" | Ulexing.InvalidCodepoint i -> error_at_end lexbuf "Invalid code point") -let lex = +let cic_lexer = { Token.tok_func = tok_func; Token.tok_using = (fun _ -> ()); @@ -125,3 +134,4 @@ let lex = Token.tok_text = Token.lexer_text; Token.tok_comm = None; } + diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli b/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli index f4cbaa1cb..85ff08bce 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli @@ -25,5 +25,5 @@ exception Error of int * int * string -val lex : (string * string) Token.glexer +val cic_lexer : (string * string) Token.glexer diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 030fa5938..bca1cdba6 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -35,7 +35,11 @@ open Printf exception Parse_error of string -let grammar = Grammar.gcreate CicTextualLexer2.lex +let choice_of_uri (uri: string) = + let cic = HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) in + (uri, (fun _ _ _ -> cic)) + +let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer let term = Grammar.Entry.create grammar "term" let term0 = Grammar.Entry.create grammar "term0" @@ -176,3 +180,73 @@ let parse_term stream = raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y (Printexc.to_string exn))) +(**/**) + +(** {2 Interface for gTopLevel} *) + +open DisambiguateTypes + +module EnvironmentP3 = + struct + type t = environment + + let empty = "" + + let aliases_grammar = Grammar.gcreate CicTextualLexer2.cic_lexer + let aliases = Grammar.Entry.create aliases_grammar "aliases" + + let to_string env = + let aliases = + Environment.fold + (fun domain_item (dsc, _) acc -> + let s = + match domain_item with + | Id id -> sprintf "alias id %s = %s" id dsc + | Symbol (symb, instance) -> + sprintf "alias symbol \"%s\" (instance %d) = \"%s\"" + symb instance dsc + | Num instance -> + sprintf "alias num (instance %d) = \"%s\"" instance dsc + in + s :: acc) + env [] + in + String.concat "\n" (List.sort compare aliases) + + EXTEND + GLOBAL: aliases; + aliases: [ (* build an environment from an aliases list *) + [ aliases = LIST0 alias; EOI -> + List.fold_left + (fun env (domain_item, codomain_item) -> + Environment.add domain_item codomain_item env) + Environment.empty aliases + ] + ]; + alias: [ (* return a pair from an alias *) + [ IDENT "alias"; + choice = + [ IDENT "id"; id = IDENT; SYMBOL "="; uri = URI -> + (Id id, choice_of_uri uri) + | IDENT "symbol"; symbol = QSTRING; + PAREN "("; IDENT "instance"; instance = NUM; PAREN ")"; + SYMBOL "="; dsc = QSTRING -> + (Symbol (symbol, int_of_string instance), + DisambiguateChoices.lookup_symbol_by_dsc symbol dsc) + | IDENT "num"; + PAREN "("; IDENT "instance"; instance = NUM; PAREN ")"; + SYMBOL "="; dsc = QSTRING -> + (Num (int_of_string instance), + DisambiguateChoices.lookup_num_by_dsc dsc) + ] -> choice ] + ]; + END + + let of_string s = + try + Grammar.Entry.parse aliases (Stream.of_string s) + with Stdpp.Exc_located ((x, y), exn) -> + raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y + (Printexc.to_string exn))) + end + diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli index a2b225143..0f13d116a 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -31,11 +31,8 @@ val parse_term: char Stream.t -> CicTextualParser2Ast.term (** {2 Grammar extensions} *) - (** recursive rule *) -val term: CicTextualParser2Ast.term Grammar.Entry.e - - (** top level rule *) -val term0: CicTextualParser2Ast.term Grammar.Entry.e +val term: CicTextualParser2Ast.term Grammar.Entry.e (** recursive rule *) +val term0: CicTextualParser2Ast.term Grammar.Entry.e (** top level rule *) val return_term: CicTextualParser2Ast.location -> CicTextualParser2Ast.term -> @@ -44,3 +41,16 @@ val return_term: (** raise a parse error *) val fail: CicTextualParser2Ast.location -> string -> 'a +(**/**) + +(** {2 Interface for gTopLevel} *) + +module EnvironmentP3: + (* environment parser/pretty-printer *) + sig + type t = DisambiguateTypes.environment + val empty : string + val to_string : t -> string + val of_string : string -> t + end + diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index e64087cf6..786971fc1 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -28,7 +28,6 @@ open Printf open DisambiguateTypes open UriManager -exception Invalid_choice exception No_choices of domain_item exception NoWellTypedInterpretation @@ -43,18 +42,6 @@ let descr_of_domain_item = function | Symbol (s, _) -> s | Num i -> string_of_int i -let symbol_choices = Hashtbl.create 1023 -let num_choices = ref [] - -let add_symbol_choice symbol codomain_item = - let current_choices = - try - Hashtbl.find symbol_choices symbol - with Not_found -> [] - in - Hashtbl.replace symbol_choices symbol (codomain_item :: current_choices) -let add_num_choice choice = num_choices := choice :: !num_choices - type test_result = | Ok of Cic.term * Cic.metasenv | Ko @@ -128,7 +115,7 @@ let interpretate ~context ~env ast = match resolve env (Id indty_ident) () with | Cic.MutInd (uri, tyno, _) -> uri, tyno | Cic.Implicit -> raise Try_again - | _ -> raise Invalid_choice + | _ -> raise DisambiguateChoices.Invalid_choice in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) @@ -338,9 +325,8 @@ module Make (C: Callbacks) = let choices = choices_of_id mqi_handle id in Hashtbl.add id_choices id choices; choices) - | Symbol (symb, _) -> - (try Hashtbl.find symbol_choices symb with Not_found -> []) - | Num instance -> !num_choices + | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb + | Num instance -> DisambiguateChoices.lookup_num_choices () in if choices = [] then raise (No_choices item); choices @@ -361,7 +347,7 @@ module Make (C: Callbacks) = refine metasenv context cic_term with | Try_again -> Uncertain - | Invalid_choice -> Ko + | DisambiguateChoices.Invalid_choice -> Ko in (* (4) build all possible interpretations *) let rec aux current_env todo_dom = diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index cbc7a54ac..13d3adc6f 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -25,18 +25,6 @@ open DisambiguateTypes -(** {2 Choice registration interface} *) - - (** to be raised when a choice is invalid due to some given parameter (e.g. - * wrong number of Cic.term arguments received) *) -exception Invalid_choice - - (** register a new symbol choice *) -val add_symbol_choice: string -> codomain_item -> unit - - (** register a new number choice *) -val add_num_choice: codomain_item -> unit - (** {2 Disambiguation interface} *) exception NoWellTypedInterpretation diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml new file mode 100644 index 000000000..aa203f8be --- /dev/null +++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml @@ -0,0 +1,65 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +open DisambiguateTypes + +exception Invalid_choice +exception Choice_not_found of string + +let symbol_choices = Hashtbl.create 1023 +let num_choices = ref [] + +let add_symbol_choice symbol codomain_item = + let current_choices = + try + Hashtbl.find symbol_choices symbol + with Not_found -> [] + in + Hashtbl.replace symbol_choices symbol (codomain_item :: current_choices) + +let add_num_choice choice = num_choices := choice :: !num_choices + +let lookup_symbol_choices symbol = + try + Hashtbl.find symbol_choices symbol + with Not_found -> [] + +let lookup_num_choices () = !num_choices + +let has_description dsc = (fun x -> fst x = dsc) + +let lookup_symbol_by_dsc symb dsc = + try + List.find (has_description dsc) (Hashtbl.find symbol_choices symb) + with Not_found -> + raise (Choice_not_found (sprintf "Symbol %s, dsc %s" symb dsc)) + +let lookup_num_by_dsc dsc = + try + List.find (has_description dsc) !num_choices + with Not_found -> raise (Choice_not_found ("Num with dsc " ^ dsc)) + diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli new file mode 100644 index 000000000..3a6e92f55 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli @@ -0,0 +1,58 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open DisambiguateTypes + +(** {2 Choice registration interface} *) + + (** to be raised when a choice is invalid due to some given parameter (e.g. + * wrong number of Cic.term arguments received) *) +exception Invalid_choice + + (** raised by lookup_XXXX below *) +exception Choice_not_found of string + + (** register a new symbol choice *) +val add_symbol_choice: string -> codomain_item -> unit + + (** register a new number choice *) +val add_num_choice: codomain_item -> unit + +(** {2 Choices lookup} + * for user defined aliases *) + + (** @param symbol symbol as per AST *) +val lookup_symbol_choices: string -> codomain_item list + +val lookup_num_choices: unit -> codomain_item list + + (** @param symbol symbol as per AST + * @param dsc description (1st component of codomain_item) + *) +val lookup_symbol_by_dsc: string -> string -> codomain_item + + (** @param dsc description (1st component of codomain_item) *) +val lookup_num_by_dsc: string -> codomain_item + diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index 522a08dc0..545099da1 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -45,47 +45,3 @@ let string_of_domain dom = dom; Buffer.contents buf -module EnvironmentP3 = - struct - type t = environment - let empty = "" - - let to_string env = - Environment.fold - (fun i v s -> - match i with - | Id id ->s ^ Printf.sprintf "alias %s %s\n" id (fst v) - | _ -> "") - env "" - - let of_string inputtext = - let regexpr = - let alfa = "[a-zA-Z_-]" in - let digit = "[0-9]" in - let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in - let blanks = "\( \|\t\|\n\)+" in - let nonblanks = "[^ \t\n]+" in - let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *) - Str.regexp - ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)") - in - let rec aux n = - try - let n' = Str.search_forward regexpr inputtext n in - let id = Id (Str.matched_group 2 inputtext) in - let uri = "cic:" ^ (Str.matched_group 5 inputtext) in - let resolve_id = aux (n' + 1) in - if Environment.mem id resolve_id then - resolve_id - else - let term = - HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) - in - (Environment.add id (uri, (fun _ _ _ -> term)) - resolve_id) - with - Not_found -> Environment.empty - in - aux 0 - end - diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index a8dda6c39..525a7e33f 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -54,13 +54,3 @@ module type Callbacks = val string_of_domain_item: domain_item -> string val string_of_domain: Domain.t -> string -(**/**) - -module EnvironmentP3: - sig - type t = environment - val empty : string - val to_string : t -> string - val of_string : string -> t - end - diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml index 011462f81..85c5be3ea 100644 --- a/helm/ocaml/cic_disambiguation/logic_notation.ml +++ b/helm/ocaml/cic_disambiguation/logic_notation.ml @@ -47,13 +47,13 @@ EXTEND END let _ = - Disambiguate.add_symbol_choice "eq" + DisambiguateChoices.add_symbol_choice "eq" ("leibnitz's equality", (fun interp _ args -> let t1, t2 = match args with | [t1; t2] -> t1, t2 - | _ -> raise Disambiguate.Invalid_choice + | _ -> raise DisambiguateChoices.Invalid_choice in Cic.Appl [ Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); diff --git a/helm/ocaml/cic_disambiguation/test_lexer.ml b/helm/ocaml/cic_disambiguation/test_lexer.ml index 520829d87..b68d26de3 100644 --- a/helm/ocaml/cic_disambiguation/test_lexer.ml +++ b/helm/ocaml/cic_disambiguation/test_lexer.ml @@ -29,7 +29,7 @@ let ic = with Invalid_argument _ -> stdin in let token_stream = - fst (CicTextualLexer2.lex.Token.tok_func (Stream.of_channel ic)) + fst (CicTextualLexer2.cic_lexer.Token.tok_func (Stream.of_channel ic)) in let rec dump () = let (a,b) = Stream.next token_stream in diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml index 1813fd641..a3bba5a5a 100644 --- a/helm/ocaml/cic_disambiguation/test_parser.ml +++ b/helm/ocaml/cic_disambiguation/test_parser.ml @@ -23,16 +23,33 @@ * http://helm.cs.unibo.it/ *) -try - let ic = - (try - open_in Sys.argv.(1) - with Invalid_argument _ -> stdin) - in - let term = CicTextualParser2.parse_term (Stream.of_channel ic) in - close_in ic; - print_endline (CicTextualParser2Pp.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)) +let mode = ref `Term + +let _ = + try + match Sys.argv.(1) with + | "alias" -> mode := `Alias + | "term" -> mode := `Term + | _ -> () + with Invalid_argument _ -> () + +let _ = + try + let ic = stdin in + (match !mode with + | `Term -> + let term = CicTextualParser2.parse_term (Stream.of_channel ic) in + close_in ic; + print_endline (CicTextualParser2Pp.pp_term term) + | `Alias -> + while true do + let line = input_line ic in + let env = CicTextualParser2.EnvironmentP3.of_string line in + print_endline (CicTextualParser2.EnvironmentP3.to_string env) + done) + with + | End_of_file -> () + | 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)) -- 2.39.2