Commit 661c16eb authored by charguer's avatar charguer
Browse files

cp

parent 386e3bfd
MAJOR TODAY
patterns
let f () =
let r : '_a ref = ref [] in
!r
let f () =
let r : int ref = ref [] in
!r
let f () : 'a list =
let r : 'a ref = ref [] in
!r
xwhile: error reporting when arguments don't have the right types.
rename xextract to xpull; and xgen to xpush.
......@@ -34,29 +21,30 @@ infix_eq_
- when clauses
- open no scope in CF.
- add support for pure records
- inline CFHeader.pred as -1
- xchanges
TopVal check brackets
MAJOR NEXT
MAJOR NEXT
- partial/over application
- xabstract => reimplement and rename as xgen
- eliminate notations for tags
MAJOR NEXT NEXT
- xwhile: error reporting when arguments don't have the right types.
- eliminate notations for tags
- record single field and array single cell notation
Notation "x `. f '~>' S" :=
Notation "x `[ i ] '~>' S" :=
......@@ -65,9 +53,12 @@ MAJOR NEXT NEXT
- see if we can get rid of make_cmj
- mutually recursive polymorhpic functions have too many type variables
quantified: we need one set of fvs for each def in the recursion.
MAJOR POSTPONED
- support char
- support float
- implement the work around for type abbreviations:
......
......@@ -11,36 +11,46 @@ open Pervasives
(********************************************************************)
(* ** Value restriction *)
(* -- accepted program: even though the internal type-checking
involves a ['_a ref] type, the result type is ['a list]. *)
(* -- rejected program: the internal type-checking involves a
['_a ref] type, even though the result type is ['a list].
let value_restriction_0 () =
let r = ref [] in
!r
*)
(* TODO: how to make this program accepted?
=> it is not currently because ocaml typechecker does not
propagate the information downwards in the term.
let value_restriction_1 () : 'a list =
let r = ref ([] : 'a list) in
!r
*)
(* -- rejected program: use of ['_a ref] type annotation is not supported.
let value_restriction_1 () =
let value_restriction_2 () =
let r : '_a ref = ref [] in
!r
*)
(* -- accepted program: monomorphic annotation on the let-bindings *)
let value_restriction_2 () =
let value_restriction_3 () =
let r : (int list) ref = ref [] in
!r
(* -- accepted program: monomorphic annotation on the empty list *)
let value_restriction_3 () =
let value_restriction_4 () =
let r = ref ([] : int list) in
!r
(* -- accepted program: the polymorphic type annotation is accepted,
but it fact it is refined by the type-checker as [(int list) ref]. *)
let value_restriction_4 () =
let value_restriction_5 () =
let r : ('a list) ref = ref [] in
r := [4];
!r
......@@ -48,7 +58,7 @@ let value_restriction_4 () =
(* -- accepted program: likewise, the list [[5]] is accepted at type
['a list], but it comes out at type [int list] from the type-checker. *)
let value_restriction_5 () : 'a list =
let value_restriction_6 () : 'a list =
let r = ref [] in
r := [5];
!r
......@@ -93,6 +103,20 @@ let ret_int_pair () =
let ret_poly () =
[]
(* --Not yet supported:
Error is: Cannot infer this placeholder of type Type
let ret_poly_internal () =
let x = ignore None in
()
*)
(* --TODO: BUG
The reference A_ was not found in the current environment.*)
let ret_poly_internal () =
let x = ignore (None : 'a option) in
()
(********************************************************************)
(* ** Sequence *)
......@@ -246,10 +270,42 @@ let compare_int () =
let compare_min () =
(min 0 1)
(*
(* not yet supported
let compare_float () =
(1. <> 0. && 1. <= 2.) || (0. = 1. && 1. >= 2. && 1. < 2. && 2. > 1.)
*)
let compare_poly () =
let _r1 = (None = None) in
let _r2 = (Some 3 = None) in
let _r3 = ((Some 3, None) = (Some 3, None)) in
let _r4 = (true = false) in
()
(* -- not yet supported (does not seem very useful)
let f () = 4 in
let _r5 = ((Some f, None) = (None, Some f)) in *)
let compare_physical_loc_func () =
let r1a = ref 1 in
let r1b = ref 1 in
let _r1 = (r1a == r1b) in
let _r2 = (r1a != r1b) in
let f () = 1 in
let _r3 = if (f == f) then f() else 1 in
()
let compare_physical_algebraic () =
let rec replace (k:int) (v:int) (l:(int*int) list) =
match l with
| [] -> l
| (k2,v2)::t2 ->
let t = replace k v t2 in
if k = k2 then (k,v)::t
else if t != t2 then (k2,v2)::t
else l (* no change *)
in
replace 1 9 [(1,3); (4,2); (2,5)]
(********************************************************************)
(* ** List operators *)
......@@ -354,13 +410,21 @@ let match_nested () =
| _::(0,0)::q -> q
| _ -> [(2,2)]
(* not yet supported when clauses
(* TODO
let match_term_when () =
let f x = x + 1 in
match f 3 with
| 0 -> 1
| n when n > 0 -> 2
| _ -> 3
let match_or_clauses p =
(* captures (Some x, _) or (_, Some x) with x > 0 *)
match p with
| (None, None) -> false
| ((Some x, _) | (_, Some x)) when x > 0 -> true
| (Some x, _) | (_, Some x) -> false
*)
......
......@@ -5,9 +5,27 @@ Require Import Demo_ml.
Require Import Stdlib.
let compare_options =
let _r1 = (None = None) in
let _r2 = (Some 3 = None) in
let _r3 = ((Some 3, None) = (None, Some 3)) in
let _r4 = ((Some 3, None) = (Some 3, None)) in
let _r5 = (true = false) in
()
let match_term_when () =
let f x = x + 1 in
match f 3 with
| 0 -> 1
| n when n > 0 -> 2
| _ -> 3
let match_or_clauses p =
(* captures (Some x, _) or (_, Some x) with x > 0 *)
match p with
| (None, None) -> false
| ((Some x, _) | (_, Some x)) when x > 0 -> true
| (Some x, _) | (_, Some x) -> false
......
# Possible to define "ML" to be the list of source files to consider
# Uncomment next line to compile only Test.ml
ML := Test.ml
CFDEBUG := 1
include ../Makefile.example
......@@ -91,6 +91,8 @@ code: ocamllib $(ML)
##############################################################
# Characteristic formula generation
ifndef CFDEBUG
cf: $(ML)
# Make sure TLC and CFML itself are up-to-date.
# Needed only when developing TLC and CFML. Ideally, should be removed.
......@@ -100,6 +102,21 @@ cf: $(ML)
@$(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
else
#----------------FOR DIRECT TEST----------------------
cf: $(ML)
@$(MAKE) -C $(CFML)/lib/tlc --no-print-directory quick
@$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick_cf
# @$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick
@$(MAKE) -C $(CFML)/lib/stdlib CFDEBUG=$(CFDEBUG) --no-print-directory cmj
@$(MAKE) CFML=$(CFML) EXTRA="-debug" OCAML_FLAGS="$(OCAML_FLAGS)" COQINCLUDE="$(COQINCLUDE)" ML="$(ML)" --no-print-directory -f $(CFML)/lib/make/Makefile.cf all
endif
proof:cf
......
......@@ -14,6 +14,8 @@ open Printf
let debug_generic = false
(*#########################################################################*)
(* ** Error messages *)
......@@ -104,14 +106,14 @@ let rec fv_btyp ?(through_arrow = true) t =
| Btyp_arrow (t1,t2) -> if through_arrow then aux t1 @ aux t2 else []
| Btyp_constr (id,ts) -> list_concat_map aux ts
| Btyp_tuple ts -> list_concat_map aux ts
| Btyp_var (b,s) -> [s]
| Btyp_var (b,s,ty) -> typvar_mark_used ty; [s]
| Btyp_poly (ss,t) -> unsupported_noloc "poly-types"
| Btyp_alias (t,s) -> s :: aux t
(** Translates a [btyp] into a Coq type *)
let rec lift_btyp t =
let aux = lift_btyp in
let rec lift_btyp loc t =
let aux = lift_btyp loc in
match t with
| Btyp_val ->
func_type
......@@ -124,8 +126,10 @@ let rec lift_btyp t =
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) ->
if b then unsupported_noloc "non-generalizable free type variables (of the form '_a); please add a type annotation";
| Btyp_var (b,s,ty) ->
typvar_mark_used ty;
if b then unsupported loc "non-generalizable free type variables (of the form '_a); please add a type annotation, because the relaxed value restriction is not supported.";
(* TODO: check if this is needed *)
Coq_var s
| Btyp_poly (ss,t) ->
unsupported_noloc "poly-types"
......@@ -155,25 +159,25 @@ let rec lift_btyp t =
(** Translates a Caml type into a Coq type *)
let lift_typ_exp ty =
lift_btyp (btyp_of_typ_exp ty)
let lift_typ_exp loc ty =
lift_btyp loc (btyp_of_typ_exp ty)
(** Translates a Caml type scheme into a Coq type *)
let lift_typ_sch ty =
let lift_typ_sch loc ty =
let t = btyp_of_typ_sch_simple ty in
let fv = fv_btyp ~through_arrow:false t in
fv, lift_btyp t
fv, lift_btyp loc t
(** Translates the type of a Caml expression into a Coq type *)
let coq_typ e =
lift_typ_exp (e.exp_type)
let coq_typ loc e =
lift_typ_exp loc (e.exp_type)
(** Translates the type of a Caml pattern into a Coq type *)
let coq_typ_pat p =
lift_typ_exp (p.pat_type)
let coq_typ_pat loc p =
lift_typ_exp loc (p.pat_type)
(** Decompose "A.B.s" as ("A.B","s") *)
......@@ -216,12 +220,24 @@ let typ_arity_constr c =
(** Translate a Caml data constructor into a Coq expression *)
let coq_of_constructor p c =
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
let x = string_of_path p in
match find_builtin_constructor x with
| None -> coq_app_var_wilds x (typ_arity_constr c)
| Some (y,arity) -> coq_app_var_wilds y arity
let coq_name, arity =
match find_builtin_constructor x with
| None -> x, (typ_arity_constr c)
| Some (coq_name,arity) -> coq_name, arity
in
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 *)
(*#########################################################################*)
(* ** Lifting of patterns *)
......@@ -233,7 +249,7 @@ let rec pattern_variables p : typed_vars = (* ignores aliases *)
let aux = pattern_variables in
match p.pat_desc with
| Tpat_any -> not_in_normal_form loc "wildcard patterns remain after normalization"
| Tpat_var s -> [var_name (Ident.name s), coq_typ_pat p]
| Tpat_var s -> [var_name (Ident.name s), coq_typ_pat loc p]
| Tpat_alias (p, s) -> aux p
| Tpat_constant c -> []
| Tpat_tuple l -> list_concat_map aux l
......@@ -257,14 +273,14 @@ let rec lift_pat ?(through_aliases=true) p : coq =
Coq_int n
| Tpat_tuple l ->
Coq_tuple (List.map aux l)
| Tpat_construct (p, c, ps) ->
coq_apps (coq_of_constructor p c) (List.map aux ps)
| Tpat_construct (path, c, ps) ->
coq_apps (coq_of_constructor loc path c p.pat_type) (List.map aux ps)
| Tpat_alias (p, ak) ->
begin match ak with
| TPat_alias id ->
if through_aliases then aux p else Coq_var (var_name (Ident.name id))
| TPat_constraint ty ->
let typ = lift_typ_exp ty.ctyp_type in
let typ = lift_typ_exp loc ty.ctyp_type in
Coq_annot (aux p, typ)
| TPat_type pp -> aux p
end
......@@ -291,7 +307,7 @@ let pattern_aliases p : (typed_var*coq) list =
| Tpat_alias (p1, ak) ->
begin match ak with
| TPat_alias id ->
((Ident.name id, coq_typ_pat p), lift_pat ~through_aliases:false p1) :: (aux p1)
((Ident.name id, coq_typ_pat loc p), lift_pat ~through_aliases:false p1) :: (aux p1)
| TPat_constraint _ -> aux p1
| TPat_type pp -> aux p1
end
......@@ -398,11 +414,13 @@ let exp_find_inlined_primitive e oargs =
| _ -> false
end in
(* Remark: by typing, [e2] has the same type as [e1] *)
if not is_number then
unsupported loc (Printf.sprintf "comparison operators on non integer arguments (here, %s)" (string_of_type_exp e1.exp_type));
begin match find_inlined_primitive name with
| Some (Primitive_binary_only_numbers, coq_name) -> Some coq_name
| _ -> failwith ("in exp_find_inlined_primitive, could not find the coq translation of the function: " ^ name)
if not is_number then begin
if List.mem name [ "Pervasives.="; "Pervasives.<>"; ]
then None
else unsupported loc (Printf.sprintf "comparison operators on non integer arguments (here, %s)" (string_of_type_exp e1.exp_type));
end else begin match find_inlined_primitive name with
| Some (Primitive_binary_only_numbers, coq_name) -> Some coq_name
| _ -> failwith ("in exp_find_inlined_primitive, could not find the coq translation of the function: " ^ name)
end
| _ ->
......@@ -458,7 +476,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 p c) (List.map aux es)
coq_apps (coq_of_constructor loc p c e.exp_type) (List.map aux es)
| 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";
......@@ -470,7 +488,7 @@ let rec lift_val env e =
let constr = record_constructor_name_from_type (prefix_for_label (e.exp_type)) in
let typ_args =
match btyp_of_typ_exp e.exp_type with
| Btyp_constr (id,ts) -> List.map lift_btyp ts
| Btyp_constr (id,ts) -> List.map (lift_btyp loc) ts
| _ -> failwith "record should have a type-constructor as type"
in
coq_apps (coq_var_at constr) (typ_args @ Array.to_list args)
......@@ -485,7 +503,7 @@ let rec lift_val env e =
| Texp_lazy e ->
aux e
| Texp_constraint (e, Some ty, None) ->
let typ = lift_typ_exp ty.ctyp_type in
let typ = lift_typ_exp loc ty.ctyp_type in
Coq_annot (aux e, typ)
(* --uncomment for debugging
......@@ -616,7 +634,7 @@ let rec cfg_exp env e =
if opt_init_expr <> None then unsupported loc "record-with";
let named_args = List.map (fun (p,li,ei) -> (li.lbl_name,ei)) lbl_expr_list in
let build_arg (name, arg) =
let value = coq_apps coq_dyn_at [coq_typ arg; lift arg] in
let value = coq_apps coq_dyn_at [coq_typ loc arg; lift arg] in
Coq_tuple [Coq_var (record_field_name name); value]
in
let arg = coq_list (List.map build_arg named_args) in
......@@ -666,11 +684,17 @@ let rec cfg_exp env e =
if (List.length pat_expr_list <> 1) then not_normal();
let (pat,bod) = List.hd pat_expr_list in
let x = pattern_name_protect_infix pat in
let fvs_typ, typ = lift_typ_sch pat.pat_type in
let fvs = List.map name_of_type fvs in
let fvs_strict = list_intersect fvs fvs_typ in
let fvs_others = list_minus fvs fvs_strict in
let get_fvs_typ () = (* needs to be called after typing the body! *)
let fvs_typ, typ = lift_typ_sch loc pat.pat_type in
let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
if debug_generic
then Printf.printf "fvs exp_let = %s\n" (show_list show_str " , " fvs);
let fvs_strict = list_intersect fvs fvs_typ in
let fvs_others = list_minus fvs fvs_strict in
(fvs_strict, fvs_others, typ)
in
(* deprecated: pure-mode let-binding
if !pure_mode then begin
......@@ -689,6 +713,7 @@ let rec cfg_exp env e =
with Not_in_normal_form (loc2, s) ->
raise (Not_in_normal_form (loc2, s ^ " (only value can satisfy the value restriction)"))
in
let (fvs_strict, fvs_others, typ) = get_fvs_typ() in
let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
let cf = cfg_exp env' body in
add_used_label x;
......@@ -696,7 +721,12 @@ let rec cfg_exp env e =
(* term let-binding *)
end else begin
let (fvs_strict, fvs_others, typ) = get_fvs_typ() in
(* if debug_generic
then *)
Printf.printf "fvs_strict = %s\n" (show_list show_str " , " fvs_strict);
Printf.printf "fvs_others = %s\n" (show_list show_str " , " fvs_others);
if fvs_strict <> [] || fvs_others <> []
then unsupported loc "relaxed value restriction";
(* not_in_normal_form loc ("(un value restriction) "
......@@ -716,8 +746,8 @@ let rec cfg_exp env e =
| Texp_apply (funct, oargs) ->
let args = simplify_apply_args loc oargs in
let tr = coq_typ e in
let ts = List.map coq_typ args in
let tr = coq_typ loc e in
let ts = List.map (coq_typ loc) args in
Cf_app (ts, tr, lift funct, List.map lift args)
| Texp_match (arg, pat_expr_list, partial) ->
......@@ -767,17 +797,17 @@ let rec cfg_exp env e =
let arg = coq_list (List.map lift args) in
let targ = (* ['a], obtained by extraction from ['a array]. *)
match btyp_of_typ_exp e.exp_type with
| Btyp_constr (id,[t]) when Path.name id = "array" -> lift_btyp t
| Btyp_constr (id,[t]) when Path.name id = "array" -> lift_btyp loc t
| _ -> failwith "Texp_array should always have type ['a array]"
in
let ts = coq_apps (Coq_var "Coq.Init.Datatypes.list") [targ] in
let tr = coq_typ e in (* 'a array *)
let tr = coq_typ loc e in (* 'a array *)
let func = Coq_var "STDLIB.Array_ml.make_empty" in
Cf_app ([ts], tr, func, [arg])
| Texp_field (arg, p, lbl) ->
let tr = coq_typ e in
let ts = coq_typ arg in (* todo: check it is always 'loc' *)
let tr = coq_typ loc e in
let ts = coq_typ loc arg in (* todo: check it is always 'loc' *)
let func = Coq_var "CFML.CFApp.record_get" in
let field = Coq_var (record_field_name lbl.lbl_name) in
Cf_app ([ts; coq_nat], tr, func, [lift arg; field])
......@@ -787,8 +817,8 @@ let rec cfg_exp env e =
*)
| Texp_setfield(arg, p, lbl, newval) ->
let ts1 = coq_typ arg in (* todo: check it is always 'loc' *)
let ts2 = coq_typ newval in
let ts1 = coq_typ loc arg in (* todo: check it is always 'loc' *)
let ts2 = coq_typ loc newval in
let func = Coq_var "CFML.CFApp.record_set" in
let field = Coq_var (record_field_name lbl.lbl_name) in
Cf_app ([ts1; coq_nat; ts2], coq_unit, func, [lift arg; field; lift newval])
......@@ -814,7 +844,7 @@ let rec cfg_exp env e =
| Texp_open (_,_) -> unsupported loc "open in term"
| Texp_constraint (e, Some ty, None) -> aux e
(* LATER: see if it is needed
let typ = lift_typ_exp ty.ctyp_type in
let typ = lift_typ_exp loc ty.ctyp_type in
CF_annot (aux e, typ)
*)
| Texp_constraint (e, _, _) -> unsupported loc "advanced type constraint"
......@@ -828,15 +858,18 @@ and cfg_func env fvs pat bod =
| Texp_constraint ({exp_desc = Texp_function (_,[p1,e1],partial)},_,_) ->
if partial <> Total
then not_in_normal_form loc (Print_tast.string_of_expression false e);
get_typed_args ((pattern_name p1, coq_typ_pat p1)::acc) e1
get_typed_args ((pattern_name p1, coq_typ_pat loc p1)::acc) e1
| _ -> List.rev acc, e
in
let loc = pat.pat_loc in
let f = pattern_name_protect_infix pat in
let targs, body = get_typed_args [] bod in
let typ = coq_typ body in
let typ = coq_typ loc body in
let cf_body = cfg_exp env body in
let cf_body = if !Mytools.use_credits then Cf_pay cf_body else cf_body in
let fvs = List.map name_of_type fvs in
let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
if debug_generic
then Printf.printf "fvs cfg_func = %s\n" (show_list show_str " , " fvs);
Cf_body (f, fvs, targs, typ, cf_body)
(* --todo: check if the set of type variables quantified is not too
conservative. Indeed, some type variables may no longer occur. *)
......@@ -891,11 +924,18 @@ let rec cfg_structure_item s : cftops =
let x = pattern_name_protect_infix pat in
(* DEPRECATED if (hack_recognize_okasaki_lazy x) then [] else *)
begin
let fvs_typ, typ = lift_typ_sch pat.pat_type in
let fvs = List.map name_of_type fvs in
let fvs_strict = list_intersect fvs fvs_typ in
let fvs_others = list_minus fvs fvs_strict in