Commit 450e1b90 authored by charguer's avatar charguer
Browse files

compiles

parent ef3b2492
......@@ -22,7 +22,6 @@ SANITY
- restriction on not binding "min" and "max" could be a bit restrictive..
LATER
- in print_tast and print_past, protect with parenth the infix names being bound
......@@ -39,7 +38,7 @@ LATER
- make systematic use of || (rm -f $@; exit 1) in cfml calls
- currently type annotations in pattern get lost
DEPRECATED?
......
......@@ -220,6 +220,10 @@ let top_val_poly_list = []
let top_val_poly_list_pair = ([],[])
let (top_val_pair_int_1,top_val_pair_int_2) = (1,2)
let (top_val_pair_fun_1,top_val_pair_fun_2) = (fun x -> x), (fun x -> x)
(********************************************************************)
(* ** Polymorphic let bindings *)
......@@ -278,14 +282,28 @@ let exn_raise () =
(* ** Assertions *)
let assert_true () =
assert true; 3
assert true;
3
let assert_pos x =
assert (x > 0); 3
assert (x > 0);
3
let assert_same (x:int) (y:int) =
assert (x = y); 3
assert (x = y);
3
let assert_let () =
assert (let x = true in true);
3
let assert_seq () =
let r = ref 0 in
assert (incr r; true);
!r
let assert_in_seq () =
(assert (true); 3) + 1
(********************************************************************)
......@@ -382,19 +400,18 @@ let order_record () =
{ nb = f(); items = g() }
*)
(* not yet supported : array initializers
let order_array () =
let r = ref 0 in
let f () = incr r; 1 in
let g () = assert (!r = 1); 1 in
[| g() ; f() |]
*)
(********************************************************************)
(* ** Arrays *)
let array_ops () =
let u = [||] in
let t = Array.make 3 0 in
let _x = t.(1) in
t.(2) <- 4;
......
......@@ -10,7 +10,7 @@ Print TLC.LibOrder.ge_from_le.
Definition f := (fun x_ y_ : int => TLC.LibReflect.isTrue (x_ >= y_)).
Print f.
Locate list.
Definition g := .
(fun x_ y_ : int => TLC.LibReflect.isTrue (TLC.LibOrder.lt (TLC.LibOrder.ge_from_le TLC.LibInt.le) x_ y_)).
......@@ -625,6 +625,18 @@ Proof using.
Qed.
let assert_let () =
assert (let x = true in true);
3
let assert_seq () =
let r = ref 0 in
assert (incr r; true);
!r
let assert_in_seq () =
(assert (true); 3) + 1
(********************************************************************)
(* ** Assertions *)
......@@ -879,4 +891,9 @@ Proof using. intros. xcf. xval as p Hp. subst p. xrets. auto. Qed.
*)
(*
let (top_val_pair_int_1,top_val_pair_int_2) = (1,2)
let (top_val_pair_fun_1,top_val_pair_fun_2) = (fun x -> x), (fun x -> x)
*)
......@@ -97,7 +97,7 @@ 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 --no-print-directory quick
@$(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
......
......@@ -478,8 +478,6 @@ let rec lift_val env e =
coq_apps (Coq_var f) (List.map aux args)
| Texp_lazy e ->
aux e
| Texp_array [] ->
Coq_var "array_empty"
| Texp_constraint (e,_,_) ->
aux e
......@@ -749,7 +747,20 @@ let rec cfg_exp env e =
| Downto -> unsupported loc "for-downto expressions" (* later *)
end
| Texp_array expr_list -> unsupported loc "array expressions" (* later *)
| Texp_array args ->
let ccons = Coq_var (get_builtin_constructor "::") in
let cnil = Coq_var (get_builtin_constructor "[]") in
let arg = List.fold_right (fun arg acc ->
coq_apps ccons [lift arg; acc]) args cnil 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
| _ -> 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 func = Coq_var "STDLIB.Array.make_empty" in
Cf_app ([ts], tr, func, [arg])
| Texp_field (arg, p, lbl) ->
let tr = coq_typ e in
......
......@@ -210,22 +210,34 @@ let create_match_one loc exp pat body =
{ pexp_loc = loc;
pexp_desc = Pexp_match (exp,[pat,body]) }
let get_assign_fct loc already_named new_name : expression -> bindings -> expression * bindings =
if already_named
then fun e b -> e,b
else let x = new_name() in
fun e b ->
let p = { ppat_loc = loc; ppat_desc = Ppat_var x } in
let e' = { pexp_loc = loc; pexp_desc = Pexp_ident (Lident x) } in
e', b @ [ p, e ]
(* argument [is_named] indicates whether the context in which appear
(* See documentation of [wrap_as_value e' b] further below *)
let wrap_if_needed loc needs_wrapping new_name e b =
(* : expression -> bindings -> expression * bindings *)
if needs_wrapping
then let x = new_name() in
let p = { ppat_loc = loc; ppat_desc = Ppat_var x } in
let e' = { pexp_loc = loc; pexp_desc = Pexp_ident (Lident x) } in
e', b @ [ p, e ]
else e,b
(* The main translation function takes an expression [e] and produces
a translated expression [e'] and a set of bindings [b] in which [e']
properly evaluates to a value. The bindings in [b] should in particular
account for all side-effects performed by [e], in the right order.
The argument [as_value] indicates whether the context in which [e] appears
requires the production of a value. In this case, if the translation of
[e] is not a value, then it is given as a fresh variable [x], together
with an additional binding from [x] to [e].
The argument [is_named] indicates whether the context in which [e] appears
is already a [let x = ... in ..]. If this is the case and we
encounter a function, then we don't need to introduce a fresh name
for it. Otherwise, any occurence of [fun .. -> ..] will be turned
into [let f = fun .. -> .. in f], for a fresh name f. *)
let normalize_expression is_named e =
let normalize_expression ?is_named:(is_named=false) ?as_value:(as_value=false) e =
let loc = e.pexp_loc in
let i = ref (-1) in (* TODO: use a gensym function *)
let next_var () =
......@@ -233,7 +245,7 @@ let normalize_expression is_named e =
let j = ref (-1) in
let next_func () =
incr j; (function_generated_name !j) in
let rec aux named (e:expression) : expression * bindings =
let rec aux ?is_named:(is_named=false) ?as_value:(as_value=false) (e:expression) : expression * bindings =
let loc = e.pexp_loc in
let return edesc' =
{ e with pexp_desc = edesc' } in
......@@ -242,40 +254,40 @@ let normalize_expression is_named e =
let explicit_arity = false in (* todo: what does it mean? *)
return (Pexp_construct (Lident svalue, None, explicit_arity)) in
(* [assign_var e' b] takes a a transformed expression and a list
(* [wrap_as_value e' b] takes a a transformed expression and a list
of bindings; and it returns a transformed expression and a list
of bindings. If the parameter [named] is true, then this returns
simply [(e',b)]. Otherwise, it returns a pair [(var x, b')],
where [b'] extends [b] with the binding from [x] to [e'].
This function should be called any time the translation
produces a term that may not be a value. *)
let assign_var e b =
get_assign_fct loc is_named next_var e b in
(* DEPRECATED *)
produces a term that may not be a value. *)
let wrap_as_value e b =
wrap_if_needed loc as_value next_var e b in
match e.pexp_desc with
| Pexp_ident li -> return (Pexp_ident li), []
| Pexp_constant c -> return (Pexp_constant c), []
| Pexp_let (Recursive, l, eb) ->
let l' = List.map protect_branch l in
let eb' = protect true eb in
let eb' = protect eb in
let e' = Pexp_let (Recursive, l', eb') in
assign_var (return e') []
wrap_as_value (return e') []
| Pexp_let (rf, [], e2) -> unsupported loc "let without any binding"
| Pexp_let (rf, [p1,e1], e2) ->
begin match p1.ppat_desc with
| Ppat_var x
| Ppat_constraint ({ ppat_desc = Ppat_var x}, _) ->
let e1',b1 = aux true e1 in
let e1',b1 = aux ~is_named:true e1 in
let e' = create_let loc b1 (
create_let loc [normalize_pattern p1, e1'] (
protect false e2)) in
assign_var e' []
protect e2)) in
wrap_as_value e' []
| _ ->
let e1',b1 = aux false e1 in
(* [let p1 = e1 in e2] is viewed as [match e1 with p1 -> e2] *)
let e1',b1 = aux ~as_value:true e1 in
let e' = create_let loc b1 (
create_match_one loc e1' (normalize_pattern p1) (protect false e2)) in
assign_var e' []
create_match_one loc e1' (normalize_pattern p1) (protect e2)) in
wrap_as_value e' []
end
| Pexp_let (rf, l, e) -> unsupported loc "non-recursive let-and construct"
(* DEPRECATED --seems buggous
......@@ -290,33 +302,38 @@ let normalize_expression is_named e =
aux true (List.fold_right (fun (pi,ei) eacc -> create_let loc [pi,ei] eacc) l e)
*)
| Pexp_function (lab, None, [_]) ->
(* function with a single pattern *)
let rec protect_func (ms : (expression * pattern) list) (e : expression) =
(* [function x1 p2 x3 p4 x5 -> e] is translated as
[fun x1 x2 x3 x4 x5 ->
match x2 with p2 ->
match x4 with p4 -> e']
*)
let rec trans_func (ms : (expression * pattern) list) (e : expression) =
match e.pexp_desc with
| Pexp_function (lab, None, [p, e']) ->
let p' = normalize_pattern p in
begin match p'.ppat_desc with
| Ppat_var x
| Ppat_constraint ({ ppat_desc = Ppat_var x}, _) ->
return (Pexp_function (lab, None, [p', protect_func ms e']))
(* todo: type annotations in pattern get lost *)
return (Pexp_function (lab, None, [p', trans_func ms e']))
(* TODO: currently type annotations in pattern get lost *)
| Ppat_construct (li, None, b) when Longident.flatten li = ["()"] ->
let x = next_var() in
let px = { ppat_loc = loc; ppat_desc = Ppat_var x } in
return (Pexp_function (lab, None, [px, protect_func ms e']))
return (Pexp_function (lab, None, [px, trans_func ms e']))
| _ ->
let x = next_var() in
let px = { ppat_loc = loc; ppat_desc = Ppat_var x } in
let vx = { pexp_loc = loc; pexp_desc = Pexp_ident (Lident x) } in
let ms' = (vx, p')::ms in
return (Pexp_function (lab, None, [px, protect_func ms' e']))
return (Pexp_function (lab, None, [px, trans_func ms' e']))
end
| _ ->
let addmatch eacc (vi,pi) =
return (Pexp_match (vi, [pi,eacc])) in
List.fold_left addmatch (protect true e) ms
in
get_assign_fct loc is_named next_func (protect_func [] e) []
List.fold_left addmatch (protect e) ms
in
(* here we force the wrapping whenever [is_named] or [as_value] is true *)
wrap_if_needed loc (as_value || not is_named) next_func (trans_func [] e) []
| Pexp_function (lab, None, l) ->
(* [function p1 -> e1 | p2 -> e2] encoded as the translation of
[function x_ match x_ with p1 -> e1 | p2 -> e2] *)
......@@ -324,49 +341,53 @@ let normalize_expression is_named e =
let px = { ppat_loc = Location.none (* hack to pass check-var *); ppat_desc = Ppat_var x } in (* todo: better hack to remember created var *)
let vx = { pexp_loc = Location.none (* hack to pass check-var *); pexp_desc = Pexp_ident (Lident x) } in
let e' = return (Pexp_match (vx, l)) in
aux named (return (Pexp_function (lab, None, [px,e'])))
aux ~is_named:is_named (return (Pexp_function (lab, None, [px,e'])))
| Pexp_function (p, Some _, l) ->
unsupported loc "function with optional expression"
| Pexp_apply (e0, l) when is_failwith_function e0 ->
return Pexp_assertfalse, []
| Pexp_apply (e0, [(l1,e1); (l2,e2)]) when is_lazy_binary_op e0 ->
(* This case is for [e1 && e2] and [e1 || e2] *)
(* TODO: assert that the labels are irrelevant here *)
let e0',b0 = aux false e0 in
let e0',b0 = aux ~as_value:true e0 in
let name = match e0.pexp_desc with
| Pexp_ident f -> name_of_lident f
| _ -> assert false (* could not be a lazy op otherwise *)
in
assert (b0 = []); (* since e0 should be "&&" or "||" *)
let e1',b1 = aux false e1 in
let e2',b2 = aux false e2 in
let e1',b1 = aux ~as_value:true e1 in
let e2',b2 = aux ~as_value:true e2 in
if b2 = [] then begin
(* produce: let <b1> in <e1> && <e2>
let <b1> in <e1> || <e2> *)
let e' = return (Pexp_apply (e0', [(l1,e1'); (l2,e2')])) in
e', b1
wrap_as_value e' b1
end else if name = "&&" then begin
(* produce: let <b1> in if <e1'> then (let <b2> in <e2'>) else false *)
assign_var (return (
wrap_as_value (return (
Pexp_ifthenelse (
e1',
create_let loc b2 e2',
Some (mk_bool false)))) b1
end else if name = "||" then begin
(* produce: let <b1> in if <e1'> then true else (let <b2> in <e2'>) *)
assign_var (return (
wrap_as_value (return (
Pexp_ifthenelse (
e1',
mk_bool true,
Some (create_let loc b2 e2')))) b1
end else assert false
| Pexp_apply (e0, l) ->
let e0',b0 = aux false e0 in
let ei',bi = List.split (List.map (fun (lk,ek) -> let ek',bk = aux false ek in (lk, ek'), bk) l) in
let is_inlined = exp_is_inlined_primitive e0 l in
let e0',b0 = aux ~as_value:true e0 in
let ei',bi = List.split (List.map (fun (lk,ek) -> let ek',bk = aux ~as_value:true ek in (lk, ek'), bk) l) in
let e' = return (Pexp_apply (e0', ei')) in
let b' = List.flatten (reverse_if_right_to_left_order (b0::bi)) in
if exp_is_inlined_primitive e0 l
if is_inlined
then e', b'
else assign_var e' b'
else wrap_as_value e' b'
| Pexp_match (e0, l) ->
let e0',b0 = aux false e0 in
let e0',b0 = aux ~as_value:true e0 in
let l' =
let rec or_pats (p,e) =
match p.ppat_desc with
......@@ -385,67 +406,67 @@ let normalize_expression is_named e =
vx, b0@[px,e0']
end in
let e' = Pexp_match (e0', List.map protect_branch l') in
assign_var (return e') b0
wrap_as_value (return e') b0
| Pexp_try (e,l) -> unsupported loc "exceptions"
| Pexp_tuple l ->
let l',bi = List.split (List.map (aux false) l) in
let l',bi = List.split (List.map (aux ~as_value:true) l) in
let b = List.flatten (reverse_if_right_to_left_order bi) in
return (Pexp_tuple l'), b
| Pexp_construct (li, None, b) ->
return (Pexp_construct (li, None, b)), []
| Pexp_construct (li, Some e, bh) ->
let e',b = aux false e in
let e',b = aux ~as_value:true e in
return (Pexp_construct (li, Some e', bh)), b
| Pexp_variant (l,eo) -> unsupported loc "variants"
| Pexp_record (l,Some eo) -> unsupported loc "record-with"
| Pexp_record (l,None) ->
let l',bi = List.split (List.map (fun (i,(e,b)) -> ((i,e),b)) (assoc_list_map (aux false) l)) in
let l',bi = List.split (List.map (fun (i,(e,b)) -> ((i,e),b)) (assoc_list_map (aux ~as_value:true) l)) in
let b = List.flatten (reverse_if_right_to_left_order bi) in
assign_var (return (Pexp_record (l', None))) b
wrap_as_value (return (Pexp_record (l', None))) b
| Pexp_field (e,i) ->
let e',b = aux false e in
assign_var (return (Pexp_field (e', i))) b
let e',b = aux ~as_value:true e in
wrap_as_value (return (Pexp_field (e', i))) b
| Pexp_setfield (e,i,e2) ->
let e',b = aux false e in
let e2',b2 = aux false e2 in
assign_var (return (Pexp_setfield (e', i, e2'))) (b2 @ b)
| Pexp_array l -> (* todo: use assign *)
let l',bi = List.split (List.map (aux false) l) in
let e',b = aux ~as_value:true e in
let e2',b2 = aux ~as_value:true e2 in
wrap_as_value (return (Pexp_setfield (e', i, e2'))) (b2 @ b)
| Pexp_array l ->
let l',bi = List.split (List.map (aux ~as_value:true) l) in
let b = List.flatten (reverse_if_right_to_left_order bi) in
return (Pexp_array l'), b
wrap_as_value (return (Pexp_array l')) b
| Pexp_ifthenelse (e1, e2, None) ->
(* old:
let e1', b = aux true e1 in
assign_var (return (Pexp_ifthenelse (e1', protect named e2, Some (return (Pexp_construct (Lident "()", None, false)))))) b
wrap_as_value (return (Pexp_ifthenelse (e1', protect named e2, Some (return (Pexp_construct (Lident "()", None, false)))))) b
*)
let e1', b = aux false e1 in
assign_var (return (Pexp_ifthenelse (e1', protect false e2, Some (return (Pexp_construct (Lident "()", None, false)))))) b
let e1', b = aux ~as_value:true e1 in
wrap_as_value (return (Pexp_ifthenelse (e1', protect e2, Some (return (Pexp_construct (Lident "()", None, false)))))) b
| Pexp_ifthenelse (e1, e2, Some e3) ->
(* old
let e1', b = aux true e1 in
assign_var (return (Pexp_ifthenelse (e1', protect named e2, Some (protect named e3)))) b
wrap_as_value (return (Pexp_ifthenelse (e1', protect named e2, Some (protect named e3)))) b
*)
let e1', b = aux false e1 in
assign_var (return (Pexp_ifthenelse (e1', protect false e2, Some (protect false e3)))) b
let e1', b = aux ~as_value:true e1 in
wrap_as_value (return (Pexp_ifthenelse (e1', protect e2, Some (protect e3)))) b
(* todo: tester: if then else fun x -> x *)
| Pexp_sequence (e1,e2) ->
let e1', b = aux true e1 in
let e1', b = aux e1 in
let tunit = Some { ptyp_desc = Ptyp_constr (Lident "unit", []); ptyp_loc = loc } in
let e1'' = return (Pexp_constraint (e1', tunit, None)) in
assign_var (return (Pexp_sequence (e1'', protect false e2))) b
wrap_as_value (return (Pexp_sequence (e1'', protect e2))) b
| Pexp_while (e1,e2) ->
assign_var (return (Pexp_while (protect false e1, protect false e2))) []
wrap_as_value (return (Pexp_while (protect e1, protect e2))) []
| Pexp_for (s,e1,e2,d,e3) ->
let e1', b1 = aux false e1 in
let e2', b2 = aux false e2 in
assign_var (return (Pexp_for (s, e1', e2', d, protect false e3))) (b1 @ b2)
let e1', b1 = aux ~as_value:true e1 in
let e2', b2 = aux ~as_value:true e2 in
wrap_as_value (return (Pexp_for (s, e1', e2', d, protect e3))) (b1 @ b2)
| Pexp_constraint (e,to1,to2) ->
let e',b = aux named e in
let e',b = aux e in
return (Pexp_constraint (e',to1,to2)), b
(* todo: if e' is just a name, then the constraint should be contained in b *)
| Pexp_when (econd,ebody) ->
let econd' = protect false econd in
let ebody' = protect false ebody in
let econd' = protect econd in
let ebody' = protect ebody in
return (Pexp_when (econd', ebody')), []
| Pexp_send (_,_) -> unsupported loc "send expression"
| Pexp_new _ -> unsupported loc "new expression"
......@@ -453,12 +474,11 @@ let normalize_expression is_named e =
| Pexp_override _ -> unsupported loc "Pexp_override expression"
| Pexp_letmodule (_,_,_) -> unsupported loc "let-module expression"
| Pexp_assert e ->
let e',b = aux false e in
return (Pexp_assert e'), b
return (Pexp_assert (protect e)), []
| Pexp_assertfalse ->
assign_var (return Pexp_assertfalse) []
wrap_as_value (return Pexp_assertfalse) []
| Pexp_lazy e ->
let e',b = aux false e in
let e',b = aux ~is_named:is_named e in
return (Pexp_lazy e'), b
| Pexp_poly (_,_) -> unsupported loc "poly expression"
| Pexp_object _ -> unsupported loc "objects"
......@@ -467,23 +487,25 @@ let normalize_expression is_named e =
| Pexp_open (id,e) -> unsupported loc "open local" (* Pexp_open (id,aux e), b *)
(* [protect named e] calls the translation function [aux named e],
(* [protect is_named e] calls the translation function [aux is_named e],
obtaining a transformed term [e'] under a list of bindings [b],
and it returns the term [let x1 = v1 in .. let xn = vn in e']
where the [b] gives the list of the [(xi,vi)] pairs. *)
and protect named e =
let (e',b) = aux named e in
and protect ?is_named:(is_named=false) e =
let (e',b) = aux ~is_named:is_named e in
create_let e.pexp_loc b e'
and protect_branch (p,e) =
(normalize_pattern p, protect true e)
(normalize_pattern p, protect e)
in
protect named e
protect ~is_named:true e
let normalize_pattern_expression (p,e) =
(normalize_pattern p, normalize_expression true e)
(* TODO: is_named is true only if the pattern is trivial *)
(normalize_pattern p,
normalize_expression ~is_named:true e)
(*#########################################################################*)
......@@ -506,7 +528,7 @@ and normalize_structure s =
and normalize_structure_item si =
let loc = si.pstr_loc in
{ si with pstr_desc = match si.pstr_desc with
| Pstr_eval e -> Pstr_eval (normalize_expression true e)
| Pstr_eval e -> Pstr_eval (normalize_expression ~is_named:true e)
| Pstr_value (r,l) -> Pstr_value (r, List.map normalize_pattern_expression l)
| Pstr_primitive (s,v) -> Pstr_primitive (s,v)
| Pstr_type l -> Pstr_type l
......
......@@ -79,14 +79,21 @@ let builtin_constructors_table =
(* --todo: add [Pervasives] as prefix *)
(** [find_builtin_constructor] finds the primitive data-constructor associated
with the argument, and return an optional result.
(** [find_builtin_constructor p] finds the primitive data-constructor associated
with the argument [p], and return an optional result.
For example, given "::" it gives "Coq.Lists.List.cons" and 1,
where 1 is the number of type arguments to cons in Coq. *)
let find_builtin_constructor p =
list_assoc_option p builtin_constructors_table
(** [get_builtin_constructor p] finds the primitive data-constructor associated
with the argument [p], and return the Coq name associated with it. *)
let get_builtin_constructor p =
match find_builtin_constructor p with
| Some (coq_name, arity) -> coq_name
| _ -> failwith ("get_builtin_constructor could not find: " ^ p)
(*#########################################################################*)
......
(* Temporary: because [||] is not supported. *)
external make_empty : unit -> 'a array = "%array_make_empty"
(* Special construction for [|v1; .. ; vN|], encoded as
Array.make_from_list [v1; .. ; vN]. *)
external make_from_list : 'a list -> 'a array = "%array_make_from_list"
(* Special case for [||], needed to implement this file. *)
let make_empty () = make_from_list []
(* Alternative:
external make_empty : unit -> 'a array = "%array_make_empty"
*)
external make : int -> 'a -> 'a array = "%array_make"
......
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