Commit f892e094 authored by charguer's avatar charguer

generation

parent 450e1b90
......@@ -22,6 +22,12 @@ 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
- in print_tast and print_past, protect with parenth the infix names being bound
......@@ -38,7 +44,7 @@ LATER
- make systematic use of || (rm -f $@; exit 1) in cfml calls
- currently type annotations in pattern get lost
DEPRECATED?
......
......@@ -220,9 +220,18 @@ let top_val_poly_list = []
let top_val_poly_list_pair = ([],[])
(* TODO
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)
let (top_val_pair_fun_1,top_val_pair_fun_2) =
((fun () -> 1), (fun () -> 1))
*)
(* problematic generalization
let (top_val_pair_fun_1,top_val_pair_fun_2) =
((fun x -> x), (fun x -> x))
*)
(********************************************************************)
......@@ -411,7 +420,7 @@ let order_array () =
(* ** Arrays *)
let array_ops () =
let u = [||] in
(* TODO let u = ([||] : int array) in *)
let t = Array.make 3 0 in
let _x = t.(1) in
t.(2) <- 4;
......
......@@ -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
......
......@@ -759,7 +759,7 @@ let rec cfg_exp env e =
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
let func = Coq_var "STDLIB.Array_ml.make_empty" in
Cf_app ([ts], tr, func, [arg])
| Texp_field (arg, p, lbl) ->
......
......@@ -268,7 +268,7 @@ let normalize_expression ?is_named:(is_named=false) ?as_value:(as_value=false) e
| 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 l' = List.map (protect_branch ~is_named:true) l in
let eb' = protect eb in
let e' = Pexp_let (Recursive, l', eb') in
wrap_as_value (return e') []
......@@ -284,7 +284,7 @@ let normalize_expression ?is_named:(is_named=false) ?as_value:(as_value=false) e
wrap_as_value e' []
| _ ->
(* [let p1 = e1 in e2] is viewed as [match e1 with p1 -> e2] *)
let e1',b1 = aux ~as_value:true e1 in
let e1',b1 = aux ~is_named:true ~as_value:true e1 in
let e' = create_let loc b1 (
create_match_one loc e1' (normalize_pattern p1) (protect e2)) in
wrap_as_value e' []
......@@ -330,7 +330,7 @@ let normalize_expression ?is_named:(is_named=false) ?as_value:(as_value=false) e
| _ ->
let addmatch eacc (vi,pi) =
return (Pexp_match (vi, [pi,eacc])) in
List.fold_left addmatch (protect e) ms
List.fold_left addmatch (protect ~is_named:is_named 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) []
......@@ -495,8 +495,9 @@ let normalize_expression ?is_named:(is_named=false) ?as_value:(as_value=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 e)
and protect_branch ?is_named:(is_named=false) (p,e) =
(normalize_pattern p,
protect ~is_named:is_named e)
in
protect ~is_named:true e
......
......@@ -137,7 +137,8 @@ let rec string_of_expression par e =
| Pexp_setfield (e,i,e2) ->
let s = Format.sprintf "@[%s.%s <- %s@]" (aux e) (string_of_lident i) (aux e2) in
show_par par s
| Pexp_array l -> unsupported_noloc "array expression" (* Pexp_array (List.map aux l)*)
| Pexp_array l ->
Format.sprintf "[| %s |]" (show_list aux "; " l)
| Pexp_ifthenelse (e1, e2, None) ->
let s = Format.sprintf "@[if %s@ then %s@]" (aux e1) (aux e2) in
show_par par s
......
......@@ -144,7 +144,8 @@ let rec string_of_expression par e =
| Texp_setfield (e,p,i,e2) ->
let s = Format.sprintf "@[%s.%s <- %s@]" (aux e) (string_of_path p) (aux e2) in
show_par par s
| Texp_array l -> unsupported_noloc "array expression" (* Texp_array (List.map aux l)*)
| Texp_array l ->
Format.sprintf "[| %s |]" (show_list aux "; " l)
| Texp_ifthenelse (e1, e2, None) ->
let s = Format.sprintf "@[if %s@ then %s@]" (aux e1) (aux e2) in
show_par par s
......
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