structures: context initialization in analyzer

model_with_structures/analyzer.ml

@@ -205,6 +205,24 @@ struct
     | PathE p -> pathtype types p
     | TupleE es -> TupleT (List.map (exprtype types) es)
 
+  (* - context initialization *)
+
+  let add_decl (state : state) (x : data) (d : decl) : state =
+    match state with (mem, types, vals) -> match d with
+    | VarD (t, e) -> let v = exprval mem vals e in
+                     let (mem', id) = mem_add mem v in
+                     (mem', (x, t) :: types, (x, id) :: vals)
+    | FunD (ts, s)  -> let (mem', id) = mem_add mem (FunV [s]) in
+                       (mem', (x, FunT ts) :: types, (x, id) :: vals)
+
+  let empty_state : state = (([], 0), [], [])
+
+  let prog_init (prog : prog) : state =
+    match prog with (decls, _) -> fst @@ List.fold_left (* TODO: FIXME: check x's order *)
+                                    (fun (st, x) d -> (add_decl st x d, x + 1))
+                                    (empty_state, 0)
+                                    decls
+
   (* - call values spoil *)
 
   (* TODO: check all cases *)
@@ -243,6 +261,7 @@ struct
     | _, _, _ ->  raise @@ Typing_error "valspoil"
 
   (* full spoil *)
+
   let rec argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
     match state with (mem, types, vals) ->
     let x = pathvar p in

model_with_structures/model.typ

@@ -756,7 +756,7 @@ $s in stmt, f in X, x in X, a in X$
     // expect well typed program
 
     $vals, mu texpre e eqmu v$,
-    $types texprt e : t'$,
+    // $types texprt e : t'$,
     $mu xarrowSquiggly(v)_#[add] cl l, mu' cr$,
 
     $cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu' cr$
@@ -770,9 +770,11 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ add function declaration],
 
+    $mu xarrowSquiggly(lambda space [[x_1, ... x_n] s])_#[add] cl l, mu' cr$,
+
     $cl types, vals, mu cr
      xarrowSquiggly("fun" f (x_1 space : space m_1 t_1, ... space x_n space : space m_n t_n) space = space s)_init
-     cl types[f <- lambda space [t_1, ... t_n]], vals[f <- lambda space [[x_1, ... x_n] s], mu cr$
+     cl types[f <- lambda space [t_1, ... t_n]], vals[f <- l], mu' cr$
   )
 ))