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 --- syntax/PPCommand.v | 247 --------------------------------------------------- syntax/PPConstr.v | 252 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 252 insertions(+), 247 deletions(-) delete mode 100755 syntax/PPCommand.v create mode 100755 syntax/PPConstr.v (limited to 'syntax') 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