Commit 39594924 authored by charguer's avatar charguer

annotations

parent f892e094
......@@ -23,13 +23,13 @@ SANITY
- restriction on not binding "min" and "max" could be a bit restrictive..
- carry through type annotations in patterns
- "fun () -> ..." is encoded as "fun x ->" but it should be "fun (x:unit) ->"
LATER
- add support for pure records
- in print_tast and print_past, protect with parenth the infix names being bound
- make sure that check_var is called where needed
......
......@@ -250,6 +250,22 @@ let let_poly_nil_pair_heterogeneous () =
let x : ('a list * int list) = ([], []) in x
(********************************************************************)
(* ** Type annotations *)
let annot_let () =
let x : int = 3 in x
let annot_tuple_arg () =
(3, ([] : int list))
let annot_pattern_var x =
match (x : int list) with [] -> 1 | _ -> 0
let annot_pattern_constr () =
match ([] : int list) with [] -> 1 | _ -> 0
(********************************************************************)
(* ** Pattern-matching *)
......
......@@ -3,6 +3,7 @@ Set Implicit Arguments.
Require Import CFLib.
Require Import Demo_ml.
(*
Require Import Pervasives_ml. (* optional, improves display of, e.g. [incr] *)
Print TLC.LibOrder.ge_from_le.
......@@ -897,3 +898,22 @@ 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)
*)
(********************************************************************)
(* ** Type annotations *)
let annot_let () =
let x : int = 3 in x
let annot_tuple_arg () =
(3, ([] : int list))
let annot_pattern_var x =
match (x : int list) with [] -> 1 | _ -> 0
let annot_pattern_constr () =
match ([] : int list) with [] -> 1 | _ -> 0
*)
\ No newline at end of file
......@@ -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
......
......@@ -263,7 +263,9 @@ let rec lift_pat ?(through_aliases=true) p : coq =
begin match ak with
| TPat_alias id ->
if through_aliases then aux p else Coq_var (Ident.name id)
| TPat_constraint _ -> aux p
| TPat_constraint ty ->
let typ = lift_typ_exp ty.ctyp_type in
Coq_annot (aux p, typ)
| TPat_type pp -> aux p
end
| Tpat_lazy p1 ->
......@@ -362,10 +364,10 @@ let exp_find_inlined_primitive e oargs =
| Texp_ident (f,d) ->
let name = get_qualified_pervasives_name f in
let debug() =
let _debug() =
Printf.printf "exp_find_inlined_primitive: %s\n arity: %d\n name: %s\n" (Path.name f) (List.length args) name
in
(* debug(); *)
(* _debug(); *)
begin match args with
| [n; {exp_desc = Texp_constant (Const_int m)}]
......@@ -390,6 +392,7 @@ let exp_find_inlined_primitive e oargs =
let is_number =
begin match btyp_of_typ_exp e1.exp_type with
| Btyp_constr (id,[]) when Path.name id = "int" -> true
| _ -> false
end in
(* Remark: by typing, [e2] has the same type as [e1] *)
if not is_number then
......@@ -478,8 +481,9 @@ let rec lift_val env e =
coq_apps (Coq_var f) (List.map aux args)
| Texp_lazy e ->
aux e
| Texp_constraint (e,_,_) ->
aux e
| Texp_constraint (e, Some ty, None) ->
let typ = lift_typ_exp ty.ctyp_type in
Coq_annot (aux e, typ)
(* --uncomment for debugging
| Texp_function _ -> not_in_normal_form loc "function"
......@@ -789,7 +793,13 @@ let rec cfg_exp env e =
| Texp_newtype (_,_) -> unsupported loc "newtype"
| Texp_pack _ -> unsupported loc "pack"
| Texp_open (_,_) -> unsupported loc "open in term"
| Texp_constraint (e,_,_) -> aux e
| Texp_constraint (e, Some ty, None) -> aux e
(* LATER: see if it is needed
let typ = lift_typ_exp ty.ctyp_type in
CF_annot (aux e, typ)
*)
| Texp_constraint (e, _, _) -> unsupported loc "advanced type constraint"
and cfg_func env fvs pat bod =
let rec get_typed_args acc e =
......@@ -1087,7 +1097,7 @@ and record_functions name record_constr repr_name params fields_names fields_typ
in
let fields_convert_focus_unfocus = List.concat (List.map (fun i -> field_convert_focus_unfocus i) indices) in
let new_spec =
let _new_spec =
let new_name_spec = new_name ^ "_spec" in
let r = "R" in
let vr = coq_var r in
......@@ -1101,7 +1111,7 @@ and record_functions name record_constr repr_name params fields_names fields_typ
[ Coqtop_param (new_name_spec, spec);
register_spec new_name new_name_spec; ]
in
let get_set_spec i =
let _get_set_spec i =
let get_name = nth i get_names in
let set_name = nth i set_names in
let get_name_spec = get_name ^ "_spec" in
......@@ -1135,7 +1145,7 @@ and record_functions name record_constr repr_name params fields_names fields_typ
register_spec set_name set_name_spec; ]
in
let get_spec_focus i =
let _get_spec_focus i =
let get_name = nth i get_names in
let get_name_spec = get_name ^ "_spec_focus" in
let r = "R" in
......@@ -1155,7 +1165,7 @@ and record_functions name record_constr repr_name params fields_names fields_typ
coqtop_register "database_spec_focus" get_name get_name_spec; ]
in
let set_spec_unfocus i =
let _set_spec_unfocus i =
let set_name = nth i set_names in
let set_name_spec = set_name ^ "_spec_unfocus" in
let r = "R" in
......
......@@ -83,7 +83,6 @@ let exp_is_inlined_primitive e largs =
| _ -> false
end
| _ -> false
end
| _ -> false
......@@ -112,7 +111,6 @@ let is_lazy_binary_op e =
(* ** Normalization of patterns *)
let normalize_pattern p =
let loc = p.ppat_loc in
let i = ref (-1) in
let next_name () =
incr i; (pattern_generated_name !i) in
......@@ -163,7 +161,6 @@ let rec pattern_variables p =
| Ppat_unpack p1 -> unsupported loc "array unpack"
let rec values_variables e =
let loc = e.pexp_loc in
let aux = values_variables in
match e.pexp_desc with
| Pexp_ident (Lident x) -> [x]
......@@ -193,6 +190,14 @@ let rec values_variables e =
*)
(*#########################################################################*)
(* ** Auxiliary types *)
let get_unit_type ?(loc=Location.none) () =
{ ptyp_desc = Ptyp_constr (Lident "unit", []); ptyp_loc = loc }
(*#########################################################################*)
(* ** Normalization of expression *)
......@@ -238,7 +243,6 @@ let wrap_if_needed loc needs_wrapping new_name e b =
into [let f = fun .. -> .. in f], for a fresh name f. *)
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 () =
incr i; (variable_generated_name !i) in
......@@ -249,6 +253,8 @@ let normalize_expression ?is_named:(is_named=false) ?as_value:(as_value=false) e
let loc = e.pexp_loc in
let return edesc' =
{ e with pexp_desc = edesc' } in
let return_pat p =
{ ppat_loc = loc; ppat_desc = p } in
let mk_bool bvalue =
let svalue = if bvalue then "true" else "false" in
let explicit_arity = false in (* todo: what does it mean? *)
......@@ -315,15 +321,17 @@ let normalize_expression ?is_named:(is_named=false) ?as_value:(as_value=false) e
| Ppat_var x
| Ppat_constraint ({ ppat_desc = Ppat_var x}, _) ->
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, trans_func ms e']))
let px = return_pat (Ppat_var x) in
let tunit = get_unit_type ~loc:loc () in
let px_typ = return_pat (Ppat_constraint (px, tunit)) in
return (Pexp_function (lab, None, [px_typ, 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 px = return_pat (Ppat_var x) in
let vx = return (Pexp_ident (Lident x)) in
(* DEPRECATED let vx = { pexp_loc = loc; pexp_desc = Pexp_ident (Lident x) } *)
let ms' = (vx, p')::ms in
return (Pexp_function (lab, None, [px, trans_func ms' e']))
end
......@@ -401,8 +409,9 @@ let normalize_expression ?is_named:(is_named=false) ?as_value:(as_value=false) e
let e0',b0 =
if not is_naming_required then e0',b0 else begin
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 px = return_pat (Ppat_var x) in
let vx = return (Pexp_ident (Lident x)) in
(* DEPRECATED let vx = { pexp_loc = loc; pexp_desc = .. } *)
vx, b0@[px,e0']
end in
let e' = Pexp_match (e0', List.map protect_branch l') in
......@@ -451,19 +460,25 @@ let normalize_expression ?is_named:(is_named=false) ?as_value:(as_value=false) e
(* todo: tester: if then else fun x -> x *)
| Pexp_sequence (e1,e2) ->
let e1', b = aux e1 in
(* DEPRECATED: enforcement strict-sequence here a type annotation
let tunit = Some { ptyp_desc = Ptyp_constr (Lident "unit", []); ptyp_loc = loc } in
let e1'' = return (Pexp_constraint (e1', tunit, None)) in
wrap_as_value (return (Pexp_sequence (e1'', protect e2))) b
let e1' = return (Pexp_constraint (e1', tunit, None)) in *)
wrap_as_value (return (Pexp_sequence (e1', protect e2))) b
| Pexp_while (e1,e2) ->
wrap_as_value (return (Pexp_while (protect e1, protect e2))) []
| Pexp_for (s,e1,e2,d,e3) ->
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) ->
| Pexp_constraint (e,Some t1,None) ->
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 *)
return (Pexp_constraint (e',Some t1,None)), b
(* LATER: check if it is enough constraint e', when e' is just a variable
and everything happens inside b *)
| Pexp_constraint (e,_,Some t2) ->
unsupported loc "type annotation with a subtyping constraint"
| Pexp_constraint (e,None,None) ->
unsupported loc "type annotation without constraints"
| Pexp_when (econd,ebody) ->
let econd' = protect econd in
let ebody' = protect ebody in
......
......@@ -155,8 +155,7 @@ let rec string_of_expression par e =
let s = Format.sprintf "@[for %s = %s to %s do@ %s@ done@]" s (aux e1) (aux e2) (aux e3) in
show_par par s
| Pexp_constraint (e,to1,to2) ->
let s = Format.sprintf "@[(%s@ : _)@]" (aux e) in
show_par par s
Format.sprintf "@[(%s@ : _)@]" (aux e)
| Pexp_when (e1,e2) -> (*todo:better printing so that compiles *)
Format.sprintf "<< when %s >> %s" (aux e1) (aux e2)
| Pexp_send (_,_) -> unsupported_noloc "send expression"
......
......@@ -182,7 +182,8 @@ let rec string_of_expression par e =
| Texp_newtype (_,_) -> unsupported_noloc "newtype"
| Texp_pack _ -> unsupported_noloc "pack"
| Texp_open (_,_) -> unsupported_noloc "open"
| Texp_constraint (e,_,_) -> aux e
| Texp_constraint (e,_,_) ->
Format.sprintf "@[(%s@ : _)@]" (aux e)
(*#########################################################################*)
......
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