summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorKathy Gray2014-02-21 23:09:09 +0000
committerKathy Gray2014-02-21 23:09:09 +0000
commit80628627e3d1bfc3cfca0d1c676f256e5fcba10b (patch)
treed1340eaca97771b3f1cd0e2b60db5ef1e9ea5514 /src
parent53146de4b82f90d1b06e9a09c5ec7c5b458fda53 (diff)
Add type annotations to lem grammar, including printing out the annotated ast, and extending the interpreter to expect annotations.
Annotations and locations are still not used by the interpreter.
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-03-02 03:08:16 +0000