aboutsummaryrefslogtreecommitdiff
path: root/dev/ocamlweb-doc
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ocamlweb-doc')
-rw-r--r--dev/ocamlweb-doc/Makefile90
-rw-r--r--dev/ocamlweb-doc/ast.ml47
-rw-r--r--dev/ocamlweb-doc/intro.tex25
-rw-r--r--dev/ocamlweb-doc/lex.mll81
-rw-r--r--dev/ocamlweb-doc/macros.tex7
-rw-r--r--dev/ocamlweb-doc/parse.ml183
-rw-r--r--dev/ocamlweb-doc/preamble.tex8
-rw-r--r--dev/ocamlweb-doc/syntax.mly224
8 files changed, 0 insertions, 665 deletions
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 }
-;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:25:39 +0000