Commit 2a3e1f33 authored by charguer's avatar charguer

ref to external modules fixed

parent f44d5ee2
#################################################################
# install coq8.5beta2 if you don't have it yet
# Requirements
# you'll need the "pprint" ocaml package installed.
#################################################################
# install coq8.5rc1 if you don't have it yet
# on ubuntu or similar:
- download https://coq.inria.fr/distrib/V8.5beta2/files/coq-8.5beta2.tar.gz
- extract the archive into ~/softs/coq-8.5beta2/ (else you'll need to adapt paths)
- download https://coq.inria.fr/distrib/V8.5rc1/files/coq-8.5rc1.tar.gz
- extract the archive into ~/softs/coq-8.5rc1/ (else you'll need to adapt paths)
- then execute the following commands:
cd ~/softs/coq-8.5beta2/
cd ~/softs/coq-8.5rc1/
./configure -local
make -j 4
......@@ -21,8 +28,8 @@ git clone -b epit https://gforge.inria.fr/git/tlc/tlc.git ~/tlc
# adapt the path below if coq8.5 is installed elsewhere
# (or skip the commands if it is in your path)
# [make sure to include the trailing slash after bin]
echo COQBIN=~/softs/coq-8.5beta2/bin/ > ~/cfml/settings.sh
echo COQBIN=~/softs/coq-8.5beta2/bin/ > ~/tlc/src/settings.sh
echo COQBIN=~/softs/coq-8.5rc1/bin/ > ~/cfml/settings.sh
echo COQBIN=~/softs/coq-8.5rc1/bin/ > ~/tlc/src/settings.sh
# adapt the path below if ~/cfml is not the path used
echo CFML=~/cfml >> ~/cfml/settings.sh
......@@ -54,5 +61,5 @@ make exo
#################################################################
# remark: .coqide is generated by the makefile, and its contents is:
~/softs/coq-8.5beta2/bin/coqide -R ../..//lib/coq CFML -R ../..//lib/tlc TLC -R . EXAMPLE $*
~/softs/coq-8.5rc1/bin/coqide -R ../..//lib/coq CFML -R ../..//lib/tlc TLC -R . EXAMPLE $*
......@@ -2,7 +2,7 @@
(* todo: warning if not the right nb of args on xapp *)
-> DemoMake, corriger let n = null
-> corriger let n = null qui ne génère pas ce qu'il faut
unifier main.ml et makecmj.ml
......
open Aux (* required for cfml to do the require in Coq, in the current implementation *)
open NullPointers
let g x = Aux.f x
(* TODO: bug:: let n = null *)
\ No newline at end of file
EXAMPLE_DIRS = \
BasicDemos \
DemoMake \
Compose \
Memoization \
......@@ -6,8 +7,11 @@ EXAMPLE_DIRS = \
MutableLists \
BatchedQueue \
PairingHeap \
SelfBalancedHeap \
BinaryTrees
SelfBalancedHeap
# TOFIX
# \ BinaryTrees
# Currently not built:
#
......
......@@ -114,10 +114,10 @@ Proof.
hdata_simpl MemoState. intros v.
hextract as Hv M' HM'. hsimpl*.
intros M' HM' Hv. xapp*. xret. hsimpl*.
intros y Hd. rewrite* map_indom_update in Hd.
intros y Hd. rewrite* indom_update in Hd.
tests: (x = y).
rewrite* map_update_read_eq.
rewrite* map_update_read_neq. destruct Hd; tryfalse; autos*.
rewrite* update_read_eq.
rewrite* update_read_neq. destruct Hd; tryfalse; autos*.
xret_no_gc. unfold Memo. hdata_simpl.
applys hsimpl_exists_give h.
hdata_simpl MemoState. hsimpl*.
......
......@@ -29,6 +29,21 @@ let not_in_normal_form s =
raise (Not_in_normal_form s)
(*#########################################################################*)
(* ** List of external modules that need to be required *)
let external_modules = ref []
let external_modules_add name =
external_modules := name::!external_modules
let external_modules_get_coqtop () =
List.map (fun name -> Coqtop_require name) !external_modules
let external_modules_reset () =
external_modules := []
(*#########################################################################*)
(* ** Lifting of paths *)
......@@ -36,7 +51,7 @@ let lift_ident_name id =
let name = Ident.name id in
if name = "OkaStream" then "CFPrim" else (* TODO : improve *)
if Ident.persistent id
then (Printf.printf "require %s\n" name; name ^ "_ml")
then (let result = name ^ "_ml" in external_modules_add result; result)
else "ML" ^ name
let rec lift_full_path = function
......@@ -1331,6 +1346,9 @@ and cfg_module id m =
a Caml file. *)
let cfg_file str =
[ Cftop_coqs [ Coqtop_set_implicit_args; Coqtop_require_import (if !pure_mode then "FuncPrim" else "CFHeader") ] ]
[ Cftop_coqs ([
Coqtop_set_implicit_args;
Coqtop_require_import (if !pure_mode then "FuncPrim" else "CFHeader") ]
@ (external_modules_get_coqtop())) ]
@ cfg_structure str
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment