X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=4b94226cbe2ae63f2c94ee85eb12d85ed9dfaa4d;hb=c347684900a4e2b17a6c1d372fb142bebd8cd250;hp=5e70ff571ecd62b8a3402da395c8aebee9b5312a;hpb=bc36fe01d5465d07ef76c445c83639e341f3eb2a;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 5e70ff571..4b94226cb 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -69,6 +69,7 @@ let alias_spec = Grammar.Entry.create grammar "alias_spec" let macro = Grammar.Entry.create grammar "macro" let script = Grammar.Entry.create grammar "script" let statement = Grammar.Entry.create grammar "statement" +let statements = Grammar.Entry.create grammar "statements" let return_term loc term = CicAst.AttributedTerm (`Loc loc, term) @@ -116,7 +117,7 @@ let mk_binder_ast binder typ vars body = vars body EXTEND - GLOBAL: term term0 statement; + GLOBAL: term term0 statement statements; int: [ [ num = NUM -> try @@ -147,20 +148,18 @@ EXTEND ] ]; subst: [ - [ subst = OPT [ - SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) - PAREN "["; - substs = LIST1 [ - i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) - ] SEP SYMBOL ";"; - PAREN "]" -> - substs - ] -> subst + [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) + PAREN "["; + substs = LIST1 [ + i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) + ] SEP SYMBOL ";"; + PAREN "]" -> + substs ] ]; substituted_name: [ (* a subs.name is an explicit substitution subject *) - [ s = IDENT; subst = subst -> CicAst.Ident (s, subst) - | s = URI; subst = subst -> CicAst.Uri (ind_expansion s, subst) + [ s = IDENT; subst = OPT subst -> CicAst.Ident (s, subst) + | s = URI; subst = OPT subst -> CicAst.Uri (ind_expansion s, subst) ] ]; name: [ (* as substituted_name with no explicit substitution *) @@ -176,9 +175,10 @@ EXTEND [ defs = LIST1 [ name = IDENT; args = LIST1 [ - PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; - ty = term; PAREN ")" -> - (names, ty) + PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; + SYMBOL ":"; ty = term; PAREN ")" -> + (names, Some ty) + | name = IDENT -> [name],None ]; index_name = OPT [ IDENT "on"; idx = IDENT -> idx ]; ty = OPT [ SYMBOL ":" ; t = term -> t ]; @@ -196,6 +196,12 @@ EXTEND list_of_binder binder ty (binder_of_arg_list binder final_term tl) l in + let args = + List.map + (function + names,Some ty -> names,ty + | names,None -> names,CicAst.Implicit + ) args in let t1' = binder_of_arg_list `Lambda t1 args in let ty' = match ty with @@ -250,6 +256,9 @@ EXTEND b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term -> let binder = mk_binder_ast b typ vars body in return_term loc binder + | b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term -> + let binder = mk_binder_ast b typ vars body in + return_term loc binder | t1 = term; SYMBOL <:unicode> (* → *); t2 = term -> return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2)) ] @@ -272,17 +281,12 @@ EXTEND in CicAst.Appl (aux t1 @ [t2]) ] - | "binder" RIGHTA - [ - b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term -> - let binder = mk_binder_ast b typ vars body in - return_term loc binder - ] | "simple" NONA [ sort = sort -> CicAst.Sort sort | n = substituted_name -> return_term loc n | i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ()))) | IMPLICIT -> return_term loc CicAst.Implicit + | PLACEHOLDER -> return_term loc CicAst.UserInput | m = META; substs = [ PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" -> @@ -297,7 +301,7 @@ EXTEND return_term loc (CicAst.Meta (index, substs)) | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ]; "match"; t = term; - indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ]; + indty_ident = OPT ["in" ; id = IDENT -> id ]; "with"; PAREN "["; patterns = LIST0 [ @@ -326,7 +330,8 @@ EXTEND reduction_kind: [ [ [ IDENT "reduce" ] -> `Reduce | [ IDENT "simplify" ] -> `Simpl - | [ IDENT "whd" ] -> `Whd ] + | [ IDENT "whd" ] -> `Whd + | [ IDENT "normalize" ] -> `Normalize ] ]; tactic: [ [ [ IDENT "absurd" ]; t = tactic_term -> @@ -377,10 +382,10 @@ EXTEND let idents = match idents with None -> [] | Some idents -> idents in TacticAst.Intros (loc, num, idents) | [ IDENT "intro" ] -> - TacticAst.Intros (loc, None, []) + TacticAst.Intros (loc, Some 1, []) | [ IDENT "left" ] -> TacticAst.Left loc - | [ "let" | "Let" ]; - t = tactic_term; "in"; where = IDENT -> + | [ IDENT "letin" ]; + where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> TacticAst.LetIn (loc, t, where) | kind = reduction_kind; pat = OPT [ @@ -391,8 +396,10 @@ EXTEND (match (pat, terms) with | None, [] -> TacticAst.Reduce (loc, kind, None) | None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal)) - | Some pat, [] -> TacticAst.Reduce (loc, kind, Some ([], pat)) + | Some pat, [] -> fail loc "Missing term [list]" | Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat))) + | kind = reduction_kind; where = IDENT ; IDENT "at" ; pat = term -> + TacticAst.ReduceAt (loc, kind, where, pat) | [ IDENT "reflexivity" ] -> TacticAst.Reflexivity loc | [ IDENT "replace" ]; @@ -473,14 +480,14 @@ EXTEND (params, ind_types) ] ]; - macro: [[ - [ IDENT "abort" ] -> TacticAst.Abort loc - | [ IDENT "quit" ] -> TacticAst.Quit loc + macro: [ + [ [ IDENT "quit" ] -> TacticAst.Quit loc +(* | [ IDENT "abort" ] -> TacticAst.Abort loc *) | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name) - | [ IDENT "undo" ]; steps = OPT NUM -> +(* | [ IDENT "undo" ]; steps = OPT NUM -> TacticAst.Undo (loc, int_opt steps) | [ IDENT "redo" ]; steps = OPT NUM -> - TacticAst.Redo (loc, int_opt steps) + TacticAst.Redo (loc, int_opt steps) *) | [ IDENT "check" ]; t = term -> TacticAst.Check (loc, t) | [ IDENT "hint" ] -> TacticAst.Hint loc @@ -495,7 +502,8 @@ EXTEND | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> TacticAst.WHint (loc,t) | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name) - ]]; + ] + ]; alias_spec: [ [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING -> @@ -540,13 +548,15 @@ EXTEND | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> TacticAst.Theorem (loc, flavour, name, typ, body) + | flavour = theorem_flavour; name = OPT IDENT; + body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + TacticAst.Theorem (loc, flavour, name, CicAst.Implicit, body) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = let_defs -> let name,ty = match defs with | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty - | ((Cic.Name name,None),_,_) :: _ -> - fail loc ("No type given for " ^ name) + | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit | _ -> assert false in let body = CicAst.Ident (name,None) in @@ -591,6 +601,10 @@ EXTEND | com = comment -> TacticAst.Comment (loc, com) ] ]; + statements: [ + [ l = LIST0 [ statement ] -> l + ] + ]; END let exc_located_wrapper f = @@ -606,6 +620,9 @@ let parse_term stream = exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream)) let parse_statement stream = exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream)) +let parse_statements stream = + exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream)) + (**/**)