From 46e708f92deef78043f4f221293df131e29aeff1 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 7 Jan 2000 22:16:40 +0000 Subject: Renommage command en constr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@262 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_command.ml4 | 223 -------------------------------------------- parsing/g_constr.ml4 | 217 +++++++++++++++++++++++++++++++++++++++++++ parsing/g_tactic.ml4 | 5 +- parsing/g_vernac.ml4 | 108 +++++++++++----------- syntax/PPCommand.v | 247 ------------------------------------------------- syntax/PPConstr.v | 252 ++++++++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 526 insertions(+), 526 deletions(-) delete mode 100644 parsing/g_command.ml4 create mode 100644 parsing/g_constr.ml4 delete mode 100755 syntax/PPCommand.v create mode 100755 syntax/PPConstr.v diff --git a/parsing/g_command.ml4 b/parsing/g_command.ml4 deleted file mode 100644 index 7a0bab447d..0000000000 --- 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 0000000000..3640db1bc7 --- /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 586a1bd67d..424591efb7 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 2bc94c2003..81f9630832 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/PPCommand.v deleted file mode 100755 index 7df18f7be4..0000000000 --- a/syntax/PPCommand.v +++ /dev/null @@ -1,247 +0,0 @@ - -(* $Id$ *) - -(* Syntax for the Calculus of Constructions. *) - -Syntax constr - level 0: - ne_command_listcons [(NECOMMANDLIST $c1 ($LIST $cl))] - -> [ $c1 [1 0] (NECOMMANDLIST ($LIST $cl)) ] - | ne_command_listone [(NECOMMANDLIST $c1)] -> [ $c1 ] - ; - -(* Things parsed in binder *) -(* ======================= *) - - level 0: - idbindercons [(IDBINDER ($VAR $id) ($LIST $L))] -> - [ $id ","[0 0] (IDBINDER ($LIST $L))] - | idbinderone [(IDBINDER ($VAR $id))] -> [$id] - | idbindernil [(IDBINDER)] -> [ ] - - | binderscons [(BINDERS (BINDER $c ($LIST $id)) ($LIST $b))] -> - [ [ [ (IDBINDER ($LIST $id))] ":" - [0 1] $c:E] ";"[1 0] - (BINDERS ($LIST $b)) ] - | bindersone [(BINDERS (BINDER $c ($LIST $id)))] -> - [ [ (IDBINDER ($LIST $id))] ":" $c:E ] - ; - - -(* Things parsed in command0 *) - level 0: - prop [(PROP)] -> ["Prop"] - | set [(SET)] -> ["Set"] - | type [(TYPE)] -> ["Type"] - | type_sp [(TYPE ($PATH $sp) ($NUM $n))] -> ["Type"] -(* Note: Atomic constants (Nvar, CONST, MUTIND, MUTCONSTRUCT) are printed in - typing/printer to deal with the duality CCI/FW *) - - | evar [<< ? >>] -> ["?"] - | meta [(META ($NUM $n))] -> [ "?" $n ] - | implicit [(IMPLICIT)] -> [""] - | indice [(REL ($NUM $n))] -> [""] - ; - -(* Things parsed in command1 *) - level 1: - soap [(XTRA "$SOAPP" $lc1 ($LIST $cl))] - -> [ [ "(" $lc1 ")@[" (NECOMMANDLIST ($LIST $cl)) "]"] ] - | let_K [(ABST #Core#let.cci $M [<>]$N)] - -> [ [ "[_=" $M "]" [0 1] $N:E ] ] - - | let [<<[$x = $M]$N>>] -> [ [ "[" $x "=" $M:E "]" [0 1] $N:E ] ] - - | abstpat [[$id1]$c] -> [ [ "<<" $id1 ">>" [0 1] $c:E ] ] - ; - -(* Things parsed in command2 *) - -(* Things parsed in command3 *) - -(* Things parsed in command4 *) - -(* Things parsed in command5 *) - - level 5: - cast [<<($C :: $T)>>] -> [ [ $C:L [0 0] "::" $T:E] ] - ; -(* Things parsed in command6 *) - -(* Things parsed in command7 *) -(* Things parsed in command8 *) - level 8: -(* - lambda [(LAMBDA $Dom $Body)] - -> [(LAMBOX (BINDERS) (LAMBDA $Dom $Body))] - | lambdalist [(LAMBDALIST $c $body)] - -> [(LAMBOX (BINDERS) (LAMBDALIST $c $body))] - - | formated_lambda [(LAMBOX $pbi $t)] - -> [ [ "[" [ $pbi] "]" [0 1] $t:E ] ] - - | lambda_cons [(LAMBOX (BINDERS ($LIST $acc)) <<[$x : $Dom]$body>>)] - -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom $x)) $body)] - | lambda_cons_anon [(LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [<>]$body))] - -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom _)) $body)] - | lambdal_start [(LAMBOX $pbi (LAMBDALIST $Dom $Body))] - -> [(LAMLBOX $pbi $Dom (IDS) $Body)] - - | lambdal_end [(LAMLBOX (BINDERS ($LIST $acc)) $c (IDS ($LIST $ids)) $t)] - -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $c ($LIST $ids))) $t)] - | lambdal_cons_anon [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [<>]$body)] - -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) _) $body)] - | lambdal_cons [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body)] - -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) $id) $body)] -*) - lambda [(LAMBDA $Dom [$x]$Body)] - -> [(LAMBOX (BINDERS (BINDER $Dom $x)) $Body)] - | lambda_anon [(LAMBDA $Dom [<>]$Body)] - -> [(LAMBOX (BINDERS (BINDER $Dom _)) $Body)] - | lambdalist [(LAMBDALIST $c [$x]$body)] - -> [(LAMLBOX (BINDERS) $c (IDS $x) $body)] - | lambdalist_anon [(LAMBDALIST $c [<>]$body)] - -> [(LAMLBOX (BINDERS) $c (IDS _) $body)] - - | formated_lambda [(LAMBOX $pbi $t)] - -> [ [ "[" [ $pbi] "]" [0 1] $t:E ] ] - - | lambda_cons [(LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [$x]$body))] - -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom $x)) $body)] - | lambda_cons_anon [(LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [<>]$body))] - -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom _)) $body)] - | lambdal_start [(LAMBOX $pbi (LAMBDALIST $Dom $Body))] - -> [(LAMLBOX $pbi $Dom (IDS) $Body)] - - | lambdal_end [(LAMLBOX (BINDERS ($LIST $acc)) $c (IDS ($LIST $ids)) $t)] - -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $c ($LIST $ids))) $t)] - | lambdal_cons_anon [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [<>]$body)] - -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) _) $body)] - | lambdal_cons [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body)] - -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) $id) $body)] - - - | pi [<<($x : $A)$B>>] -> [(PRODBOX (BINDERS) <<($x : $A)$B>>)] - | prodlist [(PRODLIST $c $b)] - -> [(PRODBOX (BINDERS) (PRODLIST $c $b))] - - | formated_prod [(PRODBOX $pbi $t)] - -> [ [ "(" [ $pbi] ")" [0 1] $t:E ] ] - - | prod_cons [(PRODBOX (BINDERS ($LIST $acc)) <<($x : $Dom)$body>>)] - -> [(PRODBOX (BINDERS ($LIST $acc) (BINDER $Dom $x)) $body)] - | prodl_start_cons [(PRODBOX $pbi (PRODLIST $Dom $Body))] - -> [(PRODLBOX $pbi $Dom (IDS) $Body)] - - | prodl_end [(PRODLBOX (BINDERS ($LIST $acc)) $c (IDS ($LIST $ids)) $t)] - -> [(PRODBOX (BINDERS ($LIST $acc) (BINDER $c ($LIST $ids))) $t)] - | prodl_cons_anon [(PRODLBOX $pbi $c (IDS ($LIST $ids)) [<>]$body)] - -> [(PRODLBOX $pbi $c (IDS ($LIST $ids) _) $body)] - | prodl_cons [(PRODLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body)] - -> [(PRODLBOX $pbi $c (IDS ($LIST $ids) $id) $body)] - - - | arrow [<< $A -> $B >>] -> [ [ $A:L [0 0] "->" (ARROWBOX $B) ] ] - | arrow_stop [(ARROWBOX $c)] -> [ $c:E ] - | arrow_again [(ARROWBOX << $A -> $B >>)] -> [ $A:L [0 0] "->" (ARROWBOX $B) ] - ; - -(* Things parsed in command9 *) - -(* Things parsed in command10 *) - level 10: - app_cons [(APPLIST $H ($LIST $T))] - -> [ [ $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))] - -> [ (APPLISTIMPL (ACC ($LIST $AC) $a) ($LIST $T)):E ] - - | app_imp_imp_arg [ (APPLISTIMPL $AC (EXPL $_ $_) ($LIST $T)) ] - -> [ (APPLISTIMPL $AC ($LIST $T)):E ] - - | 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 ] - ; - - - level 8: - recpr [(XTRA "REC" ($LIST $RECARGS))] -> [ (RECTERM ($LIST $RECARGS)) ] - - | recterm [(RECTERM $P $c ($LIST $BL))] -> - [ [ [ "<" $P:E ">" - [0 2] [ "Match" [1 1] $c:E [1 0] "with" ]] - [1 3] [ (MATCHBRANCHES ($LIST $BL)):E ] "end"] ] - - | mlcasepr [(XTRA "MLCASE" "NOREC" ($LIST $RECARGS))] - -> [ (MLCASETERM ($LIST $RECARGS)) ] - - | mlcaseterm [(MLCASETERM $c ($LIST $BL))] -> - [ [ [ "Case" [1 1] $c:E [1 0] "of" ] - [1 3] [ (MATCHBRANCHES ($LIST $BL)):E ]"end"] ] - - | mlmatchpr [(XTRA "MLCASE" "REC" ($LIST $RECARGS))] - -> [ (MLMATCHTERM ($LIST $RECARGS)) ] - - | mlmatchterm [(MLMATCHTERM $c ($LIST $BL))] -> - [ [ [ "Match" [1 1] $c:E [1 0] "with" ] - [1 3] [ (MATCHBRANCHES ($LIST $BL)):E ] "end"] ] - - - | matchbranchescons [(MATCHBRANCHES $B ($LIST $T))] - -> [ [ [ $B:E ] FNL] (MATCHBRANCHES ($LIST $T)):E ] - | matchbranchesnil [(MATCHBRANCHES)] -> [ ] - - | casepr [(MUTCASE ($LIST $MATCHARGS))] -> [ (CASETERM ($LIST $MATCHARGS)) ] - | caseterm [(CASETERM $P $c ($LIST $BL))] -> - [ [ [ "<" $P:E ">" - [0 2][ "Case" [1 1] $c:E [1 0] "of" ]] - [1 3][ (MATCHBRANCHES ($LIST $BL)):E ] "end"] ] - ; - - level 0: - fix [(FIX $f $def ($LIST $lfs))] -> - [ [ "Fix " $f - [0 2] "{" [ [ $def] - (FIXDECLS ($LIST $lfs)) ] "}"] ] - - | cofix [(COFIX $f $def ($LIST $lfs))] -> - [ [ "CoFix " $f - [0 2] "{" [ [ $def] - (FIXDECLS ($LIST $lfs)) ] "}"] ] - - | nofixdefs [(FIXDECLS)] -> [ ] - | fixdefs [(FIXDECLS $def1 ($LIST $defs))] -> - [ FNL [ "with " $def1] (FIXDECLS ($LIST $defs)) ] - ; - - level 8: - onefixnumdecl [(NUMFDECL $f ($NUM $x) $A $t)] -> - [ $f "/" $x " :" - [1 2] $A:E " :=" - [1 2] $t:E ] - | onefixdecl [(FDECL $f (BINDERS ($LIST $l)) $A $t)] -> - [ $f - [1 2] "[" [ (BINDERS ($LIST $l))] "]" - [1 2] ": " $A:E " :=" - [1 2] $t:E ] - | onecofixdecl [(CFDECL $f $A $t)] -> - [ $f " : " - [1 2] $A:E " :=" - [1 2] $t:E ]. diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v new file mode 100755 index 0000000000..493f3c23af --- /dev/null +++ b/syntax/PPConstr.v @@ -0,0 +1,252 @@ + +(* $Id$ *) + +(* Syntax for the Calculus of Constructions. *) + +Syntax constr + level 0: + ne_command_listcons [(NECOMMANDLIST $c1 ($LIST $cl))] + -> [ $c1 [1 0] (NECOMMANDLIST ($LIST $cl)) ] + | ne_command_listone [(NECOMMANDLIST $c1)] -> [ $c1 ] + ; + +(* Things parsed in binder *) +(* ======================= *) + + level 0: + idbindercons [(IDBINDER ($VAR $id) ($LIST $L))] -> + [ $id ","[0 0] (IDBINDER ($LIST $L))] + | idbinderone [(IDBINDER ($VAR $id))] -> [$id] + | idbindernil [(IDBINDER)] -> [ ] + + | binderscons [(BINDERS (BINDER $c ($LIST $id)) ($LIST $b))] -> + [ [ [ (IDBINDER ($LIST $id))] ":" + [0 1] $c:E] ";"[1 0] + (BINDERS ($LIST $b)) ] + | bindersone [(BINDERS (BINDER $c ($LIST $id)))] -> + [ [ (IDBINDER ($LIST $id))] ":" $c:E ] + ; + + +(* Things parsed in command0 *) + level 0: + prop [(PROP)] -> ["Prop"] + | set [(SET)] -> ["Set"] + | type [(TYPE)] -> ["Type"] + | type_sp [(TYPE ($PATH $sp) ($NUM $n))] -> ["Type"] +(* Note: Atomic constants (Nvar, CONST, MUTIND, MUTCONSTRUCT) are printed in + typing/printer to deal with the duality CCI/FW *) + + | evar [<< ? >>] -> ["?"] + | meta [(META ($NUM $n))] -> [ "?" $n ] + | implicit [(IMPLICIT)] -> [""] + | indice [(REL ($NUM $n))] -> [""] + ; + +(* Things parsed in command1 *) + level 1: + soap [(XTRA "$SOAPP" $lc1 ($LIST $cl))] + -> [ [ "(" $lc1 ")@[" (NECOMMANDLIST ($LIST $cl)) "]"] ] + | let_K [(ABST #Core#let.cci $M [<>]$N)] + -> [ [ "[_=" $M "]" [0 1] $N:E ] ] + + | let [<<[$x = $M]$N>>] -> [ [ "[" $x "=" $M:E "]" [0 1] $N:E ] ] + + | abstpat [[$id1]$c] -> [ [ "<<" $id1 ">>" [0 1] $c:E ] ] + ; + +(* Things parsed in command2 *) + +(* Things parsed in command3 *) + +(* Things parsed in command4 *) + +(* Things parsed in command5 *) + + level 5: + cast [<<($C :: $T)>>] -> [ [ $C:L [0 0] "::" $T:E] ] + ; +(* Things parsed in command6 *) + +(* Things parsed in command7 *) +(* Things parsed in command8 *) + level 8: +(* + lambda [(LAMBDA $Dom $Body)] + -> [(LAMBOX (BINDERS) (LAMBDA $Dom $Body))] + | lambdalist [(LAMBDALIST $c $body)] + -> [(LAMBOX (BINDERS) (LAMBDALIST $c $body))] + + | formated_lambda [(LAMBOX $pbi $t)] + -> [ [ "[" [ $pbi] "]" [0 1] $t:E ] ] + + | lambda_cons [(LAMBOX (BINDERS ($LIST $acc)) <<[$x : $Dom]$body>>)] + -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom $x)) $body)] + | lambda_cons_anon [(LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [<>]$body))] + -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom _)) $body)] + | lambdal_start [(LAMBOX $pbi (LAMBDALIST $Dom $Body))] + -> [(LAMLBOX $pbi $Dom (IDS) $Body)] + + | lambdal_end [(LAMLBOX (BINDERS ($LIST $acc)) $c (IDS ($LIST $ids)) $t)] + -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $c ($LIST $ids))) $t)] + | lambdal_cons_anon [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [<>]$body)] + -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) _) $body)] + | lambdal_cons [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body)] + -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) $id) $body)] +*) + lambda [(LAMBDA $Dom [$x]$Body)] + -> [(LAMBOX (BINDERS (BINDER $Dom $x)) $Body)] + | lambda_anon [(LAMBDA $Dom [<>]$Body)] + -> [(LAMBOX (BINDERS (BINDER $Dom _)) $Body)] + | lambdalist [(LAMBDALIST $c [$x]$body)] + -> [(LAMLBOX (BINDERS) $c (IDS $x) $body)] + | lambdalist_anon [(LAMBDALIST $c [<>]$body)] + -> [(LAMLBOX (BINDERS) $c (IDS _) $body)] + + | formated_lambda [(LAMBOX $pbi $t)] + -> [ [ "[" [ $pbi] "]" [0 1] $t:E ] ] + + | lambda_cons [(LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [$x]$body))] + -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom $x)) $body)] + | lambda_cons_anon [(LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [<>]$body))] + -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom _)) $body)] + | lambdal_start [(LAMBOX $pbi (LAMBDALIST $Dom $Body))] + -> [(LAMLBOX $pbi $Dom (IDS) $Body)] + + | lambdal_end [(LAMLBOX (BINDERS ($LIST $acc)) $c (IDS ($LIST $ids)) $t)] + -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $c ($LIST $ids))) $t)] + | lambdal_cons_anon [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [<>]$body)] + -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) _) $body)] + | lambdal_cons [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body)] + -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) $id) $body)] + + + | pi [<<($x : $A)$B>>] -> [(PRODBOX (BINDERS) <<($x : $A)$B>>)] + | prodlist [(PRODLIST $c $b)] + -> [(PRODBOX (BINDERS) (PRODLIST $c $b))] + + | formated_prod [(PRODBOX $pbi $t)] + -> [ [ "(" [ $pbi] ")" [0 1] $t:E ] ] + + | prod_cons [(PRODBOX (BINDERS ($LIST $acc)) <<($x : $Dom)$body>>)] + -> [(PRODBOX (BINDERS ($LIST $acc) (BINDER $Dom $x)) $body)] + | prodl_start_cons [(PRODBOX $pbi (PRODLIST $Dom $Body))] + -> [(PRODLBOX $pbi $Dom (IDS) $Body)] + + | prodl_end [(PRODLBOX (BINDERS ($LIST $acc)) $c (IDS ($LIST $ids)) $t)] + -> [(PRODBOX (BINDERS ($LIST $acc) (BINDER $c ($LIST $ids))) $t)] + | prodl_cons_anon [(PRODLBOX $pbi $c (IDS ($LIST $ids)) [<>]$body)] + -> [(PRODLBOX $pbi $c (IDS ($LIST $ids) _) $body)] + | prodl_cons [(PRODLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body)] + -> [(PRODLBOX $pbi $c (IDS ($LIST $ids) $id) $body)] + + + | arrow [<< $A -> $B >>] -> [ [ $A:L [0 0] "->" (ARROWBOX $B) ] ] + | arrow_stop [(ARROWBOX $c)] -> [ $c:E ] + | arrow_again [(ARROWBOX << $A -> $B >>)] -> [ $A:L [0 0] "->" (ARROWBOX $B) ] + ; + +(* Things parsed in command9 *) + +(* Things parsed in command10 *) + level 10: + app_cons [(APPLIST $H ($LIST $T))] + -> [ [ $H:E (APPTAIL ($LIST $T)):E ] ] + + | app_imp [(APPLISTEXPL $H ($LIST $T))] + -> [ [ "!" $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))] + -> [ (APPLISTIMPL (ACC ($LIST $AC) $a) ($LIST $T)):E ] + + | app_imp_imp_arg [ (APPLISTIMPL $AC (EXPL $_ $_) ($LIST $T)) ] + -> [ (APPLISTIMPL $AC ($LIST $T)):E ] + + | 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 ]*) + ; + + + level 8: + recpr [(XTRA "REC" ($LIST $RECARGS))] -> [ (RECTERM ($LIST $RECARGS)) ] + + | recterm [(RECTERM $P $c ($LIST $BL))] -> + [ [ [ "<" $P:E ">" + [0 2] [ "Match" [1 1] $c:E [1 0] "with" ]] + [1 3] [ (MATCHBRANCHES ($LIST $BL)):E ] "end"] ] + + | mlcasepr [(XTRA "MLCASE" "NOREC" ($LIST $RECARGS))] + -> [ (MLCASETERM ($LIST $RECARGS)) ] + + | mlcaseterm [(MLCASETERM $c ($LIST $BL))] -> + [ [ [ "Case" [1 1] $c:E [1 0] "of" ] + [1 3] [ (MATCHBRANCHES ($LIST $BL)):E ]"end"] ] + + | mlmatchpr [(XTRA "MLCASE" "REC" ($LIST $RECARGS))] + -> [ (MLMATCHTERM ($LIST $RECARGS)) ] + + | mlmatchterm [(MLMATCHTERM $c ($LIST $BL))] -> + [ [ [ "Match" [1 1] $c:E [1 0] "with" ] + [1 3] [ (MATCHBRANCHES ($LIST $BL)):E ] "end"] ] + + + | matchbranchescons [(MATCHBRANCHES $B ($LIST $T))] + -> [ [ [ $B:E ] FNL] (MATCHBRANCHES ($LIST $T)):E ] + | matchbranchesnil [(MATCHBRANCHES)] -> [ ] + + | casepr [(MUTCASE ($LIST $MATCHARGS))] -> [ (CASETERM ($LIST $MATCHARGS)) ] + | caseterm [(CASETERM $P $c ($LIST $BL))] -> + [ [ [ "<" $P:E ">" + [0 2][ "Case" [1 1] $c:E [1 0] "of" ]] + [1 3][ (MATCHBRANCHES ($LIST $BL)):E ] "end"] ] + ; + + level 0: + fix [(FIX $f $def ($LIST $lfs))] -> + [ [ "Fix " $f + [0 2] "{" [ [ $def] + (FIXDECLS ($LIST $lfs)) ] "}"] ] + + | cofix [(COFIX $f $def ($LIST $lfs))] -> + [ [ "CoFix " $f + [0 2] "{" [ [ $def] + (FIXDECLS ($LIST $lfs)) ] "}"] ] + + | nofixdefs [(FIXDECLS)] -> [ ] + | fixdefs [(FIXDECLS $def1 ($LIST $defs))] -> + [ FNL [ "with " $def1] (FIXDECLS ($LIST $defs)) ] + ; + + level 8: + onefixnumdecl [(NUMFDECL $f ($NUM $x) $A $t)] -> + [ $f "/" $x " :" + [1 2] $A:E " :=" + [1 2] $t:E ] + | onefixdecl [(FDECL $f (BINDERS ($LIST $l)) $A $t)] -> + [ $f + [1 2] "[" [ (BINDERS ($LIST $l))] "]" + [1 2] ": " $A:E " :=" + [1 2] $t:E ] + | onecofixdecl [(CFDECL $f $A $t)] -> + [ $f " : " + [1 2] $A:E " :=" + [1 2] $t:E ]. -- cgit v1.2.3