let default_associativity = Gramext.NonA
-let mk_rec_corec ind_kind defs loc =
+let mk_rec_corec ng ind_kind defs loc =
(* In case of mutual definitions here we produce just
the syntax tree for the first one. The others will be
generated from the completely specified term just before
else
`MutualDefinition
in
- GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
+ if ng then
+ GrafiteAst.NObj (loc, Ast.Theorem(flavour, name, ty,
+ Some (Ast.LetRec (ind_kind, defs, body))))
+ else
+ GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
Some (Ast.LetRec (ind_kind, defs, body))))
type by_continuation =
None -> None,[],Some Ast.UserInput
| Some ps -> ps]
];
+ inverter_param_list: [
+ [ params = tactic_term ->
+ let deannotate = function
+ | Ast.AttributedTerm (_,t) | t -> t
+ in match deannotate params with
+ | Ast.Implicit -> [false]
+ | Ast.UserInput -> [true]
+ | Ast.Appl l ->
+ List.map (fun x -> match deannotate x with
+ | Ast.Implicit -> false
+ | Ast.UserInput -> true
+ | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
+ | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
+ ];
direction: [
[ SYMBOL ">" -> `LeftToRight
| SYMBOL "<" -> `RightToLeft ]
using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
ntactic: [
[ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t)
+ | IDENT "nassert";
+ seqs = LIST0 [
+ hyps = LIST0
+ [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
+ | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
+ SYMBOL <:unicode<def>> ; bo = tactic_term ->
+ id,`Def (bo,ty)];
+ SYMBOL <:unicode<vdash>>;
+ concl = tactic_term -> (List.rev hyps,concl) ] ->
+ GrafiteAst.NAssert (loc, seqs)
| IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
GrafiteAst.NCases (loc, what, where)
| IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
GrafiteAst.NChange (loc, what, with_what)
| IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
GrafiteAst.NElim (loc, what, where)
+ | IDENT "ngeneralize"; p=pattern_spec ->
+ GrafiteAst.NGeneralize (loc, p)
+ | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
+ where = pattern_spec ->
+ GrafiteAst.NLetIn (loc,where,t,name)
+ | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
+ GrafiteAst.NRewrite (loc, dir, what, where)
+ | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
+ where = pattern_spec ->
+ let delta = match delta with None -> true | _ -> false in
+ GrafiteAst.NEval (loc, where, `Whd delta)
| SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
+ | SYMBOL "#"; SYMBOL "_" -> GrafiteAst.NIntro (loc,"_")
| SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
| SYMBOL "*"; n=IDENT ->
GrafiteAst.NCase1 (loc,n)
let pattern = match pattern with
| None -> None, [], Some Ast.UserInput
| Some pattern -> pattern
- in
- GrafiteAst.Elim (loc, what, using, pattern, ispecs)
+ in
+ GrafiteAst.Elim (loc, what, using, pattern, ispecs)
| IDENT "elimType"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
GrafiteAst.ElimType (loc, what, using, (num, idents))
raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
("the pattern cannot specify the term to replace, only its"
^ " paths in the hypotheses and in the conclusion")))
- else
+ else
GrafiteAst.Fold (loc, kind, t, p)
| IDENT "fourier" ->
GrafiteAst.Fourier loc
| IDENT "timeout"
| IDENT "library"
| IDENT "type"
+ | IDENT "steps"
+ | IDENT "all"
]
];
auto_params: [
| IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
| LPAREN; tac = SELF; RPAREN -> tac
| tac = tactic -> tac
- ]
- ];
+ ]
+ ];
punctuation_tactical:
[
[ SYMBOL "[" -> GrafiteAst.Branch loc
| IDENT "unfocus" -> GrafiteAst.Unfocus loc
| IDENT "skip" -> GrafiteAst.Skip loc
]
- ];
+ ];
ntheorem_flavour: [
- [ [ IDENT "ntheorem" ] -> `Theorem
+ [ [ IDENT "ndefinition" ] -> `Definition
+ | [ IDENT "nfact" ] -> `Fact
+ | [ IDENT "nlemma" ] -> `Lemma
+ | [ IDENT "nremark" ] -> `Remark
+ | [ IDENT "ntheorem" ] -> `Theorem
]
];
theorem_flavour: [
SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
fst_constructors = LIST0 constructor SEP SYMBOL "|";
tl = OPT [ "with";
- types = LIST1 [
- name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
- 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)
- ] ];
-
- record_spec: [ [
- name = IDENT;
- params = LIST0 protected_binder_vars;
- SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
- fields = LIST0 [
- name = IDENT ;
- coercion = [
- SYMBOL ":" -> false,0
- | SYMBOL ":"; SYMBOL ">" -> true,0
- | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
- ];
- ty = term ->
- let b,n = coercion in
- (name,ty,b,n)
- ] SEP SYMBOL ";"; SYMBOL "}" ->
- 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 "check" ]; t = term ->
- GrafiteAst.Check (loc, t)
- | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
- GrafiteAst.Eval (loc, kind, t)
- | [ IDENT "inline"];
- style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
- suri = QSTRING; prefix = OPT QSTRING;
- flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
- let style = match style with
- | None -> GrafiteAst.Declarative
- | Some depth -> GrafiteAst.Procedural depth
- in
- let prefix = match prefix with None -> "" | Some prefix -> prefix in
- GrafiteAst.Inline (loc,style,suri,prefix, flavour)
- | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
- if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
- | IDENT "auto"; params = auto_params ->
- GrafiteAst.AutoInteractive (loc,params)
- | [ IDENT "whelp"; "match" ] ; t = term ->
- GrafiteAst.WMatch (loc,t)
- | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
- GrafiteAst.WInstance (loc,t)
- | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
- GrafiteAst.WLocate (loc,id)
- | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
- GrafiteAst.WElim (loc, t)
- | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
- GrafiteAst.WHint (loc,t)
- ]
- ];
- alias_spec: [
- [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
- let alpha = "[a-zA-Z]" in
- let num = "[0-9]+" in
- let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
- let decoration = "\\'" in
- let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
- let rex = Str.regexp ("^"^ident^"$") in
- if Str.string_match rex id 0 then
- if (try ignore (UriManager.uri_of_string uri); true
- with UriManager.IllFormedUri _ -> false)
- then
- LexiconAst.Ident_alias (id, uri)
- else
- raise
- (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
- else
- raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
- Printf.sprintf "Not a valid identifier: %s" id)))
- | IDENT "symbol"; symbol = QSTRING;
- instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
- SYMBOL "="; dsc = QSTRING ->
- let instance =
- match instance with Some i -> i | None -> 0
+ types = LIST1 [
+ name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
+ 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
- LexiconAst.Symbol_alias (symbol, instance, dsc)
- | IDENT "num";
- instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
- SYMBOL "="; dsc = QSTRING ->
- let instance =
- match instance with Some i -> i | None -> 0
+ 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)
+ ] ];
+
+ record_spec: [ [
+ name = IDENT;
+ params = LIST0 protected_binder_vars;
+ SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
+ fields = LIST0 [
+ name = IDENT ;
+ coercion = [
+ SYMBOL ":" -> false,0
+ | SYMBOL ":"; SYMBOL ">" -> true,0
+ | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
+ ];
+ ty = term ->
+ let b,n = coercion in
+ (name,ty,b,n)
+ ] SEP SYMBOL ";"; SYMBOL "}" ->
+ let params =
+ List.fold_right
+ (fun (names, typ) acc ->
+ (List.map (fun name -> (name, typ)) names) @ acc)
+ params []
in
- LexiconAst.Number_alias (instance, dsc)
- ]
- ];
- argument: [
- [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
- id = IDENT ->
- Ast.IdentArg (List.length l, id)
- ]
- ];
- associativity: [
- [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
- | IDENT "right"; IDENT "associative" -> Gramext.RightA
- | IDENT "non"; IDENT "associative" -> Gramext.NonA
- ]
- ];
- precedence: [
- [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
- ];
- notation: [
- [ dir = OPT direction; s = QSTRING;
- assoc = OPT associativity; prec = precedence;
- IDENT "for";
- p2 =
- [ blob = UNPARSED_AST ->
- add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
- (CicNotationParser.parse_level2_ast
- (Ulexing.from_utf8_string blob))
- | blob = UNPARSED_META ->
- add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
- (CicNotationParser.parse_level2_meta
- (Ulexing.from_utf8_string blob))
- ] ->
- let assoc =
- match assoc with
- | None -> default_associativity
- | Some assoc -> assoc
+ (params,name,typ,fields)
+ ] ];
+
+ macro: [
+ [ [ IDENT "check" ]; t = term ->
+ GrafiteAst.Check (loc, t)
+ | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
+ GrafiteAst.Eval (loc, kind, t)
+ | [ IDENT "inline"];
+ style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
+ suri = QSTRING; prefix = OPT QSTRING;
+ flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
+ let style = match style with
+ | None -> GrafiteAst.Declarative
+ | Some depth -> GrafiteAst.Procedural depth
+ in
+ let prefix = match prefix with None -> "" | Some prefix -> prefix in
+ GrafiteAst.Inline (loc,style,suri,prefix, flavour)
+ | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
+ if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
+ | IDENT "auto"; params = auto_params ->
+ GrafiteAst.AutoInteractive (loc,params)
+ | [ IDENT "whelp"; "match" ] ; t = term ->
+ GrafiteAst.WMatch (loc,t)
+ | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
+ GrafiteAst.WInstance (loc,t)
+ | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
+ GrafiteAst.WLocate (loc,id)
+ | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
+ GrafiteAst.WElim (loc, t)
+ | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
+ GrafiteAst.WHint (loc,t)
+ ]
+ ];
+ alias_spec: [
+ [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
+ let alpha = "[a-zA-Z]" in
+ let num = "[0-9]+" in
+ let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
+ let decoration = "\\'" in
+ let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
+ let rex = Str.regexp ("^"^ident^"$") in
+ if Str.string_match rex id 0 then
+ if (try ignore (UriManager.uri_of_string uri); true
+ with UriManager.IllFormedUri _ -> false)
+ then
+ LexiconAst.Ident_alias (id, uri)
+ else
+ raise
+ (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
+ else
+ raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
+ Printf.sprintf "Not a valid identifier: %s" id)))
+ | IDENT "symbol"; symbol = QSTRING;
+ instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
+ SYMBOL "="; dsc = QSTRING ->
+ let instance =
+ match instance with Some i -> i | None -> 0
in
- let p1 =
- add_raw_attribute ~text:s
- (CicNotationParser.parse_level1_pattern prec
- (Ulexing.from_utf8_string s))
+ LexiconAst.Symbol_alias (symbol, instance, dsc)
+ | IDENT "num";
+ instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
+ SYMBOL "="; dsc = QSTRING ->
+ let instance =
+ match instance with Some i -> i | None -> 0
in
- (dir, p1, assoc, prec, p2)
- ]
- ];
- level3_term: [
- [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
- | id = IDENT -> Ast.VarPattern id
- | SYMBOL "_" -> Ast.ImplicitPattern
- | LPAREN; terms = LIST1 SELF; RPAREN ->
- (match terms with
- | [] -> assert false
- | [term] -> term
- | terms -> Ast.ApplPattern terms)
- ]
- ];
- interpretation: [
- [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
- (s, args, t)
- ]
- ];
-
- include_command: [ [
- IDENT "include" ; path = QSTRING ->
- loc,path,LexiconAst.WithPreferences
- | IDENT "include'" ; path = QSTRING ->
- loc,path,LexiconAst.WithoutPreferences
- ]];
+ LexiconAst.Number_alias (instance, dsc)
+ ]
+ ];
+ argument: [
+ [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
+ id = IDENT ->
+ Ast.IdentArg (List.length l, id)
+ ]
+ ];
+ associativity: [
+ [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
+ | IDENT "right"; IDENT "associative" -> Gramext.RightA
+ | IDENT "non"; IDENT "associative" -> Gramext.NonA
+ ]
+ ];
+ precedence: [
+ [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
+ ];
+ notation: [
+ [ dir = OPT direction; s = QSTRING;
+ assoc = OPT associativity; prec = precedence;
+ IDENT "for";
+ p2 =
+ [ blob = UNPARSED_AST ->
+ add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
+ (CicNotationParser.parse_level2_ast
+ (Ulexing.from_utf8_string blob))
+ | blob = UNPARSED_META ->
+ add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
+ (CicNotationParser.parse_level2_meta
+ (Ulexing.from_utf8_string blob))
+ ] ->
+ let assoc =
+ match assoc with
+ | None -> default_associativity
+ | Some assoc -> assoc
+ in
+ let p1 =
+ add_raw_attribute ~text:s
+ (CicNotationParser.parse_level1_pattern prec
+ (Ulexing.from_utf8_string s))
+ in
+ (dir, p1, assoc, prec, p2)
+ ]
+ ];
+ level3_term: [
+ [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
+ | id = IDENT -> Ast.VarPattern id
+ | SYMBOL "_" -> Ast.ImplicitPattern
+ | LPAREN; terms = LIST1 SELF; RPAREN ->
+ (match terms with
+ | [] -> assert false
+ | [term] -> term
+ | terms -> Ast.ApplPattern terms)
+ ]
+ ];
+ interpretation: [
+ [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
+ (s, args, t)
+ ]
+ ];
+
+ include_command: [ [
+ IDENT "include" ; path = QSTRING ->
+ loc,path,LexiconAst.WithPreferences
+ | IDENT "include'" ; path = QSTRING ->
+ loc,path,LexiconAst.WithoutPreferences
+ ]];
grafite_command: [ [
IDENT "set"; n = QSTRING; v = QSTRING ->
| IDENT "drop" -> GrafiteAst.Drop loc
| IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
| IDENT "qed" -> GrafiteAst.Qed loc
+ | IDENT "nqed" -> GrafiteAst.NQed loc
| IDENT "variant" ; name = IDENT; SYMBOL ":";
typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
GrafiteAst.Obj (loc,
Ast.Theorem (flavour, name, Ast.Implicit, Some body))
| IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
+ | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
+ GrafiteAst.NObj (loc, Ast.Theorem (`Axiom, name, typ, None))
| LETCOREC ; defs = let_defs ->
- mk_rec_corec `CoInductive defs loc
+ mk_rec_corec false `CoInductive defs loc
| LETREC ; defs = let_defs ->
- mk_rec_corec `Inductive defs loc
+ mk_rec_corec false `Inductive defs loc
+ | NLETCOREC ; defs = let_defs ->
+ mk_rec_corec true `CoInductive defs loc
+ | NLETREC ; defs = let_defs ->
+ mk_rec_corec true `Inductive defs loc
| IDENT "inductive"; spec = inductive_spec ->
let (params, ind_types) = spec in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
+ | IDENT "ninductive"; spec = inductive_spec ->
+ let (params, ind_types) = spec in
+ GrafiteAst.NObj (loc, Ast.Inductive (params, ind_types))
| IDENT "coinductive"; spec = inductive_spec ->
let (params, ind_types) = spec in
let ind_types = (* set inductive flags to false (coinductive) *)
ind_types
in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
+ | IDENT "ncoinductive"; 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
+ GrafiteAst.NObj (loc, Ast.Inductive (params, ind_types))
| IDENT "coercion" ;
t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
arity = OPT int ; saturations = OPT int;
(loc, t, composites, arity, saturations)
| IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
GrafiteAst.PreferCoercion (loc, t)
+ | IDENT "pump" ; steps = int ->
+ GrafiteAst.Pump(loc,steps)
| IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
GrafiteAst.UnificationHint (loc, t, n)
- | IDENT "record" ; (params,name,ty,fields) = record_spec ->
+ | IDENT "inverter"; name = IDENT; IDENT "for";
+ indty = tactic_term; paramspec = inverter_param_list ->
+ GrafiteAst.Inverter
+ (loc, name, indty, paramspec)
+ | IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
let uris = List.map UriManager.uri_of_string uris in
projects / helm.git / blobdiff