From b029556cbcecb852dfc9cf25801f3dcc0bb762bb Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 13 Feb 2004 13:33:00 +0000
Subject: [PATCH] inductive type ident optional in mutcase

---
 .../cic_disambiguation/cicTextualParser2.ml   |  4 ++--
 helm/ocaml/cic_disambiguation/disambiguate.ml | 24 +++++++++++++++----
 helm/ocaml/cic_transformations/acic2Ast.ml    |  2 +-
 helm/ocaml/cic_transformations/cicAst.ml      |  2 +-
 4 files changed, 23 insertions(+), 9 deletions(-)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 2bcbb88e8..0ac43a11e 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -179,7 +179,7 @@ EXTEND
             return_term loc (CicAst.LetRec (ind_kind, defs, body))
       | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
         "match"; t = term;
-        SYMBOL ":"; indty = IDENT;
+        indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
         "with";
         PAREN "[";
         patterns = LIST0 [
@@ -188,7 +188,7 @@ EXTEND
         ] SEP SYMBOL "|";
         PAREN "]" ->
           return_term loc
-            (CicAst.Case (t, indty, outtyp, patterns))
+            (CicAst.Case (t, indty_ident, outtyp, patterns))
       | PAREN "("; t = term; PAREN ")" -> return_term loc t
       ]
     ];
diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index edc112992..06f18080d 100644
--- 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))
@@ -283,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
diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index fc6d95531..19b6c4b4b 100644
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -166,7 +166,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
               ((name, capture_variables), rhs))
             constructors patterns
         in
-        idref id (Ast.Case (aux te, name, Some (aux ty), patterns))
+        idref id (Ast.Case (aux te, Some name, Some (aux ty), patterns))
     | Cic.AFix (id, no, funs) -> 
         let defs = 
           List.map
diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml
index f5aeb5d84..b992a916c 100644
--- a/helm/ocaml/cic_transformations/cicAst.ml
+++ b/helm/ocaml/cic_transformations/cicAst.ml
@@ -97,7 +97,7 @@ type term =
 
   | Appl of term list
   | Binder of binder_kind * capture_variable * term (* kind, name, body *)
-  | Case of term * string * term option * (case_pattern * term) list
+  | Case of term * string option * term option * (case_pattern * term) list
       (* what to match, inductive type, out type, <pattern,action> list *)
   | LetIn of capture_variable * term * term  (* name, body, where *)
   | LetRec of induction_kind * (capture_variable * term * int) list * term
-- 
2.39.2