Implementing subst over the AST

src/stages/ast_typed/combinators.ml

@@ -5,7 +5,6 @@ let make_t type_value' simplified = { type_value' ; simplified }
 let make_a_e ?(location = Location.generated) expression type_annotation environment = {
   expression ;
   type_annotation ;
-  dummy_field = () ;
   environment ;
   location ;
 }

src/stages/ast_typed/types.ml

@@ -38,7 +38,6 @@ and annotated_expression = {
   type_annotation : tv ;
   environment : full_environment ;
   location : Location.t ;
-  dummy_field : unit ;
 }
 
 and named_expression = {

src/stages/typesystem/misc.ml

@@ -7,16 +7,137 @@ module Substitution = struct
   module Pattern = struct
 
     open Trace
+    module T = Ast_typed
+    module TSMap = Trace.TMap(String)
 
-    let rec declaration ~(d : Ast_typed.declaration Location.wrap) ~v ~expr : Ast_typed.declaration Location.wrap result =
-      Trace.bind_map_location (function
+    type 'a w = 'a -> 'a result
+
+    let todo = failwith "TODO"
+
+    let rec rec_yes = true
+    and s_full_environment ~v ~expr : T.full_environment w = fun (a , b) ->
+      let%bind a = todo ~v ~expr a in
+      let%bind b = bind_map_list (todo ~v ~expr) b in
+      ok (a , b)
+
+    and s_variable ~v ~expr : T.name w = fun var -> todo
+
+    and s_type_variable ~v ~expr : T.name w = fun tvar -> todo
+
+    and s_type_value ~v ~expr : T.type_value w = fun { type_value'; simplified } -> todo
+
+    and s_expression ~v ~expr : T.expression w = function
+      | T.E_literal         x ->
+        let%bind x = s_literal ~v ~expr x in
+        ok @@ T.E_literal x
+      | T.E_constant        (var, vals) ->
+        let%bind var = s_variable ~v ~expr var in
+        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        ok @@ T.E_constant (var, vals)
+      | T.E_variable        tv ->
+        let%bind tv = s_variable ~v ~expr tv in
+        ok @@ T.E_variable tv
+      | T.E_application     (val1 , val2) ->
+        let%bind val1 = s_annotated_expression ~v ~expr val1 in
+        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        ok @@ T.E_application (val1 , val2)
+      | T.E_lambda          { binder; body } ->
+        let%bind binder = s_variable ~v ~expr binder in
+        let%bind body = s_annotated_expression ~v ~expr body in
+        ok @@ T.E_lambda { binder; body }
+      | T.E_let_in          { binder; rhs; result } ->
+        let%bind binder = s_variable ~v ~expr binder in
+        let%bind rhs = s_annotated_expression ~v ~expr rhs in
+        let%bind result = s_annotated_expression ~v ~expr result in
+        ok @@ T.E_let_in { binder; rhs; result }
+      | T.E_tuple           vals ->
+        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        ok @@ T.E_tuple vals
+      | T.E_tuple_accessor  (val_, i) ->
+        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let i = i in
+        ok @@ T.E_tuple_accessor (val_, i)
+      | T.E_constructor     (tvar, val_) ->
+        let%bind tvar = s_type_variable ~v ~expr tvar in
+        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        ok @@ T.E_constructor (tvar, val_)
+      | T.E_record          aemap ->
+        let%bind aemap = TSMap.bind_map_Map (fun ~k:key ~v:val_ ->
+            let key = s_type_variable ~v ~expr key in
+            let val_ = s_annotated_expression ~v ~expr val_ in
+            ok @@ (key , val_)) aemap in
+        ok @@ T.E_record aemap
+      | T.E_record_accessor (val_, tvar) ->
+        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let%bind tvar = s_type_variable ~v ~expr tvar in
+        ok @@ T.E_record_accessor (val_, tvar)
+      | T.E_map             val_val_list ->
+        let%bind val_val_list = bind_map_list (fun (val1 , val2) ->
+            let%bind val1 = s_annotated_expression ~v ~expr val1 in
+            let%bind val2 = s_annotated_expression ~v ~expr val2 in
+            (val1 , val2)
+          ) val_val_list in
+        ok @@ T.E_map val_val_list
+      | T.E_big_map         val_val_list ->
+        let%bind val_val_list = bind_map_list (fun (val1 , val2) ->
+            let%bind val1 = s_annotated_expression ~v ~expr val1 in
+            let%bind val2 = s_annotated_expression ~v ~expr val2 in
+            (val1 , val2)
+          ) val_val_list in
+        ok @@ T.E_big_map val_val_list
+      | T.E_list            vals ->
+        let%bind vals = bind_map_list s_annotated_expression ~v ~expr vals in
+        ok @@ T.E_list vals
+      | T.E_set             vals ->
+        let%bind vals = bind_map_list s_annotated_expression ~v ~expr vals in
+        ok @@ T.E_set vals
+      | T.E_look_up         (val1, val2) ->
+        let%bind val1 = s_annotated_expression ~v ~expr val1 in
+        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        ok @@ T.E_look_up (val1 , val2)
+      | T.E_matching         (val_ , matching) ->
+        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let%bind matching = s_matching matching in
+        ok @@ T.E_matching (val_ , matching)
+      | T.E_sequence        (val1, val2) ->
+        let%bind val1 = s_annotated_expression ~v ~expr val1 in
+        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        ok @@ T.E_sequence (val1 , val2)
+      | T.E_loop            (val1, val2) ->
+        let%bind val1 = s_annotated_expression ~v ~expr val1 in
+        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        ok @@ T.E_loop (val1 , val2)
+      | T.E_assign          (named_tval, access_path, val_) ->
+        let%bind named_tval = s_named_type_value ~v ~expr named_tval in
+        let%bind access_path = s_access_path ~v ~expr access_path in
+        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        ok @@ T.E_assign (named_tval, access_path, val_)
+
+    and s_annotated_expression ~v ~expr : T.annotated_expression w = fun { expression; type_annotation; environment; location } ->
+      let%bind expression = s_expression ~v ~expr expression in
+      let%bind type_annotation = s_type_value ~v ~expr type_annotation in
+      let%bind environment = s_full_environment ~v ~expr environment in
+      let location = location in
+      ok T.{ expression; type_annotation; environment; location }
+
+    and s_named_expression ~v ~expr : T.named_expression w = fun { name; annotated_expression } ->
+      let name = name in
+      let annotated_expression = s_annotated_expression annotated_expression in
+      ok T.{ name; annotated_expression }
+
+    and s_declaration ~v ~expr : T.declaration w =
+      function
         Ast_typed.Declaration_constant (e, (env1, env2)) ->
-            let _ = v, expr, failwith "TODO: subst" in
+        let e = s_named_expression ~v ~expr e in
+        let env1 = s_full_environment ~v ~expr env1 in
+        let env2 = s_full_environment ~v ~expr env2 in
         ok @@ Ast_typed.Declaration_constant (e, (env1, env2))
-        ) d
+
+    and s_declaration_wrap ~v ~expr : T.declaration Location.wrap w = fun d ->
+      Trace.bind_map_location (s_declaration ~v ~expr) 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
+      Trace.bind_map_list (s_declaration_wrap ~v ~expr) p
 
     (*
        Computes `P[v := expr]`.

vendors/ligo-utils/simple-utils/trace.ml

@@ -600,6 +600,17 @@ module TMap(X : Map.OrderedType) = struct
       f ~x ~k ~v
     in
     MX.fold aux map (ok init)
+
+  let bind_map_Map f map =
+    let aux k v map'  =
+      map' >>? fun map' ->
+      f ~k ~v >>? fun v' ->
+      ok @@ MX.update k (function
+          | None -> Some v'
+          | Some _ -> failwith "key collision, shouldn't happen in bind_map_Map")
+        map'
+    in
+    MX.fold aux map (ok MX.empty)
 end
 
 let bind_fold_pair f init (a,b) =