+ L.Number_alias (instance, dsc)
+ ]
+ ];
+ argument: [
+ [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
+ id = IDENT ->
+ N.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 -> N.UriPattern (UriManager.uri_of_string u)
+ | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
+ | IMPLICIT -> N.ImplicitPattern
+ | id = IDENT -> N.VarPattern id
+ | LPAREN; terms = LIST1 SELF; RPAREN ->
+ (match terms with
+ | [] -> assert false
+ | [term] -> term
+ | terms -> N.ApplPattern terms)
+ ]
+ ];
+ interpretation: [
+ [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
+ (s, args, t)
+ ]
+ ];
+
+ include_command: [ [
+ IDENT "include" ; path = QSTRING ->
+ loc,path,true,L.WithPreferences
+ | IDENT "include" ; IDENT "source" ; path = QSTRING ->
+ loc,path,false,L.WithPreferences
+ | IDENT "include'" ; path = QSTRING ->
+ loc,path,true,L.WithoutPreferences
+ ]];
+
+ grafite_ncommand: [ [
+ IDENT "nqed" -> G.NQed loc
+ | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
+ | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
+ body = term ->
+ G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
+ | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
+ G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
+ | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
+ paramspec = OPT inverter_param_list ;
+ outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
+ G.NInverter (loc,name,indty,paramspec,outsort)
+ | NLETCOREC ; defs = let_defs ->
+ nmk_rec_corec `CoInductive defs loc
+ | NLETREC ; defs = let_defs ->
+ nmk_rec_corec `Inductive defs loc
+ | IDENT "ninductive"; spec = inductive_spec ->
+ let (params, ind_types) = spec in
+ G.NObj (loc, N.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
+ G.NObj (loc, N.Inductive (params, ind_types))
+ | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
+ SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
+ let urify = function
+ | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
+ NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
+ | _ -> raise (Failure "only a Type[…] sort can be constrained")
+ in
+ let u1 = urify u1 in
+ let u2 = urify u2 in
+ G.NUnivConstraint (loc,u1,u2)
+ | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
+ G.UnificationHint (loc, t, n)
+ | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
+ SYMBOL <:unicode<def>>; t = term; "on";
+ id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
+ "to"; target = term ->
+ G.NCoercion(loc,name,t,ty,(id,source),target)
+ | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
+ G.NObj (loc, N.Record (params,name,ty,fields))
+ | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
+ m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
+ G.NCopy (loc,s,NUri.uri_of_string u,
+ List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
+ ]];