Commit aa48cc37 authored by Gabriel Scherer's avatar Gabriel Scherer
Browse files

minor fixes

parent e6953c62
Pipeline #259302 passed with stage
in 8 minutes and 24 seconds
......@@ -2,14 +2,15 @@
(* We translate from System F to P and then print the P term (resp. type). *)
let new_tyvar () =
let new_tyvar =
let id = ref 0 in
"x" ^ (string_of_int @@ Inferno.Utils.postincrement id)
fun () ->
"a" ^ (string_of_int @@ Inferno.Utils.postincrement id)
let translate_tyvar env x =
List.nth env x
List.assoc x env
let rec translate_type (env : P.tyvar list) (ty : F.nominal_type) : P.typ =
let rec translate_type (env : (F.tyvar * P.tyvar) list) (ty : F.nominal_type) : P.typ =
let self = translate_type in
match ty with
| F.TyVar x ->
......@@ -21,9 +22,11 @@ let rec translate_type (env : P.tyvar list) (ty : F.nominal_type) : P.typ =
| F.TySum tys ->
P.TySum (List.map (self env) tys)
| F.TyForall (x, ty) ->
P.TyForall (translate_tyvar env x, self (new_tyvar () :: env) ty)
let alpha = new_tyvar () in
P.TyForall (alpha, self ((x, alpha) :: env) ty)
| F.TyMu (x, ty) ->
P.TyMu (translate_tyvar env x, self (new_tyvar () :: env) ty)
let alpha = new_tyvar () in
P.TyMu (alpha, self ((x, alpha) :: env) ty)
| F.TyConstr (constr, tys) ->
P.TyConstr (constr, List.map (self env) tys)
......@@ -45,7 +48,8 @@ let rec translate_term env (t : F.nominal_term) : P.term =
| F.Let (x, t, u) ->
P.Let (P.PVar x, self env t, self env u)
| F.TyAbs (x, t) ->
P.TyAbs (translate_tyvar env x, self (new_tyvar () :: env) t)
let alpha = new_tyvar () in
P.TyAbs (alpha, self ((x, alpha) :: env) t)
| F.TyApp (t, ty) ->
P.TyApp (self env t, translate_type env ty)
| F.Tuple ts ->
......
......@@ -12,12 +12,12 @@ let test_with_log ~log (env : F.nominal_datatype_env) (t : F.nominal_term) =
let t : F.debruijn_term =
Log.attempt log
"Converting the System F term to de Bruijn style...\n"
F.Term.translate t
(fun () -> F.Term.translate t)
in
let _ty : F.debruijn_type =
Log.attempt log
"Type-checking the System F term...\n"
FTypeChecker.typeof env t
(fun () -> FTypeChecker.typeof env t)
in
()
......
......@@ -44,7 +44,7 @@ let test_with_log ~log (env : ML.datatype_env) (t : ML.term) : bool =
let outcome =
Log.attempt log
"Type inference and translation to System F...\n"
translate env t
(fun () -> translate env t)
in
match outcome with
| None ->
......
......@@ -28,10 +28,10 @@ let print_log log =
flush stdout
) (List.rev log.actions)
let attempt log msg f x =
let attempt log msg f =
log_msg log msg;
try
f x
f ()
with e ->
print_log log;
Printf.printf "%s\n" (Printexc.to_string e);
......
......@@ -2,6 +2,9 @@ open Client
(* A few manually constructed terms. *)
let hole =
ML.Hole []
let x =
ML.Var "x"
......@@ -193,6 +196,8 @@ let test =
Test.(Log.with_log CheckML.test_with_log)
let () =
assert (test Datatype.Env.empty hole);
assert (test Datatype.Env.empty id);
assert (test Datatype.Env.empty idid);
assert (test Datatype.Env.empty genid);
assert (test Datatype.Env.empty genidid);
......
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