separate use/clone from other decl for incrmental typing

Makefile.in

@@ -441,7 +441,7 @@ install_local: bin/why3ml
 # Whyml (new API)
 ########
 
-MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_module
+MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_module mlw_typing mlw_main
 
 MLWMODULES = $(addprefix src/whyml/, $(MLW_FILES))
 

src/parser/parser.mly

@@ -57,8 +57,11 @@ module Incremental = struct
     ref_set uc_ref (Typing.close_namespace loc import name (ref_get uc_ref))
 
   let new_decl d =
+    ref_set uc_ref (Typing.add_decl (ref_get uc_ref) d)
+
+  let new_use_clone d =
     let env = ref_get env_ref in let lenv = ref_get lenv_ref in
-    ref_set uc_ref (Typing.add_decl env lenv (ref_get uc_ref) d)
+    ref_set uc_ref (Typing.add_use_clone env lenv (ref_get uc_ref) d)
 end
 
   open Ptree
@@ -297,6 +300,8 @@ list0_decl:
 new_decl:
 | decl
    { Incremental.new_decl $1 }
+| use_clone
+   { Incremental.new_use_clone $1 }
 | namespace_head namespace_import namespace_name list0_decl END
    { Incremental.close_namespace (floc_i 3) $2 $3 }
 ;
@@ -334,16 +339,19 @@ decl:
     { PropDecl (floc (), Klemma, add_lab $2 $3, $5) }
 | GOAL ident labels COLON lexpr
     { PropDecl (floc (), Kgoal, add_lab $2 $3, $5) }
-| USE use
-    { UseClone (floc (), $2, None) }
-| CLONE use clone_subst
-    { UseClone (floc (), $2, Some $3) }
 | META sident list1_meta_arg_sep_comma
     { Meta (floc (), $2, $3) }
 ;
 
 /* Use and clone */
 
+use_clone:
+| USE use
+    { (floc (), $2, None) }
+| CLONE use clone_subst
+    { (floc (), $2, Some $3) }
+;
+
 use:
 | imp_exp tqualid
     { { use_theory = $2; use_as = None; use_imp_exp = $1 } }
@@ -987,10 +995,12 @@ list1_full_decl:
 ;
 
 full_decl:
-| NAMESPACE namespace_import namespace_name list0_full_decl END
-   { Dnamespace (floc_i 3, $3, $2, $4) }
 | decl
    { Dlogic $1 }
+| use_clone
+   { Duseclone $1 }
+| NAMESPACE namespace_import namespace_name list0_full_decl END
+   { Dnamespace (floc_i 3, $3, $2, $4) }
 ;
 
 list0_program_decl:
@@ -1010,6 +1020,8 @@ list1_program_decl:
 program_decl:
 | decl
     { Dlogic $1 }
+| use_clone
+    { Duseclone $1 }
 | LET lident_rich_pgm labels list1_type_v_binder opt_cast EQUAL triple
     { Dlet (add_lab $2 $3, mk_expr_i 7 (Efun ($4, cast_body $5 $7))) }
 | LET lident_rich_pgm labels EQUAL FUN list1_type_v_binder ARROW triple

src/parser/ptree.ml

@@ -153,15 +153,15 @@ type metarg =
   | PMAstr of string
   | PMAint of int
 
+type use_clone = loc * use * clone_subst list option
+
 type decl =
   | TypeDecl of type_decl list
   | LogicDecl of logic_decl list
   | IndDecl of ind_decl list
   | PropDecl of loc * prop_kind * ident * lexpr
-  | UseClone of loc * use * clone_subst list option
   | Meta of loc * ident * metarg list
 
-
 (* program files *)
 
 type assertion_kind = Aassert | Aassume | Acheck
@@ -242,6 +242,7 @@ type program_decl =
   | Dlet    of ident * expr
   | Dletrec of (ident * binder list * variant option * triple) list
   | Dlogic  of decl
+  | Duseclone of use_clone
   | Dparam  of ident * type_v
   | Dexn    of ident * pty option
   (* modules *)

src/parser/typing.ml

@@ -1109,7 +1109,7 @@ let rec clone_ns loc sl ns2 ns1 s =
   in
   { s with inst_ts = inst_ts; inst_ls = inst_ls }
 
-let add_decl env lenv th = function
+let add_decl th = function
   | TypeDecl dl ->
       add_types dl th
   | LogicDecl dl ->
@@ -1118,76 +1118,6 @@ let add_decl env lenv th = function
       add_inductives dl th
   | PropDecl (loc, k, s, f) ->
       add_prop (prop_kind k) loc s f th
-  | UseClone (loc, use, subst) ->
-      let q, id = split_qualid use.use_theory in
-      let t =
-        try
-          find_theory env lenv q id
-        with
-          | TheoryNotFound _ -> error ~loc (UnboundTheory use.use_theory)
-      in
-      let use_or_clone th = match subst with
-        | None ->
-            use_export th t
-        | Some s ->
-            let add_inst s = function
-              | CSns (p,q) ->
-                  let find ns x = find_namespace_ns x ns in
-                  let ns1 = option_fold find t.th_export p in
-                  let ns2 = option_fold find (get_namespace th) q in
-                  clone_ns loc t.th_local ns2 ns1 s
-              | CStsym (p,q) ->
-                  let ts1 = find_tysymbol_ns p t.th_export in
-                  let ts2 = find_tysymbol q th in
-                  if Mts.mem ts1 s.inst_ts
-                  then error ~loc (Clash ts1.ts_name.id_string);
-                  { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
-              | CSfsym (p,q) ->
-                  let ls1 = find_fsymbol_ns p t.th_export in
-                  let ls2 = find_fsymbol q th in
-                  if Mls.mem ls1 s.inst_ls
-                  then error ~loc (Clash ls1.ls_name.id_string);
-                  { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
-              | CSpsym (p,q) ->
-                  let ls1 = find_psymbol_ns p t.th_export in
-                  let ls2 = find_psymbol q th in
-                  if Mls.mem ls1 s.inst_ls
-                  then error ~loc (Clash ls1.ls_name.id_string);
-                  { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
-              | CSlemma p ->
-                  let pr = find_prop_ns p t.th_export in
-                  if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
-                  then error ~loc (Clash pr.pr_name.id_string);
-                  { s with inst_lemma = Spr.add pr s.inst_lemma }
-              | CSgoal p ->
-                  let pr = find_prop_ns p t.th_export in
-                  if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
-                  then error ~loc (Clash pr.pr_name.id_string);
-                  { s with inst_goal = Spr.add pr s.inst_goal }
-            in
-            let s = List.fold_left add_inst empty_inst s in
-            clone_export th t s
-      in
-      let n = match use.use_as with
-        | None -> Some t.th_name.id_string
-        | Some (Some x) -> Some x.id
-        | Some None -> None
-      in
-      begin try match use.use_imp_exp with
-        | Nothing ->
-            (* use T = namespace T use_export T end *)
-            let th = open_namespace th in
-            let th = use_or_clone th in
-            close_namespace th false n
-        | Import ->
-            (* use import T = namespace T use_export T end import T *)
-            let th = open_namespace th in
-            let th = use_or_clone th in
-            close_namespace th true n
-        | Export ->
-            use_or_clone th
-      with ClashSymbol s -> error ~loc (Clash s)
-      end
   | Meta (loc, id, al) ->
       let s = id.id in
       let convert = function
@@ -1202,9 +1132,80 @@ let add_decl env lenv th = function
       begin try add_meta th (lookup_meta s) al
       with e -> raise (Loc.Located (loc,e)) end
 
-let add_decl env lenv th d =
+let add_decl th d =
+  if Debug.test_flag debug_parse_only then th else add_decl th d
+
+let add_use_clone env lenv th (loc, use, subst) =
   if Debug.test_flag debug_parse_only then th else
-  add_decl env lenv th d
+  let q, id = split_qualid use.use_theory in
+  let t =
+    try
+      find_theory env lenv q id
+    with
+      | TheoryNotFound _ -> error ~loc (UnboundTheory use.use_theory)
+  in
+  let use_or_clone th = match subst with
+    | None ->
+      use_export th t
+    | Some s ->
+      let add_inst s = function
+        | CSns (p,q) ->
+          let find ns x = find_namespace_ns x ns in
+          let ns1 = option_fold find t.th_export p in
+          let ns2 = option_fold find (get_namespace th) q in
+          clone_ns loc t.th_local ns2 ns1 s
+        | CStsym (p,q) ->
+          let ts1 = find_tysymbol_ns p t.th_export in
+          let ts2 = find_tysymbol q th in
+          if Mts.mem ts1 s.inst_ts
+          then error ~loc (Clash ts1.ts_name.id_string);
+          { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
+        | CSfsym (p,q) ->
+          let ls1 = find_fsymbol_ns p t.th_export in
+          let ls2 = find_fsymbol q th in
+          if Mls.mem ls1 s.inst_ls
+          then error ~loc (Clash ls1.ls_name.id_string);
+          { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
+        | CSpsym (p,q) ->
+          let ls1 = find_psymbol_ns p t.th_export in
+          let ls2 = find_psymbol q th in
+          if Mls.mem ls1 s.inst_ls
+          then error ~loc (Clash ls1.ls_name.id_string);
+          { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
+        | CSlemma p ->
+          let pr = find_prop_ns p t.th_export in
+          if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
+          then error ~loc (Clash pr.pr_name.id_string);
+          { s with inst_lemma = Spr.add pr s.inst_lemma }
+        | CSgoal p ->
+          let pr = find_prop_ns p t.th_export in
+          if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
+          then error ~loc (Clash pr.pr_name.id_string);
+          { s with inst_goal = Spr.add pr s.inst_goal }
+      in
+      let s = List.fold_left add_inst empty_inst s in
+      clone_export th t s
+  in
+  let n = match use.use_as with
+    | None -> Some t.th_name.id_string
+    | Some (Some x) -> Some x.id
+    | Some None -> None
+  in
+  begin try match use.use_imp_exp with
+    | Nothing ->
+            (* use T = namespace T use_export T end *)
+      let th = open_namespace th in
+      let th = use_or_clone th in
+      close_namespace th false n
+    | Import ->
+            (* use import T = namespace T use_export T end import T *)
+      let th = open_namespace th in
+      let th = use_or_clone th in
+      close_namespace th true n
+    | Export ->
+      use_or_clone th
+    with ClashSymbol s -> error ~loc (Clash s)
+  end
 
 let close_theory loc lenv th =
   if Debug.test_flag debug_parse_only then lenv else

src/parser/typing.mli

@@ -29,8 +29,10 @@ val debug_type_only : Debug.flag
 
 (** incremental parsing *)
 
-val add_decl :
-  unit Env.library -> theory Mstr.t -> theory_uc -> Ptree.decl -> theory_uc
+val add_decl : theory_uc -> Ptree.decl -> theory_uc
+
+val add_use_clone :
+  unit Env.library -> theory Mstr.t -> theory_uc -> Ptree.use_clone -> theory_uc
 
 val close_namespace :
   Loc.position -> bool -> Ptree.ident option -> theory_uc -> theory_uc

src/programs/pgm_main.ml

@@ -43,7 +43,9 @@ let add_theory env path lenv m =
   let th = Theory.create_theory ~path (Denv.create_user_id id) in
   let rec add_decl th = function
     | Dlogic d ->
-        Typing.add_decl env lenv th d
+        Typing.add_decl th d
+    | Duseclone d ->
+        Typing.add_use_clone env lenv th d
     | Dnamespace (loc, name, import, dl) ->
         let th = Theory.open_namespace th in
         let th = List.fold_left add_decl th dl in

src/programs/pgm_module.ml

@@ -271,24 +271,21 @@ let create_module ?(path=[]) id =
   let uc = empty_module path id in
   use_export_theory uc th_prelude
 
-let add_impure_pdecl env ltm d uc =
-  let env = Lexer.library_of_env (Env.env_of_library env) in
-  { uc with uc_impure = Typing.add_decl env ltm uc.uc_impure d }
+let add_impure_pdecl d uc =
+  { uc with uc_impure = Typing.add_decl uc.uc_impure d }
 
-let add_effect_pdecl env ltm d uc =
-  let env = Lexer.library_of_env (Env.env_of_library env) in
-  { uc with uc_effect = Typing.add_decl env ltm uc.uc_effect d; }
+let add_effect_pdecl d uc =
+  { uc with uc_effect = Typing.add_decl uc.uc_effect d; }
 
-let add_pure_pdecl env ltm d uc =
-  let env = Lexer.library_of_env (Env.env_of_library env) in
-  { uc with uc_pure = Typing.add_decl env ltm uc.uc_pure d; }
+let add_pure_pdecl d uc =
+  { uc with uc_pure = Typing.add_decl uc.uc_pure d; }
 
-let add_pdecl env ltm d uc =
+let add_use_clone env ltm d uc =
   let env = Lexer.library_of_env (Env.env_of_library env) in
   { uc with
-      uc_impure = Typing.add_decl env ltm uc.uc_impure d;
-      uc_effect = Typing.add_decl env ltm uc.uc_effect d;
-      uc_pure   = Typing.add_decl env ltm uc.uc_pure   d; }
+      uc_impure = Typing.add_use_clone env ltm uc.uc_impure d;
+      uc_effect = Typing.add_use_clone env ltm uc.uc_effect d;
+      uc_pure   = Typing.add_use_clone env ltm uc.uc_pure   d; }
 
 (*
 Local Variables:

src/programs/pgm_module.mli

@@ -74,15 +74,12 @@ val add_impure_decl : Decl.decl -> uc -> uc
 val add_effect_decl : Decl.decl -> uc -> uc
 val add_pure_decl : Decl.decl -> uc -> uc
 
-val add_impure_pdecl :
-  t Mstr.t Env.library -> Theory.theory Mstr.t -> Ptree.decl -> uc -> uc
-val add_effect_pdecl :
-  t Mstr.t Env.library -> Theory.theory Mstr.t -> Ptree.decl -> uc -> uc
-val add_pure_pdecl :
-  t Mstr.t Env.library -> Theory.theory Mstr.t -> Ptree.decl -> uc -> uc
-
-val add_pdecl :
-  t Mstr.t Env.library -> Theory.theory Mstr.t -> Ptree.decl -> uc -> uc
+val add_impure_pdecl : Ptree.decl -> uc -> uc
+val add_effect_pdecl : Ptree.decl -> uc -> uc
+val add_pure_pdecl : Ptree.decl -> uc -> uc
+
+val add_use_clone :
+  t Mstr.t Env.library -> Theory.theory Mstr.t -> Ptree.use_clone -> uc -> uc
   (** add in impure, effect and pure *)
 
 (** builtins *)

src/programs/pgm_typing.ml

@@ -2012,10 +2012,10 @@ let add_logic_ps ?(nofail=false) uc x =
     (* can fail if x is a constructor of a model type (record or algebraic) *)
     assert nofail
 
-let add_types env ltm uc dl =
+let add_types uc dl =
   (* 1. type check the pure def, to have all sanity checks performed *)
   let dlp = List.map make_immutable_type dl in
-  let uc = Pgm_module.add_pure_pdecl env ltm (TypeDecl dlp) uc in
+  let uc = Pgm_module.add_pure_pdecl (TypeDecl dlp) uc in
   (* 2. compute number of regions for each type *)
   let def = List.fold_left
     (fun def d -> Mstr.add d.td_ident.id d def) Mstr.empty dl
@@ -2132,9 +2132,9 @@ let add_types env ltm uc dl =
     { d with td_params = params; td_model = false; td_def = def }
   in
   let dli = List.map (add_regions ~effect:false) dl in
-  let uc = Pgm_module.add_impure_pdecl env ltm (Ptree.TypeDecl dli) uc in
+  let uc = Pgm_module.add_impure_pdecl (Ptree.TypeDecl dli) uc in
   let dle = List.map (add_regions ~effect:true) dl in
-  let uc = Pgm_module.add_effect_pdecl env ltm (Ptree.TypeDecl dle) uc in
+  let uc = Pgm_module.add_effect_pdecl (Ptree.TypeDecl dle) uc in
   (* 4. add mtsymbols in module *)
   let add_mt d =
     let x = d.td_ident.id in
@@ -2212,8 +2212,8 @@ let add_types env ltm uc dl =
   List.iter (fun d -> visit d.td_ident.id) dl;
   uc
 
-let add_logics env ltm uc d =
-  let uc = Pgm_module.add_pure_pdecl env ltm d uc in
+let add_logics uc d =
+  let uc = Pgm_module.add_pure_pdecl d uc in
   let region =
     let c = ref (-1) in
     fun loc ->
@@ -2242,8 +2242,8 @@ let add_logics env ltm uc d =
   in
   let add uc d0 =
     let d = LogicDecl [add_regions d0] in
-    let uc = Pgm_module.add_impure_pdecl env ltm d uc in
-    let uc = Pgm_module.add_effect_pdecl env ltm d uc in
+    let uc = Pgm_module.add_impure_pdecl d uc in
+    let uc = Pgm_module.add_effect_pdecl d uc in
     add_logic_ps uc d0.ld_ident.id;
     uc
   in
@@ -2254,7 +2254,7 @@ let add_logics env ltm uc d =
   match d with
     | LogicDecl dl -> List.fold_left add uc dl
     | IndDecl dl -> List.fold_left addi uc dl
-    | Meta _ | UseClone _ | PropDecl _ | TypeDecl _ -> assert false
+    | Meta _ | PropDecl _ | TypeDecl _ -> assert false
 
 let find_module penv lmod q id = match q with
   | [] ->
@@ -2373,13 +2373,13 @@ let rec decl ~wp env ltm lmod uc = function
       begin try close_namespace uc import id
       with ClashSymbol s -> errorm ~loc "clash with previous symbol %s" s end
   | Ptree.Dlogic (TypeDecl d) ->
-      add_types env ltm uc d
+      add_types uc d
   | Ptree.Dlogic (LogicDecl _ | IndDecl _ as d) ->
-      add_logics env ltm uc d
+      add_logics uc d
   | Ptree.Dlogic (PropDecl _ | Meta _ as d) ->
-      Pgm_module.add_pure_pdecl env ltm d uc
-  | Ptree.Dlogic (UseClone _ as d) ->
-      Pgm_module.add_pdecl env ltm d uc
+      Pgm_module.add_pure_pdecl d uc
+  | Ptree.Duseclone d ->
+      Pgm_module.add_use_clone env ltm d uc
 
 (*
 Local Variables:

src/whyml/mlw_main.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2011                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Why3
+open Util
+open Mlw_typing
+
+let read_channel env path file c =
+  let lb = Lexing.from_channel c in
+  Loc.set_file file lb;
+  let ml = Lexer.parse_program_file lb in
+  if Debug.test_flag Typing.debug_parse_only then
+    Mstr.empty, Mstr.empty
+  else
+    List.fold_left (add_theory_module env path) (Mstr.empty, Mstr.empty) ml
+
+let library_of_env = Env.register_format "whyml-exp" ["mlx"] read_channel

src/whyml/mlw_typing.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2011                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Why3
+open Util
+open Theory
+open Env
+open Ptree
+open Mlw_module
+
+type mlw_contents = modul Mstr.t
+type mlw_library = mlw_contents library
+type mlw_file = mlw_contents * Theory.theory Mstr.t
+
+    (* let type_only = Debug.test_flag Typing.debug_type_only in *)
+
+let add_theory _lib path mt m =
+  let id = m.pth_name in
+  let loc = id.id_loc in
+  let uc = Theory.create_theory ~path (Denv.create_user_id id) in
+  let rec add_decl uc = function
+    | Duseclone (_loc, _use, None) (* use *) ->
+        assert false (*TODO*)
+    | Duseclone (_loc, _use, Some _s) (* clone *) ->
+       assert false (*TODO*)
+    | Dlogic d ->
+        Typing.add_decl uc d
+    | Dnamespace (loc, name, import, dl) ->
+        let uc = Theory.open_namespace uc in
+        let uc = List.fold_left add_decl uc dl in
+        Typing.close_namespace loc import name uc
+    | Dlet _ | Dletrec _ | Dparam _ | Dexn _ | Duse _ ->
+        assert false
+  in
+  let uc = List.fold_left add_decl uc m.pth_decl in
+  Typing.close_theory loc mt uc
+
+let add_theory_module lib path (mm, mt) = function
+  | Ptheory th -> mm, add_theory lib path mt th
+  | Pmodule _m -> assert false (*TODO*)
+

src/whyml/mlw_typing.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2011                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Why3
+open Util
+open Theory
+open Env
+open Ptree
+open Mlw_module
+
+type mlw_contents = modul Mstr.t
+type mlw_library = mlw_contents library
+type mlw_file = mlw_contents * Theory.theory Mstr.t
+
+val add_theory_module:
+  mlw_library -> pathname -> mlw_file -> theory_module -> mlw_file
+