[OCaml backend] translation of indrelns not supported ?

[jserot]

Taking the classical CBV as example:

(* generated by Ott 0.31 from: cbv.ott *)
open import Pervasives

type var = string (* term variable *)

type term =  (* term *)
 | T_var of var (* variable *)
 | T_lam of var * term (* lambda *)
 | T_app of term * term (* app *)

(** subrules *)
let is_val_of_term (t5:term) : bool =
  match t5 with
   | (T_var x) -> false
   | (T_lam x t) -> (true)
   | (T_app t t') -> false
  end

(** substitutions *)
let rec tsubst_term (t5:term) (x5:var) (t_6:term) : term =
  match t_6 with
   | (T_var x) -> (if x=x5 then t5 else (T_var x))
   | (T_lam x t) -> T_lam x (if  List.elem x5 ([x]) then t else (tsubst_term t5 x5 t))
   | (T_app t t') -> T_app (tsubst_term t5 x5 t) (tsubst_term t5 x5 t')
  end

(** definitions *)
(* defns Jop *)
indreln
[reduce : term -> term -> bool witness type r_wit; check r_check; eval: input -> output]
(* defn reduce *)

ax_app: forall x t1 v2 .
(is_val_of_term v2)
 ==> 
reduce (T_app  (T_lam x t1)  v2)  (tsubst_term  v2   x   t1 ) 

and
ctx_app_fun: forall t1 t t1' .
(reduce t1 t1')
 ==> 
reduce (T_app t1 t) (T_app t1' t)

and
ctx_app_arg: forall v t1 t1' .
(is_val_of_term v) &&
(reduce t1 t1')
 ==> 
reduce (T_app v t1) (T_app v t1')

i was unable to generate OCaml code for it. Invoking

lem -ocaml cbv.lem

gives

** Relation reduce :
input -> input -> list unit
input -> output -> list unit
File "cbv.lem", line 14, character 3 to line 18, character 5
  Warning: unused variables: 'x', 'x', 't', 't', 't''
DEBUG: Known variables: t t1 
DEBUG: Return expressions: 
(Cbv.T_app t1' t)
DEBUG: Equalities conditions: 
DEBUG: Side conditions: 
DEBUG: 1 notoks
No translation for relation reduce, mode input -> output ->  unit
Blocking rule is ctx_app_fun
Fatal error: exception Convert_relations.Converter(C).No_translation(0)

Am i missing sth ? The description given is the ICFP 2014 paper (sec 3.12) seems to imply that, in this simple case, lem is able to generate the OCaml implementation of the defined relation.

[PeterSewell]

That inductive-relation code generation machinery certainly did work in cases like this, but we've not used it or maintained it since, so I'm afraid I don't know what state it's in now.

Peter

On Fri, 20 Aug 2021 at 08:43, jserot @.***> wrote:

Taking the classical CBV as example:

( generated by Ott 0.31 from: cbv.ott ) open import Pervasives

type var = string ( term variable )

type term = ( term ) | T_var of var ( variable ) | T_lam of var term ( lambda ) | T_app of term term ( app )

(* subrules ) let is_val_of_term (t5:term) : bool = match t5 with | (T_var x) -> false | (T_lam x t) -> (true) | (T_app t t') -> false end

(* substitutions ) let rec tsubst_term (t5:term) (x5:var) (t_6:term) : term = match t_6 with | (T_var x) -> (if x=x5 then t5 else (T_var x)) | (T_lam x t) -> T_lam x (if List.elem x5 ([x]) then t else (tsubst_term t5 x5 t)) | (T_app t t') -> T_app (tsubst_term t5 x5 t) (tsubst_term t5 x5 t') end

(* definitions ) ( defns Jop ) indreln [reduce : term -> term -> bool witness type r_wit; check r_check; eval: input -> output] ( defn reduce )

ax_app: forall x t1 v2 . (is_val_of_term v2) ==> reduce (T_app (T_lam x t1) v2) (tsubst_term v2 x t1 )

and ctx_app_fun: forall t1 t t1' . (reduce t1 t1') ==> reduce (T_app t1 t) (T_app t1' t)

and ctx_app_arg: forall v t1 t1' . (is_val_of_term v) && (reduce t1 t1') ==> reduce (T_app v t1) (T_app v t1')

i was unable to generate OCaml code for it. Invoking

lem -ocaml cbv.lem

gives

** Relation reduce : input -> input -> list unit input -> output -> list unit File "cbv.lem", line 14, character 3 to line 18, character 5 Warning: unused variables: 'x', 'x', 't', 't', 't'' DEBUG: Known variables: t t1 DEBUG: Return expressions: (Cbv.T_app t1' t) DEBUG: Equalities conditions: DEBUG: Side conditions: DEBUG: 1 notoks No translation for relation reduce, mode input -> output -> unit Blocking rule is ctx_app_fun Fatal error: exception Convert_relations.Converter(C).No_translation(0)

Am i missing sth ? The description given is the ICFP 2014 paper (sec 3.12) seems to imply that, in this simple case, lem is able to generate the OCaml implementation of the defined relation.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/rems-project/lem/issues/32, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZSW3EHGLUVIPUAY6B3T5YBRZANCNFSM5CPY23MQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email .

[jserot]

Thanks for the answer, Peter.

Any chance this will be fixed in the near future ?

More generally, I was wondering whether there are some example (even toy) showing how to use Ott and lem to automatically derive interpreters for small DSLs.

Jocelyn

[PeterSewell]

On Sat, 21 Aug 2021 at 08:57, jserot @.***> wrote:

Thanks for the answer, Peter.

Any chance this will fixed in the near future ?

I'm afraid not. Lem remains in use, but we're not actively developing it, and that specific feature was a student internship project (by Thomas Williams) that I don't think we've used after he left.

More generally, I was wondering whether there are same example (even toy) showing how to use Ott and lem to automatically derive interpreters for small DSLs.

Doing that in general remains an interesting research problem, depending on how one wants to specify the operational semantics and what constraints (on performance, compatability with other s/w, error reporting, etc.) one has on the resulting interpreter. Ott and Lem don't really aim to support it. The most lightweight think one might do right now would be to define the concrete and abstract syntax using Ott, use Ott's experimental menhir parser+prettyprinter generation to build those,use Ott's Lem or OCaml generation to generate AST types, and then write a pure-functional interpreter above those. Alternatively, if one really wants the semantics to be expressed with inductive relations rather than functions, one could write that in Ott, generate Isabelle definitions, and then see if Isabelle's machinery for executing relational definitions can handle them.

Peter

Jocelyn

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/rems-project/lem/issues/32#issuecomment-903078414, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZQVO7ETB2UR4N2MUE3T55L7LANCNFSM5CPY23MQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email .

[jserot]

Ok, I understand.

Thanks for the clarification.

Jocelyn