diff options
| -rw-r--r-- | parsing/g_command.ml4 | 223 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 217 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 5 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 108 | ||||
| -rwxr-xr-x | syntax/PPConstr.v (renamed from syntax/PPCommand.v) | 11 |
5 files changed, 282 insertions, 282 deletions
diff --git a/parsing/g_command.ml4 b/parsing/g_command.ml4 deleted file mode 100644 index 7a0bab447..000000000 --- a/parsing/g_command.ml4 +++ /dev/null @@ -1,223 +0,0 @@ - -(* $Id$ *) - -open Pcoq -open Command - -GEXTEND Gram - ident: - [ [ id = IDENT -> <:ast< ($VAR $id) >> ] ] - ; - raw_command: - [ [ c = Prim.ast -> c ] ] - ; - command: - [ [ c = command8 -> c ] ] - ; - lcommand: - [ [ c = command10 -> c ] ] - ; - ne_command_list: - [ [ c1 = command; cl = ne_command_list -> c1::cl - | c1 = command -> [c1] ] ] - ; - command0: - [ [ "?" -> <:ast< (ISEVAR) >> - | "?"; n = Prim.number -> <:ast< (META $n) >> - | "["; id1 = IDENT; ":"; c = command; c2 = abstraction_tail -> - <:ast< (LAMBDALIST $c [$id1]$c2) >> - | "["; id1 = IDENT; ","; idl = ne_ident_comma_list; - ":"; c = command; c2 = abstraction_tail -> - <:ast< (LAMBDALIST $c [$id1]($SLAM $idl $c2)) >> - | "["; id1 = IDENT; ","; idl = ne_ident_comma_list; - c = abstraction_tail -> - <:ast< (LAMBDALIST (ISEVAR) [$id1]($SLAM $idl $c)) >> - | "["; id1 = IDENT; c = abstraction_tail -> - <:ast< (LAMBDALIST (ISEVAR) [$id1]$c) >> - | "["; id1 = IDENT; "="; c = command; "]"; c2 = command -> - <:ast< (ABST #Core#let.cci $c [$id1]$c2) >> - | "<<"; id1 = IDENT; ">>"; c = command -> <:ast< [$id1]$c >> - | "("; lc1 = lcommand; ":"; c = command; body = product_tail -> - let id = Ast.coerce_to_var "lc1" lc1 in - <:ast< (PROD $c [$id]$body) >> - | "("; lc1 = lcommand; ","; lc2 = lcommand; ":"; c = command; - body = product_tail -> - let id1 = Ast.coerce_to_var "lc1" lc1 in - let id2 = Ast.coerce_to_var "lc2" lc2 in - <:ast< (PRODLIST $c [$id1][$id2]$body) >> - | "("; lc1 = lcommand; ","; lc2 = lcommand; ","; - idl = ne_ident_comma_list; ":"; c = command; body = product_tail -> - let id1 = Ast.coerce_to_var "lc1" lc1 in - let id2 = Ast.coerce_to_var "lc2" lc2 in - <:ast< (PRODLIST $c [$id1][$id2]($SLAM $idl $body)) >> - | "("; lc1 = lcommand; ")" -> lc1 -(* - | "("; lc1 = lcommand; ")"; "@"; "["; cl = ne_command_list; "]" -> - <:ast< (XTRA"$SOAPP" $lc1 ($LIST $cl)) >> -*) - | "Prop" -> <:ast< (PROP) >> - | "Set" -> <:ast< (SET) >> - | "Type" -> <:ast< (TYPE) >> - | IDENT "Fix"; id = ident; "{"; fbinders = fixbinders; "}" -> - <:ast< (FIX $id ($LIST $fbinders)) >> - | IDENT "CoFix"; id = ident; "{"; fbinders = cofixbinders; "}" -> - <:ast< (COFIX $id ($LIST $fbinders)) >> - | v = ident -> v ] ] - ; - command1: - [ [ "<"; ":"; IDENT "ast"; ":"; "<"; c = raw_command; ">>" -> c - | "<"; l1 = lcommand; ">"; IDENT "Match"; c = command; "with"; - cl = ne_command_list; "end" -> - <:ast< (CASE "REC" $l1 $c ($LIST $cl)) >> - | "<"; l1 = lcommand; ">"; IDENT "Match"; c = command; "with"; "end" - -> - <:ast< (CASE "REC" $l1 $c) >> - | "<"; l1 = lcommand; ">"; IDENT "Case"; c = command; "of"; - cl = ne_command_list; "end" -> - <:ast< (CASE "NOREC" $l1 $c ($LIST $cl)) >> - | "<"; l1 = lcommand; ">"; IDENT "Case"; c = command; "of"; "end" -> - <:ast< (CASE "NOREC" $l1 $c) >> - | IDENT "Case"; c = command; "of"; cl = ne_command_list; "end" -> - <:ast< (CASE "NOREC" "SYNTH" $c ($LIST $cl)) >> - | IDENT "Case"; c = command; "of"; "end" -> - <:ast< (CASE "NOREC" "SYNTH" $c) >> - | IDENT "Match"; c = command; "with"; cl = ne_command_list; "end" -> - <:ast< (CASE "REC" "SYNTH" $c ($LIST $cl)) >> - | IDENT "let"; "("; b = ne_ident_comma_list; ")"; "="; - c = command; "in"; c1 = command -> - <:ast< (MLCASE "NOREC" $c (LAMBDALIST (ISEVAR) - ($SLAM $b $c1))) >> - | IDENT "let"; id1 = IDENT ; "="; c = command; "in"; - c1 = command -> <:ast< (ABST #Core#let.cci $c [$id1]$c1) >> - | IDENT "if"; c1 = command; IDENT "then"; c2 = command; - IDENT "else"; c3 = command -> - <:ast< ( MLCASE "NOREC" $c1 $c2 $c3) >> -(* EN ATTENTE DE REMPLACER CE QUI EST DANS Program.v ... *) - | "<"; l1 = lcommand; ">"; - IDENT "let"; "("; b = ne_ident_comma_list; ")"; "="; - c = command; "in"; c1 = command -> - <:ast< (MUTCASE $l1 $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >> - | "<"; l1 = lcommand; ">"; - IDENT "if"; c1 = command; IDENT "then"; - c2 = command; IDENT "else"; c3 = command -> - <:ast< (MUTCASE $l1 $c1 $c2 $c3) >> - | c = command0 -> c ] ] - ; - command2: - [ [ c = command1 -> c ] ] - ; - command3: - [ [ c1 = command2 -> c1 ] ] - ; - lassoc_command4: - [ [ c1 = command3 -> c1 ] ] - ; - command5: - [ [ c1 = lassoc_command4 -> c1 - | c1 = lassoc_command4; "::"; c2 = command5 -> - <:ast< (CAST $c1 $c2) >> ] ] - ; - command6: - [ [ c1 = command5 -> c1 ] ] - ; - command7: - [ RIGHTA [ c1 = command6 -> c1 ] ] - ; - command8: - [ [ c1 = command7 -> c1 - | c1 = command7; "->"; c2 = command8 -> - <:ast< (PROD $c1 [<>]$c2) >> ] ] - ; - command9: - [ [ c1 = command8 -> c1 ] ] - ; - command10: - [ [ "!"; f = IDENT; args = ne_command9_list -> - <:ast< (APPLISTEXPL ($VAR $f) ($LIST $args)) >> - | f = command9; args = ne_command91_list -> - <:ast< (APPLIST $f ($LIST $args)) >> - | f = command9 -> f ] ] - ; - ne_ident_comma_list: - [ [ id = ident; ","; idl = ne_ident_comma_list -> id::idl - | id = ident -> [id] ] ] - ; - binder: - [ [ idl = ne_ident_comma_list; ":"; c = command -> - <:ast< (BINDER $c ($LIST $idl)) >> ] ] - ; - ne_binder_list: - [ [ id = binder; ";"; idl = ne_binder_list -> id::idl - | id = binder -> [id] ] ] - ; - weak_binder: - [ [ idl = ne_ident_comma_list; c = type_option -> - <:ast< (BINDER $c ($LIST $idl)) >> ] ] - ; - ne_weak_binder_list: - [ [ id = weak_binder; ";"; idl = ne_weak_binder_list -> id::idl - | id = weak_binder -> [id] ] ] - ; - type_option: - [ [ ":"; c = command -> c - | -> <:ast< (ISEVAR) >> ] ] - ; -(* parameters: - [ [ "["; bl = ne_binder_semi_list; "]" -> $bl ] ] - ; - parameters_list: - [ [ - <:ast< (BINDERLIST ($LIST $bl)) >> - | -> <:ast< (BINDERLIST) >> ] ] - ; -*) command91: - [ [ n = Prim.number; "!"; c1 = command9 -> - <:ast< (EXPL $n $c1) >> - | c1 = command9 -> c1 ] ] - ; - ne_command91_list: - [ [ c1 = command91; cl = ne_command91_list -> c1::cl - | c1 = command91 -> [c1] ] ] - ; - ne_command9_list: - [ [ c1 = command9; cl = ne_command9_list -> c1::cl - | c1 = command9 -> [c1] ] ] - ; - fixbinder: - [ [ id = ident; "/"; recarg = Prim.number; ":"; type_ = command; - ":="; def = command -> <:ast< (NUMFDECL $id $recarg $type_ $def) >> - | id = ident; "["; idl = ne_weak_binder_list; "]"; ":"; type_ = command; - ":="; def = command -> - <:ast< (FDECL $id (BINDERS ($LIST $idl)) $type_ $def) >> ] ] - ; - fixbinders: - [ [ fb = fixbinder; "with"; fbs = fixbinders -> fb::fbs - | fb = fixbinder -> [fb] ] ] - ; - cofixbinder: - [ [ id = ident; ":"; type_ = command; ":="; def = command -> - <:ast< (CFDECL $id $type_ $def) >> ] ] - ; - cofixbinders: - [ [ fb = cofixbinder; "with"; fbs = cofixbinders -> fb::fbs - | fb = cofixbinder -> [fb] ] ] - ; - abstraction_tail: - [ [ ";"; idl = ne_ident_comma_list; - ":"; c = command; c2 = abstraction_tail -> - <:ast< (LAMBDALIST $c ($SLAM $idl $c2)) >> - | ";"; idl = ne_ident_comma_list; c2 = abstraction_tail -> - <:ast< (LAMBDALIST (ISEVAR) ($SLAM $idl $c2)) >> - | "]"; c = command -> c ] ] - ; - product_tail: - [ [ ";"; idl = ne_ident_comma_list; - ":"; c = command; c2 = product_tail -> - <:ast< (PRODLIST $c ($SLAM $idl $c2)) >> - | ";"; idl = ne_ident_comma_list; c2 = product_tail -> - <:ast< (PRODLIST (ISEVAR) ($SLAM $idl $c2)) >> - | ")"; c = command -> c ] ] - ; -END;; - -(* $Id$ *) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 new file mode 100644 index 000000000..3640db1bc --- /dev/null +++ b/parsing/g_constr.ml4 @@ -0,0 +1,217 @@ + +(* $Id$ *) + +open Pcoq +open Constr + +GEXTEND Gram + GLOBAL: ident constr0 constr1 constr2 constr3 lassoc_constr4 constr5 + constr6 constr7 constr8 constr9 constr10 lconstr constr + ne_ident_comma_list ne_constr_list; + + ident: + [ [ id = IDENT -> <:ast< ($VAR $id) >> ] ] + ; + raw_constr: + [ [ c = Prim.ast -> c ] ] + ; + constr: + [ [ c = constr8 -> c ] ] + ; + lconstr: + [ [ c = constr10 -> c ] ] + ; + ne_constr_list: + [ [ c1 = constr; cl = ne_constr_list -> c1::cl + | c1 = constr -> [c1] ] ] + ; + constr0: + [ [ "?" -> <:ast< (ISEVAR) >> + | "?"; n = Prim.number -> <:ast< (META $n) >> + | "["; id1 = IDENT; ":"; c = constr; c2 = abstraction_tail -> + <:ast< (LAMBDALIST $c [$id1]$c2) >> + | "["; id1 = IDENT; ","; idl = ne_ident_comma_list; + ":"; c = constr; c2 = abstraction_tail -> + <:ast< (LAMBDALIST $c [$id1]($SLAM $idl $c2)) >> + | "["; id1 = IDENT; ","; idl = ne_ident_comma_list; + c = abstraction_tail -> + <:ast< (LAMBDALIST (ISEVAR) [$id1]($SLAM $idl $c)) >> + | "["; id1 = IDENT; c = abstraction_tail -> + <:ast< (LAMBDALIST (ISEVAR) [$id1]$c) >> + | "["; id1 = IDENT; "="; c = constr; "]"; c2 = constr -> + <:ast< (ABST #Core#let.cci $c [$id1]$c2) >> + | "<<"; id1 = IDENT; ">>"; c = constr -> <:ast< [$id1]$c >> + | "("; lc1 = lconstr; ":"; c = constr; body = product_tail -> + let id = Ast.coerce_to_var "lc1" lc1 in + <:ast< (PROD $c [$id]$body) >> + | "("; lc1 = lconstr; ","; lc2 = lconstr; ":"; c = constr; + body = product_tail -> + let id1 = Ast.coerce_to_var "lc1" lc1 in + let id2 = Ast.coerce_to_var "lc2" lc2 in + <:ast< (PRODLIST $c [$id1][$id2]$body) >> + | "("; lc1 = lconstr; ","; lc2 = lconstr; ","; + idl = ne_ident_comma_list; ":"; c = constr; body = product_tail -> + let id1 = Ast.coerce_to_var "lc1" lc1 in + let id2 = Ast.coerce_to_var "lc2" lc2 in + <:ast< (PRODLIST $c [$id1][$id2]($SLAM $idl $body)) >> + | "("; lc1 = lconstr; ")" -> lc1 +(* + | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" -> + <:ast< (XTRA"$SOAPP" $lc1 ($LIST $cl)) >> +*) + | "Prop" -> <:ast< (PROP) >> + | "Set" -> <:ast< (SET) >> + | "Type" -> <:ast< (TYPE) >> + | IDENT "Fix"; id = ident; "{"; fbinders = fixbinders; "}" -> + <:ast< (FIX $id ($LIST $fbinders)) >> + | IDENT "CoFix"; id = ident; "{"; fbinders = cofixbinders; "}" -> + <:ast< (COFIX $id ($LIST $fbinders)) >> + | v = ident -> v ] ] + ; + constr1: + [ [ "<"; ":"; IDENT "ast"; ":"; "<"; c = raw_constr; ">>" -> c + | "<"; l1 = lconstr; ">"; IDENT "Match"; c = constr; "with"; + cl = ne_constr_list; "end" -> + <:ast< (CASE "REC" $l1 $c ($LIST $cl)) >> + | "<"; l1 = lconstr; ">"; IDENT "Match"; c = constr; "with"; "end" + -> + <:ast< (CASE "REC" $l1 $c) >> + | "<"; l1 = lconstr; ">"; IDENT "Case"; c = constr; "of"; + cl = ne_constr_list; "end" -> + <:ast< (CASE "NOREC" $l1 $c ($LIST $cl)) >> + | "<"; l1 = lconstr; ">"; IDENT "Case"; c = constr; "of"; "end" -> + <:ast< (CASE "NOREC" $l1 $c) >> + | IDENT "Case"; c = constr; "of"; cl = ne_constr_list; "end" -> + <:ast< (CASE "NOREC" "SYNTH" $c ($LIST $cl)) >> + | IDENT "Case"; c = constr; "of"; "end" -> + <:ast< (CASE "NOREC" "SYNTH" $c) >> + | IDENT "Match"; c = constr; "with"; cl = ne_constr_list; "end" -> + <:ast< (CASE "REC" "SYNTH" $c ($LIST $cl)) >> + | IDENT "let"; "("; b = ne_ident_comma_list; ")"; "="; + c = constr; "in"; c1 = constr -> + <:ast< (CASE "NOREC" "SYNTH" $c (LAMBDALIST (ISEVAR) + ($SLAM $b $c1))) >> + | IDENT "let"; id1 = IDENT ; "="; c = constr; "in"; + c1 = constr -> <:ast< (ABST #Core#let.cci $c [$id1]$c1) >> + | IDENT "if"; c1 = constr; IDENT "then"; c2 = constr; + IDENT "else"; c3 = constr -> + <:ast< ( CASE "NOREC" "SYNTH" $c1 $c2 $c3) >> +(* EN ATTENTE DE REMPLACER CE QUI EST DANS Program.v ... *) + | "<"; l1 = lconstr; ">"; + IDENT "let"; "("; b = ne_ident_comma_list; ")"; "="; + c = constr; "in"; c1 = constr -> + <:ast< (CASE "NOREC" $l1 $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >> + | "<"; l1 = lconstr; ">"; + IDENT "if"; c1 = constr; IDENT "then"; + c2 = constr; IDENT "else"; c3 = constr -> + <:ast< (CASE "NOREC" $l1 $c1 $c2 $c3) >> + | c = constr0 -> c ] ] + ; + constr2: + [ [ c = constr1 -> c ] ] + ; + constr3: + [ [ c1 = constr2 -> c1 ] ] + ; + lassoc_constr4: + [ [ c1 = constr3 -> c1 ] ] + ; + constr5: + [ [ c1 = lassoc_constr4 -> c1 + | c1 = lassoc_constr4; "::"; c2 = constr5 -> + <:ast< (CAST $c1 $c2) >> ] ] + ; + constr6: + [ [ c1 = constr5 -> c1 ] ] + ; + constr7: + [ RIGHTA [ c1 = constr6 -> c1 ] ] + ; + constr8: + [ [ c1 = constr7 -> c1 + | c1 = constr7; "->"; c2 = constr8 -> + <:ast< (PROD $c1 [<>]$c2) >> ] ] + ; + constr9: + [ [ c1 = constr8 -> c1 ] ] + ; + constr10: + [ [ "!"; f = IDENT; args = ne_constr9_list -> + <:ast< (APPLISTEXPL ($VAR $f) ($LIST $args)) >> + | f = constr9; args = ne_constr91_list -> + <:ast< (APPLIST $f ($LIST $args)) >> + | f = constr9 -> f ] ] + ; + ne_ident_comma_list: + [ [ id = ident; ","; idl = ne_ident_comma_list -> id::idl + | id = ident -> [id] ] ] + ; + binder: + [ [ idl = ne_ident_comma_list; c = type_option -> + <:ast< (BINDER $c ($LIST $idl)) >> ] ] + ; + ne_binder_list: + [ [ id = binder; ";"; idl = ne_binder_list -> id::idl + | id = binder -> [id] ] ] + ; + type_option: + [ [ ":"; c = constr -> c + | -> <:ast< (ISEVAR) >> ] ] + ; +(* parameters: + [ [ "["; bl = ne_binder_semi_list; "]" -> $bl ] ] + ; + parameters_list: + [ [ + <:ast< (BINDERLIST ($LIST $bl)) >> + | -> <:ast< (BINDERLIST) >> ] ] + ; +*) constr91: + [ [ n = Prim.number; "!"; c1 = constr9 -> + <:ast< (EXPL $n $c1) >> + | c1 = constr9 -> c1 ] ] + ; + ne_constr91_list: + [ [ c1 = constr91; cl = ne_constr91_list -> c1::cl + | c1 = constr91 -> [c1] ] ] + ; + ne_constr9_list: + [ [ c1 = constr9; cl = ne_constr9_list -> c1::cl + | c1 = constr9 -> [c1] ] ] + ; + fixbinder: + [ [ id = ident; "/"; recarg = Prim.number; ":"; type_ = constr; + ":="; def = constr -> <:ast< (NUMFDECL $id $recarg $type_ $def) >> + | id = ident; "["; idl = ne_binder_list; "]"; ":"; type_ = constr; + ":="; def = constr -> + <:ast< (FDECL $id (BINDERS ($LIST $idl)) $type_ $def) >> ] ] + ; + fixbinders: + [ [ fb = fixbinder; "with"; fbs = fixbinders -> fb::fbs + | fb = fixbinder -> [fb] ] ] + ; + cofixbinder: + [ [ id = ident; ":"; type_ = constr; ":="; def = constr -> + <:ast< (CFDECL $id $type_ $def) >> ] ] + ; + cofixbinders: + [ [ fb = cofixbinder; "with"; fbs = cofixbinders -> fb::fbs + | fb = cofixbinder -> [fb] ] ] + ; + abstraction_tail: + [ [ ";"; idl = ne_ident_comma_list; + ":"; c = constr; c2 = abstraction_tail -> + <:ast< (LAMBDALIST $c ($SLAM $idl $c2)) >> + | ";"; idl = ne_ident_comma_list; c2 = abstraction_tail -> + <:ast< (LAMBDALIST (ISEVAR) ($SLAM $idl $c2)) >> + | "]"; c = constr -> c ] ] + ; + product_tail: + [ [ ";"; idl = ne_ident_comma_list; + ":"; c = constr; c2 = product_tail -> + <:ast< (PRODLIST $c ($SLAM $idl $c2)) >> + | ";"; idl = ne_ident_comma_list; c2 = product_tail -> + <:ast< (PRODLIST (ISEVAR) ($SLAM $idl $c2)) >> + | ")"; c = constr -> c ] ] + ; +END;; diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 586a1bd67..424591efb 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -12,6 +12,7 @@ open Tactic (* Auxiliary grammar rules *) GEXTEND Gram + identarg: [ [ id = IDENT -> <:ast< ($VAR $id) >> ] ] ; @@ -21,10 +22,10 @@ GEXTEND Gram ] ] ; comarg: - [ [ c = Command.command -> <:ast< (COMMAND $c) >> ] ] + [ [ c = Constr.constr -> <:ast< (COMMAND $c) >> ] ] ; lcomarg: - [ [ c = Command.lcommand -> <:ast< (COMMAND $c) >> ] ] + [ [ c = Constr.lconstr -> <:ast< (COMMAND $c) >> ] ] ; ne_identarg_list: [ [ l = LIST1 identarg -> l ] ] diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 2bc94c200..81f963083 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -97,10 +97,10 @@ GEXTEND Gram | IDENT "Structure" -> <:ast< "Structure" >> ] ] ; field: - [ [ id = identarg; ":"; c = Command.command -> - <:ast< (VERNACARGLIST "" $id (COMMAND $c)) >> - | id = identarg; ":>"; c = Command.command -> - <:ast< (VERNACARGLIST "COERCION" $id (COMMAND $c)) >> ] ] + [ [ id = identarg; ":"; c = Constr.constr -> + <:ast< (VERNACARGLIST "" $id (CONSTR $c)) >> + | id = identarg; ":>"; c = Constr.constr -> + <:ast< (VERNACARGLIST "COERCION" $id (CONSTR $c)) >> ] ] ; nefields: [ [ idc = field; ";"; fs = nefields -> idc :: fs @@ -113,7 +113,7 @@ GEXTEND Gram onescheme: [ [ id = identarg; ":="; dep = dep; indid = identarg; IDENT "Sort"; s = sortdef -> - <:ast< (VERNACARGLIST $id $dep $indid (COMMAND $s)) >> ] ] + <:ast< (VERNACARGLIST $id $dep $indid (CONSTR $s)) >> ] ] ; specifscheme: [ [ rec_ = onescheme; "with"; recl = specifscheme -> rec_ :: recl @@ -180,11 +180,11 @@ GEXTEND Gram [ [ IDENT "Parameters" -> <:ast< "PARAMETERS" >> ] ] ; binder: - [ [ idl = ne_identarg_comma_list; ":"; c = Command.command -> + [ [ idl = ne_identarg_comma_list; ":"; c = Constr.constr -> <:ast< (BINDER $c ($LIST $idl)) >> ] ] ; idcom: - [ [ id = IDENT; ":"; c = Command.command -> + [ [ id = IDENT; ":"; c = Constr.constr -> <:ast< (BINDER $c ($VAR $id)) >> ] ] ; ne_lidcom: @@ -207,16 +207,16 @@ GEXTEND Gram tb = theorem_body; "Qed"; "." -> <:ast< (TheoremProof $thm $id $c $tb) >> - | def = def_tok; s = identarg; ":"; c1 = Command.command; "." -> - <:ast< (StartProof $def $s (COMMAND $c1)) >> - | def = def_tok; s = identarg; ":="; c1 = Command.command; "." -> - <:ast< (DEFINITION $def $s (COMMAND $c1)) >> - | def = def_tok; s = identarg; ":="; c1 = Command.command; ":"; - c2 = Command.command; "." -> - <:ast< (DEFINITION $def $s (COMMAND (CAST $c1 $c2))) >> - | def = def_tok; s = identarg; ":"; c1 = Command.command; ":="; - c2 = Command.command; "." -> - <:ast< (DEFINITION $def $s (COMMAND (CAST $c2 $c1))) >> + | def = def_tok; s = identarg; ":"; c1 = Constr.constr; "." -> + <:ast< (StartProof $def $s (CONSTR $c1)) >> + | def = def_tok; s = identarg; ":="; c1 = Constr.constr; "." -> + <:ast< (DEFINITION $def $s (CONSTR $c1)) >> + | def = def_tok; s = identarg; ":="; c1 = Constr.constr; ":"; + c2 = Constr.constr; "." -> + <:ast< (DEFINITION $def $s (CONSTR (CAST $c1 $c2))) >> + | def = def_tok; s = identarg; ":"; c1 = Constr.constr; ":="; + c2 = Constr.constr; "." -> + <:ast< (DEFINITION $def $s (CONSTR (CAST $c2 $c1))) >> (* CP / Juillet 99 Ajout de la possibilite d'appliquer une regle de reduction au @@ -225,17 +225,17 @@ GEXTEND Gram *) | def = def_tok; s = identarg; ":="; - IDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Command.command; "." -> - <:ast< (DEFINITION $def $s (COMMAND $c1) (TACTIC_ARG (REDEXP $r))) >> + IDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Constr.constr; "." -> + <:ast< (DEFINITION $def $s (CONSTR $c1) (TACTIC_ARG (REDEXP $r))) >> | def = def_tok; s = identarg; ":="; - IDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Command.command; ":"; - c2 = Command.command; "." -> + IDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Constr.constr; ":"; + c2 = Constr.constr; "." -> <:ast< (DEFINITION $def $s - (COMMAND (CAST $c1 $c2)) (TACTIC_ARG (REDEXP $r))) >> - | def = def_tok; s = identarg; ":"; c1 = Command.command; ":="; + (CONSTR (CAST $c1 $c2)) (TACTIC_ARG (REDEXP $r))) >> + | def = def_tok; s = identarg; ":"; c1 = Constr.constr; ":="; IDENT "Eval"; r = Tactic.red_tactic; "in"; - c2 = Command.command; "." -> - <:ast< (DEFINITION $def $s (COMMAND (CAST $c2 $c1)) + c2 = Constr.constr; "." -> + <:ast< (DEFINITION $def $s (CONSTR (CAST $c2 $c1)) (TACTIC_ARG (REDEXP $r))) >> (* Papageno / Février 99 @@ -243,13 +243,13 @@ GEXTEND Gram "Definition x := [c:nat]t" *) | def = def_tok; s = identarg; "["; id1 = IDENT; ":"; - c = Command.command; t = definition_tail; "." -> - <:ast< (DEFINITION $def $s (COMMAND (LAMBDA $c [$id1]$t))) >> + c = Constr.constr; t = definition_tail; "." -> + <:ast< (DEFINITION $def $s (CONSTR (LAMBDA $c [$id1]$t))) >> | def = def_tok; s = identarg; "["; id1 = IDENT; ","; - idl = Command.ne_ident_comma_list; ":"; c = Command.command; + idl = Constr.ne_ident_comma_list; ":"; c = Constr.constr; t = definition_tail; "." -> - <:ast< (DEFINITION $def $s (COMMAND + <:ast< (DEFINITION $def $s (CONSTR (LAMBDALIST $c [$id1]($SLAM $idl $t)))) >> @@ -266,16 +266,16 @@ GEXTEND Gram <:ast< (ABSTRACTION $id $c ($LIST $l)) >> | f = finite_tok; s = sortdef; id = identarg; indpar = indpar; ":="; lidcom = lidcom; "." -> - <:ast< (ONEINDUCTIVE $f $id (COMMAND $s) $indpar $lidcom) >> + <:ast< (ONEINDUCTIVE $f $id (CONSTR $s) $indpar $lidcom) >> | f = finite_tok; indl = block; "." -> <:ast< (MUTUALINDUCTIVE $f (VERNACARGLIST ($LIST $indl))) >> | record_tok; name = identarg; ps = indpar; ":"; s = sortdef; ":="; c = rec_constr; "{"; fs = fields; "}"; "." -> - <:ast< (RECORD "" $name $ps (COMMAND $s) $c $fs) >> + <:ast< (RECORD "" $name $ps (CONSTR $s) $c $fs) >> | record_tok; ">"; name = identarg; ps = indpar; ":"; s = sortdef; ":="; c = rec_constr; "{"; fs = fields; "}"; "." -> - <:ast< (RECORD "COERCION" $name $ps (COMMAND $s) $c $fs) >> + <:ast< (RECORD "COERCION" $name $ps (CONSTR $s) $c $fs) >> | IDENT "Mutual"; "["; bl = ne_binder_list; "]" ; f = finite_tok; indl = block_old_style; "." -> @@ -293,12 +293,12 @@ GEXTEND Gram definition_tail: - [ [ ";"; idl = Command.ne_ident_comma_list; - ":"; c = Command.command; c2 = definition_tail -> + [ [ ";"; idl = Constr.ne_ident_comma_list; + ":"; c = Constr.constr; c2 = definition_tail -> <:ast< (LAMBDALIST $c ($SLAM $idl $c2)) >> - | "]"; ":"; ty = Command.command; ":=" ; c = Command.command -> + | "]"; ":"; ty = Constr.constr; ":=" ; c = Constr.constr -> <:ast< (CAST $c $ty) >> - | "]"; ":="; c = Command.command -> c + | "]"; ":="; c = Constr.constr -> c ] ]; END @@ -356,17 +356,17 @@ GEXTEND Gram (* Grammar extensions, Coercions, Implicits *) - | IDENT "Coercion"; s = identarg; ":="; c1 = Command.command; "." -> - <:ast< (DEFINITION "COERCION" $s (COMMAND $c1)) >> - | IDENT "Coercion"; s = identarg; ":="; c1 = Command.command; ":"; - c2 = Command.command; "." -> - <:ast< (DEFINITION "COERCION" $s (COMMAND (CAST $c1 $c2))) >> + | IDENT "Coercion"; s = identarg; ":="; c1 = Constr.constr; "." -> + <:ast< (DEFINITION "COERCION" $s (CONSTR $c1)) >> + | IDENT "Coercion"; s = identarg; ":="; c1 = Constr.constr; ":"; + c2 = Constr.constr; "." -> + <:ast< (DEFINITION "COERCION" $s (CONSTR (CAST $c1 $c2))) >> | IDENT "Coercion"; IDENT "Local"; s = identarg; ":="; - c1 = Command.command; "." -> - <:ast< (DEFINITION "LCOERCION" $s (COMMAND $c1)) >> + c1 = Constr.constr; "." -> + <:ast< (DEFINITION "LCOERCION" $s (CONSTR $c1)) >> | IDENT "Coercion"; IDENT "Local"; s = identarg; ":="; - c1 = Command.command; ":"; c2 = Command.command; "." -> - <:ast< (DEFINITION "LCOERCION" $s (COMMAND (CAST $c1 $c2))) >> + c1 = Constr.constr; ":"; c2 = Constr.constr; "." -> + <:ast< (DEFINITION "LCOERCION" $s (CONSTR (CAST $c1 $c2))) >> | IDENT "Syntactic"; "Definition"; id = identarg; ":="; com = comarg; @@ -400,7 +400,7 @@ GEXTEND Gram ] ]; END -(* Proof commands *) +(* Proof constrs *) GEXTEND Gram vernac: [ [ IDENT "Goal"; c = comarg; "." -> <:ast< (GOAL $c) >> @@ -435,14 +435,14 @@ GEXTEND Gram | IDENT "Show"; IDENT "Node"; "." -> <:ast< (ShowNode) >> | IDENT "Show"; IDENT "Script"; "." -> <:ast< (ShowScript) >> | IDENT "Show"; IDENT "Existentials"; "." -> <:ast< (ShowEx) >> - | IDENT "Existential"; n = numarg; ":="; c = Command.command; "." -> - <:ast< (EXISTENTIAL $n (COMMAND $c)) >> - | IDENT "Existential"; n = numarg; ":="; c1 = Command.command; ":"; - c2 = Command.command; "." -> - <:ast< (EXISTENTIAL $n (COMMAND (CAST $c1 $c2))) >> - | IDENT "Existential"; n = numarg; ":"; c2 = Command.command; ":="; - c1 = Command.command; "." -> - <:ast< (EXISTENTIAL $n (COMMAND (CAST $c1 $c2))) >> + | IDENT "Existential"; n = numarg; ":="; c = Constr.constr; "." -> + <:ast< (EXISTENTIAL $n (CONSTR $c)) >> + | IDENT "Existential"; n = numarg; ":="; c1 = Constr.constr; ":"; + c2 = Constr.constr; "." -> + <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >> + | IDENT "Existential"; n = numarg; ":"; c2 = Constr.constr; ":="; + c1 = Constr.constr; "." -> + <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >> | IDENT "Explain"; "Proof"; l = numarg_list; "." -> <:ast< (ExplainProof ($LIST $l)) >> | IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list; "." -> diff --git a/syntax/PPCommand.v b/syntax/PPConstr.v index 7df18f7be..493f3c23a 100755 --- a/syntax/PPCommand.v +++ b/syntax/PPConstr.v @@ -154,6 +154,10 @@ Syntax constr -> [ [<hov 0> $H:E (APPTAIL ($LIST $T)):E ] ] | app_imp [(APPLISTEXPL $H ($LIST $T))] + -> [ [<hov 0> "!" $H:E (APPTAIL ($LIST $T)):E ] ] + +(* + | app_imp [(APPLISTEXPL $H ($LIST $T))] -> [ (APPLISTIMPL (ACC $H) ($LIST $T)):E ] | app_imp_arg [(APPLISTIMPL (ACC ($LIST $AC)) $a ($LIST $T))] @@ -164,20 +168,21 @@ Syntax constr | app_imp_last [(APPLISTIMPL (ACC ($LIST $A)) $T)] -> [ (APPLIST ($LIST $A) $T):E ] - +*) | apptailcons [ (APPTAIL $H ($LIST $T))] -> [ [1 1] $H:L (APPTAIL ($LIST $T)):E ] | apptailnil [(APPTAIL)] -> [ ] | apptailcons1 [(APPTAIL (EXPL "!" $n $c1) ($LIST $T))] -> [ [1 1] (EXPL $n $c1):L (APPTAIL ($LIST $T)):E ] + ; (* Implicits *) level 8: arg_implicit [(EXPL ($NUM $n) $c1)] -> [ $n "!" $c1:L ] - | arg_implicit1 [(EXPL "EX" ($NUM $n) $c1)] -> [ $n "!" $c1:L ] - | fun_explicit [(EXPL $f)] -> [ $f ] +(* | arg_implicit1 [(EXPL "EX" ($NUM $n) $c1)] -> [ $n "!" $c1:L ] + | fun_explicit [(EXPL $f)] -> [ $f ]*) ; |