- 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

diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
index 1be084795a11505eb80764da93da88e1ad79d5b6..d9b353cd708164258ac4822074a09b7444f756a3 100644 (file)
--- 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 a039921c20568d3a1f560b7c7ad3f932eace91ea..fc8bd12bae19c94b76a87c2328d7abb5e89cd868 100644 (file)
--- 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 <string> ID
 %token <int> META
 %token <int> NUM
 %token <UriManager.uri> CONURI
+%token <UriManager.uri> VARURI
 %token <UriManager.uri * int> INDTYURI
 %token <UriManager.uri * int * int> 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 fe4bf062346c95b9cf29eaeb692871f4fccab3fd..a0738ad7e36d181b19cfb151e922c500b3d488ad 100644 (file)
--- 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