Commit 664f35a2 authored by charguer's avatar charguer

demo_compiles

parent 70dacda8
......@@ -374,7 +374,10 @@ type ('a,'b) algb_erase =
type recorda = { recorda1 : int; recorda2 : int }
type ('a,'b) recordb = { recorda1 : 'a ; recorda2 : 'b -> 'b }
type ('a,'b) recordb = { recordb1 : 'a ; recordb2 : 'b -> 'b }
(* not supported: record overloading of fields
-- else would need to prefix all fields with the type... *)
(********************************************************************)
......@@ -383,8 +386,12 @@ type ('a,'b) recordb = { recorda1 : 'a ; recorda2 : 'b -> 'b }
type typereca1 = | Typereca_1 of typereca2
and typereca2 = | Typereca_2 of typereca1
(* not supported: recursive definition of inductive and record
-- technically could be supported, if the record was encoded
on the fly into a coq mutual inductive
type typerecb1 = | Typerecb_1 of typerecb2
and typerecb2 = { typerecb_2 : typerecb1 }
*)
(* not supported: recursive definitions using abbreviation
......
......@@ -51,7 +51,7 @@ ifdef V_IGNORED
endif
ifndef COQINCLUDE
COQINCLUDE := -R $(CFML)/lib/coq CFML -R $(CFML)/lib/tlc TLC -R . EXAMPLE
COQINCLUDE := -R $(CFML)/lib/coq CFML -R $(CFML)/lib/tlc TLC -R $(CFML)/lib/stdlib/ STDLIB -R . EXAMPLE
endif
OCAMLBUILD := \
......@@ -95,6 +95,7 @@ cf: $(ML)
# Needed only when developing TLC and CFML. Ideally, should be removed.
@$(MAKE) -C $(CFML)/lib/tlc --no-print-directory quick
@$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick_cf
@$(MAKE) -C $(CFML)/lib/stdlib --no-print-directory quick
@$(MAKE) CFML=$(CFML) OCAML_FLAGS=$(OCAML_FLAGS) COQINCLUDE="$(COQINCLUDE)" ML="$(ML)" --no-print-directory -f $(CFML)/lib/make/Makefile.cf all
proof:cf
......
......@@ -136,7 +136,7 @@ let rec lift_btyp t =
| Btyp_constr (id,[t]) when Path.name id = "Stream.stream_cell" || Path.name id = "stream_cell" ->
Coq_app (Coq_var "list", aux t)
| Btyp_constr (id,ts) ->
coq_apps (Coq_var (lift_path_name id)) (List.map aux ts)
coq_apps (Coq_var (type_constr_name (lift_path_name id))) (List.map aux ts)
| Btyp_tuple ts ->
coq_prod (List.map aux ts)
| Btyp_var (b,s) ->
......@@ -1128,18 +1128,18 @@ and cfg_algebraic decls =
let x = Ident.name name in
let branches = match dec.typ_type.type_kind with Type_variant l -> l | _ -> assert false in
let params = List.map name_of_type dec.typ_type.type_params in
let ret_typ = coq_apps (Coq_var x) (coq_vars params) in
let ret_typ = coq_apps (Coq_var (type_constr_name x)) (coq_vars params) in
let get_typed_constructor (c,ts) =
(c, coq_impls (List.map lift_typ_exp ts) ret_typ) in
let coqind_decl =
if List.length decls = 1 then
{ coqind_name = x;
{ coqind_name = type_constr_name x;
coqind_constructor_name = record_constructor_name x;
coqind_targs = coq_types params;
coqind_ret = Coq_type;
coqind_branches = List.map get_typed_constructor branches; }
else
{ coqind_name = x;
{ coqind_name = type_constr_name x;
coqind_constructor_name = record_constructor_name x;
coqind_targs = [];
coqind_ret = coq_impl_types (List.length params);
......
......@@ -53,7 +53,9 @@ let module_name name =
(** Convention for naming type constructors *)
let type_constr_name name =
name ^ "_"
if List.mem name [ "int"; "unit"; "bool"; "float"; "list"; "string" ]
then name
else name ^ "_"
(** Convention for naming record types,
i.e. the one that is bound to "loc" *)
......
......@@ -58,7 +58,7 @@ ifndef ML
endif
ifndef COQINCLUDE
COQINCLUDE := -R $(CFML)/lib/coq/ CFML -R $(CFML)/lib/tlc/ TLC -R . EXAMPLE
COQINCLUDE := -R $(CFML)/lib/coq/ CFML -R $(CFML)/lib/tlc/ TLC -R $(CFML)/lib/stdlib/ STDLIB -R . EXAMPLE
endif
-include $(CFML)/settings.sh
......@@ -129,7 +129,7 @@ endif
# Only the %.cmj target is known to "make".
%.cmj: %.ml $(CFML_MLV)
$(CFML_MLV) $(OCAML_FLAGS) -I $(CFML)/lib/ocaml -I . $<
$(CFML_MLV) $(OCAML_FLAGS) -nostdlib -I $(CFML)/lib/stdlib -I . $<
# We use Coq to produce a .vio file out of a .v file.
......
......@@ -23,7 +23,7 @@ ifeq ($(findstring $(MAKECMDGOALS),clean),)
endif
ifndef COQINCLUDE
COQINCLUDE := -R $(CFML)/lib/coq/ CFML -R $(CFML)/lib/tlc/ TLC -R . EXAMPLE
COQINCLUDE := -R $(CFML)/lib/coq/ CFML -R $(CFML)/lib/tlc/ TLC -R . STDLIB
endif
ifndef OCAML_FLAGS
......
......@@ -6,6 +6,8 @@
external raise : exn -> 'a = "%raise"
external failwith : string -> 'a = "%failwith"
(************************************************************)
(** Type conversion *)
......
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