From faf328f5779a7281c9c0588680b1b7bb89ae7640 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 29 Jul 2002 15:55:31 +0000
Subject: [PATCH] Updated to use the new parser that creates (stacks of)
 existential variables when an implicit arguments is found.

---
 .../cic_textual_parser/cicTextualParser.mly   | 46 ++++++++++++++++++-
 .../cic_textual_parser/cicTextualParser0.ml   |  1 +
 .../cicTextualParserContext.ml                | 11 +++--
 .../cicTextualParserContext.mli               |  4 +-
 4 files changed, 54 insertions(+), 8 deletions(-)

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 }
diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
index 7a338c249..0a8414734 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
@@ -27,3 +27,4 @@ exception Eof;;
 
 let current_uri = ref (UriManager.uri_of_string "cic:/dummy.con");;
 let binders = ref ([] : (Cic.name option) list);;
+let metasenv = ref ([] : Cic.metasenv);;
diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
index ae21e5d2e..bdf701d80 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
@@ -23,11 +23,14 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let main ~current_uri ~context lexer lexbuf =
+let main ~current_uri ~context ~metasenv lexer lexbuf =
  (* Warning: higly non-reentrant code!!! *)
  CicTextualParser0.current_uri := current_uri ;
  CicTextualParser0.binders := context ;
- let res = CicTextualParser.main lexer lexbuf in
-  CicTextualParser0.binders := [] ;
-  res
+ CicTextualParser0.metasenv := metasenv ;
+ match CicTextualParser.main lexer lexbuf with
+    None -> None
+  | Some res ->
+     CicTextualParser0.binders := [] ;
+     Some (!CicTextualParser0.metasenv,res)
 ;;
diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
index 0ab69cdd5..837628b21 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
+++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
@@ -25,5 +25,5 @@
 
 val main :
   current_uri:(UriManager.uri) -> context:((Cic.name option) list) ->
-   (Lexing.lexbuf  -> CicTextualParser.token) -> Lexing.lexbuf ->
-     Cic.term option
+   metasenv:Cic.metasenv -> (Lexing.lexbuf  -> CicTextualParser.token) ->
+   Lexing.lexbuf -> (Cic.metasenv * Cic.term) option
-- 
2.39.2