ported to new logger

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 110f3d75ea1578b8f5ae2eb7735a48e61147eeae..edc112992121133be7071cb66939920756b6e60d 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) ->
@@ -318,13 +377,13 @@ module Make (C: Callbacks) =
        (function uri,_ ->
          MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
        ) result in
-      C.output_html (`Msg (`T "Locate query:"));
+      HelmLogger.log (`Msg (`T "Locate query:"));
       MQueryUtil.text_of_query
-       (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
+       (fun s -> HelmLogger.log ~append_NL:false (`Msg (`T s)))
        "" query; 
-      C.output_html (`Msg (`T "Result:"));
+      HelmLogger.log (`Msg (`T "Result:"));
       MQueryUtil.text_of_result
-        (fun s -> C.output_html (`Msg (`T s))) "" result;
+        (fun s -> HelmLogger.log (`Msg (`T s))) "" result;
       let uris' =
        match uris with
         | [] ->