File tree Expand file tree Collapse file tree 4 files changed +47
-1
lines changed Expand file tree Collapse file tree 4 files changed +47
-1
lines changed Original file line number Diff line number Diff line change 1616(executable (name sepcomp_tyid) (modules sepcomp_tyid) (libraries sepcomp))
1717(executable (name sepcomp_tyid2) (modules sepcomp_tyid2) (libraries sepcomp))
1818(executable (name sepcomp_hover) (modules sepcomp_hover) (libraries sepcomp))
19- (executable (name sepcomp_extend_sig) (modules sepcomp_extend_sig) (libraries sepcomp))
19+ (executable (name sepcomp_extend_sig) (modules sepcomp_extend_sig) (libraries sepcomp))
20+ (executable (name sepcomp_extend_sig2) (modules sepcomp_extend_sig2) (libraries sepcomp))
Original file line number Diff line number Diff line change 1+ let u = {|
2+
3+ pred p i :int .
4+ p 2 :- ! , fail .
5+
6+ |}
7+ ;;
8+
9+ let v = {|
10+
11+ p _.
12+ main :- p 2.
13+
14+ |}
15+ ;;
16+
17+ let () =
18+ let open Sepcomp.Sepcomp_template in
19+ let elpi = init () in
20+ let flags = Elpi.API.Compile. default_flags in
21+ let base = Elpi.API.Compile. empty_base ~elpi in
22+ let _, u = cc ~elpi ~flags ~base 0 u in
23+ let su = signature_of u in
24+ let base = extend_signature ~flags ~base su in
25+ let base = extend ~flags ~base u in
26+ let base, _ = cc ~elpi ~flags ~base 0 v in
27+ let q = query ~elpi base in
28+ assert (try_exec q = false );
29+ let base, _ = cc ~elpi ~flags ~base 0 " fail." in
30+ let q = query ~elpi base in
31+ exec q
32+
Original file line number Diff line number Diff line change @@ -32,6 +32,13 @@ let exec q =
3232 | Execute. Success _ -> exit 0
3333 | Execute. NoMoreSteps -> assert false
3434
35+ let try_exec q =
36+ let exe = Compile. optimize q in
37+ match Execute. once exe with
38+ | Execute. Failure -> false
39+ | Execute. Success _ -> true
40+ | Execute. NoMoreSteps -> assert false
41+
3542let main us =
3643 let elpi = init () in
3744 let flags = Compile. default_flags in
Original file line number Diff line number Diff line change @@ -72,3 +72,9 @@ let () = declare "sepcomp_extend_sig"
7272 ~expectation: Test. Success
7373 ()
7474
75+ let () = declare " sepcomp_extend_sig2"
76+ ~source_dune: " sepcomp_extend_sig2.exe"
77+ ~description: " extend unit with signature then code"
78+ ~expectation: Test. Success
79+ ()
80+
You can’t perform that action at this time.
0 commit comments