From: Stefano Zacchiroli Date: Fri, 23 Jan 2004 17:05:20 +0000 (+0000) Subject: renamed modules so that they are more consistent with other cic modules X-Git-Tag: V_0_2_3~158 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8004125685a99b6c0f2f95fd7f3fa09a4f5c9094;p=helm.git renamed modules so that they are more consistent with other cic modules --- diff --git a/helm/gTopLevel/chosenTermEditor.mli b/helm/gTopLevel/chosenTermEditor.mli index ebd9a95e6..1cc4f5606 100644 --- a/helm/gTopLevel/chosenTermEditor.mli +++ b/helm/gTopLevel/chosenTermEditor.mli @@ -11,7 +11,7 @@ class type term_editor = end module Make : - functor (C : Disambiguate_types.Callbacks) -> + functor (C : DisambiguateTypes.Callbacks) -> sig val term_editor : MQIConn.handle -> diff --git a/helm/gTopLevel/disambiguatingParser.ml b/helm/gTopLevel/disambiguatingParser.ml index 8ce12c045..580e09bb2 100644 --- a/helm/gTopLevel/disambiguatingParser.ml +++ b/helm/gTopLevel/disambiguatingParser.ml @@ -25,13 +25,13 @@ exception NoWellTypedInterpretation -module EnvironmentP3 = Disambiguate_types.EnvironmentP3 +module EnvironmentP3 = DisambiguateTypes.EnvironmentP3 -module Make (C : Disambiguate_types.Callbacks) = +module Make (C : DisambiguateTypes.Callbacks) = struct let disambiguate_term mqi_handle context metasenv term_as_string environment = let module Disambiguate' = Disambiguate.Make (C) in - let term = Parser.parse_term (Stream.of_string term_as_string) in + let term = CicTextualParser2.parse_term (Stream.of_string term_as_string) in Disambiguate'.disambiguate_term mqi_handle context metasenv term environment end diff --git a/helm/gTopLevel/disambiguatingParser.mli b/helm/gTopLevel/disambiguatingParser.mli index 397799548..5ddf68377 100644 --- a/helm/gTopLevel/disambiguatingParser.mli +++ b/helm/gTopLevel/disambiguatingParser.mli @@ -33,7 +33,7 @@ module EnvironmentP3 : val of_string : string -> t end -module Make (C : Disambiguate_types.Callbacks) : +module Make (C : DisambiguateTypes.Callbacks) : sig val disambiguate_term : MQIConn.handle -> diff --git a/helm/gTopLevel/script.sh b/helm/gTopLevel/script.sh index 5592e25d8..848103c32 100755 --- a/helm/gTopLevel/script.sh +++ b/helm/gTopLevel/script.sh @@ -11,7 +11,6 @@ export GTOPLEVEL_INNERTYPESFILE=/public/helm_library/innertypes export GTOPLEVEL_CONSTANTTYPEFILE=/public/helm_library/constanttype export GTOPLEVEL_ENVIRONMENTFILE=/public/helm_library/environment export MATHQL_DB_MAP=/home/zack/helm/mathql_db_map.txt -export POSTGRESQL_CONNECTION_STRING="dbname=mowgli" export HELM_TMP_DIR=/tmp unset http_proxy diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml index 668bf1502..db637554f 100644 --- a/helm/gTopLevel/termEditor.ml +++ b/helm/gTopLevel/termEditor.ml @@ -51,7 +51,7 @@ class type term_editor = method environment : DisambiguatingParser.EnvironmentP3.t ref end -module Make(C:Disambiguate_types.Callbacks) = +module Make(C:DisambiguateTypes.Callbacks) = struct module Disambiguate' = DisambiguatingParser.Make(C);; diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli index 67b076505..b3fb94937 100644 --- a/helm/gTopLevel/termEditor.mli +++ b/helm/gTopLevel/termEditor.mli @@ -36,7 +36,7 @@ class type term_editor = method environment : DisambiguatingParser.EnvironmentP3.t ref end -module Make (C : Disambiguate_types.Callbacks) : +module Make (C : DisambiguateTypes.Callbacks) : sig val term_editor : MQIConn.handle -> diff --git a/helm/ocaml/cic_disambiguation/.depend b/helm/ocaml/cic_disambiguation/.depend index 00cb03a9a..0342a9b11 100644 --- a/helm/ocaml/cic_disambiguation/.depend +++ b/helm/ocaml/cic_disambiguation/.depend @@ -1,19 +1,27 @@ -pp.cmi: ast.cmi -disambiguate.cmi: ast.cmi disambiguate_types.cmi -parser.cmi: ast.cmi -disambiguate_types.cmo: disambiguate_types.cmi -disambiguate_types.cmx: disambiguate_types.cmi -pp.cmo: ast.cmi pp.cmi -pp.cmx: ast.cmi pp.cmi +cicTextualParser2Pp.cmi: cicTextualParser2Ast.cmi +disambiguate.cmi: cicTextualParser2Ast.cmi disambiguateTypes.cmi +cicTextualParser2.cmi: cicTextualParser2Ast.cmi +disambiguateTypes.cmo: disambiguateTypes.cmi +disambiguateTypes.cmx: disambiguateTypes.cmi +cicTextualParser2Pp.cmo: cicTextualParser2Ast.cmi cicTextualParser2Pp.cmi +cicTextualParser2Pp.cmx: cicTextualParser2Ast.cmi cicTextualParser2Pp.cmi macro.cmo: macro.cmi macro.cmx: macro.cmi -lexer.cmo: macro.cmi lexer.cmi -lexer.cmx: macro.cmx lexer.cmi -parser.cmo: ast.cmi lexer.cmi parser.cmi -parser.cmx: ast.cmi lexer.cmx parser.cmi -disambiguate.cmo: ast.cmi disambiguate_types.cmi parser.cmi disambiguate.cmi -disambiguate.cmx: ast.cmi disambiguate_types.cmx parser.cmx disambiguate.cmi -logic_notation.cmo: ast.cmi disambiguate.cmi parser.cmi -logic_notation.cmx: ast.cmi disambiguate.cmx parser.cmx -arit_notation.cmo: ast.cmi disambiguate.cmi parser.cmi -arit_notation.cmx: ast.cmi disambiguate.cmx parser.cmx +cicTextualLexer2.cmo: macro.cmi cicTextualLexer2.cmi +cicTextualLexer2.cmx: macro.cmx cicTextualLexer2.cmi +cicTextualParser2.cmo: cicTextualLexer2.cmi cicTextualParser2Ast.cmi \ + cicTextualParser2.cmi +cicTextualParser2.cmx: cicTextualLexer2.cmx cicTextualParser2Ast.cmi \ + cicTextualParser2.cmi +disambiguate.cmo: cicTextualParser2.cmi cicTextualParser2Ast.cmi \ + disambiguateTypes.cmi disambiguate.cmi +disambiguate.cmx: cicTextualParser2.cmx cicTextualParser2Ast.cmi \ + disambiguateTypes.cmx disambiguate.cmi +logic_notation.cmo: cicTextualParser2.cmi cicTextualParser2Ast.cmi \ + disambiguate.cmi +logic_notation.cmx: cicTextualParser2.cmx cicTextualParser2Ast.cmi \ + disambiguate.cmx +arit_notation.cmo: cicTextualParser2.cmi cicTextualParser2Ast.cmi \ + disambiguate.cmi +arit_notation.cmx: cicTextualParser2.cmx cicTextualParser2Ast.cmi \ + disambiguate.cmx diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile index 3a0ae7b80..abfcd4da9 100644 --- a/helm/ocaml/cic_disambiguation/Makefile +++ b/helm/ocaml/cic_disambiguation/Makefile @@ -5,11 +5,19 @@ REQUIRES = \ camlp4.gramlib NOTATIONS = logic arit INTERFACE_FILES = \ - ast.mli pp.mli macro.mli lexer.mli disambiguate.mli parser.mli \ - disambiguate_types.mli + cicTextualParser2Ast.mli \ + cicTextualParser2Pp.mli \ + macro.mli \ + cicTextualLexer2.mli \ + disambiguate.mli \ + cicTextualParser2.mli \ + disambiguateTypes.mli IMPLEMENTATION_FILES = \ - disambiguate_types.ml \ - pp.ml macro.ml lexer.ml parser.ml \ + disambiguateTypes.ml \ + cicTextualParser2Pp.ml \ + macro.ml \ + cicTextualLexer2.ml \ + cicTextualParser2.ml \ disambiguate.ml \ $(patsubst %,%_notation.ml,$(NOTATIONS)) \ @@ -21,12 +29,12 @@ PA_P4_OPTS = q_MLast.cmo pa_extend.cmo all: -lexer.cmo: lexer.ml +cicTextualLexer2.cmo: cicTextualLexer2.ml $(OCAMLC) -pp "camlp4o $(LEXER_P4_OPTS)" -c $< -parser.cmo: parser.ml macro.cmo pa_unicode_macro.cmo +cicTextualParser2.cmo: cicTextualParser2.ml macro.cmo pa_unicode_macro.cmo $(OCAMLC) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< -%_notation.cmo: %_notation.ml parser.cmo +%_notation.cmo: %_notation.ml cicTextualParser2.cmo $(OCAMLC) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< pa_unicode_macro.cmo: pa_unicode_macro.ml macro.cmo @@ -57,8 +65,8 @@ include ../Makefile.common depend: macro.cmi macro.cmo pa_unicode_macro.cmi pa_unicode_macro.cmo $(OCAMLDEP) -pp "camlp4o $(PARSER_P4_OPTS) $(LEXER_P4_OPTS)" $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend -disambiguate_types.cmi: disambiguate_types.mli +disambiguateTypes.cmi: disambiguateTypes.mli $(OCAMLC) -c -rectypes $< -disambiguate_types.cmo: disambiguate_types.ml disambiguate_types.cmi +disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi $(OCAMLC) -c -rectypes $< diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml index b4aaf3398..f0f8d52bc 100644 --- a/helm/ocaml/cic_disambiguation/arit_notation.ml +++ b/helm/ocaml/cic_disambiguation/arit_notation.ml @@ -23,8 +23,8 @@ * http://helm.cs.unibo.it/ *) -open Ast -open Parser +open CicTextualParser2Ast +open CicTextualParser2 (* let i = ref max_int diff --git a/helm/ocaml/cic_disambiguation/ast.mli b/helm/ocaml/cic_disambiguation/ast.mli deleted file mode 100644 index b7267ee57..000000000 --- a/helm/ocaml/cic_disambiguation/ast.mli +++ /dev/null @@ -1,111 +0,0 @@ - - (* when an 'ident option is None, the default is to apply the tactic - to the current goal *) - -type reduction_kind = [ `Reduce | `Simpl | `Whd ] - -type 'term pattern = - | Pattern of 'term - -type location = int * int - -type ('term, 'ident) tactic = - | LocatedTactic of location * ('term, 'ident) tactic - - | Absurd - | Apply of 'term - | Assumption - | Change of 'term * 'term * 'ident option (* what, with what, where *) - | Change_pattern of 'term pattern * 'term * 'ident option - (* what, with what, where *) - | Contradiction - | Cut of 'term - | Decompose of 'ident * 'ident list (* which hypothesis, which principles *) - | Discriminate of 'ident - | Elim of 'term * 'term option (* what to elim, which principle to use *) - | ElimType of 'term - | Exact of 'term - | Exists - | Fold of reduction_kind * 'term - | Fourier - | Injection of 'ident - | Intros of int option - | Left - | LetIn of 'term * 'ident - | Named_intros of 'ident list - | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *) - | Reflexivity - | Replace of 'term * 'term (* what, with what *) - | Replace_pattern of 'term pattern * 'term - | RewriteLeft of 'term * 'ident option - | RewriteRight of 'term * 'ident option - | Right - | Ring - | Split - | Symmetry - | Transitivity of 'term - -type 'tactic tactical = - | LocatedTactical of location * 'tactic tactical - - | Fail - | For of int * 'tactic tactical - | IdTac - | Repeat of 'tactic tactical - | Seq of 'tactic tactical list (* sequential composition *) - | Tactic of 'tactic - | Then of 'tactic tactical * 'tactic tactical list - | Tries of 'tactic tactical list - (* try a sequence of tacticals until one succeeds, fail otherwise *) - | Try of 'tactic tactical (* try a tactical and mask failures *) - -type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] -type induction_kind = [ `Inductive | `CoInductive ] -type sort_kind = [ `Prop | `Set | `Type | `CProp ] - -type case_pattern = string list - -type term = - | LocatedTerm of location * term - - | Appl of term list - | Appl_symbol of string * int * term list (* literal, args, instance *) - | Binder of binder_kind * Cic.name * term option * term - (* kind, name, type, body *) - | Case of term * string * term option * (case_pattern * term) list - (* what to match, inductive type, out type, list *) - | LetIn of string * term * term (* name, body, where *) - | LetRec of induction_kind * (string * term * term option * int) list * term - (* (name, body, type, decreasing argument) list, where *) - | Ident of string * subst list (* literal, substitutions *) - | Meta of int * meta_subst list - | Num of string * int (* literal, instance *) - | Sort of sort_kind - -and meta_subst = term option -and subst = string * term - -(* -type cexpr = - | Symbol of string option * string * (subst option) * string option - (* h:xref, name, subst, definitionURL *) - | LocalVar of string option * string (* h:xref, name *) - | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *) - | Num of string option * string (* h:xref, value *) - | Appl of string option * cexpr list (* h:xref, args *) - | Binder of string option *string * decl * cexpr - (* h:xref, name, decl, body *) - | Letin of string option * def * cexpr (* h:xref, def, body *) - | Letrec of string option * def list * cexpr (* h:xref, def list, body *) - | Case of string option * cexpr * ((string * cexpr) list) - (* h:xref, case_expr, named-pattern list *) -and - decl = string * cexpr (* name, type *) -and - def = string * cexpr (* name, body *) -and - subst = (UriManager.uri * cexpr) list -and - meta_subst = cexpr option list -*) - diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml new file mode 100644 index 000000000..5363d2180 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -0,0 +1,129 @@ +(* 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 blanks = blank+ +let regexp num = digit+ +let regexp tex_token = '\\' alpha+ +let regexp symbol = [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' ] +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 lparen = [ '(' '[' '{' ] +let regexp rparen = [ ')' ']' '}' ] +let regexp meta = '?' num +(* let regexp catchall = .* *) + +let keywords = Hashtbl.create 17 +let _ = + List.iter (fun keyword -> Hashtbl.add keywords keyword ("", keyword)) + [ "Prop"; "Type"; "Set"; "let"; "rec"; "using"; "match"; "with" ] + +let error lexbuf msg = + raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg)) +let error_at_end lexbuf msg = + raise (Error (Ulexing.lexeme_end lexbuf, Ulexing.lexeme_end lexbuf, msg)) + +let return lexbuf token = (token, Ulexing.loc lexbuf) + +(* +let 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 rec token = lexer + | blanks -> token lexbuf + | ident -> + let lexeme = Ulexing.utf8_lexeme lexbuf in + (try + return lexbuf (Hashtbl.find keywords lexeme) + with Not_found -> return lexbuf ("IDENT", lexeme)) + | num -> return lexbuf ("NUM", Ulexing.utf8_lexeme lexbuf) + | lparen -> return lexbuf ("LPAREN", Ulexing.utf8_lexeme lexbuf) + | rparen -> return lexbuf ("RPAREN", Ulexing.utf8_lexeme lexbuf) + | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf) + | symbol -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) + | tex_token -> + let macro = + Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1) + in + (try + return lexbuf ("SYMBOL", Macro.expand macro) + with Macro.Macro_not_found _ -> + return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)) + | eof -> return lexbuf ("EOI", "") + | _ -> error lexbuf "Invalid character" + +let tok_func stream = + let lexbuf = Ulexing.from_utf8_stream stream in + Token.make_stream_and_location + (fun () -> + try + token lexbuf + with + | Ulexing.Error -> error_at_end lexbuf "Unexpected character" + | Ulexing.InvalidCodepoint i -> error_at_end lexbuf "Invalid code point") + +let lex = + { + Token.tok_func = tok_func; + Token.tok_using = (fun _ -> ()); + Token.tok_removing = (fun _ -> ()); + Token.tok_match = Token.default_match; + Token.tok_text = Token.lexer_text; + Token.tok_comm = None; + } diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli b/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli new file mode 100644 index 000000000..f4cbaa1cb --- /dev/null +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli @@ -0,0 +1,29 @@ +(* 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 + +val lex : (string * string) Token.glexer + diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml new file mode 100644 index 000000000..d60e56378 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -0,0 +1,169 @@ +(* 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 = true +let debug_print s = + if debug then begin + prerr_endline ""; + prerr_endline s; + prerr_endline "" + end + +open Printf + +exception Parse_error of string + +let grammar = Grammar.gcreate CicTextualLexer2.lex + +let term = Grammar.Entry.create grammar "term" +(* let tactic = Grammar.Entry.create grammar "tactic" *) +(* let tactical = Grammar.Entry.create grammar "tactical" *) + +let return_term loc term = CicTextualParser2Ast.LocatedTerm (loc, term) +(* let return_term loc term = term *) + +let fail (x, y) msg = + failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) + +EXTEND + GLOBAL: term; + meta_subst: [ + [ s = SYMBOL "_" -> None + | t = term -> Some t ] + ]; + binder: [ + [ SYMBOL <:unicode> (* λ *) -> `Lambda + | SYMBOL <:unicode> (* π *) -> `Pi + | SYMBOL <:unicode> (* ∃ *) -> `Exists + | SYMBOL <:unicode> (* ∀ *) -> `Forall + ] + ]; + substituted_name: [ (* a subs.name is an explicit substitution subject *) + [ s = [ IDENT | SYMBOL ]; + subst = OPT [ + SYMBOL "\subst"; (* to avoid catching frequent "a [1]" cases *) + LPAREN "["; + substs = LIST1 [ + i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) + ] SEP SYMBOL ";"; + RPAREN "]" -> + substs + ] -> + (match subst with + | Some l -> CicTextualParser2Ast.Ident (s, l) + | None -> CicTextualParser2Ast.Ident (s, [])) + ] + ]; + name: [ (* as substituted_name with no explicit substitution *) + [ s = [ IDENT | SYMBOL ] -> s ] + ]; + pattern: [ + [ n = name -> [n] + | LPAREN "("; names = LIST1 name; RPAREN ")" -> names ] + ]; + term: + [ "arrow" RIGHTA + [ t1 = term; SYMBOL <:unicode>; t2 = term -> + return_term loc (CicTextualParser2Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2)) + ] + | "eq" LEFTA + [ t1 = term; SYMBOL "="; t2 = term -> + return_term loc (CicTextualParser2Ast.Appl_symbol ("eq", 0, [t1; t2])) + ] + | "add" LEFTA [ (* nothing here by default *) ] + | "mult" LEFTA [ (* nothing here by default *) ] + | "inv" NONA [ (* nothing here by default *) ] + | "simple" NONA + [ + (* TODO handle "_" *) + b = binder; vars = LIST1 IDENT SEP SYMBOL ","; + typ = OPT [ SYMBOL ":"; t = term -> t ]; + SYMBOL "."; body = term -> + let binder = + List.fold_right + (fun var body -> CicTextualParser2Ast.Binder (b, Cic.Name var, typ, body)) + vars body + in + return_term loc binder + | sort_kind = [ + "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type | "CProp" -> `CProp + ] -> + CicTextualParser2Ast.Sort sort_kind + | n = substituted_name -> return_term loc n + | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" -> + return_term loc (CicTextualParser2Ast.Appl (head :: args)) + | i = NUM -> return_term loc (CicTextualParser2Ast.Num (i, 0)) +(* | i = NUM -> return_term loc (CicTextualParser2Ast.Num (i, Random.int max_int)) *) + | m = META; + substs = [ + LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" -> + 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 (CicTextualParser2Ast.Meta (index, substs)) + (* actually "in" and "and" are _not_ keywords. Parsing works anyway + * since applications are required to be bound by parens *) + | "let"; name = IDENT; SYMBOL <:unicode> (* ≝ *); t1 = term; + IDENT "in"; t2 = term -> + return_term loc (CicTextualParser2Ast.LetIn (name, t1, t2)) + | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; + defs = LIST1 [ + name = IDENT; + index = OPT [ LPAREN "("; index = INT; RPAREN ")" -> + int_of_string index + ]; + typ = OPT [ SYMBOL ":"; typ = term -> typ ]; + SYMBOL <:unicode> (* ≝ *); t1 = term -> + (name, t1, typ, (match index with None -> 1 | Some i -> i)) + ] SEP (IDENT "and"); + IDENT "in"; body = term -> + return_term loc (CicTextualParser2Ast.LetRec (ind_kind, defs, body)) + | outtyp = OPT [ LPAREN "["; typ = term; RPAREN "]" -> typ ]; + "match"; t = term; + SYMBOL ":"; indty = IDENT; + "with"; + LPAREN "["; + patterns = LIST0 [ + p = pattern; SYMBOL <:unicode> (* ⇒ *); t = term -> (p, t) + ] SEP SYMBOL "|"; + RPAREN "]" -> + return_term loc (CicTextualParser2Ast.Case (t, indty, outtyp, patterns)) + | LPAREN "("; t = term; RPAREN ")" -> return_term loc t + ] + ]; +END + +let parse_term stream = + try + Grammar.Entry.parse term stream + with Stdpp.Exc_located ((x, y), exn) -> + raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y + (Printexc.to_string exn))) + diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli new file mode 100644 index 000000000..0d600cc20 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -0,0 +1,40 @@ +(* 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 string + +(** {2 Parsing functions} *) + +val parse_term: char Stream.t -> CicTextualParser2Ast.term + +(** {2 Grammar extensions} *) + +val term: CicTextualParser2Ast.term Grammar.Entry.e + +val return_term: CicTextualParser2Ast.location -> CicTextualParser2Ast.term -> CicTextualParser2Ast.term + + (** raise a parse error *) +val fail: CicTextualParser2Ast.location -> string -> 'a + diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli new file mode 100644 index 000000000..b7267ee57 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli @@ -0,0 +1,111 @@ + + (* when an 'ident option is None, the default is to apply the tactic + to the current goal *) + +type reduction_kind = [ `Reduce | `Simpl | `Whd ] + +type 'term pattern = + | Pattern of 'term + +type location = int * int + +type ('term, 'ident) tactic = + | LocatedTactic of location * ('term, 'ident) tactic + + | Absurd + | Apply of 'term + | Assumption + | Change of 'term * 'term * 'ident option (* what, with what, where *) + | Change_pattern of 'term pattern * 'term * 'ident option + (* what, with what, where *) + | Contradiction + | Cut of 'term + | Decompose of 'ident * 'ident list (* which hypothesis, which principles *) + | Discriminate of 'ident + | Elim of 'term * 'term option (* what to elim, which principle to use *) + | ElimType of 'term + | Exact of 'term + | Exists + | Fold of reduction_kind * 'term + | Fourier + | Injection of 'ident + | Intros of int option + | Left + | LetIn of 'term * 'ident + | Named_intros of 'ident list + | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *) + | Reflexivity + | Replace of 'term * 'term (* what, with what *) + | Replace_pattern of 'term pattern * 'term + | RewriteLeft of 'term * 'ident option + | RewriteRight of 'term * 'ident option + | Right + | Ring + | Split + | Symmetry + | Transitivity of 'term + +type 'tactic tactical = + | LocatedTactical of location * 'tactic tactical + + | Fail + | For of int * 'tactic tactical + | IdTac + | Repeat of 'tactic tactical + | Seq of 'tactic tactical list (* sequential composition *) + | Tactic of 'tactic + | Then of 'tactic tactical * 'tactic tactical list + | Tries of 'tactic tactical list + (* try a sequence of tacticals until one succeeds, fail otherwise *) + | Try of 'tactic tactical (* try a tactical and mask failures *) + +type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] +type induction_kind = [ `Inductive | `CoInductive ] +type sort_kind = [ `Prop | `Set | `Type | `CProp ] + +type case_pattern = string list + +type term = + | LocatedTerm of location * term + + | Appl of term list + | Appl_symbol of string * int * term list (* literal, args, instance *) + | Binder of binder_kind * Cic.name * term option * term + (* kind, name, type, body *) + | Case of term * string * term option * (case_pattern * term) list + (* what to match, inductive type, out type, list *) + | LetIn of string * term * term (* name, body, where *) + | LetRec of induction_kind * (string * term * term option * int) list * term + (* (name, body, type, decreasing argument) list, where *) + | Ident of string * subst list (* literal, substitutions *) + | Meta of int * meta_subst list + | Num of string * int (* literal, instance *) + | Sort of sort_kind + +and meta_subst = term option +and subst = string * term + +(* +type cexpr = + | Symbol of string option * string * (subst option) * string option + (* h:xref, name, subst, definitionURL *) + | LocalVar of string option * string (* h:xref, name *) + | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *) + | Num of string option * string (* h:xref, value *) + | Appl of string option * cexpr list (* h:xref, args *) + | Binder of string option *string * decl * cexpr + (* h:xref, name, decl, body *) + | Letin of string option * def * cexpr (* h:xref, def, body *) + | Letrec of string option * def list * cexpr (* h:xref, def list, body *) + | Case of string option * cexpr * ((string * cexpr) list) + (* h:xref, case_expr, named-pattern list *) +and + decl = string * cexpr (* name, type *) +and + def = string * cexpr (* name, body *) +and + subst = (UriManager.uri * cexpr) list +and + meta_subst = cexpr option list +*) + diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml new file mode 100644 index 000000000..83da77244 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml @@ -0,0 +1,89 @@ +(* 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 CicTextualParser2Ast +open Printf + +let pp_binder = function + | `Lambda -> "lambda" + | `Pi -> "pi" + | `Exists -> "exists" + | `Forall -> "forall" + +let rec pp_term = function + | LocatedTerm ((p_begin, p_end), term) -> +(* sprintf "[%d,%d]%s" p_begin p_end (pp_term term) *) + pp_term term + + | Appl terms -> sprintf "(%s)" (String.concat " " (List.map pp_term terms)) + | Appl_symbol (symbol, _, terms) -> + sprintf "(%s %s)" symbol (String.concat " " (List.map pp_term terms)) + | Binder (kind, var, typ, body) -> + sprintf "\\%s %s%s.%s" (pp_binder kind) + (match var with Cic.Anonymous -> "_" | Cic.Name s -> s) + (match typ with None -> "" | Some typ -> ": " ^ pp_term typ) + (pp_term body) + | Case (term, indtype, typ, patterns) -> + sprintf "%smatch %s with %s" + (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t)) + (pp_term term) (pp_patterns patterns) + | LetIn (name, t1, t2) -> + sprintf "let %s = %s in %s" name (pp_term t1) (pp_term t2) + | LetRec (kind, definitions, term) -> + sprintf "let %s %s in %s" + (match kind with `Inductive -> "rec" | `CoInductive -> "corec") + (String.concat " and " + (List.map + (fun (name, body, typ, index) -> + sprintf "%s%s = %s" name + (match typ with None -> "" | Some typ -> ": " ^ pp_term typ) + (pp_term body)) + definitions)) + (pp_term term) + | Ident (name, []) -> name + | Ident (name, substs) -> sprintf "%s[%s]" name (pp_substs substs) + | Meta (index, substs) -> + sprintf "%d[%s]" index + (String.concat "; " + (List.map (function None -> "_" | Some term -> pp_term term) substs)) + | Num (num, _) -> num + | Sort `Set -> "Set" + | Sort `Prop -> "Prop" + | Sort `Type -> "Type" + | Sort `CProp -> "CProp" + +and pp_subst (name, term) = sprintf "%s := %s" name (pp_term term) +and pp_substs substs = String.concat "; " (List.map pp_subst substs) + +and pp_pattern (names, term) = + sprintf "%s -> %s" + (match names with + | [n] -> n + | names -> "(" ^ String.concat " " names ^ ")") + (pp_term term) + +and pp_patterns patterns = + sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns)) + diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.mli new file mode 100644 index 000000000..555e3272c --- /dev/null +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.mli @@ -0,0 +1,26 @@ +(* 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/ + *) + +val pp_term: CicTextualParser2Ast.term -> string diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 0e2b59079..e64087cf6 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -25,7 +25,7 @@ open Printf -open Disambiguate_types +open DisambiguateTypes open UriManager exception Invalid_choice @@ -96,12 +96,12 @@ let find_in_environment name context = let interpretate ~context ~env ast = let rec aux loc context = function - | Ast.LocatedTerm (loc, term) -> aux loc context term - | Ast.Appl terms -> Cic.Appl (List.map (aux loc context) terms) - | Ast.Appl_symbol (symb, i, args) -> + | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term + | CicTextualParser2Ast.Appl terms -> Cic.Appl (List.map (aux loc context) terms) + | CicTextualParser2Ast.Appl_symbol (symb, i, args) -> let cic_args = List.map (aux loc context) args in resolve env (Symbol (symb, i)) ~args:cic_args () - | Ast.Binder (binder_kind, var, typ, body) -> + | CicTextualParser2Ast.Binder (binder_kind, var, typ, body) -> let cic_type = aux_option loc context typ in let cic_body = aux loc (var :: context) body in (match binder_kind with @@ -110,7 +110,7 @@ let interpretate ~context ~env ast = | `Exists -> resolve env (Symbol ("exists", 0)) ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ()) - | Ast.Case (term, indty_ident, outtype, branches) -> + | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) -> let cic_term = aux loc context term in let cic_outtype = aux_option loc context outtype in let do_branch (pat, term) = @@ -132,12 +132,12 @@ let interpretate ~context ~env ast = in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) - | Ast.LetIn (var, def, body) -> + | CicTextualParser2Ast.LetIn (var, def, body) -> let cic_def = aux loc context def in let name = Cic.Name var in let cic_body = aux loc (name :: context) body in Cic.LetIn (name, cic_def, cic_body) - | Ast.LetRec (kind, defs, body) -> + | CicTextualParser2Ast.LetRec (kind, defs, body) -> let context' = List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc) context defs @@ -169,48 +169,48 @@ let interpretate ~context ~env ast = Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic)) in List.fold_right (build_term inductiveFuns) inductiveFuns cic_body - | Ast.Ident (name, subst) -> + | CicTextualParser2Ast.Ident (name, subst) -> (* TODO hanlde explicit substitutions *) (try let index = find_in_environment name context in if subst <> [] then - Parser.fail loc "Explicit substitutions not allowed here"; + CicTextualParser2.fail loc "Explicit substitutions not allowed here"; Cic.Rel index with Not_found -> resolve env (Id name) ()) - | Ast.Num (num, i) -> resolve env (Num i) ~num () - | Ast.Meta (index, subst) -> + | CicTextualParser2Ast.Num (num, i) -> resolve env (Num i) ~num () + | CicTextualParser2Ast.Meta (index, subst) -> let cic_subst = List.map (function None -> None | Some term -> Some (aux loc context term)) subst in Cic.Meta (index, cic_subst) - | Ast.Sort `Prop -> Cic.Sort Cic.Prop - | Ast.Sort `Set -> Cic.Sort Cic.Set - | Ast.Sort `Type -> Cic.Sort Cic.Type - | Ast.Sort `CProp -> Cic.Sort Cic.CProp + | CicTextualParser2Ast.Sort `Prop -> Cic.Sort Cic.Prop + | CicTextualParser2Ast.Sort `Set -> Cic.Sort Cic.Set + | CicTextualParser2Ast.Sort `Type -> Cic.Sort Cic.Type + | CicTextualParser2Ast.Sort `CProp -> Cic.Sort Cic.CProp and aux_option loc context = function | None -> Cic.Implicit | Some term -> aux loc context term in match ast with - | Ast.LocatedTerm (loc, term) -> aux loc context term + | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term | _ -> assert false let domain_of_term ~context ast = let rec aux loc context = function - | Ast.LocatedTerm (_, term) -> aux loc context term - | Ast.Appl terms -> + | CicTextualParser2Ast.LocatedTerm (_, term) -> aux loc context term + | CicTextualParser2Ast.Appl terms -> List.fold_left (fun dom term -> Domain.union dom (aux loc context term)) Domain.empty terms - | Ast.Appl_symbol (symb, i, args) -> + | CicTextualParser2Ast.Appl_symbol (symb, i, args) -> List.fold_left (fun dom term -> Domain.union dom (aux loc context term)) (Domain.singleton (Symbol (symb, i))) args - | Ast.Binder (_, var, typ, body) -> + | CicTextualParser2Ast.Binder (_, var, typ, body) -> let type_dom = aux_option loc context typ in let body_dom = aux loc (var :: context) body in Domain.union type_dom body_dom - | Ast.Case (term, indty_ident, outtype, branches) -> + | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) -> let term_dom = aux loc context term in let outtype_dom = aux_option loc context outtype in let do_branch (pat, term) = @@ -228,11 +228,11 @@ let domain_of_term ~context ast = in Domain.add (Id indty_ident) (Domain.union outtype_dom (Domain.union term_dom branches_dom)) - | Ast.LetIn (var, body, where) -> + | CicTextualParser2Ast.LetIn (var, body, where) -> let body_dom = aux loc context body in let where_dom = aux loc (Cic.Name var :: context) where in Domain.union body_dom where_dom - | Ast.LetRec (kind, defs, where) -> + | CicTextualParser2Ast.LetRec (kind, defs, where) -> let context' = List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc) context defs @@ -245,26 +245,26 @@ let domain_of_term ~context ast = Domain.empty defs in Domain.union where_dom defs_dom - | Ast.Ident (name, subst) -> + | CicTextualParser2Ast.Ident (name, subst) -> (* TODO hanlde explicit substitutions *) (try let index = find_in_environment name context in if subst <> [] then - Parser.fail loc "Explicit substitutions not allowed here"; + CicTextualParser2.fail loc "Explicit substitutions not allowed here"; Domain.empty with Not_found -> Domain.singleton (Id name)) - | Ast.Num (num, i) -> Domain.singleton (Num i) - | Ast.Meta (index, local_context) -> + | CicTextualParser2Ast.Num (num, i) -> Domain.singleton (Num i) + | CicTextualParser2Ast.Meta (index, local_context) -> List.fold_left (fun dom term -> Domain.union dom (aux_option loc context term)) Domain.empty local_context - | Ast.Sort _ -> Domain.empty + | CicTextualParser2Ast.Sort _ -> Domain.empty and aux_option loc context = function | None -> Domain.empty | Some t -> aux loc context t in match ast with - | Ast.LocatedTerm (loc, term) -> aux loc context term + | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term | _ -> assert false module Make (C: Callbacks) = diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 94690373a..cbc7a54ac 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -open Disambiguate_types +open DisambiguateTypes (** {2 Choice registration interface} *) @@ -47,7 +47,7 @@ module Make (C : Callbacks) : MQIConn.handle -> Cic.context -> Cic.metasenv -> - Ast.term -> + CicTextualParser2Ast.term -> aliases:environment -> (* previous interpretation status *) environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml new file mode 100644 index 000000000..522a08dc0 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -0,0 +1,91 @@ + +type domain_item = + | Id of string (* literal *) + | Symbol of string * int (* literal, instance num *) + | Num of int (* instance num *) + +module OrderedDomain = + struct + type t = domain_item + let compare = Pervasives.compare + end + +module Domain = Set.Make (OrderedDomain) +module Environment = Map.Make (OrderedDomain) + +type codomain_item = + string * (* description *) + (environment -> string -> Cic.term list -> Cic.term) + (* environment, literal number, arguments as needed *) + +and environment = codomain_item Environment.t + +module type Callbacks = + sig + val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit + val interactive_user_uri_choice : + selection_mode:[`SINGLE | `MULTIPLE] -> + ?ok:string -> + ?enable_button_for_non_vars:bool -> + title:string -> msg:string -> id:string -> string list -> string list + val interactive_interpretation_choice : + (string * string) list list -> int + val input_or_locate_uri : title:string -> UriManager.uri + end + +let string_of_domain_item = function + | Id s -> Printf.sprintf "ID(%s)" s + | Symbol (s, i) -> Printf.sprintf "SYMBOL(%s,%d)" s i + | Num i -> Printf.sprintf "NUM(instance %d)" i + +let string_of_domain dom = + let buf = Buffer.create 1024 in + Domain.iter + (fun item -> Buffer.add_string buf (string_of_domain_item 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 + diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli new file mode 100644 index 000000000..a8dda6c39 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -0,0 +1,66 @@ +(* 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/ + *) + +type domain_item = + | Id of string (* literal *) + | Symbol of string * int (* literal, instance num *) + | Num of int (* instance num *) + +module Domain: Set.S with type elt = domain_item +module Environment: Map.S with type key = domain_item + +type codomain_item = + string * (* description *) + (environment -> string -> Cic.term list -> Cic.term) + (* environment, literal number, arguments as needed *) + +and environment = codomain_item Environment.t + +module type Callbacks = + sig + val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit + val interactive_user_uri_choice : + selection_mode:[`SINGLE | `MULTIPLE] -> + ?ok:string -> + ?enable_button_for_non_vars:bool -> + title:string -> msg:string -> id:string -> string list -> string list + val interactive_interpretation_choice : + (string * string) list list -> int + val input_or_locate_uri : title:string -> UriManager.uri + 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 + diff --git a/helm/ocaml/cic_disambiguation/disambiguate_types.ml b/helm/ocaml/cic_disambiguation/disambiguate_types.ml deleted file mode 100644 index 522a08dc0..000000000 --- a/helm/ocaml/cic_disambiguation/disambiguate_types.ml +++ /dev/null @@ -1,91 +0,0 @@ - -type domain_item = - | Id of string (* literal *) - | Symbol of string * int (* literal, instance num *) - | Num of int (* instance num *) - -module OrderedDomain = - struct - type t = domain_item - let compare = Pervasives.compare - end - -module Domain = Set.Make (OrderedDomain) -module Environment = Map.Make (OrderedDomain) - -type codomain_item = - string * (* description *) - (environment -> string -> Cic.term list -> Cic.term) - (* environment, literal number, arguments as needed *) - -and environment = codomain_item Environment.t - -module type Callbacks = - sig - val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit - val interactive_user_uri_choice : - selection_mode:[`SINGLE | `MULTIPLE] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> msg:string -> id:string -> string list -> string list - val interactive_interpretation_choice : - (string * string) list list -> int - val input_or_locate_uri : title:string -> UriManager.uri - end - -let string_of_domain_item = function - | Id s -> Printf.sprintf "ID(%s)" s - | Symbol (s, i) -> Printf.sprintf "SYMBOL(%s,%d)" s i - | Num i -> Printf.sprintf "NUM(instance %d)" i - -let string_of_domain dom = - let buf = Buffer.create 1024 in - Domain.iter - (fun item -> Buffer.add_string buf (string_of_domain_item 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 - diff --git a/helm/ocaml/cic_disambiguation/disambiguate_types.mli b/helm/ocaml/cic_disambiguation/disambiguate_types.mli deleted file mode 100644 index a8dda6c39..000000000 --- a/helm/ocaml/cic_disambiguation/disambiguate_types.mli +++ /dev/null @@ -1,66 +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/ - *) - -type domain_item = - | Id of string (* literal *) - | Symbol of string * int (* literal, instance num *) - | Num of int (* instance num *) - -module Domain: Set.S with type elt = domain_item -module Environment: Map.S with type key = domain_item - -type codomain_item = - string * (* description *) - (environment -> string -> Cic.term list -> Cic.term) - (* environment, literal number, arguments as needed *) - -and environment = codomain_item Environment.t - -module type Callbacks = - sig - val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit - val interactive_user_uri_choice : - selection_mode:[`SINGLE | `MULTIPLE] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> msg:string -> id:string -> string list -> string list - val interactive_interpretation_choice : - (string * string) list list -> int - val input_or_locate_uri : title:string -> UriManager.uri - 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 - diff --git a/helm/ocaml/cic_disambiguation/lexer.ml b/helm/ocaml/cic_disambiguation/lexer.ml deleted file mode 100644 index 5363d2180..000000000 --- a/helm/ocaml/cic_disambiguation/lexer.ml +++ /dev/null @@ -1,129 +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 blanks = blank+ -let regexp num = digit+ -let regexp tex_token = '\\' alpha+ -let regexp symbol = [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' ] -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 lparen = [ '(' '[' '{' ] -let regexp rparen = [ ')' ']' '}' ] -let regexp meta = '?' num -(* let regexp catchall = .* *) - -let keywords = Hashtbl.create 17 -let _ = - List.iter (fun keyword -> Hashtbl.add keywords keyword ("", keyword)) - [ "Prop"; "Type"; "Set"; "let"; "rec"; "using"; "match"; "with" ] - -let error lexbuf msg = - raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg)) -let error_at_end lexbuf msg = - raise (Error (Ulexing.lexeme_end lexbuf, Ulexing.lexeme_end lexbuf, msg)) - -let return lexbuf token = (token, Ulexing.loc lexbuf) - -(* -let 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 rec token = lexer - | blanks -> token lexbuf - | ident -> - let lexeme = Ulexing.utf8_lexeme lexbuf in - (try - return lexbuf (Hashtbl.find keywords lexeme) - with Not_found -> return lexbuf ("IDENT", lexeme)) - | num -> return lexbuf ("NUM", Ulexing.utf8_lexeme lexbuf) - | lparen -> return lexbuf ("LPAREN", Ulexing.utf8_lexeme lexbuf) - | rparen -> return lexbuf ("RPAREN", Ulexing.utf8_lexeme lexbuf) - | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf) - | symbol -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) - | tex_token -> - let macro = - Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1) - in - (try - return lexbuf ("SYMBOL", Macro.expand macro) - with Macro.Macro_not_found _ -> - return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)) - | eof -> return lexbuf ("EOI", "") - | _ -> error lexbuf "Invalid character" - -let tok_func stream = - let lexbuf = Ulexing.from_utf8_stream stream in - Token.make_stream_and_location - (fun () -> - try - token lexbuf - with - | Ulexing.Error -> error_at_end lexbuf "Unexpected character" - | Ulexing.InvalidCodepoint i -> error_at_end lexbuf "Invalid code point") - -let lex = - { - Token.tok_func = tok_func; - Token.tok_using = (fun _ -> ()); - Token.tok_removing = (fun _ -> ()); - Token.tok_match = Token.default_match; - Token.tok_text = Token.lexer_text; - Token.tok_comm = None; - } diff --git a/helm/ocaml/cic_disambiguation/lexer.mli b/helm/ocaml/cic_disambiguation/lexer.mli deleted file mode 100644 index f4cbaa1cb..000000000 --- a/helm/ocaml/cic_disambiguation/lexer.mli +++ /dev/null @@ -1,29 +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 - -val lex : (string * string) Token.glexer - diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml index 2f404be83..011462f81 100644 --- a/helm/ocaml/cic_disambiguation/logic_notation.ml +++ b/helm/ocaml/cic_disambiguation/logic_notation.ml @@ -23,8 +23,8 @@ * http://helm.cs.unibo.it/ *) -open Ast -open Parser +open CicTextualParser2Ast +open CicTextualParser2 EXTEND term: LEVEL "add" diff --git a/helm/ocaml/cic_disambiguation/parser.ml b/helm/ocaml/cic_disambiguation/parser.ml deleted file mode 100644 index 8b53c3aac..000000000 --- a/helm/ocaml/cic_disambiguation/parser.ml +++ /dev/null @@ -1,169 +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 = true -let debug_print s = - if debug then begin - prerr_endline ""; - prerr_endline s; - prerr_endline "" - end - -open Printf - -exception Parse_error of string - -let grammar = Grammar.gcreate Lexer.lex - -let term = Grammar.Entry.create grammar "term" -(* let tactic = Grammar.Entry.create grammar "tactic" *) -(* let tactical = Grammar.Entry.create grammar "tactical" *) - -let return_term loc term = Ast.LocatedTerm (loc, term) -(* let return_term loc term = term *) - -let fail (x, y) msg = - failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) - -EXTEND - GLOBAL: term; - meta_subst: [ - [ s = SYMBOL "_" -> None - | t = term -> Some t ] - ]; - binder: [ - [ SYMBOL <:unicode> (* λ *) -> `Lambda - | SYMBOL <:unicode> (* π *) -> `Pi - | SYMBOL <:unicode> (* ∃ *) -> `Exists - | SYMBOL <:unicode> (* ∀ *) -> `Forall - ] - ]; - substituted_name: [ (* a subs.name is an explicit substitution subject *) - [ s = [ IDENT | SYMBOL ]; - subst = OPT [ - SYMBOL "\subst"; (* to avoid catching frequent "a [1]" cases *) - LPAREN "["; - substs = LIST1 [ - i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) - ] SEP SYMBOL ";"; - RPAREN "]" -> - substs - ] -> - (match subst with - | Some l -> Ast.Ident (s, l) - | None -> Ast.Ident (s, [])) - ] - ]; - name: [ (* as substituted_name with no explicit substitution *) - [ s = [ IDENT | SYMBOL ] -> s ] - ]; - pattern: [ - [ n = name -> [n] - | LPAREN "("; names = LIST1 name; RPAREN ")" -> names ] - ]; - term: - [ "arrow" RIGHTA - [ t1 = term; SYMBOL <:unicode>; t2 = term -> - return_term loc (Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2)) - ] - | "eq" LEFTA - [ t1 = term; SYMBOL "="; t2 = term -> - return_term loc (Ast.Appl_symbol ("eq", 0, [t1; t2])) - ] - | "add" LEFTA [ (* nothing here by default *) ] - | "mult" LEFTA [ (* nothing here by default *) ] - | "inv" NONA [ (* nothing here by default *) ] - | "simple" NONA - [ - (* TODO handle "_" *) - b = binder; vars = LIST1 IDENT SEP SYMBOL ","; - typ = OPT [ SYMBOL ":"; t = term -> t ]; - SYMBOL "."; body = term -> - let binder = - List.fold_right - (fun var body -> Ast.Binder (b, Cic.Name var, typ, body)) - vars body - in - return_term loc binder - | sort_kind = [ - "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type | "CProp" -> `CProp - ] -> - Ast.Sort sort_kind - | n = substituted_name -> return_term loc n - | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" -> - return_term loc (Ast.Appl (head :: args)) - | i = NUM -> return_term loc (Ast.Num (i, 0)) -(* | i = NUM -> return_term loc (Ast.Num (i, Random.int max_int)) *) - | m = META; - substs = [ - LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" -> - 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 (Ast.Meta (index, substs)) - (* actually "in" and "and" are _not_ keywords. Parsing works anyway - * since applications are required to be bound by parens *) - | "let"; name = IDENT; SYMBOL <:unicode> (* ≝ *); t1 = term; - IDENT "in"; t2 = term -> - return_term loc (Ast.LetIn (name, t1, t2)) - | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; - defs = LIST1 [ - name = IDENT; - index = OPT [ LPAREN "("; index = INT; RPAREN ")" -> - int_of_string index - ]; - typ = OPT [ SYMBOL ":"; typ = term -> typ ]; - SYMBOL <:unicode> (* ≝ *); t1 = term -> - (name, t1, typ, (match index with None -> 1 | Some i -> i)) - ] SEP (IDENT "and"); - IDENT "in"; body = term -> - return_term loc (Ast.LetRec (ind_kind, defs, body)) - | outtyp = OPT [ LPAREN "["; typ = term; RPAREN "]" -> typ ]; - "match"; t = term; - SYMBOL ":"; indty = IDENT; - "with"; - LPAREN "["; - patterns = LIST0 [ - p = pattern; SYMBOL <:unicode> (* ⇒ *); t = term -> (p, t) - ] SEP SYMBOL "|"; - RPAREN "]" -> - return_term loc (Ast.Case (t, indty, outtyp, patterns)) - | LPAREN "("; t = term; RPAREN ")" -> return_term loc t - ] - ]; -END - -let parse_term stream = - try - Grammar.Entry.parse term stream - with Stdpp.Exc_located ((x, y), exn) -> - raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y - (Printexc.to_string exn))) - diff --git a/helm/ocaml/cic_disambiguation/parser.mli b/helm/ocaml/cic_disambiguation/parser.mli deleted file mode 100644 index 7f855a459..000000000 --- a/helm/ocaml/cic_disambiguation/parser.mli +++ /dev/null @@ -1,40 +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 string - -(** {2 Parsing functions} *) - -val parse_term: char Stream.t -> Ast.term - -(** {2 Grammar extensions} *) - -val term: Ast.term Grammar.Entry.e - -val return_term: Ast.location -> Ast.term -> Ast.term - - (** raise a parse error *) -val fail: Ast.location -> string -> 'a - diff --git a/helm/ocaml/cic_disambiguation/pp.ml b/helm/ocaml/cic_disambiguation/pp.ml deleted file mode 100644 index 081a7ab19..000000000 --- a/helm/ocaml/cic_disambiguation/pp.ml +++ /dev/null @@ -1,89 +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 Ast -open Printf - -let pp_binder = function - | `Lambda -> "lambda" - | `Pi -> "pi" - | `Exists -> "exists" - | `Forall -> "forall" - -let rec pp_term = function - | LocatedTerm ((p_begin, p_end), term) -> -(* sprintf "[%d,%d]%s" p_begin p_end (pp_term term) *) - pp_term term - - | Appl terms -> sprintf "(%s)" (String.concat " " (List.map pp_term terms)) - | Appl_symbol (symbol, _, terms) -> - sprintf "(%s %s)" symbol (String.concat " " (List.map pp_term terms)) - | Binder (kind, var, typ, body) -> - sprintf "\\%s %s%s.%s" (pp_binder kind) - (match var with Cic.Anonymous -> "_" | Cic.Name s -> s) - (match typ with None -> "" | Some typ -> ": " ^ pp_term typ) - (pp_term body) - | Case (term, indtype, typ, patterns) -> - sprintf "%smatch %s with %s" - (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t)) - (pp_term term) (pp_patterns patterns) - | LetIn (name, t1, t2) -> - sprintf "let %s = %s in %s" name (pp_term t1) (pp_term t2) - | LetRec (kind, definitions, term) -> - sprintf "let %s %s in %s" - (match kind with `Inductive -> "rec" | `CoInductive -> "corec") - (String.concat " and " - (List.map - (fun (name, body, typ, index) -> - sprintf "%s%s = %s" name - (match typ with None -> "" | Some typ -> ": " ^ pp_term typ) - (pp_term body)) - definitions)) - (pp_term term) - | Ident (name, []) -> name - | Ident (name, substs) -> sprintf "%s[%s]" name (pp_substs substs) - | Meta (index, substs) -> - sprintf "%d[%s]" index - (String.concat "; " - (List.map (function None -> "_" | Some term -> pp_term term) substs)) - | Num (num, _) -> num - | Sort `Set -> "Set" - | Sort `Prop -> "Prop" - | Sort `Type -> "Type" - | Sort `CProp -> "CProp" - -and pp_subst (name, term) = sprintf "%s := %s" name (pp_term term) -and pp_substs substs = String.concat "; " (List.map pp_subst substs) - -and pp_pattern (names, term) = - sprintf "%s -> %s" - (match names with - | [n] -> n - | names -> "(" ^ String.concat " " names ^ ")") - (pp_term term) - -and pp_patterns patterns = - sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns)) - diff --git a/helm/ocaml/cic_disambiguation/pp.mli b/helm/ocaml/cic_disambiguation/pp.mli deleted file mode 100644 index 44fa63323..000000000 --- a/helm/ocaml/cic_disambiguation/pp.mli +++ /dev/null @@ -1,26 +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/ - *) - -val pp_term: Ast.term -> string diff --git a/helm/ocaml/cic_disambiguation/tests/eq.txt b/helm/ocaml/cic_disambiguation/tests/eq.txt new file mode 100644 index 000000000..6a826fc71 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/tests/eq.txt @@ -0,0 +1 @@ +\forall n. \forall m. n + m = n