From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 23 Dec 2002 21:06:04 +0000 (+0000)
Subject: The interpretation function can now return also "Implicit".
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3ff4c222cac1ed86d6dfc0c622f0cb19c270631d;p=helm.git

The interpretation function can now return also "Implicit".
Useful for incremental ambiguous parsing.
---

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index 1d4bd933d..9f045ed36 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -119,17 +119,33 @@
  ;;
 
  let var_uri_of_id id interp =
-  match interp id with
-     None -> raise (UnknownIdentifier id)
-   | Some (CicTextualParser0.VarUri uri) -> uri
-   | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
+  let module CTP0 = CicTextualParser0 in
+   match interp id with
+      None -> raise (UnknownIdentifier id)
+    | Some (CTP0.Uri (CTP0.VarUri uri)) -> uri
+    | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
  ;;
 
  let indty_uri_of_id id interp =
-  match interp id with
-     None -> raise (UnknownIdentifier id)
-   | Some (CicTextualParser0.IndTyUri (uri,tyno)) -> (uri,tyno)
-   | Some _ -> raise InductiveTypeURIExpected
+  let module CTP0 = CicTextualParser0 in
+   match interp id with
+      None -> raise (UnknownIdentifier id)
+    | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno)) -> (uri,tyno)
+    | Some _ -> raise InductiveTypeURIExpected
+ ;;
+
+ let mk_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 ;
+     [], function _ -> Meta (newmeta+2,irl)
  ;;
 %}
 %token <string> ID
@@ -144,7 +160,7 @@
 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
 %right ARROW
 %start main
-%type <string list * ((string -> CicTextualParser0.uri option) -> Cic.term)> main
+%type <string list * ((string -> CicTextualParser0.interp_codomain option) -> Cic.term)> main
 %%
 main:
  expr EOF { $1 }
@@ -183,7 +199,11 @@ expr2:
           function interp ->
            match interp $1 with
 	      None  -> raise (UnknownIdentifier $1)
-	    | Some uri -> term_of_uri uri (mk_exp_named_subst interp)
+	    | Some (CicTextualParser0.Uri uri) ->
+               term_of_uri uri (mk_exp_named_subst interp)
+            | Some CicTextualParser0.Implicit ->
+               (*CSC: not very clean; to maximize code reusage *)
+               snd (mk_implicit ()) ""
    }
  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
     { let dom1,mk_expr1 = $3 in
@@ -260,18 +280,7 @@ expr2:
              CoFix (idx,fixfuns)
     }
  | 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 ;
-         [], function _ -> Meta (newmeta+2,irl)
-    }
+    { mk_implicit () }
  | SET  { [], function _ -> Sort Set }
  | PROP { [], function _ -> Sort Prop }
  | TYPE { [], function _ -> Sort Type }
diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
index 62bf7f23c..fab363960 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
@@ -32,5 +32,10 @@ type uri =
  | IndConUri of UriManager.uri * int * int
 ;;
 
+type interp_codomain =
+   Uri of uri
+ | Implicit
+;;
+
 let binders = ref ([] : (Cic.name option) list);;
 let metasenv = ref ([] : Cic.metasenv);;
diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
index c83ac03f8..c95e7e2e7 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
+++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
@@ -28,4 +28,5 @@ val main :
   metasenv:Cic.metasenv ->
   (Lexing.lexbuf  -> CicTextualParser.token) -> Lexing.lexbuf ->
    string list *
-    ((string -> CicTextualParser0.uri option) -> (Cic.metasenv * Cic.term))
+    ((string -> CicTextualParser0.interp_codomain option) ->
+      (Cic.metasenv * Cic.term))