[Typer] [Git][monnier/typer][there-can-be-only-one-inductive] 9 commits: Get rid of attributes on builtin.

Simon Génier pushed to branch there-can-be-only-one-inductive at Stefan / Typer

Commits: d74651cf by Simon Génier at 2020-11-25T10:59:52-05:00 Get rid of attributes on builtin.

- - - - - f73bc318 by Simon Génier at 2020-12-01T23:35:45-05:00 Merge branch 'remove-attributes' into HEAD

- - - - - c0df7b8b by Simon Génier at 2020-12-02T11:36:56-05:00 Cosmetic changes to utest_main.ml.

Some of these changes bring the style more in line with the GNU coding standard that is used for Typer. - Reindent file to 2 spaces. - Break lines before a operator. - Break lines before 80 columns.

Others are my attempts to improve readability. - Use functions specialized on refs in Arg. - Remove superfluous parenthesis. - Extract large fun expressions to local let bindings.

- - - - - 077b4494 by Simon Génier at 2020-12-02T12:05:43-05:00 Utest_main now also handle Windows paths.

- - - - - a4cc1ea7 by Simon Génier at 2020-12-03T12:13:32-05:00 Merge branch 'utests-main-windows'

- - - - - 1ce7599d by Simon Génier at 2020-12-04T09:56:45-05:00 Add opaque values for identifying data constructors.

This patch add a new primitive type, ##DataconsLabel, which uniquely identifies a data constructor within a type. Its inhabitants will be consumed by Low Level Typer to write the correct header for objects. The goal is to give an abstract type that is as useful on Typer on OCaml where the labels are strings than on a future backend which will be better for Low Level Typer and where labels will likely be integers.

Values are created through the primitive ##datacons-label<-string and there is also a macro datacons-label which allows us to write a symbol directly. I choosed to use a right pointing arrow its name, against the Lisp convention. I think it makes more sense in languages with an ML syntax because function composition is made like this

c<-b . b<-a

and it also goes in the same direction as the b_of_a convention in OCaml. I also though it was OK because there where no other primitives with arrows in their names so that convention does not clash with others.

Finally, I decided to go against the name ##Discriminent because it suggests it only applies to sum types, but ##DataconsLabel is also needed for product types.

- - - - - 5a31e992 by Simon Génier at 2020-12-05T14:46:49-05:00 Merge branch 'datacons-label'

- - - - - 9f947a9b by Simon Génier at 2020-12-07T12:38:34-05:00 Instantiate implicit arguments in datacons.

The datacons special form is datacons T C, where T is an (inductive) type and C is a symbol for one of its constructor. Before this commit, T has to syntactically be an inductive. This causes problems for types like Decidable, which is in fact not a Type, but a TypeLevel ≡> Type! Now, Typer tries to instanciate implicit arguments before deciding if something is a type or not. This currently only works for datacons, which is the only place I think it is a problem, but the same technique will work in other similar situations.

- - - - - 6973e558 by Simon Génier at 2020-12-07T12:39:58-05:00 Remove arguments to inductive types.

There used to be two ways to express indexed types: one could either add parameters directly on the type or put the type behind a lambda. These two are semantically equivalent, so we unify them into the latter in this patch.

- - - - -

14 changed files:

- btl/builtins.typer - + btl/empty.typer - + btl/heap.typer - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/eval.ml - + src/heap.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml - tests/elab_test.ml - tests/utest_main.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -192,13 +192,15 @@ Sexp_debug_print = Built-in "Sexp.debug_print" : Sexp -> IO Sexp; %% -----------------------------------------------------

%% FIXME: "List : ?" should be sufficient but triggers -List : Type_ ?ℓ -> Type_ ?ℓ; %% List a = typecons List (nil) (cons a (List a)); %% nil = lambda a ≡> datacons (List a) nil; %% cons = lambda a ≡> datacons (List a) cons; -List = typecons (List (ℓ ::: TypeLevel) (a : Type_ ℓ)) (nil) (cons a (List a)); -nil = datacons List nil; -cons = datacons List cons; +List : (ℓ : TypeLevel) ≡> Type_ ℓ -> Type_ ℓ; +List = lambda ℓ ≡> lambda α -> typecons List (nil) (cons α (List (ℓ := ℓ) α)); +nil : (ℓ : TypeLevel) ≡> (α : Type_ ℓ) ≡> List (ℓ := ℓ) α; +nil = lambda ℓ ≡> lambda α ≡> datacons (List α) nil; +cons : (ℓ : TypeLevel) ≡> (α : Type_ ℓ) ≡> α -> List (ℓ := ℓ) α -> List (ℓ := ℓ) α; +cons = lambda ℓ ≡> lambda α ≡> datacons (List α) cons;

%%%% Macro-related definitions

@@ -469,4 +471,11 @@ Test_eq = Built-in "Test.eq"; Test_neq : String -> ?a -> ?a -> IO Bool; Test_neq = Built-in "Test.neq";

+%% +%% Given a string, return an opaque DataconsLabel that identifies a data +%% constructor. +%% +datacons-label<-string : String -> ##DataconsLabel; +datacons-label<-string = Built-in "datacons-label<-string"; + %%% builtins.typer ends here.

===================================== btl/empty.typer =====================================

===================================== btl/heap.typer ===================================== @@ -0,0 +1,34 @@ +%%% heap --- Manipulate partially initialized objects on the heap + +%% Copyright (C) 2011-2020 Free Software Foundation, Inc. +%% +%% Author: Simon Génier simon.genier@umontreal.ca +%% Keywords: languages, lisp, dependent types. +%% +%% This file is part of Typer. +%% +%% Typer is free software; you can redistribute it and/or modify it under the +%% terms of the GNU General Public License as published by the Free Software +%% Foundation, either version 3 of the License, or (at your option) any +%% later version. +%% +%% Typer is distributed in the hope that it will be useful, but WITHOUT ANY +%% WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +%% FOR A PARTICULAR PURPOSE. See the GNU General Public License for +%% more details. +%% +%% You should have received a copy of the GNU General Public License along +%% with this program. If not, see http://www.gnu.org/licenses/. + +datacons-label = macro (lambda args -> + let + label = Sexp_dispatch (List_nth 0 args Sexp_error) + (lambda _ _ -> Sexp_error) + (lambda label-name -> Sexp_string label-name) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + in + IO_return (quote (datacons-label<-string (uquote label))) +)

===================================== src/builtin.ml ===================================== @@ -134,7 +134,7 @@ let add_builtin_cst (name : string) (e : lexp) lmap := SMap.add name (e, t) map

let new_builtin_type name kind = - let t = mkBuiltin ((dloc, name), kind, None) in + let t = mkBuiltin ((dloc, name), kind) in add_builtin_cst name t; t

===================================== src/debruijn.ml ===================================== @@ -84,18 +84,18 @@ let fatal = Log.log_fatal ~section:"DEBRUIJN" let dloc = dummy_location let type_level_sort = mkSort (dloc, StypeLevel) let sort_omega = mkSort (dloc, StypeOmega) -let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort, None) +let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) let level0 = mkSortLevel SLz let level1 = mkSortLevel (mkSLsucc level0) let level2 = mkSortLevel (mkSLsucc level1) let type0 = mkSort (dloc, Stype level0) let type1 = mkSort (dloc, Stype level1) let type2 = mkSort (dloc, Stype level2) -let type_int = mkBuiltin ((dloc, "Int"), type0, None) -let type_integer = mkBuiltin ((dloc, "Integer"), type0, None) -let type_float = mkBuiltin ((dloc, "Float"), type0, None) -let type_string = mkBuiltin ((dloc, "String"), type0, None) -let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0, None) +let type_int = mkBuiltin ((dloc, "Int"), type0) +let type_integer = mkBuiltin ((dloc, "Integer"), type0) +let type_float = mkBuiltin ((dloc, "Float"), type0) +let type_string = mkBuiltin ((dloc, "String"), type0) +let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_eq_type = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in @@ -108,7 +108,7 @@ let type_eq_type = mkArrow (Anormal, (dloc, None), mkVar (tv, 1), dloc, mkSort (dloc, Stype (mkVar (lv, 3))))))) -let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type, None) +let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) let eq_refl = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in @@ -124,8 +124,7 @@ let eq_refl = [Aerasable, mkVar (lv, 2); Aerasable, mkVar (tv, 1); Anormal, mkVar (xv, 0); - Anormal, mkVar (xv, 0)])))), - None) + Anormal, mkVar (xv, 0)])))))

(* easier to debug with type annotations *)

===================================== src/elab.ml ===================================== @@ -92,6 +92,9 @@ let lexp_fatal loc lexp = let value_fatal loc value = fatal ~loc ~print_action:(value_print_details value)

+let whnf (lexp : lexp) (ectx : DB.elab_context) = + OL.lexp_whnf lexp (ectx_to_lctx ectx) + (** Type info returned by elaboration. *) type sform_type = | Checked (* Checked that the expression has the requested type. *) @@ -106,7 +109,7 @@ let special_forms : special_forms_map ref = ref SMap.empty let type_special_form = BI.new_builtin_type "Special-Form" type0

let add_special_form (name, func) = - BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form, None)); + BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form)); special_forms := SMap.add name func (!special_forms)

let get_special_form name = @@ -440,28 +443,22 @@ let rec meta_to_var ids (e : lexp) = -> mkLambda (ak, v, loop o t, loop (1 + o) e) | Call (f, args) -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) - | Inductive (l, label, args, cases) - -> let alen = List.length args in - let (_, nargs) - = List.fold_right (fun (ak, v, t) (o', args) - -> let o' = o' - 1 in - (o', (ak, v, loop (o' + o) t) - :: args)) - args (alen, []) in - let ncases - = SMap.map - (fun fields - -> let flen = List.length fields in - let (_, nfields) - = List.fold_right - (fun (ak, v, t) (o', fields) - -> let o' = o' - 1 in - (o', (ak, v, loop (o' + o) t) - :: fields)) - fields (flen + alen, []) in - nfields) - cases in - mkInductive (l, label, nargs, ncases) + | Inductive (l, ((_, name) as label), cases) + -> let () = print_endline ("meta_to_var: Inductive " ^ name) in + let ncases + = SMap.map + (fun fields + -> let flen = List.length fields in + let (_, nfields) + = List.fold_right + (fun (ak, v, t) (o', fields) + -> let o' = o' - 1 in + (o', (ak, v, loop (o' + o) t) + :: fields)) + fields (flen, []) in + nfields) + cases in + mkInductive (l, label, ncases) | Cons (t, l) -> mkCons (loop o t, l) | Case (l, e, t, cases, default) -> let ncases @@ -584,7 +581,7 @@ and infer (p : sexp) (ctx : elab_context): lexp * ltype = and elab_special_form ctx f args ot = let loc = lexp_location f in match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with - | Builtin ((_, name), _, _) -> + | Builtin ((_, name), _) -> (* Special form. *) (get_special_form name) ctx loc args ot

@@ -593,42 +590,15 @@ and elab_special_form ctx f args ot =

(* Make up an argument of type `t` when none is provided. *) and get_implicit_arg ctx loc oname t = - (* lookup default attribute of t. *) - (* FIXME: Don't lookup defaults/tactics here. Instead, just always - * generate a metavar at this point. The use of defaults/tactics should be - * postponed, probably to just before we do HM-style generalization. *) - match - try (* FIXME: We shouldn't hard code as popular a name as `default`. *) - let pidx, pname = (senv_lookup "default" ctx), "default" in - let default = mkVar ((dloc, Some pname), pidx) in - get_attribute ctx loc [default; t] - with e -> None with - | Some attr - -> (* FIXME: The `default` attribute table shouldn't contain elements of - * type `Macro` but elements of type `something -> Sexp`. - * The point of the `Macro` type is to be able to distinguish - * a macro call from a function call, but here, we have no need - * to distinguish two cases. - * Better yet: let's not do any table lookup here. Instead, - * call a `default-arg-filler` function, implemented in Typer, - * just like `Macro_expand` function. That one can then look - * things up in a table and/or do anything else it wants. *) - let v = lexp_expand_macro loc attr [] ctx (Some t) in - - (* get the sexp returned by the macro *) - let lsarg = match v with - | Vcommand cmd - -> (match cmd () with - | Vsexp (sexp) -> sexp - | _ -> value_fatal loc v "default attribute should return a IO Sexp" ) - | _ -> value_fatal loc v "default attribute should return an IO" in - - (* Elaborate the argument *) - check lsarg t ctx - | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) - (loc, oname) t - -(* Build the list of implicit arguments to instantiate. *) + newMetavar + (ectx_to_lctx ctx) + (ectx_to_scope_level ctx) + (loc, oname) + t + +(** Given a value [e] of type [t], wrap [e] in applications of its implicit + arguments. Returns a pair of the wrapped [e] and the [t] stripped of its + implicit arguments *) and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp'_whnf t (ectx_to_lctx ctx) with @@ -638,6 +608,18 @@ and instantiate_implicit e t ctx = | _ -> (mkCall (e, List.rev args), t) in instantiate t []

+(** Like {!instanciate_implicit}, but works on a value directly. Wraps an + implicit (or erasable implicit) λ with an application to its instanciated + argument *) +and instantiate_implicit_of_value value ctx = + let rec instantiate e = + match whnf e ctx with + | Lambda ((Aerasable | Aimplicit), (_, arg_name), arg_ty, body), _ + -> let arg = get_implicit_arg ctx (lexp_location e) arg_name arg_ty in + instantiate (mkSusp body (S.substitute arg)) + | _ -> whnf e ctx + in instantiate value + and infer_type pexp ectx var = (* We could also use lexp_check with an argument of the form * Sort (?s), but in most cases the metavar would be allocated @@ -765,37 +747,27 @@ and check_case rtype (loc, target, ppatterns) ctx = -> unify_ind it it'; (cs, args) | None -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with - | Inductive (_, _, fargs, constructors) - -> let (s, targs) = List.fold_left - (fun (s, targs) (ak, name, t) - -> let arg = newMetavar - (ectx_to_lctx ctx) - (ectx_to_scope_level ctx) - name (mkSusp t s) in - (S.cons arg s, (ak, arg) :: targs)) - (S.identity, []) - fargs in - let (cs, args) = (constructors, List.rev targs) in - ltarget := check_inferred ctx tlxp tltp (mkCall (it', args)); - it_cs_as := Some (it', cs, args); - (cs, args) - | _ -> let call_split e = - match OL.lexp'_whnf e (ectx_to_lctx ctx) with - | Call (f, args) -> (f, args) - | _ -> (e,[]) in - let (it, targs) = call_split tltp in - unify_ind it it'; - let constructors = - match OL.lexp'_whnf it (ectx_to_lctx ctx) with - | Inductive (_, _, fargs, constructors) - -> assert (List.length fargs = List.length targs); - constructors - | _ -> lexp_error (sexp_location target) tlxp - ("Can't `case` on objects of this type: " - ^ lexp_string tltp); - SMap.empty in - it_cs_as := Some (it, constructors, targs); - (constructors, targs) in + | Inductive (_, _, constructors) + -> ltarget := check_inferred ctx tlxp tltp (mkCall (it', [])); + it_cs_as := Some (it', constructors, []); + (constructors, []) + | _ -> let call_split e = + match OL.lexp'_whnf e (ectx_to_lctx ctx) with + | Call (f, args) -> (f, args) + | _ -> (e, []) in + let (it, targs) = call_split tltp in + unify_ind it it'; + let constructors = + match OL.lexp'_whnf it (ectx_to_lctx ctx) with + | Inductive (_, _, constructors) + -> assert (List.length targs == 0); + constructors + | _ -> lexp_error (sexp_location target) tlxp + ("Can't `case` on objects of this type: " + ^ lexp_string tltp); + SMap.empty in + it_cs_as := Some (it, constructors, targs); + (constructors, targs) in

(* Read patterns one by one *) let fold_fun (lbranches, dflt) (pat, pexp) = @@ -1388,92 +1360,23 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = * Special forms implementation * -------------------------------------------------------------------------- *)

-and sform_new_attribute ctx loc sargs ot = - match sargs with - | [t] -> let ltp = infer_type t ctx (loc, None) in - (* FIXME: This creates new values for type `ltp` (very wrong if `ltp` - * is False, for example): Should be a type like `AttributeMap t` - * instead. *) - (mkBuiltin ((loc, "new-attribute"), - L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp), - Some AttributeMap.empty), - Lazy) - | _ -> fatal ~loc "new-attribute expects a single Type argument" - -and sform_add_attribute ctx loc (sargs : sexp list) ot = - let n = get_size ctx in - let table, var, attr = match List.map (lexp_parse_sexp ctx) sargs with - | [table; e; attr] when is_var e - -> table, (n - (get_var_db_index (get_var e)), U.get_vname_name (get_var_vname (get_var e))), attr - | _ -> fatal ~loc "add-attribute expects 3 arguments (table; var; attr)" in - - let map, attr_type = - match OL.lexp'_whnf table (ectx_to_lctx ctx) with - | Builtin (_, attr_type, Some map) -> map, attr_type - | _ -> fatal ~loc "add-attribute expects a table as first argument" in - - (* FIXME: Type check (attr: type == attr_type) *) - let attr' = L.clean (OL.lexp_close (ectx_to_lctx ctx) attr) in - let table = AttributeMap.add var attr' map in - (mkBuiltin ((loc, "add-attribute"), attr_type, Some table), - Lazy) - - - and get_attribute ctx loc largs = - let ctx_n = get_size ctx in - let table, var = match largs with - | [table; e] when is_var e - -> table, (ctx_n - get_var_db_index (get_var e), U.get_vname_name (get_var_vname (get_var e))) - | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in - - - let map = - match OL.lexp'_whnf table (ectx_to_lctx ctx) with - | Builtin (_, attr_type, Some map) -> map - | _ -> fatal ~loc "get-attribute expects a table as first argument" in - - try Some (AttributeMap.find var map) - with Not_found -> None - -and sform_get_attribute ctx loc (sargs : sexp list) ot = - match get_attribute ctx loc (List.map (lexp_parse_sexp ctx) sargs) with - | Some e -> (e, Lazy) - | None -> sexp_error loc "No attribute found"; sform_dummy_ret ctx loc - -and sform_has_attribute ctx loc (sargs : sexp list) ot = - let n = get_size ctx in - let table, var = match List.map (lexp_parse_sexp ctx) sargs with - | [table; e] when is_var e - -> table, (n - get_var_db_index (get_var e), U.get_vname_name (get_var_vname (get_var e))) - | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in - - - let map, attr_type = - let lp = OL.lexp_whnf table (ectx_to_lctx ctx) in - match lexp_lexp' lp with - | Builtin (_, attr_type, Some map) -> map, attr_type - | lxp -> lexp_fatal loc table - "get-attribute expects a table as first argument" in - - (BI.o2l_bool ctx (AttributeMap.mem var map), Lazy) - - and sform_declexpr ctx loc sargs ot = - match List.map (lexp_parse_sexp ctx) sargs with - | [e] when is_var e - -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with - | Some lxp -> (lxp, Lazy) - | None -> error ~loc "no expr available"; +and sform_declexpr ctx loc sargs ot = + match List.map (lexp_parse_sexp ctx) sargs with + | [e] when is_var e + -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with + | Some lxp -> (lxp, Lazy) + | None -> error ~loc "no expr available"; sform_dummy_ret ctx loc) - | _ -> error ~loc "declexpr expects one argument"; - sform_dummy_ret ctx loc + | _ -> error ~loc "declexpr expects one argument"; + sform_dummy_ret ctx loc

- let sform_decltype ctx loc sargs ot = - match List.map (lexp_parse_sexp ctx) sargs with - | [e] when is_var e - -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) - | _ -> error ~loc "decltype expects one argument"; - sform_dummy_ret ctx loc +let sform_decltype ctx loc sargs ot = + match List.map (lexp_parse_sexp ctx) sargs with + | [e] when is_var e + -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) + | _ -> error ~loc "decltype expects one argument"; + sform_dummy_ret ctx loc

@@ -1489,7 +1392,7 @@ let sform_built_in ctx loc sargs ot = * performance of type-inference (at least until we have proper * memoization of push_susp and/or whnf). *) -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in - let bi = mkBuiltin ((loc, name), ltp', None) in + let bi = mkBuiltin ((loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions)) then sexp_error loc ("Unknown built-in `" ^ name ^ "`"); BI.add_builtin_cst name bi; @@ -1507,12 +1410,14 @@ let sform_datacons ctx loc sargs ot = match sargs with | [t; Symbol ((sloc, cname) as sym)] -> let idt, _ = infer t ctx in - (mkCons (idt, sym), Lazy) - - | [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; - sform_dummy_ret ctx loc - | _ -> sexp_error loc "##constr requires two arguments"; - sform_dummy_ret ctx loc + let idt = instantiate_implicit_of_value idt ctx in + mkCons (idt, sym), Lazy + | [_;_] + -> sexp_error loc "Second arg of ##datacons should be a symbol"; + sform_dummy_ret ctx loc + | _ + -> sexp_error loc "##datacons requires two arguments"; + sform_dummy_ret ctx loc

let elab_colon_to_ak k = match k with | "_:::_" -> Aerasable @@ -1542,7 +1447,7 @@ let sform_typecons ctx loc sargs ot = -> let (label, formals) = match formals with | Node (label, formals) -> (label, formals) | _ -> (formals, []) in - let label = match label with + let (_, name) as label = match label with | Symbol label -> label | _ -> let loc = sexp_location label in sexp_error loc "Unrecognized inductive type name"; @@ -1574,12 +1479,13 @@ let sform_typecons ctx loc sargs ot = | Symbol s -> (s, [])::pcases

| _ -> sexp_error (sexp_location case) - "Unrecognized constructor declaration"; + "Unrecognized constructor declaration"; pcases) constrs [] in

let map_ctor = lexp_parse_inductive ctors nctx in - (mkInductive (loc, label, formals, map_ctor), Lazy) + let () = print_endline ("sform_typecons: " ^ name) in + (mkInductive (loc, label, map_ctor), Lazy)

let sform_hastype ctx loc sargs ot = match sargs with @@ -1926,10 +1832,6 @@ let register_special_forms () = ("Type_", sform_type); ("load", sform_load); (* FIXME: We should add here `let_in_`, `case_`, etc... *) - ("get-attribute", sform_get_attribute); - ("new-attribute", sform_new_attribute); - ("has-attribute", sform_has_attribute); - ("add-attribute", sform_add_attribute); (* FIXME: These should be functions! *) ("decltype", sform_decltype); ("declexpr", sform_declexpr); @@ -1973,6 +1875,7 @@ let default_ectx else ctx_define ctx (dloc, Some key) e t) (!BI.lmap) lctx in

+ Heap.register_builtins (); (* read base file *) let lctx = dynamic_bind parsing_internals true (fun () @@ -1988,7 +1891,7 @@ let default_ectx

builtin_size := get_size lctx; let ectx = dynamic_bind in_pervasive true - (fun () -> read_file (btl_folder ^ "/pervasive.typer") lctx) in + (fun () -> read_file (btl_folder ^ "/empty.typer") lctx) in let _ = sform_default_ectx := ectx in ectx with e ->

===================================== src/eval.ml ===================================== @@ -812,14 +812,18 @@ let erasable_p name nth ectx = | (k, _, _) -> k = Aerasable ) else false | _ -> false in - try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with - | Cons (e, _) when is_var e - -> (match (env_lookup_expr ectx (get_var e)) with - | Some i when is_inductive i - -> is_erasable (get_inductive_ctor (get_inductive i)) - | _ -> false) - | _ -> false + try + let idx = senv_lookup name ectx in + match + OL.lexp'_whnf + (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) + with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some (Inductive (_, _, constructors), _) -> is_erasable constructors + | _ -> false) + | _ -> false with Senv_Lookup_Fail _ -> false

let erasable_p2 t name ectx = @@ -833,14 +837,18 @@ let erasable_p2 t name ectx = | _ -> false) args) | _ -> false in - try let idx = senv_lookup t ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx)) (ectx_to_lctx ectx) with - | Cons (e, _) when is_var e - -> (match (env_lookup_expr ectx (get_var e)) with - | Some i when is_inductive i - -> is_erasable (get_inductive_ctor (get_inductive i)) - | _ -> false) - | _ -> false + try + let idx = senv_lookup t ectx in + match + OL.lexp'_whnf + (mkVar ((dummy_location, Some t), idx)) + (ectx_to_lctx ectx) + with + | Cons (e, _) when is_var e + -> (match env_lookup_expr ectx (get_var e) with + | Some (Inductive (_, _, constructors), _) -> is_erasable constructors + | _ -> false) + | _ -> false with Senv_Lookup_Fail _ -> false

let nth_ctor_arg name nth ectx = @@ -851,14 +859,18 @@ let nth_ctor_arg name nth ectx = | _ -> "_" | exception (Failure _) -> "_" ) | _ -> "_" in - try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with - | Cons (e, _) when is_var e - -> (match (env_lookup_expr ectx (get_var e)) with - | Some i when is_inductive i - -> find_nth (get_inductive_ctor (get_inductive i)) - | _ -> "_") - | _ -> "_" + try + let idx = senv_lookup name ectx in + match + OL.lexp'_whnf + (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) + with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some (Inductive (_, _, constructors), _) -> find_nth constructors + | _ -> "_") + | _ -> "_" with Senv_Lookup_Fail _ -> "_"

let ctor_arg_pos name arg ectx = @@ -872,14 +884,18 @@ let ctor_arg_pos name arg ectx = | None -> (-1) | Some n -> n ) | _ -> (-1) in - try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with - | Cons (e, _) when is_var e - -> (match (env_lookup_expr ectx (get_var e)) with - | Some i when is_inductive i - -> find_arg (get_inductive_ctor (get_inductive i)) - | _ -> (-1)) - | _ -> (-1) + try + let idx = senv_lookup name ectx in + match + OL.lexp'_whnf + (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) + with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some (Inductive (_, _, constructors), _) -> find_arg constructors + | _ -> (-1)) + | _ -> (-1) with Senv_Lookup_Fail _ -> (-1)

let is_constructor loc depth args_val = match args_val with

===================================== src/heap.ml ===================================== @@ -0,0 +1,40 @@ +(* Copyright (C) 2020 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. *) + +open Env +open Lexp +open Pexp + +type location = Util.location + +let error ~(location : location) (message : string) : 'a = + Log.log_fatal ~section:"HEAP" ~loc:location message + +let dloc = Util.dummy_location +let type0 = Debruijn.type0 +let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) + +let datacons_label_of_string location depth = function + | [Vstring _ as label] -> label + | _ -> error ~location "`##datacons-label<-string` expects 1 string argument" + +let register_builtins () = + Builtin.add_builtin_cst "DataconsLabel" type_datacons_label; + Eval.add_builtin_function "datacons-label<-string" datacons_label_of_string 1

===================================== src/inverse_subst.ml ===================================== @@ -281,22 +281,18 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = | Call (f, args) -> mkCall (apply_inv_subst f s, L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s)) args) - | Inductive (l, label, args, cases) - -> let (s, nargs) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, (ak, v, apply_inv_subst t s) :: nargs)) - (s, []) args in - let nargs = List.rev nargs in - let ncases = SMap.map (fun args - -> let (_, ncase) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, - (ak, v, apply_inv_subst t s) - :: nargs)) - (s, []) args in - L.rev ncase) - cases in - mkInductive (l, label, nargs, ncases) + | Inductive (l, label, cases) + -> let inv_subst_case args = + let (_, ncase) = + L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink v s, + (ak, v, apply_inv_subst t s) + :: nargs)) + (s, []) args + in + L.rev ncase + in + mkInductive (l, label, SMap.map inv_subst_case cases) | Cons (it, name) -> mkCons (apply_inv_subst it s, name) | Case (l, e, ret, cases, default) -> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s,

===================================== src/lexp.ml ===================================== @@ -37,12 +37,9 @@ module S = Subst type vname = U.vname type vref = U.vref type meta_id = int (* Identifier of a meta variable. *) - +type location = U.location type label = symbol

-type attribute_key = (int * string) (* rev_dbi * Var name *) -module AttributeMap = Map.Make (struct type t = attribute_key let compare = compare end) - (*************** Elaboration to Lexp *********************)

(* The scoping of `Let` is tricky: @@ -58,15 +55,17 @@ module AttributeMap = Map.Make (struct type t = attribute_key let compare = comp * And the type of the 3rd binding is defined in the scope of the * surrounded context extended with the first and the second bindings. *)

+ type ltype = lexp and subst = lexp S.subst (* Here we want a pair of `Lexp` and its hash value to avoid re-hashing "sub-Lexp". *) + and inductive = location * label * ((arg_kind * vname * ltype) list) SMap.t and lexp = lexp' * int and lexp' = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort - | Builtin of symbol * ltype * lexp AttributeMap.t option + | Builtin of symbol * ltype | Var of vref | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) @@ -74,9 +73,7 @@ type ltype = lexp | Arrow of arg_kind * vname * ltype * U.location * ltype | Lambda of arg_kind * vname * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of U.location * label - * ((arg_kind * vname * ltype) list) (* formal Args *) - * ((arg_kind * vname * ltype) list) SMap.t + | Inductive of inductive | Cons of lexp * symbol (* = Type info * ctor_name *) | Case of U.location * lexp * ltype (* The type of the return value of all branches *) @@ -196,12 +193,8 @@ let lexp'_hash (lp : lexp') = | Stype lp -> lexp_hash lp | StypeOmega -> Hashtbl.hash s | StypeLevel -> Hashtbl.hash s)) - | Builtin (v, t, m) - -> U.combine_hash 4 (U.combine_hash - (U.combine_hash (Hashtbl.hash v) (lexp_hash t)) - (match m with - | Some m -> Hashtbl.hash m - | None -> 404)) + | Builtin (v, t) + -> U.combine_hash 4 (U.combine_hash (Hashtbl.hash v) (lexp_hash t)) | Var v -> U.combine_hash 5 (Hashtbl.hash v) | Let (l, ds, e) -> U.combine_hash 6 (U.combine_hash (Hashtbl.hash l) @@ -220,15 +213,10 @@ let lexp'_hash (lp : lexp') = -> U.combine_hash 8 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) (U.combine_hash (lexp_hash t) (lexp_hash e))) - | Inductive (l, n, a, cs) + | Inductive (l, n, cs) -> U.combine_hash 9 (U.combine_hash (U.combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) - (U.combine_hash (U.combine_hashes - (List.map (fun e -> let (ak, n, lt) = e in - (U.combine_hash (Hashtbl.hash ak) - (U.combine_hash (Hashtbl.hash n) (lexp_hash lt)))) - a)) - (Hashtbl.hash cs))) + (Hashtbl.hash cs)) | Cons (t, n) -> U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n)) | Case (l, e, rt, bs, d) -> U.combine_hash 11 (U.combine_hash @@ -249,6 +237,9 @@ let lexp'_hash (lp : lexp') = | Susp (lp, subst) -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst))

+let datacons_equal (ak1, _, e1) (ak2, _, e2) = + ak1 = ak2 && e1 == e2 + (* Equality function for hash table * using physical equality for "sub-lexp" and compare for `subst`. *) let hc_eq e1 e2 = @@ -264,7 +255,7 @@ let hc_eq e1 e2 = | (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true | (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true | (Sort (_, Stype e1), Sort (_, Stype e2)) -> e1 == e2 - | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 + | (Builtin ((_, name1), _), Builtin ((_, name2), _)) -> name1 = name2 | (Var (_, i1), Var (_, i2)) -> i1 = i2 | (Susp (e1, s1), Susp (e2, s2)) -> e1 == e2 && compare s1 s2 = 0 | (Let (_, defs1, e1), Let (_, defs2, e2)) @@ -277,11 +268,8 @@ let hc_eq e1 e2 = | (Call (e1, as1), Call (e2, as2)) -> e1 == e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && e1 == e2) as1 as2 - | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) - -> l1 = l2 && List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2) as1 as2 - && SMap.equal (List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2)) ctor1 ctor2 + | (Inductive (_, l1, ctor1), Inductive (_, l2, ctor2)) + -> l1 = l2 && SMap.equal (List.for_all2 datacons_equal) ctor1 ctor2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> t1 == t2 && l1 = l2 | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2)) -> e1 == e2 && r1 == r2 && SMap.equal @@ -307,18 +295,18 @@ let hc_table : WHC.t = WHC.create 1000 let hc (l : lexp') : lexp = WHC.merge hc_table (l, lexp'_hash l)

-let mkImm s = hc (Imm s) -let mkSortLevel l = hc (SortLevel l) -let mkSort (l, s) = hc (Sort (l, s)) -let mkBuiltin (v, t, m) = hc (Builtin (v, t, m)) -let mkVar v = hc (Var v) -let mkLet (l, ds, e) = hc (Let (l, ds, e)) -let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) -let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) -let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) -let mkCons (t, n) = hc (Cons (t, n)) -let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) -let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) +let mkImm s = hc (Imm s) +let mkSortLevel l = hc (SortLevel l) +let mkSort (l, s) = hc (Sort (l, s)) +let mkBuiltin (v, t) = hc (Builtin (v, t)) +let mkVar v = hc (Var v) +let mkLet (l, ds, e) = hc (Let (l, ds, e)) +let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) +let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) +let mkInductive (l, n, cs) = hc (Inductive (l, n, cs)) +let mkCons (t, n) = hc (Cons (t, n)) +let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) +let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) let mkCall (f, es) = match lexp_lexp' f, es with | Call (f', es'), _ -> hc (Call (f', es' @ es)) @@ -329,18 +317,18 @@ let impossible = mkImm Sexp.dummy_epsilon

let lexp_head e = match lexp_lexp' e with - | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s - | Var _ -> "Var" - | Let _ -> "let" - | Arrow _ -> "Arrow" - | Lambda _ -> "lambda" - | Call _ -> "Call" - | Cons _ -> "datacons" - | Case _ -> "case" + | Imm s -> + if e = impossible then "impossible" else "Imm" ^ sexp_string s + | Var _ -> "Var" + | Let _ -> "let" + | Arrow _ -> "Arrow" + | Lambda _ -> "lambda" + | Call _ -> "Call" + | Cons _ -> "datacons" + | Case _ -> "case" | Inductive _ -> "typecons" | Susp _ -> "Susp" - | Builtin (_, _, None) -> "Builtin" - | Builtin _ -> "AttributeTable" + | Builtin _ -> "Builtin" | Metavar _ -> "Metavar" | Sort _ -> "Sort" | SortLevel _ -> "SortLevel" @@ -392,21 +380,16 @@ let get_var_db_index v = let get_var_vname v = let (n, idx) = v in n

-let pred_inductive l pred = +let pred_inductive l (pred : inductive -> bool) = match lexp_lexp' l with - | Inductive (l, n, a, cs) -> pred (l, n, a, cs) - | _ -> false + | Inductive inductive -> pred inductive + | _ -> false

let get_inductive l = match lexp_lexp' l with - | Inductive (l, n, a, cs) -> (l, n, a, cs) + | Inductive (l, n, cs) -> (l, n, cs) | _ -> Log.log_fatal ~section:"internal" "Lexp is not Inductive "

-let get_inductive_ctor i = - let (l, n, a, cs) = i in cs - -let is_inductive l = pred_inductive l (fun e -> true) - (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml @@ -512,12 +495,12 @@ let rec lexp_location e = | SortLevel SLz -> U.dummy_location | Imm s -> sexp_location s | Var ((l,_),_) -> l - | Builtin ((l, _), _, _) -> l + | Builtin ((l, _), _) -> l | Let (l,_,_) -> l | Arrow (_,_,_,l,_) -> l | Lambda (_,(l,_),_,_) -> l | Call (f,_) -> lexp_location f - | Inductive (l,_,_,_) -> l + | Inductive (l,_,_) -> l | Cons (_,(l,_)) -> l | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e @@ -554,21 +537,17 @@ let rec push_susp e s = (* Push a suspension one level down. *) | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s)) | Call (f, args) -> mkCall (mkSusp f s, L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args) - | Inductive (l, label, args, cases) - -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, (ak, v, mkSusp t s) :: nargs)) - (s, []) args in - let nargs = List.rev nargs in - let ncases = SMap.map (fun args - -> let (_, ncase) - = L.fold_left (fun (s, nargs) (ak, v, t) + | Inductive (l, label, cases) + -> let ncases = SMap.map (fun args + -> let (_, ncase) + = L.fold_left (fun (s, nargs) (ak, v, t) -> (ssink v s, - (ak, v, mkSusp t s) + (ak, v, mkSusp t s) :: nargs)) (s, []) args in - L.rev ncase) - cases in - mkInductive (l, label, nargs, ncases) + L.rev ncase) + cases in + mkInductive (l, label, ncases) | Cons (it, name) -> mkCons (mkSusp it s, name) | Case (l, e, ret, cases, default) -> mkCase (l, mkSusp e s, mkSusp ret s, @@ -621,21 +600,17 @@ let clean e = | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) | Call (f, args) -> mkCall (clean s f, L.map (fun (ak, arg) -> (ak, clean s arg)) args) - | Inductive (l, label, args, cases) - -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, (ak, v, clean s t) :: nargs)) - (s, []) args in - let nargs = List.rev nargs in - let ncases = SMap.map (fun args - -> let (_, ncase) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, - (ak, v, clean s t) - :: nargs)) - (s, []) args in - L.rev ncase) - cases in - mkInductive (l, label, nargs, ncases) + | Inductive (l, label, cases) + -> let ncases = SMap.map (fun args + -> let (_, ncase) + = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink v s, + (ak, v, clean s t) + :: nargs)) + (s, []) args in + L.rev ncase) + cases in + mkInductive (l, label, ncases) | Cons (it, name) -> mkCons (clean s it, name) | Case (l, e, ret, cases, default) -> mkCase (l, clean s e, clean s ret, @@ -667,7 +642,7 @@ let rec lexp_unparse lxp = match lexp_lexp' lxp with | Susp _ -> lexp_unparse (nosusp lxp) | Imm (sexp) -> sexp - | Builtin ((l,name), _, _) -> Symbol (l, "##" ^ name) + | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) | Var ((loc, name), _) -> Symbol (loc, maybename name) | Cons (t, (l, name)) @@ -710,14 +685,9 @@ let rec lexp_unparse lxp = let sargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in Node (lexp_unparse lxp, sargs)

- | Inductive(loc, label, lfargs, ctors) -> - (* (arg_kind * vdef * ltype) list *) - (* (arg_kind * pvar * pexp option) list *) - let pfargs = List.map (fun (kind, vdef, ltp) -> - (kind, sname vdef, Some (lexp_unparse ltp))) lfargs in - + | Inductive (loc, label, ctors) -> Node (stypecons, - Node (Symbol label, List.map pexp_u_formal_arg pfargs) + Symbol label :: List.map (fun (name, types) -> Node (Symbol (loc, name), @@ -893,7 +863,7 @@ let rec get_precedence expr ctx = | Arrow (Aimplicit, _, _, _, _) -> lkp "=>" | Arrow (Aerasable, _, _, _, _) -> lkp "≡>" | Call (exp, _) -> get_precedence exp ctx - | Builtin ((_, name), _, _) when is_binary_op name -> + | Builtin ((_, name), _) when is_binary_op name -> lkp (get_binary_op_name name) | Var ((_, Some name), _) when is_binary_op name -> lkp (get_binary_op_name name) @@ -950,16 +920,13 @@ and lexp_str ctx (exp : lexp) : string = let kind_str k = match k with | Anormal -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" in

- let kindp_str k = match k with - | Anormal -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in - let get_name fname = match lexp_lexp' fname with - | Builtin ((_, name), _, _) -> name, 0 - | Var((_, Some name), idx) -> name, idx - | Lambda _ -> "__", 0 - | Cons _ -> "__", 0 - | _ -> "__", -1 in + | Builtin ((_, name), _) -> name, 0 + | Var((_, Some name), idx) -> name, idx + | Lambda _ -> "__", 0 + | Cons _ -> "__", 0 + | _ -> "__", -1 in

match lexp_lexp' exp with | Imm(value) -> (match value with @@ -1033,21 +1000,10 @@ and lexp_str ctx (exp : lexp) : string = | _ -> let args = List.fold_left print_arg "" args in "(" ^ (lexp_str' fname) ^ args ^ ")")

- | Inductive (_, (_, name), [], ctors) -> + | Inductive (_, (_, name), ctors) -> (keyword "typecons") ^ " (" ^ name ^") " ^ newline ^ (lexp_str_ctor ctx ctors)

- | Inductive (_, (_, name), args, ctors) - -> let args_str - = List.fold_left - (fun str (arg_kind, (_, name), ltype) - -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " " - ^ (lexp_str' ltype) ^ ")") - "" args in - - (keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^ - (lexp_str_ctor ctx ctors) - | Case (_, target, _ret, map, dflt) ->( let str = (keyword "case ") ^ (lexp_str' target) in let arg_str arg @@ -1070,7 +1026,7 @@ and lexp_str ctx (exp : lexp) : string = | (_, Some name) -> name) ^ " => " ^ (lexp_stri 1 df))

- | Builtin ((_, name), _, _) -> "##" ^ name + | Builtin ((_, name), _) -> "##" ^ name

| Sort (_, StypeLevel) -> "##TypeLevel.Sort" | Sort (_, StypeOmega) -> "##Type_ω" @@ -1131,7 +1087,7 @@ let rec eq e1 e2 = | (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true | (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true | (Sort (_, Stype e1), Sort (_, Stype e2)) -> eq e1 e2 - | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 + | (Builtin ((_, name1), _), Builtin ((_, name2), _)) -> name1 = name2 | (Var (_, i1), Var (_, i2)) -> i1 = i2 | (Susp (e1, s1), _) -> eq (push_susp e1 s1) e2 | (_, Susp (e2, s2)) -> eq e1 (push_susp e2 s2) @@ -1145,11 +1101,8 @@ let rec eq e1 e2 = | (Call (e1, as1), Call (e2, as2)) -> eq e1 e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 - | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) - -> l1 = l2 && List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 - && SMap.equal (List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2)) ctor1 ctor2 + | (Inductive (_, l1, ctor1), Inductive (_, l2, ctor2)) + -> l1 = l2 && SMap.equal (List.for_all2 datacons_equal) ctor1 ctor2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq t1 t2 && l1 = l2 | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2)) -> eq e1 e2 && eq r1 r2 && SMap.equal

===================================== src/opslexp.ml ===================================== @@ -182,7 +182,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = args)) ctx | Call (f', xs1) -> mkCall (f', List.append xs1 xs) - | Builtin ((_, name), _, _) + | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with | Some f -> U.option_default e (f ctx args) | None -> e) @@ -196,21 +196,17 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = | _ -> Log.internal_error "" in mkCall (DB.eq_refl, [Aerasable, elevel; Aerasable, etype; Aerasable, e]) in let reduce it name aargs = - let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with - | Inductive (_,_,fargs,_) -> fargs - | _ -> Log.log_error "Case on a non-inductive type in whnf!"; [] in + let () = match lexp_lexp' (lexp_whnf_aux it ctx) with + | Inductive _ -> () + | _ -> Log.log_error "Case on a non-inductive type in whnf!" in try let (_, _, branch) = SMap.find name branches in - let (subst, _) - = List.fold_left - (fun (s, targs) (_, arg) -> - match targs with - | [] -> (S.cons (lexp_whnf_aux arg ctx) s, []) - | _targ::targs -> - (* Ignore the type arguments *) - (s, targs)) - (S.identity, targs) - aargs in + let subst = + List.fold_left + (fun s (_, arg) -> S.cons (lexp_whnf_aux arg ctx) s) + S.identity + aargs + in (* Substitute case Eq variable by the proof (Eq.refl l t e') *) let subst = S.cons (get_refl e') subst in lexp_whnf_aux (push_susp branch subst) ctx @@ -342,7 +338,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = || (match (s1, s2) with | (Stype e1, Stype e2) -> conv_p e1 e2 | _ -> false) - | (Builtin ((_, s1), _, _), Builtin ((_, s2), _, _)) -> s1 = s2 + | (Builtin ((_, s1), _), Builtin ((_, s2), _)) -> s1 = s2 | (Var (_, v1), Var (_, v2)) -> v1 = v2 | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, vd2, t21, _, t22)) -> ak1 == ak2 @@ -362,29 +358,26 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = && (conv_erase && ak1 = P.Aerasable || conv_p t1 t2)) true args1 args2 in conv_p f1 f2 && conv_arglist_p args1 args2 - | (Inductive (_, l1, args1, cases1), Inductive (_, l2, args2, cases2)) - -> let rec conv_fields ctx vs fields1 fields2 = - match fields1, fields2 with - | ([], []) -> true - | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2) - -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_fields (DB.lexp_ctx_cons ctx vd1 Variable t1) - (set_shift vs) - fields1 fields2 - | _,_ -> false in - let rec conv_args ctx vs args1 args2 = - match args1, args2 with - | ([], []) -> - (* Args checked alright, now go on with the fields, - * using the new context. *) - SMap.equal (conv_fields ctx vs) cases1 cases2 - | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2) - -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_args (DB.lexp_ctx_cons ctx l1 Variable t1) - (set_shift vs) - args1 args2 - | _,_ -> false in - l1 == l2 && conv_args ctx vs' args1 args2 + | (Inductive (_, ((_, name_l) as l1), cases1), Inductive (_, ((_, name_r) as l2), cases2)) + -> let () = print_endline ("conv_p of " ^ name_l ^ " and " ^ name_r) in + let rec conv_fields ctx vs fields1 fields2 = + match fields1, fields2 with + | ([], []) -> true + | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2) + -> ak1 == ak2 + && (let () = print_endline ("Comparing types " ^ lexp_string t1 ^ " and " ^ lexp_string t2) in + let res = conv_p' ctx vs t1 t2 in + let () = print_endline ("Done comparing types " ^ lexp_string t1 ^ " and " ^ lexp_string t2) in + res) + && conv_fields + (DB.lexp_ctx_cons ctx vd1 Variable t1) + (set_shift vs) + fields1 + fields2 + | _,_ -> false in + let res = l1 == l2 && SMap.equal (conv_fields ctx vs') cases1 cases2 in + let () = print_endline "Done" in + res | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 | (Case (_, target1, r1, cases1, def1), Case (_, target2, r2, cases2, def2)) -> (* FIXME The termination of this case conversion is very @@ -410,13 +403,11 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | Call (f, args) -> (f, args) | _ -> (etype, []) in (* 2. Build the substitution for the inductive arguments *) - let fargs, ctors = + let ctors = (match lexp'_whnf it ctx with - | Inductive (_, _, fargs, constructors) - -> fargs, constructors + | Inductive (_, _, constructors) + -> constructors | _ -> Log.log_fatal ("Case of non-inductive in conv_p")) in - let fargs_subst = List.fold_left2 (fun s _farg (_, aarg) -> S.cons aarg s) - S.identity fargs aargs in (* 3. Compare the branches *) let ctx_extend_with_eq ctx subst hlxp = let tlxp = mkSusp target subst in @@ -450,7 +441,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = vdefs1 vdefs2 fieldtypes else None | _,_,_ -> None in - match mkctx ctx [] fargs_subst (List.length fields1) + match mkctx ctx [] Subst.identity (List.length fields1) fields1 fields2 fieldtypes with | None -> false | Some (nctx, args, _subst) -> @@ -620,9 +611,8 @@ and check'' erased ctx e = -> ((* error_tc ~loc:(lexp_location e) "Reached unreachable sort!"; * Log.internal_error "Reached unreachable sort!"; *) DB.sort_omega) - | Builtin (_, t, _) + | Builtin (_, t) -> let _ = check_type DB.set_empty Myers.nil t in - (* FIXME: Check the attributemap as well! *) t (* FIXME: Check recursive references. *) | Var (((l, name), idx) as v) @@ -695,53 +685,42 @@ and check'' erased ctx e = ^ lexp_string ft ^ ")!"); ft)) ft args - | Inductive (l, label, args, cases) - -> let rec arg_loop ctx erased args = - match args with - | [] - -> let level - = SMap.fold - (fun _ case level -> - let (level, _, _, _) = - List.fold_left - (fun (level, ictx, erased, n) (ak, v, t) -> - ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in - match lexp_lexp' lwhnf with - | Sort (_, Stype _) - when ak == P.Aerasable && impredicative_erase - -> level - | Sort (_, Stype level') - -> mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (* FIXME: If it does refer, - * we get an ugly error! *) - (mkSusp level' (L.sunshift n)) - | tt -> error_tc ~loc:(lexp_location t) - ~print_action:(fun _ -> - DB.print_lexp_ctx ictx; print_newline () - ) - ("Field type " - ^ lexp_string t - ^ " is not a Type! (" - ^ lexp_string lwhnf ^")"); - level), - DB.lctx_extend ictx v Variable t, - DB.set_sink 1 erased, - n + 1)) - (level, ctx, erased, 0) - case in - level) - cases (mkSortLevel SLz) in - mkSort (l, Stype level) - | (ak, v, t)::args - -> let _k = check_type DB.set_empty ctx t in - mkArrow (ak, v, t, lexp_location t, - arg_loop (DB.lctx_extend ctx v Variable t) - (dbset_push ak erased) - args) in - let tct = arg_loop ctx erased args in - tct + | Inductive (l, label, cases) + -> let level + = SMap.fold + (fun _ case level -> + let (level, _, _, _) = + List.fold_left + (fun (level, ictx, erased, n) (ak, v, t) -> + ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in + match lexp_lexp' lwhnf with + | Sort (_, Stype _) + when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + -> mkSLlub ctx level + (* We need to unshift because the final type + * cannot refer to the fields! *) + (* FIXME: If it does refer, + * we get an ugly error! *) + (mkSusp level' (L.sunshift n)) + | tt -> error_tc ~loc:(lexp_location t) + ~print_action:(fun _ -> + DB.print_lexp_ctx ictx; print_newline () + ) + ("Field type " + ^ lexp_string t + ^ " is not a Type! (" + ^ lexp_string lwhnf ^")"); + level), + DB.lctx_extend ictx v Variable t, + DB.set_sink 1 erased, + n + 1)) + (level, ctx, erased, 0) + case in + level) + cases (mkSortLevel SLz) in + mkSort (l, Stype level) | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = @@ -758,17 +737,13 @@ and check'' erased ctx e = "Target lexp's kind is not a sort"; DB.level0 in let it, aargs = call_split etype in (match lexp'_whnf it ctx, aargs with - | Inductive (_, _, fargs, constructors), aargs -> - let rec mksubst s fargs aargs = - match fargs, aargs with - | [], [] -> s - | _farg::fargs, (_ak, aarg)::aargs - (* We don't check aarg's type, because we assume that `check` - * returns a valid type. *) - -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (error_tc ~loc:l - "Wrong arg number to inductive type!"; s) in - let s = mksubst S.identity fargs aargs in + | Inductive (_, _, constructors), aargs -> + let () = match aargs with + | [] -> () + | _ + -> let message = "Wrong arg number to inductive type!" in + error_tc ~loc:l message + in let ctx_extend_with_eq ctx subst hlxp nerased = let tlxp = mkSusp e subst in let tltp = mkSusp etype subst in @@ -803,7 +778,7 @@ and check'' erased ctx e = mkCall (mkCons (it, (l, name)), List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in let (nerased, nctx, hlxp) = - mkctx erased ctx s hctor vdefs fieldtypes in + mkctx erased ctx Subst.identity hctor vdefs fieldtypes in let subst = S.shift (List.length vdefs) in let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in assert_type nctx branch @@ -831,29 +806,18 @@ and check'' erased ctx e = ret | Cons (t, (l, name)) -> (match lexp'_whnf t ctx with - | Inductive (l, _, fargs, constructors) + | Inductive (l, _, constructors) -> (try let fieldtypes = SMap.find name constructors in - let rec indtype fargs start_index = - match fargs with - | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) - :: indtype fargs (start_index - 1) in let rec fieldargs ftypes = match ftypes with - | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), - indtype fargs (nargs - 1)) + | [] -> let nargs = List.length fieldtypes in + mkCall (mkSusp t (S.shift nargs), []) | (ak, vd, ftype) :: ftypes -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) in - let rec buildtype fargs = - match fargs with - | [] -> fieldargs fieldtypes - | (ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, - buildtype fargs) in - buildtype fargs + fieldargs ftypes) + in + fieldargs fieldtypes with Not_found -> (error_tc ~loc:l ("Constructor "" ^ name ^ "" does not exist"); @@ -940,23 +904,19 @@ and fv (e : lexp) : (DB.set * mv_set) = then fv_erase afvs else afvs)) (fv f) args - | Inductive (_, _, args, cases) - -> let alen = List.length args in - let s - = List.fold_left (fun s (_, _, t) - -> fv_sink 1 (fv_union s (fv t))) - fv_empty args in - let s - = SMap.fold - (fun _ fields s - -> fv_union + | Inductive (_, _, cases) + -> let s = + SMap.fold + (fun _ fields s + -> fv_union s (fv_hoist (List.length fields) (List.fold_left (fun s (_, _, t) -> fv_sink 1 (fv_union s (fv t))) fv_empty fields))) - cases s in - fv_hoist alen s + cases fv_empty + in + fv_hoist 0 s | Cons (t, _) -> fv_erase (fv t) | Case (_, e, t, cases, def) -> let s = fv_union (fv e) (fv_erase (fv t)) in @@ -990,7 +950,7 @@ and get_type ctx e = | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) -> DB.type_int - | Builtin (_, t, _) -> t + | Builtin (_, t) -> t | SortLevel _ -> DB.type_level | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega @@ -1021,67 +981,48 @@ and get_type ctx e = -> mkSusp t2 (S.substitute arg) | _ -> ft) ft args - | Inductive (l, label, args, cases) + | Inductive (l, label, cases) (* FIXME: Use `check` here but silencing errors? *) - -> let rec arg_loop args ctx = - match args with - | [] - -> let level - = SMap.fold - (fun _ case level -> - let (level, _, _) = - List.fold_left - (fun (level, ictx, n) (ak, v, t) -> - ((match lexp'_whnf (get_type ictx t) ictx with - | Sort (_, Stype _) - when ak == P.Aerasable && impredicative_erase - -> level - | Sort (_, Stype level') - -> mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (mkSusp level' (L.sunshift n)) - | tt -> level), - DB.lctx_extend ictx v Variable t, - n + 1)) - (level, ctx, 0) - case in - level) - cases (mkSortLevel SLz) in - mkSort (l, Stype level) - | (ak, v, t)::args - -> mkArrow (ak, v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx v Variable t)) in - let tct = arg_loop args ctx in - tct + -> let level + = SMap.fold + (fun _ case level -> + let (level, _, _) = + List.fold_left + (fun (level, ictx, n) (ak, v, t) -> + ((match lexp'_whnf (get_type ictx t) ictx with + | Sort (_, Stype _) + when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + -> mkSLlub ctx level + (* We need to unshift because the final type + * cannot refer to the fields! *) + (mkSusp level' (L.sunshift n)) + | tt -> level), + DB.lctx_extend ictx v Variable t, + n + 1)) + (level, ctx, 0) + case in + level) + cases (mkSortLevel SLz) in + mkSort (l, Stype level) | Case (l, e, ret, branches, default) -> ret | Cons (t, (l, name)) -> (match lexp'_whnf t ctx with - | Inductive (l, _, fargs, constructors) - -> (try - let fieldtypes = SMap.find name constructors in - let rec indtype fargs start_index = - match fargs with - | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) - :: indtype fargs (start_index - 1) in - let rec fieldargs ftypes = - match ftypes with - | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), - indtype fargs (nargs - 1)) - | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) in - let rec buildtype fargs = - match fargs with - | [] -> fieldargs fieldtypes - | (ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, - buildtype fargs) in - buildtype fargs - with Not_found -> DB.type_int) - | _ -> DB.type_int) + | Inductive (l, _, constructors) + -> (try + let fieldtypes = SMap.find name constructors in + let rec fieldargs ftypes = + match ftypes with + | [] -> let nargs = List.length fieldtypes in + mkCall (mkSusp t (S.shift nargs), + []) + | (ak, vd, ftype) :: ftypes + -> mkArrow (ak, vd, ftype, lexp_location ftype, + fieldargs ftypes) in + fieldargs fieldtypes + with Not_found -> DB.type_int) + | _ -> DB.type_int) | Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> get_type ctx (push_susp e s) @@ -1101,10 +1042,10 @@ let erasure_dummy = DB.type0

let rec erase_type (lxp: lexp): E.elexp = match lexp_lexp' lxp with - | L.Imm(s) -> E.Imm(s) - | L.Builtin(v, _, _) -> E.Builtin(v) - | L.Var(v) -> E.Var(v) - | L.Cons(_, s) -> E.Cons(s) + | L.Imm(s) -> E.Imm(s) + | L.Builtin(v, _) -> E.Builtin(v) + | L.Var(v) -> E.Var(v) + | L.Cons(_, s) -> E.Cons(s) | L.Lambda (P.Aerasable, _, _, body) -> erase_type (L.push_susp body (S.substitute erasure_dummy)) | L.Lambda (_, vdef, _, body) -> @@ -1123,11 +1064,11 @@ let rec erase_type (lxp: lexp): E.elexp = | L.Susp(l, s) -> erase_type (L.push_susp l s)

(* To be thrown out *) - | L.Arrow _ -> E.Type lxp - | L.SortLevel _ -> E.Type lxp - | L.Sort _ -> E.Type lxp + | L.Arrow _ -> E.Type lxp + | L.SortLevel _ -> E.Type lxp + | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) - | L.Inductive(l, label, _, _) -> E.Type lxp + | L.Inductive (l, label, _) -> E.Type lxp | L.Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> erase_type (push_susp e s) @@ -1208,7 +1149,7 @@ let ctx2tup ctx nctx = let types = List.rev types in (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*)

- mkCall (mkCons (mkInductive (loc, type_label, [], + mkCall (mkCons (mkInductive (loc, type_label, SMap.add cons_name (List.map (fun (oname, t) -> (P.Aimplicit, oname,

===================================== src/unification.ml ===================================== @@ -79,13 +79,13 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Lambda (_, _, t, e) -> oi t || oi e | Call (f, args) -> List.fold_left (fun o (_, arg) -> o || oi arg) (oi f) args - | Inductive (_, _, args, cases) + | Inductive (_, _, cases) -> SMap.fold (fun _ fields o -> List.fold_left (fun o (_, _, t) -> o || oi t) o fields) cases - (List.fold_left (fun o (_, _, t) -> o || oi t) false args) + false | Cons (t, _) -> oi t | Case (_, e, t, cases, def) -> let o = oi e || oi t in @@ -565,12 +565,12 @@ and is_same arglist arglist2 =

and unify_inductive lxp1 lxp2 ctx vs = match lexp_lexp' lxp1, lexp_lexp' lxp2 with - | (Inductive (_loc1, label1, args1, consts1), - Inductive (_loc2, label2, args2, consts2)) - -> unify_inductive' ctx vs args1 args2 consts1 consts2 lxp1 lxp2 + | (Inductive (_loc1, label1, consts1), + Inductive (_loc2, label2, consts2)) + -> unify_inductive' ctx vs consts1 consts2 lxp1 lxp2 | _, _ -> [(CKimpossible, ctx, lxp1, lxp2)]

-and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = +and unify_inductive' ctx vs consts1 consts2 e1 e2 = let unif_formals ctx vs args1 args2 = if not (List.length args1 == List.length args2) then (ctx, vs, [(CKimpossible, ctx, e1, e2)]) @@ -582,7 +582,6 @@ and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = else (unify' t1 t2 ctx vs) @ residue)) (ctx, vs, []) (List.combine args1 args2) in - let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in if not (SMap.cardinal consts1 == SMap.cardinal consts2) then [(CKimpossible, ctx, e1, e2)] else @@ -592,7 +591,7 @@ and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = = unif_formals ctx vs args1 args2 in residue' @ residue | exception Not_found -> [(CKimpossible, ctx, e1, e2)]) - consts1 residue + consts1 []

(** unify the SMap of list in Inductive *) (* and unify_induct_sub_list l1 l2 subst =

===================================== tests/elab_test.ml ===================================== @@ -216,4 +216,10 @@ test = (getProof (decideBoolEq : Decidable (Eq true true)) : Eq true true); |}

+let _ = add_elab_test_expr + "Instanciate implicit arguments in datacons" + ~setup:"A = typecons (A (prop : Type_ ?ℓ)) (c (p ::: prop));" + ~expected:"datacons (A (ℓ := ?ℓ)) c" + "datacons A c" + let _ = run_all ()

===================================== tests/utest_main.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -30,32 +30,34 @@ * * --------------------------------------------------------------------------- *)

-open Fmt +(** Search *_test.byte executable and run them. + Usage: + ./utest_main tests_folder root_folder *)

-let cut_name str = - String.sub str 0 (String.length str - 12) +open Fmt

let global_verbose_lvl = ref 5 -let global_sample_dir = ref "./" -let global_tests_dir = ref "./_build/tests/" +let global_sample_dir = ref "." +let global_tests_dir = ref (Filename.concat "_build" "tests") let global_fsection = ref "" let global_ftitle = ref "" let global_filter = ref false

-let arg_defs = [ +let arg_defs = + [ ("--verbose", - Arg.Int (fun g -> global_verbose_lvl := g), " Set verbose level"); + Arg.Set_int global_verbose_lvl, " Set verbose level"); ("--samples", - Arg.String (fun g -> global_sample_dir := g), " Set sample directory"); + Arg.Set_string global_sample_dir, " Set sample directory"); ("--tests", - Arg.String (fun g -> global_tests_dir := g), " Set tests directory"); + Arg.Set_string global_tests_dir, " Set tests directory"); (* Allow users to select which test to run *) ("--fsection", Arg.String (fun g -> global_fsection := String.uppercase_ascii g; - global_filter := true), " Set test filter"); + global_filter := true), " Set test filter"); ("--ftitle", Arg.String (fun g -> global_ftitle := String.uppercase_ascii g; - global_filter := true), " Set test filter"); + global_filter := true), " Set test filter"); ]

@@ -69,99 +71,114 @@ let cut_byte str = String.sub str 0 ((String.length str) - 10) let cut_native str = String.sub str 0 ((String.length str) - 12)

let cut_name str = - if (Filename.check_suffix str "_test.byte") - then (cut_byte str) - else (cut_native str) + if Filename.check_suffix str "_test.byte" + then cut_byte str + else cut_native str

let print_file_name i n name pass = - let line_size = 80 - (String.length (cut_name name)) - 16 in - let name = cut_name name in - - (if pass then print_string green else print_string red); - print_string " ("; - ralign_print_int i 2; print_string "/"; - ralign_print_int n 2; print_string ") "; - print_string name; - print_string (make_line '.' line_size); - if pass then print_string "..OK\n" else print_string "FAIL\n"; - print_string reset + let line_size = 80 - (String.length (cut_name name)) - 16 in + let name = cut_name name in + + (if pass then print_string green else print_string red); + print_string " ("; + ralign_print_int i 2; print_string "/"; + ralign_print_int n 2; print_string ") "; + print_string name; + print_string (make_line '.' line_size); + if pass then print_string "..OK\n" else print_string "FAIL\n"; + print_string reset

let must_run str = - not (!global_filter) + not !global_filter || String.uppercase_ascii (cut_name str) = !global_fsection

-(* search *_test.byte executable en run them - Usage: - ./utest_main tests_folder root_folder *) let main () = - parse_args (); - - print_string "\n"; - calign_print_string " Running Unit Test " 80; - print_string "\n\n"; - - (*print_string ("[ ] Test folder: " ^ folder ^ "\n"); *) - - (* get tests files *) - let folder = !global_tests_dir in - let root_folder = !global_sample_dir in - - let files = try Sys.readdir folder - with e ->( - print_string ("The folder: " ^ (! global_tests_dir) ^ " does not exist.\n" ^ - "Have you tried "./utests --tests= ./tests" ?\n"); - raise e; - ) in - - let check name = - if (Filename.check_suffix name "_test.byte") || - (Filename.check_suffix name "_test.native") then true else false in - - (* select files that are executable tests *) - let files = Array.fold_left - (fun acc elem -> if check elem then elem::acc else acc) - [] files in - - let files_n = List.length files in - - (if files_n = 0 then ( - print_string "No tests were found. Did you compiled them? \n")); - - let exit_code = ref 0 in - let failed_test = ref 0 in - let tests_n = ref 0 in - let test_args = - ["--samples"; root_folder; - "--verbose"; (string_of_int !global_verbose_lvl)] @ - (if not (!global_ftitle = "") then - ["--ftitle"; !global_ftitle] else []) in - - List.iter (fun file -> - flush stdout; - - if must_run file then ( - tests_n := !tests_n + 1; - let command = String.concat " " (List.map Filename.quote - ((folder ^ file)::test_args)) in - exit_code := Sys.command command; - - (if !exit_code != 0 then( - (if verbose 1 then print_file_name (!tests_n) files_n file false); - failed_test := !failed_test + 1) - else - (if verbose 1 then print_file_name (!tests_n) files_n file true); - ); - - (if verbose 2 then print_newline ()); - - ); - - ) files; - - print_string "\n\n"; - print_string " Test Ran : "; print_int !tests_n; - print_string "\n Test Failed : "; print_int !failed_test; - print_string "\n Test Passed : "; print_int (!tests_n - !failed_test); - print_endline "\n" + parse_args (); + + print_string "\n"; + calign_print_string " Running Unit Test " 80; + print_string "\n\n"; + + (*print_string ("[ ] Test folder: " ^ folder ^ "\n"); *) + + (* get tests files *) + let folder = !global_tests_dir in + let root_folder = !global_sample_dir in + + let files = + try Sys.readdir folder + with + | e + -> (print_string ("The folder: " ^ !global_tests_dir + ^ " does not exist.\n" + ^ "Have you tried "./utests --tests= ./tests" ?\n"); + raise e) + in + + let check name = + Filename.check_suffix name "_test.byte" + || Filename.check_suffix name "_test.native" + in + + (* select files that are executable tests *) + let files = Array.fold_left + (fun acc elem -> if check elem then elem::acc else acc) + [] files in + + let files_n = List.length files in + + (if files_n = 0 then + print_string "No tests were found. Did you compiled them? \n"); + + let exit_code = ref 0 in + let failed_test = ref 0 in + let tests_n = ref 0 in + let test_args = + ["--samples"; root_folder; + "--verbose"; string_of_int !global_verbose_lvl] + @ (if not (!global_ftitle = "") then + ["--ftitle"; !global_ftitle] else []) in + + let run_file test_path = + flush stdout; + + tests_n := !tests_n + 1; + let command_parts = Filename.concat folder test_path :: test_args in + let command_parts = + if Sys.os_type = "Win32" + then + (* I wish Filename.quote could be used on Windows. + + It would be appropriate if Ocaml spawned the process through the C + API, but Sys.command passes does it through the shell, which is + cmd.exe and has its own quoting rules. Ocaml has + Filename.quote_command, which does the right thing on every platform, + but it is only available since Ocaml 4.10. Until then, let's hope the + command does not need to be escaped. *) + command_parts + else List.map Filename.quote command_parts + in + + print_endline (String.concat " " command_parts); + exit_code := Sys.command (String.concat " " command_parts); + + (if !exit_code != 0 + then + ((if verbose 1 then print_file_name !tests_n files_n test_path false); + failed_test := !failed_test + 1) + else + (if verbose 1 then print_file_name !tests_n files_n test_path true); + ); + + (if verbose 2 then print_newline ()); + in + + List.iter run_file (List.filter must_run files); + + print_string "\n\n"; + print_string " Test Ran : "; print_int !tests_n; + print_string "\n Test Failed : "; print_int !failed_test; + print_string "\n Test Passed : "; print_int (!tests_n - !failed_test); + print_endline "\n"

let _ = main ();

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/613a880662f091a5b0cbda29ea495b6f8...