The Makefile stuff has been modified because of ocamllex and ocamlyacc rules.
META.helm-cic_cache
META.helm-xml
META.helm-cic_proof_checking
+META.helm-cic_textual_parser
Makefile
Makefile.common
configure
--- /dev/null
+requires="helm-cic"
+version="0.0.1"
+archive(byte)="cic_textual_parser.cma"
+archive(native)="cic_textual_parser.cmxa"
+linkopts=""
# $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@
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))
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)
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)
# 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@
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
cicAnnotationParser.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
+EXTRA_OBJECTS_TO_CLEAN =
include ../Makefile.common
INTERFACE_FILES = cicCache.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
+EXTRA_OBJECTS_TO_CLEAN =
include ../Makefile.common
INTERFACE_FILES = cicCache.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
+EXTRA_OBJECTS_TO_CLEAN =
include ../Makefile.common
--- /dev/null
+*.cm[iaox] *.cmxa cicTextualParser.ml cicTextualParser.mli cicTextualLexer.ml
--- /dev/null
+cicTextualParser.cmo: cicTextualParser0.cmo cicTextualParser.cmi
+cicTextualParser.cmx: cicTextualParser0.cmx cicTextualParser.cmi
+cicTextualLexer.cmo: cicTextualParser.cmi
+cicTextualLexer.cmx: cicTextualParser.cmx
--- /dev/null
+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
--- /dev/null
+{
+ 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 }
+{}
--- /dev/null
+%{
+ 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 <string> ID
+%token <int> META
+%token <int> NUM
+%token <UriManager.uri> CONURI
+%token <UriManager.uri * int> INDTYURI
+%token <UriManager.uri * int * int> 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 <Cic.term option> 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))
+ }
--- /dev/null
+exception Eof;;
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
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
INTERFACE_FILES = uriManager.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
+EXTRA_OBJECTS_TO_CLEAN =
include ../Makefile.common
INTERFACE_FILES = xml.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
+EXTRA_OBJECTS_TO_CLEAN =
include ../Makefile.common
projects / helm.git / commitdiff