diff options
| author | Kathy Gray | 2016-03-30 16:24:06 +0100 |
|---|---|---|
| committer | Kathy Gray | 2016-03-30 16:24:06 +0100 |
| commit | 85b59cb782e948a2c2128f7612f5681908e2a25e (patch) | |
| tree | c9b6feaa2e2ac0d0492ba358c063d32fa80bed7a | |
| parent | fe6e2c0a026f063876203ff73594e45fc80d555f (diff) | |
Small missing cases in patterns
| -rw-r--r-- | src/lem_interp/interp.lem | 6 | ||||
| -rw-r--r-- | src/lem_interp/pretty_interp.ml | 1 |
2 files changed, 4 insertions, 3 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 699c1cd0..52903291 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -926,7 +926,7 @@ let rec to_exp mode env v : (exp tannot * lenv) = then (E_aux (E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,((integerFromNat n),e)::acc)) (n,[]) es))) (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env') - else if n= List.length vals + else if (n+1)= List.length vals then (E_aux (E_vector es) annot, env') else (E_aux (E_vector_indexed @@ -1720,7 +1720,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (match (detaint v1, detaint v2) with | (V_lit (L_aux (L_num n1) ln1),V_lit (L_aux (L_num n2) ln2)) -> let (n1,n2) = (natFromInteger n1,natFromInteger n2) in - (match vvec with + (match detaint vvec with | V_vector _ _ _ -> Value (slice_vector vvec n1 n2) | V_vector_sparse _ _ _ _ _ -> Value (slice_vector vvec n1 n2) | V_unknown -> @@ -2112,7 +2112,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = resolve_outcome (interp_main mode t_level l_env lm cond) (fun c lm le -> - (match c with + (match detaint c with | V_lit (L_aux L_one _) -> (Value unitv,lm,l_env) | V_lit (L_aux L_true _) -> (Value unitv,lm,l_env) | V_lit (L_aux L_zero _) -> (Action (Fail v) (mk_thunk l annot t_level l_env l_mem), lm,le) diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml index a9a44dfe..8b24d692 100644 --- a/src/lem_interp/pretty_interp.ml +++ b/src/lem_interp/pretty_interp.ml @@ -393,6 +393,7 @@ let doc_exp, doc_let = let cases = separate_map (break 1) (doc_case env add_red) pexps in surround 2 1 opening cases rbrace | E_exit e -> separate space [string "exit"; exp env add_red e;] + | E_assert(e,msg) -> string "assert" ^^ parens (separate_map comma (exp env add_red) [e; msg]) (* adding parens and loop for lower precedence *) | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _) | E_cons (_, _)|E_field (_, _)|E_assign (_, _) |