Skip to content

Commit

Permalink
[compiler] modes refactor: typeAss's arrow has mode + remove pred fro…
Browse files Browse the repository at this point in the history 
…m ScopedTypeExpression

- The typechecker assigns types to terms, this types have modes:
  the node arrow has carries the mode
- To simplify translation from ScopeTypeExpression to TypeAssignement,
  the node Pred has disappeard in favour of a combination of Arrow with mode
  and Prop
- The type mode_arg and all the related auxiliary functions
  have been replaced with Mode.t where Mode is a global
  module in Utils used by Ast, Compiler, Runtime etc...
  the goal is to have a easier way to work with modes
- The DeterminacyChecker benefits from modes attached to types since it has
  no more to find them into the mode map: they are already referenced in the type
  of terms taken into account
- TODO: check if variable representing partial application of predicates
  have correct mode: e.g. in `X = map []`, the variable `X` has the type
  of `X` ha good associated mode?
  • Loading branch information
@FissoreD
FissoreD committed Dec 5, 2024
1 parent f5fdad6 commit 21b0106
Show file tree
Hide file tree
Showing 16 changed files with 238 additions and 227 deletions.
67 changes: 39 additions & 28 deletions src/compiler/compiler.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -227,7 +227,7 @@ and pbody = {
kinds : Arity.t F.Map.t;
types : TypeList.t F.Map.t;
type_abbrevs : (F.t * ScopedTypeExpression.t) list;
modes : (mode * Loc.t) F.Map.t;
modes : (Mode.hos * Loc.t) F.Map.t;
body : block list;
symbols : F.Set.t;
}
Expand All @@ -250,7 +250,7 @@ type unchecked_signature = {
kinds : Arity.t F.Map.t;
types : TypeList.t F.Map.t;
type_abbrevs : (F.t * ScopedTypeExpression.t) list;
modes : (mode * Loc.t) F.Map.t;
modes : (Mode.hos * Loc.t) F.Map.t;
type_uf : IDPosUf.t
}
[@@deriving show]
Expand All @@ -273,7 +273,7 @@ module Assembled = struct
kinds : Arity.t F.Map.t;
types : TypeAssignment.overloaded_skema_with_id F.Map.t;
type_abbrevs : (TypeAssignment.skema_w_id * Loc.t) F.Map.t;
modes : (mode * Loc.t) F.Map.t;
modes : (Mode.hos * Loc.t) F.Map.t;
functional_preds: Determinacy_checker.t;
type_uf : IDPosUf.t
}
Expand All @@ -290,7 +290,7 @@ module Assembled = struct

builtins : Builtins.t;
prolog_program : index;
indexing : (mode * indexing) C.Map.t;
indexing : (Mode.hos * indexing) C.Map.t;
chr : CHR.t;

symbols : SymbolMap.table;
Expand Down Expand Up @@ -776,7 +776,7 @@ let get_mtm, set_mtm, _drop_mtm, update_mtm =
module Scope_Quotation_Macro : sig

val run : State.t -> toplevel_macros:macro_declaration -> Ast.Structured.program -> Scoped.program
val check_duplicate_mode : F.t -> (mode * Loc.t) -> (mode * Loc.t) F.Map.t -> unit
val check_duplicate_mode : F.t -> (Mode.hos * Loc.t) -> (Mode.hos * Loc.t) F.Map.t -> unit
val scope_loc_term : state:State.t -> Ast.Term.t -> ScopedTerm.t

end = struct
Expand All @@ -803,19 +803,25 @@ end = struct
let c = (F.show f).[0] in
c = '@'

let rec scope_tye ctx ~loc t : ScopedTypeExpression.t_ =
let rec pred2arr ctx ~loc func = function
| [] -> ScopedTypeExpression.Prop func
| (m,x)::xs -> Arrow (m,NotVariadic,scope_loc_tye ctx x, {loc; it=pred2arr ctx ~loc func xs})

and scope_tye ctx ~loc t : ScopedTypeExpression.t_ =
match t with
| Ast.TypeExpression.TConst c when F.show c = "prop" -> Pred (Relation,[])
| Ast.TypeExpression.TConst c when F.show c = "prop" -> Prop Relation
| TConst c when F.show c = "any" -> Any
| TConst c when F.Set.mem c ctx -> Const(Bound elpi_language,c)
| TConst c -> Const(Scope.mkGlobal (),c)
| TApp(c,x,[y]) when F.show c = "variadic" ->
Arrow(Variadic,scope_loc_tye ctx x,scope_loc_tye ctx y)
Arrow(Output, Variadic,scope_loc_tye ctx x,scope_loc_tye ctx y)
| TApp(c,x,xs) ->
if F.Set.mem c ctx || is_uvar_name c then error ~loc "type schema parameters cannot be type formers";
App(c,scope_loc_tye ctx x, List.map (scope_loc_tye ctx) xs)
| TPred(m,xs) -> Pred(m,List.map (fun (m,t) -> m, scope_loc_tye ctx t) xs)
| TArr(s,t) -> Arrow(NotVariadic, scope_loc_tye ctx s, scope_loc_tye ctx t)
| TPred((m:Ast.Structured.functionality),xs) ->
pred2arr ctx ~loc m xs
(* Pred(m,List.map (fun (m,t) -> m, scope_loc_tye ctx t) xs) *)
| TArr(s,t) -> Arrow(Output, NotVariadic, scope_loc_tye ctx s, scope_loc_tye ctx t)
and scope_loc_tye ctx { tloc; tit } = { loc = tloc; it = scope_tye ctx ~loc:tloc tit }
let scope_loc_tye ctx (t: Ast.Structured.functionality Ast.TypeExpression.t) =
scope_loc_tye ctx t
Expand All @@ -830,9 +836,8 @@ end = struct
| Const(Bound _, _) -> assert false (* there are no binders yet *)
| Const(Global _,c) when is_uvar_name c -> F.Set.add c e
| Const(Global _,_) -> e
| Any -> e
| Arrow(_,x,y) -> aux (aux e x) y
| Pred(_,l) -> List.fold_left aux e (List.map snd l)
| Any | Prop _ -> e
| Arrow(_,_,x,y) -> aux (aux e x) y
in
aux F.Set.empty value in
let value = scope_loc_tye vars ty in
Expand Down Expand Up @@ -957,21 +962,27 @@ end = struct
match F.Map.find_opt name map with
| Some (mode2,loc2) when mode2 <> mode ->
error ~loc
(Format.asprintf "Duplicate mode declaration for %a (also at %a)\n Mode1 = %a\n Mode2 = %a" F.pp name Loc.pp loc2 pp_mode mode pp_mode mode2)
(Format.asprintf "Duplicate mode declaration for %a (also at %a)\n Mode1 = %a\n Mode2 = %a" F.pp name Loc.pp loc2 Mode.pp_hos mode Mode.pp_hos mode2)
| _ -> ()

let compile_mode_aux modes ({value;name} :ScopedTypeExpression.t) =
let fix_mode = function Ast.Mode.Input -> Util.Input | Ast.Mode.Output -> Util.Output in
let rec type_to_mode = function
| m, ScopedTypeExpression.{it = Pred(_,l)} -> Ho(fix_mode m,List.map type_to_mode l)
| m, _ -> Fo (fix_mode m) in
let rec to_mode_ho (m, ty) =
match flatten_arrow [] ty with
| None -> Mode.Fo m
| Some l -> Mode.Ho (m, List.rev_map to_mode_ho l)
and flatten_arrow acc = function
| ScopedTypeExpression.Prop _ -> Some acc
| Any | Const _ | App _ -> None
| Arrow (m,_,a,b) -> flatten_arrow ((m,a.it)::acc) b.it in
let rec type_to_mode_under_abs = function
| ScopedTypeExpression.Lam (_,b) -> type_to_mode_under_abs b
| Ty {it = Pred (_,l);loc} ->
let args = List.map type_to_mode l in
check_duplicate_mode name (args,loc) modes;
F.Map.add name (args,loc) modes
| Ty _ -> modes
| Ty {it;loc} ->
match flatten_arrow [] it with
| None -> modes
| Some l ->
let args = List.rev_map to_mode_ho l in
check_duplicate_mode name (args,loc) modes;
F.Map.add name (args,loc) modes
in
type_to_mode_under_abs value

Expand Down Expand Up @@ -1053,7 +1064,7 @@ end = struct
toplevel_macros,
{ Scoped.types; kinds; type_abbrevs; modes; body; symbols }

and compile_body macros kinds types type_abbrevs (modes : (mode * Loc.t) F.Map.t) (defs : F.Set.t) state = function
and compile_body macros kinds types type_abbrevs (modes : (Mode.hos * Loc.t) F.Map.t) (defs : F.Set.t) state = function
| [] -> kinds, types, type_abbrevs, modes, defs, []
| Clauses cl :: rest ->
let compiled_cl = List.map (compile_clause state macros) cl in
Expand Down Expand Up @@ -1112,9 +1123,9 @@ module Flatten : sig

val run : State.t -> Scoped.program -> Flat.program
val merge_modes :
(mode * Loc.t) F.Map.t ->
(mode * Loc.t) F.Map.t ->
(mode * Loc.t) F.Map.t
(Mode.hos * Loc.t) F.Map.t ->
(Mode.hos * Loc.t) F.Map.t ->
(Mode.hos * Loc.t) F.Map.t
val merge_kinds :
Arity.t F.Map.t ->
Arity.t F.Map.t ->
Expand Down Expand Up @@ -1443,7 +1454,7 @@ end = struct
else unknown in
(* if String.starts_with ~prefix:"File \"<" (Loc.show loc) then Format.eprintf "The clause is %a@." ScopedTerm.pp body; *)
let spilled = {clause with body = if needs_spilling then Spilling.main body else body; needs_spilling = false} in
if typecheck then Determinacy_checker.check_clause ~uf:type_uf ~loc ~env:functional_preds spilled.body ~modes;
if typecheck then Determinacy_checker.check_clause ~uf:type_uf ~loc ~env:functional_preds spilled.body;
unknown, spilled :: clauses) (F.Map.empty,[]) clauses in

let clauses = List.rev clauses in
Expand Down
106 changes: 58 additions & 48 deletions src/compiler/compiler_data.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -97,10 +97,10 @@ module ScopedTypeExpression = struct

type t_ =
| Any
| Prop of Ast.Structured.functionality
| Const of Scope.t * F.t
| App of F.t * e * e list
| Arrow of Ast.Structured.variadic * e * e
| Pred of Ast.Structured.functionality * (Ast.Mode.t * e) list
| Arrow of Mode.t * Ast.Structured.variadic * e * e
and e = { it : t_; loc : Loc.t }
[@@ deriving show]

Expand All @@ -111,20 +111,32 @@ module ScopedTypeExpression = struct
let app = 1

let lvl_of = function
| Arrow _ | Pred _ -> arrs
| Arrow _ -> arrs
| App _ -> app
| _ -> 2

let rec is_prop = function
| Prop f -> Some f
| Any | Const _ | App _ -> None
| Arrow(_,_,_,t) -> is_prop t.it

let rec pretty_e fmt = function
| Any -> fprintf fmt "any"
| Const(_,c) -> F.pp fmt c
| Prop _ -> fprintf fmt "prop"
| App(f,x,xs) -> fprintf fmt "@[<hov 2>%a@ %a@]" F.pp f (Util.pplist (pretty_e_parens ~lvl:app) " ") (x::xs)
| Arrow(NotVariadic,s,t) -> fprintf fmt "@[<hov 2>%a ->@ %a@]" (pretty_e_parens ~lvl:arrs) s pretty_e_loc t
| Arrow(Variadic,s,t) -> fprintf fmt "%a ..-> %a" (pretty_e_parens ~lvl:arrs) s pretty_e_loc t
| Pred(_,[]) -> fprintf fmt "prop"
| Pred(_,l) -> fprintf fmt "pred %a" (Util.pplist pretty_ie ", ") l
and pretty_ie fmt (i,e) =
fprintf fmt "%s:%a" (match i with Ast.Mode.Input -> "i" | Output -> "o") pretty_e_loc e
| Arrow(m,v,s,t) as p ->
(match is_prop p with
| None -> fprintf fmt "@[<hov 2>%a ->@ %a@]" (pretty_e_parens ~lvl:arrs) s pretty_e_loc t
| Some Function -> fprintf fmt "@[<hov 2>func%a@]" (pretty_prop m v s t) ()
| Some Relation -> fprintf fmt "@[<hov 2>pred%a@]" (pretty_prop m v s t) ()
)

and pretty_prop m v l r fmt () =
let show_var = function Ast.Structured.Variadic -> ".." | _ -> "" in
match r.it with
| Prop _ -> fprintf fmt "."
| _ -> fprintf fmt "%a:%a %s->@ %a" Mode.pp_short m pretty_e_loc l (show_var v) pretty_e_loc r
and pretty_e_parens ~lvl fmt = function
| t when lvl >= lvl_of t.it -> fprintf fmt "(%a)" pretty_e_loc t
| t -> pretty_e_loc fmt t
Expand All @@ -136,7 +148,7 @@ module ScopedTypeExpression = struct
| SimpleType.Any -> Any
| Con c -> Const(Scope.mkGlobal (),c)
| App(c,x,xs) -> App(c,of_simple_type_loc x,List.map of_simple_type_loc xs)
| Arr(s,t) -> Arrow(NotVariadic,of_simple_type_loc s, of_simple_type_loc t)
| Arr(s,t) -> Arrow(Output, NotVariadic,of_simple_type_loc s, of_simple_type_loc t)
and of_simple_type_loc { it; loc } = { it = of_simple_type it; loc }

type v_ =
Expand All @@ -152,9 +164,9 @@ module ScopedTypeExpression = struct
| Const(Global _ as b1,c1), Const(Global _ as b2,c2) -> Scope.compare b1 b2 == 0 && F.equal c1 c2
| Const(Bound l1,c1), Const(Bound l2,c2) -> Scope.compare_language l1 l2 == 0 && eq_var ctx l1 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(b1,s1,t1), Arrow(b2,s2,t2) -> b1 = b2 && 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
| Arrow(m1,b1,s1,t1), Arrow(m2,b2,s2,t2) -> Mode.compare m1 m2 == 0 && b1 = b2 && eqt ctx s1 s2 && eqt ctx t1 t2
| Any, Any -> true
| Prop _, Prop _ -> true
| _ -> false

let rec eq ctx t1 t2 =
Expand All @@ -172,7 +184,7 @@ module ScopedTypeExpression = struct
if it' == it then orig else { it = it'; loc }
and smart_map_scoped_ty f orig =
match orig with
| Any -> orig
| Any | Prop _ -> orig
| Const((Scope.Bound _| Scope.Global { escape_ns = true }),_) -> orig
| Const(Scope.Global _ as g,c) ->
let c' = f c in
Expand All @@ -182,15 +194,10 @@ module ScopedTypeExpression = struct
let x' = smart_map_scoped_loc_ty f x in
let xs' = smart_map (smart_map_scoped_loc_ty f) xs in
if c' == c && x' == x && xs' == xs then orig else App(c',x',xs')
| Arrow(v,x,y) ->
| Arrow(m,v,x,y) ->
let x' = smart_map_scoped_loc_ty f x in
let y' = smart_map_scoped_loc_ty f y in
if x' == x && y' == y then orig else Arrow(v,x',y')
| Pred(c,l) ->
let l' = smart_map (fun (m,x as orig) ->
let x' = smart_map_scoped_loc_ty f x in
if x' == x then orig else m,x') l in
if l' == l then orig else Pred(c,l')
if x' == x && y' == y then orig else Arrow(m,v,x',y')

let rec smart_map_tye f = function
| Lam(c,t) as orig ->
Expand Down Expand Up @@ -255,7 +262,7 @@ module TypeAssignment = struct
| Any
| Cons of F.t
| App of F.t * 'a t_ * 'a t_ list
| Arr of Ast.Structured.variadic * 'a t_ * 'a t_
| Arr of Mode.t * Ast.Structured.variadic * 'a t_ * 'a t_
| UVar of 'a
[@@ deriving show, fold, ord]

Expand All @@ -279,7 +286,7 @@ module TypeAssignment = struct
let rec subst map = function
| (Prop _ | Any | Cons _) as x -> x
| App(c,x,xs) -> App (c,subst map x,List.map (subst map) xs)
| Arr(v,s,t) -> Arr(v,subst map s, subst map t)
| Arr(m,v,s,t) -> Arr(m,v,subst map s, subst map t)
| UVar c ->
match map c with
| Some x -> x
Expand Down Expand Up @@ -350,7 +357,7 @@ module TypeAssignment = struct
| UVar _ -> raise Not_monomorphic
| (Prop _ | Any | Cons _) as v -> v
| App(c,x,xs) -> App(c,map x, List.map map xs)
| Arr(b,s,t) -> Arr(b,map s,map t)
| Arr(m,b,s,t) -> Arr(m,b,map s,map t)
in
try
let t = map t in
Expand All @@ -360,7 +367,7 @@ module TypeAssignment = struct
let rec is_arrow_to_prop = function
| Prop _ -> true
| Any | Cons _ | App _ -> false
| Arr(_,_,t) -> is_arrow_to_prop t
| Arr(_,_,_,t) -> is_arrow_to_prop t
| UVar _ -> false

let rec is_predicate = function
Expand All @@ -372,30 +379,33 @@ module TypeAssignment = struct
| Overloaded l -> List.exists (fun (_,x) -> is_predicate x) l

open Format

let arrs = 0
let app = 1

let lvl_of = function
| Arr _ -> arrs
| App _ -> app
| _ -> 2

let rec pretty fmt = function
| Prop Relation -> fprintf fmt "prop"
| Prop Function -> fprintf fmt "fprop"
| Any -> fprintf fmt "any"
| Cons c -> F.pp fmt c
| App(f,x,xs) -> fprintf fmt "@[<hov 2>%a@ %a@]" F.pp f (Util.pplist (pretty_parens ~lvl:app) " ") (x::xs)
| Arr(NotVariadic,s,t) -> fprintf fmt "@[<hov 2>%a ->@ %a@]" (pretty_parens ~lvl:arrs) s pretty t
| Arr(Variadic,s,t) -> fprintf fmt "%a ..-> %a" (pretty_parens ~lvl:arrs) s pretty t
| UVar m when MutableOnce.is_set m -> pretty fmt @@ deref m
| UVar m -> MutableOnce.pretty fmt m
and pretty_parens ~lvl fmt = function
| UVar m when MutableOnce.is_set m -> pretty_parens ~lvl fmt @@ deref m
| t when lvl >= lvl_of t -> fprintf fmt "(%a)" pretty t
| t -> pretty fmt t
let pretty fmt t = Format.fprintf fmt "@[%a@]" pretty t
let pretty fmt tm =

let arrs = 0 in
let app = 1 in

let lvl_of = function
| Arr _ -> arrs
| App _ -> app
| _ -> 2 in

let rec pretty fmt = function
| Prop Relation -> fprintf fmt "prop"
| Prop Function -> fprintf fmt "fprop"
| Any -> fprintf fmt "any"
| Cons c -> F.pp fmt c
| App(f,x,xs) -> fprintf fmt "@[<hov 2>%a@ %a@]" F.pp f (Util.pplist (pretty_parens ~lvl:app) " ") (x::xs)
| Arr(m,NotVariadic,s,t) -> fprintf fmt "@[<hov 2>%a:%a ->@ %a@]" Mode.pp_short m (pretty_parens ~lvl:arrs) s pretty t
| Arr(m,Variadic,s,t) -> fprintf fmt "%a:%a ..-> %a" Mode.pp_short m (pretty_parens ~lvl:arrs) s pretty t
| UVar m when MutableOnce.is_set m -> pretty fmt @@ deref m
| UVar m -> MutableOnce.pretty fmt m
and pretty_parens ~lvl fmt = function
| UVar m when MutableOnce.is_set m -> pretty_parens ~lvl fmt @@ deref m
| t when lvl >= lvl_of t -> fprintf fmt "(%a)" pretty t
| t -> pretty fmt t in
let pretty fmt t = Format.fprintf fmt "@[%a@]" pretty t
in
pretty fmt tm

let vars_of (Val t) = fold_t_ (fun xs x -> if MutableOnce.is_set x then xs else x :: xs) [] t

Expand Down
Loading

0 comments on commit 21b0106

Please sign in to comment.