From b029556cbcecb852dfc9cf25801f3dcc0bb762bb Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli 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, list *) | LetIn of capture_variable * term * term (* name, body, where *) | LetRec of induction_kind * (capture_variable * term * int) list * term -- 2.39.2