From 8d6f19ac6ca9dac3b5d6cc39df4ed9e42b6e617b Mon Sep 17 00:00:00 2001 From: Galfour Date: Sat, 1 Jun 2019 08:37:43 +0000 Subject: [PATCH] very unstable state --- src/parser/ligodity/AST.ml | 6 +- src/parser/ligodity/AST.mli | 2 +- src/parser/ligodity/Parser.mly | 146 ++------------------------------- src/simplify/ligodity.ml | 59 +++++++++---- src/simplify/pascaligo.ml | 1 - 5 files changed, 56 insertions(+), 158 deletions(-) diff --git a/src/parser/ligodity/AST.ml b/src/parser/ligodity/AST.ml index 749db38ef..7da14760e 100644 --- a/src/parser/ligodity/AST.ml +++ b/src/parser/ligodity/AST.ml @@ -116,7 +116,7 @@ and declaration = (* Non-recursive values *) and let_binding = { - variable : variable; + bindings : pattern list; lhs_type : (colon * type_expr) option; eq : equal; let_rhs : expr @@ -544,8 +544,8 @@ and print_terminator = function Some semi -> print_token semi ";" | None -> () -and print_let_binding {variable; lhs_type; eq; let_rhs} = - print_var variable; +and print_let_binding {bindings; lhs_type; eq; let_rhs} = + List.iter print_pattern bindings; (match lhs_type with None -> () | Some (colon, type_expr) -> diff --git a/src/parser/ligodity/AST.mli b/src/parser/ligodity/AST.mli index d235b72f4..ea400b6d5 100644 --- a/src/parser/ligodity/AST.mli +++ b/src/parser/ligodity/AST.mli @@ -125,7 +125,7 @@ and declaration = (* Non-recursive values *) and let_binding = { (* p = e p : t = e *) - variable : variable; + bindings : pattern list; lhs_type : (colon * type_expr) option; eq : equal; let_rhs : expr diff --git a/src/parser/ligodity/Parser.mly b/src/parser/ligodity/Parser.mly index 88f191f51..a492f2624 100644 --- a/src/parser/ligodity/Parser.mly +++ b/src/parser/ligodity/Parser.mly @@ -42,142 +42,9 @@ let rec sub_rec fresh path (map, rank) pattern = let map' = split fresh map path' pattern in map', rank+1 -and split fresh map path = function - PTuple t -> let apply = sub_rec fresh path in - Utils.nsepseq_foldl apply (map,1) t.value |> fst -| PPar p -> split fresh map path p.value.inside -| PVar v -> if VMap.mem v.value map - then - let err = - Region.{value="Non-linear pattern."; region=v.region} - in (Lexer.prerr ~kind:"Syntactical" err; exit 1) - else - let proj = mk_projection fresh path - in VMap.add v.value (None, proj) map -| PWild _ -> map -| PUnit _ -> let anon = Utils.gen_sym () in - let unit = ghost, TAlias (ghost_of "unit") - and proj = mk_projection fresh path - in VMap.add anon (Some unit, proj) map -| PRecord {region; _} -| PConstr {region; _} -| PTyped {region; _} -> - let err = Region.{value="Not implemented yet."; region} - in (Lexer.prerr ~kind:"Syntactical" err; exit 1) -| p -> let _, _, map = split_pattern p in map - -and split_pattern = function - PPar p -> split_pattern p.value.inside -| PVar v -> v, None, VMap.empty -| PWild _ -> Utils.gen_sym () |> ghost_of, None, VMap.empty -| PUnit _ -> let fresh = Utils.gen_sym () |> ghost_of in - let unit = TAlias (ghost_of "unit") - in fresh, Some unit, VMap.empty -| PTyped {value=p; _} -> - let var', type', map = split_pattern p.pattern in - (match type' with - None -> var', Some p.type_expr, map - | Some t when t = p.type_expr -> var', Some t, map (* hack *) - | Some t -> fail_syn_unif t p.type_expr) -| PTuple t -> - let fresh = Utils.gen_sym () |> ghost_of - and init = VMap.empty, 1 in - let apply (map, rank) pattern = - split fresh map (rank,[]) pattern, rank+1 in - let map = Utils.nsepseq_foldl apply init t.value |> fst - in fresh, None, map -| PRecord {region; _} -| PConstr {region; _} -> - let err = Region.{value="Not implemented yet."; region} - in (Lexer.prerr ~kind:"Syntactical" err; exit 1) -| PInt {region; _} | PTrue region -| PFalse region | PString {region; _} -| PList Sugar {region; _} | PList PCons {region; _} -> - let err = Region.{value="Incomplete pattern."; region} - in (Lexer.prerr ~kind:"Syntactical" err; exit 1) - -let mk_let_bindings = - let apply var (lhs_type, proj) = - let new_bind = { - variable = ghost_of var; - lhs_type; - eq = ghost; - let_rhs = EProj (ghost_of proj)} in - let new_let = Let (ghost_of (ghost, new_bind)) - in Utils.nseq_cons new_let - in VMap.fold apply - -let mk_let_in_bindings = - let apply var (lhs_type, proj) acc = - let binding = { - variable = ghost_of var; - lhs_type; - eq = ghost; - let_rhs = EProj (ghost_of proj)} in - let let_in = { - kwd_let = ghost; - binding; - kwd_in = ghost; - body = acc} - in ELetIn (ghost_of let_in) - in VMap.fold apply (* We rewrite "fun p -> e" into "fun x -> match x with p -> e" *) -let norm_fun_expr patterns expr = - let apply pattern expr = - match pattern with - PVar var -> - let fun_expr = { - kwd_fun = ghost; - param = var; - p_annot = None; - arrow = ghost; - body = expr} - in EFun (ghost_of fun_expr) - | PTyped p -> - let pattern = p.value.pattern - and type_expr = p.value.type_expr in - let fresh = Utils.gen_sym () |> ghost_of in - let clause = {pattern; arrow=ghost; rhs=expr} in - let clause = ghost_of clause in - let cases = ghost_of (clause, []) in - let case = { - kwd_match = ghost; - expr = EVar fresh; - opening = With ghost; - lead_vbar = None; - cases; - closing = End ghost} in - let case = ECase (ghost_of case) in - let fun_expr = { - kwd_fun = ghost; - param = fresh; - p_annot = Some (p.value.colon, type_expr); - arrow = ghost; - body = case} - in EFun (ghost_of fun_expr) - | _ -> let fresh = Utils.gen_sym () |> ghost_of in - let clause = {pattern; arrow=ghost; rhs=expr} in - let clause = ghost_of clause in - let cases = ghost_of (clause, []) in - let case = { - kwd_match = ghost; - expr = EVar fresh; - opening = With ghost; - lead_vbar = None; - cases; - closing = End ghost} in - let case = ECase (ghost_of case) in - let fun_expr = { - kwd_fun = ghost; - param = fresh; - p_annot = None; - arrow = ghost; - body = case} - in EFun (ghost_of fun_expr) - in Utils.nseq_foldr apply patterns expr - (* END HEADER *) %} @@ -416,11 +283,11 @@ field_decl: entry_binding: ident nseq(sub_irrefutable) type_annotation? eq expr { - let let_rhs = norm_fun_expr $2 $5 in - {variable = $1; lhs_type=$3; eq=$4; let_rhs} + let let_rhs = $5 in + {bindings = ($1 , $2); lhs_type=$3; eq=$4; let_rhs} } | ident type_annotation? eq fun_expr(expr) { - {variable = $1; lhs_type=$2; eq=$3; let_rhs=$4} } + {bindings = ($1 , []); lhs_type=$2; eq=$3; let_rhs=$4} } (* Top-level non-recursive definitions *) @@ -428,14 +295,15 @@ let_declaration: reg(kwd(Let) let_binding {$1,$2}) { let kwd_let, (binding, map) = $1.value in let let0 = Let {$1 with value = kwd_let, binding} - in mk_let_bindings map (let0,[]) + in + mk_let_bindings map (let0,[]) } let_binding: ident nseq(sub_irrefutable) type_annotation? eq expr { - let let_rhs = norm_fun_expr $2 $5 in + let let_rhs = $5 in let map = VMap.empty in - {variable=$1; lhs_type=$3; eq=$4; let_rhs}, map + {bindings= ($1 , $2); lhs_type=$3; eq=$4; let_rhs}, map } | irrefutable type_annotation? eq expr { let variable, type_opt, map = split_pattern $1 in diff --git a/src/simplify/ligodity.ml b/src/simplify/ligodity.ml index 168980383..9381fb251 100644 --- a/src/simplify/ligodity.ml +++ b/src/simplify/ligodity.ml @@ -237,20 +237,7 @@ let rec simpl_expression : ) | _ -> default_action () ) - | EFun lamb -> - let%bind input_type = bind_map_option - (fun (_,type_expr) -> simpl_type_expression type_expr) - lamb.value.p_annot in - let body, body_type = - match lamb.value.body with - EAnnot {value = expr, type_expr} -> expr, Some type_expr - | expr -> expr, None in - let%bind output_type = - bind_map_option simpl_type_expression body_type in - let%bind result = simpl_expression body in - let binder = lamb.value.param.value, input_type in - let lambda = {binder; input_type; output_type; result = result} - in return @@ E_lambda lambda + | EFun lamb -> simpl_fun lamb | ESeq s -> let items : Raw.expr list = pseq_to_list s.value.elements in (match items with @@ -269,6 +256,50 @@ let rec simpl_expression : let%bind match_false = simpl_expression c.ifnot in return @@ E_matching (expr, (Match_bool {match_true; match_false})) +and simpl_fun lamb : expr result = + let return x = ok x in + let rec aux args body = + match body with + | Raw.EFun l -> ( + let l' = l.value in + let annot = Option.map snd l'.p_annot in + aux (args @ [(l'.param.value , annot)]) l'.body + ) + | _ -> (args , body) in + let (args , body) = aux [] (Raw.EFun lamb) in + let%bind args' = + let aux = fun (name , ty_opt) -> + let%bind ty = + match ty_opt with + | Some ty -> simpl_type_expression ty + | None when name = "storage" -> ok (T_variable "storage") + | None -> simple_fail "missing type annotation on input" + in + ok (name , ty) + in + bind_map_list aux args + in + let arguments_name = "arguments" in + let (binder , input_type) = + let type_expression = T_tuple (List.map snd args') in + (arguments_name , type_expression) in + let body, body_type = + match body with + | EAnnot {value = expr, type_expr} -> expr, Some type_expr + | expr -> expr, None in + let%bind output_type = + bind_map_option simpl_type_expression body_type in + let%bind result = simpl_expression body in + let wrapped_result = + let aux = fun i (name , ty) wrapped -> + let accessor = E_accessor (E_variable arguments_name , [ Access_tuple i ]) in + e_let_in (name , Some ty) accessor wrapped + in + let wraps = List.mapi aux args' in + List.fold_right' (fun x f -> f x) result wraps in + let lambda = {binder = (binder , Some input_type); input_type = (Some input_type); output_type; result = wrapped_result} + in return @@ E_lambda lambda + and simpl_logic_expression ?te_annot (t:Raw.logic_expr) : expr result = let return x = ok @@ make_option_typed x te_annot in diff --git a/src/simplify/pascaligo.ml b/src/simplify/pascaligo.ml index bf907b1fb..038fd4484 100644 --- a/src/simplify/pascaligo.ml +++ b/src/simplify/pascaligo.ml @@ -351,7 +351,6 @@ and simpl_fun_declaration : Raw.fun_decl -> ((name * type_expression option) * e let arguments_name = "arguments" in let%bind params = bind_map_list simpl_param lst in let (binder , input_type) = - (* let type_expression = T_record (SMap.of_list params) in *) let type_expression = T_tuple (List.map snd params) in (arguments_name , type_expression) in let%bind tpl_declarations =