open Ast let fst = function (x, _) -> x let snd = function (_, y) -> y let const x = fun _ -> x let env_find env v = let rec index n = function | x :: xs when x = v -> n | _ :: xs -> index (n+1) xs | _ -> raise Not_found in index 0 env let rec comp env = function | TLam (t1, t2) -> ILam (term2pat t1, comp (fillenv env t1) t2) | TApp (t1, t2) -> IApp (comp env t1, comp env t2) | TAlt (t1, t2) -> IAlt (comp env t1, comp env t2) | TVar v -> (try IVar (env_find env v) with Not_found -> IGlobal v) | TInt i -> IInt i | TCons t -> ICons t and term2pat = function | TVar v -> PHole (-1) | TCons t -> PTuple (t, []) | TApp(t1, t2) -> match term2pat t1 with | PTuple(t, vs) -> PTuple(t, vs@[term2pat t2]) | _ -> failwith "invalid pattern" and fillenv env = function | TVar v -> v :: env | TCons t -> env | TApp(t1, t2) -> fillenv (fillenv env t1) t2 let rec desugar = function | TLam (TApp (TCons (v), o), t) -> TLam (TApp (TCons (v), o), desugar t) | TLam (TApp (o1, o2), t) -> desugar (TLam (o1, TLam (desugar o2, desugar t))) | TLam (t1, t2) -> TLam (desugar t1, desugar t2) | TApp (t1, t2) -> TApp (desugar t1, desugar t2) | TAlt (t1, t2) -> TAlt (desugar t1, desugar t2) | o -> o let compile term = comp [] (desugar term)