WIP: probably aborted attempt at abstract interpretation to fix #505

src/as_def/syntax.ml

@@ -219,3 +219,29 @@ let string_of_lit = function
   | TextLit t     -> t
   | FloatLit f    -> Value.Float.to_pretty_string f
   | PreLit _      -> assert false
+
+
+let rec reduce_constant = function
+  | UnE (_, op, exp) ->
+    Lib.Option.bind
+      (reduce_constant exp.it)
+      (function
+       | LitE lit ->
+         begin match !lit with
+         | NatLit n -> Some (LitE (ref (NatLit (Big_int.minus_big_int n))))
+         | PreLit (n, Type.Nat) -> Some (LitE (ref (PreLit (Big_int.(string_of_big_int (minus_big_int (big_int_of_string n))), Type.Int))))
+         | _ -> None end
+       | _ -> None)
+  | LitE lit as e -> Some e
+  | _ -> None
+
+let finalise_lit (Type.Prim t) lit =
+  let open Type in
+  let open Value in
+  match t, !lit with
+  | Int, PreLit (s, (Nat | Int)) -> lit := IntLit (Big_int.big_int_of_string s);
+  | Int8, PreLit (s, (Nat | Int)) -> lit := Int8Lit (Int_8.of_string s);
+  | Int16, PreLit (s, (Nat | Int)) -> lit := Int16Lit (Int_16.of_string s);
+  | Int32, PreLit (s, (Nat | Int)) -> lit := Int32Lit (Int_32.of_string s);
+  | Int64, PreLit (s, (Nat | Int)) -> lit := Int64Lit (Int_64.of_string s);
+  | _ -> ()

src/as_frontend/typing.ml

@@ -839,7 +839,10 @@ and check_exp' env t exp : T.typ =
     t
   | UnE (ot, op, exp1), _ when Operator.has_unop op t ->
     ot := t;
-    check_exp env t exp1;
+    begin match reduce_constant exp.it with
+    | Some (LitE lit) -> check_lit env t lit exp.at
+    | _ -> check_exp env t exp1
+    end;
     t
   | BinE (ot, exp1, op, exp2), _ when Operator.has_binop op t ->
     ot := t;

src/as_interpreter/interpret.ml

@@ -359,9 +359,13 @@ and interpret_exp_mut env exp (k : V.value V.cont) =
   | LitE lit ->
     k (interpret_lit env lit)
   | UnE (ot, op, exp1) ->
-    interpret_exp env exp1
-      (fun v1 ->
-        k (try Operator.unop op !ot v1 with Invalid_argument s -> trap exp.at "%s" s))
+    begin match reduce_constant exp.it with
+    | Some (LitE lit) -> k (finalise_lit !ot lit; interpret_lit env lit)
+    | _ -> 
+      interpret_exp env exp1
+        (fun v1 ->
+          k (try Operator.unop op !ot v1 with Invalid_argument s -> trap exp.at "%s" s))
+    end
   | BinE (ot, exp1, op, exp2) ->
     interpret_exp env exp1 (fun v1 ->
       interpret_exp env exp2 (fun v2 ->

src/lowering/desugar.ml

@@ -58,8 +58,11 @@ and exp e =
 and exp' at note = function
   | S.VarE i -> I.VarE i.it
   | S.LitE l -> I.LitE (lit !l)
-  | S.UnE (ot, o, e) ->
-    I.PrimE (I.UnPrim (!ot, o), [exp e])
+  | S.UnE (ot, o, e) as exp1 ->
+    begin match S.reduce_constant exp1 with
+    | Some (S.LitE l) -> I.LitE (S.finalise_lit !ot l; lit !l)
+    | _ -> I.PrimE (I.UnPrim (!ot, o), [exp e])
+    end
   | S.BinE (ot, e1, o, e2) ->
     I.PrimE (I.BinPrim (!ot, o), [exp e1; exp e2])
   | S.RelE (ot, e1, o, e2) ->