diff options
| author | Kathy Gray | 2016-01-26 17:50:11 +0000 |
|---|---|---|
| committer | Kathy Gray | 2016-01-26 17:50:11 +0000 |
| commit | f79c896cd9cb0592c7c57c9aba1a5a837e30b66b (patch) | |
| tree | 2846855419cf4f67d496c97c416dd3cb283c6652 /src | |
| parent | 8b08f604226d47474c7b2a98909bcc2008b4856c (diff) | |
Stop turning all decreasing vectors into indexed ones : i.e. let's print them sensibly at last
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp.lem | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 3e9fa6dc..1a70c6d7 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -923,10 +923,12 @@ 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 + else if n= List.length vals + then (E_aux (E_vector es) annot, env') + else (E_aux (E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,((integerFromNat n),e)::acc)) (n-(List.length es),[]) es)) - (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env') + (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env') | V_vector_sparse n m dir vals d -> let ((es : (list (exp tannot))),env') = mapf (List.map (fun (i,v) -> v) vals) env in let ((d : (exp tannot)),env') = to_exp mode env' d in |