diff options
| -rw-r--r-- | src/ocaml_backend.ml | 124 |
1 files changed, 65 insertions, 59 deletions
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 894d028f..a5f0653b 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -456,70 +456,76 @@ let ocaml_funcls ctx = function | [] -> failwith "Ocaml: empty function" | [FCL_aux (FCL_Funcl (id, pexp),_)] -> - let arg_typs, ret_typ = - match Bindings.find id ctx.val_specs with - | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ) - | _ -> failwith "Found val spec which was not a function!" - in - (* Any remaining type variables after simple_typ rewrite should - indicate Type-polymorphism. If we have it, we need to generate - explicit type signatures with universal quantification. *) - let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in - let pat_sym = gensym () in - let pat, exp = - match pexp with - | Pat_aux (Pat_exp (pat, exp),_) -> pat,exp - | Pat_aux (Pat_when (pat, wh, exp),_) -> failwith "OCaml: top-level pattern guards not supported" - in - let annot_pat = - let pat = + if Bindings.mem id ctx.externs + then string ("(* Omitting externed function " ^ string_of_id id ^ " *)") ^^ hardline + else + let arg_typs, ret_typ = + match Bindings.find id ctx.val_specs with + | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ) + | _ -> failwith "Found val spec which was not a function!" + in + (* Any remaining type variables after simple_typ rewrite should + ind icate Type-polymorphism. If we have it, we need to generate + explic it type signatures with universal quantification. *) + let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in + let pat_sym = gensym () in + let pat, exp = + match pexp with + | Pat_aux (Pat_exp (pat, exp),_) -> pat,exp + | Pat_aux (Pat_when (pat, wh, exp),_) -> failwith "OCaml: top-level pattern guards not supported" + in + let annot_pat = + let pat = + if KidSet.is_empty kids then + parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))) + else + ocaml_pat ctx pat + in + if !opt_trace_ocaml + then parens (separate space [pat; string "as"; pat_sym]) + else pat + in + let call_header = function_header () in + let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in + let call = if KidSet.is_empty kids then - parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))) + separate space [call_header; zencode ctx id; + annot_pat; colon; ocaml_typ ctx ret_typ; equals; + sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] + ^//^ ocaml_exp ctx exp + ^^ rparen else - ocaml_pat ctx pat + separate space [call_header; zencode ctx id; colon; + separate space (List.map zencode_kid (KidSet.elements kids)) ^^ dot; + ocaml_typ ctx (mk_typ (Typ_tup arg_typs)); string "->"; ocaml_typ ctx ret_typ; equals; + string "fun"; annot_pat; string "->"; + sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] + ^//^ ocaml_exp ctx exp + ^^ rparen in - if !opt_trace_ocaml - then parens (separate space [pat; string "as"; pat_sym]) - else pat - in - let call_header = function_header () in - let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in - let call = - if KidSet.is_empty kids then - separate space [call_header; zencode ctx id; - annot_pat; colon; ocaml_typ ctx ret_typ; equals; - sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] - ^//^ ocaml_exp ctx exp - ^^ rparen - else - separate space [call_header; zencode ctx id; colon; - separate space (List.map zencode_kid (KidSet.elements kids)) ^^ dot; - ocaml_typ ctx (mk_typ (Typ_tup arg_typs)); string "->"; ocaml_typ ctx ret_typ; equals; - string "fun"; annot_pat; string "->"; - sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] - ^//^ ocaml_exp ctx exp - ^^ rparen - in - ocaml_funcl call string_of_arg string_of_ret + ocaml_funcl call string_of_arg string_of_ret | funcls -> let id = funcls_id funcls in - let arg_typs, ret_typ = - match Bindings.find id ctx.val_specs with - | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ) - | _ -> failwith "Found val spec which was not a function!" - in - let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in - if not (KidSet.is_empty kids) then failwith "Cannot handle polymorphic multi-clause function in OCaml backend" else (); - let pat_sym = gensym () in - let call_header = function_header () in - let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in - let call = - separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))); equals; - sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] - ^//^ (separate space [string "match"; pat_sym; string "with"] ^^ hardline ^^ ocaml_funcl_matches ctx funcls) - ^^ rparen - in - ocaml_funcl call string_of_arg string_of_ret + if Bindings.mem id ctx.externs + then string ("(* Omitting externed function " ^ string_of_id id ^ " *)") ^^ hardline + else + let arg_typs, ret_typ = + match Bindings.find id ctx.val_specs with + | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ) + | _ -> failwith "Found val spec which was not a function!" + in + let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in + if not (KidSet.is_empty kids) then failwith "Cannot handle polymorphic multi-clause function in OCaml backend" else (); + let pat_sym = gensym () in + let call_header = function_header () in + let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in + let call = + separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))); equals; + sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] + ^//^ (separate space [string "match"; pat_sym; string "with"] ^^ hardline ^^ ocaml_funcl_matches ctx funcls) + ^^ rparen + in + ocaml_funcl call string_of_arg string_of_ret let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) = ocaml_funcls ctx funcls |