Last change
on this file since 2731 was
2717,
checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.
I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).
I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size:
534 bytes

Line  

1  open Preamble 

2  

3  open Bool 

4  

5  open Relations 

6  

7  open Nat 

8  

9  open Hints_declaration 

10  

11  open Core_notation 

12  

13  open Pts 

14  

15  open Logic 

16  

17  open Types 

18  

19  open List 

20  

21  type ('a, 'b) assoc_list = ('a, 'b) Types.prod List.list 

22  

23  val assoc_list_add : 

24  ('a1, 'a2) Types.prod > ('a1, 'a2) assoc_list > ('a1, 'a2) Types.prod 

25  List.list 

26  

27  val assoc_list_exists : 

28  'a1 > ('a1 > 'a1 > Bool.bool) > ('a1, 'a2) Types.prod List.list > 

29  Bool.bool 

30  

31  val assoc_list_lookup : 

32  'a1 > ('a1 > 'a1 > Bool.bool) > ('a1, 'a2) Types.prod List.list > 'a2 

33  Types.option 

34  

Note: See
TracBrowser
for help on using the repository browser.