aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_constr.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_constr.ml4')
-rw-r--r--parsing/g_constr.ml480
1 files changed, 40 insertions, 40 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index f91f0170c..7e2b41926 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -22,7 +22,7 @@ open Topconstr
open Util
let constr_kw =
- [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
+ [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
"end"; "as"; "let"; "if"; "then"; "else"; "return";
"Prop"; "Set"; "Type"; ".("; "_"; "..";
"`{"; "`("; "{|"; "|}" ]
@@ -39,10 +39,10 @@ let loc_of_binder_let = function
| _ -> dummy_loc
let binders_of_lidents l =
- List.map (fun (loc, id) ->
- LocalRawAssum ([loc, Name id], Default Rawterm.Explicit,
+ List.map (fun (loc, id) ->
+ LocalRawAssum ([loc, Name id], Default Rawterm.Explicit,
CHole (loc, Some (Evd.BinderType (Name id))))) l
-
+
let rec index_and_rec_order_of_annot loc bl ann =
match names_of_local_assums bl,ann with
| [loc,Name id], (None, r) -> Some (loc, id), r
@@ -70,7 +70,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
(id,bl,ty,body)
let mk_fix(loc,kw,id,dcls) =
- if kw then
+ if kw then
let fb = List.map mk_fixb dcls in
CFix(loc,id,fb)
else
@@ -101,16 +101,16 @@ let impl_ident =
Gram.Entry.of_parser "impl_ident"
(fun strm ->
match Stream.npeek 1 strm with
- | [(_,"{")] ->
+ | [(_,"{")] ->
(match Stream.npeek 2 strm with
| [_;("IDENT",("wf"|"struct"|"measure"))] ->
raise Stream.Failure
- | [_;("IDENT",s)] ->
+ | [_;("IDENT",s)] ->
Stream.junk strm; Stream.junk strm;
Names.id_of_string s
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
-
+
let ident_colon =
Gram.Entry.of_parser "ident_colon"
(fun strm ->
@@ -134,7 +134,7 @@ let ident_with =
Names.id_of_string s
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
-
+
let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
GEXTEND Gram
@@ -169,21 +169,21 @@ GEXTEND Gram
[ [ c = operconstr LEVEL "200" -> c ] ]
;
constr:
- [ [ c = operconstr LEVEL "8" -> c
+ [ [ c = operconstr LEVEL "8" -> c
| "@"; f=global -> CAppExpl(loc,(None,f),[]) ] ]
;
operconstr:
[ "200" RIGHTA
[ c = binder_constr -> c ]
| "100" RIGHTA
- [ c1 = operconstr; "<:"; c2 = binder_constr ->
+ [ c1 = operconstr; "<:"; c2 = binder_constr ->
CCast(loc,c1, CastConv (VMcast,c2))
- | c1 = operconstr; "<:"; c2 = SELF ->
+ | c1 = operconstr; "<:"; c2 = SELF ->
CCast(loc,c1, CastConv (VMcast,c2))
- | c1 = operconstr; ":";c2 = binder_constr ->
+ | c1 = operconstr; ":";c2 = binder_constr ->
+ CCast(loc,c1, CastConv (DEFAULTcast,c2))
+ | c1 = operconstr; ":"; c2 = SELF ->
CCast(loc,c1, CastConv (DEFAULTcast,c2))
- | c1 = operconstr; ":"; c2 = SELF ->
- CCast(loc,c1, CastConv (DEFAULTcast,c2))
| c1 = operconstr; ":>" ->
CCast(loc,c1, CastCoerce) ]
| "99" RIGHTA [ ]
@@ -205,7 +205,7 @@ GEXTEND Gram
CApp(loc,(Some (List.length args+1),CRef f),args@[c,None])
| c=operconstr; ".("; "@"; f=global;
args=LIST0 (operconstr LEVEL "9"); ")" ->
- CAppExpl(loc,(Some (List.length args+1),f),args@[c])
+ CAppExpl(loc,(Some (List.length args+1),f),args@[c])
| c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ]
| "0"
[ c=atomic_constr -> c
@@ -222,13 +222,13 @@ GEXTEND Gram
CGeneralization (loc, Explicit, None, c)
] ]
;
- forall:
- [ [ "forall" -> ()
+ forall:
+ [ [ "forall" -> ()
| IDENT "Π" -> ()
] ]
;
- lambda:
- [ [ "fun" -> ()
+ lambda:
+ [ [ "fun" -> ()
| IDENT "λ" -> ()
] ]
;
@@ -239,7 +239,7 @@ GEXTEND Gram
] ]
;
record_field_declaration:
- [ [ id = identref; params = LIST0 identref; ":="; c = lconstr ->
+ [ [ id = identref; params = LIST0 identref; ":="; c = lconstr ->
(id, Topconstr.abstract_constr_expr c (binders_of_lidents params)) ] ]
;
binder_constr:
@@ -266,10 +266,10 @@ GEXTEND Gram
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
"in"; c2 = operconstr LEVEL "200" ->
CCases (loc, LetPatternStyle, None, [(c1,(None,None))], [(loc, [(loc,[p])], c2)])
- | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
+ | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(loc, [(loc, [p])], c2)])
- | "let"; "'"; p=pattern; "in"; t = operconstr LEVEL "200";
+ | "let"; "'"; p=pattern; "in"; t = operconstr LEVEL "200";
":="; c1 = operconstr LEVEL "200"; rt = case_type;
"in"; c2 = operconstr LEVEL "200" ->
CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(loc, [(loc, [p])], c2)])
@@ -326,8 +326,8 @@ GEXTEND Gram
;
return_type:
[ [ a = OPT [ na = OPT["as"; id=name -> snd id];
- ty = case_type -> (na,ty) ] ->
- match a with
+ ty = case_type -> (na,ty) ] ->
+ match a with
| None -> None, None
| Some (na,t) -> (na, Some t)
] ]
@@ -351,7 +351,7 @@ GEXTEND Gram
[ p = pattern; lp = LIST1 NEXT ->
(match p with
| CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
- | _ -> Util.user_err_loc
+ | _ -> Util.user_err_loc
(cases_pattern_expr_loc p, "compound_pattern",
Pp.str "Constructor expected."))
| p = pattern; "as"; id = ident ->
@@ -370,9 +370,9 @@ GEXTEND Gram
| s = string -> CPatPrim (loc, String s) ] ]
;
binder_list:
- [ [ idl=LIST1 name; bl=binders_let ->
+ [ [ idl=LIST1 name; bl=binders_let ->
LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl
- | idl=LIST1 name; ":"; c=lconstr ->
+ | idl=LIST1 name; ":"; c=lconstr ->
[LocalRawAssum (idl,Default Explicit,c)]
| cl = binders_let -> cl
] ]
@@ -390,15 +390,15 @@ GEXTEND Gram
fixannot:
[ [ "{"; IDENT "struct"; id=identref; "}" -> (Some id, CStructRec)
| "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> (id, CWfRec rel)
- | "{"; IDENT "measure"; m=constr; id=OPT identref;
+ | "{"; IDENT "measure"; m=constr; id=OPT identref;
rel=OPT constr; "}" -> (id, CMeasureRec (m,rel))
] ]
;
binders_let_fixannot:
- [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot ->
+ [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot ->
(assum (loc, Name id) :: fst bl), snd bl
| f = fixannot -> [], f
- | b = binder_let; bl = binders_let_fixannot ->
+ | b = binder_let; bl = binders_let_fixannot ->
b @ fst bl, snd bl
| -> [], (None, CStructRec)
] ]
@@ -410,21 +410,21 @@ GEXTEND Gram
binder_let:
[ [ id=name ->
[LocalRawAssum ([id],Default Explicit,CHole (loc, None))]
- | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
+ | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
[LocalRawAssum (id::idl,Default Explicit,c)]
- | "("; id=name; ":"; c=lconstr; ")" ->
+ | "("; id=name; ":"; c=lconstr; ")" ->
[LocalRawAssum ([id],Default Explicit,c)]
| "("; id=name; ":="; c=lconstr; ")" ->
[LocalRawDef (id,c)]
- | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
+ | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
[LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))]
| "{"; id=name; "}" ->
[LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
- | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
+ | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
[LocalRawAssum (id::idl,Default Implicit,c)]
- | "{"; id=name; ":"; c=lconstr; "}" ->
+ | "{"; id=name; ":"; c=lconstr; "}" ->
[LocalRawAssum ([id],Default Implicit,c)]
- | "{"; id=name; idl=LIST1 name; "}" ->
+ | "{"; id=name; idl=LIST1 name; "}" ->
List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
| "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
@@ -434,8 +434,8 @@ GEXTEND Gram
;
binder:
[ [ id=name -> ([id],Default Explicit,CHole (loc, None))
- | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c)
- | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c)
+ | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c)
+ | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c)
] ]
;
typeclass_constraint:
@@ -448,7 +448,7 @@ GEXTEND Gram
(loc, Anonymous), false, c
] ]
;
-
+
type_cstr:
[ [ c=OPT [":"; c=lconstr -> c] -> (loc,c) ] ]
;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 08:31:19 +0000