added matching tests
This commit is contained in:
parent
0e8ba13660
commit
941dadeb3b
@ -65,6 +65,7 @@ and expression =
|
|||||||
| Accessor of ae * access_path
|
| Accessor of ae * access_path
|
||||||
(* Data Structures *)
|
(* Data Structures *)
|
||||||
| Map of (ae * ae) list
|
| Map of (ae * ae) list
|
||||||
|
| LookUp of (ae * ae)
|
||||||
|
|
||||||
and access =
|
and access =
|
||||||
| Tuple_access of int
|
| Tuple_access of int
|
||||||
@ -140,6 +141,7 @@ module PP = struct
|
|||||||
| Accessor (ae, p) -> fprintf ppf "%a.%a" annotated_expression ae access_path p
|
| Accessor (ae, p) -> fprintf ppf "%a.%a" annotated_expression ae access_path p
|
||||||
| Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
|
| Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
|
||||||
| Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m
|
| Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m
|
||||||
|
| LookUp (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind
|
||||||
| Lambda {binder;input_type;output_type;result;body} ->
|
| Lambda {binder;input_type;output_type;result;body} ->
|
||||||
fprintf ppf "lambda (%s:%a) : %a {%a} return %a"
|
fprintf ppf "lambda (%s:%a) : %a {%a} return %a"
|
||||||
binder type_expression input_type type_expression output_type
|
binder type_expression input_type type_expression output_type
|
||||||
@ -310,433 +312,19 @@ module Rename = struct
|
|||||||
let%bind m' = bind_map_list
|
let%bind m' = bind_map_list
|
||||||
(fun (x, y) -> bind_map_pair (rename_annotated_expression r) (x, y)) m in
|
(fun (x, y) -> bind_map_pair (rename_annotated_expression r) (x, y)) m in
|
||||||
ok (Map m')
|
ok (Map m')
|
||||||
|
| LookUp m ->
|
||||||
|
let%bind m' = bind_map_pair (rename_annotated_expression r) m in
|
||||||
|
ok (LookUp m')
|
||||||
end
|
end
|
||||||
end
|
end
|
||||||
|
|
||||||
module Simplify = struct
|
|
||||||
module Raw = Ligo_parser.AST
|
|
||||||
|
|
||||||
let nseq_to_list (hd, tl) = hd :: tl
|
|
||||||
let npseq_to_list (hd, tl) = hd :: (List.map snd tl)
|
|
||||||
let npseq_to_nelist (hd, tl) = hd, (List.map snd tl)
|
|
||||||
let pseq_to_list = function
|
|
||||||
| None -> []
|
|
||||||
| Some lst -> npseq_to_list lst
|
|
||||||
|
|
||||||
let type_constants = [
|
|
||||||
("unit", 0) ;
|
|
||||||
("nat", 0) ;
|
|
||||||
("int", 0) ;
|
|
||||||
("bool", 0) ;
|
|
||||||
("list", 1) ;
|
|
||||||
("set", 1) ;
|
|
||||||
("map", 2) ;
|
|
||||||
]
|
|
||||||
|
|
||||||
let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
|
|
||||||
match t with
|
|
||||||
| TPar x -> simpl_type_expression x.value.inside
|
|
||||||
| TAlias v -> (
|
|
||||||
match List.assoc_opt v.value type_constants with
|
|
||||||
| Some 0 ->
|
|
||||||
ok @@ Type_constant (v.value, [])
|
|
||||||
| Some _ ->
|
|
||||||
simple_fail "type constructor with wrong number of args"
|
|
||||||
| None ->
|
|
||||||
ok @@ Type_variable v.value
|
|
||||||
)
|
|
||||||
| TApp x ->
|
|
||||||
let (name, tuple) = x.value in
|
|
||||||
let lst = npseq_to_list tuple.value.inside in
|
|
||||||
let%bind _ = match List.assoc_opt name.value type_constants with
|
|
||||||
| Some n when n = List.length lst -> ok ()
|
|
||||||
| Some _ -> simple_fail "type constructor with wrong number of args"
|
|
||||||
| None -> simple_fail "unrecognized type constants" in
|
|
||||||
let%bind lst' = bind_list @@ List.map simpl_type_expression lst in
|
|
||||||
ok @@ Type_constant (name.value, lst')
|
|
||||||
| TProd p ->
|
|
||||||
let%bind tpl = simpl_list_type_expression
|
|
||||||
@@ npseq_to_list p.value in
|
|
||||||
ok tpl
|
|
||||||
| TRecord r ->
|
|
||||||
let aux = fun (x, y) -> let%bind y = simpl_type_expression y in ok (x, y) in
|
|
||||||
let%bind lst = bind_list
|
|
||||||
@@ List.map aux
|
|
||||||
@@ List.map (fun (x:Raw.field_decl Raw.reg) -> (x.value.field_name.value, x.value.field_type))
|
|
||||||
@@ npseq_to_list r.value.field_decls in
|
|
||||||
let m = List.fold_left (fun m (x, y) -> SMap.add x y m) SMap.empty lst in
|
|
||||||
ok @@ Type_record m
|
|
||||||
| TSum s ->
|
|
||||||
let aux (v:Raw.variant Raw.reg) =
|
|
||||||
let%bind te = simpl_list_type_expression
|
|
||||||
@@ npseq_to_list v.value.product.value in
|
|
||||||
ok (v.value.constr.value, te)
|
|
||||||
in
|
|
||||||
let%bind lst = bind_list
|
|
||||||
@@ List.map aux
|
|
||||||
@@ npseq_to_list s.value in
|
|
||||||
let m = List.fold_left (fun m (x, y) -> SMap.add x y m) SMap.empty lst in
|
|
||||||
ok @@ Type_sum m
|
|
||||||
|
|
||||||
and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result =
|
|
||||||
match lst with
|
|
||||||
| [] -> assert false
|
|
||||||
| [hd] -> simpl_type_expression hd
|
|
||||||
| lst ->
|
|
||||||
let%bind lst = bind_list @@ List.map simpl_type_expression lst in
|
|
||||||
ok @@ Type_tuple lst
|
|
||||||
|
|
||||||
let rec simpl_expression (t:Raw.expr) : ae result =
|
|
||||||
match t with
|
|
||||||
| EVar c ->
|
|
||||||
if c.value = "unit"
|
|
||||||
then ok @@ ae @@ Literal Unit
|
|
||||||
else ok @@ ae @@ Variable c.value
|
|
||||||
| ECall x ->
|
|
||||||
let (name, args) = x.value in
|
|
||||||
let f = name.value in
|
|
||||||
let%bind arg = simpl_list_expression
|
|
||||||
@@ npseq_to_list args.value.inside in
|
|
||||||
ok @@ ae @@ Application (ae @@ Variable f, arg)
|
|
||||||
| EPar x -> simpl_expression x.value.inside
|
|
||||||
| EUnit _ -> ok @@ ae @@ Literal Unit
|
|
||||||
| EBytes x -> ok @@ ae @@ Literal (Bytes (Bytes.of_string @@ fst x.value))
|
|
||||||
| ETuple tpl ->
|
|
||||||
let (Raw.TupleInj tpl') = tpl in
|
|
||||||
simpl_list_expression
|
|
||||||
@@ npseq_to_list tpl'.value.inside
|
|
||||||
| ERecord (RecordInj r) ->
|
|
||||||
let%bind fields = bind_list
|
|
||||||
@@ List.map (fun ((k : _ Raw.reg), v) -> let%bind v = simpl_expression v in ok (k.value, v))
|
|
||||||
@@ List.map (fun (x:Raw.field_assign Raw.reg) -> (x.value.field_name, x.value.field_expr))
|
|
||||||
@@ npseq_to_list r.value.fields in
|
|
||||||
let aux prev (k, v) = SMap.add k v prev in
|
|
||||||
ok @@ ae @@ Record (List.fold_left aux SMap.empty fields)
|
|
||||||
| EProj p' -> (
|
|
||||||
let p = p'.value in
|
|
||||||
let var =
|
|
||||||
let name = p.record_name.value in
|
|
||||||
ae @@ Variable name in
|
|
||||||
let path = p.field_path in
|
|
||||||
let path' =
|
|
||||||
let aux (s:Raw.selection) =
|
|
||||||
match s with
|
|
||||||
| FieldName property -> Record_access property.value
|
|
||||||
| Component index -> Tuple_access (Z.to_int (snd index.value))
|
|
||||||
in
|
|
||||||
List.map aux @@ npseq_to_list path in
|
|
||||||
ok @@ ae @@ Accessor (var, path')
|
|
||||||
)
|
|
||||||
| EConstr (ConstrApp c) ->
|
|
||||||
let (c, args) = c.value in
|
|
||||||
let%bind arg =
|
|
||||||
simpl_list_expression
|
|
||||||
@@ npseq_to_list args.value.inside in
|
|
||||||
ok @@ ae @@ Constructor (c.value, arg)
|
|
||||||
| EConstr _ -> simple_fail "econstr: not supported yet"
|
|
||||||
| EArith (Add c) ->
|
|
||||||
simpl_binop "ADD" c.value
|
|
||||||
| EArith (Int n) ->
|
|
||||||
let n = Z.to_int @@ snd @@ n.value in
|
|
||||||
ok @@ ae @@ Literal (Number n)
|
|
||||||
| EArith _ -> simple_fail "arith: not supported yet"
|
|
||||||
| EString (String s) ->
|
|
||||||
ok @@ ae @@ Literal (String s.value)
|
|
||||||
| EString _ -> simple_fail "string: not supported yet"
|
|
||||||
| ELogic l -> simpl_logic_expression l
|
|
||||||
| EList _ -> simple_fail "list: not supported yet"
|
|
||||||
| ESet _ -> simple_fail "set: not supported yet"
|
|
||||||
| EMap _ -> simple_fail "map: not supported yet"
|
|
||||||
|
|
||||||
and simpl_logic_expression (t:Raw.logic_expr) : ae result =
|
|
||||||
match t with
|
|
||||||
| BoolExpr (False _) ->
|
|
||||||
ok @@ ae @@ Literal (Bool false)
|
|
||||||
| BoolExpr (True _) ->
|
|
||||||
ok @@ ae @@ Literal (Bool true)
|
|
||||||
| BoolExpr (Or b) ->
|
|
||||||
simpl_binop "OR" b.value
|
|
||||||
| BoolExpr (And b) ->
|
|
||||||
simpl_binop "AND" b.value
|
|
||||||
| BoolExpr (Not b) ->
|
|
||||||
simpl_unop "NOT" b.value
|
|
||||||
| CompExpr (Lt c) ->
|
|
||||||
simpl_binop "LT" c.value
|
|
||||||
| CompExpr (Gt c) ->
|
|
||||||
simpl_binop "GT" c.value
|
|
||||||
| CompExpr (Leq c) ->
|
|
||||||
simpl_binop "LE" c.value
|
|
||||||
| CompExpr (Geq c) ->
|
|
||||||
simpl_binop "GE" c.value
|
|
||||||
| CompExpr (Equal c) ->
|
|
||||||
simpl_binop "EQ" c.value
|
|
||||||
| CompExpr (Neq c) ->
|
|
||||||
simpl_binop "NEQ" c.value
|
|
||||||
|
|
||||||
and simpl_binop (name:string) (t:_ Raw.bin_op) : ae result =
|
|
||||||
let%bind a = simpl_expression t.arg1 in
|
|
||||||
let%bind b = simpl_expression t.arg2 in
|
|
||||||
ok @@ ae @@ Constant (name, [a;b])
|
|
||||||
|
|
||||||
and simpl_unop (name:string) (t:_ Raw.un_op) : ae result =
|
|
||||||
let%bind a = simpl_expression t.arg in
|
|
||||||
ok @@ ae @@ Constant (name, [a])
|
|
||||||
|
|
||||||
and simpl_list_expression (lst:Raw.expr list) : ae result =
|
|
||||||
match lst with
|
|
||||||
| [] -> ok @@ ae @@ Literal Unit
|
|
||||||
| [hd] -> simpl_expression hd
|
|
||||||
| lst ->
|
|
||||||
let%bind lst = bind_list @@ List.map simpl_expression lst in
|
|
||||||
ok @@ ae @@ Tuple lst
|
|
||||||
|
|
||||||
and simpl_local_declaration (t:Raw.local_decl) : (instruction * named_expression) result =
|
|
||||||
match t with
|
|
||||||
| LocalData d -> simpl_data_declaration d
|
|
||||||
| LocalLam _ -> simple_fail "no local lambdas yet"
|
|
||||||
|
|
||||||
and simpl_data_declaration (t:Raw.data_decl) : (instruction * named_expression) result =
|
|
||||||
let return x = ok (Assignment x, x) in
|
|
||||||
match t with
|
|
||||||
| LocalVar x ->
|
|
||||||
let x = x.value in
|
|
||||||
let name = x.name.value in
|
|
||||||
let%bind t = simpl_type_expression x.var_type in
|
|
||||||
let type_annotation = Some t in
|
|
||||||
let%bind expression = simpl_expression x.init in
|
|
||||||
return {name;annotated_expression={expression with type_annotation}}
|
|
||||||
| LocalConst x ->
|
|
||||||
let x = x.value in
|
|
||||||
let name = x.name.value in
|
|
||||||
let%bind t = simpl_type_expression x.const_type in
|
|
||||||
let type_annotation = Some t in
|
|
||||||
let%bind expression = simpl_expression x.init in
|
|
||||||
return {name;annotated_expression={expression with type_annotation}}
|
|
||||||
|
|
||||||
|
|
||||||
and simpl_param : Raw.param_decl -> named_type_expression result = fun t ->
|
|
||||||
match t with
|
|
||||||
| ParamConst c ->
|
|
||||||
let c = c.value in
|
|
||||||
let type_name = c.var.value in
|
|
||||||
let%bind type_expression = simpl_type_expression c.param_type in
|
|
||||||
ok { type_name ; type_expression }
|
|
||||||
| ParamVar v ->
|
|
||||||
let c = v.value in
|
|
||||||
let type_name = c.var.value in
|
|
||||||
let%bind type_expression = simpl_type_expression c.param_type in
|
|
||||||
ok { type_name ; type_expression }
|
|
||||||
|
|
||||||
and simpl_declaration : Raw.declaration -> declaration result = fun t ->
|
|
||||||
let open! Raw in
|
|
||||||
match t with
|
|
||||||
| TypeDecl x ->
|
|
||||||
let {name;type_expr} : Raw.type_decl = x.value in
|
|
||||||
let%bind type_expression = simpl_type_expression type_expr in
|
|
||||||
ok @@ Type_declaration {type_name=name.value;type_expression}
|
|
||||||
| ConstDecl x ->
|
|
||||||
let {name;const_type;init} = x.value in
|
|
||||||
let%bind expression = simpl_expression init in
|
|
||||||
let%bind t = simpl_type_expression const_type in
|
|
||||||
let type_annotation = Some t in
|
|
||||||
ok @@ Constant_declaration {name=name.value;annotated_expression={expression with type_annotation}}
|
|
||||||
| LambdaDecl (FunDecl x) ->
|
|
||||||
let {name;param;ret_type;local_decls;block;return} : fun_decl = x.value in
|
|
||||||
(match npseq_to_list param.value.inside with
|
|
||||||
| [] -> simple_fail "function without parameters are not allowed"
|
|
||||||
| [a] -> (
|
|
||||||
let%bind input = simpl_param a in
|
|
||||||
let name = name.value in
|
|
||||||
let binder = input.type_name in
|
|
||||||
let input_type = input.type_expression in
|
|
||||||
let%bind local_declarations =
|
|
||||||
let%bind tmp = bind_list
|
|
||||||
@@ List.map simpl_local_declaration local_decls in
|
|
||||||
ok (List.map fst tmp) in
|
|
||||||
let%bind instructions = bind_list
|
|
||||||
@@ List.map simpl_statement
|
|
||||||
@@ npseq_to_list block.value.statements in
|
|
||||||
let%bind result = simpl_expression return in
|
|
||||||
let%bind output_type = simpl_type_expression ret_type in
|
|
||||||
let body = local_declarations @ instructions in
|
|
||||||
let decl =
|
|
||||||
let expression = Lambda {binder ; input_type ; output_type ; result ; body } in
|
|
||||||
let type_annotation = Some (Type_function (input_type, output_type)) in
|
|
||||||
Constant_declaration {name;annotated_expression = {expression;type_annotation}}
|
|
||||||
in
|
|
||||||
ok decl
|
|
||||||
)
|
|
||||||
| lst -> (
|
|
||||||
let%bind params = bind_map_list simpl_param lst in
|
|
||||||
let input =
|
|
||||||
let type_expression = Type_record (
|
|
||||||
SMap.of_list
|
|
||||||
@@ List.map (fun (x:named_type_expression) -> x.type_name, x.type_expression)
|
|
||||||
params
|
|
||||||
) in
|
|
||||||
{ type_name = "arguments" ; type_expression } in
|
|
||||||
let binder = input.type_name in
|
|
||||||
let input_type = input.type_expression in
|
|
||||||
let%bind local_declarations =
|
|
||||||
let%bind typed = bind_map_list simpl_local_declaration local_decls in
|
|
||||||
ok (List.map fst typed)
|
|
||||||
in
|
|
||||||
let%bind output_type = simpl_type_expression ret_type in
|
|
||||||
let%bind instructions = bind_list
|
|
||||||
@@ List.map simpl_statement
|
|
||||||
@@ npseq_to_list block.value.statements in
|
|
||||||
let%bind (body, result) =
|
|
||||||
let renamings =
|
|
||||||
let aux ({type_name}:named_type_expression) : Rename.Value.renaming =
|
|
||||||
type_name, ("arguments", [Record_access type_name])
|
|
||||||
in
|
|
||||||
List.map aux params
|
|
||||||
in
|
|
||||||
let%bind r =
|
|
||||||
let%bind tmp = simpl_expression return in
|
|
||||||
Rename.Value.rename_annotated_expression renamings tmp
|
|
||||||
in
|
|
||||||
let%bind b =
|
|
||||||
let tmp = local_declarations @ instructions in
|
|
||||||
Rename.Value.rename_block renamings tmp
|
|
||||||
in
|
|
||||||
ok (b, r) in
|
|
||||||
let decl =
|
|
||||||
let expression = Lambda {binder ; input_type ; output_type ; result ; body } in
|
|
||||||
let type_annotation = Some (Type_function (input_type, output_type)) in
|
|
||||||
Constant_declaration {name = name.value;annotated_expression = {expression;type_annotation}}
|
|
||||||
in
|
|
||||||
ok decl
|
|
||||||
)
|
|
||||||
)
|
|
||||||
| LambdaDecl (ProcDecl _) -> simple_fail "no proc declaration yet"
|
|
||||||
| LambdaDecl (EntryDecl _)-> simple_fail "no entry point yet"
|
|
||||||
|
|
||||||
and simpl_statement : Raw.statement -> instruction result = fun s ->
|
|
||||||
match s with
|
|
||||||
| Instr i -> simpl_instruction i
|
|
||||||
| Data d -> let%bind (i, _) = simpl_data_declaration d in ok i
|
|
||||||
|
|
||||||
and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
|
|
||||||
match t with
|
|
||||||
| ProcCall _ -> simple_fail "no proc call"
|
|
||||||
| Fail e ->
|
|
||||||
let%bind expr = simpl_expression e.value.fail_expr in
|
|
||||||
ok @@ Fail expr
|
|
||||||
| Skip _ -> ok @@ Skip
|
|
||||||
| Loop (While l) ->
|
|
||||||
let l = l.value in
|
|
||||||
let%bind cond = simpl_expression l.cond in
|
|
||||||
let%bind body = simpl_block l.block.value in
|
|
||||||
ok @@ Loop (cond, body)
|
|
||||||
| Loop (For _) ->
|
|
||||||
simple_fail "no for yet"
|
|
||||||
| Cond c ->
|
|
||||||
let c = c.value in
|
|
||||||
let%bind expr = simpl_expression c.test in
|
|
||||||
let%bind match_true = match c.ifso with
|
|
||||||
| ClauseInstr i -> let%bind i = simpl_instruction i in ok [i]
|
|
||||||
| ClauseBlock b -> simpl_statements @@ fst b.value.inside in
|
|
||||||
let%bind match_false = match c.ifnot with
|
|
||||||
| ClauseInstr i -> let%bind i = simpl_instruction i in ok [i]
|
|
||||||
| ClauseBlock b -> simpl_statements @@ fst b.value.inside in
|
|
||||||
ok @@ Matching (expr, (Match_bool {match_true; match_false}))
|
|
||||||
| Assign a ->
|
|
||||||
let a = a.value in
|
|
||||||
let%bind name = match a.lhs with
|
|
||||||
| Path (Name v) -> ok v.value
|
|
||||||
| _ -> simple_fail "no complex assignments yet"
|
|
||||||
in
|
|
||||||
let%bind annotated_expression = match a.rhs with
|
|
||||||
| Expr e -> simpl_expression e
|
|
||||||
| _ -> simple_fail "no weird assignments yet"
|
|
||||||
in
|
|
||||||
ok @@ Assignment {name ; annotated_expression}
|
|
||||||
| Case c ->
|
|
||||||
let c = c.value in
|
|
||||||
let%bind expr = simpl_expression c.expr in
|
|
||||||
let%bind cases =
|
|
||||||
let aux (x : Raw.case Raw.reg) =
|
|
||||||
let%bind i = simpl_instruction_block x.value.instr in
|
|
||||||
ok (x.value.pattern, i) in
|
|
||||||
bind_list
|
|
||||||
@@ List.map aux
|
|
||||||
@@ npseq_to_list c.cases.value in
|
|
||||||
let%bind m = simpl_cases cases in
|
|
||||||
ok @@ Matching (expr, m)
|
|
||||||
| RecordPatch r ->
|
|
||||||
let r = r.value in
|
|
||||||
let%bind record = match r.path with
|
|
||||||
| Name v -> ok v.value
|
|
||||||
| _ -> simple_fail "no complex assignments yet"
|
|
||||||
in
|
|
||||||
let%bind inj = bind_list
|
|
||||||
@@ List.map (fun (x:Raw.field_assign) -> let%bind e = simpl_expression x.field_expr in ok (x.field_name.value, e))
|
|
||||||
@@ List.map (fun (x:_ Raw.reg) -> x.value)
|
|
||||||
@@ npseq_to_list r.record_inj.value.fields in
|
|
||||||
ok @@ Record_patch (record, [], inj)
|
|
||||||
| MapPatch _ -> simple_fail "no map patch yet"
|
|
||||||
| SetPatch _ -> simple_fail "no set patch yet"
|
|
||||||
| MapRemove _ -> simple_fail "no map remove yet"
|
|
||||||
| SetRemove _ -> simple_fail "no set remove yet"
|
|
||||||
|
|
||||||
and simpl_cases : (Raw.pattern * block) list -> matching result = fun t ->
|
|
||||||
let open Raw in
|
|
||||||
let get_var (t:Raw.pattern) = match t with
|
|
||||||
| PVar v -> ok v.value
|
|
||||||
| _ -> simple_fail "not a var"
|
|
||||||
in
|
|
||||||
match t with
|
|
||||||
| [(PFalse _, f) ; (PTrue _, t)]
|
|
||||||
| [(PTrue _, t) ; (PFalse _, f)] -> ok @@ Match_bool {match_true = t ; match_false = f}
|
|
||||||
| [(PSome v, some) ; (PNone _, none)]
|
|
||||||
| [(PNone _, none) ; (PSome v, some)] -> (
|
|
||||||
let (_, v) = v.value in
|
|
||||||
let%bind v = match v.value.inside with
|
|
||||||
| PVar v -> ok v.value
|
|
||||||
| _ -> simple_fail "complex patterns not supported yet" in
|
|
||||||
ok @@ Match_option {match_none = none ; match_some = (v, some) }
|
|
||||||
)
|
|
||||||
| [(PCons c, cons) ; (PList (PNil _), nil)]
|
|
||||||
| [(PList (PNil _), nil) ; (PCons c, cons)] ->
|
|
||||||
let%bind (a, b) =
|
|
||||||
match c.value with
|
|
||||||
| a, [(_, b)] ->
|
|
||||||
let%bind a = get_var a in
|
|
||||||
let%bind b = get_var b in
|
|
||||||
ok (a, b)
|
|
||||||
| _ -> simple_fail "complex patterns not supported yet"
|
|
||||||
in
|
|
||||||
ok @@ Match_list {match_cons = (a, b, cons) ; match_nil = nil}
|
|
||||||
| _ -> simple_fail "complex patterns not supported yet"
|
|
||||||
|
|
||||||
and simpl_instruction_block : Raw.instruction -> block result = fun t ->
|
|
||||||
match t with
|
|
||||||
| Single s -> let%bind i = simpl_single_instruction s in ok [ i ]
|
|
||||||
| Block b -> simpl_block b.value
|
|
||||||
|
|
||||||
and simpl_instruction : Raw.instruction -> instruction result = fun t ->
|
|
||||||
match t with
|
|
||||||
| Single s -> simpl_single_instruction s
|
|
||||||
| Block _ -> simple_fail "no block instruction yet"
|
|
||||||
|
|
||||||
and simpl_statements : Raw.statements -> block result = fun ss ->
|
|
||||||
let lst = npseq_to_list ss in
|
|
||||||
bind_map_list simpl_statement lst
|
|
||||||
|
|
||||||
and simpl_block : Raw.block -> block result = fun t ->
|
|
||||||
simpl_statements t.statements
|
|
||||||
|
|
||||||
let simpl_program : Raw.ast -> program result = fun t ->
|
|
||||||
bind_list @@ List.map simpl_declaration @@ nseq_to_list t.decl
|
|
||||||
end
|
|
||||||
|
|
||||||
module Combinators = struct
|
module Combinators = struct
|
||||||
let t_bool : type_expression = Type_constant ("bool", [])
|
let t_bool : type_expression = Type_constant ("bool", [])
|
||||||
let t_string : type_expression = Type_constant ("string", [])
|
let t_string : type_expression = Type_constant ("string", [])
|
||||||
let t_bytes : type_expression = Type_constant ("bytes", [])
|
let t_bytes : type_expression = Type_constant ("bytes", [])
|
||||||
let t_int : type_expression = Type_constant ("int", [])
|
let t_int : type_expression = Type_constant ("int", [])
|
||||||
let t_unit : type_expression = Type_constant ("unit", [])
|
let t_unit : type_expression = Type_constant ("unit", [])
|
||||||
|
let t_option o : type_expression = Type_constant ("option", [o])
|
||||||
let t_tuple lst : type_expression = Type_tuple lst
|
let t_tuple lst : type_expression = Type_tuple lst
|
||||||
let t_pair a b = t_tuple [a ; b]
|
let t_pair a b = t_tuple [a ; b]
|
||||||
let t_record m : type_expression = (Type_record m)
|
let t_record m : type_expression = (Type_record m)
|
||||||
|
@ -66,6 +66,7 @@ and expression =
|
|||||||
| Record_accessor of ae * string
|
| Record_accessor of ae * string
|
||||||
(* Data Structures *)
|
(* Data Structures *)
|
||||||
| Map of (ae * ae) list
|
| Map of (ae * ae) list
|
||||||
|
| LookUp of (ae * ae)
|
||||||
|
|
||||||
and value = annotated_expression (* todo (for refactoring) *)
|
and value = annotated_expression (* todo (for refactoring) *)
|
||||||
|
|
||||||
@ -98,7 +99,7 @@ and matching =
|
|||||||
}
|
}
|
||||||
| Match_option of {
|
| Match_option of {
|
||||||
match_none : b ;
|
match_none : b ;
|
||||||
match_some : name * b ;
|
match_some : (name * type_value) * b ;
|
||||||
}
|
}
|
||||||
| Match_tuple of name list * b
|
| Match_tuple of name list * b
|
||||||
|
|
||||||
@ -163,6 +164,7 @@ module PP = struct
|
|||||||
| Record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s
|
| Record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s
|
||||||
| Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
|
| Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
|
||||||
| Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m
|
| Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m
|
||||||
|
| LookUp (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i
|
||||||
|
|
||||||
and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
|
and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
|
||||||
fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
|
fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
|
||||||
@ -189,7 +191,7 @@ module PP = struct
|
|||||||
| Match_list {match_nil ; match_cons = (hd, tl, match_cons)} ->
|
| Match_list {match_nil ; match_cons = (hd, tl, match_cons)} ->
|
||||||
fprintf ppf "| Nil -> %a @.| %s :: %s -> %a" block match_nil hd tl block match_cons
|
fprintf ppf "| Nil -> %a @.| %s :: %s -> %a" block match_nil hd tl block match_cons
|
||||||
| Match_option {match_none ; match_some = (some, match_some)} ->
|
| Match_option {match_none ; match_some = (some, match_some)} ->
|
||||||
fprintf ppf "| None -> %a @.| Some %s -> %a" block match_none some block match_some
|
fprintf ppf "| None -> %a @.| Some %s -> %a" block match_none (fst some) block match_some
|
||||||
|
|
||||||
and instruction ppf (i:instruction) = match i with
|
and instruction ppf (i:instruction) = match i with
|
||||||
| Skip -> fprintf ppf "skip"
|
| Skip -> fprintf ppf "skip"
|
||||||
@ -381,8 +383,7 @@ let merge_annotation (a:type_value option) (b:type_value option) : type_value re
|
|||||||
let%bind _ = assert_type_value_eq (a, b) in
|
let%bind _ = assert_type_value_eq (a, b) in
|
||||||
match a.simplified, b.simplified with
|
match a.simplified, b.simplified with
|
||||||
| _, None -> ok a
|
| _, None -> ok a
|
||||||
| None, Some _ -> ok b
|
| _, Some _ -> ok b
|
||||||
| _ -> simple_fail "both have simplified ASTs"
|
|
||||||
|
|
||||||
module Combinators = struct
|
module Combinators = struct
|
||||||
|
|
||||||
@ -406,6 +407,9 @@ module Combinators = struct
|
|||||||
let simplify_t_unit s = t_unit (Some s)
|
let simplify_t_unit s = t_unit (Some s)
|
||||||
let make_t_unit = t_unit None
|
let make_t_unit = t_unit None
|
||||||
|
|
||||||
|
let t_option o s : type_value = type_value (Type_constant ("option", [o])) s
|
||||||
|
let make_t_option o = t_option o None
|
||||||
|
|
||||||
let t_tuple lst s : type_value = type_value (Type_tuple lst) s
|
let t_tuple lst s : type_value = type_value (Type_tuple lst) s
|
||||||
let simplify_t_tuple lst s = t_tuple lst (Some s)
|
let simplify_t_tuple lst s = t_tuple lst (Some s)
|
||||||
let make_t_tuple lst = t_tuple lst None
|
let make_t_tuple lst = t_tuple lst None
|
||||||
@ -460,11 +464,18 @@ module Combinators = struct
|
|||||||
| Type_record m -> ok m
|
| Type_record m -> ok m
|
||||||
| _ -> simple_fail "not a record"
|
| _ -> simple_fail "not a record"
|
||||||
|
|
||||||
|
let get_t_map (t:type_value) : (type_value * type_value) result =
|
||||||
|
match t.type_value with
|
||||||
|
| Type_constant ("map", [k;v]) -> ok (k, v)
|
||||||
|
| _ -> simple_fail "not a map"
|
||||||
|
|
||||||
let record map : expression = Record map
|
let record map : expression = Record map
|
||||||
let record_ez (lst : (string * ae) list) : expression =
|
let record_ez (lst : (string * ae) list) : expression =
|
||||||
let aux prev (k, v) = SMap.add k v prev in
|
let aux prev (k, v) = SMap.add k v prev in
|
||||||
let map = List.fold_left aux SMap.empty lst in
|
let map = List.fold_left aux SMap.empty lst in
|
||||||
record map
|
record map
|
||||||
|
let some s : expression = Constant ("SOME", [s])
|
||||||
|
let none : expression = Constant ("NONE", [])
|
||||||
|
|
||||||
let map lst : expression = Map lst
|
let map lst : expression = Map lst
|
||||||
|
|
||||||
@ -477,6 +488,8 @@ module Combinators = struct
|
|||||||
let a_int n = annotated_expression (int n) make_t_int
|
let a_int n = annotated_expression (int n) make_t_int
|
||||||
let a_bool b = annotated_expression (bool b) make_t_bool
|
let a_bool b = annotated_expression (bool b) make_t_bool
|
||||||
let a_pair a b = annotated_expression (pair a b) (make_t_pair a.type_annotation b.type_annotation)
|
let a_pair a b = annotated_expression (pair a b) (make_t_pair a.type_annotation b.type_annotation)
|
||||||
|
let a_some s = annotated_expression (some s) (make_t_option s.type_annotation)
|
||||||
|
let a_none t = annotated_expression none (make_t_option t)
|
||||||
let a_tuple lst = annotated_expression (Tuple lst) (make_t_tuple (List.map get_type_annotation lst))
|
let a_tuple lst = annotated_expression (Tuple lst) (make_t_tuple (List.map get_type_annotation lst))
|
||||||
let a_record r = annotated_expression (record r) (make_t_record (SMap.map get_type_annotation r))
|
let a_record r = annotated_expression (record r) (make_t_record (SMap.map get_type_annotation r))
|
||||||
let a_record_ez r = annotated_expression (record_ez r) (make_t_record_ez (List.map (fun (x, y) -> x, y.type_annotation) r))
|
let a_record_ez r = annotated_expression (record_ez r) (make_t_record_ez (List.map (fun (x, y) -> x, y.type_annotation) r))
|
||||||
|
19
src/ligo/contracts/map.ligo
Normal file
19
src/ligo/contracts/map.ligo
Normal file
@ -0,0 +1,19 @@
|
|||||||
|
type foobar is map(int, int)
|
||||||
|
|
||||||
|
const fb : foobar = map
|
||||||
|
23 -> 0 ;
|
||||||
|
42 -> 0 ;
|
||||||
|
end
|
||||||
|
|
||||||
|
function get (const m : foobar) : int is
|
||||||
|
begin
|
||||||
|
skip
|
||||||
|
end with m[42] + m[23]
|
||||||
|
|
||||||
|
const bm : foobar = map
|
||||||
|
144 -> 23 ;
|
||||||
|
51 -> 23 ;
|
||||||
|
42 -> 23 ;
|
||||||
|
120 -> 23 ;
|
||||||
|
421 -> 23 ;
|
||||||
|
end
|
@ -1,8 +1,17 @@
|
|||||||
function main (const i : int) : int is
|
function match_bool (const i : int) : int is
|
||||||
var result : int := 23 ;
|
var result : int := 23 ;
|
||||||
begin
|
begin
|
||||||
if i = 2 then
|
case i = 2 of
|
||||||
result := 42
|
| True -> result := 42
|
||||||
else
|
| False -> result := 0
|
||||||
result := 0
|
end
|
||||||
|
end with result
|
||||||
|
|
||||||
|
function match_option (const o : option(int)) : int is
|
||||||
|
var result : int := 23 ;
|
||||||
|
begin
|
||||||
|
case o of
|
||||||
|
| None -> skip
|
||||||
|
| Some(s) -> result := s
|
||||||
|
end
|
||||||
end with result
|
end with result
|
||||||
|
4
src/ligo/contracts/option.ligo
Normal file
4
src/ligo/contracts/option.ligo
Normal file
@ -0,0 +1,4 @@
|
|||||||
|
type foobar is option(int)
|
||||||
|
|
||||||
|
const s : foobar = Some(42)
|
||||||
|
const n : foobar = None
|
@ -85,8 +85,8 @@ let parse_expression (s:string) : AST_Raw.expr result =
|
|||||||
) >>? fun raw ->
|
) >>? fun raw ->
|
||||||
ok raw
|
ok raw
|
||||||
|
|
||||||
let simplify (p:AST_Raw.t) : Ast_simplified.program result = AST_Simplified.Simplify.simpl_program p
|
let simplify (p:AST_Raw.t) : Ast_simplified.program result = Simplify.simpl_program p
|
||||||
let simplify_expr (e:AST_Raw.expr) : Ast_simplified.annotated_expression result = AST_Simplified.Simplify.simpl_expression e
|
let simplify_expr (e:AST_Raw.expr) : Ast_simplified.annotated_expression result = Simplify.simpl_expression e
|
||||||
let unparse_simplified_expr (e:AST_Simplified.annotated_expression) : string result =
|
let unparse_simplified_expr (e:AST_Simplified.annotated_expression) : string result =
|
||||||
ok @@ Format.asprintf "%a" AST_Simplified.PP.annotated_expression e
|
ok @@ Format.asprintf "%a" AST_Simplified.PP.annotated_expression e
|
||||||
|
|
||||||
|
@ -26,6 +26,7 @@ type type_value = [
|
|||||||
| `Shallow_closure of environment * type_value * type_value
|
| `Shallow_closure of environment * type_value * type_value
|
||||||
| `Base of type_base
|
| `Base of type_base
|
||||||
| `Map of type_value * type_value
|
| `Map of type_value * type_value
|
||||||
|
| `Option of type_value
|
||||||
]
|
]
|
||||||
|
|
||||||
and environment_element = string * type_value
|
and environment_element = string * type_value
|
||||||
@ -54,6 +55,8 @@ type value = [
|
|||||||
| `Pair of value * value
|
| `Pair of value * value
|
||||||
| `Left of value
|
| `Left of value
|
||||||
| `Right of value
|
| `Right of value
|
||||||
|
| `Some of value
|
||||||
|
| `None
|
||||||
(* | `Macro of anon_macro ... The future. *)
|
(* | `Macro of anon_macro ... The future. *)
|
||||||
| `Function of anon_function
|
| `Function of anon_function
|
||||||
]
|
]
|
||||||
@ -64,6 +67,8 @@ and expression' =
|
|||||||
| Predicate of string * expression list
|
| Predicate of string * expression list
|
||||||
| Apply of expression * expression
|
| Apply of expression * expression
|
||||||
| Var of var_name
|
| Var of var_name
|
||||||
|
| Empty_map of (type_value * type_value)
|
||||||
|
| Make_None of type_value
|
||||||
|
|
||||||
and expression = expression' * type_value * environment (* Environment in which the expressions are evaluated *)
|
and expression = expression' * type_value * environment (* Environment in which the expressions are evaluated *)
|
||||||
|
|
||||||
@ -72,6 +77,7 @@ and assignment = var_name * expression
|
|||||||
and statement' =
|
and statement' =
|
||||||
| Assignment of assignment
|
| Assignment of assignment
|
||||||
| Cond of expression * block * block
|
| Cond of expression * block * block
|
||||||
|
| If_None of expression * block * (var_name * block)
|
||||||
| While of expression * block
|
| While of expression * block
|
||||||
|
|
||||||
and statement = statement' * environment_wrap
|
and statement = statement' * environment_wrap
|
||||||
@ -125,6 +131,7 @@ module PP = struct
|
|||||||
| `Base b -> type_base ppf b
|
| `Base b -> type_base ppf b
|
||||||
| `Function(a, b) -> fprintf ppf "(%a) -> (%a)" type_ a type_ b
|
| `Function(a, b) -> fprintf ppf "(%a) -> (%a)" type_ a type_ b
|
||||||
| `Map(k, v) -> fprintf ppf "map(%a -> %a)" type_ k type_ v
|
| `Map(k, v) -> fprintf ppf "map(%a -> %a)" type_ k type_ v
|
||||||
|
| `Option(o) -> fprintf ppf "option(%a)" type_ o
|
||||||
| `Shallow_closure(_, a, b) -> fprintf ppf "[big_closure](%a) -> (%a)" type_ a type_ b
|
| `Shallow_closure(_, a, b) -> fprintf ppf "[big_closure](%a) -> (%a)" type_ a type_ b
|
||||||
| `Deep_closure(c, arg, ret) ->
|
| `Deep_closure(c, arg, ret) ->
|
||||||
fprintf ppf "[%a](%a)->(%a)"
|
fprintf ppf "[%a](%a)->(%a)"
|
||||||
@ -156,6 +163,8 @@ module PP = struct
|
|||||||
| `Left a -> fprintf ppf "L(%a)" value a
|
| `Left a -> fprintf ppf "L(%a)" value a
|
||||||
| `Right b -> fprintf ppf "R(%a)" value b
|
| `Right b -> fprintf ppf "R(%a)" value b
|
||||||
| `Function x -> function_ ppf x.content
|
| `Function x -> function_ ppf x.content
|
||||||
|
| `None -> fprintf ppf "None"
|
||||||
|
| `Some s -> fprintf ppf "Some (%a)" value s
|
||||||
|
|
||||||
and expression ppf ((e, _, _):expression) = match e with
|
and expression ppf ((e, _, _):expression) = match e with
|
||||||
| Var v -> fprintf ppf "%s" v
|
| Var v -> fprintf ppf "%s" v
|
||||||
@ -163,6 +172,8 @@ module PP = struct
|
|||||||
| Predicate(p, lst) -> fprintf ppf "%s %a" p (pp_print_list ~pp_sep:space_sep expression) lst
|
| Predicate(p, lst) -> fprintf ppf "%s %a" p (pp_print_list ~pp_sep:space_sep expression) lst
|
||||||
| Literal v -> fprintf ppf "%a" value v
|
| Literal v -> fprintf ppf "%a" value v
|
||||||
| Function_expression c -> function_ ppf c
|
| Function_expression c -> function_ ppf c
|
||||||
|
| Empty_map _ -> fprintf ppf "map[]"
|
||||||
|
| Make_None _ -> fprintf ppf "none"
|
||||||
|
|
||||||
and function_ ppf ({binder ; input ; output ; body ; result}:anon_function_content) =
|
and function_ ppf ({binder ; input ; output ; body ; result}:anon_function_content) =
|
||||||
fprintf ppf "fun (%s:%a) : %a %a return %a"
|
fprintf ppf "fun (%s:%a) : %a %a return %a"
|
||||||
@ -177,6 +188,7 @@ module PP = struct
|
|||||||
and statement ppf ((s, _) : statement) = match s with
|
and statement ppf ((s, _) : statement) = match s with
|
||||||
| Assignment ass -> assignment ppf ass
|
| Assignment ass -> assignment ppf ass
|
||||||
| Cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e
|
| Cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e
|
||||||
|
| If_None (expr, none, (name, some)) -> fprintf ppf "if (%a) %a %s.%a" expression expr block none name block some
|
||||||
| While (e, b) -> fprintf ppf "while (%a) %a" expression e block b
|
| While (e, b) -> fprintf ppf "while (%a) %a" expression e block b
|
||||||
|
|
||||||
and block ppf ((b, _):block) =
|
and block ppf ((b, _):block) =
|
||||||
@ -188,46 +200,6 @@ module PP = struct
|
|||||||
fprintf ppf "Program:\n---\n%a" (pp_print_list ~pp_sep:pp_print_newline tl_statement) p
|
fprintf ppf "Program:\n---\n%a" (pp_print_list ~pp_sep:pp_print_newline tl_statement) p
|
||||||
end
|
end
|
||||||
|
|
||||||
module Free_variables = struct
|
|
||||||
type free_variable = string
|
|
||||||
type free_variables = free_variable list
|
|
||||||
type t' = free_variable
|
|
||||||
type t = free_variables
|
|
||||||
|
|
||||||
let append_wd (* without doubles *) double x t =
|
|
||||||
if List.mem x double
|
|
||||||
then t
|
|
||||||
else x :: t
|
|
||||||
|
|
||||||
let append_bound x t = append_wd t x t
|
|
||||||
|
|
||||||
let rec expression' (bound:t) : expression' -> t = function
|
|
||||||
| Literal _ -> []
|
|
||||||
| Var x -> append_wd bound x []
|
|
||||||
| Predicate(_, exprs) -> List.(concat @@ map (expression bound) exprs)
|
|
||||||
| Apply(a, b) -> List.(concat @@ map (expression bound) [a;b])
|
|
||||||
| Function_expression {binder;body;result} -> block (binder :: bound) body @ expression (binder :: bound) result
|
|
||||||
|
|
||||||
and expression bound (expr, _, _) = expression' bound expr
|
|
||||||
|
|
||||||
and statement bound ((s, _) : statement) : (t * t) = match s with
|
|
||||||
| Assignment (n, e) -> append_bound n bound, expression bound e
|
|
||||||
| Cond (e, a, b) -> bound, (expression bound e) @ (block bound a) @ (block bound b)
|
|
||||||
| While (e, b) -> bound, (expression bound e) @ (block bound b)
|
|
||||||
|
|
||||||
and block' bound (b:block') : t = match b with
|
|
||||||
| [] -> []
|
|
||||||
| hd :: tl ->
|
|
||||||
let (bound, fv) = statement bound hd in
|
|
||||||
let fv' = block' bound tl in
|
|
||||||
fv @ fv'
|
|
||||||
|
|
||||||
and block bound (b, _ : block) : t = block' bound b
|
|
||||||
|
|
||||||
let function_ ({content = {body ; binder ; result}} : anon_function) : t =
|
|
||||||
block [binder] body @ expression [binder] result
|
|
||||||
end
|
|
||||||
|
|
||||||
module Translate_type = struct
|
module Translate_type = struct
|
||||||
open Tezos_utils.Micheline.Michelson
|
open Tezos_utils.Micheline.Michelson
|
||||||
|
|
||||||
@ -251,10 +223,11 @@ module Translate_type = struct
|
|||||||
| `Base b -> comparable_type_base b
|
| `Base b -> comparable_type_base b
|
||||||
| `Deep_closure _ -> fail (not_comparable "deep closure")
|
| `Deep_closure _ -> fail (not_comparable "deep closure")
|
||||||
| `Shallow_closure _ -> fail (not_comparable "shallow closure")
|
| `Shallow_closure _ -> fail (not_comparable "shallow closure")
|
||||||
| `Function _ -> fail (not_comparable "function closure")
|
| `Function _ -> fail (not_comparable "function")
|
||||||
| `Or _ -> fail (not_comparable "or closure")
|
| `Or _ -> fail (not_comparable "or")
|
||||||
| `Pair _ -> fail (not_comparable "pair closure")
|
| `Pair _ -> fail (not_comparable "pair")
|
||||||
| `Map _ -> fail (not_comparable "map closure")
|
| `Map _ -> fail (not_comparable "map")
|
||||||
|
| `Option _ -> fail (not_comparable "option")
|
||||||
|
|
||||||
let base_type : type_base -> ex_ty result = fun b ->
|
let base_type : type_base -> ex_ty result = fun b ->
|
||||||
let open Types in
|
let open Types in
|
||||||
@ -299,6 +272,9 @@ module Translate_type = struct
|
|||||||
let%bind (Ex_comparable_ty k') = comparable_type k in
|
let%bind (Ex_comparable_ty k') = comparable_type k in
|
||||||
let%bind (Ex_ty v') = type_ v in
|
let%bind (Ex_ty v') = type_ v in
|
||||||
ok @@ Ex_ty Types.(map k' v')
|
ok @@ Ex_ty Types.(map k' v')
|
||||||
|
| `Option t ->
|
||||||
|
let%bind (Ex_ty t') = type_ t in
|
||||||
|
ok @@ Ex_ty Types.(option t')
|
||||||
|
|
||||||
|
|
||||||
and environment_small' = let open Append_tree in function
|
and environment_small' = let open Append_tree in function
|
||||||
@ -347,6 +323,9 @@ module Translate_type = struct
|
|||||||
| `Map kv ->
|
| `Map kv ->
|
||||||
let%bind (k', v') = bind_map_pair type_ kv in
|
let%bind (k', v') = bind_map_pair type_ kv in
|
||||||
ok @@ prim ~children:[k';v'] T_map
|
ok @@ prim ~children:[k';v'] T_map
|
||||||
|
| `Option o ->
|
||||||
|
let%bind o' = type_ o in
|
||||||
|
ok @@ prim ~children:[o'] T_option
|
||||||
| `Function (arg, ret) ->
|
| `Function (arg, ret) ->
|
||||||
let%bind arg = type_ arg in
|
let%bind arg = type_ arg in
|
||||||
let%bind ret = type_ ret in
|
let%bind ret = type_ ret in
|
||||||
@ -646,6 +625,10 @@ module Translate_program = struct
|
|||||||
| Binary of michelson
|
| Binary of michelson
|
||||||
| Ternary of michelson
|
| Ternary of michelson
|
||||||
|
|
||||||
|
let simple_constant c = Constant ( seq [
|
||||||
|
c ; i_pair ;
|
||||||
|
])
|
||||||
|
|
||||||
let simple_unary c = Unary ( seq [
|
let simple_unary c = Unary ( seq [
|
||||||
i_unpair ; c ; i_pair ;
|
i_unpair ; c ; i_pair ;
|
||||||
])
|
])
|
||||||
@ -654,6 +637,10 @@ module Translate_program = struct
|
|||||||
i_unpair ; dip i_unpair ; i_swap ; c ; i_pair ;
|
i_unpair ; dip i_unpair ; i_swap ; c ; i_pair ;
|
||||||
])
|
])
|
||||||
|
|
||||||
|
let simple_ternary c = Ternary ( seq [
|
||||||
|
i_unpair ; dip i_unpair ; dip (dip i_unpair) ; i_swap ; dip i_swap ; i_swap ; c ; i_pair ;
|
||||||
|
])
|
||||||
|
|
||||||
let rec get_predicate : string -> predicate result = function
|
let rec get_predicate : string -> predicate result = function
|
||||||
| "ADD_INT" -> ok @@ simple_binary @@ prim I_ADD
|
| "ADD_INT" -> ok @@ simple_binary @@ prim I_ADD
|
||||||
| "NEG" -> ok @@ simple_unary @@ prim I_NEG
|
| "NEG" -> ok @@ simple_unary @@ prim I_NEG
|
||||||
@ -663,6 +650,8 @@ module Translate_program = struct
|
|||||||
| "CAR" -> ok @@ simple_unary @@ prim I_CAR
|
| "CAR" -> ok @@ simple_unary @@ prim I_CAR
|
||||||
| "CDR" -> ok @@ simple_unary @@ prim I_CDR
|
| "CDR" -> ok @@ simple_unary @@ prim I_CDR
|
||||||
| "EQ" -> ok @@ simple_binary @@ seq [prim I_COMPARE ; prim I_EQ]
|
| "EQ" -> ok @@ simple_binary @@ seq [prim I_COMPARE ; prim I_EQ]
|
||||||
|
| "UPDATE" -> ok @@ simple_ternary @@ prim I_UPDATE
|
||||||
|
| "SOME" -> ok @@ simple_unary @@ prim I_SOME
|
||||||
| x -> simple_fail @@ "predicate \"" ^ x ^ "\" doesn't exist"
|
| x -> simple_fail @@ "predicate \"" ^ x ^ "\" doesn't exist"
|
||||||
|
|
||||||
and translate_value (v:value) : michelson result = match v with
|
and translate_value (v:value) : michelson result = match v with
|
||||||
@ -680,6 +669,10 @@ module Translate_program = struct
|
|||||||
| `Left a -> translate_value a >>? fun a -> ok @@ prim ~children:[a] D_Left
|
| `Left a -> translate_value a >>? fun a -> ok @@ prim ~children:[a] D_Left
|
||||||
| `Right b -> translate_value b >>? fun b -> ok @@ prim ~children:[b] D_Right
|
| `Right b -> translate_value b >>? fun b -> ok @@ prim ~children:[b] D_Right
|
||||||
| `Function anon -> translate_function anon
|
| `Function anon -> translate_function anon
|
||||||
|
| `None -> ok @@ prim D_None
|
||||||
|
| `Some s ->
|
||||||
|
let%bind s' = translate_value s in
|
||||||
|
ok @@ prim ~children:[s'] D_Some
|
||||||
|
|
||||||
and translate_function ({capture;content}:anon_function) : michelson result =
|
and translate_function ({capture;content}:anon_function) : michelson result =
|
||||||
let {capture_type } = content in
|
let {capture_type } = content in
|
||||||
@ -766,6 +759,20 @@ module Translate_program = struct
|
|||||||
| _ -> simple_fail "bad arity"
|
| _ -> simple_fail "bad arity"
|
||||||
in
|
in
|
||||||
ok code
|
ok code
|
||||||
|
| Empty_map sd ->
|
||||||
|
let%bind (src, dst) = bind_map_pair Translate_type.type_ sd in
|
||||||
|
let code = seq [
|
||||||
|
prim ~children:[src;dst] I_EMPTY_MAP ;
|
||||||
|
i_pair ;
|
||||||
|
] in
|
||||||
|
ok code
|
||||||
|
| Make_None o ->
|
||||||
|
let%bind o' = Translate_type.type_ o in
|
||||||
|
let code = seq [
|
||||||
|
prim ~children:[o'] I_NONE ;
|
||||||
|
i_pair ;
|
||||||
|
] in
|
||||||
|
ok code
|
||||||
| Function_expression anon -> (
|
| Function_expression anon -> (
|
||||||
match ty with
|
match ty with
|
||||||
| `Function (_, _) ->
|
| `Function (_, _) ->
|
||||||
@ -861,12 +868,27 @@ module Translate_program = struct
|
|||||||
let%bind a = translate_regular_block a in
|
let%bind a = translate_regular_block a in
|
||||||
let%bind b = translate_regular_block b in
|
let%bind b = translate_regular_block b in
|
||||||
ok @@ (seq [
|
ok @@ (seq [
|
||||||
prim ~children:[prim T_unit ; prim D_Unit] I_PUSH ;
|
i_push_unit ;
|
||||||
expr ;
|
expr ;
|
||||||
prim I_CAR ;
|
prim I_CAR ;
|
||||||
dip Environment.to_michelson_extend ;
|
dip Environment.to_michelson_extend ;
|
||||||
prim ~children:[seq [a ; Environment.to_michelson_restrict];seq [b ; Environment.to_michelson_restrict]] I_IF ;
|
prim ~children:[seq [a ; Environment.to_michelson_restrict];seq [b ; Environment.to_michelson_restrict]] I_IF ;
|
||||||
])
|
])
|
||||||
|
| If_None (expr, none, (_, some)) ->
|
||||||
|
let%bind expr = translate_expression expr in
|
||||||
|
let%bind none' = translate_regular_block none in
|
||||||
|
let%bind some' = translate_regular_block some in
|
||||||
|
let%bind add =
|
||||||
|
let env = Environment.extend w_env.pre_environment in
|
||||||
|
Environment.to_michelson_anonymous_add env in
|
||||||
|
ok @@ (seq [
|
||||||
|
i_push_unit ; expr ; i_car ;
|
||||||
|
dip Environment.to_michelson_extend ;
|
||||||
|
prim ~children:[
|
||||||
|
seq [none' ; Environment.to_michelson_restrict] ;
|
||||||
|
seq [add ; some' ; Environment.to_michelson_restrict] ;
|
||||||
|
] I_IF_NONE
|
||||||
|
])
|
||||||
| While ((_, _, _) as expr, block) ->
|
| While ((_, _, _) as expr, block) ->
|
||||||
let%bind expr = translate_expression expr in
|
let%bind expr = translate_expression expr in
|
||||||
let%bind block = translate_regular_block block in
|
let%bind block = translate_regular_block block in
|
||||||
@ -984,6 +1006,11 @@ module Translate_ir = struct
|
|||||||
ok @@ `Bool b
|
ok @@ `Bool b
|
||||||
| (Unit_t _), () ->
|
| (Unit_t _), () ->
|
||||||
ok @@ `Unit
|
ok @@ `Unit
|
||||||
|
| (Option_t _), None ->
|
||||||
|
ok @@ `None
|
||||||
|
| (Option_t ((o_ty, _), _, _)), Some s ->
|
||||||
|
let%bind s' = translate_value @@ Ex_typed_value (o_ty, s) in
|
||||||
|
ok @@ `Some s'
|
||||||
| _ -> simple_fail "this value can't be transpiled back yet"
|
| _ -> simple_fail "this value can't be transpiled back yet"
|
||||||
end
|
end
|
||||||
|
|
||||||
@ -1065,7 +1092,16 @@ module Combinators = struct
|
|||||||
|
|
||||||
let get_unit (v:value) = match v with
|
let get_unit (v:value) = match v with
|
||||||
| `Unit -> ok ()
|
| `Unit -> ok ()
|
||||||
| _ -> simple_fail "not a bool"
|
| _ -> simple_fail "not a unit"
|
||||||
|
|
||||||
|
let get_option (v:value) = match v with
|
||||||
|
| `None -> ok None
|
||||||
|
| `Some s -> ok (Some s)
|
||||||
|
| _ -> simple_fail "not an option"
|
||||||
|
|
||||||
|
let get_t_option (v:type_value) = match v with
|
||||||
|
| `Option t -> ok t
|
||||||
|
| _ -> simple_fail "not an option"
|
||||||
|
|
||||||
let get_pair (v:value) = match v with
|
let get_pair (v:value) = match v with
|
||||||
| `Pair (a, b) -> ok (a, b)
|
| `Pair (a, b) -> ok (a, b)
|
||||||
@ -1130,6 +1166,7 @@ module Combinators = struct
|
|||||||
let statement s' e : statement =
|
let statement s' e : statement =
|
||||||
match s' with
|
match s' with
|
||||||
| Cond _ -> s', id_environment_wrap e
|
| Cond _ -> s', id_environment_wrap e
|
||||||
|
| If_None _ -> s', id_environment_wrap e
|
||||||
| While _ -> s', id_environment_wrap e
|
| While _ -> s', id_environment_wrap e
|
||||||
| Assignment (name, (_, t, _)) -> s', environment_wrap e (Environment.add (name, t) e)
|
| Assignment (name, (_, t, _)) -> s', environment_wrap e (Environment.add (name, t) e)
|
||||||
|
|
||||||
|
457
src/ligo/simplify.ml
Normal file
457
src/ligo/simplify.ml
Normal file
@ -0,0 +1,457 @@
|
|||||||
|
open Ligo_helpers.Trace
|
||||||
|
open Ast_simplified
|
||||||
|
module Raw = Ligo_parser.AST
|
||||||
|
|
||||||
|
let nseq_to_list (hd, tl) = hd :: tl
|
||||||
|
let npseq_to_list (hd, tl) = hd :: (List.map snd tl)
|
||||||
|
let npseq_to_nelist (hd, tl) = hd, (List.map snd tl)
|
||||||
|
let pseq_to_list = function
|
||||||
|
| None -> []
|
||||||
|
| Some lst -> npseq_to_list lst
|
||||||
|
let get_value : 'a Raw.reg -> 'a = fun x -> x.value
|
||||||
|
|
||||||
|
let type_constants = [
|
||||||
|
("unit", 0) ;
|
||||||
|
("nat", 0) ;
|
||||||
|
("int", 0) ;
|
||||||
|
("bool", 0) ;
|
||||||
|
("list", 1) ;
|
||||||
|
("option", 1) ;
|
||||||
|
("set", 1) ;
|
||||||
|
("map", 2) ;
|
||||||
|
]
|
||||||
|
|
||||||
|
let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
|
||||||
|
match t with
|
||||||
|
| TPar x -> simpl_type_expression x.value.inside
|
||||||
|
| TAlias v -> (
|
||||||
|
match List.assoc_opt v.value type_constants with
|
||||||
|
| Some 0 ->
|
||||||
|
ok @@ Type_constant (v.value, [])
|
||||||
|
| Some _ ->
|
||||||
|
simple_fail "type constructor with wrong number of args"
|
||||||
|
| None ->
|
||||||
|
ok @@ Type_variable v.value
|
||||||
|
)
|
||||||
|
| TApp x ->
|
||||||
|
let (name, tuple) = x.value in
|
||||||
|
let lst = npseq_to_list tuple.value.inside in
|
||||||
|
let%bind _ = match List.assoc_opt name.value type_constants with
|
||||||
|
| Some n when n = List.length lst -> ok ()
|
||||||
|
| Some _ -> simple_fail "type constructor with wrong number of args"
|
||||||
|
| None -> simple_fail "unrecognized type constants" in
|
||||||
|
let%bind lst' = bind_list @@ List.map simpl_type_expression lst in
|
||||||
|
ok @@ Type_constant (name.value, lst')
|
||||||
|
| TProd p ->
|
||||||
|
let%bind tpl = simpl_list_type_expression
|
||||||
|
@@ npseq_to_list p.value in
|
||||||
|
ok tpl
|
||||||
|
| TRecord r ->
|
||||||
|
let aux = fun (x, y) -> let%bind y = simpl_type_expression y in ok (x, y) in
|
||||||
|
let%bind lst = bind_list
|
||||||
|
@@ List.map aux
|
||||||
|
@@ List.map (fun (x:Raw.field_decl Raw.reg) -> (x.value.field_name.value, x.value.field_type))
|
||||||
|
@@ npseq_to_list r.value.field_decls in
|
||||||
|
let m = List.fold_left (fun m (x, y) -> SMap.add x y m) SMap.empty lst in
|
||||||
|
ok @@ Type_record m
|
||||||
|
| TSum s ->
|
||||||
|
let aux (v:Raw.variant Raw.reg) =
|
||||||
|
let%bind te = simpl_list_type_expression
|
||||||
|
@@ npseq_to_list v.value.product.value in
|
||||||
|
ok (v.value.constr.value, te)
|
||||||
|
in
|
||||||
|
let%bind lst = bind_list
|
||||||
|
@@ List.map aux
|
||||||
|
@@ npseq_to_list s.value in
|
||||||
|
let m = List.fold_left (fun m (x, y) -> SMap.add x y m) SMap.empty lst in
|
||||||
|
ok @@ Type_sum m
|
||||||
|
|
||||||
|
and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result =
|
||||||
|
match lst with
|
||||||
|
| [] -> assert false
|
||||||
|
| [hd] -> simpl_type_expression hd
|
||||||
|
| lst ->
|
||||||
|
let%bind lst = bind_list @@ List.map simpl_type_expression lst in
|
||||||
|
ok @@ Type_tuple lst
|
||||||
|
|
||||||
|
let rec simpl_expression (t:Raw.expr) : ae result =
|
||||||
|
let return x = ok @@ ae x in
|
||||||
|
let simpl_projection = fun (p:Raw.projection) ->
|
||||||
|
let var =
|
||||||
|
let name = p.record_name.value in
|
||||||
|
ae @@ Variable name in
|
||||||
|
let path = p.field_path in
|
||||||
|
let path' =
|
||||||
|
let aux (s:Raw.selection) =
|
||||||
|
match s with
|
||||||
|
| FieldName property -> Record_access property.value
|
||||||
|
| Component index -> Tuple_access (Z.to_int (snd index.value))
|
||||||
|
in
|
||||||
|
List.map aux @@ npseq_to_list path in
|
||||||
|
ok @@ ae @@ Accessor (var, path')
|
||||||
|
in
|
||||||
|
match t with
|
||||||
|
| EVar c ->
|
||||||
|
if c.value = "unit"
|
||||||
|
then ok @@ ae @@ Literal Unit
|
||||||
|
else ok @@ ae @@ Variable c.value
|
||||||
|
| ECall x ->
|
||||||
|
let (name, args) = x.value in
|
||||||
|
let f = name.value in
|
||||||
|
let%bind arg = simpl_list_expression
|
||||||
|
@@ npseq_to_list args.value.inside in
|
||||||
|
ok @@ ae @@ Application (ae @@ Variable f, arg)
|
||||||
|
| EPar x -> simpl_expression x.value.inside
|
||||||
|
| EUnit _ -> ok @@ ae @@ Literal Unit
|
||||||
|
| EBytes x -> ok @@ ae @@ Literal (Bytes (Bytes.of_string @@ fst x.value))
|
||||||
|
| ETuple tpl ->
|
||||||
|
let (Raw.TupleInj tpl') = tpl in
|
||||||
|
simpl_list_expression
|
||||||
|
@@ npseq_to_list tpl'.value.inside
|
||||||
|
| ERecord (RecordInj r) ->
|
||||||
|
let%bind fields = bind_list
|
||||||
|
@@ List.map (fun ((k : _ Raw.reg), v) -> let%bind v = simpl_expression v in ok (k.value, v))
|
||||||
|
@@ List.map (fun (x:Raw.field_assign Raw.reg) -> (x.value.field_name, x.value.field_expr))
|
||||||
|
@@ npseq_to_list r.value.fields in
|
||||||
|
let aux prev (k, v) = SMap.add k v prev in
|
||||||
|
ok @@ ae @@ Record (List.fold_left aux SMap.empty fields)
|
||||||
|
| EProj p' -> (
|
||||||
|
let p = p'.value in
|
||||||
|
simpl_projection p
|
||||||
|
)
|
||||||
|
| EConstr (ConstrApp c) ->
|
||||||
|
let (c, args) = c.value in
|
||||||
|
let%bind arg =
|
||||||
|
simpl_list_expression
|
||||||
|
@@ npseq_to_list args.value.inside in
|
||||||
|
ok @@ ae @@ Constructor (c.value, arg)
|
||||||
|
| EConstr (SomeApp a) ->
|
||||||
|
let (_, args) = a.value in
|
||||||
|
let%bind arg =
|
||||||
|
simpl_list_expression
|
||||||
|
@@ npseq_to_list args.value.inside in
|
||||||
|
ok @@ ae @@ Constant ("SOME", [arg])
|
||||||
|
| EConstr (NoneExpr n) ->
|
||||||
|
let type_expr = n.value.inside.opt_type in
|
||||||
|
let%bind type_expr' = simpl_type_expression type_expr in
|
||||||
|
ok @@ annotated_expression (Constant ("NONE", [])) (Some (Combinators.t_option type_expr'))
|
||||||
|
| EArith (Add c) ->
|
||||||
|
simpl_binop "ADD" c.value
|
||||||
|
| EArith (Int n) ->
|
||||||
|
let n = Z.to_int @@ snd @@ n.value in
|
||||||
|
ok @@ ae @@ Literal (Number n)
|
||||||
|
| EArith _ -> simple_fail "arith: not supported yet"
|
||||||
|
| EString (String s) ->
|
||||||
|
ok @@ ae @@ Literal (String s.value)
|
||||||
|
| EString _ -> simple_fail "string: not supported yet"
|
||||||
|
| ELogic l -> simpl_logic_expression l
|
||||||
|
| EList _ -> simple_fail "list: not supported yet"
|
||||||
|
| ESet _ -> simple_fail "set: not supported yet"
|
||||||
|
| EMap (MapInj mi) ->
|
||||||
|
let%bind lst =
|
||||||
|
let lst = List.map get_value @@ pseq_to_list mi.value.elements in
|
||||||
|
let aux : Raw.binding -> (ae * ae) result = fun b ->
|
||||||
|
let%bind src = simpl_expression b.source in
|
||||||
|
let%bind dst = simpl_expression b.image in
|
||||||
|
ok (src, dst) in
|
||||||
|
bind_map_list aux lst in
|
||||||
|
return (Map lst)
|
||||||
|
| EMap (MapLookUp lu) ->
|
||||||
|
let%bind path = match lu.value.path with
|
||||||
|
| Name v -> return (Variable v.value)
|
||||||
|
| Path p -> simpl_projection p.value
|
||||||
|
in
|
||||||
|
let%bind index = simpl_expression lu.value.index.value.inside in
|
||||||
|
return (LookUp (path, index))
|
||||||
|
|
||||||
|
and simpl_logic_expression (t:Raw.logic_expr) : ae result =
|
||||||
|
match t with
|
||||||
|
| BoolExpr (False _) ->
|
||||||
|
ok @@ ae @@ Literal (Bool false)
|
||||||
|
| BoolExpr (True _) ->
|
||||||
|
ok @@ ae @@ Literal (Bool true)
|
||||||
|
| BoolExpr (Or b) ->
|
||||||
|
simpl_binop "OR" b.value
|
||||||
|
| BoolExpr (And b) ->
|
||||||
|
simpl_binop "AND" b.value
|
||||||
|
| BoolExpr (Not b) ->
|
||||||
|
simpl_unop "NOT" b.value
|
||||||
|
| CompExpr (Lt c) ->
|
||||||
|
simpl_binop "LT" c.value
|
||||||
|
| CompExpr (Gt c) ->
|
||||||
|
simpl_binop "GT" c.value
|
||||||
|
| CompExpr (Leq c) ->
|
||||||
|
simpl_binop "LE" c.value
|
||||||
|
| CompExpr (Geq c) ->
|
||||||
|
simpl_binop "GE" c.value
|
||||||
|
| CompExpr (Equal c) ->
|
||||||
|
simpl_binop "EQ" c.value
|
||||||
|
| CompExpr (Neq c) ->
|
||||||
|
simpl_binop "NEQ" c.value
|
||||||
|
|
||||||
|
and simpl_binop (name:string) (t:_ Raw.bin_op) : ae result =
|
||||||
|
let%bind a = simpl_expression t.arg1 in
|
||||||
|
let%bind b = simpl_expression t.arg2 in
|
||||||
|
ok @@ ae @@ Constant (name, [a;b])
|
||||||
|
|
||||||
|
and simpl_unop (name:string) (t:_ Raw.un_op) : ae result =
|
||||||
|
let%bind a = simpl_expression t.arg in
|
||||||
|
ok @@ ae @@ Constant (name, [a])
|
||||||
|
|
||||||
|
and simpl_list_expression (lst:Raw.expr list) : ae result =
|
||||||
|
match lst with
|
||||||
|
| [] -> ok @@ ae @@ Literal Unit
|
||||||
|
| [hd] -> simpl_expression hd
|
||||||
|
| lst ->
|
||||||
|
let%bind lst = bind_list @@ List.map simpl_expression lst in
|
||||||
|
ok @@ ae @@ Tuple lst
|
||||||
|
|
||||||
|
and simpl_local_declaration (t:Raw.local_decl) : (instruction * named_expression) result =
|
||||||
|
match t with
|
||||||
|
| LocalData d -> simpl_data_declaration d
|
||||||
|
| LocalLam _ -> simple_fail "no local lambdas yet"
|
||||||
|
|
||||||
|
and simpl_data_declaration (t:Raw.data_decl) : (instruction * named_expression) result =
|
||||||
|
let return x = ok (Assignment x, x) in
|
||||||
|
match t with
|
||||||
|
| LocalVar x ->
|
||||||
|
let x = x.value in
|
||||||
|
let name = x.name.value in
|
||||||
|
let%bind t = simpl_type_expression x.var_type in
|
||||||
|
let type_annotation = Some t in
|
||||||
|
let%bind expression = simpl_expression x.init in
|
||||||
|
return {name;annotated_expression={expression with type_annotation}}
|
||||||
|
| LocalConst x ->
|
||||||
|
let x = x.value in
|
||||||
|
let name = x.name.value in
|
||||||
|
let%bind t = simpl_type_expression x.const_type in
|
||||||
|
let type_annotation = Some t in
|
||||||
|
let%bind expression = simpl_expression x.init in
|
||||||
|
return {name;annotated_expression={expression with type_annotation}}
|
||||||
|
|
||||||
|
|
||||||
|
and simpl_param : Raw.param_decl -> named_type_expression result = fun t ->
|
||||||
|
match t with
|
||||||
|
| ParamConst c ->
|
||||||
|
let c = c.value in
|
||||||
|
let type_name = c.var.value in
|
||||||
|
let%bind type_expression = simpl_type_expression c.param_type in
|
||||||
|
ok { type_name ; type_expression }
|
||||||
|
| ParamVar v ->
|
||||||
|
let c = v.value in
|
||||||
|
let type_name = c.var.value in
|
||||||
|
let%bind type_expression = simpl_type_expression c.param_type in
|
||||||
|
ok { type_name ; type_expression }
|
||||||
|
|
||||||
|
and simpl_declaration : Raw.declaration -> declaration result = fun t ->
|
||||||
|
let open! Raw in
|
||||||
|
match t with
|
||||||
|
| TypeDecl x ->
|
||||||
|
let {name;type_expr} : Raw.type_decl = x.value in
|
||||||
|
let%bind type_expression = simpl_type_expression type_expr in
|
||||||
|
ok @@ Type_declaration {type_name=name.value;type_expression}
|
||||||
|
| ConstDecl x ->
|
||||||
|
let {name;const_type;init} = x.value in
|
||||||
|
let%bind expression = simpl_expression init in
|
||||||
|
let%bind t = simpl_type_expression const_type in
|
||||||
|
let type_annotation = Some t in
|
||||||
|
ok @@ Constant_declaration {name=name.value;annotated_expression={expression with type_annotation}}
|
||||||
|
| LambdaDecl (FunDecl x) ->
|
||||||
|
let {name;param;ret_type;local_decls;block;return} : fun_decl = x.value in
|
||||||
|
(match npseq_to_list param.value.inside with
|
||||||
|
| [] -> simple_fail "function without parameters are not allowed"
|
||||||
|
| [a] -> (
|
||||||
|
let%bind input = simpl_param a in
|
||||||
|
let name = name.value in
|
||||||
|
let binder = input.type_name in
|
||||||
|
let input_type = input.type_expression in
|
||||||
|
let%bind local_declarations =
|
||||||
|
let%bind tmp = bind_list
|
||||||
|
@@ List.map simpl_local_declaration local_decls in
|
||||||
|
ok (List.map fst tmp) in
|
||||||
|
let%bind instructions = bind_list
|
||||||
|
@@ List.map simpl_statement
|
||||||
|
@@ npseq_to_list block.value.statements in
|
||||||
|
let%bind result = simpl_expression return in
|
||||||
|
let%bind output_type = simpl_type_expression ret_type in
|
||||||
|
let body = local_declarations @ instructions in
|
||||||
|
let decl =
|
||||||
|
let expression = Lambda {binder ; input_type ; output_type ; result ; body } in
|
||||||
|
let type_annotation = Some (Type_function (input_type, output_type)) in
|
||||||
|
Constant_declaration {name;annotated_expression = {expression;type_annotation}}
|
||||||
|
in
|
||||||
|
ok decl
|
||||||
|
)
|
||||||
|
| lst -> (
|
||||||
|
let%bind params = bind_map_list simpl_param lst in
|
||||||
|
let input =
|
||||||
|
let type_expression = Type_record (
|
||||||
|
SMap.of_list
|
||||||
|
@@ List.map (fun (x:named_type_expression) -> x.type_name, x.type_expression)
|
||||||
|
params
|
||||||
|
) in
|
||||||
|
{ type_name = "arguments" ; type_expression } in
|
||||||
|
let binder = input.type_name in
|
||||||
|
let input_type = input.type_expression in
|
||||||
|
let%bind local_declarations =
|
||||||
|
let%bind typed = bind_map_list simpl_local_declaration local_decls in
|
||||||
|
ok (List.map fst typed)
|
||||||
|
in
|
||||||
|
let%bind output_type = simpl_type_expression ret_type in
|
||||||
|
let%bind instructions = bind_list
|
||||||
|
@@ List.map simpl_statement
|
||||||
|
@@ npseq_to_list block.value.statements in
|
||||||
|
let%bind (body, result) =
|
||||||
|
let renamings =
|
||||||
|
let aux ({type_name}:named_type_expression) : Rename.Value.renaming =
|
||||||
|
type_name, ("arguments", [Record_access type_name])
|
||||||
|
in
|
||||||
|
List.map aux params
|
||||||
|
in
|
||||||
|
let%bind r =
|
||||||
|
let%bind tmp = simpl_expression return in
|
||||||
|
Rename.Value.rename_annotated_expression renamings tmp
|
||||||
|
in
|
||||||
|
let%bind b =
|
||||||
|
let tmp = local_declarations @ instructions in
|
||||||
|
Rename.Value.rename_block renamings tmp
|
||||||
|
in
|
||||||
|
ok (b, r) in
|
||||||
|
let decl =
|
||||||
|
let expression = Lambda {binder ; input_type ; output_type ; result ; body } in
|
||||||
|
let type_annotation = Some (Type_function (input_type, output_type)) in
|
||||||
|
Constant_declaration {name = name.value;annotated_expression = {expression;type_annotation}}
|
||||||
|
in
|
||||||
|
ok decl
|
||||||
|
)
|
||||||
|
)
|
||||||
|
| LambdaDecl (ProcDecl _) -> simple_fail "no proc declaration yet"
|
||||||
|
| LambdaDecl (EntryDecl _)-> simple_fail "no entry point yet"
|
||||||
|
|
||||||
|
and simpl_statement : Raw.statement -> instruction result = fun s ->
|
||||||
|
match s with
|
||||||
|
| Instr i -> simpl_instruction i
|
||||||
|
| Data d -> let%bind (i, _) = simpl_data_declaration d in ok i
|
||||||
|
|
||||||
|
and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
|
||||||
|
match t with
|
||||||
|
| ProcCall _ -> simple_fail "no proc call"
|
||||||
|
| Fail e ->
|
||||||
|
let%bind expr = simpl_expression e.value.fail_expr in
|
||||||
|
ok @@ Fail expr
|
||||||
|
| Skip _ -> ok @@ Skip
|
||||||
|
| Loop (While l) ->
|
||||||
|
let l = l.value in
|
||||||
|
let%bind cond = simpl_expression l.cond in
|
||||||
|
let%bind body = simpl_block l.block.value in
|
||||||
|
ok @@ Loop (cond, body)
|
||||||
|
| Loop (For _) ->
|
||||||
|
simple_fail "no for yet"
|
||||||
|
| Cond c ->
|
||||||
|
let c = c.value in
|
||||||
|
let%bind expr = simpl_expression c.test in
|
||||||
|
let%bind match_true = match c.ifso with
|
||||||
|
| ClauseInstr i -> let%bind i = simpl_instruction i in ok [i]
|
||||||
|
| ClauseBlock b -> simpl_statements @@ fst b.value.inside in
|
||||||
|
let%bind match_false = match c.ifnot with
|
||||||
|
| ClauseInstr i -> let%bind i = simpl_instruction i in ok [i]
|
||||||
|
| ClauseBlock b -> simpl_statements @@ fst b.value.inside in
|
||||||
|
ok @@ Matching (expr, (Match_bool {match_true; match_false}))
|
||||||
|
| Assign a ->
|
||||||
|
let a = a.value in
|
||||||
|
let%bind name = match a.lhs with
|
||||||
|
| Path (Name v) -> ok v.value
|
||||||
|
| _ -> simple_fail "no complex assignments yet"
|
||||||
|
in
|
||||||
|
let%bind annotated_expression = match a.rhs with
|
||||||
|
| Expr e -> simpl_expression e
|
||||||
|
| _ -> simple_fail "no weird assignments yet"
|
||||||
|
in
|
||||||
|
ok @@ Assignment {name ; annotated_expression}
|
||||||
|
| Case c ->
|
||||||
|
let c = c.value in
|
||||||
|
let%bind expr = simpl_expression c.expr in
|
||||||
|
let%bind cases =
|
||||||
|
let aux (x : Raw.case Raw.reg) =
|
||||||
|
let%bind i = simpl_instruction_block x.value.instr in
|
||||||
|
ok (x.value.pattern, i) in
|
||||||
|
bind_list
|
||||||
|
@@ List.map aux
|
||||||
|
@@ npseq_to_list c.cases.value in
|
||||||
|
let%bind m = simpl_cases cases in
|
||||||
|
ok @@ Matching (expr, m)
|
||||||
|
| RecordPatch r ->
|
||||||
|
let r = r.value in
|
||||||
|
let%bind record = match r.path with
|
||||||
|
| Name v -> ok v.value
|
||||||
|
| _ -> simple_fail "no complex assignments yet"
|
||||||
|
in
|
||||||
|
let%bind inj = bind_list
|
||||||
|
@@ List.map (fun (x:Raw.field_assign) -> let%bind e = simpl_expression x.field_expr in ok (x.field_name.value, e))
|
||||||
|
@@ List.map (fun (x:_ Raw.reg) -> x.value)
|
||||||
|
@@ npseq_to_list r.record_inj.value.fields in
|
||||||
|
ok @@ Record_patch (record, [], inj)
|
||||||
|
| MapPatch _ -> simple_fail "no map patch yet"
|
||||||
|
| SetPatch _ -> simple_fail "no set patch yet"
|
||||||
|
| MapRemove _ -> simple_fail "no map remove yet"
|
||||||
|
| SetRemove _ -> simple_fail "no set remove yet"
|
||||||
|
|
||||||
|
and simpl_cases : (Raw.pattern * block) list -> matching result = fun t ->
|
||||||
|
let open Raw in
|
||||||
|
let get_var (t:Raw.pattern) = match t with
|
||||||
|
| PVar v -> ok v.value
|
||||||
|
| _ -> simple_fail "not a var"
|
||||||
|
in
|
||||||
|
let%bind _assert =
|
||||||
|
trace_strong (simple_error "only pattern with two cases supported now") @@
|
||||||
|
Assert.assert_equal_int 2 (List.length t) in
|
||||||
|
let ((pa, ba), (pb, bb)) = List.(hd t, hd @@ tl t) in
|
||||||
|
let uncons p = match p with
|
||||||
|
| PCons {value = (hd, _)} -> ok hd
|
||||||
|
| _ -> simple_fail "uncons fail" in
|
||||||
|
let%bind (pa, pb) = bind_map_pair uncons (pa, pb) in
|
||||||
|
match (pa, ba), (pb, bb) with
|
||||||
|
| (PFalse _, f), (PTrue _, t)
|
||||||
|
| (PTrue _, t), (PFalse _, f) -> ok @@ Match_bool {match_true = t ; match_false = f}
|
||||||
|
| (PSome v, some), (PNone _, none)
|
||||||
|
| (PNone _, none), (PSome v, some) -> (
|
||||||
|
let (_, v) = v.value in
|
||||||
|
let%bind v = match v.value.inside with
|
||||||
|
| PVar v -> ok v.value
|
||||||
|
| _ -> simple_fail "complex none patterns not supported yet" in
|
||||||
|
ok @@ Match_option {match_none = none ; match_some = (v, some) }
|
||||||
|
)
|
||||||
|
| (PCons c, cons), (PList (PNil _), nil)
|
||||||
|
| (PList (PNil _), nil), (PCons c, cons) ->
|
||||||
|
let%bind (a, b) =
|
||||||
|
match c.value with
|
||||||
|
| a, [(_, b)] ->
|
||||||
|
let%bind a = get_var a in
|
||||||
|
let%bind b = get_var b in
|
||||||
|
ok (a, b)
|
||||||
|
| _ -> simple_fail "complex list patterns not supported yet"
|
||||||
|
in
|
||||||
|
ok @@ Match_list {match_cons = (a, b, cons) ; match_nil = nil}
|
||||||
|
| _ ->
|
||||||
|
let error = simple_error "multi-level patterns not supported yet" in
|
||||||
|
fail error
|
||||||
|
|
||||||
|
and simpl_instruction_block : Raw.instruction -> block result = fun t ->
|
||||||
|
match t with
|
||||||
|
| Single s -> let%bind i = simpl_single_instruction s in ok [ i ]
|
||||||
|
| Block b -> simpl_block b.value
|
||||||
|
|
||||||
|
and simpl_instruction : Raw.instruction -> instruction result = fun t ->
|
||||||
|
match t with
|
||||||
|
| Single s -> simpl_single_instruction s
|
||||||
|
| Block _ -> simple_fail "no block instruction yet"
|
||||||
|
|
||||||
|
and simpl_statements : Raw.statements -> block result = fun ss ->
|
||||||
|
let lst = npseq_to_list ss in
|
||||||
|
bind_map_list simpl_statement lst
|
||||||
|
|
||||||
|
and simpl_block : Raw.block -> block result = fun t ->
|
||||||
|
simpl_statements t.statements
|
||||||
|
|
||||||
|
let simpl_program : Raw.ast -> program result = fun t ->
|
||||||
|
bind_list @@ List.map simpl_declaration @@ nseq_to_list t.decl
|
@ -154,6 +154,35 @@ let tuple () : unit result =
|
|||||||
in
|
in
|
||||||
ok ()
|
ok ()
|
||||||
|
|
||||||
|
let option () : unit result =
|
||||||
|
let%bind program = type_file "./contracts/option.ligo" in
|
||||||
|
let open AST_Typed.Combinators in
|
||||||
|
let%bind _some = trace (simple_error "some") @@
|
||||||
|
let%bind result = easy_evaluate_typed "s" program in
|
||||||
|
let expect = a_some (a_int 42) in
|
||||||
|
AST_Typed.assert_value_eq (expect, result)
|
||||||
|
in
|
||||||
|
let%bind _none = trace (simple_error "none") @@
|
||||||
|
let%bind result = easy_evaluate_typed "n" program in
|
||||||
|
let expect = a_none make_t_int in
|
||||||
|
AST_Typed.assert_value_eq (expect, result)
|
||||||
|
in
|
||||||
|
ok ()
|
||||||
|
|
||||||
|
let map () : unit result =
|
||||||
|
let%bind program = type_file "./contracts/map.ligo" in
|
||||||
|
let ez lst =
|
||||||
|
let open AST_Typed.Combinators in
|
||||||
|
let lst' = List.map (fun (x, y) -> a_int x, a_int y) lst in
|
||||||
|
a_map lst' make_t_int make_t_int
|
||||||
|
in
|
||||||
|
let%bind _foobar = trace (simple_error "foobar") @@
|
||||||
|
let%bind result = easy_evaluate_typed "fb" program in
|
||||||
|
let expect = ez [(23, 0) ; (42, 0)] in
|
||||||
|
AST_Typed.assert_value_eq (expect, result)
|
||||||
|
in
|
||||||
|
ok ()
|
||||||
|
|
||||||
let condition () : unit result =
|
let condition () : unit result =
|
||||||
let%bind program = type_file "./contracts/condition.ligo" in
|
let%bind program = type_file "./contracts/condition.ligo" in
|
||||||
let aux n =
|
let aux n =
|
||||||
@ -170,6 +199,42 @@ let condition () : unit result =
|
|||||||
@@ [0 ; 2 ; 42 ; 163 ; -1] in
|
@@ [0 ; 2 ; 42 ; 163 ; -1] in
|
||||||
ok ()
|
ok ()
|
||||||
|
|
||||||
|
let matching () : unit result =
|
||||||
|
let%bind program = type_file "./contracts/match.ligo" in
|
||||||
|
let%bind _bool =
|
||||||
|
let aux n =
|
||||||
|
let open AST_Typed.Combinators in
|
||||||
|
let input = a_int n in
|
||||||
|
let%bind result = easy_run_typed "match_bool" program input in
|
||||||
|
let%bind result' =
|
||||||
|
trace (simple_error "bad result") @@
|
||||||
|
get_a_int result in
|
||||||
|
Assert.assert_equal_int (if n = 2 then 42 else 0) result'
|
||||||
|
in
|
||||||
|
let%bind _ = bind_list
|
||||||
|
@@ List.map aux
|
||||||
|
@@ [0 ; 2 ; 42 ; 163 ; -1] in
|
||||||
|
ok ()
|
||||||
|
in
|
||||||
|
let%bind _option =
|
||||||
|
let aux n =
|
||||||
|
let open AST_Typed.Combinators in
|
||||||
|
let input = match n with
|
||||||
|
| Some s -> a_some (a_int s)
|
||||||
|
| None -> a_none (make_t_int) in
|
||||||
|
let%bind result = easy_run_typed "match_option" program input in
|
||||||
|
let%bind result' =
|
||||||
|
trace (simple_error "bad result") @@
|
||||||
|
get_a_int result in
|
||||||
|
Assert.assert_equal_int (match n with None -> 23 | Some s -> s) result'
|
||||||
|
in
|
||||||
|
let%bind _ = bind_list
|
||||||
|
@@ List.map aux
|
||||||
|
@@ [Some 0 ; Some 2 ; Some 42 ; Some 163 ; Some (-1) ; None] in
|
||||||
|
ok ()
|
||||||
|
in
|
||||||
|
ok ()
|
||||||
|
|
||||||
let declarations () : unit result =
|
let declarations () : unit result =
|
||||||
let%bind program = type_file "./contracts/declarations.ligo" in
|
let%bind program = type_file "./contracts/declarations.ligo" in
|
||||||
let aux n =
|
let aux n =
|
||||||
@ -226,8 +291,11 @@ let main = "Integration (End to End)", [
|
|||||||
test "unit" unit_expression ;
|
test "unit" unit_expression ;
|
||||||
test "record" record ;
|
test "record" record ;
|
||||||
test "tuple" tuple ;
|
test "tuple" tuple ;
|
||||||
|
test "option" option ;
|
||||||
|
(* test "map" map ; *)
|
||||||
test "multiple parameters" multiple_parameters ;
|
test "multiple parameters" multiple_parameters ;
|
||||||
test "condition" condition ;
|
test "condition" condition ;
|
||||||
|
test "matching" matching ;
|
||||||
test "declarations" declarations ;
|
test "declarations" declarations ;
|
||||||
test "quote declaration" quote_declaration ;
|
test "quote declaration" quote_declaration ;
|
||||||
test "quote declarations" quote_declarations ;
|
test "quote declarations" quote_declarations ;
|
||||||
|
@ -17,6 +17,12 @@ let rec translate_type (t:AST.type_value) : type_value result =
|
|||||||
| Type_constant ("int", []) -> ok (`Base Int)
|
| Type_constant ("int", []) -> ok (`Base Int)
|
||||||
| Type_constant ("string", []) -> ok (`Base String)
|
| Type_constant ("string", []) -> ok (`Base String)
|
||||||
| Type_constant ("unit", []) -> ok (`Base Unit)
|
| Type_constant ("unit", []) -> ok (`Base Unit)
|
||||||
|
| Type_constant ("map", [key;value]) ->
|
||||||
|
let%bind kv' = bind_map_pair translate_type (key, value) in
|
||||||
|
ok (`Map kv')
|
||||||
|
| Type_constant ("option", [o]) ->
|
||||||
|
let%bind o' = translate_type o in
|
||||||
|
ok (`Option o')
|
||||||
| Type_constant (name, _) -> fail (error "unrecognized constant" name)
|
| Type_constant (name, _) -> fail (error "unrecognized constant" name)
|
||||||
| Type_sum m ->
|
| Type_sum m ->
|
||||||
let node = Append_tree.of_list @@ list_of_map m in
|
let node = Append_tree.of_list @@ list_of_map m in
|
||||||
@ -68,13 +74,25 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op
|
|||||||
let%bind (_, t, _) as expression = translate_annotated_expression env annotated_expression in
|
let%bind (_, t, _) as expression = translate_annotated_expression env annotated_expression in
|
||||||
let env' = Environment.add (name, t) env in
|
let env' = Environment.add (name, t) env in
|
||||||
return ~env' (Assignment (name, expression))
|
return ~env' (Assignment (name, expression))
|
||||||
| Matching (expr, Match_bool {match_true ; match_false}) ->
|
| Matching (expr, m) -> (
|
||||||
let%bind expr' = translate_annotated_expression env expr in
|
let%bind expr' = translate_annotated_expression env expr in
|
||||||
let env' = Environment.extend env in
|
let env' = Environment.extend env in
|
||||||
let%bind true_branch = translate_block env' match_true in
|
match m with
|
||||||
let%bind false_branch = translate_block env' match_false in
|
| Match_bool {match_true ; match_false} -> (
|
||||||
return (Cond (expr', true_branch, false_branch))
|
let%bind true_branch = translate_block env' match_true in
|
||||||
| Matching _ -> simple_fail "todo : match"
|
let%bind false_branch = translate_block env' match_false in
|
||||||
|
return (Cond (expr', true_branch, false_branch))
|
||||||
|
)
|
||||||
|
| Match_option {match_none ; match_some = ((name, t), sm)} -> (
|
||||||
|
let%bind none_branch = translate_block env' match_none in
|
||||||
|
let%bind some_branch =
|
||||||
|
let%bind t' = translate_type t in
|
||||||
|
let env' = Environment.add (name, t') env' in
|
||||||
|
translate_block env' sm in
|
||||||
|
return (If_None (expr', none_branch, (name, some_branch)))
|
||||||
|
)
|
||||||
|
| _ -> simple_fail "todo : match"
|
||||||
|
)
|
||||||
| Loop (expr, body) ->
|
| Loop (expr, body) ->
|
||||||
let%bind expr' = translate_annotated_expression env expr in
|
let%bind expr' = translate_annotated_expression env expr in
|
||||||
let%bind body' = translate_block env body in
|
let%bind body' = translate_block env body in
|
||||||
@ -85,6 +103,7 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op
|
|||||||
and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_expression) : expression result =
|
and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_expression) : expression result =
|
||||||
let%bind tv = translate_type ae.type_annotation in
|
let%bind tv = translate_type ae.type_annotation in
|
||||||
let return (expr, tv) = ok (expr, tv, env) in
|
let return (expr, tv) = ok (expr, tv, env) in
|
||||||
|
let f = translate_annotated_expression env in
|
||||||
match ae.expression with
|
match ae.expression with
|
||||||
| Literal (Bool b) -> ok (Literal (`Bool b), tv, env)
|
| Literal (Bool b) -> ok (Literal (`Bool b), tv, env)
|
||||||
| Literal (Int n) -> ok (Literal (`Int n), tv, env)
|
| Literal (Int n) -> ok (Literal (`Int n), tv, env)
|
||||||
@ -194,17 +213,26 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
|
|||||||
Append_tree.fold_ne leaf node node_tv in
|
Append_tree.fold_ne leaf node node_tv in
|
||||||
ok expr
|
ok expr
|
||||||
| Constant (name, lst) ->
|
| Constant (name, lst) ->
|
||||||
let%bind lst' = bind_list @@ List.map (translate_annotated_expression env) lst in
|
let%bind lst' = bind_list @@ List.map (translate_annotated_expression env) lst in (
|
||||||
ok (Predicate (name, lst'), tv, env)
|
match name, lst with
|
||||||
|
| "NONE", [] ->
|
||||||
|
let%bind o = Mini_c.Combinators.get_t_option tv in
|
||||||
|
ok (Make_None o, tv, env)
|
||||||
|
| _ -> ok (Predicate (name, lst'), tv, env)
|
||||||
|
)
|
||||||
| Lambda l -> translate_lambda env l tv
|
| Lambda l -> translate_lambda env l tv
|
||||||
| Map m ->
|
| Map m ->
|
||||||
|
let%bind (src, dst) = Mini_c.Combinators.get_t_map tv in
|
||||||
let aux : expression result -> (AST.ae * AST.ae) -> expression result = fun prev kv ->
|
let aux : expression result -> (AST.ae * AST.ae) -> expression result = fun prev kv ->
|
||||||
let%bind prev' = prev in
|
let%bind prev' = prev in
|
||||||
let%bind (k', v') = bind_map_pair (translate_annotated_expression env) kv in
|
let%bind (k', v') = bind_map_pair (translate_annotated_expression env) kv in
|
||||||
return (Predicate ("UPDATE", [k' ; v' ; prev']), tv)
|
return (Predicate ("UPDATE", [k' ; v' ; prev']), tv)
|
||||||
in
|
in
|
||||||
let init = return (Predicate ("EMPTY", []), tv) in
|
let init = return (Empty_map (src, dst), tv) in
|
||||||
List.fold_left aux init m
|
List.fold_left aux init m
|
||||||
|
| LookUp dsi ->
|
||||||
|
let%bind (ds', i') = bind_map_pair f dsi in
|
||||||
|
return (Predicate ("GET", [ds' ; i']), tv)
|
||||||
|
|
||||||
|
|
||||||
and translate_lambda_shallow env l tv =
|
and translate_lambda_shallow env l tv =
|
||||||
@ -370,6 +398,13 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
|
|||||||
| Type_constant ("string", []) ->
|
| Type_constant ("string", []) ->
|
||||||
let%bind n = get_string v in
|
let%bind n = get_string v in
|
||||||
return (Literal (String n))
|
return (Literal (String n))
|
||||||
|
| Type_constant ("option", [o]) -> (
|
||||||
|
match%bind get_option v with
|
||||||
|
| None -> ok (a_none o)
|
||||||
|
| Some s ->
|
||||||
|
let%bind s' = untranspile s o in
|
||||||
|
ok (a_some s')
|
||||||
|
)
|
||||||
| Type_constant _ ->
|
| Type_constant _ ->
|
||||||
simple_fail "unknown type_constant"
|
simple_fail "unknown type_constant"
|
||||||
| Type_sum m ->
|
| Type_sum m ->
|
||||||
|
@ -182,9 +182,10 @@ and type_match (e:environment) (t:O.type_value) : I.matching -> O.matching resul
|
|||||||
@@ get_t_option t in
|
@@ get_t_option t in
|
||||||
let%bind match_none = type_block e match_none in
|
let%bind match_none = type_block e match_none in
|
||||||
let (n, b) = match_some in
|
let (n, b) = match_some in
|
||||||
|
let n' = n, t_opt in
|
||||||
let e' = Environment.add e n t_opt in
|
let e' = Environment.add e n t_opt in
|
||||||
let%bind b' = type_block e' b in
|
let%bind b' = type_block e' b in
|
||||||
ok (O.Match_option {match_none ; match_some = (n, b')})
|
ok (O.Match_option {match_none ; match_some = (n', b')})
|
||||||
| Match_list {match_nil ; match_cons} ->
|
| Match_list {match_nil ; match_cons} ->
|
||||||
let%bind t_list =
|
let%bind t_list =
|
||||||
trace_strong (simple_error "Matching list on not-an-list")
|
trace_strong (simple_error "Matching list on not-an-list")
|
||||||
@ -362,7 +363,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
|
|||||||
| Constant (name, lst) ->
|
| Constant (name, lst) ->
|
||||||
let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
|
let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
|
||||||
let tv_lst = List.map get_annotation lst' in
|
let tv_lst = List.map get_annotation lst' in
|
||||||
let%bind (name', tv) = type_constant name tv_lst in
|
let%bind (name', tv) = type_constant name tv_lst tv_opt in
|
||||||
let%bind type_annotation = check tv in
|
let%bind type_annotation = check tv in
|
||||||
ok O.{expression = O.Constant (name', lst') ; type_annotation}
|
ok O.{expression = O.Constant (name', lst') ; type_annotation}
|
||||||
| Application (f, arg) ->
|
| Application (f, arg) ->
|
||||||
@ -375,8 +376,15 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
|
|||||||
| _ -> simple_fail "applying to not-a-function"
|
| _ -> simple_fail "applying to not-a-function"
|
||||||
in
|
in
|
||||||
ok O.{expression = Application (f, arg) ; type_annotation}
|
ok O.{expression = Application (f, arg) ; type_annotation}
|
||||||
|
| LookUp dsi ->
|
||||||
|
let%bind (ds, ind) = bind_map_pair (type_annotated_expression e) dsi in
|
||||||
|
let%bind (src, dst) = get_t_map ds.type_annotation in
|
||||||
|
let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in
|
||||||
|
let%bind type_annotation = check dst in
|
||||||
|
ok O.{expression = LookUp (ds, ind) ; type_annotation}
|
||||||
|
|
||||||
and type_constant (name:string) (lst:O.type_value list) : (string * O.type_value) result =
|
|
||||||
|
and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) : (string * O.type_value) result =
|
||||||
(* Constant poorman's polymorphism *)
|
(* Constant poorman's polymorphism *)
|
||||||
let open O in
|
let open O in
|
||||||
match (name, lst) with
|
match (name, lst) with
|
||||||
@ -390,6 +398,14 @@ and type_constant (name:string) (lst:O.type_value list) : (string * O.type_value
|
|||||||
| "OR", _ -> simple_fail "OR only defined over bool"
|
| "OR", _ -> simple_fail "OR only defined over bool"
|
||||||
| "AND", [a ; b] when type_value_eq (a, make_t_bool) && type_value_eq (b, make_t_bool) -> ok ("AND", make_t_bool)
|
| "AND", [a ; b] when type_value_eq (a, make_t_bool) && type_value_eq (b, make_t_bool) -> ok ("AND", make_t_bool)
|
||||||
| "AND", _ -> simple_fail "AND only defined over bool"
|
| "AND", _ -> simple_fail "AND only defined over bool"
|
||||||
|
| "NONE", [] -> (
|
||||||
|
match tv_opt with
|
||||||
|
| Some t -> ok ("NONE", t)
|
||||||
|
| None -> simple_fail "untyped NONE"
|
||||||
|
)
|
||||||
|
| "NONE", _ -> simple_fail "bad number of params to NONE"
|
||||||
|
| "SOME", [s] -> ok ("SOME", make_t_option s)
|
||||||
|
| "SOME", _ -> simple_fail "bad number of params to NONE"
|
||||||
| name, _ -> fail @@ unrecognized_constant name
|
| name, _ -> fail @@ unrecognized_constant name
|
||||||
|
|
||||||
let untype_type_value (t:O.type_value) : (I.type_expression) result =
|
let untype_type_value (t:O.type_value) : (I.type_expression) result =
|
||||||
@ -451,6 +467,9 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex
|
|||||||
| Map m ->
|
| Map m ->
|
||||||
let%bind m' = bind_map_list (bind_map_pair untype_annotated_expression) m in
|
let%bind m' = bind_map_list (bind_map_pair untype_annotated_expression) m in
|
||||||
return (Map m')
|
return (Map m')
|
||||||
|
| LookUp dsi ->
|
||||||
|
let%bind dsi' = bind_map_pair untype_annotated_expression dsi in
|
||||||
|
return (LookUp dsi')
|
||||||
|
|
||||||
and untype_block (b:O.block) : (I.block) result =
|
and untype_block (b:O.block) : (I.block) result =
|
||||||
bind_list @@ List.map untype_instruction b
|
bind_list @@ List.map untype_instruction b
|
||||||
@ -487,7 +506,7 @@ and untype_matching (m:O.matching) : (I.matching) result =
|
|||||||
| Match_option {match_none ; match_some = (v, some)} ->
|
| Match_option {match_none ; match_some = (v, some)} ->
|
||||||
let%bind match_none = untype_block match_none in
|
let%bind match_none = untype_block match_none in
|
||||||
let%bind some = untype_block some in
|
let%bind some = untype_block some in
|
||||||
let match_some = v, some in
|
let match_some = fst v, some in
|
||||||
ok @@ Match_option {match_none ; match_some}
|
ok @@ Match_option {match_none ; match_some}
|
||||||
| Match_list {match_nil ; match_cons = (hd, tl, cons)} ->
|
| Match_list {match_nil ; match_cons = (hd, tl, cons)} ->
|
||||||
let%bind match_nil = untype_block match_nil in
|
let%bind match_nil = untype_block match_nil in
|
||||||
|
Loading…
Reference in New Issue
Block a user