summaryrefslogtreecommitdiff
path: root/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'syntax')
-rw-r--r--syntax/MakeBare.v9
-rw-r--r--syntax/PPCases.v96
-rwxr-xr-xsyntax/PPConstr.v264
3 files changed, 0 insertions, 369 deletions
diff --git a/syntax/MakeBare.v b/syntax/MakeBare.v
deleted file mode 100644
index 28d9b5ea..00000000
--- a/syntax/MakeBare.v
+++ /dev/null
@@ -1,9 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-Load PPConstr.
-Load PPCases.
diff --git a/syntax/PPCases.v b/syntax/PPCases.v
deleted file mode 100644
index d0f75dcf..00000000
--- a/syntax/PPCases.v
+++ /dev/null
@@ -1,96 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* $Id: PPCases.v,v 1.11.6.1 2004/07/16 19:30:51 herbelin Exp $ *)
-
-Syntax constr
- level 8:
- tomatch_cons [ << (TOMATCH $c1 ($LIST $cl)) >> ]
- -> [ $c1:L [1 0] (TOMATCH ($LIST $cl)) ]
- | tomatch_one [ << (TOMATCH $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)) >> ]
- -> [ [<hov 0> (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 ]
- ;
-
- level 10:
- pattconstruct [ << (PATTCONSTRUCT $C $D ($LIST $T)) >> ] ->
- [(APPLIST $C $D ($LIST $T))]
- ;
-
- level 0:
- pattconstructatomic [ << (PATTCONSTRUCT $C) >> ] -> [ $C:E ]
- ;
-
- level 8:
-
- cases_exp_none [ << (CASES $pred $tomatch) >> ]
- -> [ [<hov 0> (ELIMPRED $pred)
- [<hv 0> "Cases"[1 2] $tomatch:E [1 0] "of"] [1 0] "end"] ]
-
- | cases_exp_one [ << (CASES $pred $tomatch $eqn) >> ]
- -> [ [<hov 0> (ELIMPRED $pred)
- [<hv 0> [<hv 0> "Cases"[1 2] $tomatch:E [1 0] "of"] [1 2]
- $eqn [1 0]
- "end"] ] ]
-
- | cases_exp_many [ << (CASES $pred $tomatch $eqn1 $eqn2 ($LIST $eqns)) >> ]
- -> [ [<hov 0> (ELIMPRED $pred)
- [<v 0> [<hv 0> "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 (PATTCONSTRUCT $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)) ]
-
- ;
-
- (* 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) >> ]
- -> [ [<hov 0> (ELIMPRED $pred)
- [<hv 0> "if " [<hov 0> $tomatch:L ]
- [1 0] [<hov 0> "then" [1 1] $c1:L ]
- [1 0] [<hov 0> "else" [1 1] $c2:L ] ] ] ]
-
- | let_cases [ << (FORCELET $pred $tomatch (EQN $c $pat)) >> ]
- -> [ [<hov 0> (ELIMPRED $pred)
- [<hv 0> "let " [<hov 0> (LETBINDER $pat) ] " ="
- [1 1] [<hov 0> $tomatch:L ] ]
- [1 0] "in " [<hov 0> $c:L ] ] ]
-.
-
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
deleted file mode 100755
index a4374c86..00000000
--- a/syntax/PPConstr.v
+++ /dev/null
@@ -1,264 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* $Id: PPConstr.v,v 1.25.2.1 2004/07/16 19:30:51 herbelin Exp $ *)
-
-(* 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)) >> ] ->
- [ [<hv 0> [<hov 0> (IDBINDER ($LIST $id))] ":"
- [0 1] $c:E] ";"[1 0]
- (BINDERS ($LIST $b)) ]
- | bindersone [ << (BINDERS (BINDER $c ($LIST $id))) >> ] ->
- [ [<hov 0> (IDBINDER ($LIST $id))] ":" $c:E ]
-
- | letbindercons [ << (BINDERS (LETBINDER $c $id) ($LIST $b)) >> ] ->
- [ [<hov 0> id ":=" [0 1] $c:E ";" [1 0] (BINDERS ($LIST $b)) ] ]
- | letbinderone [ << (BINDERS (LETBINDER $c $id)) >> ] ->
- [ [<hov 0> id ":=" [0 1] $c:E ] ]
- ;
-
-
-(* Things parsed in command0 *)
- level 0:
- prop [ Prop ] -> ["Prop"]
- | set [ Set ] -> ["Set"]
- | type [ Type ] -> ["Type"]
- | type_sp [ << (TYPE $id) >> ] -> ["Type" $id]
-(* Note: Atomic constants (Nvar, CONST, MUTIND, MUTCONSTRUCT) are printed in
- Printer to know if they must be qualified or not (and previously to
- deal with the duality CCI/FW) *)
-
- | evar [ ? ] -> ["?"]
- | meta [ << (META $n) >> ] -> [ $n ]
- | implicit [ << (IMPLICIT) >> ] -> ["<Implicit>"]
- | indice [ << (REL ($NUM $n)) >> ] -> ["<Unbound ref: " $n ">"]
- | instantiation [ << (INSTANCE $a ($LIST $l)) >> ] ->
- [ $a "{" (CONTEXT ($LIST $l)) "}"]
- | instantiation_nil [ << (CONTEXT) >> ] -> [ ]
- | instantiation_one [ << (CONTEXT $a) >> ] -> [ $a ]
- | instantiation_many [ << (CONTEXT $a $b ($LIST $l)) >> ] ->
- [ (CONTEXT $b ($LIST $l)) ";" $a ]
- | qualid [ << (QUALID $id ($LIST $l)) >> ] -> [ $id (FIELDS ($LIST $l)) ]
- | fieldsnil [ << (FIELDS) >> ] -> [ ]
- | fieldscons [ << (FIELDS $id ($LIST $l)) >> ] ->
- [ "." $id (FIELDS ($LIST $l)) ]
- ;
-
-(* Things parsed in command1 *)
- level 1:
- soap [ << (SOAPP $lc1 ($LIST $cl)) >> ]
- -> [ [<hov 0> "(" $lc1 ")@[" (NECOMMANDLIST ($LIST $cl)) "]"] ]
-
- (* For debug *)
- | abstpatnamed [ << [$id1]$c >> ] -> [ [<hov 0> "<<" $id1 ">>" [0 1] $c:E ] ]
- | abstpatanon [ << [ <> ]$c >> ] -> [ [<hov 0> "<<_>>" [0 1] $c:E ] ]
- ;
-
-(* Things parsed in command2 *)
-
-(* Things parsed in command3 *)
-
-(* Things parsed in command4 *)
-
-(* Things parsed in command5 *)
-
-(* Things parsed in command6 *)
-
-(* Things parsed in command7 *)
-
-(* Things parsed in command8 *)
- level 8:
- 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) >> ]
- -> [ [<hov 0> "[" [<hv 0> $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 [ << (PROD $A [$x]$B) >> ] -> [ (PRODBOX (BINDERS) (PROD $A [$x]$B)) ]
- | prodlist [ << (PRODLIST $c $b) >> ]
- -> [(PRODBOX (BINDERS) (PRODLIST $c $b))]
-
- | formated_prod [ << (PRODBOX $pbi $t) >> ]
- -> [ [<hov 0> "(" [<hov 0> $pbi] ")" [0 1] $t:E ] ]
-
- | prod_cons
- [ << (PRODBOX (BINDERS ($LIST $acc)) (PROD $Dom [$x]$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 [ << (ARROW $A [<>]$B) >> ] ->
- [ [<hv 0> $A:L " ->" [0 0] (ARROWBOX $B) ] ]
- | arrow_stop [ << (ARROWBOX $c) >> ] -> [ $c:E ]
- | arrow_again [ << (ARROWBOX (PROD $A [<>]$B)) >> ] ->
- [ $A:L " ->" [0 0] (ARROWBOX $B) ]
-
-(* These are synonymous *)
-(* redundant
- | let [ [$x = $M]$N ] -> [ [<hov 0> "[" $x "=" $M:E "]" [0 1] $N:E ] ]
-*)
- | letin [ << (LETIN $A [$x]$B) >> ] -> [ [ <hov 0> "[" $x ":=" [0 1] $A:E "]" [0 1] $B:E ] ]
- | letincast [ << (LETIN (CAST $A $C) [$x]$B) >> ] -> [ [ <hov 0> "[" $x ":=" [0 1] $A:E ":" $C:E "]" [0 1] $B:E ] ]
- ;
-
-(* Things parsed in command9 *)
- level 9:
- cast [ << (CAST $C $T) >> ] -> [ [<hv 0> $C:L [0 0] "::" $T:E] ]
- ;
-
-(* Things parsed in command10 *)
- level 10:
- app_cons [ << (APPLIST $H ($LIST $T)) >> ]
- -> [ [<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)) >> ]
- -> [ (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) >> ] -> [ ]
-
-(* Implicits *)
- | apptailcons1 [ << (APPTAIL (EXPL $n $c1) ($LIST $T)) >> ]
- -> [ [1 1] $n "!" $c1:E (APPTAIL ($LIST $T)):E ]
- ;
-(*
- 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:
- recterm [ << (MATCH $P $c ($LIST $BL)) >> ] ->
- [ [<hov 0> [<hov 0> (ELIMPRED $P)
- [0 2] [<hov 0> "Match" [1 1] $c:E [1 0] "with" ]]
- [1 3] [<hov 0> (MATCHBRANCHES ($LIST $BL)):E ] "end"] ]
-
- | matchbranchescons [ << (MATCHBRANCHES $B ($LIST $T)) >> ]
- -> [ [<hov 0> [<hov 0> $B:E ] FNL] (MATCHBRANCHES ($LIST $T)):E ]
- | matchbranchesnil [ << (MATCHBRANCHES) >> ] -> [ ]
-
- | caseterm [ << (CASE $P $c ($LIST $BL)) >> ] ->
- [ [<hov 0> [<hov 0> (ELIMPRED $P)
- [0 2][<hov 0> "Case" [1 1] $c:E [1 0] "of" ]]
- [1 3][<hov 0> (MATCHBRANCHES ($LIST $BL)):E ] "end"] ]
-
- | ifterm [ << (IF $P $c $b1 $b2) >> ] ->
- [ (FORCEIF $P $c (EQN $b1 JUNK) (EQN $b2 JUNK)):E ]
-
- | letterm [ << (LET $P $c (LAMBDALIST $_ $b)) >> ] ->
- [ (LETSLAM $P $c $b) ]
- | letslamend [ << (LETSLAM $P $c $b ($LIST $IDL))>> ] ->
- [ (FORCELET $P $c (EQN $b (PATTCONSTRUCT JUNK ($LIST $IDL)))):E ]
- | letslam [ << (LETSLAM $P $c [$ID]$b ($LIST $IDL))>> ] ->
- [ (LETSLAM $P $c $b ($LIST $IDL) $ID) ]
- | letslamanon [ << (LETSLAM $P $c [<>]$b ($LIST $IDL))>> ] ->
- [ (LETSLAM $P $c $b ($LIST $IDL) _) ]
-
- | elim_pred [ << (ELIMPRED $pred) >> ] -> [ "<" $pred:E ">" [0 2] ]
- | elim_pred_xtra [ << (ELIMPRED "SYNTH") >> ] -> [ ]
- ;
-
- level 0:
- fix [ << (FIX $f $def ($LIST $lfs)) >> ] ->
- [ [<hov 0> "Fix " $f
- [0 2] "{" [<v 0> [<hov 0> $def]
- (FIXDECLS ($LIST $lfs)) ] "}"] ]
-
- | cofix [ << (COFIX $f $def ($LIST $lfs)) >> ] ->
- [ [<hov 0> "CoFix " $f
- [0 2] "{" [<v 0> [<hov 0> $def]
- (FIXDECLS ($LIST $lfs)) ] "}"] ]
-
- | nofixdefs [ << (FIXDECLS) >> ] -> [ ]
- | fixdefs [ << (FIXDECLS $def1 ($LIST $defs)) >> ] ->
- [ FNL [<hov 0> "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] "[" [<hv 0> (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 ]
- ;
-
- level 8:
- evalconstr [ << (EVAL $c $r) >> ] ->
- [ [<hv 0> "Eval" [1 1] $r [1 0] "in" [1 1] $c:E ] ].
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 05:41:43 +0000