Moved metatheory grammars into l2_rules.ott

Added val extern specification to language, parser, printer, and interpreter

Added various def level type system support, expressions type system in place Except for assignment

4 files changed, 63 insertions, 18 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 82c975c4..4d16fef4 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -415,7 +415,11 @@ let to_ast_spec (names,k_env,t_env) (val_:Parse_ast.val_spec) : (tannot val_spec
     (match vs with
     | Parse_ast.VS_val_spec(ts,id) ->
       let typsch,_,_ = to_ast_typschm k_env ts in
-      VS_aux(VS_val_spec(typsch,to_ast_id id),(l,None)),(names,k_env,t_env)) (*Do names and t_env need updating this pass? *)
+      VS_aux(VS_val_spec(typsch,to_ast_id id),(l,None)),(names,k_env,t_env)
+    | Parse_ast.VS_extern_spec(ts,id,s) ->
+      let typsch,_,_ = to_ast_typschm k_env ts in
+      VS_aux(VS_extern_spec(typsch,to_ast_id id,s),(l,None)),(names,k_env,t_env))(*Do names and t_env need updating this pass? *)
+    
 
 let to_ast_namescm (Parse_ast.Name_sect_aux(ns,l)) = 
   Name_sect_aux(
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index b6f16d4f..aeb846d9 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -28,6 +28,7 @@ type action =
  | Write_reg of reg_form * option (nat* nat) * value
  | Read_mem of id * value * option (nat * nat)
  | Write_mem of id * value * option (nat * nat) * value
+ | Call_extern of string * value
 
 (* Inverted call stack, where top item on the stack is waiting for an action and all other frames for the right stack *)
 type stack = 
@@ -83,6 +84,7 @@ let rec has_memory_effect efcts =
     end 
   end
 
+(*Look for externs as well*)
 val to_memory_ops : defs -> list (id * typ)
 let rec to_memory_ops (Defs defs) =
   match defs with
@@ -97,6 +99,20 @@ let rec to_memory_ops (Defs defs) =
     | _ -> to_memory_ops (Defs defs) end
   end
 
+val to_externs : defs -> list (id * string)
+let rec to_externs (Defs defs) =
+  match defs with
+  | [] -> []
+  | def ::defs ->
+    match def with
+    | DEF_spec valsp ->
+      match valsp with
+      | VS_extern_spec (TypSchm_ts tq ((Typ_fn a r e) as t)) 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)
 let rec to_data_constructors (Defs defs) =
   match defs with
@@ -274,6 +290,12 @@ let rec find_memory mems id =
   | (id',t)::mems -> if id'=id then Some t else find_memory mems id
   end
 
+let rec find_extern externs id =
+  match externs with
+  | [] -> None
+  | (id',s)::externs -> if id'=id then Some s else find_extern externs id
+  end
+
 val match_pattern : pat -> value -> bool * list (id * value)
 let rec match_pattern p value =
   match p with 
@@ -406,8 +428,8 @@ let rec find_case pexps value =
     if is_matching then Some(env,e) else find_case pexps value
   end
 
-(*top_level is a three tuple of (all definitions, declared registers, memory functions (typ expected to be num -> num -> a), and Typedef union constructors) *)
-type top_level = defs * list (id*reg_form) * list (id * typ) * list (id * typ)
+(*top_level is a three tuple of (all definitions, external funcitons, declared registers, memory functions (typ expected to be num -> num -> a), and Typedef union constructors) *)
+type top_level = defs * list (id * string) * 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)
@@ -441,7 +463,7 @@ and interp_main t_level l_env l_mem exp =
 		                  | V_boxref n ->(Value (in_mem l_mem n),l_mem,l_env)
 		                  | _ -> (Value value,l_mem,l_env) end
 		 | None -> match t_level with
-		           | (defs,regs,mems,ctors) ->
+		           | (defs,externs,regs,mems,ctors) ->
 			     match in_reg regs id with
 			     | Some(regf) -> 
 			       (Action (Read_reg regf None) (Frame (Id "0") (E_id (Id "0")) l_env l_mem Top), l_mem, l_env) 
@@ -614,7 +636,7 @@ and interp_main t_level l_env l_mem exp =
     | E_block(exps) -> interp_block t_level l_env l_env l_mem exps
     | E_app f args ->
       match (f,t_level) with
-      | (E_id(id),(defs,regs,mems,ctors)) -> 
+      | (E_id(id),(defs,externs,regs,mems,ctors)) -> 
 	(match find_function defs id with
 	| Some(funcls) -> 
           resolve_outcome (interp_main t_level l_env l_mem (List.hd args))
@@ -641,8 +663,14 @@ and interp_main t_level l_env l_mem exp =
               resolve_outcome (interp_main t_level l_env l_mem (List.hd args))
                 (fun argv lm le -> (Action (Read_mem id argv None) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le))
                 (fun a -> update_stack a (add_to_top_frame (fun a -> (E_app f [a]))))
-            | None -> (Error "Unknown function call",l_mem,l_env) end)                              
-	 end) end)
+            | None -> 
+              (match find_extern externs id with
+              | Some(str) ->
+                resolve_outcome (interp_main t_level l_env l_mem (List.hd args))
+                  (fun argv lm le -> (Action (Call_extern str argv) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le))
+                  (fun a -> update_stack a (add_to_top_frame (fun a -> (E_app f [a]))))
+              | None -> (Error "Unknown function call",l_mem,l_env) end)
+	     end) end) end)
       | _ -> (Error "Application with expression other than identifier",l_mem,l_env)
       end 
     | E_app_infix l op r -> 
@@ -651,9 +679,13 @@ and interp_main t_level l_env l_mem exp =
                          resolve_outcome (interp_main t_level l_env lm r)
                                          (fun rv lm le -> 
 			                   (match t_level with
-			                   | (defs,regs,mems,ctors) ->
+			                   | (defs,externs,regs,mems,ctors) ->
 				             (match find_function defs op with
-				             | None -> (Error "No matching pattern for function",lm,l_env)
+				             | None -> 
+                                               (match find_extern externs op with
+                                               | Some(str) ->
+                                                 (Action (Call_extern str (V_tuple [lv;rv])) (Frame (Id "0") (E_id (Id "0")) le lm Top),lm,le)
+                                               | None -> (Error "No matching function",lm,l_env) end)
 				             | Some (funcls) ->
 				               (match find_funcl funcls (V_tuple [lv;rv]) with 
 				               | None -> (Error "No matching pattern for function",lm,l_env)
@@ -694,7 +726,7 @@ and interp_main t_level l_env l_mem exp =
     end
 
 and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
-   let (defs,regs,mems,ctors) = t_level in
+   let (defs,externs,regs,mems,ctors) = t_level in
    match lexp with
     | LEXP_id id -> 
       match in_env l_env id with
@@ -798,6 +830,7 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
        match a with
        | Read_reg _ _ -> ((Action a s,lm,le), Some (fun e -> LEXP_field (lexp_builder e) id))
        | Read_mem _ _ _ -> ((Action a s,lm,le), Some (fun e -> LEXP_field (lexp_builder e) id))
+       | Call_extern _ _ -> ((Action a s,lm,le), Some (fun e -> LEXP_field (lexp_builder e) id))
        | _ -> ((Error "Unimplemented feature, writing to a field in a register or memory",lm,le),None)
        end 
      | e -> e end)
@@ -825,7 +858,7 @@ end
 
 
 let interp defs exp =
-  let t_level = (defs, to_registers defs,to_memory_ops defs,to_data_constructors defs) in 
+  let t_level = (defs, to_externs defs,to_registers defs,to_memory_ops defs,to_data_constructors defs) in 
   match interp_main t_level [] emem exp with
   | (o,_,_) -> o
   end
@@ -845,5 +878,5 @@ let rec resume_main t_level stack value =
   end
 
 let resume defs stack value =
-  let t_level = (defs, to_registers defs,to_memory_ops defs,to_data_constructors defs) in
+  let t_level = (defs, to_externs defs, to_registers defs,to_memory_ops defs,to_data_constructors defs) in
   resume_main t_level stack value 
diff --git a/src/parser.mly b/src/parser.mly
index a2257879..86da9a53 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -120,8 +120,8 @@ let star = "*"
 
 /*Terminals with no content*/
 
-%token And As Bits By Case Clause Const Default Dec Effect Effects End Enumerate Else False
-%token Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order Pure Rec Register
+%token And As Bits By Case Clause Const Default Dec Effect Effects End Enumerate Else Extern
+%token False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order Pure Rec Register
 %token Scattered Struct Switch Then True Type TYPE Typedef Undefined Union With Val
 
 /* Avoid shift/reduce conflict - see right_atomic_exp rule */
@@ -863,6 +863,10 @@ val_spec:
     { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4)) }
   | Val atomic_typ id
     { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3)) }
+  | Val Extern typquant atomic_typ id Eq String
+    { vloc (VS_extern_spec (mk_typschm $3 $4 3 4,$5,$7)) }
+  | Val Extern atomic_typ id Eq String
+    { vloc (VS_extern_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, $6)) }
 
 kinded_id:
   | id
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index c85cafb3..55d09dcb 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -262,8 +262,10 @@ let pp_default ppf (DT_aux(df,_)) =
   | DT_kind(bk,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_bkind bk pp_id id
   | DT_typ(ts,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_typscm ts pp_id id
 
-let pp_spec ppf (VS_aux(VS_val_spec(ts,id),_)) =
-  fprintf ppf "@[<0>%a %a %a@]@\n" kwd "val" pp_typscm ts pp_id id
+let pp_spec ppf (VS_aux(v,_)) =
+  match v with
+  | VS_val_spec(ts,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "val" pp_typscm ts pp_id id
+  | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>%a %a %a %a %a \"%s\"@]@\n" kwd "val" kwd "extern" pp_typscm ts pp_id id kwd "=" s
 
 let pp_namescm ppf (Name_sect_aux(ns,_)) =
   match ns with
@@ -556,8 +558,10 @@ let pp_lem_default ppf (DT_aux(df,_)) =
   | DT_kind(bk,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_id id
   | 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(VS_val_spec(ts,id),_)) =
-  fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" 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
 
 let pp_lem_namescm ppf (Name_sect_aux(ns,_)) =
   match ns with