end
module Make :
- functor (C : Disambiguate_types.Callbacks) ->
+ functor (C : DisambiguateTypes.Callbacks) ->
sig
val term_editor :
MQIConn.handle ->
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
val of_string : string -> t
end
-module Make (C : Disambiguate_types.Callbacks) :
+module Make (C : DisambiguateTypes.Callbacks) :
sig
val disambiguate_term :
MQIConn.handle ->
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
method environment : DisambiguatingParser.EnvironmentP3.t ref
end
-module Make(C:Disambiguate_types.Callbacks) =
+module Make(C:DisambiguateTypes.Callbacks) =
struct
module Disambiguate' = DisambiguatingParser.Make(C);;
method environment : DisambiguatingParser.EnvironmentP3.t ref
end
-module Make (C : Disambiguate_types.Callbacks) :
+module Make (C : DisambiguateTypes.Callbacks) :
sig
val term_editor :
MQIConn.handle ->
-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
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)) \
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
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 $<
* http://helm.cs.unibo.it/
*)
-open Ast
-open Parser
+open CicTextualParser2Ast
+open CicTextualParser2
(*
let i = ref max_int
+++ /dev/null
-
- (* 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, <pattern,action> 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
-*)
-
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+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;
+ }
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+exception Error of int * int * string
+
+val lex : (string * string) Token.glexer
+
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+let debug = true
+let debug_print s =
+ if debug then begin
+ prerr_endline "<NEW_TEXTUAL_PARSER>";
+ prerr_endline s;
+ prerr_endline "</NEW_TEXTUAL_PARSER>"
+ 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>> (* λ *) -> `Lambda
+ | SYMBOL <:unicode<pi>> (* π *) -> `Pi
+ | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
+ | SYMBOL <:unicode<forall>> (* ∀ *) -> `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<Assign>> (* ≔ *); 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<to>>; 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<def>> (* ≝ *); 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<def>> (* ≝ *); 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<Rightarrow>> (* ⇒ *); 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)))
+
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+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
+
--- /dev/null
+
+ (* 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, <pattern,action> 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
+*)
+
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open 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))
+
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val pp_term: CicTextualParser2Ast.term -> string
open Printf
-open Disambiguate_types
+open DisambiguateTypes
open UriManager
exception Invalid_choice
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
| `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) =
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
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) =
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
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) =
* http://helm.cs.unibo.it/
*)
-open Disambiguate_types
+open DisambiguateTypes
(** {2 Choice registration interface} *)
MQIConn.handle ->
Cic.context ->
Cic.metasenv ->
- Ast.term ->
+ CicTextualParser2Ast.term ->
aliases:environment -> (* previous interpretation status *)
environment * (* new interpretation status *)
Cic.metasenv * (* new metasenv *)
--- /dev/null
+
+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
+
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+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
+
+++ /dev/null
-
-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
-
+++ /dev/null
-(* Copyright (C) 2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-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
-
+++ /dev/null
-(* Copyright (C) 2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-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;
- }
+++ /dev/null
-(* Copyright (C) 2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-exception Error of int * int * string
-
-val lex : (string * string) Token.glexer
-
* http://helm.cs.unibo.it/
*)
-open Ast
-open Parser
+open CicTextualParser2Ast
+open CicTextualParser2
EXTEND
term: LEVEL "add"
+++ /dev/null
-(* Copyright (C) 2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-let debug = true
-let debug_print s =
- if debug then begin
- prerr_endline "<NEW_TEXTUAL_PARSER>";
- prerr_endline s;
- prerr_endline "</NEW_TEXTUAL_PARSER>"
- 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>> (* λ *) -> `Lambda
- | SYMBOL <:unicode<pi>> (* π *) -> `Pi
- | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
- | SYMBOL <:unicode<forall>> (* ∀ *) -> `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<Assign>> (* ≔ *); 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<to>>; 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<def>> (* ≝ *); 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<def>> (* ≝ *); 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<Rightarrow>> (* ⇒ *); 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)))
-
+++ /dev/null
-(* Copyright (C) 2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-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
-
+++ /dev/null
-(* Copyright (C) 2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-open 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))
-
+++ /dev/null
-(* Copyright (C) 2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-val pp_term: Ast.term -> string
--- /dev/null
+\forall n. \forall m. n + m = n
projects / helm.git / commitdiff