Commit f54345a2 authored by charguer's avatar charguer

bugfix_constructors

parent 0229d4fa
......@@ -17,6 +17,10 @@
# ML := TestDepend_AuxCode.ml TestDepend_MainCode.ml
# For tests, use:
#ML := Test.ml
#V := $(PWD)/Test_ml.v $(PWD)/Test_proof.v
# To exclude some files:
# V := $(filter-out $(PWD)/Demo_proof.v $(PWD)/Demo_ml.v $(PWD)/Test_proof.v $(PWD)/Test_ml.v, $(wildcard $(PWD)/*.v))
......
type 'a t = A of 'a
type 'a mylist = 'a t list
let empty : 'a mylist = []
\ No newline at end of file
......@@ -233,27 +233,49 @@ let typ_arity_constr c =
(** Translate a Caml data constructor into a Coq expression *)
let coq_of_constructor loc p c ty =
let typs =
match btyp_of_typ_exp ty with
| Btyp_constr (id,ts) -> List.map (lift_btyp loc) ts
| _ -> failwith "coq_of_constructor: constructor has a type that is not a type constructor"
in
(* DEPRECATED: attempt to type the constructor is problematic,
because the type [ty] might not have a type constructor
that is the one from the definition of the constructor. E.g.
type 'a t = A of 'a
type 'a mylist = 'a t list
let empty : 'a mylist = [] ---> this is not 'a list.
let coq_of_constructor_DEPRECATED loc p c ty =
let typs =
match btyp_of_typ_exp ty with
| Btyp_constr (id,ts) -> List.map (lift_btyp loc) ts
| _ -> failwith "coq_of_constructor: constructor has a type that is not a type constructor"
in
let x = string_of_path p in
(* TODO: fixme, this can be hacked by rebinding None, Some, or :: ..*)
let coq_name, arity =
match find_builtin_constructor x with
| None -> lift_path_name p, (typ_arity_constr c)
| Some (coq_name,arity) -> coq_name, arity
in
if typs = []
then coq_var coq_name
else coq_apps (coq_var_at coq_name) typs
(* DEPRECATED: coq_app_var_wilds coq_name arity *)
| Tpat_construct (path, c, ps) ->
coq_apps (coq_of_constructor loc path c p.pat_type) (List.map aux ps)
| Texp_construct (p, c, es) ->
coq_apps (coq_of_constructor loc p c e.exp_type) (List.map aux es)
*)
let coq_of_constructor loc p c args ty =
let x = string_of_path p in
(* TODO: fixme, this can be hacked by rebinding None, Some, or :: ..*)
let coq_name, arity =
let coq_name, _arity =
match find_builtin_constructor x with
| None -> lift_path_name p, (typ_arity_constr c)
| Some (coq_name,arity) -> coq_name, arity
in
if typs = []
then coq_var coq_name
else coq_apps (coq_var_at coq_name) typs
(* DEPRECATED: coq_app_var_wilds coq_name arity *)
(* TODO: we might have some issue if type abbreviation
('a,'b) t = ('b,'a) tconstr
is used and not unfolded *)
let constr = coq_var coq_name in
let typ = lift_typ_exp loc ty in
coq_annot (coq_apps constr args) typ
(*#########################################################################*)
(* ** Lifting of patterns *)
......@@ -290,7 +312,7 @@ let rec lift_pat ?(through_aliases=true) p : coq =
| Tpat_tuple l ->
Coq_tuple (List.map aux l)
| Tpat_construct (path, c, ps) ->
coq_apps (coq_of_constructor loc path c p.pat_type) (List.map aux ps)
coq_of_constructor loc path c (List.map aux ps) p.pat_type
| Tpat_alias (p, ak) ->
begin match ak with
| TPat_alias id ->
......@@ -494,7 +516,7 @@ let rec lift_val env e =
| Texp_tuple el ->
Coq_tuple (List.map aux el)
| Texp_construct (p, c, es) ->
coq_apps (coq_of_constructor loc p c e.exp_type) (List.map aux es)
coq_of_constructor loc p c (List.map aux es) e.exp_type
| Texp_record (l, opt_init_expr) ->
if opt_init_expr <> None then unsupported loc "record-with expression"; (* todo *)
if List.length l < 1 then failwith "record should have at least one field";
......
......@@ -12,6 +12,13 @@ open Print_type
type-checker*)
(** For extra verbosity on types, turn this flag on *)
(* TODO : extend this to all constructs of the language;
currently it is only used for constructors. *)
let print_tast_with_all_types = ref true
(*#########################################################################*)
(* ** Printing of items *)
......@@ -82,6 +89,11 @@ let string_of_let_pattern par fvs p =
(* ** Printing of expression *)
let rec string_of_expression par e =
let show_par_and_type par s =
if not !print_tast_with_all_types
then show_par par s
else sprintf "(%s : %s)" s (string_of_type_exp e.exp_type)
in
let aux ?par e =
string_of_expression (bool_of_option par) e in
let aux_pat ?par e =
......@@ -133,13 +145,13 @@ let rec string_of_expression par e =
| Texp_tuple l ->
show_par true (show_list aux ", " l)
| Texp_construct (p, cd, es) ->
let c = string_of_path p in
if es = []
then c
else if List.length es = 1
then show_par par (c ^ " " ^ aux ~par:true (List.hd es))
else
show_par par (sprintf "%s (%s)" c (show_list aux "," es))
let c = string_of_path p in
if es = [] then
show_par_and_type false c
else if List.length es = 1 then
show_par_and_type par (c ^ " " ^ aux ~par:true (List.hd es))
else
show_par_and_type par (sprintf "%s (%s)" c (show_list aux "," es))
| Texp_variant (l,eo) -> unsupported_noloc "variants"
| Texp_record (l,Some eo) -> unsupported_noloc "record-with"
| Texp_record (l,None) ->
......
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