compiler: cleanup

Author: gares

src/compiler/compiler.ml

@@ -747,11 +747,11 @@ module CustomFunctorCompilation = struct
 
   let scope_singlequote ~loc state x = 
     match State.get singlequote state with
-    | None -> ScopedTerm.(App(ScopedTerm.mk_global_const ~name:x ~loc,[]))
+    | None -> ScopedTerm.(App(ScopedTerm.mk_global_const x ~loc,[]))
     | Some (language,f) -> ScopedTerm.unlock @@ ScopedTerm.of_simple_term_loc @@ f ~language state loc (F.show x)
   let scope_backtick ~loc state x =
     match State.get backtick state with
-    | None -> ScopedTerm.(App(ScopedTerm.mk_global_const ~name:x ~loc,[]))
+    | None -> ScopedTerm.(App(ScopedTerm.mk_global_const x ~loc,[]))
     | Some (language,f) -> ScopedTerm.unlock @@ ScopedTerm.of_simple_term_loc @@ f ~language state loc (F.show x)
 end
 
@@ -887,11 +887,11 @@ end = struct
         scope_term_macro ~loc ~state c []
     | Const c when F.Set.mem c ctx -> ScopedTerm.(App(ScopedTerm.mk_bound_const ~lang:elpi_language c ~loc,[]))
     | Const c ->
-        if is_uvar_name c then ScopedTerm.Var(ScopedTerm.mk_bound_const ~lang:elpi_var c ~loc,[])
+        if is_uvar_name c then ScopedTerm.UVar(ScopedTerm.mk_uvar c ~loc,[])
         else if CustomFunctorCompilation.is_singlequote c then CustomFunctorCompilation.scope_singlequote ~loc state c
         else if CustomFunctorCompilation.is_backtick c then CustomFunctorCompilation.scope_backtick ~loc state c
-        else if is_global c then ScopedTerm.(App(mk_const ~scope:(Scope.mkGlobal ~escape_ns:true ()) (of_global c) ~loc,[]))
-        else ScopedTerm.(App(mk_const ~scope:(Scope.mkGlobal ()) c ~loc,[]))
+        else if is_global c then ScopedTerm.(App(mk_global_const ~escape_ns:true (of_global c) ~loc,[]))
+        else ScopedTerm.(App(mk_global_const ~loc c,[]))
     | App ({ it = App (f,l1) },l2) -> scope_term ~state ctx ~loc (App(f, l1 @ l2))
     | App ({ it = Parens f },l) -> scope_term ~state ctx ~loc (App(f, l))
     | App({ it = Const c }, [x]) when F.equal c F.spillf ->
@@ -913,9 +913,9 @@ end = struct
          else
           let bound = F.Set.mem c ctx in
           if bound then ScopedTerm.App(ScopedTerm.mk_bound_const ~lang:elpi_language c ~loc:cloc, xs)
-          else if is_uvar_name c then ScopedTerm.Var(ScopedTerm.mk_bound_const ~lang:elpi_var c ~loc:cloc,xs)
-          else if is_global c then ScopedTerm.App(ScopedTerm.mk_const ~scope:(Scope.mkGlobal ~escape_ns:true ()) (of_global c) ~loc:cloc,xs)
-          else ScopedTerm.App(ScopedTerm.mk_const ~scope:(Scope.mkGlobal ()) c ~loc:cloc, xs)
+          else if is_uvar_name c then ScopedTerm.UVar(ScopedTerm.mk_uvar c ~loc:cloc,xs)
+          else if is_global c then ScopedTerm.App(ScopedTerm.mk_global_const ~escape_ns:true (of_global c) ~loc:cloc,xs)
+          else ScopedTerm.App(ScopedTerm.mk_global_const c ~loc:cloc, xs)
     | Cast (t,ty) ->
         let t = scope_loc_term ~state ctx t in
         let ty = scope_loc_tye F.Set.empty (RecoverStructure.structure_type_expression ty.Ast.TypeExpression.tloc Ast.Structured.Relation valid_functional ty) in
@@ -926,7 +926,7 @@ end = struct
     | Lam (c,cloc,ty,b) ->
         if has_dot c then error ~loc "Bound variables cannot contain the namespaec separator '.'";
         let ty = ty |> Option.map (fun ty -> scope_loc_tye F.Set.empty (RecoverStructure.structure_type_expression ty.Ast.TypeExpression.tloc Ast.Structured.Relation valid_functional ty)) in
-        let name = Some (ScopedTerm.mk_const ~scope:elpi_language c ~loc:cloc) in
+        let name = Some (ScopedTerm.mk_binder ~lang:elpi_language c ~loc:cloc) in
         ScopedTerm.Lam (name,ty,scope_loc_term ~state (F.Set.add c ctx) b)
     | CData c -> ScopedTerm.CData c (* CData.hcons *)
     | App ({ it = Lam _},_) ->
@@ -1173,9 +1173,9 @@ module Flatten : sig
           let b' = aux_loc b in
           let ty' = option_smart_map (ScopedTypeExpression.smart_map_scoped_loc_ty tyf) ty in
           if b == b' && ty' == ty then it else Lam(n,ty',b')
-      | Var(c,l) ->
+      | UVar(c,l) ->
           let l' = smart_map aux_loc l in
-          if l == l' then it else Var(c,l')
+          if l == l' then it else UVar(c,l')
       | Cast(t,ty) ->
           let t' = aux_loc t in
           let ty' = ScopedTypeExpression.smart_map_scoped_loc_ty tyf ty in
@@ -1642,7 +1642,7 @@ end = struct
     let allocate_global_symbol = allocate_global_symbol types symb state in
     let push_bound (n,ctx) c = (n+1,Scope.Map.add c n ctx) in
     let push_unnamed_bound (n,ctx) = (n+1,ctx) in
-    let push ctx : string ScopedTerm.const option -> 'a = function
+    let push ctx : ScopedTerm.binder option -> 'a = function
       | None -> push_unnamed_bound ctx
       | Some { scope = l; name = x } -> push_bound ctx (x,l) in
     let open ScopedTerm in
@@ -1690,7 +1690,7 @@ end = struct
           let xs = List.map (todbl ctx) xs in
           D.mkApp c x xs
       (* holes *)
-      | Var({ name = c },xs) ->
+      | UVar({ name = c },xs) ->
           let xs = List.map (todbl ctx) xs in
           R.mkAppArg (allocate_arg c) 0 xs
       | Discard -> D.mkDiscard
@@ -2560,7 +2560,7 @@ let info_of_scoped_term ~types t =
   let rec aux loc ty = function
     | Impl(_,locs,l,r) -> log_bsymb locs Global_symbols.impl; log_ty loc ty; aux_loc l; aux_loc r
     | Discard -> log_ty loc ty
-    | Var({ scope = s; ty = tys; loc = locs},args) -> if args <> [] then log_ty loc ty; log_symb locs s (TypeAssignment.deref_opt tys); List.iter aux_loc args
+    | UVar({ scope = s; ty = tys; loc = locs},args) -> if args <> [] then log_ty loc ty; log_symb locs (Scope.Bound elpi_var) (TypeAssignment.deref_opt tys); List.iter aux_loc args
     | App({ scope = s; ty = tys; loc = locs},args) -> if args <> [] then log_ty loc ty; log_symb locs s (TypeAssignment.deref_opt tys); List.iter aux_loc args
     | CData _ -> log_ty loc ty
     | Spill(t,_) -> log_ty loc ty; aux_loc t

src/compiler/compiler_data.ml

@@ -909,17 +909,21 @@ module ScopedTerm = struct
 
   end
 
-  type 'scope const = { scope: 'scope; name: F.t; ty: TypeAssignment.t MutableOnce.t; loc : Loc.t }
-  [@@ deriving show]
-
-  let mk_const ?(ty = MutableOnce.make F.dummyname) ~scope name ~loc : 'a const = { scope; name; ty; loc } 
-  let mk_bound_const ?ty ~lang name ~loc = mk_const ?ty ~scope:(Scope.Bound lang) name ~loc
-
-  let bind_const (n : string const) : Scope.t const = { n with scope = Scope.Bound n.scope }
-
-  let mk_global_const ~name ~loc : 'a const = mk_const ~scope:(Scope.mkGlobal ()) name ~loc
-  let const_of_symb ~types symb ~loc : 'a const = mk_const ~scope:(Scope.mkResolvedGlobal types symb) (Symbol.get_func symb) ~loc
-  let clone_const ?(clone_scope = Fun.id) {scope;name; loc } = mk_const ~scope:(clone_scope scope) name ~loc
+  type 'scope w_ty_loc = { scope: 'scope; name: F.t; ty: TypeAssignment.t MutableOnce.t; loc : Loc.t } [@@ deriving show]
+  type const = Scope.t w_ty_loc [@@ deriving show]
+  type uvar = unit w_ty_loc [@@ deriving show]
+  type binder = string w_ty_loc [@@ deriving show]
+
+  let mk_w_ty_loc ?(ty = MutableOnce.make F.dummyname) ~scope name ~loc : 'a w_ty_loc =
+    { scope; name; ty; loc } 
+  let mk_global_const ?escape_ns ~loc name : const = mk_w_ty_loc ~scope:(Scope.mkGlobal ?escape_ns ()) name ~loc
+  let mk_bound_const ?ty ~lang name ~loc = mk_w_ty_loc ?ty ~scope:(Scope.Bound lang) name ~loc
+  let mk_uvar ?ty name ~loc = mk_w_ty_loc ?ty ~scope:() name ~loc
+  let mk_binder ?ty ~lang name ~loc = mk_w_ty_loc ?ty ~scope:lang ~loc name
+  let bind_const (n : binder) : const = { n with scope = Scope.Bound n.scope }
+
+  let const_of_symb ~types symb ~loc : const = mk_w_ty_loc ~scope:(Scope.mkResolvedGlobal types symb) (Symbol.get_func symb) ~loc
+  let clone_const ?(clone_scope = Fun.id) {scope;name; loc } = mk_w_ty_loc ~scope:(clone_scope scope) name ~loc
 
   type spill_info =
     | NoInfo (* before typing *)
@@ -930,9 +934,9 @@ module ScopedTerm = struct
   type t_ =
    | Impl of SimpleTerm.impl_kind * Loc.t * t * t (* `Impl(true,t1,t2)` ≡ `t1 => t2` and `Impl(false,t1,t2)` ≡ `t1 :- t2` *)
    | Discard
-   | Var of Scope.t const * t list
-   | App of Scope.t const * t list
-   | Lam of (Scope.language const) option * ScopedTypeExpression.e option * t
+   | UVar of uvar * t list
+   | App of const * t list
+   | Lam of binder option * ScopedTypeExpression.e option * t
 
    | CData of CData.t
    | Spill of t * spill_info ref
@@ -949,14 +953,14 @@ module ScopedTerm = struct
 
   let lvl_of = function
     | App(_, (_::_)) -> app
-    | Var (_, (_::_)) -> app
+    | UVar (_, (_::_)) -> app
     | Lam _ -> lam
     | _ -> 2
 
   let get_lam_name = function None -> F.from_string "_" | Some (n,_) -> n
   let mk_empty_lam_type = function
     | None -> None
-    | Some (name, loc, scope) -> Some (mk_const name ~scope ~loc)
+    | Some (name, loc, scope) -> Some (mk_w_ty_loc name ~scope ~loc)
 
   (* The type of the object being constructed is irrelevant since 
     build_infix_constant is used in the pretty printer of term and the type
@@ -994,8 +998,8 @@ module ScopedTerm = struct
     | App({ name = f },x::xs) when F.equal F.pif f || F.equal F.sigmaf f -> fprintf fmt "@[<hov 2>%a@ %a@]" F.pp f (Util.pplist ~pplastelem:(pretty_parens_lam ~lvl:app)  (pretty_parens ~lvl:app) " ") (x::xs)
     | App({ scope = Global _; name = f } as n,x::xs) when is_infix_constant f -> fprintf fmt "%a" (Util.pplist ~boxed:true (pretty_parens ~lvl:0) " ") (intersperse (build_infix_constant n) (x::xs))
     | App({ name = f },x::xs) -> fprintf fmt "@[<hov 2>%a@ %a@]" F.pp f (Util.pplist ~boxed:true (pretty_parens ~lvl:app) " ") (x::xs)
-    | Var({ name = f },[]) -> fprintf fmt "@[%a@]" F.pp f
-    | Var({ name = f },xs) -> fprintf fmt "@[%a@ %a@]" F.pp f (Util.pplist ~boxed:true (pretty_parens ~lvl:app) " ") xs
+    | UVar({ name = f },[]) -> fprintf fmt "@[%a@]" F.pp f
+    | UVar({ name = f },xs) -> fprintf fmt "@[%a@ %a@]" F.pp f (Util.pplist ~boxed:true (pretty_parens ~lvl:app) " ") xs
     | CData c -> fprintf fmt "%a" CData.pp c
     | Spill (t,{ contents = NoInfo }) -> fprintf fmt "{%a}" pretty t
     | Spill (t,{ contents = Main _ }) -> fprintf fmt "{%a}" pretty t
@@ -1011,7 +1015,7 @@ module ScopedTerm = struct
     let rec eq ctx t1 t2 =
       match t1.it, t2.it with
       | Discard, Discard -> true
-      | Var(n1,l1), Var(n2,l2) -> eq_uvar ctx n1.name n2.name && Util.for_all2 (eq ctx) l1 l2
+      | UVar(n1,l1), UVar(n2,l2) -> eq_uvar ctx n1.name n2.name && Util.for_all2 (eq ctx) l1 l2
       | App({ scope = Global _ as b1; name = c1},xs), App({ scope = Global _ as b2; name = c2 },ys) -> Scope.equal env b1 b2 && F.equal c1 c2 && Util.for_all2 (eq ctx) xs ys
       | App({ scope = Bound l1; name = c1 },xs), App({ scope = Bound l2; name = c2 },ys) -> l1 = l2 && eq_var ctx l1 c1 c2 && Util.for_all2 (eq ctx) xs ys
       | Lam(None, ty1,b1), Lam (None,ty2, b2) -> eq ctx b1 b2 && (not types || Option.equal (ScopedTypeExpression.eqt env (empty ())) ty1 ty2)
@@ -1041,7 +1045,7 @@ module ScopedTerm = struct
   let rec of_simple_term ~loc = function
     | SimpleTerm.Discard -> Discard
     | Impl(b,loc,t1,t2) -> Impl(b,loc,of_simple_term_loc t1, of_simple_term_loc t2)
-    | Const(scope,c) -> App (mk_const ~scope c ~loc,[])
+    | Const(scope,c) -> App (mk_w_ty_loc ~scope c ~loc,[])
     | Opaque c -> CData c
     | Cast(t,ty) -> Cast(of_simple_term_loc t, ScopedTypeExpression.of_simple_type_loc ty)
     | Lam(c,ty,t) -> Lam(mk_empty_lam_type c,Option.map ScopedTypeExpression.of_simple_type_loc ty, of_simple_term_loc t)
@@ -1050,8 +1054,8 @@ module ScopedTerm = struct
         | [y] -> Impl(SimpleTerm.func_to_impl_kind c,cloc,of_simple_term_loc x, of_simple_term_loc y)
         | _ -> error ~loc "Use of App for Impl is allowed, but the length of the list in 3rd position must be 1"
       end
-    | App(s,c,cloc,x,xs) -> App(mk_const ~scope:s c ~loc, of_simple_term_loc x :: List.map of_simple_term_loc xs)
-    | Var(c,cloc,xs) -> Var(mk_bound_const ~lang:elpi_var c ~loc:cloc,List.map of_simple_term_loc xs)
+    | App(s,c,cloc,x,xs) -> App(mk_w_ty_loc ~scope:s c ~loc, of_simple_term_loc x :: List.map of_simple_term_loc xs)
+    | Var(c,cloc,xs) -> UVar(mk_uvar c ~loc:cloc,List.map of_simple_term_loc xs)
   and of_simple_term_loc { SimpleTerm.it; loc } =
     match it with
     | Opaque c when is_scoped_term c -> out_scoped_term c
@@ -1074,7 +1078,7 @@ module ScopedTerm = struct
       | Lam(v,tya,t) -> Lam(v,tya,rename_loc l c d t)
       | Spill(t,i) -> Spill(rename_loc l c d t,i)
       | Cast(t,ty) -> Cast(rename_loc l c d t,ty)
-      | Var(v,xs) -> Var(v,List.map (rename_loc l c d) xs)
+      | UVar(v,xs) -> UVar(v,List.map (rename_loc l c d) xs)
       | Discard | CData _ -> t
     and rename_loc l c d { it; ty; loc } = { it = rename l c d it; ty; loc } 
 
@@ -1083,7 +1087,7 @@ module ScopedTerm = struct
       | Impl (b, loc, l, r) -> Impl(b, loc, clone_loc ~loc l, clone_loc ~loc r)
       | Lam (n,ty,bo) -> Lam(Option.map clone_const n, ty, clone_loc ~loc bo)
       | Discard -> Discard
-      | Var (v, xs) -> Var (clone_const v, List.map (clone_loc ~loc) xs)
+      | UVar (v, xs) -> UVar (clone_const v, List.map (clone_loc ~loc) xs)
       | App (g, xs) -> App (clone_const g, List.map (clone_loc ~loc) xs)
       | CData _ as t -> t 
       | Spill (t, _) -> Spill (clone_loc ~loc t, ref NoInfo)
@@ -1093,7 +1097,7 @@ module ScopedTerm = struct
       let rec fv acc { it } =
         match it with
         | Impl(_,_,a,b) -> List.fold_left fv acc [a;b]
-        | Var (_,args) -> List.fold_left fv acc args
+        | UVar (_,args) -> List.fold_left fv acc args
         | App({ scope = Bound l; name = c },xs) -> List.fold_left fv (Scope.Set.add (c,l) acc) xs
         | App({ scope = Global _ },xs) -> List.fold_left fv acc xs
         | Lam(None,_,t) -> fv acc t
@@ -1121,7 +1125,7 @@ module ScopedTerm = struct
             let hd = Scope.Map.find (c,l) map in
             unlock @@ app_loc hd (List.map (subst_loc map fv) xs)
         | App(n,xs) -> App(n,List.map (subst_loc map fv) xs)
-        | Var(c,xs) -> Var(c,List.map (subst_loc map fv) xs)
+        | UVar(c,xs) -> UVar(c,List.map (subst_loc map fv) xs)
         | Spill(t,i) -> Spill(subst_loc map fv t,i)
         | Cast(t,ty) -> Cast(subst_loc map fv t,ty)
         | Discard | CData _ -> t
@@ -1131,7 +1135,7 @@ module ScopedTerm = struct
         if args = [] then t else
         match t with
         | App(n,xs) -> App(n,xs @ args)
-        | Var(c,xs) -> Var(c,xs @ args)
+        | UVar(c,xs) -> UVar(c,xs @ args)
         | Impl(_,_,_,_) -> error ~loc "cannot apply impl"
         | CData _ -> error ~loc "cannot apply cdata"
         | Spill _ -> error ~loc "cannot apply spill"
@@ -1158,7 +1162,7 @@ module ScopedTerm = struct
         match it with
         | SimpleTerm.Opaque o when is_scoped_term o ->
             begin match out_scoped_term o with
-            | { it = Var(f,xs); loc = loc'; ty } -> { SimpleTerm.loc; it = SimpleTerm.Opaque (in_scoped_term @@ { it = Var(f,xs @ l); loc = loc'; ty }) }
+            | { it = UVar(f,xs); loc = loc'; ty } -> { SimpleTerm.loc; it = SimpleTerm.Opaque (in_scoped_term @@ { it = UVar(f,xs @ l); loc = loc'; ty }) }
             | { it = App({ scope = Bound g } as n,[]); loc = loc'; ty } when g = elpi_language ->
                 { SimpleTerm.loc; it = SimpleTerm.Opaque (in_scoped_term @@ { it = App(n, l); loc = loc'; ty }) }
             | x -> anomaly ~loc (Format.asprintf "The term is not an elpi varible coming from a quotation: @[%a@]" pretty x)
@@ -1189,7 +1193,7 @@ module ScopedTerm = struct
       | _ -> false
   end
 
-  let is_var = function Var _ -> true | _ -> false
+  let is_var = function UVar _ -> true | _ -> false
 end