X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=feb161d7fe84aaa022271e5d7338b839a0f9e17b;hb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;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..feb161d7f 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 *) @@ -172,14 +171,16 @@ EXTEND (head, vars) ] ]; + arg: [ + [ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; + SYMBOL ":"; ty = term; PAREN ")" -> names,ty + | name = IDENT -> [name],CicAst.Implicit + ] + ]; let_defs:[ [ defs = LIST1 [ name = IDENT; - args = LIST1 [ - PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; - ty = term; PAREN ")" -> - (names, ty) - ]; + args = LIST1 [arg = arg -> arg]; index_name = OPT [ IDENT "on"; idx = IDENT -> idx ]; ty = OPT [ SYMBOL ":" ; t = term -> t ]; SYMBOL <:unicode> (* ≝ *); @@ -250,6 +251,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 +276,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 +296,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 +325,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 +377,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 +391,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" ]; @@ -450,9 +452,7 @@ EXTEND ] ]; inductive_spec: [ [ - fst_name = IDENT; params = LIST0 [ - PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; - typ = term; PAREN ")" -> (names, typ) ]; + fst_name = IDENT; params = LIST0 [ arg=arg -> arg ]; SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; fst_constructors = LIST0 constructor SEP SYMBOL "|"; tl = OPT [ "with"; @@ -472,15 +472,30 @@ EXTEND let ind_types = fst_ind_type :: tl_ind_types in (params, ind_types) ] ]; - - macro: [[ - [ IDENT "abort" ] -> TacticAst.Abort loc - | [ IDENT "quit" ] -> TacticAst.Quit loc + + record_spec: [ [ + name = IDENT; params = LIST0 [ arg = arg -> arg ] ; + SYMBOL ":"; typ = term; SYMBOL <:unicode>; PAREN "{" ; + fields = LIST0 [ + name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) + ] SEP SYMBOL ";"; PAREN "}" -> + let params = + List.fold_right + (fun (names, typ) acc -> + (List.map (fun name -> (name, typ)) names) @ acc) + params [] + in + (params,name,typ,fields) + ] ]; + + 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 +510,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 -> @@ -537,38 +553,42 @@ EXTEND [ IDENT "set" ]; n = QSTRING; v = QSTRING -> TacticAst.Set (loc, n, v) | [ IDENT "qed" ] -> TacticAst.Qed loc - | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term; + | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - TacticAst.Theorem (loc, flavour, name, typ, body) + TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body)) + | flavour = theorem_flavour; name = IDENT; + body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + TacticAst.Obj (loc,TacticAst.Theorem (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 - TacticAst.Theorem(loc, `Definition, Some name, ty, - Some (CicAst.LetRec (ind_kind, defs, body))) + TacticAst.Obj (loc,TacticAst.Theorem(`Definition, name, ty, + Some (CicAst.LetRec (ind_kind, defs, body)))) | [ IDENT "inductive" ]; spec = inductive_spec -> let (params, ind_types) = spec in - TacticAst.Inductive (loc, params, ind_types) + TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types)) | [ 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 - TacticAst.Inductive (loc, params, ind_types) + TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types)) | [ IDENT "coercion" ] ; name = IDENT -> TacticAst.Coercion (loc, CicAst.Ident (name,Some [])) | [ IDENT "coercion" ] ; name = URI -> TacticAst.Coercion (loc, CicAst.Uri (name,Some [])) | [ IDENT "alias" ]; spec = alias_spec -> TacticAst.Alias (loc, spec) + | [ IDENT "record" ]; (params,name,ty,fields) = record_spec -> + TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields)) ]]; executable: [ @@ -591,6 +611,10 @@ EXTEND | com = comment -> TacticAst.Comment (loc, com) ] ]; + statements: [ + [ l = LIST0 [ statement ] -> l + ] + ]; END let exc_located_wrapper f = @@ -606,6 +630,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)) + (**/**)