tmp
This commit is contained in:
parent
1918bc00d1
commit
a9f88e3ddf
@ -31,7 +31,7 @@ and named_type_expression = {
|
|||||||
and te = type_expression
|
and te = type_expression
|
||||||
and ae = annotated_expression
|
and ae = annotated_expression
|
||||||
and te_map = type_expression type_name_map
|
and te_map = type_expression type_name_map
|
||||||
and e_map = expression name_map
|
and ae_map = annotated_expression name_map
|
||||||
|
|
||||||
and type_expression =
|
and type_expression =
|
||||||
| Type_tuple of te list
|
| Type_tuple of te list
|
||||||
@ -41,17 +41,25 @@ and type_expression =
|
|||||||
| Type_constant of type_name * te list
|
| Type_constant of type_name * te list
|
||||||
|
|
||||||
and expression =
|
and expression =
|
||||||
|
(* Base *)
|
||||||
| Literal of literal
|
| Literal of literal
|
||||||
| Constant of name * ae list (* For language constants, like (Cons hd tl) or (plus i j) *)
|
| Constant of name * ae list (* For language constants, like (Cons hd tl) or (plus i j) *)
|
||||||
| Variable of name
|
| Variable of name
|
||||||
| Tuple of ae list
|
|
||||||
| Constructor of name * ae list (* For user defined constructors *)
|
|
||||||
| Lambda of {
|
| Lambda of {
|
||||||
binder: name ;
|
binder: name ;
|
||||||
input_type: type_expression ;
|
input_type: type_expression ;
|
||||||
output_type: type_expression ;
|
output_type: type_expression ;
|
||||||
|
result: ae ;
|
||||||
body: block ;
|
body: block ;
|
||||||
}
|
}
|
||||||
|
(* Tuple *)
|
||||||
|
| Tuple of ae list
|
||||||
|
| Tuple_accessor of ae * int (* Access n'th tuple's element *)
|
||||||
|
(* Sum *)
|
||||||
|
| Constructor of name * ae (* For user defined constructors *)
|
||||||
|
(* Record *)
|
||||||
|
| Record of ae_map
|
||||||
|
| Record_accessor of ae * string
|
||||||
|
|
||||||
and literal =
|
and literal =
|
||||||
| Bool of bool
|
| Bool of bool
|
||||||
@ -64,7 +72,7 @@ and b = block
|
|||||||
|
|
||||||
and instruction =
|
and instruction =
|
||||||
| Assignment of named_expression
|
| Assignment of named_expression
|
||||||
| Matching of matching
|
| Matching of ae * matching
|
||||||
| Loop of ae * b
|
| Loop of ae * b
|
||||||
| Skip
|
| Skip
|
||||||
| Fail of ae
|
| Fail of ae
|
||||||
|
@ -28,7 +28,7 @@ and named_expression = {
|
|||||||
and tv = type_value
|
and tv = type_value
|
||||||
and ae = annotated_expression
|
and ae = annotated_expression
|
||||||
and tv_map = type_value type_name_map
|
and tv_map = type_value type_name_map
|
||||||
and e_map = expression name_map
|
and ae_map = annotated_expression name_map
|
||||||
|
|
||||||
and type_value =
|
and type_value =
|
||||||
| Type_tuple of tv list
|
| Type_tuple of tv list
|
||||||
@ -37,21 +37,31 @@ and type_value =
|
|||||||
| Type_constant of type_name * tv list
|
| Type_constant of type_name * tv list
|
||||||
|
|
||||||
and expression =
|
and expression =
|
||||||
|
(* Base *)
|
||||||
| Literal of literal
|
| Literal of literal
|
||||||
| Constant of name * ae list (* For language constants, like (Cons hd tl) or (plus i j) *)
|
| Constant of name * ae list (* For language constants, like (Cons hd tl) or (plus i j) *)
|
||||||
| Variable of name
|
| Variable of name
|
||||||
| Tuple of ae list
|
|
||||||
| Constructor of name * ae list (* For user defined constructors *)
|
|
||||||
| Lambda of {
|
| Lambda of {
|
||||||
binder: name ;
|
binder: name ;
|
||||||
input_type: type_value ;
|
input_type: tv ;
|
||||||
output_type: type_value ;
|
output_type: tv ;
|
||||||
|
result: ae ;
|
||||||
body: block ;
|
body: block ;
|
||||||
}
|
}
|
||||||
|
(* Tuple *)
|
||||||
|
| Tuple of ae list
|
||||||
|
| Tuple_accessor of ae * int (* Access n'th tuple's element *)
|
||||||
|
(* Sum *)
|
||||||
|
| Constructor of name * ae (* For user defined constructors *)
|
||||||
|
(* Record *)
|
||||||
|
| Record of ae_map
|
||||||
|
| Record_accessor of ae * string
|
||||||
|
|
||||||
|
|
||||||
and literal =
|
and literal =
|
||||||
| Bool of bool
|
| Bool of bool
|
||||||
| Number of int
|
| Int of int
|
||||||
|
| Nat of int
|
||||||
| String of string
|
| String of string
|
||||||
| Bytes of bytes
|
| Bytes of bytes
|
||||||
|
|
||||||
@ -60,7 +70,7 @@ and b = block
|
|||||||
|
|
||||||
and instruction =
|
and instruction =
|
||||||
| Assignment of named_expression
|
| Assignment of named_expression
|
||||||
| Matching of matching
|
| Matching of ae * matching
|
||||||
| Loop of ae * b
|
| Loop of ae * b
|
||||||
| Skip
|
| Skip
|
||||||
| Fail of ae
|
| Fail of ae
|
||||||
@ -127,11 +137,29 @@ let rec type_value_eq (ab: (type_value * type_value)) : unit result = match ab w
|
|||||||
)
|
)
|
||||||
| _ -> simple_fail "Different kinds of types"
|
| _ -> simple_fail "Different kinds of types"
|
||||||
|
|
||||||
let merge_annotation (a:type_value option) (b:type_value option) : type_value option result =
|
let merge_annotation (a:type_value option) (b:type_value option) : type_value result =
|
||||||
match a, b with
|
match a, b with
|
||||||
| None, None -> ok None
|
| None, None -> simple_fail "no annotation"
|
||||||
| Some a, None -> ok (Some a)
|
| Some a, None -> ok a
|
||||||
| None, Some b -> ok (Some b)
|
| None, Some b -> ok b
|
||||||
| Some a, Some b ->
|
| Some a, Some b ->
|
||||||
let%bind _ = type_value_eq (a, b) in
|
let%bind _ = type_value_eq (a, b) in
|
||||||
ok (Some a)
|
ok a
|
||||||
|
|
||||||
|
let t_bool : type_value = Type_constant ("bool", [])
|
||||||
|
let t_string : type_value = Type_constant ("string", [])
|
||||||
|
let t_int : type_value = Type_constant ("int", [])
|
||||||
|
|
||||||
|
let get_annotation (x:annotated_expression) = x.type_annotation
|
||||||
|
|
||||||
|
let get_t_tuple : type_value -> type_value list result = function
|
||||||
|
| Type_tuple lst -> ok lst
|
||||||
|
| _ -> simple_fail "not a tuple"
|
||||||
|
|
||||||
|
let get_t_sum : type_value -> type_value SMap.t result = function
|
||||||
|
| Type_sum m -> ok m
|
||||||
|
| _ -> simple_fail "not a sum"
|
||||||
|
|
||||||
|
let get_t_record : type_value -> type_value SMap.t result = function
|
||||||
|
| Type_record m -> ok m
|
||||||
|
| _ -> simple_fail "not a record"
|
||||||
|
@ -1225,6 +1225,82 @@ module Run = struct
|
|||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
module Translate_new_AST = struct
|
||||||
|
|
||||||
|
module AST = Ast_typed
|
||||||
|
|
||||||
|
let list_of_map m = List.rev @@ Ligo_helpers.X_map.String.fold (fun _ v prev -> v :: prev) m []
|
||||||
|
|
||||||
|
let rec translate_type (t:AST.type_value) : type_value result =
|
||||||
|
match t with
|
||||||
|
| Type_constant ("bool", []) -> ok (`Base Bool)
|
||||||
|
| Type_constant ("int", []) -> ok (`Base Int)
|
||||||
|
| Type_constant ("string", []) -> ok (`Base String)
|
||||||
|
| Type_sum m ->
|
||||||
|
let node = Append_tree.of_list @@ list_of_map m in
|
||||||
|
let aux a b : type_value result =
|
||||||
|
let%bind a = a in
|
||||||
|
let%bind b = b in
|
||||||
|
ok (`Or (a, b))
|
||||||
|
in
|
||||||
|
Append_tree.fold_ne translate_type aux node
|
||||||
|
| Type_record m ->
|
||||||
|
let node = Append_tree.of_list @@ list_of_map m in
|
||||||
|
let aux a b : type_value result =
|
||||||
|
let%bind a = a in
|
||||||
|
let%bind b = b in
|
||||||
|
ok (`Pair (a, b))
|
||||||
|
in
|
||||||
|
Append_tree.fold_ne translate_type aux node
|
||||||
|
| Type_tuple lst ->
|
||||||
|
let node = Append_tree.of_list lst in
|
||||||
|
let aux a b : type_value result =
|
||||||
|
let%bind a = a in
|
||||||
|
let%bind b = b in
|
||||||
|
ok (`Pair (a, b))
|
||||||
|
in
|
||||||
|
Append_tree.fold_ne translate_type aux node
|
||||||
|
| _ -> simple_fail "todo"
|
||||||
|
|
||||||
|
let rec translate_block (b:AST.block) : block result =
|
||||||
|
bind_list @@ List.map translate_instruction b
|
||||||
|
|
||||||
|
and translate_instruction (i:AST.instruction) : statement result =
|
||||||
|
match i with
|
||||||
|
| Assignment {name;annotated_expression} ->
|
||||||
|
let%bind expression = translate_annotated_expression annotated_expression in
|
||||||
|
ok @@ Assignment (Variable (name, expression))
|
||||||
|
| Matching (expr, Match_bool {match_true ; match_false}) ->
|
||||||
|
let%bind expr' = translate_annotated_expression expr in
|
||||||
|
let%bind true_branch = translate_block match_true in
|
||||||
|
let%bind false_branch = translate_block match_false in
|
||||||
|
ok @@ Cond (expr', true_branch, false_branch)
|
||||||
|
| Loop (expr, body) ->
|
||||||
|
let%bind expr' = translate_annotated_expression expr in
|
||||||
|
let%bind body' = translate_block body in
|
||||||
|
ok @@ While (expr', body')
|
||||||
|
| _ -> simple_fail "todo"
|
||||||
|
|
||||||
|
and translate_annotated_expression (ae:AST.annotated_expression) : expression result =
|
||||||
|
let%bind tv = translate_type ae.type_annotation in
|
||||||
|
match ae.expression with
|
||||||
|
| Literal (Bool b) -> ok (Literal (`Bool b), tv)
|
||||||
|
| Literal (Number n) -> ok (Literal (`Int n), tv)
|
||||||
|
| Literal (String s) -> ok (Literal (`String s), tv)
|
||||||
|
| Variable name -> ok (Var name, tv)
|
||||||
|
| _ -> simple_fail "todo"
|
||||||
|
|
||||||
|
|
||||||
|
let translate_declaration (d:AST.declaration) : toplevel_statement result =
|
||||||
|
match d with
|
||||||
|
| Constant_declaration {name;annotated_expression} ->
|
||||||
|
let%bind expression = translate_annotated_expression annotated_expression in
|
||||||
|
ok @@ Variable (name, expression)
|
||||||
|
|
||||||
|
let translate_program (lst:AST.program) : program result =
|
||||||
|
bind_list @@ List.map translate_declaration lst
|
||||||
|
end
|
||||||
|
|
||||||
module Combinators = struct
|
module Combinators = struct
|
||||||
|
|
||||||
let var x : expression' = Var x
|
let var x : expression' = Var x
|
||||||
|
@ -6,20 +6,36 @@ module O = Ast_typed
|
|||||||
module SMap = O.SMap
|
module SMap = O.SMap
|
||||||
|
|
||||||
module Environment = struct
|
module Environment = struct
|
||||||
type t = unit
|
type ele = O.type_value
|
||||||
let empty : t = ()
|
|
||||||
|
|
||||||
let get (():t) (_s:string) : O.type_value option = None
|
type t = {
|
||||||
let add (():t) (_s:string) (_tv:O.type_value) : t = ()
|
environment: (string * ele) list ;
|
||||||
let get_type (():t) (_s:string) : O.type_value option = None
|
type_environment: (string * ele) list ;
|
||||||
let add_type (():t) (_s:string) (_tv:O.type_value) : t = ()
|
}
|
||||||
|
let empty : t = {
|
||||||
|
environment = [] ;
|
||||||
|
type_environment = [] ;
|
||||||
|
}
|
||||||
|
|
||||||
|
let get (e:t) (s:string) : ele option =
|
||||||
|
List.assoc_opt s e.environment
|
||||||
|
let get_constructor (e:t) (s:string) : (ele * ele) option =
|
||||||
|
let rec aux = function
|
||||||
|
| [] -> None
|
||||||
|
| (_, ((O.Type_sum m) as tv)) :: _ when SMap.mem s m -> Some (SMap.find s m, tv)
|
||||||
|
| _ :: tl -> aux tl
|
||||||
|
in
|
||||||
|
aux e.environment
|
||||||
|
let add (e:t) (s:string) (tv:ele) : t =
|
||||||
|
{e with environment = (s, tv) :: e.environment}
|
||||||
|
let get_type (e:t) (s:string) : ele option =
|
||||||
|
List.assoc_opt s e.type_environment
|
||||||
|
let add_type (e:t) (s:string) (tv:ele) : t =
|
||||||
|
{e with type_environment = (s, tv) :: e.type_environment}
|
||||||
end
|
end
|
||||||
|
|
||||||
type environment = Environment.t
|
type environment = Environment.t
|
||||||
|
|
||||||
type environment = unit
|
|
||||||
let empty : environment = ()
|
|
||||||
|
|
||||||
let rec type_program (p:I.program) : O.program result =
|
let rec type_program (p:I.program) : O.program result =
|
||||||
let aux (e, acc:(environment * O.declaration list)) (d:I.declaration) =
|
let aux (e, acc:(environment * O.declaration list)) (d:I.declaration) =
|
||||||
let%bind (e', d') = type_declaration e d in
|
let%bind (e', d') = type_declaration e d in
|
||||||
@ -27,12 +43,18 @@ let rec type_program (p:I.program) : O.program result =
|
|||||||
| None -> ok (e', acc)
|
| None -> ok (e', acc)
|
||||||
| Some d' -> ok (e', d' :: acc)
|
| Some d' -> ok (e', d' :: acc)
|
||||||
in
|
in
|
||||||
let%bind (_, lst) = bind_fold_list aux (empty, []) p in
|
let%bind (_, lst) = bind_fold_list aux (Environment.empty, []) p in
|
||||||
ok @@ List.rev lst
|
ok @@ List.rev lst
|
||||||
|
|
||||||
and type_declaration _env : I.declaration -> (environment * O.declaration option) result = function
|
and type_declaration env : I.declaration -> (environment * O.declaration option) result = function
|
||||||
| Type_declaration _ -> simple_fail ""
|
| Type_declaration {type_name;type_expression} ->
|
||||||
| Constant_declaration _ -> simple_fail ""
|
let%bind tv = evaluate_type env type_expression in
|
||||||
|
let env' = Environment.add_type env type_name tv in
|
||||||
|
ok (env', None)
|
||||||
|
| Constant_declaration {name;annotated_expression} ->
|
||||||
|
let%bind ae' = type_annotated_expression env annotated_expression in
|
||||||
|
let env' = Environment.add env name ae'.type_annotation in
|
||||||
|
ok (env', Some (O.Constant_declaration {name;annotated_expression=ae'}))
|
||||||
|
|
||||||
and type_block (e:environment) (b:I.block) : O.block result =
|
and type_block (e:environment) (b:I.block) : O.block result =
|
||||||
let aux (e, acc:(environment * O.instruction list)) (i:I.instruction) =
|
let aux (e, acc:(environment * O.instruction list)) (i:I.instruction) =
|
||||||
@ -73,9 +95,10 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
|
|||||||
let e' = Environment.add e name annotated_expression.type_annotation in
|
let e' = Environment.add e name annotated_expression.type_annotation in
|
||||||
ok (e', O.Assignment {name;annotated_expression})
|
ok (e', O.Assignment {name;annotated_expression})
|
||||||
)
|
)
|
||||||
| Matching m ->
|
| Matching (ex, m) ->
|
||||||
let%bind m' = type_match e m in
|
let%bind m' = type_match e m in
|
||||||
ok (e, O.Matching m')
|
let%bind ex' = type_annotated_expression e ex in
|
||||||
|
ok (e, O.Matching (ex', m'))
|
||||||
|
|
||||||
and type_match (e:environment) : I.matching -> O.matching result = function
|
and type_match (e:environment) : I.matching -> O.matching result = function
|
||||||
| Match_bool {match_true ; match_false} ->
|
| Match_bool {match_true ; match_false} ->
|
||||||
@ -129,10 +152,66 @@ and evaluate_type (e:environment) : I.type_expression -> O.type_value result = f
|
|||||||
ok (O.Type_constant(cst, lst'))
|
ok (O.Type_constant(cst, lst'))
|
||||||
|
|
||||||
and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.annotated_expression result =
|
and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.annotated_expression result =
|
||||||
|
let%bind tv_opt = match ae.type_annotation with
|
||||||
|
| None -> ok None
|
||||||
|
| Some s -> let%bind r = evaluate_type e s in ok (Some r) in
|
||||||
|
let check tv = O.merge_annotation (Some tv) tv_opt in
|
||||||
match ae.expression with
|
match ae.expression with
|
||||||
|
(* Basic *)
|
||||||
| Variable name ->
|
| Variable name ->
|
||||||
let%bind tv' =
|
let%bind tv' =
|
||||||
trace_option (simple_error "var not in env")
|
trace_option (simple_error "var not in env")
|
||||||
@@ Environment.get e name in
|
@@ Environment.get e name in
|
||||||
ok O.{expression = Variable name ; type_annotation = tv'}
|
let%bind type_annotation = check tv' in
|
||||||
|
ok O.{expression = Variable name ; type_annotation}
|
||||||
|
| Literal (Bool b) ->
|
||||||
|
let%bind type_annotation = check O.t_bool in
|
||||||
|
ok O.{expression = Literal (Bool b) ; type_annotation }
|
||||||
|
| Literal (String s) ->
|
||||||
|
let%bind type_annotation = check O.t_string in
|
||||||
|
ok O.{expression = Literal (String s) ; type_annotation }
|
||||||
|
| Literal (Number n) ->
|
||||||
|
let%bind type_annotation = check O.t_int in
|
||||||
|
ok O.{expression = Literal (Int n) ; type_annotation }
|
||||||
|
(* Tuple *)
|
||||||
|
| Tuple lst ->
|
||||||
|
let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
|
||||||
|
let tv_lst = List.map O.get_annotation lst' in
|
||||||
|
let%bind type_annotation = check (O.Type_tuple tv_lst) in
|
||||||
|
ok O.{expression = Tuple lst' ; type_annotation }
|
||||||
|
| Tuple_accessor (tpl, ind) ->
|
||||||
|
let%bind tpl' = type_annotated_expression e tpl in
|
||||||
|
let%bind tpl_tv = O.get_t_tuple tpl'.type_annotation in
|
||||||
|
let%bind tv =
|
||||||
|
generic_try (simple_error "bad tuple index")
|
||||||
|
@@ (fun () -> List.nth tpl_tv ind) in
|
||||||
|
let%bind type_annotation = check tv in
|
||||||
|
ok O.{expression = O.Tuple_accessor (tpl', ind) ; type_annotation}
|
||||||
|
(* Sum *)
|
||||||
|
| Constructor (c, expr) ->
|
||||||
|
let%bind (c_tv, sum_tv) =
|
||||||
|
trace_option (simple_error "no such constructor")
|
||||||
|
@@ Environment.get_constructor e c in
|
||||||
|
let%bind expr' = type_annotated_expression e expr in
|
||||||
|
let%bind _assert = O.type_value_eq (expr'.type_annotation, c_tv) in
|
||||||
|
let%bind type_annotation = check sum_tv in
|
||||||
|
ok O.{expression = O.Constructor(c, expr') ; type_annotation }
|
||||||
|
(* Record *)
|
||||||
|
| Record m ->
|
||||||
|
let aux k expr prev =
|
||||||
|
let%bind prev' = prev in
|
||||||
|
let%bind expr' = type_annotated_expression e expr in
|
||||||
|
ok (SMap.add k expr' prev')
|
||||||
|
in
|
||||||
|
let%bind m' = SMap.fold aux m (ok SMap.empty) in
|
||||||
|
let%bind type_annotation = check @@ O.Type_record (SMap.map O.get_annotation m') in
|
||||||
|
ok O.{expression = O.Record m' ; type_annotation }
|
||||||
|
| Record_accessor (r, ind) ->
|
||||||
|
let%bind r' = type_annotated_expression e r in
|
||||||
|
let%bind r_tv = O.get_t_record r'.type_annotation in
|
||||||
|
let%bind tv =
|
||||||
|
generic_try (simple_error "bad record index")
|
||||||
|
@@ (fun () -> SMap.find ind r_tv) in
|
||||||
|
let%bind type_annotation = check tv in
|
||||||
|
ok O.{expression = O.Record_accessor (r', ind) ; type_annotation }
|
||||||
| _ -> simple_fail "default"
|
| _ -> simple_fail "default"
|
||||||
|
Loading…
Reference in New Issue
Block a user