add change for typer.ml
This commit is contained in:
Pierre-Emmanuel Wulfman
parent
f657c71753
commit
e4e77da97c
@ -192,7 +192,7 @@ module Errors = struct
|
||||
error ~data title message ()
|
||||
|
||||
let not_supported_yet (message : string) (ae : I.expression) () =
|
||||
let title = (thunk "not suported yet") in
|
||||
let title = (thunk "not supported yet") in
|
||||
let message () = message in
|
||||
let data = [
|
||||
("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
|
||||
@ -201,7 +201,7 @@ module Errors = struct
|
||||
error ~data title message ()
|
||||
|
||||
let not_supported_yet_untranspile (message : string) (ae : O.expression) () =
|
||||
let title = (thunk "not suported yet") in
|
||||
let title = (thunk "not supported yet") in
|
||||
let message () = message in
|
||||
let data = [
|
||||
("expression" , fun () -> Format.asprintf "%a" O.PP.expression ae)
|
||||
@ -221,6 +221,7 @@ end
|
||||
|
||||
open Errors
|
||||
|
||||
let swap (a,b) = ok (b,a)
|
||||
let rec type_program (p:I.program) : O.program result =
|
||||
let aux (e, acc:(environment * O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
|
||||
let%bind ed' = (bind_map_location (type_declaration e)) d in
|
||||
@ -235,52 +236,55 @@ let rec type_program (p:I.program) : O.program result =
|
||||
bind_fold_list aux (Environment.full_empty, []) p in
|
||||
ok @@ List.rev lst
|
||||
|
||||
and type_declaration env : I.declaration -> (environment * O.declaration option) result = function
|
||||
(*
|
||||
Extract pairs of (name,type) in the declaration and add it to the environment
|
||||
*)
|
||||
let rec type_declaration env state : I.declaration -> (environment * Solver.state * O.declaration option) result = function
|
||||
| Declaration_type (type_name , type_expression) ->
|
||||
let%bind tv = evaluate_type env type_expression in
|
||||
let env' = Environment.add_type type_name tv env in
|
||||
ok (env', None)
|
||||
ok (env', state , None)
|
||||
| Declaration_constant (name , tv_opt , expression) -> (
|
||||
(*
|
||||
Determine the type of the expression and add it to the environment
|
||||
*)
|
||||
let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in
|
||||
let%bind ae' =
|
||||
let%bind (ae' , state') =
|
||||
trace (constant_declaration_error name expression tv'_opt) @@
|
||||
type_expression ?tv_opt:tv'_opt env expression in
|
||||
type_expression env state expression in
|
||||
let env' = Environment.add_ez_ae name ae' env in
|
||||
ok (env', Some (O.Declaration_constant ((make_n_e name ae') , (env , env'))))
|
||||
ok (env', state' , Some (O.Declaration_constant ((make_n_e name ae') , (env , env'))))
|
||||
)
|
||||
|
||||
and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> I.expression -> Location.t -> o O.matching result =
|
||||
fun f e t i ae loc -> match i with
|
||||
and type_match : environment -> Solver.state -> O.type_expression -> 'i I.matching -> I.expression -> Location.t -> (O.value O.matching * Solver.state) result =
|
||||
fun e state t i ae loc -> match i with
|
||||
| Match_bool {match_true ; match_false} ->
|
||||
let%bind _ =
|
||||
trace_strong (match_error ~expected:i ~actual:t loc)
|
||||
@@ get_t_bool t in
|
||||
let%bind match_true = f e match_true in
|
||||
let%bind match_false = f e match_false in
|
||||
ok (O.Match_bool {match_true ; match_false})
|
||||
let%bind (match_true , state') = type_expression e state match_true in
|
||||
let%bind (match_false , state'') = type_expression e state' match_false in
|
||||
ok (O.Match_bool {match_true ; match_false} , state'')
|
||||
| Match_option {match_none ; match_some} ->
|
||||
let%bind t_opt =
|
||||
trace_strong (match_error ~expected:i ~actual:t loc)
|
||||
@@ get_t_option t in
|
||||
let%bind match_none = f e match_none in
|
||||
let%bind (match_none , state') = type_expression e state match_none in
|
||||
let (n, b) = match_some in
|
||||
let n' = n, t_opt in
|
||||
let e' = Environment.add_ez_binder n t_opt e in
|
||||
let%bind b' = f e' b in
|
||||
ok (O.Match_option {match_none ; match_some = (n', b')})
|
||||
let%bind (b' , state'') = type_expression e' state' b in
|
||||
ok (O.Match_option {match_none ; match_some = (n', b')} , state'')
|
||||
| Match_list {match_nil ; match_cons} ->
|
||||
let%bind t_list =
|
||||
trace_strong (match_error ~expected:i ~actual:t loc)
|
||||
@@ get_t_list t in
|
||||
let%bind match_nil = f e match_nil in
|
||||
let%bind (match_nil , state') = type_expression e state match_nil in
|
||||
let (hd, tl, b) = match_cons in
|
||||
let e' = Environment.add_ez_binder hd t_list e in
|
||||
let e' = Environment.add_ez_binder tl t e' in
|
||||
let%bind b' = f e' b in
|
||||
ok (O.Match_list {match_nil ; match_cons = (((hd , t_list), (tl , t)), b')})
|
||||
let%bind (b' , state'') = type_expression e' state' b in
|
||||
ok (O.Match_list {match_nil ; match_cons = (hd, tl, b')} , state'')
|
||||
| Match_tuple (lst, b) ->
|
||||
let%bind t_tuple =
|
||||
trace_strong (match_error ~expected:i ~actual:t loc)
|
||||
@ -290,8 +294,8 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
|
||||
@@ (fun () -> List.combine lst t_tuple) in
|
||||
let aux prev (name, tv) = Environment.add_ez_binder name tv prev in
|
||||
let e' = List.fold_left aux e lst' in
|
||||
let%bind b' = f e' b in
|
||||
ok (O.Match_tuple (lst, b'))
|
||||
let%bind (b' , state') = type_expression e' state b in
|
||||
ok (O.Match_tuple (lst, b') , state')
|
||||
| Match_variant lst ->
|
||||
let%bind variant_opt =
|
||||
let aux acc ((constructor_name , _) , _) =
|
||||
@ -334,17 +338,17 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
|
||||
Assert.assert_true List.(length variant_cases = length match_cases) in
|
||||
ok ()
|
||||
in
|
||||
let%bind lst' =
|
||||
let aux ((constructor_name , name) , b) =
|
||||
let%bind (state'' , lst') =
|
||||
let aux state ((constructor_name , name) , b) =
|
||||
let%bind (constructor , _) =
|
||||
trace_option (unbound_constructor e constructor_name loc) @@
|
||||
Environment.get_constructor constructor_name e in
|
||||
let e' = Environment.add_ez_binder name constructor e in
|
||||
let%bind b' = f e' b in
|
||||
ok ((constructor_name , name) , b')
|
||||
let%bind (b' , state') = type_expression e' state b in
|
||||
ok (state' , ((constructor_name , name) , b'))
|
||||
in
|
||||
bind_map_list aux lst in
|
||||
ok (O.Match_variant (lst' , variant))
|
||||
bind_fold_map_list aux state lst in
|
||||
ok (O.Match_variant (lst' , variant) , state'')
|
||||
|
||||
(*
|
||||
Recursively search the type_expression and return a result containing the
|
||||
@ -385,31 +389,47 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
|
||||
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
|
||||
return (T_constant(cst, lst'))
|
||||
|
||||
and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.annotated_expression result = fun e ?tv_opt ae ->
|
||||
and type_expression : environment -> Solver.state -> I.expression -> (O.annotated_expression * Solver.state) result = fun e state ae ->
|
||||
let open Solver in
|
||||
let module L = Logger.Stateful() in
|
||||
let return expr tv =
|
||||
let%bind () =
|
||||
match tv_opt with
|
||||
| None -> ok ()
|
||||
| Some tv' -> O.assert_type_value_eq (tv' , tv) in
|
||||
let return : _ -> Solver.state -> _ -> _ (* return of type_expression *) = fun expr state constraints type_name ->
|
||||
let%bind new_state = aggregate_constraints state constraints in
|
||||
let tv = t_variable type_name () in
|
||||
let location = ae.location in
|
||||
ok @@ make_a_e ~location expr tv e in
|
||||
let expr' = make_a_e ~location expr tv e in
|
||||
ok @@ (expr' , new_state) in
|
||||
let return_wrapped expr state (constraints , expr_type) = return expr state constraints expr_type in
|
||||
let main_error =
|
||||
let title () = "typing expression" in
|
||||
let content () = "" in
|
||||
let data = [
|
||||
("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp ae.location) ;
|
||||
("location" , fun () -> Format.asprintf "%a" Location.pp @@ ae.location) ;
|
||||
("misc" , fun () -> L.get ()) ;
|
||||
] in
|
||||
error ~data title content in
|
||||
trace main_error @@
|
||||
match ae.expression with
|
||||
match ae.expression' with
|
||||
|
||||
(* TODO: this file should take care only of the order in which program fragments
|
||||
are translated by Wrap.xyz
|
||||
|
||||
TODO: produce an ordered list of sub-fragments, and use a common piece of code
|
||||
to actually perform the recursive calls *)
|
||||
|
||||
(* Basic *)
|
||||
| E_failwith expr -> (
|
||||
let%bind (expr', state') = type_expression e state expr in
|
||||
let (constraints , expr_type) = Wrap.failwith () in
|
||||
let expr'' = e_failwith expr' in
|
||||
return expr'' state' constraints expr_type
|
||||
)
|
||||
| E_variable name ->
|
||||
let%bind tv' =
|
||||
trace_option (unbound_variable e name ae.location)
|
||||
@@ Environment.get_opt name e in
|
||||
let (constraints , expr_type) = Wrap.variable name tv'.type_expression in
|
||||
let expr' = e_variable name in
|
||||
return (E_variable name) tv'.type_value
|
||||
| E_literal (Literal_bool b) ->
|
||||
return (E_literal (Literal_bool b)) (t_bool ())
|
||||
@ -433,7 +453,8 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
|
||||
return (e_operation op) (t_operation ())
|
||||
(* Tuple *)
|
||||
| E_tuple lst ->
|
||||
let%bind lst' = bind_list @@ List.map (type_expression e) lst in
|
||||
let aux state hd = type_expression e state hd >>? swap in
|
||||
let%bind (state', lst') = bind_fold_map_list aux state lst in
|
||||
let tv_lst = List.map get_type_annotation lst' in
|
||||
return (E_tuple lst') (t_tuple tv_lst ())
|
||||
| E_accessor (ae', path) ->
|
||||
@ -476,17 +497,19 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
|
||||
error title content in
|
||||
trace_option error @@
|
||||
Environment.get_constructor c e in
|
||||
let%bind expr' = type_expression e expr in
|
||||
let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in
|
||||
return (E_constructor (c , expr')) sum_tv
|
||||
let%bind (expr' , state') = type_expression e state expr in
|
||||
let%bind _assert = O.assert_type_expression_eq (expr'.type_annotation, c_tv) in
|
||||
let wrapped = Wrap.constructor expr'.type_annotation c_tv sum_tv in
|
||||
return_wrapped (E_constructor (c , expr')) state' wrapped
|
||||
(* Record *)
|
||||
| E_record m ->
|
||||
let aux prev k expr =
|
||||
let%bind expr' = type_expression e expr in
|
||||
ok (SMap.add k expr' prev)
|
||||
let aux (acc, state) k expr =
|
||||
let%bind (expr' , state') = type_expression e state expr in
|
||||
ok (SMap.add k expr' acc , state')
|
||||
in
|
||||
let%bind m' = bind_fold_smap aux (ok SMap.empty) m in
|
||||
return (E_record m') (t_record (SMap.map get_type_annotation m') ())
|
||||
let%bind (m' , state') = bind_fold_smap aux (ok (SMap.empty , state)) m in
|
||||
let wrapped = Wrap.record (SMap.map get_type_annotation m') in
|
||||
return_wrapped (E_record m') state' wrapped
|
||||
(* Data-structure *)
|
||||
| E_list lst ->
|
||||
let%bind lst' = bind_map_list (type_expression e) lst in
|
||||
@ -632,20 +655,10 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
|
||||
type_constant name tv_lst tv_opt ae.location in
|
||||
return (E_constant (name' , lst')) tv
|
||||
| E_application (f, arg) ->
|
||||
let%bind f' = type_expression e f in
|
||||
let%bind arg = type_expression e arg in
|
||||
let%bind tv = match f'.type_annotation.type_value' with
|
||||
| T_function (param, result) ->
|
||||
let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in
|
||||
ok result
|
||||
| _ ->
|
||||
fail @@ type_error_approximate
|
||||
~expected:"should be a function type"
|
||||
~expression:f
|
||||
~actual:f'.type_annotation
|
||||
f'.location
|
||||
in
|
||||
return (E_application (f' , arg)) tv
|
||||
let%bind (f' , state') = type_expression e state f in
|
||||
let%bind (arg , state'') = type_expression e state' arg in
|
||||
let wrapped = Wrap.application f'.type_annotation arg.type_annotation in
|
||||
return_wrapped (E_application (f' , arg)) state'' wrapped
|
||||
| E_look_up dsi ->
|
||||
let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in
|
||||
let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) ds.type_annotation in
|
||||
@ -677,40 +690,24 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
|
||||
return (O.E_matching (ex', m')) tv
|
||||
)
|
||||
| E_sequence (a , b) ->
|
||||
let%bind a' = type_expression e a in
|
||||
let%bind b' = type_expression e b in
|
||||
let a'_type_annot = get_type_annotation a' in
|
||||
let%bind () =
|
||||
trace_strong (type_error
|
||||
~msg:"first part of the sequence should be of unit type"
|
||||
~expected:(O.t_unit ())
|
||||
~actual:a'_type_annot
|
||||
~expression:a
|
||||
a'.location) @@
|
||||
Ast_typed.assert_type_value_eq (t_unit () , a'_type_annot) in
|
||||
return (O.E_sequence (a' , b')) (get_type_annotation b')
|
||||
let%bind (a' , state') = type_expression e state a in
|
||||
let%bind (b' , state'') = type_expression e state' b in
|
||||
let wrapped = Wrap.sequence a'.type_annotation b'.type_annotation in
|
||||
return_wrapped (O.E_sequence (a' , b')) state'' wrapped
|
||||
| E_loop (expr , body) ->
|
||||
let%bind expr' = type_expression e expr in
|
||||
let%bind body' = type_expression e body in
|
||||
let t_expr' = get_type_annotation expr' in
|
||||
let%bind () =
|
||||
trace_strong (type_error
|
||||
~msg:"while condition isn't of type bool"
|
||||
~expected:(O.t_bool ())
|
||||
~actual:t_expr'
|
||||
~expression:expr
|
||||
expr'.location) @@
|
||||
Ast_typed.assert_type_value_eq (t_bool () , t_expr') in
|
||||
let t_body' = get_type_annotation body' in
|
||||
let%bind () =
|
||||
trace_strong (type_error
|
||||
~msg:"while body isn't of unit type"
|
||||
~expected:(O.t_unit ())
|
||||
~actual:t_body'
|
||||
~expression:body
|
||||
body'.location) @@
|
||||
Ast_typed.assert_type_value_eq (t_unit () , t_body') in
|
||||
return (O.E_loop (expr' , body')) (t_unit ())
|
||||
let%bind (expr' , state') = type_expression e state expr in
|
||||
let%bind (body' , state'') = type_expression e state' body in
|
||||
let wrapped = Wrap.loop expr'.type_annotation body'.type_annotation in
|
||||
return_wrapped (O.E_loop (expr' , body')) state'' wrapped
|
||||
| E_let_in {binder ; rhs ; result} ->
|
||||
let%bind rhs_tv_opt = bind_map_option (evaluate_type e) (snd binder) in
|
||||
(* TODO: the binder annotation should just be an annotation node *)
|
||||
let%bind (rhs , state') = type_expression e state rhs in
|
||||
let e' = Environment.add_ez_declaration (fst binder) rhs e in
|
||||
let%bind (result , state'') = type_expression e' state' result in
|
||||
let wrapped =
|
||||
Wrap.let_in rhs.type_annotation rhs_tv_opt result.type_annotation in
|
||||
return_wrapped (E_let_in {binder = fst binder; rhs; result}) state'' wrapped
|
||||
| E_assign (name , path , expr) ->
|
||||
let%bind typed_name =
|
||||
let%bind ele = Environment.get_trace name e in
|
||||
@ -735,34 +732,103 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
|
||||
| Access_map _ ->
|
||||
fail @@ not_supported_yet "assign expressions with maps are not supported yet" ae
|
||||
in
|
||||
bind_fold_list aux (typed_name.type_value , []) path in
|
||||
let%bind expr' = type_expression e expr in
|
||||
let t_expr' = get_type_annotation expr' in
|
||||
let%bind () =
|
||||
trace_strong (type_error
|
||||
~msg:"type of the expression to assign doesn't match left-hand-side"
|
||||
~expected:assign_tv
|
||||
~actual:t_expr'
|
||||
~expression:expr
|
||||
expr'.location) @@
|
||||
Ast_typed.assert_type_value_eq (assign_tv , t_expr') in
|
||||
return (O.E_assign (typed_name , path' , expr')) (t_unit ())
|
||||
| E_let_in {binder ; rhs ; result} ->
|
||||
let%bind rhs_tv_opt = bind_map_option (evaluate_type e) (snd binder) in
|
||||
let%bind rhs = type_expression ?tv_opt:rhs_tv_opt e rhs in
|
||||
let e' = Environment.add_ez_declaration (fst binder) rhs e in
|
||||
let%bind result = type_expression e' result in
|
||||
return (E_let_in {binder = fst binder; rhs; result}) result.type_annotation
|
||||
bind_fold_list aux (typed_name.type_expression , []) path in
|
||||
let%bind (expr' , state') = type_expression e state expr in
|
||||
let wrapped = Wrap.assign assign_tv expr'.type_annotation in
|
||||
return_wrapped (O.E_assign (typed_name , path' , expr')) state' wrapped
|
||||
| E_annotation (expr , te) ->
|
||||
let%bind tv = evaluate_type e te in
|
||||
let%bind expr' = type_expression ~tv_opt:tv e expr in
|
||||
let%bind type_annotation =
|
||||
O.merge_annotation
|
||||
(Some tv)
|
||||
(Some expr'.type_annotation)
|
||||
(internal_assertion_failure "merge_annotations (Some ...) (Some ...) failed") in
|
||||
ok {expr' with type_annotation}
|
||||
let%bind (expr' , state') = type_expression e state expr in
|
||||
let wrapped = Wrap.annotation expr'.type_annotation tv
|
||||
(* TODO: we're probably discarding too much by using expr'.expression.
|
||||
Previously: {expr' with type_annotation = the_explicit_type_annotation}
|
||||
but then this case is not like the others and doesn't call return_wrapped,
|
||||
which might do some necessary work *)
|
||||
in return_wrapped expr'.expression state' wrapped
|
||||
|
||||
| E_matching (ex, m) -> (
|
||||
let%bind (ex' , state') = type_expression e state ex in
|
||||
let%bind (m' , state'') = type_match e state' ex'.type_annotation m ae ae.location in
|
||||
let tvs =
|
||||
let aux (cur:O.value O.matching) =
|
||||
match cur with
|
||||
| Match_bool { match_true ; match_false } -> [ match_true ; match_false ]
|
||||
| Match_list { match_nil ; match_cons = (_ , _ , match_cons) } -> [ match_nil ; match_cons ]
|
||||
| Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ]
|
||||
| Match_tuple (_ , match_tuple) -> [ match_tuple ]
|
||||
| Match_variant (lst , _) -> List.map snd lst in
|
||||
List.map get_type_annotation @@ aux m' in
|
||||
let%bind () = match tvs with
|
||||
[] -> fail @@ match_empty_variant m ae.location
|
||||
| _ -> ok () in
|
||||
(* constraints:
|
||||
all the items of tvs should be equal to the first one
|
||||
result = first item of tvs
|
||||
*)
|
||||
let wrapped = Wrap.matching tvs in
|
||||
return_wrapped (O.E_matching (ex', m')) state'' wrapped
|
||||
)
|
||||
|
||||
(* match m with *)
|
||||
(* Special case for assert-like failwiths. TODO: CLEAN THIS. *)
|
||||
(* | I.Match_bool { match_false ; match_true } when I.is_e_failwith match_true -> ( *)
|
||||
(* let%bind fw = I.get_e_failwith match_true in *)
|
||||
(* let%bind fw' = type_expression e fw in *)
|
||||
(* let%bind mf' = type_expression e match_false in *)
|
||||
(* let t = get_type_annotation ex' in *)
|
||||
(* let%bind () = *)
|
||||
(* trace_strong (match_error ~expected:m ~actual:t ae.location) *)
|
||||
(* @@ assert_t_bool t in *)
|
||||
(* let%bind () = *)
|
||||
(* trace_strong (match_error *)
|
||||
(* ~msg:"matching not-unit on an assert" *)
|
||||
(* ~expected:m *)
|
||||
(* ~actual:t *)
|
||||
(* ae.location) *)
|
||||
(* @@ assert_t_unit (get_type_annotation mf') in *)
|
||||
(* let mt' = make_a_e *)
|
||||
(* (E_constant ("ASSERT_INFERRED" , [ex' ; fw'])) *)
|
||||
(* (t_unit ()) *)
|
||||
(* e *)
|
||||
(* in *)
|
||||
(* let m' = O.Match_bool { match_true = mt' ; match_false = mf' } in *)
|
||||
(* return (O.E_matching (ex' , m')) (t_unit ()) *)
|
||||
(* ) *)
|
||||
(* | _ -> ( … ) *)
|
||||
|
||||
|
||||
| E_lambda {
|
||||
binder ;
|
||||
input_type ;
|
||||
output_type ;
|
||||
result ;
|
||||
} -> (
|
||||
let%bind input_type' = bind_map_option (evaluate_type e) input_type in
|
||||
let%bind output_type' = bind_map_option (evaluate_type e) output_type in
|
||||
|
||||
let fresh : O.type_expression = t_variable (Wrap.fresh_binder ()) () in
|
||||
let e' = Environment.add_ez_binder (fst binder) fresh e in
|
||||
|
||||
let%bind (result , state') = type_expression e' state result in
|
||||
let output_type = result.type_annotation in
|
||||
let wrapped = Wrap.lambda fresh input_type' output_type' in
|
||||
return_wrapped
|
||||
(E_lambda {binder = fst binder;input_type=fresh;output_type;result})
|
||||
state' wrapped
|
||||
)
|
||||
|
||||
| E_constant (name, lst) ->
|
||||
let () = ignore (name , lst) in
|
||||
Pervasives.failwith "TODO: E_constant"
|
||||
(*
|
||||
let%bind lst' = bind_list @@ List.map (type_expression e) lst in
|
||||
let tv_lst = List.map get_type_annotation lst' in
|
||||
let%bind (name', tv) =
|
||||
type_constant name tv_lst tv_opt ae.location in
|
||||
return (E_constant (name' , lst')) tv
|
||||
*)
|
||||
|
||||
(* Advanced *)
|
||||
|
||||
and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) (loc : Location.t) : (string * O.type_value) result =
|
||||
(* Constant poorman's polymorphism *)
|
||||
@ -777,7 +843,76 @@ let untype_type_value (t:O.type_value) : (I.type_expression) result =
|
||||
match t.simplified with
|
||||
| Some s -> ok s
|
||||
| _ -> fail @@ internal_assertion_failure "trying to untype generated type"
|
||||
(* let type_statement : environment -> I.declaration -> Solver.state -> (environment * O.declaration * Solver.state) result = fun env declaration state -> *)
|
||||
(* match declaration with *)
|
||||
(* | I.Declaration_type td -> ( *)
|
||||
(* let%bind (env', state', declaration') = type_declaration env state td in *)
|
||||
(* let%bind toto = Solver.aggregate_constraints state' constraints in *)
|
||||
(* let declaration' = match declaration' with None -> Pervasives.failwith "TODO" | Some x -> x in *)
|
||||
(* ok (env' , declaration' , toto) *)
|
||||
(* ) *)
|
||||
(* | I.Declaration_constant ((_ , _ , expr) as cd) -> ( *)
|
||||
(* let%bind state' = type_expression expr in *)
|
||||
(* let constraints = constant_declaration cd in *)
|
||||
(* Solver.aggregate_constraints state' constraints *)
|
||||
(* ) *)
|
||||
|
||||
(* TODO: we ended up with two versions of type_program… ??? *)
|
||||
|
||||
(*
|
||||
Apply type_declaration on all the node of the AST_simplified from the root p
|
||||
*)
|
||||
let type_program (p:I.program) : (environment * Solver.state * O.program) result =
|
||||
let env = Ast_typed.Environment.full_empty in
|
||||
let state = Solver.initial_state in
|
||||
let aux ((e : environment), (s : Solver.state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
|
||||
let%bind (e' , s' , d'_opt) = type_declaration e s (Location.unwrap d) in
|
||||
let ds' = match d'_opt with
|
||||
| None -> ds
|
||||
| Some d' -> ds @ [Location.wrap ~loc:(Location.get_location d) d'] (* take O(n) insted of O(1) *)
|
||||
in
|
||||
ok (e' , s' , ds')
|
||||
in
|
||||
let%bind (env' , state' , declarations) =
|
||||
trace (fun () -> program_error p ()) @@
|
||||
bind_fold_list aux (env , state , []) p in
|
||||
let () = ignore (env' , state') in
|
||||
ok (env', state', declarations)
|
||||
|
||||
(*
|
||||
Similar to type_program but use a fold_map_list and List.fold_left and add element to the left or the list which gives a better complexity
|
||||
*)
|
||||
let type_program' : I.program -> O.program result = fun p ->
|
||||
let initial_state = Solver.initial_state in
|
||||
let initial_env = Environment.full_empty in
|
||||
let aux (env, state) (statement : I.declaration Location.wrap) =
|
||||
let statement' = statement.wrap_content in (* TODO *)
|
||||
let%bind (env' , state' , declaration') = type_declaration env state statement' in
|
||||
let declaration'' = match declaration' with
|
||||
None -> None
|
||||
| Some x -> Some (Location.wrap ~loc:Location.(statement.location) x) in
|
||||
ok ((env' , state') , declaration'')
|
||||
in
|
||||
let%bind ((env' , state') , p') = bind_fold_map_list aux (initial_env, initial_state) p in
|
||||
let p' = List.fold_left (fun l e -> match e with None -> l | Some x -> x :: l) [] p' in
|
||||
|
||||
(* here, maybe ensure that there are no invalid things in env' and state' ? *)
|
||||
let () = ignore (env' , state') in
|
||||
ok p'
|
||||
|
||||
(*
|
||||
Tranform a Ast_typed type_expression into an ast_simplified type_expression
|
||||
*)
|
||||
let untype_type_expression (t:O.type_expression) : (I.type_expression) result =
|
||||
ok t
|
||||
(* match t.simplified with *)
|
||||
(* | Some s -> ok s *)
|
||||
(* | _ -> fail @@ internal_assertion_failure "trying to untype generated type" *)
|
||||
|
||||
|
||||
(*
|
||||
Tranform a Ast_typed literal into an ast_simplified literal
|
||||
*)
|
||||
let untype_literal (l:O.literal) : I.literal result =
|
||||
let open I in
|
||||
match l with
|
||||
@ -853,6 +988,9 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
|
||||
let%bind ae' = untype_expression ae in
|
||||
let%bind m' = untype_matching untype_expression m in
|
||||
return (e_matching ae' m')
|
||||
| E_failwith ae ->
|
||||
let%bind ae' = untype_expression ae in
|
||||
return (e_failwith ae')
|
||||
| E_sequence _
|
||||
| E_loop _
|
||||
| E_assign _ -> fail @@ not_supported_yet_untranspile "not possible to untranspile statements yet" e.expression
|
||||
|
||||
Loading…
Reference in New Issue
Block a user