logic

src/core/theory.ml

@@ -244,22 +244,26 @@ let add_type uc (ty, def) = match def with
   | Ty_algebraic _ ->
       assert false (*TODO*)
 
+let add_logic uc = function
+  | Lfunction (fs, _) ->
+      let uc = add_param fs.fs_name uc in
+      add_symbol add_fsymbol fs.fs_name fs uc
+  | Lpredicate (ps, _) ->
+      let uc = add_param ps.ps_name uc in
+      add_symbol add_psymbol ps.ps_name ps uc
+  | Linductive _ ->
+      assert false (*TODO*)
+
 let add_decl uc d = 
   let uc = match d with
     | Dtype dl ->
 	List.fold_left add_type uc dl
-    | Dlogic [Lfunction (fs, None)] ->
-        let uc = add_param fs.fs_name uc in
-        add_symbol add_fsymbol fs.fs_name fs uc
-    | Dlogic [Lpredicate (ps, None)] ->
-        let uc = add_param ps.ps_name uc in
-        add_symbol add_psymbol ps.ps_name ps uc
+    | Dlogic dl ->
+	List.fold_left add_logic uc dl
     | Dprop (k, id, f) ->
 	check_fmla uc.uc_known f;
 	let uc = add_known id uc in
 	add_symbol add_prop id f uc
-    | _ ->
-        assert false (* TODO *)
   in
   { uc with uc_decls = (Decl d) :: uc.uc_decls }
 

src/parser/ptree.mli

@@ -71,14 +71,14 @@ and pp_desc =
 
 type plogic_type =
   | PPredicate of pty list
-  | PFunction of pty list * pty
+  | PFunction  of pty list * pty
 
 type imp_exp =
   | Import | Export | Nothing
 
 type use = {
-  use_theory : qualid;
-  use_as : ident option;
+  use_theory  : qualid;
+  use_as      : ident option;
   use_imp_exp : imp_exp;
 }
 
@@ -86,30 +86,28 @@ type param = ident option * pty
 
 type type_def = 
   | TDabstract
-  | TDalias of pty
+  | TDalias     of pty
   | TDalgebraic of (loc * ident * param list) list
 
 type type_decl = {
-  td_loc : loc;
-  td_ident : ident;
+  td_loc    : loc;
+  td_ident  : ident;
   td_params : ident list;
-  td_def : type_def;
+  td_def    : type_def;
 }
 
 type logic_decl = { 
-  ld_loc : loc;
-  ld_ident : ident;
+  ld_loc    : loc;
+  ld_ident  : ident;
   ld_params : param list;
-  ld_type : pty option;
-  ld_def : lexpr option;
+  ld_type   : pty option;
+  ld_def    : lexpr option;
 }
 
 type decl = 
   | TypeDecl of loc * type_decl list
   | Logic of loc * logic_decl list
   | Inductive_def of loc * ident * plogic_type * (loc * ident * lexpr) list
-(*   | Function_def of loc * ident * (loc * ident * pty) list * pty * lexpr *)
-(*   | Predicate_def of loc * ident * (loc * ident * pty) list * lexpr *)
   | Axiom of loc * ident * lexpr
   | Goal of loc * ident * lexpr
   | Use of loc * use

src/parser/typing.ml

@@ -561,16 +561,85 @@ let add_predicate loc pl th {id=id} =
   let s = create_psymbol v pl in
   add_decl th (Dlogic [Lpredicate (s, None)])
 
-let fmla env f =
-  let denv = create_denv env in
-  let f = dfmla denv f in
-  fmla M.empty f
+let env_of_vsymbol_list vl =
+  List.fold_left (fun env v -> M.add v.vs_name.id_short v env) M.empty vl
+
+let add_logics loc dl th =
+  let fsymbols = Hashtbl.create 17 in
+  let psymbols = Hashtbl.create 17 in
+  (* 1. create all symbols and make an environment with these symbols *)
+  let create_symbol th d = 
+    let id = d.ld_ident.id in
+    let v = id_user id id loc in
+    let denv = create_denv th in
+    let type_ty (_,t) = ty (dty denv t) in
+    let pl = List.map type_ty d.ld_params in
+    match d.ld_type with
+      | None -> (* predicate *)
+	  let ps = create_psymbol v pl in
+	  Hashtbl.add psymbols id ps;
+	  add_decl th (Dlogic [Lpredicate (ps, None)])
+      | Some t -> (* function *)
+	  let t = type_ty (None, t) in
+	  let fs = create_fsymbol v (pl, t) false in
+	  Hashtbl.add fsymbols id fs;
+	  add_decl th (Dlogic [Lfunction (fs, None)])
+  in
+  let th' = List.fold_left create_symbol th dl in
+  (* 2. then type-check all definitions *)
+  let type_decl d = 
+    let id = d.ld_ident.id in
+    let dadd_var denv (x, ty) = match x with
+      | None -> denv
+      | Some id -> { denv with dvars = M.add id.id (dty denv ty) denv.dvars }
+    in
+    let denv = List.fold_left dadd_var (create_denv th') d.ld_params in
+    let create_var (x, _) ty = 
+      let id = match x with 
+	| None -> id_fresh "%x" "%x"
+	| Some id -> id_user id.id id.id id.id_loc
+      in
+      create_vsymbol id ty
+    in
+    match d.ld_type with
+    | None -> (* predicate *)
+	let ps = Hashtbl.find psymbols id in
+	let def = match d.ld_def with
+	  | None -> 
+	      None
+	  | Some f -> 
+	      let f = dfmla denv f in
+	      let vl = List.map2 create_var d.ld_params ps.ps_scheme in
+	      let env = env_of_vsymbol_list vl in
+	      Some (vl, fmla env f)
+	in
+	Lpredicate (ps, def)
+    | Some t -> (* function *)
+	let fs = Hashtbl.find fsymbols id in
+	let def = match d.ld_def with
+	  | None -> 
+	      None
+	  | Some t -> 
+	      let t = dterm denv t in
+	      let vl = List.map2 create_var d.ld_params (fst fs.fs_scheme) in
+	      let env = env_of_vsymbol_list vl in
+	      Some (vl, term env t)
+	in
+	Lfunction (fs, def)
+  in
+  let dl = List.map type_decl dl in
+  add_decl th (Dlogic dl)
 
 let term env t =
   let denv = create_denv env in
   let t = dterm denv t in
   term M.empty t
 
+let fmla env f =
+  let denv = create_denv env in
+  let f = dfmla denv f in
+  fmla M.empty f
+
 let add_prop k loc s f th =
   let f = fmla th f in
   try
@@ -663,10 +732,8 @@ and add_decls env th = List.fold_left (add_decl env) th
 and add_decl env th = function
   | TypeDecl (loc, dl) ->
       add_types loc dl th
-(*   | Logic (loc, ids, PPredicate pl) -> *)
-(*       List.fold_left (add_predicate loc pl) th ids *)
-(*   | Logic (loc, ids, PFunction (pl, t)) -> *)
-(*       List.fold_left (add_function loc pl t) th ids *)
+  | Logic (loc, dl) ->
+      add_logics loc dl th
   | Axiom (loc, s, f) ->
       add_prop Theory.Axiom loc s f th
   | Use (loc, use) ->
@@ -714,6 +781,6 @@ let add_theories =
 
 (*
 Local Variables: 
-compile-command: "make -C .. test"
+compile-command: "make -C ../.. test"
 End: 
 *)

src/test.why

@@ -3,8 +3,13 @@
 
 theory A
   type 'a list
-  type t 
-  type u = t list
+  logic nil : 'a list
+  logic cons('a, 'a list) : 'a list
+
+  type t
+  logic p('a list)
+  logic is_nil(x: 'a list) = p(x)
+  logic c : t list
 end
 
 theory B