diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/Makefile | 53 | ||||
| -rw-r--r-- | dev/docintro | 50 | ||||
| -rw-r--r-- | dev/html/style.css | 220 | ||||
| -rw-r--r-- | dev/ocamlweb-doc/Makefile | 90 | ||||
| -rw-r--r-- | dev/ocamlweb-doc/ast.ml | 47 | ||||
| -rw-r--r-- | dev/ocamlweb-doc/intro.tex | 25 | ||||
| -rw-r--r-- | dev/ocamlweb-doc/lex.mll | 81 | ||||
| -rw-r--r-- | dev/ocamlweb-doc/macros.tex | 7 | ||||
| -rw-r--r-- | dev/ocamlweb-doc/parse.ml | 183 | ||||
| -rw-r--r-- | dev/ocamlweb-doc/preamble.tex | 8 | ||||
| -rw-r--r-- | dev/ocamlweb-doc/syntax.mly | 224 |
11 files changed, 323 insertions, 665 deletions
diff --git a/dev/Makefile b/dev/Makefile new file mode 100644 index 0000000000..4693bd136c --- /dev/null +++ b/dev/Makefile @@ -0,0 +1,53 @@ +include ../config/Makefile + +LOCALINCLUDES=-I ../config -I ../tools -I ../tools/coqdoc \ + -I ../scripts -I ../lib -I ../kernel -I ../kernel/byterun -I ../library \ + -I ../proofs -I ../tactics -I ../pretyping \ + -I ../interp -I ../toplevel -I ../parsing -I ../ide/utils -I ../ide \ + -I ../plugins/omega -I ../plugins/romega \ + -I ../plugins/ring -I ../plugins/dp -I ../plugins/setoid_ring \ + -I ../plugins/xml -I ../plugins/extraction \ + -I ../plugins/fourier -I ../plugins/cc \ + -I ../plugins/funind -I ../plugins/firstorder \ + -I ../plugins/field -I ../plugins/subtac -I ../plugins/rtauto \ + -I ../plugins/recdef + +MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) + +MLIS=$(wildcard ../lib/*.mli ../kernel/*.mli ../library/*.mli \ + ../pretyping/*.mli ../interp/*.mli \ + ../parsing/*.mli ../proofs/*.mli \ + ../tactics/*.mli ../toplevel/*.mli) + +all:: html coq.pdf + +newsyntax.dvi: newsyntax.tex + latex $< + latex $< + +coq.dvi: coq.tex + latex coq + latex coq + +coq.tex:: + ocamldoc -latex -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\ + $(MLIS) -t "Coq mlis documentation" -intro docintro -o coq.tex + +html:: + ocamldoc -html -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\ + $(MLIS) -d html -colorize-code \ + -t "Coq mlis documentation" -intro docintro -css-style style.css + +%.dot: ../% + ocamldoc -rectypes $(MLINCLUDES) -t $* -dot -dot-reduce ../$*/*.ml ../$*/*.mli -o $@ + +%.png: %.dot + dot -Tpng $< -o $@ + +clean:: + rm -f *~ *.log *.aux + +.SUFFIXES: .tex .png + +%.pdf: %.tex + pdflatex $< && pdflatex $<
\ No newline at end of file diff --git a/dev/docintro b/dev/docintro new file mode 100644 index 0000000000..3d37d5374d --- /dev/null +++ b/dev/docintro @@ -0,0 +1,50 @@ +{!indexlist} + +This is Coq, a proof assistant for the Calculus of Inductive Construction. +This document describes the implementation of Coq. +It has been automatically generated from the source of +Coq using ocamldoc, a literate programming tool for +Objective Caml freely available at http://caml.inria.fr/. +The source files are organized in several directories ordered like that: + +{ol {- Utility libraries : lib + +describes the various utility libraries used in the code +of Coq.} +{- Kernel : kernel + +describes the \Coq\ kernel, which is a type checker for the Calculus +of Inductive Construction.} +{- Library : library + +describes the Coq library, which is made of two parts: +- a general mechanism to keep a trace of all operations and of + the state of the system, with backtrack capabilities; +- a global environment for the CCI, with functions to export and + import compiled modules. + +} +{- Pretyping : pretyping + +} +{- Front abstract syntax of terms : interp + +describes the translation from Coq context-dependent +front abstract syntax of terms {v front v} to and from the +context-free, untyped, raw form of constructions {v rawconstr v}.} +{- Parsers and printers : parsing + +describes the implementation of the \Coq\ parsers and printers.} +{- Proof engine : proofs + +describes the Coq proof engine, which is also called +the ``refiner'', since it provides a way to build terms by successive +refining steps. Those steps are either primitive rules or higher-level +tactics.} +{- Tacticts : tactics + +describes the Coq main tactics.} +{- Toplevel : toplevel + +describes the highest modules of the Coq system.} +} diff --git a/dev/html/style.css b/dev/html/style.css new file mode 100644 index 0000000000..b8f02a15fb --- /dev/null +++ b/dev/html/style.css @@ -0,0 +1,220 @@ +a:visited {
+ color: #416DFF; text-decoration: none;
+}
+
+a:link {
+ color: #416DFF; text-decoration: none;
+}
+
+a:hover {
+ color: Red; text-decoration: none; background-color: #5FFF88
+}
+
+a:active {
+ color: Red; text-decoration: underline;
+}
+
+.keyword {
+ font-weight: bold; color: Red
+}
+
+.keywordsign {
+ color: #C04600
+}
+
+.superscript {
+ font-size: 4
+}
+
+.subscript {
+ font-size: 4
+}
+
+.comment {
+ color: Green
+}
+
+.constructor {
+ color: Blue
+}
+
+.type {
+ color: #5C6585
+}
+
+.string {
+ color: Maroon
+}
+
+.warning {
+ color: Red; font-weight: bold
+}
+
+.info {
+ margin-left: 3em; margin-right: 3em
+}
+
+.param_info {
+ margin-top: 4px; margin-left: 3em; margin-right: 3em
+}
+
+.code {
+ color: #465F91;
+}
+
+h1 {
+ font-size: 20pt; text-align: center;
+}
+
+h5, h6, div.h7, div.h8, div.h9 {
+ font-size: 20pt;
+ border: 1px solid #000000;
+ margin-top: 5px;
+ margin-bottom: 2px;
+ text-align: center;
+ padding: 2px;
+}
+
+h5 {
+ background-color: #90FDFF;
+}
+
+h6 {
+ background-color: #016699;
+ color: white;
+}
+
+div.h7 {
+ background-color: #E0FFFF;
+}
+
+div.h8 {
+ background-color: #F0FFFF;
+}
+
+div.h9 {
+ background-color: #FFFFFF;
+}
+
+.typetable, .indextable, .paramstable {
+ border-style: hidden;
+}
+
+.paramstable {
+ padding: 5pt 5pt;
+}
+
+body {
+ background-color: white;
+}
+
+tr {
+ background-color: white;
+}
+
+td.typefieldcomment {
+ background-color: #FFFFFF;
+ font-size: smaller;
+}
+
+pre {
+ margin-bottom: 4px;
+}
+
+div.sig_block {
+ margin-left: 2em;
+}
+
+
+h2 {
+ font-family: Arial, Helvetica, sans-serif;
+ font-size: 16pt;
+ font-weight: normal;
+ border-bottom: 1px solid #dadada;
+ border-top: 1px solid #dadada;
+ color: #101010;
+ background: #eeeeff;
+ margin: 25px 0px 10px 0px;
+ padding: 1px 1px 1px 1px;
+}
+
+h3 {
+ font-family: Arial, Helvetica, sans-serif;
+ font-size: 12pt;
+ color: #016699;
+ font-weight: bold;
+ padding: 15px 0 0 0ex;
+ margin: 5px 0 0 0;
+}
+
+h4 {
+ font-family: Arial, Helvetica, sans-serif;
+ font-size: 10pt;
+ color: #016699;
+ padding: 15px 0 0 0ex;
+ margin: 5px 0 0 0;
+}
+
+/* Here starts the overwrite of default rules to give a better look */
+
+body {
+ font-family: Calibri, Georgia, Garamond, Baskerville, serif;
+ font-size: 12pt;
+ background-color: white;
+}
+
+a:link, a {
+ color: #6895c3 !important;
+}
+
+a:hover {
+ color: #2F4459 !important;
+ background-color: white;
+}
+
+hr {
+ height: 1px;
+ color: #016699;
+ background-color: #016699;
+ border-width: 0;
+}
+
+h1, h1 a:link, h1 a:visited, h1 a {
+ font-family: Cambria, Georgia, Garamond, Baskerville, serif;
+ color: #016699;
+}
+
+.navbar {
+ float: left;
+}
+
+.navbar a, .navbar a:link, .navbar a:visited {
+ color: #016699;
+ font-family: Arial, Helvetica, sans-serif;
+ font-weight: bold;
+ font-size: 80%;
+}
+
+.keyword {
+ color: #c13939;
+}
+
+.constructor {
+ color: #3c8f7e;
+}
+
+pre, code {
+ font-family: "DejaVu Sans Mono", "Bitstream Vera Mono", "Courrier New", monospace;
+ white-space: normal;
+ font-size: 9pt;
+ font-weight: bold;
+}
+
+.type br {
+ display: none;
+}
+
+.info {
+ margin-left: 1em;
+ font-size: 12pt;
+}
diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile deleted file mode 100644 index 3189d7c518..0000000000 --- a/dev/ocamlweb-doc/Makefile +++ /dev/null @@ -1,90 +0,0 @@ -include ../../config/Makefile - -LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \ - -I ../../scripts -I ../../lib -I ../../kernel -I ../../kernel/byterun -I ../../library \ - -I ../../proofs -I ../../tactics -I ../../pretyping \ - -I ../../interp -I ../../toplevel -I ../../parsing -I ../../ide/utils -I ../../ide \ - -I ../../plugins/omega -I ../../plugins/romega \ - -I ../../plugins/ring -I ../../plugins/dp -I ../../plugins/setoid_ring \ - -I ../../plugins/xml -I ../../plugins/extraction \ - -I ../../plugins/fourier \ - -I ../../plugins/cc \ - -I ../../plugins/funind -I ../../plugins/firstorder \ - -I ../../plugins/field -I ../../plugins/subtac -I ../../plugins/rtauto \ - -I ../../plugins/recdef - -MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) - - -all:: newparse coq.ps minicop.ps -#newsyntax.dvi minicoq.dvi - - -OBJS=lex.cmo ast.cmo parse.cmo syntax.cmo - -newparse: $(OBJS) syntax.mli lex.ml syntax.ml - ocamlc -o newparse $(OBJS) - -%.cmo: %.ml - ocamlc -c $< - -%.cmi: %.mli - ocamlc -c $< - -%.ml: %.mll - ocamllex $< - -%.ml: %.mly - ocamlyacc -v $< - -%.mli: %.mly - ocamlyacc -v $< - -clean:: - rm -f *.cm* *.output syntax.ml syntax.mli lex.ml newparse - -parse.cmo: ast.cmo -syntax.cmi: parse.cmo -syntax.cmo: lex.cmo parse.cmo syntax.cmi -lex.cmo: syntax.cmi -ast.cmo: ast.ml - -newsyntax.dvi: newsyntax.tex - latex $< - latex $< - -coq.dvi: coq.tex - latex coq - latex coq - -coq.tex:: - ocamlweb -p "\usepackage{epsfig}" \ - macros.tex intro.tex \ - ../../lib/{doc.tex,*.mli} ../../kernel/{doc.tex,*.mli} ../../library/{doc.tex,*.mli} \ - ../../pretyping/{doc.tex,*.mli} ../../interp/{doc.tex,*.mli} \ - ../../parsing/{doc.tex,*.mli} ../../proofs/{doc.tex,*.mli} \ - ../../tactics/{doc.tex,*.mli} ../../toplevel/{doc.tex,*.mli} \ - -o coq.tex - - -depend:: kernel.dep.ps library.dep.ps pretyping.dep.ps parsing.dep.ps \ - proofs.dep.ps tactics.dep.ps toplevel.dep.ps interp.dep.ps - -%.dot: ../../% - ocamldoc -rectypes $(MLINCLUDES) -t $* -dot -dot-reduce ../../$*/*.ml ../../$*/*.mli -o $@ - -%.dep.ps: %.dot - dot -Tps $< -o $@ - -clean:: - rm -f *~ *.log *.aux - -.SUFFIXES: .tex .dvi .ps .cmo .cmi .mli .ml .mll .mly - -%.dvi: %.tex - latex $< && latex $< - -%.ps: %.dvi - dvips $< -o $@ - - diff --git a/dev/ocamlweb-doc/ast.ml b/dev/ocamlweb-doc/ast.ml deleted file mode 100644 index 4eb135d83c..0000000000 --- a/dev/ocamlweb-doc/ast.ml +++ /dev/null @@ -1,47 +0,0 @@ - -type constr_ast = - Pair of constr_ast * constr_ast -| Prod of binder list * constr_ast -| Lambda of binder list * constr_ast -| Let of string * constr_ast * constr_ast -| LetCase of binder list * constr_ast * constr_ast -| IfCase of constr_ast * constr_ast * constr_ast -| Eval of red_fun * constr_ast -| Infix of string * constr_ast * constr_ast -| Prefix of string * constr_ast -| Postfix of string * constr_ast -| Appl of constr_ast * constr_arg list -| ApplExpl of string list * constr_ast list -| Scope of string * constr_ast -| Qualid of string list -| Prop | Set | Type -| Int of string -| Hole -| Meta of string -| Fixp of fix_kind * - (string * binder list * constr_ast * string option * constr_ast) list * - string -| Match of case_item list * constr_ast option * - (pattern list * constr_ast) list - -and red_fun = Simpl - -and binder = string * constr_ast - -and constr_arg = string option * constr_ast - -and fix_kind = Fix | CoFix - -and case_item = constr_ast * (string option * constr_ast option) - -and pattern = - PatAs of pattern * string -| PatType of pattern * constr_ast -| PatConstr of string * pattern list -| PatVar of string - -let mk_cast c t = - if t=Hole then c else Infix(":",c,t) - -let mk_lambda bl t = - if bl=[] then t else Lambda(bl,t) diff --git a/dev/ocamlweb-doc/intro.tex b/dev/ocamlweb-doc/intro.tex deleted file mode 100644 index 4cec8673f4..0000000000 --- a/dev/ocamlweb-doc/intro.tex +++ /dev/null @@ -1,25 +0,0 @@ - -\ocwsection This is \Coq, a proof assistant for the \CCI. -This document describes the implementation of \Coq. -It has been automatically generated from the source of -\Coq\ using \textsf{ocamlweb}, a literate programming tool for -\textsf{Objective Caml}\footnote{\Coq, \textsf{Objective Caml} and - \textsf{ocamlweb} are all freely available at - \textsf{http://coq.inria.fr/}, \textsf{http://caml.inria.fr/} and - \textsf{http://www.lri.fr/\~{}filliatr/ocamlweb}.}. -The source files are organized in several directories, which are -described here as separate chapters. - -\begin{center} - \begin{tabular}{p{10cm}rr} - Chapter & section & page \\[0.5em] - \hline\\[0.2em] - Utility libraries \dotfill & \refsec{lib} & \pageref{lib} \\[0.5em] - Kernel \dotfill & \refsec{kernel} & \pageref{kernel} \\[0.5em] - Library \dotfill & \refsec{library} & \pageref{library} \\[0.5em] - Pretyping \dotfill & \refsec{pretyping} & \pageref{pretyping} \\[0.5em] - Proof engine \dotfill & \refsec{proofs} & \pageref{proofs} \\[0.5em] - Tactics \dotfill & \refsec{tactics} & \pageref{tactics} \\[0.5em] - Toplevel \dotfill & \refsec{toplevel}& \pageref{toplevel}\\[0.5em] - \end{tabular} -\end{center}
\ No newline at end of file diff --git a/dev/ocamlweb-doc/lex.mll b/dev/ocamlweb-doc/lex.mll deleted file mode 100644 index 059526d9bf..0000000000 --- a/dev/ocamlweb-doc/lex.mll +++ /dev/null @@ -1,81 +0,0 @@ - -{ - open Lexing - open Syntax - - let chan_out = ref stdout - - let comment_depth = ref 0 - let print s = output_string !chan_out s - - exception Fin_fichier - -} - -let space = [' ' '\t' '\n'] -let letter = ['a'-'z' 'A'-'Z'] -let digit = ['0'-'9'] - -let identifier = letter (letter | digit | ['_' '\''])* -let number = digit+ -let oper = ['-' '+' '/' '*' '|' '>' '<' '=' '%' '#' '$' ':' '\\' '?' - '.' '!' '@' ]+ - -rule token = parse - | "let" {LET} - | "in" {IN} - | "match" {MATCH} - | "with" {WITH} - | "end" {END} - | "and" {AND} - | "fun" {FUN} - | "if" {IF} - | "then" {THEN} - | "else" {ELSE} - | "eval" {EVAL} - | "for" {FOR} - | "Prop" {PROP} - | "Set" {SET} - | "Type" {TYPE} - | "fix" {FIX} - | "cofix" {COFIX} - | "struct" {STRUCT} - | "as" {AS} - - | "Simpl" {SIMPL} - - | "_" {WILDCARD} - | "(" {LPAR} - | ")" {RPAR} - | "{" {LBRACE} - | "}" {RBRACE} - | "!" {BANG} - | "@" {AT} - | ":" {COLON} - | ":=" {COLONEQ} - | "." {DOT} - | "," {COMMA} - | "->" {OPER "->"} - | "=>" {RARROW} - | "|" {BAR} - | "%" {PERCENT} - - | '?' { META(ident lexbuf)} - | number { INT(Lexing.lexeme lexbuf) } - | oper { OPER(Lexing.lexeme lexbuf) } - | identifier { IDENT (Lexing.lexeme lexbuf) } - | "(*" (*"*)"*) { comment_depth := 1; - comment lexbuf; - token lexbuf } - | space+ { token lexbuf} - | eof { EOF } - -and ident = parse - | identifier { Lexing.lexeme lexbuf } - -and comment = parse - | "(*" (*"*)"*) { incr comment_depth; comment lexbuf } - | (*"(*"*) "*)" - { decr comment_depth; if !comment_depth > 0 then comment lexbuf } - | eof { raise Fin_fichier } - | _ { comment lexbuf } diff --git a/dev/ocamlweb-doc/macros.tex b/dev/ocamlweb-doc/macros.tex deleted file mode 100644 index 6beacf7b0b..0000000000 --- a/dev/ocamlweb-doc/macros.tex +++ /dev/null @@ -1,7 +0,0 @@ - -% macros for coq.tex - -\newcommand{\Coq}{\textsf{Coq}} -\newcommand{\CCI}{Calculus of Inductive Constructions} - -\newcommand{\refsec}[1]{\textbf{\ref{#1}}}
\ No newline at end of file diff --git a/dev/ocamlweb-doc/parse.ml b/dev/ocamlweb-doc/parse.ml deleted file mode 100644 index b145fffda6..0000000000 --- a/dev/ocamlweb-doc/parse.ml +++ /dev/null @@ -1,183 +0,0 @@ - -open Ast - -type assoc = L | R | N - -let level = function - | "--" -> 70,L - | "=" -> 70,N - | "+" -> 60,L - | "++" -> 60,R - | "+++" -> 60,R - | "-" -> 60,L - | "*" -> 50,L - | "/" -> 50,L - | "**" -> 40,R - | ":" -> (100,R) - | "->" -> (90,R) - | s -> failwith ("unknowm operator '"^s^"'") - -let fixity = function - | "--" -> [L] - | "=" -> [N] - | ("+"|"-"|"*"|"/") -> [L;N] - | "++" -> [R] - | _ -> [L;N;R] - -let ground_oper = function - ("-"|"+") -> true - | _ -> false - -let is_prefix op = List.mem L (fixity op) -let is_infix op = List.mem N (fixity op) -let is_postfix op = List.mem R (fixity op) - -let mk_inf op t1 t2 = - if not (is_infix op) then failwith (op^" not infix"); - Infix(op,t1,t2) - -let mk_post op t = - if not (is_postfix op) then failwith (op^" not postfix"); - Postfix(op,t) - - -(* Pb avec ground_oper: pas de diff entre -1 et -(1) *) -let mk_pre op t = - if not (is_prefix op) then failwith (op^" not prefix"); - if ground_oper op then - match t with - | Int i -> Int (op^i) - | _ -> Prefix(op,t) - else Prefix(op,t) - -(* teste si on peut reduire op suivi d'un op de niveau (n,a) - si la reponse est false, c'est que l'op (n,a) doit se reduire - avant *) -let red_left_op (nl,al) (nr,ar) = - if nl < nr then true - else - if nl = nr then - match al,ar with - | (L|N), L -> true - | R, (R|N) -> false - | R, L -> failwith "conflit d'assoc: ambigu" - | (L|N), (R|N) -> failwith "conflit d'assoc: blocage" - else false - - -type level = int * assoc -type stack = - | PrefixOper of string list - | Term of constr_ast * stack - | Oper of string list * string * constr_ast * stack - -let rec str_ast = function - | Infix(op,t1,t2) -> str_ast t1 ^ " " ^ op ^ " " ^ str_ast t2 - | Postfix(op,t) -> str_ast t ^ " " ^ op - | Prefix(op,t) -> op ^ " " ^ str_ast t - | _ -> "_" - -let rec str_stack = function - | PrefixOper ops -> String.concat " " (List.rev ops) - | Term (t,s) -> str_stack s ^ " (" ^ str_ast t ^ ")" - | Oper(ops,lop,t,s) -> - str_stack (Term(t,s)) ^ " " ^ lop ^ " " ^ - String.concat " " (List.rev ops) - -let pps s = prerr_endline (str_stack s) -let err s stk = failwith (s^": "^str_stack stk) - - -let empty = PrefixOper [] - -let check_fixity_term stk = - match stk with - Term _ -> err "2 termes successifs" stk - | _ -> () - -let shift_term t stk = - check_fixity_term stk; - Term(t,stk) - -let shift_oper op stk = - match stk with - | Oper(ops,lop,t,s) -> Oper(op::ops,lop,t,s) - | Term(t,s) -> Oper([],op,t,s) - | PrefixOper ops -> PrefixOper (op::ops) - -let is_reducible lv stk = - match stk with - | Oper([],iop,_,_) -> red_left_op (level iop) lv - | Oper(op::_,_,_,_) -> red_left_op (level op) lv - | PrefixOper(op::_) -> red_left_op (level op) lv - | _ -> false - -let reduce_head (t,stk) = - match stk with - | Oper([],iop,t1,s) -> - (Infix(iop,t1,t), s) - | Oper(op::ops,lop,t',s) -> - (mk_pre op t, Oper(ops,lop,t',s)) - | PrefixOper(op::ops) -> - (Prefix(op,t), PrefixOper ops) - | _ -> assert false - -let rec reduce_level lv (t,s) = - if is_reducible lv s then reduce_level lv (reduce_head (t, s)) - else (t, s) - -let reduce_post op (t,s) = - let (t',s') = reduce_level (level op) (t,s) in - (mk_post op t', s') - -let reduce_posts stk = - match stk with - Oper(ops,iop,t,s) -> - let pts1 = reduce_post iop (t,s) in - List.fold_right reduce_post ops pts1 - | Term(t,s) -> (t,s) - | PrefixOper _ -> failwith "reduce_posts" - - -let shift_infix op stk = - let (t,s) = reduce_level (level op) (reduce_posts stk) in - Oper([],op,t,s) - -let is_better_infix op stk = - match stk with - | Oper(ops,iop,t,s) -> - is_postfix iop && - List.for_all is_postfix ops && - (not (is_prefix op) || red_left_op (level iop) (level op)) - | Term _ -> false - | _ -> assert false - -let parse_oper op stk = - match stk with - | PrefixOper _ -> - if is_prefix op then shift_oper op stk else failwith "prefix_oper" - | Oper _ -> - if is_infix op then - if is_better_infix op stk then shift_infix op stk - else shift_oper op stk - else if is_prefix op then shift_oper op stk - else if is_postfix op then - let (t,s) = reduce_post op (reduce_posts stk) in - Term(t,s) - else assert false - | Term(t,s) -> - if is_infix op then shift_infix op stk - else if is_postfix op then - let (t2,s2) = reduce_post op (t,s) in Term(t2,s2) - else failwith "infix/postfix" - -let parse_term = shift_term - -let rec close_stack stk = - match stk with - Term(t,PrefixOper []) -> t - | PrefixOper _ -> failwith "expression sans atomes" - | _ -> - let (t,s) = reduce_head (reduce_posts stk) in - close_stack (Term(t,s)) - diff --git a/dev/ocamlweb-doc/preamble.tex b/dev/ocamlweb-doc/preamble.tex deleted file mode 100644 index 2cd21f0228..0000000000 --- a/dev/ocamlweb-doc/preamble.tex +++ /dev/null @@ -1,8 +0,0 @@ -\documentclass[11pt]{article} -\usepackage[latin1]{inputenc} -\usepackage[T1]{fontenc} -\usepackage{ocamlweb} -\pagestyle{ocamlweb} -\usepackage{fullpage} -\usepackage{epsfig} -\begin{document} diff --git a/dev/ocamlweb-doc/syntax.mly b/dev/ocamlweb-doc/syntax.mly deleted file mode 100644 index bfc7d5ccf0..0000000000 --- a/dev/ocamlweb-doc/syntax.mly +++ /dev/null @@ -1,224 +0,0 @@ -%{ -open Ast -open Parse -%} - -%token <string> META INT IDENT -%token <string> OPER -%token LPAR RPAR BAR COMMA COLON BANG FUN DOT RARROW LET COLONEQ IN IF -%token THEN ELSE EVAL AT FOR PROP SET TYPE WILDCARD FIX -%token COFIX MATCH WITH END AND LBRACE RBRACE STRUCT AS SIMPL PERCENT -%token EOF - -%start main -%type <Ast.constr_ast> main - -%start constr -%type <Ast.constr_ast> constr - -%start simple_constr -%type <Ast.constr_ast> simple_constr - -%% - -main: - constr EOF { $1 } -; - - -paren_constr: - constr COMMA paren_constr { Pair($1,$3) } - | constr { $1 } -; - -constr: - binder_constr { $1 } - | oper_constr { close_stack $1 } -; - -binder_constr: - BANG ne_binders DOT constr { Prod($2, $4) } - | FUN ne_binders type_cstr RARROW constr { Lambda($2,mk_cast $5 $3) } - | LET IDENT binders type_cstr COLONEQ constr IN constr - { Let($2,mk_lambda $3 (mk_cast $6 $4),$8) } - | LET LPAR comma_binders RPAR COLONEQ constr IN constr - { LetCase($3,$6,$8) } - | IF constr THEN constr ELSE constr { IfCase($2,$4,$6) } - | fix_constr { $1 } - | EVAL rfun IN constr { Eval($2,$4) } -; - -comma_binders: - ne_comma_binders { $1 } - | { [] } -; - -ne_comma_binders: - binder COMMA ne_comma_binders { $1 :: $3 } - | binder { [$1] } -; - -rfun: - SIMPL { Simpl } -; - - -/* 2 Conflits shift/reduce */ -oper_constr: - oper_constr oper appl_constr - { parse_term $3 (parse_oper $2 $1) } - | oper_constr oper binder_constr - { parse_term $3 (parse_oper $2 $1) } - | oper_constr oper { parse_oper $2 $1 } - | { empty } - | appl_constr { parse_term $1 empty } -; - -oper: - OPER {$1} - | COLON {":"} -; - -appl_constr: - simple_constr ne_appl_args { Appl($1,$2) } - | AT global simple_constrs { ApplExpl($2,$3) } - | simple_constr { $1 } -; - -appl_arg: - AT INT COLONEQ simple_constr { (Some $2,$4) } - | simple_constr { (None,$1) } -; - -ne_appl_args: - appl_arg { [$1] } - | appl_arg ne_appl_args { $1::$2 } -; - -simple_constr: - atomic_constr { $1 } - | match_constr { $1 } - | LPAR paren_constr RPAR { $2 } - | simple_constr PERCENT IDENT { Scope($3,$1) } -; - -simple_constrs: - simple_constr simple_constrs { $1::$2 } - | { [] } -; - -atomic_constr: - global { Qualid $1 } - | PROP { Prop } - | SET { Set } - | TYPE { Type } - | INT { Int $1 } - | WILDCARD { Hole } - | META { Meta $1 } -; - -global: - IDENT DOT global { $1 :: $3 } - | IDENT { [$1] } -; - -/* Conflit normal */ -fix_constr: - fix_kw fix_decl - { let (id,_,_,_,_ as fx) = $2 in Fixp($1,[fx],id) } - | fix_kw fix_decl fix_decls FOR IDENT { Fixp($1, $2::$3, $5) } -; - -fix_kw: FIX {Fix} | COFIX {CoFix} -; - -fix_decl: - IDENT binders type_cstr annot COLONEQ constr { ($1,$2,$3,$4,$6) } -; - -fix_decls: - AND fix_decl fix_decls { $2::$3 } - | AND fix_decl { [$2] } -; - -annot: - LBRACE STRUCT IDENT RBRACE { Some $3 } - | { None } -; - -match_constr: - MATCH case_items case_type WITH branches END { Match($2,$3,$5) } -; - -case_items: - case_item { [$1] } - | case_item COMMA case_items { $1::$3 } -; - -case_item: - constr pred_pattern { ($1,$2) } -; - -case_type: - RARROW constr { Some $2 } - | { None } -; - -pred_pattern: - AS IDENT COLON constr { (Some $2, Some $4) } - | AS IDENT { (Some $2, None) } - | COLON constr { (None, Some $2) } - | { (None,None) } -; - -branches: - BAR branch_list { $2 } - | branch_list { $1 } - | { [] } -; - -branch_list: - patterns RARROW constr { [$1, $3] } - | patterns RARROW constr BAR branch_list { ($1,$3)::$5 } -; - -patterns: - pattern { [$1] } - | pattern COMMA patterns { $1::$3 } -; - -pattern: - pattern AS IDENT { PatAs($1,$3) } - | pattern COLON constr { PatType($1,$3) } - | IDENT simple_patterns { PatConstr($1,$2) } - | simple_pattern { $1 } -; - -simple_pattern: - IDENT { PatVar $1 } - | LPAR pattern RPAR { $2 } -; - -simple_patterns: - simple_pattern { [$1] } - | simple_pattern simple_patterns { $1::$2 } -; - -binder: - IDENT { ($1,Hole) } - | LPAR IDENT type_cstr RPAR { ($2,$3) } -; - -binders: - ne_binders { $1 } - | { [] } - -ne_binders: - binder { [$1] } - | binder ne_binders { $1::$2 } -; - -type_cstr: - COLON constr { $2 } - | { Hole } -; |