X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser.mly;h=b85be0754e7194cd9efc140d365d4295339915c6;hb=faf328f5779a7281c9c0588680b1b7bb89ae7640;hp=3f6afc79a4685838fd9bb90a3f3990fe98119c5b;hpb=d45449ce9166ba5c323dfafcc653bc301d6c7a54;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index 3f6afc79a..b85be0754 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -46,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
@@ -151,7 +181,19 @@ expr2:
          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 }