Commit 20a009a2 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Coq output

parent 6c465ecb
......@@ -4,4 +4,7 @@
tmp.dk
_build/
*.native
*.glob
*.vo
test.dk
test.v
......@@ -3,9 +3,13 @@ DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
.PHONY: clean depend
.SUFFIXES: .dk .dko .ml .native
.SUFFIXES: .dk .dko .ml .native .v .vo
.dk.dko:
dkcheck -e -nc -r $<
dkcheck -e -nc $<
.v.vo:
coqc $<
.ml.native:
ocamlbuild -use-menhir $@
......@@ -20,9 +24,13 @@ clean:
rm -rf *.dko .depend tmp.dk test.dk sigmaid.native _build
test.dk: sigmaid.native
./sigmaid.native test.sigma > test.dk
./sigmaid.native test.sigma
test.v: sigmaid.native
./sigmaid.native test.sigma
test: test.dk dk_obj_examples.dko
dkcheck -nc -r test.dk
test: test.dk dk_obj_examples.dko test.v coq_obj.vo
dkcheck -nc -r test.dk
coqc -I . test.v
-include .depend
This diff is collapsed.
open Parsetree
open Scoper
open Typer
let print_id out_fmter (Id i) = Format.fprintf out_fmter "%s" i
let print_cid out_fmter (Cid c) = Format.fprintf out_fmter "%s" c
let print_label out_fmter (Label l) = Format.fprintf out_fmter "\"%s\"" l
let rec print_ty out_fmter = function
| Stcid (c, _) -> print_cid out_fmter c
| Stlist [] -> Format.fprintf out_fmter "Empty_type"
| Stlist ll ->
Format.fprintf out_fmter "[@[<hov>%a@]]"
print_ty_elems ll
| Starr (ty1, ty2) ->
Format.fprintf out_fmter "@[<hov>%a@ →@ %a@]"
print_par_ty ty1
print_par_ty ty2
| Stbool ty ->
Format.fprintf out_fmter "@[<hov>Bool@ %a@]"
print_par_ty ty
and print_ty_elem out_fmter (l, ty) =
Format.fprintf out_fmter "@[<hov>%a :@ %a@]"
print_label l
print_ty ty
and print_ty_elems out_fmter = function
| [] -> ()
| [ el ] -> print_ty_elem out_fmter el
| el :: els ->
Format.fprintf out_fmter "%a;@ %a"
print_ty_elem el
print_ty_elems els
and print_par_ty out_fmter = function
| Stcid _ | Stlist _ as ty -> print_ty out_fmter ty
| ty ->
Format.fprintf out_fmter "(%a)"
print_ty ty
let rec print_term out_fmter : tterm -> unit = function
| Tvar (id, _)
| Tconst (id, _, _) -> print_id out_fmter id
| Tpar t ->
Format.fprintf out_fmter "(%a)"
print_term t
| Tapp (t1, t2, _, _) ->
Format.fprintf out_fmter "@[<hov>%a@ @@@ %a@]"
print_par_term t1
print_par_term t2
| Tabst (x, ty, body, _) ->
Format.fprintf out_fmter "@[<hov>λ(%a !:@ %a) %a@]"
print_id x
print_ty ty
print_par_term body
| Ttrue ty ->
Format.fprintf out_fmter "@[<hov>true@ %a@]"
print_par_ty ty
| Tfalse ty ->
Format.fprintf out_fmter "@[<hov>false@ %a@]"
print_par_ty ty
| Tif (b, t, e, _) ->
Format.fprintf out_fmter "@[<hov>IF@ %a@ THEN@ %a@ ELSE@ %a@]"
print_term b
print_term t
print_par_term e
| Tobj (ll, _) ->
Format.fprintf out_fmter "[@[<hov>%a@]]"
print_obj_elems ll
| Tsel (t, l, _) ->
Format.fprintf out_fmter "@[<hov>%a#%a@]"
print_par_term t
print_label l
| Tupd (t, l, m, _) ->
Format.fprintf out_fmter "@[<hov>%a##%a@ ⇐ %a@]"
print_par_term t
print_label l
print_meth m
| Tcast (t, ty1, ty2) ->
Format.fprintf out_fmter "@[<hov>coerce@ %a@ %a@ tt@ %a@]"
print_par_ty ty1
print_par_ty ty2
print_par_term t
and print_par_term out_fmter = function
| Tvar _ | Tconst _ | Tpar _ | Tobj _ as t -> print_term out_fmter t
| t ->
Format.fprintf out_fmter "(%a)"
print_term t
and print_obj_elem out_fmter (l, m) =
Format.fprintf out_fmter "@[<hov>%a =@ %a@]"
print_label l
print_meth m
and print_obj_elems out_fmter = function
| [] -> ()
| [el] -> print_obj_elem out_fmter el
| el :: els ->
Format.fprintf out_fmter "%a;@ %a"
print_obj_elem el
print_obj_elems els
and print_meth out_fmter (Tmeth (x, ty, body, _)) =
Format.fprintf out_fmter "@[<h>ς(%a !: %a)%a@]"
print_id x
print_ty ty
print_par_term body
let print_line out_fmter = function
| Ttypedef (cid, ty) ->
Format.fprintf out_fmter "@[<h>Definition %a :=@ %a%%ty.@]@\n"
print_cid cid
print_par_ty ty
| Tvardef (id, ty, def) ->
Format.fprintf out_fmter "@[<h>Definition %a :@ Obj %a :=@ %a%%obj.@]@\n"
print_id id
print_par_ty ty
print_par_term def
| Tcheck (t, ty) ->
Format.fprintf out_fmter "@[<h>Goal Obj %a@].
Proof.
exact %a%%obj.
Qed."
print_par_ty ty
print_par_term t
| Tconv (t1, t2, _) ->
Format.fprintf out_fmter "@[<h>Goal %a%%obj =@ %a%%obj@].
Proof.
reflexivity.
Qed.
@\n"
print_par_term t1
print_par_term t2
| Tnorm t ->
Format.fprintf out_fmter "@[<h>Eval Compute %a%%obj.@]@\n"
print_par_term t
| Tprint s ->
Format.fprintf out_fmter "(* \"%s\" *)@\n" s
let print out_fmter = List.iter (print_line out_fmter)
......@@ -21,8 +21,16 @@ let main () =
Arg.parse [] (fun file ->
Base.labels := [];
let input = open_in file in
let basefile = Filename.chop_extension file in
let dk_out =
Format.formatter_of_out_channel
(open_out (basefile ^ ".dk"))
in
let coq_out =
Format.formatter_of_out_channel
(open_out (basefile ^ ".v"))
in
let lexbuf = Lexing.from_channel input in
let out_fmter = Format.std_formatter in
let prog = lex_prog lexbuf in
let scoped_prog =
try Scoper.scope prog
......@@ -40,10 +48,16 @@ expected an arrow type, found %s.@."
(Scoper.string_of_sty ty);
exit 1
in
Format.fprintf out_fmter "#NAME %s.@\n" (Filename.chop_extension file);
Printer.declare_labels out_fmter !Base.labels;
Printer.print out_fmter typed_prog;
Format.fprintf out_fmter "@.")
(* Dedukti output *)
Format.fprintf dk_out "#NAME %s.@\n" (Filename.chop_extension file);
Printer.declare_labels dk_out !Base.labels;
Printer.print dk_out typed_prog;
Format.fprintf dk_out "@.";
(* Coq output *)
Format.fprintf coq_out "Require Import coq_obj.@\n";
Coq_printer.print coq_out typed_prog;
Format.fprintf coq_out "@."
)
"Please provide a file name."
let _ = main ()
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment