From dcf5a975d444dd056694db7c763dac0424a5d29d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Mon, 28 Oct 2019 01:10:26 -0400 Subject: [PATCH] More of subst --- src/passes/4-typer/typer.ml | 10 +++++++--- src/stages/typesystem/misc.ml | 15 ++++++++++----- vendors/ligo-utils/simple-utils/trace.ml | 10 ++++++++++ 3 files changed, 27 insertions(+), 8 deletions(-) diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml index d743aa11f..f6f51b482 100644 --- a/src/passes/4-typer/typer.ml +++ b/src/passes/4-typer/typer.ml @@ -939,15 +939,19 @@ let type_program_returns_state (p:I.program) : (environment * Solver.state * O.p let () = ignore (env' , state') in ok (env', state', declarations) +module TSMap = TMap(Solver.TypeVariable) + let type_program (p : I.program) : (O.program * Solver.state) result = let%bind (env, state, program) = type_program_returns_state p in let subst_all = let assignments = state.structured_dbs.assignments in - let aux (v : O.type_name) (expr : Solver.c_constructor_simpl) (p:O.program) = + let aux (v : O.type_name) (expr : Solver.c_constructor_simpl) (p:O.program result) = + let%bind p = p in Typesystem.Misc.Substitution.Pattern.program ~p ~v ~expr in - let p = SMap.fold aux assignments program in + (* let p = TSMap.bind_fold_Map aux program assignments in *) (* TODO: Module magic: this does not work *) + let p = Solver.TypeVariableMap.fold aux assignments (ok program) in p in - let program = subst_all in + let%bind program = subst_all in let () = ignore env in (* TODO: shouldn't we use the `env` somewhere? *) ok (program, state) diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml index 096a5cea8..88b06e3fd 100644 --- a/src/stages/typesystem/misc.ml +++ b/src/stages/typesystem/misc.ml @@ -6,12 +6,17 @@ module Substitution = struct module Pattern = struct - let rec declaration ~(d : Ast_typed.declaration Location.wrap) ~v ~expr : Ast_typed.declaration Location.wrap = - let _TODO = (d, v, expr) in - failwith "TODO: subst declaration" + open Trace - and program ~(p : Ast_typed.program) ~v ~expr : Ast_typed.program = - List.map (fun d -> declaration ~d ~v ~expr) p + let rec declaration ~(d : Ast_typed.declaration Location.wrap) ~v ~expr : Ast_typed.declaration Location.wrap result = + Trace.bind_map_location (function + Ast_typed.Declaration_constant (e, (env1, env2)) -> + let _ = v, expr, failwith "TODO: subst" in + ok @@ Ast_typed.Declaration_constant (e, (env1, env2)) + ) d + + and program ~(p : Ast_typed.program) ~v ~expr : Ast_typed.program Trace.result = + Trace.bind_map_list (fun d -> declaration ~d ~v ~expr) p (* Computes `P[v := expr]`. diff --git a/vendors/ligo-utils/simple-utils/trace.ml b/vendors/ligo-utils/simple-utils/trace.ml index 7a0326eec..e8f3b43eb 100644 --- a/vendors/ligo-utils/simple-utils/trace.ml +++ b/vendors/ligo-utils/simple-utils/trace.ml @@ -592,6 +592,16 @@ let bind_fold_list f init lst = in List.fold_left aux (ok init) lst +module TMap(X : Map.OrderedType) = struct + module MX = Map.Make(X) + let bind_fold_Map f init map = + let aux k v x = + x >>? fun x -> + f ~x ~k ~v + in + MX.fold aux map (ok init) +end + let bind_fold_pair f init (a,b) = let aux x y = x >>? fun x ->