let default_associativity = Gramext.NonA
-let mk_rec_corec src ind_kind defs loc =
- let attrs = src, `Definition, `Regular in
+let mk_rec_corec src flavour ind_kind defs loc =
+ let attrs = src, flavour, `Regular in
(loc, N.LetRec (ind_kind, defs, attrs))
-let nmk_rec_corec src ind_kind defs loc index =
- let loc,t = mk_rec_corec src ind_kind defs loc in
+let nmk_rec_corec src flavour ind_kind defs loc index =
+ let loc,t = mk_rec_corec src flavour ind_kind defs loc in
G.NObj (loc,t,index)
let shift_vars binder (vars, ty) bo =
index: [[ b = OPT SYMBOL "-" -> match b with None -> true | _ -> false ]];
source: [[
- src = OPT IDENT "implied" ->
+ src = OPT [ IDENT "implied" ] ->
match src with None -> `Provided | _ -> `Implied
]];
| src = source; IDENT "axiom"; i = index; name = IDENT; SYMBOL ":"; typ = term ->
let attrs = src, `Axiom, `Regular in
G.NObj (loc, N.Theorem (name, typ, None, attrs),i)
- | IDENT "discriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
- | IDENT "inverter"; 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)
- | src = source; LETCOREC ; defs = let_codefs ->
- nmk_rec_corec src `CoInductive defs loc true
- | src = source; LETREC ; defs = let_defs ->
- nmk_rec_corec src `Inductive defs loc true
-(* FG: no source since no i_attr in N.Inductive *)
- | IDENT "inductive"; spec = inductive_spec ->
+ | src = source; IDENT "inductive"; spec = inductive_spec ->
let (params, ind_types) = spec in
- G.NObj (loc, N.Inductive (params, ind_types),true)
-(* FG: no source since no i_attr in N.Inductive *)
- | IDENT "coinductive"; spec = inductive_spec ->
+ G.NObj (loc, N.Inductive (params, ind_types, src),true)
+ | src = source; 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
- G.NObj (loc, N.Inductive (params, ind_types),true)
- | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
+ G.NObj (loc, N.Inductive (params, ind_types, src),true)
+ | src = source; IDENT "record" ; (params,name,ty,fields) = record_spec ->
+ G.NObj (loc, N.Record (params,name,ty,fields,src),true)
+(* FG: new syntax for inductive/coinductive definitions and statements *)
+ | src = source; IDENT "rec"; nflavour = ntheorem_flavour; defs = let_defs ->
+ nmk_rec_corec src nflavour `Inductive defs loc true
+ | src = source; IDENT "corec"; nflavour = ntheorem_flavour; defs = let_codefs ->
+ nmk_rec_corec src nflavour `CoInductive defs loc true
+(**)
+ | LETCOREC ; defs = let_codefs ->
+ nmk_rec_corec `Provided `Definition `CoInductive defs loc true
+ | LETREC ; defs = let_defs ->
+ nmk_rec_corec `Provided `Definition `Inductive defs loc true
+ | IDENT "discriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
+ | IDENT "inverter"; 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)
+ | IDENT "universe"; cyclic = OPT [ IDENT "cyclic" -> () ] ; IDENT "constraint"; u1 = tactic_term;
SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
+ let acyclic = match cyclic with None -> true | Some () -> false in
let urify = function
| NotationPt.AttributedTerm (_, NotationPt.Sort (`NType i)) ->
NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
in
let u1 = urify u1 in
let u2 = urify u2 in
- G.NUnivConstraint (loc,u1,u2)
+ G.NUnivConstraint (loc,acyclic,u1,u2)
| IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
G.UnificationHint (loc, t, n)
| IDENT "coercion"; name = IDENT;
"to"; target = term -> t,ty,(id,source),target ] ->
let compose = compose = None in
G.NCoercion(loc,name,compose,spec)
-(* FG: no source since no i_attr in N.Record *)
- | IDENT "record" ; (params,name,ty,fields) = record_spec ->
- G.NObj (loc, N.Record (params,name,ty,fields),true)
| IDENT "copy" ; 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,