First commit towards more powerful disambiguation possibilities, where

an expression can be disambiguated yelding totally different terms.
Required, for example, to disambiguate operators that have interpretations
with a different arity (as Leibniz equality and the decidable equality over
natural numbers).

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index 5afd56ed9d75e29110c85f12a496b8148e4e8fae..08d85a595a2b03c358f07586ffdd4eb86ab5c30a 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -120,7 +120,7 @@
 
  let var_uri_of_id id interp =
   let module CTP0 = CicTextualParser0 in
-   match interp id with
+   match interp (CicTextualParser0.Id id) with
       None -> raise (UnknownIdentifier id)
     | Some (CTP0.Uri (CTP0.VarUri uri)) -> uri
     | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
@@ -128,7 +128,7 @@
 
  let indty_uri_of_id id interp =
   let module CTP0 = CicTextualParser0 in
-   match interp id with
+   match interp (CicTextualParser0.Id id) with
       None -> raise (UnknownIdentifier id)
     | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno))) -> (uri,tyno)
     | Some _ -> raise InductiveTypeURIExpected
@@ -159,7 +159,7 @@
 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
 %right ARROW
 %start main
-%type <string list * ((string -> CicTextualParser0.interp_codomain option) -> Cic.term)> main
+%type <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
 %%
 main:
  | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */
@@ -197,22 +197,24 @@ expr2:
      with
       Not_found ->
        let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
-        let dom = union dom1 [$1] in
+        let dom = union dom1 [CicTextualParser0.Id $1] in
          dom,
           function interp ->
-           match interp $1 with
+           match interp (CicTextualParser0.Id $1) with
              None  -> raise (UnknownIdentifier $1)
            | 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 ()) ""
+            | Some (CicTextualParser0.Term mk_term) ->
+               (mk_term interp)
    }
  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
     { let dom1,mk_expr1 = $3 in
       let dom2,mk_expr2 = $7 in
       let dom3,mk_expr3 = $10 in
-       let dom = union dom1 (union dom2 dom3) in
+       let dom = (union  dom1 (union dom2 dom3)) in
         dom,
         function interp ->
          MutCase
@@ -222,7 +224,7 @@ expr2:
     { let dom1,mk_expr1 = $3 in
       let dom2,mk_expr2 = $7 in
       let dom3,mk_expr3 = $10 in
-       let dom = union [$5] (union dom1 (union dom2 dom3)) in
+       let dom = union [CicTextualParser0.Id $5] (union dom1 (union dom2 dom3)) in
         dom,
         function interp ->
          let uri,typeno = indty_uri_of_id $5 interp in
@@ -320,7 +322,7 @@ named_substs :
        dom, function interp -> [$1, mk_expr interp] }
  | ID LETIN expr2
     { let dom1,mk_expr = $3 in
-       let dom = union [$1] dom1 in
+       let dom = union [CicTextualParser0.Id $1] dom1 in
         dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
  | VARURI LETIN expr2 SEMICOLON named_substs
     { let dom1,mk_expr = $3 in
@@ -331,7 +333,7 @@ named_substs :
  | ID LETIN expr2 SEMICOLON named_substs
     { let dom1,mk_expr = $3 in
       let dom2,mk_named_substs = $5 in
-       let dom = union [$1] (union dom1 dom2) in
+       let dom = union [CicTextualParser0.Id $1] (union dom1 dom2) in
         dom,
          function interp ->
           (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
index fab36396087cb41a1ab691e71a9c28f4d4d3a6fd..e75f61bd78212f2e97b4b61adeb380f0a9c9cf25 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
@@ -32,9 +32,15 @@ type uri =
  | IndConUri of UriManager.uri * int * int
 ;;
 
-type interp_codomain =
+type interpretation_domain_item =
+   Id of string
+ | Symbol of string * (string * (interpretation -> Cic.term)) list
+and interpretation_codomain_item =
    Uri of uri
  | Implicit
+ | Term of (interpretation -> Cic.term)
+and interpretation =
+ interpretation_domain_item -> interpretation_codomain_item option
 ;;
 
 let binders = ref ([] : (Cic.name option) list);;

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
index c95e7e2e76b90b25d03f0c31e4f3e1f5ce4a6125..0b8871ee83aeb9a271ad280c45360380cb7d1fd9 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
+++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
@@ -27,6 +27,5 @@ val main :
   context:((Cic.name option) list) ->
   metasenv:Cic.metasenv ->
   (Lexing.lexbuf  -> CicTextualParser.token) -> Lexing.lexbuf ->
-   string list *
-    ((string -> CicTextualParser0.interp_codomain option) ->
-      (Cic.metasenv * Cic.term))
+   CicTextualParser0.interpretation_domain_item list *
+    (CicTextualParser0.interpretation -> (Cic.metasenv * Cic.term))