From 818c90057de4f3ca2e1971b267549fe146b89b6f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 16 Apr 2002 11:34:35 +0000 Subject: [PATCH] * identifiers can now also have digits in them * arrow notation for non-dependent Pi-abstraction introduced. It seems to be bugged w.r.t. application (a problem of priority?) * CicTextualParserContext provides an highly not-reentrant implementation of parsing in a given environment --- helm/ocaml/cic_textual_parser/.depend | 4 + helm/ocaml/cic_textual_parser/Makefile | 2 +- .../cic_textual_parser/cicTextualLexer.mll | 29 ++++- .../cic_textual_parser/cicTextualParser.mly | 100 +++++++++++++----- .../cic_textual_parser/cicTextualParser0.ml | 28 +++++ .../cicTextualParserContext.ml | 33 ++++++ .../cicTextualParserContext.mli | 29 +++++ 7 files changed, 199 insertions(+), 26 deletions(-) create mode 100644 helm/ocaml/cic_textual_parser/cicTextualParserContext.ml create mode 100644 helm/ocaml/cic_textual_parser/cicTextualParserContext.mli diff --git a/helm/ocaml/cic_textual_parser/.depend b/helm/ocaml/cic_textual_parser/.depend index 205e603ec..0301adb27 100644 --- a/helm/ocaml/cic_textual_parser/.depend +++ b/helm/ocaml/cic_textual_parser/.depend @@ -1,4 +1,8 @@ cicTextualParser.cmo: cicTextualParser0.cmo cicTextualParser.cmi cicTextualParser.cmx: cicTextualParser0.cmx cicTextualParser.cmi +cicTextualParserContext.cmo: cicTextualParser.cmi cicTextualParser0.cmo \ + cicTextualParserContext.cmi +cicTextualParserContext.cmx: cicTextualParser.cmx cicTextualParser0.cmx \ + cicTextualParserContext.cmi cicTextualLexer.cmo: cicTextualParser.cmi cicTextualLexer.cmx: cicTextualParser.cmx diff --git a/helm/ocaml/cic_textual_parser/Makefile b/helm/ocaml/cic_textual_parser/Makefile index e797dc219..8863155b0 100644 --- a/helm/ocaml/cic_textual_parser/Makefile +++ b/helm/ocaml/cic_textual_parser/Makefile @@ -2,7 +2,7 @@ PACKAGE = cic_textual_parser REQUIRES = helm-cic PREDICATES = -INTERFACE_FILES = cicTextualParser.mli +INTERFACE_FILES = cicTextualParser.mli cicTextualParserContext.mli IMPLEMENTATION_FILES = cicTextualParser0.ml $(INTERFACE_FILES:%.mli=%.ml) \ cicTextualLexer.ml EXTRA_OBJECTS_TO_INSTALL = cicTextualParser0.ml cicTextualParser0.cmi \ diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll index d35a46695..107ff356f 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll +++ b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll @@ -1,3 +1,28 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + { open CicTextualParser;; module L = Lexing;; @@ -24,7 +49,8 @@ ;; } let num = ['1'-'9']['0'-'9']* | '0' -let ident = ['A'-'Z' 'a'-'z' '_' '-']* +let alfa = ['A'-'Z' 'a'-'z' '_' '-'] +let ident = alfa (alfa | num)* let baseuri = '/'(ident '/')* ident '.' let conuri = baseuri ("con" | "var") let indtyuri = baseuri "ind#1/" num @@ -58,5 +84,6 @@ rule token = | '!' { PROD } | ':' { COLON } | '.' { DOT } + | "->" { ARROW } | eof { EOF } {} diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly index 42869a299..b322831cc 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly +++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly @@ -1,3 +1,28 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + %{ open Cic;; module U = UriManager;; @@ -7,8 +32,6 @@ let uri_of_id_map = Hashtbl.create 53;; - let binders = ref [];; - let get_index_in_list e = let rec aux i = function @@ -18,6 +41,11 @@ in aux 1 ;; + + let get_cookingno uri = + UriManager.relative_depth !CicTextualParser0.current_uri uri 0 + ;; + %} %token ID %token META @@ -27,7 +55,7 @@ %token INDCONURI %token ALIAS %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT -%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE EOF +%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW EOF %start main %type main %% @@ -41,30 +69,38 @@ expr: { let uri = UriManager.string_of_uri $1 in let suff = (String.sub uri (String.length uri - 3) 3) in match suff with - "con" -> Const ($1,0) + "con" -> + let cookingno = get_cookingno $1 in + Const ($1,cookingno) | "var" -> Var $1 | _ -> raise (InvalidSuffix suff) } - | INDTYURI { MutInd (fst $1, 0, snd $1) } + | INDTYURI + { let cookingno = get_cookingno (fst $1) in + MutInd (fst $1, cookingno, snd $1) } | INDCONURI - { let (uri,tyno,consno) = $1 in MutConstruct (uri, 0, tyno, consno) } + { let (uri,tyno,consno) = $1 in + let cookingno = get_cookingno uri in + MutConstruct (uri, cookingno, tyno, consno) } | ID { try - Rel (get_index_in_list (Name $1) !binders) + Rel (get_index_in_list (Name $1) !CicTextualParser0.binders) with Not_found -> Hashtbl.find uri_of_id_map $1 } | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY - { MutCase (fst $5, 0, snd $5, $7, $3, $10) } + { let cookingno = get_cookingno (fst $5) in + MutCase (fst $5, cookingno, snd $5, $7, $3, $10) } | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY { try - let _ = get_index_in_list (Name $5) !binders in + let _ = get_index_in_list (Name $5) !CicTextualParser0.binders in raise InductiveTypeURIExpected with Not_found -> match Hashtbl.find uri_of_id_map $5 with - MutInd (uri,0,typeno) -> MutCase (uri, 0, typeno, $7, $3, $10) + MutInd (uri,cookingno,typeno) -> + MutCase (uri, cookingno, typeno, $7, $3, $10) | _ -> raise InductiveTypeURIExpected } | fixheader LCURLY exprseplist RCURLY @@ -84,7 +120,7 @@ expr: fixfunsdecls fixfunsbodies in for i = 1 to List.length fixfuns do - binders := List.tl !binders + CicTextualParser0.binders := List.tl !CicTextualParser0.binders done ; Fix (idx,fixfuns) } @@ -105,7 +141,7 @@ expr: cofixfunsdecls cofixfunsbodies in for i = 1 to List.length cofixfuns do - binders := List.tl !binders + CicTextualParser0.binders := List.tl !CicTextualParser0.binders done ; CoFix (idx,cofixfuns) } @@ -117,16 +153,19 @@ expr: | META { Meta $1 } | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) } | pihead expr - { binders := List.tl !binders ; Prod (fst $1, snd $1,$2) } + { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ; + Prod (fst $1, snd $1,$2) } | lambdahead expr - { binders := List.tl !binders ; Lambda (fst $1, snd $1,$2) } + { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ; + Lambda (fst $1, snd $1,$2) } | letinhead expr - { binders := List.tl !binders ; LetIn (fst $1, snd $1,$2) } + { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ; + LetIn (fst $1, snd $1,$2) } ; fixheader: FIX ID LCURLY fixfunsdecl RCURLY { let bs = List.rev_map (function (name,_,_) -> Name name) $4 in - binders := bs@(!binders) ; + CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ; $2,$4 } ; @@ -139,7 +178,7 @@ fixfunsdecl: cofixheader: COFIX ID LCURLY cofixfunsdecl RCURLY { let bs = List.rev_map (function (name,_) -> Name name) $4 in - binders := bs@(!binders) ; + CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ; $2,$4 } ; @@ -150,16 +189,25 @@ cofixfunsdecl: { ($1,$3)::$5 } ; pihead: - PROD ID COLON expr DOT - { binders := (Name $2)::!binders ; (Cic.Name $2, $4) } + PROD ID COLON expr DOT + { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ; + (Cic.Name $2, $4) } + | expr ARROW + { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ; + (Anonimous, $1) } + | LPAREN expr RPAREN ARROW + { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ; + (Anonimous, $2) } ; lambdahead: LAMBDA ID COLON expr DOT - { binders := (Name $2)::!binders ; (Cic.Name $2, $4) } + { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ; + (Cic.Name $2, $4) } ; letinhead: LAMBDA ID LETIN expr DOT - { binders := (Name $2)::!binders ; (Cic.Name $2, $4) } + { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ; + (Cic.Name $2, $4) } ; branches: { [] } @@ -176,10 +224,14 @@ exprseplist: ; alias: ALIAS ID CONURI - { Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,0)) } + { let cookingno = get_cookingno $3 in + Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,cookingno)) } | ALIAS ID INDTYURI - { Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, 0, snd $3)) } + { let cookingno = get_cookingno (fst $3) in + Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, cookingno, snd $3)) } | ALIAS ID INDCONURI { let uri,indno,consno = $3 in - Hashtbl.add uri_of_id_map $2 (Cic.MutConstruct (uri, 0, indno ,consno)) + let cookingno = get_cookingno uri in + Hashtbl.add uri_of_id_map $2 + (Cic.MutConstruct (uri, cookingno, indno ,consno)) } diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml index 7917cbdd0..e89c00d22 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml +++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml @@ -1 +1,29 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + exception Eof;; + +let current_uri = ref (UriManager.uri_of_string "cic:/dummy.con");; +let binders = ref ([] : Cic.name list);; diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml new file mode 100644 index 000000000..ae21e5d2e --- /dev/null +++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml @@ -0,0 +1,33 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + +let main ~current_uri ~context lexer lexbuf = + (* Warning: higly non-reentrant code!!! *) + CicTextualParser0.current_uri := current_uri ; + CicTextualParser0.binders := context ; + let res = CicTextualParser.main lexer lexbuf in + CicTextualParser0.binders := [] ; + res +;; diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli new file mode 100644 index 000000000..7364eb6fc --- /dev/null +++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli @@ -0,0 +1,29 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + +val main : + current_uri:(UriManager.uri) -> context:(Cic.name list) -> + (Lexing.lexbuf -> CicTextualParser.token) -> Lexing.lexbuf -> + Cic.term option -- 2.39.2