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.ml4349
1 files changed, 174 insertions, 175 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 620b6a800..057494597 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -6,12 +6,60 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
(* $Id$ *)
open Pcoq
open Constr
+open Rawterm
+open Term
+open Names
+open Libnames
+open Prim
+open Topconstr
+
+(* For the very old syntax of fixpoints *)
+let split_lambda = function
+ | CLambdaN (loc,[[na],t],c) -> (na,t,c)
+ | CLambdaN (loc,([na],t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
+ | CLambdaN (loc,(na::nal,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,t)::bl,c))
+ | _ -> Util.error "ill-formed fixpoint body"
+
+let split_product = function
+ | CArrow (loc,t,c) -> c
+ | CProdN (loc,[[na],t],c) -> c
+ | CProdN (loc,([na],t)::bl,c) -> CProdN(loc,bl,c)
+ | CProdN (loc,(na::nal,t)::bl,c) -> CProdN(loc,(nal,t)::bl,c)
+ | _ -> Util.error "ill-formed fixpoint body"
+
+let rec split_fix n typ def =
+ if n = 0 then ([],typ,def)
+ else
+ let (na,t,def) = split_lambda def in
+ let typ = split_product typ in
+ let (bl,typ,def) = split_fix (n-1) typ def in
+ (([na],t)::bl,typ,def)
+
+let coerce_to_var = function
+ | CRef (Ident (_,id)) -> id
+ | ast -> Util.user_err_loc
+ (constr_loc ast,"Ast.coerce_to_var",
+ (Pp.str"This expression should be a simple identifier"))
+
+let coerce_to_name = function
+ | CRef (Ident (loc,id)) -> (loc, Name id)
+ | ast -> Util.user_err_loc
+ (constr_loc ast,"Ast.coerce_to_var",
+ (Pp.str"This expression should be a simple identifier"))
+
+open Util
+
+let rec abstract_constr loc c = function
+ | [] -> c
+ | LocalRawDef ((loc',x),b)::bl ->
+ CLetIn (join_loc loc' loc, (loc', x), b, abstract_constr loc c bl)
+ | LocalRawAssum (nal,t)::bl ->
+ let loc' = join_loc (fst (List.hd nal)) loc in
+ CLambdaN(loc', [nal, t], abstract_constr loc c bl)
(* Hack to parse "(n)" as nat without conflicts with the (useless) *)
(* admissible notation "(n)" *)
@@ -30,40 +78,22 @@ let test_int_rparen =
GEXTEND Gram
GLOBAL: constr0 constr1 constr2 constr3 lassoc_constr4 constr5
constr6 constr7 constr8 constr9 constr10 lconstr constr
- ne_ident_comma_list ne_constr_list sort ne_binders_list qualid
- global constr_pattern ident numarg;
- ident:
- [ [ id = Prim.var -> id
+ ne_name_comma_list ne_constr_list sort
+ global constr_pattern Constr.ident;
+ Constr.ident:
+ [ [ id = Prim.ident -> id
- (* This is used in quotations *)
- | id = Prim.metaident -> id ] ]
+ (* This is used in quotations and Syntax *)
+ | id = METAIDENT -> id_of_string id ] ]
;
global:
- [ [ l = qualid -> l
+ [ [ r = Prim.reference -> r
(* This is used in quotations *)
- | id = Prim.metaident -> id ] ]
- ;
- qualid:
- [ [ id = Prim.var; l = fields -> <:ast< (QUALID $id ($LIST $l)) >>
- | id = Prim.var -> <:ast< (QUALID $id) >>
- ] ]
- ;
- fields:
- [ [ id = FIELD; l = fields -> <:ast< ($VAR $id) >> :: l
- | id = FIELD -> [ <:ast< ($VAR $id) >> ]
- ] ]
- ;
- raw_constr:
- [ [ c = Prim.ast -> c ] ]
+ | id = METAIDENT -> Ident (loc,id_of_string id) ] ]
;
constr:
- [ [ c = constr8 -> (* Genarg.ConstrTerm *) c
-(* | IDENT "Inst"; id = Prim.rawident; "["; c = constr; "]" ->
- Genarg.ConstrContext (id, c)
- | IDENT "Eval"; rtc = Tactic.raw_red_tactic; "in"; c = constr ->
- Genarg.ConstrEval (rtc,c)
- | IDENT "Check"; c = constr8 -> <:ast<(CHECK $c)>> *)] ]
+ [ [ c = constr8 -> c ] ]
;
lconstr:
[ [ c = constr10 -> c ] ]
@@ -72,101 +102,85 @@ GEXTEND Gram
[ [ c = constr -> c ] ]
;
ne_constr_list:
- [ [ c1 = constr; cl = ne_constr_list -> c1::cl
- | c1 = constr -> [c1] ] ]
+ [ [ cl = LIST1 constr -> cl ] ]
;
sort:
- [ [ "Set" -> <:ast< (SET) >>
- | "Prop" -> <:ast< (PROP) >>
- | "Type" -> <:ast< (TYPE) >> ] ]
+ [ [ "Set" -> RProp Pos
+ | "Prop" -> RProp Null
+ | "Type" -> RType None ] ]
;
constr0:
- [ [ "?" -> <:ast< (ISEVAR) >>
- | "?"; n = Prim.natural ->
- let n = Coqast.Num (loc,n) in <:ast< (META $n) >>
- | bl = binders; c = constr -> <:ast< ($ABSTRACT "LAMBDALIST" $bl $c) >>
+ [ [ "?" -> CHole loc
+ | "?"; n = Prim.natural -> CMeta (loc, n)
+ | bll = binders; c = constr -> abstract_constr loc c bll
(* Hack to parse syntax "(n)" as a natural number *)
| "("; test_int_rparen; n = INT; ")" ->
- let n = Coqast.Str (loc,n) in
- <:ast< (DELIMITERS "nat_scope" (NUMERAL $n)) >>
- | "("; lc1 = lconstr; ":"; c = constr; body = product_tail ->
- let id = Ast.coerce_to_var lc1 in
- <:ast< (PROD $c [$id]$body) >>
+ let n = CNumeral (loc,Bignat.POS (Bignat.of_string n)) in
+ CDelimiters (loc,"nat_scope",n)
+ | "("; lc1 = lconstr; ":"; c = constr; (bl,body) = product_tail ->
+ let id = coerce_to_name lc1 in
+ CProdN (loc, ([id], c)::bl, body)
+(* TODO: Syntaxe (_:t...)t et (_,x...)t *)
| "("; lc1 = lconstr; ","; lc2 = lconstr; ":"; c = constr;
- body = product_tail ->
- let id1 = Ast.coerce_to_var lc1 in
- let id2 = Ast.coerce_to_var lc2 in
- <:ast< (PRODLIST $c [$id1][$id2]$body) >>
+ (bl,body) = product_tail ->
+ let id1 = coerce_to_name lc1 in
+ let id2 = coerce_to_name lc2 in
+ CProdN (loc, ([id1; id2], c)::bl, body)
| "("; lc1 = lconstr; ","; lc2 = lconstr; ",";
- idl = ne_ident_comma_list; ":"; c = constr; body = product_tail ->
- let id1 = Ast.coerce_to_var lc1 in
- let id2 = Ast.coerce_to_var lc2 in
-(* <:ast< (PRODLIST $c [$id1][$id2]($SLAM $idl $body)) >>*)
- <:ast< ($ABSTRACT "PRODLIST" (BINDERS (BINDER $c $id1 $id2 ($LIST $idl))) $body) >>
+ idl = ne_name_comma_list; ":"; c = constr; (bl,body) = product_tail ->
+ let id1 = coerce_to_name lc1 in
+ let id2 = coerce_to_name lc2 in
+ CProdN (loc, (id1::id2::idl, c)::bl, body)
| "("; lc1 = lconstr; ")" -> lc1
| "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" ->
- <:ast< (SOAPP $lc1 ($LIST $cl)) >>
- | IDENT "Fix"; id = ident; "{"; fbinders = fixbinders; "}" ->
- <:ast< (FIX $id ($LIST $fbinders)) >>
- | IDENT "CoFix"; id = ident; "{"; fbinders = cofixbinders; "}" ->
- <:ast< (COFIX $id ($LIST $fbinders)) >>
- | s = sort -> s
- | v = global -> v
- | n = INT ->
- let n = Coqast.Str (loc,n) in <:ast< (NUMERAL $n) >>
- | "-"; n = INT ->
- let n = Coqast.Str (loc,n) in <:ast< (NEGNUMERAL $n) >>
- | "!"; f = global ->
- <:ast< (APPLISTEXPL $f) >>
- ] ]
+ (match lc1 with
+ | CMeta (loc2,n) ->
+ CApp (loc,CMeta (loc2, -n), List.map (fun c -> c, None) cl)
+ | _ ->
+ Util.error "Second-order pattern-matching expects a head metavariable")
+ | IDENT "Fix"; id = identref; "{"; fbinders = fixbinders; "}" ->
+ CFix (loc, id, fbinders)
+ | IDENT "CoFix"; id = identref; "{"; fbinders = cofixbinders; "}" ->
+ CCoFix (loc, id, fbinders)
+ | s = sort -> CSort (loc, s)
+ | v = global -> CRef v
+ | n = INT -> CNumeral (loc,Bignat.POS (Bignat.of_string n))
+ | "-"; n = INT -> CNumeral (loc,Bignat.NEG (Bignat.of_string n))
+ | "!"; f = global -> CAppExpl (loc,f,[])
+ ] ]
;
constr1:
- [ [ "<"; ":"; IDENT "ast"; ":"; "<"; c = raw_constr; ">>" -> c
- | "<"; l1 = lconstr; ">"; IDENT "Match"; c = constr; "with";
- cl = ne_constr_list; "end" ->
- <:ast< (MATCH $l1 $c ($LIST $cl)) >>
- | "<"; l1 = lconstr; ">"; IDENT "Match"; c = constr; "with"; "end"
- ->
- <:ast< (MATCH $l1 $c) >>
- | "<"; l1 = lconstr; ">"; IDENT "Case"; c = constr; "of";
- cl = ne_constr_list; "end" ->
- <:ast< (CASE $l1 $c ($LIST $cl)) >>
- | "<"; l1 = lconstr; ">"; IDENT "Case"; c = constr; "of"; "end" ->
- <:ast< (CASE $l1 $c) >>
- | IDENT "Case"; c = constr; "of"; cl = ne_constr_list; "end" ->
- <:ast< (CASE "SYNTH" $c ($LIST $cl)) >>
- | IDENT "Case"; c = constr; "of"; "end" ->
- <:ast< (CASE "SYNTH" $c) >>
- | IDENT "Match"; c = constr; "with"; cl = ne_constr_list; "end" ->
- <:ast< (MATCH "SYNTH" $c ($LIST $cl)) >>
- | IDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
+ [ [ "<"; p = lconstr; ">"; IDENT "Match"; c = constr; "with";
+ cl = LIST0 constr; "end" ->
+ COrderedCase (loc, MatchStyle, Some p, c, cl)
+ | "<"; p = lconstr; ">"; IDENT "Case"; c = constr; "of";
+ cl = LIST0 constr; "end" ->
+ COrderedCase (loc, RegularStyle, Some p, c, cl)
+ | IDENT "Case"; c = constr; "of"; cl = LIST0 constr; "end" ->
+ COrderedCase (loc, RegularStyle, None, c, cl)
+ | IDENT "Match"; c = constr; "with"; cl = LIST1 constr; "end" ->
+ COrderedCase (loc, MatchStyle, None, c, cl)
+ | IDENT "let"; "("; b = ne_name_comma_list; ")"; "=";
c = constr; "in"; c1 = constr->
- <:ast< (LET "SYNTH" $c ($ABSTRACT "LAMBDALIST"
- (BINDERS (BINDER (ISEVAR) ($LIST $b))) $c1)) >>
- | IDENT "let"; id1 = ident ; "="; c = opt_casted_constr;
- "in"; c1 = constr ->
- <:ast< (LETIN $c [$id1]$c1) >>
-(*
- | IDENT "let"; id1 = ident ; "="; c = opt_casted_constr;
- "in"; c1 = constr ->
- <:ast< (LETIN $c [$id1]$c1) >>
-*)
+ (* TODO: right loc *)
+ COrderedCase
+ (loc, LetStyle, None, c, [CLambdaN (loc, [b, CHole loc], c1)])
+ | IDENT "let"; na = name; "="; c = opt_casted_constr; "in"; c1 = constr
+ -> CLetIn (loc, na, c, c1)
| IDENT "if"; c1 = constr; IDENT "then"; c2 = constr;
IDENT "else"; c3 = constr ->
- <:ast< ( IF "SYNTH" $c1 $c2 $c3) >>
-(* EN ATTENTE DE REMPLACER CE QUI EST DANS Program.v ... *)
- | "<"; l1 = lconstr; ">";
- IDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
+ COrderedCase (loc, IfStyle, None, c1, [c2; c3])
+ | "<"; p = lconstr; ">";
+ IDENT "let"; "("; b = ne_name_comma_list; ")"; "=";
c = constr; "in"; c1 = constr ->
-(* <:ast< (CASE "NOREC" $l1 $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >>*)
- <:ast< (LET $l1 $c ($ABSTRACT "LAMBDALIST" (BINDERS
- (BINDER (ISEVAR) ($LIST $b))) $c1)) >>
- | "<"; l1 = lconstr; ">";
+ (* TODO: right loc *)
+ COrderedCase (loc, LetStyle, Some p, c,
+ [CLambdaN (loc, [b, CHole loc], c1)])
+ | "<"; p = lconstr; ">";
IDENT "if"; c1 = constr; IDENT "then";
c2 = constr; IDENT "else"; c3 = constr ->
- <:ast< (IF $l1 $c1 $c2 $c3) >>
- | c = constr0 -> c
- ] ]
+ COrderedCase (loc, IfStyle, Some p, c1, [c2; c3])
+ | c = constr0 -> c ] ]
;
constr2: (* ~ will be here *)
[ [ c = constr1 -> c ] ]
@@ -188,113 +202,98 @@ GEXTEND Gram
;
constr8: (* <-> will be here *)
[ [ c1 = constr7 -> c1
- | c1 = constr7; "->"; c2 = constr8 -> <:ast< (PROD $c1 [<>]$c2) >> ] ]
+ | c1 = constr7; "->"; c2 = constr8 -> CArrow (loc, c1, c2) ] ]
;
constr9:
[ [ c1 = constr8 -> c1
- | c1 = constr8; "::"; c2 = constr8 -> <:ast< (CAST $c1 $c2) >> ] ]
- ;
- numarg:
- [ [ n = Prim.natural -> Coqast.Num (loc, n) ] ]
- ;
- simple_binding:
- [ [ id = ident; ":="; c = constr -> <:ast< (BINDING $id $c) >>
- | n = numarg; ":="; c = constr -> <:ast< (BINDING $n $c) >> ] ]
- ;
- simple_binding_list:
- [ [ b = simple_binding; l = simple_binding_list -> b :: l | -> [] ] ]
- ;
- binding_list:
- [ [ c1 = constr; ":="; c2 = constr; bl = simple_binding_list ->
- Coqast.Node
- (loc, "EXPLICITBINDINGS",
- (Coqast.Node (loc, "BINDING", [Ast.coerce_to_var c1; c2]) :: bl))
- | n = numarg; ":="; c = constr; bl = simple_binding_list ->
- <:ast<(EXPLICITBINDINGS (BINDING $n $c) ($LIST $bl))>>
- | c1 = constr; bl = LIST0 constr ->
- <:ast<(IMPLICITBINDINGS $c1 ($LIST $bl))>> ] ]
+ | c1 = constr8; "::"; c2 = constr8 -> CCast (loc, c1, c2) ] ]
;
constr10:
- [ [ "!"; f = global; args = LIST0 constr9 ->
- <:ast< (APPLISTEXPL $f ($LIST $args)) >>
+ [ [ "!"; f = global; args = LIST0 constr9 -> CAppExpl (loc, f, args)
+(*
| "!"; f = global; "with"; b = binding_list ->
<:ast< (APPLISTWITH $f $b) >>
- | f = constr9; args = LIST1 constr91 ->
- <:ast< (APPLIST $f ($LIST $args)) >>
+*)
+ | f = constr9; args = LIST1 constr91 -> CApp (loc, f, args)
| f = constr9 -> f ] ]
;
- ne_ident_comma_list:
- [ [ id = ident; ","; idl = ne_ident_comma_list -> id :: idl
- | id = ident -> [id] ] ]
+ ne_name_comma_list:
+ [ [ nal = LIST1 name SEP "," -> nal ] ]
;
- ident_comma_list_tail:
- [ [ ","; idl = ne_ident_comma_list -> idl
+ name_comma_list_tail:
+
+ [ [ ","; idl = ne_name_comma_list -> idl
| -> [] ] ]
;
opt_casted_constr:
- [ [ c = constr; ":"; t = constr -> <:ast< (CAST $c $t) >>
+ [ [ c = constr; ":"; t = constr -> CCast (loc, c, t)
| c = constr -> c ] ]
;
- vardecls: (* This is interpreted by Pcoq.abstract_binder *)
- [ [ id = ident; idl = ident_comma_list_tail; c = type_option ->
- <:ast< (BINDER $c $id ($LIST $idl)) >>
- | id = ident; ":="; c = opt_casted_constr ->
- <:ast< (LETIN $c $id) >>
- | id = ident; "="; c = opt_casted_constr ->
- <:ast< (LETIN $c $id) >> ] ]
+ vardecls:
+ [ [ na = name; nal = name_comma_list_tail; c = type_option ->
+ LocalRawAssum (na::nal,c)
+ | na = name; "="; c = opt_casted_constr ->
+ LocalRawDef (na, c)
+ | na = name; ":="; c = opt_casted_constr ->
+ LocalRawDef (na, c)
+
+ (* This is used in quotations *)
+ | id = METAIDENT; c = type_option -> LocalRawAssum ([loc, Name (id_of_string id)], c)
+ ] ]
;
ne_vardecls_list:
[ [ id = vardecls; ";"; idl = ne_vardecls_list -> id :: idl
| id = vardecls -> [id] ] ]
;
binders:
- [ [ "["; bl = ne_vardecls_list; "]" -> <:ast< (BINDERS ($LIST $bl)) >> ] ]
- ;
- rawbinders:
[ [ "["; bl = ne_vardecls_list; "]" -> bl ] ]
;
- ne_binders_list:
- [ [ bl = rawbinders; bll = ne_binders_list -> bl @ bll
- | bl = rawbinders -> bl ] ]
+ simple_params:
+ [ [ idl = LIST1 name SEP ","; ":"; c = constr -> (idl, c)
+ | idl = LIST1 name SEP "," -> (idl, CHole loc)
+ ] ]
+ ;
+ simple_binders:
+ [ [ "["; bll = LIST1 simple_params SEP ";"; "]" -> bll ] ]
+ ;
+ ne_simple_binders_list:
+ [ [ bll = LIST1 simple_binders -> List.flatten bll ] ]
;
type_option:
[ [ ":"; c = constr -> c
- | -> <:ast< (ISEVAR) >> ] ]
+ | -> CHole loc ] ]
;
constr91:
- [ [ n = INT; "!"; c1 = constr9 ->
- let n = Coqast.Num (loc,int_of_string n) in <:ast< (EXPL $n $c1) >>
- | n = INT ->
- let n = Coqast.Str (loc,n) in <:ast< (NUMERAL $n) >>
- | c1 = constr9 -> c1 ] ]
+ [ [ n = natural; "!"; c = constr9 -> (c, Some n)
+ | n = natural ->
+ (CNumeral (loc, Bignat.POS (Bignat.of_string (string_of_int n))), None)
+ | c = constr9 -> (c, None) ] ]
;
fixbinder:
- [ [ id = ident; "/"; recarg = Prim.natural; ":"; type_ = constr;
- ":="; def = constr ->
- let recarg = Coqast.Num (loc,recarg) in
- <:ast< (NUMFDECL $id $recarg $type_ $def) >>
- | id = ident; bl = ne_binders_list; ":"; type_ = constr;
+ [ [ id = base_ident; "/"; recarg = natural; ":"; type_ = constr;
":="; def = constr ->
- <:ast< (FDECL $id (BINDERS ($LIST $bl)) $type_ $def) >> ] ]
+ Options.if_verbose Pp.warning
+ "Checking of the fixpoint type not done for very-old-style fixpoint";
+ let (bl, typ, def) = split_fix recarg type_ def in (id, bl, typ, def)
+ | id = base_ident; bl = ne_simple_binders_list; ":"; type_ = constr;
+ ":="; def = constr ->
+ (id, bl, type_, def) ] ]
;
fixbinders:
- [ [ fb = fixbinder; "with"; fbs = fixbinders -> fb::fbs
- | fb = fixbinder -> [fb] ] ]
+ [ [ fbs = LIST1 fixbinder SEP "with" -> fbs ] ]
;
cofixbinder:
- [ [ id = ident; ":"; type_ = constr; ":="; def = constr ->
- <:ast< (CFDECL $id $type_ $def) >> ] ]
+ [ [ id = base_ident; ":"; type_ = constr; ":="; def = constr ->
+ (id, type_, def) ] ]
;
cofixbinders:
- [ [ fb = cofixbinder; "with"; fbs = cofixbinders -> fb::fbs
- | fb = cofixbinder -> [fb] ] ]
+ [ [ fbs = LIST1 cofixbinder SEP "with" -> fbs ] ]
;
product_tail:
- [ [ ";"; idl = ne_ident_comma_list;
- ":"; c = constr; c2 = product_tail ->
- <:ast< ($ABSTRACT "PRODLIST" (BINDERS (BINDER $c ($LIST $idl))) $c2) >>
- | ";"; idl = ne_ident_comma_list; c2 = product_tail ->
- <:ast< ($ABSTRACT "PRODLIST" (BINDERS (BINDER (ISEVAR) ($LIST $idl))) $c2) >>
- | ")"; c = constr -> c ] ]
+ [ [ ";"; idl = ne_name_comma_list; ":"; c = constr;
+ (bl,c2) = product_tail -> ((idl, c)::bl, c2)
+ | ";"; idl = ne_name_comma_list; (bl,c2) = product_tail ->
+ ((idl, CHole (fst (List.hd idl)))::bl, c2)
+ | ")"; c = constr -> ([], c) ] ]
;
END;;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 02:43:05 +0000