From 5b6965fc326021ec30894846113665d1b01fe8ee Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 28 Oct 2002 10:51:14 +0000 Subject: [PATCH] - parser improved: constant uris and variable uris are now handled differently - the callback function must now return a URI and no more a term - explicit named substitutions (with syntax { V1 := t1 ; ... ; V2 := t2}) implemented --- .../cic_textual_parser/cicTextualLexer.mll | 4 +- .../cic_textual_parser/cicTextualParser.mly | 114 +++++++++++++----- .../cic_textual_parser/cicTextualParser0.ml | 9 +- 3 files changed, 97 insertions(+), 30 deletions(-) diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll index 1be084795..d9b353cd7 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll +++ b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll @@ -52,7 +52,8 @@ let num = ['1'-'9']['0'-'9']* | '0' let alfa = ['A'-'Z' 'a'-'z' '_' ''' '-'] let ident = alfa (alfa | num)* let baseuri = '/'(ident '/')* ident '.' -let conuri = baseuri ("con" | "var") +let conuri = baseuri "con" +let varuri = baseuri "var" let indtyuri = baseuri "ind#1/" num let indconuri = baseuri "ind#1/" num "/" num let blanks = [' ' '\t' '\n'] @@ -68,6 +69,7 @@ rule token = | "Type" { TYPE } | ident { ID (L.lexeme lexbuf) } | conuri { CONURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) } + | varuri { VARURI (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)) } diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly index a039921c2..fc8bd12ba 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly +++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly @@ -30,6 +30,8 @@ exception InvalidSuffix of string;; exception InductiveTypeURIExpected;; exception UnknownIdentifier of string;; + exception ExplicitNamedSubstitutionAppliedToRel;; + exception TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable;; let uri_of_id_map = Hashtbl.create 53;; @@ -41,7 +43,7 @@ | _::tl -> aux (i+1) tl in aux 1 -;; + ;; (* Returns the first meta whose number is above the *) (* number of the higher meta. *) @@ -73,11 +75,54 @@ aux (1,canonical_context) ;; + let term_of_con_uri uri exp_named_subst = + Const (uri,exp_named_subst) + ;; + + let term_of_var_uri uri exp_named_subst = + Var (uri,exp_named_subst) + ;; + + let term_of_indty_uri (uri,tyno) exp_named_subst = + MutInd (uri, tyno, exp_named_subst) + ;; + + let term_of_indcon_uri (uri,tyno,consno) exp_named_subst = + MutConstruct (uri, tyno, consno, exp_named_subst) + ;; + + let term_of_uri uri = + match uri with + CicTextualParser0.ConUri uri -> term_of_con_uri uri + | CicTextualParser0.VarUri uri -> term_of_var_uri uri + | CicTextualParser0.IndTyUri (uri,tyno) -> term_of_indty_uri (uri,tyno) + | CicTextualParser0.IndConUri (uri,tyno,consno) -> + term_of_indcon_uri (uri,tyno,consno) + ;; + + let var_uri_of_id id = + try + (match Hashtbl.find uri_of_id_map id with + CicTextualParser0.VarUri uri -> uri + | _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable + ) + with + Not_found -> + match !CicTextualParser0.locate_object id with + None -> raise (UnknownIdentifier id) + | Some (CicTextualParser0.VarUri uri as varuri) -> + Hashtbl.add uri_of_id_map id varuri; + uri + | Some _ -> + raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable + ;; + %} %token ID %token META %token NUM %token CONURI +%token VARURI %token INDTYURI %token INDCONURI %token ALIAS @@ -93,34 +138,31 @@ main: | EOF { raise CicTextualParser0.Eof } ; expr2: - CONURI - { let uri = UriManager.string_of_uri $1 in - let suff = (String.sub uri (String.length uri - 3) 3) in - match suff with -(*CSC: parsare anche le explicit named substitutions *) - "con" -> Const ($1,[]) - | "var" -> Var ($1,[]) - | _ -> raise (InvalidSuffix suff) - } - | INDTYURI -/*CSC: parsare anche le explicit named substitutions */ - { MutInd (fst $1, snd $1, []) } - | INDCONURI - { let (uri,tyno,consno) = $1 in -(*CSC: parsare anche le explicit named substitutions *) - MutConstruct (uri, tyno, consno, []) } - | ID + CONURI exp_named_subst + { term_of_con_uri $1 $2 } + | VARURI exp_named_subst + { term_of_var_uri $1 $2 } + | INDTYURI exp_named_subst + { term_of_indty_uri $1 $2 } + | INDCONURI exp_named_subst + { term_of_indcon_uri $1 $2 } + | ID exp_named_subst { try + let res = Rel (get_index_in_list (Name $1) !CicTextualParser0.binders) + in + if $2 = [] then res else raise (ExplicitNamedSubstitutionAppliedToRel) with Not_found -> try - Hashtbl.find uri_of_id_map $1 + term_of_uri (Hashtbl.find uri_of_id_map $1) $2 with Not_found -> - match ! CicTextualParser0.locate_object $1 with + match !CicTextualParser0.locate_object $1 with | None -> raise (UnknownIdentifier $1) - | Some term -> Hashtbl.add uri_of_id_map $1 term; term + | Some uri -> + Hashtbl.add uri_of_id_map $1 uri; + term_of_uri uri $2 } | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY { MutCase (fst $5, snd $5, $7, $3, $10) } @@ -131,7 +173,7 @@ expr2: with Not_found -> match Hashtbl.find uri_of_id_map $5 with - MutInd (uri,typeno,_) -> + CicTextualParser0.IndTyUri (uri,typeno) -> MutCase (uri, typeno, $7, $3, $10) | _ -> raise InductiveTypeURIExpected } @@ -197,6 +239,21 @@ expr2: | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) } | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) } ; +exp_named_subst : + { [] } + | LCURLY named_substs RCURLY + { $2 } +; +named_substs : + VARURI LETIN expr2 + { [$1,$3] } + | ID LETIN expr2 + { [var_uri_of_id $1,$3] } + | VARURI LETIN expr2 SEMICOLON named_substs + { ($1,$3)::$5 } + | ID LETIN expr2 SEMICOLON named_substs + { (var_uri_of_id $1,$3)::$5 } +; expr : pihead expr { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ; @@ -277,14 +334,15 @@ substitutionlist: ; alias: ALIAS ID CONURI - { Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,[])) } + { Hashtbl.add uri_of_id_map $2 (CicTextualParser0.ConUri $3) } + | ALIAS ID VARURI + { Hashtbl.add uri_of_id_map $2 (CicTextualParser0.VarUri $3) } | ALIAS ID INDTYURI - { Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, snd $3, [])) } + { Hashtbl.add uri_of_id_map $2 + (CicTextualParser0.IndTyUri (fst $3, snd $3)) + } | ALIAS ID INDCONURI { let uri,indno,consno = $3 in Hashtbl.add uri_of_id_map $2 - (Cic.MutConstruct (uri, indno, consno, [])) + (CicTextualParser0.IndConUri (uri, indno, consno)) } - - - diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml index fe4bf0623..a0738ad7e 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml +++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml @@ -25,10 +25,17 @@ exception Eof;; +type uri = + ConUri of UriManager.uri + | VarUri of UriManager.uri + | IndTyUri of UriManager.uri * int + | IndConUri of UriManager.uri * int * int +;; + let current_uri = ref (UriManager.uri_of_string "cic:/dummy.con");; let binders = ref ([] : (Cic.name option) list);; let metasenv = ref ([] : Cic.metasenv);; -let locate_object = ref ((fun _ -> None):string->Cic.term option);; +let locate_object = ref ((fun _ -> None):string->uri option);; let set_locate_object f = locate_object := f -- 2.39.2