ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

extends Ptree/Typing API to the entire mlw file

Browse Source
This commit is contained in:
Rehan MALAK
2019-06-18 17:10:56 +02:00
parent b88f3d74de
commit 3d86e1c5f9
8 changed files with 335 additions and 221 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
Makefile.in
View File

@@ -1925,9 +1925,9 @@ OCAMLCODE_CALLPROVERS = proveranswer proverresult resourcelimit
OCAMLCODE_TRANSFORM = negate register
OCAMLCODE_MLWTREE = buildenv openmodule useimport \
source1 code1 helper1 source2 code2 source3 code3 \
closemodule checkingvcs
OCAMLCODE_MLWTREE = buildenv \
source1 code1 helper1 source2 code2 source3 code3 source4 code4 \
getmodules checkingvcs
OCAMLCODE_MLWEXPR = buildenv source2 code2_import code2 createmodule checkingvcs

51
doc/api.tex
View File

@@ -328,51 +328,50 @@ The examples of this section are available in the file
The first step is to build an environment as already illustrated in
Section~\ref{sec:api:callingprovers}, and open the OCaml module
\verb|Ptree| which contains most of the OCaml functions we need in
\verb|Ptree| (``parse tree'') which contains most of the OCaml functions we need in
this section.
\lstinputlisting{generated/mlw_tree__buildenv.ml}
To contain all the example programs we are going to build we need a
module. We start the creation of that module using the following
declarations, that first introduces a pseudo ``file'' to hold the
module, then the module itself called \verb|Program|.
\lstinputlisting{generated/mlw_tree__openmodule.ml}
Notice the use of a first
simple helper function \verb|mk_ident| to build an identifier without
any attributes nor any location.
To write our programs, we need to import some other modules from the
standard library. The following introduces two helper functions for
building qualified identifiers and importing modules, and finally
imports \verb|int.Int|.
\lstinputlisting{generated/mlw_tree__useimport.ml}
We want now to build a program equivalent to the following code in concrete Why3 syntax.
Each of our example programs will build a module.
Let's consider the Why3 code.
\lstinputlisting[language=why3]{generated/mlw_tree__source1.ml}
The OCaml code that programmatically build this Why3 function is as follows.
The Ocaml code that programmatically builds it is as follows.
\lstinputlisting{generated/mlw_tree__code1.ml}
This code makes uses of helper functions that are given in Figure~\ref{fig:helpers}.
Most of the code is not using directly the \verb|Ptree| constructors
but instead makes uses of the helper
functions that are given in Figure~\ref{fig:helpers}.
Notice \verb|mk_ident| which builds an identifier (\verb|Ptree.ident|) without
any attributes nor any location and \verb|use_import| which lets us to import
some other modules and in particular the ones from the standard library. At the end,
our module is no more than the identifier and a list of two declarations (\verb|Ptree.decl list|)
\begin{figure}[t]
\lstinputlisting{generated/mlw_tree__helper1.ml}
\caption{Helper functions for building WhyML programs}
\label{fig:helpers}
\end{figure}
We want now to build a program equivalent to the following code in concrete Why3 syntax.
\lstinputlisting[language=why3]{generated/mlw_tree__source2.ml}
We need to import the \verb|ref.Ref| module first. The rest is similar to the first example, the code is as follows
The OCaml code that programmatically build this Why3 function is as follows.
\lstinputlisting{generated/mlw_tree__code2.ml}
The next example makes use of arrays.
We want now to build a program equivalent to the following code in concrete Why3 syntax.
\lstinputlisting[language=why3]{generated/mlw_tree__source3.ml}
The corresponding OCaml code is as follows
We need to import the \verb|ref.Ref| module first. The rest is similar to the first example, the code is as follows
\lstinputlisting{generated/mlw_tree__code3.ml}
Having declared all the programs we wanted to write, we can now close
the module and the file, and get as a result the set of modules of our
The next example makes use of arrays.
\lstinputlisting[language=why3]{generated/mlw_tree__source4.ml}
The corresponding OCaml code is as follows
\lstinputlisting{generated/mlw_tree__code4.ml}
Having declared all the modules we wanted to write, we can now call the \why typing procedure
and get as a result the set of modules of our
file, under the form of a map of module names to modules.
\lstinputlisting{generated/mlw_tree__closemodule.ml}
\lstinputlisting{generated/mlw_tree__getmodules.ml}
We can then construct the proofs tasks for our module, and then try to
call the Alt-Ergo prover. The rest of that code is using OCaml

372
examples/use_api/mlw_tree.ml
View File

@@ -24,19 +24,10 @@ let env : Env.env = Env.create_env (Whyconf.loadpath main)
open Ptree
(* END{buildenv} *)
(* start a module *)
(* BEGIN{openmodule} *)
let () = Typing.open_file env [] (* empty pathname *)
(* BEGIN{helper1} *)
let mk_ident s = { id_str = s; id_ats = []; id_loc = Loc.dummy_position }
let () = Typing.open_module (mk_ident "Program")
(* END{openmodule} *)
(* use int.Int *)
(* BEGIN{useimport} *)
let mk_qid l =
let mk_qualid l =
let rec aux l =
match l with
| [] -> assert false
@@ -45,17 +36,10 @@ let mk_qid l =
in
aux (List.rev l)
let use_import (f, m) =
let m = mk_ident m in
let loc = Loc.dummy_position in
Typing.open_scope loc m;
Typing.add_decl loc (Ptree.Duse (Qdot (Qident (mk_ident f), m)));
Typing.close_scope loc ~import:true
let use_import l =
let qid_id_opt = (mk_qualid l, None) in
Duseimport(Loc.dummy_position,false,[qid_id_opt])
let use_int_Int = use_import ("int","Int")
(* END{useimport} *)
(* BEGIN{helper1} *)
let mk_expr e = { expr_desc = e; expr_loc = Loc.dummy_position }
let mk_term t = { term_desc = t; term_loc = Loc.dummy_position }
@@ -84,162 +68,236 @@ let mk_evar x = mk_expr(Eident(Qident x))
(* declaration of
BEGIN{source1}
let f1 (x:int) : unit
requires { x=6 }
ensures { result=42 }
= x*7
module M1
use int.Int
goal g : 2 + 2 = 4
end
END{source1}
*)
(* BEGIN{code1} *)
let eq_symb = mk_qid [Ident.op_infix "="]
let int_type_id = mk_qid ["int"]
let int_type = PTtyapp(int_type_id,[])
let mul_int = mk_qid ["Int";Ident.op_infix "*"]
let d1 : decl =
let id_x = mk_ident "x" in
let pre = mk_tapp eq_symb [mk_var id_x; mk_tconst 6] in
let result = mk_ident "result" in
let post = mk_tapp eq_symb [mk_var result; mk_tconst 42] in
let spec = {
sp_pre = [pre];
sp_post = [Loc.dummy_position,[pat_var result,post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
let mod_M1 =
(* use int.Int *)
let use_int_Int = use_import (["int";"Int"]) in
(* goal g : 2 + 2 = 4 *)
let g =
let two = mk_tconst 2 in
let four = mk_tconst 4 in
let add_int = mk_qualid ["Int";Ident.op_infix "+"] in
let two_plus_two = mk_tapp add_int [two ; two] in
let eq_int = mk_qualid ["Int";Ident.op_infix "="] in
let goal_term = mk_tapp eq_int [four ; two_plus_two] in
Dprop(Pgoal,mk_ident "g",goal_term)
in
let body = mk_eapp mul_int [mk_evar id_x; mk_econst 7] in
let f1 =
Efun(param1 id_x int_type, None, Ity.MaskVisible, spec, body)
in
Dlet(mk_ident "f1",false,Expr.RKnone, mk_expr f1)
let () =
try Typing.add_decl Loc.dummy_position d1
with e ->
Format.printf "Exception raised during typing of d:@ %a@."
Exn_printer.exn_printer e
(mk_ident "M1",[use_int_Int ; g])
(* END{code1} *)
(*
declaration of
BEGIN{source2}
let f2 () : int
requires { true }
ensures { result >= 0 }
= let x = ref 42 in !x
END{source2}
*)
(* declaration of
BEGIN{source2}
module M2
let f (x:int) : int
requires { x=6 }
ensures { result=42 }
= x*7
end
END{source2}
*)
(* BEGIN{code2} *)
let ge_int = mk_qid ["Int";Ident.op_infix ">="]
let eq_symb = mk_qualid [Ident.op_infix "="]
let int_type_id = mk_qualid ["int"]
let int_type = PTtyapp(int_type_id,[])
let mul_int = mk_qualid ["Int";Ident.op_infix "*"]
let use_ref_Ref = use_import ("ref","Ref")
let d2 =
let result = mk_ident "result" in
let post = mk_term(Tidapp(ge_int,[mk_var result;mk_tconst 0])) in
let spec = {
sp_pre = [];
sp_post = [Loc.dummy_position,[pat_var result,post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body =
let e1 = mk_eapp (mk_qid ["Ref";"ref"]) [mk_econst 42] in
let mod_M2 =
(* use int.Int *)
let use_int_Int = use_import (["int";"Int"]) in
(* f *)
let f =
let id_x = mk_ident "x" in
let e2 = mk_eapp (mk_qid ["Ref";Ident.op_prefix "!"]) [mk_evar id_x] in
mk_expr(Elet(id_x,false,Expr.RKlocal,e1,e2))
let pre = mk_tapp eq_symb [mk_var id_x; mk_tconst 6] in
let result = mk_ident "result" in
let post = mk_tapp eq_symb [mk_var result; mk_tconst 42] in
let spec = {
sp_pre = [pre];
sp_post = [Loc.dummy_position,[pat_var result,post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body = mk_eapp mul_int [mk_evar id_x; mk_econst 7] in
let f =
Efun(param1 id_x int_type, None, Ity.MaskVisible, spec, body)
in
Dlet(mk_ident "f",false,Expr.RKnone, mk_expr f)
in
let f = Efun(param0,None,Ity.MaskVisible,spec,body)
in
Dlet(mk_ident "f2",false,Expr.RKnone, mk_expr f)
let () =
try Typing.add_decl Loc.dummy_position d2
with e ->
Format.printf "Exception raised during typing of d2:@ %a@."
Exn_printer.exn_printer e
(mk_ident "M2",[use_int_Int ; f])
(* END{code2} *)
(*
BEGIN{source3}
let f (a:array int) : unit
requires { a.length >= 1 }
ensures { a[0] = 42 }
= a[0] <- 42
END{source3}
*)
(* declaration of
BEGIN{source3}
module M3
let f() : int
requires { true }
ensures { result >= 0 }
= let x = ref 42 in !x
end
END{source3}
*)
(* BEGIN{code3} *)
let () = use_import ("array","Array")
let ge_int = mk_qualid ["Int";Ident.op_infix ">="]
let array_int_type = PTtyapp(mk_qid ["Array";"array"],[int_type])
let length = mk_qid ["Array";"length"]
let array_get = mk_qid ["Array"; Ident.op_get ""]
let array_set = mk_qid ["Array"; Ident.op_set ""]
let d3 =
let id_a = mk_ident "a" in
let pre =
mk_tapp ge_int [mk_tapp length [mk_var id_a]; mk_tconst 1]
let mod_M3 =
(* use int.Int *)
let use_int_Int = use_import (["int";"Int"]) in
(* use ref.Ref *)
let use_ref_Ref = use_import (["ref";"Ref"]) in
(* f *)
let f =
let result = mk_ident "result" in
let post = mk_term(Tidapp(ge_int,[mk_var result;mk_tconst 0])) in
let spec = {
sp_pre = [];
sp_post = [Loc.dummy_position,[pat_var result,post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body =
let e1 = mk_eapp (mk_qualid ["Ref";"ref"]) [mk_econst 42] in
let id_x = mk_ident "x" in
let qid = mk_qualid ["Ref";Ident.op_prefix "!"] in
let e2 = mk_eapp qid [mk_evar id_x] in
mk_expr(Elet(id_x,false,Expr.RKnone,e1,e2))
in
let f = Efun(param0,None,Ity.MaskVisible,spec,body)
in
Dlet(mk_ident "f",false,Expr.RKnone, mk_expr f)
in
let post =
mk_tapp eq_symb [mk_tapp array_get [mk_var id_a; mk_tconst 0];
mk_tconst 42]
in
let spec = {
sp_pre = [pre];
sp_post = [Loc.dummy_position,[mk_pat Pwild,post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body =
mk_eapp array_set [mk_evar id_a; mk_econst 0; mk_econst 42]
in
let f = Efun(param1 id_a array_int_type,
None,Ity.MaskVisible,spec,body)
in
Dlet(mk_ident "f3", false, Expr.RKnone, mk_expr f)
let () =
try Typing.add_decl Loc.dummy_position d3
with e ->
Format.printf "Exception raised during typing of d3:@ %a@."
Exn_printer.exn_printer e
(mk_ident "M3",[use_int_Int ; use_ref_Ref ; f])
(* END{code3} *)
(* BEGIN{closemodule} *)
let () = Typing.close_module Loc.dummy_position
let mods : Pmodule.pmodule Wstdlib.Mstr.t = Typing.close_file ()
(* END{closemodule} *)
(* declaration of
BEGIN{source4}
module M4
let f (a:array int) : unit
requires { a.length >= 1 }
ensures { a[0] = 42 }
= a[0] <- 42
end
END{source4}
*)
(* BEGIN{code4} *)
let array_int_type = PTtyapp(mk_qualid ["Array";"array"],[int_type])
let length = mk_qualid ["Array";"length"]
let array_get = mk_qualid ["Array"; Ident.op_get ""]
let array_set = mk_qualid ["Array"; Ident.op_set ""]
let mod_M4 =
(* use int.Int *)
let use_int_Int = use_import (["int";"Int"]) in
(* use array.Array *)
let use_array_Array = use_import (["array";"Array"]) in
(* use f *)
let f =
let id_a = mk_ident "a" in
let pre =
mk_tapp ge_int [mk_tapp length [mk_var id_a]; mk_tconst 1]
in
let post =
mk_tapp eq_symb [mk_tapp array_get [mk_var id_a; mk_tconst 0];
mk_tconst 42]
in
let spec = {
sp_pre = [pre];
sp_post = [Loc.dummy_position,[mk_pat Pwild,post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let body =
mk_eapp array_set [mk_evar id_a; mk_econst 0; mk_econst 42]
in
let f = Efun(param1 id_a array_int_type,
None,Ity.MaskVisible,spec,body)
in
Dlet(mk_ident "f", false, Expr.RKnone, mk_expr f)
in
(mk_ident "M4",[use_int_Int ; use_array_Array ; f])
(* END{code4} *)
(* The following example is not in the manual
* it shows how to use Ptree API for scope/import declarations
module M5
scope S
function f (x : int) : int = x
end
import S
goal g : f 2 = 2
end
*)
let mod_M5 =
(* use int.Int *)
let use_int_Int = use_import (["int";"Int"]) in
(* scope S *)
let scope_S =
(* f *)
let f =
let logic = {
ld_loc = Loc.dummy_position;
ld_ident = mk_ident "f";
ld_params = [(Loc.dummy_position,Some (mk_ident "x"),false,int_type)] ;
ld_type = Some int_type;
ld_def = Some (mk_var (mk_ident "x")) ;
} in
Dlogic([logic])
in
Dscope(Loc.dummy_position,false,mk_ident "S",[f])
in
(* import S *)
let import_S = Dimport (mk_qualid ["S"]) in
(* goal g : f 2 = 2 *)
let g =
let two = mk_tconst 2 in
let eq_int = mk_qualid ["Int";Ident.op_infix "="] in
let f_of_two = mk_tapp (mk_qualid ["f"]) [two] in
let goal_term = mk_tapp eq_int [f_of_two ; two] in
Dprop(Pgoal,mk_ident "g",goal_term)
in
(mk_ident "M5",[use_int_Int ; scope_S ; import_S ; g])
(* BEGIN{getmodules} *)
let mods =
let mlw_file = Modules [mod_M1 ; mod_M2 ; mod_M3 ; mod_M4] in
Typing.type_mlw_file env [] "myfile.mlw" mlw_file
(* END{getmodules} *)
(* Checking the VCs *)

5
plugins/python/py_main.ml
View File

@@ -309,7 +309,7 @@ and block env ~loc = function
let e = Efun (params, None, Ity.MaskVisible, sp, body) in
Elet (id, false, Expr.RKnone, mk_expr ~loc e, s) in
mk_expr ~loc e
| (Dimport _ | Py_ast.Dlogic _) :: sl ->
| (Py_ast.Dimport _ | Py_ast.Dlogic _) :: sl ->
block env ~loc sl
let fresh_type_var =
@@ -350,7 +350,8 @@ let read_channel env path file c =
let use_import (f, m) =
let m = mk_id ~loc m in
Typing.open_scope loc m;
Typing.add_decl loc (Ptree.Duse (Qdot (Qident (mk_id ~loc f), m)));
let decl = Ptree.Duseimport(loc,false,[((Qdot (Qident (mk_id ~loc f), m)),None)]) in
Typing.add_decl loc decl ;
Typing.close_scope loc ~import:true in
List.iter use_import
["int", "Int"; "ref", "Refint"; "python", "Python"];

38
src/parser/parser.mly
View File

@@ -12,10 +12,6 @@
%{
open Ptree
let qualid_last = function Qident x | Qdot (_, x) -> x
let use_as q = function Some x -> x | None -> qualid_last q
let floc s e = Loc.extract (s,e)
let add_attr id l = (* id.id_ats is usually nil *)
@@ -322,7 +318,7 @@ module_decl:
| scope_head module_decl* END
{ Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 }
| IMPORT uqualid
{ Typing.import_scope (floc $startpos $endpos) $2 }
{ Typing.add_decl (floc $startpos $endpos) (Dimport($2)) }
| d = pure_decl | d = prog_decl | d = meta_decl
{ Typing.add_decl (floc $startpos $endpos) d;
add_record_projections d
@@ -347,27 +343,33 @@ module_decl_no_head:
use_clone:
| USE EXPORT tqualid
{ Typing.add_decl (floc $startpos $endpos) (Duse $3) }
{ let loc = floc $startpos $endpos in
let decl = Ptree.Duseexport $3 in
Typing.add_decl loc decl
}
| CLONE EXPORT tqualid clone_subst
{ Typing.add_decl (floc $startpos $endpos) (Dclone ($3, $4)) }
{ let loc = floc $startpos $endpos in
let decl = Ptree.Dcloneexport($3,$4) in
Typing.add_decl loc decl
}
| USE boption(IMPORT) m_as_list = comma_list1(use_as)
{ let loc = floc $startpos $endpos in
let exists_as = List.exists (fun (_, q) -> q <> None) m_as_list in
if $2 && not exists_as then Warning.emit ~loc
let import = $2 in
if import && not exists_as then Warning.emit ~loc
"the keyword `import' is redundant here and can be omitted";
let add_import (m, q) = let import = $2 || q = None in
Typing.open_scope loc (use_as m q);
Typing.add_decl loc (Duse m);
Typing.close_scope loc ~import in
List.iter add_import m_as_list }
let decl = Ptree.Duseimport(loc,import,m_as_list) in
Typing.add_decl loc decl
}
| CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst
{ let loc = floc $startpos $endpos in
if $2 && $4 = None then Warning.emit ~loc
let import = $2 in
let as_opt = $4 in
if import && as_opt = None then Warning.emit ~loc
"the keyword `import' is redundant here and can be omitted";
let import = $2 || $4 = None in
Typing.open_scope loc (use_as $3 $4);
Typing.add_decl loc (Dclone ($3, $5));
Typing.close_scope loc ~import }
let decl = Ptree.Dcloneimport(loc,import,$3,as_opt,$5) in
Typing.add_decl loc decl
}
use_as:
| n = tqualid q = option(preceded(AS, uident)) { (n, q) }

16
src/parser/ptree.ml
View File

@@ -263,7 +263,19 @@ type decl =
(** declaration of global exceptions *)
| Dmeta of ident * metarg list
(** `meta` *)
| Dclone of qualid * clone_subst list
| Dcloneexport of qualid * clone_subst list
(** `clone` *)
| Duse of qualid
| Duseexport of qualid
(** `use` *)
| Dcloneimport of Loc.position * bool * qualid * ident option * clone_subst list
(** `clone import ... as ...` *)
| Duseimport of Loc.position * bool * (qualid * ident option) list
(** `use import ... as ...` *)
| Dimport of qualid
(** `import` *)
| Dscope of Loc.position * bool * ident * decl list
(** `scope` *)
type mlw_file =
| Modules of (ident * decl list) list
| Decls of decl list

64
src/parser/typing.ml
View File

@@ -35,6 +35,11 @@ let debug_ignore_useless_at = Debug.register_flag "ignore_useless_at"
(** symbol lookup *)
let qualid_last = function Qident x | Qdot (_, x) -> x
let use_as q = function Some x -> x | None -> qualid_last q
let rec qloc = function
| Qdot (p, id) -> Loc.join (qloc p) id.id_loc
| Qident id -> id.id_loc
@@ -1463,7 +1468,7 @@ let type_inst ({muc_theory = tuc} as muc) ({mod_theory = t} as m) s =
in
List.fold_left add_inst (empty_mod_inst m) s
let add_decl muc env file d =
let rec add_decl muc env file d =
let vc = muc.muc_theory.uc_path = [] &&
Debug.test_noflag debug_type_only in
match d with
@@ -1501,12 +1506,57 @@ let add_decl muc env file d =
let ity = ity_of_pty muc pty in
let xs = create_xsymbol (create_user_id id) ~mask ity in
add_pdecl ~vc muc (create_exn_decl xs)
| Ptree.Duse use ->
| Ptree.Duseexport use ->
use_export muc (find_module env file use)
| Ptree.Dclone (use, inst) ->
| Ptree.Dcloneexport (use, inst) ->
let m = find_module env file use in
warn_clone_not_abstract (qloc use) m.mod_theory;
clone_export muc m (type_inst muc m inst)
| Ptree.Duseimport (_loc,import,uses) ->
let add_import muc (m, q) =
let import = import || q = None in
let muc = open_scope muc (use_as m q).id_str in
let m = find_module env file m in
let muc = use_export muc m in
close_scope muc ~import in
List.fold_left add_import muc uses
| Ptree.Dcloneimport (_loc,import,qid,as_opt,inst) ->
let import = import || as_opt = None in
let muc = open_scope muc (use_as qid as_opt).id_str in
let m = find_module env file qid in
warn_clone_not_abstract (qloc qid) m.mod_theory;
let muc = clone_export muc m (type_inst muc m inst) in
let muc = close_scope muc ~import in
muc
| Ptree.Dimport q ->
import_scope muc (string_list_of_qualid q)
| Ptree.Dscope (_loc,import,qid,decls) ->
let muc = open_scope muc qid.id_str in
let add_decl_env_file muc d = add_decl muc env file d in
let muc = List.fold_left add_decl_env_file muc decls in
let muc = close_scope muc ~import in
muc
let type_module file env loc path (id,dl) =
let muc = create_module env ~path (create_user_id id) in
let add_decl_env_file muc d = add_decl muc env file d in
let muc = List.fold_left add_decl_env_file muc dl in
let m = Loc.try1 ~loc close_module muc in
let file = Mstr.add m.mod_theory.th_name.id_string m file in
file
let type_mlw_file env path filename mlw_file =
let file = Mstr.empty in
let loc = Loc.user_position filename 0 0 0 in
let file =
match mlw_file with
| Ptree.Decls decls -> type_module file env loc path ({id_str=""; id_ats=[]; id_loc=loc},decls)
| Ptree.Modules m_or_t ->
let type_module_env_loc_path file (id,dl) = type_module file env loc path (id,dl) in
List.fold_left type_module_env_loc_path file m_or_t
in
file
(* incremental parsing *)
@@ -1574,14 +1624,6 @@ let close_scope loc ~import =
let muc = Loc.try1 ~loc (close_scope ~import) (Opt.get slice.muc) in
slice.muc <- Some muc
let import_scope loc q =
assert (not (Stack.is_empty state));
let slice = Stack.top state in
let muc = top_muc_on_demand loc slice in
if Debug.test_noflag debug_parse_only then
let muc = Loc.try2 ~loc import_scope muc (string_list_of_qualid q) in
slice.muc <- Some muc
let add_decl loc d =
assert (not (Stack.is_empty state));
let slice = Stack.top state in

4
src/parser/typing.mli
View File

@@ -17,6 +17,8 @@ val debug_parse_only : Debug.flag
val debug_type_only : Debug.flag
val type_mlw_file : Env.env -> string list -> string -> Ptree.mlw_file -> Pmodule.pmodule Wstdlib.Mstr.t
(** {2 Incremental typing of parsed modules} *)
val open_file : Env.env -> Env.pathname -> unit
@@ -33,8 +35,6 @@ val open_scope : Loc.position -> Ptree.ident -> unit
val close_scope : Loc.position -> import:bool -> unit
val import_scope : Loc.position -> Ptree.qualid -> unit
val add_decl : Loc.position -> Ptree.decl -> unit
(** {2 Typing terms and formulas in isolation} *)