From 0195d58340f7dbc852d380a8fee897e1c1f7da03 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 10 Jan 2002 16:52:05 +0000 Subject: [PATCH] CIC Textual Parser added to the repository. The Makefile stuff has been modified because of ocamllex and ocamlyacc rules. --- helm/ocaml/.cvsignore | 1 + helm/ocaml/META.helm-cic_textual_parser.src | 5 + helm/ocaml/Makefile.common.in | 16 +- helm/ocaml/Makefile.in | 2 +- helm/ocaml/cic/Makefile | 1 + helm/ocaml/cic_annotations/Makefile | 1 + helm/ocaml/cic_annotations_cache/Makefile | 1 + helm/ocaml/cic_cache/Makefile | 1 + helm/ocaml/cic_textual_parser/.cvsignore | 1 + helm/ocaml/cic_textual_parser/.depend | 4 + helm/ocaml/cic_textual_parser/Makefile | 14 ++ .../cic_textual_parser/cicTextualLexer.mll | 62 +++++++ .../cic_textual_parser/cicTextualParser.mly | 151 ++++++++++++++++++ .../cic_textual_parser/cicTextualParser0.ml | 1 + helm/ocaml/getter/Makefile | 1 + helm/ocaml/pxp/Makefile | 1 + helm/ocaml/urimanager/Makefile | 1 + helm/ocaml/xml/Makefile | 1 + 18 files changed, 261 insertions(+), 4 deletions(-) create mode 100644 helm/ocaml/META.helm-cic_textual_parser.src create mode 100644 helm/ocaml/cic_textual_parser/.cvsignore create mode 100644 helm/ocaml/cic_textual_parser/.depend create mode 100644 helm/ocaml/cic_textual_parser/Makefile create mode 100644 helm/ocaml/cic_textual_parser/cicTextualLexer.mll create mode 100644 helm/ocaml/cic_textual_parser/cicTextualParser.mly create mode 100644 helm/ocaml/cic_textual_parser/cicTextualParser0.ml diff --git a/helm/ocaml/.cvsignore b/helm/ocaml/.cvsignore index c9325bab1..2e6c28cc3 100644 --- a/helm/ocaml/.cvsignore +++ b/helm/ocaml/.cvsignore @@ -7,6 +7,7 @@ META.helm-urimanager META.helm-cic_cache META.helm-xml META.helm-cic_proof_checking +META.helm-cic_textual_parser Makefile Makefile.common configure diff --git a/helm/ocaml/META.helm-cic_textual_parser.src b/helm/ocaml/META.helm-cic_textual_parser.src new file mode 100644 index 000000000..bc4f2fcd4 --- /dev/null +++ b/helm/ocaml/META.helm-cic_textual_parser.src @@ -0,0 +1,5 @@ +requires="helm-cic" +version="0.0.1" +archive(byte)="cic_textual_parser.cma" +archive(native)="cic_textual_parser.cmxa" +linkopts="" diff --git a/helm/ocaml/Makefile.common.in b/helm/ocaml/Makefile.common.in index c871b5e12..38c43c6d1 100644 --- a/helm/ocaml/Makefile.common.in +++ b/helm/ocaml/Makefile.common.in @@ -5,6 +5,7 @@ # $INTERFACE_FILES # $IMPLEMENTATION_FILES # $EXTRA_OBJECTS_TO_INSTALL +# $EXTRA_OBJECTS_TO_CLEAN # and put in a directory where there is a .depend file. OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ @@ -13,6 +14,8 @@ OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) OCAMLDEP = ocamldep +OCAMLLEX = ocamllex +OCAMLYACC = ocamlyacc LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) @@ -23,6 +26,7 @@ ARCHIVE_OPT = $(PACKAGE).cmxa OBJECTS_TO_INSTALL = $(ARCHIVE) $(ARCHIVE_OPT) $(ARCHIVE_OPT:%.cmxa=%.a) \ $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.cmi) \ $(EXTRA_OBJECTS_TO_INSTALL) +DEPEND_FILES = $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) $(ARCHIVE): $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(LIBRARIES) $(OCAMLC) -a -o $@ $(IMPLEMENTATION_FILES:%.ml=%.cmo) @@ -33,19 +37,25 @@ $(ARCHIVE_OPT): $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(LIBRARIES_OPT) all: $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(ARCHIVE) opt: $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(ARCHIVE_OPT) -depend: +depend: $(DEPEND_FILES) $(OCAMLDEP) $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend -.SUFFIXES: .ml .mli .cmo .cmi .cmx +.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .mly .ml.cmo: $(LIBRARIES) $(OCAMLC) -c $< .mli.cmi: $(LIBRARIES) $(OCAMLC) -c $< .ml.cmx: $(LIBRARIES_OPT) $(OCAMLOPT) -c $< +.mly.ml: + $(OCAMLYACC) $< +.mly.mli: + $(OCAMLYACC) $< +.mll.ml: + $(OCAMLLEX) $< clean: - rm -f *.cm[ioax] *.cmxa *.o *.a + rm -f *.cm[ioax] *.cmxa *.o *.a $(EXTRA_OBJECTS_TO_CLEAN) install: mkdir $(OCAMLFIND_DEST_DIR)/$(PACKAGE) diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index e5d051620..4cf5bb527 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -1,6 +1,6 @@ # Warning: the modules must be in compilation order MODULES = xml urimanager getter pxp cic cic_annotations cic_annotations_cache \ - cic_cache cic_proof_checking + cic_cache cic_proof_checking cic_textual_parser OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ OCAMLFIND_META_DIR = @OCAMLFIND_META_DIR@ diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile index 8847e49b3..c18667dc2 100644 --- a/helm/ocaml/cic/Makefile +++ b/helm/ocaml/cic/Makefile @@ -5,5 +5,6 @@ PREDICATES = INTERFACE_FILES = deannotate.mli cicParser3.mli cicParser2.mli cicParser.mli IMPLEMENTATION_FILES = cic.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi +EXTRA_OBJECTS_TO_CLEAN = include ../Makefile.common diff --git a/helm/ocaml/cic_annotations/Makefile b/helm/ocaml/cic_annotations/Makefile index 865e6c406..2fbfe1bec 100644 --- a/helm/ocaml/cic_annotations/Makefile +++ b/helm/ocaml/cic_annotations/Makefile @@ -6,5 +6,6 @@ INTERFACE_FILES = cicXPath.mli cicAnnotation2Xml.mli cicAnnotationParser2.mli \ cicAnnotationParser.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = include ../Makefile.common diff --git a/helm/ocaml/cic_annotations_cache/Makefile b/helm/ocaml/cic_annotations_cache/Makefile index 5daa8160b..8b80b4f00 100644 --- a/helm/ocaml/cic_annotations_cache/Makefile +++ b/helm/ocaml/cic_annotations_cache/Makefile @@ -5,5 +5,6 @@ PREDICATES = INTERFACE_FILES = cicCache.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = include ../Makefile.common diff --git a/helm/ocaml/cic_cache/Makefile b/helm/ocaml/cic_cache/Makefile index 342124a7b..672f904d3 100644 --- a/helm/ocaml/cic_cache/Makefile +++ b/helm/ocaml/cic_cache/Makefile @@ -5,5 +5,6 @@ PREDICATES = INTERFACE_FILES = cicCache.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = include ../Makefile.common diff --git a/helm/ocaml/cic_textual_parser/.cvsignore b/helm/ocaml/cic_textual_parser/.cvsignore new file mode 100644 index 000000000..b94a8197a --- /dev/null +++ b/helm/ocaml/cic_textual_parser/.cvsignore @@ -0,0 +1 @@ +*.cm[iaox] *.cmxa cicTextualParser.ml cicTextualParser.mli cicTextualLexer.ml diff --git a/helm/ocaml/cic_textual_parser/.depend b/helm/ocaml/cic_textual_parser/.depend new file mode 100644 index 000000000..205e603ec --- /dev/null +++ b/helm/ocaml/cic_textual_parser/.depend @@ -0,0 +1,4 @@ +cicTextualParser.cmo: cicTextualParser0.cmo cicTextualParser.cmi +cicTextualParser.cmx: cicTextualParser0.cmx cicTextualParser.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 new file mode 100644 index 000000000..e797dc219 --- /dev/null +++ b/helm/ocaml/cic_textual_parser/Makefile @@ -0,0 +1,14 @@ +PACKAGE = cic_textual_parser +REQUIRES = helm-cic +PREDICATES = + +INTERFACE_FILES = cicTextualParser.mli +IMPLEMENTATION_FILES = cicTextualParser0.ml $(INTERFACE_FILES:%.mli=%.ml) \ + cicTextualLexer.ml +EXTRA_OBJECTS_TO_INSTALL = cicTextualParser0.ml cicTextualParser0.cmi \ + cicTextualLexer.mll cicTextualParser.mly + +EXTRA_OBJECTS_TO_CLEAN = cicTextualParser.ml cicTextualParser.mli \ + cicTextualLexer.ml + +include ../Makefile.common diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll new file mode 100644 index 000000000..d35a46695 --- /dev/null +++ b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll @@ -0,0 +1,62 @@ +{ + open CicTextualParser;; + module L = Lexing;; + module U = UriManager;; + + let indtyuri_of_uri uri = + let index_sharp = String.index uri '#' in + let index_num = index_sharp + 3 in + (UriManager.uri_of_string (String.sub uri 0 index_sharp), + int_of_string (String.sub uri index_num (String.length uri - index_num)) - 1 + ) + ;; + + let indconuri_of_uri uri = + let index_sharp = String.index uri '#' in + let index_div = String.rindex uri '/' in + let index_con = index_div + 1 in + (UriManager.uri_of_string (String.sub uri 0 index_sharp), + int_of_string + (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1, + int_of_string + (String.sub uri index_con (String.length uri - index_con)) + ) + ;; +} +let num = ['1'-'9']['0'-'9']* | '0' +let ident = ['A'-'Z' 'a'-'z' '_' '-']* +let baseuri = '/'(ident '/')* ident '.' +let conuri = baseuri ("con" | "var") +let indtyuri = baseuri "ind#1/" num +let indconuri = baseuri "ind#1/" num "/" num +let blanks = [' ' '\t' '\n'] +rule token = + parse + blanks { token lexbuf } (* skip blanks *) + | "alias" { ALIAS } + | "Case" { CASE } + | "Fix" { FIX } + | "CoFix" { COFIX } + | "Set" { SET } + | "Prop" { PROP } + | "Type" { TYPE } + | ident { ID (L.lexeme lexbuf) } + | conuri { CONURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) } + | indtyuri { INDTYURI (indtyuri_of_uri ("cic:" ^ L.lexeme lexbuf)) } + | indconuri { INDCONURI (indconuri_of_uri("cic:" ^ L.lexeme lexbuf)) } + | num { NUM (int_of_string (L.lexeme lexbuf)) } + | '?' num { META (int_of_string (L.lexeme lexbuf)) } + | ":>" { CAST } + | ":=" { LETIN } + | '?' { IMPLICIT } + | '(' { LPAREN } + | ')' { RPAREN } + | '{' { LCURLY } + | '}' { RCURLY } + | ';' { SEMICOLON } + | '\\' { LAMBDA } + | '!' { PROD } + | ':' { COLON } + | '.' { DOT } + | eof { EOF } +{} diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly new file mode 100644 index 000000000..844384f62 --- /dev/null +++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly @@ -0,0 +1,151 @@ +%{ + open Cic;; + module U = UriManager;; + + exception InvalidSuffix of string;; + exception InductiveTypeURIExpected;; + + let uri_of_id_map = Hashtbl.create 53;; + + let binders = ref [];; + + let get_index_in_list e = + let rec aux i = + function + [] -> raise Not_found + | he::_ when he = e -> i + | _::tl -> aux (i+1) tl + in + aux 1 +;; +%} +%token ID +%token META +%token NUM +%token CONURI +%token INDTYURI +%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 +%start main +%type main +%% +main: + expr { Some $1 } + | alias { None } + | EOF { raise CicTextualParser0.Eof } +; +expr: + CONURI + { 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) + | "var" -> Var $1 + | _ -> raise (InvalidSuffix suff) + } + | INDTYURI { MutInd (fst $1, 0, snd $1) } + | INDCONURI + { let (uri,tyno,consno) = $1 in MutConstruct (uri, 0, tyno, consno) } + | ID + { try + Rel (get_index_in_list (Name $1) !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) } + | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY + { try + let _ = get_index_in_list (Name $5) !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) + | _ -> raise InductiveTypeURIExpected + } + | FIX ID LCURLY fixfuns RCURLY + { let fixfuns = $4 in + let idx = + let rec find idx = + function + [] -> raise Not_found + | (name,_,_,_)::_ when name = $2 -> idx + | _::tl -> find (idx+1) tl + in + find 0 fixfuns + in + Fix (idx,fixfuns) + } + | COFIX ID LCURLY cofixfuns RCURLY + { let cofixfuns = $4 in + let idx = + let rec find idx = + function + [] -> raise Not_found + | (name,_,_)::_ when name = $2 -> idx + | _::tl -> find (idx+1) tl + in + find 0 cofixfuns + in + CoFix (idx,cofixfuns) + } + | IMPLICIT { Implicit } + | SET { Sort Set } + | PROP { Sort Prop } + | TYPE { Sort Type } + | LPAREN expr CAST expr RPAREN { Cast ($2,$4) } + | META { Meta $1 } + | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) } + | pihead expr + { binders := List.tl !binders ; Prod (fst $1, snd $1,$2) } + | lambdahead expr + { binders := List.tl !binders ; Lambda (fst $1, snd $1,$2) } + | letinhead expr + { binders := List.tl !binders ; LetIn (fst $1, snd $1,$2) } +; +fixfuns: + ID LPAREN NUM RPAREN COLON expr LETIN expr + { [$1,$3,$6,$8] } + | ID LPAREN NUM RPAREN COLON expr LETIN expr SEMICOLON fixfuns + { ($1,$3,$6,$8)::$10 } +; +cofixfuns: + ID COLON expr LETIN expr + { [$1,$3,$5] } + | ID COLON expr LETIN expr SEMICOLON cofixfuns + { ($1,$3,$5)::$7 } +; +pihead: + PROD ID COLON expr DOT + { binders := (Name $2)::!binders ; (Cic.Name $2, $4) } +; +lambdahead: + LAMBDA ID COLON expr DOT + { binders := (Name $2)::!binders ; (Cic.Name $2, $4) } +; +letinhead: + LAMBDA ID LETIN expr DOT + { binders := (Name $2)::!binders ; (Cic.Name $2, $4) } +; +branches: + { [] } + | expr SEMICOLON branches { $1::$3 } + | expr { [$1] } +; +exprlist: + { [] } + | expr exprlist { $1::$2 } +; +alias: + ALIAS ID CONURI + { Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,0)) } + | ALIAS ID INDTYURI + { Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, 0, snd $3)) } + | ALIAS ID INDCONURI + { let uri,indno,consno = $3 in + Hashtbl.add uri_of_id_map $2 (Cic.MutConstruct (uri, 0, indno ,consno)) + } diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml new file mode 100644 index 000000000..7917cbdd0 --- /dev/null +++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml @@ -0,0 +1 @@ +exception Eof;; diff --git a/helm/ocaml/getter/Makefile b/helm/ocaml/getter/Makefile index 32812a747..576b04619 100644 --- a/helm/ocaml/getter/Makefile +++ b/helm/ocaml/getter/Makefile @@ -5,5 +5,6 @@ PREDICATES = INTERFACE_FILES = configuration.mli clientHTTP.mli getter.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = include ../Makefile.common diff --git a/helm/ocaml/pxp/Makefile b/helm/ocaml/pxp/Makefile index 1ccb4244b..b40081f45 100644 --- a/helm/ocaml/pxp/Makefile +++ b/helm/ocaml/pxp/Makefile @@ -5,5 +5,6 @@ PREDICATES = INTERFACE_FILES = csc_pxp_reader.mli pxpUriResolver.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = include ../Makefile.common diff --git a/helm/ocaml/urimanager/Makefile b/helm/ocaml/urimanager/Makefile index 2f21b369e..8d5691aaf 100644 --- a/helm/ocaml/urimanager/Makefile +++ b/helm/ocaml/urimanager/Makefile @@ -5,5 +5,6 @@ PREDICATES = INTERFACE_FILES = uriManager.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = include ../Makefile.common diff --git a/helm/ocaml/xml/Makefile b/helm/ocaml/xml/Makefile index 502cdc18a..f6c43d228 100644 --- a/helm/ocaml/xml/Makefile +++ b/helm/ocaml/xml/Makefile @@ -5,5 +5,6 @@ PREDICATES = INTERFACE_FILES = xml.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = include ../Makefile.common -- 2.39.2