Explicit Named Substitutions now supported.

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 110f3d75ea1578b8f5ae2eb7735a48e61147eeae..d37819c6aa82a1f1a93dc91a473ee54c75367064 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -174,7 +174,61 @@ let interpretate ~context ~env ast =
             CicTextualParser2.fail loc
               "Explicit substitutions not allowed here";
           Cic.Rel index
-        with Not_found -> resolve env (Id name) ())
+        with Not_found ->
+          let cic = resolve env (Id name) () in
+          let mk_subst uris =
+            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
+         in
+          (match cic with
+          | Cic.Const (uri, []) ->
+              let uris =
+                match CicEnvironment.get_obj uri with
+                | Cic.Constant (_, _, _, uris) -> uris
+                | _ -> assert false
+              in
+              Cic.Const (uri, mk_subst uris)
+          | Cic.Var (uri, []) ->
+              let uris =
+                match CicEnvironment.get_obj uri with
+                | Cic.Variable (_, _, _, uris) -> uris
+                | _ -> assert false
+              in
+              Cic.Var (uri, mk_subst uris)
+          | Cic.MutInd (uri, i, []) ->
+              let uris =
+                match CicEnvironment.get_obj uri with
+                | Cic.InductiveDefinition (_, uris, _) -> uris
+                | _ -> assert false
+              in
+              Cic.MutInd (uri, i, mk_subst uris)
+          | Cic.MutConstruct (uri, i, j, []) ->
+              let uris =
+                match CicEnvironment.get_obj uri with
+                | Cic.InductiveDefinition (_, uris, _) -> uris
+                | _ -> assert false
+              in
+              Cic.MutConstruct (uri, i, j, mk_subst uris)
+          | Cic.Meta _ | Cic.Implicit _ as t ->
+(*
+              prerr_endline (sprintf
+                "Warning: %s must be instantiated with _[%s] but we do not enforce it"
+                (CicPp.ppterm t)
+                (String.concat "; "
+                  (List.map
+                    (fun (s, term) -> s ^ " := " ^ CicAstPp.pp_term term)
+                    subst)));
+*)
+              t
+          | _ ->
+              raise DisambiguateChoices.Invalid_choice))
     | CicAst.Implicit -> Cic.Implicit None
     | CicAst.Num (num, i) -> resolve env (Num i) ~num ()
     | CicAst.Meta (index, subst) ->
@@ -256,7 +310,12 @@ let domain_of_term ~context ast =
             CicTextualParser2.fail loc
               "Explicit substitutions not allowed here";
           []
-        with Not_found -> [ Id name ])
+        with Not_found ->
+          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) ->