diff options
| author | Peter Sewell | 2016-06-03 16:32:34 +0100 |
|---|---|---|
| committer | Peter Sewell | 2016-06-03 16:32:34 +0100 |
| commit | 0650c97b78da4efda0337192ca8fe765e38155ea (patch) | |
| tree | 9b301da1e1b3d2318ee5bf3a78bc78f04c4f3f9c /src | |
| parent | 426dea43d87e423371095f7a35f4df82c8ad53a3 (diff) | |
| parent | a0447910fc93f98897d41b4ee48ccb888cda3113 (diff) | |
Merge branch 'master' of bitbucket.org:Peter_Sewell/l2
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp.lem | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index dccbe090..0abc6220 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -13,6 +13,9 @@ open import Instruction_extractor type tannot = Interp_utilities.tannot +val debug_print : string -> unit +declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s + val intern_annot : tannot -> tannot let intern_annot annot = match annot with @@ -579,7 +582,8 @@ let access_vector v n = | V_lit (L_aux L_undef _) -> v | V_lit (L_aux L_zero _) -> v | V_lit (L_aux L_one _ ) -> v - | V_vector m dir vs -> + | V_vector m dir vs -> + (*let _ = debug_print ("access_vector given " ^ string_of_value v ^ " where dir was " ^ (if is_inc(dir) then "increasing" else "decreaseing") ^ " and start is " ^ show m ^ " and index is " ^ show n ^ "\n") in*) list_nth vs (if is_inc(dir) then (n - m) else (m - n)) | V_vector_sparse _ _ _ vs d -> match (List.lookup n vs) with @@ -1054,9 +1058,6 @@ let fix_up_nondet typ branches annot = (fun e -> E_aux (E_assign (LEXP_aux (LEXP_id redex_id) annot) e) annot) branches), Just "0") end -val debug_print : string -> unit -declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s - (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *) val match_pattern : top_level -> pat tannot -> value -> bool * bool * lenv let rec match_pattern t_level (P_aux p (_, annot)) value_whole = |