syntax.makam

%open syntax.

(*
To check the syntax of our language we have to add in a few extra
non HOAS terms with explicitly labelled variables. The concrete
library does most of the work for us.
*)

program : syntax (program term).
concrete_program : syntax (concrete (program term)).

chain : syntax term.
compound : syntax term.
expr : syntax term.

variable : syntax (concrete.name term).
termvar : concrete.namespace term.
binder : syntax term.

concrete.pick_namespace_userdef (_: term) termvar.

ccheck : concrete.name term -> term -> term -> program B -> program B.
clet : concrete.name A -> A -> program B -> program B.

concrete.resolve_conversion
         (ccheck Name A X Body)
         (bind (check X A) (concrete.lambda Name Body)).
concrete.resolve_conversion
         (clet Name X Body)
         (bind (nop X) (concrete.lambda Name Body)).

cforall : concrete.name term -> term -> term -> term.
clam : concrete.name term -> term -> term -> term.

concrete.resolve_conversion (cforall Name Obj Body) (forall Obj (concrete.lambda Name Body)).
concrete.resolve_conversion (clam Name Obj Body) (lam Obj (concrete.lambda Name Body)).

(* FIXME Use something else for variables. *)
(* FIXME Find a way to reduce generated parser size. *)
`(syntax_rules <<
  concrete_program -> concrete { <program> }
  program ->
     clet { "Let" <variable> ":=" <binder> "." <program> }
     / ccheck { "Check" <variable> ":" <expr> ":=" <binder> "." <program> }
     / pure { <binder> }

  variable ->
      concrete.name termvar { <makam.string_literal> } ;

  compound ->
      app { <expr> <expr> }
      / axiom { "axiom" <makam.string_literal> ":" <expr> }
      / expr ;

  expr ->
      typ { "□" }
      / set { "*" }
      / zobject { "Z" }
      / z { <makam.int_literal> }
      / concrete.var { <variable> }
      / { "(" <binder> ")" } ;

  chain -> compound ;

  binder ->
      cforall { "∀" <variable> ":" <expr> "." <binder> }
      / clam { "λ" <variable> ":" <expr> "." <binder> }

      / chain

>>).

`( syntax.def_toplevel_js concrete_program ).

isocast_def (Iso: iso (program term) string) :-
  eq Iso (iso.compose [ iso.inverse (iso.bidi concrete.resolve), PrettyIso ]),
  isocast_find unit (PrettyIso: iso (concrete (program term)) string).