X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=edc112992121133be7071cb66939920756b6e60d;hb=1fa2e1ad132b280dbf3a0fb670e4e79858a15e6d;hp=657eb5485a811eebd90a3a795ab044d260061949;hpb=f67ef877debe15f14da063eff415fd1748b33e54;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 657eb5485..edc112992 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -58,6 +58,7 @@ let refine metasenv context term =
         debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
         Uncertain
     | _ ->
+        (* TODO we should catch only the RefineFailure excecption *)
         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
         Ko
 
@@ -101,7 +102,7 @@ let interpretate ~context ~env ast =
                 let cic_body = do_branch' (name :: context) tl in
                 let typ =
                   match typ with
-                  | None -> Cic.Implicit
+                  | None -> Cic.Implicit (Some `Type)
                   | Some typ -> aux loc context typ
                 in
                 Cic.Lambda (name, typ, cic_body)
@@ -111,7 +112,7 @@ let interpretate ~context ~env ast =
         let (indtype_uri, indtype_no) =
           match resolve env (Id indty_ident) () with
           | Cic.MutInd (uri, tyno, _) -> uri, tyno
-          | Cic.Implicit -> raise Try_again
+          | Cic.Implicit _ -> raise Try_again
           | _ -> raise DisambiguateChoices.Invalid_choice
         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
@@ -173,8 +174,62 @@ let interpretate ~context ~env ast =
             CicTextualParser2.fail loc
               "Explicit substitutions not allowed here";
           Cic.Rel index
-        with Not_found -> resolve env (Id name) ())
-    | CicAst.Implicit -> Cic.Implicit
+        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) ->
         let cic_subst =
@@ -190,12 +245,12 @@ let interpretate ~context ~env ast =
     | CicAst.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
   and aux_option loc context = function
-    | None -> Cic.Implicit
+    | None -> Cic.Implicit (Some `Type)
     | Some term -> aux loc context term
   in
   match ast with
   | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
-  | _ -> assert false
+  | term -> aux (-1, -1) context term
 
 let domain_of_term ~context ast =
     (* "aux" keeps domain in reverse order and doesn't care about duplicates.
@@ -255,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) ->
@@ -292,9 +352,10 @@ let domain_of_term ~context ast =
       List.rev uniq_rev_l
   in
             
-  match ast with
-  | CicAst.AttributedTerm (`Loc loc, term) -> rev_uniq (aux loc context term)
-  | _ -> assert false
+  rev_uniq
+    (match ast with
+    | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
+    | term -> aux (-1, -1) context term)
 
 
   (* dom1 \ dom2 *)
@@ -316,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
         | [] ->
@@ -388,7 +449,11 @@ module Make (C: Callbacks) =
         let filled_env =
           List.fold_left
             (fun env item ->
-              Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env)
+              Environment.add item
+                ("Implicit",
+                 (match item with
+                 | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
+                 | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
             current_env todo_dom 
         in
         try