diff options
| author | Kathy Gray | 2013-11-01 17:03:40 +0000 |
|---|---|---|
| committer | Kathy Gray | 2013-11-01 17:03:40 +0000 |
| commit | b3a69210b3e3d1b5ebc1d6687884ecfe3fd202f2 (patch) | |
| tree | aef92a73dfda5888cdb53d2b0af77298edd82863 /src/pretty_print.ml | |
| parent | 7fdb44465a2eb169946ec0e23b4056aafabe1b93 (diff) | |
Moved metatheory grammars into l2_rules.ott
Added val extern specification to language, parser, printer, and interpreter
Added various def level type system support, expressions type system in place Except for assignment
Diffstat (limited to 'src/pretty_print.ml')
| -rw-r--r-- | src/pretty_print.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index c85cafb3..55d09dcb 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -262,8 +262,10 @@ let pp_default ppf (DT_aux(df,_)) = | DT_kind(bk,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_bkind bk pp_id id | DT_typ(ts,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_typscm ts pp_id id -let pp_spec ppf (VS_aux(VS_val_spec(ts,id),_)) = - fprintf ppf "@[<0>%a %a %a@]@\n" kwd "val" pp_typscm ts pp_id id +let pp_spec ppf (VS_aux(v,_)) = + match v with + | VS_val_spec(ts,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "val" pp_typscm ts pp_id id + | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>%a %a %a %a %a \"%s\"@]@\n" kwd "val" kwd "extern" pp_typscm ts pp_id id kwd "=" s let pp_namescm ppf (Name_sect_aux(ns,_)) = match ns with @@ -556,8 +558,10 @@ let pp_lem_default ppf (DT_aux(df,_)) = | DT_kind(bk,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_id id | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id -let pp_lem_spec ppf (VS_aux(VS_val_spec(ts,id),_)) = - fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id +let pp_lem_spec ppf (VS_aux(v,_)) = + match v with + | VS_val_spec(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id + | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s let pp_lem_namescm ppf (Name_sect_aux(ns,_)) = match ns with |