summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/initial_check.ml10
-rw-r--r--src/lem_interp/interp.lem448
-rw-r--r--src/lem_interp/interp_lib.lem36
-rw-r--r--src/lem_interp/run_interp.ml30
-rw-r--r--src/pretty_print.ml525
-rw-r--r--src/process_file.ml1
-rw-r--r--src/type_check.ml2
7 files changed, 646 insertions, 406 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index e7b92019..ed4a0208 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -530,17 +530,17 @@ let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt =
| Parse_ast.Rec_rec -> Rec_rec
),l)
-let to_ast_tannot_opt (k_env : kind Envmap.t) (Parse_ast.Typ_annot_opt_aux(tp,l)) : tannot tannot_opt * kind Envmap.t * kind Envmap.t=
+let to_ast_tannot_opt (k_env : kind Envmap.t) (Parse_ast.Typ_annot_opt_aux(tp,l)) : tannot_opt * kind Envmap.t * kind Envmap.t=
match tp with
| Parse_ast.Typ_annot_opt_none -> raise (Reporting_basic.err_unreachable l "Parser generated typ annot opt none")
| Parse_ast.Typ_annot_opt_some(tq,typ) ->
let typq,k_env,k_local = to_ast_typquant k_env tq in
- Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env typ),(l,None)),k_env,k_local
+ Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env typ),l),k_env,k_local
-let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) : tannot effect_opt =
+let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) : effect_opt =
match e with
- | Parse_ast.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,(l,None))
- | Parse_ast.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects k_env typ),(l,None))
+ | Parse_ast.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,l)
+ | Parse_ast.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects k_env typ),l)
let to_ast_funcl (names,k_env,t_env) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl) : (tannot funcl) =
match fcl with
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 45396a5a..c7a9da00 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -7,13 +7,15 @@ import String
open import Interp_ast
+type tannot = maybe (t * tag * list nec * effect)
+
(* Workaround Lem's inability to scrap my (type classes) boilerplate.
* Implementing only Eq, and only for literals - hopefully this will
* be enough, but we should in principle implement ordering for everything in
* Interp_ast *)
val lit_eq: lit -> lit -> bool
-let lit_eq left right =
+let lit_eq (L_aux left _) (L_aux right _) =
match (left, right) with
| (L_unit, L_unit) -> true
| (L_zero, L_zero) -> true
@@ -39,7 +41,7 @@ end
let foldr2 f x l l' = List.foldr (Tuple.uncurry f) x (List.zip l l')
let map2 f l l' = List.map (Tuple.uncurry f) (List.zip l l')
-let get_id id = match id with Id s -> s | DeIid s -> s end
+let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end
type value =
| V_boxref of nat
@@ -92,7 +94,7 @@ type action =
(* Inverted call stack, where top item on the stack is waiting for an action and all other frames for the right stack *)
type stack =
| Top
- | Frame of id * exp * env * mem * stack
+ | Frame of id * exp tannot * env * mem * stack
(* Either a case must be added for parallel options or action must be tied to a list *)
type outcome =
@@ -101,25 +103,26 @@ type outcome =
| Error of string (* When we store location information, it should be added here *)
(* interprets the exp sequentially in the presence of a set of top level definitions and returns a value or a memory request *)
-val interp : defs -> exp -> outcome
+val interp : defs tannot -> exp tannot -> outcome
-val to_registers : defs -> list (id * reg_form)
+val to_registers : defs tannot -> list (id * reg_form)
let rec to_registers (Defs defs) =
match defs with
| [ ] -> [ ]
- | def::defs ->
+ | (DEF_aux def _)::defs ->
match def with
| DEF_spec valsp ->
match valsp with
- | VS_val_spec (TypSchm_ts tq ((Typ_app (Id "reg") _) as t)) id -> (id, Reg id t):: (to_registers (Defs defs))
+ | (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts tq ((Typ_aux (Typ_app (Id_aux (Id "reg") _) _) _) as t)) _) id) _) ->
+ (id, Reg id t):: (to_registers (Defs defs))
| _ -> to_registers (Defs defs)
end
| DEF_reg_dec typ id -> (id, Reg id typ) :: (to_registers (Defs defs))
| DEF_type tdef ->
match tdef with
- | TD_register id n1 n2 ranges ->
- (id,Reg id (Typ_app (Id "vector")[]))::
- ((to_reg_ranges id (Reg id (Typ_app (Id "vector")[])) ranges) ++ (to_registers (Defs defs)))
+ | (TD_aux (TD_register id n1 n2 ranges) _) ->
+ (id,Reg id (Typ_aux (Typ_app (Id_aux (Id "vector") Unknown) []) Unknown))::
+ ((to_reg_ranges id (Reg id (Typ_aux (Typ_app (Id_aux (Id "vector") Unknown) []) Unknown)) ranges) ++ (to_registers (Defs defs)))
| _ -> to_registers (Defs defs)
end
| _ -> to_registers (Defs defs)
@@ -135,7 +138,7 @@ val has_memory_effect : list base_effect -> bool
let rec has_memory_effect efcts =
match efcts with
| [] -> false
- | e::efcts ->
+ | (BE_aux e _)::efcts ->
match e with
| BE_wreg -> true
| BE_wmem -> true
@@ -143,53 +146,66 @@ let rec has_memory_effect efcts =
end
end
+let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
+let get_effects (Typ_aux t _) =
+ match t with
+ | Typ_fn a r (Effect_aux (Effect_set eff) _) -> eff
+ | _ -> []
+ end
+
(*Look for externs as well*)
-val to_memory_ops : defs -> list (id * typ)
+val to_memory_ops : defs tannot -> list (id * typ)
let rec to_memory_ops (Defs defs) =
match defs with
| [] -> []
- | def ::defs ->
+ | (DEF_aux def _) ::defs ->
match def with
- | DEF_spec valsp ->
+ | DEF_spec (VS_aux valsp _) ->
match valsp with
- | VS_val_spec (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id ->
+ | VS_val_spec ts id ->
+ let t = get_typ ts in
+ let eff = get_effects t in
if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
- | VS_extern_spec (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id _ ->
+ | VS_extern_spec ts id _ ->
+ let t = get_typ ts in
+ let eff = get_effects t in
if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
- | VS_extern_no_rename (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id ->
+ | VS_extern_no_rename ts id ->
+ let t = get_typ ts in
+ let eff = get_effects t in
if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
| _ -> to_memory_ops (Defs defs) end
| _ -> to_memory_ops (Defs defs) end
end
-val to_externs : defs -> list (id * string)
+val to_externs : defs tannot -> list (id * string)
let rec to_externs (Defs defs) =
match defs with
| [] -> []
- | def ::defs ->
+ | (DEF_aux def _) ::defs ->
match def with
- | DEF_spec valsp ->
+ | DEF_spec (VS_aux valsp _) ->
match valsp with
- | VS_extern_spec (TypSchm_ts tq ((Typ_fn a r e) as t)) id s ->
+ | VS_extern_spec (TypSchm_aux (TypSchm_ts tq (Typ_aux (Typ_fn a r e) _)) _) id s ->
(id,s)::(to_externs (Defs defs))
| _ -> to_externs (Defs defs) end
| _ -> to_externs (Defs defs) end
end
-val to_data_constructors : defs -> list (id * typ)
+val to_data_constructors : defs tannot -> list (id * typ)
let rec to_data_constructors (Defs defs) =
match defs with
| [] -> []
- | def :: defs ->
+ | (DEF_aux def _) :: defs ->
match def with
- | DEF_type t ->
+ | DEF_type (TD_aux t _)->
match t with
| TD_variant id _ tq tid_list _ ->
(List.map
- (fun t ->
+ (fun (Tu_aux t _) ->
match t with
| (Tu_ty_id x y) -> (y,x)
- | Tu_id x -> (id,Typ_app (Id "unit") []) end) tid_list)++(to_data_constructors (Defs defs))
+ | Tu_id x -> (id,Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown) end) tid_list)++(to_data_constructors (Defs defs))
| _ -> to_data_constructors (Defs defs) end
| _ -> to_data_constructors (Defs defs) end
end
@@ -198,7 +214,7 @@ val in_env : env -> id -> maybe value
let rec in_env env id =
match env with
| [] -> Nothing
- | (eid,value)::env -> if eid = id then Just value else in_env env id
+ | (eid,value)::env -> if (get_id eid) = (get_id id) then Just value else in_env env id
end
val in_mem : mem -> nat -> value
@@ -213,7 +229,7 @@ let update_mem (Mem c m) loc value =
Mem c m'
val is_lit_vector : lit -> bool
-let is_lit_vector l =
+let is_lit_vector (L_aux l _) =
match l with
| L_bin _ -> true
| L_hex _ -> true
@@ -221,8 +237,8 @@ let is_lit_vector l =
end
val litV_to_vec : lit -> value
-let litV_to_vec l =
- match l with
+let litV_to_vec (L_aux lit l) =
+ match lit with
| L_hex s ->
let hexes = String.toCharList s in
(* XXX unimplemented *)
@@ -230,7 +246,7 @@ let litV_to_vec l =
| L_bin s ->
let bits = String.toCharList s in
let exploded_bits = List.map (fun c -> String.toString [c]) bits in
- let bits = List.map (fun s -> match s with | "0" -> (V_lit L_zero) | "1" -> (V_lit L_one) end) exploded_bits in
+ let bits = List.map (fun s -> match s with | "0" -> (V_lit (L_aux L_zero l)) | "1" -> (V_lit (L_aux L_one l)) end) exploded_bits in
(* XXX assume binary constants are written in big-endian, convert them to
* little-endian by default - we might need syntax to change both of those
* assumptions. *)
@@ -332,13 +348,13 @@ val in_reg : list (id * reg_form) -> id -> maybe reg_form
let rec in_reg regs id =
match regs with
| [] -> Nothing
- | (eid,regf)::regs -> if eid = id then Just regf else in_reg regs id
+ | (eid,regf)::regs -> if (get_id eid) = (get_id id) then Just regf else in_reg regs id
end
val in_ctors : list (id * typ) -> id -> maybe typ
let rec in_ctors ctors id =
match ctors with
| [] -> Nothing
- | (cid,typ)::ctors -> if cid = id then Just typ else in_ctors ctors id
+ | (cid,typ)::ctors -> if (get_id cid) = (get_id id) then Just typ else in_ctors ctors id
end
let add_to_top_frame e_builder stack =
@@ -347,32 +363,37 @@ let add_to_top_frame e_builder stack =
end
let rec to_exp v =
- match v with
- | V_boxref n -> E_id (Id ("XXX string_of_num n"))
- | V_lit lit -> E_lit lit
- | V_tuple(vals) -> E_tuple (List.map to_exp vals)
- | V_vector n inc vals ->
- if (inc && n=0)
- then E_vector (List.map to_exp vals)
- else if inc then
- E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals)))
- else
- E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals))
- | V_record(ivals) -> E_record(FES_Fexps (List.map (fun (id,value) -> (FE_Fexp id (to_exp value))) ivals) false)
- | V_list(vals) -> E_list (List.map to_exp vals)
- | V_ctor id vals -> E_app id [to_exp vals]
- end
-
-val find_type_def : defs -> id -> maybe type_def
-val find_function : defs -> id -> maybe (list funcl)
-
-let get_funcls id (FD_function _ _ _ fcls) =
- List.filter (fun (FCL_Funcl name pat exp) -> id = name) fcls
+ E_aux
+ (match v with
+ | V_boxref n -> E_id (Id_aux (Id ("XXX string_of_num n")) Unknown)
+ | V_lit lit -> E_lit lit
+ | V_tuple(vals) -> E_tuple (List.map to_exp vals)
+ | V_vector n inc vals ->
+ if (inc && n=0)
+ then E_vector (List.map to_exp vals)
+ else if inc then
+ E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals)))
+ else
+ E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals))
+ | V_record(ivals) ->
+ E_record(FES_aux (FES_Fexps
+ (List.map (fun (id,value) -> (FE_aux (FE_Fexp id (to_exp value)) (Unknown,Nothing))) ivals) false)
+ (Unknown,Nothing))
+ | V_list(vals) -> E_list (List.map to_exp vals)
+ | V_ctor id vals -> E_app id [to_exp vals]
+ end)
+ (Unknown,Nothing)
+
+val find_type_def : defs tannot -> id -> maybe (type_def tannot)
+val find_function : defs tannot -> id -> maybe (list (funcl tannot))
+
+let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) =
+ List.filter (fun (FCL_aux (FCL_Funcl name pat exp) _) -> (get_id id) = (get_id name)) fcls
let rec find_function (Defs defs) id =
match defs with
| [] -> Nothing
- | def::defs ->
+ | (DEF_aux def _)::defs ->
match def with
| DEF_fundef f -> match get_funcls id f with
| [] -> find_function (Defs defs) id
@@ -386,8 +407,8 @@ let find_memory mems id = List.lookup id mems
val find_extern : list ( id * string ) -> id -> maybe string
let find_extern externs id = List.lookup id externs
-val match_pattern : pat -> value -> bool * list (id * value)
-let rec match_pattern p value =
+val match_pattern : pat tannot -> value -> bool * list (id * value)
+let rec match_pattern (P_aux p _) value =
match p with
| P_lit(lit) ->
if is_lit_vector lit then
@@ -431,7 +452,7 @@ let rec match_pattern p value =
match value with
| V_record fvals ->
List.foldr
- (fun (FP_Fpat id pat) (matched_p,bounds) ->
+ (fun (FP_aux (FP_Fpat id pat) _) (matched_p,bounds) ->
if matched_p then
let (matched_p,new_bounds) = match in_env fvals id with
| Nothing -> (false,[])
@@ -471,7 +492,7 @@ let rec match_pattern p value =
| V_vector n inc vals ->
let (matched_p,bounds,remaining_vals) =
List.foldl
- (fun (matched_p,bounds,r_vals) pat ->
+ (fun (matched_p,bounds,r_vals) (P_aux pat _) ->
match pat with
| P_vector pats -> vec_concat_match pats r_vals
| P_id id -> (false,[],[]) (*Need to have at least a guess of how many to consume*)
@@ -518,31 +539,31 @@ and vec_concat_match pats r_vals =
end
-val find_funcl : list funcl -> value -> maybe (env * exp)
+val find_funcl : list (funcl tannot) -> value -> maybe (env * (exp tannot))
let rec find_funcl funcls value =
match funcls with
| [] -> Nothing
- | (FCL_Funcl id pat exp)::funcls ->
+ | (FCL_aux (FCL_Funcl id pat exp) _)::funcls ->
let (is_matching,env) = match_pattern pat value in
if is_matching then Just (env,exp) else find_funcl funcls value
end
-val find_case : list pexp -> value -> maybe (env * exp)
+val find_case : list (pexp tannot) -> value -> maybe (env * (exp tannot))
let rec find_case pexps value =
match pexps with
| [] -> Nothing
- | (Pat_exp p e)::pexps ->
+ | (Pat_aux (Pat_exp p e) _)::pexps ->
let (is_matching,env) = match_pattern p value in
if is_matching then Just(env,e) else find_case pexps value
end
(*top_level is a tuple of
(all definitions, external functions, letbound values, declared registers, memory functions (typ expected to be num -> num -> a), and Typedef union constructors) *)
-type top_level = Env of defs * list (id * string) * env * list (id*reg_form) * list (id * typ) * list (id * typ)
+type top_level = Env of (defs tannot) * list (id * string) * env * list (id*reg_form) * list (id * typ) * list (id * typ)
-val interp_main : top_level -> env -> mem -> exp -> (outcome * mem * env)
-val exp_list : top_level -> (list exp -> exp) -> (list value -> value) -> env -> mem -> list value -> list exp -> (outcome * mem * env)
-val interp_lbind : top_level -> env -> mem -> letbind -> ((outcome * mem * env) * (maybe (exp -> letbind)))
+val interp_main : top_level -> env -> mem -> (exp tannot) -> (outcome * mem * env)
+val exp_list : top_level -> (list (exp tannot) -> (exp tannot)) -> (list value -> value) -> env -> mem -> list value -> list (exp tannot) -> (outcome * mem * env)
+val interp_lbind : top_level -> env -> mem -> (letbind tannot) -> ((outcome * mem * env) * (maybe ((exp tannot) -> (letbind tannot))))
let resolve_outcome to_match value_thunk action_thunk =
match to_match with
@@ -563,7 +584,7 @@ let rec exp_list t_level build_e build_v l_env l_mem vals exps =
(fun a -> update_stack a (add_to_top_frame (fun e -> (build_e ((List.map to_exp vals)++(e::exps))))))
end
-and interp_main t_level l_env l_mem exp =
+and interp_main t_level l_env l_mem (E_aux exp annot) =
match exp with
| E_lit lit -> if is_lit_vector lit then (Value (litV_to_vec lit),l_mem,l_env) else (Value (V_lit lit), l_mem,l_env)
| E_cast typ exp -> interp_main t_level l_env l_mem exp (* Potentially introduce coercions ie vectors and numbers *)
@@ -578,7 +599,9 @@ and interp_main t_level l_env l_mem exp =
| Nothing ->
match in_reg regs id with
| Just(regf) ->
- (Action (Read_reg regf Nothing) (Frame (Id "0") (E_id (Id "0")) l_env l_mem Top), l_mem, l_env)
+ (Action (Read_reg regf Nothing)
+ (Frame (Id_aux (Id "0") Unknown)
+ (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) l_env l_mem Top), l_mem, l_env)
| Nothing ->
let name = get_id id in
(Error (String.stringAppend "unbound identifier " name ),l_mem,l_env)
@@ -590,61 +613,93 @@ and interp_main t_level l_env l_mem exp =
resolve_outcome (interp_main t_level l_env l_mem cond)
(fun value lm le ->
match value with
- | V_lit(L_true) -> interp_main t_level l_env lm thn
- | V_lit(L_false) -> interp_main t_level l_env lm els
+ | V_lit(L_aux L_true _) -> interp_main t_level l_env lm thn
+ | V_lit(L_aux L_false _) -> interp_main t_level l_env lm els
| _ -> (Error "Type error, not provided boolean for if",lm,l_env) end)
- (fun a -> update_stack a (add_to_top_frame (fun c -> (E_if c thn els))))
+ (fun a -> update_stack a (add_to_top_frame (fun c -> (E_aux (E_if c thn els) annot))))
| E_for id from to_ by order exp ->
resolve_outcome (interp_main t_level l_env l_mem from)
(fun from_val lm le ->
match from_val with
- | V_lit(L_num from_num) ->
+ | V_lit(L_aux(L_num from_num) _) ->
resolve_outcome (interp_main t_level le lm to_)
(fun to_val lm le ->
match to_val with
- | V_lit(L_num to_num) ->
+ | V_lit(L_aux (L_num to_num) _) ->
resolve_outcome
(interp_main t_level le lm by)
(fun by_val lm le ->
match by_val with
- | V_lit (L_num by_num) ->
+ | V_lit (L_aux (L_num by_num) _) ->
if (from_num = to_num)
- then (Value(V_lit L_unit),lm,le)
+ then (Value(V_lit (L_aux L_unit Unknown)),lm,le)
else interp_main t_level le lm
- (E_block [(E_let (LB_val_implicit (P_id id) (E_lit (L_num from_num))) exp);
- (E_for id (E_lit (L_num (from_num + by_num))) (E_lit (L_num to_num)) (E_lit (L_num by_num)) order exp)])
+ (E_aux
+ (E_block
+ [(E_aux (E_let
+ (LB_aux (LB_val_implicit
+ (P_aux (P_id id) (Unknown,Nothing))
+ (E_aux (E_lit(L_aux(L_num from_num) Unknown)) (Unknown,Nothing)))
+ (Unknown,Nothing))
+ exp) (Unknown,Nothing));
+ (E_aux (E_for id
+ (E_aux (E_lit (L_aux (L_num (from_num + by_num)) Unknown))
+ (Unknown,Nothing))
+ (E_aux (E_lit (L_aux (L_num to_num) Unknown)) (Unknown,Nothing))
+ (E_aux (E_lit (L_aux (L_num by_num) Unknown)) (Unknown,Nothing))
+ order exp) annot)])
+ annot)
| _ -> (Error "by must be a number",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun b -> (E_for id (E_lit (L_num from_num)) (E_lit (L_num to_num)) b order exp))))
+ (fun a -> update_stack a
+ (add_to_top_frame (fun b ->
+ (E_aux (E_for id
+ (E_aux (E_lit (L_aux (L_num from_num) Unknown)) (Unknown,Nothing))
+ (E_aux (E_lit (L_aux (L_num to_num) Unknown)) (Unknown,Nothing))
+ b order exp) annot))))
| _ -> (Error "to must be a number",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun t -> (E_for id (E_lit (L_num from_num)) t by order exp))))
+ (fun a -> update_stack a
+ (add_to_top_frame (fun t ->
+ (E_aux (E_for id (E_aux (E_lit (L_aux (L_num from_num) Unknown)) (Unknown,Nothing))
+ t by order exp) annot))))
| _ -> (Error "from must be a number",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun f -> (E_for id f to_ by order exp))))
+ (fun a -> update_stack a (add_to_top_frame (fun f -> (E_aux (E_for id f to_ by order exp) annot))))
| E_case exp pats ->
resolve_outcome (interp_main t_level l_env l_mem exp)
(fun v lm le ->
match find_case pats v with
| Nothing -> (Error "No matching patterns in case",lm,le)
| Just (env,exp) -> interp_main t_level (env++l_env) lm exp end)
- (fun a -> update_stack a (add_to_top_frame (fun e -> E_case e pats)))
- | E_record(FES_Fexps fexps _) ->
- let (fields,exps) = List.unzip (List.map (fun (FE_Fexp id exp) -> (id,exp)) fexps) in
- exp_list t_level (fun es -> (E_record(FES_Fexps (map2 (fun id exp -> FE_Fexp id exp) fields es) false)))
- (fun vs -> (V_record (List.zip fields vs))) l_env l_mem [] exps
- | E_record_update exp (FES_Fexps fexps _) ->
+ (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_case e pats) annot))))
+ | E_record(FES_aux (FES_Fexps fexps _) fes_annot) ->
+ let (fields,exps) = List.unzip (List.map (fun (FE_aux (FE_Fexp id exp) _) -> (id,exp)) fexps) in
+ exp_list t_level
+ (fun es ->
+ (E_aux (E_record
+ (FES_aux (FES_Fexps (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing))) fields es) false) fes_annot))
+ annot))
+ (fun vs -> (V_record (List.zip fields vs))) l_env l_mem [] exps
+ | E_record_update exp (FES_aux (FES_Fexps fexps _) fes_annot) ->
resolve_outcome (interp_main t_level l_env l_mem exp)
(fun rv lm le ->
match rv with
| V_record fvs ->
- let (fields,exps) = List.unzip (List.map (fun (FE_Fexp id exp) -> (id,exp)) fexps) in
- resolve_outcome (exp_list t_level (fun es -> (E_record_update (to_exp rv) (FES_Fexps (map2 (fun id exp -> FE_Fexp id exp) fields es) false)))
- (fun vs -> (V_record (List.zip fields vs))) l_env l_mem [] exps)
+ let (fields,exps) = List.unzip (List.map (fun (FE_aux (FE_Fexp id exp) _) -> (id,exp)) fexps) in
+ resolve_outcome (exp_list t_level
+ (fun es ->
+ (E_aux (E_record_update (to_exp rv)
+ (FES_aux (FES_Fexps
+ (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing)))
+ fields es) false) fes_annot))
+ annot))
+ (fun vs -> (V_record (List.zip fields vs))) l_env l_mem [] exps)
(fun vs lm le ->
(Value (fupdate_record rv vs), lm, le))
(fun a -> a)
| _ -> (Error "record upate requires record",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun e -> E_record_update e (FES_Fexps fexps false))))
+ (fun a -> update_stack a (add_to_top_frame
+ (fun e -> E_aux(E_record_update e (FES_aux(FES_Fexps fexps false) fes_annot)) annot)))
| E_list(exps) ->
- exp_list t_level E_list V_list l_env l_mem [] exps
+ exp_list t_level (fun exps -> E_aux (E_list exps) annot) V_list l_env l_mem [] exps
| E_cons hd tl ->
resolve_outcome (interp_main t_level l_env l_mem hd)
(fun hdv lm le -> resolve_outcome
@@ -652,8 +707,8 @@ and interp_main t_level l_env l_mem exp =
(fun tlv lm le -> match tlv with
| V_list t -> (Value(V_list (hdv::t)),lm,le)
| _ -> (Error ":: of non-list value",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun t -> E_cons (to_exp hdv) t))))
- (fun a -> update_stack a (add_to_top_frame (fun h -> E_cons h tl)))
+ (fun a -> update_stack a (add_to_top_frame (fun t ->E_aux (E_cons (to_exp hdv) t) annot))))
+ (fun a -> update_stack a (add_to_top_frame (fun h -> E_aux (E_cons h tl) annot)))
| E_field exp id ->
resolve_outcome (interp_main t_level l_env l_mem exp)
(fun value lm le ->
@@ -663,45 +718,54 @@ and interp_main t_level l_env l_mem exp =
| Nothing -> (Error "Field not found in record",lm,le) end
| _ -> (Error "Field access requires a record",lm,le)
end )
- (fun a -> update_stack a (add_to_top_frame (fun e -> E_field e id)))
+ (fun a -> update_stack a (add_to_top_frame (fun e -> E_aux(E_field e id) annot)))
| E_vector_access vec i ->
resolve_outcome (interp_main t_level l_env l_mem i)
(fun iv lm le ->
match iv with
- | V_lit (L_num n) ->
+ | V_lit (L_aux (L_num n) ln) ->
resolve_outcome (interp_main t_level l_env lm vec)
(fun vvec lm le ->
match vvec with
| V_vector base inc vals -> (Value (access_vector vvec n),lm,le)
| _ -> (Error "Vector access of non-vector",lm,le)end)
- (fun a -> update_stack a (add_to_top_frame (fun v -> (E_vector_access v (E_lit (L_num n))))))
+ (fun a -> update_stack a
+ (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) annot))))
| _ -> (Error "Vector access not given a number for index",lm,l_env) end)
- (fun a -> update_stack a (add_to_top_frame (fun i -> E_vector_access vec i)))
+ (fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_access vec i) annot)))
| E_vector_subrange vec i1 i2 ->
resolve_outcome (interp_main t_level l_env l_mem i1)
(fun i1v lm le ->
match i1v with
- | V_lit (L_num n1) ->
+ | V_lit (L_aux (L_num n1) ln1) ->
resolve_outcome (interp_main t_level l_env lm i2)
(fun i2v lm le ->
match i2v with
- | V_lit (L_num n2) ->
+ | V_lit (L_aux (L_num n2) ln2) ->
resolve_outcome (interp_main t_level l_env lm vec)
(fun vvec lm le ->
match vvec with
| V_vector base inc vals -> (Value (slice_vector vvec n1 n2),lm,le)
| _ -> (Error "Vector slice of non-vector",lm,le)end)
(fun a -> update_stack a
- (add_to_top_frame (fun v -> (E_vector_subrange v (E_lit (L_num n1)) (E_lit (L_num n2))))))
+ (add_to_top_frame
+ (fun v -> (E_aux (E_vector_subrange v
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)))
+ annot))))
| _ -> (Error "vector slice given non number for last index",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun i2 -> (E_vector_subrange vec (E_lit (L_num n1)) i2))))
+ (fun a -> update_stack a
+ (add_to_top_frame
+ (fun i2 -> (E_aux (E_vector_subrange vec
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ i2) annot))))
| _ -> (Error "Vector slice given non-number for first index",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun i1 -> (E_vector_subrange vec i1 i2))))
+ (fun a -> update_stack a (add_to_top_frame (fun i1 -> (E_aux (E_vector_subrange vec i1 i2) annot))))
| E_vector_update vec i exp ->
resolve_outcome (interp_main t_level l_env l_mem i)
(fun vi lm le ->
match vi with
- | V_lit (L_num n1) ->
+ | V_lit (L_aux (L_num n1) ln1) ->
resolve_outcome (interp_main t_level le lm exp)
(fun vup lm le ->
resolve_outcome (interp_main t_level le lm vec)
@@ -709,20 +773,27 @@ and interp_main t_level l_env l_mem exp =
match vec with
| V_vector base inc vals -> (Value (fupdate_vec vec n1 vup), lm,le)
| _ -> (Error "Update of vector given non-vector",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun v -> E_vector_update v (E_lit (L_num n1)) (to_exp vup)))))
- (fun a -> update_stack a (add_to_top_frame (fun e -> E_vector_update vec (E_lit (L_num n1)) e)))
+ (fun a -> update_stack a
+ (add_to_top_frame
+ (fun v -> E_aux (E_vector_update v
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ (to_exp vup)) annot))))
+ (fun a -> update_stack a
+ (add_to_top_frame (fun e -> E_aux (E_vector_update vec
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ e) annot)))
| _ -> (Error "Update of vector requires number for access",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun i -> E_vector_update vec i exp)))
+ (fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_update vec i exp) annot)))
| E_vector_update_subrange vec i1 i2 exp ->
resolve_outcome (interp_main t_level l_env l_mem i1)
(fun vi1 lm le ->
match vi1 with
- | V_lit (L_num n1) ->
+ | V_lit (L_aux (L_num n1) ln1) ->
resolve_outcome
(interp_main t_level l_env lm i2)
(fun vi2 lm le ->
match vi2 with
- | V_lit (L_num n2) ->
+ | V_lit (L_aux (L_num n2) ln2) ->
resolve_outcome (interp_main t_level l_env lm exp)
(fun v_rep lm le ->
(resolve_outcome
@@ -732,24 +803,32 @@ and interp_main t_level l_env l_mem exp =
| V_vector m inc vals -> (Value (fupdate_vector_slice vvec v_rep n1 n2),lm,le)
| _ -> (Error "Vector update requires vector",lm,le) end)
(fun a -> update_stack a
- (add_to_top_frame (fun v -> E_vector_update_subrange v (E_lit (L_num n1)) (E_lit (L_num n2)) (to_exp v_rep))))))
+ (add_to_top_frame
+ (fun v -> E_aux (E_vector_update_subrange v
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing))
+ (to_exp v_rep)) annot)))))
(fun a -> update_stack a
- (add_to_top_frame (fun e -> E_vector_update_subrange vec (to_exp vi1) (to_exp vi2) e)))
+ (add_to_top_frame
+ (fun e -> E_aux (E_vector_update_subrange vec (to_exp vi1) (to_exp vi2) e) annot)))
| _ -> (Error "vector update requires number",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun i2 -> E_vector_update_subrange vec (to_exp vi1) i2 exp)))
+ (fun a ->
+ update_stack a (add_to_top_frame (fun i2 -> E_aux (E_vector_update_subrange vec (to_exp vi1) i2 exp) annot)))
| _ -> (Error "vector update requires number",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun i1 -> E_vector_update_subrange vec i1 i2 exp)))
+ (fun a -> update_stack a (add_to_top_frame (fun i1 -> E_aux (E_vector_update_subrange vec i1 i2 exp) annot)))
| E_tuple(exps) ->
- exp_list t_level E_tuple V_tuple l_env l_mem [] exps
+ exp_list t_level (fun exps -> E_aux (E_tuple exps) annot) V_tuple l_env l_mem [] exps
| E_vector(exps) ->
- exp_list t_level E_vector (fun vals -> V_vector 0 true vals) l_env l_mem [] exps
+ exp_list t_level (fun exps -> E_aux (E_vector exps) annot) (fun vals -> V_vector 0 true vals) l_env l_mem [] exps
| E_vector_indexed(iexps) ->
let (indexes,exps) = List.unzip iexps in
- exp_list t_level (fun es -> (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)))
+ exp_list t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)) annot))
(fun vals -> V_vector (List_extra.head indexes) true vals) (*Need to see increasing or not, can look at types later*) l_env l_mem [] exps
| E_block(exps) -> interp_block t_level l_env l_env l_mem exps
| E_app f args ->
- (match (exp_list t_level (fun es -> E_app f es) (fun vs -> match vs with | [] -> V_lit L_unit | [v] -> v | vs -> V_tuple vs end) l_env l_mem [] args) with
+ (match (exp_list t_level (fun es -> E_aux (E_app f es) annot)
+ (fun vs -> match vs with | [] -> V_lit (L_aux L_unit Unknown) | [v] -> v | vs -> V_tuple vs end)
+ l_env l_mem [] args) with
| (Value v,lm,le) ->
(match (f,t_level) with
| (id,(Env defs externs lets regs mems ctors)) ->
@@ -762,7 +841,9 @@ and interp_main t_level l_env l_mem exp =
| Just(env,exp) ->
resolve_outcome (interp_main t_level env l_mem exp)
(fun ret lm le -> (Value ret, lm,l_env))
- (fun a -> update_stack a (fun stack -> (Frame (Id "0") (E_id (Id "0")) l_env l_mem stack)))
+ (fun a -> update_stack a
+ (fun stack -> (Frame (Id_aux (Id "0") Unknown)
+ (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) l_env l_mem stack)))
end)
| Nothing ->
(match in_ctors ctors id with
@@ -770,18 +851,20 @@ and interp_main t_level l_env l_mem exp =
| Nothing ->
(match find_memory mems id with
| Just(typ) ->
- (Action (Read_mem id v Nothing) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le)
+ (Action (Read_mem id v Nothing)
+ (Frame (Id_aux (Id "0") Unknown) (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) le lm Top), lm, le)
| Nothing ->
(match find_extern externs id with
| Just(str) ->
- (Action (Call_extern str v) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le)
+ (Action (Call_extern str v)
+ (Frame (Id_aux (Id "0") Unknown) (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) le lm Top), lm, le)
| Nothing -> (Error (String.stringAppend "Unknown function call " (get_id id)),lm,le) end)
end) end) end) end)
| out -> out end)
| E_app_infix l op r ->
let op = match op with
- | Id x -> DeIid x
- | DeIid _ -> op
+ | Id_aux (Id x) il -> Id_aux (DeIid x) il
+ | _ -> op
end in
resolve_outcome (interp_main t_level l_env l_mem l)
(fun lv lm le ->
@@ -793,27 +876,30 @@ and interp_main t_level l_env l_mem exp =
| Nothing ->
(match find_extern externs op with
| Just(str) ->
- (Action (Call_extern str (V_tuple [lv;rv])) (Frame (Id "0") (E_id (Id "0")) le lm Top),lm,le)
+ (Action (Call_extern str (V_tuple [lv;rv]))
+ (Frame (Id_aux (Id "0") Unknown)
+ (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) le lm Top),lm,le)
| Nothing ->
- (Error (String.stringAppend
- "No matching function "
- (get_id op)),lm,l_env) end)
+ (Error (String.stringAppend "No matching function " (get_id op)),lm,l_env) end)
| Just (funcls) ->
(match find_funcl funcls (V_tuple [lv;rv]) with
| Nothing -> (Error "No matching pattern for function",lm,l_env)
| Just(env,exp) ->
resolve_outcome (interp_main t_level env emem exp)
(fun ret lm le -> (Value ret,l_mem,l_env))
- (fun a -> update_stack a (fun stack -> (Frame (Id "0") (E_id (Id "0")) l_env l_mem stack)))
+ (fun a -> update_stack a
+ (fun stack -> (Frame (Id_aux (Id "0") Unknown)
+ (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) l_env l_mem stack)))
end)
end)
end))
- (fun a -> update_stack a (add_to_top_frame (fun r -> (E_app_infix (to_exp lv) op r)))))
- (fun a -> update_stack a (add_to_top_frame (fun l -> (E_app_infix l op r))))
- | E_let lbind exp ->
+ (fun a -> update_stack a (add_to_top_frame (fun r ->E_aux (E_app_infix (to_exp lv) op r) annot))))
+ (fun a -> update_stack a (add_to_top_frame (fun l -> (E_aux (E_app_infix l op r) annot))))
+ | E_let (lbind : letbind tannot) exp ->
match (interp_letbind t_level l_env l_mem lbind) with
| ((Value v,lm,le),_) -> interp_main t_level le lm exp
- | (((Action a s as o),lm,le),Just lbuild) -> ((update_stack o (add_to_top_frame (fun e -> (E_let (lbuild e) exp)))),lm,le)
+ | (((Action a s as o),lm,le),Just lbuild) ->
+ ((update_stack o (add_to_top_frame (fun e -> (E_aux (E_let (lbuild e) exp) annot)))),lm,le)
| (e,_) -> e end
| E_assign lexp exp ->
resolve_outcome (interp_main t_level l_env l_mem exp)
@@ -829,65 +915,77 @@ and interp_main t_level l_env l_mem exp =
(Action (Write_reg regf range value) stack)
| (Action (Write_mem id a range value) stack) ->
(Action (Write_mem id a range value) stack)
- | _ -> update_stack a (add_to_top_frame (fun e -> (E_assign (lexp_builder e) (to_exp v)))) end))
+ | _ -> update_stack a (add_to_top_frame
+ (fun e -> (E_aux (E_assign (lexp_builder e) (to_exp v)) annot) )) end))
end))
- (fun a -> update_stack a (add_to_top_frame (fun v -> (E_assign lexp v))))
+ (fun a -> update_stack a (add_to_top_frame (fun v -> (E_aux (E_assign lexp v) annot))))
end
and interp_block t_level init_env local_env local_mem exps =
match exps with
- | [ ] -> (Value (V_lit (L_unit)), local_mem, init_env)
+ | [ ] -> (Value (V_lit (L_aux (L_unit) Unknown)), local_mem, init_env)
| [ exp ] -> interp_main t_level local_env local_mem exp
| exp:: exps ->
resolve_outcome (interp_main t_level local_env local_mem exp)
(fun _ lm le -> interp_block t_level init_env le lm exps)
- (fun a -> update_stack a (add_to_top_frame (fun e -> E_block(e::exps))))
+ (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_block(e::exps)) (Unknown,Nothing)))))
end
-and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
+and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP_aux lexp annot):lexp tannot) =
let (Env defs externs lets regs mems ctors) = t_level in
match lexp with
| LEXP_id id ->
match in_env l_env id with
| Just (V_boxref n) ->
if is_top_level
- then ((Value (V_lit L_unit), update_mem l_mem n value, l_env),Nothing)
- else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_id id))
- | Just v -> if is_top_level then ((Error "Writes must be to reg values",l_mem,l_env),Nothing) else ((Value v,l_mem,l_env),Just (fun e -> LEXP_id id))
+ then ((Value (V_lit (L_aux L_unit Unknown)), update_mem l_mem n value, l_env),Nothing)
+ else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_id id) annot))
+ | Just v ->
+ if is_top_level then ((Error "Writes must be to reg values",l_mem,l_env),Nothing)
+ else ((Value v,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_id id) annot))
| Nothing ->
match in_reg regs id with
- | Just regf -> let request = (Action (Write_reg regf Nothing value) (Frame (Id "0") (E_id (Id "0")) l_env l_mem Top),l_mem,l_env) in
- if is_top_level then (request,Nothing) else (request,Just (fun e -> LEXP_id id))
+ | Just regf ->
+ let request = (Action (Write_reg regf Nothing value)
+ (Frame (Id_aux (Id "0") Unknown)
+ (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) l_env l_mem Top),l_mem,l_env) in
+ if is_top_level then (request,Nothing) else (request,Just (fun e -> LEXP_aux (LEXP_id id) annot))
| Nothing ->
if is_top_level
then begin
let (Mem c m) = l_mem in
let l_mem = (Mem (c+1) m) in
- ((Value (V_lit L_unit), update_mem l_mem c value, (id,(V_boxref c))::l_env),Nothing)
+ ((Value (V_lit (L_aux L_unit Unknown)), update_mem l_mem c value, (id,(V_boxref c))::l_env),Nothing)
end
else ((Error "Undefined id",l_mem,l_env),Nothing)
end
end
| LEXP_memory id exps ->
- match (exp_list t_level E_tuple (fun vs -> match vs with | [] -> V_lit L_unit | [v] -> v | vs -> V_tuple vs end) l_env l_mem [] exps) with
+ match (exp_list t_level (fun exps -> E_aux (E_tuple exps) (Unknown,Nothing))
+ (fun vs -> match vs with | [] -> V_lit (L_aux L_unit Unknown) | [v] -> v | vs -> V_tuple vs end)
+ l_env l_mem [] exps) with
| (Value v,lm,le) ->
- let request = (Action (Write_mem id v Nothing value) (Frame (Id "0") (E_id (Id "0")) l_env lm Top),lm,l_env) in
- if is_top_level then (request,Nothing) else (request,Just (fun e -> (LEXP_memory id (match v with | V_tuple vs -> (List.map to_exp vs) | v -> [to_exp v]end))))
- | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_tuple es) -> (LEXP_memory id es)))
+ let request = (Action (Write_mem id v Nothing value)
+ (Frame (Id_aux (Id "0") Unknown) (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) l_env lm Top),lm,l_env) in
+ if is_top_level then (request,Nothing)
+ else (request,Just (fun e ->
+ (LEXP_aux (LEXP_memory id (match v with | V_tuple vs -> (List.map to_exp vs) | v -> [to_exp v]end)) annot)))
+ | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) -> (LEXP_aux (LEXP_memory id es) annot)))
| e -> (e,Nothing) end
| LEXP_vector lexp exp ->
match (interp_main t_level l_env l_mem exp) with
| (Value i,lm,le) ->
(match i with
- | V_lit (L_num n) ->
- let next_builder le_builder = (fun e -> LEXP_vector (le_builder e) (E_lit (L_num n))) in
+ | V_lit (L_aux (L_num n) ln) ->
+ let next_builder le_builder = (fun e ->
+ LEXP_aux (LEXP_vector (le_builder e) (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) annot) in
(match (create_write_message_or_update t_level value l_env lm false lexp) with
| ((Value v,lm,le),maybe_builder) ->
(match v with
| V_vector inc m vs ->
let nth = access_vector v n in
(match (nth,is_top_level,maybe_builder) with
- | (V_boxref n,true,_) -> ((Value (V_lit L_unit), update_mem lm n value, l_env),Nothing)
+ | (V_boxref n,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
| (v,true,_) -> ((Error "Vector does not contain reg values",lm,l_env),Nothing)
| ((V_boxref n),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
| (v,false, Just lexp_builder) -> ((Value v,lm,le), Just (next_builder lexp_builder)) end)
@@ -895,29 +993,34 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
| ((Action a s,lm,le),Just lexp_builder) ->
(match (a,is_top_level) with
| ((Write_reg regf Nothing value),true) -> ((Action (Write_reg regf (Just (n,n)) value) s, lm,le), Nothing)
- | ((Write_reg regf Nothing value),false) -> ((Action (Write_reg regf (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
+ | ((Write_reg regf Nothing value),false) ->
+ ((Action (Write_reg regf (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
| ((Write_mem id a Nothing value),true) -> ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Nothing)
- | ((Write_mem id a Nothing value),false) -> ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
+ | ((Write_mem id a Nothing value),false) ->
+ ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
| _ -> ((Action a s,lm,le), Just (next_builder lexp_builder)) end)
| e -> e end)
| _ -> ((Error "Vector access must be a number",lm,le),Nothing) end)
- | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e -> (LEXP_vector lexp e)))
+ | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e -> (LEXP_aux (LEXP_vector lexp e) annot)))
| e -> (e,Nothing) end
| LEXP_vector_range lexp exp1 exp2 ->
match (interp_main t_level l_env l_mem exp1) with
| (Value i1, lm, le) ->
(match i1 with
- | V_lit (L_num n1) ->
+ | V_lit (L_aux (L_num n1) ln1) ->
(match (interp_main t_level l_env l_mem exp2) with
| (Value i2,lm,le) ->
(match i2 with
- | V_lit (L_num n2) ->
- let next_builder le_builder = (fun e -> LEXP_vector_range (le_builder e) (E_lit (L_num n1)) (E_lit (L_num n2))) in
+ | V_lit (L_aux (L_num n2) ln2) ->
+ let next_builder le_builder =
+ (fun e -> LEXP_aux (LEXP_vector_range (le_builder e)
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing))) annot) in
(match (create_write_message_or_update t_level value l_env lm false lexp) with
| ((Value v,lm,le), Just lexp_builder) ->
(match (v,is_top_level) with
| (V_vector m inc vs,true) ->
- ((Value (V_lit L_unit), update_vector_slice (slice_vector v n1 n2) value lm, l_env), Nothing)
+ ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice (slice_vector v n1 n2) value lm, l_env), Nothing)
| (V_vector m inc vs,false) ->
((Value (slice_vector v n1 n2),lm,l_env), Just (next_builder lexp_builder))
| _ -> ((Error "Vector required",lm,le),Nothing) end)
@@ -930,56 +1033,59 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
| e -> e end)
| _ -> ((Error "Vector slice requires a number", lm, le),Nothing) end)
| (Action a s,lm,le) ->
- ((Action a s,lm, le), Just (fun e -> LEXP_vector_range lexp (E_lit (L_num n1)) e))
+ ((Action a s,lm, le), Just (fun e -> LEXP_aux (LEXP_vector_range lexp
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ e) annot))
| e -> (e,Nothing) end)
| _ -> ((Error "Vector slice requires a number", lm, le),Nothing) end)
| (Action a s,lm,le) ->
- ((Action a s, lm,le), Just (fun e -> LEXP_vector_range lexp e exp2))
+ ((Action a s, lm,le), Just (fun e -> LEXP_aux (LEXP_vector_range lexp e exp2) annot))
| e -> (e,Nothing) end
| LEXP_field lexp id ->
(match (create_write_message_or_update t_level value l_env l_mem false lexp) with
| ((Value (V_record fexps),lm,le),Just lexp_builder) ->
match (in_env fexps id,is_top_level) with
- | (Just (V_boxref n),true) -> ((Value (V_lit L_unit), update_mem lm n value, l_env),Nothing)
- | (Just (V_boxref n),false) -> ((Value (in_mem lm n),lm,l_env),Just (fun e -> LEXP_field (lexp_builder e) id))
+ | (Just (V_boxref n),true) -> ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
+ | (Just (V_boxref n),false) ->
+ ((Value (in_mem lm n),lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) annot))
| (Just v, true) -> ((Error "Field access requires record",lm,le),Nothing)
- | (Just v,false) -> ((Value v,lm,l_env),Just (fun e -> LEXP_field (lexp_builder e) id))
+ | (Just v,false) -> ((Value v,lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) annot))
| (Nothing,_) -> ((Error "Field not found in specified record",lm,le),Nothing) end
| ((Action a s,lm,le), Just lexp_builder) ->
match a with
- | Read_reg _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_field (lexp_builder e) id))
- | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_field (lexp_builder e) id))
- | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_field (lexp_builder e) id))
+ | Read_reg _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) annot))
+ | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) annot))
+ | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) annot))
| _ -> ((Error "Unimplemented feature, writing to a field in a register or memory",lm,le),Nothing)
end
| e -> e end)
end
-and interp_letbind t_level l_env l_mem lbind =
+and interp_letbind t_level l_env l_mem (LB_aux lbind annot) =
match lbind with
| LB_val_explicit t pat exp ->
match (interp_main t_level l_env l_mem exp) with
| (Value v,lm,le) ->
(match match_pattern pat v with
- | (true,env) -> ((Value (V_lit L_unit), lm, env++l_env),Nothing)
+ | (true,env) -> ((Value (V_lit (L_aux L_unit Unknown)), lm, env++l_env),Nothing)
| _ -> ((Error "Pattern in letbind did not match value",lm,le),Nothing) end)
- | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> LB_val_explicit t pat e)))
+ | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_explicit t pat e) annot))))
| e -> (e,Nothing) end
| LB_val_implicit pat exp ->
match (interp_main t_level l_env l_mem exp) with
| (Value v,lm,le) ->
(match match_pattern pat v with
- | (true,env) -> ((Value (V_lit L_unit), lm, env++l_env),Nothing)
+ | (true,env) -> ((Value (V_lit (L_aux L_unit Unknown)), lm, env++l_env),Nothing)
| _ -> ((Error "Pattern in letbind did not match value",lm,le),Nothing) end)
- | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> LB_val_implicit pat e)))
+ | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_implicit pat e) annot))))
| e -> (e,Nothing) end
end
let rec to_global_letbinds (Defs defs) t_level =
let (Env defs' externs lets regs mems ctors) = t_level in
match defs with
- | [] -> ((Value (V_lit L_unit), emem, []),t_level)
- | def ::defs ->
+ | [] -> ((Value (V_lit (L_aux L_unit Unknown)), emem, []),t_level)
+ | (DEF_aux def _)::defs ->
match def with
| DEF_val lbind ->
match interp_letbind t_level [] emem lbind with
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index aeb81085..b18d031e 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -8,51 +8,51 @@ open import Word
let compose f g x = f (V_tuple [g x]) ;;
-let is_one (V_lit b) = V_lit (if b = L_one then L_true else L_false) ;;
+let is_one (V_lit (L_aux b lb)) = V_lit (L_aux (if b = L_one then L_true else L_false) lb) ;;
-let eq (V_tuple [x; y]) = V_lit (if x = y then L_true else L_false) ;;
+let eq (V_tuple [x; y]) = V_lit (L_aux (if x = y then L_true else L_false) Unknown) ;;
-let neg (V_tuple [V_lit arg]) = V_lit (match arg with
+let neg (V_tuple [V_lit (L_aux arg la)]) = V_lit (L_aux (match arg with
| L_true -> L_false
- | L_false -> L_true end) ;;
+ | L_false -> L_true end) la) ;;
let neq = compose neg eq ;;
let bit_to_bool b = match b with
- V_lit L_zero -> false
- | V_lit L_one -> true
+ V_lit (L_aux L_zero _) -> false
+ | V_lit (L_aux L_one _) -> true
end ;;
let bool_to_bit b = match b with
- false -> V_lit L_zero
- | true -> V_lit L_one
+ false -> V_lit (L_aux L_zero Unknown)
+ | true -> V_lit (L_aux L_one Unknown)
end ;;
(* XXX always interpret as positive ? *)
let to_num_dec (V_vector idx false l) =
- V_lit(L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool (reverse l)))));;
+ V_lit(L_aux (L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool (reverse l))))) Unknown);;
let to_num_inc (V_vector idx true l) =
- V_lit(L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool l))));;
+ V_lit(L_aux (L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool l)))) Unknown);;
(* XXX not quite sure about list reversal here - what is the convention for
* V_vector? cf. above too *)
-let to_vec_dec len (V_lit(L_num n)) =
- let BitSeq _ false l = bitSeqFromNatural len n in
+let to_vec_dec len (V_lit(L_aux (L_num n) ln)) =
+ let (BitSeq _ false l) = bitSeqFromNatural len n in
V_vector 0 false (map bool_to_bit (reverse l)) ;;
-let to_vec_inc len (V_lit(L_num n)) =
- let BitSeq _ false l = bitSeqFromNatural len n in
+let to_vec_inc len (V_lit(L_aux (L_num n) ln)) =
+ let (BitSeq _ false l) = bitSeqFromNatural len n in
V_vector 0 true (map bool_to_bit l) ;;
let rec add (V_tuple args) = match args with
(* vector case *)
| [(V_vector _ d l as v); (V_vector _ d' l' as v')] ->
- let V_lit (L_num x) = (if d then to_num_inc else to_num_dec) v in
- let V_lit (L_num y) = (if d' then to_num_inc else to_num_dec) v' in
+ let (V_lit (L_aux (L_num x) lx)) = (if d then to_num_inc else to_num_dec) v in
+ let (V_lit (L_aux (L_num y) ly)) = (if d' then to_num_inc else to_num_dec) v' in
(* XXX how shall I decide this? max? max+1? *)
let len = max (List.length l) (List.length l') in
(* XXX assume d = d' *)
- (if d then to_vec_inc else to_vec_dec) (Just len) (V_lit (L_num (x+y)))
+ (if d then to_vec_inc else to_vec_dec) (Just len) (V_lit (L_aux (L_num (x+y)) lx))
(* integer case *)
- | [V_lit(L_num x); V_lit(L_num y)] -> V_lit(L_num (x+y))
+ | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (x+y)) lx)
(* assume other literals are L_bin or L_hex, ie. vectors *)
| [V_lit l; x ] -> add (V_tuple [litV_to_vec l; x])
| [ x ; V_lit l ] -> add (V_tuple [x; litV_to_vec l])
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 2440f60f..76973c04 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -19,18 +19,18 @@ let lit_to_string = function
;;
let id_to_string = function
- | Id s | DeIid s -> s
+ | Id_aux(Id s,_) | Id_aux(DeIid s,_) -> s
;;
let bitvec_to_string l = "0b" ^ (String.concat "" (List.map (function
- | V_lit(L_zero) -> "0"
- | V_lit(L_one) -> "1"
+ | V_lit(L_aux(L_zero, _)) -> "0"
+ | V_lit(L_aux(L_one, _)) -> "1"
| _ -> assert false) l))
;;
let rec val_to_string = function
| V_boxref n -> sprintf "boxref %d" n
- | V_lit l -> sprintf (*"literal %s" *) "%s" (lit_to_string l)
+ | V_lit (L_aux(l,_)) -> sprintf (*"literal %s" *) "%s" (lit_to_string l)
| V_tuple l ->
let repr = String.concat ", " (List.map val_to_string l) in
sprintf "tuple <%s>" repr
@@ -106,22 +106,22 @@ let vconcat v v' = vec_concat (V_tuple [v; v']) ;;
let perform_action ((reg, mem) as env) = function
| Read_reg ((Reg (id, _) | SubReg (id, _, _)), sub) ->
slice (Reg.find id reg) sub, env
- | Read_mem (id, V_lit(L_num n), sub) ->
+ | Read_mem (id, V_lit(L_aux((L_num n),_)), sub) ->
slice (Mem.find (id, n) mem) sub, env
| Write_reg ((Reg (id, _) | SubReg (id, _, _)), None, value) ->
- V_lit L_unit, (Reg.add id value reg, mem)
+ V_lit (L_aux(L_unit,Interp_ast.Unknown)), (Reg.add id value reg, mem)
| Write_reg ((Reg (id, _) | SubReg (id, _, _)), Some (start, stop), value) ->
(* XXX if updating a single element, wrap value into a vector -
* should the typechecker do that coercion for us automatically? *)
let value = if eq_big_int start stop then V_vector (zero_big_int, true, [value]) else value in
let old_val = Reg.find id reg in
let new_val = fupdate_vector_slice old_val value start stop in
- V_lit L_unit, (Reg.add id new_val reg, mem)
- | Write_mem (id, V_lit(L_num n), None, value) ->
- V_lit L_unit, (reg, Mem.add (id, n) value mem)
+ V_lit (L_aux(L_unit,Interp_ast.Unknown)), (Reg.add id new_val reg, mem)
+ | Write_mem (id, V_lit(L_aux(L_num n,_)), None, value) ->
+ V_lit (L_aux(L_unit, Interp_ast.Unknown)), (reg, Mem.add (id, n) value mem)
(* multi-byte accesses to memory *)
(* XXX this doesn't deal with endianess at all, and it seems broken in tests *)
- | Read_mem (id, V_tuple [V_lit(L_num n); V_lit(L_num size)], sub) ->
+ | Read_mem (id, V_tuple [V_lit(L_aux(L_num n,_)); V_lit(L_aux(L_num size,_))], sub) ->
let rec fetch k acc =
if eq_big_int k size then slice acc sub else
let slice = Mem.find (id, add_big_int n k) mem in
@@ -131,7 +131,7 @@ let perform_action ((reg, mem) as env) = function
(* XXX no support for multi-byte slice write at the moment - not hard to add,
* but we need a function basic read/write first since slice access involves
* read, fupdate, write. *)
- | Write_mem (id, V_tuple [V_lit(L_num n); V_lit(L_num size)], None, value) ->
+ | Write_mem (id, V_tuple [V_lit(L_aux(L_num n,_)); V_lit(L_aux(L_num size,_))], None, value) ->
(* assumes smallest unit of memory is 8 bit *)
let byte_size = 8 in
let rec update k mem =
@@ -141,15 +141,15 @@ let perform_action ((reg, mem) as env) = function
(mult_int_big_int byte_size (succ_big_int k)) in
let mem' = Mem.add (id, add_big_int n k) slice mem in
update (succ_big_int k) mem'
- in V_lit L_unit, (reg, update zero_big_int mem)
+ in V_lit (L_aux(L_unit, Interp_ast.Unknown)), (reg, update zero_big_int mem)
(* This case probably never happens in the POWER spec anyway *)
- | Write_mem (id, V_lit(L_num n), Some (start, stop), value) ->
+ | Write_mem (id, V_lit(L_aux(L_num n,_)), Some (start, stop), value) ->
(* XXX if updating a single element, wrap value into a vector -
* should the typechecker do that coercion for us automatically? *)
let value = if eq_big_int start stop then V_vector (zero_big_int, true, [value]) else value in
let old_val = Mem.find (id, n) mem in
let new_val = fupdate_vector_slice old_val value start stop in
- V_lit L_unit, (reg, Mem.add (id, n) new_val mem)
+ V_lit (L_aux(L_unit, Interp_ast.Unknown)), (reg, Mem.add (id, n) new_val mem)
| Call_extern (name, arg) -> eval_external name arg, env
| _ -> assert false
;;
@@ -165,7 +165,7 @@ let run (name, test) =
eprintf "%s: action returned %s\n" name (val_to_string return);
loop env' (resume test s return)
| Error e -> eprintf "%s: error: %s\n" name e; false in
- let entry = E_app((Id "main"), [E_lit L_unit]) in
+ let entry = E_aux(E_app(Id_aux((Id "main"),Unknown), [E_aux(E_lit (L_aux(L_unit,Interp_ast.Unknown)),(Unknown,None))]),(Unknown,None)) in
eprintf "%s: starting\n" name;
try
Printexc.record_backtrace true;
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 236bfc91..4190ad9b 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1,3 +1,4 @@
+open Type_internal
open Ast
open Format
@@ -349,86 +350,115 @@ let pp_defs ppf (Defs(defs)) =
(****************************************************************************
- * source to Lem ast pretty printer
+ * annotated source to Lem ast pretty printer
****************************************************************************)
-let pp_format_id_lem (Id_aux(i,_)) =
- match i with
- | Id(i) -> "(Id \"" ^ i ^ "\")"
- | DeIid(x) -> "(DeIid \"" ^ x ^ "\")"
+let rec pp_format_l_lem = function
+ | Parse_ast.Unknown -> "Unknown"
+ | Parse_ast.Trans(s,None) -> "(Trans \"" ^ s ^ "\" Nothing)"
+ | Parse_ast.Trans(s,(Some l)) -> "(Trans \"" ^ s ^ "\" (Just " ^ (pp_format_l_lem l) ^ "))"
+ | Parse_ast.Range(p1,p2) -> "(Range \"" ^ p1.Lexing.pos_fname ^ "\" " ^
+ (string_of_int p1.Lexing.pos_lnum) ^ " " ^
+ (string_of_int (p1.Lexing.pos_cnum - p1.Lexing.pos_bol)) ^ " " ^
+ (string_of_int p2.Lexing.pos_lnum) ^ " " ^
+ (string_of_int (p2.Lexing.pos_cnum - p2.Lexing.pos_bol)) ^ ")"
+
+let pp_lem_l ppf l = base ppf (pp_format_l_lem l)
+
+let pp_format_id_lem (Id_aux(i,l)) =
+ "(Id_aux " ^
+ (match i with
+ | Id(i) -> "(Id \"" ^ i ^ "\")"
+ | DeIid(x) -> "(DeIid \"" ^ x ^ "\")") ^ " " ^
+ (pp_format_l_lem l) ^ ")"
let pp_lem_id ppf id = base ppf (pp_format_id_lem id)
-let pp_format_var_lem (Kid_aux(Var v,_)) = "(Var \"" ^ v ^ "\")"
+let pp_format_var_lem (Kid_aux(Var v,l)) = "(Kid_aux (Var \"" ^ v ^ "\") " ^ (pp_format_l_lem l) ^ ")"
let pp_lem_var ppf var = base ppf (pp_format_var_lem var)
-let pp_format_bkind_lem (BK_aux(k,_)) =
- match k with
- | BK_type -> "BK_type"
- | BK_nat -> "BK_nat"
- | BK_order -> "BK_order"
- | BK_effect -> "BK_effect"
+let pp_format_bkind_lem (BK_aux(k,l)) =
+ "(BK_aux " ^
+ (match k with
+ | BK_type -> "BK_type"
+ | BK_nat -> "BK_nat"
+ | BK_order -> "BK_order"
+ | BK_effect -> "BK_effect") ^ " " ^
+ (pp_format_l_lem l) ^ ")"
let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk)
-let pp_format_kind_lem (K_aux(K_kind(klst),_)) =
- "(K_kind [" ^ list_format "; " pp_format_bkind_lem klst ^ "])"
+let pp_format_kind_lem (K_aux(K_kind(klst),l)) =
+ "(K_aux (K_kind [" ^ list_format "; " pp_format_bkind_lem klst ^ "]) " ^ (pp_format_l_lem l) ^ ")"
let pp_lem_kind ppf k = base ppf (pp_format_kind_lem k)
-let rec pp_format_typ_lem (Typ_aux(t,_)) =
- match t with
- | Typ_id(id) -> "(Typ_id " ^ pp_format_id_lem id ^ ")"
- | Typ_var(var) -> "(Typ_var " ^ pp_format_var_lem var ^ ")"
- | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^
- pp_format_typ_lem ret ^ " " ^
- (pp_format_effects_lem efct) ^ ")"
- | Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])"
- | Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])"
- | Typ_wild -> "Typ_wild"
-and pp_format_nexp_lem (Nexp_aux(n,_)) =
- match n with
- | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
- | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")"
- | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
- | Nexp_times(n1,n2) -> "(Nexp_times " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
- | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")"
-and pp_format_ord_lem (Ord_aux(o,_)) =
- match o with
- | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")"
- | Ord_inc -> "Ord_inc"
- | Ord_dec -> "Ord_dec"
-and pp_format_effects_lem (Effect_aux(e,_)) =
- match e with
+let rec pp_format_typ_lem (Typ_aux(t,l)) =
+ "(Typ_aux " ^
+ (match t with
+ | Typ_id(id) -> "(Typ_id " ^ pp_format_id_lem id ^ ")"
+ | Typ_var(var) -> "(Typ_var " ^ pp_format_var_lem var ^ ")"
+ | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^
+ pp_format_typ_lem ret ^ " " ^
+ (pp_format_effects_lem efct) ^ ")"
+ | Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])"
+ | Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])"
+ | Typ_wild -> "Typ_wild") ^ " " ^
+ (pp_format_l_lem l) ^ ")"
+and pp_format_nexp_lem (Nexp_aux(n,l)) =
+ "(Nexp_aux " ^
+ (match n with
+ | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
+ | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")"
+ | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
+ | Nexp_times(n1,n2) -> "(Nexp_times " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
+ | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")") ^ " " ^
+ (pp_format_l_lem l) ^ ")"
+and pp_format_ord_lem (Ord_aux(o,l)) =
+ "(Ord_aux " ^
+ (match o with
+ | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")"
+ | Ord_inc -> "Ord_inc"
+ | Ord_dec -> "Ord_dec") ^ " " ^
+ (pp_format_l_lem l) ^ ")"
+and pp_format_base_effect_lem (BE_aux(e,l)) =
+ "(BE_aux " ^
+ (match e with
+ | BE_rreg -> "BE_rreg"
+ | BE_wreg -> "BE_wreg"
+ | BE_rmem -> "BE_rmem"
+ | BE_wmem -> "BE_wmem"
+ | BE_undef -> "BE_undef"
+ | BE_unspec -> "BE_unspec"
+ | BE_nondet -> "BE_nondet") ^ " " ^
+ (pp_format_l_lem l) ^ ")"
+and pp_format_effects_lem (Effect_aux(e,l)) =
+ "(Effect_aux " ^
+ (match e with
| Effect_var(v) -> "(Effect_var " ^ pp_format_var v ^ ")"
| Effect_set(efcts) ->
"(Effect_set [" ^
- (list_format "; "
- (fun (BE_aux(e,l)) ->
- match e with
- | BE_rreg -> "BE_rreg"
- | BE_wreg -> "BE_wreg"
- | BE_rmem -> "BE_rmem"
- | BE_wmem -> "BE_wmem"
- | BE_undef -> "BE_undef"
- | BE_unspec -> "BE_unspec"
- | BE_nondet -> "BE_nondet")
- efcts) ^ " ])"
-and pp_format_typ_arg_lem (Typ_arg_aux(t,_)) =
- match t with
+ (list_format "; " pp_format_base_effect_lem efcts) ^ " ])") ^ " " ^
+ (pp_format_l_lem l) ^ ")"
+and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) =
+ "(Typ_arg_aux " ^
+ (match t with
| Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")"
| Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")"
| Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")"
- | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")"
+ | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")") ^ " " ^
+ (pp_format_l_lem l) ^ ")"
let pp_lem_typ ppf t = base ppf (pp_format_typ_lem t)
let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n)
let pp_lem_ord ppf o = base ppf (pp_format_ord_lem o)
let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e)
+let pp_lem_beffect ppf be = base ppf (pp_format_base_effect_lem be)
-let pp_format_nexp_constraint_lem (NC_aux(nc,_)) =
- match nc with
+let pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
+ "(NC_aux " ^
+ (match nc with
| NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
| NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
| NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
@@ -436,38 +466,46 @@ let pp_format_nexp_constraint_lem (NC_aux(nc,_)) =
pp_format_var_lem id ^
" [" ^
list_format "; " string_of_int bounds ^
- "])"
+ "])") ^ " " ^
+ (pp_format_l_lem l) ^ ")"
let pp_lem_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint_lem nc)
-let pp_format_qi_lem (QI_aux(qi,_)) =
- match qi with
+let pp_format_qi_lem (QI_aux(qi,lq)) =
+ "(QI_aux " ^
+ (match qi with
| QI_const(n_const) -> "(QI_const " ^ pp_format_nexp_constraint_lem n_const ^ ")"
- | QI_id(KOpt_aux(ki,_)) ->
- "(QI_id " ^
+ | QI_id(KOpt_aux(ki,lk)) ->
+ "(QI_id (KOpt_aux " ^
(match ki with
| KOpt_none(var) -> "(KOpt_none " ^ pp_format_var_lem var ^ ")"
- | KOpt_kind(k,var) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_var_lem var ^ ")") ^ ")"
+ | KOpt_kind(k,var) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_var_lem var ^ ")") ^ " " ^
+ (pp_format_l_lem lk) ^ "))") ^ " " ^
+ (pp_format_l_lem lq) ^ ")"
let pp_lem_qi ppf qi = base ppf (pp_format_qi_lem qi)
-let pp_format_typquant_lem (TypQ_aux(tq,_)) =
- match tq with
+let pp_format_typquant_lem (TypQ_aux(tq,l)) =
+ "(TypQ_aux " ^
+ (match tq with
| TypQ_no_forall -> "TypQ_no_forall"
| TypQ_tq(qlist) ->
"(TypQ_tq [" ^
(list_format "; " pp_format_qi_lem qlist) ^
- "])"
+ "])") ^ " " ^
+ (pp_format_l_lem l) ^ ")"
let pp_lem_typquant ppf tq = base ppf (pp_format_typquant_lem tq)
-let pp_format_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),_)) =
- "(TypSchm_ts " ^ (pp_format_typquant_lem tq) ^ " " ^ pp_format_typ_lem t ^ ")"
+let pp_format_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),l)) =
+ "(TypSchm_aux (TypSchm_ts " ^ (pp_format_typquant_lem tq) ^ " " ^ pp_format_typ_lem t ^ ") " ^
+ (pp_format_l_lem l) ^ ")"
let pp_lem_typscm ppf ts = base ppf (pp_format_typscm_lem ts)
-let pp_format_lit_lem (L_aux(l,_)) =
- match l with
+let pp_format_lit_lem (L_aux(lit,l)) =
+ "(L_aux " ^
+ (match lit with
| L_unit -> "L_unit"
| L_zero -> "L_zero"
| L_one -> "L_one"
@@ -477,12 +515,81 @@ let pp_format_lit_lem (L_aux(l,_)) =
| L_hex(n) -> "(L_hex \"" ^ n ^ "\")"
| L_bin(n) -> "(L_bin \"" ^ n ^ "\")"
| L_undef -> "L_undef"
- | L_string(s) -> "(L_string \"" ^ s ^ "\")"
+ | L_string(s) -> "(L_string \"" ^ s ^ "\")") ^ " " ^
+ (pp_format_l_lem l) ^ ")"
let pp_lem_lit ppf l = base ppf (pp_format_lit_lem l)
-let rec pp_format_pat_lem (P_aux(p,l)) =
- match p with
+
+let rec pp_format_t t =
+ match t.t with
+ | Tid i -> "(T_id (Id_aux (Id \"" ^ i ^ "\") Unknown))"
+ | Tvar i -> "(T_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+ | Tfn(t1,t2,e) -> "(T_fn " ^ (pp_format_t t1) ^ " " ^ (pp_format_t t2) ^ " " ^ pp_format_e e ^ ")"
+ | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t tups) ^ "])"
+ | Tapp(i,args) -> "(T_app (Id_aux (Id \"" ^ i ^ "\") Unknown) (T_args [" ^ list_format "; " pp_format_targ args ^ "]))"
+ | Tuvar(_) -> "(T_var (Kid_aux (Var \"fresh_v\") Unknown))"
+and pp_format_targ = function
+ | TA_typ t -> "(T_arg_typ " ^ pp_format_t t ^ ")"
+ | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n n ^ ")"
+ | TA_eft e -> "(T_arg_effect " ^ pp_format_e e ^ ")"
+ | TA_ord o -> "(T_arg_order " ^ pp_format_o o ^ ")"
+and pp_format_n n =
+ match n.nexp with
+ | Nvar i -> "(Ne_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+ | Nconst i -> "(Ne_const " ^ string_of_int i ^ ")"
+ | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n n1) ^ "; " ^ (pp_format_n n2) ^ "])"
+ | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")"
+ | N2n n -> "(Ne_exp " ^ (pp_format_n n) ^ ")"
+ | Nneg n -> "(Ne_unary " ^ (pp_format_n n) ^ ")"
+ | Nuvar(_) -> "(Ne_var (Kid_aux (Var \"fresh_v\") Unknown))"
+and pp_format_e e =
+ "(Effect_aux " ^
+ (match e.effect with
+ | Evar i -> "(Effect_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+ | Eset es -> "(Effect_set [" ^
+ (list_format "; " pp_format_base_effect_lem es) ^ " ])"
+ | Euvar(_) -> "(Effect_var (Kid_aux (Var \"fresh_v\") Unknown))")
+ ^ " Unknown)"
+and pp_format_o o =
+ "(Ord_aux " ^
+ (match o.order with
+ | Ovar i -> "(Ord_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+ | Oinc -> "Ord_inc"
+ | Odec -> "Ord_dec"
+ | Ouvar(_) -> "(Ord_var (Kid_aux (Var \"fresh_v\") Unknown))")
+ ^ " Unknown)"
+
+let pp_format_tag = function
+ | Emp -> "Tag_empty"
+ | External (Some s) -> "(Tag_extern (Just \""^s^"\"))"
+ | External None -> "(Tag_extern Nothing)"
+ | Default -> "Tag_default"
+ | Constructor -> "Tag_ctor"
+ | Enum -> "Tag_enum"
+ | Spec -> "Tag_spec"
+
+let pp_format_nes nes =
+ "[" ^
+ (list_format "; "
+ (fun ne -> match ne with
+ | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
+ | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
+ | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
+ | In(_,i,ns) -> "(Nec_in (Kid_aux (Var \"" ^ i ^ "\") Unknown) [" ^ (list_format "; " string_of_int ns)^ "])")
+ nes) ^ "]"
+
+let pp_format_annot = function
+ | None -> "Nothing"
+ | Some((_,t),tag,nes,efct) ->
+ "(Just (" ^ pp_format_t t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ pp_format_e efct ^ "))"
+
+let pp_annot ppf ant = base ppf (pp_format_annot ant)
+
+
+let rec pp_format_pat_lem (P_aux(p,(l,annot))) =
+ "(P_aux " ^
+ (match p with
| P_lit(lit) -> "(P_lit " ^ pp_format_lit_lem lit ^ ")"
| P_wild -> "P_wild"
| P_id(id) -> "(P_id " ^ pp_format_id_lem id ^ ")"
@@ -499,156 +606,182 @@ let rec pp_format_pat_lem (P_aux(p,l)) =
"(P_vector_indexed [" ^ list_format "; " (fun (i,p) -> Printf.sprintf "(%d, %s)" i (pp_format_pat_lem p)) ipats ^ "])"
| P_vector_concat(pats) -> "(P_vector_concat [" ^ list_format "; " pp_format_pat_lem pats ^ "])"
| P_tup(pats) -> "(P_tup [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
- | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
+ | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])") ^
+ " (" ^ pp_format_l_lem l ^ ", " ^ pp_format_annot annot ^ "))"
let pp_lem_pat ppf p = base ppf (pp_format_pat_lem p)
-let rec pp_lem_let ppf (LB_aux(lb,_)) =
- match lb with
- | LB_val_explicit(ts,pat,exp) ->
- fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp
- | LB_val_implicit(pat,exp) ->
- fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat pp_lem_exp exp
-
-and pp_lem_exp ppf (E_aux(e,_)) =
- match e with
- | E_block(exps) -> fprintf ppf "@[<0>%a [%a] %a@]"
+let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) =
+ let print_lb ppf lb =
+ match lb with
+ | LB_val_explicit(ts,pat,exp) ->
+ fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp
+ | LB_val_implicit(pat,exp) ->
+ fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat pp_lem_exp exp in
+ fprintf ppf "@[<0>(LB_aux %a (%a, %a))@]" print_lb lb pp_lem_l l pp_annot annot
+
+and pp_lem_exp ppf (E_aux(e,(l,annot))) =
+ let print_e ppf e =
+ match e with
+ | E_block(exps) -> fprintf ppf "@[<0>%a [%a] %a@]"
kwd "(E_block"
(list_pp pp_semi_lem_exp pp_lem_exp) exps
kwd ")"
- | E_id(id) -> fprintf ppf "(%a %a)" kwd "E_id" pp_lem_id id
- | E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit
- | E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp
- | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args
- | E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r
- | E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")"
- | E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e
- | E_for(id,exp1,exp2,exp3,order,exp4) ->
- fprintf ppf "@[<0>(%a %a %a %a %a %a @ @[<1> %a @])@]"
- kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4
- | E_vector(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps
- | E_vector_indexed(iexps) ->
- let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in
- let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in
- fprintf ppf "@[<0>(%a [%a]) @]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps
- | E_vector_access(v,e) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_vector_access" pp_lem_exp v pp_lem_exp e
- | E_vector_subrange(v,e1,e2) ->
- fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e1
- | E_vector_update(v,e1,e2) ->
- fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_update" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2
- | E_vector_update_subrange(v,e1,e2,e3) ->
- fprintf ppf "@[<0>(%a %a %a %a %a)@]" kwd "E_vector_update_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3
- | E_list(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_list" (list_pp pp_semi_lem_exp pp_lem_exp) exps
- | E_cons(e1,e2) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cons" pp_lem_exp e1 pp_lem_exp e2
- | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
- fprintf ppf "@[<0>(%a [%a]))@]" kwd "E_record(FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps
- | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),_))) ->
- fprintf ppf "@[<0>(%a %a (%a [%a]))@]"
- kwd "E_record_update" pp_lem_exp exp kwd "FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps
- | E_field(fexp,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_field" pp_lem_exp fexp pp_lem_id id
- | E_case(exp,pexps) ->
- fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps
- | E_let(leb,exp) -> fprintf ppf "@[<0>(%a %a %a) @]" kwd "E_let" pp_lem_let leb pp_lem_exp exp
- | E_assign(lexp,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp
+ | E_id(id) -> fprintf ppf "(%a %a)" kwd "E_id" pp_lem_id id
+ | E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit
+ | E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp
+ | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args
+ | E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r
+ | E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")"
+ | E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e
+ | E_for(id,exp1,exp2,exp3,order,exp4) ->
+ fprintf ppf "@[<0>(%a %a %a %a %a %a @ @[<1> %a @])@]"
+ kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4
+ | E_vector(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps
+ | E_vector_indexed(iexps) ->
+ let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in
+ let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in
+ fprintf ppf "@[<0>(%a [%a]) @]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps
+ | E_vector_access(v,e) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_vector_access" pp_lem_exp v pp_lem_exp e
+ | E_vector_subrange(v,e1,e2) ->
+ fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e1
+ | E_vector_update(v,e1,e2) ->
+ fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_update" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2
+ | E_vector_update_subrange(v,e1,e2,e3) ->
+ fprintf ppf "@[<0>(%a %a %a %a %a)@]" kwd "E_vector_update_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3
+ | E_list(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_list" (list_pp pp_semi_lem_exp pp_lem_exp) exps
+ | E_cons(e1,e2) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cons" pp_lem_exp e1 pp_lem_exp e2
+ | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
+ fprintf ppf "@[<0>(%a [%a]))@]" kwd "E_record(FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps
+ | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),_))) ->
+ fprintf ppf "@[<0>(%a %a (%a [%a]))@]"
+ kwd "E_record_update" pp_lem_exp exp kwd "FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps
+ | E_field(fexp,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_field" pp_lem_exp fexp pp_lem_id id
+ | E_case(exp,pexps) ->
+ fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps
+ | E_let(leb,exp) -> fprintf ppf "@[<0>(%a %a %a) @]" kwd "E_let" pp_lem_let leb pp_lem_exp exp
+ | E_assign(lexp,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp
+ in
+ fprintf ppf "@[<0>(E_aux %a (%a, %a))@]" print_e e pp_lem_l l pp_annot annot
and pp_semi_lem_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_lem_exp e kwd ";"
-and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),_)) = fprintf ppf "@[<1>(%a %a %a)@]" kwd "FE_Fexp" pp_lem_id id pp_lem_exp exp
+and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),(l,annot))) =
+ fprintf ppf "@[<1>(FE_aux (%a %a %a) (%a, %a))@]" kwd "FE_Fexp" pp_lem_id id pp_lem_exp exp pp_lem_l l pp_annot annot
and pp_semi_lem_fexp ppf fexp = fprintf ppf "@[<1>%a %a@]" pp_lem_fexp fexp kwd ";"
-and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),_)) =
- fprintf ppf "@[<1>(%a %a@ %a)@]" kwd "Pat_exp" pp_lem_pat pat pp_lem_exp exp
+and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),(l,annot))) =
+ fprintf ppf "@[<1>(Pat_aux (%a %a@ %a) (%a, %a))@]" kwd "Pat_exp" pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot
and pp_semi_lem_case ppf case = fprintf ppf "@[<1>%a %a@]" pp_lem_case case kwd ";"
-and pp_lem_lexp ppf (LEXP_aux(lexp,_)) =
- match lexp with
- | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
- | LEXP_memory(id,args) -> fprintf ppf "(%a %a [%a])" kwd "LEXP_memory" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args
- | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp
- | LEXP_vector_range(v,e1,e2) ->
- fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v pp_lem_exp e1 pp_lem_exp e2
- | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id
-
-let pp_lem_default ppf (DT_aux(df,_)) =
- match df with
- | DT_kind(bk,var) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_var var
- | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id
-
-let pp_lem_spec ppf (VS_aux(v,_)) =
- match v with
- | VS_val_spec(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id
- | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s
- | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_extern_no_rename" pp_lem_typscm ts pp_lem_id id
-
-let pp_lem_namescm ppf (Name_sect_aux(ns,_)) =
+and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) =
+ let print_le ppf lexp =
+ match lexp with
+ | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
+ | LEXP_memory(id,args) -> fprintf ppf "(%a %a [%a])" kwd "LEXP_memory" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args
+ | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp
+ | LEXP_vector_range(v,e1,e2) ->
+ fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v pp_lem_exp e1 pp_lem_exp e2
+ | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id
+ in
+ fprintf ppf "@[(LEXP_aux %a (%a, %a))@]" print_le lexp pp_lem_l l pp_annot annot
+
+let pp_lem_default ppf (DT_aux(df,(l,annot))) =
+ let print_de ppf df =
+ match df with
+ | DT_kind(bk,var) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_var var
+ | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id
+ in
+ fprintf ppf "@[<0>(DT_aux %a (%a, %a))@]" print_de df pp_lem_l l pp_annot annot
+
+let pp_lem_spec ppf (VS_aux(v,(l,annot))) =
+ let print_spec ppf v =
+ match v with
+ | VS_val_spec(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id
+ | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s
+ | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_extern_no_rename" pp_lem_typscm ts pp_lem_id id
+ in
+ fprintf ppf "@[<0>(VS_aux %a (%a, %a))@]" print_spec v pp_lem_l l pp_annot annot
+
+let pp_lem_namescm ppf (Name_sect_aux(ns,l)) =
match ns with
- | Name_sect_none -> fprintf ppf "Name_sect_none"
- | Name_sect_some(s) -> fprintf ppf "(%a \"%s\")" kwd "Name_sect_some" s
+ | Name_sect_none -> fprintf ppf "(Name_sect_aux Name_sect_none %a)" pp_lem_l l
+ | Name_sect_some(s) -> fprintf ppf "(Name_sect_aux (Name_sect_some \"%s\") %a)" s pp_lem_l l
-let rec pp_lem_range ppf (BF_aux(r,_)) =
+let rec pp_lem_range ppf (BF_aux(r,l)) =
match r with
- | BF_single(i) -> fprintf ppf "(BF_single %i)" i
- | BF_range(i1,i2) -> fprintf ppf "(BF_range %i %i)" i1 i2
- | BF_concat(ir1,ir2) -> fprintf ppf "(%a %a %a)" kwd "BF_concat" pp_lem_range ir1 pp_lem_range ir2
-
-let pp_lem_typdef ppf (TD_aux(td,_)) =
- match td with
- | TD_abbrev(id,namescm,typschm) ->
- fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm
- | TD_record(id,nm,typq,fs,_) ->
- let f_pp ppf (typ,id) =
- fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
- fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
- kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
- | TD_variant(id,nm,typq,ar,_) ->
- let a_pp ppf (Tu_aux(typ_u,_)) =
- match typ_u with
- | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_ty_id %a %a);@]" pp_lem_typ typ pp_lem_id id
- | Tu_id(id) -> fprintf ppf "@[<1>(Tu_id %a);@]" pp_lem_id id
- in
- fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
- kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar
- | TD_enum(id,ns,enums,_) ->
- let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in
- fprintf ppf "@[<0>(%a %a %a [%a] false)@]"
- kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums
- | TD_register(id,n1,n2,rs) ->
- let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
- let pp_rids = (list_pp pp_rid pp_rid) in
- fprintf ppf "@[<0>(%a %a %a %a [%a])@]"
- kwd "TD_register" pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs
-
-let pp_lem_rec ppf (Rec_aux(r,_)) =
+ | BF_single(i) -> fprintf ppf "(BF_aux (BF_single %i) %a)" i pp_lem_l l
+ | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" i1 i2 pp_lem_l l
+ | BF_concat(ir1,ir2) -> fprintf ppf "(BF_aux (BF_concat %a %a) %a)" pp_lem_range ir1 pp_lem_range ir2 pp_lem_l l
+
+let pp_lem_typdef ppf (TD_aux(td,(l,annot))) =
+ let print_td ppf td =
+ match td with
+ | TD_abbrev(id,namescm,typschm) ->
+ fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm
+ | TD_record(id,nm,typq,fs,_) ->
+ let f_pp ppf (typ,id) =
+ fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
+ fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
+ kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
+ | TD_variant(id,nm,typq,ar,_) ->
+ let a_pp ppf (Tu_aux(typ_u,l)) =
+ match typ_u with
+ | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]"
+ pp_lem_typ typ pp_lem_id id pp_lem_l l
+ | Tu_id(id) -> fprintf ppf "@[<1>(Tu_aux (Tu_id %a) %a);@]" pp_lem_id id pp_lem_l l
+ in
+ fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
+ kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar
+ | TD_enum(id,ns,enums,_) ->
+ let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in
+ fprintf ppf "@[<0>(%a %a %a [%a] false)@]"
+ kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums
+ | TD_register(id,n1,n2,rs) ->
+ let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
+ let pp_rids = (list_pp pp_rid pp_rid) in
+ fprintf ppf "@[<0>(%a %a %a %a [%a])@]"
+ kwd "TD_register" pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs
+ in
+ fprintf ppf "@[<0>(TD_aux %a (%a, %a))@]" print_td td pp_lem_l l pp_annot annot
+
+let pp_lem_rec ppf (Rec_aux(r,l)) =
match r with
- | Rec_nonrec -> fprintf ppf "Rec_nonrec"
- | Rec_rec -> fprintf ppf "Rec_rec"
-
-let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,_)) =
+ | Rec_nonrec -> fprintf ppf "(Rec_aux Rec_nonrec %a)" pp_lem_l l
+ | Rec_rec -> fprintf ppf "(Rec_aux Rec_rec %a)" pp_lem_l l
+
+let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,l)) =
match t with
- | Typ_annot_opt_some(tq,typ) -> fprintf ppf "(Typ_annot_opt_some %a %a)" pp_lem_typquant tq pp_lem_typ typ
+ | Typ_annot_opt_some(tq,typ) ->
+ fprintf ppf "(Typ_annot_opt_aux (Typ_annot_opt_some %a %a) %a)" pp_lem_typquant tq pp_lem_typ typ pp_lem_l l
-let pp_lem_effects_opt ppf (Effect_opt_aux(e,_)) =
+let pp_lem_effects_opt ppf (Effect_opt_aux(e,l)) =
match e with
- | Effect_opt_pure -> fprintf ppf "Effect_opt_pure"
- | Effect_opt_effect e -> fprintf ppf "(Effect_opt_effect %a)" pp_lem_effects e
+ | Effect_opt_pure -> fprintf ppf "(Effect_opt_aux Effect_opt_pure %a)" pp_lem_l l
+ | Effect_opt_effect e -> fprintf ppf "(Effect_opt_aux (Effect_opt_effect %a) %a)" pp_lem_effects e pp_lem_l l
-let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
- fprintf ppf "@[<0>(%a %a %a %a)@]@\n" kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp
+let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),(l,annot))) =
+ fprintf ppf "@[<0>(FCL_aux (%a %a %a %a) (%a, %a))@]@\n"
+ kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot
-let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),_)) =
+let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) =
let pp_funcls ppf funcl = fprintf ppf "%a %a" pp_lem_funcl funcl kwd ";" in
- fprintf ppf "@[<0>(%a %a %a %a [%a])@]"
+ fprintf ppf "@[<0>(FD_aux (%a %a %a %a [%a]) (%a, %a))@]"
kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls
-
-let pp_lem_def ppf (DEF_aux(d,(l,_))) =
- match d with
- | DEF_default(df) -> fprintf ppf "(DEF_default %a);@\n" pp_lem_default df
- | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a);@\n" pp_lem_spec v_spec
- | DEF_type(t_def) -> fprintf ppf "(DEF_type %a);@\n" pp_lem_typdef t_def
- | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a);@\n" pp_lem_fundef f_def
- | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind
- | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>(%a %a %a)@];@\n" kwd "DEF_reg_dec" pp_lem_typ typ pp_lem_id id
- | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs")
+ pp_lem_l l pp_annot annot
+
+let pp_lem_def ppf (DEF_aux(d,(l,annot))) =
+ let print_d ppf d =
+ match d with
+ | DEF_default(df) -> fprintf ppf "(DEF_default %a)" pp_lem_default df
+ | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a)" pp_lem_spec v_spec
+ | DEF_type(t_def) -> fprintf ppf "(DEF_type %a)" pp_lem_typdef t_def
+ | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a)" pp_lem_fundef f_def
+ | DEF_val(lbind) -> fprintf ppf "(DEF_val %a)" pp_lem_let lbind
+ | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DEF_reg_dec" pp_lem_typ typ pp_lem_id id
+ | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs")
+ in
+ fprintf ppf "@[<0>(DEF_aux %a (%a, %a))@];@\n" print_d d pp_lem_l l pp_annot annot
let pp_lem_defs ppf (Defs(defs)) =
fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs
diff --git a/src/process_file.ml b/src/process_file.ml
index 25fbe49b..592c8cf5 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -159,6 +159,7 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo
let (o, ext_o) = open_output_with_check (f' ^ ".lem") in
Format.fprintf o "(* %s *)@\n" (generated_line filename);
Format.fprintf o "open import Interp_ast@\n";
+ Format.fprintf o "open import Pervasives@\n";
Format.fprintf o "let defs = ";
Pretty_print.pp_lem_defs o defs;
close_output_with_check ext_o
diff --git a/src/type_check.ml b/src/type_check.ml
index c9b12fe6..7e999c3d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1141,7 +1141,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
| None -> Some(id_to_string id)) funcls None in
let in_env = Envmap.apply t_env id in
let ret_t,param_t,tannot = match tannotopt with
- | Typ_annot_opt_aux(Typ_annot_opt_some(typq,typ),(l',annot')) ->
+ | Typ_annot_opt_aux(Typ_annot_opt_some(typq,typ),l') ->
let (ids,constraints) = typq_to_params envs typq in
let t = typ_to_t typ in
let p_t = new_t () in
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-15 16:40:07 +0000