Require Import Coq.Strings.String. Require Import Coq.Lists.List.

Inductive tm: Type := | tvar: nat -> tm | tfun: string -> list tm -> tm.

Inductive fm: Type := | ffalse: fm -> fm | fpre: string -> list tm -> fm | fimp: fm -> fm -> fm | fdis: fm -> fm -> fm | fcon: fm -> fm -> fm | fexi: fm -> fm | funi: fm -> fm.

Definition domain := nat. Definition env_t := (nat -> domain). Definition f_map_t := (string -> list domain -> domain).

Inductive semantics_tm : tm -> domain -> Prop := | s_var: forall (env:env_t) (n:nat), semantics_tm (tvar n) n | s_fun: forall (env:env_t) (f_map:f_map_t) (i:string) (l:list tm) (tl: list domain), (forall j, semantics_tm (nth j l (tvar 0)) (nth j tl 0)) -> semantics_tm (tfun i l) ((f_map i) tl).

Example semantics : semantics_tm (tfun "+" ((tvar 1) :: (tvar 2) :: nil)) 3. Abort.