added tactic and tactical (still heavily bugged!!!)

[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..06f18080d07466aaccba41ca71b3d83599ae4678 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -110,10 +110,23 @@ let interpretate ~context ~env ast =
           do_branch' context args
         in
         let (indtype_uri, indtype_no) =
-          match resolve env (Id indty_ident) () with
-          | Cic.MutInd (uri, tyno, _) -> uri, tyno
-          | Cic.Implicit _ -> raise Try_again
-          | _ -> raise DisambiguateChoices.Invalid_choice
+          match indty_ident with
+          | Some indty_ident ->
+              (match resolve env (Id indty_ident) () with
+              | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
+              | Cic.Implicit _ -> raise Try_again
+              | _ -> raise DisambiguateChoices.Invalid_choice)
+          | None ->
+              let fst_constructor =
+                match branches with
+                | ((head, _), _) :: _ -> head
+                | [] -> raise DisambiguateChoices.Invalid_choice
+              in
+              (match resolve env (Id fst_constructor) () with
+              | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
+                  (indtype_uri, indtype_no)
+              | Cic.Implicit _ -> raise Try_again
+              | _ -> raise DisambiguateChoices.Invalid_choice)
         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))
@@ -174,7 +187,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) ->
@@ -229,7 +296,8 @@ let domain_of_term ~context ast =
         let branches_dom =
           List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
         in
-        branches_dom @ outtype_dom @ term_dom @ [ Id indty_ident ]
+        branches_dom @ outtype_dom @ term_dom @
+        (match indty_ident with None -> [] | Some ident -> [ Id ident ])
     | CicAst.LetIn ((var, typ), body, where) ->
         let body_dom = aux loc context body in
         let type_dom = aux_option loc context typ in
@@ -256,7 +324,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 +391,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
         | [] ->