summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/ocaml_rts/Makefile2
-rw-r--r--lib/ocaml_rts/sail_lib.ml45
-rw-r--r--src/gen_lib/sail_operators_mwords.lem10
-rw-r--r--src/initial_check.ml1
-rw-r--r--src/monomorphise.ml322
-rw-r--r--src/ocaml_backend.ml71
-rw-r--r--src/pretty_print_lem.ml44
-rw-r--r--src/process_file.ml2
-rw-r--r--src/rewriter.mli12
-rw-r--r--src/sail.ml61
-rw-r--r--src/trace_viewer/.gitignore6
-rw-r--r--src/trace_viewer/List-add.svg56
-rw-r--r--src/trace_viewer/List-remove.svg117
-rw-r--r--src/trace_viewer/README11
-rw-r--r--src/trace_viewer/index.css86
-rw-r--r--src/trace_viewer/index.html19
-rw-r--r--src/trace_viewer/index.ts287
-rw-r--r--src/trace_viewer/main.ts12
-rw-r--r--src/trace_viewer/package.json15
-rw-r--r--src/trace_viewer/tsconfig.json18
-rw-r--r--src/type_check.ml26
21 files changed, 1128 insertions, 95 deletions
diff --git a/lib/ocaml_rts/Makefile b/lib/ocaml_rts/Makefile
index eee59dd7..3d837e25 100644
--- a/lib/ocaml_rts/Makefile
+++ b/lib/ocaml_rts/Makefile
@@ -53,7 +53,7 @@ import:
rsync -rv --include "*/" --include="*.ml" --include="*.mli" --exclude="*" $(BITBUCKET_ROOT)/lem/ocaml-lib/ lem
main: import
- ocamlbuild -pkg uint -pkg zarith main.native
+ ocamlbuild -pkg uint -pkg zarith main.native -use-ocamlfind
clean:
rm -r linksem
diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml
index 5f83b9c2..c550b2ce 100644
--- a/lib/ocaml_rts/sail_lib.ml
+++ b/lib/ocaml_rts/sail_lib.ml
@@ -2,6 +2,8 @@ open Big_int
type 'a return = { return : 'b . 'a -> 'b }
+let opt_trace = ref false
+
let trace_depth = ref 0
let random = ref false
@@ -15,12 +17,20 @@ let sail_call (type t) (f : _ -> t) =
with M.Return x -> x
let trace str =
- if !trace_depth < 0 then trace_depth := 0 else ();
- prerr_endline (String.make (!trace_depth * 2) ' ' ^ str)
+ if !opt_trace
+ then
+ begin
+ if !trace_depth < 0 then trace_depth := 0 else ();
+ prerr_endline (String.make (!trace_depth * 2) ' ' ^ str)
+ end
+ else ()
let trace_write name str =
trace ("Write: " ^ name ^ " " ^ str)
+let trace_read name str =
+ trace ("Read: " ^ name ^ " " ^ str)
+
let sail_trace_call (type t) (name : string) (in_string : string) (string_of_out : t -> string) (f : _ -> t) =
let module M =
struct exception Return of t end
@@ -122,7 +132,7 @@ let slice (list, n, m) =
let m = int_of_big_int m in
List.rev (take m (drop n (List.rev list)))
-let eq_list (xs, ys) = List.for_all2 (fun x y -> x == y) xs ys
+let eq_list (xs, ys) = List.for_all2 (fun x y -> x = y) xs ys
let access (xs, n) = List.nth (List.rev xs) (int_of_big_int n)
@@ -233,8 +243,14 @@ let sub_vec_int (v, n) =
sub_vec(v, n_bits)
let get_slice_int (n, m, o) =
- let bits = bits_of_big_int (power_int_positive_big_int 2 (add_big_int n o)) m in
+ let bits = bits_of_big_int (power_int_positive_big_int 2 (add_big_int n o)) (abs_big_int m) in
+ let bits =
+ if lt_big_int m zero_big_int
+ then sub_vec (List.map (fun _ -> B0) bits, bits)
+ else bits
+ in
let slice = List.rev (take (int_of_big_int n) (drop (int_of_big_int o) (List.rev bits))) in
+ assert (eq_big_int (big_int_of_int (List.length slice)) n);
slice
let hex_char = function
@@ -373,7 +389,9 @@ let eq_string (str1, str2) = String.compare str1 str2 == 0
let lt_int (x, y) = lt_big_int x y
let set_slice (out_len, slice_len, out, n, slice) =
- update_subrange(out, n, sub_big_int n (big_int_of_int (List.length slice - 1)), slice)
+ let out = update_subrange(out, add_big_int n (big_int_of_int (List.length slice - 1)), n, slice) in
+ assert (List.length out = int_of_big_int out_len);
+ out
let set_slice_int (_, _, _, _) = assert false
@@ -403,8 +421,18 @@ let min_int (x, y) = min_big_int x y
let undefined_real () = Num.num_of_int 0
+let real_of_string str =
+ try
+ let point = String.index str '.' in
+ let whole = Num.num_of_string (String.sub str 0 point) in
+ let frac_str = String.sub str (point + 1) (String.length str - (point + 1)) in
+ let frac = Num.div_num (Num.num_of_string frac_str) (Num.num_of_big_int (power_int_positive_int 10 (String.length frac_str))) in
+ Num.add_num whole frac
+ with
+ | Not_found -> Num.num_of_string str
+
(* Not a very good sqrt implementation *)
-let sqrt_real x = Num.num_of_string (string_of_float (sqrt (Num.float_of_num x)))
+let sqrt_real x = real_of_string (string_of_float (sqrt (Num.float_of_num x)))
let print_int (str, x) =
prerr_endline (str ^ string_of_big_int x)
@@ -418,3 +446,8 @@ let string_of_zbool = function
| false -> "false"
let string_of_zreal r = Num.string_of_num r
let string_of_zstring str = "\"" ^ String.escaped str ^ "\""
+
+let rec string_of_list sep string_of = function
+ | [] -> ""
+ | [x] -> string_of x
+ | x::ls -> (string_of x) ^ sep ^ (string_of_list sep string_of ls)
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index d4dca80c..8fb55137 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -3,6 +3,16 @@ open import Machine_word
open import Sail_impl_base
open import Sail_values
+(* Translating between a type level number (itself 'n) and an integer *)
+
+let size_itself_int x = integerFromNat (size_itself x)
+
+(* NB: the corresponding sail type is forall 'n. atom('n) -> itself('n),
+ the actual integer is ignored. *)
+
+val make_the_value : forall 'n. integer -> itself 'n
+let inline make_the_value x = the_value
+
(*** Bit vector operations *)
let bitvector_length bs = integerFromNat (word_length bs)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 61e352f5..b33d90f5 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -913,6 +913,7 @@ let initial_kind_env =
("atom", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})});
("option", { k = K_Lam( [{k=K_Typ}], {k=K_Typ}) });
("implicit", {k = K_Lam( [{k = K_Nat}], {k=K_Typ})} );
+ ("itself", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})});
]
let typschm_of_string order str =
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index f00cfd44..f79c1dc3 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -264,24 +264,24 @@ and contains_exist_arg (Typ_arg_aux (arg,_)) =
-> false
| Typ_arg_typ typ -> contains_exist typ
+let rec size_nvars_nexp (Nexp_aux (ne,_)) =
+ match ne with
+ | Nexp_var v -> [v]
+ | Nexp_id _
+ | Nexp_constant _
+ -> []
+ | Nexp_times (n1,n2)
+ | Nexp_sum (n1,n2)
+ | Nexp_minus (n1,n2)
+ -> size_nvars_nexp n1 @ size_nvars_nexp n2
+ | Nexp_exp n
+ | Nexp_neg n
+ -> size_nvars_nexp n
+
(* Given a type for a constructor, work out which refinements we ought to produce *)
(* TODO collision avoidance *)
let split_src_type id ty (TypQ_aux (q,ql)) =
let i = string_of_id id in
- let rec size_nvars_nexp (Nexp_aux (ne,_)) =
- match ne with
- | Nexp_var v -> [v]
- | Nexp_id _
- | Nexp_constant _
- -> []
- | Nexp_times (n1,n2)
- | Nexp_sum (n1,n2)
- | Nexp_minus (n1,n2)
- -> size_nvars_nexp n1 @ size_nvars_nexp n2
- | Nexp_exp n
- | Nexp_neg n
- -> size_nvars_nexp n
- in
(* This was originally written for the general case, but I cut it down to the
more manageable prenex-form below *)
let rec size_nvars_ty (Typ_aux (ty,l) as typ) =
@@ -575,6 +575,32 @@ let lit_match = function
| (L_one | L_true ), (L_one | L_true ) -> true
| l1,l2 -> l1 = l2
+(* There's no undefined nexp, so replace undefined sizes with a plausible size.
+ 32 is used as a sensible default. *)
+let fabricate_nexp l = function
+ | None -> Nexp_aux (Nexp_constant 32,Unknown)
+ | Some (env,typ,_) ->
+ match Type_check.destruct_exist env typ with
+ | None -> Nexp_aux (Nexp_constant 32,Unknown)
+ | Some (kids,nc,typ') ->
+ match kids,nc,Env.expand_synonyms env typ' with
+ | ([kid],NC_aux (NC_set (kid',i::_),_),
+ Typ_aux (Typ_app (Id_aux (Id "range",_),
+ [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_);
+ Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_))
+ when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 &&
+ Kid.compare kid kid''' = 0 ->
+ Nexp_aux (Nexp_constant i,Unknown)
+ | ([kid],NC_aux (NC_true,_),
+ Typ_aux (Typ_app (Id_aux (Id "range",_),
+ [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_);
+ Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_))
+ when Kid.compare kid kid'' = 0 &&
+ Kid.compare kid kid''' = 0 ->
+ Nexp_aux (Nexp_constant 32,Unknown)
+ | _ -> raise (Reporting_basic.err_general l
+ ("Undefined value at unsupported type " ^ string_of_typ typ))
+
type 'a matchresult =
| DoesMatch of 'a
| DoesNotMatch
@@ -614,12 +640,20 @@ let can_match_with_env env (E_aux (e,(l,annot)) as exp0) cases =
let checkpat = function
| P_aux (P_lit (L_aux (lit_p, _)),_) ->
if lit_match (lit_e,lit_p) then DoesMatch ([],[]) else DoesNotMatch
- | P_aux (P_var (P_aux (P_id id,_), kid),_) ->
+ | P_aux (P_var (P_aux (P_id id,p_id_annot), kid),_) ->
begin
match lit_e with
| L_num i ->
DoesMatch ([id, E_aux (e,(l,annot))],
[kid,Nexp_aux (Nexp_constant i,Unknown)])
+ (* For undefined we fix the type-level size (because there's no good
+ way to construct an undefined size), but leave the term as undefined
+ to make the meaning clear. *)
+ | L_undef ->
+ let nexp = fabricate_nexp l annot in
+ let typ = subst_src_typ (KBindings.singleton kid nexp) (typ_of_annot p_id_annot) in
+ DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,None))),(l,None))],
+ [kid,nexp])
| _ ->
(Reporting_basic.print_err false true lit_l "Monomorphisation"
"Unexpected kind of literal for var match"; GiveUp)
@@ -692,7 +726,7 @@ let try_app (l,ann) (Id_aux (id,_),args) =
| _ -> None
else if id = Id "ex_int" then
match args with
- | [E_aux (E_lit (L_aux (L_num _,_)),_) as exp] -> Some exp
+ | [E_aux (E_lit lit,(l,_))] -> Some (E_aux (E_lit lit,(l,ann)))
| _ -> None
else if id = Id "vector_access" || id = Id "bitvector_access" then
match args with
@@ -1444,8 +1478,262 @@ let split_defs splits defs =
| DEF_fundef fd -> [DEF_fundef (map_fundef fd)]
| DEF_val lb -> [DEF_val (map_letbind lb)]
| DEF_scattered sd -> List.map (fun x -> DEF_scattered x) (map_scattered_def sd)
-
in
Defs (List.concat (List.map map_def defs))
in
map_locs splits defs'
+
+
+
+(* The next section of code turns atom('n) types into itself('n) types, which
+ survive into the Lem output, so can be used to parametrise functions over
+ internal bitvector lengths (such as datasize and regsize in ARM specs *)
+
+module AtomToItself =
+struct
+
+let findi f =
+ let rec aux n = function
+ | [] -> None
+ | h::t -> match f h with Some x -> Some (n,x) | _ -> aux (n+1) t
+ in aux 0
+
+let mapat f is xs =
+ let rec aux n = function
+ | _, [] -> []
+ | (i,_)::is, h::t when i = n ->
+ let h' = f h in
+ let t' = aux (n+1) (is, t) in
+ h'::t'
+ | is, h::t ->
+ let t' = aux (n+1) (is, t) in
+ h::t'
+ in aux 0 (is, xs)
+
+let mapat_extra f is xs =
+ let rec aux n = function
+ | _, [] -> [], []
+ | (i,v)::is, h::t when i = n ->
+ let h',x = f v h in
+ let t',xs = aux (n+1) (is, t) in
+ h'::t',x::xs
+ | is, h::t ->
+ let t',xs = aux (n+1) (is, t) in
+ h::t',xs
+ in aux 0 (is, xs)
+
+let tyvars_bound_in_pat pat =
+ let open Rewriter in
+ fst (fold_pat
+ { (compute_pat_alg KidSet.empty KidSet.union) with
+ p_var = (fun ((s,pat),kid) -> KidSet.add kid s, P_var (pat,kid)) }
+ pat)
+let tyvars_bound_in_lb (LB_aux (LB_val (pat,_),_)) = tyvars_bound_in_pat pat
+
+let rec sizes_of_typ (Typ_aux (t,l)) =
+ match t with
+ Typ_wild
+ | Typ_id _
+ | Typ_var _
+ -> KidSet.empty
+ | Typ_fn _ -> raise (Reporting_basic.err_general l
+ "Function type on expressinon")
+ | Typ_tup typs -> kidset_bigunion (List.map sizes_of_typ typs)
+ | Typ_exist (kids,_,typ) ->
+ List.fold_left (fun s k -> KidSet.remove k s) (sizes_of_typ typ) kids
+ | Typ_app (Id_aux (Id "vector",_),
+ [_;Typ_arg_aux (Typ_arg_nexp size,_);
+ _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) ->
+ KidSet.of_list (size_nvars_nexp size)
+ | Typ_app (_,tas) ->
+ kidset_bigunion (List.map sizes_of_typarg tas)
+and sizes_of_typarg (Typ_arg_aux (ta,_)) =
+ match ta with
+ Typ_arg_nexp _
+ | Typ_arg_order _
+ -> KidSet.empty
+ | Typ_arg_typ typ -> sizes_of_typ typ
+
+let sizes_of_annot = function
+ | _,None -> KidSet.empty
+ | _,Some (_,typ,_) -> sizes_of_typ typ
+
+let change_parameter_pat kid = function
+ | P_aux (P_id var, (l,_))
+ | P_aux (P_typ (_,P_aux (P_id var, (l,_))),_)
+ -> P_aux (P_id var, (l,None)), (var,kid)
+ | P_aux (_,(l,_)) -> raise (Reporting_basic.err_unreachable l
+ "Expected variable pattern")
+
+(* We add code to change the itself('n) parameter into the corresponding
+ integer. *)
+let add_var_rebind exp (var,kid) =
+ let l = Generated Unknown in
+ let annot = (l,None) in
+ E_aux (E_let (LB_aux (LB_val (P_aux (P_id var,annot),
+ E_aux (E_app (mk_id "size_itself_int",[E_aux (E_id var,annot)]),annot)),annot),exp),annot)
+
+(* atom('n) arguments to function calls need to be rewritten *)
+let replace_with_the_value (E_aux (_,(l,_)) as exp) =
+ let env = env_of exp in
+ let typ, wrap = match typ_of exp with
+ | Typ_aux (Typ_exist (kids,nc,typ),l) -> typ, fun t -> Typ_aux (Typ_exist (kids,nc,t),l)
+ | typ -> typ, fun x -> x
+ in
+ let typ = Env.expand_synonyms env typ in
+ let mk_exp nexp l l' =
+ E_aux (E_cast (wrap (Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown),
+ [Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated Unknown)),
+ E_aux (E_app (Id_aux (Id "make_the_value",Generated Unknown),[exp]),(Generated l,None))),
+ (Generated l,None))
+ in
+ match typ with
+ | Typ_aux (Typ_app (Id_aux (Id "range",_),
+ [Typ_arg_aux (Typ_arg_nexp nexp,l');Typ_arg_aux (Typ_arg_nexp nexp',_)]),_)
+ when nexp = nexp' ->
+ mk_exp nexp l l'
+ | _ -> raise (Reporting_basic.err_unreachable l
+ "atom stopped being an atom?")
+
+let replace_type env typ =
+ let Typ_aux (t,l) = Env.expand_synonyms env typ in
+ match t with
+ | Typ_app (Id_aux (Id "range",_),
+ [Typ_arg_aux (Typ_arg_nexp nexp,l');Typ_arg_aux (Typ_arg_nexp _,_)]) ->
+ Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown),
+ [Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated l)
+ | _ -> raise (Reporting_basic.err_unreachable l
+ "atom stopped being an atom?")
+
+
+let rewrite_size_parameters env (Defs defs) =
+ let open Rewriter in
+ let size_vars exp =
+ fst (fold_exp
+ { (compute_exp_alg KidSet.empty KidSet.union) with
+ e_aux = (fun ((s,e),annot) -> KidSet.union s (sizes_of_annot annot), E_aux (e,annot));
+ e_let = (fun ((sl,lb),(s2,e2)) -> KidSet.union sl (KidSet.diff s2 (tyvars_bound_in_lb lb)), E_let (lb,e2));
+ pat_exp = (fun ((sp,pat),(s,e)) -> KidSet.diff s (tyvars_bound_in_pat pat), Pat_exp (pat,e))}
+ exp)
+ in
+ let sizes_funcl fsizes (FCL_aux (FCL_Funcl (id,pat,exp),(l,_))) =
+ let sizes = size_vars exp in
+ (* TODO: what, if anything, should sequential be? *)
+ let visible_tyvars =
+ KidSet.union (Pretty_print_lem.lem_tyvars_of_typ false true (pat_typ_of pat))
+ (Pretty_print_lem.lem_tyvars_of_typ false true (typ_of exp))
+ in
+ let expose_tyvars = KidSet.diff sizes visible_tyvars in
+ let parameters = match pat with
+ | P_aux (P_tup ps,_) -> ps
+ | _ -> [pat]
+ in
+ let to_change = List.map
+ (fun kid ->
+ let check (P_aux (_,(_,Some (env,typ,_)))) =
+ match Env.expand_synonyms env typ with
+ Typ_aux (Typ_app(Id_aux (Id "range",_),
+ [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_);
+ Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_) ->
+ if Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 then Some kid else None
+ | _ -> None
+ in match findi check parameters with
+ | None -> raise (Reporting_basic.err_general l
+ ("Unable to find an argument for " ^ string_of_kid kid))
+ | Some i -> i)
+ (KidSet.elements expose_tyvars)
+ in
+ let to_change = List.sort compare to_change in
+ match Bindings.find id fsizes with
+ | old -> if old = to_change then fsizes else
+ raise (Reporting_basic.err_general l
+ ("Different size type variables in different clauses of " ^ string_of_id id))
+ | exception Not_found -> Bindings.add id to_change fsizes
+ in
+ let sizes_def fsizes = function
+ | DEF_fundef (FD_aux (FD_function (_,_,_,funcls),_)) ->
+ List.fold_left sizes_funcl fsizes funcls
+ | _ -> fsizes
+ in
+ let fn_sizes = List.fold_left sizes_def Bindings.empty defs in
+
+ let rewrite_e_app (id,args) =
+ match Bindings.find id fn_sizes with
+ | [] -> E_app (id,args)
+ | to_change ->
+ let args' = mapat replace_with_the_value to_change args in
+ E_app (id,args')
+ | exception Not_found -> E_app (id,args)
+ in
+ let rewrite_funcl (FCL_aux (FCL_Funcl (id,pat,body),(l,annot))) =
+ let pat,body =
+ (* Update pattern and add itself -> nat wrapper to body *)
+ match Bindings.find id fn_sizes with
+ | [] -> pat,body
+ | to_change ->
+ let pat, vars =
+ match pat with
+ P_aux (P_tup pats,(l,_)) ->
+ let pats, vars = mapat_extra change_parameter_pat to_change pats in
+ P_aux (P_tup pats,(l,None)), vars
+ | P_aux (_,(l,_)) ->
+ begin
+ match to_change with
+ | [0,kid] ->
+ let pat, var = change_parameter_pat kid pat in
+ pat, [var]
+ | _ ->
+ raise (Reporting_basic.err_unreachable l
+ "Expected multiple parameters at single parameter")
+ end
+ in
+ let body = List.fold_left add_var_rebind body vars in
+ pat,body
+ | exception Not_found -> pat,body
+ in
+ (* Update function applications *)
+ let body = fold_exp { id_exp_alg with e_app = rewrite_e_app } body in
+ FCL_aux (FCL_Funcl (id,pat,body),(l,None))
+ in
+ let rewrite_def = function
+ | DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,funcls),(l,_))) ->
+ (* TODO rewrite tannopt? *)
+ DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,List.map rewrite_funcl funcls),(l,None)))
+ | DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,annot))) as spec ->
+ begin
+ match Bindings.find id fn_sizes with
+ | [] -> spec
+ | to_change ->
+ let typschm = match typschm with
+ | TypSchm_aux (TypSchm_ts (tq,typ),l) ->
+ let typ = match typ with
+ | Typ_aux (Typ_fn (Typ_aux (Typ_tup ts,l),t2,eff),l2) ->
+ Typ_aux (Typ_fn (Typ_aux (Typ_tup (mapat (replace_type env) to_change ts),l),t2,eff),l2)
+ | _ -> replace_type env typ
+ in TypSchm_aux (TypSchm_ts (tq,typ),l)
+ in
+ DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,None)))
+ | exception Not_found -> spec
+ end
+ | def -> def
+ in
+(*
+ Bindings.iter (fun id args ->
+ print_endline (string_of_id id ^ " needs " ^
+ String.concat ", " (List.map string_of_int args))) fn_sizes
+*)
+ Defs (List.map rewrite_def defs)
+
+end
+
+let monomorphise mwords splits defs =
+ let defs = split_defs splits defs in
+ (* TODO: currently doing this because constant propagation leaves numeric literals as
+ int, try to avoid this later; also use final env for DEF_spec case above, because the
+ type checker doesn't store the env at that point :( *)
+ if mwords then
+ let (defs,env) = Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs in
+ let defs = AtomToItself.rewrite_size_parameters env defs in
+ defs
+ else
+ defs
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 384d8109..5a378fa6 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -3,6 +3,9 @@ open Ast_util
open PPrint
open Type_check
+(* Option to turn tracing features on or off *)
+let opt_trace_ocaml = ref false
+
type ctx =
{ register_inits : tannot exp list;
externs : id Bindings.t;
@@ -61,7 +64,10 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, _)) arg =
match typ_aux with
| Typ_id id -> ocaml_string_of id ^^ space ^^ arg
| Typ_app (id, []) -> ocaml_string_of id ^^ space ^^ arg
- | Typ_app (id, typs) -> string ("\"APP" ^ string_of_id id ^ "\"")
+ | Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) ->
+ let farg = gensym () in
+ separate space [string "string_of_list \", \""; parens (separate space [string "fun"; farg; string "->"; ocaml_string_typ typ farg]); arg]
+ | Typ_app (_, _) -> assert false
| Typ_tup typs ->
let args = List.map (fun _ -> gensym ()) typs in
let body =
@@ -72,6 +78,7 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, _)) arg =
| Typ_fn (typ1, typ2, _) -> string "\"FN\""
| Typ_var kid -> string "\"VAR\""
| Typ_exist _ | Typ_wild -> assert false
+
let ocaml_typ_id ctx = function
| id when Id.compare id (mk_id "string") = 0 -> string "string"
| id when Id.compare id (mk_id "list") = 0 -> string "list"
@@ -119,7 +126,7 @@ let ocaml_lit (L_aux (lit_aux, _)) =
| L_num n -> parens (string "big_int_of_int" ^^ space ^^ string (string_of_int n))
| L_undef -> failwith "undefined should have been re-written prior to ocaml backend"
| L_string str -> string_lit str
- | L_real str -> parens (string "Num.num_of_string" ^^ space ^^ dquotes (string (String.escaped str)))
+ | L_real str -> parens (string "real_of_string" ^^ space ^^ dquotes (string (String.escaped str)))
| _ -> string "LIT"
let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) =
@@ -199,11 +206,20 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
^/^ string "in"
^/^ string "loop ()"
| E_lit _ | E_list _ | E_id _ | E_tuple _ -> ocaml_atomic_exp ctx exp
- | E_for (id, exp_from, exp_to, exp_step, _, exp_body) ->
+ | E_for (id, exp_from, exp_to, exp_step, ord, exp_body) ->
let loop_var = separate space [string "let"; zencode ctx id; equals; string "ref"; ocaml_atomic_exp ctx exp_from; string "in"] in
- let loop_mod = string "add_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step in
+ let loop_mod =
+ match ord with
+ | Ord_aux (Ord_inc, _) -> string "add_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step
+ | Ord_aux (Ord_dec, _) -> string "sub_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step
+ in
+ let loop_compare =
+ match ord with
+ | Ord_aux (Ord_inc, _) -> string "le_big_int"
+ | Ord_aux (Ord_dec, _) -> string "gt_big_int"
+ in
let loop_body =
- separate space [string "if"; zencode ctx id; string "<="; ocaml_atomic_exp ctx exp_to]
+ separate space [string "if"; loop_compare; zencode ctx id; ocaml_atomic_exp ctx exp_to]
^/^ separate space [string "then";
parens (ocaml_atomic_exp ctx exp_body ^^ semi ^^ space ^^ string "loop" ^^ space ^^ parens loop_mod)]
^/^ string "else ()"
@@ -240,7 +256,13 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
match Env.lookup_id id (env_of exp) with
| Local (Immutable, _) | Unbound -> zencode ctx id
| Enum _ | Union _ -> zencode_upper ctx id
- | Register _ -> parens (string ("trace \"Read: " ^ string_of_id id ^ "\";") ^^ space ^^ bang ^^ zencode ctx id)
+ | Register typ ->
+ if !opt_trace_ocaml then
+ let var = gensym () in
+ let str_typ = parens (ocaml_string_typ (Rewriter.simple_typ typ) var) in
+ parens (separate space [string "let"; var; equals; bang ^^ zencode ctx id; string "in";
+ string "trace_read" ^^ space ^^ string_lit (string_of_id id) ^^ space ^^ str_typ ^^ semi; var])
+ else bang ^^ zencode ctx id
| Local (Mutable, _) -> bang ^^ zencode ctx id
end
| E_list exps -> enclose lbracket rbracket (separate_map (semi ^^ space) (ocaml_exp ctx) exps)
@@ -254,8 +276,12 @@ and ocaml_assignment ctx (LEXP_aux (lexp_aux, _) as lexp) exp =
| Register typ ->
let var = gensym () in
let traced_exp =
- parens (separate space [string "let"; var; equals; ocaml_atomic_exp ctx exp; string "in";
- string "trace_write" ^^ space ^^ string_lit (string_of_id id) ^^ space ^^ parens (ocaml_string_typ (Rewriter.simple_typ typ) var) ^^ semi; var])
+ if !opt_trace_ocaml then
+ let var = gensym () in
+ let str_typ = parens (ocaml_string_typ (Rewriter.simple_typ typ) var) in
+ parens (separate space [string "let"; var; equals; ocaml_atomic_exp ctx exp; string "in";
+ string "trace_write" ^^ space ^^ string_lit (string_of_id id) ^^ space ^^ str_typ ^^ semi; var])
+ else ocaml_atomic_exp ctx exp
in
separate space [zencode ctx id; string ":="; traced_exp]
| _ -> separate space [zencode ctx id; string ":="; ocaml_exp ctx exp]
@@ -331,22 +357,36 @@ let ocaml_funcls ctx =
in
(arg_sym, string_of_arg, ret_sym, string_of_ret)
in
+ let sail_call id arg_sym pat_sym ret_sym =
+ if !opt_trace_ocaml
+ then separate space [string "sail_trace_call"; string_lit (string_of_id id); parens (arg_sym ^^ space ^^ pat_sym); ret_sym]
+ else separate space [string "sail_call"]
+ in
+ let ocaml_funcl call string_of_arg string_of_ret =
+ if !opt_trace_ocaml
+ then (call ^^ twice hardline ^^ string_of_arg ^^ twice hardline ^^ string_of_ret)
+ else call
+ in
function
| [] -> failwith "Ocaml: empty function"
| [FCL_aux (FCL_Funcl (id, pat, exp),_)] ->
let Typ_aux (Typ_fn (typ1, typ2, _), _) = Bindings.find id ctx.val_specs in
let pat_sym = gensym () in
- let annot_pat = parens (separate space [parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1); string "as"; pat_sym]) in
+ let annot_pat =
+ let pat = parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1) in
+ if !opt_trace_ocaml
+ then parens (separate space [pat; string "as"; pat_sym])
+ else pat
+ in
let call_header = function_header () in
let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info typ1 typ2 in
let call =
separate space [call_header; zencode ctx id; annot_pat; colon; ocaml_typ ctx typ2; equals;
- string "sail_trace_call"; string_lit (string_of_id id); parens (arg_sym ^^ space ^^ pat_sym); ret_sym;
- string "(fun r ->"]
+ sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
^//^ ocaml_exp ctx exp
^^ rparen
in
- call ^^ twice hardline ^^ string_of_arg ^^ twice hardline ^^ string_of_ret
+ ocaml_funcl call string_of_arg string_of_ret
| funcls ->
let id = funcls_id funcls in
let Typ_aux (Typ_fn (typ1, typ2, _), _) = Bindings.find id ctx.val_specs in
@@ -355,12 +395,11 @@ let ocaml_funcls ctx =
let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info typ1 typ2 in
let call =
separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1); equals;
- string "sail_trace_call"; string_lit (string_of_id id); parens (arg_sym ^^ space ^^ pat_sym); ret_sym;
- string "(fun r ->"]
+ sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
^//^ (separate space [string "match"; pat_sym; string "with"] ^^ hardline ^^ ocaml_funcl_matches ctx funcls)
^^ rparen
in
- call ^^ twice hardline ^^ string_of_arg ^^ twice hardline ^^ string_of_ret
+ ocaml_funcl call string_of_arg string_of_ret
let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) =
ocaml_funcls ctx funcls
@@ -391,7 +430,6 @@ let rec ocaml_enum ctx = function
(* We generate a string_of_X ocaml function for each type X, to be used for debugging purposes *)
-
let ocaml_def_end = string ";;" ^^ twice hardline
let ocaml_string_of_enum ctx id ids =
@@ -491,6 +529,7 @@ let ocaml_main spec =
separate space [string "let"; string "()"; equals]
^//^ (string "Random.self_init ();"
^/^ string "load_elf ();"
+ ^/^ string (if !opt_trace_ocaml then "Sail_lib.opt_trace := true;" else "Sail_lib.opt_trace := false;")
^/^ string "initialize_registers ();"
^/^ string "Printexc.record_backtrace true;"
^/^ string "zmain ()")
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index d6ec25dc..7a29579b 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -152,7 +152,9 @@ let is_regtyp (Typ_aux (typ, _)) env = match typ with
| Typ_id(id) when Env.is_regtyp id env -> true
| _ -> false
-let doc_nexp_lem (Nexp_aux (nexp, l) as full_nexp) = match nexp with
+let doc_nexp_lem nexp =
+ let (Nexp_aux (nexp, l) as full_nexp) = nexp_simp nexp in
+ match nexp with
| Nexp_constant i -> string ("ty" ^ string_of_int i)
| Nexp_var v -> string (string_of_kid (orig_kid v))
| _ ->
@@ -427,9 +429,12 @@ let rec typeclass_nexps (Typ_aux(t,_)) = match t with
| Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts)
| Typ_app (Id_aux (Id "vector",_),
[_;Typ_arg_aux (Typ_arg_nexp size_nexp,_);
- _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) ->
- if is_nexp_constant (nexp_simp size_nexp) then NexpSet.empty else
- NexpSet.singleton (nexp_simp (orig_nexp size_nexp))
+ _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)])
+| Typ_app (Id_aux (Id "itself",_),
+ [Typ_arg_aux (Typ_arg_nexp size_nexp,_)]) ->
+ let size_nexp = nexp_simp size_nexp in
+ if is_nexp_constant size_nexp then NexpSet.empty else
+ NexpSet.singleton (orig_nexp size_nexp)
| Typ_app _ -> NexpSet.empty
| Typ_exist (kids,_,t) -> NexpSet.empty (* todo *)
@@ -493,13 +498,14 @@ let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) =
| P_cons (p,p') -> doc_op (string "::") (doc_pat_lem sequential mwords true p) (doc_pat_lem sequential mwords true p')
| P_record (_,_) -> empty (* TODO *)
-let rec contains_bitvector_typ (Typ_aux (t,_) as typ) = match t with
- | Typ_tup ts -> List.exists contains_bitvector_typ ts
- | Typ_app (_, targs) -> is_bitvector_typ typ || List.exists contains_bitvector_typ_arg targs
- | Typ_fn (t1,t2,_) -> contains_bitvector_typ t1 || contains_bitvector_typ t2
+let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with
+ | Typ_tup ts -> List.exists typ_needs_printed ts
+ | Typ_app (Id_aux (Id "itself",_),_) -> true
+ | Typ_app (_, targs) -> is_bitvector_typ typ || List.exists typ_needs_printed_arg targs
+ | Typ_fn (t1,t2,_) -> typ_needs_printed t1 || typ_needs_printed t2
| _ -> false
-and contains_bitvector_typ_arg (Typ_arg_aux (targ, _)) = match targ with
- | Typ_arg_typ t -> contains_bitvector_typ t
+and typ_needs_printed_arg (Typ_arg_aux (targ, _)) = match targ with
+ | Typ_arg_typ t -> typ_needs_printed t
| _ -> false
let contains_early_return exp =
@@ -698,7 +704,7 @@ let doc_exp_lem, doc_let_lem =
let (taepp,aexp_needed) =
let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
let eff = effect_of full_exp in
- if contains_bitvector_typ t && not (contains_t_pp_var t)
+ if typ_needs_printed t && not (contains_t_pp_var t)
then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true)
else (epp, aexp_needed) in
if aexp_needed then parens (align taepp) else taepp*)
@@ -740,7 +746,7 @@ let doc_exp_lem, doc_let_lem =
let (taepp,aexp_needed) =
let t = (*Env.base_typ_of (env_of full_exp)*) (typ_of full_exp) in
let eff = effect_of full_exp in
- if contains_bitvector_typ (Env.base_typ_of (env_of full_exp) t)
+ if typ_needs_printed (Env.base_typ_of (env_of full_exp) t)
then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true)
else (epp, aexp_needed) in
liftR (if aexp_needed then parens (align taepp) else taepp)
@@ -798,7 +804,7 @@ let doc_exp_lem, doc_let_lem =
let (epp,aexp_needed) =
if has_effect eff BE_rreg then
let epp = align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in
- if contains_bitvector_typ t && not (contains_t_pp_var t)
+ if typ_needs_printed t && not (contains_t_pp_var t)
then (epp ^^ doc_tannot_lem sequential mwords true t, true)
else (epp, aexp_needed)
else
@@ -819,7 +825,7 @@ let doc_exp_lem, doc_let_lem =
let eff = effect_of full_exp in
let field_f = doc_id_lem tid ^^ underscore ^^ doc_id_lem id ^^ dot ^^ string "get_field" in
let (ta,aexp_needed) =
- if contains_bitvector_typ t
+ if typ_needs_printed t
then (doc_tannot_lem sequential mwords (effectful eff) t, true)
else (empty, aexp_needed) in
let epp = field_f ^^ space ^^ (expY fexp) in
@@ -854,7 +860,7 @@ let doc_exp_lem, doc_let_lem =
| Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> "read_reg_bitfield"
| _ -> "read_reg_field" in
let ta =
- if contains_bitvector_typ t && not (contains_t_pp_var t)
+ if typ_needs_printed t && not (contains_t_pp_var t)
then doc_tannot_lem sequential mwords true t else empty in
let epp = separate space [string call;string reg;string_lit(string field)] ^^ ta in
if aexp_needed then parens (align epp) else epp
@@ -862,7 +868,7 @@ let doc_exp_lem, doc_let_lem =
let (call,ta) =
if has_effect eff BE_rreg then
let ta =
- if contains_bitvector_typ t && not (contains_t_pp_var t)
+ if typ_needs_printed t && not (contains_t_pp_var t)
then doc_tannot_lem sequential mwords true t else empty in
("read_two_regs", ta)
else
@@ -875,7 +881,7 @@ let doc_exp_lem, doc_let_lem =
separate space [string "read_reg_bit";string reg;doc_int start]
else
let ta =
- if contains_bitvector_typ t && not (contains_t_pp_var t)
+ if typ_needs_printed t && not (contains_t_pp_var t)
then doc_tannot_lem sequential mwords true t else empty in
separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in
if aexp_needed then parens (align epp) else epp
@@ -887,7 +893,7 @@ let doc_exp_lem, doc_let_lem =
| Base((_,t),External _,_,_,_,_) ->
(* TODO: Does this case still exist with the new type checker? *)
let epp = string "read_reg" ^^ space ^^ expY e in
- if contains_bitvector_typ t && not (contains_t_pp_var t)
+ if typ_needs_printed t && not (contains_t_pp_var t)
then parens (epp ^^ doc_tannot_lem sequential mwords true t) else epp
| Base((_,t),_,_,_,_,_) ->
(match typ with
@@ -1117,7 +1123,7 @@ let doc_exp_lem, doc_let_lem =
| _ ->
string name ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in
let (epp,aexp_needed) =
- if contains_bitvector_typ t && not (contains_t_pp_var t)
+ if typ_needs_printed t && not (contains_t_pp_var t)
then (parens epp ^^ doc_tannot_lem sequential mwords false t, true)
else (epp, aexp_needed) in
if aexp_needed then parens (align epp) else epp
diff --git a/src/process_file.ml b/src/process_file.ml
index 59518075..aea53ca7 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -121,7 +121,7 @@ let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.E
let opt_ddump_raw_mono_ast = ref false
let monomorphise_ast locs ast =
- let ast = Monomorphise.split_defs locs ast in
+ let ast = Monomorphise.monomorphise (!opt_lem_mwords) locs ast in
let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in
let ienv = Type_check.Env.no_casts Type_check.initial_env in
Type_check.check ienv ast
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 3125c410..3f375e25 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -151,12 +151,24 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg
}
+(* fold over patterns *)
+val fold_pat : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg -> 'a pat -> 'pat
+
(* fold over expressions *)
val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a exp -> 'exp
val id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg
+val id_exp_alg :
+ ('a,'a exp,'a exp_aux,'a lexp,'a lexp_aux,'a fexp,
+ 'a fexp_aux,'a fexps,'a fexps_aux,
+ 'a opt_default_aux,'a opt_default,'a pexp,'a pexp_aux,
+ 'a letbind_aux,'a letbind,
+ 'a pat,'a pat_aux,'a fpat,'a fpat_aux) exp_alg
+
+val compute_pat_alg : 'b -> ('b -> 'b -> 'b) ->
+ ('a,('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) pat_alg
val compute_exp_alg : 'b -> ('b -> 'b -> 'b) ->
('a,('b * 'a exp),('b * 'a exp_aux),('b * 'a lexp),('b * 'a lexp_aux),('b * 'a fexp),
diff --git a/src/sail.ml b/src/sail.ml
index 9c447f36..8a70cb70 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -56,39 +56,35 @@ let opt_libs_lem = ref ([]:string list)
let opt_libs_ocaml = ref ([]:string list)
let opt_file_arguments = ref ([]:string list)
let opt_mono_split = ref ([]:((string * int) * string) list)
+
let options = Arg.align ([
( "-o",
Arg.String (fun f -> opt_file_out := Some f),
"<prefix> select output filename prefix");
+ ( "-ocaml",
+ Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen],
+ " output an OCaml translated version of the input");
+ ( "-ocaml_trace",
+ Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen; Arg.Set Ocaml_backend.opt_trace_ocaml],
+ " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml");
+ ( "-ocaml_lib",
+ Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml),
+ "<filename> provide additional library to open in OCaml output");
( "-lem_ast",
Arg.Set opt_print_lem_ast,
" output a Lem AST representation of the input");
( "-lem",
Arg.Set opt_print_lem,
" output a Lem translated version of the input");
- ( "-ocaml",
- Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen],
- " output an OCaml translated version of the input");
( "-lem_lib",
Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem),
"<filename> provide additional library to open in Lem output");
- ( "-ocaml_lib",
- Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml),
- "<filename> provide additional library to open in OCaml output");
( "-lem_sequential",
Arg.Set Process_file.opt_lem_sequential,
" use sequential state monad for Lem output");
( "-lem_mwords",
Arg.Set Process_file.opt_lem_mwords,
" use native machine word library for Lem output");
-(*
- ( "-i",
- Arg.String (fun l -> lib := l::!lib),
- "<library_filename> treat this file as input only and generate no output for it");
-*)
- ( "-verbose",
- Arg.Set opt_print_verbose,
- " (debug) pretty-print the input to standard output");
( "-mono-split",
Arg.String (fun s ->
let l = Util.split_on_char ':' s in
@@ -96,39 +92,42 @@ let options = Arg.align ([
| [fname;line;var] -> opt_mono_split := ((fname,int_of_string line),var)::!opt_mono_split
| _ -> raise (Arg.Bad (s ^ " not of form <filename>:<line>:<variable>"))),
"<filename>:<line>:<variable> to case split for monomorphisation");
- ( "-ddump_raw_mono_ast",
- Arg.Set opt_ddump_raw_mono_ast,
- " (debug) dump the monomorphised ast before type-checking");
+ ( "-memo_z3",
+ Arg.Set opt_memo_z3,
+ " memoize calls to z3, improving performance when typechecking repeatedly");
+ ( "-undefined_gen",
+ Arg.Set Initial_check.opt_undefined_gen,
+ " generate undefined_type functions for types in the specification");
+ ( "-no_effects",
+ Arg.Set Type_check.opt_no_effects,
+ " (experimental) turn off effect checking");
( "-new_parser",
Arg.Set Process_file.opt_new_parser,
" (experimental) use new parser");
+ ( "-convert",
+ Arg.Set opt_convert,
+ " (experimental) convert sail to new syntax for use with -new_parser");
( "-just_check",
Arg.Set opt_just_check,
" (experimental) terminate immediately after typechecking");
- ( "-convert",
- Arg.Set opt_convert,
- " Convert sail to new syntax");
- ( "-memo_z3",
- Arg.Set opt_memo_z3,
- " Memoize calls to z3");
+ ( "-ddump_raw_mono_ast",
+ Arg.Set opt_ddump_raw_mono_ast,
+ " (debug) dump the monomorphised ast before type-checking");
+ ( "-verbose",
+ Arg.Set opt_print_verbose,
+ " (debug) pretty-print the input to standard output");
( "-ddump_tc_ast",
Arg.Set opt_ddump_tc_ast,
" (debug) dump the typechecked ast to stdout");
( "-ddump_rewrite_ast",
Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0)),
- " <prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem");
+ "<prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem");
( "-dtc_verbose",
Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity),
- " (debug) verbose typechecker output: 0 is silent");
+ "<verbosity> (debug) verbose typechecker output: 0 is silent");
( "-dno_cast",
Arg.Set opt_dno_cast,
" (debug) typecheck without any implicit casting");
- ( "-no_effects",
- Arg.Set Type_check.opt_no_effects,
- " turn off effect checking");
- ( "-undefined_gen",
- Arg.Set Initial_check.opt_undefined_gen,
- " generate undefined_type functions for types in the specification");
( "-v",
Arg.Set opt_print_version,
" print version");
diff --git a/src/trace_viewer/.gitignore b/src/trace_viewer/.gitignore
new file mode 100644
index 00000000..c1f9aea6
--- /dev/null
+++ b/src/trace_viewer/.gitignore
@@ -0,0 +1,6 @@
+*~
+*.js
+*.js.map
+
+# Dependencies
+node_modules/
diff --git a/src/trace_viewer/List-add.svg b/src/trace_viewer/List-add.svg
new file mode 100644
index 00000000..f8031599
--- /dev/null
+++ b/src/trace_viewer/List-add.svg
@@ -0,0 +1,56 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+<svg id="svg6431" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns="http://www.w3.org/2000/svg" sodipodi:docname="list-add.svg" xmlns:sodipodi="http://inkscape.sourceforge.net/DTD/sodipodi-0.dtd" height="48px" sodipodi:version="0.32" width="48px" xmlns:cc="http://web.resource.org/cc/" xmlns:xlink="http://www.w3.org/1999/xlink" sodipodi:docbase="/home/jimmac/src/cvs/tango-icon-theme/scalable/actions" xmlns:dc="http://purl.org/dc/elements/1.1/">
+ <defs id="defs6433">
+ <linearGradient id="linearGradient4975" y2="48.548" gradientUnits="userSpaceOnUse" x2="45.919" gradientTransform="translate(-18.018 -13.571)" y1="36.423" x1="34.893">
+ <stop id="stop1324" stop-color="#729fcf" offset="0"/>
+ <stop id="stop1326" stop-color="#5187d6" offset="1"/>
+ </linearGradient>
+ <linearGradient id="linearGradient7922" y2="34.977" gradientUnits="userSpaceOnUse" x2="27.901" y1="22.852" x1="16.875">
+ <stop id="stop7918" stop-color="#fff" offset="0"/>
+ <stop id="stop7920" stop-color="#fff" stop-opacity=".34021" offset="1"/>
+ </linearGradient>
+ <radialGradient id="radialGradient2097" gradientUnits="userSpaceOnUse" cy="35.127" cx="23.071" gradientTransform="matrix(.91481 .012650 -.0082150 .21356 2.2539 27.189)" r="10.319">
+ <stop id="stop2093" offset="0"/>
+ <stop id="stop2095" stop-opacity="0" offset="1"/>
+ </radialGradient>
+ </defs>
+ <sodipodi:namedview id="base" bordercolor="#666666" pagecolor="#ffffff" showgrid="false" borderopacity="0.15686275" showguides="true"/>
+ <metadata id="metadata6436">
+ <rdf:RDF>
+ <cc:Work rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type rdf:resource="http://purl.org/dc/dcmitype/StillImage"/>
+ <dc:title>Add</dc:title>
+ <dc:date>2006-01-04</dc:date>
+ <dc:creator>
+ <cc:Agent>
+ <dc:title>Andreas Nilsson</dc:title>
+ </cc:Agent>
+ </dc:creator>
+ <dc:source>http://tango-project.org</dc:source>
+ <dc:subject>
+ <rdf:Bag>
+ <rdf:li>add</rdf:li>
+ <rdf:li>plus</rdf:li>
+ </rdf:Bag>
+ </dc:subject>
+ <cc:license rdf:resource="http://creativecommons.org/licenses/by-sa/2.0/"/>
+ </cc:Work>
+ <cc:License rdf:about="http://creativecommons.org/licenses/by-sa/2.0/">
+ <cc:permits rdf:resource="http://web.resource.org/cc/Reproduction"/>
+ <cc:permits rdf:resource="http://web.resource.org/cc/Distribution"/>
+ <cc:requires rdf:resource="http://web.resource.org/cc/Notice"/>
+ <cc:requires rdf:resource="http://web.resource.org/cc/Attribution"/>
+ <cc:permits rdf:resource="http://web.resource.org/cc/DerivativeWorks"/>
+ <cc:requires rdf:resource="http://web.resource.org/cc/ShareAlike"/>
+ </cc:License>
+ </rdf:RDF>
+ </metadata>
+ <g id="layer1">
+ <path id="path1361" sodipodi:rx="10.319340" sodipodi:ry="2.3201940" sodipodi:type="arc" d="m33.278 34.941a10.319 2.3202 0 1 1 -20.638 0 10.319 2.3202 0 1 1 20.638 0z" opacity=".2" transform="matrix(1.5505 0 0 1.293 -11.597 -8.1782)" sodipodi:cy="34.940620" sodipodi:cx="22.958872" fill="url(#radialGradient2097)"/>
+ <path id="text1314" d="m27.514 37.543v-9.027l9.979-0.04v-6.996h-9.97l-0.009-9.96-7.016 0.011 0.005 9.931-9.99 0.074-0.036 6.969 10.034-0.029 0.007 9.04 6.996 0.027z" sodipodi:nodetypes="ccccccccccccc" stroke="#3465a4" stroke-width="1px" fill="#75a1d0"/>
+ <path id="path7076" opacity=".40860" d="m26.499 36.534v-9.034h10.002l-0.006-5.025h-9.987v-9.995l-4.995 0.018 0.009 9.977-10.026 0.018-0.027 4.973 10.064 0.009-0.013 9.028 4.979 0.031z" sodipodi:nodetypes="ccccccccccccc" stroke="url(#linearGradient7922)" stroke-width="1px" fill="url(#linearGradient4975)"/>
+ <path id="path7914" opacity=".31183" d="m11 25c0 1.938 25.984-0.969 25.984-0.031v-3l-9.984 0.031v-9.965h-6v9.965h-10v3z" fill-rule="evenodd" sodipodi:nodetypes="ccccccccc" fill="#fff"/>
+ </g>
+</svg>
diff --git a/src/trace_viewer/List-remove.svg b/src/trace_viewer/List-remove.svg
new file mode 100644
index 00000000..18c9a135
--- /dev/null
+++ b/src/trace_viewer/List-remove.svg
@@ -0,0 +1,117 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+<svg xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:cc="http://web.resource.org/cc/" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:svg="http://www.w3.org/2000/svg" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:sodipodi="http://inkscape.sourceforge.net/DTD/sodipodi-0.dtd" xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape" width="48px" height="48px" id="svg6431" sodipodi:version="0.32" inkscape:version="0.43+devel" sodipodi:docbase="/home/jimmac/src/cvs/tango-icon-theme/scalable/actions" sodipodi:docname="list-remove.svg">
+ <defs id="defs6433">
+ <linearGradient inkscape:collect="always" id="linearGradient2091">
+ <stop style="stop-color:#000000;stop-opacity:1;" offset="0" id="stop2093"/>
+ <stop style="stop-color:#000000;stop-opacity:0;" offset="1" id="stop2095"/>
+ </linearGradient>
+ <radialGradient inkscape:collect="always" xlink:href="#linearGradient2091" id="radialGradient2097" cx="23.070683" cy="35.127438" fx="23.070683" fy="35.127438" r="10.319340" gradientTransform="matrix(0.914812,1.265023e-2,-8.21502e-3,0.213562,2.253914,27.18889)" gradientUnits="userSpaceOnUse"/>
+ <linearGradient id="linearGradient7916">
+ <stop style="stop-color:#ffffff;stop-opacity:1;" offset="0" id="stop7918"/>
+ <stop style="stop-color:#ffffff;stop-opacity:0.34020618;" offset="1.0000000" id="stop7920"/>
+ </linearGradient>
+ <linearGradient inkscape:collect="always" id="linearGradient8662">
+ <stop style="stop-color:#000000;stop-opacity:1;" offset="0" id="stop8664"/>
+ <stop style="stop-color:#000000;stop-opacity:0;" offset="1" id="stop8666"/>
+ </linearGradient>
+ <radialGradient inkscape:collect="always" xlink:href="#linearGradient8662" id="radialGradient1503" gradientUnits="userSpaceOnUse" gradientTransform="matrix(1.000000,0.000000,0.000000,0.536723,-1.018989e-13,16.87306)" cx="24.837126" cy="36.421127" fx="24.837126" fy="36.421127" r="15.644737"/>
+ <linearGradient inkscape:collect="always" id="linearGradient2847">
+ <stop style="stop-color:#3465a4;stop-opacity:1;" offset="0" id="stop2849"/>
+ <stop style="stop-color:#3465a4;stop-opacity:0;" offset="1" id="stop2851"/>
+ </linearGradient>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient2847" id="linearGradient1488" gradientUnits="userSpaceOnUse" gradientTransform="matrix(-1.000000,0.000000,0.000000,-1.000000,-1.242480,40.08170)" x1="37.128052" y1="29.729605" x2="37.065414" y2="26.194071"/>
+ <linearGradient id="linearGradient2831">
+ <stop style="stop-color:#3465a4;stop-opacity:1;" offset="0" id="stop2833"/>
+ <stop id="stop2855" offset="0.33333334" style="stop-color:#5b86be;stop-opacity:1;"/>
+ <stop style="stop-color:#83a8d8;stop-opacity:0;" offset="1" id="stop2835"/>
+ </linearGradient>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient2831" id="linearGradient1486" gradientUnits="userSpaceOnUse" gradientTransform="translate(-48.30498,-6.043298)" x1="13.478554" y1="10.612206" x2="15.419417" y2="19.115122"/>
+ <linearGradient id="linearGradient2380">
+ <stop style="stop-color:#b9cfe7;stop-opacity:1" offset="0" id="stop2382"/>
+ <stop style="stop-color:#729fcf;stop-opacity:1" offset="1" id="stop2384"/>
+ </linearGradient>
+ <linearGradient id="linearGradient2682">
+ <stop style="stop-color:#3977c3;stop-opacity:1;" offset="0" id="stop2684"/>
+ <stop style="stop-color:#89aedc;stop-opacity:0;" offset="1" id="stop2686"/>
+ </linearGradient>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient2682" id="linearGradient2688" x1="36.713837" y1="31.455952" x2="37.124462" y2="24.842253" gradientUnits="userSpaceOnUse" gradientTransform="translate(-48.77039,-5.765705)"/>
+ <linearGradient inkscape:collect="always" id="linearGradient2690">
+ <stop style="stop-color:#c4d7eb;stop-opacity:1;" offset="0" id="stop2692"/>
+ <stop style="stop-color:#c4d7eb;stop-opacity:0;" offset="1" id="stop2694"/>
+ </linearGradient>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient2690" id="linearGradient2696" x1="32.647972" y1="30.748846" x2="37.124462" y2="24.842253" gradientUnits="userSpaceOnUse" gradientTransform="translate(-48.77039,-5.765705)"/>
+ <linearGradient inkscape:collect="always" id="linearGradient2871">
+ <stop style="stop-color:#3465a4;stop-opacity:1;" offset="0" id="stop2873"/>
+ <stop style="stop-color:#3465a4;stop-opacity:1" offset="1" id="stop2875"/>
+ </linearGradient>
+ <linearGradient id="linearGradient2402">
+ <stop style="stop-color:#729fcf;stop-opacity:1;" offset="0" id="stop2404"/>
+ <stop style="stop-color:#528ac5;stop-opacity:1;" offset="1" id="stop2406"/>
+ </linearGradient>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient2797" id="linearGradient1493" gradientUnits="userSpaceOnUse" x1="5.9649176" y1="26.048164" x2="52.854097" y2="26.048164"/>
+ <linearGradient inkscape:collect="always" id="linearGradient2797">
+ <stop style="stop-color:#ffffff;stop-opacity:1;" offset="0" id="stop2799"/>
+ <stop style="stop-color:#ffffff;stop-opacity:0;" offset="1" id="stop2801"/>
+ </linearGradient>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient2797" id="linearGradient1491" gradientUnits="userSpaceOnUse" x1="5.9649176" y1="26.048164" x2="52.854097" y2="26.048164"/>
+ <linearGradient inkscape:collect="always" id="linearGradient7179">
+ <stop style="stop-color:#ffffff;stop-opacity:1;" offset="0" id="stop7181"/>
+ <stop style="stop-color:#ffffff;stop-opacity:0;" offset="1" id="stop7183"/>
+ </linearGradient>
+ <linearGradient id="linearGradient2316">
+ <stop style="stop-color:#000000;stop-opacity:1;" offset="0" id="stop2318"/>
+ <stop style="stop-color:#ffffff;stop-opacity:0.65979379;" offset="1" id="stop2320"/>
+ </linearGradient>
+ <linearGradient id="linearGradient1322">
+ <stop id="stop1324" offset="0.0000000" style="stop-color:#729fcf"/>
+ <stop id="stop1326" offset="1.0000000" style="stop-color:#5187d6;stop-opacity:1.0000000;"/>
+ </linearGradient>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient1322" id="linearGradient4975" x1="34.892849" y1="36.422989" x2="45.918697" y2="48.547989" gradientUnits="userSpaceOnUse" gradientTransform="translate(-18.01785,-13.57119)"/>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient7179" id="linearGradient7185" x1="13.435029" y1="13.604306" x2="22.374878" y2="23.554308" gradientUnits="userSpaceOnUse"/>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient7179" id="linearGradient7189" gradientUnits="userSpaceOnUse" x1="13.435029" y1="13.604306" x2="22.374878" y2="23.554308" gradientTransform="matrix(-1.000000,0.000000,0.000000,-1.000000,47.93934,50.02474)"/>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient2380" id="linearGradient7180" gradientUnits="userSpaceOnUse" x1="62.513836" y1="36.061237" x2="15.984863" y2="20.60858"/>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient2871" id="linearGradient7182" gradientUnits="userSpaceOnUse" x1="46.834816" y1="45.264122" x2="45.380436" y2="50.939667"/>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient2402" id="linearGradient7184" gradientUnits="userSpaceOnUse" x1="18.935766" y1="23.667896" x2="53.588622" y2="26.649362"/>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient2871" id="linearGradient7186" gradientUnits="userSpaceOnUse" x1="46.834816" y1="45.264122" x2="45.380436" y2="50.939667"/>
+ <linearGradient inkscape:collect="always" xlink:href="#linearGradient7916" id="linearGradient7922" x1="16.874998" y1="22.851799" x2="27.900846" y2="34.976799" gradientUnits="userSpaceOnUse"/>
+ </defs>
+ <sodipodi:namedview id="base" pagecolor="#ffffff" bordercolor="#666666" borderopacity="0.10980392" inkscape:pageopacity="0.0" inkscape:pageshadow="2" inkscape:zoom="1" inkscape:cx="38.727739" inkscape:cy="26.974252" inkscape:current-layer="layer1" showgrid="false" inkscape:grid-bbox="true" inkscape:document-units="px" inkscape:window-width="1280" inkscape:window-height="949" inkscape:window-x="380" inkscape:window-y="79" inkscape:showpageshadow="false"/>
+ <metadata id="metadata6436">
+ <rdf:RDF>
+ <cc:Work rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type rdf:resource="http://purl.org/dc/dcmitype/StillImage"/>
+ <dc:title>Remove</dc:title>
+ <dc:date>2006-01-04</dc:date>
+ <dc:creator>
+ <cc:Agent>
+ <dc:title>Andreas Nilsson</dc:title>
+ </cc:Agent>
+ </dc:creator>
+ <dc:source>http://tango-project.org</dc:source>
+ <dc:subject>
+ <rdf:Bag>
+ <rdf:li>remove</rdf:li>
+ <rdf:li>delete</rdf:li>
+ </rdf:Bag>
+ </dc:subject>
+ <cc:license rdf:resource="http://creativecommons.org/licenses/by-sa/2.0/"/>
+ </cc:Work>
+ <cc:License rdf:about="http://creativecommons.org/licenses/by-sa/2.0/">
+ <cc:permits rdf:resource="http://web.resource.org/cc/Reproduction"/>
+ <cc:permits rdf:resource="http://web.resource.org/cc/Distribution"/>
+ <cc:requires rdf:resource="http://web.resource.org/cc/Notice"/>
+ <cc:requires rdf:resource="http://web.resource.org/cc/Attribution"/>
+ <cc:permits rdf:resource="http://web.resource.org/cc/DerivativeWorks"/>
+ <cc:requires rdf:resource="http://web.resource.org/cc/ShareAlike"/>
+ </cc:License>
+ </rdf:RDF>
+ </metadata>
+ <g id="layer1" inkscape:label="Layer 1" inkscape:groupmode="layer">
+ <path style="font-size:59.901077px;font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;text-align:start;line-height:125.00000%;writing-mode:lr-tb;text-anchor:start;fill:#75a1d0;fill-opacity:1.0000000;stroke:#3465a4;stroke-width:1.0000004px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1.0000000;font-family:Bitstream Vera Sans" d="M 27.514356,28.359472 L 39.633445,28.475543 L 39.633445,21.480219 L 27.523285,21.480219 L 20.502546,21.462362 L 8.5441705,21.489147 L 8.5084565,28.457686 L 20.511475,28.475543 L 27.514356,28.359472 z " id="text1314" sodipodi:nodetypes="ccccccccc"/>
+ <path style="font-size:59.901077px;font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;text-align:start;line-height:125.00000%;writing-mode:lr-tb;text-anchor:start;opacity:0.40860215;fill:url(#linearGradient4975);fill-opacity:1.0000000;stroke:url(#linearGradient7922);stroke-width:1.0000006px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1.0000000;font-family:Bitstream Vera Sans" d="M 38.579429,27.484113 L 38.588357,22.475309 L 9.5267863,22.493166 L 9.5000003,27.466256 L 38.579429,27.484113 z " id="path7076" sodipodi:nodetypes="ccccc"/>
+ <path style="fill:#ffffff;fill-opacity:1.0000000;fill-rule:evenodd;stroke:none;stroke-width:1.0000000px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1.0000000;opacity:0.31182796" d="M 9.0000000,25.000000 C 9.0000000,26.937500 39.125000,24.062500 39.125000,25.000000 L 39.125000,22.000000 L 9.0000000,22.000000 L 9.0000000,25.000000 z " id="path7914" sodipodi:nodetypes="ccccc"/>
+ <path sodipodi:type="arc" style="opacity:0.10439561;fill:url(#radialGradient2097);fill-opacity:1;stroke:none;stroke-width:3;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" id="path1361" sodipodi:cx="22.958872" sodipodi:cy="34.94062" sodipodi:rx="10.31934" sodipodi:ry="2.320194" d="M 33.278212 34.94062 A 10.31934 2.320194 0 1 1 12.639532,34.94062 A 10.31934 2.320194 0 1 1 33.278212 34.94062 z" transform="matrix(2.32573,0,0,1.293,-29.39613,-8.178198)" inkscape:r_cx="true" inkscape:r_cy="true"/>
+ </g>
+</svg> \ No newline at end of file
diff --git a/src/trace_viewer/README b/src/trace_viewer/README
new file mode 100644
index 00000000..547a1435
--- /dev/null
+++ b/src/trace_viewer/README
@@ -0,0 +1,11 @@
+
+To use, first make sure node.js and npm are installed (e.g. via the
+Ubuntu package manager), then run the following in this directory:
+
+> npm install
+
+> npm run tsc
+
+> ./node_modules/.bin/electron .
+
+and point the file selector at a trace produced by sail -ocaml_trace \ No newline at end of file
diff --git a/src/trace_viewer/index.css b/src/trace_viewer/index.css
new file mode 100644
index 00000000..35ebcb23
--- /dev/null
+++ b/src/trace_viewer/index.css
@@ -0,0 +1,86 @@
+
+body {
+ background-color: #202020;
+ color: #DCDCCC;
+ font-family: monospace;
+ font-size: 14pt;
+ font-weight: bold;
+}
+
+img {
+ height: 30px;
+}
+
+#control {
+ position: fixed;
+ bottom: 0px;
+ left:10%;
+ right:10%;
+ width:80%;
+}
+
+#command {
+ font-size: 16pt;
+ width: 100%;
+}
+
+.call {
+ background-color: #313131;
+ border: 1px;
+ border-left: 5px;
+ border-color: rgb(118, 173, 160);
+ border-style: solid;
+ padding-top: 2px;
+ padding-bottom: 2px;
+ margin: 0px;
+ min-height: 32px;
+ display: flex;
+ align-items: center;
+}
+
+.write {
+ background-color: #313131;
+ border: 1px;
+ border-left: 5px;
+ border-color: rgb(255, 40, 40);
+ border-style: solid;
+ padding-top: 2px;
+ padding-bottom: 2px;
+ margin: 0px;
+ min-height: 32px;
+ display: flex;
+ align-items: center;
+}
+
+.load {
+ background-color: #313131;
+ color: white;
+ border: 1px;
+ border-left: 5px;
+ border-color: #ff9100;
+ border-style: solid;
+ padding-top: 2px;
+ padding-bottom: 2px;
+ margin: 0px;
+ min-height: 32px;
+ display: flex;
+ align-items: center;
+}
+
+.read {
+ background-color: #313131;
+ border: 1px;
+ border-left: 5px;
+ border-color: rgb(107, 199, 47);
+ border-style: solid;
+ padding-top: 2px;
+ padding-bottom: 2px;
+ margin: 0px;
+ min-height: 32px;
+ display: flex;
+ align-items: center;
+}
+
+.tree {
+ padding-left: 20px;
+} \ No newline at end of file
diff --git a/src/trace_viewer/index.html b/src/trace_viewer/index.html
new file mode 100644
index 00000000..75c5e035
--- /dev/null
+++ b/src/trace_viewer/index.html
@@ -0,0 +1,19 @@
+<!DOCTYPE html>
+<html>
+ <head>
+ <meta charset="UTF-8">
+ <title>Sail Log Viewer</title>
+ <script type="text/javascript">
+ var exports = {}
+ </script>
+ <script type="text/javascript" src="index.js"></script>
+ <link rel="stylesheet" type="text/css" href="index.css">
+ </head>
+ <body>
+ <div id="container">
+ </div>
+ <div id="control">
+ <input type="text" id="command">
+ </div>
+ </body>
+</html> \ No newline at end of file
diff --git a/src/trace_viewer/index.ts b/src/trace_viewer/index.ts
new file mode 100644
index 00000000..f9b5041b
--- /dev/null
+++ b/src/trace_viewer/index.ts
@@ -0,0 +1,287 @@
+import {remote} from "electron"
+import fs = require("fs")
+const dialog = remote.dialog
+const app = remote.app
+
+let topCallDiv = document.createElement("div")
+
+const max_arg_length = 5000
+
+abstract class Event {
+ caller: Call
+
+ protected div: HTMLDivElement | null = null
+
+ public hide(): void {
+ if (this.div != null) {
+ this.div.remove()
+ this.div = null
+ }
+ }
+
+ protected abstract showText(text: HTMLParagraphElement): void
+
+ public show(): HTMLDivElement {
+ let callerDiv: HTMLDivElement = (this.caller != null) ? this.caller.show() : topCallDiv
+
+ if (this.div != null) {
+ return this.div
+ } else {
+ this.div = document.createElement("div")
+ this.div.className = "tree"
+ callerDiv.appendChild(this.div)
+ let text = document.createElement("p")
+ this.showText(text)
+ this.div.appendChild(text)
+ return this.div
+ }
+ }
+}
+
+class Load extends Event {
+ loc: string
+ val: string
+
+ constructor(loc: string, val: string) {
+ super()
+ this.loc = loc
+ this.val = val
+ }
+
+ protected showText(text: HTMLParagraphElement): void {
+ text.className = "load"
+ text.insertAdjacentText('beforeend', this.loc + " " + this.val)
+ }
+}
+
+class Read extends Event {
+ reg: string
+ value: string
+
+ constructor(reg: string, value: string) {
+ super()
+ this.reg = reg
+ this.value = value
+ }
+
+ public showText(text: HTMLParagraphElement): void {
+ text.className = "read"
+ text.insertAdjacentText('beforeend', this.reg + " " + this.value)
+ }
+}
+
+class Write extends Event {
+ reg: string
+ value: string
+
+ constructor(reg: string, value: string) {
+ super()
+ this.reg = reg
+ this.value = value
+ }
+
+ public showText(text: HTMLParagraphElement): void {
+ text.className = "write"
+ text.insertAdjacentText('beforeend', this.reg + " " + this.value)
+ }
+}
+
+class Call {
+ fn: string
+ arg: string
+ ret: string
+ callees: (Call | Event)[] = []
+ caller: Call
+
+ private div: HTMLDivElement | null = null
+
+ private toggle: boolean = false
+ private toggleImg: HTMLImageElement | null = null
+
+ constructor(fn: string, arg: string, ret: string) {
+ this.fn = fn
+ this.arg = arg
+ this.ret = ret
+ }
+
+ public expand() {
+ if (this.caller != undefined) {
+ this.caller.expand()
+ }
+ this.showChildren()
+ }
+
+ public iter(f: (call: Call) => void): void {
+ f(this)
+ this.callees.forEach((callee) => {
+ if (callee instanceof Call) { callee.iter(f) }
+ })
+
+ }
+
+ public show(): HTMLDivElement {
+ let callerDiv: HTMLDivElement = (this.caller != null) ? this.caller.show() : topCallDiv
+
+ if (this.div != null) {
+ return this.div
+ } else {
+ this.div = document.createElement("div")
+ this.div.className = "tree"
+ callerDiv.appendChild(this.div)
+ let text = document.createElement("p")
+ text.className = "call"
+ if (this.callees.length > 0) {
+ this.toggleImg = document.createElement("img")
+ this.toggleImg.src = "List-add.svg"
+ this.toggleImg.addEventListener('click', () => {
+ if (this.toggle) {
+ this.hideChildren()
+ } else {
+ this.showChildren()
+ }
+ })
+ text.appendChild(this.toggleImg)
+ }
+ this.toggle = false
+ let display_arg = this.arg
+ if (this.arg.length > max_arg_length) {
+ display_arg = this.arg.slice(0, max_arg_length)
+ }
+ let display_ret = this.ret
+ if (this.ret.length > max_arg_length) {
+ display_ret = this.ret.slice(0, max_arg_length)
+ }
+
+ text.insertAdjacentText('beforeend', this.fn + " " + display_arg + " -> " + display_ret)
+ this.div.appendChild(text)
+ return this.div
+ }
+ }
+
+ public hide(): void {
+ if (this.toggle == true) {
+ this.hideChildren()
+ }
+
+ if (this.div != null) {
+ this.div.remove()
+ this.div = null
+ }
+ if (this.toggleImg != null) {
+ this.toggleImg.remove()
+ this.toggleImg = null
+ }
+ }
+
+ public hideChildren(): void {
+ this.callees.forEach(call => {
+ call.hide()
+ })
+
+ if (this.toggleImg != null) {
+ this.toggleImg.src = "List-add.svg"
+ this.toggle = false
+ } else {
+ alert("this.toggleImg was null!")
+ }
+ }
+
+ public showChildren(): void {
+ this.callees.forEach(call => {
+ call.show()
+ });
+
+ if (this.toggleImg != null) {
+ this.toggleImg.src = "List-remove.svg"
+ this.toggle = true
+ } else {
+ alert("this.toggleImg was null!")
+ }
+ }
+
+ public appendChild(child: Call | Write | Read | Load): void {
+ child.caller = this
+
+ this.callees.push(child)
+ }
+}
+
+document.addEventListener('DOMContentLoaded', () => {
+ let rootCall = new Call("ROOT", "", "")
+ topCallDiv.id = "root"
+ document.getElementById("container")!.appendChild(topCallDiv)
+
+ let commandInput = document.getElementById("command") as HTMLInputElement
+
+ commandInput.addEventListener("keydown", (event) => {
+ if(event.keyCode == 13) {
+ let cmd = commandInput.value.split(" ")
+ commandInput.value = ""
+
+ if (cmd[0] == "function") {
+ rootCall.iter((call) => {
+ if (call.fn == cmd[1]) { call.caller.expand() }
+ })
+ }
+ }
+ })
+
+ let files = dialog.showOpenDialog(remote.getCurrentWindow(), {title: "Select log file", defaultPath: app.getAppPath()})
+
+ if (files == [] || files == undefined) {
+ dialog.showErrorBox("Error", "No file selected")
+ app.exit(1)
+ }
+
+ fs.readFile(files[0], 'utf-8', (err, data) => {
+ if (err) {
+ dialog.showErrorBox("Error", "An error occurred when reading the log: " + err.message)
+ app.exit(1)
+ }
+
+ let lines = data.split("\n")
+ // let indents = lines.map(line => line.search(/[^\s]/) / 2)
+ lines = lines.map(line => line.trim())
+
+ let stack : Call[] = [rootCall]
+
+ lines.forEach(line => {
+ if (line.match(/^Call:/)) {
+ let words = line.slice(6).split(" ")
+ let call = new Call(words[0], words.slice(1).join(" "), "")
+ if (stack.length > 0) {
+ stack[stack.length - 1].appendChild(call)
+ }
+ stack.push(call)
+ } else if (line.match(/^Return:/)) {
+ let call = stack.pop()
+ if (call == undefined) {
+ alert("Unbalanced return")
+ app.exit(1)
+ } else {
+ call.ret = line.slice(8)
+ }
+ } else if (line.match(/^Write:/)) {
+ let words = line.slice(7).split(" ")
+ let write = new Write(words[0], words.slice(1).join(" "))
+ if (stack.length > 0) {
+ stack[stack.length - 1].appendChild(write)
+ }
+ } else if (line.match(/^Read:/)) {
+ let words = line.slice(6).split(" ")
+ let read = new Read(words[0], words.slice(1).join(" "))
+ if (stack.length > 0) {
+ stack[stack.length - 1].appendChild(read)
+ }
+ } else if (line.match(/^Load:/)) {
+ let words = line.slice(6).split(" ")
+ let load = new Load(words[0], words[1])
+ if (stack.length > 0) {
+ stack[stack.length - 1].appendChild(load)
+ }
+ }
+ })
+
+ rootCall.show()
+ })
+}) \ No newline at end of file
diff --git a/src/trace_viewer/main.ts b/src/trace_viewer/main.ts
new file mode 100644
index 00000000..5cc33452
--- /dev/null
+++ b/src/trace_viewer/main.ts
@@ -0,0 +1,12 @@
+import {app, BrowserWindow} from 'electron'
+
+let win : BrowserWindow | null = null
+
+app.on('ready', () => {
+ win = new BrowserWindow({width: 1920, height: 1200})
+ win.loadURL('file://' + __dirname + '/index.html')
+ //win.webContents.openDevTools()
+ win.on('close', () => {
+ win = null
+ })
+}) \ No newline at end of file
diff --git a/src/trace_viewer/package.json b/src/trace_viewer/package.json
new file mode 100644
index 00000000..e3a88d30
--- /dev/null
+++ b/src/trace_viewer/package.json
@@ -0,0 +1,15 @@
+{
+ "name": "trace_viewer",
+ "version": "1.0.0",
+ "description": "",
+ "main": "main.js",
+ "scripts": {
+ "test": "echo \"Error: no test specified\" && exit 1",
+ "tsc": "./node_modules/typescript/bin/tsc"
+ },
+ "devDependencies": {
+ "@types/node": "^8.0.46",
+ "electron": "1.7.9",
+ "typescript": "^2.5.3"
+ }
+}
diff --git a/src/trace_viewer/tsconfig.json b/src/trace_viewer/tsconfig.json
new file mode 100644
index 00000000..e66156b3
--- /dev/null
+++ b/src/trace_viewer/tsconfig.json
@@ -0,0 +1,18 @@
+{
+ "compileOnSave": true,
+ "compilerOptions": {
+ "target": "es5",
+ "moduleResolution": "node",
+ "pretty": true,
+ "newLine": "LF",
+ "allowSyntheticDefaultImports": true,
+ "strict": true,
+ "noUnusedLocals": true,
+ "noUnusedParameters": true,
+ "sourceMap": true,
+ "strictNullChecks": true,
+ "skipLibCheck": true,
+ "allowJs": true,
+ "jsx": "preserve"
+ }
+} \ No newline at end of file
diff --git a/src/type_check.ml b/src/type_check.ml
index 816f6d04..6489195a 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -507,6 +507,7 @@ end = struct
|| Id.compare id (mk_id "real") = 0
|| Id.compare id (mk_id "list") = 0
|| Id.compare id (mk_id "string") = 0
+ || Id.compare id (mk_id "itself") = 0
(* Check if a type, order, or n-expression is well-formed. Throws a
type error if the type is badly formed. FIXME: Add arity to type
@@ -922,6 +923,21 @@ let initial_env =
Env.empty
|> Env.add_typ_synonym (mk_id "atom") (fun _ args -> mk_typ (Typ_app (mk_id "range", args @ args)))
+ (* Internal functions for Monomorphise.AtomToItself *)
+
+ |> Env.add_extern (mk_id "size_itself_int") "size_itself_int"
+ |> Env.add_val_spec (mk_id "size_itself_int")
+ (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
+ Parse_ast.Unknown)],Parse_ast.Unknown),
+ function_typ (app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))])
+ (atom_typ (nvar (mk_kid "n"))) no_effect)
+ |> Env.add_extern (mk_id "make_the_value") "make_the_value"
+ |> Env.add_val_spec (mk_id "make_the_value")
+ (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
+ Parse_ast.Unknown)],Parse_ast.Unknown),
+ function_typ (atom_typ (nvar (mk_kid "n")))
+ (app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))]) no_effect)
+
let ex_counter = ref 0
let fresh_existential ?name:(n="") () =
@@ -2644,9 +2660,9 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
annot_exp (E_loop (loop_type, checked_cond, checked_body)) unit_typ
| E_for (v, f, t, step, ord, body) ->
begin
- let f, t = match ord with
- | Ord_aux (Ord_inc, _) -> f, t
- | Ord_aux (Ord_dec, _) -> t, f (* reverse direction for downto loop *)
+ let f, t, is_dec = match ord with
+ | Ord_aux (Ord_inc, _) -> f, t, false
+ | Ord_aux (Ord_dec, _) -> t, f, true (* reverse direction to typechecking downto as upto loop *)
in
let inferred_f = irule infer_exp env f in
let inferred_t = irule infer_exp env t in
@@ -2668,7 +2684,9 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
let env = Env.add_constraint (nc_and (nc_lteq l1 (nvar kid)) (nc_lteq (nvar kid) u2)) env in
let loop_vtyp = atom_typ (nvar kid) in
let checked_body = crule check_exp (Env.add_local v (Immutable, loop_vtyp) env) body unit_typ in
- annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ
+ if not is_dec (* undo reverse direction in annoteded ast for downto loop *)
+ then annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ
+ else annot_exp (E_for (v, inferred_t, inferred_f, checked_step, ord, checked_body)) unit_typ
end
| _, _ -> typ_error l "Ranges in foreach overlap"
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 10:29:37 +0000