From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 2 Mar 2004 17:14:15 +0000 (+0000)
Subject: - ported to latest CicAst.Ident format (Some [] <> None)
X-Git-Tag: v0_0_4~54
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=de34baf0da4b2d4e50eba307e86d518bb3a071cc;p=helm.git

- ported to latest CicAst.Ident format (Some [] <> None)
- unspecified local contexes are now inferred
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 7c8261fae..f530a31be 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -112,9 +112,7 @@ EXTEND
         PAREN "]" ->
           substs
       ] ->
-        (match subst with
-        | Some l -> CicAst.Ident (s, l)
-        | None -> CicAst.Ident (s, []))
+        CicAst.Ident (s, subst)
     ]
   ];
   name: [ (* as substituted_name with no explicit substitution *)
diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index bc78f55ed..6a6ab9b27 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -182,10 +182,9 @@ let interpretate ~context ~env ast =
         in
         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
     | CicAst.Ident (name, subst) ->
-        (* TODO hanlde explicit substitutions *)
         (try
           let index = find_in_environment name context in
-          if subst <> [] then
+          if subst <> None then
             CicTextualParser2.fail loc
               "Explicit substitutions not allowed here";
           Cic.Rel index
@@ -195,12 +194,16 @@ let interpretate ~context ~env ast =
             let ids_to_uris =
               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
             in
-            List.map
-              (fun (s, term) ->
-                (try
-                  List.assoc s ids_to_uris, aux loc context term
-                 with Not_found -> raise DisambiguateChoices.Invalid_choice))
-              subst
+            (match subst with
+            | Some subst ->
+                List.map
+                  (fun (s, term) ->
+                    (try
+                      List.assoc s ids_to_uris, aux loc context term
+                     with Not_found ->
+                       raise DisambiguateChoices.Invalid_choice))
+                  subst
+            | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
          in
           (match cic with
           | Cic.Const (uri, []) ->
@@ -324,19 +327,22 @@ let domain_of_term ~context ast =
         in
         where_dom @ defs_dom
     | CicAst.Ident (name, subst) ->
-        (* TODO hanlde explicit substitutions *)
         (try
           let index = find_in_environment name context in
-          if subst <> [] then
+          if subst <> None then
             CicTextualParser2.fail loc
-              "Explicit substitutions not allowed here";
-          []
+              "Explicit substitutions not allowed here"
+          else
+            []
         with Not_found ->
-          List.fold_left
-            (fun dom (_, term) ->
-              let dom' = aux loc context term in
-              dom' @ dom)
-            [ Id name ] subst)
+          (match subst with
+          | None -> [Id name]
+          | Some subst ->
+              List.fold_left
+                (fun dom (_, term) ->
+                  let dom' = aux loc context term in
+                  dom' @ dom)
+                [Id name] subst))
     | CicAst.Implicit -> []
     | CicAst.Num (num, i) -> [ Num i ]
     | CicAst.Meta (index, local_context) ->