Ismaila FALL pushed to branch track-sexp-lexp at Stefan / Typer

Commits: 96adbad9 by “falismai@iro.umontreal.ca” at 2022-04-13T20:02:44+00:00 redac

- - - - -

10 changed files:

- + .idea/misc.xml - + redaction/Rapport Mémoire Typer.zip - src/debruijn.ml - src/debug.ml - src/elexp.ml - src/inverse_subst.ml - src/lexp.ml - src/pexp.ml - src/sexp.ml - src/util.ml

Changes:

===================================== .idea/misc.xml ===================================== @@ -0,0 +1,8 @@ +<?xml version="1.0" encoding="UTF-8"?> +<project version="4"> + <component name="SwUserDefinedSpecifications"> + <option name="specTypeByUrl"> + <map /> + </option> + </component> +</project> \ No newline at end of file

===================================== redaction/Rapport Mémoire Typer.zip ===================================== Binary files /dev/null and "b/redaction/Rapport M\303\251moire Typer.zip" differ

===================================== src/debruijn.ml ===================================== @@ -35,10 +35,10 @@ module Str = Str

open Util - - open Lexp

+open Sexp + module M = Myers open Fmt

@@ -83,21 +83,21 @@ let fatal ?print_action ?loc fmt = (* Type definitions * ---------------------------------- *)

-let dloc = dummy_location +let dloc = dummy_sinfo let type_level_sort = mkSort (dloc, StypeLevel) let sort_omega = mkSort (dloc, StypeOmega) -let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) +let type_level = mkBuiltin ((sexp_location 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) -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_int = mkBuiltin ((sexp_location dloc, "Int"), type0) +let type_integer = mkBuiltin ((sexp_location dloc, "Integer"), type0) +let type_float = mkBuiltin ((sexp_location dloc, "Float"), type0) +let type_string = mkBuiltin ((sexp_location dloc, "String"), type0) +let type_elabctx = mkBuiltin ((sexp_location dloc, "Elab_Context"), type0) let type_eq_type = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in @@ -111,13 +111,13 @@ let type_eq_type = mkVar (tv, 1) , dloc, mkSort (dloc, Stype (mkVar (lv, 3)))))))

-let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) +let type_eq = mkBuiltin ((sexp_location dloc, "Eq"), type_eq_type)

let eq_refl = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in let xv = (dloc, Some "x") in - mkBuiltin ((dloc, "Eq.refl"), + mkBuiltin ((sexp_location dloc, "Eq.refl"), mkArrow (Aerasable, lv, type_level, dloc, mkArrow (Aerasable, tv,

===================================== src/debug.ml ===================================== @@ -119,9 +119,9 @@ let debug_pexp_print ptop = let debug_lexp_decls decls = let sep = " : " in List.iter (fun e -> - let ((loc, _name), lxp, _ltp) = e in + let (((loc: sinfo), _name), lxp, _ltp) = e in

- printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string loc); + printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string (sexp_location loc));

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

===================================== src/elexp.ml ===================================== @@ -36,8 +36,8 @@ open Sexp (* Sexp type *) module U = Util module L = Lexp

-type vname = U.vname -type vref = U.vref +type vname = Sexp.vname +type vref = Sexp.vref type label = symbol

module SMap = U.SMap @@ -53,7 +53,7 @@ type elexp = | Var of vref

(* Recursive `let` binding. *) - | Let of U.location * (vname * elexp) list * elexp + | Let of sinfo * (vname * elexp) list * elexp

(* An anonymous function. *) | Lambda of vname * elexp @@ -71,8 +71,8 @@ type elexp = * Case (l, e, branches, default) * tests the value of `e`, and either selects the corresponding branch * in `branches` or branches to the `default`. *) - | Case of U.location * elexp - * (U.location * vname list * elexp) SMap.t + | Case of sinfo * elexp + * (sinfo * vname list * elexp) SMap.t * (vname * elexp) option

(* A Type expression. There's no useful operation we can apply to it, @@ -82,14 +82,14 @@ type elexp = let rec elexp_location e = match e with | Imm s -> sexp_location s - | Var ((l,_), _) -> l + | Var ((l,_), _) -> sexp_location l | Builtin ((l, _)) -> l - | Let (l,_,_) -> l - | Lambda ((l,_),_) -> l + | Let (l,_,_) -> sexp_location l + | Lambda ((l,_),_) -> sexp_location l | Call (f,_) -> elexp_location f | Cons (_, (l, _)) -> l - | Case (l,_,_,_) -> l - | Type e -> L.lexp_location e + | Case (l,_,_,_) -> sexp_location l + | Type e -> sexp_location (L.lexp_location e)

let elexp_name e =

===================================== src/inverse_subst.ml ===================================== @@ -42,6 +42,7 @@ this program. If not, see http://www.gnu.org/licenses/. *) open Lexp open Util module S = Subst +open Sexp

(** Provide inverse function for computing the inverse of a substitution *)

@@ -94,7 +95,7 @@ let sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - mkVar ((U.dummy_location, None), idx) + mkVar ((dummy_sinfo, None), idx)

(** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables.

===================================== src/lexp.ml ===================================== @@ -33,8 +33,8 @@ open Grammar (* open Unify *) module S = Subst

-type vname = U.vname -type vref = U.vref +type vname = Sexp.vname +type vref = Sexp.vref type meta_id = int (* Identifier of a meta variable. *) type sinfo = sexp

@@ -172,6 +172,14 @@ let metavar_lookup (id : meta_id) : metavar_info with Not_found -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!"

+ + + + + + + + (********************** Hash-consing **********************)

(** Hash-consing test ** @@ -516,25 +524,25 @@ let rec lexp_location e = | SortLevel (SLlub (e, _)) -> lexp_location e | SortLevel SLz -> dummy_sinfo | Imm s -> s - | Var ((l,_),_) -> dummy_sinfo - | Builtin ((l, _), _) -> dummy_sinfo + | Var ((_l,_),_) -> dummy_sinfo + | Builtin ((_l, _), _) -> dummy_sinfo | Let (l,_,_) -> l | Arrow (_,_,_,l,_) -> l - | Lambda (_,(l,_),_,_) -> dummy_sinfo + | Lambda (_,(_l,_),_,_) -> dummy_sinfo | Call (f,_) -> lexp_location f | Inductive (l,_,_,_) -> l - | Cons (_,(l,_)) -> dummy_sinfo + | Cons (_,(_l,_)) -> dummy_sinfo | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) - | Metavar (_,_,(l,_)) -> dummy_sinfo + | Metavar (_,_,(_l,_)) -> dummy_sinfo

(********* Normalizing a term *********)

let vdummy = (U.dummy_location, None) let maybename n = match n with None -> "<anon>" | Some v -> v -let sname (l,n) = (l, maybename n) +let sname (l, n) = (sexp_location l, maybename n)

let rec push_susp e s = (* Push a suspension one level down. *) match lexp_lexp' e with @@ -577,7 +585,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) | Cons (it, name) -> mkCons (mkSusp it s , name) | Case (l, e, ret, cases, default) -> mkCase (l, mkSusp e s , mkSusp ret s , - SMap.map (fun ((l: sinfo), cargs, e) + SMap.map (fun (l, cargs, e) -> let s' = L.fold_left (fun s (_,ov) -> ssink ov s) s cargs in @@ -674,27 +682,27 @@ let rec lexp_unparse lxp = | Imm (sexp) -> sexp | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) - | Var ((loc, name), _) -> Symbol (loc, maybename name) + | Var ((loc, name), _) -> Symbol (sexp_location loc, maybename name) | Cons (t, (l, name)) -> Node (sdatacons, [lexp_unparse t; Symbol (l, name)]) | Lambda (kind, vdef, ltp, body) -> let l = lexp_location lxp in let st = lexp_unparse ltp in - Node (Symbol (l, match kind with + Node (Symbol (sexp_location l, match kind with | Anormal -> "lambda_->_" | Aimplicit -> "lambda_=>_" | Aerasable -> "lambda_≡>_"), - [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); + [Node (Symbol (sexp_location l, "_:_"), [Symbol (sname vdef); st]); lexp_unparse body ]) | Arrow (arg_kind, (l,oname), ltp1, loc, ltp2) -> let ut1 = lexp_unparse ltp1 in - Node (Symbol (loc, match arg_kind with Anormal -> "_->_" + Node (Symbol (sexp_location loc, match arg_kind with Anormal -> "_->_" | Aimplicit -> "_=>_" | Aerasable -> "_≡>_"), [(match oname with None -> ut1 - | Some v -> Node (Symbol (l, "_:_"), - [Symbol (l,v); ut1])); + | Some v -> Node (Symbol (sexp_location l, "_:_"), + [Symbol (sexp_location l,v); ut1])); lexp_unparse ltp2 ])

| Let (loc, ldecls, body) @@ -707,7 +715,7 @@ let rec lexp_unparse lxp = [Symbol (sname vdef); lexp_unparse lxp ]) :: acc) [] ldecls in - Node (Symbol (loc, "let_in_"), + Node (Symbol (sexp_location loc, "let_in_"), [Node (Symbol (U.dummy_location, "_;_"), sdecls); lexp_unparse body ])

@@ -725,7 +733,7 @@ let rec lexp_unparse lxp = Node (Symbol label, List.map pexp_u_formal_arg pfargs) :: List.map (fun (name, types) - -> Node (Symbol (loc, name), + -> Node (Symbol (sexp_location loc, name), List.map (fun arg -> match arg with @@ -749,13 +757,13 @@ let rec lexp_unparse lxp = let pat_args = List.map (fun (_kind, ((l,oname) as name)) -> match oname with - | Some vdef -> (Some (l,vdef), name) + | Some vdef -> (Some (sexp_location l, vdef), name) | None -> (None, name)) args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) in (Ppatcons (Node (sdatacons, - [bt; Symbol (loc, str)]), + [bt; Symbol (sexp_location loc, str)]), pat_args), lexp_unparse bch ) ) (SMap.bindings branches) in @@ -765,29 +773,29 @@ let rec lexp_unparse lxp = lexp_unparse dft )::pbranch | None -> pbranch in let e = lexp_unparse target in - Node (Symbol (loc, "case_"), + Node (Symbol (sexp_location loc, "case_"), e :: List.map (fun (pat, branch) -> - Node (Symbol (pexp_pat_location pat, "_=>_"), + Node (Symbol (sexp_location (pexp_pat_location pat), "_=>_"), [pexp_u_pat pat; branch])) pbranch)

(* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name)) - -> Symbol (loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx + -> Symbol (sexp_location loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx ^ "[" ^ subst_string subst ^ "]")

| SortLevel (SLz) -> Symbol (U.dummy_location, "##TypeLevel.z") | SortLevel (SLsucc l) - -> Node (Symbol (lexp_location l, "##TypeLevel.succ"), + -> Node (Symbol (sexp_location (lexp_location l), "##TypeLevel.succ"), [lexp_unparse l]) | SortLevel (SLlub (l1, l2)) - -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), + -> Node (Symbol (sexp_location (lexp_location l1), "##TypeLevel.∪"), [lexp_unparse l1 ; lexp_unparse l2 ]) - | Sort (l, StypeOmega) -> Symbol (l, "##Type_ω") - | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel.Sort") + | Sort (l, StypeOmega) -> Symbol (sexp_location l, "##Type_ω") + | Sort (l, StypeLevel) -> Symbol (sexp_location l, "##TypeLevel.Sort") | Sort (_l, Stype sl) - -> Node (Symbol (lexp_location sl, "##Type_"), + -> Node (Symbol (sexp_location (lexp_location sl), "##Type_"), [lexp_unparse sl ])

(* FIXME: ¡Unify lexp_print and lexp_string! *)

===================================== src/pexp.ml ===================================== @@ -20,7 +20,7 @@ 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 Util +(*open Util*) open Sexp (* Symbol *)

let pexp_error loc = Log.log_error ~section:"PEXP" ~loc @@ -43,7 +43,7 @@ type ppat =

let pexp_pat_location e = match e with | Ppatsym (l,_) -> l - | Ppatcons (e, _) -> sexp_location e + | Ppatcons (e, _) -> e

let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = match arg with @@ -56,28 +56,28 @@ let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = | None -> Symbol (l, "_")])

let pexp_p_pat_arg (s : sexp) = match s with - | Symbol (l , n) -> (None, (l, match n with "_" -> None | _ -> Some n)) - | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (l,n)]) - -> (Some f, (l, Some n)) + | Symbol (_l , n) -> (None, (s, match n with "_" -> None | _ -> Some n)) + | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (_l,n)]) + -> (Some f, (s, Some n)) | _ -> let loc = sexp_location s in pexp_error loc "Unknown pattern arg"; - (None, (loc, None)) + (None, (s, None))

let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp = - let pname = Symbol (l, match oname with None -> "_" | Some n -> n) in + let pname = Symbol (sexp_location l, match oname with None -> "_" | Some n -> n) in match okn with | None -> pname | Some ((l,_) as n) -> Node (Symbol (l, "_:=_"), [Symbol n; pname])

let pexp_p_pat (s : sexp) : ppat = match s with - | Symbol (l, n) -> Ppatsym (l, match n with "_" -> None | _ -> Some n) + | Symbol (_l, n) -> Ppatsym (s, match n with "_" -> None | _ -> Some n) | Node (c, args) -> Ppatcons (c, List.map pexp_p_pat_arg args) | _ -> let l = sexp_location s in - pexp_error l "Unknown pattern"; Ppatsym (l, None) + pexp_error l "Unknown pattern"; Ppatsym (s, None)

let pexp_u_pat (p : ppat) : sexp = match p with - | Ppatsym (l, None) -> Symbol (l, "_") - | Ppatsym (l, Some n) -> Symbol (l, n) + | Ppatsym (l, None) -> Symbol (sexp_location l, "_") + | Ppatsym (l, Some n) -> Symbol (sexp_location l, n) | Ppatcons (c, args) -> Node (c, List.map pexp_u_pat_arg args)

===================================== src/sexp.ml ===================================== @@ -39,8 +39,15 @@ type sexp = (* Syntactic expression, kind of like Lisp. *) | Node of sexp * sexp list type token = sexp

+type sinfo = sexp +type vname = sinfo * string option +type vref = vname * db_index (*Name redundancy*) + + + let epsilon l = Symbol (l, "") let dummy_epsilon = epsilon dummy_location + let dummy_sinfo = epsilon dummy_location

(********************** Sexp tests **********************)

===================================== src/util.ml ===================================== @@ -33,11 +33,9 @@ let dummy_location = Source.Location.dummy (* Occurrence of a variable's symbol: we use DeBruijn index, and for * debugging purposes, we remember the name that was used in the source * code. *) -type vname = location * string option type db_index = int (* DeBruijn index. *) type db_offset = int (* DeBruijn index offset. *) type db_revindex = int (* DeBruijn index counting from the root. *) -type vref = vname * db_index

type bottom = | B_o_t_t_o_m_ of bottom

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/96adbad9c495b49e977ef61778b70cae23...