From 80697ce416e2af26b86f0b81bec5b702710fcf1f Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 6 Dec 1999 22:21:36 +0000 Subject: PPMultipleCase.v -> PPCases.v et MAJ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@215 85f007b7-540e-0410-9357-904b9bb8a0f7 --- syntax/MakeBare.v | 2 +- syntax/PPCases.v | 86 +++++++++++++++++++++++++++++++++++++++ syntax/PPMultipleCase.v | 106 ------------------------------------------------ 3 files changed, 87 insertions(+), 107 deletions(-) create mode 100644 syntax/PPCases.v delete mode 100755 syntax/PPMultipleCase.v (limited to 'syntax') diff --git a/syntax/MakeBare.v b/syntax/MakeBare.v index a3fe30035c..8740d5a04d 100644 --- a/syntax/MakeBare.v +++ b/syntax/MakeBare.v @@ -1,3 +1,3 @@ Load PPCommand. Load PPTactic. -Load PPMultipleCase. +Load PPCases. diff --git a/syntax/PPCases.v b/syntax/PPCases.v new file mode 100644 index 0000000000..801de0a67d --- /dev/null +++ b/syntax/PPCases.v @@ -0,0 +1,86 @@ + +(* $Id$ *) + +Syntax constr + level 0: + ne_command_listcons2 [(NECOMMANDLIST2 $c1 ($LIST $cl))] + -> [ $c1:L [1 0] (NECOMMANDLIST2 ($LIST $cl)) ] + | ne_command_listone2 [(NECOMMANDLIST2 $c1)] -> [$c1:L] + ; + + level 10: + as_patt [(PATTAS $var $patt)] -> [$patt:L" as "$var] + ; + + level 0: + ne_pattlist_nil [(PATTLIST)] -> [ ] + | ne_pattlist_cons [(PATTLIST $patt ($LIST $lpatt))] + -> [$patt:E " " (PATTLIST ($LIST $lpatt))] + ; + + level 8: + equation [(EQN $rhs ($LIST $lhs))] + -> [ [ (PATTLIST ($LIST $lhs)) "=> " [0 1] $rhs:E] ] + ; + + level 0: + bar_eqnlist_nil [(BAREQNLIST)] -> [ ] + | bar_eqnlist_cons [(BAREQNLIST $eqn ($LIST $leqn))] + -> [ "| " $eqn [1 0] (BAREQNLIST ($LIST $leqn)) ] + | bar_eqnlist_one [(BAREQNLIST $eqn)] + -> [ "| " $eqn ] + + | tomatch [(TOMATCH ($LIST $lc))] -> [(NECOMMANDLIST2 ($LIST $lc)):E] + ; + + level 10: + pattconstruct [(PATTCONSTRUCT ($LIST $T))] -> [(APPLIST ($LIST $T))] + ; + + level 8: + + cases_exp_none [(MULTCASE $pred $tomatch)] + -> [ [ (ELIMPRED $pred) + [ "Cases"[1 2] $tomatch:E [1 0] "of"] [1 0] "end"] ] + + | cases_exp_one [(MULTCASE $pred $tomatch $eqn)] + -> [ [ (ELIMPRED $pred) + [ [ "Cases"[1 2] $tomatch:E [1 0] "of"] [1 2] + $eqn [1 0] + "end"] ] ] + + | cases_exp_many [(MULTCASE $pred $tomatch $eqn1 $eqn2 ($LIST $eqns))] + -> [ [ (ELIMPRED $pred) + [ [ "Cases"[1 2] $tomatch:E [1 0] "of"] [1 2] + $eqn1 [1 0] + (BAREQNLIST $eqn2 ($LIST $eqns)) [1 0] + "end"] ] ] + + (* "level" indifférent pour ce qui suit *) + | let_binder_var [(LETBINDER ($VAR $id))] -> [ $id ] + | let_binder_app [(LETBINDER (APPLIST $toforget ($VAR $id) ($LIST $vars)))] + -> [ "(" $id (LETBINDERTAIL ($LIST $vars)) ")" ] + + | let_binder_tail_nil [(LETBINDERTAIL)] -> [ ] + | let_binder_tail_cons [(LETBINDERTAIL $var ($LIST $vars))] + -> [ "," [1 0] $var (LETBINDERTAIL ($LIST $vars)) ] + + | elim_pred [(ELIMPRED $pred)] -> [ "<" $pred:E ">" [0 2] ] + | elim_pred_xtra [(ELIMPRED "SYNTH")] -> [ ] + ; + + (* On force les parenthèses autour d'un "if" sous-terme (même si le + parsing est lui plus tolérant) *) + level 10: + boolean_cases [(FORCEIF $pred $tomatch (EQN $c1 $_) (EQN $c2 $_))] + -> [ [ (ELIMPRED $pred) + [ "if " [ $tomatch:E ] + [1 0] [ "then" [1 1] $c1:E ] + [1 0] [ "else" [1 1] $c2:E ] ] ] ] + + | let_cases [(FORCELET $pred $tomatch (EQN $c $pat))] + -> [ [ (ELIMPRED $pred) + [ "let " [ (LETBINDER $pat) ] " =" + [1 1] [ $tomatch:E ] ] + [1 0] "in " [ $c:E ] ] ] +. diff --git a/syntax/PPMultipleCase.v b/syntax/PPMultipleCase.v deleted file mode 100755 index 51f75569eb..0000000000 --- a/syntax/PPMultipleCase.v +++ /dev/null @@ -1,106 +0,0 @@ -(****************************************************************************) -(* The Calculus of Inductive Constructions *) -(* *) -(* Projet Coq *) -(* *) -(* INRIA ENS-CNRS *) -(* Rocquencourt Lyon *) -(* *) -(* Coq V5.10 *) -(* Nov 25th 1994 *) -(* *) -(****************************************************************************) -(* PPMutilpleCase.v *) -(****************************************************************************) - - -Syntax constr - level 0: - ne_command_listcons2 [(NECOMMANDLIST2 $c1 ($LIST $cl))] - -> [ $c1:L [1 0] (NECOMMANDLIST2 ($LIST $cl)) ] - | ne_command_listone2 [(NECOMMANDLIST2 $c1)] -> [$c1:L] - ; - - level 10: - as_patt [(XTRA "AS" $var $patt)] -> [$patt:L" as "$var] - ; - - level 0: - ne_pattlist_nil [(PATTLIST)] -> [ ] - | ne_pattlist_cons [(PATTLIST $patt ($LIST $lpatt))] - -> [$patt:E " " (PATTLIST ($LIST $lpatt))] - ; - - level 8: - equation [(XTRA "EQN" $rhs ($LIST $lhs))] - -> [ [ (PATTLIST ($LIST $lhs)) "=> " [0 1] $rhs:E] ] - | lam_eqn [(XTRA "LAMEQN" $eq)] -> [ $eq ] - | lam_eqn_var [(XTRA "LAMEQN" ($ID $id) ($LIST $l))] - -> [(XTRA "LAMEQN" ($LIST $l))] - | lam_eqn_dlam [(XTRA "LAMEQN" [$_]$eq)] -> [(XTRA "LAMEQN" $eq)] - | lam_eqn_dlam_anon [(XTRA "LAMEQN" [<>]$eq)] -> [(XTRA "LAMEQN" $eq)] - ; - - level 0: - bar_eqnlist_nil [(BAREQNLIST)] -> [ ] - | bar_eqnlist_cons [(BAREQNLIST $eqn ($LIST $leqn))] - -> [ "| " $eqn [1 0] (BAREQNLIST ($LIST $leqn)) ] - | bar_eqnlist_one [(BAREQNLIST $eqn)] - -> [ "| " $eqn ] - - | tomatch [(XTRA "TOMATCH" ($LIST $lc))] -> [(NECOMMANDLIST2 ($LIST $lc)):E] - ; - - level 8: - - cases_exp_none [(XTRA "MULTCASE" $pred $tomatch)] - -> [ [ (ELIMPRED $pred) - [ "Cases"[1 2] $tomatch:E [1 0] "of"] [1 0] "end"] ] - - | cases_exp_one [(XTRA "MULTCASE" $pred $tomatch $eqn)] - -> [ [ (ELIMPRED $pred) - [ [ "Cases"[1 2] $tomatch:E [1 0] "of"] [1 2] - $eqn [1 0] - "end"] ] ] - - | cases_exp_many [(XTRA "MULTCASE" $pred $tomatch $eqn1 $eqn2 ($LIST $eqns))] - -> [ [ (ELIMPRED $pred) - [ [ "Cases"[1 2] $tomatch:E [1 0] "of"] [1 2] - $eqn1 [1 0] - (BAREQNLIST $eqn2 ($LIST $eqns)) [1 0] - "end"] ] ] - - (* "level" indifférent pour ce qui suit *) - | let_binder_var [(LETBINDER ($VAR $id))] -> [ $id ] - | let_binder_app [(LETBINDER (APPLIST $toforget ($VAR $id) ($LIST $vars)))] - -> [ "(" $id (LETBINDERTAIL ($LIST $vars)) ")" ] - - | let_binder_tail_nil [(LETBINDERTAIL)] -> [ ] - | let_binder_tail_cons [(LETBINDERTAIL $var ($LIST $vars))] - -> [ "," [1 0] $var (LETBINDERTAIL ($LIST $vars)) ] - - | elim_pred [(ELIMPRED $pred)] -> [ "<" $pred:E ">" [0 2] ] - | elim_pred_xtra [(ELIMPRED (XTRA"SYNTH"))] -> [ ] - ; - - (* On force les parenthèses autour d'un "if" sous-terme (même si le - parsing est lui plus tolérant) *) - level 10: - boolean_cases [(FORCEIF $pred $tomatch $c1 $c2)] - -> [ [ (ELIMPRED $pred) - [ "if " [ $tomatch:E ] - [1 0] [ "then" [1 1] $c1:E ] - [1 0] [ "else" [1 1] $c2:E ] ] ] ] - - (* Tiens ! - Pourquoi l'AST n'est pas (FORCELET $pred tomatch (EQN $c $pat)) ? - Réponse : FORCELET, c'est par commodité, EQN, c'est parce qu'au parsing - il y a un XTRA devant **) - - - | let_cases [(XTRA "FORCELET" $pred $tomatch (XTRA "EQN" $c $pat))] - -> [ [ (ELIMPRED $pred) - [ "let " [ (LETBINDER $pat) ] " =" - [1 1] [ $tomatch:E ] ] - [1 0] "in " [ $c:E ] ] ] -. -- cgit v1.2.3