X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser.mly;h=af67f1c1454a8a367ef033b3034e1275b4be7aa0;hb=b1fb6b8e1767d775bc452303629e95941d142bea;hp=b322831cc8052f08596c7dbadfe7e7677e6394a9;hpb=818c90057de4f3ca2e1971b267549fe146b89b6f;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index b322831cc..af67f1c14 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000, HELM Team.
+/* Copyright (C) 2000, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -21,7 +21,7 @@
  * 
  * For details, see the HELM World-Wide-Web page,
  * http://cs.unibo.it/helm/.
- *)
+ */
 
 %{
  open Cic;;
@@ -29,6 +29,7 @@
 
  exception InvalidSuffix of string;;
  exception InductiveTypeURIExpected;;
+ exception UnknownIdentifier of string;;
  
  let uri_of_id_map = Hashtbl.create 53;;
 
@@ -36,7 +37,7 @@
   let rec aux i =
    function
       [] -> raise Not_found
-    | he::_ when he = e -> i
+    | (Some he)::_ when he = e -> i
     | _::tl -> aux (i+1) tl
   in
    aux 1
@@ -45,7 +46,37 @@
  let get_cookingno uri =
   UriManager.relative_depth !CicTextualParser0.current_uri uri 0
  ;;
-  
+
+ (* Returns the first meta whose number is above the *)
+ (* number of the higher meta.                       *)
+ (*CSC: cut&pasted from proofEngine.ml *)
+ let new_meta () =
+  let rec aux =
+   function
+      None,[] -> 1
+    | Some n,[] -> n
+    | None,(n,_,_)::tl -> aux (Some n,tl)
+    | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
+  in
+   1 + aux (None,!CicTextualParser0.metasenv)
+ ;;
+
+ (* identity_relocation_list_for_metavariable i canonical_context         *)
+ (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
+ (* where n = List.length [canonical_context]                             *)
+ (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
+ (*CSC: cut&pasted from proofEngine.ml *)
+ let identity_relocation_list_for_metavariable canonical_context =
+  let canonical_context_length = List.length canonical_context in
+   let rec aux =
+    function
+       (_,[]) -> []
+     | (n,None::tl) -> None::(aux ((n+1),tl))
+     | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
+   in
+    aux (1,canonical_context)
+ ;;
+
 %}
 %token <string> ID
 %token <int> META
@@ -54,8 +85,9 @@
 %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 ARROW EOF
+%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
+%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
+%right ARROW
 %start main
 %type <Cic.term option> main
 %%
@@ -64,7 +96,7 @@ main:
  | alias { None }
  | EOF   { raise CicTextualParser0.Eof }
 ;
-expr:
+expr2:
    CONURI
    { let uri = UriManager.string_of_uri $1 in
      let suff = (String.sub uri (String.length uri - 3) 3) in
@@ -87,7 +119,13 @@ expr:
        Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
      with
       Not_found ->
-       Hashtbl.find uri_of_id_map $1
+       try
+        Hashtbl.find uri_of_id_map $1
+       with
+        Not_found ->
+	 match ! CicTextualParser0.locate_object $1 with
+	  | None      -> raise (UnknownIdentifier $1)
+	  | Some term -> Hashtbl.add uri_of_id_map $1 term; term  
    }
  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
     { let cookingno = get_cookingno (fst $5) in
@@ -145,26 +183,42 @@ expr:
          done ;
          CoFix (idx,cofixfuns)
     }
- | IMPLICIT { Implicit }
+ | IMPLICIT
+    { let newmeta = new_meta () in
+       let new_canonical_context = [] in
+        let irl =
+         identity_relocation_list_for_metavariable new_canonical_context
+        in
+         CicTextualParser0.metasenv :=
+          [newmeta, new_canonical_context, Sort Type ;
+           newmeta+1, new_canonical_context, Meta (newmeta,irl);
+           newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
+          ] @ !CicTextualParser0.metasenv ;
+         Meta (newmeta+2,irl)
+    }
  | SET { Sort Set }
  | PROP { Sort Prop }
  | TYPE { Sort Type }
  | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
- | META { Meta $1 }
+ | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) } 
  | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
- | pihead expr 
+;
+expr :
+   pihead expr
     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
       Prod (fst $1, snd $1,$2) }
- | lambdahead expr 
+ | lambdahead expr
     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
       Lambda (fst $1, snd $1,$2) }
- | letinhead expr 
+ | letinhead expr
     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
       LetIn (fst $1, snd $1,$2) }
+ | expr2
+    { $1 }
 ;
 fixheader:
    FIX ID LCURLY fixfunsdecl RCURLY
-    { let bs = List.rev_map (function (name,_,_) -> Name name) $4 in
+    { let bs = List.rev_map (function (name,_,_) -> Some (Name name)) $4 in
        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
        $2,$4
     }
@@ -177,7 +231,7 @@ fixfunsdecl:
 ;
 cofixheader:
    COFIX ID LCURLY cofixfunsdecl RCURLY
-    { let bs = List.rev_map (function (name,_) -> Name name) $4 in
+    { let bs = List.rev_map (function (name,_) -> Some (Name name)) $4 in
        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
        $2,$4
     }
@@ -190,23 +244,23 @@ cofixfunsdecl:
 ;
 pihead:
    PROD ID COLON expr DOT
-    { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
+    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
       (Cic.Name $2, $4) }
- | expr ARROW
-   { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
+ | expr2 ARROW
+   { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
      (Anonimous, $1) }
  | LPAREN expr RPAREN ARROW
-   { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
+   { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
      (Anonimous, $2) }
 ;
 lambdahead:
   LAMBDA ID COLON expr DOT
-   { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
+   { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
      (Cic.Name $2, $4) }
 ;
 letinhead:
   LAMBDA ID LETIN expr DOT
-   { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
+   { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
      (Cic.Name $2, $4) }
 ;
 branches:
@@ -222,6 +276,11 @@ exprseplist:
    expr                        { [$1] }
  | expr SEMICOLON exprseplist  { $1::$3 }
 ;
+substitutionlist:
+                                     { [] }
+ | expr SEMICOLON substitutionlist   { (Some $1)::$3 }
+ | NONE SEMICOLON substitutionlist   { None::$3 }
+;
 alias:
    ALIAS ID CONURI
     { let cookingno = get_cookingno $3 in
@@ -235,3 +294,6 @@ alias:
         Hashtbl.add uri_of_id_map $2
          (Cic.MutConstruct (uri, cookingno, indno ,consno))
     }
+
+
+