From 549387d72420ea749aa6b1faffc2a17dab62ad31 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 9 Dec 2004 17:20:06 +0000 Subject: [PATCH] (first) complete implementation of (mutual) (co)inductive types syntax --- .../cic_disambiguation/cicTextualParser2.ml | 44 +++++++++++++------ 1 file changed, 31 insertions(+), 13 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index a1f431b60..3a5f76b67 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -364,6 +364,29 @@ EXTEND | [ IDENT "theorem" | IDENT "Theorem" ] -> `Theorem ] ]; + inductive_spec: [ [ + fst_name = IDENT; params = LIST0 [ + PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; + typ = term; PAREN ")" -> (names, typ) ]; + SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; + fst_constructors = LIST0 constructor SEP SYMBOL "|"; + tl = OPT [ "with"; + types = LIST1 [ + name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode>; + OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> + (name, true, typ, constructors) ] SEP "with" -> types + ] -> + let params = + List.fold_right + (fun (names, typ) acc -> + (List.map (fun name -> (name, typ)) names) @ acc) + params [] + in + let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in + let tl_ind_types = match tl with None -> [] | Some types -> types in + let ind_types = fst_ind_type :: tl_ind_types in + (params, ind_types) + ] ]; command: [ [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof @@ -375,20 +398,15 @@ EXTEND | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> return_command loc (TacticAst.Theorem (flavour, name, typ, body)) - | [ IDENT "inductive" | IDENT "Inductive" ]; fst_name = IDENT; - params = LIST0 [ - PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; - typ = term; PAREN ")" -> (names, typ) ]; - SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; - fst_constructors = LIST0 constructor SEP SYMBOL "|" -> - let params = - List.fold_right - (fun (names, typ) acc -> - (List.map (fun name -> (name, typ)) names) @ acc) - params [] + | [ IDENT "inductive" | IDENT "Inductive" ]; spec = inductive_spec -> + let (params, ind_types) = spec in + return_command loc (TacticAst.Inductive (params, ind_types)) + | [ IDENT "coinductive" | IDENT "CoInductive" ]; spec = inductive_spec -> + let (params, ind_types) = spec in + let ind_types = (* set inductive flags to false (coinductive) *) + List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) + ind_types in - let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in - let ind_types = [fst_ind_type] in return_command loc (TacticAst.Inductive (params, ind_types)) | [ IDENT "goal" | IDENT "Goal" ]; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> -- 2.39.2