Stefan pushed to branch master at Stefan / Typer

Commits: 76a477f1 by Stefan Monnier at 2018-09-21T02:27:11Z Get rid of identifiers starting with underscore in *.ml

- - - - -

8 changed files:

- src/REPL.ml - src/debruijn.ml - src/debug.ml - src/debug_util.ml - src/elab.ml - src/eval.ml - src/lexp.ml - src/unification.ml

Changes:

===================================== src/REPL.ml ===================================== @@ -103,21 +103,21 @@ type lexpr = lexp (* Grouping declaration together will enable us to support mutually recursive * declarations while bringing us closer to normal typer *) let ipexp_parse (sxps: sexp list): (sexp list * sexp list) = - let rec _pxp_parse sxps dacc pacc = + let rec pxp_parse sxps dacc pacc = match sxps with | [] -> (List.rev dacc), (List.rev pacc) | sxp::tl -> match sxp with (* Declaration *) | Node (Symbol (_, ("_=_" | "_:_")), [Symbol s; t]) -> - _pxp_parse tl (sxp :: dacc) pacc + pxp_parse tl (sxp :: dacc) pacc

(* f arg1 arg2 = function body; *) | Node (Symbol (_, "_=_"), [Node (Symbol s, args); t]) -> - _pxp_parse tl (sxp :: dacc) pacc + pxp_parse tl (sxp :: dacc) pacc

(* Expression *) - | _ -> _pxp_parse tl dacc (sxp::pacc) in - _pxp_parse sxps [] [] + | _ -> pxp_parse tl dacc (sxp::pacc) in + pxp_parse sxps [] []

let ierase_type (lexps: (ldecl list list * lexpr list)) =

===================================== src/debruijn.ml ===================================== @@ -257,7 +257,7 @@ let print_lexp_ctx_n (ctx : lexp_context) start =

let ord = extract_names ctx [] in

- let rec _print idx ord = + let rec print idx ord = match ord with | [] -> () | hd::tl ->( @@ -281,7 +281,7 @@ let print_lexp_ctx_n (ctx : lexp_context) start = let _ = match exp with | None -> print_string "<var>" | Some exp -> ( - let str = _lexp_str (!debug_ppctx) exp in + let str = lexp_str (!debug_ppctx) exp in let str = (match str_split str '\n' with | hd::tl -> print_string hd; tl | _ -> []) in @@ -291,12 +291,12 @@ let print_lexp_ctx_n (ctx : lexp_context) start =

print_string (": "); lexp_print tp; print_string "\n";

- _print (idx + 1) tl + print (idx + 1) tl

with Not_found -> - (print_string "Not_found |\n"; _print (idx + 1) tl)) in + (print_string "Not_found |\n"; print (idx + 1) tl)) in

- _print (start - 1) ord; print_string (make_sep '=') + print (start - 1) ord; print_string (make_sep '=')

(* Only print user defined variables *)

===================================== src/debug.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -131,7 +131,7 @@ let debug_lexp_decls decls = lalign_print_string (lexp_name lxp) 15; print_string "["; loc_print loc; print_string "]";

- let str = _lexp_str_decls (!debug_ppctx) [e] in + let str = lexp_str_decls (!debug_ppctx) [e] in

(* First col size = 15 + 1 + 2 + 3 + 5 + 6 * = 32 *)

===================================== src/debug_util.ml ===================================== @@ -183,7 +183,7 @@ let format_source () =

print_string (make_sep '-'); print_string "\n";

- let result = _lexp_str_decls (!ppctx) (List.flatten lexps) in + let result = lexp_str_decls (!ppctx) (List.flatten lexps) in

if (!write_file) then ( print_string (" " ^ " Writing output file: " ^ (!format_dest) ^ "\n");

===================================== src/elab.ml ===================================== @@ -1012,7 +1012,7 @@ and lexp_decls_1 (pending_defs : (symbol * sexp) list) (* Pending definitions. *) : (vname * lexp * ltype) list * sexp list * elab_context =

- let rec _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs = + let rec lexp_decls_1 sdecls ectx nctx pending_decls pending_defs = match sdecls with | [] -> (if not (SMap.is_empty pending_decls) then let (s, l) = SMap.choose pending_decls in @@ -1022,10 +1022,10 @@ and lexp_decls_1 [], [], nctx

| Symbol (_, "") :: sdecls - -> _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + -> lexp_decls_1 sdecls ectx nctx pending_decls pending_defs

| Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls') :: sdecls - -> _lexp_decls_1 (List.append sdecls' sdecls) + -> lexp_decls_1 (List.append sdecls' sdecls) ectx nctx pending_decls pending_defs

| Node (Symbol (l, "_:_"), args) :: sdecls @@ -1048,17 +1048,17 @@ and lexp_decls_1 ^ lexp_string ltp ^ "` incompatible with previous `" ^ lexp_string pt ^ "`") | Some [] -> () in - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then (error l ("Variable `" ^ vname ^ "` already defined!"); - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - else _lexp_decls_1 sdecls ectx + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + else lexp_decls_1 sdecls ectx (ectx_extend nctx (l, Some vname) ForwardRef ltp) (SMap.add vname l pending_decls) pending_defs | _ -> error l "Invalid type declaration syntax"; - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)

| Node (Symbol (l, "_=_") as head, args) :: sdecls (* FIXME: Move this to a "special form"! *) @@ -1090,15 +1090,15 @@ and lexp_decls_1 let decls, nctx = lexp_check_decls ectx nctx pending_defs in decls, sdecls, nctx else - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs

else (error l ("`" ^ vname ^ "` defined but not declared!"); - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)

| [Node (Symbol s, args) as d; body] -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *) - _lexp_decls_1 ((Node (head, + lexp_decls_1 ((Node (head, [Symbol s; Node (Symbol (sexp_location d, "lambda_->_"), [sexp_u_list args; body])])) @@ -1106,25 +1106,25 @@ and lexp_decls_1 ectx nctx pending_decls pending_defs

| _ -> error l "Invalid definition syntax"; - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)

| Node (Symbol (l, "define-operator"), args) :: sdecls (* FIXME: Move this to a "special form"! *) - -> _lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None) + -> lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None) pending_decls pending_defs

| Node (Symbol ((l, _) as v), sargs) :: sdecls -> (* expand macro and get the generated declarations *) let sdecl' = lexp_decls_macro v sargs nctx in - _lexp_decls_1 (sdecl' :: sdecls) ectx nctx + lexp_decls_1 (sdecl' :: sdecls) ectx nctx pending_decls pending_defs

| sexp :: sdecls -> error (sexp_location sexp) "Invalid declaration syntax"; - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs

in (EV.set_getenv nctx; - let res = _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in + let res = lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in (stop_on_error (); res))

and lexp_p_decls (sdecls : sexp list) (ctx : elab_context)

===================================== src/eval.ml ===================================== @@ -365,10 +365,10 @@ let file_write loc depth args_val = match args_val with | _ -> List.iter (fun v -> value_print v) args_val; error loc "File.write expects an out_channel and a string"

-let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) = +let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) =

let trace = append_eval_trace trace lxp in - let eval lxp ctx = _eval lxp ctx trace in + let eval' lxp ctx = eval lxp ctx trace in

(* This creates an O(N^2) cost for deep recursion because rec_depth * uses `length` on the stack trace. *) @@ -398,14 +398,14 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type (* Nodes *) (* ---------------- *) | Let(_, decls, inst) - -> let nctx = _eval_decls decls ctx trace in - eval inst nctx + -> let nctx = eval_decls decls ctx trace in + eval' inst nctx

(* Function call *) | Call (f, args) -> eval_call (elexp_location f) f trace - (_eval f ctx trace) - (List.map (fun e -> _eval e ctx trace) args) + (eval f ctx trace) + (List.map (fun e -> eval e ctx trace) args)

(* Case *) | Case (loc, target, pat, dflt) @@ -451,8 +451,8 @@ and eval_call loc unef i f args = -> bindargs e vs (add_rte_variable x v ctx) | ([], _) -> let trace = append_typer_trace i unef in - _eval e ctx trace - | _ -> eval_call loc unef i (_eval e ctx i) vs in + eval e ctx trace + | _ -> eval_call loc unef i (eval e ctx i) vs in bindargs e vs (add_rte_variable x v ctx)

| Vbuiltin (name), args @@ -496,7 +496,7 @@ and eval_call loc unef i f args =

and eval_case ctx i loc target pat dflt = (* Eval target *) - let v = _eval target ctx i in + let v = eval target ctx i in

(* extract constructor name and arguments *) let ctor_name, args = match v with @@ -521,23 +521,23 @@ and eval_case ctx i loc target pat dflt = | [], [] -> nctx in

let nctx = fold2 ctx pat_args args in - _eval exp nctx i + eval exp nctx i

(* Run default *) with Not_found -> (match dflt with | Some (var, lxp) - -> _eval lxp (add_rte_variable var v ctx) i + -> eval lxp (add_rte_variable var v ctx) i | _ -> error loc "Match Failure")

and build_arg_list args ctx i = - (* _eval every args *) - let arg_val = List.map (fun (k, e) -> _eval e ctx i) args in + (* eval every args *) + let arg_val = List.map (fun (k, e) -> eval e ctx i) args in

(* Add args inside context *) List.fold_left (fun c v -> add_rte_variable vdummy v c) ctx arg_val

-and _eval_decls (decls: (vname * elexp) list) - (ctx: runtime_env) i: runtime_env = +and eval_decls (decls: (vname * elexp) list) + (ctx: runtime_env) i: runtime_env =

let n = (List.length decls) - 1 in

@@ -546,7 +546,7 @@ and _eval_decls (decls: (vname * elexp) list) add_rte_variable name Vundefined ctx) ctx decls in

List.iteri (fun idx (name, lxp) -> - let v = _eval lxp nctx i in + let v = eval lxp nctx i in let offset = n - idx in ignore (set_rte_variable offset name v nctx)) decls;

@@ -559,7 +559,7 @@ and _eval_decls (decls: (vname * elexp) list) (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) and sexp_dispatch loc depth args = - let eval a b = _eval a b depth in + let eval a b = eval a b depth in let sxp, nd, ctx_nd, sym, ctx_sym, str, ctx_str, @@ -1048,7 +1048,7 @@ let register_builtin_constants () = ] let _ = register_builtin_constants ()

-let eval lxp ctx = _eval lxp ctx ([], []) +let eval lxp ctx = eval lxp ctx ([], [])

let debug_eval lxp ctx = try eval lxp ctx @@ -1058,7 +1058,7 @@ let debug_eval lxp ctx = raise e)

-let eval_decls decls ctx = _eval_decls decls ctx ([], []) +let eval_decls decls ctx = eval_decls decls ctx ([], [])

let eval_decls_toplevel (decls: (vname * elexp) list list) ctx = (* Add toplevel decls function *)

===================================== src/lexp.ml ===================================== @@ -670,15 +670,15 @@ and lexp_string e = lexp_cstring (!debug_ppctx) e

(* Context Print *) and lexp_cprint ctx e = print_string (lexp_cstring ctx e) -and lexp_cstring ctx e = _lexp_str ctx e +and lexp_cstring ctx e = lexp_str ctx e

(* Implementation *) -and _lexp_str ctx (exp : lexp) : string = +and lexp_str ctx (exp : lexp) : string =

let ctx = set_parent exp ctx in let inter_ctx = add_indent ctx 1 in - let lexp_str = _lexp_str ctx in - let lexp_stri idt e = _lexp_str (add_indent ctx idt) e in + let lexp_str' = lexp_str ctx in + let lexp_stri idt e = lexp_str (add_indent ctx idt) e in

let pretty = pp_pretty ctx in let color = pp_color ctx in @@ -731,7 +731,7 @@ and _lexp_str ctx (exp : lexp) : string = | Float (_, s) -> tval (string_of_float s) | e -> sexp_string e)

- | Susp (e, s) -> _lexp_str ctx (push_susp e s) + | Susp (e, s) -> lexp_str ctx (push_susp e s)

| Var ((loc, name), idx) -> maybename name ^ (index idx) ;

@@ -739,7 +739,7 @@ and _lexp_str ctx (exp : lexp) : string = (* print metavar result if any *) -> (let print_meta exp = let ctx = set_meta exp ctx in - _lexp_str ctx (clean exp) in + lexp_str ctx (clean exp) in

match pp_meta ctx with | None -> print_meta exp @@ -750,7 +750,7 @@ and _lexp_str ctx (exp : lexp) : string = | Let (_, decls, body) -> (* Print first decls without indent *) let h1, decls, idt_lvl = - match _lexp_str_decls inter_ctx decls with + match lexp_str_decls inter_ctx decls with | h1::decls -> h1, decls, 2 | _ -> "", [], 1 in

@@ -767,32 +767,32 @@ and _lexp_str ctx (exp : lexp) : string = (make_indent idt_lvl) ^ (lexp_stri idt_lvl body)

| Arrow(k, (_, Some name), tp, loc, expr) -> - "(" ^ name ^ " : " ^ (lexp_str tp) ^ ") " ^ - (kind_str k) ^ " " ^ (lexp_str expr) + "(" ^ name ^ " : " ^ (lexp_str' tp) ^ ") " ^ + (kind_str k) ^ " " ^ (lexp_str' expr)

| Arrow(k, (_, None), tp, loc, expr) -> - "(" ^ (lexp_str tp) ^ " " - ^ (kind_str k) ^ " " ^ (lexp_str expr) ^ ")" + "(" ^ (lexp_str' tp) ^ " " + ^ (kind_str k) ^ " " ^ (lexp_str' expr) ^ ")"

| Lambda(k, (loc, name), ltype, lbody) -> - let arg = "(" ^ maybename name ^ " : " ^ (lexp_str ltype) ^ ")" in + let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype) ^ ")" in

(keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ (make_indent 1) ^ (lexp_stri 1 lbody)

| Cons(t, (_, ctor_name)) -> - (keyword "datacons ") ^ (lexp_str t) ^ " " ^ ctor_name + (keyword "datacons ") ^ (lexp_str' t) ^ " " ^ ctor_name

| Call(fname, args) -> let name, idx = get_name fname in let binop_str op (_, lhs) (_, rhs) = - "(" ^ (lexp_str lhs) ^ op ^ (index idx) ^ " " ^ (lexp_str rhs) ^ ")" in + "(" ^ (lexp_str' lhs) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs) ^ ")" in

let print_arg str (arg_type, lxp) = match arg_type with - | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str lxp) - | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str lxp) - | Aexplicit -> str ^ " " ^ (lexp_str lxp) + | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp) + | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp) + | Aexplicit -> str ^ " " ^ (lexp_str' lxp) | _ -> str in (

match args with @@ -800,7 +800,7 @@ and _lexp_str ctx (exp : lexp) : string = binop_str (" " ^ (get_binary_op_name name)) lhs rhs

| _ -> let args = List.fold_left print_arg "" args in - "(" ^ (lexp_str fname) ^ args ^ ")") + "(" ^ (lexp_str' fname) ^ args ^ ")")

| Inductive (_, (_, name), [], ctors) -> (keyword "typecons") ^ " (" ^ name ^") " ^ newline ^ @@ -811,14 +811,14 @@ and _lexp_str ctx (exp : lexp) : string = = List.fold_left (fun str (arg_kind, (_, name), ltype) -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " " - ^ (lexp_str ltype) ^ ")") + ^ (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 str = (keyword "case ") ^ (lexp_str' target) in let arg_str arg = List.fold_left (fun str v -> match v with @@ -861,24 +861,24 @@ and lexp_str_ctor ctx ctors = SMap.fold (fun key value str -> let str = str ^ newline ^ (make_indent 1) ^ "(" ^ key in let str = List.fold_left (fun str (k, _, arg) - -> str ^ " " ^ (_lexp_str ctx arg)) + -> str ^ " " ^ (lexp_str ctx arg)) str value in str ^ ")") ctors ""

-and _lexp_str_decls ctx decls = +and lexp_str_decls ctx decls =

- let lexp_str = _lexp_str ctx in + let lexp_str' = lexp_str ctx in let sepdecl = (if pp_decl ctx then "\n" else "") in

let type_str name lxp = (if pp_type ctx then ( - name ^ " : " ^ (lexp_str lxp) ^ ";") else "") in + name ^ " : " ^ (lexp_str' lxp) ^ ";") else "") in

let ret = List.fold_left (fun str ((_, name), lxp, ltp) -> let name = maybename name in let str = if pp_type ctx then (type_str name ltp)::str else str in - (name ^ " = " ^ (lexp_str lxp) ^ ";" ^ sepdecl)::str) + (name ^ " = " ^ (lexp_str' lxp) ^ ";" ^ sepdecl)::str) [] decls in List.rev ret

===================================== src/unification.ml ===================================== @@ -120,7 +120,7 @@ let unify_and res op = match res with

(** Dispatch to the right unifier.

- If (<code>_unify_X X Y</code>) don't handle the case <b>(X, Y)</b>, it call (<code>unify Y X</code>) + If (<code>unify_X X Y</code>) don't handle the case <b>(X, Y)</b>, it call (<code>unify Y X</code>)

The metavar unifier is the end rule, it can't call unify with its parameter (changing their order) *) @@ -141,17 +141,17 @@ and unify' (e1: lexp) (e2: lexp) | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _) | (Inductive _, Inductive _)) -> if OL.conv_p ctx e1' e2' then Some [] else None - | (l, (Metavar (idx, s, _) as r)) -> _unify_metavar ctx idx s r l - | ((Metavar (idx, s, _) as l), r) -> _unify_metavar ctx idx s l r - | (l, (Call _ as r)) -> _unify_call r l ctx vs' - (* | (l, (Case _ as r)) -> _unify_case r l subst *) - | (Arrow _ as l, r) -> _unify_arrow l r ctx vs' - | (Lambda _ as l, r) -> _unify_lambda l r ctx vs' - | (Call _ as l, r) -> _unify_call l r ctx vs' - (* | (Case _ as l, r) -> _unify_case l r subst *) - (* | (Inductive _ as l, r) -> _unify_induct l r subst *) - | (Sort _ as l, r) -> _unify_sort l r ctx vs' - | (SortLevel _ as l, r) -> _unify_sortlvl l r ctx vs' + | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s r l + | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s l r + | (l, (Call _ as r)) -> unify_call r l ctx vs' + (* | (l, (Case _ as r)) -> unify_case r l subst *) + | (Arrow _ as l, r) -> unify_arrow l r ctx vs' + | (Lambda _ as l, r) -> unify_lambda l r ctx vs' + | (Call _ as l, r) -> unify_call l r ctx vs' + (* | (Case _ as l, r) -> unify_case l r subst *) + (* | (Inductive _ as l, r) -> unify_induct l r subst *) + | (Sort _ as l, r) -> unify_sort l r ctx vs' + | (SortLevel _ as l, r) -> unify_sortlvl l r ctx vs' | _ -> Some (if OL.conv_p ctx e1' e2' then [] else [(e1, e2)])

(********************************* Type specific unify *******************************) @@ -163,7 +163,7 @@ and unify' (e1: lexp) (e2: lexp) - (Arrow, Var) -> Constraint - (_, _) -> None *) -and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs +and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs : return_type = match (arrow, lxp) with | (Arrow (var_kind1, v1, ltype1, _, lexp1), @@ -187,7 +187,7 @@ and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs - Lambda , Let -> Constraint - Lambda , lexp -> unify lexp lambda subst *) -and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = +and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lambda, lxp) with | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) @@ -211,7 +211,7 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = - metavar , metavar -> if Metavar = Metavar then OK else ERROR - metavar , lexp -> OK *) -and _unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) +and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) : return_type = let unif idx s lxp = let t = match metavar_lookup idx with @@ -258,7 +258,7 @@ and _unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) - Call , Call -> UNIFY - Call , lexp -> CONSTRAINT *) -and _unify_call (call: lexp) (lxp: lexp) ctx vs +and unify_call (call: lexp) (lxp: lexp) ctx vs : return_type = match (call, lxp) with | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) @@ -276,15 +276,15 @@ and _unify_call (call: lexp) (lxp: lexp) ctx vs - Case, Case -> try to unify - Case, _ -> Constraint *) -(* and _unify_case (case: lexp) (lxp: lexp) (subst: meta_subst) : return_type = +(* and unify_case (case: lexp) (lxp: lexp) (subst: meta_subst) : return_type = * let merge (_, const) subst_res = match subst_res with * | None -> None * | Some (s', c') -> Some (s', const@c') * in * let match_unify_inner lst smap1 smap2 subst = - * match _unify_inner lst subst with + * match unify_inner lst subst with * | None -> None - * | Some (s, c) -> merge (s, c) (_unify_inner_case (zip (SMap.bindings smap1) (SMap.bindings smap2)) s) + * | Some (s, c) -> merge (s, c) (unify_inner_case (zip (SMap.bindings smap1) (SMap.bindings smap2)) s) * in * let match_lxp_opt lxp_opt1 lxp_opt2 tail smap1 smap2 subst = * match lxp_opt1, lxp_opt2 with @@ -304,15 +304,15 @@ and _unify_call (call: lexp) (lxp: lexp) ctx vs - Inductive, Call/Metavar/Case/Let -> constraint - Inductive, _ -> None *) -(* and _unify_induct (induct: lexp) (lxp: lexp) (subst: meta_subst) : return_type = +(* and unify_induct (induct: lexp) (lxp: lexp) (subst: meta_subst) : return_type = * let transform (a, b, c) (d, e, f) = ((a, Some b, c), (d, Some e, f)) * and merge map1 map2 (subst, const) : return_type = - * match (_unify_induct_sub_list (SMap.bindings map1) (SMap.bindings map2) subst) with + * match (unify_induct_sub_list (SMap.bindings map1) (SMap.bindings map2) subst) with * | Some (s', c') -> Some (s', const@c') * | None -> None * in * let zip_unify lst subst map1 map2 : return_type = - * match _unify_inner_induct lst subst with + * match unify_inner_induct lst subst with * | None -> None * | Some (s, c) -> merge map1 map2 (s, c) * in @@ -329,7 +329,7 @@ and _unify_call (call: lexp) (lxp: lexp) ctx vs - SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR - SortLevel, _ -> ERROR *) -and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = +and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = match sortlvl, lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> Some [] @@ -343,7 +343,7 @@ and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = - Sort, Var -> Constraint - Sort, lexp -> ERROR *) -and _unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = +and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = match sort_, lxp with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs @@ -364,18 +364,18 @@ and is_same arglist arglist2 = | _, _ -> false

(** try to unify the SMap part of the case *) -(* and _unify_inner_case lst subst = +(* and unify_inner_case lst subst = * let merge (_, c) res = * match res with * | Some (s', c') -> Some (s', c@c') * | None -> None * in - * let rec _unify_inner_case list_ subst = + * let rec unify_inner_case list_ subst = * match list_ with * | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::tail when key = key2 -> * (if is_same arglist arglist2 * then ( match unify lxp lxp2 subst with - * | Some (s', c) -> merge (s', c) (_unify_inner_case tail s') + * | Some (s', c) -> merge (s', c) (unify_inner_case tail s') * | None -> None) * else None) * | [] -> Some (subst, []) @@ -383,11 +383,11 @@ and is_same arglist arglist2 = * in (match lst with * | Some [] -> Some (subst, []) * | None -> None - * | Some l -> _unify_inner_case l subst) *) + * | Some l -> unify_inner_case l subst) *)

(***** for Inductive *****) -(** for _unify_induct : unify the formal arg*) -(* and _unify_inner_induct lst subst : return_type = +(** for unify_induct : unify the formal arg*) +(* and unify_inner_induct lst subst : return_type = * let test ((a1, _, l1), (a2, _, l2)) subst : return_type = * if a1 = a2 then unify l1 l2 subst * else None @@ -402,16 +402,16 @@ and is_same arglist arglist2 = * ) None lst *)

(** unify the SMap of list in Inductive *) -(* and _unify_induct_sub_list l1 l2 subst = +(* and unify_induct_sub_list l1 l2 subst = * let test l1 l2 subst = * let merge l1 l2 subst (s, c) = - * match (_unify_induct_sub_list l1 l2 subst) with + * match (unify_induct_sub_list l1 l2 subst) with * | Some (s1, c1) -> Some (s1, c1@c) * | None -> Some (s, c) * in - * let unify_zip lst t1 t2 = match _unify_inner_induct lst subst with + * let unify_zip lst t1 t2 = match unify_inner_induct lst subst with * | Some (s, c) -> merge l1 l2 subst (s, c) - * | None -> (_unify_induct_sub_list t1 t2 subst) + * | None -> (unify_induct_sub_list t1 t2 subst) * in * match l1, l2 with * | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 ->

View it on GitLab: https://gitlab.com/monnier/typer/commit/76a477f15316f73fdf45ebe6b552b04299f6...