pinterp.ml 22.1 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

open Format
open Term


let debug = Debug.register_info_flag "trace_exec"
  ~desc:"trace execution of code given by --exec or --eval"

(* environment *)

open Ity
open Expr


25
(* module Nummap = Map.Make(BigInt) *)
26 27

type value =
28
  | Vconstr of rsymbol * field list
29 30 31
  | Vnum of BigInt.t
  | Vbool of bool
  | Vvoid
32
  | Varray of value array
33

34 35 36 37 38 39 40 41 42
and field = Fimmutable of value | Fmutable of value ref

let field_get f =
  match f with
  | Fimmutable v | Fmutable { contents = v } -> v

let constr rs vl =
  Vconstr(rs,List.map (fun v -> Fimmutable v) vl)

43 44 45 46 47 48 49 50 51 52 53
let rec print_value fmt v =
  match v with
  | Vnum n ->
    if BigInt.ge n BigInt.zero then
      fprintf fmt "%s" (BigInt.to_string n)
    else
      fprintf fmt "(%s)" (BigInt.to_string n)
  | Vbool b ->
    fprintf fmt "%b" b
  | Vvoid ->
    fprintf fmt "()"
54 55 56 57
  | Varray a ->
    fprintf fmt "@[[%a]@]"
      (Pp.print_list Pp.comma print_value)
      (Array.to_list a)
58 59
  | Vconstr(rs,vl) when is_rs_tuple rs ->
    fprintf fmt "@[(%a)@]"
60
      (Pp.print_list Pp.comma print_field) vl
61 62 63 64
  | Vconstr(rs,[]) ->
    fprintf fmt "@[%a@]" print_rs rs
  | Vconstr(rs,vl) ->
    fprintf fmt "@[(%a %a)@]"
65
      print_rs rs (Pp.print_list Pp.space print_field) vl
66

67 68
and print_field fmt f = print_value fmt (field_get f)

69
type env = {
70
  known : Pdecl.known_map;
71 72 73 74
  funenv : Expr.cexp Mrs.t;
  vsenv : value Mvs.t;
}

75 76 77 78 79 80
let add_local_funs locals env =
  { env with funenv =
      List.fold_left
        (fun acc (rs,ce) -> Mrs.add rs ce acc) env.funenv locals}


81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120
let bind_vs vs (v:value) env =
(*
  eprintf "[interp] binding var %s to %a@."
    vs.vs_name.Ident.id_string
    print_value v;
*)
  { env with vsenv = Mvs.add vs v env.vsenv }

let bind_pvs pv v env = bind_vs pv.pv_vs v env

let multibind_pvs l tl env =
  try
    List.fold_right2 bind_pvs l tl env
  with Invalid_argument _ -> assert false


let p_vsvar fmt (vs,t) =
  fprintf fmt "@[<hov 2>%a -> %a@]"
    Pretty.print_vs vs print_value t

let print_vsenv fmt s =
  let l = Mvs.bindings s in
  fprintf fmt "@[<v 0>%a@]" (Pp.print_list Pp.semi p_vsvar) l

(* evaluation of terms *)

exception NoMatch
exception Undetermined
exception CannotCompute

let rec matching env (v:value) p =
  match p.pat_node with
  | Pwild -> env
  | Pvar vs -> bind_vs vs v env
  | Por(p1,p2) ->
    begin
      try matching env v p1
      with NoMatch -> matching env v p2
    end
  | Pas(p,vs) -> matching (bind_vs vs v env) v p
121
  | Papp(ls,pl) ->
122
    match v with
123 124 125
      | Vconstr({rs_logic = RLls ls2},tl) ->
        if ls_equal ls ls2 then
          List.fold_left2 matching env (List.map field_get tl) pl
126 127 128
        else
          if ls2.ls_constr > 0 then raise NoMatch
          else raise Undetermined
129 130 131
      | Vbool b ->
        let ls2 = if b then fs_bool_true else fs_bool_false in
        if ls_equal ls ls2 then env else raise NoMatch
132 133 134 135 136 137 138
      | _ -> raise Undetermined


exception NotNum

let big_int_of_const c =
  match c with
139
    | Number.ConstInt i -> i.Number.il_int
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156
    | _ -> raise NotNum

let big_int_of_value v =
  match v with
    | Vnum i -> i
    | _ -> raise NotNum

let eval_true _ls _l = Vbool true

let eval_false _ls _l = Vbool false

let eval_int_op op ls l =
  match l with
  | [Vnum i1;Vnum i2] ->
    begin
      try Vnum (op i1 i2)
      with NotNum | Division_by_zero ->
157
        constr ls l
158
    end
159
  | _ -> constr ls l
160 161 162 163 164 165 166

let eval_int_uop op ls l =
  match l with
  | [Vnum i1] ->
    begin
      try Vnum (op i1)
      with NotNum ->
167
        constr ls l
168
    end
169
  | _ -> constr ls l
170 171 172 173 174 175 176

let eval_int_rel op ls l =
  match l with
  | [Vnum i1;Vnum i2] ->
    begin
      try Vbool (op i1 i2)
      with NotNum ->
177
        constr ls l
178
    end
179
  | _ -> constr ls l
180 181


182 183 184 185 186 187
let rec default_value_of_type env ity =
  match ity.ity_node with
  | Ityvar _ -> assert false
  | Ityreg r ->
    default_value_of_types env r.reg_its r.reg_args r.reg_regs
  | Ityapp(ts,_,_) when its_equal ts its_int ->
188
    Vnum BigInt.zero
189
  | Ityapp(ts,_,_) when its_equal ts its_real ->
190
    assert false (* TODO *)
191
  | Ityapp(ts,_,_) when its_equal ts its_bool ->
192 193
    Vbool false
(*
194 195
  | Ityapp(ts,_,_) when is_its_tuple ts ->
    assert false (* TODO *)
196
*)
197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212
  | Ityapp(ts,l1,l2) ->
    default_value_of_types env ts l1 l2

and default_value_of_types env ts l1 l2 =
  try
    let d = Pdecl.find_its_defn env.known ts in
    match d.Pdecl.itd_constructors with
    | [] -> assert false
    | cs :: _ ->
      let subst = its_match_regs ts l1 l2 in
      let tyl = List.map (ity_full_inst subst)
        (List.map (fun pv -> pv.pv_ity) cs.rs_cty.cty_args)
      in
      let vl = List.map (default_value_of_type env) tyl in
      Vconstr(cs, List.map (fun v -> Fmutable (ref v)) vl)
  with Not_found -> assert false
213 214 215 216 217 218 219 220 221

type result =
  | Normal of value
  | Excep of xsymbol * value
  | Irred of expr
  | Fun of rsymbol * pvsymbol list * int

let builtin_progs = Hrs.create 17

222
let builtin_array_type _kn _its = ()
223
(*
224 225 226 227
  match (Pdecl.find_its_defn kn its).Pdecl.itd_constructors with
  | [rs] -> array_cons_rs := rs
  | _ ->  assert false
*)
228

229
let exec_array_make _ args =
230 231
  match args with
    | [Vnum n;def] ->
232 233 234 235 236 237 238
      begin
        try
          let n = BigInt.to_int n in
          let v = Varray(Array.make n def) in
          v
        with _ -> raise CannotCompute
      end
239 240 241
    | _ ->
      raise CannotCompute

242
let exec_array_copy _ args =
243
  match args with
244
    | [Varray a] -> Varray(Array.copy a)
245 246 247
    | _ ->
      raise CannotCompute

248
let exec_array_get _ args =
249
  match args with
250
    | [Varray a;Vnum i] ->
251
      begin
252 253 254
        try
          a.(BigInt.to_int i)
        with _ -> raise CannotCompute
255 256 257
      end
    | _ -> raise CannotCompute

258
let exec_array_length _ args =
259
  match args with
260
    | [Varray a] -> Vnum (BigInt.of_int (Array.length a))
261 262
    | _ -> raise CannotCompute

263
let exec_array_set _ args =
264
  match args with
265
    | [Varray a;Vnum i;v] ->
266
      begin
267 268 269 270
        try
          a.(BigInt.to_int i) <- v;
          Vvoid
        with _ -> raise CannotCompute
271 272 273 274 275 276
      end
    | _ -> assert false


let built_in_modules =
  [
277
    ["bool"],"Bool", [],
278 279
    [ "True", eval_true ;
      "False", eval_false ;
280
    ] ;
281
    ["int"],"Int", [],
282
    [ Ident.op_infix "+", eval_int_op BigInt.add;
283
      (* defined as x+(-y)
284 285 286 287 288 289 290 291
         Ident.op_infix "-", eval_int_op BigInt.sub; *)
      Ident.op_infix "*", eval_int_op BigInt.mul;
      Ident.op_prefix "-", eval_int_uop BigInt.minus;
      Ident.op_infix "=", eval_int_rel BigInt.eq;
      Ident.op_infix "<", eval_int_rel BigInt.lt;
      Ident.op_infix "<=", eval_int_rel BigInt.le;
      Ident.op_infix ">", eval_int_rel BigInt.gt;
      Ident.op_infix ">=", eval_int_rel BigInt.ge;
292 293 294 295
    ] ;
    ["int"],"MinMax", [],
    [ "min", eval_int_op BigInt.min;
      "max", eval_int_op BigInt.max;
296 297
    ] ;
    ["int"],"ComputerDivision", [],
298 299 300 301 302 303
    [ "div", eval_int_op BigInt.computer_div;
      "mod", eval_int_op BigInt.computer_mod;
    ] ;
    ["int"],"EuclideanDivision", [],
    [ "div", eval_int_op BigInt.euclidean_div;
      "mod", eval_int_op BigInt.euclidean_mod;
304 305 306
    ] ;
   ["array"],"Array",
    ["array", builtin_array_type],
307
    ["make", exec_array_make ;
308
     Ident.op_get "", exec_array_get ;
309
     "length", exec_array_length ;
310
     Ident.op_set "", exec_array_set ;
311
     "copy", exec_array_copy ;
312 313 314 315 316 317 318 319 320 321 322 323 324
    ] ;
  ]

let add_builtin_mo env (l,n,t,d) =
  let mo = Pmodule.read_module env l n in
  let exp = mo.Pmodule.mod_export in
  let kn = mo.Pmodule.mod_known in
  List.iter
    (fun (id,r) ->
      let its = Pmodule.ns_find_its exp [id] in
      r kn its)
    t;
  List.iter
325
    (fun (id,f) ->
326
      let ps = Pmodule.ns_find_rs exp [id] in
327
      Hrs.add builtin_progs ps f)
328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385
    d

let get_builtin_progs lib =
  List.iter (add_builtin_mo lib) built_in_modules


let get_pvs env pvs =
  let t =
    try
      Mvs.find pvs.pv_vs env.vsenv
  with Not_found ->
    eprintf "program variable %s not found in env@."
      pvs.pv_vs.vs_name.Ident.id_string;
    assert false
  in
  t


(* explicit printing of expr *)

(*

let p_pvs fmt pvs =
  fprintf fmt "@[{ pv_vs =@ %a;@ pv_ity =@ %a;@ pv_ghost =@ %B }@]"
    Pretty.print_vs pvs.pv_vs Ppretty.print_ity pvs.pv_ity
    pvs.pv_ghost

let p_ps fmt ps =
  fprintf fmt "@[{ ps_name =@ %s;@ ... }@]"
    ps.ps_name.Ident.id_string

let p_pls fmt pls =
  fprintf fmt "@[{ pl_ls =@ %s;@ ... }@]"
    pls.pl_ls.ls_name.Ident.id_string

let p_letsym fmt lsym =
  match lsym with
    | LetV pvs -> fprintf fmt "@[LetV(%a)@]" p_pvs pvs
    | LetA _ -> fprintf fmt "@[LetA(_)@]"

let rec p_let fmt ld =
  fprintf fmt "@[{ let_sym =@ %a;@ let_expr =@ %a }@]"
    p_letsym ld.let_sym p_expr ld.let_expr

and p_expr fmt e =
  match e.e_node with
    | Elogic t ->
      fprintf fmt "@[Elogic{type=%a}(%a)@]"
        Ppretty.print_vty e.e_vty
        Pretty.print_term t
    | Evalue pvs -> fprintf fmt "@[Evalue(%a)@]" p_pvs pvs
    | Earrow ps -> fprintf fmt "@[Earrow(%a)@]" p_ps ps
    | Eapp (e1, pvs, _) ->
      fprintf fmt "@[Eapp(%a,@ %a,@ <spec>)@]" p_expr e1 p_pvs pvs
    | Elet(ldefn,e1) ->
      fprintf fmt "@[Elet(%a,@ %a)@]" p_let ldefn p_expr e1
    | Erec (_, _) -> fprintf fmt "@[Erec(_,@ _,@ _)@]"
    | Eif (_, _, _) -> fprintf fmt "@[Eif(_,@ _,@ _)@]"
386
    | Ematch (_, _) -> fprintf fmt "@[Ematch(_,@ _)@]"
387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419
    | Eassign (pls, e1, reg, pvs) ->
      fprintf fmt "@[Eassign(%a,@ %a,@ %a,@ %a)@]"
        p_pls pls p_expr e1 Ppretty.print_reg reg p_pvs pvs
    | Eghost _ -> fprintf fmt "@[Eghost(_)@]"
    | Eany _ -> fprintf fmt "@[Eany(_)@]"
    | Eloop (_, _, _) -> fprintf fmt "@[Eloop(_,@ _,@ _)@]"
    | Efor (_, _, _, _) -> fprintf fmt "@[Efor(_,@ _,@ _,@ _)@]"
    | Eraise (_, _) -> fprintf fmt "@[Eraise(_,@ _)@]"
    | Eabstr (_, _) -> fprintf fmt "@[Eabstr(_,@ _)@]"
    | Eassert (_, _) -> fprintf fmt "@[Eassert(_,@ _)@]"
    | Eabsurd -> fprintf fmt "@[Eabsurd@]"

*)

let print_logic_result fmt r =
  match r with
    | Normal v ->
      fprintf fmt "@[%a@]" print_value v
    | Excep(x,v) ->
      fprintf fmt "@[exception %s(@[%a@])@]"
        x.xs_name.Ident.id_string print_value v
    | Irred e ->
      fprintf fmt "@[Cannot execute expression@ @[%a@]@]"
        print_expr e
    | Fun _ ->
      fprintf fmt "@[Result is a function@]"


(* evaluation of WhyML expressions *)


(* find routine definitions *)

420 421 422 423 424 425
type routine_defn =
  | Builtin of (rsymbol -> value list -> value)
  | Function of (rsymbol * cexp) list * cexp
  | Constructor of Pdecl.its_defn
  | Projection of Pdecl.its_defn

426 427 428 429 430
let rec find_def rs = function
  | d :: _ when rs_equal rs d.rec_sym -> d.rec_fun (* TODO : put rec_rsym in local env *)
  | _ :: l -> find_def rs l
  | [] -> raise Not_found

431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452
let rec find_constr_or_proj dl rs =
  match dl with
  | [] -> raise Not_found
  | d :: rem ->
    if List.mem rs d.Pdecl.itd_constructors then
      begin
        Debug.dprintf debug
          "@[<hov 2>[interp] found constructor:@ %s@]@."
          rs.rs_name.Ident.id_string;
        Constructor d
      end
    else
      if List.mem rs d.Pdecl.itd_fields then
        begin
          Debug.dprintf debug
            "@[<hov 2>[interp] found projection:@ %s@]@."
            rs.rs_name.Ident.id_string;
          Projection d
        end
      else
        find_constr_or_proj rem rs

453 454
let find_global_definition kn rs =
  match (Ident.Mid.find rs.rs_name kn).Pdecl.pd_node with
455
  | Pdecl.PDtype dl -> find_constr_or_proj dl rs
456
  | Pdecl.PDlet (LDvar _) -> raise Not_found
457 458 459 460
  | Pdecl.PDlet (LDsym(_,ce)) -> Function([],ce)
  | Pdecl.PDlet (LDrec dl) ->
    let locs = List.map (fun d -> (d.rec_rsym,d.rec_fun)) dl in
    Function(locs, find_def rs dl)
461 462 463 464
  | Pdecl.PDexn _ -> raise Not_found
  | Pdecl.PDpure -> raise Not_found

let find_definition env rs =
465 466 467 468 469 470 471 472 473 474 475
  try
    (* first try if it is a built-in symbol *)
    Builtin (Hrs.find builtin_progs rs)
  with Not_found ->
    try
      (* then try if it is a local function *)
      let f = Mrs.find rs env.funenv in
      Function([],f)
    with Not_found ->
      (* else look for a global function *)
      find_global_definition env.known rs
476 477 478 479 480 481 482 483 484


(* evaluate expressions *)
let rec eval_expr env (e : expr) : result =
  match e.e_node with
  | Evar pvs ->
    begin
      try
        let v = get_pvs env pvs in
485 486
        Debug.dprintf debug
          "[interp] reading var %s from env -> %a@."
487 488 489 490 491 492 493 494 495 496 497 498
          pvs.pv_vs.vs_name.Ident.id_string
          print_value v;
        Normal v
      with Not_found -> assert false (* Irred e ? *)
    end
  | Econst c -> Normal (Vnum (big_int_of_const c))
  | Eexec (ce,cty) ->
    assert (cty.cty_args = []);
    assert (ce.c_cty.cty_args = []);
    begin match ce.c_node with
    | Cpur _ -> assert false (* TODO ? *)
    | Cfun _ -> assert false (* TODO ? *)
499
    | Cany -> raise CannotCompute
500 501
    | Capp(rs,pvsl) -> exec_call env rs pvsl e.e_ity
    end
502 503 504
  | Eassign l ->
    List.iter
      (fun (pvs,rs,value) ->
505
        let fld = fd_of_rs rs in
506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523
        let value = get_pvs env value in
        match get_pvs env pvs with
        | Vconstr(cstr,args) ->
          let rec aux constr_args args =
            match constr_args,args with
            | pv :: pvl, v :: vl ->
              if pv_equal pv fld then
                match v with
                | Fmutable r -> r := value
                | Fimmutable _ -> assert false
              else
                aux pvl vl
            | _ -> raise CannotCompute
          in
          aux cstr.rs_cty.cty_args args
        | _ -> assert false)
      l;
    Normal Vvoid
524 525 526 527 528 529 530 531
  | Elet(ld,e2) ->
    begin match ld with
      | LDvar(pvs,e1) ->
        begin match eval_expr env e1 with
          | Normal v ->
            eval_expr (bind_pvs pvs v env) e2
          | r -> r
        end
532 533 534 535 536 537 538 539 540 541 542 543
      | LDsym(rs,ce) ->
        let env' = { env with funenv = Mrs.add rs ce env.funenv }
        in eval_expr env' e2
      | LDrec l ->
        let env' =
          { env with funenv =
              List.fold_left
                (fun acc d ->
                  Mrs.add d.rec_sym d.rec_fun
                    (Mrs.add d.rec_rsym d.rec_fun acc))
                env.funenv l }
        in eval_expr env' e2
544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562
    end
  | Eif(e1,e2,e3) ->
    begin
      match eval_expr env e1 with
        | Normal t ->
          begin
            match t with
              | Vbool true -> eval_expr env e2
              | Vbool false -> eval_expr env e3
              | _ ->
              begin
                eprintf
                  "@[[Exec] Cannot decide condition of if: @[%a@]@]@."
                  print_value t;
                Irred e
              end
          end
        | r -> r
    end
563
  | Ewhile(cond,_inv,_var,e1) ->
564
    begin
565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585
      match eval_expr env cond with
      | Normal t ->
        begin
          match t with
          | Vbool true ->
            let r = eval_expr env e1 in
            begin
              match r with
              | Normal _ -> eval_expr env e
              | _ -> r
            end
          | Vbool false -> Normal Vvoid
          | _ ->
            begin
              eprintf
                "@[[Exec] Cannot decide condition of while: @[%a@]@]@."
                print_value t;
              Irred e
            end
        end
      | r -> r
586
    end
587
  | Efor(pvs,(pvs1,dir,pvs2),_i,_inv,e1) ->
588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609
    begin
      try
        let a = big_int_of_value (get_pvs env pvs1) in
        let b = big_int_of_value (get_pvs env pvs2) in
        let le,suc = match dir with
          | To -> BigInt.le, BigInt.succ
          | DownTo -> BigInt.ge, BigInt.pred
        in
        let rec iter i =
          Debug.dprintf debug "[interp] for loop with index = %s@."
            (BigInt.to_string i);
          if le i b then
            let env' = bind_vs pvs.pv_vs (Vnum i) env in
            match eval_expr env' e1 with
              | Normal _ -> iter (suc i)
              | r -> r
          else Normal Vvoid
        in
        iter a
      with
          NotNum -> Irred e
    end
610
  | Ematch(e0,ebl,el) ->
611
    begin
612
      let r = eval_expr env e0 in
613
      match r with
614 615
        | Normal t ->
          if ebl = [] then r else
616
          begin try exec_match env t ebl
617
            with Undetermined -> Irred e
618
          end
619
        | Excep(ex,t) ->
620
          begin
621
            match Mxs.find ex el with
622
            | ([], e2) ->
623 624
              (* assert (t = Vvoid); *)
              eval_expr env e2
625
            | ([v], e2) ->
626 627 628
              let env' = bind_vs v.pv_vs t env in
              eval_expr env' e2
            | _ -> assert false (* TODO ? *)
629
            | exception Not_found -> r
630
          end
631 632 633 634 635 636 637 638 639
        | _ -> r
    end
  | Eraise(xs,e1) ->
    begin
      let r = eval_expr env e1 in
      match r with
        | Normal t -> Excep(xs,t)
        | _ -> r
    end
640
  | Eexn(_,e1) -> eval_expr env e1
641
  | Eassert(_,_t) -> Normal Vvoid (* TODO *)
642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660
    (* TODO: do not eval t if no assertion check *)
(*
    if true then (* noassert *) Normal Vvoid
    else
      begin match (eval_term env t) with
      | Vbool true -> Normal Vvoid
      | Vbool false ->
        eprintf "@[Assertion failed at %a@]@."
          (Pp.print_option Pretty.print_loc) e.e_loc;
        Irred e
      | _ ->
        Warning.emit "@[Warning: assertion cannot be evaluated at %a@]@."
          (Pp.print_option Pretty.print_loc) e.e_loc;
        Normal Vvoid
      end
*)
  | Eghost e1 ->
    (* TODO: do not eval ghost if no assertion check *)
    eval_expr env e1
661
  | Epure _ -> Normal Vvoid (* TODO *)
662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683
  | Eabsurd ->
    eprintf "@[[Exec] unsupported expression: @[%a@]@]@."
      (if Debug.test_flag debug then print_expr (* p_expr *) else print_expr) e;
    Irred e

and exec_match env t ebl =
  let rec iter ebl =
    match ebl with
    | [] ->
      eprintf "[Exec] Pattern matching not exhaustive in evaluation@.";
      assert false
    | (p,e)::rem ->
      try
        let env' = matching env t p.pp_pat in
        eval_expr env' e
      with NoMatch -> iter rem
  in
  iter ebl

and exec_call env rs args ity_result =
  let args' = List.map (fun pvs -> get_pvs env pvs) args in
  try
684 685 686 687 688
    match find_definition env rs with
    | Function(locals,d) ->
      let env = add_local_funs locals env in
      begin
        match d.c_node with
689 690
        | Capp (rs',pvl) ->
          exec_call env rs' (pvl @ args) ity_result
691
        | Cpur _ -> assert false (* TODO ? *)
692
        | Cany -> raise CannotCompute
693 694 695 696 697 698 699 700 701 702 703 704 705 706
        | Cfun body ->
          let pvsl = d.c_cty.cty_args in
          let env' = multibind_pvs pvsl args' env in
          Debug.dprintf debug
            "@[Evaluating function body of %s@]@."
            rs.rs_name.Ident.id_string;
          let r = eval_expr env' body
          in
          Debug.dprintf debug
            "@[Return from function %s@ result@ %a@]@."
            rs.rs_name.Ident.id_string print_logic_result r;
          r
      end
    | Builtin f ->
707 708 709 710 711 712 713 714 715
      Debug.dprintf debug
        "@[Evaluating builtin function %s@]@."
        rs.rs_name.Ident.id_string;
      let r = Normal (f rs (* env ity_result *) args') in
      Debug.dprintf debug
        "@[Return from builtin function %s result %a@]@."
        rs.rs_name.Ident.id_string
        print_logic_result r;
      r
716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739
    | Constructor _d ->
      Debug.dprintf debug
        "[interp] create record with type %a@."
        print_ity ity_result;
      (* FIXME : put a ref only on mutable fields *)
      let args' = List.map (fun v -> Fmutable (ref v)) args' in
      let v = Vconstr(rs,args') in
      Normal v
    | Projection _d ->
      match rs.rs_field, args' with
      | Some pv,[Vconstr(cstr,args)] ->
        let rec aux constr_args args =
          match constr_args,args with
          | pv2 :: pvl, v :: vl ->
            if pv_equal pv pv2 then Normal (field_get v) else
              aux pvl vl
          | _ -> raise CannotCompute
        in
        aux cstr.rs_cty.cty_args args
      | _ -> assert false
  with Not_found ->
    eprintf "[interp] cannot find definition of routine %s@."
      rs.rs_name.Ident.id_string;
    raise CannotCompute
740 741 742 743




744
let eval_global_expr env km locals e =
745 746
  get_builtin_progs env;
  let env = {
747
    known = km;
748 749 750 751 752 753 754
    funenv = Mrs.empty;
    vsenv = Mvs.empty;
  }
  in
  let add_glob _ d acc =
    match d.Pdecl.pd_node with
      | Pdecl.PDlet (LDvar (pvs,_)) ->
755
        (*
756 757
        eprintf "@[<hov 2>[interp] global:@ %s@]@."
          pvs.pv_vs.vs_name.Ident.id_string;
758
        *)
759
        let ity = pvs.pv_ity in
760
        let v = default_value_of_type env ity in
761 762 763 764
        Mvs.add pvs.pv_vs v acc
      | _ -> acc
  in
  let global_env =
765
    Ident.Mid.fold add_glob km Mvs.empty
766 767
  in
  let env = {
768
    known = km;
769 770 771 772
    funenv = Mrs.empty;
    vsenv = global_env;
  }
  in
773
  let env = add_local_funs locals env in
774 775 776 777 778 779 780
  let res = eval_expr env e in
  res, global_env



let eval_global_symbol env m fmt rs =
  try
781 782
    match find_global_definition m.Pmodule.mod_known rs with
    | Function(locals,d) ->
783
      begin
784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810
        match d.c_node with
        | Capp _ -> assert false (* TODO ? *)
        | Cpur _ -> assert false (* TODO ? *)
        | Cany -> assert false (* TODO ? *)
        | Cfun body ->
          begin
            fprintf fmt "@[<hov 2>   type:@ %a@]@."
              print_ity body.e_ity;
            let res, final_env =
              eval_global_expr env
                m.Pmodule.mod_known
                locals
                body
            in
            match res with
            | Normal _ ->
              fprintf fmt "@[<hov 2>   result:@ %a@\nglobals:@ %a@]@."
                print_logic_result res print_vsenv final_env
            | Excep _ ->
              fprintf fmt "@[<hov 2>exceptional result:@ %a@\nglobals:@ %a@]@."
                print_logic_result res print_vsenv final_env;
              exit 1
            | Irred _ | Fun _ ->
              fprintf fmt "@\n@]@.";
              eprintf "Execution error: %a@." print_logic_result res;
              exit 2
          end
811
      end
812 813 814 815
    | _ -> assert false
  with Not_found ->
    eprintf "Symbol '%s' has no definition.@." rs.rs_name.Ident.id_string;
    exit 1