From: Stefano Zacchiroli Date: Mon, 18 Jul 2005 13:26:38 +0000 (+0000) Subject: - removed old parser X-Git-Tag: V_0_7_2~198 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7dbab245dee64ceb23e3f07a661101d6b78ed96a;p=helm.git - removed old parser - reorganized module structure this directory should now be renamed to ocaml/disambiguation/ --- diff --git a/helm/ocaml/cic_disambiguation/.depend b/helm/ocaml/cic_disambiguation/.depend index c83a3c6ae..72f85a734 100644 --- a/helm/ocaml/cic_disambiguation/.depend +++ b/helm/ocaml/cic_disambiguation/.depend @@ -11,5 +11,5 @@ disambiguate.cmo: disambiguateTypes.cmi disambiguateChoices.cmi \ disambiguate.cmi disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \ disambiguate.cmi -arit_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi -arit_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx +number_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi +number_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile index b995f537d..dcc99fdec 100644 --- a/helm/ocaml/cic_disambiguation/Makefile +++ b/helm/ocaml/cic_disambiguation/Makefile @@ -4,7 +4,7 @@ REQUIRES = \ helm-tactics helm-logger helm-cic_unification helm-cic_notation \ helm-utf8_macros \ ulex -NOTATIONS = arit +NOTATIONS = number INTERFACE_FILES = \ disambiguateTypes.mli \ disambiguatePp.mli \ @@ -16,11 +16,9 @@ IMPLEMENTATION_FILES = \ all: -clean: extra_clean -distclean: extra_clean +clean: +distclean: rm -f macro_table.dump -extra_clean: - rm -f test_lexer test_parser include ../Makefile.common OCAMLARCHIVEOPTIONS += -linkall diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml deleted file mode 100644 index 7ce0ec0a0..000000000 --- a/helm/ocaml/cic_disambiguation/arit_notation.ml +++ /dev/null @@ -1,56 +0,0 @@ -(* 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/ - *) - -let _ = - let const s = Cic.Const (s, []) in - let mutind s = Cic.MutInd (s, 0, []) in - - DisambiguateChoices.add_num_choice - ("natural number", - (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num))); - DisambiguateChoices.add_num_choice - ("real number", - (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num))); - DisambiguateChoices.add_num_choice - ("binary positive number", - (fun _ num _ -> - let num = int_of_string num in - if num = 0 then - raise DisambiguateTypes.Invalid_choice - else - HelmLibraryObjects.build_bin_pos num)); - DisambiguateChoices.add_num_choice - ("binary integer number", - (fun _ num _ -> - let num = int_of_string num in - if num = 0 then - HelmLibraryObjects.BinInt.z0 - else if num > 0 then - Cic.Appl [ - HelmLibraryObjects.BinInt.zpos; - HelmLibraryObjects.build_bin_pos num ] - else - assert false)) - diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml deleted file mode 100644 index 7606344d1..000000000 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ /dev/null @@ -1,176 +0,0 @@ -(* 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/ - *) - -exception Error of int * int * string - -exception Not_an_extended_ident - -let regexp alpha = [ 'a' - 'z' 'A' - 'Z' ] -let regexp digit = [ '0' - '9' ] -let regexp blank = [ ' ' '\t' '\n' ] -let regexp paren = [ '(' '[' '{' ')' ']' '}' ] -let regexp implicit = '?' -let regexp placeholder = '%' -let regexp symbol_char = - [^ 'a' - 'z' 'A' - 'Z' '0' - '9' - ' ' '\t' '\n' - '\\' '(' '[' '{' ')' ']' '}' '?' - ] - -let regexp comment_char = [^'*'] | '*'[^')'] -let regexp note = "(*" ([^'*'] | "**") comment_char* "*)" - -let regexp commentbegin = "(**" blank -let regexp commentend = "*)" - -let regexp blanks = blank+ -let regexp num = digit+ -let regexp tex_token = '\\' alpha+ -let regexp symbol = symbol_char -let regexp ident_cont = alpha | num | '_' | '\'' -let regexp ident_cont' = ident_cont | tex_token -let regexp ident = (alpha ident_cont*) | ('_' ident_cont+) -let regexp ident' = ((alpha | tex_token) ident_cont'*) | ('_' ident_cont'+) -let regexp uri_step = (alpha (ident_cont|'-')*) -let regexp meta = implicit num -let regexp qstring = '"' [^ '"']* '"' -let regexp uri_suffix = "con"|"ind"|"var" -let regexp uri = - ("cic:/" | "theory:/") (* schema *) - uri_step ('/' uri_step)* (* path *) - ('.' uri_suffix)+ (* ext *) - ("#xpointer(" num ('/' num)+ ")")? (* xpointer *) -(* let regexp catchall = .* *) - -let keywords = Hashtbl.create 17 -let _ = - List.iter (fun keyword -> Hashtbl.add keywords keyword ("", keyword)) - [ "Prop"; "Type"; "Set"; "let"; "Let"; "rec"; "using"; "match"; "with"; - "in"; "and"; "to"; "as"; "on"; "names"] - -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 = - let flocation_begin = - { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; - Lexing.pos_cnum = Ulexing.lexeme_start lexbuf } - in - let flocation_end = - { flocation_begin with Lexing.pos_cnum = Ulexing.lexeme_end lexbuf } - in - (token, (flocation_begin, flocation_end)) - -(* -let parse_ext_ident ident = - let len = String.length ident in - let buf = Buffer.create len in - let in_tex_token = ref false in - let tex_token = Buffer.create 10 in - try - for i = 0 to len - 1 do - match ident.[i] with - | '\' when not !in_tex_token -> - if i < len - 1 && - in_tex_token := true - done - with Invalid_argument -> assert false - -let rec token' = lexer - | ident' -> - (try - let ident = parse_ext_ident (Ulexing.utf8_lexeme lexbuf) in - return lexbuf ("IDENT'", ident) - with Not_an_extended_ident -> - Ulexing.rollback lexbuf; - token lexbuf) - | _ -> - Ulexing.rollback lexbuf; - token lexbuf - -and token = lexer -*) - -let remove_quotes s = String.sub s 1 (String.length s - 2) - -let rec token comments = lexer - | blanks -> token comments lexbuf - | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme 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 ("NUM", Ulexing.utf8_lexeme lexbuf) - | paren -> return lexbuf ("PAREN", Ulexing.utf8_lexeme lexbuf) - | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf) - | implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf) - | placeholder -> return lexbuf ("PLACEHOLDER", Ulexing.utf8_lexeme lexbuf) - | qstring -> - return lexbuf ("QSTRING", remove_quotes (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", Utf8Macro.expand macro) - with Utf8Macro.Macro_not_found _ -> - return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)) - | note -> - (*if comments then*) - let comment = - Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 4) - in - return lexbuf ("NOTE", comment) - (*else - token comments lexbuf*) - | commentbegin -> return lexbuf ("BEGINCOMMENT","") - | commentend -> return lexbuf ("ENDCOMMENT","") - | eof -> return lexbuf ("EOI", "") - | _ -> error lexbuf "Invalid character" - -let tok_func comments stream = - let lexbuf = Ulexing.from_utf8_stream stream in - Token.make_stream_and_flocation - (fun () -> - try - token comments lexbuf - with - | Ulexing.Error -> error_at_end lexbuf "Unexpected character" - | Ulexing.InvalidCodepoint i -> error_at_end lexbuf "Invalid code point") - -let cic_lexer ?(comments = false) () = - { - Token.tok_func = tok_func comments; - 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/cicTextualLexer2.mli b/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli deleted file mode 100644 index 7e3ac625b..000000000 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli +++ /dev/null @@ -1,32 +0,0 @@ -(* 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/ - *) - -exception Error of int * int * string - - (** lexer - * @param comments if true the lexer will return COMMENT tokens, otherwise they - * will be ignored. Defaults to false *) -val cic_lexer: ?comments:bool -> unit -> (string * string) Token.glexer - diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml deleted file mode 100644 index 451d77292..000000000 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ /dev/null @@ -1,779 +0,0 @@ -(* 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/ - *) - -let debug = false -let debug_print s = - if debug then begin - prerr_endline ""; - prerr_endline s; - prerr_endline "" - end - - (** if set to true each number will have a different insance number and can - * thus be interpreted differently than others *) -let use_fresh_num_instances = false - - (** does the lexer return COMMENT tokens? *) -let return_comments = false - -open Printf - -open DisambiguateTypes - -exception Parse_error of Token.flocation * string - -let cic_lexer = CicTextualLexer2.cic_lexer ~comments:return_comments () - -let fresh_num_instance = - let n = ref 0 in - if use_fresh_num_instances then - (fun () -> incr n; !n) - else - (fun () -> 0) - -let choice_of_uri suri = - let term = CicUtil.term_of_uri (UriManager.uri_of_string suri) in - (suri, (fun _ _ _ -> term)) - -let grammar = Grammar.gcreate cic_lexer - -let term = Grammar.Entry.create grammar "term" -let term0 = Grammar.Entry.create grammar "term0" -let tactic = Grammar.Entry.create grammar "tactic" -let tactical = Grammar.Entry.create grammar "tactical" -let tactical0 = Grammar.Entry.create grammar "tactical0" -let command = Grammar.Entry.create grammar "command" -let alias_spec = Grammar.Entry.create grammar "alias_spec" -let macro = Grammar.Entry.create grammar "macro" -let script = Grammar.Entry.create grammar "script" -let statement = Grammar.Entry.create grammar "statement" -let statements = Grammar.Entry.create grammar "statements" - -let return_term loc term = CicAst.AttributedTerm (`Loc loc, term) - -let fail floc msg = - let (x, y) = CicAst.loc_of_floc floc in - failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) - -let name_of_string = function - | "_" -> Cic.Anonymous - | s -> Cic.Name s - -let string_of_name = function - | Cic.Anonymous -> "_" - | Cic.Name s -> s - -let int_opt = function - | None -> None - | Some lexeme -> Some (int_of_string lexeme) - -let int_of_string s = - try - Pervasives.int_of_string s - with Failure _ -> - failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s) - - (** the uri of an inductive type (a ".ind" uri) is not meaningful without an - * xpointer. Still, it's likely that an user who wrote "cic:/blabla/foo.ind" - * actually meant "cic:/blabla/foo.ind#xpointer(1/1)", i.e. the first inductive - * type in a block of mutual inductive types. - * - * This function performs the expansion foo.ind -> foo#xpointer..., if needed - *) -let ind_expansion uri = - let len = String.length uri in - if len >= 4 && String.sub uri (len - 4) 4 = ".ind" then - uri ^ "#xpointer(1/1)" - else - uri - -let mk_binder_ast binder typ vars body = - List.fold_right - (fun var body -> - let name = name_of_string var in - CicAst.Binder (binder, (name, typ), body)) - vars body - -EXTEND - GLOBAL: term term0 statement statements; - int: [ - [ num = NUM -> - try - int_of_string num - with Failure _ -> raise (Parse_error (loc, "integer literal expected")) - ] - ]; - meta_subst: [ - [ s = SYMBOL "_" -> None - | t = term -> Some t ] - ]; - binder_low: [ - [ SYMBOL <:unicode> (* Π *) -> `Pi - | SYMBOL <:unicode> (* ∃ *) -> `Exists - | SYMBOL <:unicode> (* ∀ *) -> `Forall ] - ]; - binder_high: [ [ SYMBOL <:unicode> (* λ *) -> `Lambda ] ]; - sort: [ - [ "Prop" -> `Prop - | "Set" -> `Set - | "Type" -> `Type - | "CProp" -> `CProp ] - ]; - typed_name: [ - [ PAREN "("; i = IDENT; SYMBOL ":"; typ = term; PAREN ")" -> - (Cic.Name i, Some typ) - | i = IDENT -> (Cic.Name i, None) - ] - ]; - subst: [ - [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) - PAREN "["; - substs = LIST1 [ - i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) - ] SEP SYMBOL ";"; - PAREN "]" -> - substs - ] - ]; - substituted_name: [ (* a subs.name is an explicit substitution subject *) - [ s = IDENT; subst = OPT subst -> CicAst.Ident (s, subst) - | s = URI; subst = OPT subst -> CicAst.Uri (ind_expansion s, subst) - ] - ]; - name: [ (* as substituted_name with no explicit substitution *) - [ s = [ IDENT | SYMBOL ] -> s ] - ]; - pattern: [ - [ n = name -> (n, []) - | PAREN "("; head = name; vars = LIST1 typed_name; PAREN ")" -> - (head, vars) - ] - ]; - arg: [ - [ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; - SYMBOL ":"; ty = term; PAREN ")" -> names,ty - | name = IDENT -> [name],CicAst.Implicit - ] - ]; - let_defs:[ - [ defs = LIST1 [ - name = IDENT; - args = LIST1 [arg = arg -> arg]; - index_name = OPT [ "on"; idx = IDENT -> idx ]; - ty = OPT [ SYMBOL ":" ; t = term -> t ]; - SYMBOL <:unicode> (* ≝ *); - t1 = term -> - let rec list_of_binder binder ty final_term = function - | [] -> final_term - | name::tl -> - CicAst.Binder (binder, (Cic.Name name, Some ty), - list_of_binder binder ty final_term tl) - in - let rec binder_of_arg_list binder final_term = function - | [] -> final_term - | (l,ty)::tl -> - list_of_binder binder ty - (binder_of_arg_list binder final_term tl) l - in - let t1' = binder_of_arg_list `Lambda t1 args in - let ty' = - match ty with - | None -> None - | Some ty -> Some (binder_of_arg_list `Pi ty args) - in - let rec get_position_of name n = function - | [] -> (None,n) - | nam::tl -> - if nam = name then - (Some n,n) - else - (get_position_of name (n+1) tl) - in - let rec find_arg name n = function - | [] -> (fail loc (sprintf "Argument %s not found" name)) - | (l,_)::tl -> - let (got,len) = get_position_of name 0 l in - (match got with - | None -> (find_arg name (n+len) tl) - | Some where -> n + where) - in - let index = - (match index_name with - | None -> 0 - | (Some name) -> find_arg name 0 args) - in - ((Cic.Name name,ty'), t1', index) - ] SEP "and" -> defs - ]]; - constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; - binder_vars: [ - [ vars = [ l = LIST1 IDENT SEP SYMBOL "," -> l | SYMBOL "_" -> ["_"]]; - typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ) - | PAREN "("; - vars = [ l = LIST1 IDENT SEP SYMBOL "," -> l | SYMBOL "_" -> ["_"]]; - typ = OPT [ SYMBOL ":"; t = term -> t ]; - PAREN ")" -> (vars, typ) - ] - ]; - term0: [ [ t = term; EOI -> return_term loc t ] ]; - term: - [ "letin" NONA - [ "let"; var = typed_name; - SYMBOL <:unicode> (* ≝ *); - t1 = term; "in"; t2 = term -> - return_term loc (CicAst.LetIn (var, t1, t2)) - | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; - defs = let_defs; "in"; body = term -> - return_term loc (CicAst.LetRec (ind_kind, defs, body)) - ] - | "binder" RIGHTA - [ - b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term -> - let binder = mk_binder_ast b typ vars body in - return_term loc binder - | b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term -> - let binder = mk_binder_ast b typ vars body in - return_term loc binder - | t1 = term; SYMBOL <:unicode> (* → *); t2 = term -> - return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2)) - ] - | "logic_add" LEFTA [ (* nothing here by default *) ] - | "logic_mult" LEFTA [ (* nothing here by default *) ] - | "logic_inv" NONA [ (* nothing here by default *) ] - | "relop" LEFTA - [ t1 = term; SYMBOL "="; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2]) - ] - | "add" LEFTA [ (* nothing here by default *) ] - | "mult" LEFTA [ (* nothing here by default *) ] - | "power" LEFTA [ (* nothing here by default *) ] - | "inv" NONA [ (* nothing here by default *) ] - | "apply" LEFTA - [ t1 = term; t2 = term -> - let rec aux = function - | CicAst.Appl (hd :: tl) -> aux hd @ tl - | term -> [term] - in - CicAst.Appl (aux t1 @ [t2]) - ] - | "simple" NONA - [ sort = sort -> CicAst.Sort sort - | n = substituted_name -> return_term loc n - | i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ()))) - | IMPLICIT -> return_term loc CicAst.Implicit - | PLACEHOLDER -> return_term loc CicAst.UserInput - | m = META; - substs = [ - PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" -> - substs - ] -> - let index = - try - int_of_string (String.sub m 1 (String.length m - 1)) - with Failure "int_of_string" -> - fail loc ("Invalid meta variable number: " ^ m) - in - return_term loc (CicAst.Meta (index, substs)) - | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ]; - "match"; t = term; - indty_ident = OPT ["in" ; id = IDENT -> id ]; - "with"; - PAREN "["; - patterns = LIST0 [ - lhs = pattern; SYMBOL <:unicode> (* ⇒ *); rhs = term - -> - ((lhs: CicAst.case_pattern), rhs) - ] SEP SYMBOL "|"; - PAREN "]" -> - return_term loc - (CicAst.Case (t, indty_ident, outtyp, patterns)) - | PAREN "("; t1 = term; SYMBOL ":"; t2 = term; PAREN ")" -> - return_term loc (CicAst.Appl [CicAst.Symbol ("cast", 0); t1; t2]) - | PAREN "("; t = term; PAREN ")" -> return_term loc t - ] - ]; - tactic_term: [ [ t = term -> t ] ]; - ident_list0: [ - [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] - ]; - tactic_term_list1: [ - [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] - ]; - reduction_kind: [ - [ [ IDENT "reduce" ] -> `Reduce - | [ IDENT "simplify" ] -> `Simpl - | [ IDENT "whd" ] -> `Whd - | [ IDENT "normalize" ] -> `Normalize ] - ]; - sequent_pattern_spec : [ - [ hyp_paths = - LIST0 - [ id = IDENT ; - path = OPT [SYMBOL ":" ; path = term -> path ] -> - (id,match path with Some p -> p | None -> CicAst.UserInput) ] - SEP SYMBOL ";"; - goal_path = OPT [ SYMBOL <:unicode>; term = term -> term ] -> - let goal_path = - match goal_path with - None -> CicAst.UserInput - | Some goal_path -> goal_path - in - hyp_paths,goal_path - ] - ]; - pattern_spec: [ - [ res = OPT [ - "in"; - wanted_and_sps = - [ "match" ; wanted = term ; - sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] -> - Some wanted,sps - | sps = sequent_pattern_spec -> - None,Some sps - ] -> - let wanted,hyp_paths,goal_path = - match wanted_and_sps with - wanted,None -> wanted, [], CicAst.UserInput - | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path - in - wanted, hyp_paths, goal_path ] -> - match res with - None -> None,[],CicAst.UserInput - | Some ps -> ps] - ]; - direction: [ - [ SYMBOL ">" -> `LeftToRight - | SYMBOL "<" -> `RightToLeft ] - ]; - tactic: [ - [ IDENT "absurd"; t = tactic_term -> - TacticAst.Absurd (loc, t) - | IDENT "apply"; t = tactic_term -> - TacticAst.Apply (loc, t) - | IDENT "assumption" -> - TacticAst.Assumption loc - | IDENT "auto"; - depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ]; - width = OPT [ IDENT "width"; SYMBOL "="; i = NUM -> int_of_string i ] -> - TacticAst.Auto (loc,depth,width) - | IDENT "clear"; id = IDENT -> - TacticAst.Clear (loc,id) - | IDENT "clearbody"; id = IDENT -> - TacticAst.ClearBody (loc,id) - | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> - TacticAst.Change (loc, what, t) - | IDENT "compare"; t = tactic_term -> - TacticAst.Compare (loc,t) - | IDENT "constructor"; n = NUM -> - TacticAst.Constructor (loc,int_of_string n) - | IDENT "contradiction" -> - TacticAst.Contradiction loc - | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] -> - TacticAst.Cut (loc, ident, t) - | IDENT "decide"; IDENT "equality" -> - TacticAst.DecideEquality loc - | IDENT "decompose"; where = tactic_term -> - TacticAst.Decompose (loc, where) - | IDENT "discriminate"; t = tactic_term -> - TacticAst.Discriminate (loc, t) - | IDENT "elim"; what = tactic_term; - using = OPT [ "using"; using = tactic_term -> using ]; - OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in - TacticAst.Elim (loc, what, using, num, idents) - | IDENT "elimType"; what = tactic_term; - using = OPT [ "using"; using = tactic_term -> using ]; - OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in - TacticAst.ElimType (loc, what, using, num, idents) - | IDENT "exact"; t = tactic_term -> - TacticAst.Exact (loc, t) - | IDENT "exists" -> - TacticAst.Exists loc - | IDENT "fail" -> TacticAst.Fail loc - | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec -> - let (pt,_,_) = p in - if pt <> None then - raise - (Parse_error - (loc,"the pattern cannot specify the term to replace, only its paths in the hypotheses and in the conclusion")) - else - TacticAst.Fold (loc, kind, t, p) - | IDENT "fourier" -> - TacticAst.Fourier loc - | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in - TacticAst.FwdSimpl (loc, hyp, idents) - | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] -> - TacticAst.Generalize (loc,p,id) - | IDENT "goal"; n = NUM -> - TacticAst.Goal (loc, int_of_string n) - | IDENT "id" -> TacticAst.IdTac loc - | IDENT "injection"; t = tactic_term -> - TacticAst.Injection (loc, t) - | IDENT "intro"; ident = OPT IDENT -> - let idents = match ident with None -> [] | Some id -> [id] in - TacticAst.Intros (loc, Some 1, idents) - | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in - TacticAst.Intros (loc, num, idents) - | IDENT "lapply"; - depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ]; - what = tactic_term; - to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; - ident = OPT [ "using" ; ident = IDENT -> ident ] -> - let to_what = match to_what with None -> [] | Some to_what -> to_what in - TacticAst.LApply (loc, depth, to_what, what, ident) - | IDENT "left" -> TacticAst.Left loc - | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> - TacticAst.LetIn (loc, t, where) - | kind = reduction_kind; p = pattern_spec -> - TacticAst.Reduce (loc, kind, p) - | IDENT "reflexivity" -> - TacticAst.Reflexivity loc - | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term -> - TacticAst.Replace (loc, p, t) - | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec -> - let (pt,_,_) = p in - if pt <> None then - raise - (Parse_error - (loc,"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")) - else - TacticAst.Rewrite (loc, d, t, p) - | IDENT "right" -> - TacticAst.Right loc - | IDENT "ring" -> - TacticAst.Ring loc - | IDENT "split" -> - TacticAst.Split loc - | IDENT "symmetry" -> - TacticAst.Symmetry loc - | IDENT "transitivity"; t = tactic_term -> - TacticAst.Transitivity (loc, t) - ] - ]; - tactical: - [ "sequence" LEFTA - [ tacticals = LIST1 NEXT SEP SYMBOL ";" -> - match tacticals with - [] -> assert false - | [tac] -> tac - | l -> TacticAst.Seq (loc, l) - ] - | "then" NONA - [ tac = tactical; SYMBOL ";"; - PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" -> - (TacticAst.Then (loc, tac, tacs)) - ] - | "loops" RIGHTA - [ IDENT "do"; count = int; tac = tactical -> - TacticAst.Do (loc, count, tac) - | IDENT "repeat"; tac = tactical -> - TacticAst.Repeat (loc, tac) - ] - | "simple" NONA - [ IDENT "first"; - PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" -> - TacticAst.First (loc, tacs) - | IDENT "try"; tac = NEXT -> - TacticAst.Try (loc, tac) - | IDENT "solve"; - PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" -> - TacticAst.Solve (loc, tacs) - | PAREN "("; tac = tactical; PAREN ")" -> tac - | tac = tactic -> TacticAst.Tactic (loc, tac) - ] - ]; - theorem_flavour: [ - [ [ IDENT "definition" ] -> `Definition - | [ IDENT "fact" ] -> `Fact - | [ IDENT "lemma" ] -> `Lemma - | [ IDENT "remark" ] -> `Remark - | [ IDENT "theorem" ] -> `Theorem - ] - ]; - inductive_spec: [ [ - fst_name = IDENT; params = LIST0 [ arg=arg -> arg ]; - SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; - fst_constructors = LIST0 constructor SEP SYMBOL "|"; - tl = OPT [ "with"; - types = LIST1 [ - name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode>; - OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> - (name, true, typ, constructors) ] SEP "with" -> types - ] -> - let params = - List.fold_right - (fun (names, typ) acc -> - (List.map (fun name -> (name, typ)) names) @ acc) - params [] - in - let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in - let tl_ind_types = match tl with None -> [] | Some types -> types in - let ind_types = fst_ind_type :: tl_ind_types in - (params, ind_types) - ] ]; - - record_spec: [ [ - name = IDENT; params = LIST0 [ arg = arg -> arg ] ; - SYMBOL ":"; typ = term; SYMBOL <:unicode>; PAREN "{" ; - fields = LIST0 [ - name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) - ] SEP SYMBOL ";"; PAREN "}" -> - let params = - List.fold_right - (fun (names, typ) acc -> - (List.map (fun name -> (name, typ)) names) @ acc) - params [] - in - (params,name,typ,fields) - ] ]; - - macro: [ - [ [ IDENT "quit" ] -> TacticAst.Quit loc -(* | [ IDENT "abort" ] -> TacticAst.Abort loc *) - | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name) -(* | [ IDENT "undo" ]; steps = OPT NUM -> - TacticAst.Undo (loc, int_opt steps) - | [ IDENT "redo" ]; steps = OPT NUM -> - TacticAst.Redo (loc, int_opt steps) *) - | [ IDENT "check" ]; t = term -> - TacticAst.Check (loc, t) - | [ IDENT "hint" ] -> TacticAst.Hint loc - | [ IDENT "whelp"; "match" ] ; t = term -> - TacticAst.WMatch (loc,t) - | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> - TacticAst.WInstance (loc,t) - | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> - TacticAst.WLocate (loc,id) - | [ IDENT "whelp"; IDENT "elim" ] ; t = term -> - TacticAst.WElim (loc, t) - | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> - TacticAst.WHint (loc,t) - | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name) - ] - ]; - - alias_spec: [ - [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING -> - let alpha = "[a-zA-Z]" in - let num = "[0-9]+" in - let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in - let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in - let rex = Str.regexp ("^"^ident^"$") in - if Str.string_match rex id 0 then - if (try ignore (UriManager.uri_of_string uri); true - with UriManager.IllFormedUri _ -> false) - then - TacticAst.Ident_alias (id, uri) - else - raise (Parse_error (loc,sprintf "Not a valid uri: %s" uri)) - else - raise (Parse_error (loc,sprintf "Not a valid identifier: %s" id)) - | IDENT "symbol"; symbol = QSTRING; - instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ]; - SYMBOL "="; dsc = QSTRING -> - let instance = - match instance with Some i -> int_of_string i | None -> 0 - in - TacticAst.Symbol_alias (symbol, instance, dsc) - | IDENT "num"; - instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ]; - SYMBOL "="; dsc = QSTRING -> - let instance = - match instance with Some i -> int_of_string i | None -> 0 - in - TacticAst.Number_alias (instance, dsc) - ] - ]; - - command: [[ - [ IDENT "set" ]; n = QSTRING; v = QSTRING -> - TacticAst.Set (loc, n, v) - | [ IDENT "drop" ] -> TacticAst.Drop loc - | [ IDENT "qed" ] -> TacticAst.Qed loc - | IDENT "variant" ; name = IDENT; SYMBOL ":"; - typ = term; SYMBOL <:unicode> ; newname = IDENT -> - TacticAst.Obj (loc, - TacticAst.Theorem - (`Variant,name,typ,Some (CicAst.Ident (newname, None)))) - | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; - body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body)) - | flavour = theorem_flavour; name = IDENT; - body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, CicAst.Implicit, body)) - | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; - defs = let_defs -> - let name,ty = - match defs with - | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty - | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit - | _ -> assert false - in - let body = CicAst.Ident (name,None) in - TacticAst.Obj (loc,TacticAst.Theorem(`Definition, name, ty, - Some (CicAst.LetRec (ind_kind, defs, body)))) - - | [ IDENT "inductive" ]; spec = inductive_spec -> - let (params, ind_types) = spec in - TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types)) - | [ IDENT "coinductive" ]; spec = inductive_spec -> - let (params, ind_types) = spec in - let ind_types = (* set inductive flags to false (coinductive) *) - List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) - ind_types - in - TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types)) - | IDENT "coercion" ; name = IDENT -> - TacticAst.Coercion (loc, CicAst.Ident (name,Some [])) - | IDENT "coercion" ; name = URI -> - TacticAst.Coercion (loc, CicAst.Uri (name,Some [])) - | IDENT "alias" ; spec = alias_spec -> - TacticAst.Alias (loc, spec) - | IDENT "record" ; (params,name,ty,fields) = record_spec -> - TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields)) - | IDENT "include" ; path = QSTRING -> - TacticAst.Include (loc,path) - | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> - let uris = List.map UriManager.uri_of_string uris in - TacticAst.Default (loc,what,uris) - ]]; - - executable: [ - [ cmd = command; SYMBOL "." -> TacticAst.Command (loc, cmd) - | tac = tactical; SYMBOL "." -> TacticAst.Tactical (loc, tac) - | mac = macro; SYMBOL "." -> TacticAst.Macro (loc, mac) - ] - ]; - - comment: [ - [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT -> - TacticAst.Code (loc, ex) - | str = NOTE -> - TacticAst.Note (loc, str) - ] - ]; - - statement: [ - [ ex = executable -> TacticAst.Executable (loc,ex) - | com = comment -> TacticAst.Comment (loc, com) - ] - ]; - statements: [ - [ l = LIST0 statement ; EOI -> l - ] - ]; -END - -let exc_located_wrapper f = - try - f () - with - | Stdpp.Exc_located (floc, Stream.Error msg) -> - raise (Parse_error (floc, msg)) - | Stdpp.Exc_located (floc, exn) -> - raise (Parse_error (floc, (Printexc.to_string exn))) - -let parse_term stream = - exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream)) -let parse_statement stream = - exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream)) -let parse_statements stream = - exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream)) - - -(**/**) - -(** {2 Interface for gTopLevel} *) - -module EnvironmentP3 = - struct - type t = environment - - let empty = "" - - let aliases_grammar = Grammar.gcreate 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 -> - TacticAstPp.pp_alias (TacticAst.Ident_alias (id, dsc)) ^ "." - | Symbol (symb, i) -> - TacticAstPp.pp_alias (TacticAst.Symbol_alias (symb, i, dsc)) - ^ "." - | Num i -> - TacticAstPp.pp_alias (TacticAst.Number_alias (i, dsc)) ^ "." - in - s :: acc) - env [] - in - String.concat "\n" (List.sort compare aliases) ^ - (if aliases = [] then "" else "\n") - - 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 "="; suri = URI -> - (Id id, choice_of_uri suri) - | 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 = - if s = empty then - Environment.empty - else - exc_located_wrapper - (fun () -> Grammar.Entry.parse aliases (Stream.of_string s)) - end - -(* vim:set encoding=utf8: *) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli deleted file mode 100644 index c95485e52..000000000 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ /dev/null @@ -1,58 +0,0 @@ -(* 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/ - *) - -exception Parse_error of Token.flocation * string - -(** {2 Parsing functions} *) - -val parse_term: char Stream.t -> DisambiguateTypes.term -val parse_statement: - char Stream.t -> (CicAst.term, TacticAst.obj,string) TacticAst.statement -val parse_statements: - char Stream.t -> (CicAst.term, TacticAst.obj, string) TacticAst.statement list - -(** {2 Grammar extensions} *) - -val term: CicAst.term Grammar.Entry.e (** recursive rule *) -val term0: CicAst.term Grammar.Entry.e (** top level rule *) - -val return_term: CicAst.location -> CicAst.term -> CicAst.term - - (** raise a parse error *) -val fail: CicAst.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/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml deleted file mode 100644 index 2227b2741..000000000 --- a/helm/ocaml/cic_disambiguation/logic_notation.ml +++ /dev/null @@ -1,73 +0,0 @@ -(* 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 CicTextualParser2 - -EXTEND - term: LEVEL "logic_add" - [ - [ t1 = term; SYMBOL <:unicode> (* ∨ *); t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("or", 0); t1; t2]) - ] - ]; - term: LEVEL "logic_mult" - [ - [ t1 = term; SYMBOL <:unicode> (* ∧ *); t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("and", 0); t1; t2]) - ] - ]; - term: LEVEL "logic_inv" - [ - [ SYMBOL <:unicode> (* ¬ *); t = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("not", 0); t]) - ] - ]; -END - -let _ = - (* TODO cut-and-pasted code: here, in arit_notation.ml and - * disambiguateChoices.ml *) - let const s = Cic.Const (s, []) in - let mutind s = Cic.MutInd (s, 0, []) in - DisambiguateChoices.add_symbol_choice "eq" - ("leibnitz's equality", - (fun interp _ args -> - let t1, t2 = - match args with - | [t1; t2] -> t1, t2 - | _ -> raise DisambiguateChoices.Invalid_choice - in - Cic.Appl [ - Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); - Cic.Implicit (Some `Type); t1; t2 - ])); - DisambiguateChoices.add_binary_op "and" "logical and" - (mutind HelmLibraryObjects.Logic.and_URI); - DisambiguateChoices.add_binary_op "or" "logical or" - (mutind HelmLibraryObjects.Logic.or_URI); - DisambiguateChoices.add_unary_op "not" "logical not" - (const HelmLibraryObjects.Logic.not_URI); - -(* vim:set encoding=utf8: *) diff --git a/helm/ocaml/cic_disambiguation/number_notation.ml b/helm/ocaml/cic_disambiguation/number_notation.ml new file mode 100644 index 000000000..7ce0ec0a0 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/number_notation.ml @@ -0,0 +1,56 @@ +(* 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/ + *) + +let _ = + let const s = Cic.Const (s, []) in + let mutind s = Cic.MutInd (s, 0, []) in + + DisambiguateChoices.add_num_choice + ("natural number", + (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num))); + DisambiguateChoices.add_num_choice + ("real number", + (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num))); + DisambiguateChoices.add_num_choice + ("binary positive number", + (fun _ num _ -> + let num = int_of_string num in + if num = 0 then + raise DisambiguateTypes.Invalid_choice + else + HelmLibraryObjects.build_bin_pos num)); + DisambiguateChoices.add_num_choice + ("binary integer number", + (fun _ num _ -> + let num = int_of_string num in + if num = 0 then + HelmLibraryObjects.BinInt.z0 + else if num > 0 then + Cic.Appl [ + HelmLibraryObjects.BinInt.zpos; + HelmLibraryObjects.build_bin_pos num ] + else + assert false)) + diff --git a/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml b/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml deleted file mode 100644 index dc15b8c8b..000000000 --- a/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml +++ /dev/null @@ -1,65 +0,0 @@ -(* 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/ - *) - -let debug = false -let debug_print s = if debug then prerr_endline s - -let loc = - let dummy_pos = - { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; - Lexing.pos_cnum = -1 } - in - (dummy_pos, dummy_pos) - -let expand_unicode_macro macro = - debug_print (Printf.sprintf "Expanding macro '%s' ..." macro); - let expansion = CicTextualParser2Macro.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/test_lexer.ml b/helm/ocaml/cic_disambiguation/test_lexer.ml deleted file mode 100644 index 3e61e702c..000000000 --- a/helm/ocaml/cic_disambiguation/test_lexer.ml +++ /dev/null @@ -1,42 +0,0 @@ -(* 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/ - *) - -let ic = - try - open_in Sys.argv.(1) - with Invalid_argument _ -> stdin -in -let token_stream = - fst ((CicTextualLexer2.cic_lexer ()).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 deleted file mode 100644 index 4f918b0a0..000000000 --- a/helm/ocaml/cic_disambiguation/test_parser.ml +++ /dev/null @@ -1,95 +0,0 @@ -(* 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 - -(* -let pp_tactical = TacticAst2Box.tacticalPp -*) - -let modes = ("term",`Term) :: ("statement",`Statement) :: [] - -let mode = - try - List.assoc (Sys.argv.(1)) modes - with - | _ -> - prerr_endline - (sprintf "What? Supported modes are: %s\n" - (String.concat " " (List.map fst modes))); - exit 1 - -let _ = -(* - if mode = `Script then - let ic = open_in Sys.argv.(2) in - let istream = Stream.of_channel ic in - let (loc, script) = CicTextualParser2.parse_script istream in - List.iter - (function - | DisambiguateTypes.Command cmd -> print_endline (pp_tactical cmd) - | DisambiguateTypes.Comment (loc, s) -> print_endline s) - script - else -*) - let ic = stdin in - try - while true do - let line = input_line ic in - let istream = Stream.of_string line in - try - (match mode with - | `Term -> - let term = CicTextualParser2.parse_term istream in - print_endline (BoxPp.pp_term term) - | `Statement -> - (match CicTextualParser2.parse_statement istream with - | TacticAst.Executable (_, exe) - | TacticAst.Comment (_,TacticAst.Code (_, exe)) -> - print_endline (TacticAstPp.pp_executable exe) - | TacticAst.Comment (_,TacticAst.Note (_, note)) -> - print_endline note) -(* - | `Tactical -> - let tac = CicTextualParser2.parse_tactical istream in - print_endline (pp_tactical tac) -*) - | `Alias -> - let env = CicTextualParser2.EnvironmentP3.of_string line in - print_endline (CicTextualParser2.EnvironmentP3.to_string env) - | _ -> assert false); - flush stdout - with - | CicTextualParser2.Parse_error (floc, msg) -> - let (x, y) = CicAst.loc_of_floc floc in - let before = String.sub line 0 x in - let error = String.sub line x (y - x) in - let after = String.sub line y (String.length line - y) in - eprintf "%s%s%s\n" before error after; - prerr_endline (sprintf "at character %d-%d: %s" x y msg) - done - with End_of_file -> - close_in ic - diff --git a/helm/ocaml/cic_disambiguation/tex_notation.ml b/helm/ocaml/cic_disambiguation/tex_notation.ml deleted file mode 100644 index cd0f47282..000000000 --- a/helm/ocaml/cic_disambiguation/tex_notation.ml +++ /dev/null @@ -1,47 +0,0 @@ -(* 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 CicTextualParser2 - -EXTEND - term: LEVEL "simple" - [ - (* for tex parsing *) - [ PAREN "{"; t = term; PAREN "}" -> return_term loc t - | SYMBOL "\\"; PAREN "{"; t = term; SYMBOL "\\"; PAREN "}" -> - return_term loc t - ] - ]; - term0: - [ - [ SYMBOL "$"; PAREN "{"; t = term; PAREN "}"; SYMBOL "$" -> - return_term loc t - | SYMBOL "$"; t = term; SYMBOL "$" -> - return_term loc t - ] - ]; -END - -(* vim:set encoding=utf8: *)