+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
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
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)
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 ]));
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
*)
let rec token = lexer
| blanks -> token lexbuf
+ | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
| ident ->
let lexeme = Ulexing.utf8_lexeme lexbuf in
(try
| 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 =
| 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 _ -> ());
Token.tok_text = Token.lexer_text;
Token.tok_comm = None;
}
+
exception Error of int * int * string
-val lex : (string * string) Token.glexer
+val cic_lexer : (string * string) Token.glexer
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"
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 <domain_item, codomain_item> 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
+
(** {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 ->
(** 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
+
open DisambiguateTypes
open UriManager
-exception Invalid_choice
exception No_choices of domain_item
exception NoWellTypedInterpretation
| 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
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))
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
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 =
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
--- /dev/null
+(* 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))
+
--- /dev/null
+(* 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
+
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
-
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
-
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, []);
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
* 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))
projects / helm.git / commitdiff