From d57e3491720e912b4e2fd6c73f9d356901a42df5 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Tue, 17 Jun 2014 14:34:40 +0200 Subject: Write transformation of program into logical formula. --- interpret/ast_util.ml | 2 +- interpret/interface.ml | 6 ++++++ interpret/interpret.ml | 2 ++ 3 files changed, 9 insertions(+), 1 deletion(-) (limited to 'interpret') diff --git a/interpret/ast_util.ml b/interpret/ast_util.ml index e7428bd..80411d8 100644 --- a/interpret/ast_util.ml +++ b/interpret/ast_util.ml @@ -70,4 +70,4 @@ let combinatorial_cycle v = error ("Combinatorial cycle with variable: " ^ v) let no_variable e = error ("No such variable: " ^ e) let type_error e = error ("Type error: " ^ e) let not_implemented e = error ("Not implemented: " ^ e) - +let invalid_arity e = error ("Invalid arity (" ^ e ^ ")") diff --git a/interpret/interface.ml b/interpret/interface.ml index 7b84396..621bfa2 100644 --- a/interpret/interface.ml +++ b/interpret/interface.ml @@ -1,4 +1,5 @@ open Ast +open Util module type INTERPRET = sig @@ -23,6 +24,11 @@ module type INTERPRET = sig type io = (id * value) list + (* + Get the constants only + *) + val consts : prog -> id -> value VarMap.t + (* Construct initial state for a program. The id is the root node of the program evaluation. diff --git a/interpret/interpret.ml b/interpret/interpret.ml index 063dad0..24903f1 100644 --- a/interpret/interpret.ml +++ b/interpret/interpret.ml @@ -451,5 +451,7 @@ module I : INTERPRET = struct do_weak_transitions env st.root_scope; extract_st env, out + let consts p root = + (init_state p root).save end -- cgit v1.2.3