Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
@gares
gares committed Oct 10, 2024
1 parent d6f46be commit b569aa0
Show file tree
Hide file tree
Showing 6 changed files with 75 additions and 34 deletions.
46 changes: 39 additions & 7 deletions src/compiler.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -665,19 +665,24 @@ module ScopedTypeExpression = struct
type t_ =
| Const of scope * F.t
| App of F.t * e * e list
| Arrow of e * e
| Pred of Ast.Structured.functionality * (Ast.Mode.t * e) list
| CData of CData.t
and e = { it : t_; loc : Loc.t }
[@@ deriving show]

type t =
| Lam of F.t * t
type v_ =
| Lam of F.t * v_
| Ty of e
type t = { name : F.t; value : v_; nparams : int; loc : Loc.t }

let rec eqt ctx t1 t2 =
match t1.it, t2.it with
| Const(Global,c1), Const(Global,c2) -> F.equal c1 c2
| Const(Local,c1), Const(Local,c2) -> ScopedTerm.eq_var ctx c1 c2
| App(c1,x,xs), App(c2,y,ys) -> F.equal c1 c2 && eqt ctx x y && Util.for_all2 (eqt ctx) xs ys
| Arrow(s1,t1), Arrow(s2,t2) -> eqt ctx s1 s2 && eqt ctx t1 t2
| Pred(f1,l1), Pred(f2,l2) -> f1 == f2 && Util.for_all2 (fun (m1,t1) (m2,t2) -> Ast.Mode.compare m1 m2 == 0 && eqt ctx t1 t2) l1 l2
| CData c1, CData c2 -> CData.equal c1 c2
| _ -> false

Expand Down Expand Up @@ -881,19 +886,22 @@ end = struct (* {{{ *)
{ c with Chr.attributes = aux_chr { cid; cifexpr = None } attributes }


let rec structure_type_expression_aux ~loc = function
let rec structure_type_expression_aux ~loc t = { t with TypeExpression.tit =
match t.TypeExpression.tit with
| TypeExpression.TPred([Functional],p) -> TypeExpression.TPred(Function,List.map (fun (m,p) -> m, structure_type_expression_aux ~loc p) p)
| TypeExpression.TPred([],p) -> TypeExpression.TPred(Relation,List.map (fun (m,p) -> m, structure_type_expression_aux ~loc p) p)
| TypeExpression.TPred(a :: _, _) -> error ~loc ("illegal attribute " ^ show_raw_attribute a)
| TypeExpression.TArr(s,t) -> TypeExpression.TArr(structure_type_expression_aux ~loc s,structure_type_expression_aux ~loc t)
| TypeExpression.TApp(c,x,xs) -> TypeExpression.TApp(c,structure_type_expression_aux ~loc x,List.map (structure_type_expression_aux ~loc) xs)
| TypeExpression.TCData c -> TypeExpression.TCData c
| TypeExpression.TConst c -> TypeExpression.TConst c
}

let structure_type_expression loc toplevel_func = function
let structure_type_expression loc toplevel_func t =
match t.TypeExpression.tit with
| TypeExpression.TPred([],p) ->
TypeExpression.TPred(toplevel_func,List.map (fun (m,p) -> m, structure_type_expression_aux ~loc p) p)
| x -> structure_type_expression_aux ~loc x
{ t with TypeExpression.tit = TypeExpression.TPred(toplevel_func,List.map (fun (m,p) -> m, structure_type_expression_aux ~loc p) p) }
| x -> structure_type_expression_aux ~loc t

let structure_type_attributes { Type.attributes; loc; name; ty } =
let duplicate_err s =
Expand Down Expand Up @@ -934,7 +942,7 @@ end = struct (* {{{ *)

let structure_type_abbreviation { TypeAbbreviation.name; value; nparams; loc } =
let rec aux = function
| TypeAbbreviation.Lam(c,t) -> TypeAbbreviation.Lam(c,aux t)
| TypeAbbreviation.Lam(c,loc,t) -> TypeAbbreviation.Lam(c,loc,aux t)
| TypeAbbreviation.Ty t -> TypeAbbreviation.Ty (structure_type_expression loc Relation t)
in
{ TypeAbbreviation.name; value = aux value; nparams; loc }
Expand Down Expand Up @@ -1183,6 +1191,30 @@ end = struct
let it = scope_term ctx ~loc it in
{ ScopedTerm.it; loc }

let rec scope_tye ctx ~loc t =
match t with
| Ast.TypeExpression.TConst c when F.Set.mem c ctx -> ScopedTypeExpression.(Const(ScopedTerm.Local,c))
| Ast.TypeExpression.TConst c -> ScopedTypeExpression.(Const(ScopedTerm.Global,c))
| Ast.TypeExpression.TApp(c,x,xs) ->
if F.Set.mem c ctx then error ~loc "type schema parameters cannot be type formers";
ScopedTypeExpression.App(c,scope_loc_tye ctx x, List.map (scope_loc_tye ctx) xs)
| Ast.TypeExpression.TPred(m,xs) ->
ScopedTypeExpression.Pred(m,List.map (fun (m,t) -> m, scope_loc_tye ctx t) xs)
| Ast.TypeExpression.TArr(s,t) ->
ScopedTypeExpression.Arrow(scope_loc_tye ctx s, scope_loc_tye ctx t)
| Ast.TypeExpression.TCData c -> ScopedTypeExpression.CData c
and scope_loc_tye ctx { tloc; tit } = { loc = tloc; it = scope_tye ctx ~loc:tloc tit }

let scope_type_abbrev { Ast.TypeAbbreviation.name; value; nparams; loc } =
let rec aux ctx = function
| Ast.TypeAbbreviation.Lam(c,loc,t) when is_uvar_name c ->
if F.Set.mem c ctx then error ~loc "duplicate type schema variable";
ScopedTypeExpression.Lam(c,aux (F.Set.add c ctx) t)
| Ast.TypeAbbreviation.Lam(c,loc,_) -> error ~loc "only variables can be abstracted in type schema"
| Ast.TypeAbbreviation.Ty t -> ScopedTypeExpression.Ty (scope_loc_tye ctx t)
in
{ ScopedTypeExpression.name; value = aux F.Set.empty value; nparams; loc }

let scope_loc_term = scope_loc_term F.Set.empty

let compile_type_abbrev abbrvs { Ast.TypeAbbreviation.name; value; nparams; loc } =
Expand Down
20 changes: 11 additions & 9 deletions src/parser/ast.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ end

module Mode = struct

type mode = Util.arg_mode = Input | Output
type t = Util.arg_mode = Input | Output
[@@deriving show, ord]

end
Expand All @@ -79,18 +79,20 @@ type raw_attribute =
| Functional
[@@deriving show, ord]


module TypeExpression = struct

type 'attribute t =
| TConst of Func.t
| TApp of Func.t * 'attribute t * 'attribute t list
| TPred of 'attribute * (Mode.mode * 'attribute t) list
| TArr of 'attribute t * 'attribute t
| TCData of CData.t
type 'attribute t_ =
| TConst of Func.t
| TApp of Func.t * 'attribute t * 'attribute t list
| TPred of 'attribute * (Mode.t * 'attribute t) list
| TArr of 'attribute t * 'attribute t
| TCData of CData.t
and 'a t = { tit : 'a t_; tloc : Loc.t }
[@@ deriving show, ord]

end

module Term = struct

type t_ =
Expand Down Expand Up @@ -225,7 +227,7 @@ end
module TypeAbbreviation = struct

type 'ty closedTypeexpression =
| Lam of Func.t * 'ty closedTypeexpression
| Lam of Func.t * Loc.t * 'ty closedTypeexpression
| Ty of 'ty
[@@ deriving show, ord]

Expand Down
11 changes: 6 additions & 5 deletions src/parser/ast.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ end

module Mode : sig

type mode = Input | Output
type t = Input | Output
[@@deriving show, ord]

end
Expand All @@ -61,13 +61,14 @@ type raw_attribute =

module TypeExpression : sig

type 'attribute t =
type 'attribute t_ =
| TConst of Func.t
| TApp of Func.t * 'attribute t * 'attribute t list
| TPred of 'attribute * ((Mode.mode * 'attribute t) list)
| TPred of 'attribute * (Mode.t * 'attribute t) list
| TArr of 'attribute t * 'attribute t
| TCData of CData.t
[@@ deriving show, ord]
and 'a t = { tit : 'a t_; tloc : Loc.t }
[@@ deriving show, ord]

end

Expand Down Expand Up @@ -153,7 +154,7 @@ end
module TypeAbbreviation : sig

type 'ty closedTypeexpression =
| Lam of Func.t * 'ty closedTypeexpression
| Lam of Func.t * Loc.t * 'ty closedTypeexpression
| Ty of 'ty
[@@ deriving show, ord]

Expand Down
24 changes: 13 additions & 11 deletions src/parser/grammar.mly
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ let loc (startpos, endpos) = {
line_starts_at = startpos.Lexing.pos_bol;
}

let desugar_multi_binder loc t =
let desugar_multi_binder loc (t : Ast.Term.t) =
match t.it with
| App( { it = Const hd } as binder,args)
when Func.equal hd Func.pif || Func.equal hd Func.sigmaf && List.length args > 1 ->
Expand Down Expand Up @@ -112,6 +112,8 @@ let mode_of_IO io =
%type < Func.t > prefix_SYMB
%type < Func.t > postfix_SYMB
%type < Func.t > constant
%type < 'a TypeExpression.t > type_term
%type < 'a TypeExpression.t > atype_term

(* entry points *)
%start program
Expand Down Expand Up @@ -175,14 +177,14 @@ chr_rule:
pred:
| attributes = attributes; PRED;
name = constant; args = separated_list(option(CONJ),pred_item) {
{ Type.loc=loc $sloc; name; attributes; ty = TPred ([], args) }
{ Type.loc=loc $sloc; name; attributes; ty = { tloc = loc $loc; tit = TPred ([], args) } }
}
pred_item:
| io = IO_COLON; ty = type_term { (mode_of_IO io,ty) }

anonymous_pred:
| attributes = attributes; PRED;
args = separated_list(option(CONJ),pred_item) { TPred (attributes, args) }
args = separated_list(option(CONJ),pred_item) { { tloc = loc $loc; tit = TPred (attributes, args) } }

kind:
| KIND; names = separated_nonempty_list(CONJ,constant); k = kind_term {
Expand All @@ -197,20 +199,20 @@ type_:
}

atype_term:
| c = STRING { TCData (cstring.Util.CData.cin c) }
| c = constant { TConst (fix_church c) }
| c = STRING { { tloc = loc $loc; tit = TCData (cstring.Util.CData.cin c) } }
| c = constant { { tloc = loc $loc; tit = TConst (fix_church c) } }
| LPAREN; t = type_term; RPAREN { t }
| LPAREN; t = anonymous_pred; RPAREN { t }
type_term:
| c = constant { TConst (fix_church c) }
| hd = constant; args = nonempty_list(atype_term) { TApp (hd, List.hd args, List.tl args) }
| hd = type_term; ARROW; t = type_term { TArr (hd, t) }
| c = constant { { tloc = loc $loc; tit = TConst (fix_church c) } }
| hd = constant; args = nonempty_list(atype_term) { { tloc = loc $loc; tit = TApp (hd, List.hd args, List.tl args) } }
| hd = type_term; ARROW; t = type_term { { tloc = loc $loc; tit = TArr (hd, t) } }
| LPAREN; t = anonymous_pred; RPAREN { t }
| LPAREN; t = type_term; RPAREN { t }

kind_term:
| TYPE { TConst (Func.from_string "type") }
| TYPE; ARROW; t = kind_term { TArr (TConst (Func.from_string "type"), t) }
| TYPE { { tloc = loc $loc; tit = TConst (Func.from_string "type") } }
| x = TYPE; ARROW; t = kind_term { { tloc = loc $loc; tit = TArr ({ tloc = loc $loc(x); tit = TConst (Func.from_string "type") }, t) } }

macro:
| MACRO; m = term; VDASH; b = term {
Expand All @@ -222,7 +224,7 @@ typeabbrev:
| TYPEABBREV; a = abbrevform; t = type_term {
let name, args = a in
let nparams = List.length args in
let mkLam (n,_) body = TypeAbbreviation.Lam (n, body) in
let mkLam (n,l) body = TypeAbbreviation.Lam (n, l, body) in
let value = List.fold_right mkLam args (Ty t) in
{ TypeAbbreviation.name = name;
nparams = nparams;
Expand Down
4 changes: 3 additions & 1 deletion src/utils/util.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -232,7 +232,9 @@ let rec for_all3b p l1 l2 bl b =
;;

type arg_mode = Input | Output
and mode_aux =
[@@deriving show, ord]

type mode_aux =
| Fo of arg_mode
| Ho of arg_mode * mode
and mode = mode_aux list
Expand Down
4 changes: 3 additions & 1 deletion src/utils/util.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,7 +118,9 @@ val for_all2 : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
val for_all23 : argsdepth:int -> (argsdepth:int -> matching:bool -> 'x -> 'y -> 'z -> 'a -> 'a -> bool) -> 'x -> 'y -> 'z -> 'a list -> 'a list -> bool
val for_all3b : ('a -> 'a -> bool -> bool) -> 'a list -> 'a list -> bool list -> bool -> bool
type arg_mode = Input | Output
and mode_aux =
[@@deriving show, ord]

type mode_aux =
| Fo of arg_mode
| Ho of arg_mode * mode
and mode = mode_aux list
Expand Down

0 comments on commit b569aa0

Please sign in to comment.