-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathExtractBigStepSemanticsTraced.v
More file actions
32 lines (25 loc) · 1023 Bytes
/
ExtractBigStepSemanticsTraced.v
File metadata and controls
32 lines (25 loc) · 1023 Bytes
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
Require Core_Erlang_Coverage.
Import Core_Erlang_Coverage.
Import Core_Erlang_Syntax.Value_Notations.
Import ListNotations.
(********************************)
(* Extraction Language: Haskell *)
(********************************)
Extraction Language Haskell.
(***************************)
(* Use Haskell basic types *)
(***************************)
Require Import ExtrHaskellBasic.
Require Import ExtrHaskellString.
Require Import ExtrHaskellZInteger.
Require Import ExtrHaskellNatNum.
Require Import ExtrHaskellNatInt.
(****************************************)
(* Use Haskell support for Nat handling *)
(****************************************)
(*Require Import ExtrHaskellNatNum.*)
(*Extract Inductive Datatypes.nat => "Prelude.Integer" ["0" "succ"]*)
(*"(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".*)
Definition fbs_helper (limit : nat)(expr : Expression) : (ResultType * Log) :=
(fbs_expr limit init_logs [] 0 expr []).
Extraction "BigStepSemanticsTraced.hs" fbs_helper result_value.